Commit f522e56e authored by Andrei Paskevich's avatar Andrei Paskevich

Mlw: admit fields with mutable types in private records

this should not be problematic as long as these fields do not occur
in the invariants (actual or refined). In other words, a value of
a private type exists no matter what is stored in the field.

Also, admit non-private mutable types without actual mutable fields.
It is actually impossible to create a write effect for such types,
and the only consequence of being mutable is that they are assigned
a region, and so every value of such type can be tracked individually.
One use case for this is a non-private record with an invariant,
which either has fields with mutable types or has type parameters
that we wish to instantiate with mutable types. If we modify these
mutable components, this may break the record's invariant. Now, if
the record itself is immutable (and thus has no associated region),
then we must reestablish the invariant immediately, otherwise we
lose track of the value. Even if this extra flexibility does not
prove useful in the end, it seems to be harmless.

Also, admit type definitions of the form
  type t 'a = (private|abstract)? mutable? {} invariant*
which define private empty records (even if not declared private).

Also, "type t 'a" is now equivalent to "type t 'a = private {}".
parent e368d43a
......@@ -805,6 +805,8 @@ let effect_of_dspec dsp =
let fs = match fd with
| Some fd -> Spv.singleton (Opt.get fd.rs_field)
| None -> Spv.of_list reg.reg_its.its_mfields in
if not reg.reg_its.its_private && Spv.is_empty fs then
Loc.errorm ?loc:t.t_loc "mutable expression expected";
let rd = Spv.singleton v and wr = Mreg.singleton reg fs in
let e = Loc.try2 ?loc:t.t_loc eff_write rd wr in
(e,t)::l, eff_union_par eff e
......
......@@ -177,19 +177,16 @@ let create_projection s v =
exception FieldExpected of rsymbol
let mfield_of_rs s = match s.rs_cty.cty_args, s.rs_field with
| [{pv_ity = {ity_node = Ityreg {reg_its = ts}}}], Some f
when List.exists (pv_equal f) ts.its_mfields -> f
| [{pv_ity = {ity_node = Ityreg {reg_its = its}}}], Some f
when List.exists (pv_equal f) its.its_mfields -> f
| _ -> raise (FieldExpected s)
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_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
if not (Spv.subset mfs fs) then raise exn
end else if constr < 1 then raise exn;
if List.exists (fun f -> not (Spv.mem f fs)) s.its_mfields ||
s.its_private || s.its_def <> None || constr < 1 ||
(s.its_mutable && 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
let rgl = List.map ity_reg s.its_regions in
......@@ -375,7 +372,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_privmut ||
| Some fds -> r.reg_its.its_private ||
Spv.exists (fun fd -> not fd.pv_ghost) fds
| None -> false in
(* check if some component taints region r *)
......
......@@ -18,7 +18,8 @@ open Term
type itysymbol = {
its_ts : tysymbol; (** logical type symbol *)
its_privmut : bool; (** private mutable type *)
its_private : bool; (** private type *)
its_mutable : bool; (** mutable type *)
its_mfields : pvsymbol list; (** mutable record fields *)
its_regions : region list; (** shareable components *)
its_arg_imm : bool list; (** non-updatable parameters *)
......@@ -176,11 +177,9 @@ let ity_app_unsafe s tl rl = Hsity.hashcons (mk_ity (Ityapp (s,tl,rl)))
(* immutability and purity *)
let its_immutable s = not s.its_privmut && s.its_mfields = [] &&
match s.its_def with Some {ity_node = Ityreg _} -> false | _ -> true
let its_immutable s = not s.its_mutable
let its_pure s = its_immutable s && s.its_regions = [] &&
match s.its_def with Some ity -> ity.ity_imm | None -> true
let its_pure s = not s.its_mutable && s.its_regions = []
let ity_immutable ity = ity.ity_imm
......@@ -441,7 +440,7 @@ let ity_app_raw sbs id s tl rl = match s.its_def with
let tl = List.map (ity_full_inst sbs) r.reg_args in
let rl = List.map (ity_full_inst sbs) r.reg_regs in
ity_reg (mk_reg id r.reg_its tl rl)
| None when s.its_privmut || s.its_mfields <> [] ->
| None when s.its_mutable ->
ity_reg (mk_reg id s tl rl)
| Some ity -> ity_full_inst sbs ity
| None -> ity_app_unsafe s tl rl
......@@ -521,10 +520,12 @@ let ity_app_pure s tl rl =
let create_its, restore_its =
let ts_to_its = Wts.create 17 in
(fun ~ts ~pm ~mfld ~regs ~aimm ~aexp ~avis ~afrz ~rexp ~rvis ~rfrz ~def ->
(fun ~ts ~priv ~mut ~mfld ~regs ~aimm ~aexp
~avis ~afrz ~rexp ~rvis ~rfrz ~def ->
let its = {
its_ts = ts;
its_privmut = pm;
its_private = priv;
its_mutable = mut;
its_mfields = mfld;
its_regions = regs;
its_arg_imm = aimm;
......@@ -554,62 +555,61 @@ let rec ity_of_ty_pure ty = match ty.ty_node with
invalid_arg "Ity.ity_of_ty_pure" in
ity_app_pure s (List.map ity_of_ty_pure tl) []
let its_of_ts ts imm =
let its_of_ts ts priv =
assert (ts.ts_def = None);
let tl = List.map Util.ttrue ts.ts_args in
let il = if imm then tl else List.map Util.ffalse ts.ts_args in
let def = match ts.ts_def with None -> None | Some def ->
let def = ity_of_ty def in assert def.ity_imm; Some def in
create_its ~ts ~pm:false ~mfld:[] ~regs:[] ~aimm:il ~aexp:tl
~avis:tl ~afrz:tl ~rexp:[] ~rvis:[] ~rfrz:[] ~def
let il = if priv then tl else List.map Util.ffalse ts.ts_args in
create_its ~ts ~priv ~mut:false ~mfld:[] ~regs:[] ~aimm:il
~aexp:tl ~avis:tl ~afrz:tl ~rexp:[] ~rvis:[] ~rfrz:[] ~def:None
let create_itysymbol_pure id args =
its_of_ts (create_tysymbol id args None) true
let create_itysymbol_rec id args =
let ts = create_tysymbol id args None in
let tl = List.map Util.ttrue ts.ts_args in
create_its ~ts ~priv:false ~mut:false ~mfld:[] ~regs:[] ~aimm:tl
~aexp:tl ~avis:tl ~afrz:tl ~rexp:[] ~rvis:[] ~rfrz:[] ~def:None
let create_itysymbol_alias id args def =
let ts = create_tysymbol id args (Some (ty_of_ity def)) in
let ity = match def.ity_node with (* ignore the top region *)
| Ityreg r -> ity_app_pure r.reg_its r.reg_args r.reg_regs
| _ -> def in
let mut, ity = match def.ity_node with (* ignore the top region *)
| Ityreg r -> true, ity_app_pure r.reg_its r.reg_args r.reg_regs
| _ -> false, def in
let regs = Sreg.elements (ity_top_regs Sreg.empty ity) in
let tl = List.map Util.ttrue args in
let rl = List.map Util.ttrue regs in
create_its ~ts ~pm:false ~mfld:[] ~regs ~aimm:tl ~aexp:tl
create_its ~ts ~priv:false ~mut ~mfld:[] ~regs ~aimm:tl ~aexp:tl
~avis:tl ~afrz:tl ~rexp:rl ~rvis:rl ~rfrz:rl ~def:(Some def)
exception ImpureField of ity
let create_itysymbol_rich id args pm flds =
let create_itysymbol_plain ~priv ~mut id args flds =
let ts = create_tysymbol id args None in
let collect_vis fn acc =
Mpv.fold (fun f _ a -> if f.pv_ghost then a else fn a f.pv_ity) flds acc in
let collect_imm fn acc =
Mpv.fold (fun f m a -> if m then a else fn a f.pv_ity) flds acc in
let collect_all fn acc =
Mpv.fold (fun f _ a -> fn a f.pv_ity) flds acc in
let collect_imm fn acc =
Mpv.fold (fun f m a -> if m then a else fn a f.pv_ity) flds acc in
let collect_vis fn acc =
Mpv.fold (fun f _ a -> if f.pv_ghost then a else fn a f.pv_ity) flds acc in
let sargs = Stv.of_list args in
let dargs = collect_all ity_freevars Stv.empty in
if not (Stv.subset dargs sargs) then
raise (Ty.UnboundTypeVar (Stv.choose (Stv.diff dargs sargs)));
let mfld = Mpv.fold (fun f m l -> if m then f::l else l) flds [] in
if pm then begin (* private mutable record *)
let tl = List.map Util.ttrue args in
Mpv.iter (fun {pv_vs = v; pv_ity = i} _ -> if not i.ity_imm
then Loc.error ?loc:v.vs_name.id_loc (ImpureField i)) flds;
create_its ~ts ~pm ~mfld ~regs:[] ~aimm:tl ~aexp:tl ~avis:tl
~afrz:tl ~rexp:[] ~rvis:[] ~rfrz:[] ~def:None
end else (* non-private updatable type *)
let regs = Sreg.elements (collect_all ity_top_regs Sreg.empty) in
let check_args s = List.map (Stv.contains s) args in
let check_regs s = List.map (Sreg.contains s) regs in
let rexp = check_regs (collect_all ity_exp_regs Sreg.empty) in
let rvis = check_regs (collect_vis ity_vis_regs Sreg.empty) in
let rfrz = check_regs (collect_imm ity_exp_regs Sreg.empty) in
let mut = mut || mfld <> [] in
if priv then (* private record *)
let tl = List.map Util.ttrue args in
create_its ~ts ~priv ~mut ~mfld ~regs ~aimm:tl ~aexp:tl
~avis:tl ~afrz:tl ~rexp ~rvis ~rfrz ~def:None
else (* non-private updatable type *)
let aimm = check_args (collect_all ity_imm_vars Stv.empty) in
let aexp = check_args (collect_all ity_exp_vars Stv.empty) in
let rexp = check_regs (collect_all ity_exp_regs Sreg.empty) in
let avis = check_args (collect_vis ity_vis_vars Stv.empty) in
let rvis = check_regs (collect_vis ity_vis_regs Sreg.empty) in
let afrz = check_args (collect_imm ity_exp_vars Stv.empty) in
let rfrz = check_regs (collect_imm ity_exp_regs Sreg.empty) in
create_its ~ts ~pm ~mfld ~regs ~aimm ~aexp ~avis ~afrz ~rexp
~rvis ~rfrz ~def:None
create_its ~ts ~priv ~mut ~mfld ~regs ~aimm ~aexp ~avis ~afrz
~rexp ~rvis ~rfrz ~def:None
(** pvsymbol creation *)
......@@ -743,7 +743,7 @@ let check_taints tnt pvs =
if Sreg.mem r tnt then raise (BadGhostWrite (v,r))) () v.pv_ity) pvs
let visible_writes e =
Mreg.subdomain (fun {reg_its = {its_privmut = priv}} fs ->
Mreg.subdomain (fun {reg_its = {its_private = priv}} fs ->
priv || Spv.exists (fun fd -> not fd.pv_ghost) fs) e.eff_writes
let visible_reads e =
......@@ -798,8 +798,9 @@ let read_regs rd =
let eff_write rd wr =
if Mreg.is_empty wr then { eff_empty with eff_reads = rd } else
let kn = read_regs rd in
let wr = Mreg.filter (fun ({reg_its = {its_privmut = p}} as r) fs ->
if not p && Spv.is_empty fs then invalid_arg "Ity.eff_write";
let wr = Mreg.filter (fun ({reg_its = s} as r) fs ->
if Spv.is_empty fs && not (s.its_private && s.its_mutable)
then invalid_arg "Ity.eff_write";
Spv.iter (check_mutable_field "Ity.eff_write" r) fs;
Sreg.mem r kn) wr in
reset_taints { eff_empty with eff_reads = rd; eff_writes = wr;
......@@ -833,7 +834,7 @@ let eff_assign asl =
let writes = List.fold_left (fun wr (r,f,v) ->
let r = get_reg r and ity = v.pv_ity in
check_mutable_field "Ity.eff_assign" r f;
if r.reg_its.its_privmut then raise (AssignPrivate r);
if r.reg_its.its_private then raise (AssignPrivate r);
Mreg.change (fun fs -> Some (match fs with
| Some fs -> Mpv.add_new (DuplicateField (r,f)) f ity fs
| None -> Mpv.singleton f ity)) r wr) Mreg.empty asl in
......@@ -1387,11 +1388,8 @@ let () = Exn_printer.register (fun fmt e -> match e with
| UnboundRegion r -> fprintf fmt
"Unbound region %a" print_reg r
| ImpureType (v,ity) -> fprintf fmt
"Cannot instantiate pure type variable %a with type %a"
"Cannot instantiate pure type variable {%a} with type %a"
print_tv v print_ity ity
| ImpureField ity -> fprintf fmt
"Field type %a is mutable, it cannot be used in a type which is \
private, recursive, or has an invariant" print_ity ity
(*
| UnboundException xs -> fprintf fmt
"This function raises %a but does not specify a post-condition for it"
......
......@@ -17,7 +17,8 @@ open Term
type itysymbol = private {
its_ts : tysymbol; (** logical type symbol *)
its_privmut : bool; (** private mutable type *)
its_private : bool; (** private type *)
its_mutable : bool; (** mutable type *)
its_mfields : pvsymbol list; (** mutable record fields *)
its_regions : region list; (** shareable components *)
its_arg_imm : bool list; (** non-updatable parameters *)
......@@ -92,29 +93,29 @@ val ity_hash : ity -> int
val reg_hash : region -> int
val pv_hash : pvsymbol -> int
exception ImpureField of ity
exception DuplicateRegion of region
exception UnboundRegion of region
(** creation of a symbol for type in programs *)
(** creation of a type symbol in programs *)
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_plain :
priv:bool -> mut:bool -> preid -> tvsymbol list -> bool Mpv.t -> itysymbol
(** [create_itysymbol_plain ~priv ~mut id args fields] creates a new type
symbol for a non-recursive algebraic type, including private and/or
mutable records. Every known field is represented by a [pvsymbol]
mapped to its mutability status in [fields]. Variables corresponding
to mutable fields are stored in the created type symbol and used in
effects. The [priv] flag should be set to [true] for private records.
The [mut] flag should be set to [true] to mark the new type as mutable
even if it does not have known mutable fields. Abstract types are
considered to be private immutable records with no fields. *)
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 -> bool Mpv.t -> itysymbol
(** [create_itysymbol_rich id args privmut fields] creates a new type symbol.
Each field is represented by a [pvsymbol] mapped to its mutability status
in [fields]. The variables corresponding to mutable fields are stored in
the created type symbol and used in effects. If [privmut] is [true],
then all types in [fields] must be pure. *)
val create_itysymbol_rec : preid -> tvsymbol list -> itysymbol
(** [create_itysymbol_rec id args] creates a new type symbol for
a recursively defined type. *)
val restore_its : tysymbol -> itysymbol
(** raises [Not_found] if the argument is not a [its_ts] *)
......
......@@ -40,25 +40,30 @@ let check_field stv f =
let ftv = ity_freevars Stv.empty f.pv_ity in
if not (Stv.subset ftv stv) then Loc.error ?loc
(UnboundTypeVar (Stv.choose (Stv.diff ftv stv)));
if not f.pv_ity.ity_imm then Loc.error ?loc
(ImpureField f.pv_ity)
if not f.pv_ity.ity_imm then Loc.errorm ?loc
"This field has non-pure type, it cannot be used \
in a recursive type definition"
let check_invariant stv svs p =
let check_invariant stv svs mfs p =
let ptv = t_ty_freevars Stv.empty p in
let pvs = t_freevars Mvs.empty p in
if not (Stv.subset ptv stv) then Loc.error ?loc:p.t_loc
(UnboundTypeVar (Stv.choose (Stv.diff ptv stv)));
if not (Mvs.set_submap pvs svs) then Loc.error ?loc:p.t_loc
(UnboundVar (fst (Mvs.choose (Mvs.set_diff pvs svs))))
(UnboundVar (fst (Mvs.choose (Mvs.set_diff pvs svs))));
if not (Mvs.set_disjoint pvs mfs) then Loc.errorm ?loc:p.t_loc
"This invariant of a private type depends on a non-pure field %a"
Pretty.print_vs (fst (Mvs.choose (Mvs.set_inter pvs mfs)))
let check_pure_its s = not s.its_privmut &&
let its_recursive s =
not s.its_private && not s.its_mutable &&
s.its_mfields = [] && s.its_regions = [] &&
List.for_all (fun x -> x) s.its_arg_imm &&
List.for_all (fun x -> x) s.its_arg_exp &&
List.for_all (fun x -> x) s.its_arg_vis &&
List.for_all (fun x -> x) s.its_arg_frz &&
s.its_reg_vis = [] && s.its_reg_frz = [] &&
s.its_def = None
s.its_reg_exp = [] && s.its_reg_vis = [] &&
s.its_reg_frz = [] && s.its_def = None
let create_semi_constructor id s fl pjl invl =
let tvl = List.map ity_var s.its_ts.ts_args in
......@@ -75,45 +80,26 @@ let create_semi_constructor id s fl pjl invl =
let c = create_cty fl invl [q] Mexn.empty Mpv.empty eff ity in
create_rsymbol id c
let create_flat_record_decl id args priv mut fldl invl =
let exn = Invalid_argument "Mdecl.create_flat_record_decl" in
let create_plain_record_decl ~priv ~mut id args fldl invl =
let exn = Invalid_argument "Pdecl.create_plain_record_decl" in
let cid = id_fresh ?loc:id.pre_loc ("mk " ^ id.pre_name) in
let add_fd fs (fm,fd) = Mpv.add_new exn fd fm fs in
let flds = List.fold_left add_fd Mpv.empty fldl in
let fmut = List.exists fst fldl in
let fldl = List.map snd fldl in
let mut = mut || fmut in
if not priv && fldl = [] then raise exn;
if not priv && mut && not fmut then raise exn;
let stv = Stv.of_list args in
let mfs = if not priv then Svs.empty else List.fold_left (fun s v ->
if v.pv_ity.ity_imm then s else Svs.add v.pv_vs s) Svs.empty fldl in
let svs = List.fold_left (fun s v -> Svs.add v.pv_vs s) Svs.empty fldl in
List.iter (check_invariant stv svs) invl;
let s = if not mut && (priv || invl <> []) then begin
(* a type with an invariant must be declared as mutable in order
to accept mutable subvalues (we need a head region to track the
values that must be rechecked if a change is made to a subvalue).
If we have an immutable type with an invariant, then we create
an opaque type symbol for it, and forbid subregions. *)
List.iter (check_field stv) fldl;
create_itysymbol_pure id args
end else
create_itysymbol_rich id args (priv && mut) flds in
List.iter (check_invariant stv svs mfs) invl;
let s = create_itysymbol_plain ~priv ~mut id args flds in
let pjl = List.map (create_projection s) fldl in
let cl = if priv then [] else if invl <> [] then
[create_semi_constructor cid s fldl pjl invl] else
[create_constructor ~constr:1 cid s fldl] in
mk_itd s pjl cl invl
let create_abstract_type_decl id args mut =
(* = create_flat_record_decl id args true mut [] [] *)
let s = if mut
then create_itysymbol_rich id args true Mpv.empty
else create_itysymbol_pure id args in
mk_itd s [] [] []
let create_rec_record_decl s fldl =
if not (check_pure_its s) || fldl = [] then
invalid_arg "Mdecl.create_rec_record_decl";
if not (its_recursive s) then invalid_arg "Pdecl.create_rec_record_decl";
let id = s.its_ts.ts_name in
let cid = id_fresh ?loc:id.id_loc ("mk " ^ id.id_string) in
List.iter (check_field (Stv.of_list s.its_ts.ts_args)) fldl;
......@@ -122,7 +108,7 @@ let create_rec_record_decl s fldl =
mk_itd s pjl [cs] []
let create_variant_decl get_its cl =
let exn = Invalid_argument "Mdecl.create_variant_decl" in
let exn = Invalid_argument "Pdecl.create_variant_decl" in
let pjl, fds = match cl with
| cs::cl ->
let add_fd (pjs,fds) (pj,f) =
......@@ -137,11 +123,12 @@ let create_variant_decl get_its cl =
let mk_cs (cid,fl) = create_constructor ~constr cid s (List.map snd fl) in
mk_itd s (List.map (create_projection s) pjl) (List.map mk_cs cl) []
let create_flat_variant_decl id args cl =
create_variant_decl (fun fds -> create_itysymbol_rich id args false fds) cl
let create_plain_variant_decl id args cl =
create_variant_decl (fun fds ->
create_itysymbol_plain ~priv:false ~mut:false id args fds) cl
let create_rec_variant_decl s cl =
if not (check_pure_its s) then invalid_arg "Mdecl.create_rec_variant_decl";
if not (its_recursive s) then invalid_arg "Pdecl.create_rec_variant_decl";
let stv = Stv.of_list s.its_ts.ts_args in
let check_field fd _ = check_field stv fd in
create_variant_decl (fun fds -> Mpv.iter check_field fds; s) cl
......@@ -570,13 +557,13 @@ let print_its_defn fst fmt itd =
let print_defn fmt () =
match s.its_def, itd.itd_fields, itd.itd_constructors with
| Some ity, _, _ -> fprintf fmt " = %a" print_ity ity
| _, [], [] -> if s.its_privmut then fprintf fmt " = mutable {}"
| _, [], [] when not s.its_mutable -> ()
| _, fl, [] -> fprintf fmt " = private%s { %a }"
(if s.its_privmut && s.its_mfields = [] then " mutable" else "")
(if s.its_mutable && s.its_mfields = [] then " mutable" else "")
(Pp.print_list Pp.semi print_field) fl
| _, fl, [_] when s.its_mfields <> [] || itd.itd_invariant <> [] ->
(* only records can have mutable fields or invariants *)
fprintf fmt " = { %a }"
| _, fl, [{rs_name = {id_string = n}}]
when n = "mk " ^ s.its_ts.ts_name.id_string -> fprintf fmt " =%s { %a }"
(if s.its_mutable && s.its_mfields = [] then " mutable" else "")
(Pp.print_list Pp.semi print_field) fl
| _, fl, cl ->
let add s f = Mpv.add (Opt.get f.rs_field) f s in
......
......@@ -24,20 +24,47 @@ type its_defn = private {
itd_invariant : term list;
}
val create_abstract_type_decl : preid -> tvsymbol list -> bool -> its_defn
val create_alias_decl : preid -> tvsymbol list -> ity -> its_defn
val create_flat_record_decl : preid -> tvsymbol list ->
bool -> bool -> (bool * pvsymbol) list -> term list -> its_defn
val create_plain_record_decl : priv:bool -> mut:bool ->
preid -> tvsymbol list -> (bool * pvsymbol) list -> term list -> its_defn
(** [create_plain_record_decl ~priv ~mut id args fields inv] creates
a declaration for a non-recursive record type, possibly private
and/or mutable. The known record fields are listed with their
mutability status. The [priv] flag should be set to [true] for
private records. The [mut] flag should be set to [true] to mark
the new type as mutable even if it has no known mutable fields.
This is the case for private mutable records with no known mutable
fields, as well as for non-private records that have an invariant:
marking such a type as mutable gives every value of this type a
distinct identity, allowing us to track values with broken invariants.
The [inv] parameter contains the list of invariant formulas that may
only depend on free variables from [fields]. If the type is private,
then every field occurring in [inv] must have an immutable type.
Abstract types are considered to be private records with no fields. *)
val create_rec_record_decl : itysymbol -> pvsymbol list -> its_defn
(** [create_rec_record_decl its fields] creates a declaration for
a recursive record type. The type symbol should be created using
[Ity.create_itysymbol_rec]. All fields must be immutable. *)
val create_plain_variant_decl :
preid -> tvsymbol list -> (preid * (bool * pvsymbol) list) list -> its_defn
(** [create_plain_variant_decl id args constructors] creates a declaration
for a non-recursive algebraic type. Each constructor field carries a
Boolean flag denoting whether a projection function should be generated
for this field. Any such field must be present in each constructor, so
that the projection function is total. *)
val create_rec_variant_decl :
itysymbol -> (preid * (bool * pvsymbol) list) list -> its_defn
(** [create_rec_variant_decl id args constructors] creates a declaration
for a recursive algebraic type. The type symbol should be created using
[Ity.create_itysymbol_rec]. Each constructor field carries a Boolean flag
denoting whether a projection function should be generated for this field.
Any such field must be present in each constructor, so that the projection
function is total. All fields must be immutable. *)
val create_flat_variant_decl : preid -> tvsymbol list ->
(preid * (bool * pvsymbol) list) list -> its_defn
val create_rec_variant_decl : itysymbol ->
(preid * (bool * pvsymbol) list) list -> its_defn
val create_alias_decl : preid -> tvsymbol list -> ity -> its_defn
(** [create_alias_decl id args def] creates a new alias type declaration. *)
(** {2 Module declarations} *)
......
......@@ -228,10 +228,9 @@ let count_regions {muc_known = kn} {pv_ity = ity} mr =
| Ityreg r -> fields (add_reg r mr) r.reg_its r.reg_args r.reg_regs
| Ityapp (s,tl,rl) -> fields mr s tl rl
| Ityvar _ -> assert false
and fields mr s tl rl = if s.its_privmut then mr else
let add_arg isb v ity = ity_match isb (ity_var v) ity in
let isb = List.fold_left2 add_arg isb_empty s.its_ts.ts_args tl in
let isb = List.fold_left2 reg_match isb s.its_regions rl in
and fields mr s tl rl =
if s.its_private && rl = [] then mr else
let isb = its_match_regs s tl rl in
let add_ity mr ity = down mr (ity_full_inst isb ity) in
let add_proj mr f = add_ity mr f.rs_cty.cty_result in
let add_field mr v = add_ity mr v.pv_ity in
......@@ -596,13 +595,14 @@ let clone_type_decl inst cl tdl =
if d.itd_fields = [] && d.itd_constructors = [] &&
d.itd_invariant = [] then begin
if cloned then Hits.add htd s None else begin
let itd = create_abstract_type_decl id' ts.ts_args s.its_privmut in
let itd = create_plain_record_decl id' ts.ts_args
~priv:s.its_private ~mut:s.its_mutable [] [] in
cl.ts_table <- Mts.add ts itd.itd_its cl.ts_table;
save_itd itd
end
end else
(* variant *)
if s.its_mfields = [] && d.itd_constructors <> [] &&
if not s.its_mutable && d.itd_constructors <> [] &&
d.itd_invariant = [] then begin
if cloned then raise (CannotInstantiate id);
let conv_fd m fd =
......@@ -618,15 +618,13 @@ let clone_type_decl inst cl tdl =
let itd = create_rec_variant_decl s' csl in
save_itd itd
| None ->
let itd = create_flat_variant_decl id' ts.ts_args csl in
let itd = create_plain_variant_decl id' ts.ts_args csl in
cl.ts_table <- Mts.add ts itd.itd_its cl.ts_table;
save_itd itd
end else begin
(* flat record *)
if cloned then raise (CannotInstantiate id);
let mfld = Spv.of_list s.its_mfields in
let priv = d.itd_constructors = [] in
let mut = not (its_immutable s) in
let pjl = List.map (fun fd -> Opt.get fd.rs_field) d.itd_fields in
let fdl = List.map (fun v -> Spv.mem v mfld, conv_pj v) pjl in
let inv =
......@@ -634,7 +632,8 @@ let clone_type_decl inst cl tdl =
let add mv u (_,v) = Mvs.add u.pv_vs v.pv_vs mv in
let mv = List.fold_left2 add Mvs.empty pjl fdl in
List.map (clone_term cl mv) d.itd_invariant in
let itd = create_flat_record_decl id' ts.ts_args priv mut fdl inv in
let itd = create_plain_record_decl id' ts.ts_args
~priv:s.its_private ~mut:s.its_mutable fdl inv in
cl.ts_table <- Mts.add ts itd.itd_its cl.ts_table;
save_itd itd
end
......@@ -646,7 +645,7 @@ let clone_type_decl inst cl tdl =
if Sits.mem s alg then begin
if not (Mts.mem s.its_ts cl.ts_table) then
let id = id_clone s.its_ts.ts_name in
let s = create_itysymbol_pure id s.its_ts.ts_args in
let s = create_itysymbol_rec id s.its_ts.ts_args in
cl.ts_table <- Mts.add s.its_ts s cl.ts_table
end else Opt.iter (visit alg s) (Mits.find_opt s def);
List.iter down tl
......
......@@ -266,20 +266,12 @@ type_decl:
ty_var:
| labels(quote_lident) { $1 }
(* TODO: should global "mutable" imply "private"?
"type t 'a = mutable { x : int }"
- if "x" is immutable then the type can only be private
- if "x" is automatically mutable then I don't like it
- if there are known mutable fields, then a global "mutable"
is redundant, unless it also means "private" *)
(* TODO: what should be the syntax for mutable private records
without known fields? *)
typedefn:
| (* epsilon *)
{ (Public, false), TDabstract }
{ (Abstract, false), TDrecord [] }
| EQUAL vis_mut bar_list1(type_case)
{ $2, TDalgebraic $3 }
| EQUAL vis_mut LEFTBRC semicolon_list1(type_field) RIGHTBRC
| EQUAL vis_mut LEFTBRC loption(semicolon_list1(type_field)) RIGHTBRC
{ $2, TDrecord $4 }
| EQUAL vis_mut ty
{ $2, TDalias $3 }
......
......@@ -162,7 +162,6 @@ type field = {
}
type type_def =
| TDabstract
| TDalias of pty
| TDalgebraic of (Loc.position * ident * param list) list
| TDrecord of field list
......
......@@ -781,14 +781,9 @@ let add_types muc tdl =
let id = create_user_id d.td_ident and loc = d.td_loc in
let args = List.map (fun id -> tv_of_string id.id_str) d.td_params in
match d.td_def with
| TDabstract ->
if d.td_inv <> [] then Loc.errorm ~loc
"Abstract non-record types cannot have invariants";
let itd = create_abstract_type_decl id args d.td_mut in
Hstr.add hts x itd.itd_its; Hstr.add htd x itd
| TDalias pty ->
if d.td_vis <> Public || d.td_mut then Loc.errorm ~loc
"Alias types cannot be abstract, private. or mutable";
"Alias types cannot be abstract, private, or mutable";
if d.td_inv <> [] then Loc.errorm ~loc
"Alias types cannot have invariants";
let alias = Sstr.add x alias in
......@@ -798,7 +793,7 @@ let add_types muc tdl =
Hstr.add hts x itd.itd_its; Hstr.add htd x itd
| TDalgebraic csl ->
if d.td_vis <> Public || d.td_mut then Loc.errorm ~loc
"Algebraic types cannot be abstract, private. or mutable";
"Algebraic types cannot be abstract, private, or mutable";
if d.td_inv <> [] then Loc.errorm ~loc
"Algebraic types cannot have invariants";
let hfd = Hstr.create 5 in
......@@ -836,7 +831,7 @@ let add_types muc tdl =
| Some s ->
Hstr.add htd x (create_rec_variant_decl s csl)
| None ->
let itd = create_flat_variant_decl id args csl in
let itd = create_plain_variant_decl id args csl in
Hstr.add hts x itd.itd_its; Hstr.add htd x itd end
| TDrecord fl ->
let alias = Sstr.empty in
......@@ -855,19 +850,21 @@ let add_types muc tdl =
begin match try Some (Hstr.find hts x) with Not_found -> None with
| Some s ->
if d.td_vis <> Public || d.td_mut then Loc.errorm ~loc
"Recursive types cannot be abstract, private. or mutable";
"Recursive types cannot be abstract, private, or mutable";
if d.td_inv <> [] then Loc.errorm ~loc
"Recursive types cannot have invariants";
let get_fd (mut, fd) = if mut then Loc.errorm ~loc
"Recursive types cannot have mutable fields" else fd in
Hstr.add htd x (create_rec_record_decl s (List.map get_fd fl))
| None ->
let priv = d.td_vis <> Public and mut = d.td_mut in
(* empty records are automatically private, otherwise they are
just unit types that can be neither constructed nor refined *)
let priv = d.td_vis <> Public || fl = [] and mut = d.td_mut in
let add_fd m (_, v) = Mstr.add v.pv_vs.vs_name.id_string v m in
let gvars = List.fold_left add_fd Mstr.empty fl in
let type_inv f = type_fmla_pure muc gvars Dterm.denv_empty f in
let invl = List.map type_inv d.td_inv in
let itd = create_flat_record_decl id args priv mut fl invl in
let itd = create_plain_record_decl ~priv ~mut id args fl invl in
Hstr.add hts x itd.itd_its; Hstr.add htd x itd end
and parse ~loc ~alias ~alg pty =
......@@ -882,7 +879,7 @@ let add_types muc tdl =
Hstr.find hts x
| Qident {id_str = x} when Mstr.mem x alg ->
let id, args = Mstr.find x alg in
let s = create_itysymbol_pure id args in
let s = create_itysymbol_rec id args in
Hstr.add hts x s;
(* visit ~alias ~alg x (Mstr.find x def); *)
s
......
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