Commit 6aace661 authored by Andrei Paskevich's avatar Andrei Paskevich

WhyML: match ... with exception ... end

parent 7617dc8e
......@@ -984,10 +984,9 @@ let rec itere (e:expr) : int
diverges (* termination could be proved but that's not the point *)
ensures { eval_0 e = result }
=
try
let e' = reduce e in
itere e'
with Stuck ->
match reduce e with
| e' -> itere e'
| exception Stuck ->
match e with
| Cte n -> n
| _ -> absurd
......@@ -1010,10 +1009,9 @@ let refocus c e
let rec itere_opt (c:context) (e:expr) : int
diverges
ensures { result = eval_0 (recompose c e) }
= try
let (c,r) = refocus c e in
itere_opt c (contract r)
with Stuck ->
= match refocus c e with
| c, r -> itere_opt c (contract r)
| exception Stuck ->
assert { is_empty_context c };
match e with
| Cte n -> n
......
......@@ -92,7 +92,7 @@ module Palindrome
let palindrome (x: list elt) : bool
ensures { result=True <-> pal x (length x) }
= try let _ = palindrome_rec x x in True
with Exit -> False end
= match palindrome_rec x x with _ -> True
| exception Exit -> False end
end
......@@ -224,7 +224,7 @@ let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) =
let var = List.map (fun (t, o) -> deref env t, o) var in
let loop = mk_expr ~loc
(Ewhile (expr env e, inv, var, block env ~loc s)) in
if has_breakl s then mk_expr ~loc (Etry (loop, break_handler ~loc))
if has_breakl s then mk_expr ~loc (Etry (loop, false, break_handler ~loc))
else loop
| Py_ast.Sbreak ->
mk_expr ~loc (Eraise (break ~loc, None))
......@@ -296,7 +296,7 @@ and block env ~loc = function
let body = block env' ~loc:id.id_loc bl in
let body = if not (has_returnl bl) then body else
let loc = id.id_loc in
mk_expr ~loc (Etry (body, return_handler ~loc)) in
mk_expr ~loc (Etry (body, false, return_handler ~loc)) in
let local bl id =
let loc = id.id_loc in
let ref = mk_ref ~loc (mk_var ~loc id) in
......
......@@ -564,7 +564,8 @@ module Translate = struct
| Eassign al ->
ML.mk_expr (Mltree.Eassign al) (Mltree.I e.e_ity) eff
| Epure _ -> (* assert false (\*TODO*\) *) ML.mk_hole
| Etry (etry, pvl_e_map) ->
| Etry (etry, case, pvl_e_map) ->
assert (not case); (* TODO *)
let etry = expr info etry in
let bl =
let bl_map = Mxs.bindings pvl_e_map in
......
......@@ -424,7 +424,7 @@ and dexpr_node =
| DEassign of (dexpr * rsymbol * dexpr) list
| DEwhile of dexpr * dinvariant later * variant list later * dexpr
| DEfor of preid * dexpr * for_direction * dexpr * dinvariant later * dexpr
| DEtry of dexpr * (dxsymbol * dpattern * dexpr) list
| DEtry of dexpr * bool * (dxsymbol * dpattern * dexpr) list
| DEraise of dxsymbol * dexpr
| DEghost of dexpr
| DEexn of preid * dity * mask * dexpr
......@@ -789,9 +789,9 @@ let dexpr ?loc node =
dexpr_expected_type de_to bty;
dexpr_expected_type de dity_unit;
dvty_unit
| DEtry (_,[]) ->
| DEtry (_,_,[]) ->
invalid_arg "Dexpr.dexpr: empty branch list in DEtry"
| DEtry (de,bl) ->
| DEtry (de,_,bl) ->
let res = dity_fresh () in
dexpr_expected_type de res;
List.iter (fun (xs,dp,de) ->
......@@ -1398,7 +1398,7 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
let e = expr uloc env de in
let inv = get_later env dinv in
e_for v e_from dir e_to i (create_invariant inv) e
| DEtry (de1,bl) ->
| DEtry (de1,case,bl) ->
let e1 = expr uloc env de1 in
let add_branch m (xs,dp,de) =
let xs = get_xs env xs in
......@@ -1442,7 +1442,7 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
let _,pp = create_prog_pattern PPwild xs.xs_ity mask in
(pp, e_raise xs e (ity_of_dity res)) :: bl in
vl, e_case e (List.rev bl) in
e_try e1 (Mxs.mapi mk_branch xsm)
e_try e1 ~case (Mxs.mapi mk_branch xsm)
| DEraise (xs,de) ->
let {xs_mask = mask} as xs = get_xs env xs in
let env = {env with ugh = mask = MaskGhost} in
......@@ -1533,7 +1533,7 @@ and lambda uloc env pvl mask dsp dvl de =
if not (Sxs.mem xs e.e_effect.eff_raises) then e else
let vl = vl_of_mask (id_fresh "r") mask xs.xs_ity in
let branches = Mxs.singleton xs (vl, e_of_vl vl) in
e_exn xs (e_try e branches) in
e_exn xs (e_try e ~case:false branches) in
let dsp = get_later env dsp e.e_ity in
let dvl = get_later env dvl in
let dvl = rebase_variant env preold old dvl in
......
......@@ -117,7 +117,7 @@ and dexpr_node =
| DEassign of (dexpr * rsymbol * dexpr) list
| DEwhile of dexpr * dinvariant later * variant list later * dexpr
| DEfor of preid * dexpr * for_direction * dexpr * dinvariant later * dexpr
| DEtry of dexpr * (dxsymbol * dpattern * dexpr) list
| DEtry of dexpr * bool * (dxsymbol * dpattern * dexpr) list
| DEraise of dxsymbol * dexpr
| DEghost of dexpr
| DEexn of preid * dity * mask * dexpr
......
......@@ -324,7 +324,7 @@ and expr_node =
| Ecase of expr * (prog_pattern * expr) list
| Ewhile of expr * invariant list * variant list * expr
| Efor of pvsymbol * for_bounds * pvsymbol * invariant list * expr
| Etry of expr * (pvsymbol list * expr) Mxs.t
| Etry of expr * bool * (pvsymbol list * expr) Mxs.t
| Eraise of xsymbol * expr
| Eexn of xsymbol * expr
| Eassert of assertion_kind * term
......@@ -390,7 +390,7 @@ let e_fold fn acc e = match e.e_node with
| Elet (LDvar (_,d), e) | Ewhile (d,_,_,e) -> fn (fn acc d) e
| Eif (c,d,e) -> fn (fn (fn acc c) d) e
| Ecase (d,bl) -> List.fold_left (fun acc (_,e) -> fn acc e) (fn acc d) bl
| Etry (d,xl) -> Mxs.fold (fun _ (_,e) acc -> fn acc e) xl (fn acc d)
| Etry (d,_,xl) -> Mxs.fold (fun _ (_,e) acc -> fn acc e) xl (fn acc d)
exception FoundExpr of Loc.position option * expr
......@@ -942,7 +942,7 @@ let e_case e bl =
let eff = try_effect (e::dl) eff_ghostify ghost eff in
mk_expr (Ecase (e,bl)) ity mask eff
let e_try e xl =
let e_try e ~case xl =
let get_mask = function
| [] -> ity_unit, MaskVisible
| [v] -> v.pv_ity, mask_of_pv v
......@@ -955,18 +955,25 @@ let e_try e xl =
ity_equal_check ity xs.xs_ity;
ity_equal_check d.e_ity e.e_ity) xl;
let ghost = e.e_effect.eff_ghost in
let e0, bl = if not case then e, [] else
match e.e_node with Ecase (e,bl) -> e,bl
| _ -> invalid_arg "Expr.e_try" in
let eeff = Mxs.fold (fun xs _ eff ->
eff_catch eff xs) xl e.e_effect in
eff_catch eff xs) xl e0.e_effect in
let dl = Mxs.fold (fun _ (_,d) l -> d::l) xl [] in
let add_mask mask d = mask_union mask d.e_mask in
let mask = List.fold_left add_mask e.e_mask dl in
let bldl = List.map snd bl @ dl in
let xeff = List.fold_left (fun eff (p,d) ->
let pvs = pvs_of_vss Spv.empty p.pp_pat.pat_vars in
eff_union_par eff (eff_bind pvs d.e_effect)) eff_empty bl in
let xeff = Mxs.fold (fun _ (vl,d) eff ->
let add s v = Spv.add_new (Invalid_argument "Expr.e_try") v s in
let deff = eff_bind (List.fold_left add Spv.empty vl) d.e_effect in
try_effect dl eff_union_par eff deff) xl eff_empty in
let eff = try_effect (e::dl) eff_union_seq eeff xeff in
let eff = try_effect (e::dl) eff_ghostify ghost eff in
mk_expr (Etry (e,xl)) e.e_ity mask eff
try_effect bldl eff_union_par eff deff) xl xeff in
let eff = try_effect (e0::bldl) eff_union_seq eeff xeff in
let eff = try_effect (e0::bldl) eff_ghostify ghost eff in
mk_expr (Etry (e,case,xl)) e.e_ity mask eff
let e_raise xs e ity =
ity_equal_check e.e_ity xs.xs_ity;
......@@ -1034,7 +1041,7 @@ let rec e_rs_subst sm e = e_label_copy e (match e.e_node with
| Eraise (xs,d) -> e_raise xs (e_rs_subst sm d) e.e_ity
| Ecase (d,bl) -> e_case (e_rs_subst sm d)
(List.map (fun (pp,e) -> pp, e_rs_subst sm e) bl)
| Etry (d,xl) -> e_try (e_rs_subst sm d)
| Etry (d,case,xl) -> e_try (e_rs_subst sm d) ~case
(Mxs.map (fun (v,e) -> v, e_rs_subst sm e) xl))
and c_rs_subst sm ({c_node = n; c_cty = c} as d) = match n with
......@@ -1388,10 +1395,15 @@ and print_enode pri fmt e = match e.e_node with
fprintf fmt "raise %a" print_xs xs
| Eraise (xs,e) ->
fprintf fmt "raise (%a %a)" print_xs xs print_expr e
| Etry (e,bl) ->
let bl = Mxs.bindings bl in
fprintf fmt "try %a with@\n@[<hov>%a@]@\nend"
print_expr e (Pp.print_list Pp.newline print_xbranch) bl
| Etry ({e_node = Ecase (e,bl)},true,xl) ->
let xl = Mxs.bindings xl in
fprintf fmt "match %a with@\n@[<hov>%a@\n%a@]@\nend"
print_expr e (Pp.print_list Pp.newline print_branch) bl
(Pp.print_list Pp.newline (print_xbranch true)) xl
| Etry (e,_,xl) ->
let xl = Mxs.bindings xl in
fprintf fmt "try %a with@\n@[<hov>%a@]@\nend" print_expr e
(Pp.print_list Pp.newline (print_xbranch false)) xl
| Eabsurd ->
fprintf fmt "absurd"
| Eassert (Assert,f) ->
......@@ -1409,12 +1421,13 @@ and print_branch fmt ({pp_pat = p},e) =
fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p print_expr e;
Svs.iter forget_var p.pat_vars
and print_xbranch fmt (xs,(vl,e)) =
and print_xbranch case fmt (xs,(vl,e)) =
let pvs = Spv.inter (Spv.of_list vl) e.e_effect.eff_reads in
let print_var fmt v =
if Spv.mem v pvs then fprintf fmt " %a" print_pv v
else pp_print_string fmt " _" in
fprintf fmt "@[<hov 4>| %a%a ->@ %a@]" print_xs xs
fprintf fmt "@[<hov 4>| %s%a%a ->@ %a@]"
(if case then "exception " else "") print_xs xs
(Pp.print_list Pp.nothing print_var) vl print_expr e;
Spv.iter forget_pv pvs
......
......@@ -132,7 +132,7 @@ and expr_node =
| Ecase of expr * (prog_pattern * expr) list
| Ewhile of expr * invariant list * variant list * expr
| Efor of pvsymbol * for_bounds * pvsymbol * invariant list * expr
| Etry of expr * (pvsymbol list * expr) Mxs.t
| Etry of expr * bool * (pvsymbol list * expr) Mxs.t
| Eraise of xsymbol * expr
| Eexn of xsymbol * expr
| Eassert of assertion_kind * term
......@@ -231,7 +231,7 @@ val e_exn : xsymbol -> expr -> expr
val e_raise : xsymbol -> expr -> ity -> expr
val e_try : expr -> (pvsymbol list * expr) Mxs.t -> expr
val e_try : expr -> case:bool -> (pvsymbol list * expr) Mxs.t -> expr
val e_case : expr -> (prog_pattern * expr) list -> expr
......
......@@ -234,7 +234,7 @@ let get_syms node pure =
let add_branch syms (p,e) =
syms_pat (syms_expr syms e) p.pp_pat in
List.fold_left add_branch (syms_eity syms d) bl
| Etry (d,xl) ->
| Etry (d,_,xl) ->
let add_branch xs (vl,e) syms =
syms_xs xs (syms_pvl (syms_expr syms e) vl) in
Mxs.fold add_branch xl (syms_expr syms d)
......
......@@ -617,10 +617,20 @@ let rec eval_expr env (e : expr) : result =
with
NotNum -> Irred e
end
| Etry(e1,el) ->
| Etry(e1,case,el) ->
begin
let r = eval_expr env e1 in
let e0,ebl =
if not case then e1,[]
else match e1.e_node with
| Ecase(e0,ebl) -> e0,ebl
| _ -> assert false
in
let r = eval_expr env e0 in
match r with
| Normal t when case ->
begin try exec_match env t ebl
with Undetermined -> Irred e1
end
| Excep(ex,t) ->
begin
match Mxs.find ex el with
......
......@@ -921,12 +921,12 @@ let rec clone_expr cl sm e = e_label_copy e (match e.e_node with
e_for v'
(e_var (sm_find_pv sm f)) dir (e_var (sm_find_pv sm t))
i' (clone_invl cl ism invl) (clone_expr cl ism e)
| Etry (d, xl) ->
| Etry (d, case, xl) ->
let conv_br xs (vl, e) m =
let vl' = List.map (clone_pv cl) vl in
let sm = List.fold_left2 sm_save_pv sm vl vl' in
Mxs.add (sm_find_xs sm xs) (vl', clone_expr cl sm e) m in
e_try (clone_expr cl sm d) (Mxs.fold conv_br xl Mxs.empty)
e_try (clone_expr cl sm d) ~case (Mxs.fold conv_br xl Mxs.empty)
| Eraise (xs, e) ->
e_raise (sm_find_xs sm xs) (clone_expr cl sm e) (clone_ity cl e.e_ity)
| Eexn ({xs_name = id; xs_mask = mask; xs_ity = ity} as xs, e) ->
......
......@@ -23,6 +23,9 @@ open Pdecl
let debug = Debug.register_info_flag "vc_debug"
~desc:"Print@ details@ of@ verification@ conditions@ generation."
let debug_reflow = Debug.register_info_flag "vc_reflow"
~desc:"Debug@ elimination@ of@ the@ dead@ code@ in@ VC."
let debug_sp = Debug.register_flag "vc_sp"
~desc:"Use@ 'Efficient@ Weakest@ Preconditions'@ for@ verification."
......@@ -474,14 +477,18 @@ let inv_of_pure {known_map = kn} loc fl k =
[res] names the result of the normal execution of [e]
[xmap] maps every raised exception to a pair [i,xres]:
- [i] is a positive int assigned at the catching site
- [xres] names the value carried by the exception *)
let rec k_expr env lps ({e_loc = loc} as e) res xmap =
- [xres] names the value carried by the exception
[case_xmap] is used for match-with-exceptions *)
let rec k_expr env lps e res ?case_xmap xmap =
let loc = e.e_loc in
let lab = Slab.diff e.e_label vc_labels in
let t_lab t = t_label ?loc lab t in
let var_or_proxy e k = match e.e_node with
let var_or_proxy_case xmap e k =
match e.e_node with
| Evar v -> k v
| _ -> let v = proxy_of_expr e in
Kseq (k_expr env lps e v xmap, 0, k v) in
Kseq (k_expr env lps e v xmap, 0, k v) in
let var_or_proxy = var_or_proxy_case xmap in
let k = match e.e_node with
| Evar v ->
Klet (res, t_lab (t_var v.pv_vs), t_true)
......@@ -580,9 +587,11 @@ let rec k_expr env lps ({e_loc = loc} as e) res xmap =
Kseq (k_expr env lps e0 v xmap, 0, k)
| Ecase (e0, [{pp_pat = {pat_node = Pvar v}}, e1]) ->
let k = k_expr env lps e1 res xmap in
let xmap = Opt.get_def xmap case_xmap in
Kseq (k_expr env lps e0 (restore_pv v) xmap, 0, k)
| Ecase (e0, [pp, e1]) when Svs.is_empty pp.pp_pat.pat_vars ->
let k = k_expr env lps e1 res xmap in
let xmap = Opt.get_def xmap case_xmap in
Kseq (k_expr env lps e0 (proxy_of_expr e0) xmap, 0, k)
| Elet ((LDsym _| LDrec _) as ld, e1) ->
let k = k_expr env lps e1 res xmap in
......@@ -671,8 +680,9 @@ let rec k_expr env lps ({e_loc = loc} as e) res xmap =
Kseq (Ktag (SP, Kcase (v, bl)), 0, Klet (res, t, f))
with Exit -> Ktag (SP, Kcase (v, bl))
else Kcase (v, bl) in
var_or_proxy e0 kk
| Etry (e0, bl) ->
let xmap = Opt.get_def xmap case_xmap in
var_or_proxy_case xmap e0 kk
| Etry (e0, case, bl) ->
(* try-with is just another semicolon *)
let branch xs (vl,e) (xl,xm) =
let i = new_exn env in
......@@ -687,8 +697,10 @@ let rec k_expr env lps ({e_loc = loc} as e) res xmap =
let pl = List.map (fun v -> pat_var v.pv_vs) vl in
v, Kcase (v, [pat_app cs pl v.pv_vs.vs_ty, xk]) in
(i,xk)::xl, Mxs.add xs (i,v) xm in
let xl, xmap = Mxs.fold branch bl ([], xmap) in
let k = k_expr env lps e0 res xmap in
let xl, cxmap = Mxs.fold branch bl ([], xmap) in
let case_xmap, xmap =
if case then Some cxmap, xmap else None, cxmap in
let k = k_expr env lps e0 res ?case_xmap xmap in
(* catched xsymbols are converted to unique integers,
so that we can now serialise the "with" clauses
and avoid capturing the wrong exceptions *)
......@@ -1362,9 +1374,11 @@ and wp_expr kn k q = match k with
(** VCgen *)
let vc_kode {known_map = kn} vc_wp k =
let k = reflow vc_wp k in
if Debug.test_flag debug then
Format.eprintf "K @[%a@]@\n" k_print k;
let k = reflow vc_wp k in
if Debug.test_flag debug_reflow then
Format.eprintf "R @[%a@]@\n" k_print k;
wp_expr kn k Mint.empty
let vc_fun env vc_wp cty e =
......
......@@ -608,7 +608,10 @@ field_list1(X):
| fl = semicolon_list1(separated_pair(lqualid, EQUAL, X)) { fl }
match_cases(X):
| cl = bar_list1(separated_pair(pattern, ARROW, X)) { cl }
| cl = bar_list1(match_case(X)) { cl }
match_case(X):
| mc = separated_pair(pattern, ARROW, X) { mc }
quant_vars:
| binder_var+ cast? { List.map (fun (l,i) -> l, i, false, $2) $1 }
......@@ -770,10 +773,17 @@ expr_:
{ Eany ([], Expr.RKnone, Some (fst $2), snd $2, $3) }
| VAL ghost kind labels(lident_rich) mk_expr(val_defn) IN seq_expr
{ Elet ($4, $2, $3, $5, $7) }
| MATCH seq_expr WITH match_cases(seq_expr) END
{ Ematch ($2, $4) }
| MATCH comma_list2(expr) WITH match_cases(seq_expr) END
{ Ematch (mk_expr (Etuple $2) $startpos($2) $endpos($2), $4) }
| MATCH seq_expr WITH ext_match_cases END
{ let bl, xl = $4 in
if xl = [] then Ematch ($2, bl) else
if bl = [] then Etry ($2, false, xl) else
Etry (mk_expr (Ematch ($2, bl)) $startpos $endpos, true, xl) }
| MATCH comma_list2(expr) WITH ext_match_cases END
{ let e = mk_expr (Etuple $2) $startpos($2) $endpos($2) in
let bl, xl = $4 in
if xl = [] then Ematch (e, bl) else
if bl = [] then Etry (e, false, xl) else
Etry (mk_expr (Ematch (e, bl)) $startpos $endpos, true, xl) }
| EXCEPTION labels(uident) IN seq_expr
{ Eexn ($2, PTtuple [], Ity.MaskVisible, $4) }
| EXCEPTION labels(uident) return IN seq_expr
......@@ -793,7 +803,7 @@ expr_:
| RETURN expr_arg?
{ Eraise (Qident (mk_id Dexpr.old_mark $startpos($1) $endpos($1)), $2) }
| TRY seq_expr WITH bar_list1(exn_handler) END
{ Etry ($2, $4) }
{ Etry ($2, false, $4) }
| GHOST expr
{ Eghost $2 }
| assertion_kind LEFTBRC term RIGHTBRC
......@@ -863,6 +873,17 @@ loop_annotation:
| variant loop_annotation
{ let inv, var = $2 in inv, variant_union $1 var }
ext_match_cases:
| ioption(BAR) ext_match_cases1 { $2 }
ext_match_cases1:
| match_case(seq_expr) ext_match_cases0 { let bl,xl = $2 in $1::bl, xl }
| EXCEPTION exn_handler ext_match_cases0 { let bl,xl = $3 in bl, $2::xl }
ext_match_cases0:
| (* epsilon *) { [], [] }
| BAR ext_match_cases1 { $2 }
exn_handler:
| uqualid pat_arg? ARROW seq_expr { $1, $2, $4 }
......
......@@ -144,7 +144,7 @@ and expr_desc =
| Eidpur of qualid
| Eraise of qualid * expr option
| Eexn of ident * pty * Ity.mask * expr
| Etry of expr * (qualid * pattern option * expr) list
| Etry of expr * bool * (qualid * pattern option * expr) list
| Efor of ident * expr * Expr.for_direction * expr * invariant * expr
(* annotations *)
| Eassert of Expr.assertion_kind * term
......
......@@ -776,7 +776,7 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
| None when mb_unit -> Dexpr.dexpr ~loc (DEsym (RS rs_void))
| _ -> Loc.errorm ~loc "exception argument expected" in
DEraise (xs, e1)
| Ptree.Etry (e1, cl) ->
| Ptree.Etry (e1, case, cl) ->
let e1 = dexpr muc denv e1 in
let branch (q, pp, e) =
let xs = find_dxsymbol q in
......@@ -790,7 +790,7 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
let denv = denv_add_pat denv pp in
let e = dexpr muc denv e in
xs, pp, e in
DEtry (e1, List.map branch cl)
DEtry (e1, case, List.map branch cl)
| Ptree.Eghost e1 ->
DEghost (dexpr muc denv e1)
| Ptree.Eexn (id, pty, mask, e1) ->
......
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