Commit da42c225 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: private types

parent 5760e7db
......@@ -143,9 +143,10 @@ let create_data_decl tdl =
ignore (List.for_all check_arg vtvs);
(* build the constructor ps *)
let hidden = its.its_abst in
let rdonly = its.its_priv in
let tvl = List.map ity_var its.its_args in
let res = vty_value (ity_app its tvl its.its_regs) in
let pls = create_plsymbol ~hidden id vtvs res in
let pls = create_plsymbol ~hidden ~rdonly id vtvs res in
news := Sid.add pls.pl_ls.ls_name !news;
(* build the projections, if any *)
let build_proj id vtv =
......
......@@ -60,11 +60,12 @@ type plsymbol = {
pl_value : vty_value;
pl_effect : effect;
pl_hidden : bool;
pl_rdonly : bool;
}
let pl_equal : plsymbol -> plsymbol -> bool = (==)
let create_plsymbol ?(hidden=false) id args value =
let create_plsymbol ?(hidden=false) ?(rdonly=false) id args value =
let ty_of_vtv vtv = ty_of_ity vtv.vtv_ity in
let pure_args = List.map ty_of_vtv args in
let ls = create_fsymbol id pure_args (ty_of_vtv value) in
......@@ -77,6 +78,7 @@ let create_plsymbol ?(hidden=false) id args value =
pl_value = value;
pl_effect = effect;
pl_hidden = hidden;
pl_rdonly = rdonly;
}
let ity_of_ty_opt ty = ity_of_ty (Util.def_option ty_bool ty)
......@@ -86,9 +88,11 @@ let fake_pls = Wls.memoize 17 (fun ls ->
pl_args = List.map (fun ty -> vty_value (ity_of_ty ty)) ls.ls_args;
pl_value = vty_value (ity_of_ty_opt ls.ls_value);
pl_effect = eff_empty;
pl_hidden = false })
pl_hidden = false;
pl_rdonly = false; })
exception HiddenPLS of lsymbol
exception RdOnlyPLS of lsymbol
(** specification *)
......@@ -204,7 +208,8 @@ let ppat_plapp pls ppl vtv =
if ghost <> (vtv.vtv_ghost || arg.vtv_ghost) then
Loc.errorm "Ghost pattern in a non-ghost context";
let effect = eff_union eff pp.ppat_effect in
match arg.vtv_mut, pp.ppat_vtv.vtv_mut with
let arg_mut = if pls.pl_rdonly then None else arg.vtv_mut in
match arg_mut, pp.ppat_vtv.vtv_mut with
| _ when ppat_is_wild pp ->
effect
| Some r1, Some r2 ->
......@@ -291,7 +296,8 @@ let make_ppattern pp vtv =
let mtch arg pp =
let ity = ity_full_inst sbs arg.vtv_ity in
let ghost = vtv.vtv_ghost || arg.vtv_ghost in
let mut = Util.option_map (reg_full_inst sbs) arg.vtv_mut in
let arg_mut = if pls.pl_rdonly then None else arg.vtv_mut in
let mut = Util.option_map (reg_full_inst sbs) arg_mut in
let pp = make (vty_value ~ghost ?mut ity) pp in
if ppat_is_wild pp then pp.ppat_effect, pp else
Util.option_fold (eff_read ~ghost) pp.ppat_effect mut, pp
......@@ -562,13 +568,18 @@ let e_app = List.fold_left (fun e -> on_value (e_app_real e))
let e_plapp pls el ity =
if pls.pl_hidden then raise (HiddenPLS pls.pl_ls);
if pls.pl_rdonly then raise (RdOnlyPLS pls.pl_ls);
let rec app tl varm ghost eff sbs vtvl argl =
match vtvl, argl with
| [],[] ->
let vtv = pls.pl_value in
let ghost = ghost || vtv.vtv_ghost in
let sbs = ity_match sbs vtv.vtv_ity ity in
let mut = Util.option_map (reg_full_inst sbs) vtv.vtv_mut in
let mut = match pls.pl_args with
(* if our sole argument is a private type, then we are immutable *)
| [{vtv_ity = {ity_node = Ityapp ({its_priv = true},_,_)}}] -> None
| _ -> vtv.vtv_mut in
let mut = Util.option_map (reg_full_inst sbs) mut in
let vty = VTvalue (vty_value ~ghost ?mut ity) in
let eff = eff_union eff (eff_full_inst sbs pls.pl_effect) in
let t = match pls.pl_ls.ls_value with
......
......@@ -65,16 +65,18 @@ type plsymbol = private {
pl_value : vty_value;
pl_effect : effect;
pl_hidden : bool;
pl_rdonly : bool;
}
val pl_equal : plsymbol -> plsymbol -> bool
val create_plsymbol :
?hidden:bool -> preid -> vty_value list -> vty_value -> plsymbol
val create_plsymbol : ?hidden:bool -> ?rdonly:bool ->
preid -> vty_value list -> vty_value -> plsymbol
(* FIXME? Effect calculation is hardwired to correspond to constructors
and projections: mutable arguments are reset, mutable result is read. *)
exception HiddenPLS of lsymbol
exception RdOnlyPLS of lsymbol
(** specification *)
......
......@@ -456,6 +456,8 @@ let () = Exn_printer.register
fprintf fmt "The type of exception %s has mutable components" id.id_string
| Mlw_ty.IllegalAlias _reg ->
fprintf fmt "This application creates an illegal alias"
| Mlw_expr.RdOnlyPLS _ls ->
fprintf fmt "Cannot construct values of a private type"
| Mlw_expr.HiddenPLS ls ->
fprintf fmt "'%a' is a constructor/field of an abstract type \
and cannot be used in a program" print_ls ls;
......
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