Skip to content

why3
why3
Commit 969c5c0b authored by Jean-Christophe Filliatre's avatar Jean-Christophe Filliatre
Browse files
Options

program API (in progress)

parent f4b22c4d
Hide whitespace changes
Inline Side-by-side
Showing with 91 additions and 203 deletions
src/whyml/mlw_ty.ml
View file @ 969c5c0b
......@@ -22,70 +22,32 @@ open Util
open Ident
open Ty
(** region variables *)
(** value types (w/o effects) *)
type rvsymbol = {
rv_name : ident;
type vtysymbol = {
vts_pure : tysymbol;
vts_args : tvsymbol list;
vts_regs : region list;
vts_def : vty option;
}
module Rvar = WeakStructMake (struct
type t = rvsymbol
let tag rv = rv.rv_name.id_tag
end)
module Srv = Rvar.S
module Mrv = Rvar.M
module Hrv = Rvar.H
module Wrv = Rvar.W
let rv_equal : rvsymbol -> rvsymbol -> bool = (==)
let rv_hash rv = id_hash rv.rv_name
let create_rvsymbol n = { rv_name = id_register n }
(** subregion projections *)
type srsymbol = {
srs_name : ident;
and vty = {
vty_node : vty_node;
vty_tag : Hashweak.tag;
}
let srs_equal : srsymbol -> srsymbol -> bool = (==)
let srs_hash srs = id_hash srs.srs_name
let create_srsymbol n = { srs_name = id_register n }
(** regions *)
and vty_node =
| Vtyvar of tvsymbol
| Vtypur of tysymbol * vty list
| Vtyapp of vtysymbol * vty list * region list
| Vtymod of tysymbol * vty
type region = {
reg_node : reg_node;
reg_tag : Hashweak.tag;
and region = {
reg_ty : vty;
reg_tag : Hashweak.tag;
}
and reg_node =
| Rvar of rvsymbol
| Rsub of srsymbol * region
let reg_equal : region -> region -> bool = (==)
let reg_hash r = Hashweak.tag_hash r.reg_tag
module Hregion = Hashcons.Make (struct
type t = region
let equal r1 r2 = match r1.reg_node, r2.reg_node with
| Rvar n1, Rvar n2 -> rv_equal n1 n2
| Rsub (s1,r1), Rsub (s2,r2) ->
srs_equal s1 s2 && reg_equal r1 r2
| _ -> false
let hash r = match r.reg_node with
| Rvar v -> rv_hash v
| Rsub (s,r) -> Hashcons.combine (srs_hash s) (reg_hash r)
let tag n r = { r with reg_tag = Hashweak.create_tag n }
end)
(** regions *)
module Reg = WeakStructMake (struct
type t = region
......@@ -97,43 +59,16 @@ module Mreg = Reg.M
module Hreg = Reg.H
module Wreg = Reg.W
let mk_reg n = {
reg_node = n;
reg_tag = Hashweak.dummy_tag;
}
let reg_var n = Hregion.hashcons (mk_reg (Rvar n))
let reg_sub s r = Hregion.hashcons (mk_reg (Rsub (s,r)))
let rec reg_getrv r = match r.reg_node with
| Rvar v -> v
| Rsub (_,r) -> reg_getrv r
let rec reg_v_map fn r = match r.reg_node with
| Rvar v -> fn v
| Rsub (s,r) -> reg_sub s (reg_v_map fn r)
let reg_full_inst m r = reg_v_map (fun v -> Mrv.find v m) r
(** value types (w/o effects) *)
type vtysymbol = {
vts_pure : tysymbol;
vts_args : tvsymbol list;
vts_regs : rvsymbol list;
vts_def : vty option;
vts_model : bool;
}
let reg_equal : region -> region -> bool = (==)
let reg_hash r = Hashweak.tag_hash r.reg_tag
and vty = {
vty_node : vty_node;
vty_tag : Hashweak.tag;
}
let create_region =
let r = ref 0 in
fun ty ->
incr r;
{ reg_ty = ty; reg_tag = Hashweak.create_tag !r }
and vty_node =
| Vtyvar of tvsymbol
| Vtypur of tysymbol * vty list
| Vtyapp of vtysymbol * vty list * region list
(* value type symbols *)
module VTsym = WeakStructMake (struct
type t = vtysymbol
......@@ -169,6 +104,8 @@ module Hsvty = Hashcons.Make (struct
| Vtyapp (s,tl,rl) ->
Hashcons.combine_list reg_hash
(Hashcons.combine_list vty_hash (vts_hash s) tl) rl
| Vtymod (ts, vty) ->
Hashcons.combine (ts_hash ts) (vty_hash vty)
let tag n vty = { vty with vty_tag = Hashweak.create_tag n }
end)
......@@ -191,6 +128,7 @@ let mk_vty n = {
let vty_var n = Hsvty.hashcons (mk_vty (Vtyvar n))
let vty_pur s tl = Hsvty.hashcons (mk_vty (Vtypur (s,tl)))
let vty_app s tl rl = Hsvty.hashcons (mk_vty (Vtyapp (s,tl,rl)))
let vty_mod ts vty = Hsvty.hashcons (mk_vty (Vtymod (ts,vty)))
(* generic traversal functions *)
......@@ -198,11 +136,13 @@ let vty_map fn vty = match vty.vty_node with
| Vtyvar _ -> vty
| Vtypur (f,tl) -> vty_pur f (List.map fn tl)
| Vtyapp (f,tl,rl) -> vty_app f (List.map fn tl) rl
| Vtymod (ts, vty) -> vty_mod ts (fn vty)
let vty_fold fn acc vty = match vty.vty_node with
| Vtyvar _ -> acc
| Vtypur (_,tl)
| Vtyapp (_,tl,_) -> List.fold_left fn acc tl
| Vtymod (_,vty) -> fn acc vty
let vty_all pr vty =
try vty_fold (all_fn pr) true vty with FoldSkip -> false
......@@ -219,6 +159,8 @@ let rec vty_v_map fnv fnr vty = match vty.vty_node with
vty_pur f (List.map (vty_v_map fnv fnr) tl)
| Vtyapp (f,tl,rl) ->
vty_app f (List.map (vty_v_map fnv fnr) tl) (List.map fnr rl)
| Vtymod (ts, vty) ->
vty_mod ts (vty_v_map fnv fnr vty)
let rec vty_v_fold fnv fnr acc vty = match vty.vty_node with
| Vtyvar v ->
......@@ -227,6 +169,8 @@ let rec vty_v_fold fnv fnr acc vty = match vty.vty_node with
List.fold_left (vty_v_fold fnv fnr) acc tl
| Vtyapp (_,tl,rl) ->
List.fold_left (vty_v_fold fnv fnr) (List.fold_left fnr acc rl) tl
| Vtymod (_, vty) ->
vty_v_fold fnv fnr acc vty
let vty_v_all prv prr vty =
try vty_v_fold (all_fn prv) (all_fn prr) true vty with FoldSkip -> false
......@@ -235,7 +179,7 @@ let vty_v_any prv prr vty =
try vty_v_fold (any_fn prv) (any_fn prr) false vty with FoldSkip -> true
let vty_full_inst mv mr vty =
vty_v_map (fun v -> Mtv.find v mv) (reg_full_inst mr) vty
vty_v_map (fun v -> Mtv.find v mv) (fun r -> Mreg.find r mr) vty
let vty_freevars s vty = vty_v_fold (fun s v -> Stv.add v s) Util.const s vty
......@@ -247,84 +191,71 @@ let vty_pure vty = vty_v_all Util.ttrue Util.ffalse vty
exception BadVtyArity of vtysymbol * int * int
exception BadRegArity of vtysymbol * int * int
exception DuplicateRegVar of rvsymbol
exception UnboundRegVar of rvsymbol
exception DuplicateRegion of region
exception UnboundRegion of region
exception InvalidRegion of region
let rec ty_of_vty vty = match vty.vty_node with
| Vtyvar v -> ty_var v
| Vtypur (s,tl) -> ty_app s (List.map ty_of_vty tl)
| Vtyapp (s,tl,_) -> ty_app s.vts_pure (List.map ty_of_vty tl)
| Vtymod (_,vty) -> ty_of_vty vty
let rec vty_of_ty ty = match ty.ty_node with
| Tyvar v -> vty_var v
| Tyapp (s,tl) -> vty_pur s (List.map vty_of_ty tl)
let rec vty_app_real s tl rl model =
let vty_app s tl rl =
let tll = List.length tl in
let rll = List.length rl in
let stl = List.length s.vts_args in
let srl = List.length s.vts_regs in
if tll <> stl then raise (BadVtyArity (s,stl,tll));
if rll <> srl then raise (BadRegArity (s,srl,rll));
let expand = not s.vts_model || model in
let subexp = not s.vts_model && model in
match s.vts_def with
| Some vty when expand ->
| Some vty ->
let add m v t = Mtv.add v t m in
let mv = List.fold_left2 add Mtv.empty s.vts_args tl in
let add m v r = Mrv.add v r m in
let mr = List.fold_left2 add Mrv.empty s.vts_regs rl in
(* if s is a model alias, vty is already expanded *)
let vty = if subexp then vty_model vty else vty in
let add m v r = Mreg.add v r m in
let mr = List.fold_left2 add Mreg.empty s.vts_regs rl in
vty_full_inst mv mr vty
| None when expand && rll = 0 ->
(* if a pure non-model vts is an alias, the RHS can contain
pure model alias types, so we cannot replace vts with ts *)
(* also, model types should never be replaced with pure types *)
vty_pur s.vts_pure tl
| _ ->
| None ->
vty_app s tl rl
and vty_model vty = match vty.vty_node with
let rec vty_unmod vty = match vty.vty_node with
| Vtyvar _ -> vty
| Vtypur (s,tl) -> vty_pur s (List.map vty_model tl)
| Vtyapp (s,tl,rl) -> vty_app_real s (List.map vty_model tl) rl true
| Vtypur (s,tl) -> vty_pur s (List.map vty_unmod tl)
| Vtyapp (s,tl,rl) -> vty_app s (List.map vty_unmod tl) rl
| Vtymod (_,vty) -> vty_unmod vty
let vty_pur s tl = match s.ts_def with
| Some ty ->
let add m v t = Mtv.add v t m in
let m = List.fold_left2 add Mtv.empty s.ts_args tl in
vty_full_inst m Mrv.empty (vty_of_ty ty)
vty_full_inst m Mreg.empty (vty_of_ty ty)
| None ->
vty_pur s tl
let vty_app s tl rl = vty_app_real s tl rl false
let vty_app_model s tl rl = vty_app_real s tl rl true
let create_vtysymbol name args regs def model =
let puredef = option_map ty_of_vty def in
let purets = create_tysymbol name args puredef in
let add s v = Srv.add_new v (DuplicateRegVar v) s in
let s = List.fold_left add Srv.empty regs in
let check r = match r.reg_node with
| Rvar v -> Srv.mem v s || raise (UnboundRegVar v)
| _ -> raise (InvalidRegion r) in
let add s v = Sreg.add_new v (DuplicateRegion v) s in
let s = List.fold_left add Sreg.empty regs in
let check r = Sreg.mem r s || raise (UnboundRegion r) in
ignore (option_map (vty_v_all Util.ttrue check) def);
(* if a type is a model alias, expand everything on the RHS *)
let def = if model then option_map vty_model def else def in
let def = if model then option_map (vty_mod purets) def else def in
{ vts_pure = purets;
vts_args = args;
vts_regs = regs;
vts_def = def;
vts_model = model; }
vts_def = def; }
(*
(* symbol-wise map/fold *)
let rec ty_s_map fn ty = match ty.ty_node with
| Tyvar _ -> ty
| Tyapp (f, tl) -> ty_app (fn f) (List.map (ty_s_map fn) tl)
(*
let rec vty_s_map fn vty = match vty.vty_node with
| Vtyvar _ -> ty
| Vtyapp (f, tl) -> vty_app (fn f) (List.map (vty_s_map fn) tl)
let rec ty_s_fold fn acc ty = match ty.ty_node with
| Tyvar _ -> acc
......
src/whyml/mlw_ty.mli
View file @ 969c5c0b
......@@ -22,68 +22,13 @@ open Stdlib
open Ident
open Ty
(** region variables *)
type rvsymbol = private {
rv_name : ident;
}
module Mrv : Map.S with type key = rvsymbol
module Srv : Mrv.Set
module Hrv : Hashtbl.S with type key = rvsymbol
module Wrv : Hashweak.S with type key = rvsymbol
val rv_equal : rvsymbol -> rvsymbol -> bool
val rv_hash : rvsymbol -> int
val create_rvsymbol : preid -> rvsymbol
(** subregion projections *)
type srsymbol = private {
srs_name : ident;
}
val srs_equal : srsymbol -> srsymbol -> bool
val srs_hash : srsymbol -> int
val create_srsymbol : preid -> srsymbol
(** regions *)
type region = private {
reg_node : reg_node;
reg_tag : Hashweak.tag;
}
and reg_node = private
| Rvar of rvsymbol
| Rsub of srsymbol * region
val reg_equal : region -> region -> bool
val reg_hash : region -> int
module Mreg : Map.S with type key = region
module Sreg : Mreg.Set
module Hreg : Hashtbl.S with type key = region
module Wreg : Hashweak.S with type key = region
val reg_var : rvsymbol -> region
val reg_sub : srsymbol -> region -> region
val reg_getrv : region -> rvsymbol
(** value types (w/o effects) *)
type vtysymbol = private {
vts_pure : tysymbol;
vts_args : tvsymbol list;
vts_regs : rvsymbol list;
vts_regs : region list;
vts_def : vty option;
vts_model : bool;
}
and vty = private {
......@@ -95,6 +40,12 @@ and vty_node = private
| Vtyvar of tvsymbol
| Vtypur of tysymbol * vty list
| Vtyapp of vtysymbol * vty list * region list
| Vtymod of tysymbol * vty
and region = private {
reg_ty : vty;
reg_tag : Hashweak.tag;
}
module Mvts : Map.S with type key = vtysymbol
module Svts : Mvts.Set
......@@ -106,32 +57,38 @@ module Svty : Mvty.Set
module Hvty : Hashtbl.S with type key = vty
module Wvty : Hashweak.S with type key = vty
module Mreg : Map.S with type key = region
module Sreg : Mreg.Set
module Hreg : Hashtbl.S with type key = region
module Wreg : Hashweak.S with type key = region
val vts_equal : vtysymbol -> vtysymbol -> bool
val vty_equal : vty -> vty -> bool
val vts_hash : vtysymbol -> int
val vty_hash : vty -> int
val reg_equal : region -> region -> bool
val reg_hash : region -> int
exception BadVtyArity of vtysymbol * int * int
exception BadRegArity of vtysymbol * int * int
exception DuplicateRegVar of rvsymbol
exception UnboundRegVar of rvsymbol
exception DuplicateRegion of region
exception UnboundRegion of region
exception InvalidRegion of region
val create_region : vty -> region
val create_vtysymbol :
preid -> tvsymbol list -> rvsymbol list -> vty option -> bool -> vtysymbol
preid -> tvsymbol list -> region list -> vty option -> bool -> vtysymbol
val vty_var : tvsymbol -> vty
val vty_pur : tysymbol -> vty list -> vty
(* this constructor expands type aliases only in non-model types *)
val vty_app : vtysymbol -> vty list -> region list -> vty
(* this constructor expands type aliases even in model types *)
val vty_app_model : vtysymbol -> vty list -> region list -> vty
(* expands all type aliases *)
val vty_model : vty -> vty
(* erases all [Vtymod] *)
val vty_unmod : vty -> vty
(* all aliases expanded, all regions removed *)
val ty_of_vty : vty -> ty
......@@ -157,22 +114,22 @@ val vty_v_fold :
val vty_v_all : (tvsymbol -> bool) -> (region -> bool) -> vty -> bool
val vty_v_any : (tvsymbol -> bool) -> (region -> bool) -> vty -> bool
(*
(** {3 symbol-wise map/fold} *)
(** visits every symbol of the type *)
val ty_s_map : (tysymbol -> tysymbol) -> ty -> ty
val ty_s_fold : ('a -> tysymbol -> 'a) -> 'a -> ty -> 'a
val ty_s_all : (tysymbol -> bool) -> ty -> bool
val ty_s_any : (tysymbol -> bool) -> ty -> bool
(*
val vty_s_map : (vtysymbol -> vtysymbol) -> vty -> vty
val vty_s_fold : ('a -> vtysymbol -> 'a) -> 'a -> vty -> 'a
val vty_s_all : (vtysymbol -> bool) -> vty -> bool
val vty_s_any : (vtysymbol -> bool) -> vty -> bool
exception TypeMismatch of ty * ty
exception TypeMismatch of vty * vty
val ty_match : ty Mrv.t -> ty -> ty -> ty Mrv.t
val ty_inst : ty Mrv.t -> ty -> ty
val ty_freevars : Srv.t -> ty -> Srv.t
val ty_closed : ty -> bool
val vty_match : vty Mreg.t -> vty -> vty -> vty Mreg.t
val vty_inst : vty Mreg.t -> vty -> vty
val vty_freevars : Srv.t -> vty -> Srv.t
val vty_closed : vty -> bool
val ty_equal_check : ty -> ty -> unit
val vty_equal_check : vty -> vty -> unit
*)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment