Identify ML functions that are implemented differently in native-coq and in standard coq

5 files changed, 42 insertions, 75 deletions

diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index 8046a47..d71ba45 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -170,7 +170,7 @@ let make_certif_ops modules =
   gen_constant modules "LiaMicromega", gen_constant modules "LiaDiseq", gen_constant modules "SplArith", gen_constant modules "SplDistinctElim")
   
 
-(** Usefull construction *)
+(** Useful construction *)
 
 let ceq_refl_true = 
   lazy (SmtMisc.mklApp crefl_equal [|Lazy.force cbool;Lazy.force ctrue|])
diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml
index 849c0d7..893a9be 100644
--- a/src/trace/smtMisc.ml
+++ b/src/trace/smtMisc.ml
@@ -35,11 +35,11 @@ let mklApp f args = Term.mkApp (Lazy.force f, args)
 let coqtype = lazy Term.mkSet
 
 let declare_new_type t =
-  Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) (Lazy.force coqtype) [] false None (Pp.dummy_loc,t);
+  Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) (Lazy.force coqtype) [] false None (Structures.dummy_loc,t);
   Term.mkVar t
 
 let declare_new_variable v constr_t =
-  Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) constr_t [] false None (Pp.dummy_loc,v);
+  Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) constr_t [] false None (Structures.dummy_loc,v);
   Term.mkVar v
 
 let mkName s =
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index 0ae0bc9..cb670c4 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -145,12 +145,7 @@ let parse_certif t_i t_func t_atom t_form root used_root trace fsmt fproof =
   let (tres, last_root) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) certif_ops confl in
   let certif =
    mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
-  let ce4 =
-    { const_entry_body = certif;
-      const_entry_type = None;
-      const_entry_secctx = None;
-      const_entry_opaque = false;
-      const_entry_inline_code = false} in
+  let ce4 = Structures.mkConst certif in
   let _ = declare_constant trace (DefinitionEntry ce4, IsDefinition Definition) in
   let used_roots = compute_roots roots last_root in
   let roots =
@@ -164,49 +159,19 @@ let parse_certif t_i t_func t_atom t_form root used_root trace fsmt fproof =
     let i = ref (l-1) in
     List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots;
     mklApp cSome [|mklApp carray [|Lazy.force cint|]; Structures.mkArray (Lazy.force cint, res)|] in
-  let ce3 =
-    { const_entry_body = roots;
-      const_entry_type = None;
-      const_entry_secctx = None;
-      const_entry_opaque = false;
-      const_entry_inline_code = false} in
+  let ce3 = Structures.mkConst roots in
   let _ = declare_constant root (DefinitionEntry ce3, IsDefinition Definition) in
-  let ce3' =
-    { const_entry_body = used_roots;
-      const_entry_type = None;
-      const_entry_secctx = None;
-      const_entry_opaque = false;
-      const_entry_inline_code = false} in
+  let ce3' = Structures.mkConst used_roots in
   let _ = declare_constant used_root (DefinitionEntry ce3', IsDefinition Definition) in
   let t_i' = make_t_i rt in
   let t_func' = make_t_func ro t_i' in
-  let ce5 =
-    { const_entry_body = t_i';
-      const_entry_type = None;
-      const_entry_secctx = None;
-      const_entry_opaque = false;
-      const_entry_inline_code = false} in
+  let ce5 = Structures.mkConst t_i' in
   let _ = declare_constant t_i (DefinitionEntry ce5, IsDefinition Definition) in
-  let ce6 =
-    { const_entry_body = t_func';
-      const_entry_type = None;
-      const_entry_secctx = None;
-      const_entry_opaque = false;
-      const_entry_inline_code = false} in
+  let ce6 = Structures.mkConst t_func' in
   let _ = declare_constant t_func (DefinitionEntry ce6, IsDefinition Definition) in
-  let ce1 =
-    { const_entry_body = Atom.interp_tbl ra;
-      const_entry_type = None;
-      const_entry_secctx = None;
-      const_entry_opaque = false;
-      const_entry_inline_code = false} in
+  let ce1 = Structures.mkConst (Atom.interp_tbl ra) in
   let _ = declare_constant t_atom (DefinitionEntry ce1, IsDefinition Definition) in
-  let ce2 =
-    { const_entry_body = snd (Form.interp_tbl rf);
-      const_entry_type = None;
-      const_entry_secctx = None;
-      const_entry_opaque = false;
-      const_entry_inline_code = false} in
+  let ce2 = Structures.mkConst (snd (Form.interp_tbl rf)) in
   let _ = declare_constant t_form (DefinitionEntry ce2, IsDefinition Definition) in
   ()
 
@@ -263,12 +228,7 @@ let theorem name fsmt fproof =
      [|Term.mkRel 2; Term.mkRel 1; Term.mkRel 6; Term.mkRel 5; Term.mkRel 4; Term.mkRel 7; Term.mkRel 3;
 	vm_cast_true
 	  (mklApp cchecker [|Term.mkRel 2; Term.mkRel 1; Term.mkRel 6; Term.mkRel 5; Term.mkRel 4; Term.mkRel 7; Term.mkRel 3|])|]))))))) in
