From 5143129baac805d3a49ac3ee9f3344c7a447634f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 30 Oct 2016 17:53:07 +0100 Subject: Termops API using EConstr. --- plugins/firstorder/rules.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/firstorder/rules.ml') diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 7ffc78928d..1d107e9afe 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -38,8 +38,8 @@ let wrap n b continue seq gls= []->anomaly (Pp.str "Not the expected number of hyps") | nd::q-> let id = NamedDecl.get_id nd in - if occur_var env id (pf_concl gls) || - List.exists (occur_var_in_decl env id) ctx then + if occur_var env (project gls) id (EConstr.of_constr (pf_concl gls)) || + List.exists (occur_var_in_decl env (project gls) id) ctx then (aux (i-1) q (nd::ctx)) else add_formula Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) gls in -- cgit v1.2.3 From 485bbfbed4ae4a28119c4e42c5e40fd77abf4f8a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 13 Nov 2016 20:38:41 +0100 Subject: Tactics API using EConstr. --- plugins/firstorder/rules.ml | 27 ++++++++++++++------------- 1 file changed, 14 insertions(+), 13 deletions(-) (limited to 'plugins/firstorder/rules.ml') diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 1d107e9afe..bed7a727f7 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -59,7 +59,7 @@ let clear_global=function (* connection rules *) let axiom_tac t seq= - try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check c)) + try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check (EConstr.of_constr c))) with Not_found->tclFAIL 0 (Pp.str "No axiom link") let ll_atom_tac a backtrack id continue seq= @@ -68,7 +68,7 @@ let ll_atom_tac a backtrack id continue seq= tclTHENLIST [pf_constr_of_global (find_left a seq) (fun left -> pf_constr_of_global id (fun id -> - Proofview.V82.of_tactic (generalize [mkApp(id, [|left|])]))); + Proofview.V82.of_tactic (generalize [EConstr.of_constr (mkApp(id, [|left|]))]))); clear_global id; Proofview.V82.of_tactic intro] with Not_found->tclFAIL 0 (Pp.str "No link")) @@ -95,7 +95,7 @@ let left_and_tac ind backtrack id continue seq gls= let n=(construct_nhyps ind gls).(0) in tclIFTHENELSE (tclTHENLIST - [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim); + [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim)); clear_global id; tclDO n (Proofview.V82.of_tactic intro)]) (wrap n false continue seq) @@ -109,12 +109,12 @@ let left_or_tac ind backtrack id continue seq gls= tclDO n (Proofview.V82.of_tactic intro); wrap n false continue seq] in tclIFTHENSVELSE - (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)) + (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim))) (Array.map f v) backtrack gls let left_false_tac id= - Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim) + Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim)) (* left arrow connective rules *) @@ -131,7 +131,7 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl= let vars=Array.init p (fun j->mkRel (p-j)) in let capply=mkApp ((lift p cstr),vars) in let head=mkApp ((lift p idc),[|capply|]) in - it_mkLambda_or_LetIn head rc in + EConstr.of_constr (it_mkLambda_or_LetIn head rc) in let lp=Array.length rcs in let newhyps idc =List.init lp (myterm idc) in tclIFTHENELSE @@ -143,16 +143,16 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl= let ll_arrow_tac a b c backtrack id continue seq= let cc=mkProd(Anonymous,a,(lift 1 b)) in - let d idc =mkLambda (Anonymous,b, - mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in + let d idc =EConstr.of_constr (mkLambda (Anonymous,b, + mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|]))) in tclORELSE - (tclTHENS (Proofview.V82.of_tactic (cut c)) + (tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr c))) [tclTHENLIST [Proofview.V82.of_tactic introf; clear_global id; wrap 1 false continue seq]; - tclTHENS (Proofview.V82.of_tactic (cut cc)) - [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check c)); + tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr cc))) + [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check (EConstr.of_constr c))); tclTHENLIST [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize [d idc])); clear_global id; @@ -177,7 +177,7 @@ let forall_tac backtrack continue seq= let left_exists_tac ind backtrack id continue seq gls= let n=(construct_nhyps ind gls).(0) in tclIFTHENELSE - (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)) + (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim))) (tclTHENLIST [clear_global id; tclDO n (Proofview.V82.of_tactic intro); (wrap (n-1) false continue seq)]) @@ -186,13 +186,14 @@ let left_exists_tac ind backtrack id continue seq gls= let ll_forall_tac prod backtrack id continue seq= tclORELSE - (tclTHENS (Proofview.V82.of_tactic (cut prod)) + (tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr prod))) [tclTHENLIST [Proofview.V82.of_tactic intro; pf_constr_of_global id (fun idc -> (fun gls-> let id0=pf_nth_hyp_id gls 1 in let term=mkApp(idc,[|mkVar(id0)|]) in + let term = EConstr.of_constr term in tclTHEN (Proofview.V82.of_tactic (generalize [term])) (Proofview.V82.of_tactic (clear [id0])) gls)); clear_global id; Proofview.V82.of_tactic intro; -- cgit v1.2.3 From 02dd160233adc784eac732d97a88356d1f0eaf9b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Nov 2016 18:34:53 +0100 Subject: Removing various compatibility layers of tactics. --- plugins/firstorder/rules.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/firstorder/rules.ml') diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index bed7a727f7..38dae0b204 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -38,14 +38,14 @@ let wrap n b continue seq gls= []->anomaly (Pp.str "Not the expected number of hyps") | nd::q-> let id = NamedDecl.get_id nd in - if occur_var env (project gls) id (EConstr.of_constr (pf_concl gls)) || + if occur_var env (project gls) id (pf_concl gls) || List.exists (occur_var_in_decl env (project gls) id) ctx then (aux (i-1) q (nd::ctx)) else add_formula Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) gls in let seq1=aux n nc [] in let seq2=if b then - add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in + add_formula Concl dummy_id (EConstr.Unsafe.to_constr (pf_concl gls)) seq1 gls else seq1 in continue seq2 gls let basename_of_global=function -- cgit v1.2.3 From 01849481fbabc3a3fa6c483e703996b01e37fca5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 01:25:11 +0100 Subject: Removing compatibility layers from Tacticals --- plugins/firstorder/rules.ml | 32 +++++++++++++++++++------------- 1 file changed, 19 insertions(+), 13 deletions(-) (limited to 'plugins/firstorder/rules.ml') diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 38dae0b204..36bd91ab6a 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -59,16 +59,17 @@ let clear_global=function (* connection rules *) let axiom_tac t seq= - try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check (EConstr.of_constr c))) + try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check c)) with Not_found->tclFAIL 0 (Pp.str "No axiom link") let ll_atom_tac a backtrack id continue seq= + let open EConstr in tclIFTHENELSE (try tclTHENLIST [pf_constr_of_global (find_left a seq) (fun left -> pf_constr_of_global id (fun id -> - Proofview.V82.of_tactic (generalize [EConstr.of_constr (mkApp(id, [|left|]))]))); + Proofview.V82.of_tactic (generalize [(mkApp(id, [|left|]))]))); clear_global id; Proofview.V82.of_tactic intro] with Not_found->tclFAIL 0 (Pp.str "No link")) @@ -95,7 +96,7 @@ let left_and_tac ind backtrack id continue seq gls= let n=(construct_nhyps ind gls).(0) in tclIFTHENELSE (tclTHENLIST - [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim)); + [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim); clear_global id; tclDO n (Proofview.V82.of_tactic intro)]) (wrap n false continue seq) @@ -109,12 +110,12 @@ let left_or_tac ind backtrack id continue seq gls= tclDO n (Proofview.V82.of_tactic intro); wrap n false continue seq] in tclIFTHENSVELSE - (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim))) + (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)) (Array.map f v) backtrack gls let left_false_tac id= - Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim)) + Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim) (* left arrow connective rules *) @@ -133,7 +134,7 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl= let head=mkApp ((lift p idc),[|capply|]) in EConstr.of_constr (it_mkLambda_or_LetIn head rc) in let lp=Array.length rcs in - let newhyps idc =List.init lp (myterm idc) in + let newhyps idc =List.init lp (myterm (EConstr.Unsafe.to_constr idc)) in tclIFTHENELSE (tclTHENLIST [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize (newhyps idc))); @@ -142,17 +143,22 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl= (wrap lp false continue seq) backtrack gl let ll_arrow_tac a b c backtrack id continue seq= + let open EConstr in + let open Vars in + let a = EConstr.of_constr a in + let b = EConstr.of_constr b in + let c = EConstr.of_constr c in let cc=mkProd(Anonymous,a,(lift 1 b)) in - let d idc =EConstr.of_constr (mkLambda (Anonymous,b, - mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|]))) in + let d idc = mkLambda (Anonymous,b, + mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in tclORELSE - (tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr c))) + (tclTHENS (Proofview.V82.of_tactic (cut c)) [tclTHENLIST [Proofview.V82.of_tactic introf; clear_global id; wrap 1 false continue seq]; - tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr cc))) - [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check (EConstr.of_constr c))); + tclTHENS (Proofview.V82.of_tactic (cut cc)) + [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check c)); tclTHENLIST [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize [d idc])); clear_global id; @@ -177,7 +183,7 @@ let forall_tac backtrack continue seq= let left_exists_tac ind backtrack id continue seq gls= let n=(construct_nhyps ind gls).(0) in tclIFTHENELSE - (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim))) + (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)) (tclTHENLIST [clear_global id; tclDO n (Proofview.V82.of_tactic intro); (wrap (n-1) false continue seq)]) @@ -191,9 +197,9 @@ let ll_forall_tac prod backtrack id continue seq= [Proofview.V82.of_tactic intro; pf_constr_of_global id (fun idc -> (fun gls-> + let open EConstr in let id0=pf_nth_hyp_id gls 1 in let term=mkApp(idc,[|mkVar(id0)|]) in - let term = EConstr.of_constr term in tclTHEN (Proofview.V82.of_tactic (generalize [term])) (Proofview.V82.of_tactic (clear [id0])) gls)); clear_global id; Proofview.V82.of_tactic intro; -- cgit v1.2.3 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/firstorder/rules.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/firstorder/rules.ml') diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 36bd91ab6a..a60fd4d8f1 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -42,7 +42,7 @@ let wrap n b continue seq gls= List.exists (occur_var_in_decl env (project gls) id) ctx then (aux (i-1) q (nd::ctx)) else - add_formula Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) gls in + add_formula Hyp (VarRef id) (EConstr.Unsafe.to_constr (NamedDecl.get_type nd)) (aux (i-1) q (nd::ctx)) gls in let seq1=aux n nc [] in let seq2=if b then add_formula Concl dummy_id (EConstr.Unsafe.to_constr (pf_concl gls)) seq1 gls else seq1 in -- cgit v1.2.3