Hopefully solved the problem with universes for the tactic

1 files changed, 35 insertions, 10 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))