From 28000ead7870114795b21b3cc819aadc4dab329d Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 13 Jan 2012 18:38:38 +0000 Subject: Added a Btauto plugin, that solves boolean tautologies. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14897 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/btauto/refl_btauto.ml | 253 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 253 insertions(+) create mode 100644 plugins/btauto/refl_btauto.ml (limited to 'plugins/btauto/refl_btauto.ml') diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml new file mode 100644 index 000000000..1d01f3e54 --- /dev/null +++ b/plugins/btauto/refl_btauto.ml @@ -0,0 +1,253 @@ +let contrib_name = "btauto" + +let init_constant dir s = + let find_constant contrib dir s = + Libnames.constr_of_global (Coqlib.find_reference contrib dir s) + in + find_constant contrib_name dir s + +let get_constant dir s = lazy (Coqlib.gen_constant contrib_name dir s) + +let get_inductive dir s = + let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in + Lazy.lazy_from_fun (fun () -> Libnames.destIndRef (glob_ref ())) + +let decomp_term (c : Term.constr) = + Term.kind_of_term (Term.strip_outer_cast c) + +let lapp c v = Term.mkApp (Lazy.force c, v) + +let (===) = Term.eq_constr + +module CoqList = struct + let path = ["Init"; "Datatypes"] + let typ = get_constant path "list" + let _nil = get_constant path "nil" + let _cons = get_constant path "cons" + + let cons ty h t = lapp _cons [|ty; h ; t|] + let nil ty = lapp _nil [|ty|] + let rec of_list ty = function + | [] -> nil ty + | t::q -> cons ty t (of_list ty q) + let type_of_list ty = lapp typ [|ty|] + +end + +module CoqNat = struct + let path = ["Init"; "Datatypes"] + let typ = get_constant path "nat" + let _S = get_constant path "S" + let _O = get_constant path "O" + + (* A coq nat from an int *) + let rec of_int n = + if n <= 0 then Lazy.force _O + else + let ans = of_int (pred n) in + lapp _S [|ans|] + +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) + + type t = (int ConstrHashtbl.t * int ref) + + let add (tbl, off) (t : Term.constr) = + try ConstrHashtbl.find tbl t + with + | Not_found -> + let i = !off in + let () = ConstrHashtbl.add tbl t i in + let () = incr off in + i + + let empty () = (ConstrHashtbl.create 16, ref 0) + + let to_list (env, _) = + (* we need to get an ordered list *) + let fold constr key accu = (key, constr) :: accu in + let l = ConstrHashtbl.fold fold env [] in + let sorted_l = List.sort (fun p1 p2 -> compare (fst p1) (fst p2)) l in + List.map snd sorted_l + +end + +module Bool = struct + + let typ = get_constant ["Init"; "Datatypes"] "bool" + let ind = get_inductive ["Init"; "Datatypes"] "bool" + let trueb = get_constant ["Init"; "Datatypes"] "true" + let falseb = get_constant ["Init"; "Datatypes"] "false" + let andb = get_constant ["Init"; "Datatypes"] "andb" + let orb = get_constant ["Init"; "Datatypes"] "orb" + let xorb = get_constant ["Init"; "Datatypes"] "xorb" + let negb = get_constant ["Init"; "Datatypes"] "negb" + + type t = + | Var of int + | Const of bool + | Andb of t * t + | Orb of t * t + | Xorb of t * t + | Negb of t + | Ifb of t * t * t + + let quote (env : Env.t) (c : Term.constr) : t = + let trueb = Lazy.force trueb in + let falseb = Lazy.force falseb in + let andb = Lazy.force andb in + let orb = Lazy.force orb in + let xorb = Lazy.force xorb in + let negb = Lazy.force negb in + + let rec aux c = match decomp_term c with + | Term.App (head, args) -> + if head === andb && Array.length args = 2 then + Andb (aux args.(0), aux args.(1)) + else if head === orb && Array.length args = 2 then + Orb (aux args.(0), aux args.(1)) + else if head === xorb && Array.length args = 2 then + Xorb (aux args.(0), aux args.(1)) + else if head === negb && Array.length args = 1 then + Negb (aux args.(0)) + else Var (Env.add env c) + | Term.Case (info, r, arg, pats) -> + let is_bool = + let i = info.Term.ci_ind in + Names.eq_ind i (Lazy.force ind) + in + if is_bool then + Ifb ((aux arg), (aux pats.(0)), (aux pats.(1))) + else + Var (Env.add env c) + | _ -> + if c === falseb then Const false + else if c === trueb then Const true + else Var (Env.add env c) + in + aux c + +end + +module Btauto = struct + + open Pp + + let eq = get_constant ["Init"; "Logic"] "eq" + + let f_var = get_constant ["btauto"; "Reflect"] "formula_var" + let f_btm = get_constant ["btauto"; "Reflect"] "formula_btm" + let f_top = get_constant ["btauto"; "Reflect"] "formula_top" + let f_cnj = get_constant ["btauto"; "Reflect"] "formula_cnj" + let f_dsj = get_constant ["btauto"; "Reflect"] "formula_dsj" + let f_neg = get_constant ["btauto"; "Reflect"] "formula_neg" + let f_xor = get_constant ["btauto"; "Reflect"] "formula_xor" + let f_ifb = get_constant ["btauto"; "Reflect"] "formula_ifb" + + let eval = get_constant ["btauto"; "Reflect"] "formula_eval" + let witness = get_constant ["btauto"; "Reflect"] "boolean_witness" + + let soundness = get_constant ["btauto"; "Reflect"] "reduce_poly_of_formula_sound_alt" + + let rec convert = function + | Bool.Var n -> lapp f_var [|CoqNat.of_int n|] + | Bool.Const true -> Lazy.force f_top + | Bool.Const false -> Lazy.force f_btm + | Bool.Andb (b1, b2) -> lapp f_cnj [|convert b1; convert b2|] + | Bool.Orb (b1, b2) -> lapp f_dsj [|convert b1; convert b2|] + | Bool.Negb b -> lapp f_neg [|convert b|] + | 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 = + 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 + (* Compute an assignment that dissatisfies the goal *) + let var = Tacmach.pf_reduction_of_red_expr gl Glob_term.CbvVm var in + let rec to_list l = match decomp_term l with + | Term.App (c, _) + when c === (Lazy.force CoqList._nil) -> [] + | Term.App (c, [|_; h; t|]) + when c === (Lazy.force CoqList._cons) -> + if h === (Lazy.force Bool.trueb) then (true :: to_list t) + else if h === (Lazy.force Bool.falseb) then (false :: to_list t) + else invalid_arg "to_list" + | _ -> invalid_arg "to_list" + in + let concat sep = function + | [] -> mt () + | h :: t -> + let rec aux = function + | [] -> mt () + | x :: t -> (sep ++ x ++ aux t) + in + h ++ aux t + in + let msg = + try + let var = to_list var in + 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 + term ++ spc () ++ str ":=" ++ spc () ++ b + in + let assign = List.map map_msg assign in + let l = str "[" ++ (concat (str ";" ++ spc ()) assign) ++ str "]" in + str "Not a tautology:" ++ spc () ++ l + with _ -> (str "Not a tautology") + in + Tacticals.tclFAIL 0 msg gl + + let try_unification env gl = + let eq = Lazy.force eq in + let concl = Tacmach.pf_concl gl in + let t = decomp_term concl in + match t with + | Term.App (c, [|typ; p; _|]) when c === eq -> + (* should be an equality [@eq poly ?p (Cst false)] *) + let tac = Tacticals.tclORELSE0 Tactics.reflexivity (print_counterexample p env) in + tac gl + | _ -> + let msg = str "Btauto: Internal error" in + Tacticals.tclFAIL 0 msg gl + + let tac gl = + let eq = Lazy.force eq in + let bool = Lazy.force Bool.typ in + let concl = Tacmach.pf_concl gl in + let t = decomp_term 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 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 + Tacticals.tclTHENLIST [ + Tactics.change_in_concl None changed_gl; + Tactics.apply (Lazy.force soundness); + Tactics.normalise_vm_in_concl; + try_unification env + ] gl + | _ -> + let msg = str "Cannot recognize a boolean equality" in + Tacticals.tclFAIL 0 msg gl + +end -- cgit v1.2.3