- auto-generated mli files for future documentation

- new Makefiles to handle these mli

7 files changed, 471 insertions, 0 deletions

diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli
new file mode 100644
index 0000000..8fd166e
--- /dev/null
+++ b/src/trace/coqTerms.mli
@@ -0,0 +1,112 @@
+val gen_constant : string list list -> string -> Term.constr lazy_t
+val cint : Term.constr lazy_t
+val ceq63 : Term.constr lazy_t
+val carray : Term.constr lazy_t
+val positive_modules : string list list
+val cpositive : Term.constr lazy_t
+val cxI : Term.constr lazy_t
+val cxO : Term.constr lazy_t
+val cxH : Term.constr lazy_t
+val ceqbP : Term.constr lazy_t
+val z_modules : string list list
+val cZ : Term.constr lazy_t
+val cZ0 : Term.constr lazy_t
+val cZpos : Term.constr lazy_t
+val cZneg : Term.constr lazy_t
+val copp : Term.constr lazy_t
+val cadd : Term.constr lazy_t
+val csub : Term.constr lazy_t
+val cmul : Term.constr lazy_t
+val cltb : Term.constr lazy_t
+val cleb : Term.constr lazy_t
+val cgeb : Term.constr lazy_t
+val cgtb : Term.constr lazy_t
+val ceqbZ : Term.constr lazy_t
+val bool_modules : string list list
+val cbool : Term.constr lazy_t
+val ctrue : Term.constr lazy_t
+val cfalse : Term.constr lazy_t
+val candb : Term.constr lazy_t
+val corb : Term.constr lazy_t
+val cxorb : Term.constr lazy_t
+val cnegb : Term.constr lazy_t
+val cimplb : Term.constr lazy_t
+val ceqb : Term.constr lazy_t
+val cifb : Term.constr lazy_t
+val creflect : Term.constr lazy_t
+val clist : Term.constr lazy_t
+val cnil : Term.constr lazy_t
+val ccons : Term.constr lazy_t
+val coption : Term.constr lazy_t
+val cSome : Term.constr lazy_t
+val cNone : Term.constr lazy_t
+val cpair : Term.constr lazy_t
+val csigT : Term.constr lazy_t
+val cnot : Term.constr lazy_t
+val ceq : Term.constr lazy_t
+val crefl_equal : Term.constr lazy_t
+val smt_modules : string list list
+val cState_C_t : Term.constr lazy_t
+val cdistinct : Term.constr lazy_t
+val ctype : Term.constr lazy_t
+val cTZ : Term.constr lazy_t
+val cTbool : Term.constr lazy_t
+val cTpositive : Term.constr lazy_t
+val cTindex : Term.constr lazy_t
+val ctyp_eqb : Term.constr lazy_t
+val cTyp_eqb : Term.constr lazy_t
+val cte_carrier : Term.constr lazy_t
+val cte_eqb : Term.constr lazy_t
+val ctyp_eqb_of_typ_eqb_param : Term.constr lazy_t
+val cunit_typ_eqb : Term.constr lazy_t
+val ctval : Term.constr lazy_t
+val cTval : Term.constr lazy_t
+val cCO_xH : Term.constr lazy_t
+val cCO_Z0 : Term.constr lazy_t
+val cUO_xO : Term.constr lazy_t
+val cUO_xI : Term.constr lazy_t
+val cUO_Zpos : Term.constr lazy_t
+val cUO_Zneg : Term.constr lazy_t
+val cUO_Zopp : Term.constr lazy_t
+val cBO_Zplus : Term.constr lazy_t
+val cBO_Zminus : Term.constr lazy_t
+val cBO_Zmult : Term.constr lazy_t
+val cBO_Zlt : Term.constr lazy_t
+val cBO_Zle : Term.constr lazy_t
+val cBO_Zge : Term.constr lazy_t
+val cBO_Zgt : Term.constr lazy_t
+val cBO_eq : Term.constr lazy_t
+val cNO_distinct : Term.constr lazy_t
+val catom : Term.constr lazy_t
+val cAcop : Term.constr lazy_t
+val cAuop : Term.constr lazy_t
+val cAbop : Term.constr lazy_t
+val cAnop : Term.constr lazy_t
+val cAapp : Term.constr lazy_t
+val cform : Term.constr lazy_t
+val cFatom : Term.constr lazy_t
+val cFtrue : Term.constr lazy_t
+val cFfalse : Term.constr lazy_t
+val cFnot2 : Term.constr lazy_t
+val cFand : Term.constr lazy_t
+val cFor : Term.constr lazy_t
+val cFxor : Term.constr lazy_t
+val cFimp : Term.constr lazy_t
+val cFiff : Term.constr lazy_t
+val cFite : Term.constr lazy_t
+val cis_true : Term.constr lazy_t
+val cvalid_sat_checker : Term.constr lazy_t
+val cinterp_var_sat_checker : Term.constr lazy_t
+val make_certif_ops :
+  string list list ->
+  Term.constr array option ->
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t
+val ceq_refl_true : Term.constr lazy_t
+val eq_refl_true : unit -> Term.constr
+val vm_cast_true : Term.constr -> Term.constr
diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli
new file mode 100644
index 0000000..5d4201b
--- /dev/null
+++ b/src/trace/satAtom.mli
@@ -0,0 +1,112 @@
+module Atom :
+  sig
+    type t = int
+    val index : 'a -> 'a
+    val equal : 'a -> 'a -> bool
+    val is_bool_type : 'a -> bool
+    type reify_tbl = {
+      mutable count : int;
+      tbl : (Term.constr, int) Hashtbl.t;
+    }
+    val create : unit -> reify_tbl
+    val declare : reify_tbl -> Term.constr -> int
+    val get : reify_tbl -> Term.constr -> int
+    val atom_tbl : reify_tbl -> Term.constr array
+    val interp_tbl : reify_tbl -> Term.constr
+  end
+module Form :
+  sig
+    type hatom = Atom.t
+    type t = SmtForm.Make(Atom).t
+    type pform = (hatom, t) SmtForm.gen_pform
+    val pform_true : pform
+    val pform_false : pform
+    val equal : t -> t -> bool
+    val to_lit : t -> int
+    val index : t -> int
+    val pform : t -> pform
+    val neg : t -> t
+    val is_pos : t -> bool
+    val is_neg : t -> bool
+    val to_smt :
+      (Format.formatter -> hatom -> unit) -> Format.formatter -> t -> unit
+    exception NotWellTyped of pform
+    type reify = SmtForm.Make(Atom).reify
+    val create : unit -> reify
+    val clear : reify -> unit
+    val get : reify -> pform -> t
+    val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
+    val flatten : reify -> t -> t
+    val to_coq : t -> Term.constr
+    val pform_tbl : reify -> pform array
+    val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
+    val interp_tbl : reify -> Term.constr * Term.constr
+    val nvars : reify -> int
+    val interp_to_coq :
+      (hatom -> Term.constr) ->
+      (int, Term.constr) Hashtbl.t -> t -> Term.constr
+  end
+module Trace :
+  sig
+    val share_value : Form.t SmtCertif.clause -> unit
+    module HashedHeadRes :
+      sig
+        type t = Form.t SmtCertif.resolution
+        val equal :
+          'a SmtCertif.resolution -> 'b SmtCertif.resolution -> bool
+        val hash : 'a SmtCertif.resolution -> int
+      end
+    module HRtbl :
+      sig
+        type key = HashedHeadRes.t
+        type 'a t = 'a Hashtbl.Make(HashedHeadRes).t
+        val create : int -> 'a t
+        val clear : 'a t -> unit
+        val reset : 'a t -> unit
+        val copy : 'a t -> 'a t
+        val add : 'a t -> key -> 'a -> unit
+        val remove : 'a t -> key -> unit
+        val find : 'a t -> key -> 'a
+        val find_all : 'a t -> key -> 'a list
+        val replace : 'a t -> key -> 'a -> unit
+        val mem : 'a t -> key -> bool
+        val iter : (key -> 'a -> unit) -> 'a t -> unit
+        val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+        val length : 'a t -> int
+        val stats : 'a t -> Hashtbl.statistics
+      end
+    val common_head :
+      'a SmtCertif.clause list ->
+      'b SmtCertif.clause list ->
+      'a SmtCertif.clause list * 'a SmtCertif.clause list *
+      'b SmtCertif.clause list
+    val share_prefix : Form.t SmtCertif.clause -> int -> unit
+  end
+module Cnf :
+  sig
+    type form_info =
+      SmtCnf.MakeCnf(Form).form_info =
+        Immediate of bool
+      | Done
+      | Todo
+    val info : (int, form_info) Hashtbl.t
+    val init_last : Form.t SmtCertif.clause
+    val last : Form.t SmtCertif.clause ref
+    val cnf_todo : Form.t array list ref
+    val clear : unit -> unit
+    val push_cnf : Form.t array -> unit
+    val get_info : Form.t -> form_info
+    val set_done : Form.t -> unit
+    val set_immediate : Form.t -> unit
+    val test_immediate : Form.t -> bool
+    val check_trivial : Form.t list -> bool
+    val link_Other : Form.t SmtCertif.rule -> Form.t list -> unit
+    val both_lit : Form.t -> Form.t * Form.t
+    val or_of_imp : Form.t array -> Form.t array
+    val cnf : Form.t -> unit
+    exception Cnf_done
+    val imm_link_Other : Form.t SmtCertif.rule -> Form.t -> unit
+    val imm_cnf : Form.t SmtCertif.clause -> unit
+    val make_cnf :
+      Form.reify -> Form.t SmtCertif.clause -> Form.t SmtCertif.clause
+  end
diff --git a/src/trace/smtCertif.mli b/src/trace/smtCertif.mli
new file mode 100644
index 0000000..dee465c
--- /dev/null
+++ b/src/trace/smtCertif.mli
@@ -0,0 +1,42 @@
+type used = int
+type clause_id = int
+type 'hform rule =
+    ImmFlatten of 'hform clause * 'hform
+  | True
+  | False
+  | BuildDef of 'hform
+  | BuildDef2 of 'hform
+  | BuildProj of 'hform * int
+  | ImmBuildDef of 'hform clause
+  | ImmBuildDef2 of 'hform clause
+  | ImmBuildProj of 'hform clause * int
+  | EqTr of 'hform * 'hform list
+  | EqCgr of 'hform * 'hform option list
+  | EqCgrP of 'hform * 'hform * 'hform option list
+  | LiaMicromega of 'hform list *
+      Structures.Micromega_plugin_Certificate.Mc.zArithProof list
+  | LiaDiseq of 'hform
+  | SplArith of 'hform clause * 'hform *
+      Structures.Micromega_plugin_Certificate.Mc.zArithProof list
+  | SplDistinctElim of 'hform clause * 'hform
+  | Hole of 'hform clause list * 'hform list
+and 'hform clause = {
+  id : clause_id;
+  mutable kind : 'hform clause_kind;
+  mutable pos : int option;
+  mutable used : used;
+  mutable prev : 'hform clause option;
+  mutable next : 'hform clause option;
+  value : 'hform list option;
+}
+and 'hform clause_kind =
+    Root
+  | Same of 'hform clause
+  | Res of 'hform resolution
+  | Other of 'hform rule
+and 'hform resolution = {
+  mutable rc1 : 'hform clause;
+  mutable rc2 : 'hform clause;
+  mutable rtail : 'hform clause list;
+}
+val used_clauses : 'a rule -> 'a clause list
diff --git a/src/trace/smtCnf.mli b/src/trace/smtCnf.mli
new file mode 100644
index 0000000..47fbd8c
--- /dev/null
+++ b/src/trace/smtCnf.mli
@@ -0,0 +1,25 @@
+module MakeCnf :
+  functor (Form : SmtForm.FORM) ->
+    sig
+      type form_info = Immediate of bool | Done | Todo
+      val info : (int, form_info) Hashtbl.t
+      val init_last : Form.t SmtCertif.clause
+      val last : Form.t SmtCertif.clause ref
+      val cnf_todo : Form.t array list ref
+      val clear : unit -> unit
+      val push_cnf : Form.t array -> unit
+      val get_info : Form.t -> form_info
+      val set_done : Form.t -> unit
+      val set_immediate : Form.t -> unit
+      val test_immediate : Form.t -> bool
+      val check_trivial : Form.t list -> bool
+      val link_Other : Form.t SmtCertif.rule -> Form.t list -> unit
+      val both_lit : Form.t -> Form.t * Form.t
+      val or_of_imp : Form.t array -> Form.t array
+      val cnf : Form.t -> unit
+      exception Cnf_done
+      val imm_link_Other : Form.t SmtCertif.rule -> Form.t -> unit
+      val imm_cnf : Form.t SmtCertif.clause -> unit
+      val make_cnf :
+        Form.reify -> Form.t SmtCertif.clause -> Form.t SmtCertif.clause
+    end
diff --git a/src/trace/smtCommands.mli b/src/trace/smtCommands.mli
new file mode 100644
index 0000000..b90e3ff
--- /dev/null
+++ b/src/trace/smtCommands.mli
@@ -0,0 +1,92 @@
+val euf_checker_modules : string list list
+val certif_ops :
+  Term.constr array option ->
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t
+val cCertif : Term.constr lazy_t
+val ccertif : Term.constr lazy_t
+val cchecker : Term.constr lazy_t
+val cchecker_correct : Term.constr lazy_t
+val cchecker_b_correct : Term.constr lazy_t
+val cchecker_b : Term.constr lazy_t
+val cchecker_eq_correct : Term.constr lazy_t
+val cchecker_eq : Term.constr lazy_t
+val compute_roots :
+  SmtAtom.Form.t list -> SmtAtom.Form.t SmtCertif.clause -> int list
+val interp_uf :
+  (int, Term.constr) Hashtbl.t ->
+  (int, Term.constr) Hashtbl.t -> SmtAtom.Form.t list -> Term.constr
+val interp_conseq_uf :
+  SmtAtom.Form.t list list * SmtAtom.Form.t list -> Term.types
+val print_assm : Term.constr -> unit
+val parse_certif :
+  Names.identifier ->
+  Names.identifier ->
+  Names.identifier ->
+  Names.identifier ->
+  Names.identifier ->
+  Names.identifier ->
+  Names.identifier ->
+  SmtAtom.Btype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl *
+  SmtAtom.Form.reify * SmtAtom.Form.t list * int *
+  SmtAtom.Form.t SmtCertif.clause -> unit
+val interp_roots : SmtAtom.Form.t list -> Term.constr
+val theorem :
+  Names.identifier ->
+  SmtAtom.Btype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl *
+  SmtAtom.Form.reify * SmtAtom.Form.t list * int *
+  SmtAtom.Form.t SmtCertif.clause -> unit
+val checker :
+  SmtAtom.Btype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl *
+  SmtAtom.Form.reify * SmtAtom.Form.t list * int *
+  SmtAtom.Form.t SmtCertif.clause -> unit
+val build_body :
+  SmtAtom.Btype.reify_tbl ->
+  SmtAtom.Op.reify_tbl ->
+  SmtAtom.Atom.reify_tbl ->
+  SmtAtom.Form.reify ->
+  Term.constr ->
+  Term.constr ->
+  int * SmtAtom.Form.t SmtCertif.clause ->
+  Term.constr * Term.constr * (Names.identifier * Term.types) list
+val build_body_eq :
+  SmtAtom.Btype.reify_tbl ->
+  SmtAtom.Op.reify_tbl ->
+  SmtAtom.Atom.reify_tbl ->
+  SmtAtom.Form.reify ->
+  Term.constr ->
+  Term.constr ->
+  Term.constr ->
+  int * SmtAtom.Form.t SmtCertif.clause ->
+  Term.constr * Term.constr * (Names.identifier * Term.types) list
+val get_arguments : Term.constr -> Term.constr * Term.constr
+val make_proof :
+  ('a ->
+   'b ->
+   SmtAtom.Form.t -> SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t -> 'c) ->
+  'a -> 'b -> SmtAtom.Form.reify -> SmtAtom.Form.t -> 'c
+val core_tactic :
+  (SmtAtom.Btype.reify_tbl ->
+   SmtAtom.Op.reify_tbl ->
+   SmtAtom.Form.t ->
+   SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t ->
+   int * SmtAtom.Form.t SmtCertif.clause) ->
+  SmtAtom.Btype.reify_tbl ->
+  SmtAtom.Op.reify_tbl ->
+  SmtAtom.Atom.reify_tbl ->
+  SmtAtom.Form.reify ->
+  Environ.env -> Evd.evar_map -> Term.constr -> Proof_type.tactic
+val tactic :
+  (SmtAtom.Btype.reify_tbl ->
+   SmtAtom.Op.reify_tbl ->
+   SmtAtom.Form.t ->
+   SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t ->
+   int * SmtAtom.Form.t SmtCertif.clause) ->
+  SmtAtom.Btype.reify_tbl ->
+  SmtAtom.Op.reify_tbl ->
+  SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> Proof_type.tactic
diff --git a/src/trace/smtMisc.mli b/src/trace/smtMisc.mli
new file mode 100644
index 0000000..d6aa792
--- /dev/null
+++ b/src/trace/smtMisc.mli
@@ -0,0 +1,7 @@
+val cInt_tbl : (int, Term.constr) Hashtbl.t
+val mkInt : int -> Term.constr
+type 'a gen_hashed = { index : int; hval : 'a; }
+val mklApp : Term.constr Lazy.t -> Term.constr array -> Term.constr
+val declare_new_type : Names.variable -> Term.constr
+val declare_new_variable : Names.variable -> Term.types -> Term.constr
+val mkName : string -> Names.name
diff --git a/src/trace/smtTrace.mli b/src/trace/smtTrace.mli
new file mode 100644
index 0000000..533725b
--- /dev/null
+++ b/src/trace/smtTrace.mli
@@ -0,0 +1,81 @@
+val notUsed : int
+val clear : unit -> unit
+val next_id : unit -> SmtCertif.clause_id
+val mk_scertif :
+  'a SmtCertif.clause_kind -> 'a list option -> 'a SmtCertif.clause
+val mkRootGen : 'a list option -> 'a SmtCertif.clause
+val mkRootV : 'a list -> 'a SmtCertif.clause
+val isRoot : 'a SmtCertif.clause_kind -> bool
+val mkRes :
+  'a SmtCertif.clause ->
+  'a SmtCertif.clause -> 'a SmtCertif.clause list -> 'a SmtCertif.clause
+val isRes : 'a SmtCertif.clause_kind -> bool
+val mkOther : 'a SmtCertif.rule -> 'a list option -> 'a SmtCertif.clause
+val next : 'a SmtCertif.clause -> 'a SmtCertif.clause
+val has_prev : 'a SmtCertif.clause -> bool
+val prev : 'a SmtCertif.clause -> 'a SmtCertif.clause
+val link : 'a SmtCertif.clause -> 'a SmtCertif.clause -> unit
+val clear_links : 'a SmtCertif.clause -> unit
+val skip : 'a SmtCertif.clause -> unit
+val insert_before : 'a SmtCertif.clause -> 'a SmtCertif.clause -> unit
+val get_res : 'a SmtCertif.clause -> string -> 'a SmtCertif.resolution
+val get_other : 'a SmtCertif.clause -> string -> 'a SmtCertif.rule
+val get_val : 'a SmtCertif.clause -> 'a list
+val repr : 'a SmtCertif.clause -> 'a SmtCertif.clause
+val set_same : 'a SmtCertif.clause -> 'a SmtCertif.clause -> unit
+val get_pos : 'a SmtCertif.clause -> int
+val eq_clause : 'a SmtCertif.clause -> 'b SmtCertif.clause -> bool
+val select : 'a SmtCertif.clause -> unit
+val occur : 'a SmtCertif.clause -> unit
+val alloc : 'a SmtCertif.clause -> int
+val naive_alloc : 'a SmtCertif.clause -> int
+val build_certif : 'a SmtCertif.clause -> 'b SmtCertif.clause -> int
+val to_coq :
+  ('a -> Term.constr) ->
+  ('a list list * 'a list -> 'b) ->
+  Term.types Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
+  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
+  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
+  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
+  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
+  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
+  Term.constr Lazy.t ->
+  'a SmtCertif.clause ->
+  Term.constr * 'a SmtCertif.clause * (Names.identifier * 'b) list
+module MakeOpt :
+  functor (Form : SmtForm.FORM) ->
+    sig
+      val share_value : Form.t SmtCertif.clause -> unit
+      module HashedHeadRes :
+        sig
+          type t = Form.t SmtCertif.resolution
+          val equal :
+            'a SmtCertif.resolution -> 'b SmtCertif.resolution -> bool
+          val hash : 'a SmtCertif.resolution -> int
+        end
+      module HRtbl :
+        sig
+          type key = HashedHeadRes.t
+          type 'a t = 'a Hashtbl.Make(HashedHeadRes).t
+          val create : int -> 'a t
+          val clear : 'a t -> unit
+          val reset : 'a t -> unit
+          val copy : 'a t -> 'a t
+          val add : 'a t -> key -> 'a -> unit
+          val remove : 'a t -> key -> unit
+          val find : 'a t -> key -> 'a
+          val find_all : 'a t -> key -> 'a list
+          val replace : 'a t -> key -> 'a -> unit
+          val mem : 'a t -> key -> bool
+          val iter : (key -> 'a -> unit) -> 'a t -> unit
+          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+          val length : 'a t -> int
+          val stats : 'a t -> Hashtbl.statistics
+        end
+      val common_head :
+        'a SmtCertif.clause list ->
+        'b SmtCertif.clause list ->
+        'a SmtCertif.clause list * 'a SmtCertif.clause list *
+        'b SmtCertif.clause list
+      val share_prefix : Form.t SmtCertif.clause -> int -> unit
+    end