Hopefully solved the problem with universes for the tactic

4 files changed, 83 insertions, 25 deletions

diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index 8365b21..87b5cb7 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -145,7 +145,7 @@ let interp_roots roots =
     | [] -> Lazy.force ctrue
     | f::roots -> List.fold_left (fun acc f -> mklApp candb [|acc; interp f|]) (interp f) roots
 
-let theorem name ((rt, ro, ra, rf, roots, max_id, confl) as p) =
+let theorem name (rt, ro, ra, rf, roots, max_id, confl) =
   let nti = mkName "t_i" in
   let ntfunc = mkName "t_func" in
   let ntatom = mkName "t_atom" in
@@ -219,7 +219,7 @@ let theorem name ((rt, ro, ra, rf, roots, max_id, confl) as p) =
 
 (* Given an SMT-LIB2 file and a certif, call the checker *)
 
-let checker ((rt, ro, ra, rf, roots, max_id, confl) as p) =
+let checker (rt, ro, ra, rf, roots, max_id, confl) =
   let nti = mkName "t_i" in
   let ntfunc = mkName "t_func" in
   let ntatom = mkName "t_atom" in
@@ -292,7 +292,7 @@ let build_body rt ro ra rf l b (max_id, confl) =
   let certif =
     mklApp cCertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*); mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
 
-  let proof =
+  let proof_cast =
     Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|],
     Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1 (*t_i*)|]|],
     Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
@@ -302,8 +302,17 @@ let build_body rt ro ra rf l b (max_id, confl) =
       [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l; b; v 1 (*certif*);
 	vm_cast_true (mklApp cchecker_b [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l; b; v 1 (*certif*)|])|])))))
   in
+  let proof_nocast =
+    Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|],
+    Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1 (*t_i*)|]|],
+    Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+    Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+    Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
+    mklApp cchecker_b_correct
+      [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l; b; v 1 (*certif*)|])))))
+  in
 
-  (proof, cuts)
+  (proof_cast, proof_nocast, cuts)
 
 
 let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) =
@@ -323,7 +332,7 @@ let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) =
   let certif =
     mklApp cCertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*); mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
 
-  let proof =
+  let proof_cast =
     Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|],
     Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1 (*t_i*)|]|],
     Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
@@ -333,8 +342,17 @@ let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) =
       [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l1; l2; l; v 1 (*certif*);
 	vm_cast_true (mklApp cchecker_eq [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l1; l2; l; v 1 (*certif*)|])|])))))
   in
+  let proof_nocast =
+    Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|],
+    Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1 (*t_i*)|]|],
+    Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+    Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+    Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
+    mklApp cchecker_eq_correct
+      [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l1; l2; l; v 1 (*certif*)|])))))
+  in
 
-  (proof, cuts)
+  (proof_cast, proof_nocast, cuts)
 
 
 let get_arguments concl =
@@ -355,7 +373,7 @@ 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
-  let (body, cuts) =
+  let (body_cast, body_nocast, cuts) =
     if ((Term.eq_constr b (Lazy.force ctrue)) || (Term.eq_constr b (Lazy.force cfalse))) then
       let l = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf a in
       let l' = if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in
@@ -367,10 +385,17 @@ let tactic call_solver rt ro ra rf env sigma t =
       let l = Form.neg (Form.get rf (Fapp(Fiff,[|l1;l2|]))) in
       let max_id_confl = make_proof call_solver rt ro rf l in
       build_body_eq rt ro ra rf (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
+  let res_cast = compose_lam_assum forall_let body_cast in
+  let res_nocast = compose_lam_assum forall_let body_nocast in
+
   let cuts = (Btype.get_cuts rt)@cuts 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)
+      Structures.tclTHENLAST (Structures.assert_before (Names.Name eqn) eqt) tac
+    ) cuts
+      (Structures.tclTHEN
+         (Structures.set_evars_tac res_nocast)
+         (Structures.vm_cast_no_check res_cast))
diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
index f6b21c8..9a56d43 100644
--- a/src/versions/native/structures.ml
+++ b/src/versions/native/structures.ml
@@ -108,6 +108,7 @@ let pr_constr_env = Printer.pr_constr_env
 
 let lift = Term.lift
 
+let tclTHEN = Tacticals.tclTHEN
 let tclTHENLAST = Tacticals.tclTHENLAST
 let assert_before = Tactics.assert_tac
 let vm_cast_no_check = Tactics.vm_cast_no_check
@@ -116,6 +117,7 @@ let mk_tactic tac gl =
   let sigma = Tacmach.project gl in
   let t = Tacmach.pf_concl gl in
   tac env sigma t gl
