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, 18 insertions, 5 deletions

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index f3c7680b01..0a9182e0b9 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) =