-  let ce =
-    { const_entry_body = theorem_proof;
-      const_entry_type = Some theorem_concl;
-      const_entry_secctx = None;
-      const_entry_opaque = true;
-      const_entry_inline_code = false} in
+  let ce = Structures.mkConst theorem_proof in
   let _ = declare_constant name (DefinitionEntry ce, IsDefinition Definition) in
     ()
 
@@ -421,7 +381,7 @@ let call_verit rt ro fl root =
   try
     import_trace logfilename (Some root)
   with
-    | VeritSyntax.Sat -> Errors.error "veriT can't prove this"
+    | VeritSyntax.Sat -> Structures.error "veriT can't prove this"
 
 
 let cchecker_b_correct =
diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
index 8f74c32..de2879c 100644
--- a/src/versions/native/structures.ml
+++ b/src/versions/native/structures.ml
@@ -13,14 +13,36 @@
 (*                                                                        *)
 (**************************************************************************)
 
+
+open Entries
+
+
 (* Int63 *)
 let int63_modules = [["Coq";"Numbers";"Cyclic";"Int63";"Int63Native"]]
 
-let mkInt i = Term.mkInt (Uint63.of_int i)
+let mkInt : int -> Term.constr =
+  fun i -> Term.mkInt (Uint63.of_int i)
 
 
 (* PArray *)
 let parray_modules = [["Coq";"Array";"PArray"]]
 
-let max_array_size = Parray.trunc_size (Uint63.of_int 4194303)
-let mkArray = Term.mkArray
+let max_array_size : int =
+  Parray.trunc_size (Uint63.of_int 4194303)
+let mkArray : Term.types * Term.constr array -> Term.constr =
+  Term.mkArray
+
+
+(* Differences between the two versions of Coq *)
+let dummy_loc = Pp.dummy_loc
+
+let mkConst c =
+  { const_entry_body = c;
+    const_entry_type = None;
+    const_entry_secctx = None;
+    const_entry_opaque = false;
+    const_entry_inline_code = false}
+
+let glob_term_CbvVm = Glob_term.CbvVm None
+
+let error = Errors.error
diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml
index 8c07fc7..e843d1f 100644
--- a/src/zchaff/zchaff.ml
+++ b/src/zchaff/zchaff.ml
@@ -200,24 +200,14 @@ let parse_certif dimacs trace fdimacs ftrace =
   SmtTrace.clear ();
   let _,first,last,reloc = import_cnf fdimacs in
   let d = make_roots first last in
-  let ce1 =
-    { const_entry_body = d;
-      const_entry_type = None;
-      const_entry_secctx = None;
-      const_entry_opaque = false;
-      const_entry_inline_code = false} in
+  let ce1 = Structures.mkConst d in
   let _ = declare_constant dimacs (DefinitionEntry ce1, IsDefinition Definition) in
 
   let max_id, confl = import_cnf_trace reloc ftrace first last in
   let (tres,_) = SmtTrace.to_coq (fun _ -> assert false) certif_ops confl in
   let certif = 
    mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in 
-  let ce2 =
-    { const_entry_body = certif;
-      const_entry_type = None;
-      const_entry_secctx = None;
-      const_entry_opaque = false;
-      const_entry_inline_code = false} in
+  let ce2 = Structures.mkConst certif in
   let _ = declare_constant trace (DefinitionEntry ce2, IsDefinition Definition) in
   ()
 
@@ -250,12 +240,7 @@ let theorem name fdimacs ftrace =
 		  vm_cast_true 
 		    (mklApp cchecker [|Term.mkRel 3(*d*); Term.mkRel 2(*c*)|]);
                   Term.mkRel 1(*v*)|]))) in
-  let ce =
-    { const_entry_body = theorem_proof;
-      const_entry_type = Some theorem_type;
-      const_entry_secctx = None;
-      const_entry_opaque = true;
-      const_entry_inline_code = false} in
+  let ce = Structures.mkConst theorem_proof in
   let _ = declare_constant name (DefinitionEntry ce, IsDefinition Definition) in
   ()
 
@@ -273,7 +258,7 @@ let checker fdimacs ftrace =
 
   let tm = mklApp cchecker [|d; certif|] in
   let expr = Constrextern.extern_constr true Environ.empty_env tm in
-  Vernacentries.interp (Vernacexpr.VernacCheckMayEval (Some (Glob_term.CbvVm None), None, expr))
+  Vernacentries.interp (Vernacexpr.VernacCheckMayEval (Some Structures.glob_term_CbvVm, None, expr))
 
 
 
@@ -479,7 +464,7 @@ let make_proof pform_tbl atom_tbl env reify_form l =
   let (reloc, resfilename, logfilename, last) =
     call_zchaff (Form.nvars reify_form) root in
   (try check_unsat resfilename with
-    | Sat model -> Errors.error (List.fold_left (fun acc i ->
+    | Sat model -> Structures.error (List.fold_left (fun acc i ->
       let index = if i > 0 then i-1 else -i-1 in
       let ispos = i > 0 in
       try (