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

1 files changed, 16 insertions, 129 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