Skip to content

GitLab

Commit afa16279 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

whyml: introduce rich specification types, rework e_any

parent ccdb4088
Hide whitespace changes
Inline Side-by-side
Showing with 299 additions and 166 deletions
Makefile.in
View file @ afa16279
......@@ -393,8 +393,8 @@ install_local: bin/why3
# Whyml (new API)
########
MLW_FILES = mlw_ty mlw_expr mlw_decl mlw_module mlw_pretty \
mlw_wp mlw_dtree mlw_dty mlw_typing mlw_main
MLW_FILES = mlw_ty mlw_expr mlw_wp mlw_decl mlw_module \
mlw_pretty mlw_dtree mlw_dty mlw_typing mlw_main
MLWMODULES = $(addprefix src/whyml/, $(MLW_FILES))
......
src/whyml/mlw_dtree.ml
View file @ afa16279
......@@ -38,13 +38,6 @@ type ghost = bool
type dpre = Ptree.pre
type dpost = Ptree.pre
type dxpost = (xsymbol * dpost) list
type deffect = {
deff_reads : Ptree.lexpr list;
deff_writes : Ptree.lexpr list;
deff_raises : xsymbol list;
}
type dbinder = ident * ghost * dity
(**
......@@ -82,7 +75,6 @@ and dexpr_desc =
| DElet of ident * dexpr * dexpr
| DEletrec of drecfun list * dexpr
| DEassign of dexpr * dexpr
| DEsequence of dexpr * dexpr
| DEif of dexpr * dexpr * dexpr
| DEloop of dvariant list * dinvariant * dexpr
| DElazy of Ptree.lazy_op * dexpr * dexpr
......@@ -94,8 +86,19 @@ and dexpr_desc =
| DEfor of ident * dexpr * Ptree.for_direction * dexpr * dinvariant * dexpr
| DEassert of Ptree.assertion_kind * Ptree.lexpr
| DEmark of ident * dexpr
(* | DEany of dutype_c *)
| DEghost of dexpr
(*
| DEany of deffect
*)
and drecfun = ident * dity * dlambda
and dlambda = dbinder list * dvariant list * dpre * dexpr * dpost * dxpost
(*
and deffect = {
deff_reads : dexpr list;
deff_writes : dexpr list;
deff_raises : (ghost * xsymbol) list;
}
*)
src/whyml/mlw_expr.ml
View file @ afa16279
......@@ -92,6 +92,137 @@ let create_plsymbol id args value =
pl_effect = effect;
}
(** specification *)
type pre = term (* precondition *)
type post = term (* postcondition *)
type xpost = post Mexn.t (* exceptional postconditions *)
type type_c = {
c_pre : pre;
c_effect : effect;
c_result : type_v;
c_post : post;
c_xpost : xpost;
}
and type_v =
| SpecV of vty_value
| SpecA of pvsymbol list * type_c
type let_var =
| LetV of pvsymbol
| LetA of psymbol
type val_decl = {
val_name : let_var;
val_decl : type_v;
val_vars : varset Mid.t;
}
type variant = {
v_term : term; (* : tau *)
v_rel : lsymbol option; (* tau tau : prop *)
}
let create_post vs f = t_eps_close vs f
let open_post f = match f.t_node with
| Teps bf -> t_open_bound bf
| _ -> assert false
let varmap_join = Mid.fold (fun _ -> vars_union)
let varmap_union = Mid.set_union
let add_pv_vars pv m = Mid.add pv.pv_vs.vs_name pv.pv_vtv.vtv_vars m
let add_vs_vars vs m = add_pv_vars (restore_pv vs) m
let spec_vars varm variant pre post xpost _effect result =
(* sanity check *)
if pre.t_ty <> None then raise (FmlaExpected pre);
let check_post ity post =
let ty = ty_of_ity ity in
if not (ty_equal ty (t_type post)) then
raise (Ty.TypeMismatch (ty, t_type post))
in
begin match result with
| Some vtv -> check_post vtv.vtv_ity post
| None -> ()
(* FIXME? Should we check that the bound variable does not occur
in the postcondition formula when result is an arrow? *)
end;
(* FIXME? Should we check that every raised exception is in xpost? *)
Mexn.iter (fun xs t -> check_post xs.xs_ity t) xpost;
(* compute rec_vars and ps.ps_vars *)
let add_term t s = Mvs.set_union t.t_vars s in
let add_variant { v_term = t; v_rel = ps } s =
ignore (Util.option_map (fun ps -> ps_app ps [t;t]) ps);
add_term t s in
let vsset = add_term post (add_term pre Mvs.empty) in
let vsset = Mexn.fold (fun _ -> add_term) xpost vsset in
let vsset = List.fold_right add_variant variant vsset in
Mvs.fold (fun vs _ m -> add_vs_vars vs m) vsset varm
let spec_arrow pvl effect vty =
let arg,argl = match List.rev pvl with
| [] -> Loc.errorm "Empty argument list"
| arg::argl -> arg, argl in
let vta = vty_arrow arg.pv_vtv ~effect vty in
let add_arg vta pv = vty_arrow pv.pv_vtv (VTarrow vta) in
List.fold_left add_arg vta argl
let rec check_c tyc =
let varm = check_v tyc.c_result in
let result = match tyc.c_result with
| SpecV v -> Some v
| SpecA _ -> None in
spec_vars varm [] tyc.c_pre tyc.c_post tyc.c_xpost tyc.c_effect result
and check_v = function
| SpecV _ -> Mid.empty
| SpecA (pvl,tyc) ->
let del_pv m pv = Mid.remove pv.pv_vs.vs_name m in
List.fold_left del_pv (check_c tyc) pvl
let eff_check vars result e =
let check r =
if not (reg_occurs r vars) then
Loc.errorm "every external effect must be covered in a post-condition"
in
let reset r u = match result with
| _ when u <> None -> Loc.errorm "abstract parameters cannot reset regions"
| SpecV v when reg_occurs r v.vtv_vars -> ()
| _ -> check r
in
Sreg.iter check e.eff_reads;
Sreg.iter check e.eff_writes;
Sreg.iter check e.eff_ghostr;
Sreg.iter check e.eff_ghostw;
Mreg.iter reset e.eff_resets
let rec build_c vars tyc =
let vty = build_v vars tyc.c_result in
eff_check vars tyc.c_result tyc.c_effect;
vty
and build_v vars = function
| SpecV vtv ->
if vtv.vtv_mut <> None then
Loc.errorm "abstract parameters cannot produce mutable values";
VTvalue vtv
| SpecA (pvl,tyc) ->
let add_arg vars pv = vars_union vars pv.pv_vtv.vtv_vars in
let vty = build_c (List.fold_left add_arg vars pvl) tyc in
VTarrow (spec_arrow pvl tyc.c_effect vty)
let create_val_decl id tyv =
let varm = check_v tyv in
let vars = varmap_join varm vars_empty in
let name = match build_v vars tyv with
| VTarrow vta -> LetA (create_psymbol id vta vars)
| VTvalue vtv -> LetV (create_pvsymbol id vtv) in
{ val_name = name; val_decl = tyv; val_vars = varm }
(** patterns *)
type ppattern = {
......@@ -199,8 +330,6 @@ type pre_ppattern =
| PPor of pre_ppattern * pre_ppattern
| PPas of pre_ppattern * preid
let vtv_unmut vtv = vty_value ~ghost:vtv.vtv_ghost vtv.vtv_ity
let make_ppattern pp vtv =
let hv = Hashtbl.create 3 in
let find id vtv =
......@@ -280,17 +409,8 @@ let make_ppattern pp vtv =
(** program expressions *)
type pre = term (* precondition *)
type post = term (* postcondition *)
type xpost = post Mexn.t (* exceptional postconditions *)
type assertion_kind = Aassert | Aassume | Acheck
type variant = {
v_term : term; (* : tau *)
v_rel : lsymbol option; (* tau tau : prop *)
}
type expr = {
e_node : expr_node;
e_vty : vty;
......@@ -311,7 +431,7 @@ and expr_node =
| Ecase of expr * (ppattern * expr) list
| Eassign of expr * region * pvsymbol
| Eghost of expr
| Eany of any_effect
| Eany of type_c
| Eraise of xsymbol * expr
| Etry of expr * (xsymbol * pvsymbol * expr) list
| Eassert of assertion_kind * term
......@@ -322,10 +442,6 @@ and let_defn = {
let_expr : expr;
}
and let_var =
| LetV of pvsymbol
| LetA of psymbol
and rec_defn = {
rec_ps : psymbol;
rec_lambda : lambda;
......@@ -341,12 +457,6 @@ and lambda = {
l_xpost : xpost;
}
and any_effect = {
aeff_reads : expr list;
aeff_writes : expr list;
aeff_raises : (bool * xsymbol) list;
}
(* smart constructors *)
let e_label ?loc l e = { e with e_label = l; e_loc = loc }
......@@ -370,12 +480,6 @@ let mk_expr node vty eff vars = {
e_loc = None;
}
let varmap_join = Mid.fold (fun _ -> vars_union)
let varmap_union = Mid.set_union
let add_pv_vars pv m = Mid.add pv.pv_vs.vs_name pv.pv_vtv.vtv_vars m
let add_vs_vars vs m = add_pv_vars (restore_pv vs) m
let add_t_vars t m = Mvs.fold (fun vs _ m -> add_vs_vars vs m) t.t_vars m
let add_e_vars e m = varmap_union e.e_vars m
......@@ -466,52 +570,21 @@ let e_app_real e pv =
let eff = eff_union e.e_effect eff in
mk_expr (Eapp (e,pv)) vty eff (add_pv_vars pv e.e_vars)
let create_post vs f = t_eps_close vs f
let open_post f = match f.t_node with
| Teps bf -> t_open_bound bf
| _ -> assert false
let create_fun_defn id lam =
(* sanity check *)
if lam.l_pre.t_ty <> None then raise (FmlaExpected lam.l_pre);
let check_post ity post =
let ty = ty_of_ity ity in
if not (ty_equal ty (t_type post)) then
raise (Ty.TypeMismatch (ty, t_type post))
in
begin match lam.l_expr.e_vty with
| VTvalue vtv -> check_post vtv.vtv_ity lam.l_post
| VTarrow _ -> ()
(* FIXME? Should we check that the bound variable does not occur
in the postcondition formula when lam.l_expr.e_vty is an arrow? *)
end;
Mexn.iter (fun xs t -> check_post xs.xs_ity t) lam.l_xpost;
(* compute rec_vars and ps.ps_vars *)
let add_term t s = Mvs.set_union t.t_vars s in
let add_variant { v_term = t; v_rel = ps } s =
ignore (Util.option_map (fun ps -> ps_app ps [t;t]) ps);
add_term t s in
let vsset = add_term lam.l_post (add_term lam.l_pre Mvs.empty) in
let vsset = Mexn.fold (fun _ -> add_term) lam.l_xpost vsset in
let vsset = List.fold_right add_variant lam.l_variant vsset in
let add_vs vs _ m = add_vs_vars vs m in
let del_pv m pv = Mid.remove pv.pv_vs.vs_name m in
let recvars = Mvs.fold add_vs vsset lam.l_expr.e_vars in
let recvars = List.fold_left del_pv recvars lam.l_args in
let vars = varmap_join recvars vars_empty in
(* compute rec_ps.ps_vta *)
let e = lam.l_expr in
let arg, argl = match List.rev lam.l_args with
| [] -> Loc.errorm "Empty argument list"
| arg::argl -> arg, argl in
let vta = vty_arrow arg.pv_vtv ~effect:e.e_effect e.e_vty in
let add_arg vta pv = vty_arrow pv.pv_vtv (VTarrow vta) in
let vta = List.fold_left add_arg vta argl in
let result = match e.e_vty with
| VTvalue v -> Some v
| VTarrow _ -> None in
let varm = spec_vars e.e_vars lam.l_variant
lam.l_pre lam.l_post lam.l_xpost e.e_effect result in
let del_pv m pv = Mid.remove pv.pv_vs.vs_name m in
let varm = List.fold_left del_pv varm lam.l_args in
let vars = varmap_join varm vars_empty in
let vta = spec_arrow lam.l_args e.e_effect e.e_vty in
(* construct rec_defn *)
{ rec_ps = create_psymbol id vta vars;
rec_lambda = lam;
rec_vars = recvars; }
rec_vars = varm; }
let e_rec rdl e =
let add_vars m rd = varmap_union m rd.rec_vars in
......@@ -684,26 +757,10 @@ let e_assign me e = on_value (e_assign_real me) e
let e_ghost e =
mk_expr (Eghost e) (vty_ghostify e.e_vty) e.e_effect e.e_vars
let e_any ee ity =
let add_effect fn eff e =
let vtv = vtv_of_expr e in
let r = match vtv.vtv_mut with
| Some r -> r
| None -> raise (Immutable e) in
fn eff ?ghost:(Some vtv.vtv_ghost) r
in
let add_raise eff (ghost,xs) =
eff_raise eff ~ghost xs
in
let eff = eff_empty in
let eff = List.fold_left (add_effect eff_read) eff ee.aeff_reads in
let eff = List.fold_left (add_effect eff_read) eff ee.aeff_writes in
let eff = List.fold_left add_raise eff ee.aeff_raises in
let eff = Sreg.fold (fun r e -> eff_reset e r) ity.ity_vars.vars_reg eff in
let vars = Mid.empty in
let vars = List.fold_right add_e_vars ee.aeff_reads vars in
let vars = List.fold_right add_e_vars ee.aeff_writes vars in
mk_expr (Eany ee) (VTvalue (vty_value ity)) eff vars
let e_any tyc =
let varm = check_c tyc in
let vars = varmap_join varm vars_empty in
mk_expr (Eany tyc) (build_c vars tyc) tyc.c_effect varm
let e_const t =
let vtv = vty_value (ity_of_ty_opt t.t_ty) in
......@@ -872,18 +929,12 @@ 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)
| Eany ee ->
e_any {
aeff_reads = List.map (expr_subst psm) ee.aeff_reads;
aeff_writes = List.map (expr_subst psm) ee.aeff_writes;
aeff_raises = ee.aeff_raises;
} (vtv_of_expr e).vtv_ity
| Eraise (xs,e0) ->
e_raise xs (expr_subst psm e0) (vtv_of_expr e).vtv_ity
| Etry (e,bl) ->
let branch (xs,pv,e) = xs, pv, expr_subst psm e in
e_try (expr_subst psm e) (List.map branch bl)
| Elogic _ | Evalue _ | Earrow _ | Eabsurd | Eassert _ -> e
| Elogic _ | Evalue _ | Earrow _ | Eany _ | Eabsurd | Eassert _ -> e
and create_rec_defn defl =
let conv m (ps,lam) =
......
src/whyml/mlw_expr.mli
View file @ afa16279
......@@ -83,6 +83,39 @@ val create_plsymbol : preid -> vty_value list -> vty_value -> plsymbol
(* FIXME? Effect calculation is hardwired to correspond to constructors
and projections: mutable arguments are reset, mutable result is read. *)
(** specification *)
type pre = term (* precondition *)
type post (* postcondition: a formula with a bound variable *)
type xpost = post Mexn.t (* exceptional postconditions *)
val create_post : vsymbol -> term -> post
val open_post : post -> vsymbol * term
type type_c = {
c_pre : pre;
c_effect : effect;
c_result : type_v;
c_post : post;
c_xpost : xpost;
}
and type_v =
| SpecV of vty_value
| SpecA of pvsymbol list * type_c
type let_var =
| LetV of pvsymbol
| LetA of psymbol
type val_decl = private {
val_name : let_var;
val_decl : type_v;
val_vars : varset Mid.t;
}
val create_val_decl : Ident.preid -> type_v -> val_decl
(** patterns *)
type ppattern = private {
......@@ -112,18 +145,6 @@ val make_ppattern : pre_ppattern -> vty_value -> pvsymbol Mstr.t * ppattern
type assertion_kind = Aassert | Aassume | Acheck
type pre = term (* precondition *)
type post (* postcondition: a formula with a bound variable *)
type xpost = post Mexn.t (* exceptional postconditions *)
val create_post : vsymbol -> term -> post
val open_post : post -> vsymbol * term
type variant = {
v_term : term; (* : tau *)
v_rel : lsymbol option; (* tau tau : prop *)
}
type expr = private {
e_node : expr_node;
e_vty : vty;
......@@ -144,7 +165,7 @@ and expr_node = private
| Ecase of expr * (ppattern * expr) list
| Eassign of expr * region * pvsymbol
| Eghost of expr
| Eany of any_effect
| Eany of type_c
| Eraise of xsymbol * expr
| Etry of expr * (xsymbol * pvsymbol * expr) list
| Eassert of assertion_kind * term
......@@ -155,10 +176,6 @@ and let_defn = private {
let_expr : expr;
}
and let_var =
| LetV of pvsymbol
| LetA of psymbol
and rec_defn = private {
rec_ps : psymbol;
rec_lambda : lambda;
......@@ -174,13 +191,9 @@ and lambda = {
l_xpost : xpost;
}
(* TODO? Every top region in the type of Eany is reset.
This is enough for our current purposes, but we might
need to be more flexible later. *)
and any_effect = {
aeff_reads : expr list; (* for a ghost read, use a ghost expression *)
aeff_writes : expr list; (* for a ghost write, use a ghost expression *)
aeff_raises : (bool * xsymbol) list; (* ghost raise * exception symbol *)
and variant = {
v_term : term; (* : tau *)
v_rel : lsymbol option; (* tau tau : prop *)
}
val e_label : ?loc:Loc.position -> Slab.t -> expr -> expr
......@@ -222,7 +235,7 @@ exception Immutable of expr
val e_assign : expr -> expr -> expr
val e_ghost : expr -> expr
val e_any : any_effect -> ity -> expr
val e_any : type_c -> expr
val e_void : expr
......@@ -239,4 +252,3 @@ val e_try : expr -> (xsymbol * pvsymbol * expr) list -> expr
val e_absurd : ity -> expr
val e_assert : assertion_kind -> term -> expr
src/whyml/mlw_ty.ml
View file @ afa16279
......@@ -131,6 +131,10 @@ let create_varset tvs regs = {
vars_reg = regs;
}
let rec reg_occurs r vars =
let check r r' = reg_equal r r' || reg_occurs r r'.reg_ity.ity_vars in
Sreg.exists (check r) vars.vars_reg
(* value type symbols *)
module Itsym = WeakStructMake (struct
......@@ -601,12 +605,7 @@ let eff_full_inst s e =
}
let eff_filter vars e =
let rec check r vars =
Sreg.exists (occurs r) vars.vars_reg
and occurs r r' =
reg_equal r r' || check r r'.reg_ity.ity_vars
in
let check r = check r vars in
let check r = reg_occurs r vars in
let reset r = function
| _ when not (check r) -> None
| Some u as v when check u -> Some v
......@@ -665,6 +664,10 @@ let vty_value ?(ghost=false) ?mut ity =
vtv_vars = vars;
}
let vtv_unmut vtv =
if vtv.vtv_mut = None then vtv else
vty_value ~ghost:vtv.vtv_ghost vtv.vtv_ity
let vty_arrow vtv ?(effect=eff_empty) ?(ghost=false) vty =
(* mutable arguments are rejected outright *)
if vtv.vtv_mut <> None then
......@@ -672,10 +675,8 @@ let vty_arrow vtv ?(effect=eff_empty) ?(ghost=false) vty =
(* we accept a mutable vty_value as a result to simplify Mlw_expr,
but erase it in the signature: only projections return mutables *)
let vty = match vty with
| VTvalue ({ vtv_mut = Some r ; vtv_vars = vars } as vtv) ->
let vars = { vars with vars_reg = Sreg.remove r vars.vars_reg } in
VTvalue { vtv with vtv_mut = None ; vtv_vars = vars }
| _ -> vty
| VTvalue v -> VTvalue (vtv_unmut v)
| VTarrow _ -> vty
in {
vta_arg = vtv;
vta_result = vty;
......@@ -722,16 +723,16 @@ and vty_full_inst s = function
| VTvalue vtv -> VTvalue (vtv_full_inst s vtv)
| VTarrow vta -> VTarrow (vta_full_inst s vta)
let vta_filter vars vta =
let vars = vars_union vars vta.vta_vars in
let rec filter a =
let vty = match a.vta_result with
| VTarrow a -> VTarrow (filter a)
| v -> v in
let effect = eff_filter vars a.vta_effect in
vty_arrow ~ghost:a.vta_ghost ~effect a.vta_arg vty
in
filter vta
let rec vta_filter vars a =
let vars = vars_union vars a.vta_arg.vtv_vars in
let vty, vars = match a.vta_result with
(* FIXME? We allow effects on the regions from a VTvalue result,
but only reset is actually meaningful. Should we require that
any new region in the result be reset? *)
| VTvalue v -> a.vta_result, vars_union vars v.vtv_vars
| VTarrow a -> VTarrow (vta_filter vars a), vars in
let effect = eff_filter vars a.vta_effect in
vty_arrow ~ghost:a.vta_ghost ~effect a.vta_arg vty
(** THE FOLLOWING CODE MIGHT BE USEFUL LATER FOR WPgen *)
(*
......
src/whyml/mlw_ty.mli
View file @ afa16279
......@@ -86,6 +86,8 @@ val ity_hash : ity -> int
val reg_equal : region -> region -> bool
val reg_hash : region -> int
val reg_occurs : region -> varset -> bool
exception BadItyArity of itysymbol * int * int
exception BadRegArity of itysymbol * int * int
exception DuplicateRegion of region
......@@ -255,6 +257,8 @@ val vty_vars : varset -> vty -> varset
val vty_ghost : vty -> bool
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 *)
val vta_full_inst : ity_subst -> vty_arrow -> vty_arrow
......
src/whyml/mlw_typing.ml
View file @ afa16279
......@@ -211,12 +211,17 @@ let mk_var e =
dexpr_loc = e.dexpr_loc;
dexpr_lab = [] }
let mk_id s loc =
{ id = s; id_loc = loc; id_lab = [] }
let mk_dexpr desc dity loc labs =
{ dexpr_desc = desc; dexpr_type = dity; dexpr_loc = loc; dexpr_lab = labs }
let mk_let ~loc ~uloc e (desc,dity) =
if test_var e then desc, dity else
let loc = def_option loc uloc in
let e1 = {
dexpr_desc = desc; dexpr_type = dity; dexpr_loc = loc; dexpr_lab = [] } in
DElet ({ id = "q"; id_lab = []; id_loc = loc }, e, e1), dity
let e1 = mk_dexpr desc dity loc [] in
DElet (mk_id "q" loc, e, e1), dity
(* patterns *)
......@@ -257,9 +262,6 @@ let find_variant_ls ~loc uc p =
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 }
let rec dpattern denv ({ pat_loc = loc } as pp) = match pp.pat_desc with
| Ptree.PPpwild ->
PPwild, create_type_variable (), denv
......@@ -309,6 +311,16 @@ and dpat_app denv ({ dexpr_loc = loc } as de) ppl =
Loc.try2 loc unify de.dexpr_type (make_arrow_type tyl res);
pp, res, denv
(*