Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Delete Jkind_axis.Modal in favor of Mode.Alloc.axis #3409

Merged
merged 6 commits into from
Jan 6, 2025
+169 −171
Merged

Delete Jkind_axis.Modal in favor of Mode.Alloc.axis #3409

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
a111f80
Delete Jkind_axis.Modal in favor of Mode.Alloc.axis
glittershark Dec 23, 2024
6ab8dcd
Simplify modality_is_const_for_axis
glittershark Dec 26, 2024
f5fc400
move more functionality from Jkind_axis to Mode
glittershark Jan 1, 2025
eb56b1c
move the logic for is_constant_for from Mode.Modality to Jkind_axis
glittershark Jan 1, 2025
28e90a4
Clean up packed_value_axis and axis conversion
glittershark Jan 1, 2025
e8310be
print areality as locality
glittershark Jan 4, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 9 additions & 9 deletions typing/jkind.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1204,10 +1204,10 @@ module Jkind_desc = struct
in
let upper_bounds = to_.upper_bounds in
let upper_bounds, added1 =
add_crossing ~axis:(Modal Portability) upper_bounds
add_crossing ~axis:(Modal (Comonadic Portability)) upper_bounds
in
let upper_bounds, added2 =
add_crossing ~axis:(Modal Contention) upper_bounds
add_crossing ~axis:(Modal (Monadic Contention)) upper_bounds
in
{ to_ with upper_bounds }, added1 || added2

Expand Down Expand Up @@ -1613,19 +1613,19 @@ let extract_layout jk = jk.jkind.layout
let get_modal_upper_bounds ~type_equal ~jkind_of_type jk : Alloc.Const.t =
let bounds = jk.jkind.upper_bounds in
{ areality =
Bound.reduce ~axis:(Modal Locality) ~type_equal ~jkind_of_type
Bound.reduce ~axis:(Modal (Comonadic Areality)) ~type_equal ~jkind_of_type
bounds.locality;
linearity =
Bound.reduce ~axis:(Modal Linearity) ~type_equal ~jkind_of_type
bounds.linearity;
Bound.reduce ~axis:(Modal (Comonadic Linearity)) ~type_equal
~jkind_of_type bounds.linearity;
uniqueness =
Bound.reduce ~axis:(Modal Uniqueness) ~type_equal ~jkind_of_type
Bound.reduce ~axis:(Modal (Monadic Uniqueness)) ~type_equal ~jkind_of_type
bounds.uniqueness;
portability =
Bound.reduce ~axis:(Modal Portability) ~type_equal ~jkind_of_type
bounds.portability;
Bound.reduce ~axis:(Modal (Comonadic Portability)) ~type_equal
~jkind_of_type bounds.portability;
contention =
Bound.reduce ~axis:(Modal Contention) ~type_equal ~jkind_of_type
Bound.reduce ~axis:(Modal (Monadic Contention)) ~type_equal ~jkind_of_type
bounds.contention
}

Expand Down
179 changes: 51 additions & 128 deletions typing/jkind_axis.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -109,138 +109,61 @@ module Nullability = struct
end

module Axis = struct
module Modal = struct
type 'a t =
| Locality : Mode.Locality.Const.t t
| Linearity : Mode.Linearity.Const.t t
| Uniqueness : Mode.Uniqueness.Const.t t
| Portability : Mode.Portability.Const.t t
| Contention : Mode.Contention.Const.t t
end

module Nonmodal = struct
type 'a t =
| Externality : Externality.t t
| Nullability : Nullability.t t
end

