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, 12 insertions, 6 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 3b01e988af..324efe53e9 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -254,6 +254,12 @@ GEXTEND Gram
   pattern_occ:
     [ [ c = constr; nl = occs -> (nl,c) ] ]
   ;
+  ref_or_pattern_occ:
+    (* If a string, it is interpreted as a ref
+       (anyway a Coq string does not reduce) *)
+    [ [ c = smart_global; nl = occs -> nl,Inl c
+      | c = constr; nl = occs -> nl,Inr c ] ]
+  ;
   unfold_occ:
     [ [ c = smart_global; nl = occs -> (nl,c) ] ]
   ;
@@ -336,13 +342,13 @@ GEXTEND Gram
   red_tactic:
     [ [ IDENT "red" -> Red false
       | IDENT "hnf" -> Hnf
-      | IDENT "simpl"; po = OPT pattern_occ -> Simpl po
+      | IDENT "simpl"; po = OPT ref_or_pattern_occ -> Simpl po
       | IDENT "cbv"; s = strategy_flag -> Cbv s
       | IDENT "cbn"; s = strategy_flag -> Cbn s
       | IDENT "lazy"; s = strategy_flag -> Lazy s
       | IDENT "compute"; delta = delta_flag -> Cbv (all_with delta)
-      | IDENT "vm_compute"; po = OPT pattern_occ -> CbvVm po
-      | IDENT "native_compute"; po = OPT pattern_occ -> CbvNative po
+      | IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> CbvVm po
+      | IDENT "native_compute"; po = OPT ref_or_pattern_occ -> CbvNative po
       | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
       | IDENT "fold"; cl = LIST1 constr -> Fold cl
       | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl ] ]
@@ -351,13 +357,13 @@ GEXTEND Gram
   red_expr:
     [ [ IDENT "red" -> Red false
       | IDENT "hnf" -> Hnf
-      | IDENT "simpl"; po = OPT pattern_occ -> Simpl po
+      | IDENT "simpl"; po = OPT ref_or_pattern_occ -> Simpl po
       | IDENT "cbv"; s = strategy_flag -> Cbv s
       | IDENT "cbn"; s = strategy_flag -> Cbn s
       | IDENT "lazy"; s = strategy_flag -> Lazy s
       | IDENT "compute"; delta = delta_flag -> Cbv (all_with delta)
-      | IDENT "vm_compute"; po = OPT pattern_occ -> CbvVm po
-      | IDENT "native_compute"; po = OPT pattern_occ -> CbvNative po
+      | IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> CbvVm po
+      | IDENT "native_compute"; po = OPT ref_or_pattern_occ -> CbvNative po
       | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
       | IDENT "fold"; cl = LIST1 constr -> Fold cl
       | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl