New files SmtBtype.ml(i) for module formerly in SmtAtom

17 files changed, 191 insertions, 202 deletions

diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml
index b320d7a..27ac8d3 100644
--- a/src/smtlib2/smtlib2_genConstr.ml
+++ b/src/smtlib2/smtlib2_genConstr.ml
@@ -19,6 +19,7 @@ open SmtAtom
 open SmtForm
 open SmtMisc
 open CoqTerms
+open SmtBtype
 
 (* For debugging *)
 
@@ -79,7 +80,7 @@ let declare_sort rt sym =
   let eq_refl = Term.mkProd (x,cons_t,Term.mkProd (y,cons_t,mklApp creflect [|mklApp ceq [|cons_t;rx;ry|];mklApp (lazy eq_t) [|rx;ry|]|])) in
   let eq_refl_v = declare_new_variable (Names.id_of_string ("eq_refl_"^s)) eq_refl in
   let ce = mklApp cTyp_eqb [|cons_t;eq_t;eq_refl_v|] in
-  let res = Btype.declare rt cons_t ce in
+  let res = declare rt cons_t ce in
   VeritSyntax.add_btype s res;
   res
 
@@ -89,7 +90,7 @@ let declare_fun rt ro sym arg cod =
   let tyl = List.map sort_of_sort arg in
   let ty = sort_of_sort cod in
 
-  let coqTy = List.fold_right (fun typ c -> Term.mkArrow (Btype.interp_to_coq rt (fst typ)) c) tyl (Btype.interp_to_coq rt (fst ty)) in
+  let coqTy = List.fold_right (fun typ c -> Term.mkArrow (interp_to_coq rt (fst typ)) c) tyl (interp_to_coq rt (fst ty)) in
   let cons_v = declare_new_variable (Names.id_of_string ("Smt_var_"^s)) coqTy in
 
   let op = Op.declare ro cons_v (Array.of_list (List.map fst tyl)) (fst ty) in
diff --git a/src/smtlib2/smtlib2_genConstr.mli b/src/smtlib2/smtlib2_genConstr.mli
index ba69741..1aa992e 100644
--- a/src/smtlib2/smtlib2_genConstr.mli
+++ b/src/smtlib2/smtlib2_genConstr.mli
@@ -2,16 +2,16 @@ val pp_symbol : Smtlib2_ast.symbol -> string
 val string_of_symbol : Smtlib2_ast.symbol -> string
 val identifier_of_qualidentifier :
   Smtlib2_ast.qualidentifier -> Smtlib2_ast.identifier
-val string_type : string -> SmtAtom.btype
-val sort_of_string : string -> SmtAtom.btype * 'a list
-val sort_of_symbol : Smtlib2_ast.symbol -> SmtAtom.btype * 'a list
+val string_type : string -> SmtBtype.btype
+val sort_of_string : string -> SmtBtype.btype * 'a list
+val sort_of_symbol : Smtlib2_ast.symbol -> SmtBtype.btype * 'a list
 val string_of_identifier : Smtlib2_ast.identifier -> string
 val string_of_qualidentifier : Smtlib2_ast.qualidentifier -> string
-val sort_of_sort : Smtlib2_ast.sort -> (SmtAtom.btype * 'a list as 'a)
+val sort_of_sort : Smtlib2_ast.sort -> (SmtBtype.btype * 'a list as 'a)
 val declare_sort :
-  SmtAtom.Btype.reify_tbl -> Smtlib2_ast.symbol -> SmtAtom.btype
+  SmtBtype.reify_tbl -> Smtlib2_ast.symbol -> SmtBtype.btype
 val declare_fun :
-  SmtAtom.Btype.reify_tbl ->
+  SmtBtype.reify_tbl ->
   SmtAtom.Op.reify_tbl ->
   Smtlib2_ast.symbol ->
   Smtlib2_ast.sort list -> Smtlib2_ast.sort -> SmtAtom.indexed_op
@@ -22,13 +22,13 @@ val make_root :
   SmtAtom.Atom.reify_tbl ->
   SmtAtom.Form.reify -> Smtlib2_ast.term -> SmtAtom.Form.t
 val declare_commands :
