Identify ML functions that depend on native-coq

12 files changed, 74 insertions, 41 deletions

diff --git a/src/configure.sh b/src/configure.sh
index 04da739..d889828 100755
--- a/src/configure.sh
+++ b/src/configure.sh
@@ -3,7 +3,7 @@
 set -e
 
 if [ $@ -a $@ = -standard ]; then
-    cp Makefile.standard Makefile
+    cp versions/standard/Makefile Makefile
 else
-    cp Makefile.native Makefile
+    cp versions/native/Makefile Makefile
 fi
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index 1ee6448..8046a47 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -18,15 +18,11 @@ open Coqlib
 let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant)
 
 (* Int63 *)
-let int63_modules = [["Coq";"Numbers";"Cyclic";"Int63";"Int63Native"]]
-
-let cint = gen_constant int63_modules "int"
-let ceq63 = gen_constant int63_modules "eqb"
+let cint = gen_constant Structures.int63_modules "int"
+let ceq63 = gen_constant Structures.int63_modules "eqb"
 
 (* PArray *)
-let parray_modules = [["Coq";"Array";"PArray"]]
-
-let carray = gen_constant parray_modules "array"
+let carray = gen_constant Structures.parray_modules "array"
 
 (* Positive *)
 let positive_modules = [["Coq";"Numbers";"BinNums"];
diff --git a/src/trace/satAtom.ml b/src/trace/satAtom.ml
index ca72504..f381407 100644
--- a/src/trace/satAtom.ml
+++ b/src/trace/satAtom.ml
@@ -53,7 +53,7 @@ module Atom =
       t
 
     let interp_tbl reify =
-      Term.mkArray (Lazy.force cbool, atom_tbl reify)
+      Structures.mkArray (Lazy.force cbool, atom_tbl reify)
 
   end
 
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index 3164692..392ef2e 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -100,7 +100,7 @@ module Btype =
 	| Tindex it -> t.(it.index) <- it.hval
 	| _ -> () in
       Hashtbl.iter set reify.tbl;
-      Term.mkArray (Lazy.force ctyp_eqb, t)
+      Structures.mkArray (Lazy.force ctyp_eqb, t)
 
     let to_list reify =
       let set _ t acc = match t with
@@ -291,7 +291,7 @@ module Op =
       let set _ v = 
 	t.(v.index) <- mk_Tval v.hval.tparams v.hval.tres v.hval.op_val in
       Hashtbl.iter set reify.tbl;
-      Term.mkArray (tval, t)
+      Structures.mkArray (tval, t)
 
     let to_list reify =
       let set _ op acc =
@@ -651,7 +651,7 @@ module Atom =
 
     let interp_tbl reify =
       let t = to_array reify (Lazy.force dft_atom) a_to_coq in
-      Term.mkArray (Lazy.force catom, t)
+      Structures.mkArray (Lazy.force catom, t)
 
 
     (** Producing a Coq term corresponding to the interpretation of an atom *)
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index 6075b3f..c7856f3 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -413,7 +413,7 @@ module Make (Atom:ATOM) =
     let args_to_coq args =
       let cargs = Array.make (Array.length args + 1) (mkInt 0) in
       Array.iteri (fun i hf -> cargs.(i) <- to_coq hf) args;
-      Term.mkArray (Lazy.force cint, cargs)
+      Structures.mkArray (Lazy.force cint, cargs)
 	
     let pf_to_coq = function
       | Fatom a -> mklApp cFatom [|mkInt (Atom.index a)|]	
@@ -449,7 +449,7 @@ module Make (Atom:ATOM) =
 
     let interp_tbl reify =
       let (i,t) = to_array reify (Lazy.force cFtrue) pf_to_coq in
-      (mkInt i, Term.mkArray (Lazy.force cform, t))
+      (mkInt i, Structures.mkArray (Lazy.force cform, t))
 
     let nvars reify = reify.count
     (** Producing a Coq term corresponding to the interpretation of a formula *)
diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml
index 02e5f26..849c0d7 100644
--- a/src/trace/smtMisc.ml
+++ b/src/trace/smtMisc.ml
@@ -20,7 +20,7 @@ let cInt_tbl = Hashtbl.create 17
 let mkInt i = 
   try Hashtbl.find cInt_tbl i 
   with Not_found ->
-    let ci = Term.mkInt (Uint63.of_int i) in
+    let ci = Structures.mkInt i in
     Hashtbl.add cInt_tbl i ci;
     ci
 
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index 8420ca1..b96807f 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.ml
@@ -295,7 +295,7 @@ let to_coq to_lit (cstep,
 	      l := tl
 	  | _ -> assert false 
 	done;
-	mklApp cRes [|mkInt (get_pos c); Term.mkArray (Lazy.force cint, args)|]
+	mklApp cRes [|mkInt (get_pos c); Structures.mkArray (Lazy.force cint, args)|]
     | Other other ->
 	begin match other with
 	| ImmFlatten (c',f) -> mklApp cImmFlatten [|out_c c;out_c c'; out_f f|]
@@ -330,25 +330,25 @@ let to_coq to_lit (cstep,
     | _ -> assert false in
   let step = Lazy.force cstep in
   let def_step = 
-    mklApp cRes [|mkInt 0; Term.mkArray (Lazy.force cint, [|mkInt 0|]) |] in
+    mklApp cRes [|mkInt 0; Structures.mkArray (Lazy.force cint, [|mkInt 0|]) |] in
   let r = ref confl in
   let nc = ref 0 in
   while not (isRoot !r.kind) do r := prev !r; incr nc done;
   let last_root = !r in
   let size = !nc in
-  let max = (Parray.trunc_size (Uint63.of_int 4194303)) - 1 in
+  let max = Structures.max_array_size - 1 in
   let q,r1 = size / max, size mod max in
 
   let trace = 
     let len = if r1 = 0 then q + 1 else q + 2 in
-    Array.make len (Term.mkArray (step, [|def_step|])) in
+    Array.make len (Structures.mkArray (step, [|def_step|])) in
   for j = 0 to q - 1 do
-    let tracej = Array.make (Parray.trunc_size (Uint63.of_int 4194303)) def_step in
+    let tracej = Array.make Structures.max_array_size def_step in
     for i = 0 to max - 1 do
       r := next !r;
       tracej.(i) <- step_to_coq !r; 
     done;
-    trace.(j) <- Term.mkArray (step, tracej)
+    trace.(j) <- Structures.mkArray (step, tracej)
   done;
   if r1 <> 0 then begin
     let traceq = Array.make (r1 + 1) def_step in
@@ -356,10 +356,10 @@ let to_coq to_lit (cstep,
     r := next !r; 
     traceq.(i) <- step_to_coq !r; 
     done;
-    trace.(q) <- Term.mkArray (step, traceq)
+    trace.(q) <- Structures.mkArray (step, traceq)
   end;
 
-  (Term.mkArray (mklApp carray [|step|], trace), last_root)
+  (Structures.mkArray (mklApp carray [|step|], trace), last_root)
 
 
 
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index 87e74a6..0ae0bc9 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -157,13 +157,13 @@ let parse_certif t_i t_func t_atom t_form root used_root trace fsmt fproof =
     let res = Array.make (List.length roots + 1) (mkInt 0) in
     let i = ref 0 in
     List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
-    Term.mkArray (Lazy.force cint, res) in
+    Structures.mkArray (Lazy.force cint, res) in
   let used_roots =
     let l = List.length used_roots in
     let res = Array.make (l + 1) (mkInt 0) in
     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|]; Term.mkArray (Lazy.force cint, res)|] in
+    mklApp cSome [|mklApp carray [|Lazy.force cint|]; Structures.mkArray (Lazy.force cint, res)|] in
   let ce3 =
     { const_entry_body = roots;
       const_entry_type = None;
@@ -238,12 +238,12 @@ let theorem name fsmt fproof =
     let res = Array.make (l + 1) (mkInt 0) in
     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|]; Term.mkArray (Lazy.force cint, res)|] in
+    mklApp cSome [|mklApp carray [|Lazy.force cint|]; Structures.mkArray (Lazy.force cint, res)|] in
   let rootsCstr =
     let res = Array.make (List.length roots + 1) (mkInt 0) in
     let i = ref 0 in
     List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
-    Term.mkArray (Lazy.force cint, res) in
+    Structures.mkArray (Lazy.force cint, res) in
 
   let t_atom = Atom.interp_tbl ra in
   let t_form = snd (Form.interp_tbl rf) in
@@ -298,13 +298,13 @@ let checker fsmt fproof =
     let res = Array.make (l + 1) (mkInt 0) in
     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|]; Term.mkArray (Lazy.force cint, res)|] in
