Commit 4eb22501 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

whyml: keep track of visible (non-ghost) regions

parent fd3f256b
......@@ -68,54 +68,63 @@ let null_invariant { its_ts = ts } =
let create_data_decl tdl =
let news = ref Sid.empty in
let projections = Hstr.create 17 in (* id -> plsymbol *)
let build_constructor its res cll (id,al) =
(* check well-formedness *)
let fds = List.map snd al in
let tvs = List.fold_right Stv.add its.its_ts.ts_args Stv.empty in
let regs = List.fold_right Sreg.add its.its_regs Sreg.empty in
let check_vars { vars_tv = atvs; vars_reg = aregs } =
if not (Stv.subset atvs tvs) then
raise (UnboundTypeVar (Stv.choose (Stv.diff atvs tvs)));
if not (Sreg.subset aregs regs) then
raise (UnboundRegion (Sreg.choose (Sreg.diff aregs regs))) in
let check_arg fd = match fd.fd_mut with
| Some r -> if not (Sreg.mem r regs) then raise (UnboundRegion r)
| None -> check_vars fd.fd_ity.ity_vars in
List.iter check_arg fds;
(* build the constructor ps *)
let hidden = its.its_abst and rdonly = its.its_priv in
let cs = create_plsymbol ~hidden ~rdonly ~constr:cll id fds res in
news := news_id !news cs.pl_ls.ls_name;
(* build the projections, if any *)
let build_proj fd id =
try
let pj = Hstr.find projections (preid_name id) in
ity_equal_check pj.pl_value.fd_ity fd.fd_ity;
begin match pj.pl_value.fd_mut, fd.fd_mut with
| None, None -> ()
| Some r1, Some r2 -> reg_equal_check r1 r2
| _,_ -> invalid_arg "Mlw_decl.create_data_decl"
end;
if pj.pl_value.fd_ghost <> fd.fd_ghost then
invalid_arg "Mlw_decl.create_data_decl";
pj
with Not_found ->
let pj = create_plsymbol ~hidden id [res] fd in
news := news_id !news pj.pl_ls.ls_name;
Hstr.add projections (preid_name id) pj;
pj
in
cs, List.map (fun (id,fd) -> Opt.map (build_proj fd) id) al
in
let build_type (its,cl) =
Hstr.clear projections;
news := news_id !news its.its_ts.ts_name;
let cll = List.length cl in
let projections = Hstr.create 3 in
let hidden = its.its_abst in
let rdonly = its.its_priv in
let constr = List.length cl in
let tvl = List.map ity_var its.its_ts.ts_args in
let ity = ity_app its tvl its.its_regs in
let res = { fd_ity = ity; fd_ghost = false; fd_mut = None } in
its, List.map (build_constructor its res cll) cl, null_invariant its
let tvs = List.fold_right Stv.add its.its_ts.ts_args Stv.empty in
let regs = List.fold_right Sreg.add its.its_regs Sreg.empty in
let nogh = ity_nonghost_reg Sreg.empty ity in
let build_constructor (id,al) =
(* check well-formedness *)
let fds = List.map snd al in
let check_vars { vars_tv = atvs; vars_reg = aregs } =
if not (Stv.subset atvs tvs) then
raise (UnboundTypeVar (Stv.choose (Stv.diff atvs tvs)));
if not (Sreg.subset aregs regs) then
raise (UnboundRegion (Sreg.choose (Sreg.diff aregs regs))) in
let check_vars fd = match fd.fd_mut with
| Some r -> if not (Sreg.mem r regs) then raise (UnboundRegion r)
| None -> check_vars fd.fd_ity.ity_vars in
let check_ghost fd =
let regs = ity_nonghost_reg Sreg.empty fd.fd_ity in
let regs = Opt.fold_right Sreg.add fd.fd_mut regs in
if not (Sreg.subset regs nogh) then
invalid_arg "Mlw_decl.create_data_decl" in
let check_fd fd =
if not fd.fd_ghost then check_ghost fd;
check_vars fd in
List.iter check_fd fds;
(* build the constructor symbol *)
let cs = create_plsymbol ~hidden ~rdonly ~constr id fds res in
news := news_id !news cs.pl_ls.ls_name;
(* build the projections, if any *)
let build_proj fd id =
try
let pj = Hstr.find projections (preid_name id) in
ity_equal_check pj.pl_value.fd_ity fd.fd_ity;
begin match pj.pl_value.fd_mut, fd.fd_mut with
| None, None -> ()
| Some r1, Some r2 -> reg_equal_check r1 r2
| _,_ -> invalid_arg "Mlw_decl.create_data_decl"
end;
if pj.pl_value.fd_ghost <> fd.fd_ghost then
invalid_arg "Mlw_decl.create_data_decl";
pj
with Not_found ->
let pj = create_plsymbol ~hidden id [res] fd in
news := news_id !news pj.pl_ls.ls_name;
Hstr.add projections (preid_name id) pj;
pj
in
cs, List.map (fun (id,fd) -> Opt.map (build_proj fd) id) al
in
its, List.map build_constructor cl, null_invariant its
in
let tdl = List.map build_type tdl in
mk_decl (PDdata tdl) Sid.empty !news
......
......@@ -27,6 +27,7 @@ module rec T : sig
its_ts : tysymbol;
its_regs : region list;
its_def : ity option;
its_ghrl : bool list;
its_inv : bool;
its_abst : bool;
its_priv : bool;
......@@ -59,6 +60,7 @@ end = struct
its_ts : tysymbol;
its_regs : region list;
its_def : ity option;
its_ghrl : bool list;
its_inv : bool;
its_abst : bool;
its_priv : bool;
......@@ -157,16 +159,16 @@ module Hsity = Hashcons.Make (struct
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
let vars ity = match ity.ity_node with
| Ityvar v ->
{ s with vars_tv = Stv.add v s.vars_tv }
{ vars_tv = Stv.singleton v; vars_reg = Sreg.empty }
| Itypur (_,tl) ->
List.fold_left ity_vars s tl
List.fold_left ity_vars vars_empty tl
| Ityapp (_,tl,rl) ->
List.fold_left reg_vars (List.fold_left ity_vars s tl) rl
List.fold_left reg_vars (List.fold_left ity_vars vars_empty tl) rl
let tag n ity = { ity with
ity_vars = vars vars_empty ity;
ity_vars = vars ity;
ity_tag = Weakhtbl.create_tag n }
end)
......@@ -264,6 +266,31 @@ let rec reg_iter fn vars =
let reg_occurs r vars = reg_any (reg_equal r) vars
(* detect non-ghost type variables and regions *)
let rec ity_nonghost_reg regs ity = match ity.ity_node with
| _ when ity_immutable ity -> regs
| Ityvar _ -> regs
| Itypur (_,tl) -> List.fold_left ity_nonghost_reg regs tl
| Ityapp ({ its_ghrl = ghrl },tl,rl) ->
let regs = List.fold_left ity_nonghost_reg regs tl in
List.fold_left2 (fun s gh ({ reg_ity = ity } as r) ->
if gh then s else ity_nonghost_reg (Sreg.add r s) ity) regs ghrl rl
let lookup_nonghost_reg regs ity =
let rec any ity = match ity.ity_node with
| _ when ity_immutable ity -> ()
| Ityvar _ -> ()
| Itypur (_,tl) -> List.iter any tl
| Ityapp ({ its_ghrl = ghrl },tl,rl) ->
List.iter any tl;
List.iter2 (fun gh ({ reg_ity = ity } as r) -> if not gh then
(if Sreg.mem r regs then raise Util.FoldSkip else any ity)) ghrl rl
in
if reg_any (fun r -> Sreg.mem r regs) ity.ity_vars
then try any ity; false with Util.FoldSkip -> true
else false
(* smart constructors *)
exception BadItyArity of itysymbol * int * int
......@@ -408,11 +435,12 @@ let ity_pur s tl =
let create_itysymbol_unsafe, restore_its =
let ts_to_its = Wts.create 17 in
(fun ts ~abst ~priv ~inv regs def ->
(fun ts ~abst ~priv ~inv ~ghrl regs def ->
let its = {
its_ts = ts;
its_regs = regs;
its_def = def;
its_ghrl = ghrl;
its_inv = inv;
its_abst = abst;
its_priv = priv;
......@@ -421,12 +449,13 @@ let create_itysymbol_unsafe, restore_its =
its),
Wts.find ts_to_its
let create_itysymbol
name ?(abst=false) ?(priv=false) ?(inv=false) args regs def =
let create_itysymbol name
?(abst=false) ?(priv=false) ?(inv=false) ?(ghost_reg=Sreg.empty)
args regs def =
let puredef = Opt.map ty_of_ity def in
let purets = create_tysymbol name args puredef in
(* all regions *)
let add s v = Sreg.add_new (DuplicateRegion v) v s in
let add s r = Sreg.add_new (DuplicateRegion r) r s in
let sregs = List.fold_left add Sreg.empty regs in
(* all type variables *)
let sargs = List.fold_right Stv.add args Stv.empty in
......@@ -444,7 +473,16 @@ let create_itysymbol
if priv then Loc.errorm "Type aliases cannot be private";
if inv then Loc.errorm "Type aliases cannot have invariants"
end;
create_itysymbol_unsafe purets ~abst ~priv ~inv regs def
(* every ghost region argument must be in [regs] *)
if not (Sreg.subset ghost_reg sregs) then
invalid_arg "Mlw_ty.create_itysymbol";
Opt.iter (fun ity ->
let nogh = ity_nonghost_reg Sreg.empty ity in
if Sreg.exists (fun r -> Sreg.mem r ghost_reg) nogh then
invalid_arg "Mlw_ty.create_itysymbol") def;
let ghrl = List.map (fun r -> Sreg.mem r ghost_reg) regs in
(* create the type symbol *)
create_itysymbol_unsafe purets ~abst ~priv ~inv ~ghrl regs def
let ts_unit = ts_tuple 0
let ty_unit = ty_tuple []
......@@ -467,10 +505,11 @@ let its_clone sm =
let nits = try restore_its nts with Not_found ->
let abst = oits.its_abst in
let priv = oits.its_priv in
let ghrl = oits.its_ghrl in
let inv = oits.its_inv in
let regs = List.map conv_reg oits.its_regs in
let def = Opt.map conv_ity oits.its_def in
create_itysymbol_unsafe nts ~abst ~priv ~inv regs def
create_itysymbol_unsafe nts ~abst ~priv ~inv ~ghrl regs def
in
Hits.replace itsh oits nits;
nits
......
......@@ -24,12 +24,13 @@ module rec T : sig
}
type itysymbol = private {
its_ts : tysymbol;
its_regs : region list;
its_def : ity option;
its_inv : bool;
its_abst : bool;
its_priv : bool;
its_ts : tysymbol; (* "pure snapshot" type symbol *)
its_regs : region list; (* region arguments *)
its_def : ity option; (* type alias definition *)
its_ghrl : bool list; (* ghost region arguments *)
its_inv : bool; (* carries a type invariant *)
its_abst : bool; (* is an abstract (= "model") type *)
its_priv : bool; (* is a private (à la Ocaml) type *)
}
(** ity = individual type in programs, first-order, i.e. no functions *)
......@@ -86,7 +87,8 @@ val create_region : preid -> ity -> region
(** creation of a symbol for type in programs *)
val create_itysymbol :
preid -> ?abst:bool -> ?priv:bool -> ?inv:bool ->
preid ->
?abst:bool -> ?priv:bool -> ?inv:bool -> ?ghost_reg:Sreg.t ->
tvsymbol list -> region list -> ity option -> itysymbol
val restore_its : tysymbol -> itysymbol
......@@ -134,6 +136,11 @@ val reg_iter : (region -> unit) -> varset -> unit
val reg_occurs : region -> varset -> bool
(* detect non-ghost regions *)
val ity_nonghost_reg : Sreg.t -> ity -> Sreg.t
val lookup_nonghost_reg : Sreg.t -> ity -> bool
(* built-in types *)
val ts_unit : tysymbol (* the same as [Ty.ts_tuple 0] *)
......
......@@ -1706,13 +1706,17 @@ let add_types ~wp uc tdl =
let ts = match d.td_def with
| TDalias ty when Hstr.find impures x ->
let def = parse ty in
let nogh = ity_nonghost_reg Sreg.empty def in
let ghost_reg = Sreg.diff def.ity_vars.vars_reg nogh in
let rl = Sreg.elements def.ity_vars.vars_reg in
PT (create_itysymbol id ~abst ~priv ~inv:false vl rl (Some def))
PT (create_itysymbol id
~abst ~priv ~inv:false ~ghost_reg vl rl (Some def))
| TDalias ty ->
let def = ty_of_ity (parse ty) in
TS (create_tysymbol id vl (Some def))
| TDalgebraic csl when Hstr.find mutables x ->
let projs = Hstr.create 5 in
let nogh = ref Sreg.empty in
(* to check projections' types we must fix the tyvars *)
let add s v = let t = ity_var v in ity_match s t t in
let sbs = List.fold_left add ity_subst_empty vl in
......@@ -1722,6 +1726,7 @@ let add_types ~wp uc tdl =
let inv = inv || ity_has_inv ity in
match id with
| None ->
if not gh then nogh := ity_nonghost_reg !nogh ity;
let regs = Sreg.union regs ity.ity_vars.vars_reg in
(regs, inv), (None, fd)
| Some id ->
......@@ -1733,6 +1738,7 @@ let add_types ~wp uc tdl =
(regs, inv), (Some (Denv.create_user_id id), fd)
with Not_found ->
Hstr.replace projs id.id fd;
if not gh then nogh := ity_nonghost_reg !nogh ity;
let regs = Sreg.union regs ity.ity_vars.vars_reg in
(regs, inv), (Some (Denv.create_user_id id), fd)
in
......@@ -1742,10 +1748,12 @@ let add_types ~wp uc tdl =
in
let init = (Sreg.empty, d.td_inv <> []) in
let (regs,inv),def = Lists.map_fold_left mk_constr init csl in
let ghost_reg = Sreg.diff regs !nogh in
let rl = Sreg.elements regs in
Hstr.replace predefs x def;
PT (create_itysymbol id ~abst ~priv ~inv vl rl None)
PT (create_itysymbol id ~abst ~priv ~inv ~ghost_reg vl rl None)
| TDrecord fl when Hstr.find mutables x ->
let nogh = ref Sreg.empty in
let mk_field (regs,inv) f =
let ity = parse f.f_pty in
let inv = inv || ity_has_inv ity in
......@@ -1756,14 +1764,17 @@ let add_types ~wp uc tdl =
else
Sreg.union regs ity.ity_vars.vars_reg, None
in
if not f.f_ghost then nogh :=
Opt.fold_right Sreg.add mut (ity_nonghost_reg !nogh ity);
(regs, inv), (Some fid, mk_field ity f.f_ghost mut)
in
let init = (Sreg.empty, d.td_inv <> []) in
let (regs,inv),pjl = Lists.map_fold_left mk_field init fl in
let ghost_reg = Sreg.diff regs !nogh in
let rl = Sreg.elements regs in
let cid = { d.td_ident with id = "mk " ^ d.td_ident.id } in
Hstr.replace predefs x [Denv.create_user_id cid, pjl];
PT (create_itysymbol id ~abst ~priv ~inv vl rl None)
PT (create_itysymbol id ~abst ~priv ~inv ~ghost_reg vl rl None)
| TDalgebraic _ | TDrecord _ when Hstr.find impures x ->
PT (create_itysymbol id ~abst ~priv ~inv:false vl [] None)
| TDalgebraic _ | TDrecord _ | TDabstract ->
......
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