Skip to content

GitLab

why3
why3
Commit ae369448 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

whyml: another attempt on program types

parent ebfefedf
Hide whitespace changes
Inline Side-by-side
Showing with 483 additions and 190 deletions
src/whyml/mlw_decl.ml
View file @ ae369448
......@@ -27,9 +27,7 @@ open Decl
open Mlw_ty
open Mlw_expr
type ps_ls = { ps : psymbol; ls : lsymbol }
type constructor = ps_ls * ps_ls option list
type constructor = plsymbol * plsymbol option list
type data_decl = itysymbol * constructor list
......@@ -58,7 +56,7 @@ let syms_ts s ts = Sid.add ts.ts_name s
let syms_ls s ls = Sid.add ls.ls_name s
let syms_its s its = Sid.add its.its_pure.ts_name s
let syms_ps s ps = Sid.add ps.p_name s
let syms_ps s ps = Sid.add ps.ps_name s
let syms_ty s ty = ty_s_fold syms_ts s ty
let syms_term s t = t_s_fold syms_ty syms_ls s t
......@@ -76,66 +74,47 @@ type pre_constructor = preid * (pvsymbol * bool) list
type pre_data_decl = itysymbol * pre_constructor list
exception ConstantConstructor of ident
let create_data_decl tdl =
let syms = ref Sid.empty in
let add s (its,_) = news_id s its.its_pure.ts_name in
let news = ref (List.fold_left add Sid.empty tdl) in
let projections = Hvs.create 17 in (* vs -> ps_ls *)
let build_constructor its (id, al) =
if al = [] then raise (ConstantConstructor (id_register id));
let projections = Hid.create 17 in (* id -> plsymbol *)
let build_constructor its (id,al) =
(* check well-formedness *)
let vtvs = List.map (fun (pv,_) -> vtv_of_pv pv) al in
let tvs = List.fold_right Stv.add its.its_args Stv.empty in
let regs = List.fold_right Sreg.add its.its_regs Sreg.empty in
let check_tv tv =
if not (Stv.mem tv tvs) then raise (UnboundTypeVar tv); true in
let check_reg r =
if not (Sreg.mem r regs) then raise (UnboundRegion r); true in
let check_pv (pv,_) = match pv.pv_mutable with
| None -> ignore (ity_v_all check_tv check_reg pv.pv_ity)
| Some r -> if not (Sreg.mem r regs) then raise (UnboundRegion r)
let check_arg vtv = match vtv.vtv_mut with
| None -> ity_v_all check_tv check_reg vtv.vtv_ity
| Some r -> check_reg r
in
List.iter check_pv al;
ignore (List.for_all check_arg vtvs);
(* build the constructor ps *)
let ity = ity_app its (List.map ity_var its.its_args) its.its_regs in
let result = create_pvsymbol (id_fresh "result") ity in
let ty_args = List.map (fun (pv, _) -> pv.pv_vs.vs_ty) al in
let ls = create_fsymbol id ty_args (ty_of_ity ity) in
let tl = List.map (fun (pv,_) -> t_var pv.pv_vs) al in
let post = t_equ (t_var result.pv_vs) (t_app ls tl ls.ls_value) in
let add_erase ef (pv,_) = option_fold eff_reset ef pv.pv_mutable in
let effect = List.fold_left add_erase eff_empty al in
let al, (a, _) = Util.chop_last al in
let c = vty_arrow a ~post ~effect (vty_value result) in
let arrow (pv,_) c = vty_arrow pv c in
let v = List.fold_right arrow al c in
let ps = create_psymbol id Stv.empty Sreg.empty v in
let ps_ls = { ps = ps; ls = ls } in
news := Sid.add ps.p_name !news;
let tvl = List.map ity_var its.its_args in
let res = vty_value (ity_app its tvl its.its_regs) in
let pls = create_plsymbol id vtvs res in
news := Sid.add pls.pl_ls.ls_name !news;
(* build the projections, if any *)
let build_proj pv =
let id = id_clone pv.pv_vs.vs_name in
let ls = create_fsymbol id [result.pv_vs.vs_ty] pv.pv_vs.vs_ty in
let t = fs_app ls [t_var result.pv_vs] pv.pv_vs.vs_ty in
let post = t_equ (t_var pv.pv_vs) t in
let effect = option_fold eff_read eff_empty pv.pv_mutable in
let vty = vty_arrow result ~post ~effect (vty_value pv) in
let ps = create_psymbol id Stv.empty Sreg.empty vty in
let ps_ls = { ps = ps; ls = ls } in
news := Sid.add ps.p_name !news;
Hvs.add projections pv.pv_vs ps_ls;
ps_ls
let build_proj id vtv =
try Hid.find projections id with Not_found ->
let pls = create_plsymbol (id_clone id) [res] vtv in
news := Sid.add pls.pl_ls.ls_name !news;
Hid.add projections id pls;
pls
in
let build_proj (pv,pj) =
let vtv = vtv_of_pv pv in
syms := ity_s_fold syms_its syms_ts !syms vtv.vtv_ity;
if pj then Some (build_proj pv.pv_vs.vs_name vtv) else None
in
let build_proj pv =
try Hvs.find projections pv.pv_vs with Not_found -> build_proj pv in
let build_proj (pv, pj) =
syms := ity_s_fold syms_its syms_ts !syms pv.pv_ity;
if pj then Some (build_proj pv) else None in
ps_ls, List.map build_proj al
pls, List.map build_proj al
in
let build_type (its, cl) =
Hvs.clear projections;
let build_type (its,cl) =
Hid.clear projections;
its, List.map (build_constructor its) cl
in
let tdl = List.map build_type tdl in
......
src/whyml/mlw_decl.mli
View file @ ae369448
......@@ -27,9 +27,7 @@ open Mlw_expr
(** {2 Type declaration} *)
type ps_ls = private { ps : psymbol; ls : lsymbol }
type constructor = ps_ls * ps_ls option list
type constructor = plsymbol * plsymbol option list
type data_decl = itysymbol * constructor list
......@@ -42,7 +40,7 @@ type pdecl = private {
pd_tag : int; (* unique tag *)
}
and pdecl_node =
and pdecl_node = private
| PDtype of itysymbol
| PDdata of data_decl list
......
src/whyml/mlw_expr.ml
View file @ ae369448
......@@ -24,6 +24,134 @@ open Ty
open Term
open Mlw_ty
(** program variables *)
type pvsymbol = {
pv_vs : vsymbol; (* has a dummy type if pv_vty is an arrow *)
pv_vty : vty;
pv_tvs : Stv.t;
pv_regs : Sreg.t;
}
module Pv = Util.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 = (==)
let ts_dummy = create_tysymbol (id_fresh "arrow_dummy") [] None
let ty_dummy = ty_app ts_dummy []
let create_pvsymbol id vtv =
let ty = ty_of_ity vtv.vtv_ity in
let vs = create_vsymbol id ty in
{ pv_vs = vs;
pv_vty = VTvalue vtv;
pv_tvs = vtv.vtv_tvs;
pv_regs = vtv.vtv_regs;
}
exception NotValue of pvsymbol
let vtv_of_pv pv = match pv.pv_vty with
| VTvalue vtv -> vtv
| VTarrow _ -> raise (NotValue pv)
(** program symbols *)
type psymbol = {
ps_name : ident;
ps_vty : vty_arrow;
ps_tvs : Stv.t;
ps_regs : Sreg.t;
(* these sets cover the type variables and regions of the defining
lambda that cannot be instantiated. Every other type variable
and region in ps_vty is generalized and can be instantiated. *)
}
let ps_equal : psymbol -> psymbol -> bool = (==)
(** program/logic symbols *)
type plsymbol = {
pl_ls : lsymbol;
pl_args : vty_value list;
pl_value : vty_value;
pl_effect : effect;
}
let pl_equal : plsymbol -> plsymbol -> bool = (==)
let create_plsymbol id args value =
let ty_of_vtv vtv = ty_of_ity vtv.vtv_ity in
let pure_args = List.map ty_of_vtv args in
let ls = create_fsymbol id pure_args (ty_of_vtv value) in
let effect = Util.option_fold eff_read eff_empty value.vtv_mut in
let arg_reset acc a = Util.option_fold eff_reset acc a.vtv_mut in
let effect = List.fold_left arg_reset effect args in {
pl_ls = ls;
pl_args = args;
pl_value = value;
pl_effect = effect;
}
(* TODO: patterns *)
(* program expressions *)
type pre = term (* precondition *)
type post = term (* postcondition *)
type xpost = (vsymbol * post) Mexn.t (* exceptional postconditions *)
type variant = {
v_term : term; (* : tau *)
v_rel : lsymbol option; (* tau tau : prop *)
}
type expr = private {
e_node : expr_node;
e_vty : vty;
e_effect : effect;
e_tvs : Stv.t Mid.t;
e_regs : Sreg.t Mid.t;
e_label : Slab.t;
e_loc : Loc.position option;
}
and expr_node =
| Elogic of term
| Esymb of pvsymbol
| Ecast of psymbol * ity_subst
| Eapp of pvsymbol * pvsymbol
| Elet of let_defn * expr
| Erec of rec_defn list * expr
| Eif of pvsymbol * expr * expr
| Eassign of pvsymbol * pvsymbol (* mutable pv <- expr *)
| Eany
and let_defn = {
ld_pv : pvsymbol;
ld_expr : expr;
}
and rec_defn = {
rd_ps : psymbol;
rd_lambda : lambda;
}
and lambda = {
l_args : pvsymbol list;
l_variant : variant list; (* lexicographic order *)
l_pre : pre;
l_expr : expr;
l_post : post;
l_xpost : xpost;
}
(*
- A "proper type" of a vty [v] is [v] with empty specification
(effect/pre/post/xpost). Basically, it is formed from pv_ity's
......@@ -82,66 +210,3 @@ open Mlw_ty
region in [e.e_vty] appear in the range of [e.e_tvs] and [e.e_regs].
*)
type variant = {
v_term : term; (* : tau *)
v_rel : lsymbol option; (* tau tau : prop *)
}
(* program symbols *)
type psymbol = {
p_name : ident;
p_tvs : Stv.t;
p_reg : Sreg.t;
p_vty : vty;
}
let create_psymbol id tvars regs = function
| VTvalue pv ->
let pv =
create_pvsymbol id ?mut:pv.pv_mutable ~ghost:pv.pv_ghost pv.pv_ity in
{ p_name = pv.pv_vs.vs_name;
p_tvs = tvars; p_reg = regs; p_vty = vty_value pv; }
| VTarrow _ as vty ->
(* TODO? check that tvars/regs are in vty *)
{ p_name = id_register id; p_tvs = tvars; p_reg = regs; p_vty = vty; }
let ps_equal : psymbol -> psymbol -> bool = (==)
type expr = private {
e_node : expr_node;
e_vty : vty;
e_eff : effect;
e_ghost : bool;
e_label : Slab.t;
e_loc : Loc.position option;
}
and expr_node =
| Elogic of term
| Esym of psymbol (* function *)
| Eapp of psymbol * expr
| Elet of psymbol * expr * expr
| Eletrec of recfun list * expr
| Efun of lambda
| Eif of expr * expr * expr
| Eassign of pvsymbol * psymbol * region * expr (* e1.f<rho> <- e2 *)
and recfun = psymbol * lambda
and lambda = {
l_args : pvsymbol list;
l_variant : variant list; (* lexicographic order *)
l_pre : term;
l_body : expr;
l_post : term;
l_xpost : xpost;
}
let lapp _ = assert false (*TODO*)
let papp _ = assert false (*TODO*)
let app _ = assert false (*TODO*)
let plet _ = assert false (*TODO*)
let pletrec _ = assert false (*TODO*)
let pfun _ = assert false (*TODO*)
let assign _ = assert false (*TODO*)
src/whyml/mlw_expr.mli
View file @ ae369448
......@@ -24,19 +24,79 @@ open Ty
open Term
open Mlw_ty
(* program symbols *)
type psymbol = private {
p_name : ident;
p_tvs : Stv.t; (* type variables that cannot be instantiated *)
p_reg : Sreg.t; (* regions that cannot be instantiated *)
p_vty : vty;
(** program variables *)
(* pvsymbols represent function arguments (then they must be VTvalue's),
pattern variables (again, VTvalue) or intermediate computation results
introduced by let-expressions. They cannot be type-instantiated. *)
type pvsymbol = private {
pv_vs : vsymbol; (* has a dummy type if pv_vty is an arrow *)
pv_vty : vty;
pv_tvs : Stv.t;
pv_regs : Sreg.t;
(* If pv_vty is a value, these sets coinside with pv_vty.vty_tvs/regs.
If pv_vty is an arrow, we additionally count all type variables
and regions of the defining expression, in order to cover effects
and specification and not overgeneralize. *)
}
val create_psymbol : preid -> Stv.t -> Sreg.t -> vty -> psymbol
val pv_equal : pvsymbol -> pvsymbol -> bool
(* a value-typed pvsymbol to use in function arguments and patterns *)
val create_pvsymbol : preid -> vty_value -> pvsymbol
exception NotValue of pvsymbol
val vtv_of_pv : pvsymbol -> vty_value
(** program symbols *)
(* psymbols represent lambda-abstractions. They are polymorphic and
can be type-instantiated in some type variables and regions of
their type signature. *)
type psymbol = private {
ps_name : ident;
ps_vty : vty_arrow;
ps_tvs : Stv.t;
ps_regs : Sreg.t;
(* these sets cover the type variables and regions of the defining
lambda that cannot be instantiated. Every other type variable
and region in ps_vty is generalized and can be instantiated. *)
}
val ps_equal : psymbol -> psymbol -> bool
(* program expressions *)
(** program/logic symbols *)
(* plymbols represent algebraic type constructors and projections.
They must be fully applied and the result is equal to the application of
the lsymbol. We need this kind of symbols to cover nullary constructors,
such as Nil, which cannot be given a post-condition. They cannot be
locally defined and therefore every type variable and region in their
type signature can be instantiated. *)
type plsymbol = private {
pl_ls : lsymbol;
pl_args : vty_value list;
pl_value : vty_value;
pl_effect : effect;
}
val pl_equal : plsymbol -> plsymbol -> bool
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. *)
(* TODO: patterns *)
(** program expressions *)
type pre = term (* precondition *)
type post = term (* postcondition *)
type xpost = (vsymbol * post) Mexn.t (* exceptional postconditions *)
type variant = {
v_term : term; (* : tau *)
......@@ -44,35 +104,49 @@ type variant = {
}
type expr = private {
e_node : expr_node;
e_vty : vty;
e_eff : effect;
e_ghost : bool;
e_label : Slab.t;
e_loc : Loc.position option;
e_node : expr_node;
e_vty : vty;
e_effect : effect;
e_tvs : Stv.t Mid.t;
e_regs : Sreg.t Mid.t;
e_label : Slab.t;
e_loc : Loc.position option;
}
and expr_node = private
| Elogic of term
| Esym of psymbol (* function *)
| Eapp of psymbol * expr
| Elet of psymbol * expr * expr
| Eletrec of recfun list * expr
| Efun of lambda
| Eif of expr * expr * expr
| Eassign of pvsymbol * psymbol * region * expr (* e1.f<rho> <- e2 *)
| Esymb of pvsymbol
| Ecast of psymbol * ity_subst
| Eapp of pvsymbol * pvsymbol
| Elet of let_defn * expr
| Erec of rec_defn list * expr
| Eif of pvsymbol * expr * expr
| Eassign of pvsymbol * pvsymbol (* mutable pv <- expr *)
| Eany
and recfun = psymbol * lambda
and let_defn = private {
ld_pv : pvsymbol;
ld_expr : expr;
}
and lambda = private {
and rec_defn = private {
rd_ps : psymbol;
rd_lambda : lambda;
}
and lambda = {
l_args : pvsymbol list;
l_variant : variant list; (* lexicographic order *)
l_pre : term;
l_body : expr;
l_post : term;
l_pre : pre;
l_expr : expr;
l_post : post;
l_xpost : xpost;
}
(* TODO: when should we check for escaping identifiers (regions?)
in pre/post/xpost/effects? Here or in WP? *)
(*
val lapp : lsymbol -> expr list -> expr
val papp : psymbol -> expr list -> expr
val app : expr -> expr -> expr
......@@ -80,3 +154,4 @@ val plet : psymbol -> expr -> expr -> expr
val pletrec : recfun list -> expr -> expr
val pfun : lambda -> expr
val assign : expr -> psymbol -> expr -> expr
*)
src/whyml/mlw_module.ml
View file @ ae369448
......@@ -22,6 +22,7 @@ open Why3
open Util
open Ident
open Ty
open Term
open Theory
open Mlw_ty
open Mlw_expr
......@@ -39,9 +40,15 @@ open Mlw_decl
2. logic decls (no types)
3. program decls
*)
type prgsymbol =
| PV of pvsymbol
| PS of psymbol
| PL of plsymbol
type namespace = {
ns_it : itysymbol Mstr.t; (* type symbols *)
ns_ps : psymbol Mstr.t; (* program symbols *)
ns_ps : prgsymbol Mstr.t; (* program symbols *)
ns_ns : namespace Mstr.t; (* inner namespaces *)
}
......@@ -59,11 +66,17 @@ let ns_replace eq chk x vo vn =
let ns_union eq chk =
Mstr.union (fun x vn vo -> Some (ns_replace eq chk x vo vn))
let prg_equal p1 p2 = match p1,p2 with
| PV p1, PV p2 -> pv_equal p1 p2
| PS p1, PS p2 -> ps_equal p1 p2
| PL p1, PL p2 -> pl_equal p1 p2
| _, _ -> false
let rec merge_ns chk ns1 ns2 =
let fusion _ ns1 ns2 = Some (merge_ns chk ns1 ns2) in
{ ns_it = ns_union its_equal chk ns1.ns_it ns2.ns_it;
ns_ps = ns_union ps_equal chk ns1.ns_ps ns2.ns_ps;
ns_ns = Mstr.union fusion ns1.ns_ns ns2.ns_ns; }
ns_ps = ns_union prg_equal chk ns1.ns_ps ns2.ns_ps;
ns_ns = Mstr.union fusion ns1.ns_ns ns2.ns_ns; }
let nm_add chk x ns m = Mstr.change (function
| None -> Some ns
......@@ -74,7 +87,7 @@ let ns_add eq chk x v m = Mstr.change (function
| Some vo -> Some (ns_replace eq chk x vo v)) x m
let it_add = ns_add its_equal
let ps_add = ns_add ps_equal
let ps_add = ns_add prg_equal
let add_it chk x ts ns = { ns with ns_it = it_add chk x ts ns.ns_it }
let add_ps chk x pf ns = { ns with ns_ps = ps_add chk x pf ns.ns_ps }
......@@ -214,9 +227,9 @@ let add_type uc its =
add_symbol add_it its.its_pure.ts_name its uc
let add_data uc (its,csl) =
let add_ps uc {ps=ps} = add_symbol add_ps ps.p_name ps uc in
let add_proj = option_fold add_ps in
let add_constr uc (ps,pjl) = List.fold_left add_proj (add_ps uc ps) pjl in
let add_pls uc pls = add_symbol add_ps pls.pl_ls.ls_name (PL pls) uc in
let add_proj = option_fold add_pls in
let add_constr uc (ps,pjl) = List.fold_left add_proj (add_pls uc ps) pjl in
let uc = add_symbol add_it its.its_pure.ts_name its uc in
List.fold_left add_constr uc csl
......@@ -232,8 +245,8 @@ let add_pdecl uc d =
add_to_theory Theory.add_ty_decl uc its.its_pure
| PDdata dl ->
let uc = List.fold_left add_data uc dl in
let projection = option_map (fun ps -> ps.ls) in
let constructor (ps,pjl) = ps.ls, List.map projection pjl in
let projection = option_map (fun pls -> pls.pl_ls) in
let constructor (pls,pjl) = pls.pl_ls, List.map projection pjl in
let defn cl = List.map constructor cl in
let dl = List.map (fun (its,cl) -> its.its_pure, defn cl) dl in
add_to_theory Theory.add_data_decl uc dl
......
src/whyml/mlw_module.mli
View file @ ae369448
......@@ -29,14 +29,19 @@ open Mlw_ty
open Mlw_expr
open Mlw_decl
type prgsymbol =
| PV of pvsymbol
| PS of psymbol
| PL of plsymbol
type namespace = private {
ns_it : itysymbol Mstr.t; (* type symbols *)
ns_ps : psymbol Mstr.t; (* program symbols *)
ns_ps : prgsymbol Mstr.t; (* program symbols *)
ns_ns : namespace Mstr.t; (* inner namespaces *)
}
val ns_find_it : namespace -> string list -> itysymbol
val ns_find_ps : namespace -> string list -> psymbol
val ns_find_ps : namespace -> string list -> prgsymbol
val ns_find_ns : namespace -> string list -> namespace
(** Module *)
......
src/whyml/mlw_pretty.ml
View file @ ae369448
......@@ -50,7 +50,7 @@ let print_reg fmt reg =
(id_unique rprinter reg.reg_name)
let print_pv fmt pv =
fprintf fmt "%s%a" (if pv.pv_ghost then "?" else "")
fprintf fmt "%s%a" (if vty_ghost pv.pv_vty then "?" else "")
print_vs pv.pv_vs
let forget_pv pv = forget_var pv.pv_vs
......@@ -87,8 +87,10 @@ let print_reg_opt fmt = function
| Some r -> fprintf fmt "<%a>" print_regty r
| None -> ()
(*
let print_pvty fmt pv = fprintf fmt "%a%a:@,%a"
print_pv pv print_reg_opt pv.pv_mutable print_ity pv.pv_ity
*)
(* Labels and locs - copied from Pretty *)
......@@ -107,31 +109,25 @@ let print_tv_arg fmt tv = fprintf fmt "@ %a" print_tv tv
let print_ty_arg fmt ty = fprintf fmt "@ %a" (print_ity_node true) ty
let print_constr fmt (cs,pjl) =
let rec cs_args vty pjl = match vty, pjl with
| VTvalue _, [] -> []
| VTarrow a, pj::pjl ->
let pv, vty = open_vty_arrow a in
(pv,pj) :: cs_args vty pjl
| _, _ -> assert false
in
let pjl = cs_args cs.ps.p_vty pjl in
let print_pj fmt (pv,pj) = match pj with
| Some { ls = ls } ->
let print_pj fmt (vtv,pj) = match pj with
| Some { pl_ls = ls } ->
fprintf fmt "@ (%s%s%a%a:@,%a)"
(if pv.pv_ghost then "ghost " else "")
(if pv.pv_mutable <> None then "mutable " else "")
print_ls ls print_reg_opt pv.pv_mutable print_ity pv