Commit 2a1ef857 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: split pvsymbol into two types for values and arrows

parent 77124a18
......@@ -81,7 +81,7 @@ let create_data_decl tdl =
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 vtvs = List.map (fun (pv,_) -> pv.pv_vtv) 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 =
......@@ -107,7 +107,7 @@ let create_data_decl tdl =
pls
in
let build_proj (pv,pj) =
let vtv = vtv_of_pv pv in
let vtv = pv.pv_vtv 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
......
......@@ -27,10 +27,8 @@ 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;
pv_vs : vsymbol;
pv_vtv : vty_value;
}
module Pv = Util.StructMake (struct
......@@ -45,21 +43,17 @@ let pv_equal : pvsymbol -> pvsymbol -> bool = (==)
let create_pvsymbol id vtv = {
pv_vs = create_vsymbol id (ty_of_ity vtv.vtv_ity);
pv_vty = VTvalue vtv;
pv_tvs = vtv.vtv_tvs;
pv_regs = vtv.vtv_regs;
pv_vtv = vtv;
}
exception ValueExpected of pvsymbol
exception ArrowExpected of pvsymbol
let vtv_of_pv pv = match pv.pv_vty with
| VTvalue vtv -> vtv
| VTarrow _ -> raise (ValueExpected pv)
type pasymbol = {
pa_name : ident;
pa_vta : vty_arrow;
pa_tvs : Stv.t;
pa_regs : Sreg.t;
}
let vta_of_pv pv = match pv.pv_vty with
| VTarrow vta -> vta
| VTvalue _ -> raise (ArrowExpected pv)
let pa_equal : pasymbol -> pasymbol -> bool = (==)
(** program symbols *)
......@@ -105,11 +99,6 @@ 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 = {
e_node : expr_node;
e_vty : vty;
......@@ -122,9 +111,9 @@ type expr = {
and expr_node =
| Elogic of term
| Evar of pvsymbol
| Esym of psymbol * ity_subst
| Eapp of pvsymbol * pvsymbol
| Earrow of pasymbol
| Einst of psymbol * ity_subst
| Eapp of pasymbol * pvsymbol
| Elet of let_defn * expr
| Erec of rec_defn list * expr
| Eif of pvsymbol * expr * expr
......@@ -132,13 +121,17 @@ and expr_node =
| Eany
and let_defn = {
ld_pv : pvsymbol;
ld_expr : expr;
let_var : let_var;
let_expr : expr;
}
and let_var =
| LetV of pvsymbol
| LetA of pasymbol
and rec_defn = {
rd_ps : psymbol;
rd_lambda : lambda;
rec_ps : psymbol;
rec_lambda : lambda;
}
and lambda = {
......@@ -150,6 +143,12 @@ and lambda = {
l_xpost : xpost;
}
and variant = {
v_term : term; (* : tau *)
v_rel : lsymbol option; (* tau tau : prop *)
}
(* smart constructors *)
let e_label ?loc l e = { e with e_label = l; e_loc = loc }
......@@ -172,8 +171,11 @@ let e_dummy node vty = {
e_loc = None;
}
let add_pv_tvs s pv = Mid.add pv.pv_vs.vs_name pv.pv_tvs s
let add_pv_regs s pv = Mid.add pv.pv_vs.vs_name pv.pv_regs s
let add_pv_tvs s pv = Mid.add pv.pv_vs.vs_name pv.pv_vtv.vtv_tvs s
let add_pv_regs s pv = Mid.add pv.pv_vs.vs_name pv.pv_vtv.vtv_regs s
let add_pa_tvs s pa = Mid.add pa.pa_name pa.pa_tvs s
let add_pa_regs s pa = Mid.add pa.pa_name pa.pa_regs s
let add_expr_tvs m e =
Mid.union (fun _ s1 s2 -> Some (Stv.union s1 s2)) m e.e_tvs
......@@ -181,22 +183,23 @@ let add_expr_tvs m e =
let add_expr_regs m e =
Mid.union (fun _ s1 s2 -> Some (Sreg.union s1 s2)) m e.e_regs
let e_var pv =
let node = match pv.pv_vty with
| VTarrow _ -> Evar pv
| VTvalue _ -> Elogic (t_var pv.pv_vs)
in
{ (e_dummy node pv.pv_vty) with
let e_value pv =
{ (e_dummy (Elogic (t_var pv.pv_vs)) (VTvalue pv.pv_vtv)) with
e_tvs = add_pv_tvs Mid.empty pv;
e_regs = add_pv_regs Mid.empty pv; }
let e_sym ps sbs =
let e_arrow pa =
{ (e_dummy (Earrow pa) (VTarrow pa.pa_vta)) with
e_tvs = add_pa_tvs Mid.empty pa;
e_regs = add_pa_regs Mid.empty pa; }
let e_inst ps sbs =
let vty =
if not (Mtv.is_empty sbs.ity_subst_tv && Mreg.is_empty sbs.ity_subst_reg)
then VTarrow (vta_full_inst (ity_subst_union ps.ps_subst sbs) ps.ps_vta)
else VTarrow ps.ps_vta
in
{ (e_dummy (Esym (ps,sbs)) vty) with
{ (e_dummy (Einst (ps,sbs)) vty) with
e_tvs = Mid.singleton ps.ps_name ps.ps_tvs;
e_regs = Mid.singleton ps.ps_name ps.ps_regs; }
(* we only count the fixed type variables and regions of ps, so that
......@@ -216,35 +219,34 @@ let ghost_effect e =
else e
else e
let e_app pvf pva =
let eff,vty = vty_app_arrow (vta_of_pv pvf) (vtv_of_pv pva) in
ghost_effect { (e_dummy (Eapp (pvf,pva)) vty) with
let e_app pa pv =
let eff,vty = vty_app_arrow pa.pa_vta pv.pv_vtv in
ghost_effect { (e_dummy (Eapp (pa,pv)) vty) with
e_effect = eff;
e_tvs = add_pv_tvs (add_pv_tvs Mid.empty pvf) pva;
e_regs = add_pv_regs (add_pv_regs Mid.empty pvf) pva; }
let ts_dummy = create_tysymbol (id_fresh "arrow_dummy") [] None
let ty_dummy = ty_app ts_dummy []
e_tvs = add_pv_tvs (add_pa_tvs Mid.empty pa) pv;
e_regs = add_pv_regs (add_pa_regs Mid.empty pa) pv; }
let create_let_defn id e =
let pv = match e.e_vty with
| VTvalue vtv ->
create_pvsymbol id vtv
| VTarrow vta ->
{ pv_vs = create_vsymbol id ty_dummy;
pv_vty = e.e_vty;
pv_tvs = Mid.fold (fun _ -> Stv.union) e.e_tvs vta.vta_tvs;
pv_regs = Mid.fold (fun _ -> Sreg.union) e.e_regs vta.vta_regs; }
let lv = match e.e_vty with
| VTvalue vtv -> LetV (create_pvsymbol id vtv)
| VTarrow vta -> LetA {
pa_name = Ident.id_register id;
pa_vta = vta;
pa_tvs = Mid.fold (fun _ -> Stv.union) e.e_tvs vta.vta_tvs;
pa_regs = Mid.fold (fun _ -> Sreg.union) e.e_regs vta.vta_regs; }
in
{ ld_pv = pv ; ld_expr = e }
{ let_var = lv ; let_expr = e }
exception StaleRegion of region * ident * expr
let e_let ld e =
let { ld_pv = pv ; ld_expr = d } = ld in
let e_let ({ let_var = lv ; let_expr = d } as ld) e =
let eff = d.e_effect in
let tvs = Mid.remove pv.pv_vs.vs_name e.e_tvs in
let regs = Mid.remove pv.pv_vs.vs_name e.e_regs in
let id = match lv with
| LetV pv -> pv.pv_vs.vs_name
| LetA pa -> pa.pa_name
in
let tvs = Mid.remove id e.e_tvs in
let regs = Mid.remove id e.e_regs in
(* If we reset some region in the first expression d, then it may only
pccur in the second expression e in association to pv. Otherwise,
this is a freshness violation: some symbol defined earlier carries
......
......@@ -26,31 +26,31 @@ open Mlw_ty
(** 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. *)
(* pvsymbols represent function arguments and pattern variables *)
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. *)
pv_vs : vsymbol;
pv_vtv : vty_value;
}
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 ValueExpected of pvsymbol
exception ArrowExpected of pvsymbol
(* pasymbols represent higher-order intermediate computation results
introduced by let-expressions. They cannot be type-instantiated. *)
type pasymbol = private {
pa_name : ident;
pa_vta : vty_arrow;
pa_tvs : Stv.t;
pa_regs : Sreg.t;
(* these sets contain pa_vta.vta_tvs/regs together with all type
variables and regions of the defining expression, in order to
cover effects and specification and not overgeneralize *)
}
val vtv_of_pv : pvsymbol -> vty_value
val vta_of_pv : pvsymbol -> vty_arrow
val pa_equal : pasymbol -> pasymbol -> bool
(** program symbols *)
......@@ -103,11 +103,6 @@ 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;
......@@ -120,9 +115,9 @@ type expr = private {
and expr_node = private
| Elogic of term
| Evar of pvsymbol
| Esym of psymbol * ity_subst
| Eapp of pvsymbol * pvsymbol
| Earrow of pasymbol
| Einst of psymbol * ity_subst
| Eapp of pasymbol * pvsymbol
| Elet of let_defn * expr
| Erec of rec_defn list * expr
| Eif of pvsymbol * expr * expr
......@@ -130,13 +125,17 @@ and expr_node = private
| Eany
and let_defn = private {
ld_pv : pvsymbol;
ld_expr : expr;
let_var : let_var;
let_expr : expr;
}
and let_var =
| LetV of pvsymbol
| LetA of pasymbol
and rec_defn = private {
rd_ps : psymbol;
rd_lambda : lambda;
rec_ps : psymbol;
rec_lambda : lambda;
}
and lambda = {
......@@ -148,14 +147,19 @@ and lambda = {
l_xpost : xpost;
}
and variant = {
v_term : term; (* : tau *)
v_rel : lsymbol option; (* tau tau : prop *)
}
val e_label : ?loc:Loc.position -> Slab.t -> expr -> expr
val e_label_add : label -> expr -> expr
val e_label_copy : expr -> expr -> expr
val e_var : pvsymbol -> expr
(* produces Elogic if a value or Evar if an arrow *)
val e_value : pvsymbol -> expr
val e_arrow : pasymbol -> expr
val e_sym : psymbol -> ity_subst -> expr
val e_inst : psymbol -> ity_subst -> expr
(* FIXME? We store the substitution in the expr as given, though it could
be restricted to type variables and regions (both top and subordinate)
of ps_vta.vta_tvs/regs. *)
......@@ -164,7 +168,7 @@ exception GhostWrite of expr * region
exception GhostRaise of expr * xsymbol
(* a ghost expression writes in a non-ghost region or raises an exception *)
val e_app : pvsymbol -> pvsymbol -> expr
val e_app : pasymbol -> pvsymbol -> expr
val create_let_defn : preid -> expr -> let_defn
......
......@@ -43,6 +43,7 @@ open Mlw_decl
type prgsymbol =
| PV of pvsymbol
| PA of pasymbol
| PS of psymbol
| PL of plsymbol
......@@ -68,6 +69,7 @@ let ns_union eq chk =
let prg_equal p1 p2 = match p1,p2 with
| PV p1, PV p2 -> pv_equal p1 p2
| PA p1, PA p2 -> pa_equal p1 p2
| PS p1, PS p2 -> ps_equal p1 p2
| PL p1, PL p2 -> pl_equal p1 p2
| _, _ -> false
......
......@@ -31,6 +31,7 @@ open Mlw_decl
type prgsymbol =
| PV of pvsymbol
| PA of pasymbol
| PS of psymbol
| PL of plsymbol
......
......@@ -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 vty_ghost pv.pv_vty then "?" else "")
fprintf fmt "%s%a" (if pv.pv_vtv.vtv_ghost then "?" else "")
print_vs pv.pv_vs
let forget_pv pv = forget_var pv.pv_vs
......
......@@ -232,7 +232,7 @@ let add_types uc tdl =
| Some id ->
try
let pv = Hashtbl.find projs id.id in
let ty = (vtv_of_pv pv).vtv_ity in
let ty = pv.pv_vtv.vtv_ity in
(* once we have ghost/mutable fields in algebraics,
don't forget to check here that they coincide, too *)
ignore (Loc.try3 id.id_loc ity_match sbs ty ity);
......@@ -319,7 +319,7 @@ let add_types uc tdl =
| Some id ->
try
let pv = Hashtbl.find projs id.id in
let ty = (vtv_of_pv pv).vtv_ity in
let ty = pv.pv_vtv.vtv_ity in
(* once we have ghost/mutable fields in algebraics,
don't forget to check here that they coincide, too *)
Loc.try2 id.id_loc ity_equal_check ty ity;
......@@ -353,7 +353,7 @@ let add_types uc tdl =
option_apply false check ts.its_def
in
let check (pv,_) =
let vtv = vtv_of_pv pv in
let vtv = pv.pv_vtv in
vtv.vtv_ghost || vtv.vtv_mut <> None || check vtv.vtv_ity in
let is_impure_data (ts,csl) =
is_impure_type ts ||
......
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