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

6 files changed, 158 insertions, 179 deletions

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