Commit 07d793f0 authored by Andrei Paskevich's avatar Andrei Paskevich

WhyML: generalize in let-in (value restriction)

Up to now, WhyML managed without generalization in let-in,
since we only generalized function definitions in Erec.
This patch adds generalization of arrow-types values,
such as effectless Eany (= abstract local functions),
anonymous functions and psymbols.
parent 7e7c332c
......@@ -414,7 +414,7 @@ and dexpr_node =
| DEabstract of dexpr * dspec later
| DEmark of preid * dexpr
| DEghost of dexpr
| DEany of dtype_c
| DEany of dtype_v * dspec later option
| DEcast of dexpr * ity
| DEuloc of dexpr * Loc.position
| DElabel of dexpr * Slab.t
......@@ -494,8 +494,15 @@ let dvty_of_dtype_v dtv =
let denv_add_var denv id dity = denv_add_mono denv id ([], dity)
let denv_add_let denv (id,_,{de_dvty = dvty}) =
denv_add_mono denv id dvty
let denv_add_let denv (id,_,({de_dvty = dvty} as de)) =
if fst dvty = [] then denv_add_mono denv id dvty else
let rec is_value de = match de.de_node with
| DEghost de | DEuloc (de,_) | DElabel (de,_) -> is_value de
| DEvar _ | DEgpsym _ | DElam _ | DEany (_,None) -> true
| _ -> false in
if is_value de
then denv_add_poly denv id dvty
else denv_add_mono denv id dvty
let denv_add_fun denv (id,_,bl,{de_dvty = (argl,res)},_) =
if bl = [] then invalid_arg "Mlw_dexpr.denv_add_fun: empty argument list";
......@@ -1074,8 +1081,7 @@ let rec type_c env pvs vars otv (dtyv, dsp) =
let add_vs vs varl = (t_var vs, None) :: varl in
let varl = Svs.fold add_vs esvs spec.c_variant in
let spec = { spec with c_variant = varl } in
(* add the invariants *)
spec_invariant env pvs vty spec, vty
spec, vty
and type_v env pvs vars otv = function
| DSpecV v ->
......@@ -1088,6 +1094,7 @@ and type_v env pvs vars otv = function
let vars = List.fold_right add_pv pvl vars in
let pvs = List.fold_right Spv.add pvl pvs in
let spec, vty = type_c env pvs vars otv tyc in
let spec = spec_invariant env pvs vty spec in
VTarrow (vty_arrow pvl ~spec vty)
let val_decl env (id,ghost,dtyv) =
......@@ -1095,9 +1102,6 @@ let val_decl env (id,ghost,dtyv) =
| VTvalue v -> LetV (create_pvsymbol id ~ghost v)
| VTarrow a -> LetA (create_psymbol id ~ghost a)
let comp_decl env dtyc =
type_c env Spv.empty vars_empty Stv.empty dtyc
(** Expressions *)
let implicit_post = Debug.register_flag "implicit_post"
......@@ -1281,10 +1285,11 @@ and try_expr keep_loc uloc env ({de_dvty = argl,res} as de0) =
e_let ld (get env de)
| DEghost de -> (* keep user ghost annotations even if redundant *)
e_ghost (get env de)
| DEany dtyc ->
let spec, result = comp_decl env dtyc in
(* no invariants on arbitrary computations *)
e_any spec result
| DEany (dtyv, Some dsp) -> (* we do not add invariants to the top spec *)
let spec, vty = type_c env Spv.empty vars_empty Stv.empty (dtyv,dsp) in
e_any (Some spec) vty
| DEany (dtyv, None) ->
e_any None (type_v env Spv.empty vars_empty Stv.empty dtyv)
| DEfun (fd,de) ->
let fd = expr_fun ~keep_loc ~strict:true uloc env fd in
let e = get (add_fundef env fd) de in
......
......@@ -125,7 +125,7 @@ and dexpr_node =
| DEabstract of dexpr * dspec later
| DEmark of preid * dexpr
| DEghost of dexpr
| DEany of dtype_c
| DEany of dtype_v * dspec later option
| DEcast of dexpr * ity
| DEuloc of dexpr * Loc.position
| DElabel of dexpr * Slab.t
......
......@@ -220,7 +220,7 @@ let ps_equal : psymbol -> psymbol -> bool = (==)
let add_pv_vars vars pv = vars_union vars pv.pv_ity.ity_vars
let add_ps_vars vars ps = vars_union vars ps.ps_vars
let create_psymbol_real ~poly id ghost syms aty =
let create_psymbol_raw ~poly id ghost syms aty =
let { syms_pv = pvset; syms_ps = psset } = syms in
let tyvars = if poly then vars_empty else aty_vars aty in
let pvvars = Spv.fold_left add_pv_vars vars_empty pvset in
......@@ -237,9 +237,6 @@ let create_psymbol_real ~poly id ghost syms aty =
ps_vars = vars;
ps_subst = vars_freeze vars; }
let create_psymbol_poly = create_psymbol_real ~poly:true
let create_psymbol_mono = create_psymbol_real ~poly:false
(** specification *)
let rec aty_pvset aty =
......@@ -268,7 +265,7 @@ let create_psymbol id ?(ghost=false) aty =
let syms = { syms_pv = aty_pvset aty; syms_ps = Sps.empty } in
let vars = Spv.fold_left add_pv_vars vars_empty syms.syms_pv in
aty_check vars aty;
create_psymbol_poly id ghost syms aty
create_psymbol_raw ~poly:true id ghost syms aty
(** program expressions *)
......@@ -498,8 +495,17 @@ let e_arrow_aty ps aty =
let create_let_defn id e =
let lv = match e.e_vty with
| VTarrow aty -> LetA (create_psymbol_mono id e.e_ghost e.e_syms aty)
| VTvalue ity -> LetV (create_pvsymbol id ~ghost:e.e_ghost ity) in
| VTarrow aty ->
let rec is_value e = match e.e_node with
| Earrow _ -> true
| Erec ([fd], {e_node = Earrow ps}) -> (* (fun ... -> ...) *)
ps_equal fd.fun_ps ps && fd.fun_lambda.l_spec.c_letrec = 0
| Eany spec -> eff_is_empty spec.c_effect (* && empty spec? *)
| Eghost e -> is_value e
| _ -> false in
LetA (create_psymbol_raw ~poly:(is_value e) id e.e_ghost e.e_syms aty)
| VTvalue ity ->
LetV (create_pvsymbol id ~ghost:e.e_ghost ity) in
{ let_sym = lv ; let_expr = e }
let create_let_pv_defn id e =
......@@ -813,7 +819,7 @@ let e_try e0 bl =
let pv_dummy = create_pvsymbol (id_fresh "dummy") ity_unit
let e_any spec vty =
let aty = vty_arrow [pv_dummy] ~spec vty in
let aty = vty_arrow [pv_dummy] ?spec vty in
let ps = create_psymbol (id_fresh "dummy") aty in
let syms = del_ps_syms ps (add_ps_syms ps syms_empty) in
let vty = ps.ps_aty.aty_result in
......@@ -844,7 +850,7 @@ let create_fun_defn id ({l_expr = e; l_spec = c} as lam) =
let syms = add_spec_syms lam.l_spec lam.l_expr.e_syms in
let syms = List.fold_right del_pv_syms lam.l_args syms in
let aty = vty_arrow lam.l_args ~spec e.e_vty in
{ fun_ps = create_psymbol_poly id e.e_ghost syms aty;
{ fun_ps = create_psymbol_raw ~poly:true id e.e_ghost syms aty;
fun_lambda = lam;
fun_syms = syms; }
......@@ -887,14 +893,18 @@ let rec expr_subst psm e = e_label_copy e (match e.e_node with
e_arrow_aty (Mps.find ps psm) (aty_of_expr e)
| Eapp (e,pv,_) ->
e_app_real (expr_subst psm e) pv
| Elet ({ let_sym = LetV pv ; let_expr = d }, e) ->
| Elet ({ let_sym = LetV pv; let_expr = d }, e) ->
let nd = expr_subst psm d in
if not (ity_equal (ity_of_expr nd) pv.pv_ity) then
Loc.errorm "vty_value mismatch";
e_let { let_sym = LetV pv ; let_expr = nd } (expr_subst psm e)
| Elet ({ let_sym = LetA ps ; let_expr = d }, e) ->
e_let { let_sym = LetV pv; let_expr = nd } (expr_subst psm e)
| Elet ({ let_sym = LetA ps; let_expr = d }, e) ->
let ld,ns = create_let_ps_defn (id_clone ps.ps_name) (expr_subst psm d) in
e_let ld (expr_subst (Mps.add ps ns psm) e)
| Erec ([{fun_ps = ps; fun_lambda = lam}], e) when lam.l_spec.c_letrec = 0 ->
let lam = { lam with l_expr = expr_subst psm lam.l_expr } in
let fd = create_fun_defn (id_clone ps.ps_name) lam in
e_rec [fd] (expr_subst (Mps.add ps fd.fun_ps psm) e)
| Erec (fdl, e) ->
let conv lam = { lam with l_expr = expr_subst psm lam.l_expr } in
let defl = List.map (fun fd -> fd.fun_ps, conv fd.fun_lambda) fdl in
......
......@@ -246,7 +246,7 @@ val e_for :
pvsymbol -> expr -> for_direction -> expr -> invariant -> expr -> expr
val e_abstract : expr -> spec -> expr
val e_any : spec -> vty -> expr
val e_any : spec option -> vty -> expr
val e_assert : assertion_kind -> term -> expr
val e_absurd : ity -> expr
......
......@@ -561,8 +561,13 @@ let rec dexpr ({uc = uc} as lenv) denv {expr_desc = desc; expr_loc = loc} =
DEtry (e1, List.map branch cl)
| Ptree.Eghost e1 ->
DEghost (dexpr lenv denv e1)
| Ptree.Eany tyc ->
DEany (dtype_c lenv tyc)
| Ptree.Eany (tyv, sp) ->
let dsp = if
sp.sp_pre = [] && sp.sp_post = [] && sp.sp_xpost = [] &&
sp.sp_reads = [] && sp.sp_writes = [] && sp.sp_variant = []
then None
else Some (dspec lenv sp) in
DEany (dtype_v lenv tyv, dsp)
| Ptree.Eabstract (e1, sp) ->
DEabstract (dexpr lenv denv e1, dspec lenv sp)
| Ptree.Eabsurd -> DEabsurd
......
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