diff options
Diffstat (limited to 'src/trace/smtBtype.ml')
| -rw-r--r-- | src/trace/smtBtype.ml | 216 |
1 files changed, 167 insertions, 49 deletions
diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml index f3245ea..8580ed0 100644 --- a/src/trace/smtBtype.ml +++ b/src/trace/smtBtype.ml @@ -1,3 +1,15 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2019 *) +(* *) +(* See file "AUTHORS" for the list of authors *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + open SmtMisc open CoqTerms @@ -13,6 +25,8 @@ type btype = | TZ | Tbool | Tpositive + | TBV of int + | TFArray of btype * btype | Tindex of indexed_type let index_tbl = Hashtbl.create 17 @@ -26,31 +40,45 @@ let index_to_coq i = let indexed_type_of_int i = {index = i; hval = index_to_coq i } - -let equal t1 t2 = + +let rec equal t1 t2 = match t1,t2 with - | Tindex i, Tindex j -> i.index == j.index - | _ -> t1 == t2 + | Tindex i, Tindex j -> i.index == j.index + | TBV i, TBV j -> i == j + | TFArray (ti, te), TFArray (ti', te') -> equal ti ti' && equal te te' + | _ -> t1 == t2 -let to_coq = function +let rec to_coq = function | TZ -> Lazy.force cTZ | Tbool -> Lazy.force cTbool | Tpositive -> Lazy.force cTpositive + | TBV n -> mklApp cTBV [|mkN n|] | Tindex i -> index_to_coq i.index - -let to_string = function - | TZ -> "Int" - | Tbool -> "Bool" - | Tpositive -> "Int" - | Tindex i -> "Tindex_" ^ string_of_int i.index - -let to_smt fmt b = Format.fprintf fmt "%s" (to_string b) + | TFArray (ti, te) -> + mklApp cTFArray [|to_coq ti; to_coq te|] + +let rec to_smt fmt = function + | TZ -> Format.fprintf fmt "Int" + | Tbool -> Format.fprintf fmt "Bool" + | Tpositive -> Format.fprintf fmt "Int" + | TBV i -> Format.fprintf fmt "(_ BitVec %i)" i + | Tindex i -> Format.fprintf fmt "Tindex_%i" i.index + | TFArray (ti, te) -> + Format.fprintf fmt "(Array %a %a)" to_smt ti to_smt te + +let rec logic = function + | TZ | Tpositive -> SL.singleton LLia + | Tbool -> SL.empty + | TBV _ -> SL.singleton LBitvectors + | Tindex _ -> SL.singleton LUF + | TFArray (ti, te) -> SL.add LArrays (SL.union (logic ti) (logic te)) (* reify table *) type reify_tbl = { mutable count : int; tbl : (Term.constr, btype) Hashtbl.t; - mutable cuts : (Structures.names_id_t * Term.types) list + mutable cuts : (Structures.names_id_t * Term.types) list; + unsup_tbl : (btype, btype) Hashtbl.t; } let create () = @@ -60,58 +88,148 @@ let create () = (* 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 + cuts = []; + unsup_tbl = Hashtbl.create 17; + } -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 +(* Should we give a way to clear it? *) +let op_coq_types = Hashtbl.create 17 +let get_coq_type_op = Hashtbl.find op_coq_types - 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 +(* let logic_of_coq reify t = logic (of_coq reify t) *) - 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 t = Array.make (reify.count + 1) (Lazy.force cunit_typ_compdec) in let set _ = function | Tindex it -> t.(it.index) <- it.hval | _ -> () in Hashtbl.iter set reify.tbl; - Structures.mkArray (Lazy.force ctyp_eqb, t) + Structures.mkArray (Lazy.force ctyp_compdec, t) + let to_list reify = let set _ t acc = match t with - | Tindex it -> (it.index,it)::acc - | _ -> acc in + | Tindex it -> (it.index,it)::acc + | _ -> acc in Hashtbl.fold set reify.tbl [] -let interp_to_coq reify = function +let make_t_i rt = interp_tbl rt + + +let interp_t t_i t = + mklApp cinterp_t [|t_i ; to_coq t|] + +let dec_interp t_i t = + mklApp cdec_interp [|t_i ; to_coq t|] + +let ord_interp t_i t = + mklApp cord_interp [|t_i ; to_coq t|] + +let comp_interp t_i t = + mklApp ccomp_interp [|t_i ; to_coq t|] + +let inh_interp t_i t = + mklApp cinh_interp [|t_i ; to_coq t|] + +let rec interp t_i = function | TZ -> Lazy.force cZ | Tbool -> Lazy.force cbool | Tpositive -> Lazy.force cpositive + | TBV n -> mklApp cbitvector [|mkN n|] | Tindex c -> mklApp cte_carrier [|c.hval|] + (* | TFArray _ as t -> interp_t t_i t *) + | TFArray (ti,te) -> + mklApp cfarray [| interp t_i ti; interp t_i te; + ord_interp t_i ti; inh_interp t_i te |] + + +let interp_to_coq reify t = interp (make_t_i reify) t + +let get_cuts reify = reify.cuts + +let declare reify t typ_compdec = + (* TODO: allows to have only typ_compdec *) + assert (not (Hashtbl.mem reify.tbl t)); + let res = Tindex {index = reify.count; hval = typ_compdec} in + Hashtbl.add reify.tbl t res; + reify.count <- reify.count + 1; + res + +exception Unknown_type of btype + +let check_known ty known_logic = + let l = logic ty in + if not (SL.subset l known_logic) then raise (Unknown_type ty) + else ty + +let rec compdec_btype reify = function + | Tbool -> Lazy.force cbool_compdec + | TZ -> Lazy.force cZ_compdec + | Tpositive -> Lazy.force cPositive_compdec + | TBV s -> mklApp cBV_compdec [|mkN s|] + | TFArray (ti, te) -> + mklApp cFArray_compdec + [|interp_to_coq reify ti; interp_to_coq reify te; + compdec_btype reify ti; compdec_btype reify te|] + | Tindex i -> + let c, args = Term.decompose_app i.hval in + if Term.eq_constr c (Lazy.force cTyp_compdec) then + match args with + | [_; tic] -> tic + | _ -> assert false + else assert false + + +let declare_and_compdec reify t ty = + try Hashtbl.find reify.unsup_tbl ty + with Not_found -> + let res = + declare reify t (mklApp cTyp_compdec [|t; compdec_btype reify ty|]) + in + Hashtbl.add reify.unsup_tbl ty res; + res + + +let rec of_coq reify known_logic t = + try + let c, args = Term.decompose_app t in + if Term.eq_constr c (Lazy.force cbool) || + Term.eq_constr c (Lazy.force cTbool) then Tbool + else if Term.eq_constr c (Lazy.force cZ) || + Term.eq_constr c (Lazy.force cTZ) then + check_known TZ known_logic + else if Term.eq_constr c (Lazy.force cpositive) || + Term.eq_constr c (Lazy.force cTpositive) then + check_known Tpositive known_logic + else if Term.eq_constr c (Lazy.force cbitvector) || + Term.eq_constr c (Lazy.force cTBV) then + match args with + | [s] -> check_known (TBV (mk_bvsize s)) known_logic + | _ -> assert false + else if Term.eq_constr c (Lazy.force cfarray) || + Term.eq_constr c (Lazy.force cTFArray) then + match args with + | ti :: te :: _ -> + let ty = TFArray (of_coq reify known_logic ti, + of_coq reify known_logic te) in + check_known ty known_logic + | _ -> assert false + else + try Hashtbl.find reify.tbl t + with Not_found -> + let n = string_of_int (List.length reify.cuts) in + let compdec_name = Names.id_of_string ("CompDec"^n) in + let compdec_var = Term.mkVar compdec_name in + let compdec_type = mklApp cCompDec [| t |]in + reify.cuts <- (compdec_name, compdec_type) :: reify.cuts; + let ce = mklApp cTyp_compdec [|t; compdec_var|] in + let ty = declare reify t ce in + (match ty with Tindex h -> Hashtbl.add op_coq_types h.index t | _ -> assert false); + ty + + with Unknown_type ty -> + try Hashtbl.find reify.tbl t + with Not_found -> declare_and_compdec reify t ty |