From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- plugins/btauto/refl_btauto.ml | 59 +++++++++++++++++++++---------------------- 1 file changed, 29 insertions(+), 30 deletions(-) (limited to 'plugins/btauto/refl_btauto.ml') diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 6e8b2eb0..a09abfa1 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -1,5 +1,3 @@ -open Proofview.Notations - let contrib_name = "btauto" let init_constant dir s = @@ -8,18 +6,18 @@ let init_constant dir s = in find_constant contrib_name dir s -let get_constant dir s = lazy (Coqlib.gen_constant contrib_name dir s) +let get_constant dir s = lazy (Universes.constr_of_global @@ Coqlib.coq_reference contrib_name dir s) 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 (Term.strip_outer_cast c) +let decomp_term sigma (c : Constr.t) = + Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast sigma (EConstr.of_constr c))) -let lapp c v = Term.mkApp (Lazy.force c, v) +let lapp c v = Constr.mkApp (Lazy.force c, v) -let (===) = Term.eq_constr +let (===) = Constr.equal module CoqList = struct let path = ["Init"; "Datatypes"] @@ -55,17 +53,11 @@ end module Env = struct - module ConstrHashed = struct - type t = Term.constr - let equal = Term.eq_constr - let hash = Term.hash_constr - end - - module ConstrHashtbl = Hashtbl.Make (ConstrHashed) + module ConstrHashtbl = Hashtbl.Make (Constr) type t = (int ConstrHashtbl.t * int ref) - let add (tbl, off) (t : Term.constr) = + let add (tbl, off) (t : Constr.t) = try ConstrHashtbl.find tbl t with | Not_found -> @@ -105,7 +97,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 : Constr.t) : t = let trueb = Lazy.force trueb in let falseb = Lazy.force falseb in let andb = Lazy.force andb in @@ -113,7 +105,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)) @@ -172,16 +164,18 @@ module Btauto = struct | Bool.Xorb (b1, b2) -> lapp f_xor [|convert b1; convert b2|] | Bool.Ifb (b1, b2, b3) -> lapp f_ifb [|convert b1; convert b2; convert b3|] - let convert_env env : Term.constr = + let convert_env env : Constr.t = CoqList.of_list (Lazy.force Bool.typ) env let reify env t = lapp eval [|convert_env env; convert t|] 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 l with + 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) -> [] | Term.App (c, [|_; h; t|]) @@ -206,7 +200,8 @@ module Btauto = struct let assign = List.combine env var in let map_msg (key, v) = let b = if v then str "true" else str "false" in - let term = Printer.pr_constr key in + let sigma, env = Pfedit.get_current_context () in + let term = Printer.pr_constr_env env sigma key in term ++ spc () ++ str ":=" ++ spc () ++ b in let assign = List.map map_msg assign in @@ -217,10 +212,11 @@ module Btauto = struct Tacticals.tclFAIL 0 msg gl let try_unification env = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in let eq = Lazy.force eq in - let t = decomp_term concl 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 -> (* should be an equality [@eq poly ?p (Cst false)] *) @@ -229,33 +225,36 @@ module Btauto = struct | _ -> let msg = str "Btauto: Internal error" in Tacticals.New.tclFAIL 0 msg - end } + end let tac = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_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 - 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 - let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in + let changed_gl = Constr.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 ] | _ -> let msg = str "Cannot recognize a boolean equality" in Tacticals.New.tclFAIL 0 msg - end } + end end -- cgit v1.2.3