diff --git a/src/whyml/mlw_decl.ml b/src/whyml/mlw_decl.ml
index 5f57f674af8eefc99f9a23464cec70e8b8427cd8..5e53511d9827da6611497313662ffbafa12aaf51 100644
--- a/src/whyml/mlw_decl.ml
+++ b/src/whyml/mlw_decl.ml
@@ -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
diff --git a/src/whyml/mlw_expr.ml b/src/whyml/mlw_expr.ml
index 4b10299d8241d7e86fe2ab97d790ff3e1dea0249..ff420557058cb93c98eb6a96d2537a8915764057 100644
--- a/src/whyml/mlw_expr.ml
+++ b/src/whyml/mlw_expr.ml
@@ -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
diff --git a/src/whyml/mlw_expr.mli b/src/whyml/mlw_expr.mli
index c468e226bc2459f90455c5f369238b985d82627d..84336582b5939f8615054cd55a3eb2c282fed638 100644
--- a/src/whyml/mlw_expr.mli
+++ b/src/whyml/mlw_expr.mli
@@ -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
diff --git a/src/whyml/mlw_module.ml b/src/whyml/mlw_module.ml
index e64278127726dbe479223bfd104a2ec5f93ff81d..6c8f3701e631a6ef27b8f65621fbda8509f62632 100644
--- a/src/whyml/mlw_module.ml
+++ b/src/whyml/mlw_module.ml
@@ -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
diff --git a/src/whyml/mlw_module.mli b/src/whyml/mlw_module.mli
index 1983333a9542e87dc5473bde1e0bea26cd8bd461..c6b43f3aa0432e68f396e3768afc02c57f72f88a 100644
--- a/src/whyml/mlw_module.mli
+++ b/src/whyml/mlw_module.mli
@@ -31,6 +31,7 @@ open Mlw_decl
type prgsymbol =
| PV of pvsymbol
+ | PA of pasymbol
| PS of psymbol
| PL of plsymbol
diff --git a/src/whyml/mlw_pretty.ml b/src/whyml/mlw_pretty.ml
index b96a8ad88c091807e5edf5bfb3594d9cadc6c93d..90eb9548ad11b5f84c8372c5b8b4459a2c0c8e3a 100644
--- a/src/whyml/mlw_pretty.ml
+++ b/src/whyml/mlw_pretty.ml
@@ -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
diff --git a/src/whyml/mlw_typing.ml b/src/whyml/mlw_typing.ml
index 5d06b4575a662d6de0df53cb5c936c7f86ef7a24..a6b7164de63bd8a4b91ea11637c2833608569947 100644
--- a/src/whyml/mlw_typing.ml
+++ b/src/whyml/mlw_typing.ml
@@ -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 ||