From 84a655b14bfc886447da9abc5cf141ab87ae4bd7 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 7 Dec 2017 22:27:13 +0100 Subject: Remove deprecated option Dependent Propositions Eliminiation. And a bit of code simplification. --- tactics/tactics.ml | 28 ++++++---------------------- 1 file changed, 6 insertions(+), 22 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e072bd95f..cc5593f3f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -59,20 +59,6 @@ let typ_of env sigma c = open Goptions -(* Option for 8.2 compatibility *) -let dependent_propositions_elimination = ref true - -let use_dependent_propositions_elimination () = - !dependent_propositions_elimination - -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "dependent-propositions-elimination tactic"; - optkey = ["Dependent";"Propositions";"Elimination"]; - optread = (fun () -> !dependent_propositions_elimination) ; - optwrite = (fun b -> dependent_propositions_elimination := b) } - let _ = declare_bool_option { optdepr = true; (* remove in 8.8 *) @@ -4141,8 +4127,7 @@ let guess_elim isrec dep s hyp0 gl = let env = Tacmach.New.pf_env gl in let sigma = Tacmach.New.project gl in let u = EInstance.kind (Tacmach.New.project gl) u in - if use_dependent_propositions_elimination () && dep = Some true - then + if dep then let (sigma, ind) = build_case_analysis_scheme env sigma (mind, u) true s in let ind = EConstr.of_constr ind in (sigma, ind) @@ -4174,11 +4159,10 @@ let find_induction_type isrec elim hyp0 gl = match elim with | None -> let sort = Tacticals.New.elimination_sort_of_goal gl in - let _, (elimc,elimt),_ = - guess_elim isrec None sort hyp0 gl in - let scheme = compute_elim_sig sigma ~elimc elimt in - (* We drop the scheme waiting to know if it is dependent *) - scheme, ElimOver (isrec,hyp0) + let _, (elimc,elimt),_ = guess_elim isrec false sort hyp0 gl in + let scheme = compute_elim_sig sigma ~elimc elimt in + (* We drop the scheme waiting to know if it is dependent *) + scheme, ElimOver (isrec,hyp0) | Some e -> let evd, (elimc,elimt),ind_guess = given_elim hyp0 e gl in let scheme = compute_elim_sig sigma ~elimc elimt in @@ -4209,7 +4193,7 @@ let get_eliminator elim dep s gl = | ElimUsing (elim,indsign) -> Tacmach.New.project gl, (* bugged, should be computed *) true, elim, indsign | ElimOver (isrec,id) -> - let evd, (elimc,elimt),_ as elims = guess_elim isrec (Some dep) s id gl in + let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in let _, (l, s) = compute_elim_signature elims id in let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (Tacmach.New.project gl) (RelDecl.get_type d))) (List.rev s.branches) -- cgit v1.2.3 From ac2b757a7835672ba494bf42244b5d393e8db089 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 7 Dec 2017 22:27:19 +0100 Subject: Remove deprecated option Tactic Compat Context. And some code simplification. --- API/API.mli | 7 ++-- lib/flags.ml | 1 - lib/flags.mli | 4 --- plugins/ltac/g_ltac.ml4 | 5 ++- plugins/ltac/pptactic.ml | 6 ++-- plugins/ltac/tacexpr.mli | 2 +- plugins/ltac/tacintern.ml | 4 +-- plugins/ltac/tacinterp.ml | 2 +- plugins/ltac/tacsubst.ml | 2 +- plugins/ltac/tactic_matching.ml | 4 +-- pretyping/constr_matching.ml | 77 ++++++++++++----------------------------- pretyping/constr_matching.mli | 12 ++----- tactics/tactics.ml | 8 ----- 13 files changed, 39 insertions(+), 95 deletions(-) (limited to 'tactics') diff --git a/API/API.mli b/API/API.mli index 3ed008ff5..3f52ac62b 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3853,10 +3853,9 @@ sig type matching_result = { m_sub : bound_ident_map * Ltac_pretype.patvar_map; m_ctx : EConstr.constr } - val match_subterm_gen : Environ.env -> Evd.evar_map -> - bool -> - binding_bound_vars * Pattern.constr_pattern -> EConstr.constr -> - matching_result IStream.t + val match_subterm : Environ.env -> Evd.evar_map -> + binding_bound_vars * Pattern.constr_pattern -> EConstr.constr -> + matching_result IStream.t val matches : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> Ltac_pretype.patvar_map end diff --git a/lib/flags.ml b/lib/flags.ml index ddc8f8482..5079b4b01 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -200,7 +200,6 @@ let native_compiler = ref false (* Print the mod uid associated to a vo file by the native compiler *) let print_mod_uid = ref false -let tactic_context_compat = ref false let profile_ltac = ref false let profile_ltac_cutoff = ref 2.0 diff --git a/lib/flags.mli b/lib/flags.mli index c4afb8318..8825390e6 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -160,10 +160,6 @@ val native_compiler : bool ref (** Print the mod uid associated to a vo file by the native compiler *) val print_mod_uid : bool ref -val tactic_context_compat : bool ref -(** Set to [true] to trigger the compatibility bugged context matching (old - context vs. appcontext) is set. *) - val profile_ltac : bool ref val profile_ltac_cutoff : float ref diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 8b9eb3983..872bea612 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -242,12 +242,11 @@ GEXTEND Gram match_pattern: [ [ IDENT "context"; oid = OPT Constr.ident; "["; pc = Constr.lconstr_pattern; "]" -> - let mode = not (!Flags.tactic_context_compat) in - Subterm (mode, oid, pc) + Subterm (oid, pc) | IDENT "appcontext"; oid = OPT Constr.ident; "["; pc = Constr.lconstr_pattern; "]" -> warn_deprecated_appcontext ~loc:!@loc (); - Subterm (true,oid, pc) + Subterm (oid, pc) | pc = Constr.lconstr_pattern -> Term pc ] ] ; match_hyps: diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 6aa2f6f89..e5ff47356 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -526,11 +526,9 @@ let pr_goal_selector ~toplevel s = let pr_match_pattern pr_pat = function | Term a -> pr_pat a - | Subterm (b,None,a) -> - (** ppedrot: we don't make difference between [appcontext] and [context] - anymore, and the interpretation is governed by a flag instead. *) + | Subterm (None,a) -> keyword "context" ++ str" [ " ++ pr_pat a ++ str " ]" - | Subterm (b,Some id,a) -> + | Subterm (Some id,a) -> keyword "context" ++ spc () ++ pr_id id ++ str "[ " ++ pr_pat a ++ str " ]" let pr_match_hyps pr_pat = function diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 9bd3efc6b..ccd555b61 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -81,7 +81,7 @@ type 'a with_bindings_arg = clear_flag * 'a with_bindings (* Type of patterns *) type 'a match_pattern = | Term of 'a - | Subterm of bool * Id.t option * 'a + | Subterm of Id.t option * 'a (* Type of hypotheses for a Match Context rule *) type 'a match_context_hyps = diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index b16b0a7ba..ebffde441 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -428,9 +428,9 @@ let intern_hyp_location ist ((occs,id),hl) = (* Reads a pattern *) let intern_pattern ist ?(as_type=false) ltacvars = function - | Subterm (b,ido,pc) -> + | Subterm (ido,pc) -> let (metas,pc) = intern_constr_pattern ist ~as_type:false ~ltacvars pc in - ido, metas, Subterm (b,ido,pc) + ido, metas, Subterm (ido,pc) | Term pc -> let (metas,pc) = intern_constr_pattern ist ~as_type ~ltacvars pc in None, metas, Term pc diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index e0d7eca5f..d190cc2cd 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1040,7 +1040,7 @@ let eval_pattern lfun ist env sigma (bvars,(glob,_),pat as c) = (bvars,instantiate_pattern env sigma lfun pat) let read_pattern lfun ist env sigma = function - | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c) + | Subterm (ido,c) -> Subterm (ido,eval_pattern lfun ist env sigma c) | Term c -> Term (eval_pattern lfun ist env sigma c) (* Reads the hypotheses of a Match Context rule *) diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 918d1faeb..79bf3685e 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -121,7 +121,7 @@ let subst_raw_may_eval subst = function | ConstrTerm c -> ConstrTerm (subst_glob_constr subst c) let subst_match_pattern subst = function - | Subterm (b,ido,pc) -> Subterm (b,ido,(subst_glob_constr_or_pattern subst pc)) + | Subterm (ido,pc) -> Subterm (ido,(subst_glob_constr_or_pattern subst pc)) | Term pc -> Term (subst_glob_constr_or_pattern subst pc) let rec subst_match_goal_hyps subst = function diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 89b78e590..e87951dd7 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -237,7 +237,7 @@ module PatternMatching (E:StaticEnvironment) = struct return lhs with Constr_matching.PatternMatchingFailure -> fail end - | Subterm (with_app_context,id_ctxt,p) -> + | Subterm (id_ctxt,p) -> let rec map s (e, info) = { stream = fun k ctx -> match IStream.peek s with @@ -252,7 +252,7 @@ module PatternMatching (E:StaticEnvironment) = struct | Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx) } in - map (Constr_matching.match_subterm_gen E.env E.sigma with_app_context p term) imatching_error + map (Constr_matching.match_subterm E.env E.sigma p term) imatching_error (** [rule_match_term term rule] matches the term [term] with the diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 478ba73fd..ec7c3077f 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -206,7 +206,7 @@ let merge_binding sigma allow_bound_rels ctx n cT subst = in constrain sigma n c subst -let matches_core env sigma allow_partial_app allow_bound_rels +let matches_core env sigma allow_bound_rels (binding_vars,pat) c = let open EConstr in let convref ref c = @@ -260,7 +260,7 @@ let matches_core env sigma allow_partial_app allow_bound_rels | PApp (PApp (h, a1), a2), _ -> sorec ctx env subst (PApp(h,Array.append a1 a2)) t - | PApp (PMeta meta,args1), App (c2,args2) when allow_partial_app -> + | PApp (PMeta meta,args1), App (c2,args2) -> (let diff = Array.length args2 - Array.length args1 in if diff >= 0 then let args21, args22 = Array.chop diff args2 in @@ -373,14 +373,14 @@ let matches_core env sigma allow_partial_app allow_bound_rels in sorec [] env (Id.Map.empty, Id.Map.empty) pat c -let matches_core_closed env sigma allow_partial_app pat c = - let names, subst = matches_core env sigma allow_partial_app false pat c in +let matches_core_closed env sigma pat c = + let names, subst = matches_core env sigma false pat c in (names, Id.Map.map snd subst) -let extended_matches env sigma = matches_core env sigma true true +let extended_matches env sigma = matches_core env sigma true let matches env sigma pat c = - snd (matches_core_closed env sigma true (Id.Set.empty,pat) c) + snd (matches_core_closed env sigma (Id.Set.empty,pat) c) let special_meta = (-1) @@ -405,9 +405,9 @@ let matches_head env sigma pat c = matches env sigma pat head (* Tells if it is an authorized occurrence and if the instance is closed *) -let authorized_occ env sigma partial_app closed pat c mk_ctx = +let authorized_occ env sigma closed pat c mk_ctx = try - let subst = matches_core_closed env sigma partial_app pat c in + let subst = matches_core_closed env sigma pat c in if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst) then (fun next -> next ()) else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next) @@ -416,10 +416,10 @@ let authorized_occ env sigma partial_app closed pat c mk_ctx = let subargs env v = Array.map_to_list (fun c -> (env, c)) v (* Tries to match a subterm of [c] with [pat] *) -let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = +let sub_match ?(closed=true) env sigma pat c = let open EConstr in let rec aux env c mk_ctx next = - let here = authorized_occ env sigma partial_app closed pat c mk_ctx in + let here = authorized_occ env sigma closed pat c mk_ctx in let next () = match EConstr.kind sigma c with | Cast (c1,k,c2) -> let next_mk_ctx = function @@ -449,34 +449,12 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let env' = EConstr.push_rel (LocalDef (x,c1,t)) env in try_aux [(env, c1); (env', c2)] next_mk_ctx next | App (c1,lc) -> - let topdown = true in - if partial_app then - if topdown then - let lc1 = Array.sub lc 0 (Array.length lc - 1) in - let app = mkApp (c1,lc1) in - let mk_ctx = function - | [app';c] -> mk_ctx (mkApp (app',[|c|])) - | _ -> assert false in - try_aux [(env, app); (env, Array.last lc)] mk_ctx next - else - let rec aux2 app args next = - match args with - | [] -> - let mk_ctx le = - mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in - let sub = (env, c1) :: subargs env lc in - try_aux sub mk_ctx next - | arg :: args -> - let app = mkApp (app,[|arg|]) in - let next () = aux2 app args next in - let mk_ctx ce = mk_ctx (mkApp (ce, Array.of_list args)) in - aux env app mk_ctx next in - aux2 c1 (Array.to_list lc) next - else - let mk_ctx le = - mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in - let sub = (env, c1) :: subargs env lc in - try_aux sub mk_ctx next + let lc1 = Array.sub lc 0 (Array.length lc - 1) in + let app = mkApp (c1,lc1) in + let mk_ctx = function + | [app';c] -> mk_ctx (mkApp (app',[|c|])) + | _ -> assert false in + try_aux [(env, app); (env, Array.last lc)] mk_ctx next | Case (ci,hd,c1,lc) -> let next_mk_ctx = function | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) @@ -499,14 +477,11 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let sub = subargs env types @ subargs env bodies in try_aux sub next_mk_ctx next | Proj (p,c') -> - let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in - if partial_app then - try - let term = Retyping.expand_projection env sigma p c' [] in - aux env term mk_ctx next - with Retyping.RetypeError _ -> next () - else - try_aux [env, c'] next_mk_ctx next + begin try + let term = Retyping.expand_projection env sigma p c' [] in + aux env term mk_ctx next + with Retyping.RetypeError _ -> next () + end | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ -> next () in @@ -527,13 +502,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let result () = aux env c (fun x -> x) lempty in IStream.thunk result -let match_subterm env sigma pat c = sub_match env sigma (Id.Set.empty,pat) c - -let match_appsubterm env sigma pat c = - sub_match ~partial_app:true env sigma (Id.Set.empty,pat) c - -let match_subterm_gen env sigma app pat c = - sub_match ~partial_app:app env sigma pat c +let match_subterm env sigma pat c = sub_match env sigma pat c let is_matching env sigma pat c = try let _ = matches env sigma pat c in true @@ -545,5 +514,5 @@ let is_matching_head env sigma pat c = let is_matching_appsubterm ?(closed=true) env sigma pat c = let pat = (Id.Set.empty,pat) in - let results = sub_match ~partial_app:true ~closed env sigma pat c in + let results = sub_match ~closed env sigma pat c in not (IStream.is_empty results) diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 60e1c34a1..e4d9ff9e1 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -61,18 +61,10 @@ type matching_result = { m_sub : bound_ident_map * patvar_map; m_ctx : EConstr.t } -(** [match_subterm n pat c] returns the substitution and the context - corresponding to each **closed** subterm of [c] matching [pat]. *) -val match_subterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_result IStream.t - -(** [match_appsubterm pat c] returns the substitution and the context +(** [match_subterm pat c] returns the substitution and the context corresponding to each **closed** subterm of [c] matching [pat], considering application contexts as well. *) -val match_appsubterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_result IStream.t - -(** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *) -val match_subterm_gen : env -> Evd.evar_map -> - bool (** true = with app context *) -> +val match_subterm : env -> Evd.evar_map -> binding_bound_vars * constr_pattern -> constr -> matching_result IStream.t diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cc5593f3f..bf05c9b83 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -59,14 +59,6 @@ let typ_of env sigma c = open Goptions -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "trigger bugged context matching compatibility"; - optkey = ["Tactic";"Compat";"Context"]; - optread = (fun () -> !Flags.tactic_context_compat) ; - optwrite = (fun b -> Flags.tactic_context_compat := b) } - let apply_solve_class_goals = ref false let _ = -- cgit v1.2.3