Both native-coq and Coq 8.5 are fully supported

11 files changed, 91 insertions, 41 deletions

diff --git a/src/SMT_terms.v b/src/SMT_terms.v
index 2d16d3e..6c5ba27 100644
--- a/src/SMT_terms.v
+++ b/src/SMT_terms.v
@@ -234,6 +234,22 @@ Record typ_eqb : Type := Typ_eqb {
   te_reflect : forall x y, reflect (x = y) (te_eqb x y)
 }.
 
+Section Typ_eqb_param.
+
+  Variable A : Type.
+
+  Record typ_eqb_param : Type := Typ_eqb_param {
+    te_eqb_param : A -> A -> bool;
+    te_reflect_param : forall x y, reflect (x = y) (te_eqb_param x y)
+  }.
+
+  Variable r : typ_eqb_param.
+
+  Definition typ_eqb_of_typ_eqb_param :=
+    Typ_eqb A (te_eqb_param r) (te_reflect_param r).
+
+End Typ_eqb_param.
+
 (* Common used types into which we interpret *)
 
 (* Unit *)
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index e8a7737..1cc6d4f 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -112,6 +112,8 @@ let ctyp_eqb = gen_constant smt_modules "typ_eqb"
 let cTyp_eqb = gen_constant smt_modules "Typ_eqb"
 let cte_carrier = gen_constant smt_modules "te_carrier"
 let cte_eqb = gen_constant smt_modules "te_eqb"
+let ctyp_eqb_param = gen_constant smt_modules "typ_eqb_param"
+let ctyp_eqb_of_typ_eqb_param = gen_constant smt_modules "typ_eqb_of_typ_eqb_param"
 let cunit_typ_eqb = gen_constant smt_modules "unit_typ_eqb"
 
 let ctval =  gen_constant smt_modules "tval"
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index 80c012f..bbad580 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -61,7 +61,8 @@ module Btype =
     (* reify table *)
     type reify_tbl = 
         { mutable count : int;
-	          tbl : (Term.constr, btype) Hashtbl.t
+	          tbl : (Term.constr, btype) Hashtbl.t;
+          mutable cuts : (Structures.names_id_t * Term.types) list
 	}
 
     let create () = 
@@ -70,7 +71,10 @@ module Btype =
       Hashtbl.add htbl (Lazy.force cbool) Tbool;
       (* Hashtbl.add htbl (Lazy.force cpositive) Tpositive; *)
       { count = 0;
-	tbl = htbl }
+	tbl = htbl;
+        cuts = [] }
+
+    let get_cuts reify = reify.cuts
 
     let declare reify t typ_eqb =
       (* TODO: allows to have only typ_eqb *)
@@ -84,14 +88,23 @@ module Btype =
       try
         Hashtbl.find reify.tbl t
       with | Not_found ->
-        let eq_t = declare_new_variable (Names.id_of_string "eq") (Term.mkArrow t (Term.mkArrow t (Lazy.force cbool))) in
-        let x = mkName "x" in
-        let y = mkName "y" in
-        let rx = Term.mkRel 2 in
-        let ry = Term.mkRel 1 in
-        let eq_refl = Term.mkProd (x,t,Term.mkProd (y,t,mklApp creflect [|mklApp ceq [|t;rx;ry|];mklApp (lazy eq_t) [|rx;ry|]|])) in
-        let eq_refl_v = declare_new_variable (Names.id_of_string ("eq_refl")) eq_refl in
-        let ce = mklApp cTyp_eqb [|t;eq_t;eq_refl_v|] in
+        let n = string_of_int (List.length reify.cuts) in
+        let eq_name = Names.id_of_string ("eq"^n) in
+        let eq_var = Term.mkVar eq_name in
+
+        (* let eq_ty = Term.mkArrow t (Term.mkArrow t (Lazy.force cbool)) in *)
+
+        (* let eq = mkName "eq" in *)
+        (* let x = mkName "x" in *)
+        (* let y = mkName "y" in *)
+        (* let req = Term.mkRel 3 in *)
+        (* let rx = Term.mkRel 2 in *)
+        (* let ry = Term.mkRel 1 in *)
+        (* let eq_refl_ty = Term.mkLambda (eq, eq_ty, Term.mkProd (x,t,Term.mkProd (y,t,mklApp creflect [|mklApp ceq [|t;rx;ry|]; Term.mkApp (req, [|rx;ry|])|]))) in *)
+
+        let eq_ty = mklApp ctyp_eqb_param [|t|] in
+        reify.cuts <- (eq_name, eq_ty)::reify.cuts;
+        let ce = mklApp ctyp_eqb_of_typ_eqb_param [|t; eq_var|] in
         declare reify t ce
 
     let interp_tbl reify =
diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli
index 9b8a613..fd0a30c 100644
--- a/src/trace/smtAtom.mli
+++ b/src/trace/smtAtom.mli
@@ -48,6 +48,8 @@ module Btype :
 
       val interp_to_coq : reify_tbl -> btype -> Term.constr
 
+      val get_cuts : reify_tbl -> (Structures.names_id_t * Term.types) list
+
     end
 
 (** Operators *)
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index 53ea75c..b019f24 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -230,11 +230,7 @@ let make_proof call_solver rt ro rf l =
   call_solver rt ro fl (root,l)
 
 
-let tactic call_solver rt ro ra rf gl =
-  let env = Tacmach.pf_env gl in
-  let sigma = Tacmach.project gl in
-  let t = Tacmach.pf_concl gl in
-
+let tactic call_solver rt ro ra rf env sigma t =
   let (forall_let, concl) = Term.decompose_prod_assum t in
   let env = Environ.push_rel_context forall_let env in
   let a, b = get_arguments concl in
@@ -253,4 +249,7 @@ let tactic call_solver rt ro ra rf gl =
   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
