Commit 4aee41ca authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: move ghost info out of vty_(value|arrow)

Instead, we now store the ghostness boolean directly
in pvsymbols, pssymbols, ppatterns, and exprs. We thus
remove one level of indirection, and vty_value becomes
a one-field record which we remove in the next commit.
parent fa45d3df
......@@ -394,7 +394,7 @@ let check_ghost lkn kn d =
raise (GhostRaise (e_void, Sexn.choose eff.eff_ghostx));
let pvs = List.fold_right Spv.add vta.vta_args pvs in
let test pv =
if pv.pv_vtv.vtv_ghost then () else
if pv.pv_ghost then () else
access eff.eff_ghostw pv.pv_vtv.vtv_ity
in
Spv.iter test pvs;
......@@ -403,7 +403,7 @@ let check_ghost lkn kn d =
| VTvalue _ -> ()
in
let check ps =
if ps.ps_vta.vta_ghost then () else
if ps.ps_ghost then () else
check (ps_pvset Spv.empty ps) ps.ps_vta
in
match d.pd_node with
......
......@@ -37,7 +37,7 @@ type dspec = {
type dbinder = ident * ghost * dity
type dtype_v =
| DSpecV of ghost * dity
| DSpecV of dity
| DSpecA of dbinder list * dtype_c
and dtype_c = dtype_v * dspec
......
This diff is collapsed.
......@@ -62,6 +62,7 @@ val pl_clone : Theory.symbol_map -> symbol_map
type ppattern = private {
ppat_pattern : pattern;
ppat_vtv : vty_value;
ppat_ghost : bool;
ppat_effect : effect;
}
......@@ -73,7 +74,8 @@ type pre_ppattern =
| PPor of pre_ppattern * pre_ppattern
| PPas of pre_ppattern * preid
val make_ppattern : pre_ppattern -> vty_value -> pvsymbol Mstr.t * ppattern
val make_ppattern :
pre_ppattern -> ?ghost:bool -> vty_value -> pvsymbol Mstr.t * ppattern
(** program symbols *)
......@@ -84,6 +86,7 @@ val make_ppattern : pre_ppattern -> vty_value -> pvsymbol Mstr.t * ppattern
type psymbol = private {
ps_name : ident;
ps_vta : vty_arrow;
ps_ghost : bool;
ps_varm : varmap;
ps_vars : varset;
(* this varset covers the type variables and regions of the defining
......@@ -101,9 +104,10 @@ module Wps : Weakhtbl.S with type key = psymbol
val ps_equal : psymbol -> psymbol -> bool
val create_psymbol : preid -> vty_arrow -> psymbol
val create_psymbol : preid -> ?ghost:bool -> vty_arrow -> psymbol
val create_psymbol_extra : preid -> vty_arrow -> Spv.t -> Sps.t -> psymbol
val create_psymbol_extra :
preid -> ?ghost:bool -> vty_arrow -> Spv.t -> Sps.t -> psymbol
val spec_pvset : Spv.t -> spec -> Spv.t
val ps_pvset : Spv.t -> psymbol -> Spv.t
......@@ -125,6 +129,7 @@ type let_sym =
type expr = private {
e_node : expr_node;
e_vty : vty;
e_ghost : bool;
e_effect : effect;
e_varm : varmap;
e_label : Slab.t;
......
......@@ -416,10 +416,10 @@ let clone_export uc m inst =
let nr = create_region (id_clone r.reg_name) (conv_ity r.reg_ity) in
Hreg.replace regh r nr;
nr in
let conv_vtv v =
vty_value ~ghost:v.vtv_ghost (conv_ity v.vtv_ity) in
let conv_vtv v = vty_value (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
create_pvsymbol (id_clone pv.pv_vs.vs_name)
~ghost:pv.pv_ghost (conv_vtv pv.pv_vtv) in
let psh = Hid.create 3 in
let conv_xs xs = try match Hid.find psh xs.xs_name with
| XS xs -> xs | _ -> assert false with Not_found -> xs in
......@@ -456,7 +456,7 @@ let clone_export uc m inst =
let vty = match a.vta_result with
| VTarrow a -> VTarrow (conv_vta mv a)
| VTvalue v -> VTvalue (conv_vtv v) in
vty_arrow args ~spec ~ghost:a.vta_ghost vty in
vty_arrow args ~spec vty in
let mvs = ref (Mvs.singleton Mlw_wp.pv_old.pv_vs Mlw_wp.pv_old.pv_vs) in
let add_pdecl uc d = { uc with
muc_decls = d :: uc.muc_decls;
......@@ -484,7 +484,7 @@ let clone_export uc m inst =
add_pdecl uc (create_val_decl (LetV npv))
| PDval (LetA ps) ->
let vta = conv_vta !mvs ps.ps_vta in
let nps = create_psymbol (id_clone ps.ps_name) vta in
let nps = create_psymbol (id_clone ps.ps_name) ~ghost:ps.ps_ghost vta in
Hid.add psh ps.ps_name (PS nps);
add_pdecl uc (create_val_decl (LetA nps))
| PDrec fdl ->
......@@ -513,7 +513,7 @@ let clone_export uc m inst =
let vta = conv_vta !mvs ps.ps_vta in
(* we must retrieve all pvsymbols and psymbols in ps.ps_varm *)
let pvs,pss = Mid.fold add_id ps.ps_varm (Spv.empty,Sps.empty) in
let nps = create_psymbol_extra id vta pvs pss in
let nps = create_psymbol_extra id ~ghost:ps.ps_ghost vta pvs pss in
Hid.add psh ps.ps_name (PS nps);
add_pdecl uc (create_val_decl (LetA nps)) in
List.fold_left conv_fd uc fdl
......
......@@ -446,7 +446,7 @@ and print_app pri ls info fmt tl =
and print_tnode pri info fmt t = match t.t_node with
| Tvar v ->
let gh = try (restore_pv v).pv_vtv.vtv_ghost with Not_found -> false in
let gh = try (restore_pv v).pv_ghost with Not_found -> false in
if gh then fprintf fmt "()" else print_vs fmt v
| Tconst c ->
print_const fmt c
......@@ -609,12 +609,12 @@ open Mlw_module
let print_its info fmt ts = print_ts info fmt ts.its_ts
let print_pv info fmt pv =
if pv.pv_vtv.vtv_ghost then
if pv.pv_ghost then
fprintf fmt "((* ghost %a *))" (print_lident info) pv.pv_vs.vs_name
else
print_lident info fmt pv.pv_vs.vs_name
let print_ps info fmt ps =
if ps.ps_vta.vta_ghost then
if ps.ps_ghost then
fprintf fmt "((* ghost %a *))" (print_lident info) ps.ps_name
else
print_lident info fmt ps.ps_name
......@@ -667,7 +667,7 @@ let print_ity info = print_ity_node false info
let print_vtv info fmt vtv = print_ity info fmt vtv.vtv_ity
let print_pvty info fmt pv =
if pv.pv_vtv.vtv_ghost then fprintf fmt "((* ghost *))" else
if pv.pv_ghost then fprintf fmt "((* ghost *))" else
fprintf fmt "@[(%a:@ %a)@]"
(print_lident info) pv.pv_vs.vs_name (print_vtv info) pv.pv_vtv
......@@ -689,7 +689,7 @@ let ity_mark = ity_pur Mlw_wp.ts_mark []
let rec print_expr info fmt e = print_lexpr 0 info fmt e
and print_lexpr pri info fmt e =
if vty_ghost e.e_vty then
if e.e_ghost then
fprintf fmt "((* ghost *))"
else match e.e_node with
| Elogic t ->
......@@ -702,7 +702,7 @@ and print_lexpr pri info fmt e =
| None -> print_ps info fmt a end
| Eapp (e,v,_) ->
fprintf fmt "(%a@ %a)" (print_lexpr pri info) e (print_pv info) v
| Elet ({ let_expr = e1 }, e2) when vty_ghost e1.e_vty ->
| Elet ({ let_expr = e1 }, e2) when e1.e_ghost ->
print_expr info fmt e2
| Elet ({ let_sym = LetV pv }, e2)
when ity_equal pv.pv_vtv.vtv_ity ity_mark ->
......@@ -753,7 +753,7 @@ and print_lexpr pri info fmt e =
| Eany _ ->
fprintf fmt "@[(%a :@ %a)@]" to_be_implemented "any"
(print_vty info) e.e_vty
| Ecase (e1, [_,e2]) when vty_ghost e1.e_vty ->
| Ecase (e1, [_,e2]) when e1.e_ghost ->
print_lexpr pri info fmt e2
| Ecase (e1, bl) ->
fprintf fmt "@[(match @[%a@] with@\n@[<hov>%a@])@]"
......@@ -761,14 +761,14 @@ and print_lexpr pri info fmt e =
| Erec (fdl, e) ->
(* print non-ghost first *)
let cmp {fun_ps=ps1} {fun_ps=ps2} =
Pervasives.compare ps1.ps_vta.vta_ghost ps2.ps_vta.vta_ghost in
Pervasives.compare ps1.ps_ghost ps2.ps_ghost in
let fdl = List.sort cmp fdl in
fprintf fmt "@[<v>%a@\nin@\n%a@]"
(print_list_next newline (print_rec_decl (is_letrec fdl) info)) fdl
(print_expr info) e
and print_rec lr info fst fmt { fun_ps = ps ; fun_lambda = lam } =
if ps.ps_vta.vta_ghost then
if ps.ps_ghost then
fprintf fmt "(* %s %a *)"
(if fst then if lr then "let rec" else "let" else "with")
(print_ps info) ps
......@@ -815,8 +815,8 @@ let lv_name = function
| LetA ps -> ps.ps_name
let is_ghost_lv = function
| LetV pv -> pv.pv_vtv.vtv_ghost
| LetA ps -> ps.ps_vta.vta_ghost
| LetV pv -> pv.pv_ghost
| LetA ps -> ps.ps_ghost
let print_let_decl info fmt ld =
if is_ghost_lv ld.let_sym then
......@@ -974,8 +974,8 @@ let pdecl info fmt pd = match pd.pd_node with
(* print defined, non-ghost first *)
let cmp {fun_ps=ps1} {fun_ps=ps2} =
Pervasives.compare
(ps1.ps_vta.vta_ghost || has_syntax info ps1.ps_name)
(ps2.ps_vta.vta_ghost || has_syntax info ps2.ps_name) in
(ps1.ps_ghost || has_syntax info ps1.ps_name)
(ps2.ps_ghost || has_syntax info ps2.ps_name) in
let fdl = List.sort cmp fdl in
print_list_next newline (print_rec_decl (is_letrec fdl) info) fmt fdl;
fprintf fmt "@\n@\n"
......
......@@ -57,7 +57,7 @@ let print_reg fmt reg =
fprintf fmt "%s" (id_unique rprinter reg.reg_name)
let print_pv fmt pv =
fprintf fmt "%s%a" (if pv.pv_vtv.vtv_ghost then "?" else "")
fprintf fmt "%s%a" (if pv.pv_ghost then "?" else "")
print_vs pv.pv_vs
let forget_pv pv = forget_var pv.pv_vs
......@@ -68,7 +68,7 @@ let print_name fmt id =
let print_xs fmt xs = print_name fmt xs.xs_name
let print_ps fmt ps =
fprintf fmt "%s%a" (if ps.ps_vta.vta_ghost then "?" else "")
fprintf fmt "%s%a" (if ps.ps_ghost then "?" else "")
print_name ps.ps_name
let forget_ps ps = forget_id iprinter ps.ps_name
......@@ -125,7 +125,7 @@ let print_effect fmt eff =
Mreg.iter print_reset eff.eff_resets
let print_vtv fmt vtv =
fprintf fmt "%s%a" (if vtv.vtv_ghost then "?" else "") print_ity vtv.vtv_ity
fprintf fmt "%a" print_ity vtv.vtv_ity
let rec print_vta fmt vta =
let print_arg fmt pv = fprintf fmt "%a ->@ " print_vtv pv.pv_vtv in
......
......@@ -601,6 +601,8 @@ let eff_ghostify e = {
eff_resets = e.eff_resets;
}
let eff_ghostify gh e = if gh then eff_ghostify e else e
let eff_read e ?(ghost=false) r = if ghost
then { e with eff_ghostr = Sreg.add r e.eff_ghostr }
else { e with eff_reads = Sreg.add r e.eff_reads }
......@@ -786,17 +788,17 @@ let spec_check c ty =
type vty_value = {
vtv_ity : ity;
vtv_ghost : bool;
}
let vty_value ?(ghost=false) ity = { vtv_ity = ity; vtv_ghost = ghost }
let vty_value ity = { vtv_ity = ity; }
let vtv_vars vtv = vtv.vtv_ity.ity_vars
type pvsymbol = {
pv_vs : vsymbol;
pv_vtv : vty_value;
pv_vars : varset;
pv_vs : vsymbol;
pv_vtv : vty_value;
pv_ghost : bool;
pv_vars : varset;
}
module PVsym = MakeMSHW (struct
......@@ -811,16 +813,17 @@ module Wpv = PVsym.W
let pv_equal : pvsymbol -> pvsymbol -> bool = (==)
let create_pvsymbol id vtv = {
pv_vs = create_vsymbol id (ty_of_ity vtv.vtv_ity);
pv_vtv = vtv;
pv_vars = vtv_vars vtv;
let create_pvsymbol id ghost vtv = {
pv_vs = create_vsymbol id (ty_of_ity vtv.vtv_ity);
pv_vtv = vtv;
pv_ghost = ghost;
pv_vars = vtv_vars vtv;
}
let create_pvsymbol, restore_pv, restore_pv_by_id =
let id_to_pv = Wid.create 17 in
(fun id vtv ->
let pv = create_pvsymbol id vtv in
(fun id ?(ghost=false) vtv ->
let pv = create_pvsymbol id ghost vtv in
Wid.set id_to_pv pv.pv_vs.vs_name pv;
pv),
(fun vs -> Wid.find id_to_pv vs.vs_name),
......@@ -836,7 +839,6 @@ and vty_arrow = {
vta_args : pvsymbol list;
vta_result : vty;
vta_spec : spec;
vta_ghost : bool;
}
let rec vta_vars vta =
......@@ -847,10 +849,6 @@ and vty_vars = function
| VTvalue vtv -> vtv_vars vtv
| VTarrow vta -> vta_vars vta
let vty_ghost = function
| VTvalue vtv -> vtv.vtv_ghost
| VTarrow vta -> vta.vta_ghost
let ity_of_vty = function
| VTvalue vtv -> vtv.vtv_ity
| VTarrow _ -> ity_unit
......@@ -861,14 +859,13 @@ let ty_of_vty = function
let spec_check spec vty = spec_check spec (ty_of_vty vty)
let vty_arrow_unsafe argl spec ghost vty = {
let vty_arrow_unsafe argl spec vty = {
vta_args = argl;
vta_result = vty;
vta_spec = spec;
vta_ghost = ghost || vty_ghost vty;
}
let vty_arrow argl ?spec ?(ghost=false) vty =
let vty_arrow argl ?spec vty =
let exn = Invalid_argument "Mlw.vty_arrow" in
(* the arguments must be all distinct *)
if argl = [] then raise exn;
......@@ -880,7 +877,7 @@ let vty_arrow argl ?spec ?(ghost=false) vty =
(* we admit non-empty variant list even for null letrec,
so that we can store there external variables from
user-written effects to save them from spec_filter *)
vty_arrow_unsafe argl spec ghost vty
vty_arrow_unsafe argl spec vty
(* this only compares the types of arguments and results, and ignores
the spec. In other words, only the type variables and regions
......@@ -905,10 +902,9 @@ let rec vta_vars_match s a1 a2 =
but also every type variable and every region in vta_spec *)
let vta_full_inst sbs vta =
let tvm = Mtv.map ty_of_ity sbs.ity_subst_tv in
let vtv_inst { vtv_ity = ity; vtv_ghost = ghost } =
vty_value ~ghost (ity_full_inst sbs ity) in
let pv_inst { pv_vs = vs; pv_vtv = vtv } =
create_pvsymbol (id_clone vs.vs_name) (vtv_inst vtv) in
let vtv_inst { vtv_ity = ity } = vty_value (ity_full_inst sbs ity) in
let pv_inst { pv_vs = vs; pv_vtv = vtv; pv_ghost = ghost } =
create_pvsymbol (id_clone vs.vs_name) ~ghost (vtv_inst vtv) in
let add_arg vsm pv =
let nv = pv_inst pv in
Mvs.add pv.pv_vs (t_var nv.pv_vs) vsm, nv in
......@@ -918,7 +914,7 @@ let vta_full_inst sbs vta =
let vty = match vta.vta_result with
| VTarrow vta -> VTarrow (vta_inst vsm vta)
| VTvalue vtv -> VTvalue (vtv_inst vtv) in
vty_arrow_unsafe args spec vta.vta_ghost vty
vty_arrow_unsafe args spec vty
in
vta_inst Mvs.empty vta
......@@ -949,18 +945,11 @@ let rec vta_filter varm vars vta =
let eff = reg_fold on_reg v.vtv_ity.ity_vars spec.c_effect in
{ spec with c_effect = eff }
| VTarrow _ -> spec in
vty_arrow_unsafe vta.vta_args spec vta.vta_ghost vty
vty_arrow_unsafe vta.vta_args spec vty
let vta_filter varm vta =
vta_filter varm (vars_merge varm vars_empty) vta
let vtv_ghostify vtv = { vtv with vtv_ghost = true }
let vta_ghostify vta = { vta with vta_ghost = true }
let vty_ghostify = function
| VTvalue vtv -> VTvalue (vtv_ghostify vtv)
| VTarrow vta -> VTarrow (vta_ghostify vta)
let vta_app vta pv =
let vtv = pv.pv_vtv in
let arg, rest = match vta.vta_args with
......@@ -971,13 +960,12 @@ let vta_app vta pv =
| VTarrow a when not (List.exists (pv_equal arg) a.vta_args) ->
let result = vty_subst a.vta_result in
let spec = spec_subst sbs a.vta_spec in
VTarrow (vty_arrow_unsafe a.vta_args spec a.vta_ghost result)
VTarrow (vty_arrow_unsafe a.vta_args spec result)
| vty -> vty in
let result = vty_subst vta.vta_result in
let spec = spec_subst sbs vta.vta_spec in
if not vtv.vtv_ghost && arg.pv_vtv.vtv_ghost then
if not pv.pv_ghost && arg.pv_ghost then
Loc.errorm "non-ghost value passed as a ghost argument";
let ghost =
vta.vta_ghost || (vtv.vtv_ghost && not arg.pv_vtv.vtv_ghost) in
if rest = [] then spec, (if ghost then vty_ghostify result else result)
else spec_empty ty_unit, VTarrow (vty_arrow_unsafe rest spec ghost result)
let ghost = pv.pv_ghost && not arg.pv_ghost in
if rest = [] then spec, ghost, result
else spec_empty ty_unit, ghost, VTarrow (vty_arrow_unsafe rest spec result)
......@@ -209,7 +209,7 @@ type effect = private {
val eff_empty : effect
val eff_union : effect -> effect -> effect
val eff_ghostify : effect -> effect
val eff_ghostify : bool -> effect -> effect
val eff_read : effect -> ?ghost:bool -> region -> effect
val eff_write : effect -> ?ghost:bool -> region -> effect
......@@ -256,15 +256,15 @@ type spec = {
type vty_value = private {
vtv_ity : ity;
vtv_ghost : bool;
}
val vty_value : ?ghost:bool -> ity -> vty_value
val vty_value : ity -> vty_value
type pvsymbol = private {
pv_vs : vsymbol;
pv_vtv : vty_value;
pv_vars : varset;
pv_vs : vsymbol;
pv_vtv : vty_value;
pv_ghost : bool;
pv_vars : varset;
}
module Mpv : Extmap.S with type key = pvsymbol
......@@ -274,7 +274,7 @@ module Wpv : Weakhtbl.S with type key = pvsymbol
val pv_equal : pvsymbol -> pvsymbol -> bool
val create_pvsymbol : preid -> vty_value -> pvsymbol
val create_pvsymbol : preid -> ?ghost:bool -> vty_value -> pvsymbol
val restore_pv : vsymbol -> pvsymbol
(* raises Not_found if the argument is not a pv_vs *)
......@@ -292,13 +292,12 @@ and vty_arrow = private {
vta_args : pvsymbol list;
vta_result : vty;
vta_spec : spec;
vta_ghost : bool;
}
exception UnboundException of xsymbol
(* every raised exception must have a postcondition in spec.c_xpost *)
val vty_arrow : pvsymbol list -> ?spec:spec -> ?ghost:bool -> vty -> vty_arrow
val vty_arrow : pvsymbol list -> ?spec:spec -> vty -> vty_arrow
(* this only compares the types of arguments and results, and ignores
the spec. In other words, only the type variables and regions in
......@@ -315,11 +314,7 @@ val vta_full_inst : ity_subst -> vty_arrow -> vty_arrow
val vta_filter : varmap -> vty_arrow -> vty_arrow
(* apply a function specification to a variable argument *)
val vta_app : vty_arrow -> pvsymbol -> spec * vty
(* test for ghostness and convert to ghost *)
val vty_ghost : vty -> bool
val vty_ghostify : vty -> vty
val vta_app : vty_arrow -> pvsymbol -> spec * bool * vty
(* verify that the spec corresponds to the result type *)
val spec_check : spec -> vty -> unit
......
......@@ -422,7 +422,7 @@ let rec dtype_c denv (tyv, sp) =
and dtype_v denv = function
| Tpure pty ->
let dity = dity_of_pty denv pty in
DSpecV (false,dity), ([],dity)
DSpecV dity, ([],dity)
| Tarrow (bl,tyc) ->
let denv,bl,tyl = dbinders denv bl in
let tyc,(argl,res) = dtype_c denv tyc in
......@@ -710,9 +710,9 @@ let rec rtype_c denv (tyv, sp) =
let tyv, dvty = rtype_v denv tyv in (tyv, sp), dvty
and rtype_v denv = function
| DSpecV (gh, dity) ->
| DSpecV dity ->
let dity = dity_refresh dity in
DSpecV (gh,dity), ([],dity)
DSpecV dity, ([],dity)
| DSpecA (bl,tyc) ->
let denv,bl,tyl = rbinders denv bl in
let tyc,(argl,res) = rtype_c denv tyc in
......@@ -1025,8 +1025,8 @@ let add_local x lv lenv = match lv with
let binders bl =
let binder (id, ghost, dity) =
let vtv = vty_value ~ghost (ity_of_dity dity) in
create_pvsymbol (Denv.create_user_id id) vtv in
let vtv = vty_value (ity_of_dity dity) in
create_pvsymbol (Denv.create_user_id id) ~ghost vtv in
List.map binder bl
let add_binders lenv pvl =
......@@ -1034,7 +1034,7 @@ let add_binders lenv pvl =
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
let fd_of_pv pv = mk_field pv.pv_vtv.vtv_ity pv.pv_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
......@@ -1152,8 +1152,8 @@ let spec_of_dspec lenv eff vty dsp = {
c_letrec = 0;
}
let rec type_c lenv gh pvs vars (dtyv, dsp) =
let vty = type_v lenv gh pvs vars dtyv in
let rec type_c lenv pvs vars (dtyv, dsp) =
let vty = type_v lenv pvs vars dtyv in
let eff, esvs = eff_of_deff lenv dsp in
(* reset every new region in the result *)
let eff = match vty with
......@@ -1187,23 +1187,21 @@ let rec type_c lenv gh pvs vars (dtyv, dsp) =
(* add the invariants *)
spec_invariant lenv pvs vty spec, vty
and type_v lenv gh pvs vars = function
| DSpecV (ghost,v) ->
let ghost = ghost || gh in
VTvalue (vty_value ~ghost (ity_of_dity v))
and type_v lenv pvs vars = function
| DSpecV v ->
VTvalue (vty_value (ity_of_dity v))
| DSpecA (bl,tyc) ->
let pvl = binders bl in
let lenv = add_binders lenv pvl in
let add_pv pv s = vars_union pv.pv_vars s in
let vars = List.fold_right add_pv pvl vars in
let pvs = List.fold_right Spv.add pvl pvs in
let spec, vty = type_c lenv gh pvs vars tyc in
let spec, vty = type_c lenv pvs vars tyc in
VTarrow (vty_arrow pvl ~spec vty)
(* expressions *)
let e_ghostify gh e =
if gh && not (vty_ghost e.e_vty) then e_ghost e else e
let e_ghostify gh e = if gh && not e.e_ghost then e_ghost e else e
let e_app_gh e el =
let rec decomp = function
......@@ -1213,7 +1211,7 @@ let e_app_gh e el =
| _, [] -> []
| [], _ -> assert false
| pv :: pvl, e :: el ->
e_ghostify pv.pv_vtv.vtv_ghost e :: ghostify (pvl, el)
e_ghostify pv.pv_ghost e :: ghostify (pvl, el)
in
e_app e (ghostify (decomp e.e_vty, el))
......@@ -1261,23 +1259,23 @@ and expr_desc lenv loc de = match de.de_desc with
| LetA ps -> ps.ps_name | LetV pv -> pv.pv_vs.vs_name in
let lenv = add_local x.id def1.let_sym lenv in
let e2 = expr lenv de2 in
let ghost_unit = match e2.e_vty with
| VTvalue { vtv_ghost = true; vtv_ity = ity } ->
ity_equal ity ity_unit
let e2_unit = match e2.e_vty with
| VTvalue { vtv_ity = ity } -> ity_equal ity ity_unit
| _ -> false in
let e2 =
if ghost_unit (* e2 is ghost unit *)
&& not (vty_ghost e1.e_vty) (* and e1 is non-ghost *)
if e2_unit (* e2 is ghost unit *)
&& e2.e_ghost (* and e2 is ghost *)
&& not e1.e_ghost (* and e1 is non-ghost *)
&& not (Mid.mem name e2.e_varm) (* and x doesn't occur in e2 *)
then e_let (create_let_defn (id_fresh "gh") e2) e_void else e2 in
e_let def1 e2 in
let rec flatten e1 = match e1.e_node with
| Elet (ld,_) (* can't let a non-ghost expr from a ghost one *)
when gh && not (vty_ghost ld.let_expr.e_vty) -> mk_expr e1
when gh && not ld.let_expr.e_ghost -> mk_expr e1
| Elet (ld,e1) -> e_let ld (flatten e1)
| _ -> mk_expr e1 in
begin match e1.e_vty with
| VTarrow { vta_ghost = true } when not gh ->
| VTarrow _ when e1.e_ghost && not gh ->
errorm ~loc "%s must be a ghost function" x.id
| VTarrow _ -> flatten e1
| VTvalue _ -> mk_expr e1
......@@ -1321,7 +1319,7 @@ and expr_desc lenv loc de = match de.de_desc with
let e1 = expr lenv de1 in
let vtv = vtv_of_expr e1 in
let branch (pp,de) =
let vm, pp = make_ppattern pp vtv in
let vm, pp = make_ppattern pp ~ghost:e1.e_ghost vtv in
let lenv = Mstr.fold (fun s pv -> add_local s (LetV pv)) vm lenv in
pp, expr lenv de in
e_case e1 (List.map branch bl)
......@@ -1386,7 +1384,7 @@ and expr_desc lenv loc de = match de.de_desc with
let lenv = add_local x.id ld.let_sym lenv in
e_let ld (expr lenv de1)
| DEany dtyc ->
let spec, result = type_c lenv false Spv.empty vars_empty dtyc in
let spec, result = type_c lenv Spv.empty vars_empty dtyc in
e_any spec result
| DEghost de1 ->
e_ghostify true (expr lenv de1)
......@@ -1409,9 +1407,9 @@ and expr_desc lenv loc de = match de.de_desc with
and expr_rec lenv dfdl =
let step1 lenv (id, gh, _, bl, ((de, _) as tr)) =
let pvl = binders bl in
let vta = vty_arrow pvl ~ghost:gh (vty_of_dvty de.de_type) in
let vta = vty_arrow pvl (vty_of_dvty de.de_type) in
let vta = vta_filter Mid.empty vta (* add reset effects *) in
let ps = create_psymbol (Denv.create_user_id id) vta in
let ps = create_psymbol (Denv.create_user_id id) ~ghost:gh vta in
add_local id.id (LetA ps) lenv, (ps, gh, pvl, tr) in
let lenv, fdl = Lists.map_fold_left step1 lenv dfdl in
let step2 (ps, gh, pvl, tr) = ps, expr_lam lenv gh pvl tr in
......@@ -1451,7 +1449,7 @@ and expr_fun lenv x gh bl (_, dsp as tr) =
and expr_lam lenv gh pvl (de, dsp) =
let lenv = add_binders lenv pvl in
let e = e_ghostify gh (expr lenv de) in
if not gh && vty_ghost e.e_vty then
if not gh && e.e_ghost then
errorm ~loc:de.de_loc "ghost body in a non-ghost function";
let spec = spec_of_dspec lenv e.e_effect e.e_vty dsp in
{ l_args = pvl; l_expr = e; l_spec = spec }
......@@ -1950,7 +1948,7 @@ let add_pdecl ~wp loc uc = function
create_rec_decl [fd]
| _ ->
let e = e_ghostify gh (expr (create_lenv uc) e) in
if not gh && vty_ghost e.e_vty then
if not gh && e.e_ghost then
errorm ~loc "%s must be a ghost variable" id.id;
let def = create_let_defn (Denv.create_user_id id) e in
create_let_decl def in
......@@ -1967,16 +1965,12 @@ let add_pdecl ~wp loc uc = function
add_pdecl_with_tuples ~wp uc pd
| Dparam (id, gh, tyv) ->
let tyv, _ = dtype_v (create_denv uc) tyv in
let tyv = type_v (create_lenv uc) gh Spv.empty vars_empty tyv in
let tyv = type_v (create_lenv uc) Spv.empty vars_empty tyv in
let lv = match tyv with
| VTvalue v ->
if v.vtv_ghost && not gh then
errorm ~loc "%s must be a ghost variable" id.id;
LetV (create_pvsymbol (Denv.create_user_id id) v)
LetV (create_pvsymbol (Denv.create_user_id id) ~ghost:gh v)
| VTarrow a ->
if a.vta_ghost && not gh then
errorm ~loc "%s must be a ghost function" id.id;
LetA (create_psymbol (Denv.create_user_id id) a) in
LetA (create_psymbol (Denv.create_user_id id) ~ghost:gh a) in
let pd = create_val_decl lv in
add_pdecl_with_tuples ~wp uc pd
......
......@@ -734,7 +734,7 @@ and wp_desc env e q xq = match e.e_node with
| _ ->
let id = id_fresh ?loc:e1.e_loc "o" in
(* must be a pvsymbol or restore_pv will fail *)
let npv = create_pvsymbol id (vtv_of_expr e1) in
let npv = create_pvsymbol id ~ghost:e1.e_ghost (vtv_of_expr e1) in
npv.pv_vs, t_var npv.pv_vs
in
let res, t = get_term e1 in
......
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