+let set_evars_tac _ = Tacticals.tclIDTAC
 
 let ppconstr_lsimpleconstr = Ppconstr.lsimple
 let constrextern_extern_constr =
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index 4206006..168c9b2 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -132,6 +132,7 @@ let pr_constr_env env = Printer.pr_constr_env env Evd.empty
 
 let lift = Vars.lift
 
+let tclTHEN = Tacticals.New.tclTHEN
 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)
@@ -142,6 +143,11 @@ let mk_tactic tac =
     let t = Proofview.Goal.concl gl in
     tac env sigma t
   )
+let set_evars_tac noc =
+  mk_tactic (
+      fun env sigma _ ->
+      let sigma, _ = Typing.type_of env sigma noc in
+      Proofview.Unsafe.tclEVARS sigma)
 
 let ppconstr_lsimpleconstr = Ppconstr.lsimpleconstr
 let constrextern_extern_constr =
diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml
index 2f08d99..bd656aa 100644
--- a/src/zchaff/zchaff.ml
+++ b/src/zchaff/zchaff.ml
@@ -368,12 +368,22 @@ let build_body reify_atom reify_form l b (max_id, confl) =
   let vtvar = Term.mkRel 3 in
   let vtform = Term.mkRel 2 in
   let vc = Term.mkRel 1 in
-  Term.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|],
-  Term.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|],
-  Term.mkLetIn (nc, certif, Lazy.force ccertif, 
-  mklApp cchecker_b_correct 
-	 [|vtvar; vtform; l; b; vc; 
-	   vm_cast_true (mklApp cchecker_b [|vtform;l;b;vc|])|])))
+  let proof_cast =
+    Term.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|],
+    Term.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|],
+    Term.mkLetIn (nc, certif, Lazy.force ccertif,
+    mklApp cchecker_b_correct
+	   [|vtvar; vtform; l; b; vc;
+	     vm_cast_true (mklApp cchecker_b [|vtform;l;b;vc|])|])))
+  in
+  let proof_nocast =
+    Term.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|],
+    Term.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|],
+    Term.mkLetIn (nc, certif, Lazy.force ccertif,
+    mklApp cchecker_b_correct
+	   [|vtvar; vtform; l; b; vc|])))
+  in
+  (proof_cast, proof_nocast)
 
 
 let build_body_eq reify_atom reify_form l1 l2 l (max_id, confl) =
@@ -389,12 +399,22 @@ let build_body_eq reify_atom reify_form l1 l2 l (max_id, confl) =
   let vtvar = Term.mkRel 3 in
   let vtform = Term.mkRel 2 in
   let vc = Term.mkRel 1 in
-  Term.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|],
-  Term.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|],
-  Term.mkLetIn (nc, certif, Lazy.force ccertif, 
-  mklApp cchecker_eq_correct 
-         [|vtvar; vtform; l1; l2; l; vc;
-	   vm_cast_true (mklApp cchecker_eq [|vtform;l1;l2;l;vc|])|])))
+  let proof_cast =
+    Term.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|],
+    Term.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|],
+    Term.mkLetIn (nc, certif, Lazy.force ccertif,
+    mklApp cchecker_eq_correct
+           [|vtvar; vtform; l1; l2; l; vc;
+	     vm_cast_true (mklApp cchecker_eq [|vtform;l1;l2;l;vc|])|])))
+  in
+  let proof_nocast =
+    Term.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|],
+    Term.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|],
+    Term.mkLetIn (nc, certif, Lazy.force ccertif,
+    mklApp cchecker_eq_correct
+           [|vtvar; vtform; l1; l2; l; vc|])))
+  in
+  (proof_cast, proof_nocast)
 
 let get_arguments concl = 
   let f, args = Term.decompose_app concl in
@@ -501,7 +521,7 @@ let tactic env sigma t =
   let a, b = get_arguments concl in
   let reify_atom = Atom.create () in
   let reify_form = Form.create () in
-  let body = 
+  let (body_cast, body_nocast) =
     if ((Term.eq_constr b (Lazy.force ctrue)) || (Term.eq_constr b (Lazy.force cfalse))) then
       let l = Form.of_coq (Atom.get reify_atom) reify_form a in
       let l' = if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in
@@ -519,7 +539,12 @@ let tactic env sigma t =
       build_body_eq reify_atom reify_form 
 	(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
-  Structures.vm_cast_no_check res
+  let res_cast = compose_lam_assum forall_let body_cast in
+  let res_nocast = compose_lam_assum forall_let body_nocast in
+
+  (Structures.tclTHEN
+     (Structures.set_evars_tac res_nocast)
+     (Structures.vm_cast_no_check res_cast))