Commit b54d03f2 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: admit restricted forms of partial application

parent 0c11fc9a
......@@ -509,6 +509,16 @@ let e_app_real e pv =
let eff = eff_union e.e_effect spec.c_effect in
mk_expr (Eapp (e,pv,spec)) vty eff (add_pv_vars pv e.e_varm)
let rec e_app_flatten e pv = match e.e_node with
(* TODO/FIXME? here, we avoid capture in the first case,
but such an expression would break WP anyway. Though
it cannot come from a parsed WhyML program where the
typing ensures the uniqueness of pvsymbols, one can
construct it using the API directly. *)
| Elet ({ let_sym = LetV pv' }, _) when pv_equal pv pv' -> e_app_real e pv
| Elet (ld, e) -> e_let ld (e_app_flatten e pv)
| _ -> e_app_real e pv
let create_fun_defn id lam letrec recsyms =
let e = lam.l_expr in
let spec = {
......@@ -560,7 +570,7 @@ let on_value fn e = match e.e_node with
will be rejected, since local_get_ref is instantiated to
the region introduced (reset) by create_ref. Is it bad? *)
let e_app = List.fold_left (fun e -> on_value (e_app_real e))
let e_app = List.fold_left (fun e -> on_value (e_app_flatten e))
let e_plapp pls el ity =
if pls.pl_hidden then raise (HiddenPLS pls.pl_ls);
......
......@@ -907,15 +907,20 @@ and expr_desc lenv loc de = match de.de_desc with
e_rec def e2
| DElet (x, gh, de1, de2) ->
let e1 = e_ghostify gh (expr lenv de1) in
let mk_expr e1 =
let def1 = create_let_defn (Denv.create_user_id x) e1 in
let lenv = add_local x.id def1.let_sym lenv in
let e2 = expr lenv de2 in
e_let def1 e2 in
let rec flatten e1 = match e1.e_node with
| Elet (ld,e1) -> e_let ld (flatten e1)
| _ -> mk_expr e1 in
begin match e1.e_vty with
| VTarrow { vta_ghost = true } when not gh ->
errorm ~loc "%s must be a ghost function" x.id
| _ -> ()
| VTarrow _ -> flatten e1
| VTvalue _ -> mk_expr e1
end;
let def1 = create_let_defn (Denv.create_user_id x) e1 in
let lenv = add_local x.id def1.let_sym lenv in
let e2 = expr lenv de2 in
e_let def1 e2
| DEletrec (rdl, de1) ->
let rdl = expr_rec lenv rdl in
let add_rd { fun_ps = ps } = add_local ps.ps_name.id_string (LetA ps) in
......
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