Commit 0e35697f authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: rename vty_arrow to aty

Now, there are three kinds of types used in WhyML API:
  ity -- the type of first-order values, "i" stands for "individual"
  aty -- the type of higher-order values, "a" stands for "arrow"
  vty -- the sum of the previous two, "v" stands for "value"

We should probably rename the VTvalue constructor, since it carries
an ity, and not a vty. And I would gladly rename ity to something
more appropriate, too.
parent 2d0fb535
......@@ -358,9 +358,9 @@ let d2 =
(* 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 ity) in
let aty = 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
let e1 = Mlw_expr.e_arrow ref_fun aty in
(* we apply it to 0 *)
let c0 = Mlw_expr.e_const (Number.ConstInt (Number.int_const_dec "0")) in
Mlw_expr.e_app e1 [c0]
......@@ -376,8 +376,8 @@ 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.ity_int) in
let e1 = Mlw_expr.e_arrow get_fun vta in
let aty = Mlw_ty.vty_arrow [var_x] (Mlw_ty.VTvalue Mlw_ty.ity_int) in
let e1 = Mlw_expr.e_arrow get_fun aty in
Mlw_expr.e_app e1 [Mlw_expr.e_value var_x]
in
(* the complete body *)
......
......@@ -196,20 +196,20 @@ let any _ty =
let mk_ref ty =
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 ity) in
Mlw_expr.e_arrow ref_fun vta
let aty = Mlw_ty.vty_arrow [pv] (Mlw_ty.VTvalue ity) in
Mlw_expr.e_arrow ref_fun aty
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 ty) in
Mlw_expr.e_arrow get_fun vta
let aty = Mlw_ty.vty_arrow [pv] (Mlw_ty.VTvalue ty) in
Mlw_expr.e_arrow get_fun aty
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") 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
let aty = Mlw_ty.vty_arrow [pv1;pv2] (Mlw_ty.VTvalue Mlw_ty.ity_unit) in
Mlw_expr.e_arrow set_fun aty
......
......@@ -89,14 +89,14 @@ and syms_type_v s = function
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 in
let s = syms_effect s a.vta_effect in
syms_vty s a.vta_result
let rec syms_aty s a =
let s = syms_ity s a.aty_arg in
let s = syms_effect s a.aty_effect in
syms_vty s a.aty_result
and syms_vty s = function
| VTvalue ity -> syms_ity s ity
| VTarrow vta -> syms_vta s vta
| VTarrow aty -> syms_aty s aty
let syms_expr s _e = s (* TODO *)
*)
......@@ -232,7 +232,7 @@ let create_rec_decl fdl =
(*
let add_fd syms { rec_ps = ps; rec_lambda = l; rec_vars = vm } =
let syms = syms_varmap syms vm in
let syms = syms_vta syms ps.ps_vta in
let syms = syms_aty syms ps.ps_aty in
let syms = syms_term syms l.l_pre in
let syms = syms_post syms l.l_post in
let syms = syms_xpost syms l.l_xpost in
......@@ -388,23 +388,23 @@ let check_ghost lkn kn d =
if not (Sreg.exists occurs regs) then () else
List.iter check (inst_constructors lkn kn ity)
in
let rec check pvs vta =
let eff = vta.vta_spec.c_effect in
let rec check pvs aty =
let eff = aty.aty_spec.c_effect in
if not (Sexn.is_empty eff.eff_ghostx) then
raise (GhostRaise (e_void, Sexn.choose eff.eff_ghostx));
let pvs = List.fold_right Spv.add vta.vta_args pvs in
let pvs = List.fold_right Spv.add aty.aty_args pvs in
let test pv =
if pv.pv_ghost then () else
access eff.eff_ghostw pv.pv_ity
in
Spv.iter test pvs;
match vta.vta_result with
| VTarrow vta -> check pvs vta
match aty.aty_result with
| VTarrow aty -> check pvs aty
| VTvalue _ -> ()
in
let check ps =
if ps.ps_ghost then () else
check (ps_pvset Spv.empty ps) ps.ps_vta
check (ps_pvset Spv.empty ps) ps.ps_aty
in
match d.pd_node with
| PDrec fdl -> List.iter (fun fd -> check fd.fun_ps) fdl
......
......@@ -282,21 +282,21 @@ let specialize_pvsymbol pv = specialize_ity pv.pv_ity
let specialize_xsymbol xs = specialize_ity xs.xs_ity
let specialize_vtarrow vars vta =
let specialize_arrow vars aty =
let htv = Htv.create 3 and hreg = Hreg.create 3 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
let argl = List.map conv a.aty_args in
let narg,res = match a.aty_result with
| VTvalue v -> [], dity_of_ity htv hreg vars v
| VTarrow a -> specialize a
in
argl @ narg, res
in
specialize vta
specialize aty
let specialize_psymbol ps =
specialize_vtarrow ps.ps_vars ps.ps_vta
specialize_arrow ps.ps_vars ps.ps_aty
let specialize_plsymbol pls =
let htv = Htv.create 3 and hreg = Hreg.create 3 in
......
......@@ -215,7 +215,7 @@ let make_ppattern pp ?(ghost=false) ity =
type psymbol = {
ps_name : ident;
ps_vta : vty_arrow;
ps_aty : aty;
ps_ghost : bool;
ps_varm : varmap;
ps_vars : varset;
......@@ -234,11 +234,11 @@ module Wps = Psym.W
let ps_equal : psymbol -> psymbol -> bool = (==)
let create_psymbol_real ~poly id ghost vta varm =
let vars = if poly then vars_empty else vta_vars vta in
let create_psymbol_real ~poly id ghost aty varm =
let vars = if poly then vars_empty else aty_vars aty in
let vars = vars_merge varm vars in
{ ps_name = id_register id;
ps_vta = vta_filter varm vta;
ps_aty = aty_filter varm aty;
ps_ghost = ghost;
ps_varm = varm;
ps_vars = vars;
......@@ -279,13 +279,13 @@ let spec_pvset pvs spec =
let add_vs vs _ s = Spv.add (restore_pv vs) s in
Mvs.fold add_vs (spec_vsset spec) pvs
let rec vta_varmap vta =
let varm = match vta.vta_result with
| VTarrow a -> vta_varmap a
let rec aty_varmap aty =
let varm = match aty.aty_result with
| VTarrow a -> aty_varmap a
| VTvalue _ -> Mid.empty in
let varm = spec_varmap varm vta.vta_spec in
let varm = spec_varmap varm aty.aty_spec in
let del_pv m pv = Mid.remove pv.pv_vs.vs_name m in
List.fold_left del_pv varm vta.vta_args
List.fold_left del_pv varm aty.aty_args
let eff_check vars result e =
let check vars r = if not (reg_occurs r vars) then
......@@ -300,33 +300,33 @@ let eff_check vars result e =
let reset = reset (vars_union vars (vty_vars result)) in
Mreg.iter reset e.eff_resets
let vtv_check vars eff ity =
let ity_check vars eff ity =
let on_reg r =
if not (reg_occurs r vars) &&
(try Mreg.find r eff.eff_resets <> None with Not_found -> true)
then Loc.errorm "every fresh region in the result must be reset" in
reg_iter on_reg ity.ity_vars
let rec vta_check vars vta =
let rec aty_check vars aty =
let add_arg vars pv = vars_union vars pv.pv_ity.ity_vars in
let vars = List.fold_left add_arg vars vta.vta_args in
eff_check vars vta.vta_result vta.vta_spec.c_effect;
if vta.vta_spec.c_letrec <> 0 then invalid_arg "Mlw_expr.vta_check";
match vta.vta_result with
| VTarrow a -> vta_check vars a
| VTvalue v -> vtv_check vars vta.vta_spec.c_effect v
let create_psymbol id ?(ghost=false) vta =
let ps = create_psymbol_poly id ghost vta (vta_varmap vta) in
vta_check ps.ps_vars vta;
let vars = List.fold_left add_arg vars aty.aty_args in
eff_check vars aty.aty_result aty.aty_spec.c_effect;
if aty.aty_spec.c_letrec <> 0 then invalid_arg "Mlw_expr.aty_check";
match aty.aty_result with
| VTarrow a -> aty_check vars a
| VTvalue v -> ity_check vars aty.aty_spec.c_effect v
let create_psymbol id ?(ghost=false) aty =
let ps = create_psymbol_poly id ghost aty (aty_varmap aty) in
aty_check ps.ps_vars aty;
ps
let create_psymbol_extra id ?(ghost=false) vta pvs pss =
let varm = vta_varmap vta in
let create_psymbol_extra id ?(ghost=false) aty pvs pss =
let varm = aty_varmap aty in
let varm = Spv.fold add_pv_vars pvs varm in
let varm = Sps.fold add_ps_vars pss varm in
let ps = create_psymbol_poly id ghost vta varm in
vta_check ps.ps_vars vta;
let ps = create_psymbol_poly id ghost aty varm in
aty_check ps.ps_vars aty;
ps
(** program expressions *)
......@@ -408,9 +408,9 @@ let ity_of_expr e = match e.e_vty with
| VTvalue ity -> ity
| VTarrow _ -> Loc.error ?loc:e.e_loc (ValueExpected e)
let vta_of_expr e = match e.e_vty with
let aty_of_expr e = match e.e_vty with
| VTvalue _ -> Loc.error ?loc:e.e_loc (ArrowExpected e)
| VTarrow vta -> vta
| VTarrow aty -> aty
let add_e_vars e m = varmap_union e.e_varm m
......@@ -475,17 +475,17 @@ let e_value pv =
let varm = add_pv_vars pv Mid.empty in
mk_expr (Evalue pv) (VTvalue pv.pv_ity) pv.pv_ghost eff_empty varm
let e_arrow ps vta =
let e_arrow ps aty =
let varm = add_ps_vars ps Mid.empty in
let sbs = vta_vars_match ps.ps_subst ps.ps_vta vta in
let vta = vta_full_inst sbs ps.ps_vta in
mk_expr (Earrow ps) (VTarrow vta) ps.ps_ghost eff_empty varm
let sbs = aty_vars_match ps.ps_subst ps.ps_aty aty in
let aty = aty_full_inst sbs ps.ps_aty in
mk_expr (Earrow ps) (VTarrow aty) ps.ps_ghost eff_empty varm
(* let-definitions *)
let create_let_defn id e =
let lv = match e.e_vty with
| VTarrow vta -> LetA (create_psymbol_mono id e.e_ghost vta e.e_varm)
| VTarrow aty -> LetA (create_psymbol_mono id e.e_ghost aty e.e_varm)
| VTvalue ity -> LetV (create_pvsymbol id ~ghost:e.e_ghost ity) in
{ let_sym = lv ; let_expr = e }
......@@ -511,7 +511,7 @@ let on_value fn e = match e.e_node with
(* application *)
let e_app_real e pv =
let spec,ghost,vty = vta_app (vta_of_expr e) pv in
let spec,ghost,vty = aty_app (aty_of_expr e) pv in
let ghost = e.e_ghost || ghost in
let eff = eff_ghostify ghost spec.c_effect in
check_postexpr e eff (add_pv_vars pv Mid.empty);
......@@ -806,9 +806,9 @@ let pv_dummy = create_pvsymbol (id_fresh "dummy") ity_unit
let e_any spec vty =
if spec.c_letrec <> 0 then invalid_arg "Mlw_expr.e_any";
let vta = vty_arrow [pv_dummy] ~spec vty in
let varm = vta_varmap vta in
vta_check (vars_merge varm vars_empty) vta;
let aty = vty_arrow [pv_dummy] ~spec vty in
let varm = aty_varmap aty in
aty_check (vars_merge varm vars_empty) aty;
mk_expr (Eany spec) vty false spec.c_effect varm
let e_abstract e spec =
......@@ -832,8 +832,8 @@ let create_fun_defn id ({l_expr = e} as lam) recsyms =
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 varm_ps = Mid.set_diff varm recsyms in
let vta = vty_arrow lam.l_args ~spec e.e_vty in
{ fun_ps = create_psymbol_poly id e.e_ghost vta varm_ps;
let aty = vty_arrow lam.l_args ~spec e.e_vty in
{ fun_ps = create_psymbol_poly id e.e_ghost aty varm_ps;
fun_lambda = lam;
fun_varm = varm; }
......@@ -841,8 +841,8 @@ let rec_varmap varm fdl =
let fd, rest = match fdl with
| [] -> invalid_arg "Mlw_expr.rec_varm"
| fd :: fdl -> fd, fdl in
let lr = fd.fun_ps.ps_vta.vta_spec.c_letrec in
let bad fd = fd.fun_ps.ps_vta.vta_spec.c_letrec <> lr in
let lr = fd.fun_ps.ps_aty.aty_spec.c_letrec in
let bad fd = fd.fun_ps.ps_aty.aty_spec.c_letrec <> lr in
if List.exists bad rest then invalid_arg "Mlw_expr.rec_varm";
let add_fd m fd = varmap_union fd.fun_varm m in
let del_fd m fd = Mid.remove fd.fun_ps.ps_name m in
......@@ -865,23 +865,23 @@ let eff_equal eff1 eff2 =
Sexn.equal eff1.eff_ghostx eff2.eff_ghostx &&
Mreg.equal (Opt.equal reg_equal) eff1.eff_resets eff2.eff_resets
let rec vta_compat a1 a2 =
assert (List.for_all2 pv_equal a1.vta_args a2.vta_args);
let rec aty_compat a1 a2 =
assert (List.for_all2 pv_equal a1.aty_args a2.aty_args);
(* no need to compare the rest of the spec, see below *)
eff_equal a1.vta_spec.c_effect a2.vta_spec.c_effect &&
match a1.vta_result, a2.vta_result with
| VTarrow a1, VTarrow a2 -> vta_compat a1 a2
eff_equal a1.aty_spec.c_effect a2.aty_spec.c_effect &&
match a1.aty_result, a2.aty_result with
| VTarrow a1, VTarrow a2 -> aty_compat a1 a2
| VTvalue v1, VTvalue v2 -> ity_equal v1 v2
| _,_ -> assert false
let ps_compat ps1 ps2 =
vta_compat ps1.ps_vta ps2.ps_vta &&
aty_compat ps1.ps_aty ps2.ps_aty &&
ps1.ps_ghost = ps2.ps_ghost &&
Mid.equal (fun _ _ -> true) ps1.ps_varm ps2.ps_varm
let rec expr_subst psm e = e_label_copy e (match e.e_node with
| Earrow ps when Mid.mem ps.ps_name psm ->
e_arrow (Mid.find ps.ps_name psm) (vta_of_expr e)
e_arrow (Mid.find ps.ps_name psm) (aty_of_expr e)
| Eapp (e,pv,_) ->
e_app_real (expr_subst psm e) pv
| Elet ({ let_sym = LetV pv ; let_expr = d }, e) ->
......
......@@ -85,13 +85,13 @@ val make_ppattern :
type psymbol = private {
ps_name : ident;
ps_vta : vty_arrow;
ps_aty : aty;
ps_ghost : bool;
ps_varm : varmap;
ps_vars : varset;
(* this varset covers the type variables and regions of the defining
lambda that cannot be instantiated. Every other type variable
and region in ps_vta is generalized and can be instantiated. *)
and region in ps_aty is generalized and can be instantiated. *)
ps_subst : ity_subst;
(* this substitution instantiates every type variable and region
in ps_vars to itself *)
......@@ -104,10 +104,10 @@ module Wps : Weakhtbl.S with type key = psymbol
val ps_equal : psymbol -> psymbol -> bool
val create_psymbol : preid -> ?ghost:bool -> vty_arrow -> psymbol
val create_psymbol : preid -> ?ghost:bool -> aty -> psymbol
val create_psymbol_extra :
preid -> ?ghost:bool -> vty_arrow -> Spv.t -> Sps.t -> psymbol
preid -> ?ghost:bool -> aty -> Spv.t -> Sps.t -> psymbol
val spec_pvset : Spv.t -> spec -> Spv.t
val ps_pvset : Spv.t -> psymbol -> Spv.t
......@@ -181,9 +181,9 @@ val e_label_add : label -> expr -> expr
val e_label_copy : expr -> expr -> expr
val e_value : pvsymbol -> expr
val e_arrow : psymbol -> vty_arrow -> expr
val e_arrow : psymbol -> aty -> expr
(** [e_arrow p ty] instantiates the program function symbol [p] into a
program expression having the given value type [ty], instantiating
program expression having the given arrow type [ty], instantiating
appropriately the type variables and region variables. The
resulting expression can be applied to arguments using [e_app]
given below.
......@@ -195,7 +195,7 @@ exception ValueExpected of expr
exception ArrowExpected of expr
val ity_of_expr : expr -> ity
val vta_of_expr : expr -> vty_arrow
val aty_of_expr : expr -> aty
exception GhostWrite of expr * region
exception GhostRaise of expr * xsymbol
......
......@@ -447,13 +447,13 @@ let clone_export uc m inst =
c_effect = conv_eff c.c_effect;
c_variant = List.map (conv_vari mv) c.c_variant;
c_letrec = 0; } in
let rec conv_vta mv a =
let args = List.map conv_pv a.vta_args in
let rec conv_aty mv a =
let args = List.map conv_pv a.aty_args in
let add mv pv npv = Mvs.add pv.pv_vs npv.pv_vs mv in
let mv = List.fold_left2 add mv a.vta_args args in
let spec = conv_spec mv a.vta_spec in
let vty = match a.vta_result with
| VTarrow a -> VTarrow (conv_vta mv a)
let mv = List.fold_left2 add mv a.aty_args args in
let spec = conv_spec mv a.aty_spec in
let vty = match a.aty_result with
| VTarrow a -> VTarrow (conv_aty mv a)
| 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
......@@ -482,8 +482,8 @@ let clone_export uc m inst =
mvs := Mvs.add pv.pv_vs npv.pv_vs !mvs;
add_pdecl uc (create_val_decl (LetV npv))
| PDval (LetA ps) ->
let vta = conv_vta !mvs ps.ps_vta in
let nps = create_psymbol (id_clone ps.ps_name) ~ghost:ps.ps_ghost vta in
let aty = conv_aty !mvs ps.ps_aty in
let nps = create_psymbol (id_clone ps.ps_name) ~ghost:ps.ps_ghost aty in
Hid.add psh ps.ps_name (PS nps);
add_pdecl uc (create_val_decl (LetA nps))
| PDrec fdl ->
......@@ -509,10 +509,10 @@ let clone_export uc m inst =
end in
let conv_fd uc { fun_ps = ps } =
let id = id_clone ps.ps_name in
let vta = conv_vta !mvs ps.ps_vta in
let aty = conv_aty !mvs ps.ps_aty in
(* we must retrieve all pvsymbols and psymbols in ps.ps_varm *)
let pvs,pss = Mid.fold add_id ps.ps_varm (Spv.empty,Sps.empty) in
let nps = create_psymbol_extra id ~ghost:ps.ps_ghost vta pvs pss in
let nps = create_psymbol_extra id ~ghost:ps.ps_ghost aty pvs pss in
Hid.add psh ps.ps_name (PS nps);
add_pdecl uc (create_val_decl (LetA nps)) in
List.fold_left conv_fd uc fdl
......
......@@ -669,14 +669,14 @@ let print_pvty info fmt pv =
fprintf fmt "@[(%a:@ %a)@]"
(print_lident info) pv.pv_vs.vs_name (print_ity info) pv.pv_ity
let rec print_vta info fmt vta =
let rec print_aty info fmt aty =
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
fprintf fmt "(%a -> %a)" (print_list Pp.arrow print_arg) aty.aty_args
(print_vty info) aty.aty_result
and print_vty info fmt = function
| VTvalue ity -> print_ity info fmt ity
| VTarrow vta -> print_vta info fmt vta
| VTarrow aty -> print_aty info fmt aty
let is_letrec = function
| [fd] -> Mid.mem fd.fun_ps.ps_name fd.fun_varm
......@@ -829,16 +829,16 @@ let print_let_decl info fmt ld =
else
print_let_decl info fmt ld
let rec extract_vta_args args vta =
let new_args = List.map (fun pv -> pv.pv_vs) vta.vta_args in
let rec extract_aty_args args aty =
let new_args = List.map (fun pv -> pv.pv_vs) aty.aty_args in
let args = List.rev_append new_args args in
match vta.vta_result with
match aty.aty_result with
| VTvalue ity -> List.rev args, ity
| VTarrow vta -> extract_vta_args args vta
| VTarrow aty -> extract_aty_args args aty
let extract_lv_args = function
| LetV pv -> [], pv.pv_ity
| LetA ps -> extract_vta_args [] ps.ps_vta
| LetA ps -> extract_aty_args [] ps.ps_aty
let print_val_decl info fmt lv =
let vars, ity = extract_lv_args lv in
......
......@@ -124,13 +124,13 @@ let print_effect fmt eff =
Sexn.iter (print_xs "ghost raise") eff.eff_ghostx;
Mreg.iter print_reset eff.eff_resets
let rec print_vta fmt vta =
let rec print_aty fmt aty =
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
fprintf fmt "%a%a%a" (print_list nothing print_arg) aty.aty_args
print_effect aty.aty_spec.c_effect print_vty aty.aty_result
and print_vty fmt = function
| VTarrow vta -> print_vta fmt vta
| VTarrow aty -> print_aty fmt aty
| VTvalue ity -> print_ity fmt ity
let print_pvty fmt pv = fprintf fmt "@[%a:@,%a@]"
......@@ -141,12 +141,12 @@ let print_psty fmt ps =
fprintf fmt "[%a]@ " (print_list comma print_tv) (Stv.elements tvs) in
let print_regs fmt regs = if not (Sreg.is_empty regs) then
fprintf fmt "<%a>@ " (print_list comma print_regty) (Sreg.elements regs) in
let vars = vta_vars ps.ps_vta in
let vars = aty_vars ps.ps_aty in
fprintf fmt "@[%a :@ %a%a%a@]"
print_ps ps
print_tvs (Mtv.set_diff vars.vars_tv ps.ps_subst.ity_subst_tv)
print_regs (Mreg.set_diff vars.vars_reg ps.ps_subst.ity_subst_reg)
print_vta ps.ps_vta
print_aty ps.ps_aty
(* specification *)
......@@ -165,12 +165,12 @@ let forget_lv = function
let rec print_type_v fmt = function
| VTvalue ity -> print_ity fmt ity
| VTarrow vta ->
| VTarrow aty ->
let print_arg fmt pv = fprintf fmt "@[(%a)@] ->@ " print_pvty pv in
fprintf fmt "%a%a"
(print_list nothing print_arg) vta.vta_args
(print_type_c vta.vta_spec) vta.vta_result;
List.iter forget_pv vta.vta_args
(print_list nothing print_arg) aty.aty_args
(print_type_c aty.aty_spec) aty.aty_result;
List.iter forget_pv aty.aty_args
and print_type_c spec fmt vty =
fprintf fmt "{ %a }@ %a%a@ { %a }"
......@@ -395,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_ity | LetA ps -> VTarrow ps.ps_vta in
| LetV pv -> VTvalue pv.pv_ity | LetA ps -> VTarrow ps.ps_aty 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 () | _ -> ()
......
......@@ -27,9 +27,9 @@ val print_xs : formatter -> xsymbol -> unit (* exception symbol *)
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_vta : formatter -> vty_arrow -> unit (* arrow type *)
val print_ity : formatter -> ity -> unit (* individual type *)
val print_aty : formatter -> aty -> unit (* arrow type *)
val print_vty : formatter -> vty -> unit (* expression type *)
val print_pv : formatter -> pvsymbol -> unit (* program variable *)
......
......@@ -823,21 +823,21 @@ let create_pvsymbol, restore_pv, restore_pv_by_id =
type vty =
| VTvalue of ity
| VTarrow of vty_arrow
| VTarrow of aty
and vty_arrow = {
vta_args : pvsymbol list;
vta_result : vty;
vta_spec : spec;
and aty = {
aty_args : pvsymbol list;
aty_result : vty;
aty_spec : spec;
}
let rec vta_vars vta =
let rec aty_vars aty =
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
List.fold_left add_arg (vty_vars aty.aty_result) aty.aty_args
and vty_vars = function
| VTvalue ity -> ity.ity_vars
| VTarrow vta -> vta_vars vta
| VTarrow aty -> aty_vars aty
let ity_of_vty = function
| VTvalue ity -> ity
......@@ -850,9 +850,9 @@ let ty_of_vty = function
let spec_check spec vty = spec_check spec (ty_of_vty vty)
let vty_arrow_unsafe argl spec vty = {
vta_args = argl;
vta_result = vty;
vta_spec = spec;
aty_args = argl;
aty_result = vty;
aty_spec = spec;
}
let vty_arrow argl ?spec vty =
......@@ -870,56 +870,56 @@ let vty_arrow argl ?spec vty =
vty_arrow_unsafe argl spec vty
(* this only compares the types of arguments and results, and ignores
the spec. In other words, only the type variables and regions
in .vta_vars are matched. The caller should supply a "freezing"
the spec. In other words, only the type variables and regions in
[aty_vars aty] 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 rec aty_vars_match s a1 a2 =
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
| [],[] -> s, a1.aty_result, a2.aty_result
| [], _ -> s, a1.aty_result, VTarrow { a2 with aty_args = l2 }
| _, [] -> s, VTarrow { a1 with aty_args = l1 }, a2.aty_result
| {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
let s, vty1, vty2 = match_args s a1.aty_args a2.aty_args in
match vty1, vty2 with
| VTarrow a1, VTarrow a2 -> vta_vars_match s a1 a2
| VTarrow a1, VTarrow a2 -> aty_vars_match s a1 a2
| VTvalue v1, VTvalue v2 -> ity_match s v1 v2
| _ -> invalid_arg "Mlw_ty.vta_vars_match"
| _ -> invalid_arg "Mlw_ty.aty_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 =
(* the substitution must cover not only [aty_vars aty] but
also every type variable and every region in [aty_spec] *)
let aty_full_inst sbs aty =
let tvm = Mtv.map ty_of_ity sbs.ity_subst_tv 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
let rec vta_inst vsm vta =
let vsm, args = Lists.map_fold_left add_arg vsm vta.vta_args in
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)
let rec aty_inst vsm aty =
let vsm, args = Lists.map_fold_left add_arg vsm aty.aty_args in
let spec = spec_full_inst sbs tvm vsm aty.aty_spec in
let vty = match aty.aty_result with
| VTarrow aty -> VTarrow (aty_inst vsm aty)
| VTvalue ity -> VTvalue (ity_full_inst sbs ity) in
vty_arrow_unsafe args spec vty
in
vta_inst Mvs.empty vta
aty_inst Mvs.empty aty
(* remove from the given arrow every effect that is covered
neither by the arrow's vta_vars nor by the given varmap *)