Commit 9635816d authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

whyml: get rid of mutable variables and expressions

This simplifies semantics, makes a lot of checks unnecessary,
and makes us compatible with OCaml.
parent 2b74c319
......@@ -9,6 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Ident
open Ty
open Term
......@@ -109,7 +110,9 @@ let create_ty_decl its =
if its.its_def = None then invalid_arg "Mlw_decl.create_ty_decl";
mk_decl (PDtype its) Sid.empty news
type pre_constructor = preid * (pvsymbol * bool) list
type pre_field = preid option * field
type pre_constructor = preid * pre_field list
type pre_data_decl = itysymbol * pre_constructor list
......@@ -121,10 +124,10 @@ let null_invariant { its_ts = ts } =
let create_data_decl tdl =
(* let syms = ref Sid.empty in *)
let news = ref Sid.empty in
let projections = Hid.create 17 in (* id -> plsymbol *)
let build_constructor its (id,al) =
let projections = Hstr.create 17 in (* id -> plsymbol *)
let build_constructor its res (id,al) =
(* check well-formedness *)
let vtvs = List.map (fun (pv,_) -> pv.pv_vtv) al in
let fds = List.map snd al in
let tvs = List.fold_right Stv.add its.its_ts.ts_args Stv.empty in
let regs = List.fold_right Sreg.add its.its_regs Sreg.empty in
let check_vars { vars_tv = atvs; vars_reg = aregs } =
......@@ -132,36 +135,42 @@ let create_data_decl tdl =
raise (UnboundTypeVar (Stv.choose (Stv.diff atvs tvs)));
if not (Sreg.subset aregs regs) then
raise (UnboundRegion (Sreg.choose (Sreg.diff aregs regs))) in
let check_arg vtv = match vtv.vtv_mut with
let check_arg fd = match fd.fd_mut with
| Some r -> if not (Sreg.mem r regs) then raise (UnboundRegion r)
| None -> check_vars vtv.vtv_ity.ity_vars in
List.iter check_arg vtvs;
| None -> check_vars fd.fd_ity.ity_vars in
List.iter check_arg fds;
(* build the constructor ps *)
let hidden = its.its_abst in
let rdonly = its.its_priv in
let tvl = List.map ity_var its.its_ts.ts_args in
let res = vty_value (ity_app its tvl its.its_regs) in
let pls = create_plsymbol ~hidden ~rdonly id vtvs res in
news := news_id !news pls.pl_ls.ls_name;
let hidden = its.its_abst and rdonly = its.its_priv in
let cs = create_plsymbol ~hidden ~rdonly id fds res in
news := news_id !news cs.pl_ls.ls_name;
(* build the projections, if any *)
let build_proj id vtv =
try Hid.find projections id with Not_found ->
let pls = create_plsymbol ~hidden (id_clone id) [res] vtv in
news := news_id !news pls.pl_ls.ls_name;
Hid.add projections id pls;
pls
let build_proj fd id =
try
let pj = Hstr.find projections (preid_name id) in
ity_equal_check pj.pl_value.fd_ity fd.fd_ity;
begin match pj.pl_value.fd_mut, fd.fd_mut with
| None, None -> ()
| Some r1, Some r2 -> reg_equal_check r1 r2
| _,_ -> invalid_arg "Mlw_decl.create_data_decl"
end;
if pj.pl_value.fd_ghost <> fd.fd_ghost then
invalid_arg "Mlw_decl.create_data_decl";
pj
with Not_found ->
let pj = create_plsymbol ~hidden id [res] fd in
news := news_id !news pj.pl_ls.ls_name;
Hstr.add projections (preid_name id) pj;
pj
in
let build_proj (pv,pj) =
let vtv = pv.pv_vtv in
(* syms := ity_s_fold syms_its syms_ts !syms vtv.vtv_ity; *)
if pj then Some (build_proj pv.pv_vs.vs_name vtv) else None
in
pls, List.map build_proj al
cs, List.map (fun (id,fd) -> Opt.map (build_proj fd) id) al
in
let build_type (its,cl) =
Hid.clear projections;
Hstr.clear projections;
news := news_id !news its.its_ts.ts_name;
its, List.map (build_constructor its) cl, null_invariant its
let tvl = List.map ity_var its.its_ts.ts_args in
let ity = ity_app its tvl its.its_regs in
let res = { fd_ity = ity; fd_ghost = false; fd_mut = None } in
its, List.map (build_constructor its res) cl, null_invariant its
in
let tdl = List.map build_type tdl in
mk_decl (PDdata tdl) Sid.empty !news
......@@ -238,8 +247,6 @@ let create_rec_decl fdl =
let create_val_decl lv =
let news = letvar_news lv in
let news, syms = match lv with
| LetV { pv_vtv = { vtv_mut = Some _ }} ->
Loc.errorm "abstract parameters cannot be mutable"
| LetV pv -> new_regs vars_empty news pv.pv_vars, Sid.empty
| LetA ps -> news, Mid.map (fun _ -> ()) ps.ps_varm in
(*
......@@ -349,7 +356,10 @@ let inst_constructors lkn kn ity = match ity.ity_node with
if csl = [] || is_rec then raise (NonupdatableType ity);
let base = ity_pur ts (List.map ity_var ts.ts_args) in
let sbs = ity_match ity_subst_empty base ity in
let subst ty = vty_value (ity_full_inst sbs (ity_of_ty ty)) in
let subst ty = {
fd_ity = ity_full_inst sbs (ity_of_ty ty);
fd_ghost = false;
fd_mut = None; } in
List.map (fun (cs,_) -> cs, List.map subst cs.ls_args) csl
| Ityapp (its,_,_) ->
let csl = find_constructors kn its in
......@@ -359,21 +369,21 @@ let inst_constructors lkn kn ity = match ity.ity_node with
let args = List.map ity_var its.its_ts.ts_args in
let base = ity_app its args its.its_regs in
let sbs = ity_match ity_subst_empty base ity in
let subst vtv =
let ghost = vtv.vtv_ghost in
let mut = Opt.map (reg_full_inst sbs) vtv.vtv_mut in
vty_value ~ghost ?mut (ity_full_inst sbs vtv.vtv_ity) in
let subst fd = {
fd_ity = ity_full_inst sbs fd.fd_ity;
fd_ghost = fd.fd_ghost;
fd_mut = Opt.map (reg_full_inst sbs) fd.fd_mut; } in
List.map (fun (cs,_) -> cs.pl_ls, List.map subst cs.pl_args) csl
| Ityvar _ ->
invalid_arg "Mlw_decl.inst_constructors"
let check_ghost lkn kn d =
let rec access regs ity =
let check vtv = match vtv.vtv_mut with
| _ when vtv.vtv_ghost -> ()
let check fd = match fd.fd_mut with
| _ when fd.fd_ghost -> ()
| Some r when Sreg.mem r regs -> raise (GhostWrite (e_void, r))
| _ -> access regs vtv.vtv_ity in
let check (_cs,vtvl) = List.iter check vtvl in
| _ -> access regs fd.fd_ity in
let check (_cs,fdl) = List.iter check fdl in
let occurs r = reg_occurs r ity.ity_vars in
if not (Sreg.exists occurs regs) then () else
List.iter check (inst_constructors lkn kn ity)
......
......@@ -41,7 +41,9 @@ and pdecl_node = private
(** {2 Declaration constructors} *)
type pre_constructor = preid * (pvsymbol * bool) list
type pre_field = preid option * field
type pre_constructor = preid * pre_field list
type pre_data_decl = itysymbol * pre_constructor list
......@@ -81,4 +83,4 @@ val find_invariant : known_map -> itysymbol -> post
exception NonupdatableType of ity
val inst_constructors :
Decl.known_map -> known_map -> ity -> (lsymbol * vty_value list) list
Decl.known_map -> known_map -> ity -> (lsymbol * field list) list
......@@ -60,7 +60,7 @@ and dexpr_desc =
| DEfun of dbinder list * dtriple
| DElet of ident * ghost * dexpr * dexpr
| DEletrec of drecfun list * dexpr
| DEassign of dexpr * dexpr
| DEassign of plsymbol * dexpr * dexpr
| DEif of dexpr * dexpr * dexpr
| DEloop of dvariant list * dinvariant * dexpr
| DElazy of Ptree.lazy_op * dexpr * dexpr
......
......@@ -304,7 +304,7 @@ let specialize_psymbol ps =
let specialize_plsymbol pls =
let htv = Htv.create 3 and hreg = Hreg.create 3 in
let conv vtv = dity_of_vtv htv hreg vars_empty vtv in
let conv fd = dity_of_ity htv hreg vars_empty fd.fd_ity in
List.map conv pls.pl_args, conv pls.pl_value
let dity_of_ty htv hreg vars ty =
......
This diff is collapsed.
......@@ -25,24 +25,27 @@ open Mlw_ty.T
locally defined and therefore every type variable and region in their
type signature can be instantiated. *)
type field = {
fd_ity : ity;
fd_ghost : bool;
fd_mut : region option;
}
type plsymbol = private {
pl_ls : lsymbol;
pl_args : vty_value list;
pl_value : vty_value;
pl_effect : effect;
pl_args : field list;
pl_value : field;
pl_hidden : bool;
pl_rdonly : bool;
}
val pl_equal : plsymbol -> plsymbol -> bool
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. *)
val create_plsymbol :
?hidden:bool -> ?rdonly:bool -> preid -> field list -> field -> plsymbol
exception HiddenPLS of lsymbol
exception RdOnlyPLS of lsymbol
exception HiddenPLS of plsymbol
exception RdOnlyPLS of plsymbol
(** cloning *)
......@@ -137,7 +140,7 @@ and expr_node = private
| Erec of fun_defn list * expr
| Eif of expr * expr * expr
| Ecase of expr * (ppattern * expr) list
| Eassign of expr * region * pvsymbol
| Eassign of plsymbol * expr * region * pvsymbol
| Eghost of expr
| Eany of spec
| Eloop of invariant * variant list * expr
......@@ -220,7 +223,7 @@ val e_case : expr -> (ppattern * expr) list -> expr
exception Immutable of expr
val e_assign : expr -> expr -> expr
val e_assign : plsymbol -> expr -> expr -> expr
val e_ghost : expr -> expr
val fs_void : lsymbol
......
......@@ -417,11 +417,7 @@ let clone_export uc m inst =
Hreg.replace regh r nr;
nr in
let conv_vtv v =
let ghost = v.vtv_ghost in
let mut, ity = match v.vtv_mut with
| Some r -> let r = conv_reg r in Some r, r.reg_ity
| None -> None, conv_ity v.vtv_ity in
vty_value ~ghost ?mut ity in
vty_value ~ghost:v.vtv_ghost (conv_ity v.vtv_ity) in
let conv_pv pv =
create_pvsymbol (id_clone pv.pv_vs.vs_name) (conv_vtv pv.pv_vtv) in
let psh = Hid.create 3 in
......
......@@ -720,9 +720,9 @@ and print_lexpr pri info fmt e =
fprintf fmt (protect_on (pri > 0)
"@[<hv>if %a@ @[<hov 2>then %a@]@ @[<hov 2>else %a@]@]")
(print_expr info) e0 (print_expr info) e1 (print_expr info) e2
| Eassign (e,_,pv) ->
fprintf fmt (protect_on (pri > 0) "%a <- %a")
(print_expr info) e (print_pv info) pv
| Eassign (pl,e,_,pv) ->
fprintf fmt (protect_on (pri > 0) "%a.%a <- %a")
(print_expr info) e (print_ls info) pl.pl_ls (print_pv info) pv
| Eloop (_,_,e) ->
fprintf fmt "@[while true do@ %a@ done@]" (print_expr info) e
| Efor (pv,(pvfrom,dir,pvto),_,e) ->
......@@ -895,21 +895,23 @@ let print_exn_decl info fmt xs =
else
print_exn_decl info fmt xs
let print_field info fmt fd =
if fd.fd_ghost then fprintf fmt "unit" else print_ity info fmt fd.fd_ity
let print_pconstr info fmt (cs,_) = match cs.pl_args with
| [] ->
fprintf fmt "@[<hov 4>| %a@]" (print_cs info) cs.pl_ls
| tl ->
let print_vtv fmt vtv =
if vtv.vtv_ghost then fprintf fmt "unit" else print_vtv info fmt vtv in
fprintf fmt "@[<hov 4>| %a of %a@]" (print_cs info) cs.pl_ls
(print_list star print_vtv) tl
(print_list star (print_field info)) tl
let print_pdata_decl info fst fmt (its, csl, _) =
let print_default () = print_list newline (print_pconstr info) fmt csl in
let print_field fmt (ls, vtv) =
fprintf fmt "%s%a: "
(if vtv.vtv_mut <> None then "mutable " else "") (print_ls info) ls;
if vtv.vtv_ghost then fprintf fmt "unit" else print_vtv info fmt vtv in
let print_field fmt (ls, fd) =
fprintf fmt "%s%a: %a"
(if fd.fd_mut <> None then "mutable " else "")
(print_ls info) ls (print_field info) fd
in
let print_defn fmt = function
| [cs, _] ->
let pjl = get_record info cs.pl_ls in
......
......@@ -136,8 +136,8 @@ and print_vty fmt = function
| VTarrow vta -> print_vta fmt vta
| VTvalue vtv -> print_vtv fmt vtv
let print_pvty fmt pv = fprintf fmt "@[%a%a:@,%a@]"
print_pv pv print_reg_opt pv.pv_vtv.vtv_mut print_vtv pv.pv_vtv
let print_pvty fmt pv = fprintf fmt "@[%a:@,%a@]"
print_pv pv print_vtv pv.pv_vtv
let print_psty fmt ps =
let print_tvs fmt tvs = if not (Stv.is_empty tvs) then
......@@ -285,9 +285,9 @@ and print_enode pri fmt e = match e.e_node with
| Eif (e0,e1,e2) ->
fprintf fmt (protect_on (pri > 0) "if %a then %a@ else %a")
print_expr e0 print_expr e1 print_expr e2
| Eassign (e,r,pv) ->
fprintf fmt (protect_on (pri > 0) "%a <%a> <- %a")
print_expr e print_regty r print_pv pv
| Eassign (pl,e,r,pv) ->
fprintf fmt (protect_on (pri > 0) "%a.%a <%a> <- %a")
print_expr e print_ls pl.pl_ls print_regty r print_pv pv
| Ecase (e0,bl) ->
fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
print_expr e0 (print_list newline print_branch) bl
......@@ -350,25 +350,24 @@ let print_ty_arg fmt ty =
fprintf fmt "@ %a" (print_ity_node ity_subst_empty true) ty
let print_constr fmt (cs,pjl) =
let print_pj fmt (vtv,pj) = match pj with
let print_pj fmt (fd,pj) = match pj with
| Some { pl_ls = ls } ->
fprintf fmt "@ (%s%s%a%a:@,%a)"
(if vtv.vtv_ghost then "ghost " else "")
(if vtv.vtv_mut <> None then "mutable " else "")
print_ls ls print_reg_opt vtv.vtv_mut print_ity vtv.vtv_ity
| None when vtv.vtv_ghost || vtv.vtv_mut <> None ->
(if fd.fd_ghost then "ghost " else "")
(if fd.fd_mut <> None then "mutable " else "")
print_ls ls print_reg_opt fd.fd_mut print_ity fd.fd_ity
| None when fd.fd_ghost || fd.fd_mut <> None ->
fprintf fmt "@ (%s%s%a@ %a)"
(if vtv.vtv_ghost then "ghost" else "")
(if vtv.vtv_mut <> None then "mutable " else "")
print_reg_opt vtv.vtv_mut
print_ity vtv.vtv_ity
(if fd.fd_ghost then "ghost" else "")
(if fd.fd_mut <> None then "mutable " else "")
print_reg_opt fd.fd_mut print_ity fd.fd_ity
| None ->
print_ty_arg fmt vtv.vtv_ity
print_ty_arg fmt fd.fd_ity
in
fprintf fmt "@[<hov 4>| %a%a%a@]" print_cs cs.pl_ls
print_ident_labels cs.pl_ls.ls_name
(print_list nothing print_pj)
(List.map2 (fun vtv pj -> (vtv,pj)) cs.pl_args pjl)
(List.map2 (fun fd pj -> (fd,pj)) cs.pl_args pjl)
let print_head fst fmt ts =
fprintf fmt "%s %s%s%a%a <%a>%a"
......@@ -461,10 +460,10 @@ let () = Exn_printer.register
| 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 "Cannot construct or modify values of a private type"
| Mlw_expr.HiddenPLS pl ->
fprintf fmt "'%a' is a constructor/field of an abstract type \
and cannot be used in a program" print_ls ls;
and cannot be used in a program" print_ls pl.pl_ls;
| Mlw_expr.GhostWrite (_e, _reg) ->
fprintf fmt
"This expression performs a ghost write in a non-ghost location"
......
......@@ -787,22 +787,11 @@ let spec_check c ty =
type vty_value = {
vtv_ity : ity;
vtv_ghost : bool;
vtv_mut : region option;
}
let vty_value ?(ghost=false) ?mut ity =
Opt.iter (fun r -> ity_equal_check ity r.reg_ity) mut;
{ vtv_ity = ity;
vtv_ghost = ghost;
vtv_mut = mut }
let vty_value ?(ghost=false) ity = { vtv_ity = ity; vtv_ghost = ghost }
let vtv_vars {vtv_ity = {ity_vars = vars}; vtv_mut = mut} = match mut with
| Some r -> { vars with vars_reg = Sreg.add r vars.vars_reg }
| None -> vars
let vtv_unmut vtv =
if vtv.vtv_mut = None then vtv else
vty_value ~ghost:vtv.vtv_ghost vtv.vtv_ity
let vtv_vars vtv = vtv.vtv_ity.ity_vars
type pvsymbol = {
pv_vs : vsymbol;
......@@ -883,16 +872,8 @@ let vty_arrow argl ?spec ?(ghost=false) vty =
let exn = Invalid_argument "Mlw.vty_arrow" in
(* the arguments must be all distinct *)
if argl = [] then raise exn;
let add_arg pvs pv =
(* mutable arguments are rejected outright *)
if pv.pv_vtv.vtv_mut <> None then raise exn;
Spv.add_new exn pv pvs in
let add_arg pvs pv = Spv.add_new exn pv pvs in
ignore (List.fold_left add_arg Spv.empty argl);
(* only projections may return mutable values *)
begin match vty with
| VTvalue { vtv_mut = Some _ } -> raise exn
| _ -> ()
end;
let spec = match spec with
| Some spec -> spec_check spec vty; spec
| None -> spec_empty (ty_of_vty vty) in
......
......@@ -257,12 +257,9 @@ type spec = {
type vty_value = private {
vtv_ity : ity;
vtv_ghost : bool;
vtv_mut : region option;
}
val vty_value : ?ghost:bool -> ?mut:region -> ity -> vty_value
val vtv_unmut : vty_value -> vty_value (* remove mutability *)
val vty_value : ?ghost:bool -> ity -> vty_value
type pvsymbol = private {
pv_vs : vsymbol;
......
......@@ -220,7 +220,7 @@ let parse_record uc fll =
| [] -> raise EmptyRecord
| (pl,_)::_ -> pl in
let its = match pl.pl_args with
| [{ vtv_ity = { ity_node = Ityapp (its,_,_) }}] -> its
| [{ fd_ity = { ity_node = Ityapp (its,_,_) }}] -> its
| _ -> raise (BadRecordField pl.pl_ls) in
let cs, pjl = match find_constructors (get_known uc) its with
| [cs,pjl] -> cs, List.map (Opt.get_exn (BadRecordField pl.pl_ls)) pjl
......@@ -552,14 +552,19 @@ and de_desc denv loc = function
let res = de_app loc (hidden_pl ~loc cs) (List.map get_val pjl) in
mk_let ~loc ~uloc:denv.uloc e1 res
| Ptree.Eassign (e1, q, e2) ->
let fl = { expr_desc = Eident q; expr_loc = loc } in
let e1 = { expr_desc = Eapply (fl,e1); expr_loc = loc } in
let fl = dexpr denv { expr_desc = Eident q; expr_loc = qloc q } in
let pl = match fl.de_desc with
| DEglobal_pl pl -> pl
| _ -> Loc.errorm ~loc:(qloc q) "%a is not a field name" print_qualid q
in
let e1 = dexpr denv e1 in
let e2 = dexpr denv e2 in
let d, ty = de_app loc fl [e1] in
let e0 = mk_dexpr d ty loc Slab.empty in
let res = create_type_variable () in
expected_type e1 res;
expected_type e0 res;
expected_type_weak e2 res;
DEassign (e1, e2), ([], dity_unit)
DEassign (pl, e1, e2), ([], dity_unit)
| Ptree.Econstant (Number.ConstInt _ as c) ->
DEconstant c, ([], dity_int)
| Ptree.Econstant (Number.ConstReal _ as c) ->
......@@ -752,13 +757,12 @@ and re_desc denv de = match de.de_desc with
let denv = List.fold_left add_one denv fdl in
let e1 = rexpr denv e1 in
DEletrec (fdl, e1), e1.de_type
| DEassign (e1, e2) ->
| DEassign (pl, e1, e2) ->
let e1 = rexpr denv e1 in
let e2 = rexpr denv e2 in
let res = create_type_variable () in
expected_type e1 res;
expected_type_weak e2 res;
DEassign (e1, e2), ([], dity_unit)
(* no need to weakly reunify e1.pl with e2,
since both dexprs retain their "pure" types *)
DEassign (pl, e1, e2), ([], dity_unit)
| DEif (e1, e2, e3) ->
let e1 = rexpr denv e1 in
expected_type e1 dity_bool;
......@@ -1029,28 +1033,31 @@ let add_binders lenv pvl =
let add lenv pv = add_local pv.pv_vs.vs_name.id_string (LetV pv) lenv in
List.fold_left add lenv pvl
let mk_field ity gh mut = { fd_ity = ity; fd_ghost = gh; fd_mut = mut }
let fd_of_pv pv = mk_field pv.pv_vtv.vtv_ity pv.pv_vtv.vtv_ghost None
(* TODO: devise a good grammar for effect expressions *)
let rec get_eff_expr lenv { pp_desc = d; pp_loc = loc } = match d with
| Ptree.PPvar (Ptree.Qident {id=x}) when Mstr.mem x lenv.let_vars ->
begin match Mstr.find x lenv.let_vars with
| LetV pv -> pv.pv_vs, pv.pv_vtv
| LetV pv -> pv.pv_vs, fd_of_pv pv
| LetA _ -> errorm ~loc "'%s' must be a first-order value" x
end
| Ptree.PPvar p ->
begin match uc_find_ps lenv.mod_uc p with
| PV pv -> pv.pv_vs, pv.pv_vtv
| PV pv -> pv.pv_vs, fd_of_pv pv
| _ -> errorm ~loc:(qloc p) "'%a' must be a variable" print_qualid p
end
| Ptree.PPapp (p, [le]) ->
let vs, vtv = get_eff_expr lenv le in
let vs, fda = get_eff_expr lenv le in
let quit () = errorm ~loc:le.pp_loc "This expression is not a record" in
let pjm = match vtv.vtv_ity.ity_node with
let pjm = match fda.fd_ity.ity_node with
| Ityapp (its,_,_) ->
let pjl = match find_constructors (get_known lenv.mod_uc) its with
| (_,pjl)::_ -> pjl | _ -> quit () in
let add_pj m pj = match pj with
| Some { pl_ls = ls; pl_args = [vtva]; pl_value = vtvv } ->
Mls.add ls (vtva.vtv_ity, vtvv) m
| Some { pl_ls = ls; pl_args = [fda]; pl_value = fdv } ->
Mls.add ls (fda.fd_ity, fdv) m
| Some _ -> assert false
| None -> m in
List.fold_left add_pj Mls.empty pjl
......@@ -1060,40 +1067,41 @@ let rec get_eff_expr lenv { pp_desc = d; pp_loc = loc } = match d with
| (_,pjl)::_ -> pjl | _ -> quit () in
let add_pj m pj = match pj with
| Some ({ ls_args = [tya]; ls_value = Some tyv } as ls) ->
Mls.add ls (ity_of_ty tya, vty_value (ity_of_ty tyv)) m
let fdv = mk_field (ity_of_ty tyv) false None in
Mls.add ls (ity_of_ty tya, fdv) m
| Some _ -> assert false
| None -> m in
List.fold_left add_pj Mls.empty pjl
| _ -> quit ()
in
let itya, vtvv =
let itya, fdv =
try Mls.find (uc_find_ls lenv.mod_uc p) pjm with Not_found ->
errorm ~loc:(qloc p) "'%a' must be a field name" print_qualid p in
let sbs = unify_loc (ity_match ity_subst_empty) loc itya vtv.vtv_ity in
let mut = Opt.map (reg_full_inst sbs) vtvv.vtv_mut in
let ghost = vtv.vtv_ghost || vtvv.vtv_ghost in
vs, vty_value ~ghost ?mut (ity_full_inst sbs vtvv.vtv_ity)
let sbs = unify_loc (ity_match ity_subst_empty) loc itya fda.fd_ity in
let mut = Opt.map (reg_full_inst sbs) fdv.fd_mut in
let ghost = fda.fd_ghost || fdv.fd_ghost in
vs, mk_field (ity_full_inst sbs fdv.fd_ity) ghost mut
| Ptree.PPcast (e,_) | Ptree.PPnamed (_,e) ->
get_eff_expr lenv e
| _ ->
errorm ~loc "unsupported effect expression"
let get_eff_regs lenv fn (eff,svs) le =
let vs, vtv = get_eff_expr lenv le in
match vtv.vtv_mut, vtv.vtv_ity.ity_node with
let vs, fd = get_eff_expr lenv le in
match fd.fd_mut, fd.fd_ity.ity_node with
| Some reg, _ ->
fn eff ?ghost:(Some vtv.vtv_ghost) reg, Svs.add vs svs
fn eff ?ghost:(Some fd.fd_ghost) reg, Svs.add vs svs
| None, Ityapp (its,_,(_::_ as regl)) ->
let csl = find_constructors (get_known lenv.mod_uc) its in
let add_arg ((ngr,ghr) as regs) vtv = match vtv.vtv_mut with
| Some r when vtv.vtv_ghost -> ngr, Sreg.add r ghr
| Some r -> Sreg.add r ngr, ghr
let add_arg ((ngr,ghr) as regs) fd = match fd.fd_mut with
| Some r when fd.fd_ghost -> ngr, Sreg.add r ghr
| Some r -> Sreg.add r ngr, ghr
| None -> regs in
let add_cs regs (cs,_) = List.fold_left add_arg regs cs.pl_args in
let ngr, ghr = List.fold_left add_cs (Sreg.empty,Sreg.empty) csl in
let add_reg eff reg0 reg =
let eff = if not (Sreg.mem reg0 ngr) then eff else
fn eff ?ghost:(Some vtv.vtv_ghost) reg in
fn eff ?ghost:(Some fd.fd_ghost) reg in
let eff = if not (Sreg.mem reg0 ghr) then eff else
fn eff ?ghost:(Some true) reg in
eff in
......@@ -1210,7 +1218,7 @@ let e_app_gh e el =
e_app e (ghostify (decomp e.e_vty, el))
let e_plapp_gh pl el ity =
let ghostify vtv e = e_ghostify vtv.vtv_ghost e in
let ghostify fd e = e_ghostify fd.fd_ghost e in
e_plapp pl (List.map2 ghostify pl.pl_args el) ity
let rec expr lenv de =
......@@ -1254,11 +1262,11 @@ and expr_desc lenv loc de = match de.de_desc with
<