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/btauto/refl_btauto.ml | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) (limited to 'plugins/btauto') diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 2c5b108e55..3ba5da149a 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -14,8 +14,8 @@ let get_inductive dir s = let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in Lazy.from_fun (fun () -> Globnames.destIndRef (glob_ref ())) -let decomp_term (c : Term.constr) = - Term.kind_of_term (Termops.strip_outer_cast c) +let decomp_term sigma (c : Term.constr) = + Term.kind_of_term (Termops.strip_outer_cast sigma (EConstr.of_constr c)) let lapp c v = Term.mkApp (Lazy.force c, v) @@ -105,7 +105,7 @@ module Bool = struct | Negb of t | Ifb of t * t * t - let quote (env : Env.t) (c : Term.constr) : t = + let quote (env : Env.t) sigma (c : Term.constr) : t = let trueb = Lazy.force trueb in let falseb = Lazy.force falseb in let andb = Lazy.force andb in @@ -113,7 +113,7 @@ module Bool = struct let xorb = Lazy.force xorb in let negb = Lazy.force negb in - let rec aux c = match decomp_term c with + let rec aux c = match decomp_term sigma c with | Term.App (head, args) -> if head === andb && Array.length args = 2 then Andb (aux args.(0), aux args.(1)) @@ -181,7 +181,7 @@ module Btauto = struct let var = lapp witness [|p|] in (* Compute an assignment that dissatisfies the goal *) let _, var = Tacmach.pf_reduction_of_red_expr gl (Genredexpr.CbvVm None) var in - let rec to_list l = match decomp_term l with + let rec to_list l = match decomp_term (Tacmach.project gl) l with | Term.App (c, _) when c === (Lazy.force CoqList._nil) -> [] | Term.App (c, [|_; h; t|]) @@ -220,7 +220,7 @@ module Btauto = struct Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let eq = Lazy.force eq in - let t = decomp_term concl in + let t = decomp_term (Tacmach.New.project gl) concl in match t with | Term.App (c, [|typ; p; _|]) when c === eq -> (* should be an equality [@eq poly ?p (Cst false)] *) @@ -234,15 +234,16 @@ module Btauto = struct let tac = Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in + let sigma = Tacmach.New.project gl in let eq = Lazy.force eq in let bool = Lazy.force Bool.typ in - let t = decomp_term concl in + let t = decomp_term sigma concl in match t with | Term.App (c, [|typ; tl; tr|]) when typ === bool && c === eq -> let env = Env.empty () in - let fl = Bool.quote env tl in - let fr = Bool.quote env tr in + let fl = Bool.quote env sigma tl in + let fr = Bool.quote env sigma tr in let env = Env.to_list env in let fl = reify env fl in let fr = reify env fr in -- cgit v1.2.3 From cbea91d815f134d63d02d8fb1bd78ed97db28cd1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 19:52:48 +0100 Subject: Tacmach API using EConstr. --- plugins/btauto/refl_btauto.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'plugins/btauto') diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 3ba5da149a..1e49d8cad9 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -179,6 +179,7 @@ module Btauto = struct let print_counterexample p env gl = let var = lapp witness [|p|] in + let var = EConstr.of_constr var in (* Compute an assignment that dissatisfies the goal *) let _, var = Tacmach.pf_reduction_of_red_expr gl (Genredexpr.CbvVm None) var in let rec to_list l = match decomp_term (Tacmach.project gl) l with -- 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/btauto/refl_btauto.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'plugins/btauto') diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 1e49d8cad9..27398cf65a 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -249,9 +249,10 @@ module Btauto = struct let fl = reify env fl in let fr = reify env fr in let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in + let changed_gl = EConstr.of_constr changed_gl in Tacticals.New.tclTHENLIST [ Tactics.change_concl changed_gl; - Tactics.apply (Lazy.force soundness); + Tactics.apply (EConstr.of_constr (Lazy.force soundness)); Tactics.normalise_vm_in_concl; try_unification env ] -- 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/btauto/refl_btauto.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/btauto') diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 27398cf65a..4d2859fb07 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -15,7 +15,7 @@ let get_inductive dir s = Lazy.from_fun (fun () -> Globnames.destIndRef (glob_ref ())) let decomp_term sigma (c : Term.constr) = - Term.kind_of_term (Termops.strip_outer_cast sigma (EConstr.of_constr c)) + Term.kind_of_term (EConstr.Unsafe.to_constr (Termops.strip_outer_cast sigma (EConstr.of_constr c))) let lapp c v = Term.mkApp (Lazy.force c, v) -- 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/btauto/refl_btauto.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'plugins/btauto') diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 4d2859fb07..93bd88fe4b 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -221,6 +221,7 @@ module Btauto = struct Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let eq = Lazy.force eq in + let concl = EConstr.Unsafe.to_constr concl in let t = decomp_term (Tacmach.New.project gl) concl in match t with | Term.App (c, [|typ; p; _|]) when c === eq -> @@ -235,6 +236,7 @@ module Btauto = struct let tac = Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in + let concl = EConstr.Unsafe.to_constr concl in let sigma = Tacmach.New.project gl in let eq = Lazy.force eq in let bool = Lazy.force Bool.typ in -- cgit v1.2.3 From 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 21 Nov 2016 12:13:05 +0100 Subject: Reductionops now return EConstrs. --- plugins/btauto/refl_btauto.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'plugins/btauto') diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 93bd88fe4b..a0b04ce3b5 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -182,6 +182,7 @@ module Btauto = struct let var = EConstr.of_constr var in (* Compute an assignment that dissatisfies the goal *) let _, var = Tacmach.pf_reduction_of_red_expr gl (Genredexpr.CbvVm None) var in + let var = EConstr.Unsafe.to_constr var in let rec to_list l = match decomp_term (Tacmach.project gl) l with | Term.App (c, _) when c === (Lazy.force CoqList._nil) -> [] -- cgit v1.2.3