From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 16:18:47 +0100 Subject: Definining EConstr-based contexts. This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr. --- plugins/rtauto/refl_tauto.ml | 28 +++++++++++++++------------- plugins/rtauto/refl_tauto.mli | 6 +++--- 2 files changed, 18 insertions(+), 16 deletions(-) (limited to 'plugins/rtauto') diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 475380512..adb11f4f8 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -66,19 +66,18 @@ let l_E_Or = lazy (constant "E_Or") let l_D_Or = lazy (constant "D_Or") -let special_whd gl= - let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in - (fun t -> CClosure.whd_val infos (CClosure.inject t)) +let special_whd gl c = + Reductionops.clos_whd_flags CClosure.all (pf_env gl) (Tacmach.project gl) c -let special_nf gl= - let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in - (fun t -> CClosure.norm_val infos (CClosure.inject t)) +let special_nf gl c = + Reductionops.clos_norm_flags CClosure.betaiotazeta (pf_env gl) (Tacmach.project gl) c type atom_env= {mutable next:int; mutable env:(constr*int) list} let make_atom atom_env term= + let term = EConstr.Unsafe.to_constr term in try let (_,i)= List.find (fun (t,_)-> eq_constr term t) atom_env.env @@ -90,13 +89,17 @@ let make_atom atom_env term= Atom i let rec make_form atom_env gls term = + let open EConstr in + let open Vars in let normalize=special_nf gls in let cciterm=special_whd gls term in - match kind_of_term cciterm with + let sigma = Tacmach.project gls in + let inj = EConstr.Unsafe.to_constr in + match EConstr.kind sigma cciterm with Prod(_,a,b) -> - if EConstr.Vars.noccurn (Tacmach.project gls) 1 (EConstr.of_constr b) && + if noccurn sigma 1 b && Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) (EConstr.of_constr a) == InProp + (pf_env gls) sigma a == InProp then let fa=make_form atom_env gls a in let fb=make_form atom_env gls b in @@ -113,7 +116,7 @@ let rec make_form atom_env gls term = | App(hd,argv) when Int.equal (Array.length argv) 2 -> begin try - let ind, _ = destInd hd in + let ind, _ = destInd sigma hd in if Names.eq_ind ind (fst (Lazy.force li_and)) then let fa=make_form atom_env gls argv.(0) in let fb=make_form atom_env gls argv.(1) in @@ -134,9 +137,9 @@ let rec make_hyps atom_env gls lenv = function | LocalAssum (id,typ)::rest -> let hrec= make_hyps atom_env gls (typ::lenv) rest in - if List.exists (fun c -> Termops.local_occur_var Evd.empty (** FIXME *) id (EConstr.of_constr c)) lenv || + if List.exists (fun c -> Termops.local_occur_var Evd.empty (** FIXME *) id c) lenv || (Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) (EConstr.of_constr typ) != InProp) + (pf_env gls) (Tacmach.project gls) typ != InProp) then hrec else @@ -264,7 +267,6 @@ let rtauto_tac gls= if Retyping.get_sort_family_of (pf_env gls) (Tacmach.project gls) gl != InProp then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in - let gl = EConstr.Unsafe.to_constr gl in let glf=make_form gamma gls gl in let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in let formula= diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index 9a14ac6c7..092552364 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -12,13 +12,13 @@ type atom_env= mutable env:(Term.constr*int) list} val make_form : atom_env -> - Proof_type.goal Tacmach.sigma -> Term.types -> Proof_search.form + Proof_type.goal Tacmach.sigma -> EConstr.types -> Proof_search.form val make_hyps : atom_env -> Proof_type.goal Tacmach.sigma -> - Term.types list -> - Context.Named.t -> + EConstr.types list -> + EConstr.named_context -> (Names.Id.t * Proof_search.form) list val rtauto_tac : Proof_type.tactic -- cgit v1.2.3