type 'a t =
| Modal of 'a Modal.t
| Nonmodal of 'a Nonmodal.t
| Modal : ('m, 'a, 'd) Mode.Alloc.axis -> 'a t
| Nonmodal : 'a Nonmodal.t -> 'a t

type packed = Pack : 'a t -> packed

module Accent_lattice (M : Mode_intf.Lattice) = struct
(* A functor to add some convenient functions to modal axes *)
include M

let less_or_equal a b : Misc.Le_result.t =
match le a b, le b a with
| true, true -> Equal
| true, false -> Less
| false, _ -> Not_le

let equal a b = Misc.Le_result.is_equal (less_or_equal a b)
end

let get (type a) : a t -> (module Lattice with type t = a) = function
| Modal Locality ->
(module Accent_lattice (Mode.Locality.Const) : Lattice with type t = a)
| Modal Linearity ->
(module Accent_lattice (Mode.Linearity.Const) : Lattice with type t = a)
| Modal Uniqueness ->
(module Accent_lattice (Mode.Uniqueness.Const) : Lattice with type t = a)
| Modal Portability ->
(module Accent_lattice (Mode.Portability.Const) : Lattice with type t = a)
| Modal Contention ->
(module Accent_lattice (Mode.Contention.Const) : Lattice with type t = a)
| Modal axis -> Mode.Alloc.lattice_of_axis axis
| Nonmodal Externality -> (module Externality : Lattice with type t = a)
| Nonmodal Nullability -> (module Nullability : Lattice with type t = a)

let all =
[ Pack (Modal Locality);
Pack (Modal Uniqueness);
Pack (Modal Linearity);
Pack (Modal Contention);
Pack (Modal Portability);
[ Pack (Modal (Comonadic Areality));
Pack (Modal (Monadic Uniqueness));
Pack (Modal (Comonadic Linearity));
Pack (Modal (Monadic Contention));
Pack (Modal (Comonadic Portability));
Pack (Nonmodal Externality);
Pack (Nonmodal Nullability) ]

let name (type a) : a t -> string = function
| Modal Locality -> "locality"
| Modal Linearity -> "linearity"
| Modal Uniqueness -> "uniqueness"
| Modal Portability -> "portability"
| Modal Contention -> "contention"
| Modal axis -> Format.asprintf "%a" Mode.Alloc.print_axis axis
| Nonmodal Externality -> "externality"
| Nonmodal Nullability -> "nullability"

let is_deep (type a) : a t -> bool = function
| Modal Locality -> true
| Modal Linearity -> true
| Modal Uniqueness -> true
| Modal Portability -> true
| Modal Contention -> true
| Modal (Comonadic Areality) -> true
| Modal (Comonadic Linearity) -> true
| Modal (Monadic Uniqueness) -> true
| Modal (Comonadic Portability) -> true
| Modal (Monadic Contention) -> true
| Nonmodal Externality -> true
| Nonmodal Nullability -> false

(* CR aspsmith: This can get a lot simpler once we unify jkind axes with the axes in
Mode *)
let modality_is_const_for_axis (type a) (t : a t) modality =
let modality_is_const_for_axis (type a) (t : a t)
(modality : Mode.Modality.Value.Const.t) =
match t with
| Nonmodal Nullability | Nonmodal Externality -> false
| Modal axis ->
let atoms = Mode.Modality.Value.Const.to_list modality in
List.exists
(fun (modality : Mode.Modality.t) ->
match axis, modality with
(* Constant modalities *)
| Locality, Atom (Comonadic Areality, Meet_with Global) -> true
| Linearity, Atom (Comonadic Linearity, Meet_with Many) -> true
| Uniqueness, Atom (Monadic Uniqueness, Join_with Aliased) -> true
| Portability, Atom (Comonadic Portability, Meet_with Portable) ->
true
| Contention, Atom (Monadic Contention, Join_with Contended) -> true
(* Modalities which are actually identity *)
| Locality, Atom (Comonadic Areality, Meet_with Local)
| Linearity, Atom (Comonadic Linearity, Meet_with Once)
| Uniqueness, Atom (Monadic Uniqueness, Join_with Unique)
| Portability, Atom (Comonadic Portability, Meet_with Nonportable)
| Contention, Atom (Monadic Contention, Join_with Uncontended) ->
false
(* Modalities which are neither constant nor identiy *)
| Locality, Atom (Comonadic Areality, Meet_with Regional)
| Contention, Atom (Monadic Contention, Join_with Shared) ->
Misc.fatal_error
"Don't yet know how to interpret non-constant, non-identity \
modalities"
(* Modalities which join or meet on an illegal axis *)
| _, Atom (Comonadic _, Join_with _) | _, Atom (Monadic _, Meet_with _)
->
Misc.fatal_error "Illegal modality"
(* Mismatched axes *)
| Locality, Atom (Monadic Uniqueness, _)
| Locality, Atom (Monadic Contention, _)
| Locality, Atom (Comonadic Linearity, _)
| Locality, Atom (Comonadic Portability, _)
| Linearity, Atom (Comonadic Areality, _)
| Linearity, Atom (Monadic Uniqueness, _)
| Portability, Atom (Monadic Uniqueness, _)
| Contention, Atom (Monadic Uniqueness, _)
| Linearity, Atom (Comonadic Portability, _)
| Linearity, Atom (Monadic Contention, _)
| Uniqueness, Atom (Comonadic Areality, _)
| Uniqueness, Atom (Comonadic Linearity, _)
| Uniqueness, Atom (Comonadic Portability, _)
| Contention, Atom (Comonadic Areality, _)
| Contention, Atom (Comonadic Linearity, _)
| Contention, Atom (Comonadic Portability, _)
| Uniqueness, Atom (Monadic Contention, _)
| Portability, Atom (Comonadic Areality, _)
| Portability, Atom (Comonadic Linearity, _)
| Portability, Atom (Monadic Contention, _) ->
false)
atoms
let (P axis) = Mode.Const.Axis.alloc_as_value (P axis) in
let modality = Mode.Modality.Value.Const.proj axis modality in
if Mode.Modality.is_constant modality
then true
else if Mode.Modality.is_id modality
then false
else
Misc.fatal_error
"Don't yet know how to interpret non-constant, non-identity \
modalities"
end

module type Axed = sig
Expand All @@ -261,21 +184,21 @@ module Axis_collection (T : Axed) = struct

let get (type a) ~(axis : a Axis.t) values : (_, _, a) T.t =
match axis with
| Modal Locality -> values.locality
| Modal Linearity -> values.linearity
| Modal Uniqueness -> values.uniqueness
| Modal Portability -> values.portability
| Modal Contention -> values.contention
| Modal (Comonadic Areality) -> values.locality
| Modal (Comonadic Linearity) -> values.linearity
| Modal (Monadic Uniqueness) -> values.uniqueness
| Modal (Comonadic Portability) -> values.portability
| Modal (Monadic Contention) -> values.contention
| Nonmodal Externality -> values.externality
| Nonmodal Nullability -> values.nullability

let set (type a) ~(axis : a Axis.t) values (value : (_, _, a) T.t) =
match axis with
| Modal Locality -> { values with locality = value }
| Modal Linearity -> { values with linearity = value }
| Modal Uniqueness -> { values with uniqueness = value }
| Modal Portability -> { values with portability = value }
| Modal Contention -> { values with contention = value }
| Modal (Comonadic Areality) -> { values with locality = value }
| Modal (Comonadic Linearity) -> { values with linearity = value }
| Modal (Monadic Uniqueness) -> { values with uniqueness = value }
| Modal (Comonadic Portability) -> { values with portability = value }
| Modal (Monadic Contention) -> { values with contention = value }
| Nonmodal Externality -> { values with externality = value }
| Nonmodal Nullability -> { values with nullability = value }

Expand All @@ -289,11 +212,11 @@ module Axis_collection (T : Axed) = struct

let[@inline] f { f } =
let open M.Syntax in
let* locality = f ~axis:Axis.(Modal Locality) in
let* uniqueness = f ~axis:Axis.(Modal Uniqueness) in
let* linearity = f ~axis:Axis.(Modal Linearity) in
let* contention = f ~axis:Axis.(Modal Contention) in
let* portability = f ~axis:Axis.(Modal Portability) in
let* locality = f ~axis:Axis.(Modal (Comonadic Areality)) in
let* uniqueness = f ~axis:Axis.(Modal (Monadic Uniqueness)) in
let* linearity = f ~axis:Axis.(Modal (Comonadic Linearity)) in
let* contention = f ~axis:Axis.(Modal (Monadic Contention)) in
let* portability = f ~axis:Axis.(Modal (Comonadic Portability)) in
let* externality = f ~axis:Axis.(Nonmodal Externality) in
let* nullability = f ~axis:Axis.(Nonmodal Nullability) in
M.return
Expand Down Expand Up @@ -382,11 +305,11 @@ module Axis_collection (T : Axed) = struct
externality;
nullability
} ~combine =
combine (f ~axis:Axis.(Modal Locality) locality)
@@ combine (f ~axis:Axis.(Modal Uniqueness) uniqueness)
@@ combine (f ~axis:Axis.(Modal Linearity) linearity)
@@ combine (f ~axis:Axis.(Modal Contention) contention)
@@ combine (f ~axis:Axis.(Modal Portability) portability)
combine (f ~axis:Axis.(Modal (Comonadic Areality)) locality)
@@ combine (f ~axis:Axis.(Modal (Monadic Uniqueness)) uniqueness)
@@ combine (f ~axis:Axis.(Modal (Comonadic Linearity)) linearity)
@@ combine (f ~axis:Axis.(Modal (Monadic Contention)) contention)
@@ combine (f ~axis:Axis.(Modal (Comonadic Portability)) portability)
@@ combine (f ~axis:Axis.(Nonmodal Externality) externality)
@@ f ~axis:Axis.(Nonmodal Nullability) nullability
end
Expand Down Expand Up @@ -419,11 +342,11 @@ module Axis_collection (T : Axed) = struct
externality = ext2;
nullability = nul2
} ~combine =
combine (f ~axis:Axis.(Modal Locality) loc1 loc2)
@@ combine (f ~axis:Axis.(Modal Uniqueness) uni1 uni2)
@@ combine (f ~axis:Axis.(Modal Linearity) lin1 lin2)
@@ combine (f ~axis:Axis.(Modal Contention) con1 con2)
@@ combine (f ~axis:Axis.(Modal Portability) por1 por2)
combine (f ~axis:Axis.(Modal (Comonadic Areality)) loc1 loc2)
@@ combine (f ~axis:Axis.(Modal (Monadic Uniqueness)) uni1 uni2)
@@ combine (f ~axis:Axis.(Modal (Comonadic Linearity)) lin1 lin2)
@@ combine (f ~axis:Axis.(Modal (Monadic Contention)) con1 con2)
@@ combine (f ~axis:Axis.(Modal (Comonadic Portability)) por1 por2)
@@ combine (f ~axis:Axis.(Nonmodal Externality) ext1 ext2)
@@ f ~axis:Axis.(Nonmodal Nullability) nul1 nul2
end
Expand Down
14 changes: 2 additions & 12 deletions typing/jkind_axis.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,16 +35,6 @@ module Nullability : sig
end

module Axis : sig
(* CR zqian: remove this and use [Mode.Alloc.axis] instead *)
module Modal : sig
type 'a t =
| Locality : Mode.Locality.Const.t t
| Linearity : Mode.Linearity.Const.t t
| Uniqueness : Mode.Uniqueness.Const.t t
| Portability : Mode.Portability.Const.t t
| Contention : Mode.Contention.Const.t t
end

module Nonmodal : sig
type 'a t =
| Externality : Externality.t t
Expand All @@ -53,8 +43,8 @@ module Axis : sig

(** Represents an axis of a jkind *)
type 'a t =
| Modal of 'a Modal.t
| Nonmodal of 'a Nonmodal.t
| Modal : ('m, 'a, 'd) Mode.Alloc.axis -> 'a t
| Nonmodal : 'a Nonmodal.t -> 'a t

type packed = Pack : 'a t -> packed

Expand Down
Loading
Loading