From 3c1cd2338fcddc4a6c0e97b0af53eb2b2f238c4a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 15 Dec 2016 10:45:19 +0100 Subject: Removing most nf_enter in tactics. Now they are useless because all of the primitives are (should?) be evar-insensitive. --- plugins/cc/cctac.ml | 44 +++++++++++++++++++++++--------------------- plugins/omega/coq_omega.ml | 35 +++++++++++++++++++++-------------- 2 files changed, 44 insertions(+), 35 deletions(-) (limited to 'plugins') diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 5d894c677..c9c904e35 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -182,9 +182,10 @@ let litteral_of_constr env sigma term= (* store all equalities from the context *) let make_prb gls depth additionnal_terms = + let open Tacmach.New in let env=pf_env gls in - let sigma=sig_sig gls in - let state = empty depth gls in + let sigma=project gls in + let state = empty depth {it = Proofview.Goal.goal (Proofview.Goal.assume gls); sigma } in let pos_hyps = ref [] in let neg_hyps =ref [] in List.iter @@ -196,7 +197,7 @@ let make_prb gls depth additionnal_terms = let id = NamedDecl.get_id decl in begin let cid=Constr.mkVar id in - match litteral_of_constr env sigma (EConstr.of_constr (NamedDecl.get_type decl)) with + match litteral_of_constr env sigma (NamedDecl.get_type decl) with `Eq (t,a,b) -> add_equality state cid a b | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b | `Other ph -> @@ -213,7 +214,7 @@ let make_prb gls depth additionnal_terms = neg_hyps:=(cid,nh):: !neg_hyps | `Rule patts -> add_quant state id true patts | `Nrule patts -> add_quant state id false patts - end) (Environ.named_context_of_val (Goal.V82.nf_hyps gls.sigma gls.it)); + end) (Proofview.Goal.hyps gls); begin match atom_of_constr env sigma (pf_concl gls) with `Eq (t,a,b) -> add_disequality state Goal a b @@ -227,6 +228,7 @@ let make_prb gls depth additionnal_terms = (* indhyps builds the array of arrays of constructor hyps for (ind largs) *) let build_projection intype (cstr:pconstructor) special default gls= + let open Tacmach.New in let ci= (snd(fst cstr)) in let body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in let id=pf_get_new_id (Id.of_string "t") gls in @@ -266,7 +268,7 @@ let refresh_universes ty k = let constr_of_term c = EConstr.of_constr (constr_of_term c) let rec proof_tac p : unit Proofview.tactic = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let type_of t = Tacmach.New.pf_unsafe_type_of gl t in try (* type_of can raise exceptions *) match p.p_rule with @@ -296,7 +298,7 @@ let rec proof_tac p : unit Proofview.tactic = refresh_universes (type_of tf1) (fun typf -> refresh_universes (type_of tx1) (fun typx -> refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx -> - let id = Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) gl in + let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in let lemma1 = app_global _f_equal [|typf;typfx;appx1;tf1;tf2;_M 1|] in let lemma2 = app_global _f_equal [|typx;typfx;tf2;tx1;tx2;_M 1|] in @@ -322,7 +324,7 @@ let rec proof_tac p : unit Proofview.tactic = refresh_universes (type_of ti) (fun intype -> refresh_universes (type_of default) (fun outtype -> let proj = - Tacmach.New.of_old (build_projection intype cstr special default) gl + build_projection intype cstr special default gl in let injt= app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in @@ -331,9 +333,9 @@ let rec proof_tac p : unit Proofview.tactic = end } let refute_tac c t1 t2 p = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in - let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in + let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in let false_t=mkApp (c,[|mkVar hid|]) in let k intype = let neweq= new_app_global _eq [|intype;tt1;tt2|] in @@ -347,12 +349,12 @@ let refine_exact_check c gl = Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl let convert_to_goal_tac c t1 t2 p = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let k sort = let neweq= new_app_global _eq [|sort;tt1;tt2|] in - let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in - let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in + let e = Tacmach.New.pf_get_new_id (Id.of_string "e") gl in + let x = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in let identity=mkLambda (Name x,sort,mkRel 1) in let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in Tacticals.New.tclTHENS (neweq (assert_before (Name e))) @@ -361,9 +363,9 @@ let convert_to_goal_tac c t1 t2 p = end } let convert_to_hyp_tac c1 t1 c2 t2 p = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let tt2=constr_of_term t2 in - let h = Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) gl in + let h = Tacmach.New.pf_get_new_id (Id.of_string "H") gl in let false_t=mkApp (c2,[|mkVar h|]) in Tacticals.New.tclTHENS (assert_before (Name h) tt2) [convert_to_goal_tac c1 t1 t2 p; @@ -371,11 +373,11 @@ let convert_to_hyp_tac c1 t1 c2 t2 p = end } let discriminate_tac (cstr,u as cstru) p = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in - let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in + let xid = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in let identity = Universes.constr_of_global (Lazy.force _I) in let identity = EConstr.of_constr identity in let trivial = Universes.constr_of_global (Lazy.force _True) in @@ -385,8 +387,8 @@ let discriminate_tac (cstr,u as cstru) p = let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in let outtype = mkSort outtype in let pred = mkLambda(Name xid,outtype,mkRel 1) in - let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in - let proj = Tacmach.New.of_old (build_projection intype cstru trivial concl) gl in + let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in + let proj = build_projection intype cstru trivial concl gl in let injt=app_global _f_equal [|intype;outtype;proj;t1;t2;mkVar hid|] in let endt k = @@ -409,11 +411,11 @@ let build_term_to_complete uf meta pac = applist (mkConstructU cinfo.ci_constr, all_args) let cc_tactic depth additionnal_terms = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let sigma = Tacmach.New.project gl in Coqlib.check_required_library Coqlib.logic_module_name; let _ = debug (fun () -> Pp.str "Reading subgoal ...") in - let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in + let state = make_prb gl depth additionnal_terms in let _ = debug (fun () -> Pp.str "Problem built, solving ...") in let sol = execute true state in let _ = debug (fun () -> Pp.str "Computation completed.") in @@ -498,7 +500,7 @@ let mk_eq f c1 c2 k = end }) let f_equal = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in let cut_eq c1 c2 = diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 72aeb9066..adf926958 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -38,7 +38,7 @@ open OmegaSolver (* Added by JCF, 09/03/98 *) let elim_id id = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> simplest_elim (Tacmach.New.pf_global id gl) end } let resolve_id id gl = Proofview.V82.of_tactic (apply (pf_global gl id)) gl @@ -1391,7 +1391,10 @@ let normalize_equation sigma id flag theorem pos t t1 t2 (tactic,defs) = else (tactic,defs) +let pf_nf gl c = Tacmach.New.pf_apply Tacred.simpl gl c + let destructure_omega gl tac_def (id,c) = + let open Tacmach.New in let sigma = project gl in if String.equal (atompart_of_id id) "State" then tac_def @@ -1433,10 +1436,10 @@ let reintroduce id = open Proofview.Notations let coq_omega = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> clear_constr_tables (); let hyps_types = Tacmach.New.pf_hyps_types gl in - let destructure_omega = Tacmach.New.of_old destructure_omega gl in + let destructure_omega = destructure_omega gl in let tactic_normalisation, system = List.fold_left destructure_omega ([],[]) hyps_types in let prelude,sys = @@ -1486,7 +1489,7 @@ let coq_omega = let coq_omega = coq_omega let nat_inject = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let is_conv = Tacmach.New.pf_apply Reductionops.is_conv gl in let rec explore p t : unit Proofview.tactic = Proofview.tclEVARMAP >>= fun sigma -> @@ -1657,6 +1660,7 @@ let not_binop = function exception Undecidable let rec decidability gl t = + let open Tacmach.New in match destructurate_prop (project gl) t with | Kapp(Or,[t1;t2]) -> mkApp (Lazy.force coq_dec_or, [| t1; t2; @@ -1687,22 +1691,25 @@ let rec decidability gl t = | Kapp(True,[]) -> Lazy.force coq_dec_True | _ -> raise Undecidable +let fresh_id avoid id gl = + fresh_id_in_env avoid id (Proofview.Goal.env gl) + let onClearedName id tac = (* We cannot ensure that hyps can be cleared (because of dependencies), *) (* so renaming may be necessary *) Tacticals.New.tclTHEN (Tacticals.New.tclTRY (clear [id])) - (Proofview.Goal.nf_enter { enter = begin fun gl -> - let id = Tacmach.New.of_old (fresh_id [] id) gl in + (Proofview.Goal.enter { enter = begin fun gl -> + let id = fresh_id [] id gl in Tacticals.New.tclTHEN (introduction id) (tac id) end }) let onClearedName2 id tac = Tacticals.New.tclTHEN (Tacticals.New.tclTRY (clear [id])) - (Proofview.Goal.nf_enter { enter = begin fun gl -> - let id1 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_left")) gl in - let id2 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_right")) gl in + (Proofview.Goal.enter { enter = begin fun gl -> + let id1 = fresh_id [] (add_suffix id "_left") gl in + let id2 = fresh_id [] (add_suffix id "_right") gl in Tacticals.New.tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] end }) @@ -1712,10 +1719,10 @@ let rec is_Prop sigma c = match EConstr.kind sigma c with | _ -> false let destructure_hyps = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let type_of = Tacmach.New.pf_unsafe_type_of gl in - let decidability = Tacmach.New.of_old decidability gl in - let pf_nf = Tacmach.New.of_old pf_nf gl in + let decidability = decidability gl in + let pf_nf = pf_nf gl in let rec loop = function | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega) | decl::lit -> @@ -1854,9 +1861,9 @@ let destructure_hyps = end } let destructure_goal = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in - let decidability = Tacmach.New.of_old decidability gl in + let decidability = decidability gl in let rec loop t = Proofview.tclEVARMAP >>= fun sigma -> let prop () = Proofview.tclUNIT (destructurate_prop sigma t) in -- cgit v1.2.3