Commit 6ebd407c authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Ity: specialized itysymbol creation functions

parent 293b3b5a
......@@ -223,7 +223,7 @@ let rec print_dity pri fmt = function
(print_dity 1) t1 (print_dity 0) t2
| Dpur (s,tl) when is_ts_tuple s.its_ts ->
Format.fprintf fmt "(%a)" (Pp.print_list Pp.comma (print_dity 0)) tl
| Dpur (s,tl) when s.its_mutable || s.its_regions <> [] ->
| Dpur (s,tl) when its_impure s ->
Format.fprintf fmt (protect_on (pri > 1 && tl <> []) "{%a}%a")
Pretty.print_ts s.its_ts (print_args (print_dity 2)) tl
| Dpur (s,tl) ->
......
......@@ -162,10 +162,7 @@ let rs_dup ({rs_name = {id_loc = loc}} as s) c =
check_effects ?loc c;
mk_rs id c RLlemma None
let create_field id s v =
if not (List.exists (fun u -> pv_equal u v) s.its_mfields ||
List.exists (fun u -> pv_equal u v) s.its_ifields) then
invalid_arg "Expr.create_field";
let create_projection id s v =
let eff = eff_ghostify v.pv_ghost eff_empty in
let tyl = List.map ity_var s.its_ts.ts_args in
let ity = ity_app s tyl s.its_regions in
......@@ -173,18 +170,17 @@ let create_field id s v =
let ls = create_fsymbol id [arg.pv_vs.vs_ty] v.pv_vs.vs_ty in
let q = make_post (fs_app ls [t_var arg.pv_vs] v.pv_vs.vs_ty) in
let c = create_cty [arg] [] [q] Mexn.empty eff v.pv_ity in
mk_rs ls.ls_name c (RLls ls) (Some v)
let fld = if List.exists (pv_equal v) s.its_mfields then Some v else None in
mk_rs ls.ls_name c (RLls ls) fld
let create_constructor ~constr id s fl =
let exn = Invalid_argument "Expr.create_constructor" in
let fs = List.fold_right (Spv.add_new exn) fl Spv.empty in
if s.its_private || s.its_def <> None then raise exn;
if s.its_mutable then begin
if s.its_privmut || s.its_def <> None then raise exn;
if s.its_mfields <> [] then begin
if constr <> 1 then raise exn;
let mfs = Spv.of_list s.its_mfields in
let ifs = Spv.of_list s.its_ifields in
let sfs = Spv.union mfs ifs in
if not (Spv.equal fs sfs) then raise exn
if not (Spv.subset mfs fs) then raise exn
end else if constr < 1 then raise exn;
let argl = List.map (fun a -> a.pv_vs.vs_ty) fl in
let tyl = List.map ity_var s.its_ts.ts_args in
......@@ -366,7 +362,7 @@ let e_locate_effect pr e = fst (find_effect pr None e)
let localize_ghost_write v r el =
let taints eff = Mreg.mem r eff.eff_taints in
let writes eff = match Mreg.find_opt r eff.eff_writes with
| Some fds -> r.reg_its.its_private ||
| Some fds -> r.reg_its.its_privmut ||
Spv.exists (fun fd -> not fd.pv_ghost) fds
| None -> false in
(* check if some component taints region r *)
......
......@@ -58,7 +58,7 @@ val create_rsymbol : preid -> ?ghost:bool -> ?kind:rs_kind -> cty -> rsymbol
val create_constructor :
constr:int -> preid -> itysymbol -> pvsymbol list -> rsymbol
val create_field : preid -> itysymbol -> pvsymbol -> rsymbol
val create_projection : preid -> itysymbol -> pvsymbol -> rsymbol
val restore_rs : lsymbol -> rsymbol
(** raises [Not_found] if the argument is not a [rs_logic] *)
......
This diff is collapsed.
......@@ -17,16 +17,16 @@ open Term
type itysymbol = private {
its_ts : tysymbol; (** pure "snapshot" type symbol *)
its_private : bool; (** is a private/abstract type *)
its_mutable : bool; (** is a record with mutable fields *)
its_mfields : pvsymbol list; (** mutable fields of a mutable type *)
its_ifields : pvsymbol list; (** immutable fields of a mutable type *)
its_privmut : bool; (** private mutable record type *)
its_mfields : pvsymbol list; (** mutable record fields *)
its_regions : region list; (** mutable shareable components *)
its_reg_vis : bool list; (** non-ghost shareable components *)
its_arg_vis : bool list; (** non-ghost type parameters *)
its_arg_upd : bool list; (** updatable type parameters *)
its_arg_imm : bool list; (** non-updatable type parameters *)
its_arg_exp : bool list; (** exposed type parameters *)
its_def : ity option; (** is a type alias *)
its_arg_vis : bool list; (** non-ghost type parameters *)
its_arg_frz : bool list; (** irreplaceable type parameters *)
its_reg_vis : bool list; (** non-ghost shareable components *)
its_reg_frz : bool list; (** irreplaceable shareable components *)
its_def : ity option; (** type alias *)
}
and ity = private {
......@@ -93,18 +93,40 @@ val ity_hash : ity -> int
val reg_hash : region -> int
val pv_hash : pvsymbol -> int
exception ImpurePrivateField of ity
exception DuplicateRegion of region
exception UnboundRegion of region
(** creation of a symbol for type in programs *)
val create_itysymbol :
preid -> (tvsymbol * bool * bool * bool) list ->
bool -> bool -> (region * bool) list ->
bool Mpv.t -> ity option -> itysymbol
val create_itysymbol_pure : preid -> tvsymbol list -> itysymbol
(** [create_itysymbol_pure id args] creates a new type symbol with
immutable type arguments and with no mutable fields or subregions.
This function should be used for all immutable non-updatable types:
abstract types, private immutable records, immutable records with
invariant, and recursive algebraic types. *)
val create_itysymbol_alias : preid -> tvsymbol list -> ity -> itysymbol
(** [create_itysymbol_alias id args def] creates a new type alias. *)
val create_itysymbol_rich :
preid -> tvsymbol list -> bool -> Spv.t -> Spv.t -> itysymbol
(** [create_itysymbol_rich id args privmut mfields ifields] creates
a new type symbol. Every mutable and immutable field is represented
by a [pvsymbol] of the corresponding ghost status in the [mfields]
or [ifields] set, respectively. The variables from [mfields] are
stored in the created type symbol and used in effects. If [privmut]
is [true], then all types in [mfields] and [ifields] must be pure. *)
val restore_its : tysymbol -> itysymbol
(** raises [Not_found] if the argument is not a [its_ts] *)
val its_mutable : itysymbol -> bool
(** [its_mutable s] checks if [s] is a mutable record or an alias for one *)
val its_impure : itysymbol -> bool
(** [its_impure s] checks if [s] is mutable or has mutable components *)
(** {2 Type constructors} *)
exception BadItyArity of itysymbol * int
......@@ -173,7 +195,6 @@ val ity_r_stale : region -> Sreg.t -> ity -> bool
val reg_r_stale : region -> Sreg.t -> region -> bool
val ity_closed : ity -> bool
val ity_immutable : ity -> bool
(* detect non-ghost type variables and regions *)
......@@ -261,7 +282,6 @@ exception AssignPrivate of region
exception StaleVariable of pvsymbol * region
exception BadGhostWrite of pvsymbol * region
exception DuplicateField of region * pvsymbol
exception WriteImmutable of region * pvsymbol
exception GhostDivergence
type effect = private {
......
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