Commit e74a301d authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: type "abstract" expressions

parent d4a06c97
......@@ -88,6 +88,7 @@ and dexpr_desc =
| DEtry of dexpr * (xsymbol * ident * dexpr) list
| DEfor of ident * dexpr * Ptree.for_direction * dexpr * dinvariant * dexpr
| DEassert of Ptree.assertion_kind * Ptree.lexpr
| DEabstract of dexpr * dpost * dxpost
| DEmark of ident * dexpr
| DEghost of dexpr
| DEany of dtype_c
......
......@@ -443,6 +443,7 @@ and expr_node =
| Efor of pvsymbol * for_bounds * invariant * expr
| Eraise of xsymbol * expr
| Etry of expr * (xsymbol * pvsymbol * expr) list
| Eabstr of expr * post * xpost
| Eassert of assertion_kind * term
| Eabsurd
......@@ -897,6 +898,13 @@ let e_try e0 bl =
in
branch vtv0.vtv_ghost eff_empty Mid.empty bl
let e_abstract e q xq =
let result = match e.e_vty with
| VTvalue v -> v.vtv_ity
| VTarrow _ -> ity_unit in
let vars = spec_vars e.e_vars [] t_true q xq e.e_effect result in
mk_expr (Eabstr (e,q,xq)) e.e_vty e.e_effect vars
let e_assert ak f =
let vars = add_t_vars f Mid.empty in
let vty = VTvalue (vty_value ity_unit) in
......@@ -968,6 +976,8 @@ let rec expr_subst psm e = match e.e_node with
e_assign_real (expr_subst psm e) pv
| Eghost e ->
e_ghost (expr_subst psm e)
| Eabstr (e,q,xq) ->
e_abstract (expr_subst psm e) q xq
| Eraise (xs,e0) ->
e_raise xs (expr_subst psm e0) (vtv_of_expr e).vtv_ity
| Etry (e,bl) ->
......
......@@ -176,6 +176,7 @@ and expr_node = private
| Efor of pvsymbol * for_bounds * invariant * expr
| Eraise of xsymbol * expr
| Etry of expr * (xsymbol * pvsymbol * expr) list
| Eabstr of expr * post * xpost
| Eassert of assertion_kind * term
| Eabsurd
......@@ -263,5 +264,6 @@ val e_loop : invariant -> variant list -> expr -> expr
val e_for :
pvsymbol -> expr -> for_direction -> expr -> invariant -> expr -> expr
val e_abstract : expr -> post -> xpost -> expr
val e_assert : assertion_kind -> term -> expr
val e_absurd : ity -> expr
......@@ -308,6 +308,9 @@ and print_enode pri fmt e = match e.e_node with
fprintf fmt "absurd"
| Eassert (ak,f) ->
fprintf fmt "%a@ { %a }" print_ak ak print_term f
| Eabstr (e,q,_xq) ->
(* TODO: print_xpost *)
fprintf fmt "abstract %a@ { %a }" print_expr e print_post q
| Eghost e ->
fprintf fmt "ghost@ %a" print_expr e
| Eany tyc ->
......
......@@ -540,6 +540,10 @@ and de_desc denv loc = function
| Ptree.Eghost e1 ->
let e1 = dexpr denv e1 in
DEghost e1, e1.de_type
| Ptree.Eabstract (e1, (q,xq)) ->
let e1 = dexpr denv e1 in
let xq = dxpost denv.uc xq in
DEabstract (e1, q, xq), e1.de_type
| Ptree.Eloop ({ loop_invariant = inv; loop_variant = var }, e1) ->
let e1 = dexpr denv e1 in
let var = dvariant denv.uc var in
......@@ -554,8 +558,6 @@ and de_desc denv loc = function
expected_type eto dity_int;
expected_type e1 dity_unit;
DEfor (id,efrom,dir,eto,inv,e1), e1.de_type
| Ptree.Eabstract (_e1, _post) ->
assert false (*TODO*)
and dletrec denv rdl =
(* add all functions into environment *)
......@@ -829,6 +831,13 @@ and expr_desc lenv loc de = match de.de_desc with
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)
| DEabstract (de1, q, xq) ->
let e1 = expr lenv de1 in
let ty = match e1.e_vty with
| VTvalue v -> ty_of_ity v.vtv_ity
| VTarrow _ -> ty_unit in
let q = create_post lenv "result" ty q in
e_abstract e1 q (xpost lenv xq)
| DEassert (ak, f) ->
let ak = match ak with
| Ptree.Aassert -> Aassert
......@@ -901,9 +910,8 @@ and expr_lam lenv gh (bl, var, p, de, q, xq) =
if not gh && vty_ghost e.e_vty then
errorm ~loc:de.de_loc "ghost body in a non-ghost function";
let ty = match e.e_vty with
| VTarrow _ -> ty_unit
| VTvalue vtv -> ty_of_ity vtv.vtv_ity
in
| VTarrow _ -> ty_unit in
{ l_args = pvl;
l_variant = List.map (create_variant lenv) var;
l_pre = create_pre lenv p;
......
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