1 files changed, 113 insertions, 0 deletions
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|]