Improved performance with coq-8.5

4 files changed, 50 insertions, 24 deletions

diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index 4c0ea6d..8365b21 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -184,20 +184,35 @@ let theorem name ((rt, ro, ra, rf, roots, max_id, confl) as p) =
     Structures.mkArray (Lazy.force cint, res) in
 
   let theorem_concl = mklApp cnot [|mklApp cis_true [|interp_roots roots|]|] in
-  let theorem_proof =
-   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*)|],
-   Term.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|],
-   Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
-   mklApp cchecker_correct
-     [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*);
-	vm_cast_true
-	  (mklApp cchecker [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|])|]))))))) in
+  let theorem_proof_cast =
+    Term.mkCast (
+        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*)|],
+        Term.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|],
+        Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
+        mklApp cchecker_correct
+               [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*);
+	         vm_cast_true
+	           (mklApp cchecker [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|])|]))))))),
+        Term.VMcast,
+        theorem_concl)
+  in
+  let theorem_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*)|],
+        Term.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|],
+        Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
+        mklApp cchecker_correct
+               [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|])))))))
+  in
 
-  let ce = Structures.mkTConst theorem_proof theorem_concl in
+  let ce = Structures.mkTConst theorem_proof_cast theorem_proof_nocast theorem_concl in
   let _ = declare_constant name (DefinitionEntry ce, IsDefinition Definition) in
   ()
 
diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
index 60ea0e5..1eb43fb 100644
--- a/src/versions/native/structures.ml
+++ b/src/versions/native/structures.ml
@@ -80,7 +80,7 @@ let mkUConst c =
     const_entry_opaque = false;
     const_entry_inline_code = false}
 
-let mkTConst c ty =
+let mkTConst c _ ty =
   { const_entry_body = c;
     const_entry_type = Some ty;
     const_entry_secctx = None;
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index bf53f41..519103f 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -97,10 +97,10 @@ let mkUConst c =
     const_entry_opaque      = false;
     const_entry_inline_code = false }
 
-let mkTConst c ty =
+let mkTConst c noc ty =
   let env = Global.env () in
   let evd = Evd.from_env env in
-  let evd, _ = Typing.type_of env evd c in
+  let evd, _ = Typing.type_of env evd noc in
   { const_entry_body        = Future.from_val ((c, Univ.ContextSet.empty),
                                                Safe_typing.empty_private_constants);
     const_entry_secctx      = None;
diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml
index 74ae918..c9ed267 100644
--- a/src/zchaff/zchaff.ml
+++ b/src/zchaff/zchaff.ml
@@ -231,16 +231,27 @@ let theorem name fdimacs ftrace =
   let vtype = Term.mkProd(Names.Anonymous, Lazy.force cint, Lazy.force cbool) in
   let theorem_type = 
     Term.mkProd (mkName "v", vtype, theorem_concl) in
-  let theorem_proof =
-   Term.mkLetIn (mkName "d", d, Lazy.force cdimacs,
-   Term.mkLetIn (mkName "c", certif, Lazy.force ccertif,
-   Term.mkLambda (mkName "v", vtype,
-   mklApp ctheorem_checker
+  let theorem_proof_cast =
+    Term.mkCast (
+        Term.mkLetIn (mkName "d", d, Lazy.force cdimacs,
+        Term.mkLetIn (mkName "c", certif, Lazy.force ccertif,
+        Term.mkLambda (mkName "v", vtype,
+        mklApp ctheorem_checker
                [| Term.mkRel 3(*d*); Term.mkRel 2(*c*);
-		  vm_cast_true 
+		  vm_cast_true
 		    (mklApp cchecker [|Term.mkRel 3(*d*); Term.mkRel 2(*c*)|]);
-                  Term.mkRel 1(*v*)|]))) in
-  let ce = Structures.mkTConst theorem_proof theorem_type in
+                  Term.mkRel 1(*v*)|]))),
+      Term.VMcast,
+      theorem_type)
+  in
+  let theorem_proof_nocast =
+    Term.mkLetIn (mkName "d", d, Lazy.force cdimacs,
+    Term.mkLetIn (mkName "c", certif, Lazy.force ccertif,
+    Term.mkLambda (mkName "v", vtype,
+    mklApp ctheorem_checker
+           [| Term.mkRel 3(*d*); Term.mkRel 2(*c*)|])))
+  in
+  let ce = Structures.mkTConst theorem_proof_cast theorem_proof_nocast theorem_type in
   let _ = declare_constant name (DefinitionEntry ce, IsDefinition Definition) in
   ()