From 364decf59c14ec8a672d3c4d46fa1939ea0e52d3 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 16 Nov 2014 12:52:13 +0100 Subject: 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"). --- tactics/tacintern.ml | 23 ++++++++++++++++++----- tactics/tacinterp.ml | 6 ++++-- tactics/tacsubst.ml | 16 +++++----------- 3 files changed, 27 insertions(+), 18 deletions(-) (limited to 'tactics') 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) = diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 54fbbbe274..63eb200de8 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 2f47b90002..5a02a53f3e 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) -- cgit v1.2.3