Skip to content

GitLab

Commit 67d896b8 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

whyml: compute varset for ity's on construction

parent 6b219bee
Hide whitespace changes
Inline Side-by-side
src/whyml/mlw_decl.ml
View file @ 67d896b8
......@@ -25,6 +25,7 @@ open Ty
open Term
open Decl
open Mlw_ty
open Mlw_ty.T
open Mlw_expr
type constructor = plsymbol * plsymbol option list
......
src/whyml/mlw_decl.mli
View file @ 67d896b8
......@@ -23,6 +23,7 @@ open Ident
open Ty
open Term
open Mlw_ty
open Mlw_ty.T
open Mlw_expr
(** {2 Type declaration} *)
......
src/whyml/mlw_expr.ml
View file @ 67d896b8
......@@ -23,6 +23,7 @@ open Ident
open Ty
open Term
open Mlw_ty
open Mlw_ty.T
(** program variables *)
......
src/whyml/mlw_expr.mli
View file @ 67d896b8
......@@ -23,6 +23,7 @@ open Ident
open Ty
open Term
open Mlw_ty
open Mlw_ty.T
(** program variables *)
......
src/whyml/mlw_module.ml
View file @ 67d896b8
......@@ -25,6 +25,7 @@ open Ty
open Term
open Theory
open Mlw_ty
open Mlw_ty.T
open Mlw_expr
open Mlw_decl
......
src/whyml/mlw_module.mli
View file @ 67d896b8
......@@ -26,6 +26,7 @@ open Term
open Decl
open Theory
open Mlw_ty
open Mlw_ty.T
open Mlw_expr
open Mlw_decl
......
src/whyml/mlw_pretty.ml
View file @ 67d896b8
......@@ -28,6 +28,7 @@ open Term
open Theory
open Pretty
open Mlw_ty
open Mlw_ty.T
open Mlw_expr
open Mlw_decl
open Mlw_module
......
src/whyml/mlw_pretty.mli
View file @ 67d896b8
......@@ -21,6 +21,7 @@
open Format
open Why3
open Mlw_ty
open Mlw_ty.T
open Mlw_expr
open Mlw_decl
open Mlw_module
......
src/whyml/mlw_ty.ml
View file @ 67d896b8
......@@ -19,6 +19,7 @@
(**************************************************************************)
open Why3
open Stdlib
open Util
open Ident
open Ty
......@@ -26,38 +27,88 @@ open Term
(** value types (w/o effects) *)
type itysymbol = {
its_pure : tysymbol;
its_args : tvsymbol list;
its_regs : region list;
its_def : ity option;
its_abst : bool;
its_priv : bool;
}
module rec T : sig
and ity = {
ity_node : ity_node;
ity_tag : Hashweak.tag;
}
type varset = {
vars_tv : Stv.t;
vars_reg : Reg.S.t;
}
and ity_node =
| Ityvar of tvsymbol
| Itypur of tysymbol * ity list
| Ityapp of itysymbol * ity list * region list
type itysymbol = {
its_pure : tysymbol;
its_args : tvsymbol list;
its_regs : region list;
its_def : ity option;
its_abst : bool;
its_priv : bool;
}
and region = {
reg_name : ident;
reg_ity : ity;
reg_ghost : bool;
}
and ity = {
ity_node : ity_node;
ity_vars : varset;
ity_tag : Hashweak.tag;
}
(** regions *)
and ity_node =
| Ityvar of tvsymbol
| Itypur of tysymbol * ity list
| Ityapp of itysymbol * ity list * region list
module Reg = WeakStructMake (struct
type t = region
let tag r = r.reg_name.id_tag
and region = {
reg_name : ident;
reg_ity : ity;
reg_ghost : bool;
}
end = struct
type varset = {
vars_tv : Stv.t;
vars_reg : Reg.S.t;
}
type itysymbol = {
its_pure : tysymbol;
its_args : tvsymbol list;
its_regs : region list;
its_def : ity option;
its_abst : bool;
its_priv : bool;
}
and ity = {
ity_node : ity_node;
ity_vars : varset;
ity_tag : Hashweak.tag;
}
and ity_node =
| Ityvar of tvsymbol
| Itypur of tysymbol * ity list
| Ityapp of itysymbol * ity list * region list
and region = {
reg_name : ident;
reg_ity : ity;
reg_ghost : bool;
}
end
and Reg : sig
module M : Map.S with type key = T.region
module S : M.Set
module H : Hashtbl.S with type key = T.region
module W : Hashweak.S with type key = T.region
end = WeakStructMake (struct
type t = T.region
let tag r = r.T.reg_name.id_tag
end)
open T
(** regions *)
module Sreg = Reg.S
module Mreg = Reg.M
module Hreg = Reg.H
......@@ -78,6 +129,17 @@ let reg_hash r = id_hash r.reg_name
let create_region id ?(ghost=false) ty =
{ reg_name = id_register id; reg_ity = ty; reg_ghost = ghost }
(* variable sets *)
let vars_empty = { vars_tv = Stv.empty ; vars_reg = Sreg.empty }
let vars_union s1 s2 = {
vars_tv = Stv.union s1.vars_tv s2.vars_tv;
vars_reg = Sreg.union s1.vars_reg s2.vars_reg;
}
let vs_vars s vs = { s with vars_tv = ty_freevars s.vars_tv vs.vs_ty }
(* value type symbols *)
module Itsym = WeakStructMake (struct
......@@ -117,7 +179,21 @@ module Hsity = Hashcons.Make (struct
Hashcons.combine_list reg_hash
(Hashcons.combine_list ity_hash (its_hash s) tl) rl
let tag n ity = { ity with ity_tag = Hashweak.create_tag n }
let ity_vars s ity = vars_union s ity.ity_vars
let reg_vars s r = { s with vars_reg = Sreg.add r s.vars_reg }
let vars s ity = match ity.ity_node with
| Ityvar v ->
{ s with vars_tv = Stv.add v s.vars_tv }
| Itypur (_,tl) ->
List.fold_left ity_vars s tl
| Ityapp (_,tl,rl) ->
List.fold_left reg_vars (List.fold_left ity_vars s tl) rl
let tag n ity = { ity with
ity_vars = vars vars_empty ity;
ity_tag = Hashweak.create_tag n }
end)
module Ity = WeakStructMake (struct
......@@ -132,6 +208,7 @@ module Wity = Ity.W
let mk_ity n = {
ity_node = n;
ity_vars = vars_empty;
ity_tag = Hashweak.dummy_tag;
}
......@@ -199,11 +276,8 @@ let ity_v_any prv prr ity =
let ity_subst_unsafe mv mr ity =
ity_v_map_unsafe (fun v -> Mtv.find v mv) (fun r -> Mreg.find r mr) ity
let ity_freevars = ity_v_fold (fun s v -> Stv.add v s) Util.const
let ity_topregions = ity_v_fold Util.const (fun s r -> Sreg.add r s)
let ity_closed = ity_v_all Util.ffalse Util.ttrue
let ity_pure = ity_v_all Util.ttrue Util.ffalse
let ity_closed ity = Stv.is_empty ity.ity_vars.vars_tv
let ity_pure ity = Sreg.is_empty ity.ity_vars.vars_reg
(* smart constructors *)
......@@ -385,28 +459,6 @@ let ity_int = ity_of_ty Ty.ty_int
let ity_bool = ity_of_ty Ty.ty_bool
let ity_unit = ity_of_ty (Ty.ty_tuple [])
type varset = {
vars_tv : Stv.t;
vars_reg : Sreg.t;
}
let vars_empty = { vars_tv = Stv.empty ; vars_reg = Sreg.empty }
let ity_vars s ity = {
vars_tv = ity_freevars s.vars_tv ity;
vars_reg = ity_topregions s.vars_reg ity;
}
let vs_vars s vs = {
vars_tv = ty_freevars s.vars_tv vs.vs_ty;
vars_reg = s.vars_reg;
}
let vars_union s1 s2 = {
vars_tv = Stv.union s1.vars_tv s2.vars_tv;
vars_reg = Sreg.union s1.vars_reg s2.vars_reg;
}
let vars_freeze s =
let sbs = Stv.fold (fun v -> Mtv.add v (ity_var v)) s.vars_tv Mtv.empty in
let sbs = { ity_subst_tv = sbs ; ity_subst_reg = Mreg.empty } in
......@@ -547,7 +599,7 @@ let vty_vars s = function
| VTarrow vta -> vars_union s vta.vta_vars
let vty_value ?(ghost=false) ?mut ity =
let vars = ity_vars vars_empty ity in
let vars = ity.ity_vars in
let vars = match mut with
| Some r ->
if r.reg_ghost && not ghost then
......
src/whyml/mlw_ty.mli
View file @ 67d896b8
......@@ -26,30 +26,43 @@ open Term
(** individual types (first-order types w/o effects) *)
type itysymbol = private {
its_pure : tysymbol;
its_args : tvsymbol list;
its_regs : region list;
its_def : ity option;
its_abst : bool;
its_priv : bool;
}
and ity = private {
ity_node : ity_node;
ity_tag : Hashweak.tag;
}
and ity_node = private
| Ityvar of tvsymbol
| Itypur of tysymbol * ity list
| Ityapp of itysymbol * ity list * region list
and region = private {
reg_name : ident;
reg_ity : ity;
reg_ghost : bool;
}
module rec T : sig
type varset = private {
vars_tv : Stv.t;
vars_reg : Mreg.Set.t;
}
type itysymbol = private {
its_pure : tysymbol;
its_args : tvsymbol list;
its_regs : region list;
its_def : ity option;
its_abst : bool;
its_priv : bool;
}
and ity = private {
ity_node : ity_node;
ity_vars : varset;
ity_tag : Hashweak.tag;
}
and ity_node = private
| Ityvar of tvsymbol
| Itypur of tysymbol * ity list
| Ityapp of itysymbol * ity list * region list
and region = private {
reg_name : ident;
reg_ity : ity;
reg_ghost : bool;
}
end
and Mreg : sig include Map.S with type key = T.region end
open T
module Mits : Map.S with type key = itysymbol
module Sits : Mits.Set
......@@ -61,7 +74,6 @@ module Sity : Mity.Set
module Hity : Hashtbl.S with type key = ity
module Wity : Hashweak.S with type key = ity
module Mreg : Map.S with type key = region
module Sreg : Mreg.Set
module Hreg : Hashtbl.S with type key = region
module Wreg : Hashweak.S with type key = region
......@@ -122,8 +134,6 @@ val ity_v_fold :
val ity_v_all : (tvsymbol -> bool) -> (region -> bool) -> ity -> bool
val ity_v_any : (tvsymbol -> bool) -> (region -> bool) -> ity -> bool
val ity_freevars : Stv.t -> ity -> Stv.t
val ity_topregions : Sreg.t -> ity -> Sreg.t
val ity_closed : ity -> bool
val ity_pure : ity -> bool
......@@ -153,19 +163,12 @@ val ity_full_inst : ity_subst -> ity -> ity
val reg_full_inst : ity_subst -> region -> region
type varset = private {
vars_tv : Stv.t;
vars_reg : Sreg.t;
}
val vars_empty : varset
val vars_union : varset -> varset -> varset
val vars_freeze : varset -> ity_subst
val ity_vars : varset -> ity -> varset
val vs_vars : varset -> vsymbol -> varset
(* exception symbols *)
......
src/whyml/mlw_typing.ml
View file @ 67d896b8
......@@ -29,6 +29,7 @@ open Env
open Ptree
open Mlw_dtree
open Mlw_ty
open Mlw_ty.T
open Mlw_expr
open Mlw_decl
open Mlw_module
......@@ -300,8 +301,8 @@ let add_types uc tdl =
let ts = match d.td_def with
| TDalias ty ->
let def = parse ty in
let s = ity_topregions Sreg.empty def in
create_itysymbol id ~abst ~priv vl (Sreg.elements s) (Some def)
let rl = Sreg.elements def.ity_vars.vars_reg in
create_itysymbol id ~abst ~priv vl rl (Some def)
| TDalgebraic csl when Hashtbl.find mutables x ->
let projs = Hashtbl.create 5 in
(* to check projections' types we must fix the tyvars *)
......@@ -313,7 +314,7 @@ let add_types uc tdl =
match id with
| None ->
let pv = create_pvsymbol (id_fresh "pj") vtv in
ity_topregions s ity, (pv, false)
Sreg.union s ity.ity_vars.vars_reg, (pv, false)
| Some id ->
try
let pv = Hashtbl.find projs id.id in
......@@ -325,7 +326,7 @@ let add_types uc tdl =
with Not_found ->
let pv = create_pvsymbol (Denv.create_user_id id) vtv in
Hashtbl.replace projs id.id pv;
ity_topregions s ity, (pv, true)
Sreg.union s ity.ity_vars.vars_reg, (pv, true)
in
let mk_constr s (_loc,cid,pjl) =
let s,pjl = Util.map_fold_left mk_proj s pjl in
......@@ -343,7 +344,7 @@ let add_types uc tdl =
let r = create_region fid ~ghost ity in
Sreg.add r s, Some r
else
ity_topregions s ity, None
Sreg.union s ity.ity_vars.vars_reg, None
in
let vtv = vty_value ?mut ~ghost ity in
s, (create_pvsymbol fid vtv, true)
......
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