Commit b3563418 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

whyml: drop the "ghost" specifier in user effects

parent 71b2aa03
......@@ -147,8 +147,6 @@ end
let { pe_reads = r2; pe_writes = w2; pe_raises = x2 } = e2 in
{ pe_reads = r1 @ r2; pe_writes = w1 @ w2; pe_raises = x1 @ x2 }
let effect_exprs ghost l = List.map (fun x -> (ghost, x)) l
let spec p (q,xq) ef vl = {
sp_pre = p;
sp_post = q;
......@@ -1357,18 +1355,9 @@ effects:
;
effect:
| READS list1_lexpr_arg
{ { pe_reads = effect_exprs false $2; pe_writes = []; pe_raises = [] } }
| WRITES list1_lexpr_arg
{ { pe_writes = effect_exprs false $2; pe_reads = []; pe_raises = [] } }
| RAISES list1_uqualid
{ { pe_raises = effect_exprs false $2; pe_writes = []; pe_reads = [] } }
| GHOST READS list1_lexpr_arg
{ { pe_reads = effect_exprs true $3; pe_writes = []; pe_raises = [] } }
| GHOST WRITES list1_lexpr_arg
{ { pe_writes = effect_exprs true $3; pe_reads = []; pe_raises = [] } }
| GHOST RAISES list1_uqualid
{ { pe_raises = effect_exprs true $3; pe_writes = []; pe_reads = [] } }
| READS list1_lexpr_arg { { pe_reads = $2; pe_writes = []; pe_raises = [] } }
| WRITES list1_lexpr_arg { { pe_writes = $2; pe_reads = []; pe_raises = [] } }
| RAISES list1_uqualid { { pe_raises = $2; pe_writes = []; pe_reads = [] } }
;
opt_variant:
......
......@@ -191,9 +191,9 @@ type for_direction = To | Downto
type ghost = bool
type effect = {
pe_reads : (ghost * lexpr) list;
pe_writes : (ghost * lexpr) list;
pe_raises : (ghost * qualid) list;
pe_reads : lexpr list;
pe_writes : lexpr list;
pe_raises : qualid list;
}
type pre = lexpr
......
......@@ -260,14 +260,12 @@ let dexception uc qid =
let no_ghost gh =
if gh then errorm "ghost types are not supported in this version of WhyML"
let eff_no_ghost l = List.map (fun (gh,x) -> no_ghost gh; x) l
let dueffect env e =
{ du_reads = eff_no_ghost e.Ptree.pe_reads;
du_writes = eff_no_ghost e.Ptree.pe_writes;
du_raises =
List.map (fun id -> let ls,_,_ = dexception env.uc id in ls)
(eff_no_ghost e.Ptree.pe_raises); }
{ du_reads = e.Ptree.pe_reads;
du_writes = e.Ptree.pe_writes;
du_raises = List.map
(fun id -> let ls,_,_ = dexception env.uc id in ls)
e.Ptree.pe_raises; }
let dpost uc (q, ql) =
let dexn (id, l) = let s, _, _ = dexception uc id in s, l in
......
......@@ -27,16 +27,17 @@ type loc = Loc.position
type ident = Ptree.ident
type ghost = bool
type dpre = Ptree.pre
type dpost = Ptree.pre
type dxpost = dpost Mexn.t
type dinvariant = Ptree.lexpr option
type dvariant = Ptree.lexpr * Term.lsymbol option
type dinvariant = Ptree.lexpr option
type deffect = {
deff_reads : (ghost * Ptree.lexpr) list;
deff_writes : (ghost * Ptree.lexpr) list;
deff_raises : (ghost * xsymbol) list;
deff_reads : Ptree.lexpr list;
deff_writes : Ptree.lexpr list;
deff_raises : xsymbol list;
}
type dspec = {
......
......@@ -368,7 +368,7 @@ let dbinders denv bl =
let deff_of_peff uc pe =
{ deff_reads = pe.pe_reads;
deff_writes = pe.pe_writes;
deff_raises = List.map (fun (gh,q) -> gh, find_xsymbol uc q) pe.pe_raises; }
deff_raises = List.map (find_xsymbol uc) pe.pe_raises; }
exception DuplicateException of xsymbol
......@@ -854,54 +854,58 @@ let rec get_eff_expr lenv { pp_desc = d; pp_loc = loc } = match d with
| _ ->
errorm ~loc "unsupported effect expression"
let get_eff_regs lenv fn (eff,svs) ghost le =
let get_eff_regs lenv fn (eff,svs) le =
let vs, vtv = get_eff_expr lenv le in
let ghost = ghost || vtv.vtv_ghost in
match vtv.vtv_mut, vtv.vtv_ity.ity_node with
| Some reg, _ ->
fn eff ?ghost:(Some ghost) reg, Svs.add vs svs
fn eff ?ghost:(Some vtv.vtv_ghost) reg, Svs.add vs svs
| None, Ityapp (its,_,(_::_ as regl)) ->
let add_arg regs vtv = match vtv.vtv_mut with
| Some r when vtv.vtv_ghost -> Sreg.add r regs | _ -> regs in
let add_cs regs (cs,_) = List.fold_left add_arg regs cs.pl_args in
let csl = find_constructors (get_known lenv.mod_uc) its in
let ghost_regs = List.fold_left add_cs Sreg.empty csl 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
| 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 ghost = ghost || Sreg.mem reg0 ghost_regs in
fn eff ?ghost:(Some ghost) reg in
let eff = if not (Sreg.mem reg0 ngr) then eff else
fn eff ?ghost:(Some vtv.vtv_ghost) reg in
let eff = if not (Sreg.mem reg0 ghr) then eff else
fn eff ?ghost:(Some true) reg in
eff in
List.fold_left2 add_reg eff its.its_regs regl, Svs.add vs svs
| _ ->
errorm ~loc:le.pp_loc "mutable expression expected"
let eff_of_deff lenv deff =
let acc = eff_empty, Svs.empty in
let add_read acc (gh,e) = get_eff_regs lenv eff_read acc gh e in
let add_read acc e = get_eff_regs lenv eff_read acc e in
let acc = List.fold_left add_read acc deff.deff_reads in
let add_write acc (gh,e) = get_eff_regs lenv eff_write acc gh e in
let add_write acc e = get_eff_regs lenv eff_write acc e in
let eff, svs = List.fold_left add_write acc deff.deff_writes in
let add_raise eff (gh,xs) = eff_raise eff ~ghost:gh xs in
let eff = List.fold_left add_raise eff deff.deff_raises in
eff, svs
List.fold_left (eff_raise ~ghost:false) eff deff.deff_raises, svs
let check_user_effect lenv e dsp =
let acc = eff_empty, Svs.empty in
let read le eff ?(ghost=false) reg =
if (not ghost && Sreg.mem reg e.e_effect.eff_reads) ||
(ghost && Sreg.mem reg e.e_effect.eff_ghostr)
ignore ghost;
if Sreg.mem reg e.e_effect.eff_reads ||
Sreg.mem reg e.e_effect.eff_ghostr
then eff else Loc.errorm ~loc:le.pp_loc
"this read effect never happens in the expression" in
let check_read (gh,e) = ignore (get_eff_regs lenv (read e) acc gh e) in
let check_read e = ignore (get_eff_regs lenv (read e) acc e) in
List.iter check_read dsp.ds_effect.deff_reads;
let write le eff ?(ghost=false) reg =
if (not ghost && Sreg.mem reg e.e_effect.eff_writes) ||
(ghost && Sreg.mem reg e.e_effect.eff_ghostw)
ignore ghost;
if Sreg.mem reg e.e_effect.eff_writes ||
Sreg.mem reg e.e_effect.eff_ghostw
then eff else Loc.errorm ~loc:le.pp_loc
"this write effect never happens in the expression" in
let check_write (gh,e) = ignore (get_eff_regs lenv (write e) acc gh e) in
let check_write e = ignore (get_eff_regs lenv (write e) acc e) in
List.iter check_write dsp.ds_effect.deff_writes;
let check_raise (ghost,xs) =
if (not ghost && Sexn.mem xs e.e_effect.eff_raises) ||
(ghost && Sexn.mem xs e.e_effect.eff_ghostx)
let check_raise xs =
if Sexn.mem xs e.e_effect.eff_raises ||
Sexn.mem xs e.e_effect.eff_ghostx
then () else Loc.errorm
"this expression does not raise exception %a" print_xs xs in
List.iter check_raise dsp.ds_effect.deff_raises
......
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