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/fourier/fourierR.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'plugins/fourier') diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 8e193c753e..a14ec8a2ca 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -461,8 +461,9 @@ exception GoalDone let rec fourier () = Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in + let sigma = Tacmach.New.project gl in Coqlib.check_required_library ["Coq";"fourier";"Fourier"]; - let goal = Termops.strip_outer_cast concl in + let goal = Termops.strip_outer_cast sigma (EConstr.of_constr concl) in let fhyp=Id.of_string "new_hyp_for_fourier" in (* si le but est une inéquation, on introduit son contraire, et le but à prouver devient False *) -- 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/fourier/fourierR.ml | 31 ++++++++++++++++++++----------- 1 file changed, 20 insertions(+), 11 deletions(-) (limited to 'plugins/fourier') diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index a14ec8a2ca..fa64b276c8 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -281,6 +281,8 @@ let fourier_lineq lineq1 = (* Defined constants *) let get = Lazy.force +let cget = get +let eget c = EConstr.of_constr (Lazy.force c) let constant = Coqlib.gen_constant "Fourier" (* Standard library *) @@ -373,6 +375,7 @@ let rational_to_real x = (* preuve que 0 False *) let tac_zero_inf_false gl (n,d) = - if n=0 then (apply (get coq_Rnot_lt0)) + let get = eget in +if n=0 then (apply (get coq_Rnot_lt0)) else (Tacticals.New.tclTHEN (apply (get coq_Rle_not_lt)) (tac_zero_infeq_pos gl (-n,d))) @@ -408,6 +413,7 @@ let tac_zero_inf_false gl (n,d) = (* preuve que 0<=(-n)*(1/d) => False *) let tac_zero_infeq_false gl (n,d) = + let get = eget in (Tacticals.New.tclTHEN (apply (get coq_Rlt_not_le_frac_opp)) (tac_zero_inf_pos gl (-n,d))) ;; @@ -415,7 +421,8 @@ let tac_zero_infeq_false gl (n,d) = let exact = exact_check;; let tac_use h = - let tac = exact h.hname in + let get = eget in + let tac = exact (EConstr.of_constr h.hname) in match h.htype with "Rlt" -> tac |"Rle" -> tac @@ -470,6 +477,7 @@ let rec fourier () = try match (kind_of_term goal) with App (f,args) -> + let get = eget in (match (string_of_R_constr f) with "Rlt" -> (Tacticals.New.tclTHEN @@ -548,6 +556,7 @@ let rec fourier () = !t2 |] in let tc=rational_to_real cres in (* puis sa preuve *) + let get = eget in let tac1=ref (if h1.hstrict then (Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt)) [tac_use h1; @@ -584,29 +593,29 @@ let rec fourier () = then tac_zero_inf_false gl (rational_to_fraction cres) else tac_zero_infeq_false gl (rational_to_fraction cres) in - tac:=(Tacticals.New.tclTHENS (cut ineq) + tac:=(Tacticals.New.tclTHENS (cut (EConstr.of_constr ineq)) [Tacticals.New.tclTHEN (change_concl - (mkAppL [| get coq_not; ineq|] - )) + (EConstr.of_constr (mkAppL [| cget coq_not; ineq|] + ))) (Tacticals.New.tclTHEN (apply (if sres then get coq_Rnot_lt_lt else get coq_Rnot_le_le)) (Tacticals.New.tclTHENS (Equality.replace - (mkAppL [|get coq_Rminus;!t2;!t1|] + (mkAppL [|cget coq_Rminus;!t2;!t1|] ) tc) [tac2; (Tacticals.New.tclTHENS (Equality.replace - (mkApp (get coq_Rinv, - [|get coq_R1|])) - (get coq_R1)) + (mkApp (cget coq_Rinv, + [|cget coq_R1|])) + (cget coq_R1)) (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *) [Tacticals.New.tclORELSE (* TODO : Ring.polynom []*) (Proofview.tclUNIT ()) (Proofview.tclUNIT ()); - Tacticals.New.pf_constr_of_global (get coq_sym_eqT) (fun symeq -> - (Tacticals.New.tclTHEN (apply symeq) + Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) (fun symeq -> + (Tacticals.New.tclTHEN (apply (EConstr.of_constr symeq)) (apply (get coq_Rinv_1))))] ) -- cgit v1.2.3 From 3f9e56fcbf479999325a86bbdaeefd6a0be13c65 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 18 Nov 2016 20:35:01 +0100 Subject: Equality API using EConstr. --- plugins/fourier/fourierR.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'plugins/fourier') diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index fa64b276c8..dbb5cc2de7 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -600,15 +600,15 @@ let rec fourier () = (Tacticals.New.tclTHEN (apply (if sres then get coq_Rnot_lt_lt else get coq_Rnot_le_le)) (Tacticals.New.tclTHENS (Equality.replace - (mkAppL [|cget coq_Rminus;!t2;!t1|] - ) - tc) + (EConstr.of_constr (mkAppL [|cget coq_Rminus;!t2;!t1|] + )) + (EConstr.of_constr tc)) [tac2; (Tacticals.New.tclTHENS (Equality.replace - (mkApp (cget coq_Rinv, - [|cget coq_R1|])) - (cget coq_R1)) + (EConstr.of_constr (mkApp (cget coq_Rinv, + [|cget coq_R1|]))) + (get coq_R1)) (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *) [Tacticals.New.tclORELSE -- cgit v1.2.3 From d4b344acb23f19b089098b7788f37ea22bc07b81 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 20:09:26 +0100 Subject: Eliminating parts of the right-hand side compatibility layer --- plugins/fourier/fourierR.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'plugins/fourier') diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index dbb5cc2de7..f9802ee5e1 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -471,6 +471,7 @@ let rec fourier () = let sigma = Tacmach.New.project gl in Coqlib.check_required_library ["Coq";"fourier";"Fourier"]; let goal = Termops.strip_outer_cast sigma (EConstr.of_constr concl) in + let goal = EConstr.Unsafe.to_constr goal in let fhyp=Id.of_string "new_hyp_for_fourier" in (* si le but est une inéquation, on introduit son contraire, et le but à prouver devient False *) -- cgit v1.2.3 From e09f3b44bb381854b647a6d9debdeddbfc49177e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 22:16:08 +0100 Subject: Proofview.Goal primitive now return EConstrs. --- plugins/fourier/fourierR.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/fourier') diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index f9802ee5e1..bffca62231 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -470,7 +470,7 @@ let rec fourier () = let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in Coqlib.check_required_library ["Coq";"fourier";"Fourier"]; - let goal = Termops.strip_outer_cast sigma (EConstr.of_constr concl) in + let goal = Termops.strip_outer_cast sigma concl in let goal = EConstr.Unsafe.to_constr goal in let fhyp=Id.of_string "new_hyp_for_fourier" in (* si le but est une inéquation, on introduit son contraire, -- 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/fourier/fourierR.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/fourier') diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index bffca62231..ec73fccb5b 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -616,7 +616,7 @@ let rec fourier () = (* TODO : Ring.polynom []*) (Proofview.tclUNIT ()) (Proofview.tclUNIT ()); Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) (fun symeq -> - (Tacticals.New.tclTHEN (apply (EConstr.of_constr symeq)) + (Tacticals.New.tclTHEN (apply symeq) (apply (get coq_Rinv_1))))] ) -- 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/fourier/fourierR.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'plugins/fourier') diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index ec73fccb5b..e11cbc279a 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -190,6 +190,8 @@ type hineq={hname:constr; (* le nom de l'hypothèse *) exception NoIneq let ineq1_of_constr (h,t) = + let h = EConstr.Unsafe.to_constr h in + let t = EConstr.Unsafe.to_constr t in match (kind_of_term t) with | App (f,args) -> (match kind_of_term f with @@ -504,7 +506,7 @@ let rec fourier () = |_-> raise GoalDone with GoalDone -> (* les hypothèses *) - let hyps = List.map (fun (h,t)-> (mkVar h,t)) + let hyps = List.map (fun (h,t)-> (EConstr.mkVar h,t)) (list_of_sign (Proofview.Goal.hyps gl)) in let lineq =ref [] in List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq)) -- cgit v1.2.3