-  SmtAtom.Btype.reify_tbl ->
+  SmtBtype.reify_tbl ->
   SmtAtom.Op.reify_tbl ->
   SmtAtom.Atom.reify_tbl ->
   SmtAtom.Form.reify ->
   SmtAtom.Form.t list -> Smtlib2_ast.command -> SmtAtom.Form.t list
 val import_smtlib2 :
-  SmtAtom.Btype.reify_tbl ->
+  SmtBtype.reify_tbl ->
   SmtAtom.Op.reify_tbl ->
   SmtAtom.Atom.reify_tbl ->
   SmtAtom.Form.reify -> string -> SmtAtom.Form.t list
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index 72e7ed3..ed0402c 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -16,120 +16,7 @@
 
 open SmtMisc
 open CoqTerms
-
-(** Syntaxified version of Coq type *)
-type indexed_type = Term.constr gen_hashed
-
-let dummy_indexed_type i = {index = i; hval = Term.mkProp}
-let indexed_type_index i = i.index
-
-type btype =
-  | TZ
-  | Tbool
-  | Tpositive
-  | Tindex of indexed_type
-
-module Btype = 
-  struct 
-
-    let index_tbl = Hashtbl.create 17 
-
-    let index_to_coq i =
-      let i = i.index in 
-      try Hashtbl.find index_tbl i
-      with Not_found ->
-	let interp = mklApp cTindex [|mkInt i|] in
-	Hashtbl.add index_tbl i interp;
-	interp
-
-    let equal t1 t2 =
-      match t1,t2 with
-        | Tindex i, Tindex j -> i.index == j.index
-        | _ -> t1 == t2
-
-    let to_coq = function 
-      | TZ -> Lazy.force cTZ
-      | Tbool -> Lazy.force cTbool
-      | Tpositive -> Lazy.force cTpositive
-      | Tindex i -> index_to_coq i
-
-    let to_smt fmt = function
-      | TZ -> Format.fprintf fmt "Int"
-      | Tbool -> Format.fprintf fmt "Bool"
-      | Tpositive -> Format.fprintf fmt "Int"
-      | Tindex i -> Format.fprintf fmt "Tindex_%i" i.index
-
-    (* reify table *)
-    type reify_tbl = 
-        { mutable count : int;
-	          tbl : (Term.constr, btype) Hashtbl.t;
-          mutable cuts : (Structures.names_id_t * Term.types) list
-	}
-
-    let create () = 
-      let htbl = Hashtbl.create 17 in  
-      Hashtbl.add htbl (Lazy.force cZ) TZ;
-      Hashtbl.add htbl (Lazy.force cbool) Tbool;
-      (* Hashtbl.add htbl (Lazy.force cpositive) Tpositive; *)
-      { count = 0;
-	tbl = htbl;
-        cuts = [] }
-
-    let get_cuts reify = reify.cuts
-
-    let declare reify t typ_eqb =
-      (* TODO: allows to have only typ_eqb *)
-      assert (not (Hashtbl.mem reify.tbl t));
-      let res = Tindex {index = reify.count; hval = typ_eqb} in
-      Hashtbl.add reify.tbl t res;
-      reify.count <- reify.count + 1;
-      res
-
-    let of_coq reify t =
-      try
-        Hashtbl.find reify.tbl t
-      with | Not_found ->
-        let n = string_of_int (List.length reify.cuts) in
-        let eq_name = Names.id_of_string ("eq"^n) in
-        let eq_var = Term.mkVar eq_name in
-
-        let eq_ty = Term.mkArrow t (Term.mkArrow t (Lazy.force cbool)) in
-
-        let eq = mkName "eq" in
-        let x = mkName "x" in
-        let y = mkName "y" in
-        let req = Term.mkRel 3 in
-        let rx = Term.mkRel 2 in
-        let ry = Term.mkRel 1 in
-        let refl_ty = Term.mkLambda (eq, eq_ty, Term.mkProd (x,t,Term.mkProd (y,t,mklApp creflect [|mklApp ceq [|t;rx;ry|]; Term.mkApp (req, [|rx;ry|])|]))) in
-
-        let pair_ty = mklApp csigT [|eq_ty; refl_ty|] in
-
-        reify.cuts <- (eq_name, pair_ty)::reify.cuts;
-        let ce = mklApp ctyp_eqb_of_typ_eqb_param [|t; eq_var|] in
-        declare reify t ce
-
-    let interp_tbl reify =
-      let t = Array.make (reify.count + 1) (Lazy.force cunit_typ_eqb) in
-      let set _ = function 
-	| Tindex it -> t.(it.index) <- it.hval
-	| _ -> () in
-      Hashtbl.iter set reify.tbl;
-      Structures.mkArray (Lazy.force ctyp_eqb, t)
-
-    let to_list reify =
-      let set _ t acc = match t with
-	| Tindex it -> (it.index,it)::acc
-	| _ -> acc in
-      Hashtbl.fold set reify.tbl []
-
-    let interp_to_coq reify = function
-      | TZ -> Lazy.force cZ
-      | Tbool -> Lazy.force cbool
-      | Tpositive -> Lazy.force cpositive
-      | Tindex c -> mklApp cte_carrier [|c.hval|]
-
-  end
+open SmtBtype
 
 (** Operators *)
 
@@ -215,7 +102,7 @@ module Op =
     let eq_to_coq t =
       try Hashtbl.find eq_tbl t
       with Not_found ->
-	let op = mklApp cBO_eq [|Btype.to_coq t|] in
+	let op = mklApp cBO_eq [|SmtBtype.to_coq t|] in
 	Hashtbl.add eq_tbl t op;
 	op
 
@@ -242,7 +129,7 @@ module Op =
       | TZ -> Lazy.force ceqbZ
       | Tbool -> Lazy.force ceqb
       | Tpositive -> Lazy.force ceqbP
-      | Tindex i -> mklApp cte_eqb [|i.hval|]
+      | Tindex i -> mklApp cte_eqb [|indexed_type_hval i|]
 
     let interp_bop = function
       | BO_Zplus -> Lazy.force cadd
@@ -255,7 +142,7 @@ module Op =
       | BO_eq t -> interp_eq t
 
     let n_to_coq = function
-      | NO_distinct t -> mklApp cNO_distinct [|Btype.to_coq t|]
+      | NO_distinct t -> mklApp cNO_distinct [|SmtBtype.to_coq t|]
 
     let n_type_of = function
       | NO_distinct _ -> Tbool
@@ -267,7 +154,7 @@ module Op =
       | TZ -> Lazy.force cZ
       | Tbool -> Lazy.force cbool
       | Tpositive -> Lazy.force cpositive
-      | Tindex i -> mklApp cte_carrier [|i.hval|]
+      | Tindex i -> mklApp cte_carrier [|indexed_type_hval i|]
 
     let interp_nop = function
       | NO_distinct ty -> mklApp cdistinct [|interp_distinct ty;interp_eq ty|]
@@ -320,12 +207,12 @@ module Op =
 
     let b_equal op1 op2 =
       match op1,op2 with
-      | BO_eq t1, BO_eq t2 -> Btype.equal t1 t2
+      | BO_eq t1, BO_eq t2 -> SmtBtype.equal t1 t2
       | _ -> op1 == op2
 
     let n_equal op1 op2 =
       match op1,op2 with
-      | NO_distinct t1, NO_distinct t2 -> Btype.equal t1 t2
+      | NO_distinct t1, NO_distinct t2 -> SmtBtype.equal t1 t2
 
     let i_equal op1 op2 = op1.index == op2.index
 
@@ -437,7 +324,7 @@ module Atom =
       | Anop (op,_) -> Op.n_type_of op
       | Aapp (op,_) -> Op.i_type_of op
 
-    let is_bool_type h = Btype.equal (type_of h) Tbool
+    let is_bool_type h = SmtBtype.equal (type_of h) Tbool
 
 
     let rec compute_int = function
@@ -513,19 +400,19 @@ module Atom =
       match a with
       | Acop _ -> ()
       | Auop(op,h) ->
-	 if not (Btype.equal (Op.u_type_arg op) (type_of h))
+	 if not (SmtBtype.equal (Op.u_type_arg op) (type_of h))
          then raise (NotWellTyped a)
       | Abop(op,h1,h2) ->
 	 let (t1,t2) = Op.b_type_args op in
