Tactic zchaff for 8.5

2 files changed, 20 insertions, 12 deletions

diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index c7856f3..a235859 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -272,9 +272,16 @@ module Make (Atom:ATOM) =
       | CCifb
       | CCunknown
 
+    module ConstrHash = struct
+      type t = Constr.constr
+      let equal = Constr.equal
+      let hash = Constr.hash
+    end
+    module ConstrHashtbl = Hashtbl.Make(ConstrHash)
+
     let op_tbl () =
-      let tbl = Hashtbl.create 29 in
-      let add (c1,c2) = Hashtbl.add tbl (Lazy.force c1) c2 in
+      let tbl = ConstrHashtbl.create 29 in
+      let add (c1,c2) = ConstrHashtbl.add tbl (Lazy.force c1) c2 in
       List.iter add 
 	[
 	 ctrue,CCtrue; cfalse,CCfalse;
@@ -289,7 +296,7 @@ module Make (Atom:ATOM) =
     let of_coq atom_of_coq reify c =
       let op_tbl = Lazy.force op_tbl in
       let get_cst c = 
-	try Hashtbl.find op_tbl c with Not_found -> CCunknown in
+	try ConstrHashtbl.find op_tbl c with Not_found -> CCunknown in
       let rec mk_hform h =
 	let c, args = Term.decompose_app h in
 	match get_cst c with
@@ -308,7 +315,7 @@ module Make (Atom:ATOM) =
               get reify (Fapp (Fimp, [|l1;l2|]))
             | _ -> error "SmtForm.Form.of_coq: wrong number of arguments for implb")
 	| CCifb ->
-	    (* We should also be able to syntaxify if then else *)
+	    (* We should also be able to reify if then else *)
 	    begin match args with
 	    | [b1;b2;b3] ->
 		let l1 = mk_hform b1 in
@@ -333,7 +340,7 @@ module Make (Atom:ATOM) =
 	match args with
 	| [t] -> 
 	    let c,args = Term.decompose_app t in
-	    if c = Lazy.force cnegb then
+	    if Constr.equal c (Lazy.force cnegb) then
               mk_fnot (i+1) args
 	    else 
               let q,r = i lsr 1 , i land 1 in
@@ -348,7 +355,7 @@ module Make (Atom:ATOM) =
 	| [t1;t2] -> 
 	    let l2 = mk_hform t2 in
 	    let c, args = Term.decompose_app t1 in
-	    if c = Lazy.force candb then
+	    if Constr.equal c (Lazy.force candb) then
               mk_fand (l2::acc) args
 	    else 
 	      let l1 = mk_hform t1 in
@@ -360,7 +367,7 @@ module Make (Atom:ATOM) =
 	| [t1;t2] -> 
 	    let l2 = mk_hform t2 in
 	    let c, args = Term.decompose_app t1 in
-	    if c = Lazy.force corb then
+	    if Constr.equal c (Lazy.force corb) then
               mk_for (l2::acc) args
 	    else 
 	      let l1 = mk_hform t1 in
diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml
index 9cde196..e62a459 100644
--- a/src/zchaff/zchaff.ml
+++ b/src/zchaff/zchaff.ml
@@ -388,8 +388,8 @@ let build_body_eq reify_atom reify_form l1 l2 l (max_id, confl) =
 let get_arguments concl = 
   let f, args = Term.decompose_app concl in
   match args with
-  | [ty;a;b] when f = Lazy.force ceq && ty = Lazy.force cbool -> a, b
-  | [a] when f = Lazy.force cis_true -> a, Lazy.force ctrue
+  | [ty;a;b] when (Constr.equal f (Lazy.force ceq)) && (Constr.equal ty (Lazy.force cbool)) -> a, b
+  | [a] when (Constr.equal f (Lazy.force cis_true)) -> a, Lazy.force ctrue
   | _ -> failwith ("Zchaff.get_arguments :can only deal with equality over bool")
 
 
@@ -495,9 +495,9 @@ let tactic gl =
   let reify_atom = Atom.create () in
   let reify_form = Form.create () in
   let body = 
-    if (b = Lazy.force ctrue || b = Lazy.force cfalse) then
+    if ((Constr.equal b (Lazy.force ctrue)) || (Constr.equal b (Lazy.force cfalse))) then
       let l = Form.of_coq (Atom.get reify_atom) reify_form a in
-      let l' = if b = Lazy.force ctrue then Form.neg l else l in
+      let l' = if (Constr.equal b (Lazy.force ctrue)) then Form.neg l else l in
       let atom_tbl = Atom.atom_tbl reify_atom in
       let pform_tbl = Form.pform_tbl reify_form in
       let max_id_confl = make_proof pform_tbl atom_tbl (Environ.push_rel_context forall_let env) reify_form l' in
@@ -510,7 +510,8 @@ let tactic gl =
       let pform_tbl = Form.pform_tbl reify_form in
       let max_id_confl = make_proof pform_tbl atom_tbl (Environ.push_rel_context forall_let env) reify_form l in
       build_body_eq reify_atom reify_form 
-	(Form.to_coq l1) (Form.to_coq l2) (Form.to_coq l) max_id_confl in
+	(Form.to_coq l1) (Form.to_coq l2) (Form.to_coq l) max_id_confl
+  in
   let compose_lam_assum forall_let body =
     List.fold_left (fun t rd -> Term.mkLambda_or_LetIn rd t) body forall_let in
   let res = compose_lam_assum forall_let body in