Commit d7301905 authored by Andrei Paskevich's avatar Andrei Paskevich

drop purified type variables

parent dd7e5df5
......@@ -326,7 +326,7 @@ module Translate = struct
let mlty_of_ity mask t =
let rec loop t = match t.ity_node with
| _ when mask_equal mask MaskGhost -> ML.tunit
| Ityvar (tvs, _) ->
| Ityvar tvs ->
Mltree.Tvar tvs
| Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
let itl = visible_of_mask mask itl in
......
......@@ -60,8 +60,7 @@ let app_map fn s tl rl = Dapp (s, List.map fn tl, List.map fn rl)
let dity_of_ity ity =
let hr = Hreg.create 3 in
let rec dity ity = match ity.ity_node with
| Ityvar (v,false) -> Dutv v
| Ityvar (v,true) -> dity_pur (Dutv v)
| Ityvar v -> Dutv v
| Ityapp (s,tl,rl) -> app_map dity s tl rl
| Ityreg ({reg_its = s; reg_args = tl; reg_regs = rl} as r) ->
try Hreg.find hr r with Not_found ->
......@@ -78,13 +77,12 @@ let rec ity_of_dity = function
let rec refresh ity = match ity.ity_node with
| Ityreg {reg_its = s; reg_args = tl} | Ityapp (s,tl,_) ->
ity_app s (List.map refresh tl) []
| Ityvar (v,_) -> ity_var v in
| Ityvar v -> ity_var v in
let rec dity ity = match ity.ity_node with
| Ityreg r ->
Durg (app_map dity r.reg_its r.reg_args r.reg_regs, r)
| Ityapp (s,tl,rl) -> app_map dity s tl rl
| Ityvar (v,true) -> dity_pur (Dutv v)
| Ityvar (v,false) -> Dutv v in
| Ityvar v -> Dutv v in
let t = refresh (ity_of_dity d) in
r := Dval (dity t); t
| Dvar ({contents = Dreg (Dapp (s,tl,rl) as d,_)} as r) ->
......@@ -132,8 +130,7 @@ let dity_app_fresh s dl =
let hr = Hreg.create 3 in
let rec ity_inst ity = match ity.ity_node with
| Ityreg r -> reg_inst r
| Ityvar (v, false) -> Mtv.find v mv
| Ityvar (v, true) -> dity_pur (Mtv.find v mv)
| Ityvar v -> Mtv.find v mv
| Ityapp (s,tl,rl) -> app_map ity_inst s tl rl
and reg_inst ({reg_its = s; reg_args = tl; reg_regs = rl} as r) =
try Hreg.find hr r with Not_found ->
......@@ -148,10 +145,10 @@ let rec dity_refresh = function
| Dvar {contents = Dtvs _} -> dity_fresh ()
| Dapp (s,dl,_) ->
let d = dity_app_fresh s (List.map dity_refresh dl) in
if its_immutable s then d else dity_reg d
if s.its_mutable then dity_reg d else d
let rec dity_unify_asym d1 d2 = match d1,d2 with
| Durg _, _ | Dutv _, _ -> raise Exit (* we cannot be pure then *)
| Durg _, _ -> raise Exit (* we cannot be pure then *)
| d1, Dvar {contents = (Dval d2|Dpur d2|Dsim (d2,_)|Dreg (d2,_))}
| d1, Durg (d2,_)
| Dvar {contents = Dval d1}, d2 ->
......@@ -175,6 +172,8 @@ let rec dity_unify_asym d1 d2 = match d1,d2 with
let d2 = dity_refresh d in
dity_unify_asym d d2;
r := Dval d2
| Dutv u, Dutv v when tv_equal u v ->
()
| Dapp (s1,dl1,rl1), Dapp (s2,dl2,rl2) when its_equal s1 s2 ->
List.iter2 dity_unify_asym dl1 dl2;
List.iter2 dity_unify_asym rl1 rl2
......@@ -275,7 +274,7 @@ let rec print_dity pur pri fmt = function
| Dapp (s,tl,_) when pur ->
Format.fprintf fmt (protect_on (pri > 1 && tl <> []) "%a%a")
Pretty.print_ts s.its_ts (print_args (print_dity pur 2)) tl
| Dapp (s,tl,rl) when its_immutable s ->
| Dapp (s,tl,rl) when not s.its_mutable ->
Format.fprintf fmt
(protect_on (pri > 1 && (tl <> [] || rl <> [])) "%a%a%a")
Pretty.print_ts s.its_ts (print_args (print_dity pur 2)) tl
......@@ -319,14 +318,10 @@ let spec_ity hv hr frz ity =
let d = app_map dity r.reg_its r.reg_args r.reg_regs in
let nd = if Mreg.mem r frz.isb_reg then Durg (d,r) else dity_reg d in
Hreg.add hr r nd; nd)
| Ityvar (v,pure) ->
let nd = try Htv.find hv v with Not_found ->
let nd =
if Mtv.mem v frz.isb_var then Dutv v else
if Mtv.mem v frz.isb_pur then dity_sim (Dutv v) else
dity_fresh () in
Htv.add hv v nd; nd in
if pure then dity_pur nd else nd
| Ityvar v ->
(try Htv.find hv v with Not_found ->
let nd = if Mtv.mem v frz.isb_var then Dutv v else dity_fresh () in
Htv.add hv v nd; nd)
| Ityapp (s,tl,rl) -> app_map dity s tl rl in
dity ity
......@@ -1021,7 +1016,7 @@ let env_empty = {
exception UnboundLabel of string
let find_old pvm (ovm,old) v =
if v.pv_ity.ity_imm then v else
if v.pv_ity.ity_pure 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.
......
......@@ -772,7 +772,7 @@ let c_app s vl ityl ity =
mk_cexp (Capp (s,vl)) cty
let c_pur s vl ityl ity =
if not (ity_pure ity) then Loc.errorm "This expression must have pure type";
if not ity.ity_pure then Loc.errorm "This expression must have pure type";
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
......@@ -1241,9 +1241,7 @@ let ambig_cty c =
let sarg = List.fold_right freeze_pv c.cty_args isb_empty in
let sarg = Spv.fold freeze_pv c.cty_effect.eff_reads sarg in
let sres = ity_freeze isb_empty c.cty_result in
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))
not (Mtv.set_submap sres.isb_var sarg.isb_var)
let ambig_ls s =
let sarg = List.fold_left ty_freevars Stv.empty s.ls_args in
......
This diff is collapsed.
......@@ -38,7 +38,7 @@ and its_flag = private {
and ity = private {
ity_node : ity_node;
ity_imm : bool;
ity_pure : bool;
ity_tag : Weakhtbl.tag;
}
......@@ -47,8 +47,8 @@ and ity_node = private
(** record with mutable fields and shareable components *)
| Ityapp of itysymbol * ity list * ity list
(** immutable type with shareable components *)
| Ityvar of tvsymbol * bool
(** type variable and its purity status *)
| Ityvar of tvsymbol
(** type variable *)
and region = private {
reg_name : ident;
......@@ -140,18 +140,9 @@ val restore_its : tysymbol -> itysymbol
(* {2 Basic properties} *)
val its_immutable : itysymbol -> bool
(** an immutable type symbol is not a mutable record nor an alias for one *)
val its_pure : itysymbol -> bool
(** a pure type symbol is immutable and has no mutable components *)
val ity_immutable : ity -> bool
(** an immutable type contains no regions (returns the [ity_imm] field) *)
val ity_pure : ity -> bool
(** a pure type is immutable and all type variables in it are pure *)
val ity_closed : ity -> bool
(** a closed type contains no type variables *)
......@@ -182,17 +173,15 @@ val ity_reg : region -> ity
val ity_var : tvsymbol -> ity
val ity_var_pure : tvsymbol -> ity
val ity_purify : ity -> ity
(** replaces regions with pure snapshots and variables with pure variables. *)
(** replaces regions with pure snapshots *)
val ity_of_ty : ty -> ity
(** fresh regions are created when needed and all variables are impure.
(** fresh regions are created when needed.
Raises [Invalid_argument] for any non-its tysymbol. *)
val ity_of_ty_pure : ty -> ity
(** pure snapshots are substituted when needed and all variables are pure.
(** pure snapshots are substituted when needed.
Raises [Invalid_argument] for any non-its tysymbol. *)
val ty_of_ity : ity -> ty
......@@ -268,12 +257,10 @@ val ity_tuple : ity list -> ity
type ity_subst = private {
isb_var : ity Mtv.t;
isb_pur : ity Mtv.t;
isb_reg : ity Mreg.t;
}
exception TypeMismatch of ity * ity * ity_subst
exception ImpureType of tvsymbol * ity
val isb_empty : ity_subst
......@@ -342,6 +329,8 @@ val create_xsymbol : preid -> ?mask:mask -> ity -> xsymbol
exception IllegalSnapshot of ity
exception IllegalAlias of region
exception AssignPrivate of region
exception AssignSnapshot of ity
exception WriteImmutable of region * pvsymbol
exception IllegalUpdate of pvsymbol * region
exception StaleVariable of pvsymbol * region
exception BadGhostWrite of pvsymbol * region
......
......@@ -48,7 +48,7 @@ let check_field stv f =
let ftv = ity_freevars Stv.empty f.pv_ity in
if not (Stv.subset ftv stv) then Loc.error ?loc
(UnboundTypeVar (Stv.choose (Stv.diff ftv stv)));
if not f.pv_ity.ity_imm then Loc.errorm ?loc
if not f.pv_ity.ity_pure then Loc.errorm ?loc
"This field has non-pure type, it cannot be used \
in a recursive type definition"
......@@ -557,7 +557,7 @@ let create_let_decl ld =
let create_exn_decl xs =
if not (ity_closed xs.xs_ity) then Loc.errorm ?loc:xs.xs_name.id_loc
"Top-level exception %a has a polymorphic type" print_xs xs;
if not (ity_immutable xs.xs_ity) then Loc.errorm ?loc:xs.xs_name.id_loc
if not xs.xs_ity.ity_pure then Loc.errorm ?loc:xs.xs_name.id_loc
"The type of top-level exception %a has mutable components" print_xs xs;
mk_decl (PDexn xs) []
......
......@@ -61,7 +61,7 @@ let overload_of_rs {rs_cty = cty} =
| a::al when not a.pv_ghost && List.for_all (same_type a.pv_ity) al ->
let res = cty.cty_result in
if ity_equal res a.pv_ity then SameType else
if ity_closed res && ity_immutable res then FixedRes res else NoOver
if ity_closed res && res.ity_pure then FixedRes res else NoOver
| _ -> NoOver
let same_overload r1 r2 =
......@@ -931,7 +931,7 @@ let clone_type_decl inst cl tdl kn =
private types with no fields and no invariant? *)
let stv = Stv.of_list ts.ts_args in
if not (Stv.subset (ity_freevars Stv.empty ity) stv &&
its_pure s && ity_immutable ity) then raise (BadInstance id);
its_pure s && ity.ity_pure) then raise (BadInstance id);
cl.ty_table <- Mts.add ts ity cl.ty_table
| None -> assert false end end;
Hits.add htd s None;
......
......@@ -252,7 +252,7 @@ let old_of_pv {pv_vs = v; pv_ity = ity} =
let oldify_variant varl =
let fpv = Mpv.mapi_filter (fun v _ -> (* oldify mutable vars *)
if ity_immutable v.pv_ity then None else Some (old_of_pv v))
if v.pv_ity.ity_pure then None else Some (old_of_pv v))
(List.fold_left (fun s (t,_) -> t_freepvs s t) Spv.empty varl) in
if Mpv.is_empty fpv then Mpv.empty, varl else
let o2v = Mpv.fold (fun v o s -> Mpv.add o v s) fpv Mpv.empty in
......@@ -1025,7 +1025,7 @@ let advancement dst0 dst1 =
(* express shared region values as "v.f1.f2.f3" when possible *)
let rec explore_paths kn aff regs t ity =
if ity.ity_imm then regs else
if ity.ity_pure then regs else
match ity.ity_node with
| Ityvar _ -> assert false
| Ityreg r when not (Sreg.mem r aff) -> regs
......@@ -1222,8 +1222,8 @@ let rec sp_expr kn k rdm dst = match k with
let get_wr _ (_, w) m = Mpv.set_union w m in
let wr2 = Mint.fold get_wr sp2 Mpv.empty in
let fresh_wr2 v _ = clone_pv v in
let fresh_rd2 v _ = if ity_immutable v.pv_ity
then None else Some (clone_pv v) in
let fresh_rd2 v _ = if v.pv_ity.ity_pure then None
else Some (clone_pv v) in
let wp1, sp1, rd1 = sp_expr kn k1 (Mint.add i rd2 rdm)
(Mpv.set_union (Mpv.set_union (Mpv.mapi fresh_wr2 wr2)
(Mpv.mapi_filter fresh_rd2 (Mpv.set_diff rd2 dst))) dst) in
......
......@@ -1149,7 +1149,7 @@ let type_inst ({muc_theory = tuc} as muc) ({mod_theory = t} as m) s =
(id_clone ts1.ts_name) tvl (ity_of_pty muc pty) in
let ty2 = ity_app ts2 (List.map ity_var ts1.ts_args) [] in
let check v ty = match ty.ity_node with
| Ityvar (u, _) -> tv_equal u v | _ -> false in
| Ityvar u -> tv_equal u v | _ -> false in
begin match ty2.ity_node with
| Ityapp (ts2, tyl, _) | Ityreg { reg_its = ts2; reg_args = tyl }
when Lists.equal check tvl tyl ->
......
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