+    mklApp cSome [|mklApp carray [|Lazy.force cint|]; Structures.mkArray (Lazy.force cint, res)|] in
   let t9 = Unix.time () in  (* for debug *)
   let rootsCstr =
     let res = Array.make (List.length roots + 1) (mkInt 0) in
     let i = ref 0 in
     List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
-    Term.mkArray (Lazy.force cint, res) in
+    Structures.mkArray (Lazy.force cint, res) in
   let t10 = Unix.time () in  (* for debug *)
 
   let t_i = make_t_i rt in
diff --git a/src/Make.native b/src/versions/native/Make
index 34e6dc2..5695872 100644
--- a/src/Make.native
+++ b/src/versions/native/Make
@@ -14,7 +14,7 @@
 ## Change the "install-natdynlink" target: change CMXSFILES into CMXS and add the same thing for CMXA and VCMXS. ##
 ## Change the "install" target: change CMO into CMX.                  ##
 ## Finally, suppress the "Makefile" target and add to the "clean" target: ##
-##   - rm -f NSMTCoq* cnf/NSMTCoq* euf/NSMTCoq* lia/NSMTCoq* spl/NSMTCoq* ../unit-tests/NSMTCoq* ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml verit/smtlib2_parse.mli verit/smtlib2_parse.ml verit/smtlib2_lex.ml ##
+##   - rm -f NSMTCoq* cnf/NSMTCoq* euf/NSMTCoq* lia/NSMTCoq* spl/NSMTCoq* ../unit-tests/NSMTCoq* ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml verit/smtlib2_parse.mli verit/smtlib2_parse.ml verit/smtlib2_lex.ml ##
 ########################################################################
 
 
