diff --git a/ocaml/lambda/translmode.ml b/ocaml/lambda/translmode.ml index 41b42c06751..b2ed9c9b47a 100644 --- a/ocaml/lambda/translmode.ml +++ b/ocaml/lambda/translmode.ml @@ -29,11 +29,11 @@ let transl_locality_mode_r locality = let transl_alloc_mode_l mode = (* we only take the locality axis *) - Alloc.locality mode |> transl_locality_mode_l + Alloc.proj (Comonadic Areality) mode |> transl_locality_mode_l let transl_alloc_mode_r mode = (* we only take the locality axis *) - Alloc.locality mode |> transl_locality_mode_r + Alloc.proj (Comonadic Areality) mode |> transl_locality_mode_r let transl_modify_mode locality = match Locality.zap_to_floor locality with diff --git a/ocaml/typing/ctype.ml b/ocaml/typing/ctype.ml index 9752f0a9a94..91520386357 100644 --- a/ocaml/typing/ctype.ml +++ b/ocaml/typing/ctype.ml @@ -1583,9 +1583,9 @@ let prim_mode mvar = function put in [mode.ml] *) let with_locality locality m = let m' = Alloc.newvar () in - Locality.equate_exn (Alloc.locality m') locality; - Alloc.submode_exn m' (Alloc.join_with_locality Locality.Const.max m); - Alloc.submode_exn (Alloc.meet_with_locality Locality.Const.min m) m'; + Locality.equate_exn (Alloc.proj (Comonadic Areality) m') locality; + Alloc.submode_exn m' (Alloc.join_with (Comonadic Areality) Locality.Const.max m); + Alloc.submode_exn (Alloc.meet_with (Comonadic Areality) Locality.Const.min m) m'; m' let rec instance_prim_locals locals mvar macc finalret ty = @@ -5578,7 +5578,7 @@ let mode_cross_left env ty mode = now; will return and figure this out later. *) let jkind = type_jkind_purely env ty in let upper_bounds = Jkind.get_modal_upper_bounds jkind in - Alloc.meet_with upper_bounds mode + Alloc.meet_const upper_bounds mode (* CR layouts v2.8: merge with Typecore.expect_mode_cross when [Value] and [Alloc] get unified *) diff --git a/ocaml/typing/env.ml b/ocaml/typing/env.ml index d2e13f91b3d..93016434b91 100644 --- a/ocaml/typing/env.ml +++ b/ocaml/typing/env.ml @@ -2958,7 +2958,7 @@ let lookup_ident_module (type a) (load : a load) ~errors ~use ~loc s env = let escape_mode ~errors ~env ~loc id vmode escaping_context = match Mode.Regionality.submode - (Mode.Value.regionality vmode) + (Mode.Value.proj (Comonadic Areality) vmode) (Mode.Regionality.global) with | Ok () -> () @@ -2969,13 +2969,13 @@ let escape_mode ~errors ~env ~loc id vmode escaping_context = let share_mode ~errors ~env ~loc id vmode shared_context = match Mode.Linearity.submode - (Mode.Value.linearity vmode) + (Mode.Value.proj (Comonadic Linearity) vmode) Mode.Linearity.many with | Error _ -> may_lookup_error errors loc env (Once_value_used_in (id, shared_context)) - | Ok () -> Mode.Value.join [Mode.Value.min_with_uniqueness Mode.Uniqueness.shared; vmode] + | Ok () -> Mode.Value.join [Mode.Value.min_with (Monadic Uniqueness) Mode.Uniqueness.shared; vmode] let closure_mode ~errors ~env ~loc id {Mode.monadic; comonadic} closure_context comonadic0 : Mode.Value.l = @@ -2998,7 +2998,7 @@ let closure_mode ~errors ~env ~loc id {Mode.monadic; comonadic} let exclave_mode ~errors ~env ~loc id vmode = match Mode.Regionality.submode - (Mode.Value.regionality vmode) + (Mode.Value.proj (Comonadic Areality) vmode) Mode.Regionality.regional with | Ok () -> vmode |> Mode.value_to_alloc_r2l |> Mode.alloc_as_value @@ -3962,15 +3962,15 @@ let report_lookup_error _loc env ppf = function | Value_used_in_closure (lid, error, context) -> let e0, e1 = match error with - | `Regionality _ -> "local", "might escape" - | `Linearity _ -> "once", "is many" + | Error (Areality, _) -> "local", "might escape" + | Error (Linearity, _) -> "once", "is many" in fprintf ppf "@[The value %a is %s, so cannot be used \ inside a closure that %s.@]" !print_longident lid e0 e1; begin match error, context with - | `Regionality _, Some Tailcall_argument -> + | Error (Areality, _), Some Tailcall_argument -> fprintf ppf "@.@[Hint: The closure might escape because it \ is an argument to a tail call@]" | _ -> () diff --git a/ocaml/typing/mode.ml b/ocaml/typing/mode.ml index cdd6b3f45cd..6eff3ff6fcf 100644 --- a/ocaml/typing/mode.ml +++ b/ocaml/typing/mode.ml @@ -25,20 +25,6 @@ type nonrec disallowed = disallowed type nonrec equate_step = equate_step -module Axis = struct - type t = - [ `Locality - | `Regionality - | `Uniqueness - | `Linearity ] - - let to_string = function - | `Locality -> "locality" - | `Regionality -> "regionality" - | `Uniqueness -> "uniqueness" - | `Linearity -> "linearity" -end - module Global_flag = struct type t = | Global @@ -288,12 +274,14 @@ module Lattices = struct end) end + type monadic = Uniqueness.t * Unit.t + module Monadic = struct (* CR zqian: the extra unit is to distinguish [Moandic.t] from [Uniqueness.t], in order to eliminate some GADT match cases. There might be smarter ways to do this, but we will very soon replace [unit] with proper [Contention.t] anyway, so this seem like a easy quick fix. *) - type t = Uniqueness.t * Unit.t + type t = monadic let min = Uniqueness.min, Unit.min @@ -371,63 +359,6 @@ module Lattices = struct | Comonadic_with_regionality -> Format.fprintf ppf "Comonadic_with_regionality" - (** ('t, 'r) represents a projection from a product of type ['t] to a element - of type ['r]. *) - type ('t, 'r) axis = - | Areality : ('a comonadic_with, 'a) axis - | Linearity : ('areality comonadic_with, Linearity.t) axis - | Uniqueness : (Monadic_op.t, Uniqueness_op.t) axis - - let print_axis : type t r. _ -> (t, r) axis -> unit = - fun ppf -> function - | Areality -> Format.fprintf ppf "areality" - | Linearity -> Format.fprintf ppf "linearity" - | Uniqueness -> Format.fprintf ppf "uniqueness" - - let eq_axis : - type t r0 r1. (t, r0) axis -> (t, r1) axis -> (r0, r1) Misc.eq option = - fun ax0 ax1 -> - match ax0, ax1 with - | Areality, Areality -> Some Refl - | Linearity, Linearity -> Some Refl - | Uniqueness, Uniqueness -> Some Refl - | (Areality | Linearity | Uniqueness), _ -> None - - let proj : type t r. (t, r) axis -> t -> r = - fun ax t -> - match ax, t with - | Areality, (a, _) -> a - | Linearity, (_, lin) -> lin - | Uniqueness, (uni, ()) -> uni - - let update : type t r. (t, r) axis -> r -> t -> t = - fun ax r t -> - match ax, t with - | Areality, (_, lin) -> r, lin - | Linearity, (area, _) -> area, r - | Uniqueness, (_, ()) -> r, () - - let set_areality : type a0 a1. a1 -> a0 comonadic_with -> a1 comonadic_with = - fun r (_, lin) -> r, lin - - let proj_obj : type t r. (t, r) axis -> t obj -> r obj = - fun ax obj -> - match ax, obj with - | Areality, Comonadic_with_locality -> Locality - | Areality, Comonadic_with_regionality -> Regionality - | Linearity, Comonadic_with_locality -> Linearity - | Linearity, Comonadic_with_regionality -> Linearity - | Uniqueness, Monadic_op -> Uniqueness_op - - let comonadic_with_obj : type a. a obj -> a comonadic_with obj = - fun a0 -> - match a0 with - | Locality -> Comonadic_with_locality - | Regionality -> Comonadic_with_regionality - | Uniqueness_op | Linearity | Monadic_op | Comonadic_with_regionality - | Comonadic_with_locality -> - assert false - let min : type a. a obj -> a = function | Locality -> Locality.min | Regionality -> Regionality.min @@ -536,6 +467,41 @@ end module Lattices_mono = struct include Lattices + module Axis = struct + type ('t, 'r) t = + | Areality : ('a comonadic_with, 'a) t + | Linearity : ('areality comonadic_with, Linearity.t) t + | Uniqueness : (Monadic_op.t, Uniqueness_op.t) t + + let print : type p r. _ -> (p, r) t -> unit = + fun ppf -> function + | Areality -> Format.fprintf ppf "areality" + | Linearity -> Format.fprintf ppf "linearity" + | Uniqueness -> Format.fprintf ppf "uniqueness" + + let eq : type p r0 r1. (p, r0) t -> (p, r1) t -> (r0, r1) Misc.eq option = + fun ax0 ax1 -> + match ax0, ax1 with + | Areality, Areality -> Some Refl + | Linearity, Linearity -> Some Refl + | Uniqueness, Uniqueness -> Some Refl + | (Areality | Linearity | Uniqueness), _ -> None + + let proj : type p r. (p, r) t -> p -> r = + fun ax t -> + match ax, t with + | Areality, (a, _) -> a + | Linearity, (_, lin) -> lin + | Uniqueness, (uni, ()) -> uni + + let update : type p r. (p, r) t -> r -> p -> p = + fun ax r t -> + match ax, t with + | Areality, (_, lin) -> r, lin + | Linearity, (area, _) -> area, r + | Uniqueness, (_, ()) -> r, () + end + type ('a, 'b, 'd) morph = | Id : ('a, 'a, 'd) morph (** identity morphism *) | Meet_with : 'a -> ('a, 'a, 'd * disallowed) morph @@ -546,11 +512,11 @@ module Lattices_mono = struct (** Join the input with the parameter *) | Subtract : 'a -> ('a, 'a, 'd * disallowed) morph (** The left adjoint of [Join_with] *) - | Proj : 't obj * ('t, 'r_) axis -> ('t, 'r_, 'l * 'r) morph + | Proj : 't obj * ('t, 'r_) Axis.t -> ('t, 'r_, 'l * 'r) morph (** Project from a product to an axis *) - | Max_with : ('t, 'r_) axis -> ('r_, 't, disallowed * 'r) morph + | Max_with : ('t, 'r_) Axis.t -> ('r_, 't, disallowed * 'r) morph (** Combine an axis with maxima along other axes *) - | Min_with : ('t, 'r_) axis -> ('r_, 't, 'l * disallowed) morph + | Min_with : ('t, 'r_) Axis.t -> ('r_, 't, 'l * disallowed) morph (** Combine an axis with minima along other axes *) | Map_comonadic : ('a0, 'a1, 'd) morph @@ -683,6 +649,27 @@ module Lattices_mono = struct Map_comonadic f end) + let set_areality : type a0 a1. a1 -> a0 comonadic_with -> a1 comonadic_with = + fun r (_, lin) -> r, lin + + let proj_obj : type t r. (t, r) Axis.t -> t obj -> r obj = + fun ax obj -> + match ax, obj with + | Areality, Comonadic_with_locality -> Locality + | Areality, Comonadic_with_regionality -> Regionality + | Linearity, Comonadic_with_locality -> Linearity + | Linearity, Comonadic_with_regionality -> Linearity + | Uniqueness, Monadic_op -> Uniqueness_op + + let comonadic_with_obj : type a. a obj -> a comonadic_with obj = + fun a0 -> + match a0 with + | Locality -> Comonadic_with_locality + | Regionality -> Comonadic_with_regionality + | Uniqueness_op | Linearity | Monadic_op | Comonadic_with_regionality + | Comonadic_with_locality -> + assert false + let rec src : type a b d. b obj -> (a, b, d) morph -> a obj = fun dst f -> match f with @@ -724,12 +711,12 @@ module Lattices_mono = struct | Proj (src0, ax0), Proj (src1, ax1) -> ( match eq_obj src0 src1 with | Some Refl -> ( - match eq_axis ax0 ax1 with None -> None | Some Refl -> Some Refl) + match Axis.eq ax0 ax1 with None -> None | Some Refl -> Some Refl) | None -> None) | Max_with ax0, Max_with ax1 -> ( - match eq_axis ax0 ax1 with Some Refl -> Some Refl | None -> None) + match Axis.eq ax0 ax1 with Some Refl -> Some Refl | None -> None) | Min_with ax0, Min_with ax1 -> ( - match eq_axis ax0 ax1 with Some Refl -> Some Refl | None -> None) + match Axis.eq ax0 ax1 with Some Refl -> Some Refl | None -> None) | Meet_with c0, Meet_with c1 -> (* This polymorphic equality is correct only if runtime representation uniquely identifies a constant, which could be false. For example, @@ -778,9 +765,9 @@ module Lattices_mono = struct | Meet_with c -> Format.fprintf ppf "meet_%a" (print dst) c | Imply c -> Format.fprintf ppf "imply_%a" (print dst) c | Subtract c -> Format.fprintf ppf "subtract_%a" (print dst) c - | Proj (_, ax) -> Format.fprintf ppf "proj_%a" print_axis ax - | Max_with ax -> Format.fprintf ppf "max_with_%a" print_axis ax - | Min_with ax -> Format.fprintf ppf "min_with_%a" print_axis ax + | Proj (_, ax) -> Format.fprintf ppf "proj_%a" Axis.print ax + | Max_with ax -> Format.fprintf ppf "max_with_%a" Axis.print ax + | Min_with ax -> Format.fprintf ppf "min_with_%a" Axis.print ax | Map_comonadic f -> let dst0 = proj_obj Areality dst in Format.fprintf ppf "map_comonadic(%a)" (print_morph dst0) f @@ -828,9 +815,9 @@ module Lattices_mono = struct | Locality.Local -> Regionality.Local | Locality.Global -> Regionality.Regional - let min_with dst ax a = update ax a (min dst) + let min_with dst ax a = Axis.update ax a (min dst) - let max_with dst ax a = update ax a (max dst) + let max_with dst ax a = Axis.update ax a (max dst) let monadic_to_comonadic_min : type a. a comonadic_with obj -> Monadic_op.t -> a comonadic_with = @@ -862,7 +849,7 @@ module Lattices_mono = struct let f' = apply dst f in f' (g' a) | Id -> a - | Proj (_, ax) -> proj ax a + | Proj (_, ax) -> Axis.proj ax a | Max_with ax -> max_with dst ax a | Min_with ax -> min_with dst ax a | Meet_with c -> meet dst c a @@ -926,13 +913,13 @@ module Lattices_mono = struct | Some m -> Some (compose dst m g1) | None -> None) | Proj (mid, ax), Meet_with c -> - Some (compose dst (Meet_with (proj ax c)) (Proj (mid, ax))) + Some (compose dst (Meet_with (Axis.proj ax c)) (Proj (mid, ax))) | Proj (mid, ax), Join_with c -> - Some (compose dst (Join_with (proj ax c)) (Proj (mid, ax))) + Some (compose dst (Join_with (Axis.proj ax c)) (Proj (mid, ax))) | Proj (_, ax0), Max_with ax1 -> ( - match eq_axis ax0 ax1 with None -> None | Some Refl -> Some Id) + match Axis.eq ax0 ax1 with None -> None | Some Refl -> Some Id) | Proj (_, ax0), Min_with ax1 -> ( - match eq_axis ax0 ax1 with None -> None | Some Refl -> Some Id) + match Axis.eq ax0 ax1 with None -> None | Some Refl -> Some Id) | Proj (mid, ax), Map_comonadic f -> ( let src' = src mid m1 in match ax with @@ -975,28 +962,28 @@ module Lattices_mono = struct Locality_as_regionality) | Map_comonadic f, Join_with c -> let dst0 = proj_obj Areality dst in - let areality = proj Areality c in + let areality = Axis.proj Areality c in Some (compose dst (Join_with (set_areality (min dst0) c)) (Map_comonadic (compose dst0 f (Join_with areality)))) | Map_comonadic f, Meet_with c -> let dst0 = proj_obj Areality dst in - let areality = proj Areality c in + let areality = Axis.proj Areality c in Some (compose dst (Meet_with (set_areality (max dst0) c)) (Map_comonadic (compose dst0 f (Meet_with areality)))) | Map_comonadic f, Imply c -> let dst0 = proj_obj Areality dst in - let areality = proj Areality c in + let areality = Axis.proj Areality c in Some (compose dst (Imply (set_areality (max dst0) c)) (Map_comonadic (compose dst0 f (Imply areality)))) | Map_comonadic f, Subtract c -> let dst0 = proj_obj Areality dst in - let areality = proj Areality c in + let areality = Axis.proj Areality c in Some (compose dst (Subtract (set_areality (min dst0) c)) @@ -1100,6 +1087,12 @@ end module C = Lattices_mono module S = Solvers_polarized (C) +type monadic = C.monadic + +type 'a comonadic_with = 'a C.comonadic_with + +module Axis = C.Axis + type changes = S.changes let undo_changes = S.undo_changes @@ -1109,6 +1102,10 @@ let append_changes : (changes ref -> unit) ref = ref (fun _ -> assert false) let set_append_changes f = append_changes := f +type ('a, 'd) mode_monadic = ('a, 'd) S.Negative.mode + +type ('a, 'd) mode_comonadic = ('a, 'd) S.Positive.mode + (** Representing a single object *) module type Obj = sig type const @@ -1252,8 +1249,6 @@ module Regionality = struct let global = of_const Const.Global let legacy = of_const Const.legacy - - let zap_to_legacy = zap_to_floor end module Linearity = struct @@ -1322,70 +1317,37 @@ module Comonadic_with_regionality = struct end include Common (Obj) - open Obj - type error = - [ `Regionality of Regionality.error - | `Linearity of Linearity.error ] + type error = Error : (Const.t, 'a) C.Axis.t * 'a Solver.error -> error type equate_error = equate_step * error - let regionality m = - S.Positive.via_monotone Regionality.Obj.obj (Proj (Obj.obj, Areality)) m - - let min_with_regionality m = - S.Positive.via_monotone Obj.obj (Min_with Areality) - (S.Positive.disallow_right m) - - let max_with_regionality m = - S.Positive.via_monotone Obj.obj (Max_with Areality) - (S.Positive.disallow_left m) - - let join_with_regionality c m = - S.Positive.via_monotone Obj.obj - (Join_with (C.min_with Obj.obj Areality c)) - (S.Positive.disallow_left m) + open Obj - let meet_with_regionality c m = - S.Positive.via_monotone Obj.obj - (Meet_with (C.max_with Obj.obj Areality c)) - (S.Positive.disallow_right m) + let proj ax m = Solver.via_monotone (C.proj_obj ax obj) (Proj (Obj.obj, ax)) m - let linearity m = - S.Positive.via_monotone Linearity.Obj.obj (Proj (Obj.obj, Linearity)) m + let meet_const c m = + Solver.via_monotone obj (Meet_with c) (Solver.disallow_right m) - let min_with_linearity m = - S.Positive.via_monotone Obj.obj (Min_with Linearity) - (S.Positive.disallow_right m) + let join_const c m = + Solver.via_monotone obj (Join_with c) (Solver.disallow_left m) - let max_with_linearity m = - S.Positive.via_monotone Obj.obj (Max_with Linearity) - (S.Positive.disallow_left m) + let min_with ax m = + Solver.via_monotone Obj.obj (Min_with ax) (Solver.disallow_right m) - let join_with_linearity c m = - S.Positive.via_monotone Obj.obj - (Join_with (C.min_with Obj.obj Linearity c)) - (S.Positive.disallow_left m) + let max_with ax m = + Solver.via_monotone Obj.obj (Max_with ax) (Solver.disallow_left m) - let meet_with_linearity c m = - S.Positive.via_monotone Obj.obj - (Meet_with (C.max_with Obj.obj Linearity c)) - (S.Positive.disallow_right m) + let join_with ax c m = join_const (C.min_with Obj.obj ax c) m - let meet_with c m = - Solver.via_monotone obj (Meet_with c) (Solver.disallow_right m) + let meet_with ax c m = meet_const (C.max_with Obj.obj ax c) m let imply c m = Solver.via_monotone obj (Imply c) (Solver.disallow_left m) - let zap_to_legacy m = - let regionality = regionality m |> Regionality.zap_to_legacy in - let linearity = linearity m |> Linearity.zap_to_legacy in - regionality, linearity - let legacy = of_const Const.legacy (* overriding to report the offending axis *) - let submode_log m0 m1 ~log = + let submode_log m0 m1 ~log : _ result = match submode_log m0 m1 ~log with | Ok () -> Ok () | Error { left = reg0, lin0; right = reg1, lin1 } -> @@ -1393,8 +1355,8 @@ module Comonadic_with_regionality = struct then if Linearity.Const.le lin0 lin1 then assert false - else Error (`Linearity { left = lin0; right = lin1 }) - else Error (`Regionality { left = reg0; right = reg1 }) + else Error (Error (Linearity, { left = lin0; right = lin1 })) + else Error (Error (Areality, { left = reg0; right = reg1 })) let submode a b = try_with_log (submode_log a b) @@ -1418,70 +1380,42 @@ module Comonadic_with_locality = struct end include Common (Obj) - open Obj - type error = - [ `Locality of Locality.error - | `Linearity of Linearity.error ] + type error = Error : (Const.t, 'a) C.Axis.t * 'a Solver.error -> error type equate_error = equate_step * error - let locality m = - S.Positive.via_monotone Locality.Obj.obj (Proj (Obj.obj, Areality)) m - - let min_with_locality m = - S.Positive.via_monotone Obj.obj (Min_with Areality) - (S.Positive.disallow_right m) - - let max_with_locality m = - S.Positive.via_monotone Obj.obj (Max_with Areality) - (S.Positive.disallow_left m) + open Obj - let join_with_locality c m = - S.Positive.via_monotone Obj.obj - (Join_with (C.min_with Obj.obj Areality c)) - (S.Positive.disallow_left m) + let proj ax m = Solver.via_monotone (C.proj_obj ax obj) (Proj (Obj.obj, ax)) m - let meet_with_locality c m = - S.Positive.via_monotone Obj.obj - (Meet_with (C.max_with Obj.obj Areality c)) - (S.Positive.disallow_right m) + let meet_const c m = + Solver.via_monotone obj (Meet_with c) (Solver.disallow_right m) - let linearity m = - S.Positive.via_monotone Linearity.Obj.obj (Proj (Obj.obj, Linearity)) m + let join_const c m = + Solver.via_monotone obj (Join_with c) (Solver.disallow_left m) - let min_with_linearity m = - S.Positive.via_monotone Obj.obj (Min_with Linearity) - (S.Positive.disallow_right m) + let min_with ax m = + Solver.via_monotone Obj.obj (Min_with ax) (Solver.disallow_right m) - let max_with_linearity m = - S.Positive.via_monotone Obj.obj (Max_with Linearity) - (S.Positive.disallow_left m) + let max_with ax m = + Solver.via_monotone Obj.obj (Max_with ax) (Solver.disallow_left m) - let join_with_linearity c m = - S.Positive.via_monotone Obj.obj - (Join_with (C.min_with Obj.obj Linearity c)) - (S.Positive.disallow_left m) + let join_with ax c m = join_const (C.min_with Obj.obj ax c) m - let meet_with_linearity c m = - S.Positive.via_monotone Obj.obj - (Meet_with (C.max_with Obj.obj Linearity c)) - (S.Positive.disallow_right m) + let meet_with ax c m = meet_const (C.max_with Obj.obj ax c) m let zap_to_legacy m = - let locality = locality m |> Locality.zap_to_legacy in - let linearity = linearity m |> Linearity.zap_to_legacy in + let locality = proj Areality m |> Locality.zap_to_legacy in + let linearity = proj Linearity m |> Linearity.zap_to_legacy in locality, linearity - let meet_with c m = - Solver.via_monotone obj (Meet_with c) (Solver.disallow_right m) - let imply c m = Solver.via_monotone obj (Imply c) (Solver.disallow_left m) let legacy = of_const Const.legacy (* overriding to report the offending axis *) - let submode_log m0 m1 ~log = + let submode_log m0 m1 ~log : _ result = match submode_log m0 m1 ~log with | Ok () -> Ok () | Error { left = loc0, lin0; right = loc1, lin1 } -> @@ -1489,8 +1423,8 @@ module Comonadic_with_locality = struct then if Linearity.Const.le lin0 lin1 then assert false - else Error (`Linearity { left = lin0; right = lin1 }) - else Error (`Locality { left = loc0; right = loc1 }) + else Error (Error (Linearity, { left = lin0; right = lin1 })) + else Error (Error (Areality, { left = loc0; right = loc1 })) let submode a b = try_with_log (submode_log a b) @@ -1499,8 +1433,8 @@ module Comonadic_with_locality = struct (** overriding to check per-axis *) let check_const m = - let locality = Locality.check_const (locality m) in - let linearity = Linearity.check_const (linearity m) in + let locality = Locality.check_const (proj Areality m) in + let linearity = Linearity.check_const (proj Linearity m) in locality, linearity end @@ -1518,56 +1452,51 @@ module Monadic = struct end include Common (Obj) - open Obj - type error = [`Uniqueness of Uniqueness.error] + type error = Error : (Const.t, 'a) C.Axis.t * 'a Solver.error -> error type equate_error = equate_step * error - let uniqueness m = - S.Negative.via_monotone Uniqueness.Obj.obj (Proj (Obj.obj, Uniqueness)) m + open Obj + + let proj ax m = Solver.via_monotone (C.proj_obj ax obj) (Proj (Obj.obj, ax)) m (* The monadic fragment is inverted. Most of the inversion logic is taken care by [Solver_polarized], but some remain, such as the [Min_with] below which is inverted from [Max_with]. *) - let max_with_uniqueness m = - S.Negative.via_monotone Obj.obj (Min_with Uniqueness) - (S.Negative.disallow_left m) + let meet_const c m = + Solver.via_monotone obj (Join_with c) (Solver.disallow_right m) - let min_with_uniqueness m = - S.Negative.via_monotone Obj.obj (Max_with Uniqueness) - (S.Negative.disallow_right m) + let join_const c m = + Solver.via_monotone obj (Meet_with c) (Solver.disallow_left m) - let join_with_uniqueness c m = - S.Negative.via_monotone Obj.obj - (Meet_with (C.max_with Obj.obj Uniqueness c)) - (S.Negative.disallow_left m) + let max_with ax m = + Solver.via_monotone Obj.obj (Min_with ax) (Solver.disallow_left m) - let meet_with_uniqueness c m = - S.Negative.via_monotone Obj.obj - (Join_with (C.min_with Obj.obj Uniqueness c)) - (S.Negative.disallow_right m) + let min_with ax m = + Solver.via_monotone Obj.obj (Max_with ax) (Solver.disallow_right m) - let meet_with c m = - Solver.via_monotone obj (Join_with c) (Solver.disallow_right m) + let join_with ax c m = join_const (C.max_with Obj.obj ax c) m + + let meet_with ax c m = meet_const (C.min_with Obj.obj ax c) m let imply c m = Solver.via_monotone obj (Subtract c) (Solver.disallow_left m) let zap_to_legacy m = - let uniqueness = uniqueness m |> Uniqueness.zap_to_legacy in + let uniqueness = proj Uniqueness m |> Uniqueness.zap_to_legacy in uniqueness, () let legacy = of_const Const.legacy (* overriding to report the offending axis *) - let submode_log m0 m1 ~log = + let submode_log m0 m1 ~log : _ result = match submode_log m0 m1 ~log with | Ok () -> Ok () | Error { left = uni0, (); right = uni1, () } -> if Uniqueness.Const.le uni0 uni1 then assert false - else Error (`Uniqueness { left = uni0; right = uni1 }) + else Error (Error (Uniqueness, { left = uni0; right = uni1 })) let submode a b = try_with_log (submode_log a b) @@ -1576,8 +1505,8 @@ module Monadic = struct (** overriding to check per-axis *) let check_const m = - let uniqueness = Uniqueness.check_const (uniqueness m) in - uniqueness + let uniqueness = Uniqueness.check_const (proj Uniqueness m) in + uniqueness, () end type ('mo, 'como) monadic_comonadic = @@ -1597,18 +1526,88 @@ module Value = struct type lr = (allowed * allowed) t + type ('m, 'a, 'd) axis = + | Monadic : + (Monadic.Const.t, 'a) Axis.t + -> (('a, 'd) mode_monadic, 'a, 'd) axis + | Comonadic : + (Comonadic.Const.t, 'a) Axis.t + -> (('a, 'd) mode_comonadic, 'a, 'd) axis + type ('a, 'b, 'c) modes = { regionality : 'a; linearity : 'b; uniqueness : 'c } + let split { regionality; linearity; uniqueness } = + let monadic = uniqueness, () in + let comonadic = regionality, linearity in + { comonadic; monadic } + + let merge { comonadic; monadic } = + let regionality, linearity = comonadic in + let uniqueness, () = monadic in + { regionality; linearity; uniqueness } + + let print_raw ?verbose () ppf { monadic; comonadic } = + Format.fprintf ppf "%a,%a" + (Comonadic.print_raw ?verbose ()) + comonadic + (Monadic.print_raw ?verbose ()) + monadic + + let print ?verbose () ppf { monadic; comonadic } = + Format.fprintf ppf "%a,%a" + (Comonadic.print ?verbose ()) + comonadic + (Monadic.print ?verbose ()) + monadic + + let of_const c = + let { monadic; comonadic } = split c in + let comonadic = Comonadic.of_const comonadic in + let monadic = Monadic.of_const monadic in + { comonadic; monadic } + + module Const = struct + type t = (Regionality.Const.t, Linearity.Const.t, Uniqueness.Const.t) modes + + module Monadic = Monadic.Const + module Comonadic = Comonadic.Const + + let min = merge { comonadic = Comonadic.min; monadic = Monadic.min } + + let max = merge { comonadic = Comonadic.max; monadic = Monadic.max } + + let le m0 m1 = + let m0 = split m0 in + let m1 = split m1 in + Comonadic.le m0.comonadic m1.comonadic && Monadic.le m0.monadic m1.monadic + + let print ppf m = print_raw () ppf (of_const m) + + let legacy = + merge { comonadic = Comonadic.legacy; monadic = Monadic.legacy } + + let meet m0 m1 = + let m0 = split m0 in + let m1 = split m1 in + let monadic = Monadic.meet m0.monadic m1.monadic in + let comonadic = Comonadic.meet m0.comonadic m1.comonadic in + merge { monadic; comonadic } + + let join m0 m1 = + let m0 = split m0 in + let m1 = split m1 in + let monadic = Monadic.join m0.monadic m1.monadic in + let comonadic = Comonadic.join m0.comonadic m1.comonadic in + merge { monadic; comonadic } + end + let min = { comonadic = Comonadic.min; monadic = Monadic.min } - let max = - { comonadic = Comonadic.max; - monadic = Monadic.max |> Monadic.allow_left |> Monadic.allow_right - } + let max = { comonadic = Comonadic.max; monadic = Monadic.max } include Magic_allow_disallow (struct type (_, _, 'd) sided = 'd t constraint 'd = 'l * 'r @@ -1649,28 +1648,19 @@ module Value = struct let monadic, b1 = Monadic.newvar_below monadic in { monadic; comonadic }, b0 || b1 - let uniqueness { monadic; _ } = Monadic.uniqueness monadic - - let linearity { comonadic; _ } = Comonadic.linearity comonadic - - let regionality { comonadic; _ } = Comonadic.regionality comonadic - - type error = - [ `Regionality of Regionality.error - | `Uniqueness of Uniqueness.error - | `Linearity of Linearity.error ] + type error = Error : ('m, 'a, 'd) axis * 'a Solver.error -> error type equate_error = equate_step * error let submode_log { monadic = monadic0; comonadic = comonadic0 } - { monadic = monadic1; comonadic = comonadic1 } ~log = + { monadic = monadic1; comonadic = comonadic1 } ~log : (_, error) result = (* comonadic before monadic, so that locality errors dominate (error message backward compatibility) *) match Comonadic.submode_log comonadic0 comonadic1 ~log with - | Error e -> Error e + | Error (Error (ax, e)) -> Error (Error (Comonadic ax, e)) | Ok () -> ( match Monadic.submode_log monadic0 monadic1 ~log with - | Error e -> Error e + | Error (Error (ax, e)) -> Error (Error (Monadic ax, e)) | Ok () -> Ok ()) let submode a b = try_with_log (submode_log a b) @@ -1685,109 +1675,91 @@ module Value = struct let equate_exn m0 m1 = match equate m0 m1 with Ok () -> () | Error _ -> invalid_arg "equate_exn" - let print_raw ?verbose () ppf { monadic; comonadic } = - Format.fprintf ppf "%a,%a" - (Comonadic.print_raw ?verbose ()) - comonadic - (Monadic.print_raw ?verbose ()) - monadic - - let print ?verbose () ppf { monadic; comonadic } = - Format.fprintf ppf "%a,%a" - (Comonadic.print ?verbose ()) - comonadic - (Monadic.print ?verbose ()) - monadic - - let zap_to_floor { comonadic; monadic } = - match Monadic.zap_to_floor monadic, Comonadic.zap_to_floor comonadic with - | (uniqueness, ()), (regionality, linearity) -> - { regionality; linearity; uniqueness } - - let zap_to_ceil { comonadic; monadic } = - match Monadic.zap_to_ceil monadic, Comonadic.zap_to_ceil comonadic with - | (uniqueness, ()), (regionality, linearity) -> - { regionality; linearity; uniqueness } - - let zap_to_legacy { comonadic; monadic } = - match Monadic.zap_to_legacy monadic, Comonadic.zap_to_legacy comonadic with - | (uniqueness, ()), (regionality, linearity) -> - { regionality; linearity; uniqueness } - - let of_const { regionality; linearity; uniqueness } = - let comonadic = Comonadic.of_const (regionality, linearity) in - let monadic = Monadic.of_const (uniqueness, ()) in - { comonadic; monadic } - let legacy = let comonadic = Comonadic.legacy in let monadic = Monadic.legacy in { comonadic; monadic } - let max_with_uniqueness uniqueness = + let proj_monadic ax { monadic; _ } = Monadic.proj ax monadic + + let proj_comonadic ax { comonadic; _ } = Comonadic.proj ax comonadic + + let proj : type m a l r. (m, a, l * r) axis -> (l * r) t -> m = + fun ax m -> + match ax with + | Monadic ax -> proj_monadic ax m + | Comonadic ax -> proj_comonadic ax m + + let max_with_monadic ax m = let comonadic = Comonadic.max |> Comonadic.disallow_left |> Comonadic.allow_right in - let monadic = Monadic.max_with_uniqueness uniqueness in + let monadic = Monadic.max_with ax m in + { comonadic; monadic } + + let max_with_comonadic ax m = + let comonadic = Comonadic.max_with ax m in + let monadic = Monadic.max |> Monadic.disallow_left |> Monadic.allow_right in { comonadic; monadic } - let min_with_uniqueness uniqueness = + let max_with : type m a l r. (m, a, l * r) axis -> m -> (disallowed * r) t = + fun ax m -> + match ax with + | Monadic ax -> max_with_monadic ax m + | Comonadic ax -> max_with_comonadic ax m + + let min_with_monadic ax m = let comonadic = Comonadic.min |> Comonadic.disallow_right |> Comonadic.allow_left in - let monadic = Monadic.min_with_uniqueness uniqueness in + let monadic = Monadic.min_with ax m in { comonadic; monadic } - let join_with_uniqueness c { monadic; comonadic } = - let comonadic = Comonadic.disallow_left comonadic in - let monadic = Monadic.join_with_uniqueness c monadic in - { monadic; comonadic } - - let meet_with_uniqueness c { monadic; comonadic } = - let comonadic = Comonadic.disallow_right comonadic in - let monadic = Monadic.meet_with_uniqueness c monadic in - { monadic; comonadic } - - let min_with_regionality regionality = - let comonadic = Comonadic.min_with_regionality regionality in + let min_with_comonadic ax m = + let comonadic = Comonadic.min_with ax m in let monadic = Monadic.min |> Monadic.disallow_right |> Monadic.allow_left in { comonadic; monadic } - let max_with_regionality regionality = - let comonadic = Comonadic.max_with_regionality regionality in - let monadic = Monadic.max |> Monadic.disallow_left |> Monadic.allow_right in - { comonadic; monadic } + let min_with : type m a l r. (m, a, l * r) axis -> m -> (l * disallowed) t = + fun ax m -> + match ax with + | Monadic ax -> min_with_monadic ax m + | Comonadic ax -> min_with_comonadic ax m - let meet_with_regionality c { monadic; comonadic } = - let monadic = Monadic.disallow_right monadic in - let comonadic = Comonadic.meet_with_regionality c comonadic in - { comonadic; monadic } + let join_with_monadic ax c { monadic; comonadic } = + let comonadic = Comonadic.disallow_left comonadic in + let monadic = Monadic.join_with ax c monadic in + { monadic; comonadic } - let join_with_regionality c { monadic; comonadic } = + let join_with_comonadic ax c { monadic; comonadic } = let monadic = Monadic.disallow_left monadic in - let comonadic = Comonadic.join_with_regionality c comonadic in + let comonadic = Comonadic.join_with ax c comonadic in { comonadic; monadic } - let min_with_linearity linearity = - let comonadic = Comonadic.min_with_linearity linearity in - let monadic = Monadic.min |> Monadic.disallow_right |> Monadic.allow_left in - { comonadic; monadic } + let join_with : + type m a d l r. (m, a, d) axis -> a -> (l * r) t -> (disallowed * r) t = + fun ax c m -> + match ax with + | Monadic ax -> join_with_monadic ax c m + | Comonadic ax -> join_with_comonadic ax c m - let max_with_linearity linearity = - let comonadic = Comonadic.max_with_linearity linearity in - let monadic = Monadic.max |> Monadic.disallow_left |> Monadic.allow_right in - { comonadic; monadic } - - let join_with_linearity c { monadic; comonadic } = - let monadic = Monadic.disallow_left monadic in - let comonadic = Comonadic.join_with_linearity c comonadic in - { comonadic; monadic } + let meet_with_monadic ax c { monadic; comonadic } = + let comonadic = Comonadic.disallow_right comonadic in + let monadic = Monadic.meet_with ax c monadic in + { monadic; comonadic } - let meet_with_linearity c { monadic; comonadic } = + let meet_with_comonadic ax c { monadic; comonadic } = let monadic = Monadic.disallow_right monadic in - let comonadic = Comonadic.meet_with_linearity c comonadic in + let comonadic = Comonadic.meet_with ax c comonadic in { comonadic; monadic } + let meet_with : + type m a d l r. (m, a, d) axis -> a -> (l * r) t -> (l * disallowed) t = + fun ax c m -> + match ax with + | Monadic ax -> meet_with_monadic ax c m + | Comonadic ax -> meet_with_comonadic ax c m + let join l = let como, mo = List.fold_left @@ -1814,65 +1786,14 @@ module Value = struct S.Negative.via_antitone Monadic.Obj.obj (Comonadic_to_monadic Comonadic.Obj.obj) m - module Const = struct - type t = (Regionality.Const.t, Linearity.Const.t, Uniqueness.Const.t) modes - - let split { regionality; linearity; uniqueness } = - let monadic = uniqueness, () in - let comonadic = regionality, linearity in - { comonadic; monadic } - - let _merge { comonadic; monadic } = - let regionality, linearity = comonadic in - let uniqueness, () = monadic in - { regionality; linearity; uniqueness } - - let min = - { regionality = Regionality.Const.min; - linearity = Linearity.Const.min; - uniqueness = Uniqueness.Const.min - } - - let max = - { regionality = Regionality.Const.max; - linearity = Linearity.Const.max; - uniqueness = Uniqueness.Const.max - } - - let le m0 m1 = - Regionality.Const.le m0.regionality m1.regionality - && Uniqueness.Const.le m0.uniqueness m1.uniqueness - && Linearity.Const.le m0.linearity m1.linearity - - let print ppf m = print_raw () ppf (of_const m) - - let legacy = - { regionality = Regionality.Const.legacy; - linearity = Linearity.Const.legacy; - uniqueness = Uniqueness.Const.legacy - } - - let meet m0 m1 = - let regionality = Regionality.Const.meet m0.regionality m1.regionality in - let linearity = Linearity.Const.meet m0.linearity m1.linearity in - let uniqueness = Uniqueness.Const.meet m0.uniqueness m1.uniqueness in - { regionality; linearity; uniqueness } - - let join m0 m1 = - let regionality = Regionality.Const.join m0.regionality m1.regionality in - let linearity = Linearity.Const.join m0.linearity m1.linearity in - let uniqueness = Uniqueness.Const.join m0.uniqueness m1.uniqueness in - { regionality; linearity; uniqueness } - end - - let meet_with c { comonadic; monadic } = - let c = Const.split c in - let comonadic = Comonadic.meet_with c.comonadic comonadic in - let monadic = Monadic.meet_with c.monadic monadic in + let meet_const c { comonadic; monadic } = + let c = split c in + let comonadic = Comonadic.meet_const c.comonadic comonadic in + let monadic = Monadic.meet_const c.monadic monadic in { monadic; comonadic } let imply c { comonadic; monadic } = - let c = Const.split c in + let c = split c in let comonadic = Comonadic.imply c.comonadic comonadic in let monadic = Monadic.imply c.monadic monadic in { monadic; comonadic } @@ -1906,12 +1827,30 @@ module Alloc = struct type lr = (allowed * allowed) t + type ('m, 'a, 'd) axis = + | Monadic : + (Monadic.Const.t, 'a) Axis.t + -> (('a, 'd) mode_monadic, 'a, 'd) axis + | Comonadic : + (Comonadic.Const.t, 'a) Axis.t + -> (('a, 'd) mode_comonadic, 'a, 'd) axis + type ('a, 'b, 'c) modes = { locality : 'a; linearity : 'b; uniqueness : 'c } + let split { locality; linearity; uniqueness } = + let monadic = uniqueness, () in + let comonadic = locality, linearity in + { comonadic; monadic } + + let merge { comonadic; monadic } = + let locality, linearity = comonadic in + let uniqueness, () = monadic in + { locality; linearity; uniqueness } + let min = { comonadic = Comonadic.min; monadic = Monadic.min } let max = { comonadic = Comonadic.min; monadic = Monadic.max } @@ -1955,26 +1894,17 @@ module Alloc = struct let monadic, b1 = Monadic.newvar_below monadic in { monadic; comonadic }, b0 || b1 - let uniqueness { monadic; _ } = Monadic.uniqueness monadic - - let linearity { comonadic; _ } = Comonadic.linearity comonadic - - let locality { comonadic; _ } = Comonadic.locality comonadic - - type error = - [ `Locality of Locality.error - | `Uniqueness of Uniqueness.error - | `Linearity of Linearity.error ] + type error = Error : ('m, 'a, 'd) axis * 'a Solver.error -> error type equate_error = equate_step * error let submode_log { monadic = monadic0; comonadic = comonadic0 } - { monadic = monadic1; comonadic = comonadic1 } ~log = + { monadic = monadic1; comonadic = comonadic1 } ~log : (_, error) result = match Monadic.submode_log monadic0 monadic1 ~log with - | Error e -> Error e + | Error (Error (ax, e)) -> Error (Error (Monadic ax, e)) | Ok () -> ( match Comonadic.submode_log comonadic0 comonadic1 ~log with - | Error e -> Error e + | Error (Error (ax, e)) -> Error (Error (Comonadic ax, e)) | Ok () -> Ok ()) let submode a b = try_with_log (submode_log a b) @@ -2013,70 +1943,86 @@ module Alloc = struct on modes numerically, instead of defining symbolic functions *) (* type const = (LR.Const.t, Linearity.Const.t, Uniqueness.Const.t) modes *) - let max_with_uniqueness uniqueness = + let proj_monadic ax { monadic; _ } = Monadic.proj ax monadic + + let proj_comonadic ax { comonadic; _ } = Comonadic.proj ax comonadic + + let proj : type m a l r. (m, a, l * r) axis -> (l * r) t -> m = + fun ax m -> + match ax with + | Monadic ax -> proj_monadic ax m + | Comonadic ax -> proj_comonadic ax m + + let max_with_monadic ax m = let comonadic = Comonadic.max |> Comonadic.disallow_left |> Comonadic.allow_right in - let monadic = Monadic.max_with_uniqueness uniqueness in + let monadic = Monadic.max_with ax m in { comonadic; monadic } - let min_with_uniqueness uniqueness = + let max_with_comonadic ax m = + let comonadic = Comonadic.max_with ax m in + let monadic = Monadic.max |> Monadic.disallow_left |> Monadic.allow_right in + { comonadic; monadic } + + let max_with : type m a l r. (m, a, l * r) axis -> m -> (disallowed * r) t = + fun ax m -> + match ax with + | Monadic ax -> max_with_monadic ax m + | Comonadic ax -> max_with_comonadic ax m + + let min_with_monadic ax m = let comonadic = Comonadic.min |> Comonadic.disallow_right |> Comonadic.allow_left in - let monadic = Monadic.min_with_uniqueness uniqueness in + let monadic = Monadic.min_with ax m in { comonadic; monadic } - let join_with_uniqueness c { monadic; comonadic } = - let comonadic = Comonadic.disallow_left comonadic in - let monadic = Monadic.join_with_uniqueness c monadic in - { monadic; comonadic } - - let meet_with_uniqueness c { monadic; comonadic } = - let comonadic = Comonadic.disallow_right comonadic in - let monadic = Monadic.meet_with_uniqueness c monadic in - { monadic; comonadic } - - let min_with_locality locality = - let comonadic = Comonadic.min_with_locality locality in + let min_with_comonadic ax m = + let comonadic = Comonadic.min_with ax m in let monadic = Monadic.min |> Monadic.disallow_right |> Monadic.allow_left in { comonadic; monadic } - let max_with_locality locality = - let comonadic = Comonadic.max_with_locality locality in - let monadic = Monadic.max |> Monadic.disallow_left |> Monadic.allow_right in - { comonadic; monadic } + let min_with : type m a l r. (m, a, l * r) axis -> m -> (l * disallowed) t = + fun ax m -> + match ax with + | Monadic ax -> min_with_monadic ax m + | Comonadic ax -> min_with_comonadic ax m - let meet_with_locality c { monadic; comonadic } = - let monadic = Monadic.disallow_right monadic in - let comonadic = Comonadic.meet_with_locality c comonadic in - { comonadic; monadic } + let join_with_monadic ax c { monadic; comonadic } = + let comonadic = Comonadic.disallow_left comonadic in + let monadic = Monadic.join_with ax c monadic in + { monadic; comonadic } - let join_with_locality c { monadic; comonadic } = + let join_with_comonadic ax c { monadic; comonadic } = let monadic = Monadic.disallow_left monadic in - let comonadic = Comonadic.join_with_locality c comonadic in + let comonadic = Comonadic.join_with ax c comonadic in { comonadic; monadic } - let min_with_linearity linearity = - let comonadic = Comonadic.min_with_linearity linearity in - let monadic = Monadic.min |> Monadic.disallow_right |> Monadic.allow_left in - { comonadic; monadic } + let join_with : + type m a d l r. (m, a, d) axis -> a -> (l * r) t -> (disallowed * r) t = + fun ax c m -> + match ax with + | Monadic ax -> join_with_monadic ax c m + | Comonadic ax -> join_with_comonadic ax c m - let max_with_linearity linearity = - let comonadic = Comonadic.max_with_linearity linearity in - let monadic = Monadic.max |> Monadic.disallow_left |> Monadic.allow_right in - { comonadic; monadic } - - let join_with_linearity c { monadic; comonadic } = - let monadic = Monadic.disallow_left monadic in - let comonadic = Comonadic.join_with_linearity c comonadic in - { comonadic; monadic } + let meet_with_monadic ax c { monadic; comonadic } = + let comonadic = Comonadic.disallow_right comonadic in + let monadic = Monadic.meet_with ax c monadic in + { monadic; comonadic } - let meet_with_linearity c { monadic; comonadic } = + let meet_with_comonadic ax c { monadic; comonadic } = let monadic = Monadic.disallow_right monadic in - let comonadic = Comonadic.meet_with_linearity c comonadic in + let comonadic = Comonadic.meet_with ax c comonadic in { comonadic; monadic } + let meet_with : + type m a d l r. (m, a, d) axis -> a -> (l * r) t -> (l * disallowed) t = + fun ax c m -> + match ax with + | Monadic ax -> meet_with_monadic ax c m + | Comonadic ax -> meet_with_comonadic ax c m + let join l = let como, mo = List.fold_left @@ -2111,42 +2057,36 @@ module Alloc = struct module Const = struct type t = (Locality.Const.t, Linearity.Const.t, Uniqueness.Const.t) modes - let min = - let locality = Locality.Const.min in - let linearity = Linearity.Const.min in - let uniqueness = Uniqueness.Const.min in - { locality; linearity; uniqueness } + module Monadic = Monadic.Const + module Comonadic = Comonadic.Const - let max = - let locality = Locality.Const.max in - let linearity = Linearity.Const.max in - let uniqueness = Uniqueness.Const.max in - { locality; linearity; uniqueness } + let min = merge { comonadic = Comonadic.min; monadic = Monadic.min } + + let max = merge { comonadic = Comonadic.max; monadic = Monadic.max } let le m0 m1 = - Locality.Const.le m0.locality m1.locality - && Uniqueness.Const.le m0.uniqueness m1.uniqueness - && Linearity.Const.le m0.linearity m1.linearity + let m0 = split m0 in + let m1 = split m1 in + Comonadic.le m0.comonadic m1.comonadic && Monadic.le m0.monadic m1.monadic let print ppf m = print_raw () ppf (of_const m) let legacy = - let locality = Locality.Const.legacy in - let linearity = Linearity.Const.legacy in - let uniqueness = Uniqueness.Const.legacy in - { locality; linearity; uniqueness } + merge { comonadic = Comonadic.legacy; monadic = Monadic.legacy } let meet m0 m1 = - let locality = Locality.Const.meet m0.locality m1.locality in - let linearity = Linearity.Const.meet m0.linearity m1.linearity in - let uniqueness = Uniqueness.Const.meet m0.uniqueness m1.uniqueness in - { locality; linearity; uniqueness } + let m0 = split m0 in + let m1 = split m1 in + let monadic = Monadic.meet m0.monadic m1.monadic in + let comonadic = Comonadic.meet m0.comonadic m1.comonadic in + merge { monadic; comonadic } let join m0 m1 = - let locality = Locality.Const.join m0.locality m1.locality in - let linearity = Linearity.Const.join m0.linearity m1.linearity in - let uniqueness = Uniqueness.Const.join m0.uniqueness m1.uniqueness in - { locality; linearity; uniqueness } + let m0 = split m0 in + let m1 = split m1 in + let monadic = Monadic.join m0.monadic m1.monadic in + let comonadic = Comonadic.join m0.comonadic m1.comonadic in + merge { monadic; comonadic } module Option = struct type some = t @@ -2168,64 +2108,53 @@ module Alloc = struct { locality; uniqueness; linearity } end - let split { locality; linearity; uniqueness } = - let monadic = uniqueness, () in - let comonadic = locality, linearity in - { comonadic; monadic } - - let merge { comonadic; monadic } = - let locality, linearity = comonadic in - let uniqueness, () = monadic in - { locality; linearity; uniqueness } - (** See [Alloc.close_over] for explanation. *) let close_over m = let { monadic; comonadic } = split m in let comonadic = - Comonadic.Const.join comonadic - (C.monadic_to_comonadic_min Comonadic.Obj.obj monadic) + Comonadic.join comonadic + (C.monadic_to_comonadic_min C.Comonadic_with_locality monadic) in - let monadic = Monadic.Const.min in + let monadic = Monadic.min in merge { comonadic; monadic } (** See [Alloc.partial_apply] for explanation. *) let partial_apply m = let { comonadic; _ } = split m in - let monadic = Monadic.Const.min in + let monadic = Monadic.min in merge { comonadic; monadic } + + let split = split + + let merge = merge end - let meet_with c { comonadic; monadic } = - let c = Const.split c in - let comonadic = Comonadic.meet_with c.comonadic comonadic in - let monadic = Monadic.meet_with c.monadic monadic in + let meet_const c { comonadic; monadic } = + let c = split c in + let comonadic = Comonadic.meet_const c.comonadic comonadic in + let monadic = Monadic.meet_const c.monadic monadic in { monadic; comonadic } let imply c { comonadic; monadic } = - let c = Const.split c in + let c = split c in let comonadic = Comonadic.imply c.comonadic comonadic in let monadic = Monadic.imply c.monadic monadic in { monadic; comonadic } - let zap_to_floor { comonadic; monadic } : Const.t = - match Monadic.zap_to_floor monadic, Comonadic.zap_to_floor comonadic with - | (uniqueness, ()), (locality, linearity) -> - { locality; linearity; uniqueness } - - let zap_to_ceil { comonadic; monadic } : Const.t = - match Monadic.zap_to_ceil monadic, Comonadic.zap_to_ceil comonadic with - | (uniqueness, ()), (locality, linearity) -> - { locality; linearity; uniqueness } - - let zap_to_legacy { comonadic; monadic } : Const.t = - match Monadic.zap_to_legacy monadic, Comonadic.zap_to_legacy comonadic with - | (uniqueness, ()), (locality, linearity) -> - { locality; linearity; uniqueness } + let zap_to_ceil { comonadic; monadic } = + let monadic = Monadic.zap_to_ceil monadic in + let comonadic = Comonadic.zap_to_ceil comonadic in + merge { monadic; comonadic } - let check_const { comonadic; monadic } : Const.Option.t = - let locality, linearity = Comonadic.check_const comonadic in - let uniqueness = Monadic.check_const monadic in - { locality; linearity; uniqueness } + let zap_to_legacy { comonadic; monadic } = + let monadic = Monadic.zap_to_legacy monadic in + let comonadic = Comonadic.zap_to_legacy comonadic in + merge { monadic; comonadic } + + let check_const { comonadic; monadic } = + let comonadic = Comonadic.check_const comonadic in + let monadic = Monadic.check_const monadic in + merge { monadic; comonadic } (** This is about partially applying [A -> B -> C] to [A] and getting [B -> C]. [comonadic] and [monadic] constutute the mode of [A], and we need to diff --git a/ocaml/typing/mode_intf.mli b/ocaml/typing/mode_intf.mli index 2df6d0d8b32..52776ff3f50 100644 --- a/ocaml/typing/mode_intf.mli +++ b/ocaml/typing/mode_intf.mli @@ -89,24 +89,10 @@ module type Common = sig val print : ?verbose:bool -> unit -> Format.formatter -> (allowed * allowed) t -> unit - val zap_to_floor : (allowed * 'r) t -> Const.t - - val zap_to_ceil : ('l * allowed) t -> Const.t - val of_const : Const.t -> ('l * 'r) t end module type S = sig - module Axis : sig - type t = - [ `Locality - | `Regionality - | `Uniqueness - | `Linearity ] - - val to_string : t -> string - end - module Global_flag : sig type t = | Global @@ -127,6 +113,10 @@ module type S = sig type nonrec equate_step = equate_step + type ('a, 'd) mode_monadic constraint 'd = 'l * 'r + + type ('a, 'd) mode_comonadic constraint 'd = 'l * 'r + type ('a, 'b) monadic_comonadic = { monadic : 'a; comonadic : 'b @@ -143,13 +133,19 @@ module type S = sig type error = Const.t Solver.error - include Common with module Const := Const and type error := error + include + Common + with module Const := Const + and type error := error + and type 'd t = (Const.t, 'd) mode_comonadic val global : lr val local : lr - val zap_to_legacy : (allowed * 'r) t -> Const.t + val zap_to_floor : (allowed * 'r) t -> Const.t + + val zap_to_ceil : ('l * allowed) t -> Const.t val check_const : (allowed * allowed) t -> Const.t option end @@ -166,15 +162,17 @@ module type S = sig type error = Const.t Solver.error - include Common with module Const := Const and type error := error + include + Common + with module Const := Const + and type error := error + and type 'd t = (Const.t, 'd) mode_comonadic val global : lr val regional : lr val local : lr - - val zap_to_legacy : (allowed * 'r) t -> Const.t end module Linearity : sig @@ -188,13 +186,15 @@ module type S = sig type error = Const.t Solver.error - include Common with module Const := Const and type error := error + include + Common + with module Const := Const + and type error := error + and type 'd t = (Const.t, 'd) mode_comonadic val many : lr val once : lr - - val zap_to_legacy : (allowed * 'r) t -> Const.t end module Uniqueness : sig @@ -208,25 +208,48 @@ module type S = sig type error = Const.t Solver.error - include Common with module Const := Const and type error := error + include + Common + with module Const := Const + and type error := error + and type 'd t = (Const.t, 'd) mode_monadic val shared : lr val unique : lr + end + + type 'a comonadic_with = private 'a * Linearity.Const.t - val zap_to_legacy : ('l * allowed) t -> Const.t + type monadic = private Uniqueness.Const.t * unit + + module Axis : sig + (** ('p, 'r) t represents a projection from a product of type ['p] to an + element of type ['r]. *) + type ('p, 'r) t = + | Areality : ('a comonadic_with, 'a) t + | Linearity : ('areality comonadic_with, Linearity.Const.t) t + | Uniqueness : (monadic, Uniqueness.Const.t) t + + val print : Format.formatter -> ('p, 'r) t -> unit end (** The most general mode. Used in most type checking, including in value bindings in [Env] *) module Value : sig - module Monadic : Common with type error = [`Uniqueness of Uniqueness.error] + module Monadic : sig + module Const : Lattice with type t = monadic - module Comonadic : - Common - with type error = - [ `Regionality of Regionality.error - | `Linearity of Linearity.error ] + include Common with module Const := Const + end + + module Comonadic : sig + module Const : Lattice with type t = Regionality.Const.t comonadic_with + + type error = Error : (Const.t, 'a) Axis.t * 'a Solver.error -> error + + include Common with type error := error and module Const := Const + end type ('a, 'b, 'c) modes = { regionality : 'a; @@ -239,10 +262,17 @@ module type S = sig with type t = (Regionality.Const.t, Linearity.Const.t, Uniqueness.Const.t) modes - type error = - [ `Regionality of Regionality.error - | `Uniqueness of Uniqueness.error - | `Linearity of Linearity.error ] + (** Represents a mode axis in this product whose constant is ['a], and + whose variable is ['m] given the allowness ['d]. *) + type ('m, 'a, 'd) axis = + | Monadic : + (Monadic.Const.t, 'a) Axis.t + -> (('a, 'd) mode_monadic, 'a, 'd) axis + | Comonadic : + (Comonadic.Const.t, 'a) Axis.t + -> (('a, 'd) mode_comonadic, 'a, 'd) axis + + type error = Error : ('m, 'a, 'd) axis * 'a Solver.error -> error type 'd t = ('d Monadic.t, 'd Comonadic.t) monadic_comonadic @@ -257,47 +287,19 @@ module type S = sig include Allow_disallow with type (_, _, 'd) sided = 'd t list end - val regionality : ('l * 'r) t -> ('l * 'r) Regionality.t - - val uniqueness : ('l * 'r) t -> ('l * 'r) Uniqueness.t - - val linearity : ('l * 'r) t -> ('l * 'r) Linearity.t - - val max_with_uniqueness : ('l * 'r) Uniqueness.t -> (disallowed * 'r) t - - val min_with_uniqueness : ('l * 'r) Uniqueness.t -> ('l * disallowed) t - - val min_with_regionality : ('l * 'r) Regionality.t -> ('l * disallowed) t - - val max_with_regionality : ('l * 'r) Regionality.t -> (disallowed * 'r) t - - val min_with_linearity : ('l * 'r) Linearity.t -> ('l * disallowed) t - - val max_with_linearity : ('l * 'r) Linearity.t -> (disallowed * 'r) t - - val meet_with_regionality : - Regionality.Const.t -> ('l * 'r) t -> ('l * disallowed) t - - val join_with_regionality : - Regionality.Const.t -> ('l * 'r) t -> (disallowed * 'r) t + val proj : ('m, 'a, 'l * 'r) axis -> ('l * 'r) t -> 'm - val meet_with_linearity : - Linearity.Const.t -> ('l * 'r) t -> ('l * disallowed) t + val max_with : ('m, 'a, 'l * 'r) axis -> 'm -> (disallowed * 'r) t - val join_with_linearity : - Linearity.Const.t -> ('l * 'r) t -> (disallowed * 'r) t + val min_with : ('m, 'a, 'l * 'r) axis -> 'm -> ('l * disallowed) t - val meet_with_uniqueness : - Uniqueness.Const.t -> ('l * 'r) t -> ('l * disallowed) t + val meet_with : (_, 'a, _) axis -> 'a -> ('l * 'r) t -> ('l * disallowed) t - val join_with_uniqueness : - Uniqueness.Const.t -> ('l * 'r) t -> (disallowed * 'r) t - - val zap_to_legacy : lr -> Const.t + val join_with : (_, 'a, _) axis -> 'a -> ('l * 'r) t -> (disallowed * 'r) t val comonadic_to_monadic : ('l * 'r) Comonadic.t -> ('r * 'l) Monadic.t - val meet_with : Const.t -> ('l * 'r) t -> ('l * disallowed) t + val meet_const : Const.t -> ('l * 'r) t -> ('l * disallowed) t val imply : Const.t -> ('l * 'r) t -> (disallowed * 'r) t end @@ -307,26 +309,23 @@ module type S = sig and would be hard to understand if it involves [Regionality]. *) module Alloc : sig module Monadic : sig - include Common with type error = [`Uniqueness of Uniqueness.error] + module Const : Lattice with type t = monadic + + include Common with module Const := Const val imply : Const.t -> ('l * 'r) t -> (disallowed * 'r) t end module Comonadic : sig module Const : sig - include Lattice + include Lattice with type t = Locality.Const.t comonadic_with val eq : t -> t -> bool end - include - Common - with type error = - [ `Locality of Locality.error - | `Linearity of Linearity.error ] - and module Const := Const + include Common with module Const := Const - val meet_with : Const.t -> ('l * 'r) t -> ('l * disallowed) t + val meet_const : Const.t -> ('l * 'r) t -> ('l * disallowed) t end type ('loc, 'lin, 'uni) modes = @@ -366,10 +365,17 @@ module type S = sig val partial_apply : t -> t end - type error = - [ `Locality of Locality.error - | `Uniqueness of Uniqueness.error - | `Linearity of Linearity.error ] + (** Represents a mode axis in this product whose constant is ['a], and + whose variable is ['m] given the allowness ['d]. *) + type ('m, 'a, 'd) axis = + | Monadic : + (Monadic.Const.t, 'a) Axis.t + -> (('a, 'd) mode_monadic, 'a, 'd) axis + | Comonadic : + (Comonadic.Const.t, 'a) Axis.t + -> (('a, 'd) mode_comonadic, 'a, 'd) axis + + type error = Error : ('m, 'a, 'd) axis * 'a Solver.error -> error type 'd t = ('d Monadic.t, 'd Comonadic.t) monadic_comonadic @@ -381,45 +387,21 @@ module type S = sig val check_const : (allowed * allowed) t -> Const.Option.t - val locality : ('l * 'r) t -> ('l * 'r) Locality.t - - val uniqueness : ('l * 'r) t -> ('l * 'r) Uniqueness.t - - val linearity : ('l * 'r) t -> ('l * 'r) Linearity.t - - val max_with_uniqueness : ('l * 'r) Uniqueness.t -> (disallowed * 'r) t + val proj : ('m, 'a, 'l * 'r) axis -> ('l * 'r) t -> 'm - val min_with_uniqueness : ('l * 'r) Uniqueness.t -> ('l * disallowed) t + val max_with : ('m, 'a, 'l * 'r) axis -> 'm -> (disallowed * 'r) t - val min_with_locality : ('l * 'r) Locality.t -> ('l * disallowed) t + val min_with : ('m, 'a, 'l * 'r) axis -> 'm -> ('l * disallowed) t - val max_with_locality : ('l * 'r) Locality.t -> (disallowed * 'r) t + val meet_with : (_, 'a, _) axis -> 'a -> ('l * 'r) t -> ('l * disallowed) t - val min_with_linearity : ('l * 'r) Linearity.t -> ('l * disallowed) t - - val max_with_linearity : ('l * 'r) Linearity.t -> (disallowed * 'r) t - - val meet_with_locality : - Locality.Const.t -> ('l * 'r) t -> ('l * disallowed) t - - val join_with_locality : - Locality.Const.t -> ('l * 'r) t -> (disallowed * 'r) t - - val meet_with_linearity : - Linearity.Const.t -> ('l * 'r) t -> ('l * disallowed) t - - val join_with_linearity : - Linearity.Const.t -> ('l * 'r) t -> (disallowed * 'r) t - - val meet_with_uniqueness : - Uniqueness.Const.t -> ('l * 'r) t -> ('l * disallowed) t - - val join_with_uniqueness : - Uniqueness.Const.t -> ('l * 'r) t -> (disallowed * 'r) t + val join_with : (_, 'a, _) axis -> 'a -> ('l * 'r) t -> (disallowed * 'r) t val zap_to_legacy : lr -> Const.t - val meet_with : Const.t -> ('l * 'r) t -> ('l * disallowed) t + val zap_to_ceil : ('l * allowed) t -> Const.t + + val meet_const : Const.t -> ('l * 'r) t -> ('l * disallowed) t val imply : Const.t -> ('l * 'r) t -> (disallowed * 'r) t diff --git a/ocaml/typing/typecore.ml b/ocaml/typing/typecore.ml index 59ac426e0c2..465746eb2ae 100644 --- a/ocaml/typing/typecore.ml +++ b/ocaml/typing/typecore.ml @@ -347,8 +347,9 @@ type expected_mode = strictly_local : bool; (** Indicates that the expression was directly annotated with [local], which - should force any allocations to be on the stack. If [true] the [mode] field - must be greater than [local]. *) + should force any allocations to be on the stack. No invariant between this + field and [mode]: this field being [true] while [mode] being [global] is + sensible, but not very useful as it will fail all expressions. *) tuple_modes : Value.r list; (** For t in tuple_modes, t <= regional_to_global mode *) @@ -411,19 +412,16 @@ let check_tail_call_local_returning loc env ap_mode {region_mode; _} = let meet_regional mode = let mode = Value.disallow_left mode in - Value.meet [mode; (Value.max_with_regionality Regionality.regional)] + Value.meet [mode; (Value.max_with (Comonadic Areality) Regionality.regional)] let meet_global mode = - Value.meet [mode; (Value.max_with_regionality Regionality.global)] - -let meet_unique mode = - Value.meet [mode; (Value.max_with_uniqueness Uniqueness.unique)] + Value.meet [mode; (Value.max_with (Comonadic Areality) Regionality.global)] let meet_many mode = - Value.meet [mode; (Value.max_with_linearity Linearity.many)] + Value.meet [mode; (Value.max_with (Comonadic Linearity) Linearity.many)] let join_shared mode = - Value.join [mode; Value.min_with_uniqueness Uniqueness.shared] + Value.join [mode; Value.min_with (Monadic Uniqueness) Uniqueness.shared] let value_regional_to_local mode = mode @@ -437,9 +435,9 @@ let modality_unbox_left global_flag mode = match global_flag with | Global_flag.Global -> mode - |> Value.meet_with_regionality Regionality.Const.Global + |> Value.meet_with (Comonadic Areality) Regionality.Const.Global |> join_shared - |> Value.meet_with_linearity Linearity.Const.Many + |> Value.meet_with (Comonadic Linearity) Linearity.Const.Many | Global_flag.Unrestricted -> mode (* Describes how a modality affects record construction. Gives the @@ -449,7 +447,7 @@ let modality_box_right global_flag mode = | Global_flag.Global -> mode |> meet_global - |> Value.join_with_uniqueness Uniqueness.Const.max + |> Value.join_with (Monadic Uniqueness) Uniqueness.Const.max |> meet_many | Global_flag.Unrestricted -> mode @@ -466,7 +464,8 @@ let mode_legacy = mode_default Value.legacy mode is the mode of the function region *) let mode_return mode = { (mode_default (meet_regional mode)) with - position = RTail (Regionality.disallow_left (Value.regionality mode), FTail); + position = RTail (Regionality.disallow_left + (Value.proj (Comonadic Areality) mode), FTail); closure_context = Some Return; } @@ -474,7 +473,8 @@ let mode_return mode = let mode_region mode = { (mode_default (meet_regional mode)) with position = - RTail (Regionality.disallow_left (Value.regionality mode), FNontail); + RTail (Regionality.disallow_left + (Value.proj (Comonadic Areality) mode), FNontail); closure_context = None; } @@ -491,30 +491,23 @@ let mode_global expected_mode = let mode = meet_global expected_mode.mode in {expected_mode with mode} -let mode_local expected_mode = - { expected_mode with - mode = Value.join_with_regionality Regionality.Const.Local expected_mode.mode } - let mode_exclave expected_mode = let mode = - Value.join_with_regionality Regionality.Const.Local expected_mode.mode + Value.join_with (Comonadic Areality) + Regionality.Const.Local expected_mode.mode in { (mode_default mode) with strictly_local = true } let mode_strictly_local expected_mode = - { (mode_local expected_mode) + { expected_mode with strictly_local = true } -let mode_unique expected_mode = - let mode = meet_unique expected_mode.mode in - { expected_mode with mode } - -let mode_once expected_mode = - { expected_mode with - mode = Value.join_with_linearity Linearity.Const.Once expected_mode.mode} +let mode_coerce mode expected_mode = + let mode = Value.meet [expected_mode.mode; mode] in + { expected_mode with mode; tuple_modes = [] } let mode_tailcall_function mode = { (mode_default mode) with @@ -562,7 +555,8 @@ let mode_argument ~funct ~index ~position_and_mode ~partial_app marg = | _, _, (Nontail | Default) -> mode_default vmode, vmode | _, _, Tail -> begin - Regionality.submode_exn (Value.regionality vmode) Regionality.regional; + Regionality.submode_exn (Value.proj (Comonadic Areality) vmode) + Regionality.regional; mode_tailcall_argument vmode, vmode end @@ -804,7 +798,7 @@ let mode_cross_left env ty mode = let jkind = type_jkind_purely env ty in let upper_bounds = Jkind.get_modal_upper_bounds jkind in let upper_bounds = Const.alloc_as_value upper_bounds in - Value.meet_with upper_bounds mode + Value.meet_const upper_bounds mode (** Mode cross a mode whose monadic fragment is a right mode, and whose comonadic fragment is a left mode. *) @@ -815,7 +809,7 @@ let alloc_mode_cross_to_max_min env ty { monadic; comonadic } = let jkind = type_jkind_purely env ty in let upper_bounds = Jkind.get_modal_upper_bounds jkind in let upper_bounds = Alloc.Const.split upper_bounds in - let comonadic = Alloc.Comonadic.meet_with upper_bounds.comonadic comonadic in + let comonadic = Alloc.Comonadic.meet_const upper_bounds.comonadic comonadic in let monadic = Alloc.Monadic.imply upper_bounds.monadic monadic in { monadic; comonadic } @@ -858,21 +852,14 @@ let apply_mode_annots ~loc ~env (m : Alloc.Const.Option.t) mode = let error axis = raise (Error(loc, env, Param_mode_mismatch axis)) in - Option.iter (fun locality -> - match Locality.equate (Locality.of_const locality) (Alloc.locality mode) with - | Ok () -> () - | Error (s, e) -> error (s, `Locality e) - ) m.locality; - Option.iter (fun uniqueness -> - match Uniqueness.equate (Uniqueness.of_const uniqueness) (Alloc.uniqueness mode) with - | Ok () -> () - | Error (s, e) -> error (s, `Uniqueness e) - ) m.uniqueness; - Option.iter (fun linearity -> - match Linearity.equate (Linearity.of_const linearity) (Alloc.linearity mode) with - | Ok () -> () - | Error (s, e) -> error (s, `Linearity e) - ) m.linearity + let min = Alloc.Const.Option.value ~default:Alloc.Const.min m in + let max = Alloc.Const.Option.value ~default:Alloc.Const.max m in + (match Alloc.submode (Alloc.of_const min) mode with + | Ok () -> () + | Error e -> error (Left_le_right, e)); + (match Alloc.submode mode (Alloc.of_const max) with + | Ok () -> () + | Error e -> error (Right_le_left, e)) (** Takes the mutability and modalities on a record field, and [m] which is a left mode on the record being accessed, returns the left mode of the @@ -4719,8 +4706,8 @@ let with_explanation explanation f = raise (Error (loc', env', err)) let unique_use ~loc ~env mode_l mode_r = - let uniqueness = Uniqueness.disallow_left (Value.uniqueness mode_r) in - let linearity = Linearity.disallow_right (Value.linearity mode_l) in + let uniqueness = Uniqueness.disallow_left (Value.proj (Monadic Uniqueness) mode_r) in + let linearity = Linearity.disallow_right (Value.proj (Comonadic Linearity) mode_l) in if not (Language_extension.is_enabled Unique) then begin (* if unique extension is not enabled, we will not run uniqueness analysis; instead, we force all uses to be shared and many. This is equivalent to @@ -4728,12 +4715,14 @@ let unique_use ~loc ~env mode_l mode_r = (match Uniqueness.submode Uniqueness.shared uniqueness with | Ok () -> () | Error e -> - raise (Error(loc, env, Submode_failed(`Uniqueness e, Other, None, None))) + let e : Mode.Value.error = Error (Monadic Uniqueness, e) in + raise (Error(loc, env, Submode_failed(e, Other, None, None))) ); (match Linearity.submode linearity Linearity.many with | Ok () -> () | Error e -> - raise (Error (loc, env, Submode_failed(`Linearity e, Other, None, None))) + let e : Mode.Value.error = Error (Comonadic Linearity, e) in + raise (Error (loc, env, Submode_failed(e, Other, None, None))) ); (Uniqueness.disallow_left Uniqueness.shared, Linearity.disallow_right Linearity.many) @@ -4819,7 +4808,7 @@ let split_function_ty fst (register_allocation_value_mode mode) in if expected_mode.strictly_local then - Locality.submode_exn Locality.local (Alloc.locality alloc_mode); + Locality.submode_exn Locality.local (Alloc.proj (Comonadic Areality) alloc_mode); let { ty_fun = { ty = ty_fun; explanation }; loc_fun; region_locked } = in_function in @@ -4884,7 +4873,7 @@ let split_function_ty else begin (* if the function has no region, we force the ret_mode to be local *) match - Locality.submode Locality.local (Alloc.locality ret_mode) + Locality.submode Locality.local (Alloc.proj (Comonadic Areality) ret_mode) with | Ok () -> mode_default ret_value_mode | Error _ -> raise (Error (loc_fun, env, Function_returns_local)) @@ -5287,7 +5276,7 @@ and type_expect_ type_expect ~recarg new_env mode' sbody ty_expected_explained in submode ~loc ~env ~reason:Other - (Value.min_with_regionality Regionality.regional) expected_mode; + (Value.min_with (Comonadic Areality) Regionality.regional) expected_mode; { exp_desc = Texp_exclave exp; exp_loc = loc; exp_extra = []; @@ -5302,7 +5291,10 @@ and type_expect_ let funct_mode, funct_expected_mode = match pm.apply_position with | Tail -> - let mode, _ = Value.newvar_below (Value.max_with_regionality Regionality.regional) in + let mode, _ = + Value.newvar_below + (Value.max_with (Comonadic Areality) Regionality.regional) + in mode, mode_tailcall_function mode | Nontail | Default -> let mode = Value.newvar () in @@ -5709,7 +5701,8 @@ and type_expect_ unify_exp env record ty_record; rue { exp_desc = Texp_setfield(record, - Locality.disallow_right (regional_to_local (Value.regionality rmode)), + Locality.disallow_right (regional_to_local + (Value.proj (Comonadic Areality) rmode)), label_loc, label, newval); exp_loc = loc; exp_extra = []; exp_type = instance Predef.type_unit; @@ -6520,8 +6513,8 @@ and type_ident env ?(recarg=Rejected) lid = we then register allocation for further optimization *) | (Prim_poly, _), Some mode -> register_allocation_mode - (Alloc.meet [Alloc.max_with_locality mode; - Alloc.max_with_linearity Linearity.many]) + (Alloc.meet [Alloc.max_with (Comonadic Areality) mode; + Alloc.max_with (Comonadic Linearity) Linearity.many]) | _ -> () end; ty, Id_prim (Option.map Locality.disallow_right mode, sort) @@ -7378,7 +7371,8 @@ and type_argument ?explanation ?recarg env (mode : expected_mode) sarg desc, Id_value, uu)} in let eta_mode, _ = Value.newvar_below (alloc_as_value marg) in - Regionality.submode_exn (Value.regionality eta_mode) Regionality.regional; + Regionality.submode_exn + (Value.proj (Comonadic Areality) eta_mode) Regionality.regional; let eta_pat, eta_var = var_pair ~mode:eta_mode "eta" ty_arg in (* CR layouts v10: When we add abstract jkinds, the eta expansion here becomes impossible in some cases - we'll need better errors. For test @@ -7400,7 +7394,7 @@ and type_argument ?explanation ?recarg env (mode : expected_mode) sarg (texp, args @ [Nolabel, Arg (eta_var, arg_sort)], Nontail, ret_mode - |> Value.regionality + |> Value.proj (Comonadic Areality) |> regional_to_global |> Locality.disallow_right)} in @@ -7548,7 +7542,7 @@ and type_application env app_loc expected_mode position_and_mode | Error err -> raise (Error (app_loc, env, Function_type_not_rep (ty, err))) in let arg_sort = type_sort ~why:Function_argument ty_arg in - let ap_mode = Locality.disallow_right (Alloc.locality ret_mode) in + let ap_mode = Locality.disallow_right (Alloc.proj (Comonadic Areality) ret_mode) in let mode_res = mode_cross_left env ty_ret (alloc_as_value ret_mode) in @@ -7610,7 +7604,7 @@ and type_application env app_loc expected_mode position_and_mode ty_ret, mode_ret, args, position_and_mode end ~post:(fun (ty_ret, _, _, _) -> generalize_structure ty_ret) in - let ap_mode = Locality.disallow_right (Alloc.locality mode_ret) in + let ap_mode = Locality.disallow_right (Alloc.proj (Comonadic Areality) mode_ret) in let mode_ret = mode_cross_left env ty_ret (alloc_as_value mode_ret) in @@ -8692,38 +8686,14 @@ and type_mode_expr : Jane_syntax.Modes.expression -> _ = function | Coerce (m, sbody) -> let modes = Typemode.transl_mode_annots m in - (* CR zqian: All axes should be handled in one go. We can't do that yet - because [mode_strictly_local] is special. *) - let expected_mode = - match modes.uniqueness with - | Some Unique -> - let expected_mode = mode_unique expected_mode in - expect_mode_cross env ty_expected expected_mode - | Some m -> - Misc.fatal_errorf "The mode %a should not interpret" Uniqueness.Const.print m - | None -> expected_mode - in - let expected_mode = - match modes.linearity with - | Some Once -> - let expected_mode = expect_mode_cross env ty_expected expected_mode in - submode ~loc ~env ~reason:Other - (Value.min_with_linearity Linearity.once) expected_mode; - mode_once expected_mode - | Some m -> - Misc.fatal_errorf "The mode %a should not interpret" Linearity.Const.print m - | None -> expected_mode - in + let min = Alloc.Const.Option.value ~default:Alloc.Const.min modes |> Const.alloc_as_value in + let max = Alloc.Const.Option.value ~default:Alloc.Const.max modes |> Const.alloc_as_value in + submode ~loc ~env ~reason:Other (Value.of_const min) expected_mode; + let expected_mode = mode_coerce (Value.of_const max) expected_mode in let expected_mode = match modes.locality with - | Some Local -> - let expected_mode = expect_mode_cross env ty_expected expected_mode in - submode ~loc ~env ~reason:Other - (Value.min_with_regionality Regionality.local) expected_mode; - mode_strictly_local expected_mode - | Some m -> - Misc.fatal_errorf "The mode %a should not interpret" Locality.Const.print m - | None -> expected_mode + | Some Local -> mode_strictly_local expected_mode + | _ -> expected_mode in let exp = type_expect env expected_mode sbody (mk_expected ty_expected ?explanation) @@ -9420,22 +9390,26 @@ let report_type_expected_explanation expl ppf = let escaping_hint (failure_reason : Value.error) submode_reason (context : Env.closure_context option) = begin match failure_reason, context with - | `Regionality {left=Local; right=Regional}, Some Return -> + | Error (Comonadic Areality, e), Some h -> + begin match e, h with + | {left=Local; right=Regional}, Return -> (* Only hint to use exclave_, when the user wants to return local, but expected mode is regional. If the expected mode is as strict as global, then exclave_ won't solve the problem. *) [ Location.msg "@[Hint: Cannot return a local value without an@ \ \"exclave_\" annotation@]" ] - | `Regionality _, Some Tailcall_argument -> + | _, Return -> [] + | _, Tailcall_argument -> [ Location.msg "@[Hint: This argument cannot be local, because it is an argument in a tail call@]" ] - | `Regionality _, Some Tailcall_function -> + | _, Tailcall_function -> [ Location.msg "@[Hint: This function cannot be local, because it is the function in a tail call@]" ] - | `Regionality _, Some Partial_application -> + | _, Partial_application -> [ Location.msg "@[Hint: It is captured by a partial application@]" ] + end | _, _ -> [] end @ @@ -9450,7 +9424,7 @@ let escaping_hint (failure_reason : Value.error) submode_reason match get_desc ty with | Tarrow ((_, _, res_mode), _, res_ty, _) -> begin match - Locality.check_const (Alloc.locality res_mode) + Locality.check_const (Alloc.proj (Comonadic Areality) res_mode) with | Some Global -> Some (n+1, true) @@ -10078,18 +10052,21 @@ let report_error ~loc env = function -> let sub = match fail_reason with - | `Linearity _ | `Uniqueness _ -> + | Error (Comonadic Linearity, _) | Error (Monadic Uniqueness, _) -> sharedness_hint fail_reason submode_reason shared_context - | `Regionality _ -> + | Error (Comonadic Areality, _) -> escaping_hint fail_reason submode_reason closure_context in Location.errorf ~loc ~sub "%t" begin match fail_reason with - | `Regionality _ -> Format.dprintf "This value escapes its region" - | `Uniqueness {left; right} -> Format.dprintf "Found a %a value where a %a value was expected" - Uniqueness.Const.print left Uniqueness.Const.print right - | `Linearity {left; right} -> Format.dprintf "Found a %a value where a %a value was expected" - Linearity.Const.print left Linearity.Const.print right + | Error (Comonadic Areality, _) -> + Format.dprintf "This value escapes its region" + | Error (Monadic Uniqueness, {left; right}) -> + Format.dprintf "Found a %a value where a %a value was expected" + Uniqueness.Const.print left Uniqueness.Const.print right + | Error (Comonadic Linearity, {left; right}) -> + Format.dprintf "Found a %a value where a %a value was expected" + Linearity.Const.print left Linearity.Const.print right end | Local_application_complete (lbl, loc_kind) -> let sub = @@ -10127,17 +10104,20 @@ let report_error ~loc env = function f actual f expected in begin match mkind with - | `Locality e -> print_error Locality.Const.print (s, e) - | `Uniqueness e -> print_error Uniqueness.Const.print (s, e) - | `Linearity e -> print_error Linearity.Const.print (s, e) + | Error (Comonadic Areality, e) -> + print_error Locality.Const.print (s, e) + | Error (Monadic Uniqueness, e) -> + print_error Uniqueness.Const.print (s, e) + | Error (Comonadic Linearity, e) -> + print_error Linearity.Const.print (s, e) end | Uncurried_function_escapes e -> begin match e with - | `Locality _ -> + | Error (Comonadic Areality, _) -> Location.errorf ~loc "This function or one of its parameters escape their region @ \ when it is partially applied." - | `Uniqueness _ -> assert false - | `Linearity {left; right} -> + | Error (Monadic Uniqueness, _) -> assert false + | Error (Comonadic Linearity, {left; right}) -> Location.errorf ~loc "This function when partially applied returns a %a value,@ \ but expected to be %a." Linearity.Const.print left Linearity.Const.print right end diff --git a/ocaml/typing/typedecl.ml b/ocaml/typing/typedecl.ml index 26a06a4fc35..19efdcba4a5 100644 --- a/ocaml/typing/typedecl.ml +++ b/ocaml/typing/typedecl.ml @@ -2343,11 +2343,11 @@ let rec parse_native_repr_attributes env core_type ty rmode let mode = if Builtin_attributes.has_local_opt ct1.ptyp_attributes then Prim_poly - else prim_const_mode (Mode.Alloc.locality marg) + else prim_const_mode (Mode.Alloc.proj (Comonadic Areality) marg) in let repr_args, repr_res = parse_native_repr_attributes env ct2 t2 - (prim_const_mode (Mode.Alloc.locality mret)) + (prim_const_mode (Mode.Alloc.proj (Comonadic Areality) mret)) ~global_repr ~is_layout_poly in ((mode, repr_arg) :: repr_args, repr_res) diff --git a/ocaml/typing/typemode.ml b/ocaml/typing/typemode.ml index 60172893a02..70be7eb7762 100644 --- a/ocaml/typing/typemode.ml +++ b/ocaml/typing/typemode.ml @@ -3,7 +3,7 @@ open Mode open Jane_syntax type error = - | Duplicated_mode of Axis.t + | Duplicated_mode : ('a, 'b) Axis.t -> error | Unrecognized_mode of string | Unrecognized_modality of string @@ -22,15 +22,15 @@ let transl_mode_annots modes = | "local" -> ( match acc.locality with | None -> { acc with locality = Some Local } - | Some _ -> raise (Error (loc, Duplicated_mode `Locality))) + | Some _ -> raise (Error (loc, Duplicated_mode Areality))) | "unique" -> ( match acc.uniqueness with | None -> { acc with uniqueness = Some Unique } - | Some _ -> raise (Error (loc, Duplicated_mode `Uniqueness))) + | Some _ -> raise (Error (loc, Duplicated_mode Uniqueness))) | "once" -> ( match acc.linearity with | None -> { acc with linearity = Some Once } - | Some _ -> raise (Error (loc, Duplicated_mode `Linearity))) + | Some _ -> raise (Error (loc, Duplicated_mode Linearity))) | "global" -> (* CR zqian: global modality might leak to here by ppxes. This is a dirty fix that needs to be fixed ASAP. *) @@ -72,7 +72,12 @@ open Format let report_error ppf = function | Duplicated_mode ax -> - fprintf ppf "The %s axis has already been specified." (Axis.to_string ax) + let ax = + match ax with + | Areality -> dprintf "locality" + | _ -> dprintf "%a" Axis.print ax + in + fprintf ppf "The %t axis has already been specified." ax | Unrecognized_mode s -> fprintf ppf "Unrecognized mode name %s." s | Unrecognized_modality s -> fprintf ppf "Unrecognized modality %s." s