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

Mlw: allow non-ghost expressions to return (partially) ghost values

this is still work in progress and no testing was done so far.

Highlights of this commit:

- "(ghost 42, 15)" is now a non-ghost expression that can be returned
  from a function and/or matched against a "(ghost x, y)" pattern.
  Only the tuple constructor and direct pattern matching are magical:
  "let z = (ghost 42, 15) in ..." still makes z ghost, and therefore
  "snd (ghost 42, 15)" is ghost, too.

- "if c then e1 else ghost e2" and "let z = e1 in ghost e2" are now
  non-ghost expressions with a ghost result. This means that e1 may
  have visible effects. Of course, if e2 raises exceptions, the whole
  expression is ghostified. Contamination is still done when possible,
  that is, when the contaminated expression has no visible effects.

- "let ghost x = e1 in e2" no longer ghostifies e1.

- "let f (ghost x) = ... in f e1" no longer ghostifies e1.

- new syntax: variables in program patterns may be marked ghost.
  In particular: "let x, ghost y = ...".

- new syntax: the function result type may be written as a partially
  ghost tuple: "val f ... : ghost int" or "any (int, ghost bool)".
  The ghostness annotation is required for top-level and recursive
  functions.

- exceptions can carry partially ghost tuples (API only, WIP)
parent fbedf74b
......@@ -353,10 +353,10 @@ type dpattern = {
type dpattern_node =
| DPwild
| DPvar of preid
| DPvar of preid * bool
| DPapp of rsymbol * dpattern list
| DPas of dpattern * preid * bool
| DPor of dpattern * dpattern
| DPas of dpattern * preid
| DPcast of dpattern * ity
(** Specifications *)
......@@ -405,8 +405,8 @@ and dexpr_node =
| DEls of lsymbol
| DEconst of Number.constant
| DEapp of dexpr * dexpr
| DEfun of dbinder list * dspec later * dexpr
| DEany of dbinder list * dspec later * dity
| DEfun of dbinder list * mask * dspec later * dexpr
| DEany of dbinder list * mask * dspec later * dity
| DElet of dlet_defn * dexpr
| DErec of drec_defn * dexpr
| DEnot of dexpr
......@@ -435,7 +435,7 @@ and dlet_defn = preid * ghost * rs_kind * dexpr
and drec_defn = { fds : dfun_defn list }
and dfun_defn = preid * ghost * rs_kind *
dbinder list * dspec later * variant list later * dexpr
dbinder list * mask * dspec later * variant list later * dexpr
(** Environment *)
......@@ -558,26 +558,26 @@ let dexpr_expected_type_weak {de_dvty = dvty; de_loc = loc} dity =
(** Generation of letrec blocks *)
type pre_fun_defn = preid * ghost * rs_kind * dbinder list *
dity * (denv -> dspec later * variant list later * dexpr)
dity * mask * (denv -> dspec later * variant list later * dexpr)
exception DupId of preid
let drec_defn denv0 prel =
if prel = [] then invalid_arg "Dexpr.drec_defn: empty function list";
let add s (id,_,_,_,_,_) = Sstr.add_new (DupId id) id.pre_name s in
let add s (id,_,_,_,_,_,_) = Sstr.add_new (DupId id) id.pre_name s in
let _ = try List.fold_left add Sstr.empty prel with DupId id ->
Loc.errorm ?loc:id.pre_loc "duplicate function name %s" id.pre_name in
let add denv (id,_,_,bl,res,_) =
let add denv (id,_,_,bl,res,_,_) =
if bl = [] then invalid_arg "Dexpr.drec_defn: empty argument list";
let argl = List.map (fun (_,_,t) -> t) bl in
denv_add_rec denv denv0.frozen id (argl,res) in
let denv1 = List.fold_left add denv0 prel in
let parse (id,gh,pk,bl,res,pre) =
let parse (id,gh,pk,bl,res,msk,pre) =
let dsp, dvl, de = pre (denv_add_args denv1 bl) in
dexpr_expected_type de res;
(id,gh,pk,bl,dsp,dvl,de) in
(id,gh,pk,bl,msk,dsp,dvl,de) in
let fdl = List.map parse prel in
let add denv (id,_,_,bl,_,_,{de_dvty = dvty}) =
let add denv (id,_,_,bl,_,_,_,{de_dvty = dvty}) =
(* just in case we linked some polymorphic type var to the outer context *)
let check tv = if is_frozen denv0.frozen tv then Loc.errorm ?loc:id.pre_loc
"This function is expected to be polymorphic in type variable %a"
......@@ -598,9 +598,9 @@ let dpattern ?loc node =
let dpat = function
| DPwild ->
mk_dpat PPwild (dity_fresh ()) Mstr.empty
| DPvar id ->
| DPvar (id,gh) ->
let dity = dity_fresh () in
mk_dpat (PPvar id) dity (Mstr.singleton id.pre_name dity)
mk_dpat (PPvar (id,gh)) dity (Mstr.singleton id.pre_name dity)
| DPapp ({rs_logic = RLls ls} as rs, dpl) when ls.ls_constr > 0 ->
let argl, res = specialize_rs rs in
dity_unify_app ls dpat_expected_type dpl argl;
......@@ -619,10 +619,10 @@ let dpattern ?loc node =
n print_dity dity1 print_dity dity2 in
let vars = Mstr.union join dp1.dp_vars dp2.dp_vars in
mk_dpat (PPor (dp1.dp_pat, dp2.dp_pat)) dp1.dp_dity vars
| DPas (dp, ({pre_name = n} as id)) ->
| DPas (dp, ({pre_name = n} as id), gh) ->
let { dp_pat = pat; dp_dity = dity; dp_vars = vars } = dp in
let vars = Mstr.add_new (Dterm.DuplicateVar n) n dity vars in
mk_dpat (PPas (pat, id)) dity vars
mk_dpat (PPas (pat, id, gh)) dity vars
| DPcast (dp, ity) ->
dpat_expected_type dp (dity_of_ity ity);
dp
......@@ -662,9 +662,9 @@ let dexpr ?loc node =
end;
dexpr_expected_type de2 a;
[], r
| DEfun (bl,_,de) ->
| DEfun (bl,_,_,de) ->
List.map (fun (_,_,t) -> t) bl, dity_of_dvty de.de_dvty
| DEany (bl,_,res) ->
| DEany (bl,_,_,res) ->
List.map (fun (_,_,t) -> t) bl, res
| DElet (_,de)
| DErec (_,de) ->
......@@ -978,7 +978,7 @@ let add_binders env pvl = List.fold_left add_pvsymbol env pvl
(** Abstract values *)
let cty_of_spec env bl dsp dity =
let cty_of_spec env bl mask dsp dity =
let ity = ity_of_dity dity in
let bl = binders bl in
let env = add_binders env bl in
......@@ -991,7 +991,7 @@ let cty_of_spec env bl dsp dity =
let p = rebase_pre env preold old dsp.ds_pre in
let q = create_post ity dsp.ds_post in
let xq = create_xpost dsp.ds_xpost in
create_cty bl p q xq (get_oldies old) eff ity
create_cty ~mask bl p q xq (get_oldies old) eff ity
(** Expressions *)
......@@ -1015,6 +1015,8 @@ let rec strip uloc labs de = match de.de_node with
let get_pv env n = Mstr.find_exn (Dterm.UnboundVar n) n env.pvm
let get_rs env n = Mstr.find_exn (Dterm.UnboundVar n) n env.rsm
let proxy_labels = Slab.singleton proxy_label
let rec expr uloc env ({de_loc = loc} as de) =
let uloc, labs, de = strip uloc Slab.empty de in
let e = Loc.try3 ?loc try_expr uloc env de in
......@@ -1022,48 +1024,59 @@ let rec expr uloc env ({de_loc = loc} as de) =
if loc = None && Slab.is_empty labs
then e else e_label ?loc labs e
and cexp uloc env ghost ({de_loc = loc} as de) =
and cexp uloc env ghost ({de_loc = loc} as de) vl =
let uloc, labs, de = strip uloc Slab.empty de in
if not (Slab.is_empty labs) then Warning.emit ?loc
"Ignoring labels over a higher-order expression";
Loc.try4 ?loc try_cexp uloc env ghost de
and try_cexp uloc env ghost de0 = match de0.de_node with
| DEvar _ | DErs _ | DEls _ | DEapp _ ->
let argl, res = de0.de_dvty in
let argl = List.map ity_of_dity argl in
let res = ity_of_dity res in
let app (ldl,c) el =
ext_c_app (ldl, c_ghostify ghost c) el argl res in
let rec down de el = match de.de_node with
| DEapp (de1,de2) -> down de1 (expr uloc env de2 :: el)
| DEvar (n,_) -> app (ext_c_sym (get_rs env n)) el
| DErs s -> app (ext_c_sym s) el
| DEls _ when not (ity_pure res) ->
Loc.errorm "This expression must have pure type"
| DEls s -> ext_c_pur s el argl res
| _ -> app (cexp uloc env ghost de) el in
down de0 []
| DEfun (bl,dsp,de) ->
Loc.try5 ?loc try_cexp uloc env ghost de vl
and try_cexp uloc env ghost ({de_dvty = argl,res} as de0) vl =
let rec drop vl al = match vl, al with
| _::vl, _::al -> drop vl al | _ -> al in
let apply app s =
let argl = List.map ity_of_dity (drop vl argl) in
let c = app s vl argl (ity_of_dity res) in
ghost || c_ghost c, [], c in
let add_ld ld (gh,l,c) = gh, ld :: l, c in
let add_ldl ldl (gh,l,c) = gh, ldl @ l, c in
let proxy c =
if vl = [] then ghost || c_ghost c,[],c else
let loc = Opt.get_def de0.de_loc uloc in
let id = id_fresh ?loc ~label:proxy_labels "h" in
let ld, s = let_sym id ~ghost c in
add_ld ld (apply c_app s) in
match de0.de_node with
| DEvar (n,_) -> apply c_app (get_rs env n)
| DErs s -> apply c_app s
| DEls s -> apply c_pur s
| DEapp (de1,de2) ->
let e2 = expr uloc env de2 in
begin match e2.e_node with
| Evar v when Slab.is_empty e2.e_label ->
cexp uloc env ghost de1 (v::vl)
| _ ->
let id = id_fresh ?loc:e2.e_loc ~label:proxy_labels "o" in
let ld, v = let_var id (e_ghostify ghost e2) in
add_ld ld (cexp uloc env ghost de1 (v::vl))
end
| DEghost de ->
cexp uloc env true de vl
| DEfun (bl,msk,dsp,de) ->
let dvl _ _ = [] in
let c, dsp, _ = lambda uloc env (binders bl) dsp dvl de in
let c, dsp, _ = lambda uloc env (binders bl) msk dsp dvl de in
check_fun None dsp c;
[], c_ghostify ghost c
| DEany (bl,dsp,dity) ->
[], c_ghostify ghost (c_any (cty_of_spec env bl dsp dity))
proxy c
| DEany (bl,msk,dsp,dity) ->
proxy (c_any (cty_of_spec env bl msk dsp dity))
| DElet ((_,_,_,{de_dvty = ([],_)}) as dldf,de) ->
let ld, env = var_defn uloc env ghost dldf in
let ldl, c = cexp uloc env ghost de in
ld::ldl, c
add_ld ld (cexp uloc env ghost de vl)
| DElet (dldf,de) ->
let ldl0, env = sym_defn uloc env ghost dldf in
let ldl, c = cexp uloc env ghost de in
ldl0 @ ldl, c
add_ldl ldl0 (cexp uloc env ghost de vl)
| DErec (drdf,de) ->
let ld, env = rec_defn uloc env ghost drdf in
let ldl, c = cexp uloc env ghost de in
ld::ldl, c
| DEghost de -> cexp uloc env true de
add_ld ld (cexp uloc env ghost de vl)
| DEmark _ ->
Loc.errorm "Marks are not allowed over higher-order expressions"
| DEpv _ | DEconst _ | DEnot _ | DEand _ | DEor _ | DEif _ | DEcase _
......@@ -1084,31 +1097,12 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
let e2 = expr uloc env de2 in
e_app rs_func_app [e1; e2] [] (ity_of_dity res)
| DEvar _ | DErs _ | DEls _ | DEapp _ | DEfun _ | DEany _ ->
let ldl,c = try_cexp uloc env false de0 in
List.fold_right e_let_check ldl (e_exec c)
| DElet ((id,_,_,{de_dvty = ([],_)}) as dldf,de) ->
let cgh,ldl,c = try_cexp uloc env false de0 [] in
let e = e_ghostify cgh (e_exec c) in
List.fold_right e_let_check ldl e
| DElet ((_,_,_,{de_dvty = ([],_)}) as dldf,de) ->
let ld, env = var_defn uloc env false dldf in
let e2 = expr uloc env de in
let e2 =
let v, e1 = match ld with
| LDvar (v,e1) -> v, e1
| _ -> assert false in
let e2_unit = ity_equal e2.e_ity ity_unit in
let id_in_e2 = Spv.mem v e2.e_effect.eff_reads in
if not id_in_e2 then warn_unused id.pre_name id.pre_loc;
(* if e1 is a recursive call, we may not know yet its effects,
so we have to rely on an heuristic: if the result of e1 is
not used in e2, then it was probably called for the effect. *)
let e1_no_eff = eff_pure e1.e_effect && id_in_e2 in
if e2_unit (* e2 is unit *)
&& e_ghost e2 (* and e2 is ghost *)
&& not (e_ghost e1) (* and e1 is non-ghost *)
&& not e1_no_eff (* and e1 has observable effects *)
then
let ld,_ = let_var (id_fresh "_") e2 in
e_label ?loc:e2.e_loc Slab.empty (e_let ld e_void)
else e2
in
e_let ld e2
| DElet (dldf,de) ->
let ldl, env = sym_defn uloc env false dldf in
......@@ -1126,9 +1120,8 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
e_if (expr uloc env de1) (expr uloc env de2) (expr uloc env de3)
| DEcase (de1,bl) ->
let e1 = expr uloc env de1 in
let ghost = e_ghost e1 in
let mk_branch (dp,de) =
let vm, pat = create_prog_pattern dp.dp_pat ~ghost e1.e_ity in
let vm, pat = create_prog_pattern dp.dp_pat e1.e_ity e1.e_mask in
let e = expr uloc (add_pv_map env vm) de in
Mstr.iter (fun _ v -> check_used_pv e v) vm;
pat, e in
......@@ -1138,7 +1131,7 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
let bl = if Pattern.is_exhaustive [t_var v] pl then bl else begin
if List.length bl > 1 then Warning.emit ?loc:de0.de_loc
"Non-exhaustive pattern matching, asserting `absurd'";
let _,pp = create_prog_pattern PPwild ~ghost e1.e_ity in
let _,pp = create_prog_pattern PPwild e1.e_ity e1.e_mask in
(pp, e_absurd (ity_of_dity res)) :: bl end in
e_case e1 (List.rev bl)
| DEassign al ->
......@@ -1161,7 +1154,7 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
| DEtry (de1,bl) ->
let e1 = expr uloc env de1 in
let add_branch (m,l) (xs,dp,de) =
let vm, pat = create_prog_pattern dp.dp_pat xs.xs_ity in
let vm, pat = create_prog_pattern dp.dp_pat xs.xs_ity MaskVisible in
let e = expr uloc (add_pv_map env vm) de in
Mstr.iter (fun _ v -> check_used_pv e v) vm;
try Mexn.add xs ((pat,e) :: Mexn.find xs m) m, l
......@@ -1179,7 +1172,7 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
let v = create_pvsymbol (id_fresh "res") xs.xs_ity in
let pl = List.rev_map (fun (p,_) -> [p.pp_pat]) bl in
let bl = if Pattern.is_exhaustive [t_var v.pv_vs] pl then bl
else let _,pp = create_prog_pattern PPwild v.pv_ity in
else let _,pp = create_prog_pattern PPwild v.pv_ity MaskVisible in
(pp, e_raise xs (e_var v) (ity_of_dity res)) :: bl in
xs, v, e_case (e_var v) (List.rev bl)
in
......@@ -1210,34 +1203,35 @@ and var_defn uloc env ghost (id,gh,kind,de) =
| RKlemma -> Loc.errorm ?loc:id.pre_loc
"Lemma-functions must have parameters"
| RKfunc | RKpred | RKlocal | RKnone ->
expr uloc env de in
let ld, v = let_var id ~ghost:(gh || ghost) e in
e_ghostify ghost (expr uloc env de) in
let ld, v = let_var id ~ghost:gh e in
ld, add_pvsymbol env v
and sym_defn uloc env ghost (id,gh,kind,de) =
let ldl, c = cexp uloc env (gh || ghost) de in
if c_ghost c && not (gh || ghost) then Loc.errorm ?loc:id.pre_loc
"Function %s must be explicitly marked ghost" id.pre_name;
let ghost, ldl, c = cexp uloc env ghost de [] in
let ld, s = let_sym id ~ghost:(gh || ghost) ~kind c in
ldl @ [ld], add_rsymbol env s
and rec_defn uloc env ghost {fds = dfdl} =
let step1 env (id, gh, kind, bl, dsp, dvl, ({de_dvty = dvty} as de)) =
let step1 env (id, gh, kind, bl, mask, dsp, dvl, ({de_dvty = dvty} as de)) =
let pvl = binders bl in
let ity = Loc.try1 ?loc:de.de_loc ity_of_dity (dity_of_dvty dvty) in
let cty = create_cty pvl [] [] Mexn.empty Mpv.empty eff_empty ity in
let cty = create_cty ~mask pvl [] [] Mexn.empty Mpv.empty eff_empty ity in
let rs = create_rsymbol id ~ghost:(gh || ghost) ~kind:RKnone cty in
add_rsymbol env rs, (rs, kind, dsp, dvl, de) in
add_rsymbol env rs, (rs, kind, mask, dsp, dvl, de) in
let env, fdl = Lists.map_fold_left step1 env dfdl in
let step2 ({rs_cty = c} as rs, kind, dsp, dvl, de) (fdl, dspl) =
let lam, dsp, dvl = lambda uloc env c.cty_args dsp dvl de in
if c_ghost lam && not (rs_ghost rs) then Loc.errorm ?loc:rs.rs_name.id_loc
"Function %s must be explicitly marked ghost" rs.rs_name.id_string;
let step2 (rs, kind, mask, dsp, dvl, de) (fdl,dspl) =
let {rs_name = {id_string = nm; id_loc = loc}; rs_cty = c} = rs in
let lam, dsp, dvl = lambda uloc env c.cty_args mask dsp dvl de in
if c_ghost lam && not (rs_ghost rs) then Loc.errorm ?loc
"Function %s must be explicitly marked ghost" nm;
if mask_spill lam.c_cty.cty_mask c.cty_mask then Loc.errorm ?loc
"Function %s returns more ghost results than expected" nm;
(rs, lam, dvl, kind)::fdl, dsp::dspl in
(* check for unexpected aliases in case of trouble *)
let fdl, dspl = try List.fold_right step2 fdl ([],[]) with
| Loc.Located (_, Ity.TypeMismatch _) | Ity.TypeMismatch _ as exn ->
List.iter (fun ({rs_name = {id_loc = loc}} as rs,_,_,_,_) ->
List.iter (fun ({rs_name = {id_loc = loc}} as rs,_,_,_,_,_) ->
Loc.try2 ?loc check_aliases true rs.rs_cty) fdl;
raise exn in
let ld, rdl = try let_rec fdl with
......@@ -1250,7 +1244,7 @@ and rec_defn uloc env ghost {fds = dfdl} =
add_rsymbol env s in
ld, List.fold_left2 add_fd env rdl dspl
and lambda uloc env pvl dsp dvl de =
and lambda uloc env pvl mask dsp dvl de =
let env = add_binders env pvl in
let preold = Mstr.find_opt "0" env.old in
let env, old = add_label env "0" in
......@@ -1261,26 +1255,37 @@ and lambda uloc env pvl dsp dvl de =
let p = rebase_pre env preold old dsp.ds_pre in
let q = create_post e.e_ity dsp.ds_post in
let xq = create_xpost dsp.ds_xpost in
c_fun pvl p q xq (get_oldies old) e, dsp, dvl
c_fun ~mask pvl p q xq (get_oldies old) e, dsp, dvl
let rec_defn ?(keep_loc=true) drdf =
let uloc = if keep_loc then None else Some None in
fst (rec_defn uloc env_empty false drdf)
let let_defn ?(keep_loc=true) (id,ghost,kind,de) =
let rec mask_of_fun de = match de.de_node with
| DEfun (_,msk,_,_) -> msk
| DEghost de | DEcast (de,_)
| DEuloc (de,_) | DElabel (de,_) -> mask_of_fun de
| _ -> MaskGhost (* a safe default for checking *)
let let_defn ?(keep_loc=true) (id, ghost, kind, de) =
let uloc = if keep_loc then None else Some None in
let {pre_name = nm; pre_loc = loc} = id in
match kind, de.de_dvty with
| _, (_::_, _) ->
let ldl, c = cexp uloc env_empty ghost de in
let cgh, ldl, c = cexp uloc env_empty false de [] in
if ldl <> [] then Loc.errorm ?loc:de.de_loc
"Illegal top-level function definition";
if c_ghost c && not ghost then Loc.errorm ?loc:id.pre_loc
"Function %s must be explicitly marked ghost" id.pre_name;
if cgh && not ghost then Loc.errorm ?loc
"Function %s must be explicitly marked ghost" nm;
let spl = mask_spill c.c_cty.cty_mask (mask_of_fun de) in
if spl && not ghost then Loc.errorm ?loc
"Function %s returns more ghost results than expected" nm;
fst (let_sym id ~ghost ~kind c)
| (RKfunc | RKpred), ([], _) ->
(* FIXME: let ghost constant c = <effectful> *)
let e = expr uloc env_empty de in
if e_ghost e && not ghost then Loc.errorm ?loc:id.pre_loc
"Function %s must be explicitly marked ghost" id.pre_name;
if mask_ghost e.e_mask && not ghost then Loc.errorm ?loc
"Function %s must be explicitly marked ghost" nm;
let c = c_fun [] [] [] Mexn.empty Mpv.empty e in
(* the rsymbol will carry a single postcondition "the result
is equal to the logical constant". Any user-written spec
......@@ -1294,10 +1299,10 @@ let let_defn ?(keep_loc=true) (id,ghost,kind,de) =
fst (let_sym id ~ghost ~kind c)
| RKnone, ([], _) ->
let e = expr uloc env_empty de in
if e_ghost e && not ghost then Loc.errorm ?loc:id.pre_loc
"Variable %s must be explicitly marked ghost" id.pre_name;
if mask_ghost e.e_mask && not ghost then Loc.errorm ?loc
"Variable %s must be explicitly marked ghost" nm;
fst (let_var id ~ghost e)
| RKlemma, ([], _) -> Loc.errorm ?loc:id.pre_loc
| RKlemma, ([], _) -> Loc.errorm ?loc
"Lemma-functions must have parameters"
| RKlocal, _ -> invalid_arg "Dexpr.let_defn"
......
......@@ -36,10 +36,10 @@ type dpattern = private {
type dpattern_node =
| DPwild
| DPvar of preid
| DPvar of preid * bool
| DPapp of rsymbol * dpattern list
| DPas of dpattern * preid * bool
| DPor of dpattern * dpattern
| DPas of dpattern * preid
| DPcast of dpattern * ity
(** Binders *)
......@@ -94,8 +94,8 @@ and dexpr_node =
| DEls of lsymbol
| DEconst of Number.constant
| DEapp of dexpr * dexpr
| DEfun of dbinder list * dspec later * dexpr
| DEany of dbinder list * dspec later * dity
| DEfun of dbinder list * mask * dspec later * dexpr
| DEany of dbinder list * mask * dspec later * dity
| DElet of dlet_defn * dexpr
| DErec of drec_defn * dexpr
| DEnot of dexpr
......@@ -124,7 +124,7 @@ and dlet_defn = preid * ghost * rs_kind * dexpr
and drec_defn = private { fds : dfun_defn list }
and dfun_defn = preid * ghost * rs_kind *
dbinder list * dspec later * variant list later * dexpr
dbinder list * mask * dspec later * variant list later * dexpr
(** Environment *)
......@@ -151,7 +151,7 @@ val dpattern : ?loc:Loc.position -> dpattern_node -> dpattern
val dexpr : ?loc:Loc.position -> dexpr_node -> dexpr
type pre_fun_defn = preid * ghost * rs_kind * dbinder list *
dity * (denv -> dspec later * variant list later * dexpr)
dity * mask * (denv -> dspec later * variant list later * dexpr)
val drec_defn : denv -> pre_fun_defn list -> denv * drec_defn
......
This diff is collapsed.
......@@ -70,20 +70,21 @@ val rs_ghost : rsymbol -> bool
type prog_pattern = private {
pp_pat : pattern;
pp_ity : ity;
pp_mask : mask;
pp_ghost : bool;
}
type pre_pattern =
| PPwild
| PPvar of preid
| PPvar of preid * bool
| PPapp of rsymbol * pre_pattern list
| PPas of pre_pattern * preid * bool
| PPor of pre_pattern * pre_pattern
| PPas of pre_pattern * preid
exception ConstructorExpected of rsymbol
val create_prog_pattern :
pre_pattern -> ?ghost:bool -> ity -> pvsymbol Mstr.t * prog_pattern
pre_pattern -> ity -> mask -> pvsymbol Mstr.t * prog_pattern
(** {2 Program expressions} *)
......@@ -102,6 +103,7 @@ type assign = pvsymbol * rsymbol * pvsymbol (* region * field * value *)
type expr = private {
e_node : expr_node;
e_ity : ity;
e_mask : mask;
e_effect : effect;
e_label : Slab.t;
e_loc : Loc.position option;
......@@ -120,6 +122,7 @@ and expr_node = private
| Etry of expr * (xsymbol * pvsymbol * expr) list
| Eraise of xsymbol * expr
| Eassert of assertion_kind * term
| Eghost of expr
| Epure of term
| Eabsurd
......@@ -152,12 +155,6 @@ val e_label : ?loc:Loc.position -> Slab.t -> expr -> expr
val e_label_add : label -> expr -> expr
val e_label_copy : expr -> expr -> expr
val e_ghost : expr -> bool
val c_ghost : cexp -> bool
val e_ghostify : bool -> expr -> expr
val c_ghostify : bool -> cexp -> cexp
(** {2 Definitions} *)
val let_var :
......@@ -176,22 +173,13 @@ val ls_decr_of_rec_defn : rec_defn -> lsymbol option
(** {2 Callable expressions} *)
val c_app : rsymbol -> pvsymbol list -> ity list -> ity -> cexp
val c_pur : lsymbol -> pvsymbol list -> ity list -> ity -> cexp
val c_fun : pvsymbol list ->
val c_fun : ?mask:mask -> pvsymbol list ->
pre list -> post list -> post list Mexn.t -> pvsymbol Mpv.t -> expr -> cexp
val c_any : cty -> cexp
type ext_cexp = let_defn list * cexp
val ext_c_sym : rsymbol -> ext_cexp
val ext_c_app : ext_cexp -> expr list -> ity list -> ity -> ext_cexp
val ext_c_pur : lsymbol -> expr list -> ity list -> ity -> ext_cexp
(** {2 Expression constructors} *)
val e_var : pvsymbol -> expr
......@@ -202,6 +190,7 @@ val e_nat_const : int -> expr
val e_exec : cexp -> expr
val e_app : rsymbol -> expr list -> ity list -> ity -> expr
val e_pur : lsymbol -> expr list -> ity list -> ity -> expr
val e_let : let_defn -> expr -> expr
......@@ -232,10 +221,12 @@ val e_while : expr -> invariant list -> variant list -> expr -> expr
val e_for : pvsymbol ->
expr -> for_direction -> expr -> invariant list -> expr -> expr
val e_pure : term -> expr
val e_assert : assertion_kind -> term -> expr
val e_ghostify : bool -> expr -> expr
val e_pure : term -> expr
val e_absurd : ity -> expr
(** {2 Expression manipulation tools} *)
......@@ -255,6 +246,9 @@ val c_rs_subst : rsymbol Mrs.t -> cexp -> cexp
val term_of_expr : prop:bool -> expr -> term option
val post_of_expr : term -> expr -> term option
val e_ghost : expr -> bool
val c_ghost : cexp -> bool
(** {2 Built-in symbols} *)
val rs_true : rsymbol
......@@ -278,9 +272,6 @@ val e_func_app_l : expr -> expr list -> expr
(** {2 Pretty-printing} *)
val forget_rs : rsymbol -> unit (* flush id_unique for a program symbol *)
val print_rs : Format.formatter -> rsymbol -> unit (* program symbol *)
val print_expr : Format.formatter -> expr -> unit (* expression *)
val print_let_defn : Format.formatter -> let_defn -> unit
......@@ -734,21 +734,65 @@ let ity_unit = ity_tuple []
(* exception symbols *)
type mask =
| MaskVisible
| MaskTuple of mask list
| MaskGhost
let mask_of_pv v = if v.pv_ghost then MaskGhost else MaskVisible
let rec mask_norm mask = match mask with
| MaskVisible | MaskGhost -> mask
| MaskTuple l ->
let l = List.map mask_norm l in
if List.for_all ((=) MaskVisible) l then MaskVisible else
if List.for_all ((=) MaskGhost) l then MaskGhost else
MaskTuple l
let rec mask_check exn ity mask = match ity.ity_node, mask with
| _, (MaskVisible | MaskGhost) -> ()
| Ityapp ({its_ts = s},tl,_), MaskTuple l
when is_ts_tuple s && List.length tl = List.length l ->
List.iter2 (mask_check exn) tl l
| _ -> raise exn
let rec mask_ghost = function
| MaskVisible -> false
| MaskTuple l -> List.exists mask_ghost l
| MaskGhost -> true
let rec mask_union mask1 mask2 = match mask1, mask2 with
| MaskVisible, _ | _, MaskGhost -> mask2
| _, MaskVisible | MaskGhost, _ -> mask1
| MaskTuple l1, MaskTuple l2 -> MaskTuple (List.map2 mask_union l1 l2)
let mask_equal : mask -> mask -> bool = (=)
let rec mask_sub mask1 mask2 = match mask1, mask2 with
| MaskVisible, _ | _, MaskGhost -> true
| MaskGhost, _ -> mask_norm mask2 = MaskGhost
| _, MaskVisible -> mask_norm mask1 = MaskVisible
| MaskTuple l1, MaskTuple l2 -> Lists.equal mask_sub l1 l2
let mask_spill mask1 mask2 = not (mask_sub mask1 mask2)