-	 if not (Btype.equal t1 (type_of h1) && Btype.equal t2 (type_of h2))
+	 if not (SmtBtype.equal t1 (type_of h1) && SmtBtype.equal t2 (type_of h2))
 	 then raise (NotWellTyped a)
       | Anop(op,ha) ->
          let ty = Op.n_type_args op in
-         Array.iter (fun h -> if not (Btype.equal ty (type_of h)) then raise (NotWellTyped a)) ha
+         Array.iter (fun h -> if not (SmtBtype.equal ty (type_of h)) then raise (NotWellTyped a)) ha
       | Aapp(op,args) ->
 	 let tparams = Op.i_type_args op in
 	 Array.iteri (fun i t ->
-	     if not (Btype.equal t (type_of args.(i))) then
+	     if not (SmtBtype.equal t (type_of args.(i))) then
 	       raise (NotWellTyped a)) tparams
 
     type reify_tbl =
@@ -632,7 +519,7 @@ module Atom =
         let op = try Op.of_coq ro c
                  with Not_found ->
                    let targs = Array.map type_of hargs in
-                   let tres = Btype.of_coq rt ty in
+                   let tres = SmtBtype.of_coq rt ty in
                    Op.declare ro c targs tres in
         get reify (Aapp (op,hargs)) in
 
@@ -768,9 +655,9 @@ module Trace = SmtTrace.MakeOpt(Form)
 let mk_ftype cod dom =
   let typeb = Lazy.force ctype in
   let typea = mklApp clist [|typeb|] in
-  let a = Array.fold_right (fun bt acc -> mklApp ccons [|typeb; Btype.to_coq bt; acc|]) cod (mklApp cnil [|typeb|]) in
-  let b = Btype.to_coq dom in
+  let a = Array.fold_right (fun bt acc -> mklApp ccons [|typeb; SmtBtype.to_coq bt; acc|]) cod (mklApp cnil [|typeb|]) in
+  let b = SmtBtype.to_coq dom in
   mklApp cpair [|typea;typeb;a;b|]
 
-let make_t_i rt = Btype.interp_tbl rt
+let make_t_i rt = SmtBtype.interp_tbl rt
 let make_t_func ro t_i = Op.interp_tbl (mklApp ctval [|t_i|]) (fun cod dom value -> mklApp cTval [|t_i; mk_ftype cod dom; value|]) ro
diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli
index e6a3c47..8e69265 100644
--- a/src/trace/smtAtom.mli
+++ b/src/trace/smtAtom.mli
@@ -13,44 +13,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-
-type indexed_type
-
-val dummy_indexed_type: int -> indexed_type
-val indexed_type_index : indexed_type -> int
-
-type btype =
-  | TZ
-  | Tbool
-  | Tpositive
-  | Tindex of indexed_type
-
-module Btype : 
-    sig
-      
-      val equal : btype -> btype -> bool
-	  
-      val to_coq : btype -> Term.constr
-
-      val to_smt : Format.formatter -> btype -> unit
-
-      type reify_tbl
-	  
-      val create : unit -> reify_tbl
-
-      val declare : reify_tbl -> Term.constr -> Term.constr -> btype
-
-      val of_coq : reify_tbl -> Term.constr -> btype
-
-      val interp_tbl : reify_tbl -> Term.constr
-
-      val to_list : reify_tbl -> (int * indexed_type) list
-
-      val interp_to_coq : reify_tbl -> btype -> Term.constr
-
-      val get_cuts : reify_tbl -> (Structures.names_id_t * Term.types) list
-
-    end
+open SmtBtype
 
 (** Operators *)
 
@@ -142,7 +105,7 @@ module Atom :
       val get : reify_tbl -> atom -> hatom
 
       (** Given a coq term, build the corresponding atom *)
-      val of_coq : Btype.reify_tbl -> Op.reify_tbl ->
+      val of_coq : SmtBtype.reify_tbl -> Op.reify_tbl ->
         reify_tbl -> Environ.env -> Evd.evar_map -> Term.constr -> t
 
       val to_coq : hatom -> Term.constr