-  Tactics.exact_no_check res gl
+  let cuts = Btype.get_cuts rt in
+  List.fold_right (fun (eqn, eqt) tac ->
+    Structures.tclTHENLAST (Structures.assert_before (Names.Name eqn) eqt) tac
+  ) cuts (Structures.vm_cast_no_check res)
diff --git a/src/trace/smt_tactic.ml4 b/src/trace/smt_tactic.ml4
index c3cae79..a1f8790 100644
--- a/src/trace/smt_tactic.ml4
+++ b/src/trace/smt_tactic.ml4
@@ -51,9 +51,9 @@ END
 
 
 TACTIC EXTEND Tactic_zchaff
-| [ "zchaff" ] -> [ Structures.mk_tactic Zchaff.tactic ]
+| [ "zchaff" ] -> [ Structures.mk_sat_tactic Zchaff.tactic ]
 END
 
 TACTIC EXTEND Tactic_verit
-| [ "verit" ] -> [ Structures.mk_tactic Verit.tactic ]
+| [ "verit" ] -> [ Structures.mk_smt_tactic Verit.tactic ]
 END
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index 3a1abc0..d2db93e 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -149,10 +149,10 @@ let call_verit rt ro fl root =
     | VeritSyntax.Sat -> Structures.error "veriT can't prove this"
 
 
-let tactic gl =
+let tactic env sigma t =
   clear_all ();
   let rt = Btype.create () in
   let ro = Op.create () in
   let ra = VeritSyntax.ra in
   let rf = VeritSyntax.rf in
-  SmtCommands.tactic call_verit rt ro ra rf gl
+  SmtCommands.tactic call_verit rt ro ra rf env sigma t
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml
index 3ff11e9..33c059d 100644
--- a/src/verit/veritSyntax.ml
+++ b/src/verit/veritSyntax.ml
@@ -136,7 +136,7 @@ let mkCongrPred p =
                 Other (EqCgrP (p_p,c,cert))
               else failwith "VeritSyntax.mkCongrPred: unmatching predicates"
             | _ -> failwith "VeritSyntax.mkCongrPred : not pred app")
-        |_ ->  failwith "VeritSyntax.mkCongr: no or more than one predicate app premice in congruence")
+        |_ ->  failwith "VeritSyntax.mkCongr: no or more than one predicate app premise in congruence")
     |[] ->  failwith "VeritSyntax.mkCongrPred: no conclusion in congruence"
     |_ -> failwith "VeritSyntax.mkCongrPred: more than one conclusion in congruence"
 
diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
index 62907d1..919f2f1 100644
--- a/src/versions/native/structures.ml
+++ b/src/versions/native/structures.ml
@@ -41,6 +41,8 @@ let mkArray : Term.types * Term.constr array -> Term.constr =
 
 
 (* Differences between the two versions of Coq *)
+type names_id_t = Names.identifier
+
 let dummy_loc = Pp.dummy_loc
 
 let mkConst c =
@@ -71,4 +73,12 @@ let pr_constr_env = Printer.pr_constr_env
 
 let lift = Term.lift
 
-let mk_tactic t = t
+let mk_sat_tactic tac = tac
+let tclTHENLAST = Tacticals.tclTHENLAST
+let assert_before = Tactics.assert_tac
+let vm_cast_no_check = Tactics.vm_cast_no_check
+let mk_smt_tactic tac gl =
+  let env = Tacmach.pf_env gl in
+  let sigma = Tacmach.project gl in
+  let t = Tacmach.pf_concl gl in
+  tac env sigma t gl
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index 93546b3..66106a6 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -64,6 +64,8 @@ let mkArray : Term.types * Term.constr array -> Term.constr =
 
 
 (* Differences between the two versions of Coq *)
+type names_id_t = Names.Id.t
+
 let dummy_loc = Loc.ghost
 
 let mkConst c =
@@ -101,4 +103,14 @@ let pr_constr_env env = Printer.pr_constr_env env Evd.empty
 
 let lift = Vars.lift
 
-let mk_tactic = Proofview.V82.tactic
+let mk_sat_tactic = Proofview.V82.tactic
+let tclTHENLAST = Tacticals.New.tclTHENLAST
+let assert_before = Tactics.assert_before
+let vm_cast_no_check t = Proofview.V82.tactic (Tactics.vm_cast_no_check t)
+let mk_smt_tactic tac =
+  Proofview.Goal.nf_enter (fun gl ->
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
+    let t = Proofview.Goal.concl gl in
+    tac env sigma t
+  )
diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v
index 7e356bb..e63bbaf 100644
--- a/unit-tests/Tests_verit.v
+++ b/unit-tests/Tests_verit.v
@@ -842,25 +842,21 @@ Proof.
   verit.
 Qed.
 
-Section Concrete.
-  Goal forall (i j:int),
+Goal forall (i j:int),
     (i == j) && (negb (i == j)) = false.
-  Proof.
-    verit.
-  Qed.
-End Concrete.
-
-Section Concrete2.
-  Lemma concrete2 : forall i j, (i == j) || (negb (i == j)).
-  Proof.
-    verit.
-  Qed.
-  Check concrete2.
-End Concrete2.
-Check concrete2.
-
-
-(* Congruence in which some premices are REFL *)
+Proof.
+  verit.
+  econstructor; eexact Int63Properties.reflect_eqb.
+Qed.
+
+Goal forall i j, (i == j) || (negb (i == j)).
+Proof.
+  verit.
+  econstructor; eexact Int63Properties.reflect_eqb.
+Qed.
+
+
+(* Congruence in which some premises are REFL *)
 
 Goal forall (f:Z -> Z -> Z) x y z,
   implb (Zeq_bool x y) (Zeq_bool (f z x) (f z y)).