- auto-generated mli files for future documentation

- new Makefiles to handle these mli

5 files changed, 71 insertions, 4 deletions

diff --git a/src/extraction/Makefile b/src/extraction/Makefile
index 043afa1..73b0ae4 100644
--- a/src/extraction/Makefile
+++ b/src/extraction/Makefile
@@ -1,6 +1,6 @@
 # List of user's files and name of the final program (edit this part)
 
-USERFILES=smtcoq.ml
+USERFILES=smtcoq.ml smtcoq.mli
 PROGRAM=smtcoq
 # USERFILES=test.ml
 # PROGRAM=test
@@ -19,9 +19,12 @@ SMTLIB=-I .. -I ../zchaff -I ../verit -I ../trace -I ../smtlib2 -I ../lia -I ../
 COQLIB=-I ${COQTOP}kernel -I ${COQTOP}lib -I ${COQTOP}library -I ${COQTOP}parsing -I ${COQTOP}pretyping -I ${COQTOP}interp -I ${COQTOP}proofs -I ${COQTOP}tactics -I ${COQTOP}toplevel -I ${COQTOP}plugins/btauto -I ${COQTOP}plugins/cc -I ${COQTOP}plugins/decl_mode -I ${COQTOP}plugins/extraction -I ${COQTOP}plugins/field -I ${COQTOP}plugins/firstorder -I ${COQTOP}plugins/fourier -I ${COQTOP}plugins/funind -I ${COQTOP}plugins/micromega -I ${COQTOP}plugins/nsatz -I ${COQTOP}plugins/omega -I ${COQTOP}plugins/quote -I ${COQTOP}plugins/ring -I ${COQTOP}plugins/romega -I ${COQTOP}plugins/rtauto -I ${COQTOP}plugins/setoid_ring -I ${COQTOP}plugins/syntax -I ${COQTOP}plugins/xml -I /usr/lib/ocaml/camlp5
 
 CMXA=nums.cmxa str.cmxa unix.cmxa gramlib.cmxa dynlink.cmxa ${COQTOP}kernel/byterun/coq_fix_code.o ${COQTOP}kernel/byterun/coq_interp.o ${COQTOP}kernel/byterun/coq_memory.o ${COQTOP}kernel/byterun/coq_values.o clib.cmxa lib.cmxa kernel.cmxa library.cmxa pretyping.cmxa interp.cmxa proofs.cmxa parsing.cmxa tactics.cmxa toplevel.cmxa micromega_plugin.cmxa smtcoq.cmxa
-CMI=extrNative.cmi sat_checker.cmi smt_checker.cmi
+CMI=extrNative.cmi sat_checker.cmi zchaff_checker.cmi smt_checker.cmi verit_checker.cmi
 CMX=extrNative.cmx sat_checker.cmx zchaff_checker.cmx smt_checker.cmx verit_checker.cmx
-USERCMX=$(USERFILES:.ml=.cmx)
+USERML=$(filter %.ml,$(USERFILES))
+USERCMX=$(USERML:%.ml=%.cmx)
+USERMLI=$(filter %.mli,$(USERFILES))
+USERCMI=$(USERMLI:%.mli=%.cmi)
 
 OCAMLC=ocamlc
 OCAMLOPT=ocamlopt
@@ -35,7 +38,7 @@ all: $(PROGRAM)
 %.cmx: %.ml
 	$(OCAMLOPT) -c $(FLAGS) $(SMTLIB) $(COQLIB) $<
 
-$(PROGRAM): $(CMI) $(CMX) $(USERCMX)
+$(PROGRAM): $(CMI) $(CMX) $(USERCMI) $(USERCMX)
 	$(OCAMLOPT) $(FLAGS) $(SMTLIB) $(COQLIB) -o $@ $(COMPILEFLAGS) $(CMXA) $(CMX) $(USERCMX)
 
 