@@ -26,6 +26,7 @@
 -I trace
 -I verit
 -I zchaff
+-I versions/native
 
 -custom "cd ../unit-tests; make" "" "test"
 
@@ -33,7 +34,7 @@
 -custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli"
 -custom "" "verit/veritParser.ml verit/veritLexer.ml verit/smtlib2_parse.ml verit/smtlib2_lex.ml" "ml"
 
--custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx verit/smtlib2_util.cmx verit/smtlib2_ast.cmx verit/smtlib2_parse.cmx verit/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx verit/smtlib2_genConstr.cmx verit/verit.cmx trace/smt_tactic.cmx" "$(CMXA)"
+-custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx verit/smtlib2_util.cmx verit/smtlib2_ast.cmx verit/smtlib2_parse.cmx verit/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx verit/smtlib2_genConstr.cmx verit/verit.cmx trace/smt_tactic.cmx" "$(CMXA)"
 -custom "$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)"
 
 CMXA = trace/smtcoq.cmxa
@@ -42,6 +43,8 @@ VCMXS = "NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq
 CAMLLEX = $(CAMLBIN)ocamllex
 CAMLYACC = $(CAMLBIN)ocamlyacc
 
+versions/native/structures.ml
+
 trace/coqTerms.ml
 trace/satAtom.ml
 trace/smtAtom.ml
diff --git a/src/Makefile.native b/src/versions/native/Makefile
index 2ec982f..7162b56 100644
--- a/src/Makefile.native
+++ b/src/versions/native/Makefile
@@ -14,7 +14,7 @@
 
 #
 # This Makefile was generated by the command line :
