Skip to content

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

Mlw: rework snapshot types (wip)

parent cc509106
Hide whitespace changes
Inline Side-by-side
Showing with 551 additions and 483 deletions
src/mlw/dexpr.ml
View file @ ea3387ff
......@@ -24,7 +24,6 @@ type dity =
| Durg of ity * dity (* undestructible "user" region, for global refs *)
| Dreg of dvar ref * dity (* destructible "fresh" region *)
| Dapp of itysymbol * dity list * dity list
| Dpur of itysymbol * dity list
and dvar =
| Dtvs of tvsymbol (* unassigned fresh type variable *)
......@@ -47,21 +46,16 @@ let dreg_fresh dity = Dreg (dvar_fresh "rho", dity)
let dity_of_ity ity =
let hr = Hreg.create 3 in
let rec dity ity = match ity.ity_node with
| Ityapp (s,tl,rl) -> Dapp (s, List.map dity tl, List.map dreg rl)
| Itypur (s,tl) -> Dpur (s, List.map dity tl)
| Ityvar v -> Dutv v
| Ityapp (s,tl,rl) -> Dapp (s, List.map dity tl, List.map dity rl)
| Ityvar (v,_) -> Dutv v
| Ityreg r -> dreg r
and dreg reg =
try Hreg.find hr reg with Not_found ->
let {reg_its = s; reg_args = tl; reg_regs = rl} = reg in
let d = Dapp (s, List.map dity tl, List.map dreg rl) in
let d = Dapp (s, List.map dity tl, List.map dity rl) in
let r = dreg_fresh d in Hreg.add hr reg r; r in
dity ity
let reg_of_ity = function
| {ity_node = Ityreg reg} -> reg
| _ -> assert false
let rec ity_of_dity = function
| Dvar ({contents = Dval d})
| Dreg ({contents = Dval d}, _) ->
......@@ -75,17 +69,14 @@ let rec ity_of_dity = function
| Dutv v -> ity_var v
| Durg (ity,_) -> ity
| Dapp (s,tl,rl) ->
let reg_of_dity r = reg_of_ity (ity_of_dity r) in
ity_app s (List.map ity_of_dity tl) (List.map reg_of_dity rl)
| Dpur (s,tl) ->
ity_pur s (List.map ity_of_dity tl)
ity_app s (List.map ity_of_dity tl) (List.map ity_of_dity rl)
(** Destructive type unification *)
let rec occur_check v = function
| Dvar {contents = Dval d} | Dreg (_,d) | Durg (_,d) -> occur_check v d
| Dvar {contents = Dtvs u} | Dutv u -> if tv_equal u v then raise Exit
| Dapp (_,dl,_) | Dpur (_,dl) -> List.iter (occur_check v) dl
| Dapp (_,dl,_) -> List.iter (occur_check v) dl
let rec dity_unify d1 d2 = match d1,d2 with
| Dvar {contents = Dval d1}, d2
......@@ -102,8 +93,7 @@ let rec dity_unify d1 d2 = match d1,d2 with
r := Dval d
| Dutv u, Dutv v when tv_equal u v ->
()
|(Dapp (s1,dl1,_), Dapp (s2,dl2,_)
| Dpur (s1,dl1), Dpur (s2,dl2)) when its_equal s1 s2 ->
| Dapp (s1,dl1,_), Dapp (s2,dl2,_) when its_equal s1 s2 ->
List.iter2 dity_unify dl1 dl2
| _ -> raise Exit
......@@ -124,7 +114,6 @@ let rec dity_refresh ht = function
let r = dreg_fresh (dity_refresh ht d) in
Htv.add ht v r; r end
| Dreg _ -> assert false
| Dpur (s,dl) -> Dpur (s, List.map (dity_refresh ht) dl)
| Dapp (s,dl,rl) -> Dapp (s, List.map (dity_refresh ht) dl,
List.map (dity_refresh ht) rl)
| Dvar {contents = Dval d} -> dity_refresh (Htv.create 3) d
......@@ -155,8 +144,6 @@ let rec reunify d1 d2 = match d1,d2 with
| Dapp (_,dl1,rl1), Dapp (_,dl2,rl2) ->
List.iter2 reunify dl1 dl2;
List.iter2 reunify rl1 rl2
| Dpur (_,dl1), Dpur (_,dl2) ->
List.iter2 reunify dl1 dl2
| _ -> assert false
let reunify_regions () =
......@@ -204,6 +191,8 @@ let rec print_dity pri fmt = function
Format.fprintf fmt (protect_on (pri > 1) "%a@ @@%s")
(print_dity 0) d (Ident.id_unique rprinter v.tv_name)
| Durg (ity,d) ->
let reg_of_ity = function
| {ity_node = Ityreg reg} -> reg | _ -> assert false in
Format.fprintf fmt (protect_on (pri > 1) "%a@ @@%s")
(print_dity 0) d (Ident.id_unique rprinter (reg_of_ity ity).reg_name)
| Dapp (s,[t1;t2],[]) when its_equal s its_func ->
......@@ -215,9 +204,11 @@ let rec print_dity pri fmt = function
Format.fprintf fmt (protect_on (pri > 1) "%a%a%a")
Pretty.print_ts s.its_ts (print_args (print_dity 2)) tl
(print_regs (print_dity 0)) rl
(*
| Dpur (s,tl) ->
Format.fprintf fmt (protect_on (pri > 1 && tl <> []) "{%a}%a")
Pretty.print_ts s.its_ts (print_args (print_dity 2)) tl
*)
let print_dity fmt d = print_dity 0 fmt d
......@@ -231,7 +222,6 @@ let specialize_scheme tvs (argl,res) =
| Dvar {contents = Dtvs v} | Dutv v as d -> get_tv v d
| Dreg ({contents = Dtvs v},d) -> get_reg v d
| Dapp (s,dl,rl) -> Dapp (s, List.map spec_dity dl, List.map spec_dity rl)
| Dpur (s,dl) -> Dpur (s, List.map spec_dity dl)
and get_tv v d = try Htv.find hv v with Not_found ->
let nd = dity_fresh () in
(* can't return d, might differ in regions *)
......@@ -245,14 +235,13 @@ let specialize_scheme tvs (argl,res) =
let spec_ity hv hr frz ity =
let rec dity ity = match ity.ity_node with
| Ityreg r -> dreg r
| Ityvar v -> if Mtv.mem v frz.isb_tv then Dutv v else get_tv v
| Ityapp (s,tl,rl) -> Dapp (s, List.map dity tl, List.map dreg rl)
| Itypur (s,tl) -> Dpur (s, List.map dity tl)
| Ityvar (v,_) -> if Mtv.mem v frz.isb_var then Dutv v else get_tv v
| Ityapp (s,tl,rl) -> Dapp (s, List.map dity tl, List.map dity rl)
and get_tv v = try Htv.find hv v with Not_found ->
let nd = dity_fresh () in Htv.add hv v nd; nd
and dreg reg = try Hreg.find hr reg with Not_found ->
let {reg_its = s; reg_args = tl; reg_regs = rl} = reg in
let d = Dapp (s, List.map dity tl, List.map dreg rl) in
let d = Dapp (s, List.map dity tl, List.map dity rl) in
let r = if Mreg.mem reg frz.isb_reg then
Durg (ity_reg reg, d) else dreg_fresh d in
Hreg.add hr reg r; r in
......@@ -272,7 +261,7 @@ let specialize_rs {rs_cty = cty} =
let specialize_ls {ls_args = args; ls_value = res} =
let hv = Htv.create 3 and hr = Hreg.create 3 in
let rec ity ty = match ty.ty_node with
| Tyapp (s,tl) -> ity_app_fresh (restore_its s) (List.map ity tl)
| Tyapp (s,tl) -> ity_app (restore_its s) (List.map ity tl) []
| Tyvar v -> ity_var v in
let spec ty = spec_ity hv hr isb_empty (ity ty) in
List.map spec args, Opt.fold (Util.const spec) dity_bool res
......@@ -390,7 +379,7 @@ let freeze_dvty frozen (argl,res) =
| Dvar { contents = Dval d } -> add l d
| Dvar { contents = Dtvs _ } as d -> d :: l
| Dutv _ as d -> d :: l
| Dapp (_,tl,_) | Dpur (_,tl) -> List.fold_left add l tl in
| Dapp (_,tl,_) -> List.fold_left add l tl in
List.fold_left add (add frozen res) argl
let free_vars frozen (argl,res) =
......@@ -399,7 +388,7 @@ let free_vars frozen (argl,res) =
| Dvar { contents = Dval d } -> add s d
| Dvar { contents = Dtvs v }
| Dutv v -> if is_frozen frozen v then s else Stv.add v s
| Dapp (_,tl,_) | Dpur (_,tl) -> List.fold_left add s tl in
| Dapp (_,tl,_) -> List.fold_left add s tl in
List.fold_left add (add Stv.empty res) argl
let denv_add_mono { frozen = frozen; locals = locals } id dvty =
......@@ -426,7 +415,7 @@ let denv_add_rec denv frozen0 id ((argl,res) as dvty) =
| Dvar { contents = Dval d } -> is_explicit d
| Dvar { contents = Dtvs _ } -> false
| Dutv _ -> true
| Dapp (_,tl,_) | Dpur (_,tl) -> List.for_all is_explicit tl in
| Dapp (_,tl,_) -> List.for_all is_explicit tl in
if List.for_all is_explicit argl && is_explicit res
then denv_add_rec_poly denv frozen0 id dvty
else denv_add_rec_mono denv id dvty
......@@ -848,7 +837,7 @@ let env_empty = {
exception UnboundLabel of string
let find_old pvm (ovm,old) v =
if v.pv_ity.ity_pure then v else
if v.pv_ity.ity_imm then v else
let n = v.pv_vs.vs_name.id_string in
(* if v is top-level, both ov and pv are None.
If v is local, ov and pv must be equal to v.
......@@ -925,6 +914,7 @@ let cty_of_spec env bl dsp dity =
let dsp = get_later env dsp ity in
let _, eff = effect_of_dspec dsp in
let eff = eff_reset_overwritten eff in
let eff = eff_reset eff (ity_freeregs Sreg.empty ity) in
let p = rebase_pre env preold old dsp.ds_pre in
let q = create_post ity dsp.ds_post in
let xq = create_xpost dsp.ds_xpost in
......@@ -976,7 +966,7 @@ and try_cexp uloc env ghost de0 = match de0.de_node with
| DEapp (de1,de2) -> down de1 (expr uloc env de2 :: el)
| DEvar (n,_) -> app (ext_c_sym (get_rs env n)) el
| DErs s -> app (ext_c_sym s) el
| DEls _ when not res.ity_pure ->
| DEls _ when not res.ity_imm ->
Loc.errorm "This expression must have pure type"
| DEls s -> ext_c_pur s el argl res
| _ -> app (cexp uloc env ghost de) el in
......
src/mlw/expr.ml
View file @ ea3387ff
......@@ -166,7 +166,8 @@ let create_projection s v =
let id = id_clone v.pv_vs.vs_name in
let eff = eff_ghostify v.pv_ghost eff_empty in
let tyl = List.map ity_var s.its_ts.ts_args in
let ity = ity_app s tyl s.its_regions in
let rgl = List.map ity_reg s.its_regions in
let ity = ity_app s tyl rgl in
let arg = create_pvsymbol (id_fresh "arg") ity in
let ls = create_fsymbol id [arg.pv_vs.vs_ty] v.pv_vs.vs_ty in
let q = make_post (fs_app ls [t_var arg.pv_vs] v.pv_vs.vs_ty) in
......@@ -191,12 +192,16 @@ let create_constructor ~constr id s fl =
end else if constr < 1 then raise exn;
let argl = List.map (fun a -> a.pv_vs.vs_ty) fl in
let tyl = List.map ity_var s.its_ts.ts_args in
let ity = ity_app s tyl s.its_regions in
let rgl = List.map ity_reg s.its_regions in
let ity = ity_app s tyl rgl in
let ty = ty_of_ity ity in
let ls = create_fsymbol ~constr id argl ty in
let argl = List.map (fun a -> t_var a.pv_vs) fl in
let q = make_post (fs_app ls argl ty) in
let c = create_cty fl [] [q] Mexn.empty Mpv.empty eff_empty ity in
let eff = match ity.ity_node with
| Ityreg r -> eff_reset eff_empty (Sreg.singleton r)
| _ -> eff_empty in
let c = create_cty fl [] [q] Mexn.empty Mpv.empty eff ity in
mk_rs ls.ls_name c (RLls ls) None
let rs_of_ls ls =
......@@ -442,7 +447,7 @@ let e_ghostify gh ({e_effect = eff} as e) =
let c_ghostify gh ({c_cty = cty} as c) =
if cty.cty_effect.eff_ghost || not gh then c else
let el = match c.c_node with Cfun e -> [e] | _ -> [] in
mk_cexp c.c_node (try_effect el cty_ghostify gh cty)
mk_cexp c.c_node (try_effect el Ity.cty_ghostify gh cty)
(* purify expressions *)
......@@ -645,8 +650,8 @@ let e_exec ({c_cty = cty} as c) = match cty.cty_args with
| _::_ as al ->
check_effects cty; check_state cty;
(* no need to check eff_covers since we are completely pure *)
if List.exists (fun a -> not a.pv_ity.ity_pure) al ||
not cty.cty_result.ity_pure then Loc.errorm "This function \
if List.exists (fun a -> not a.pv_ity.ity_imm) al ||
not cty.cty_result.ity_imm then Loc.errorm "This function \
has mutable type signature, it cannot be used as pure";
let ghost = List.exists (fun a -> a.pv_ghost) al in
let effect = eff_bind (Spv.of_list al) cty.cty_effect in
......@@ -667,8 +672,8 @@ let c_app s vl ityl ity =
mk_cexp (Capp (s,vl)) (cty_apply s.rs_cty vl ityl ity)
let c_pur s vl ityl ity =
if not ity.ity_pure then invalid_arg "Expr.c_pur";
let v_args = List.map (create_pvsymbol (id_fresh "u")) ityl in
if not (ity_pure ity) then invalid_arg "Expr.c_pur";
let v_args = List.map (create_pvsymbol ~ghost:false (id_fresh "u")) ityl in
let t_args = List.map (fun v -> t_var v.pv_vs) (vl @ v_args) in
let res = Opt.map (fun _ -> ty_of_ity ity) s.ls_value in
let q = make_post (t_app s t_args res) in
......@@ -871,7 +876,7 @@ let e_raise xs e ity =
(* snapshots, assertions, "any" *)
let e_pure t =
let ity = Opt.fold (fun _ -> ity_of_ty) ity_bool t.t_ty in
let ity = Opt.fold (Util.const ity_of_ty_pure) ity_bool t.t_ty in
let eff = eff_ghostify true (eff_read (t_freepvs Spv.empty t)) in
mk_expr (Epure t) ity eff
......@@ -1099,10 +1104,12 @@ let debug_print_locs = Debug.register_info_flag "print_locs"
~desc:"Print@ locations@ of@ identifiers@ and@ expressions."
let ambig_cty c =
let sarg = List.fold_left (fun s v ->
ity_freeze s v.pv_ity) isb_empty c.cty_args in
let freeze_pv v s = ity_freeze s v.pv_ity in
let sarg = Spv.fold freeze_pv c.cty_effect.eff_reads isb_empty in
let sres = ity_freeze isb_empty c.cty_result in
not (Mtv.set_submap sres.isb_tv sarg.isb_tv)
not (Mtv.set_submap sres.isb_var sarg.isb_var) ||
not (Mtv.set_submap sres.isb_pur
(Mtv.set_union sarg.isb_var sarg.isb_pur))
let ambig_ls s =
let sarg = List.fold_left ty_freevars Stv.empty s.ls_args in
......
src/mlw/ity.ml
View file @ ea3387ff
......@@ -17,14 +17,15 @@ open Term
(** {2 Individual types (first-order types without effects)} *)
type itysymbol = {
its_ts : tysymbol; (** pure "snapshot" type symbol *)
its_privmut : bool; (** private mutable record type *)
its_ts : tysymbol; (** logical type symbol *)
its_privmut : bool; (** private mutable type *)
its_mfields : pvsymbol list; (** mutable record fields *)
its_regions : region list; (** mutable shareable components *)
its_arg_imm : bool list; (** non-updatable type parameters *)
its_regions : region list; (** shareable components *)
its_arg_imm : bool list; (** non-updatable parameters *)
its_arg_exp : bool list; (** exposed type parameters *)
its_arg_vis : bool list; (** non-ghost type parameters *)
its_arg_frz : bool list; (** irreplaceable type parameters *)
its_reg_exp : bool list; (** exposed shareable components *)
its_reg_vis : bool list; (** non-ghost shareable components *)
its_reg_frz : bool list; (** irreplaceable shareable components *)
its_def : ity option; (** type alias *)
......@@ -32,25 +33,23 @@ type itysymbol = {
and ity = {
ity_node : ity_node;
ity_pure : bool;
ity_imm : bool;
ity_tag : Weakhtbl.tag;
}
and ity_node =
| Ityreg of region
(** record with mutable fields and shareable components *)
| Ityapp of itysymbol * ity list * region list
(** immutable type or algebraic type with shareable components *)
| Itypur of itysymbol * ity list
(** pure snapshot of a mutable type *)
| Ityvar of tvsymbol
(** type variable *)
| Ityapp of itysymbol * ity list * ity list
(** immutable type with shareable components *)
| Ityvar of tvsymbol * bool
(** type variable and its purity status *)
and region = {
reg_name : ident;
reg_its : itysymbol;
reg_args : ity list;
reg_regs : region list;
reg_regs : ity list;
}
and pvsymbol = {
......@@ -116,138 +115,145 @@ let ity_compare ity1 ity2 = Pervasives.compare (ity_hash ity1) (ity_hash ity2)
let reg_compare reg1 reg2 = id_compare reg1.reg_name reg2.reg_name
let pv_compare pv1 pv2 = id_compare pv1.pv_vs.vs_name pv2.pv_vs.vs_name
let its_mutable s = s.its_privmut || s.its_mfields <> [] ||
match s.its_def with Some {ity_node = Ityreg _} -> true | _ -> false
let its_impure s = its_mutable s || s.its_regions <> [] ||
match s.its_def with Some ity -> not ity.ity_pure | None -> false
exception NonUpdatable of itysymbol * ity
let check_its_args s tl =
assert (s.its_def = None);
let check_imm acc imm ity =
if imm && not ity.ity_pure then raise (NonUpdatable (s,ity));
acc && ity.ity_pure in
List.fold_left2 check_imm true s.its_arg_imm tl
let check imm ity =
if imm && not ity.ity_imm then raise (NonUpdatable (s,ity)) in
List.iter2 check s.its_arg_imm tl
module Hsity = Hashcons.Make (struct
type t = ity
let equal ity1 ity2 = match ity1.ity_node, ity2.ity_node with
| Ityvar v1, Ityvar v2 -> tv_equal v1 v2
| Ityvar (v1,p1), Ityvar (v2,p2) -> tv_equal v1 v2 && p1 = p2
| Ityreg r1, Ityreg r2 -> reg_equal r1 r2
| Itypur (s1,l1), Itypur (s2,l2) ->
its_equal s1 s2 &&
List.for_all2 ity_equal l1 l2
| Ityapp (s1,l1,r1), Ityapp (s2,l2,r2) ->
its_equal s1 s2 &&
List.for_all2 ity_equal l1 l2 &&
List.for_all2 reg_equal r1 r2
List.for_all2 ity_equal r1 r2
| _ -> false
let hash ity = match ity.ity_node with
| Ityvar v -> tv_hash v
| Ityvar (v,p) ->
Hashcons.combine (tv_hash v) (Hashtbl.hash p)
| Ityreg r -> reg_hash r
| Itypur (s,tl) ->
Hashcons.combine_list ity_hash (its_hash s) tl
| Ityapp (s,tl,rl) ->
Hashcons.combine_list reg_hash
Hashcons.combine_list ity_hash
(Hashcons.combine_list ity_hash (its_hash s) tl) rl
let pure ity = match ity.ity_node with
let immutable ity = match ity.ity_node with
| Ityvar _ -> true
| Ityreg _ -> false
| Itypur (s,tl) -> check_its_args s tl
| Ityapp (s,tl,[]) -> check_its_args s tl
| Ityapp (s,tl,_::_) -> check_its_args s tl && false
| Ityapp (s,tl,rl) ->
check_its_args s tl;
let imm ity = ity.ity_imm in
List.for_all imm tl && List.for_all imm rl
let tag n ity = { ity with
ity_pure = pure ity;
ity_tag = Weakhtbl.create_tag n }
ity_imm = immutable ity;
ity_tag = Weakhtbl.create_tag n }
end)
let mk_ity node = {
ity_node = node;
ity_pure = true;
ity_imm = true;
ity_tag = Weakhtbl.dummy_tag;
}
let mk_reg name s tl rl = {
reg_name = id_register name;
reg_its = s;
reg_args = (ignore (check_its_args s tl); tl);
reg_args = (check_its_args s tl; tl);
reg_regs = rl;
}
let ity_var v = Hsity.hashcons (mk_ity (Ityvar v))
let ity_reg r = Hsity.hashcons (mk_ity (Ityreg r))
let ity_pur_unsafe s tl = Hsity.hashcons (mk_ity (Itypur (s,tl)))
let ity_reg r = Hsity.hashcons (mk_ity (Ityreg r))
let ity_var v = Hsity.hashcons (mk_ity (Ityvar (v,false)))
let ity_var_pure v = Hsity.hashcons (mk_ity (Ityvar (v,true)))
let ity_app_unsafe s tl rl = Hsity.hashcons (mk_ity (Ityapp (s,tl,rl)))
(* immutability and purity *)
let its_immutable s = not s.its_privmut && s.its_mfields = [] &&
match s.its_def with Some {ity_node = Ityreg _} -> false | _ -> true
let its_pure s = its_immutable s && s.its_regions = [] &&
match s.its_def with Some ity -> ity.ity_imm | None -> true
let ity_immutable ity = ity.ity_imm
let rec ity_pure ity = match ity.ity_node with
| Ityreg _ -> false
| Ityapp (_,tl,rl) -> List.for_all ity_pure tl && List.for_all ity_pure rl
| Ityvar (_,p) -> p
let ity_pure ity = ity_immutable ity && ity_pure ity
let rec ity_purify ity = match ity.ity_node with
| Ityreg {reg_its = s; reg_args = tl; reg_regs = rl} | Ityapp (s,tl,rl) ->
ity_app_unsafe s (List.map ity_purify tl) (List.map ity_purify rl)
| Ityvar (v,_) -> ity_var_pure v
let rec ty_of_ity ity = match ity.ity_node with
| Ityreg {reg_its = s; reg_args = tl} | Ityapp (s,tl,_) ->
ty_app s.its_ts (List.map ty_of_ity tl)
| Ityvar (v,_) -> ty_var v
(* generic traversal functions *)
let dfold fn1 fn2 acc l1 l2 =
List.fold_left fn2 (List.fold_left fn1 acc l1) l2
let dfold fn acc l1 l2 =
List.fold_left fn (List.fold_left fn acc l1) l2
let dfold2 fn1 fn2 acc l1 r1 l2 r2 =
List.fold_left2 fn2 (List.fold_left2 fn1 acc l1 r1) l2 r2
let dfold2 fn acc l1 r1 l2 r2 =
List.fold_left2 fn (List.fold_left2 fn acc l1 r1) l2 r2
let ity_fold fnt fnr acc ity = match ity.ity_node with
| Ityapp (_,tl,rl) -> dfold fnt fnr acc tl rl
| Itypur (_,tl) -> List.fold_left fnt acc tl
| Ityreg r -> fnr acc r
let ity_fold fn acc ity = match ity.ity_node with
| Ityreg {reg_args = tl; reg_regs = rl}
| Ityapp (_,tl,rl) -> dfold fn acc tl rl
| Ityvar _ -> acc
let reg_fold fnt fnr acc r = dfold fnt fnr acc r.reg_args r.reg_regs
let reg_fold fn acc reg = dfold fn acc reg.reg_args reg.reg_regs
(* symbol-wise fold *)
let rec ity_s_fold fn acc ity = match ity.ity_node with
| Ityapp (s,_,_) | Itypur (s,_) ->
ity_fold (ity_s_fold fn) (reg_s_fold fn) (fn acc s) ity
| Ityreg r -> reg_s_fold fn acc r
| Ityreg {reg_its = s; reg_args = tl; reg_regs = rl}
| Ityapp (s,tl,rl) -> dfold (ity_s_fold fn) (fn acc s) tl rl
| Ityvar _ -> acc
and reg_s_fold fn acc r =
reg_fold (ity_s_fold fn) (reg_s_fold fn) (fn acc r.reg_its) r
let reg_s_fold fn acc r = reg_fold (ity_s_fold fn) (fn acc r.reg_its) r
(* traversal functions on type variables *)
let rec ity_v_fold fn acc ity = match ity.ity_node with
| Ityapp (_,tl,_) | Itypur (_,tl) | Ityreg {reg_args = tl} ->
| Ityreg {reg_args = tl} | Ityapp (_,tl,_) ->
List.fold_left (ity_v_fold fn) acc tl
| Ityvar v -> fn acc v
| Ityvar (v,_) -> fn acc v
let reg_v_fold fn acc r = List.fold_left (ity_v_fold fn) acc r.reg_args
let ity_freevars s ity = ity_v_fold (fun s v -> Stv.add v s) s ity
let reg_freevars s reg = reg_v_fold (fun s v -> Stv.add v s) s reg
let ity_freevars s ity = ity_v_fold Stv.add_left s ity
let reg_freevars s reg = reg_v_fold Stv.add_left s reg
let ity_v_occurs v ity = Util.any ity_v_fold (tv_equal v) ity
let reg_v_occurs v reg = Util.any reg_v_fold (tv_equal v) reg
let ity_closed ity = Util.all ity_v_fold Util.ffalse ity
(* traversal functions on regions *)
(* traversal functions on top regions *)
let rec ity_r_fold fn acc ity =
if ity.ity_pure then acc else
if ity.ity_imm then acc else
match ity.ity_node with
| Ityapp (_,tl,rl) -> dfold (ity_r_fold fn) acc tl rl
| Ityreg r -> fn acc r
| Ityapp (s,tl,rl) -> its_r_fold fn acc s tl rl
| Itypur (_,tl) ->
(* snapshot types expose all arguments *)
List.fold_left (ity_r_fold fn) acc tl
| Ityvar _ -> assert false
| Ityvar _ -> acc
and its_r_fold fn acc s tl rl =
let add_arg acc exp t = if exp then ity_r_fold fn acc t else acc in
List.fold_left2 add_arg (List.fold_left fn acc rl) s.its_arg_exp tl
let reg_r_fold fn acc reg = reg_fold (ity_r_fold fn) acc reg
let reg_r_fold fn acc reg =
its_r_fold fn acc reg.reg_its reg.reg_args reg.reg_regs
let ity_top_regs regs ity = ity_r_fold Sreg.add_left regs ity
let rec reg_freeregs s reg = reg_r_fold reg_freeregs (Sreg.add reg s) reg
let ity_freeregs s ity = ity_r_fold reg_freeregs s ity
......@@ -256,67 +262,87 @@ let rec reg_r_occurs r reg = reg_equal r reg ||
Util.any reg_r_fold (reg_r_occurs r) reg
let ity_r_occurs r ity = Util.any ity_r_fold (reg_r_occurs r) ity
let rec reg_r_stale rst cvr reg = Sreg.mem reg rst || not (Mreg.mem reg cvr) &&
Util.any reg_r_fold (reg_r_stale rst cvr) reg
let ity_r_stale rst cvr ity = Util.any ity_r_fold (reg_r_stale rst cvr) ity
(* traversal functions on exposed regions *)
let rec ity_exp_fold fn acc ity =
if ity.ity_imm then acc else
match ity.ity_node with
| Ityapp (s,tl,rl) -> its_exp_fold fn acc s tl rl
| Ityreg r -> fn acc r
| Ityvar _ -> acc
and its_exp_fold fn acc s tl rl =
let fn a x t = if x then ity_exp_fold fn a t else a in
dfold2 fn acc s.its_arg_exp tl s.its_reg_exp rl
let reg_exp_fold fn acc reg =
its_exp_fold fn acc reg.reg_its reg.reg_args reg.reg_regs
(* detect exposed type variables and regions *)
let ity_exp_regs regs ity = ity_exp_fold Sreg.add_left regs ity
let rec ity_v_exposed vars ity = match ity.ity_node with
| Ityreg _ -> vars
| Ityapp (s,tl,_) ->
let add_arg vars exp t = if exp then ity_v_exposed vars t else vars in
List.fold_left2 add_arg vars s.its_arg_exp tl
| Itypur (_,tl) ->
(* snapshot types expose all arguments *)
List.fold_left ity_v_exposed vars tl
| Ityvar v -> Stv.add v vars
let rec reg_rch_regs s reg = reg_exp_fold reg_rch_regs (Sreg.add reg s) reg
let ity_rch_regs s ity = ity_exp_fold reg_rch_regs s ity
let ity_r_exposed regs ity = ity_r_fold (fun s r -> Sreg.add r s) regs ity
let reg_r_exposed regs reg = reg_r_fold (fun s r -> Sreg.add r s) regs reg
let rec reg_r_reachable r reg = reg_equal r reg ||
Util.any reg_exp_fold (reg_r_reachable r) reg
let ity_r_reachable r ity = Util.any ity_exp_fold (reg_r_reachable r) ity
(* detect non-ghost type variables and regions *)
let rec reg_r_stale rs cv reg = Sreg.mem reg rs || not (Mreg.mem reg cv) &&
Util.any reg_exp_fold (reg_r_stale rs cv) reg
let ity_r_stale rs cv ity = Util.any ity_exp_fold (reg_r_stale rs cv) ity
let rec ity_visible fnv fnr acc vis ity =
if not vis then acc else
(* traversal functions on non-ghost regions *)
let rec ity_vis_fold fn acc ity =
if ity.ity_imm then acc else
match ity.ity_node with
| Ityreg r ->
reg_visible fnv fnr acc vis r
| Ityapp (s,tl,rl) -> its_vis_fold fn acc s tl rl
| Ityreg r -> reg_vis_fold fn acc r
| Ityvar _ -> acc
and its_vis_fold fn acc s tl rl =
let fn a v t = if v then ity_vis_fold fn a t else a in
dfold2 fn acc s.its_arg_vis tl s.its_reg_vis rl
and reg_vis_fold fn acc reg =
its_exp_fold fn (fn acc reg) reg.reg_its reg.reg_args reg.reg_regs
let ity_vis_regs regs ity = ity_vis_fold Sreg.add_left regs ity
(* collect exposed type variables *)
let rec ity_exp_vars vars ity = match ity.ity_node with
| Ityapp (s,tl,rl) ->
dfold2 (ity_visible fnv fnr) (reg_visible fnv fnr)
acc s.its_arg_vis tl s.its_reg_vis rl
| Itypur (s,tl) ->
(* nothing requires snapshot types to be exclusively ghost,
as we can soundly extract them into the same OCaml types
as the original mutable WhyML types. TODO: verify this *)
List.fold_left2 (ity_visible fnv fnr) acc s.its_arg_vis tl
| Ityvar v -> fnv acc v
and reg_visible fnv fnr acc vis r =
if not vis then acc else
dfold2 (ity_visible fnv fnr) (reg_visible fnv fnr)
(fnr acc r) r.reg_its.its_arg_vis r.reg_args
r.reg_its.its_reg_vis r.reg_regs
let ity_v_visible vars ity =
ity_visible (fun s v -> Stv.add v s) Util.const vars true ity
let ity_r_visible regs ity = if ity.ity_pure then regs else
ity_visible Util.const (fun s r -> Sreg.add r s) regs true ity
(* detect non-updatable type variables *)
let rec ity_v_immutable vars imm ity =
if imm then ity_freevars vars ity else
match ity.ity_node with
| Ityreg {reg_its = s; reg_args = tl}
| Ityapp (s,tl,_) | Itypur (s,tl) ->
List.fold_left2 ity_v_immutable vars s.its_arg_imm tl
let fn a x t = if x then ity_exp_vars a t else a in
dfold2 fn vars s.its_arg_exp tl s.its_reg_exp rl
| Ityvar (v,false) -> Stv.add v vars
| Ityvar (_,true) | Ityreg _ -> vars
(* collect non-ghost type variables *)
let rec ity_vis_vars vars ity = match ity.ity_node with
| Ityreg {reg_its = s; reg_args = tl} | Ityapp (s,tl,_) ->
let fn a v t = if v then ity_vis_vars a t else a in
List.fold_left2 fn vars s.its_arg_vis tl
| Ityvar (v,false) -> Stv.add v vars
| Ityvar (_,true) -> vars
(* collect non-updatable type variables *)
let rec ity_realvars vars ity = match ity.ity_node with
| Ityreg {reg_args = tl} | Ityapp (_,tl,_) ->
List.fold_left ity_realvars vars tl
| Ityvar (v,false) -> Stv.add v vars
| Ityvar (_,true) -> vars
let rec ity_imm_vars vars ity = match ity.ity_node with
| Ityreg {reg_its = s; reg_args = tl} | Ityapp (s,tl,_) ->
let fn a i t = if i then ity_realvars a t
else ity_imm_vars a t in
List.fold_left2 fn vars s.its_arg_imm tl
| Ityvar _ -> vars
let ity_v_immutable vars ity = ity_v_immutable vars false ity
(* smart constructors *)
(* type matching *)
exception BadItyArity of itysymbol * int
exception BadRegArity of itysymbol * int
......@@ -324,13 +350,17 @@ exception BadRegArity of itysymbol * int
exception DuplicateRegion of region
exception UnboundRegion of region
exception ImpureType of tvsymbol * ity
type ity_subst = {
isb_tv : ity Mtv.t;
isb_reg : region Mreg.t;
isb_var : ity Mtv.t;
isb_pur : ity Mtv.t;
isb_reg : ity Mreg.t;
}
let isb_empty = {
isb_tv = Mtv.empty;
isb_var = Mtv.empty;
isb_pur = Mtv.empty;
isb_reg = Mreg.empty;
}
......@@ -343,14 +373,15 @@ let reg_equal_check r1 r2 = if not (reg_equal r1 r2) then
raise (TypeMismatch (ity_reg r1, ity_reg r2, isb_empty))
let ity_full_inst sbs ity =
let freg r = Mreg.find r sbs.isb_reg in
let rec inst ity = match ity.ity_node with
| Ityreg r -> Mreg.find r sbs.isb_reg
| Ityapp (s,tl,rl) ->
ity_app_unsafe s (List.map inst tl) (List.map freg rl)