1 files changed, 260 insertions, 0 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
new file mode 100644
index 00000000..57268a9c
--- /dev/null
+++ b/plugins/btauto/refl_btauto.ml
@@ -0,0 +1,260 @@
+
+let contrib_name = "btauto"
+
+let init_constant dir s =
+  let find_constant contrib dir s =
+    Universes.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 () -> Globnames.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 CoqPositive = struct
+  let path = ["Numbers"; "BinNums"]
+  let typ = get_constant path "positive"
+  let _xH = get_constant path "xH"
+  let _xO = get_constant path "xO"
+  let _xI = get_constant path "xI"
+
+  (* A coq nat from an int *)
+  let rec of_int n =
+    if n <= 1 then Lazy.force _xH
+    else
+      let ans = of_int (n / 2) in
+      if n mod 2 = 0 then lapp _xO [|ans|]
+      else lapp _xI [|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 1)
+
+  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 -> Int.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 [|CoqPositive.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 (Genredexpr.CbvVm None) 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 e when Errors.noncritical e -> (str "Not a tautology")
+    in
+    Tacticals.tclFAIL 0 msg gl
+
+  let try_unification env =
+    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
+      match t with
+      | Term.App (c, [|typ; p; _|]) when c === eq ->
+      (* should be an equality [@eq poly ?p (Cst false)] *)
+          let tac = Tacticals.New.tclORELSE0 Tactics.reflexivity (Proofview.V82.tactic (print_counterexample p env)) in
+          tac
+      | _ ->
+          let msg = str "Btauto: Internal error" in
+          Tacticals.New.tclFAIL 0 msg
+    end
+
+  let tac =
+    Proofview.Goal.nf_enter begin fun gl ->
+      let concl = Proofview.Goal.concl gl in
+      let eq = Lazy.force eq in
+      let bool = Lazy.force Bool.typ 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.New.tclTHENLIST [
+            Tactics.change_concl changed_gl;
+            Tactics.apply (Lazy.force soundness);
+            Proofview.V82.tactic (Tactics.normalise_vm_in_concl);
+            try_unification env
+          ]
+      | _ ->
+          let msg = str "Cannot recognize a boolean equality" in
+          Tacticals.New.tclFAIL 0 msg
+    end
+
+end