-# coq_makefile -f Make.native -o Makefile 
+# coq_makefile -f Make -o Makefile 
 #
 
 .DEFAULT_GOAL := all
@@ -39,13 +39,20 @@ $(call includecmdwithout@,$(COQBIN)coqtop -config)
 #                        #
 ##########################
 
-OCAMLLIBS?=-I zchaff\
+OCAMLLIBS?=-I versions/native\
+  -I zchaff\
   -I verit\
   -I trace\
   -I lia\
   -I euf\
   -I cnf
-COQLIBS?= -R . SMTCoq
+COQLIBS?=-I versions/native\
+  -I zchaff\
+  -I verit\
+  -I trace\
+  -I lia\
+  -I euf\
+  -I cnf -R . SMTCoq
 COQDOCLIBS?=-R . SMTCoq
 
 ##########################
@@ -174,7 +181,8 @@ MLFILES:=lia/lia.ml\
   trace/smtCertif.ml\
   trace/smtAtom.ml\
   trace/satAtom.ml\
-  trace/coqTerms.ml
+  trace/coqTerms.ml\
+  versions/native/structures.ml
 
 -include $(addsuffix .d,$(MLFILES))
 .SECONDARY: $(addsuffix .d,$(MLFILES))
@@ -250,7 +258,7 @@ beautify: $(VFILES:=.beautified)
 $(CMXS): $(CMXA)
 	$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^
 
-$(CMXA): trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx verit/smtlib2_util.cmx verit/smtlib2_ast.cmx verit/smtlib2_parse.cmx verit/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx verit/smtlib2_genConstr.cmx verit/verit.cmx trace/smt_tactic.cmx
+$(CMXA): versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx verit/smtlib2_util.cmx verit/smtlib2_ast.cmx verit/smtlib2_parse.cmx verit/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx verit/smtlib2_genConstr.cmx verit/verit.cmx trace/smt_tactic.cmx
 	$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^
 
 ml: verit/veritParser.ml verit/veritLexer.ml verit/smtlib2_parse.ml verit/smtlib2_lex.ml
diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
new file mode 100644
index 0000000..8f74c32
--- /dev/null
+++ b/src/versions/native/structures.ml
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* Int63 *)
+let int63_modules = [["Coq";"Numbers";"Cyclic";"Int63";"Int63Native"]]
+
+let mkInt 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
diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml
index b94a0cc..8c07fc7 100644
--- a/src/zchaff/zchaff.ml
+++ b/src/zchaff/zchaff.ml
@@ -139,7 +139,7 @@ let import_cnf_trace reloc filename first last =
 
 let make_roots first last =
   let cint = Lazy.force cint in
-  let roots = Array.make (last.id + 2) (Term.mkArray (cint, Array.make 1 (mkInt 0))) in
+  let roots = Array.make (last.id + 2) (Structures.mkArray (cint, Array.make 1 (mkInt 0))) in
   let mk_elem l = 
     let x = match Form.pform l with
     | Fatom x -> x + 2
@@ -150,15 +150,15 @@ let make_roots first last =
     let root = Array.of_list (get_val !r) in
     let croot = Array.make (Array.length root + 1) (mkInt 0) in
     Array.iteri (fun i l -> croot.(i) <- mk_elem l) root;
-    roots.(!r.id) <- Term.mkArray (cint, croot);
+    roots.(!r.id) <- Structures.mkArray (cint, croot);
     r := next !r 
   done;
   let root = Array.of_list (get_val !r) in
   let croot = Array.make (Array.length root + 1) (mkInt 0) in
   Array.iteri (fun i l -> croot.(i) <- mk_elem l) root;
-  roots.(!r.id) <- Term.mkArray (cint, croot);
+  roots.(!r.id) <- Structures.mkArray (cint, croot);
 
-  Term.mkArray (mklApp carray [|cint|], roots)
+  Structures.mkArray (mklApp carray [|cint|], roots)
 
 let interp_roots first last =
   let tbl = Hashtbl.create 17 in