Skip to content

GitLab

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

whyml: remove vty_value type, work directly with ity

parent 4aee41ca
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 188 additions and 268 deletions
examples/use_api/use_api.ml
View file @ 2d0fb535
......@@ -259,8 +259,7 @@ let unit_type = Ty.ty_tuple []
*)
let d =
let args =
[Mlw_ty.create_pvsymbol
(Ident.id_fresh "_dummy") (Mlw_ty.vty_value Mlw_ty.ity_unit)]
[Mlw_ty.create_pvsymbol (Ident.id_fresh "_dummy") Mlw_ty.ity_unit]
in
let result = Term.create_vsymbol (Ident.id_fresh "result") unit_type in
let spec = {
......@@ -337,8 +336,7 @@ let get_fun : Mlw_expr.psymbol =
let d2 =
let args =
[Mlw_ty.create_pvsymbol
(Ident.id_fresh "_dummy") (Mlw_ty.vty_value Mlw_ty.ity_unit)]
[Mlw_ty.create_pvsymbol (Ident.id_fresh "_dummy") Mlw_ty.ity_unit]
in
let result = Term.create_vsymbol (Ident.id_fresh "result") Ty.ty_int in
let spec = {
......@@ -356,14 +354,11 @@ let d2 =
(* recall that "ref" has type "(v:'a) -> ref 'a". We need to build an
instance of it *)
(* we first built a dummy effective parameter v of type int *)
let pv =
Mlw_ty.create_pvsymbol
(Ident.id_fresh "v") (Mlw_ty.vty_value Mlw_ty.ity_int)
in
let pv = Mlw_ty.create_pvsymbol (Ident.id_fresh "v") Mlw_ty.ity_int in
(* we build "ref int" with a *fresh* region *)
let ity = Mlw_ty.ity_app_fresh ref_type [Mlw_ty.ity_int] in
(* we build the type "(v:int) -> ref <fresh region> int)" *)
let vta = Mlw_ty.vty_arrow [pv] (Mlw_ty.VTvalue (Mlw_ty.vty_value ity)) in
let vta = Mlw_ty.vty_arrow [pv] (Mlw_ty.VTvalue ity) in
(* e1 : the appropriate instance of "ref" *)
let e1 = Mlw_expr.e_arrow ref_fun vta in
(* we apply it to 0 *)
......@@ -381,10 +376,7 @@ let d2 =
let bang_x =
(* recall that "!" as type "ref 'a -> 'a" *)
(* we build a dummy parameter r of the same type as x *)
let vta =
Mlw_ty.vty_arrow [var_x]
(Mlw_ty.VTvalue (Mlw_ty.vty_value Mlw_ty.ity_int))
in
let vta = Mlw_ty.vty_arrow [var_x] (Mlw_ty.VTvalue Mlw_ty.ity_int) in
let e1 = Mlw_expr.e_arrow get_fun vta in
Mlw_expr.e_app e1 [Mlw_expr.e_value var_x]
in
......
src/jessie/ACSLtoWhy3.ml
View file @ 2d0fb535
......@@ -194,28 +194,21 @@ let any _ty =
let mk_ref ty =
let pv =
Mlw_ty.create_pvsymbol (Ident.id_fresh "a") (Mlw_ty.vty_value ty)
in
let pv = Mlw_ty.create_pvsymbol (Ident.id_fresh "a") ty in
let ity = Mlw_ty.ity_app_fresh ref_type [ty] in
let vta = Mlw_ty.vty_arrow [pv] (Mlw_ty.VTvalue (Mlw_ty.vty_value ity)) in
let vta = Mlw_ty.vty_arrow [pv] (Mlw_ty.VTvalue ity) in
Mlw_expr.e_arrow ref_fun vta
let mk_get ref_ty ty =
let pv = Mlw_ty.create_pvsymbol (Ident.id_fresh "r") ref_ty in
let vta = Mlw_ty.vty_arrow [pv] (Mlw_ty.VTvalue (Mlw_ty.vty_value ty)) in
let vta = Mlw_ty.vty_arrow [pv] (Mlw_ty.VTvalue ty) in
Mlw_expr.e_arrow get_fun vta
let mk_set ref_ty ty =
(* (:=) has type (r:ref 'a) (v:'a) unit *)
let pv1 = Mlw_ty.create_pvsymbol (Ident.id_fresh "r") ref_ty in
let pv2 =
Mlw_ty.create_pvsymbol (Ident.id_fresh "v") (Mlw_ty.vty_value ty)
in
let vta =
Mlw_ty.vty_arrow [pv1;pv2]
(Mlw_ty.VTvalue (Mlw_ty.vty_value Mlw_ty.ity_unit))
in
let pv2 = Mlw_ty.create_pvsymbol (Ident.id_fresh "v") ty in
let vta = Mlw_ty.vty_arrow [pv1;pv2] (Mlw_ty.VTvalue Mlw_ty.ity_unit) in
Mlw_expr.e_arrow set_fun vta
......@@ -613,7 +606,7 @@ let lval (host,offset) =
if is_mutable then
begin try
Mlw_expr.e_app
(mk_get v.Mlw_ty.pv_vtv ty)
(mk_get v.Mlw_ty.pv_ity ty)
[Mlw_expr.e_value v]
with e ->
Self.fatal "Exception raised during application of !@ %a@."
......@@ -735,7 +728,7 @@ let assignment (lhost,offset) e _loc =
let v,is_mutable,ty = get_var v in
if is_mutable then
Mlw_expr.e_app
(mk_set v.Mlw_ty.pv_vtv ty)
(mk_set v.Mlw_ty.pv_ity ty)
[Mlw_expr.e_value v; expr e]
else
Self.not_yet_implemented "mutation of formal parameters"
......@@ -796,8 +789,7 @@ let rec stmt s =
let annots = Annotations.code_annot s in
let inv, var = loop_annot annots in
let v =
Mlw_ty.create_pvsymbol (Ident.id_fresh "_dummy")
(Mlw_ty.vty_value Mlw_ty.ity_unit)
Mlw_ty.create_pvsymbol (Ident.id_fresh "_dummy") Mlw_ty.ity_unit
in
Mlw_expr.e_try
(Mlw_expr.e_loop inv var (block body))
......@@ -879,16 +871,12 @@ let fundecl fdec =
let args =
match Kernel_function.get_formals kf with
| [] ->
[ Mlw_ty.create_pvsymbol
(Ident.id_fresh "_dummy")
(Mlw_ty.vty_value Mlw_ty.ity_unit) ]
[ Mlw_ty.create_pvsymbol (Ident.id_fresh "_dummy") Mlw_ty.ity_unit ]
| l ->
List.map (fun v ->
let ity = ctype v.vtype in
let vs =
Mlw_ty.create_pvsymbol
(Ident.id_fresh v.vname)
(Mlw_ty.vty_value ity)
Mlw_ty.create_pvsymbol (Ident.id_fresh v.vname) ity
in
Hashtbl.add program_vars v.vid (vs,false,ity);
vs)
......
src/whyml/mlw_decl.ml
View file @ 2d0fb535
......@@ -84,18 +84,18 @@ let rec syms_type_c s tyc =
syms_type_v s tyc.c_result
and syms_type_v s = function
| SpecV vtv -> syms_ity s vtv.vtv_ity
| SpecV ity -> syms_ity s ity
| SpecA (pvl,tyc) ->
let add_pv s pv = syms_ity s pv.pv_vtv.vtv_ity in
let add_pv s pv = syms_ity s pv.pv_ity in
List.fold_left add_pv (syms_type_c s tyc) pvl
let rec syms_vta s a =
let s = syms_ity s a.vta_arg.vtv_ity in
let s = syms_ity s a.vta_arg in
let s = syms_effect s a.vta_effect in
syms_vty s a.vta_result
and syms_vty s = function
| VTvalue vtv -> syms_ity s vtv.vtv_ity
| VTvalue ity -> syms_ity s ity
| VTarrow vta -> syms_vta s vta
let syms_expr s _e = s (* TODO *)
......@@ -199,7 +199,7 @@ let check_vars vars =
raise (UnboundTypeVar (Stv.choose vars.vars_tv))
let letvar_news = function
| LetV pv -> check_vars pv.pv_vars; Sid.singleton pv.pv_vs.vs_name
| LetV pv -> check_vars pv.pv_ity.ity_vars; Sid.singleton pv.pv_vs.vs_name
| LetA ps -> check_vars ps.ps_vars; Sid.singleton ps.ps_name
let new_regs old_vars news vars =
......@@ -214,7 +214,7 @@ let create_let_decl ld =
let news = letvar_news ld.let_sym in
let news = match ld.let_sym with
| LetA ps -> new_regs vars news ps.ps_vars
| LetV pv -> new_regs vars news pv.pv_vars in
| LetV pv -> new_regs vars news pv.pv_ity.ity_vars in
let syms = Mid.map (fun _ -> ()) ld.let_expr.e_varm in
(*
let syms = syms_varmap Sid.empty ld.let_expr.e_vars in
......@@ -247,7 +247,7 @@ let create_rec_decl fdl =
let create_val_decl lv =
let news = letvar_news lv in
let news, syms = match lv with
| LetV pv -> new_regs vars_empty news pv.pv_vars, Sid.empty
| LetV pv -> new_regs vars_empty news pv.pv_ity.ity_vars, Sid.empty
| LetA ps -> news, Mid.map (fun _ -> ()) ps.ps_varm in
(*
let syms = syms_type_v Sid.empty vd.val_spec in
......@@ -330,8 +330,8 @@ let find_invariant kn its =
let check_match lkn _kn d =
let rec checkE () e = match e.e_node with
| Ecase (e1,bl) ->
let typ = ty_of_ity (vtv_of_expr e1).vtv_ity in
let tye = ty_of_ity (vtv_of_expr e).vtv_ity in
let typ = ty_of_ity (ity_of_expr e1) in
let tye = ty_of_ity (ity_of_expr e) in
let t_p = t_var (create_vsymbol (id_fresh "x") typ) in
let t_e = t_var (create_vsymbol (id_fresh "y") tye) in
let bl = List.map (fun (pp,_) -> [pp.ppat_pattern], t_e) bl in
......@@ -395,7 +395,7 @@ let check_ghost lkn kn d =
let pvs = List.fold_right Spv.add vta.vta_args pvs in
let test pv =
if pv.pv_ghost then () else
access eff.eff_ghostw pv.pv_vtv.vtv_ity
access eff.eff_ghostw pv.pv_ity
in
Spv.iter test pvs;
match vta.vta_result with
......
src/whyml/mlw_dty.ml
View file @ 2d0fb535
......@@ -196,9 +196,9 @@ let unify d1 d2 = unify ~weak:false d1 d2
type dvty = dity list * dity (* A -> B -> C == ([A;B],C) *)
let vty_of_dvty (argl,res) =
let vtv = VTvalue (vty_value (ity_of_dity res)) in
let conv a = create_pvsymbol (id_fresh "x") (vty_value (ity_of_dity a)) in
if argl = [] then vtv else VTarrow (vty_arrow (List.map conv argl) vtv)
let vty = VTvalue (ity_of_dity res) in
let conv a = create_pvsymbol (id_fresh "x") (ity_of_dity a) in
if argl = [] then vty else VTarrow (vty_arrow (List.map conv argl) vty)
type tvars = dity list
......@@ -274,25 +274,21 @@ and dreg_of_reg htv hreg vars r =
Hreg.add hreg r dreg;
dreg
let dity_of_vtv htv hreg vars v = dity_of_ity htv hreg vars v.vtv_ity
let specialize_vtvalue vtv =
let specialize_ity ity =
let htv = Htv.create 3 and hreg = Hreg.create 3 in
dity_of_vtv htv hreg vtv.vtv_ity.ity_vars vtv
dity_of_ity htv hreg ity.ity_vars ity
let specialize_pvsymbol pv =
specialize_vtvalue pv.pv_vtv
let specialize_pvsymbol pv = specialize_ity pv.pv_ity
let specialize_xsymbol xs =
specialize_vtvalue (vty_value xs.xs_ity)
let specialize_xsymbol xs = specialize_ity xs.xs_ity
let specialize_vtarrow vars vta =
let htv = Htv.create 3 and hreg = Hreg.create 3 in
let conv pv = dity_of_vtv htv hreg vars pv.pv_vtv in
let conv pv = dity_of_ity htv hreg vars pv.pv_ity in
let rec specialize a =
let argl = List.map conv a.vta_args in
let narg,res = match a.vta_result with
| VTvalue v -> [], dity_of_vtv htv hreg vars v
| VTvalue v -> [], dity_of_ity htv hreg vars v
| VTarrow a -> specialize a
in
argl @ narg, res
......
src/whyml/mlw_expr.ml
View file @ 2d0fb535
This diff is collapsed.
src/whyml/mlw_expr.mli
View file @ 2d0fb535
......@@ -61,7 +61,7 @@ val pl_clone : Theory.symbol_map -> symbol_map
type ppattern = private {
ppat_pattern : pattern;
ppat_vtv : vty_value;
ppat_ity : ity;
ppat_ghost : bool;
ppat_effect : effect;
}
......@@ -75,7 +75,7 @@ type pre_ppattern =
| PPas of pre_ppattern * preid
val make_ppattern :
pre_ppattern -> ?ghost:bool -> vty_value -> pvsymbol Mstr.t * ppattern
pre_ppattern -> ?ghost:bool -> ity -> pvsymbol Mstr.t * ppattern
(** program symbols *)
......@@ -194,7 +194,7 @@ val e_arrow : psymbol -> vty_arrow -> expr
exception ValueExpected of expr
exception ArrowExpected of expr
val vtv_of_expr : expr -> vty_value
val ity_of_expr : expr -> ity
val vta_of_expr : expr -> vty_arrow
exception GhostWrite of expr * region
......
src/whyml/mlw_module.ml
View file @ 2d0fb535
......@@ -416,10 +416,9 @@ let clone_export uc m inst =
let nr = create_region (id_clone r.reg_name) (conv_ity r.reg_ity) in
Hreg.replace regh r nr;
nr in
let conv_vtv v = vty_value (conv_ity v.vtv_ity) in
let conv_pv pv =
create_pvsymbol (id_clone pv.pv_vs.vs_name)
~ghost:pv.pv_ghost (conv_vtv pv.pv_vtv) in
~ghost:pv.pv_ghost (conv_ity pv.pv_ity) in
let psh = Hid.create 3 in
let conv_xs xs = try match Hid.find psh xs.xs_name with
| XS xs -> xs | _ -> assert false with Not_found -> xs in
......@@ -455,7 +454,7 @@ let clone_export uc m inst =
let spec = conv_spec mv a.vta_spec in
let vty = match a.vta_result with
| VTarrow a -> VTarrow (conv_vta mv a)
| VTvalue v -> VTvalue (conv_vtv v) in
| VTvalue v -> VTvalue (conv_ity v) in
vty_arrow args ~spec vty in
let mvs = ref (Mvs.singleton Mlw_wp.pv_old.pv_vs Mlw_wp.pv_old.pv_vs) in
let add_pdecl uc d = { uc with
......
src/whyml/mlw_ocaml.ml
View file @ 2d0fb535
......@@ -664,20 +664,18 @@ let rec print_ity_node inn info fmt ity = match ity.ity_node with
let print_ity info = print_ity_node false info
let print_vtv info fmt vtv = print_ity info fmt vtv.vtv_ity
let print_pvty info fmt pv =
if pv.pv_ghost then fprintf fmt "((* ghost *))" else
fprintf fmt "@[(%a:@ %a)@]"
(print_lident info) pv.pv_vs.vs_name (print_vtv info) pv.pv_vtv
(print_lident info) pv.pv_vs.vs_name (print_ity info) pv.pv_ity
let rec print_vta info fmt vta =
let print_arg fmt pv = print_vtv info fmt pv.pv_vtv in
let print_arg fmt pv = print_ity info fmt pv.pv_ity in
fprintf fmt "(%a -> %a)" (print_list arrow print_arg) vta.vta_args
(print_vty info) vta.vta_result
and print_vty info fmt = function
| VTvalue vtv -> print_vtv info fmt vtv
| VTvalue ity -> print_ity info fmt ity
| VTarrow vta -> print_vta info fmt vta
let is_letrec = function
......@@ -705,11 +703,11 @@ and print_lexpr pri info fmt e =
| Elet ({ let_expr = e1 }, e2) when e1.e_ghost ->
print_expr info fmt e2
| Elet ({ let_sym = LetV pv }, e2)
when ity_equal pv.pv_vtv.vtv_ity ity_mark ->
when ity_equal pv.pv_ity ity_mark ->
print_expr info fmt e2
| Elet ({ let_sym = LetV pv ; let_expr = e1 }, e2)
when pv.pv_vs.vs_name.id_string = "_" &&
ity_equal pv.pv_vtv.vtv_ity ity_unit ->
ity_equal pv.pv_ity ity_unit ->
fprintf fmt (protect_on (pri > 0) "@[begin %a;@ %a end@]")
(print_expr info) e1 (print_expr info) e2;
| Elet ({ let_sym = lv ; let_expr = e1 }, e2) ->
......@@ -835,19 +833,19 @@ let rec extract_vta_args args vta =
let new_args = List.map (fun pv -> pv.pv_vs) vta.vta_args in
let args = List.rev_append new_args args in
match vta.vta_result with
| VTvalue vtv -> List.rev args, vtv
| VTvalue ity -> List.rev args, ity
| VTarrow vta -> extract_vta_args args vta
let extract_lv_args = function
| LetV pv -> [], pv.pv_vtv
| LetV pv -> [], pv.pv_ity
| LetA ps -> extract_vta_args [] ps.ps_vta
let print_val_decl info fmt lv =
let vars, vtv = extract_lv_args lv in
let vars, ity = extract_lv_args lv in
fprintf fmt "@[<hov 2>let %a %a : %a =@ %a@]"
(print_lv info) lv
(print_list space (print_vs_arg info)) vars
(print_vtv info) vtv
(print_ity info) ity
to_be_implemented "val";
forget_vars vars;
forget_tvs ()
......
src/whyml/mlw_pretty.ml
View file @ 2d0fb535
......@@ -124,20 +124,17 @@ let print_effect fmt eff =
Sexn.iter (print_xs "ghost raise") eff.eff_ghostx;
Mreg.iter print_reset eff.eff_resets
let print_vtv fmt vtv =
fprintf fmt "%a" print_ity vtv.vtv_ity
let rec print_vta fmt vta =
let print_arg fmt pv = fprintf fmt "%a ->@ " print_vtv pv.pv_vtv in
let print_arg fmt pv = fprintf fmt "%a ->@ " print_ity pv.pv_ity in
fprintf fmt "%a%a%a" (print_list nothing print_arg) vta.vta_args
print_effect vta.vta_spec.c_effect print_vty vta.vta_result
and print_vty fmt = function
| VTarrow vta -> print_vta fmt vta
| VTvalue vtv -> print_vtv fmt vtv
| VTvalue ity -> print_ity fmt ity
let print_pvty fmt pv = fprintf fmt "@[%a:@,%a@]"
print_pv pv print_vtv pv.pv_vtv
print_pv pv print_ity pv.pv_ity
let print_psty fmt ps =
let print_tvs fmt tvs = if not (Stv.is_empty tvs) then
......@@ -167,7 +164,7 @@ let forget_lv = function
| LetA ps -> forget_ps ps
let rec print_type_v fmt = function
| VTvalue vtv -> print_vtv fmt vtv
| VTvalue ity -> print_ity fmt ity
| VTarrow vta ->
let print_arg fmt pv = fprintf fmt "@[(%a)@] ->@ " print_pvty pv in
fprintf fmt "%a%a"
......@@ -271,7 +268,7 @@ and print_enode pri fmt e = match e.e_node with
fprintf fmt "(%a@ %a)" (print_lexpr pri) e print_pv v
| Elet ({ let_sym = LetV pv ; let_expr = e1 }, e2)
when pv.pv_vs.vs_name.id_string = "_" &&
ity_equal pv.pv_vtv.vtv_ity ity_unit ->
ity_equal pv.pv_ity ity_unit ->
fprintf fmt (protect_on (pri > 0) "%a;@\n%a")
print_expr e1 print_expr e2;
| Elet ({ let_sym = lv ; let_expr = e1 }, e2) ->
......@@ -398,7 +395,7 @@ let print_data_decl fst fmt (ts,csl,inv) =
let print_val_decl fmt lv =
let vty = match lv with
| LetV pv -> VTvalue pv.pv_vtv | LetA ps -> VTarrow ps.ps_vta in
| LetV pv -> VTvalue pv.pv_ity | LetA ps -> VTarrow ps.ps_vta in
fprintf fmt "@[<hov 2>val (%a) :@ %a@]" print_lv lv print_type_v vty;
(* FIXME: forget only generalized regions *)
match lv with LetA _ -> forget_tvs_regs () | _ -> ()
......
src/whyml/mlw_pretty.mli
View file @ 2d0fb535
......@@ -29,7 +29,6 @@ val print_reg : formatter -> region -> unit (* region *)
val print_its : formatter -> itysymbol -> unit (* type symbol *)
val print_ity : formatter -> ity -> unit (* individual type *)
val print_vtv : formatter -> vty_value -> unit (* value type *)
val print_vta : formatter -> vty_arrow -> unit (* arrow type *)
val print_vty : formatter -> vty -> unit (* expression type *)
......
src/whyml/mlw_ty.ml
View file @ 2d0fb535
......@@ -786,19 +786,10 @@ let spec_check c ty =
(** program variables *)
type vty_value = {
vtv_ity : ity;
}
let vty_value ity = { vtv_ity = ity; }
let vtv_vars vtv = vtv.vtv_ity.ity_vars
type pvsymbol = {
pv_vs : vsymbol;
pv_vtv : vty_value;
pv_ity : ity;
pv_ghost : bool;
pv_vars : varset;
}
module PVsym = MakeMSHW (struct
......@@ -813,17 +804,16 @@ module Wpv = PVsym.W
let pv_equal : pvsymbol -> pvsymbol -> bool = (==)
let create_pvsymbol id ghost vtv = {
pv_vs = create_vsymbol id (ty_of_ity vtv.vtv_ity);
pv_vtv = vtv;
let create_pvsymbol id ghost ity = {
pv_vs = create_vsymbol id (ty_of_ity ity);
pv_ity = ity;
pv_ghost = ghost;
pv_vars = vtv_vars vtv;
}
let create_pvsymbol, restore_pv, restore_pv_by_id =
let id_to_pv = Wid.create 17 in
(fun id ?(ghost=false) vtv ->
let pv = create_pvsymbol id ghost vtv in
(fun id ?(ghost=false) ity ->
let pv = create_pvsymbol id ghost ity in
Wid.set id_to_pv pv.pv_vs.vs_name pv;
pv),
(fun vs -> Wid.find id_to_pv vs.vs_name),
......@@ -832,7 +822,7 @@ let create_pvsymbol, restore_pv, restore_pv_by_id =
(** program types *)
type vty =
| VTvalue of vty_value
| VTvalue of ity
| VTarrow of vty_arrow
and vty_arrow = {
......@@ -842,19 +832,19 @@ and vty_arrow = {
}
let rec vta_vars vta =
let add_arg vars pv = vars_union vars pv.pv_vars in
let add_arg vars pv = vars_union vars pv.pv_ity.ity_vars in
List.fold_left add_arg (vty_vars vta.vta_result) vta.vta_args
and vty_vars = function
| VTvalue vtv -> vtv_vars vtv
| VTvalue ity -> ity.ity_vars
| VTarrow vta -> vta_vars vta
let ity_of_vty = function
| VTvalue vtv -> vtv.vtv_ity
| VTvalue ity -> ity
| VTarrow _ -> ity_unit
let ty_of_vty = function
| VTvalue vtv -> ty_of_ity vtv.vtv_ity
| VTvalue ity -> ty_of_ity ity
| VTarrow _ -> ty_unit
let spec_check spec vty = spec_check spec (ty_of_vty vty)
......@@ -884,27 +874,25 @@ let vty_arrow argl ?spec vty =
in .vta_vars are matched. The caller should supply a "freezing"
substitution that covers all external type variables and regions. *)
let rec vta_vars_match s a1 a2 =
let vtv_match s v1 v2 = ity_match s v1.vtv_ity v2.vtv_ity in
let rec match_args s l1 l2 = match l1, l2 with
| [],[] -> s, a1.vta_result, a2.vta_result
| [], _ -> s, a1.vta_result, VTarrow { a2 with vta_args = l2 }
| _, [] -> s, VTarrow { a1 with vta_args = l1 }, a2.vta_result
| {pv_vtv = v1}::l1, {pv_vtv = v2}::l2 ->
match_args (vtv_match s v1 v2) l1 l2
| {pv_ity = v1}::l1, {pv_ity = v2}::l2 ->
match_args (ity_match s v1 v2) l1 l2
in
let s, vty1, vty2 = match_args s a1.vta_args a2.vta_args in
match vty1, vty2 with
| VTarrow a1, VTarrow a2 -> vta_vars_match s a1 a2
| VTvalue v1, VTvalue v2 -> vtv_match s v1 v2
| VTvalue v1, VTvalue v2 -> ity_match s v1 v2
| _ -> invalid_arg "Mlw_ty.vta_vars_match"
(* the substitution must cover not only vta.vta_tvs and vta.vta_regs
but also every type variable and every region in vta_spec *)
let vta_full_inst sbs vta =
let tvm = Mtv.map ty_of_ity sbs.ity_subst_tv in
let vtv_inst { vtv_ity = ity } = vty_value (ity_full_inst sbs ity) in
let pv_inst { pv_vs = vs; pv_vtv = vtv; pv_ghost = ghost } =
create_pvsymbol (id_clone vs.vs_name) ~ghost (vtv_inst vtv) in
let pv_inst { pv_vs = vs; pv_ity = ity; pv_ghost = ghost } =
create_pvsymbol (id_clone vs.vs_name) ~ghost (ity_full_inst sbs ity) in
let add_arg vsm pv =
let nv = pv_inst pv in
Mvs.add pv.pv_vs (t_var nv.pv_vs) vsm, nv in
......@@ -913,7 +901,7 @@ let vta_full_inst sbs vta =
let spec = spec_full_inst sbs tvm vsm vta.vta_spec in
let vty = match vta.vta_result with
| VTarrow vta -> VTarrow (vta_inst vsm vta)
| VTvalue vtv -> VTvalue (vtv_inst vtv) in
| VTvalue ity -> VTvalue (ity_full_inst sbs ity) in
vty_arrow_unsafe args spec vty
in
vta_inst Mvs.empty vta
......@@ -921,8 +909,8 @@ let vta_full_inst sbs vta =
(* remove from the given arrow every effect that is covered
neither by the arrow's vta_vars nor by the given varmap *)
let rec vta_filter varm vars vta =
let add_m pv m = Mid.add pv.pv_vs.vs_name pv.pv_vars m in
let add_s pv s = vars_union pv.pv_vars s in
let add_m pv m = Mid.add pv.pv_vs.vs_name pv.pv_ity.ity_vars m in
let add_s pv s = vars_union pv.pv_ity.ity_vars s in
let varm = List.fold_right add_m vta.vta_args varm in
let vars = List.fold_right add_s vta.vta_args vars in
let vty = match vta.vta_result with
......@@ -942,7 +930,7 @@ let rec vta_filter varm vars vta =
let spec = match vta.vta_result with
| VTvalue v ->
let on_reg r e = if reg_occurs r vars then e else eff_reset e r in
let eff = reg_fold on_reg v.vtv_ity.ity_vars spec.c_effect in
let eff = reg_fold on_reg v.ity_vars spec.c_effect in
{ spec with c_effect = eff }
| VTarrow _ -> spec in
vty_arrow_unsafe vta.vta_args spec vty
......@@ -951,10 +939,9 @@ let vta_filter varm vta =
vta_filter varm (vars_merge varm vars_empty) vta
let vta_app vta pv =
let vtv = pv.pv_vtv in
let arg, rest = match vta.vta_args with
| arg::rest -> arg,rest | _ -> assert false in
ity_equal_check arg.pv_vtv.vtv_ity vtv.vtv_ity;
ity_equal_check arg.pv_ity pv.pv_ity;
let sbs = Mvs.singleton arg.pv_vs (t_var pv.pv_vs) in
let rec vty_subst = function
| VTarrow a when not (List.exists (pv_equal arg) a.vta_args) ->
......@@ -967,5 +954,7 @@ let vta_app vta pv =
if not pv.pv_ghost && arg.pv_ghost then
Loc.errorm "non-ghost value passed as a ghost argument";
let ghost = pv.pv_ghost && not arg.pv_ghost in
if rest = [] then spec, ghost, result
else spec_empty ty_unit, ghost, VTarrow (vty_arrow_unsafe rest spec result)
if rest = [] then
spec, ghost, result
else
spec_empty ty_unit, ghost, VTarrow (vty_arrow_unsafe rest spec result)
src/whyml/mlw_ty.mli
View file @ 2d0fb535
......@@ -254,17 +254,10 @@ type spec = {
(** program variables *)
type vty_value = private {
vtv_ity : ity;
}
val vty_value : ity -> vty_value
type pvsymbol = private {
pv_vs : vsymbol;
pv_vtv : vty_value;
pv_ity : ity;
pv_ghost : bool;
pv_vars : varset;
}
module Mpv : Extmap.S with type key = pvsymbol
......@@ -274,7 +267,7 @@ module Wpv : Weakhtbl.S with type key = pvsymbol
val pv_equal : pvsymbol -> pvsymbol -> bool
val create_pvsymbol : preid -> ?ghost:bool -> vty_value -> pvsymbol
val create_pvsymbol : preid -> ?ghost:bool -> ity -> pvsymbol
val restore_pv : vsymbol -> pvsymbol
(* raises Not_found if the argument is not a pv_vs *)
......@@ -285,7 +278,7 @@ val restore_pv_by_id : ident -> pvsymbol
(** program types *)
type vty =
| VTvalue of vty_value
| VTvalue of ity
| VTarrow of vty_arrow
and vty_arrow = private {
......
src/whyml/mlw_typing.ml
View file @ 2d0fb535
......@@ -886,7 +886,7 @@ let env_invariant lenv eff pvs =
let lkn = Theory.get_known (get_theory lenv.mod_uc) in
let regs = Sreg.union eff.eff_writes eff.eff_ghostw in
let add_pv pv (pinv,qinv) =
let ity = pv.pv_vtv.vtv_ity in
let ity = pv.pv_ity in
let written r = reg_occurs r ity.ity_vars in
let inv = Mlw_wp.full_invariant lkn kn pv.pv_vs ity in
let qinv = (* we reprove invariants for modified non-reset variables *)
......@@ -918,12 +918,12 @@ let post_invariant lenv rvs inv ity q =
Mlw_ty.create_post vs q
let ity_or_unit = function
| VTvalue v -> v.vtv_ity
| VTvalue v -> v
| VTarrow _ -> ity_unit
let reset_vars eff pvs =
let add pv s =
if eff_stale_region eff pv.pv_vtv.vtv_ity.ity_vars
if eff_stale_region eff pv.pv_ity.ity_vars
then Svs.add pv.pv_vs s else s in
if Mreg.is_empty eff.eff_resets then Svs.empty else
Spv.fold add pvs Svs.empty
......@@ -1025,8 +1025,7 @@ let add_local x lv lenv = match lv with
let binders bl =
let binder (id, ghost, dity) =
let vtv = vty_value (ity_of_dity dity) in
create_pvsymbol (Denv.create_user_id id) ~ghost vtv in
create_pvsymbol (Denv.create_user_id id) ~ghost (ity_of_dity dity) in
List.map binder bl
let add_binders lenv pvl =
......@@ -1034,7 +1033,7 @@ let add_binders lenv pvl =
List.fold_left add lenv pvl
let mk_field ity gh mut = { fd_ity = ity; fd_ghost = gh; fd_mut = mut }
let fd_of_pv pv = mk_field pv.pv_vtv.vtv_ity pv.pv_ghost None
let fd_of_pv pv = mk_field pv.pv_ity pv.pv_ghost None
(* TODO: devise a good grammar for effect expressions *)
let rec get_eff_expr lenv { pp_desc = d; pp_loc = loc } = match d with
......@@ -1159,7 +1158,7 @@ let rec type_c lenv pvs vars (dtyv, dsp) =
let eff = match vty with
| VTvalue v ->
let on_reg r e = if reg_occurs r vars then e else eff_reset e r in
reg_fold on_reg v.vtv_ity.ity_vars eff
reg_fold on_reg v.ity_vars eff
| VTarrow _ -> eff in
(* refresh every unmodified subregion of a modified region *)
let writes = Sreg.union eff.eff_writes eff.eff_ghostw in
......@@ -1189,11 +1188,11 @@ let rec type_c lenv pvs vars (dtyv, dsp) =
and type_v lenv pvs vars = function
| DSpecV v ->
VTvalue (vty_value (ity_of_dity v))
VTvalue (ity_of_dity v)
<