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").

3 files changed, 27 insertions, 18 deletions

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index f3c7680b0..0a9182e0b 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -344,8 +344,21 @@ let intern_typed_pattern ist p =
   (* type it, so we remember the pattern as a glob_constr only *)
   (intern_constr_gen true false ist p,dummy_pat)
 
-let intern_typed_pattern_with_occurrences ist (l,p) =
-  (l,intern_typed_pattern ist p)
+let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
+  match p with
+  | Inl r -> l,
+      (try Inl (intern_evaluable ist r)
+       with e when Logic.catchable_exception e ->
+         (* Compatibility. In practice, this means that the code above
+            is useless. Still the idea of having either an evaluable
+            ref or a pattern seems interesting, with "head" reduction
+            in case of an evaluable ref, and "strong" reduction in the
+            subterm matched when a pattern) *)
+         let r = match r with
+         | AN r -> r
+         | _ -> Qualid (loc_of_smart_reference r,qualid_of_path (path_of_global (smart_global r))) in
+         Inr (intern_typed_pattern ist (CRef(r,None))))
+  | Inr c -> l, Inr (intern_typed_pattern ist c)
 
 (* This seems fairly hacky, but it's the first way I've found to get proper
    globalization of [unfold].  --adamc *)
@@ -370,9 +383,9 @@ let intern_red_expr ist = function
   | Cbn f -> Cbn (intern_flag ist f)
   | Lazy f -> Lazy (intern_flag ist f)
   | Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l)
-  | Simpl o -> Simpl (Option.map (intern_typed_pattern_with_occurrences ist) o)
-  | CbvVm o -> CbvVm (Option.map (intern_typed_pattern_with_occurrences ist) o)
-  | CbvNative o -> CbvNative (Option.map (intern_typed_pattern_with_occurrences ist) o)
+  | Simpl o -> Simpl (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
+  | CbvVm o -> CbvVm (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
+  | CbvNative o -> CbvNative (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
   | (Red _ | Hnf | ExtraRedExpr _ as r ) -> r
 
 let intern_in_hyp_as ist lf (clear,id,ipat) =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 54fbbbe27..63eb200de 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -680,8 +680,10 @@ let interp_constr_with_occurrences ist env sigma (occs,c) =
   let (sigma,c_interp) = interp_constr ist env sigma c in
   sigma , (interp_occurrences ist occs, c_interp)
 
-let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, c) =
-  let _, p = interp_typed_pattern ist env sigma c in
+let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
+  let p = match a with
+  | Inl b -> Inl (interp_evaluable ist env sigma b)
+  | Inr c -> Inr (snd (interp_typed_pattern ist env sigma c)) in
   interp_occurrences ist occs, p
 
 let interp_constr_with_occurrences_and_name_as_list =
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 2f47b9000..5a02a53f3 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -114,17 +114,11 @@ let subst_glob_constr_or_pattern subst (c,p) =
 let subst_pattern_with_occurrences subst (l,p) =
   (l,subst_glob_constr_or_pattern subst p)
 
-let subst_redexp subst = function
-  | Unfold l -> Unfold (List.map (subst_unfold subst) l)
-  | Fold l -> Fold (List.map (subst_glob_constr subst) l)
-  | Cbv f -> Cbv (subst_flag subst f)
-  | Cbn f -> Cbn (subst_flag subst f)
-  | Lazy f -> Lazy (subst_flag subst f)
-  | Pattern l -> Pattern (List.map (subst_constr_with_occurrences subst) l)
-  | Simpl o -> Simpl (Option.map (subst_pattern_with_occurrences subst) o)
-  | CbvVm o -> CbvVm (Option.map (subst_pattern_with_occurrences subst) o)
-  | CbvNative o -> CbvNative (Option.map (subst_pattern_with_occurrences subst) o)
-  | (Red _ | Hnf | ExtraRedExpr _ as r) -> r
+let subst_redexp subst =
+  Miscops.map_red_expr_gen
+    (subst_glob_constr subst)
+    (subst_evaluable subst)
+    (subst_glob_constr_or_pattern subst)
 
 let subst_raw_may_eval subst = function
   | ConstrEval (r,c) -> ConstrEval (subst_redexp subst r,subst_glob_constr subst c)