@@ -178,5 +141,5 @@ module Trace : sig
 end
 
 
-val make_t_i : Btype.reify_tbl -> Term.constr
+val make_t_i : SmtBtype.reify_tbl -> Term.constr
 val make_t_func : Op.reify_tbl -> Term.constr -> Term.constr
diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml
new file mode 100644
index 0000000..92b8ad7
--- /dev/null
+++ b/src/trace/smtBtype.ml
@@ -0,0 +1,113 @@
+open SmtMisc
+open CoqTerms
+
+(** Syntaxified version of Coq type *)
+
+type indexed_type = Term.constr gen_hashed
+
+let dummy_indexed_type i = {index = i; hval = Term.mkProp}
+let indexed_type_index i = i.index
+let indexed_type_hval i = i.hval
+
+type btype =
+  | TZ
+  | Tbool
+  | Tpositive
+  | Tindex of indexed_type
+
+let index_tbl = Hashtbl.create 17
+
+let index_to_coq i =
+  let i = i.index in 
+  try Hashtbl.find index_tbl i
+  with Not_found ->
+    let interp = mklApp cTindex [|mkInt i|] in
+    Hashtbl.add index_tbl i interp;
+    interp
+
+let equal t1 t2 =
+  match t1,t2 with
+  | Tindex i, Tindex j -> i.index == j.index
+  | _ -> t1 == t2
+
+let to_coq = function
+  | TZ -> Lazy.force cTZ
+  | Tbool -> Lazy.force cTbool
+  | Tpositive -> Lazy.force cTpositive
+  | Tindex i -> index_to_coq i
+
+let to_smt fmt = function
+  | TZ -> Format.fprintf fmt "Int"
+  | Tbool -> Format.fprintf fmt "Bool"
+  | Tpositive -> Format.fprintf fmt "Int"
+  | Tindex i -> Format.fprintf fmt "Tindex_%i" i.index
+
+(* reify table *)
+type reify_tbl =
+  { mutable count : int;
+    tbl : (Term.constr, btype) Hashtbl.t;
+    mutable cuts : (Structures.names_id_t * Term.types) list
+  }
+
+let create () =
+  let htbl = Hashtbl.create 17 in
+  Hashtbl.add htbl (Lazy.force cZ) TZ;
+  Hashtbl.add htbl (Lazy.force cbool) Tbool;
+  (* Hashtbl.add htbl (Lazy.force cpositive) Tpositive; *)
+  { count = 0;
+    tbl = htbl;
+    cuts = [] }
+
+let get_cuts reify = reify.cuts
+
+let declare reify t typ_eqb =
+  (* TODO: allows to have only typ_eqb *)
+  assert (not (Hashtbl.mem reify.tbl t));
+  let res = Tindex {index = reify.count; hval = typ_eqb} in
+  Hashtbl.add reify.tbl t res;
+  reify.count <- reify.count + 1;
+  res
+
+let of_coq reify t =
+  try
+    Hashtbl.find reify.tbl t
+  with | Not_found ->
+          let n = string_of_int (List.length reify.cuts) in
+          let eq_name = Names.id_of_string ("eq"^n) in
+          let eq_var = Term.mkVar eq_name in
+
+          let eq_ty = Term.mkArrow t (Term.mkArrow t (Lazy.force cbool)) in
+
+          let eq = mkName "eq" in
+          let x = mkName "x" in
+          let y = mkName "y" in
+          let req = Term.mkRel 3 in
+          let rx = Term.mkRel 2 in
+          let ry = Term.mkRel 1 in
+          let refl_ty = Term.mkLambda (eq, eq_ty, Term.mkProd (x,t,Term.mkProd (y,t,mklApp creflect [|mklApp ceq [|t;rx;ry|]; Term.mkApp (req, [|rx;ry|])|]))) in
+
+          let pair_ty = mklApp csigT [|eq_ty; refl_ty|] in
+
+          reify.cuts <- (eq_name, pair_ty)::reify.cuts;
+          let ce = mklApp ctyp_eqb_of_typ_eqb_param [|t; eq_var|] in
+          declare reify t ce
+
+let interp_tbl reify =
+  let t = Array.make (reify.count + 1) (Lazy.force cunit_typ_eqb) in
+  let set _ = function
+    | Tindex it -> t.(it.index) <- it.hval
+    | _ -> () in
+  Hashtbl.iter set reify.tbl;
+  Structures.mkArray (Lazy.force ctyp_eqb, t)
+
+let to_list reify =
+  let set _ t acc = match t with
+    | Tindex it -> (it.index,it)::acc
+    | _ -> acc in
+  Hashtbl.fold set reify.tbl []
+
+let interp_to_coq reify = function
+  | TZ -> Lazy.force cZ
+  | Tbool -> Lazy.force cbool
+  | Tpositive -> Lazy.force cpositive
+  | Tindex c -> mklApp cte_carrier [|c.hval|]
diff --git a/src/trace/smtBtype.mli b/src/trace/smtBtype.mli
new file mode 100644
index 0000000..11d596f
--- /dev/null
+++ b/src/trace/smtBtype.mli
@@ -0,0 +1,16 @@
+type indexed_type
+val dummy_indexed_type : int -> indexed_type
+val indexed_type_index : indexed_type -> int
+val indexed_type_hval : indexed_type -> Term.constr
+type btype = TZ | Tbool | Tpositive | Tindex of indexed_type
+val equal : btype -> btype -> bool
+val to_coq : btype -> Term.constr
+val to_smt : Format.formatter -> btype -> unit
+type reify_tbl
+val create : unit -> reify_tbl
+val declare : reify_tbl -> Term.constr -> Term.constr -> btype
+val of_coq : reify_tbl -> Term.constr -> btype
+val interp_tbl : reify_tbl -> Term.constr
+val to_list : reify_tbl -> (int * indexed_type) list
+val interp_to_coq : reify_tbl -> btype -> Term.constr
+val get_cuts : reify_tbl -> (Structures.names_id_t * Term.types) list
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index 8950022..ba86a5b 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -383,7 +383,7 @@ let core_tactic call_solver rt ro ra rf env sigma concl =
       let max_id_confl = make_proof call_solver rt ro rf l in
       build_body_eq rt ro ra rf (Form.to_coq l1) (Form.to_coq l2) (Form.to_coq l) max_id_confl in
 
