Commit 34e53616 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: some API simplification

parent 0b7efcad
......@@ -9,6 +9,31 @@ WhyML
subregion rho' of rho is not, should we reset rho' under rho?
In Mlw_typing or in Mlw_expr?
- current WP does not respect the lexical scope. In the program
let r = create 0 in
let v = !r in
incr r;
let () =
let v = !r in
()
in
assert { v = 1 }
the last assert will be proven if the same let_defn [let v = !r]
and therefore the same pvsymbol v is used in both places (which
can be done using API). One possible solution is to ensure the
one-time usage of let_defns and rec_defns in programs.
- are mutable values worth it? They can only appear as pattern
variables standing for mutable fields, and allow us to have
mutable fields in algebraic types. On the other hand, they
require tedious checks pretty much everywhere in the code,
and they cannot be translated to OCaml.
- get rid of %Exit, implement unit-typed "break" and "continue",
usable in all kinds of loops, including "for". Why the heck
aren't these in OCaml?
syntaxe
-------
......
......@@ -555,24 +555,19 @@ let add_e_vars e m = varmap_union e.e_vars m
let e_value pv =
mk_expr (Evalue pv) (VTvalue pv.pv_vtv) eff_empty (add_pv_vars pv Mid.empty)
let e_inst ps sbs =
(* we only count the fixed type variables and regions of ps, so that
type variables and regions introduced by the substitution could be
generalized in this expression *)
let vars = Mid.singleton ps.ps_name ps.ps_vars in
let vta = vta_full_inst (ity_subst_union ps.ps_subst sbs) ps.ps_vta in
mk_expr (Earrow ps) (VTarrow vta) eff_empty vars
exception ValueExpected of expr
exception ArrowExpected of expr
let e_cast ps vty =
let rec vty_match sbs t1 t2 = match t1,t2 with
| VTvalue v1, VTvalue v2 ->
ity_match sbs v1.vtv_ity v2.vtv_ity
| VTarrow a1, VTarrow a2 ->
let sbs = ity_match sbs a1.vta_arg.vtv_ity a2.vta_arg.vtv_ity in
vty_match sbs a1.vta_result a2.vta_result
| _ -> invalid_arg "Mlw_expr.e_cast"
in
let sbs = vty_match ps.ps_subst (VTarrow ps.ps_vta) vty in
let vtv_of_expr e = match e.e_vty with
| VTvalue vtv -> vtv
| VTarrow _ -> Loc.error ?loc:e.e_loc (ValueExpected e)
let vta_of_expr e = match e.e_vty with
| VTvalue _ -> Loc.error ?loc:e.e_loc (ArrowExpected e)
| VTarrow vta -> vta
let e_arrow ps vta =
let sbs = vta_vars_match ps.ps_subst ps.ps_vta vta in
let vars = Mid.singleton ps.ps_name ps.ps_vars in
let vta = vta_full_inst sbs ps.ps_vta in
mk_expr (Earrow ps) (VTarrow vta) eff_empty vars
......@@ -629,14 +624,8 @@ let e_let ({ let_var = lv ; let_expr = d } as ld) e =
let eff = eff_union d.e_effect e.e_effect in
mk_expr (Elet (ld,e)) e.e_vty eff (add_e_vars d vars)
exception ValueExpected of expr
exception ArrowExpected of expr
let e_app_real e pv =
let vta = match e.e_vty with
| VTvalue _ -> Loc.error ?loc:e.e_loc (ArrowExpected e)
| VTarrow vta -> vta in
let eff,vty = vty_app_arrow vta pv.pv_vtv in
let eff,vty = vty_app_arrow (vta_of_expr e) pv.pv_vtv in
check_postexpr e eff (add_pv_vars pv Mid.empty);
let eff = eff_union e.e_effect eff in
mk_expr (Eapp (e,pv)) vty eff (add_pv_vars pv e.e_vars)
......@@ -693,10 +682,6 @@ let on_value fn e = match e.e_node with
let e_app = List.fold_left (fun e -> on_value (e_app_real e))
let vtv_of_expr e = match e.e_vty with
| VTvalue vtv -> vtv
| VTarrow _ -> Loc.error ?loc:e.e_loc (ValueExpected e)
let e_plapp pls el ity =
if pls.pl_hidden then raise (HiddenPLS pls.pl_ls);
let rec app tl vars ghost eff sbs vtvl argl =
......@@ -1009,7 +994,7 @@ let ps_compat ps1 ps2 =
let rec expr_subst psm e = match e.e_node with
| Earrow ps when Mid.mem ps.ps_name psm ->
e_cast (Mid.find ps.ps_name psm) e.e_vty
e_arrow (Mid.find ps.ps_name psm) (vta_of_expr e)
| Eapp (e,pv) ->
e_app_real (expr_subst psm e) pv
| Elet ({ let_var = LetV pv ; let_expr = d }, e) ->
......
......@@ -236,14 +236,13 @@ val e_label_add : label -> expr -> expr
val e_label_copy : expr -> expr -> expr
val e_value : pvsymbol -> expr
val e_inst : psymbol -> ity_subst -> expr
val e_cast : psymbol -> vty -> expr
val e_arrow : psymbol -> vty_arrow -> expr
exception ValueExpected of expr
exception ArrowExpected of expr
val vtv_of_expr : expr -> vty_value
val vta_of_expr : expr -> vty_arrow
exception GhostWrite of expr * region
exception GhostRaise of expr * xsymbol
......
......@@ -327,10 +327,15 @@ let th_unit =
let uc = Theory.add_ty_decl uc ts in
close_theory uc
let pd_exit =
let xs = create_xsymbol (id_fresh "%Exit") ity_unit in
create_exn_decl xs
let create_module env ?(path=[]) n =
let m = empty_module env n path in
let m = use_export_theory m bool_theory in
let m = use_export_theory m th_unit in
let m = add_pdecl m pd_exit in
m
(** Clone *)
......
......@@ -37,7 +37,7 @@ module rec T : sig
type itysymbol = {
its_pure : tysymbol;
its_args : tvsymbol list;
its_regs : region list;
its_regs : region list;
its_def : ity option;
its_abst : bool;
its_priv : bool;
......@@ -708,6 +708,13 @@ let vty_app_arrow vta vtv =
of every ghost expression is properly ghostified *)
effect, result
let rec vta_vars_match s vta1 vta2 =
let s = ity_match s vta1.vta_arg.vtv_ity vta2.vta_arg.vtv_ity in
match vta1.vta_result, vta2.vta_result with
| VTarrow vta1, VTarrow vta2 -> vta_vars_match s vta1 vta2
| VTvalue vtv1, VTvalue vtv2 -> ity_match s vtv1.vtv_ity vtv2.vtv_ity
| _ -> invalid_arg "Mlw_ty.vta_vars_match"
(* vty instantiation *)
let vtv_full_inst s vtv =
......@@ -737,231 +744,3 @@ let rec vta_filter vars a =
let rst = eff_filter (vty_vars vars a.vta_result) rst in
let eff = { eff with eff_resets = rst.eff_resets } in
vty_arrow ~ghost:a.vta_ghost ~effect:eff a.vta_arg vty
(** THE FOLLOWING CODE MIGHT BE USEFUL LATER FOR WPgen *)
(*
(* program variables *)
type pvsymbol = {
pv_vs : vsymbol;
pv_ity : ity;
pv_ghost : bool;
pv_mutable : region option;
pv_tvs : Stv.t;
pv_regs : Sreg.t;
}
module Pv = StructMake (struct
type t = pvsymbol
let tag pv = Hashweak.tag_hash pv.pv_vs.vs_name.id_tag
end)
module Spv = Pv.S
module Mpv = Pv.M
let pv_equal : pvsymbol -> pvsymbol -> bool = (==)
exception InvalidPVsymbol of ident
let create_pvsymbol id ?mut ?(ghost=false) ity =
let ty = ty_of_ity ity in
let vs = create_vsymbol id ty in
begin match mut with
| Some r when
(* A ghost variable may contain a non-ghost region.
No writes are allowed in such a ghost variable. *)
not (ity_equal r.reg_ity ity) || (r.reg_ghost && not ghost) ->
raise (InvalidPVsymbol vs.vs_name)
| _ ->
()
end;
let tvs = ity_freevars Stv.empty ity in
let regs = ity_topregions Sreg.empty ity in
let regs = option_fold (fun s r -> Sreg.add r s) regs mut in
{ pv_vs = vs;
pv_ity = ity;
pv_ghost = ghost;
pv_mutable = mut;
pv_tvs = tvs;
pv_regs = regs;
}
let pv_clone pv =
let id = id_clone pv.pv_vs.vs_name in
let vs = create_vsymbol id pv.pv_vs.vs_ty in
{ pv with pv_vs = vs }
let pv_full_inst s pv =
let ghost = pv.pv_ghost in
let mut = option_map (reg_full_inst s) pv.pv_mutable in
let ity = ity_full_inst s pv.pv_ity in
create_pvsymbol (id_clone pv.pv_vs.vs_name) ~ghost ?mut ity
(* value types *)
type vty =
| VTvalue of pvsymbol
| VTarrow of vty_arrow
(* computation types *)
and vty_arrow = {
a_arg : pvsymbol;
a_vty : vty;
a_eff : effect;
a_pre : term; (* epsilon under a dummy variable, to accumulate substs *)
a_post : term; (* epsilon under the value variable or under a dummy vs *)
a_xpost : term Mexn.t; (* epsilon under the exception value variable *)
a_tvs : Stv.t; (* we do not count type variables in eff/pre/post/xpost *)
a_regs : Sreg.t; (* we do not count regions in eff/pre/post/xpost *)
}
type pre = term
type post = term
type xpost = (vsymbol * post) Mexn.t
type vty_comp = {
c_vty : vty;
c_eff : effect;
c_pre : pre;
c_post : post;
c_xpost : xpost;
}
let vty_freevars s = function
| VTvalue pv -> Stv.union s pv.pv_tvs
| VTarrow a -> Stv.union s a.a_tvs
let vty_topregions s = function
| VTvalue pv -> Sreg.union s pv.pv_regs
| VTarrow a -> Sreg.union s a.a_regs
(* smart constructors *)
let vty_value pvs = VTvalue pvs
exception InvalidExceptionPost of xsymbol
(* this vs is used to close pre- and post-conditions in order
to accumulate substitutions into a_arg pvsymbols *)
let close_spec =
let dummy = create_vsymbol (id_fresh "dummy") ty_int in
let dumbf = t_eps_close dummy t_true in
function
| { t_node = Ttrue } -> dumbf
| f -> t_eps_close dummy f
let open_spec = function
| { t_node = Teps bf } -> t_open_bound bf
| _ -> assert false
let vty_arrow
x ?(pre=t_true) ?(post=t_true) ?(xpost=Mexn.empty) ?(effect=eff_empty) vty =
(* check for clashes *)
(* let check_vs y = if vs_equal x.pv_vs y then raise (DuplicateVar y) in *)
let check_pv y = if pv_equal x y then raise (DuplicateVar x.pv_vs) in
let rec check = function
| VTarrow a ->
(* Mexn.iter (fun _ (y,_) -> check_vs y) a.a_xpost; *)
check_pv a.a_arg;
check a.a_vty
| VTvalue y ->
check_pv y
in
check vty;
(* check that every raised exception is mentioned in xpost *)
if not (Mexn.set_submap effect.eff_raises xpost) then
(let d = Mexn.set_diff xpost effect.eff_raises in
raise (InvalidExceptionPost (fst (Mexn.choose d))));
(* check that every exception mentioned in xpost is raised *)
if not (Mexn.set_submap xpost effect.eff_raises) then
(let d = Mexn.set_diff effect.eff_raises xpost in
raise (InvalidExceptionPost (fst (Mexn.choose d))));
(* check that vsymbols in xpost have valid types *)
let conv_xpost xs (vs,f) =
if not (ty_equal (ty_of_ity xs.xs_ity) vs.vs_ty)
then raise (InvalidExceptionPost xs);
(* check_vs vs; *)
t_eps_close vs f
in
let post = match vty with
| VTvalue pv -> t_eps_close pv.pv_vs post
| VTarrow _ -> close_spec post
in
VTarrow {
a_arg = x;
a_vty = vty;
a_eff = effect;
a_pre = close_spec pre;
a_post = post;
a_xpost = Mexn.mapi conv_xpost xpost;
a_tvs = vty_freevars x.pv_tvs vty;
a_regs = vty_topregions x.pv_regs vty;
}
(*
exception NotAFunction
let get_arrow = function
| VTvalue _ -> raise NotAFunction
| VTarrow a -> a
*)
let vty_app_arrow arr x =
ity_equal_check arr.a_arg.pv_ity x.pv_ity;
let subst f = t_subst_single arr.a_arg.pv_vs (t_var x.pv_vs) f in
let _,pre = open_spec (subst arr.a_pre) in
let res,post = open_spec (subst arr.a_post) in
let xsubst e = open_spec (subst e) in
let rec arr_subst arr = { arr with
a_vty = (match arr.a_vty with
| VTarrow a -> VTarrow (arr_subst a)
| VTvalue _ -> arr.a_vty);
a_pre = subst arr.a_pre;
a_post = subst arr.a_post;
a_xpost = Mexn.map subst arr.a_xpost;
}
in
let vty = match arr.a_vty with
(* here we make a new pvsymbol in a bad fashion. It should however
be safe, since res comes from t_open_bound and is guaranteed to
be fresh, so there can be no illegal sharing of idents *)
| VTvalue pv -> VTvalue { pv with pv_vs = res }
| VTarrow a -> VTarrow (arr_subst a)
in {
c_vty = vty;
c_eff = arr.a_eff;
c_pre = pre;
c_post = post;
c_xpost = Mexn.map xsubst arr.a_xpost;
}
let open_vty_arrow arr =
let pv = pv_clone arr.a_arg in
let c = vty_app_arrow arr pv in
pv, c.c_vty
let vty_full_inst s vty =
let subT = Mtv.map ty_of_ity s.ity_subst_tv in
let rec inst subV = function
| VTvalue pv ->
(* this is not the same vsymbol anymore that is bound in
the preceding post. However, this should not matter. *)
VTvalue (pv_full_inst s pv)
| VTarrow a ->
let x = pv_full_inst s a.a_arg in
let subV = Mvs.add a.a_arg.pv_vs (t_var x.pv_vs) subV in
let subst = t_ty_subst subT subV in
let vty = inst subV a.a_vty in
VTarrow {
a_arg = x;
a_vty = vty;
a_eff = eff_full_inst s a.a_eff;
a_pre = subst a.a_pre;
a_post = subst a.a_post;
a_xpost = Mexn.map subst a.a_xpost;
a_tvs = vty_freevars x.pv_tvs vty;
a_regs = vty_topregions x.pv_regs vty;
}
in
inst Mvs.empty vty
*)
......@@ -36,7 +36,7 @@ module rec T : sig
type itysymbol = private {
its_pure : tysymbol;
its_args : tvsymbol list;
its_regs : region list;
its_regs : region list;
its_def : ity option;
its_abst : bool;
its_priv : bool;
......@@ -245,8 +245,7 @@ and vty_arrow = private {
vta_ghost : bool;
vta_vars : varset;
(* this varset covers every type variable and region in vta_arg
and vta_result, but may skip some type variables and regions
in vta_effect *)
and vta_result, but not necessarily in vta_effect *)
}
(* smart constructors *)
......@@ -264,65 +263,16 @@ val vty_ghostify : vty -> vty
val vtv_unmut : vty_value -> vty_value
(* the substitution must cover not only vta.vta_tvs and vta.vta_regs
but also every type variable and every region in vta_effect *)
(* this only compares the types of arguments and results, and ignores
the effects. In other words, only the type variables and regions
in .vta_vars are matched. The caller should supply a "freezing"
substitution that covers all external type variables and regions. *)
val vta_vars_match : ity_subst -> vty_arrow -> vty_arrow -> ity_subst
(* the substitution must cover not only vta_vars but also every
type variable and every region in vta_effect *)
val vta_full_inst : ity_subst -> vty_arrow -> vty_arrow
(* remove from the given arrow every effect that is covered
neither by the arrow's vta_vars nor by the given varset *)
val vta_filter : varset -> vty_arrow -> vty_arrow
(** THE FOLLOWING CODE MIGHT BE USEFUL LATER FOR WPgen *)
(*
(* program variables *)
type pvsymbol = private {
pv_vs : vsymbol;
pv_ity : ity;
pv_ghost : bool;
pv_mutable : region option;
pv_tvs : Stv.t;
pv_regs : Sreg.t;
}
val create_pvsymbol : preid -> ?mut:region -> ?ghost:bool -> ity -> pvsymbol
val pv_equal : pvsymbol -> pvsymbol -> bool
(* value types *)
type pre = term (* precondition *)
type post = term (* postcondition *)
type xpost = (vsymbol * post) Mexn.t (* exceptional postconditions *)
type vty_arrow (* pvsymbol -> vty_comp *)
type vty = private
| VTvalue of pvsymbol
| VTarrow of vty_arrow
type vty_comp = private {
c_vty : vty;
c_eff : effect;
c_pre : pre;
c_post : post;
c_xpost : xpost;
}
(* smart constructors *)
val vty_value : pvsymbol -> vty
val vty_arrow : pvsymbol ->
?pre:term -> ?post:term -> ?xpost:xpost -> ?effect:effect -> vty -> vty
val vty_app_arrow : vty_arrow -> pvsymbol -> vty_comp
val open_vty_arrow : vty_arrow -> pvsymbol * vty
val vty_freevars : Stv.t -> vty -> Stv.t (* only args and values count... *)
val vty_topregions : Sreg.t -> vty -> Sreg.t (* ...not eff/pre/post/xpost *)
(* the substitution must cover not only the vty_freevars and
vty_topregions of vty, but also every type variable and
every region in effects and pre/post/xpost formulas *)
val vty_full_inst : ity_subst -> vty -> vty
*)
......@@ -823,7 +823,11 @@ and expr_desc lenv loc de = match de.de_desc with
assert (Mstr.mem x lenv.let_vars);
begin match Mstr.find x lenv.let_vars with
| LetV pv -> e_value pv
| LetA ps -> e_cast ps (vty_of_dvty de.de_type)
| LetA ps ->
begin match vty_of_dvty de.de_type with
| VTarrow vta -> e_arrow ps vta
| VTvalue _ -> assert false
end
end
| DElet (x, gh, { de_desc = DEfun lam }, de2) ->
let def = expr_fun lenv x gh lam in
......@@ -833,13 +837,13 @@ and expr_desc lenv loc de = match de.de_desc with
| DEfun lam ->
let x = mk_id "fn" loc in
let def = expr_fun lenv x false lam in
let e2 = e_cast def.rec_ps (VTarrow def.rec_ps.ps_vta) in
let e2 = e_arrow def.rec_ps def.rec_ps.ps_vta in
e_rec [def] e2
(* FIXME? (ghost "lab" fun x -> ...) loses the label "lab" *)
| DEghost { de_desc = DEfun lam } ->
let x = mk_id "fn" loc in
let def = expr_fun lenv x true lam in
let e2 = e_cast def.rec_ps (VTarrow def.rec_ps.ps_vta) in
let e2 = e_arrow def.rec_ps def.rec_ps.ps_vta in
e_rec [def] e2
| DElet (x, gh, de1, de2) ->
let e1 = e_ghostify gh (expr lenv de1) in
......@@ -867,7 +871,10 @@ and expr_desc lenv loc de = match de.de_desc with
| DEglobal_pv pv ->
e_value pv
| DEglobal_ps ps ->
e_cast ps (vty_of_dvty de.de_type)
begin match vty_of_dvty de.de_type with
| VTarrow vta -> e_arrow ps vta
| VTvalue _ -> assert false
end
| DEglobal_pl pl ->
e_plapp pl [] (ity_of_dity (snd de.de_type))
| DEglobal_ls ls ->
......
......@@ -228,15 +228,7 @@ and spec_expr e = match e.e_node with
(* TODO: a ps may not be in the table, if it comes from a module
for which we never computed WPs. Pass the known_map to spec_expr
and compute it now. *)
let rec vty_match sbs t1 t2 = match t1,t2 with
| VTvalue v1, VTvalue v2 ->
ity_match sbs v1.vtv_ity v2.vtv_ity
| VTarrow a1, VTarrow a2 ->
let sbs = ity_match sbs a1.vta_arg.vtv_ity a2.vta_arg.vtv_ity in
vty_match sbs a1.vta_result a2.vta_result
| _ -> assert false
in
let sbs = vty_match ps.ps_subst (VTarrow ps.ps_vta) e.e_vty in
let sbs = vta_vars_match ps.ps_subst ps.ps_vta (vta_of_expr e) in
let tvm = Mtv.map ty_of_ity sbs.ity_subst_tv in
let tyv = Wps.find psymbol_spec_t ps in
spec_inst_v sbs tvm Mvs.empty tyv
......
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