Commit 3b66ba38 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: exceptions

parent 188182e0
......@@ -104,8 +104,8 @@ and dexpr_desc =
| DEnot of dexpr
| DEmatch of dexpr * (pre_ppattern * dexpr) list
| DEabsurd
| DEraise of xsymbol * dexpr option
| DEtry of dexpr * (xsymbol * string option * dexpr) list
| DEraise of xsymbol * dexpr
| DEtry of dexpr * (xsymbol * ident * dexpr) list
| DEfor of ident * dexpr * for_direction * dexpr * Ptree.lexpr option * dexpr
| DEassert of assertion_kind * Ptree.lexpr
| DEmark of string * dexpr
......
......@@ -279,6 +279,9 @@ let specialize_vtvalue ~user vtv =
let specialize_pvsymbol pv =
specialize_vtvalue ~user:true pv.pv_vtv
let specialize_xsymbol xs =
specialize_vtvalue ~user:true (vty_value xs.xs_ity)
let make_arrow_type tyl ty =
let arrow ty1 ty2 = ts_app_real ts_arrow [ty1;ty2] in
List.fold_right arrow tyl ty
......
......@@ -56,3 +56,4 @@ val specialize_lsymbol: lsymbol -> dity
val specialize_pvsymbol: pvsymbol -> dity
val specialize_psymbol: psymbol -> dity
val specialize_plsymbol: plsymbol -> dity
val specialize_xsymbol: xsymbol -> dity
......@@ -590,6 +590,8 @@ let e_lapp ls el ity =
in
e_plapp pls el ity
let e_void = e_lapp (fs_tuple 0) [] ity_unit
let e_if_real pv e1 e2 =
let vtv1 = vtv_of_expr e1 in
let vtv2 = vtv_of_expr e2 in
......@@ -738,15 +740,15 @@ let e_lazy_and e1 e2 =
let e_lazy_or e1 e2 =
if eff_is_empty e2.e_effect then e_binop Tor e1 e2 else e_if e1 e_true e2
let e_raise_real xs pv =
let e_raise_real xs ity pv =
ity_equal_check xs.xs_ity pv.pv_vtv.vtv_ity;
let ghost = pv.pv_vtv.vtv_ghost in
let vars = add_pv_vars pv Mid.empty in
let vtv = vty_value ~ghost ity_unit in
let vtv = vty_value ~ghost ity in
let eff = eff_raise eff_empty ~ghost xs in
mk_expr (Eraise (xs,pv)) (VTvalue vtv) eff vars
let e_raise xs e = on_value (e_raise_real xs) e
let e_raise xs e ity = on_value (e_raise_real xs ity) e
let e_try d bl =
let dvtv = vtv_of_expr d in
......
......@@ -223,6 +223,8 @@ val e_assign : expr -> expr -> expr
val e_ghost : expr -> expr
val e_any : any_effect -> ity -> expr
val e_void : expr
val e_const : constant -> expr
val e_int_const : string -> expr
val e_real_const : real_constant -> expr
......@@ -231,7 +233,7 @@ val e_lazy_and : expr -> expr -> expr
val e_lazy_or : expr -> expr -> expr
val e_not : expr -> expr
val e_raise : xsymbol -> expr -> expr
val e_raise : xsymbol -> expr -> ity -> expr
val e_try : expr -> (xsymbol * pvsymbol * expr) list -> expr
val e_absurd : ity -> expr
......
......@@ -238,6 +238,11 @@ and print_enode pri fmt e = match e.e_node with
| Ecase (pv,bl) ->
fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
print_pv pv (print_list newline print_branch) bl
| Eraise (xs,pv) ->
fprintf fmt "raise (%a %a)" print_xs xs print_pv pv
| Etry (e,bl) ->
fprintf fmt "try %a with@\n@[<hov>%a@]@\nend"
print_expr e (print_list newline print_xbranch) bl
| _ ->
fprintf fmt "<expr TODO>"
......@@ -245,6 +250,10 @@ and print_branch fmt ({ ppat_pattern = 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, pv, e) =
fprintf fmt "@[<hov 4>| %a %a ->@ %a@]" print_xs xs print_pv pv print_expr e;
forget_pv pv
and print_rec fst fmt { rec_ps = ps ; rec_lambda = lam } =
let print_post fmt post =
let vs,f = open_post post in
......
......@@ -236,6 +236,14 @@ let specialize_qualid ~loc uc p =
with Not_found ->
errorm ~loc "unbound symbol %a" Typing.print_qualid p
let specialize_exception ~loc uc p =
let x = Typing.string_list_of_qualid [] p in
try match ns_find_ps (get_namespace uc) x with
| PX xs -> xs, specialize_xsymbol xs
| _ -> errorm ~loc "exception symbol expected"
with Not_found ->
errorm ~loc "unbound symbol %a" Typing.print_qualid p
let mk_dexpr desc dity loc labs =
{ dexpr_desc = desc; dexpr_type = dity; dexpr_loc = loc; dexpr_lab = labs }
......@@ -430,16 +438,32 @@ and dexpr_desc ~userloc denv loc = function
expected_type e res;
ppat, e in
DEmatch (e1, List.map branch bl), res
| Ptree.Eraise (q, e1) ->
let res = create_type_variable () in
let xs, dity = specialize_exception ~loc denv.uc q in
let e1 = match e1 with
| Some e1 -> dexpr ~userloc denv e1
| None when ity_equal xs.xs_ity ity_unit -> hidden_ls ~loc (fs_tuple 0)
| _ -> errorm ~loc "exception argument expected" in
expected_type e1 dity;
DEraise (xs, e1), res
| Ptree.Etry (e1, cl) ->
let e1 = dexpr ~userloc denv e1 in
let branch (q, id, e) =
let xs, dity = specialize_exception ~loc denv.uc q in
let id, denv = match id with
| Some id -> id, add_var id dity denv
| None -> { id = "void" ; id_loc = loc ; id_lab = [] }, denv in
xs, id, dexpr ~userloc denv e
in
let cl = List.map branch cl in
DEtry (e1, cl), e1.dexpr_type
| Ptree.Eabsurd ->
DEabsurd, create_type_variable ()
| Ptree.Eassert (ass, lexpr) ->
DEassert (ass, lexpr), dity_unit
| Ptree.Eloop (_ann, _e1) ->
assert false (*TODO*)
| Ptree.Eraise (_q, _e1) ->
assert false (*TODO*)
| Ptree.Etry (_e1, _cl) ->
assert false (*TODO*)
| Ptree.Efor (_id, _e1, _dir, _e2, _lexpr_opt, _e3) ->
assert false (*TODO*)
| Ptree.Emark (_id, _e1) ->
......@@ -453,10 +477,7 @@ and dletrec ~userloc denv rdl =
(* add all functions into environment *)
let add_one denv (id, bl, var, tr) =
let res = create_type_variable () in
let tvars = add_tvars denv.tvars res in
let locals = Mstr.add id.id (tvars, res) denv.locals in
let denv = { denv with locals = locals; tvars = tvars } in
denv, (id, res, bl, var, tr) in
add_var id res denv, (id, res, bl, var, tr) in
let denv, rdl = Util.map_fold_left add_one denv rdl in
(* then type-check all of them and unify *)
let type_one (id, res, bl, var, tr) =
......@@ -468,7 +489,7 @@ and dletrec ~userloc denv rdl =
and dlambda ~userloc denv bl _var (p, e, q) =
let dbinder denv (id, pty) =
let dity = match pty with
| Some pty -> dity_of_pty ~user:false denv pty
| Some pty -> dity_of_pty ~user:true denv pty
| None -> create_type_variable () in
add_var id dity denv, (id, false, dity) in
let denv, bl = Util.map_fold_left dbinder denv bl in
......@@ -578,6 +599,16 @@ let rec expr uc locals de = match de.dexpr_desc with
e_assert ass f
| DEabsurd ->
e_absurd (ity_of_dity de.dexpr_type)
| DEraise (xs, de1) ->
e_raise xs (expr uc locals de1) (ity_of_dity de.dexpr_type)
| DEtry (de1, bl) ->
let e1 = expr uc locals de1 in
let branch (xs,id,de) =
let vtv = vty_value xs.xs_ity in
let pv = create_pvsymbol (Denv.create_user_id id) vtv in
let locals = add_local id.id (LetV pv) locals in
xs, pv, expr uc locals de in
e_try e1 (List.map branch bl)
| _ ->
assert false (*TODO*)
......
......@@ -30,13 +30,13 @@ module N
let myfun r =
let rec on_tree t = match t with
| Node {| contents = v |} f -> v + on_forest f
| Leaf -> 0
| Leaf -> raise (Exit Leaf)
end with on_forest f = match f with
| Cons t f -> let ee = Leaf in on_tree t + on_forest f + on_tree ee
| Nil -> 1
end
in
on_tree r
try on_tree r with Exit -> 0 end
end
(*
......
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