diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-02-23 18:02:59 +0100 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-02-23 18:02:59 +0100 |
commit | dbf1adc5daaadf92bc3245648f30cf79bd010e86 (patch) | |
tree | d4e54f6ace255a98adaebf22bf6c915cbb08a81b /src/trace/smtBtype.ml | |
parent | 68ca86514065cef3d5fc6ce54a86ef15452d8f0a (diff) | |
parent | 240b76807340e59bb85b35e3ebbb807792459912 (diff) | |
download | smtcoq-dbf1adc5daaadf92bc3245648f30cf79bd010e86.tar.gz smtcoq-dbf1adc5daaadf92bc3245648f30cf79bd010e86.zip |
Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10
Diffstat (limited to 'src/trace/smtBtype.ml')
-rw-r--r-- | src/trace/smtBtype.ml | 146 |
1 files changed, 110 insertions, 36 deletions
diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml index 948acaa..3c4cd53 100644 --- a/src/trace/smtBtype.ml +++ b/src/trace/smtBtype.ml @@ -15,11 +15,28 @@ open CoqTerms (** Syntaxified version of Coq type *) -type indexed_type = Structures.constr gen_hashed - -let dummy_indexed_type i = {index = i; hval = Structures.mkProp} +type uninterpreted_type = + (* Uninterpreted type for which a CompDec is already known + The constr is of type typ_compdec + *) + | CompDec of Structures.constr + (* Uninterpreted type for which the knowledge of a CompDec is delayed + until either: + - one is used + - we have reached the end of the process and we generate a new one + via a cut + The constr is of type Type + *) + | Delayed of Structures.constr + +type indexed_type = uninterpreted_type gen_hashed + +let dummy_indexed_type i = {index = i; hval = Delayed (Structures.mkProp)} let indexed_type_index i = i.index -let indexed_type_hval i = i.hval +let indexed_type_compdec i = + match i.hval with + | CompDec compdec -> compdec + | Delayed _ -> assert false type btype = | TZ @@ -39,14 +56,26 @@ let index_to_coq i = interp let indexed_type_of_int i = - {index = i; hval = index_to_coq i } - -let rec equal t1 t2 = - match t1,t2 with - | 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 + {index = i; hval = Delayed (index_to_coq i) } + +module HashedBtype : Hashtbl.HashedType with type t = btype = struct + type t = btype + + let rec equal t1 t2 = + match t1,t2 with + | 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 rec hash = function + | TZ -> 1 + | Tbool -> 2 + | Tpositive -> 3 + | TBV s -> s lxor 4 + | TFArray (t1, t2) -> ((((hash t1) lsl 3) land (hash t2)) lsl 3) lxor 5 + | Tindex i -> (i.index lsl 3) lxor 6 +end let rec to_coq = function | TZ -> Lazy.force cTZ @@ -103,10 +132,24 @@ let get_coq_type_op = Hashtbl.find op_coq_types let interp_tbl reify = 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; + let set c bt = + match bt with + | Tindex it -> + (match it.hval with + | CompDec compdec -> t.(it.index) <- compdec; Some bt + | Delayed ty -> + let n = string_of_int (List.length reify.cuts) in + let compdec_name = Structures.mkId ("CompDec"^n) in + let compdec_var = Structures.mkVar compdec_name in + let compdec_type = mklApp cCompDec [| ty |] in + reify.cuts <- (compdec_name, compdec_type) :: reify.cuts; + let ce = mklApp cTyp_compdec [|ty; compdec_var|] in + t.(it.index) <- ce; + Some (Tindex {index = it.index; hval = CompDec ce}) + ) + | _ -> Some bt + in + Hashtbl.filter_map_inplace set reify.tbl; Structures.mkArray (Lazy.force ctyp_compdec, t) @@ -139,7 +182,11 @@ let rec interp t_i = function | Tbool -> Lazy.force cbool | Tpositive -> Lazy.force cpositive | TBV n -> mklApp cbitvector [|mkN n|] - | Tindex c -> mklApp cte_carrier [|c.hval|] + | Tindex c -> + (match c.hval with + | CompDec t -> mklApp cte_carrier [|t|] + | Delayed _ -> assert false + ) (* | TFArray _ as t -> interp_t t_i t *) | TFArray (ti,te) -> mklApp cfarray [| interp t_i ti; interp t_i te; @@ -150,14 +197,25 @@ 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 *) +let declare reify t typ_uninterpreted_type = assert (not (Hashtbl.mem reify.tbl t)); - let res = Tindex {index = reify.count; hval = typ_compdec} in + let res = Tindex {index = reify.count; hval = typ_uninterpreted_type} in Hashtbl.add reify.tbl t res; reify.count <- reify.count + 1; res +let declare_compdec reify t compdec = + let ce = mklApp cTyp_compdec [|t; compdec|] in + let ty = declare reify t (CompDec ce) in + (match ty with Tindex h -> Hashtbl.add op_coq_types h.index t | _ -> assert false); + ty + +let declare_delayed reify t delayed = + let ty = declare reify t (Delayed delayed) in + (match ty with Tindex h -> Hashtbl.add op_coq_types h.index t | _ -> assert false); + ty + + exception Unknown_type of btype let check_known ty known_logic = @@ -175,24 +233,29 @@ let rec compdec_btype reify = function [|interp_to_coq reify ti; interp_to_coq reify te; compdec_btype reify ti; compdec_btype reify te|] | Tindex i -> - let c, args = Structures.decompose_app i.hval in - if Structures.eq_constr c (Lazy.force cTyp_compdec) then - match args with - | [_; tic] -> tic - | _ -> assert false - else assert false + (match i.hval with + | CompDec compdec -> + let c, args = Structures.decompose_app compdec in + if Structures.eq_constr c (Lazy.force cTyp_compdec) then + match args with + | [_; tic] -> tic + | _ -> assert false + else assert false + | _ -> 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|]) + declare reify t (CompDec (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 = Structures.decompose_app t in @@ -220,16 +283,27 @@ let rec of_coq reify known_logic t = else try Hashtbl.find reify.tbl t with Not_found -> - let n = string_of_int (List.length reify.cuts) in - let compdec_name = Structures.mkId ("CompDec"^n) in - let compdec_var = Structures.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 + declare_delayed reify t t with Unknown_type ty -> try Hashtbl.find reify.tbl t with Not_found -> declare_and_compdec reify t ty + + +let of_coq_compdec reify t compdec = + try + let ty = Hashtbl.find reify.tbl t in + match ty with + | Tindex i -> + (match i.hval with + | CompDec _ -> ty + | Delayed _ -> + Hashtbl.remove reify.tbl t; + let ce = mklApp cTyp_compdec [|t; compdec|] in + let res = Tindex {index = i.index; hval = CompDec ce} in + Hashtbl.add reify.tbl t res; + res + ) + | _ -> assert false + with Not_found -> + declare_compdec reify t compdec |