-  let cuts = (Btype.get_cuts rt)@cuts in
+  let cuts = SmtBtype.get_cuts rt @ cuts in
 
   List.fold_right (fun (eqn, eqt) tac ->
       Structures.tclTHENLAST (Structures.assert_before (Names.Name eqn) eqt) tac)
diff --git a/src/trace/smtCommands.mli b/src/trace/smtCommands.mli
index d6fa756..3cac245 100644
--- a/src/trace/smtCommands.mli
+++ b/src/trace/smtCommands.mli
@@ -32,21 +32,21 @@ val parse_certif :
   Names.identifier ->
   Names.identifier ->
   Names.identifier ->
-  SmtAtom.Btype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl *
+  SmtBtype.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 *
+  SmtBtype.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 *
+  SmtBtype.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 ->
+  SmtBtype.reify_tbl ->
   SmtAtom.Op.reify_tbl ->
   SmtAtom.Atom.reify_tbl ->
   SmtAtom.Form.reify ->
@@ -55,7 +55,7 @@ val build_body :
   int * SmtAtom.Form.t SmtCertif.clause ->
   Term.constr * Term.constr * (Names.identifier * Term.types) list
 val build_body_eq :
-  SmtAtom.Btype.reify_tbl ->
+  SmtBtype.reify_tbl ->
   SmtAtom.Op.reify_tbl ->
   SmtAtom.Atom.reify_tbl ->
   SmtAtom.Form.reify ->
@@ -71,22 +71,22 @@ val make_proof :
    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 ->