diff --git a/src/extraction/smtcoq.mli b/src/extraction/smtcoq.mli
new file mode 100644
index 0000000..7b33e0f
--- /dev/null
+++ b/src/extraction/smtcoq.mli
@@ -0,0 +1,5 @@
+type solver = Zchaff | Verit
+val usage : string
+val string_of_solver : solver -> string
+val verifier_of_solver : solver -> string -> string -> bool
+val run : solver -> string -> string -> unit
diff --git a/src/extraction/test.mli b/src/extraction/test.mli
new file mode 100644
index 0000000..8b13789
--- /dev/null
+++ b/src/extraction/test.mli
@@ -0,0 +1 @@
+
diff --git a/src/extraction/verit_checker.mli b/src/extraction/verit_checker.mli
new file mode 100644
index 0000000..3c43d22
--- /dev/null
+++ b/src/extraction/verit_checker.mli
@@ -0,0 +1,45 @@
+module Mc = Structures.Micromega_plugin_Certificate.Mc
+val mkInt : int -> ExtrNative.uint
+val mkArray : 'a array -> 'a ExtrNative.parray
+val dump_nat : Mc.nat -> Smt_checker.nat
+val dump_positive : Mc.positive -> Smt_checker.positive
+val dump_z : Mc.z -> Smt_checker.z
+val dump_pol : Mc.z Mc.pol -> Smt_checker.z Smt_checker.pol
+val dump_psatz : Mc.z Mc.psatz -> Smt_checker.z Smt_checker.psatz
+val dump_list : ('a -> 'b) -> 'a list -> 'b Smt_checker.list
+val dump_proof_term : Micromega.zArithProof -> Smt_checker.zArithProof
+val to_coq :
+  ('a -> Smt_checker.int) ->
+  'a SmtCertif.clause ->
+  Smt_checker.Euf_Checker.step ExtrNative.parray ExtrNative.parray *
+  'a SmtCertif.clause
+val btype_to_coq : SmtAtom.btype -> Smt_checker.Typ.coq_type
+val c_to_coq : SmtAtom.cop -> Smt_checker.Atom.cop
+val u_to_coq : SmtAtom.uop -> Smt_checker.Atom.unop
+val b_to_coq : SmtAtom.bop -> Smt_checker.Atom.binop
+val n_to_coq : SmtAtom.nop -> Smt_checker.Typ.coq_type
+val i_to_coq : SmtAtom.indexed_op -> ExtrNative.uint
+val a_to_coq : SmtAtom.atom -> Smt_checker.Atom.atom
+val atom_interp_tbl :
+  SmtAtom.Atom.reify_tbl -> Smt_checker.Atom.atom ExtrNative.parray
+val form_to_coq : SmtAtom.Form.t -> ExtrNative.uint
+val args_to_coq : SmtAtom.Form.t array -> ExtrNative.uint ExtrNative.parray
+val pf_to_coq :
+  (SmtAtom.hatom, SmtAtom.Form.t) SmtForm.gen_pform -> Smt_checker.Form.form
+val form_interp_tbl :
+  SmtAtom.Form.reify -> Smt_checker.Form.form ExtrNative.parray
+val count_btype : int ref
+val count_op : int ref
+val declare_sort : Smtlib2_ast.symbol -> SmtAtom.btype
+val declare_fun :
+  Smtlib2_ast.symbol ->
+  Smtlib2_ast.sort list -> Smtlib2_ast.sort -> SmtAtom.indexed_op
+val declare_commands :
+  SmtAtom.Atom.reify_tbl ->
+  SmtAtom.Form.reify ->
+  SmtAtom.Form.t list -> Smtlib2_ast.command -> SmtAtom.Form.t list
+val import_smtlib2 :
+  SmtAtom.Atom.reify_tbl ->
+  SmtAtom.Form.reify -> string -> SmtAtom.Form.t list
+val this_clear_all : unit -> unit
+val checker : string -> string -> bool
diff --git a/src/extraction/zchaff_checker.mli b/src/extraction/zchaff_checker.mli
new file mode 100644
index 0000000..d24a1e3
--- /dev/null
+++ b/src/extraction/zchaff_checker.mli
@@ -0,0 +1,13 @@
+val mkInt : int -> ExtrNative.uint
+val mkArray : 'a array -> 'a ExtrNative.parray
+val make_roots :
+  SatAtom.Form.t SmtCertif.clause ->
+  'a SmtCertif.clause -> ExtrNative.uint ExtrNative.parray ExtrNative.parray
+val to_coq :
+  'a ->
+  'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l * 'm * 'n * 'o * 'p *
+  'q * 'r * 's * 't ->
+  'u SmtCertif.clause ->
+  Sat_checker.Sat_Checker.step ExtrNative.parray ExtrNative.parray *
+  'u SmtCertif.clause
+val checker : string -> string -> bool