Enforcing a stronger difference between the two syntaxes "simpl

reference" and "simpl pattern" in the code (maybe we should have
merged them instead, but I finally decided to enforce their
difference, even if some compatibility is to be preversed - the idea
is that at some time "simpl reference" would only call a weak-head
simpl (or eventually cbn), leading e.g. to reduce 2+n into S(1+n)
rather than S(S(n)) which could be useful for better using induction
hypotheses.

In the process we also implement the following:
- 'simpl "+"' is accepted to reduce all applicative subterms whose
  head symbol is written "+" (in the toplevel scope); idem for
  vm_compute and native_compute
- 'simpl reference' works even if reference has maximally inserted
  implicit arguments (this solves the "simpl fst" incompatibility)
- compatibility of ltac expressions referring to vm_compute and
  native_compute with functor application should now work (i.e.
  vm_compute and native_compute are now taken into account in
  tacsubst.ml)
- for compatibility, "simpl eq" (assuming no maximal implicit args in
  eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed.

By the way, is "mul" on nat defined optimally? "3*n" simplifies to
"n+(n+(n+0))". Are there some advantages of this compared to have it
simplified to "n+n+n" (i.e. to "(n+n)+n").

1 files changed, 7 insertions, 3 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index f90ded281f..fd46765300 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -753,10 +753,14 @@ end) = struct
 
   let pr_metaid id = str"?" ++ pr_id id
 
+  let pr_union pr1 pr2 = function
+    | Inl a -> pr1 a
+    | Inr b -> pr2 b
+
   let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function
     | Red false -> keyword "red"
     | Hnf -> keyword "hnf"
-    | Simpl o -> keyword "simpl" ++ pr_opt (pr_with_occurrences pr_pattern) o
+    | Simpl o -> keyword "simpl" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
     | Cbv f ->
       if f.rBeta && f.rIota && f.rZeta && f.rDelta && List.is_empty f.rConst then
         keyword "compute"
@@ -779,9 +783,9 @@ end) = struct
     | ExtraRedExpr s ->
       str s
     | CbvVm o ->
-      keyword "vm_compute" ++ pr_opt (pr_with_occurrences pr_pattern) o
+      keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
     | CbvNative o ->
-      keyword "native_compute" ++ pr_opt (pr_with_occurrences pr_pattern) o
+      keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
 
   let pr_may_eval test prc prlc pr2 pr3 = function
     | ConstrEval (r,c) ->