+  (SmtBtype.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 ->
+  SmtBtype.reify_tbl ->
   SmtAtom.Op.reify_tbl ->
   SmtAtom.Atom.reify_tbl ->
   SmtAtom.Form.reify ->
   Environ.env -> Evd.evar_map -> Term.constr -> Structures.tactic
 val tactic :
-  (SmtAtom.Btype.reify_tbl ->
+  (SmtBtype.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 ->
+  SmtBtype.reify_tbl ->
   SmtAtom.Op.reify_tbl ->
   SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> Structures.tactic
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index 643ce8f..88d0769 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -81,7 +81,7 @@ let clear_all () =
 
 let import_all fsmt fproof =
   clear_all ();
-  let rt = Btype.create () in
+  let rt = SmtBtype.create () in
   let ro = Op.create () in
   let ra = VeritSyntax.ra in
   let rf = VeritSyntax.rf in
@@ -109,16 +109,16 @@ let export out_channel rt ro l =
     let s = "Tindex_"^(string_of_int i) in
     VeritSyntax.add_btype s (Tindex t);
     Format.fprintf fmt "(declare-sort %s 0)@." s
-  ) (Btype.to_list rt);
+  ) (SmtBtype.to_list rt);
 
   List.iter (fun (i,cod,dom,op) ->
     let s = "op_"^(string_of_int i) in
     VeritSyntax.add_fun s op;
     Format.fprintf fmt "(declare-fun %s (" s;
     let is_first = ref true in
-    Array.iter (fun t -> if !is_first then is_first := false else Format.fprintf fmt " "; Btype.to_smt fmt t) cod;
+    Array.iter (fun t -> if !is_first then is_first := false else Format.fprintf fmt " "; SmtBtype.to_smt fmt t) cod;
     Format.fprintf fmt ") ";
-    Btype.to_smt fmt dom;
+    SmtBtype.to_smt fmt dom;
     Format.fprintf fmt ")@."
   ) (Op.to_list ro);
 
@@ -150,7 +150,7 @@ let call_verit rt ro fl root =
 
 let tactic () =
   clear_all ();
-  let rt = Btype.create () in
+  let rt = SmtBtype.create () in
   let ro = Op.create () in
   let ra = VeritSyntax.ra in
   let rf = VeritSyntax.rf in
diff --git a/src/verit/verit.mli b/src/verit/verit.mli
index 126a02b..68ee317 100644
--- a/src/verit/verit.mli
+++ b/src/verit/verit.mli
@@ -7,7 +7,7 @@ val clear_all : unit -> unit
 val import_all :
   string ->
   string ->
-  SmtAtom.Btype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl *
+  SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl *
   SmtAtom.Form.reify * SmtAtom.Form.t list * int *
   SmtAtom.Form.t SmtCertif.clause
 val parse_certif :
@@ -21,10 +21,10 @@ val theorem : Names.identifier -> string -> string -> unit
 val checker : string -> string -> unit
 val export :
   out_channel ->
-  SmtAtom.Btype.reify_tbl -> SmtAtom.Op.reify_tbl ->
+  SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl ->
   SmtAtom.Form.t -> unit
 val call_verit :
-  SmtAtom.Btype.reify_tbl ->
+  SmtBtype.reify_tbl ->
   SmtAtom.Op.reify_tbl ->
   SmtAtom.Form.t ->
   SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t ->
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml
index e03cbec..b598e2c 100644
--- a/src/verit/veritSyntax.ml
+++ b/src/verit/veritSyntax.ml
@@ -335,7 +335,7 @@ let get_solver id =
 let add_solver id cl = Hashtbl.add solver id cl
 let clear_solver () = Hashtbl.clear solver
 
-let btypes : (string,btype) Hashtbl.t = Hashtbl.create 17
+let btypes : (string, SmtBtype.btype) Hashtbl.t = Hashtbl.create 17
 let get_btype id =
   try Hashtbl.find btypes id
   with | Not_found -> failwith ("VeritSyntax.get_btype : sort symbol \""^id^"\" not found\n")
diff --git a/src/verit/veritSyntax.mli b/src/verit/veritSyntax.mli
index 281deef..c7bf659 100644
--- a/src/verit/veritSyntax.mli
+++ b/src/verit/veritSyntax.mli
@@ -31,8 +31,8 @@ val lit_of_atom_form_lit : SmtAtom.Form.reify -> atom_form_lit -> SmtAtom.Form.t
 val get_solver : int -> atom_form_lit
 val add_solver : int -> atom_form_lit -> unit
 
-val get_btype : string -> SmtAtom.btype
-val add_btype : string -> SmtAtom.btype -> unit
+val get_btype : string -> SmtBtype.btype
+val add_btype : string -> SmtBtype.btype -> unit
 
 val get_fun : string -> SmtAtom.indexed_op
 val add_fun : string -> SmtAtom.indexed_op -> unit
diff --git a/src/versions/native/Make b/src/versions/native/Make
index c6ce237..69cbbfb 100644
--- a/src/versions/native/Make
+++ b/src/versions/native/Make
@@ -40,7 +40,7 @@
 -custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli"
 -custom "" "verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml" "ml"
 
--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 smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx smtcoq_plugin.cmx" "$(CMXA)"
+-custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtBtype.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 smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx smtcoq_plugin.cmx" "$(CMXA)"
 -custom "$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)"
 
 CMXA = smtcoq.cmxa
@@ -59,6 +59,8 @@ trace/satAtom.ml
 trace/satAtom.mli
 trace/smtAtom.ml
 trace/smtAtom.mli
+trace/smtBtype.ml
+trace/smtBtype.mli
 trace/smtCertif.ml
 trace/smtCertif.mli
 trace/smtCnf.ml
diff --git a/src/versions/native/Makefile b/src/versions/native/Makefile
index d443fe9..61c8c01 100644
--- a/src/versions/native/Makefile
+++ b/src/versions/native/Makefile
@@ -185,6 +185,7 @@ MLFILES:=lia/lia.ml\
   trace/smtCommands.ml\
   trace/smtCnf.ml\
   trace/smtCertif.ml\
+  trace/smtBtype.ml\
   trace/smtAtom.ml\
   trace/satAtom.ml\
   trace/coqTerms.ml\
@@ -213,6 +214,7 @@ MLIFILES:=lia/lia.mli\
   trace/smtCommands.mli\
   trace/smtCnf.mli\
   trace/smtCertif.mli\
+  trace/smtBtype.mli\
   trace/smtAtom.mli\
   trace/satAtom.mli\
   trace/coqTerms.mli\
@@ -285,7 +287,7 @@ beautify: $(VFILES:=.beautified)
 $(CMXS): $(CMXA)
 	$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^
 
-$(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 smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx smtcoq_plugin.cmx
+$(CMXA): versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtBtype.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 smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx smtcoq_plugin.cmx
 	$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^
 
 ml: verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml
diff --git a/src/versions/standard/Make b/src/versions/standard/Make
index 37822db..b674ce9 100644
--- a/src/versions/standard/Make
+++ b/src/versions/standard/Make
@@ -60,6 +60,8 @@ versions/standard/structures.mli
 
 trace/coqTerms.ml
 trace/coqTerms.mli
+trace/smtBtype.ml
+trace/smtBtype.mli
 trace/satAtom.ml
 trace/satAtom.mli
 trace/smtAtom.ml
diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile
index 9d2a5de..0225e3c 100644
--- a/src/versions/standard/Makefile
+++ b/src/versions/standard/Makefile
@@ -235,6 +235,7 @@ endif
 
 MLFILES:=versions/standard/structures.ml\
   trace/coqTerms.ml\
+  trace/smtBtype.ml\
   trace/satAtom.ml\
   trace/smtAtom.ml\
   trace/smtCertif.ml\
@@ -282,6 +283,7 @@ endif
 
 MLIFILES:=versions/standard/structures.mli\
   trace/coqTerms.mli\
+  trace/smtBtype.mli\
   trace/satAtom.mli\
   trace/smtAtom.mli\
   trace/smtCertif.mli\
diff --git a/src/versions/standard/smtcoq_plugin_standard.mlpack b/src/versions/standard/smtcoq_plugin_standard.mlpack
index 3ab358b..b316040 100644
--- a/src/versions/standard/smtcoq_plugin_standard.mlpack
+++ b/src/versions/standard/smtcoq_plugin_standard.mlpack
@@ -2,6 +2,7 @@ Structures
 
 SmtMisc
 CoqTerms
+SmtBtype
 SmtForm
 SmtCertif
 SmtTrace