From 6e71c0018cc36cbdc7a863a161ae3de7186badf7 Mon Sep 17 00:00:00 2001 From: Zesen Qian Date: Thu, 21 Mar 2024 09:48:22 +0000 Subject: [PATCH 1/5] make mode constants scale --- ocaml/typing/mode.ml | 208 ++++++++++++++++--------------------- ocaml/typing/mode_intf.mli | 18 +--- 2 files changed, 92 insertions(+), 134 deletions(-) diff --git a/ocaml/typing/mode.ml b/ocaml/typing/mode.ml index cdd6b3f45cd..c6156db94be 100644 --- a/ocaml/typing/mode.ml +++ b/ocaml/typing/mode.ml @@ -1252,8 +1252,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 @@ -1377,11 +1375,6 @@ module Comonadic_with_regionality = struct 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 *) @@ -1577,7 +1570,7 @@ module Monadic = struct (** overriding to check per-axis *) let check_const m = let uniqueness = Uniqueness.check_const (uniqueness m) in - uniqueness + uniqueness, () end type ('mo, 'como) monadic_comonadic = @@ -1603,6 +1596,16 @@ module Value = struct 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 min = { comonadic = Comonadic.min; monadic = Monadic.min } let max = @@ -1699,24 +1702,10 @@ module Value = struct (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 + 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 } let legacy = @@ -1817,62 +1806,46 @@ module Value = struct 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 } + module Monadic = Monadic.Const + module Comonadic = Comonadic.Const - let _merge { comonadic; monadic } = - let regionality, linearity = comonadic in - let uniqueness, () = monadic in - { regionality; linearity; uniqueness } + let min = merge { comonadic = Comonadic.min; monadic = Monadic.min } - 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 max = merge { comonadic = Comonadic.max; monadic = Monadic.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 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 = - { regionality = Regionality.Const.legacy; - linearity = Linearity.Const.legacy; - uniqueness = Uniqueness.Const.legacy - } + merge { comonadic = Comonadic.legacy; monadic = Monadic.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 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 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 } + 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 meet_with c { comonadic; monadic } = - let c = Const.split c in + let c = split c in let comonadic = Comonadic.meet_with c.comonadic comonadic in let monadic = Monadic.meet_with 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 } @@ -1912,6 +1885,16 @@ module Alloc = struct 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 } @@ -2111,42 +2094,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 min = merge { comonadic = Comonadic.min; monadic = Monadic.min } - let max = - let locality = Locality.Const.max in - let linearity = Linearity.Const.max in - let uniqueness = Uniqueness.Const.max in - { locality; linearity; uniqueness } + 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 +2145,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 c = split c in let comonadic = Comonadic.meet_with c.comonadic comonadic in let monadic = Monadic.meet_with 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..cd4710b4ba1 100644 --- a/ocaml/typing/mode_intf.mli +++ b/ocaml/typing/mode_intf.mli @@ -89,10 +89,6 @@ 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 @@ -149,7 +145,9 @@ module type S = sig 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 @@ -173,8 +171,6 @@ module type S = sig val regional : lr val local : lr - - val zap_to_legacy : (allowed * 'r) t -> Const.t end module Linearity : sig @@ -193,8 +189,6 @@ module type S = sig val many : lr val once : lr - - val zap_to_legacy : (allowed * 'r) t -> Const.t end module Uniqueness : sig @@ -213,8 +207,6 @@ module type S = sig val shared : lr val unique : lr - - val zap_to_legacy : ('l * allowed) t -> Const.t end (** The most general mode. Used in most type checking, @@ -293,8 +285,6 @@ module type S = sig val join_with_uniqueness : Uniqueness.Const.t -> ('l * 'r) t -> (disallowed * 'r) t - val zap_to_legacy : lr -> Const.t - val comonadic_to_monadic : ('l * 'r) Comonadic.t -> ('r * 'l) Monadic.t val meet_with : Const.t -> ('l * 'r) t -> ('l * disallowed) t @@ -419,6 +409,8 @@ module type S = sig val zap_to_legacy : lr -> Const.t + val zap_to_ceil : ('l * allowed) t -> Const.t + val meet_with : Const.t -> ('l * 'r) t -> ('l * disallowed) t val imply : Const.t -> ('l * 'r) t -> (disallowed * 'r) t From 89dfd97b964b43e4a8c5aa2322ff9d169f5b7747 Mon Sep 17 00:00:00 2001 From: Zesen Qian Date: Mon, 25 Mar 2024 17:56:35 +0000 Subject: [PATCH 2/5] make mode checking scale --- ocaml/typing/typecore.ml | 82 ++++++++++------------------------------ 1 file changed, 21 insertions(+), 61 deletions(-) diff --git a/ocaml/typing/typecore.ml b/ocaml/typing/typecore.ml index 59ac426e0c2..3a8a5b7ca5a 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 *) @@ -416,8 +417,6 @@ let meet_regional mode = 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)] let meet_many mode = Value.meet [mode; (Value.max_with_linearity Linearity.many)] @@ -491,10 +490,6 @@ 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 @@ -504,17 +499,13 @@ let mode_exclave expected_mode = } 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 @@ -858,21 +849,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 @@ -8692,38 +8676,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) From b99eac3da915c243c1074a30bd0ae702a426eae5 Mon Sep 17 00:00:00 2001 From: Zesen Qian Date: Thu, 28 Mar 2024 14:51:30 +0000 Subject: [PATCH 3/5] decompose axis access --- ocaml/lambda/translmode.ml | 4 +- ocaml/typing/ctype.ml | 6 +- ocaml/typing/env.ml | 14 +- ocaml/typing/mode.ml | 478 ++++++++++++++++--------------------- ocaml/typing/mode_intf.mli | 173 ++++++++------ ocaml/typing/typecore.ml | 114 +++++---- ocaml/typing/typedecl.ml | 4 +- 7 files changed, 388 insertions(+), 405 deletions(-) diff --git a/ocaml/lambda/translmode.ml b/ocaml/lambda/translmode.ml index 41b42c06751..3d45f47f51d 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 Locality 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 Locality 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..48d89bd4e46 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 Locality m') locality; + Alloc.submode_exn m' (Alloc.join_with_comonadic Locality Locality.Const.max m); + Alloc.submode_exn (Alloc.meet_with_comonadic Locality Locality.Const.min m) m'; m' let rec instance_prim_locals locals mvar macc finalret ty = diff --git a/ocaml/typing/env.ml b/ocaml/typing/env.ml index d2e13f91b3d..a5cc4320a2f 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 Regionality 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 Regionality 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 (Regionality, _) -> "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 (Regionality, _), 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 c6156db94be..635d10f4259 100644 --- a/ocaml/typing/mode.ml +++ b/ocaml/typing/mode.ml @@ -1109,6 +1109,10 @@ let append_changes : (changes ref -> unit) ref = ref (fun _ -> assert false) let set_append_changes f = append_changes := f +type ('a, 'd) monadic = ('a, 'd) S.Negative.mode + +type ('a, 'd) comonadic = ('a, 'd) S.Positive.mode + (** Representing a single object *) module type Obj = sig type const @@ -1320,65 +1324,56 @@ module Comonadic_with_regionality = struct end include Common (Obj) - open Obj - type error = - [ `Regionality of Regionality.error - | `Linearity of Linearity.error ] + type 'a ax = + | Regionality : Regionality.Const.t ax + | Linearity : Linearity.Const.t ax - type equate_error = equate_step * error + let axis_of_ax : type a. a ax -> (Const.t, a) C.axis = function + | Regionality -> Areality + | Linearity -> Linearity + [@@inline] - let regionality m = - S.Positive.via_monotone Regionality.Obj.obj (Proj (Obj.obj, Areality)) m + let obj_of_ax : type a. a ax -> a C.obj = function + | Regionality -> Regionality.Obj.obj + | Linearity -> Linearity.Obj.obj + [@@inline] - let min_with_regionality m = - S.Positive.via_monotone Obj.obj (Min_with Areality) - (S.Positive.disallow_right m) + type error = Error : 'a ax * 'a Solver.error -> error - let max_with_regionality m = - S.Positive.via_monotone Obj.obj (Max_with Areality) - (S.Positive.disallow_left m) + type equate_error = equate_step * error - 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 (obj_of_ax ax) (Proj (Obj.obj, axis_of_ax 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 (axis_of_ax 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 (axis_of_ax 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 (axis_of_ax 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 (axis_of_ax ax) c) 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 = reg0, lin0; right = reg1, lin1 } -> @@ -1386,8 +1381,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 (Regionality, { left = reg0; right = reg1 })) let submode a b = try_with_log (submode_log a b) @@ -1411,70 +1406,60 @@ module Comonadic_with_locality = struct end include Common (Obj) - open Obj - type error = - [ `Locality of Locality.error - | `Linearity of Linearity.error ] + type 'a ax = + | Locality : Locality.Const.t ax + | Linearity : Linearity.Const.t ax - type equate_error = equate_step * error + let axis_of_ax : type a. a ax -> (Const.t, a) C.axis = function + | Locality -> Areality + | Linearity -> Linearity + [@@inline] - let locality m = - S.Positive.via_monotone Locality.Obj.obj (Proj (Obj.obj, Areality)) m + let obj_of_ax : type a. a ax -> a C.obj = function + | Locality -> Locality.Obj.obj + | Linearity -> Linearity.Obj.obj - let min_with_locality m = - S.Positive.via_monotone Obj.obj (Min_with Areality) - (S.Positive.disallow_right m) + type error = Error : 'a ax * 'a Solver.error -> error - let max_with_locality m = - S.Positive.via_monotone Obj.obj (Max_with Areality) - (S.Positive.disallow_left m) + type equate_error = equate_step * error - 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) + open Obj - 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 proj ax m = + Solver.via_monotone (obj_of_ax ax) (Proj (Obj.obj, axis_of_ax ax)) 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 (axis_of_ax 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 (axis_of_ax 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 (axis_of_ax 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 (axis_of_ax 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 Locality 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 } -> @@ -1482,8 +1467,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 (Locality, { left = loc0; right = loc1 })) let submode a b = try_with_log (submode_log a b) @@ -1492,8 +1477,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 Locality m) in + let linearity = Linearity.check_const (proj Linearity m) in locality, linearity end @@ -1511,56 +1496,64 @@ module Monadic = struct end include Common (Obj) - open Obj - type error = [`Uniqueness of Uniqueness.error] + type 'a ax = Uniqueness : Uniqueness.Const.t ax + + let axis_of_ax : type a. a ax -> (Const.t, a) C.axis = function + | Uniqueness -> Uniqueness + + let obj_of_ax : type a. a ax -> a C.obj = function + | Uniqueness -> Uniqueness.Obj.obj + + type error = Error : 'a ax * '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 (obj_of_ax ax) (Proj (Obj.obj, axis_of_ax 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 (axis_of_ax 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 (axis_of_ax 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 (axis_of_ax ax) c) m + + let meet_with ax c m = meet_const (C.min_with Obj.obj (axis_of_ax 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) @@ -1569,7 +1562,7 @@ module Monadic = struct (** overriding to check per-axis *) let check_const m = - let uniqueness = Uniqueness.check_const (uniqueness m) in + let uniqueness = Uniqueness.check_const (proj Uniqueness m) in uniqueness, () end @@ -1606,12 +1599,64 @@ module Value = struct 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 @@ -1652,16 +1697,13 @@ module Value = struct let monadic, b1 = Monadic.newvar_below monadic in { monadic; comonadic }, b0 || b1 - let uniqueness { monadic; _ } = Monadic.uniqueness monadic + let proj_monadic ax { monadic; _ } = Monadic.proj ax monadic - let linearity { comonadic; _ } = Comonadic.linearity comonadic - - let regionality { comonadic; _ } = Comonadic.regionality comonadic + let proj_comonadic ax { comonadic; _ } = Comonadic.proj ax comonadic type error = - [ `Regionality of Regionality.error - | `Uniqueness of Uniqueness.error - | `Linearity of Linearity.error ] + | Monadic of Monadic.error + | Comonadic of Comonadic.error type equate_error = equate_step * error @@ -1670,10 +1712,10 @@ module Value = struct (* 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 e -> Error (Comonadic e) | Ok () -> ( match Monadic.submode_log monadic0 monadic1 ~log with - | Error e -> Error e + | Error e -> Error (Monadic e) | Ok () -> Ok ()) let submode a b = try_with_log (submode_log a b) @@ -1688,93 +1730,53 @@ 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 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 } - let legacy = let comonadic = Comonadic.legacy in let monadic = Monadic.legacy in { comonadic; monadic } - let max_with_uniqueness uniqueness = + 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 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 join_with_monadic ax c { monadic; comonadic } = let comonadic = Comonadic.disallow_left comonadic in - let monadic = Monadic.join_with_uniqueness c monadic in + let monadic = Monadic.join_with ax c monadic in { monadic; comonadic } - let meet_with_uniqueness c { monadic; comonadic } = + let meet_with_monadic ax c { monadic; comonadic } = let comonadic = Comonadic.disallow_right comonadic in - let monadic = Monadic.meet_with_uniqueness c monadic in + let monadic = Monadic.meet_with ax 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 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 meet_with_regionality c { monadic; comonadic } = + let meet_with_comonadic ax c { monadic; comonadic } = let monadic = Monadic.disallow_right monadic in - let comonadic = Comonadic.meet_with_regionality c comonadic in + let comonadic = Comonadic.meet_with ax c comonadic in { comonadic; monadic } - 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 - { 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 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_linearity c { monadic; comonadic } = - let monadic = Monadic.disallow_right monadic in - let comonadic = Comonadic.meet_with_linearity c comonadic in + let comonadic = Comonadic.join_with ax c comonadic in { comonadic; monadic } let join l = @@ -1803,45 +1805,10 @@ 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 - - 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 meet_with c { comonadic; monadic } = + let meet_const c { comonadic; monadic } = let c = split c in - let comonadic = Comonadic.meet_with c.comonadic comonadic in - let monadic = Monadic.meet_with c.monadic monadic 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 } = @@ -1938,26 +1905,23 @@ 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 proj_monadic ax { monadic; _ } = Monadic.proj ax monadic - let locality { comonadic; _ } = Comonadic.locality comonadic + let proj_comonadic ax { comonadic; _ } = Comonadic.proj ax comonadic type error = - [ `Locality of Locality.error - | `Uniqueness of Uniqueness.error - | `Linearity of Linearity.error ] + | Monadic of Monadic.error + | Comonadic of Comonadic.error type equate_error = equate_step * error let submode_log { monadic = monadic0; comonadic = comonadic0 } { monadic = monadic1; comonadic = comonadic1 } ~log = match Monadic.submode_log monadic0 monadic1 ~log with - | Error e -> Error e + | Error e -> Error (Monadic e) | Ok () -> ( match Comonadic.submode_log comonadic0 comonadic1 ~log with - | Error e -> Error e + | Error e -> Error (Comonadic e) | Ok () -> Ok ()) let submode a b = try_with_log (submode_log a b) @@ -1996,68 +1960,48 @@ 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 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 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 join_with_monadic ax c { monadic; comonadic } = let comonadic = Comonadic.disallow_left comonadic in - let monadic = Monadic.join_with_uniqueness c monadic in + let monadic = Monadic.join_with ax c monadic in { monadic; comonadic } - let meet_with_uniqueness c { monadic; comonadic } = + let meet_with_monadic ax c { monadic; comonadic } = let comonadic = Comonadic.disallow_right comonadic in - let monadic = Monadic.meet_with_uniqueness c monadic in + let monadic = Monadic.meet_with ax 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 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 meet_with_locality c { monadic; comonadic } = + let meet_with_comonadic ax c { monadic; comonadic } = let monadic = Monadic.disallow_right monadic in - let comonadic = Comonadic.meet_with_locality c comonadic in - { comonadic; monadic } - - let join_with_locality c { monadic; comonadic } = - let monadic = Monadic.disallow_left monadic in - let comonadic = Comonadic.join_with_locality 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 max_with_linearity linearity = - let comonadic = Comonadic.max_with_linearity linearity in - let monadic = Monadic.max |> Monadic.disallow_left |> Monadic.allow_right in + let comonadic = Comonadic.meet_with ax c comonadic in { comonadic; monadic } - let join_with_linearity c { monadic; comonadic } = + let join_with_comonadic ax c { monadic; comonadic } = let monadic = Monadic.disallow_left monadic in - let comonadic = Comonadic.join_with_linearity c comonadic in - { comonadic; monadic } - - let meet_with_linearity c { monadic; comonadic } = - let monadic = Monadic.disallow_right monadic in - let comonadic = Comonadic.meet_with_linearity c comonadic in + let comonadic = Comonadic.join_with ax c comonadic in { comonadic; monadic } let join l = @@ -2168,8 +2112,8 @@ module Alloc = struct let meet_with c { comonadic; monadic } = let c = split c in - let comonadic = Comonadic.meet_with c.comonadic comonadic in - let monadic = Monadic.meet_with c.monadic monadic 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 } = diff --git a/ocaml/typing/mode_intf.mli b/ocaml/typing/mode_intf.mli index cd4710b4ba1..7aab806c672 100644 --- a/ocaml/typing/mode_intf.mli +++ b/ocaml/typing/mode_intf.mli @@ -123,6 +123,10 @@ module type S = sig type nonrec equate_step = equate_step + type ('a, 'd) monadic constraint 'd = 'l * 'r + + type ('a, 'd) comonadic constraint 'd = 'l * 'r + type ('a, 'b) monadic_comonadic = { monadic : 'a; comonadic : 'b @@ -139,7 +143,11 @@ 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) comonadic val global : lr @@ -164,7 +172,11 @@ 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) comonadic val global : lr @@ -184,7 +196,11 @@ 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) comonadic val many : lr @@ -202,7 +218,11 @@ 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) monadic val shared : lr @@ -212,13 +232,23 @@ module type S = sig (** 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 + type 'a ax = Uniqueness : Uniqueness.Const.t ax - module Comonadic : - Common - with type error = - [ `Regionality of Regionality.error - | `Linearity of Linearity.error ] + type error = Error : 'a ax * 'a Solver.error -> error + + include Common with type error := error + end + + module Comonadic : sig + type 'a ax = + | Regionality : Regionality.Const.t ax + | Linearity : Linearity.Const.t ax + + type error = Error : 'a ax * 'a Solver.error -> error + + include Common with type error := error + end type ('a, 'b, 'c) modes = { regionality : 'a; @@ -232,9 +262,8 @@ module type S = sig (Regionality.Const.t, Linearity.Const.t, Uniqueness.Const.t) modes type error = - [ `Regionality of Regionality.error - | `Uniqueness of Uniqueness.error - | `Linearity of Linearity.error ] + | Monadic of Monadic.error + | Comonadic of Comonadic.error type 'd t = ('d Monadic.t, 'd Comonadic.t) monadic_comonadic @@ -249,45 +278,38 @@ 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 proj_comonadic : + 'a Comonadic.ax -> ('l * 'r) t -> ('a, 'l * 'r) comonadic - val linearity : ('l * 'r) t -> ('l * 'r) Linearity.t + val proj_monadic : 'a Monadic.ax -> ('l * 'r) t -> ('a, 'l * 'r) monadic - val max_with_uniqueness : ('l * 'r) Uniqueness.t -> (disallowed * 'r) t + val max_with_monadic : + 'a Monadic.ax -> ('a, 'l * 'r) monadic -> (disallowed * 'r) t - val min_with_uniqueness : ('l * 'r) Uniqueness.t -> ('l * disallowed) t + val min_with_monadic : + 'a Monadic.ax -> ('a, 'l * 'r) monadic -> ('l * disallowed) t - val min_with_regionality : ('l * 'r) Regionality.t -> ('l * disallowed) t + val min_with_comonadic : + 'a Comonadic.ax -> ('a, 'l * 'r) comonadic -> ('l * disallowed) t - val max_with_regionality : ('l * 'r) Regionality.t -> (disallowed * 'r) t + val max_with_comonadic : + 'a Comonadic.ax -> ('a, 'l * 'r) comonadic -> (disallowed * 'r) t - val min_with_linearity : ('l * 'r) Linearity.t -> ('l * disallowed) t + val meet_with_comonadic : + 'a Comonadic.ax -> 'a -> ('l * 'r) t -> ('l * disallowed) t - val max_with_linearity : ('l * 'r) Linearity.t -> (disallowed * 'r) t + val join_with_comonadic : + 'a Comonadic.ax -> 'a -> ('l * 'r) t -> (disallowed * 'r) t - val meet_with_regionality : - Regionality.Const.t -> ('l * 'r) t -> ('l * disallowed) t + val meet_with_monadic : + 'a Monadic.ax -> 'a -> ('l * 'r) t -> ('l * disallowed) t - val join_with_regionality : - Regionality.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_monadic : + 'a Monadic.ax -> '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 @@ -297,7 +319,11 @@ 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] + type 'a ax = Uniqueness : Uniqueness.Const.t ax + + type error = Error : 'a ax * 'a Solver.error -> error + + include Common with type error := error val imply : Const.t -> ('l * 'r) t -> (disallowed * 'r) t end @@ -309,14 +335,15 @@ module type S = sig val eq : t -> t -> bool end - include - Common - with type error = - [ `Locality of Locality.error - | `Linearity of Linearity.error ] - and module Const := Const + type 'a ax = + | Locality : Locality.Const.t ax + | Linearity : Linearity.Const.t ax + + type error = Error : 'a ax * 'a Solver.error -> error + + include Common with type error := error and 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 = @@ -357,9 +384,8 @@ module type S = sig end type error = - [ `Locality of Locality.error - | `Uniqueness of Uniqueness.error - | `Linearity of Linearity.error ] + | Monadic of Monadic.error + | Comonadic of Comonadic.error type 'd t = ('d Monadic.t, 'd Comonadic.t) monadic_comonadic @@ -371,41 +397,34 @@ 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 min_with_uniqueness : ('l * 'r) Uniqueness.t -> ('l * disallowed) t - - val min_with_locality : ('l * 'r) Locality.t -> ('l * disallowed) t + val proj_comonadic : + 'a Comonadic.ax -> ('l * 'r) t -> ('a, 'l * 'r) comonadic - val max_with_locality : ('l * 'r) Locality.t -> (disallowed * 'r) t + val proj_monadic : 'a Monadic.ax -> ('l * 'r) t -> ('a, 'l * 'r) monadic - val min_with_linearity : ('l * 'r) Linearity.t -> ('l * disallowed) t + val max_with_monadic : + 'a Monadic.ax -> ('a, 'l * 'r) monadic -> (disallowed * 'r) t - val max_with_linearity : ('l * 'r) Linearity.t -> (disallowed * 'r) t + val min_with_monadic : + 'a Monadic.ax -> ('a, 'l * 'r) monadic -> ('l * disallowed) t - val meet_with_locality : - Locality.Const.t -> ('l * 'r) t -> ('l * disallowed) t + val min_with_comonadic : + 'a Comonadic.ax -> ('a, 'l * 'r) comonadic -> ('l * disallowed) t - val join_with_locality : - Locality.Const.t -> ('l * 'r) t -> (disallowed * 'r) t + val max_with_comonadic : + 'a Comonadic.ax -> ('a, 'l * 'r) comonadic -> (disallowed * 'r) t - val meet_with_linearity : - Linearity.Const.t -> ('l * 'r) t -> ('l * disallowed) t + val meet_with_comonadic : + 'a Comonadic.ax -> 'a -> ('l * 'r) t -> ('l * disallowed) t - val join_with_linearity : - Linearity.Const.t -> ('l * 'r) t -> (disallowed * 'r) t + val join_with_comonadic : + 'a Comonadic.ax -> 'a -> ('l * 'r) t -> (disallowed * 'r) t - val meet_with_uniqueness : - Uniqueness.Const.t -> ('l * 'r) t -> ('l * disallowed) t + val meet_with_monadic : + 'a Monadic.ax -> 'a -> ('l * 'r) t -> ('l * disallowed) t - val join_with_uniqueness : - Uniqueness.Const.t -> ('l * 'r) t -> (disallowed * 'r) t + val join_with_monadic : + 'a Monadic.ax -> 'a -> ('l * 'r) t -> (disallowed * 'r) t val zap_to_legacy : lr -> Const.t diff --git a/ocaml/typing/typecore.ml b/ocaml/typing/typecore.ml index 3a8a5b7ca5a..620f40362ba 100644 --- a/ocaml/typing/typecore.ml +++ b/ocaml/typing/typecore.ml @@ -412,17 +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 Regionality Regionality.regional)] let meet_global mode = - Value.meet [mode; (Value.max_with_regionality Regionality.global)] - + Value.meet [mode; (Value.max_with_comonadic Regionality 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 @@ -436,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 Regionality 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 @@ -448,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 @@ -465,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 Regionality mode), FTail); closure_context = Some Return; } @@ -473,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 Regionality mode), FNontail); closure_context = None; } @@ -492,7 +493,8 @@ let mode_global expected_mode = let mode_exclave expected_mode = let mode = - Value.join_with_regionality Regionality.Const.Local expected_mode.mode + Value.join_with_comonadic Regionality + Regionality.Const.Local expected_mode.mode in { (mode_default mode) with strictly_local = true @@ -553,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 Regionality vmode) + Regionality.regional; mode_tailcall_argument vmode, vmode end @@ -795,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. *) @@ -806,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 } @@ -4703,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 @@ -4712,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.Monadic (Error (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.Comonadic (Error (Linearity, e)) in + raise (Error (loc, env, Submode_failed(e, Other, None, None))) ); (Uniqueness.disallow_left Uniqueness.shared, Linearity.disallow_right Linearity.many) @@ -4803,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 Locality alloc_mode); let { ty_fun = { ty = ty_fun; explanation }; loc_fun; region_locked } = in_function in @@ -4868,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 Locality ret_mode) with | Ok () -> mode_default ret_value_mode | Error _ -> raise (Error (loc_fun, env, Function_returns_local)) @@ -5271,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 Regionality Regionality.regional) expected_mode; { exp_desc = Texp_exclave exp; exp_loc = loc; exp_extra = []; @@ -5286,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 Regionality Regionality.regional) + in mode, mode_tailcall_function mode | Nontail | Default -> let mode = Value.newvar () in @@ -5693,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 Regionality rmode)), label_loc, label, newval); exp_loc = loc; exp_extra = []; exp_type = instance Predef.type_unit; @@ -6504,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 Locality mode; + Alloc.max_with_comonadic Linearity Linearity.many]) | _ -> () end; ty, Id_prim (Option.map Locality.disallow_right mode, sort) @@ -7362,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 Regionality 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 @@ -7384,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 Regionality |> regional_to_global |> Locality.disallow_right)} in @@ -7532,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 Locality ret_mode) in let mode_res = mode_cross_left env ty_ret (alloc_as_value ret_mode) in @@ -7594,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 Locality mode_ret) in let mode_ret = mode_cross_left env ty_ret (alloc_as_value mode_ret) in @@ -9380,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 -> + | Comonadic (Error (Regionality, 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 @ @@ -9410,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 Locality res_mode) with | Some Global -> Some (n+1, true) @@ -10038,18 +10052,21 @@ let report_error ~loc env = function -> let sub = match fail_reason with - | `Linearity _ | `Uniqueness _ -> + | Comonadic (Error (Linearity, _)) | Monadic (Error (Uniqueness, _)) -> sharedness_hint fail_reason submode_reason shared_context - | `Regionality _ -> + | Comonadic (Error (Regionality, _)) -> 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 + | Comonadic (Error (Regionality, _)) -> + Format.dprintf "This value escapes its region" + | Monadic (Error (Uniqueness, {left; right})) -> + Format.dprintf "Found a %a value where a %a value was expected" + Uniqueness.Const.print left Uniqueness.Const.print right + | Comonadic (Error (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 = @@ -10087,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) + | Comonadic (Error (Locality, e)) -> + print_error Locality.Const.print (s, e) + | Monadic (Error (Uniqueness, e)) -> + print_error Uniqueness.Const.print (s, e) + | Comonadic (Error (Linearity, e)) -> + print_error Linearity.Const.print (s, e) end | Uncurried_function_escapes e -> begin match e with - | `Locality _ -> + | Comonadic (Error (Locality, _)) -> Location.errorf ~loc "This function or one of its parameters escape their region @ \ when it is partially applied." - | `Uniqueness _ -> assert false - | `Linearity {left; right} -> + | Monadic (Error (Uniqueness, _)) -> assert false + | Comonadic (Error (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..5eb29758411 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 Locality 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 Locality mret)) ~global_repr ~is_layout_poly in ((mode, repr_arg) :: repr_args, repr_res) From eceb41348fb1b95273a2c78f04910c13878abab8 Mon Sep 17 00:00:00 2001 From: Zesen Qian Date: Wed, 3 Apr 2024 10:50:24 +0100 Subject: [PATCH 4/5] reuse existing representation of axis --- ocaml/lambda/translmode.ml | 4 +- ocaml/typing/ctype.ml | 6 +- ocaml/typing/env.ml | 8 +- ocaml/typing/mode.ml | 275 +++++++++++++++---------------------- ocaml/typing/mode_intf.mli | 127 ++++++++++------- ocaml/typing/typecore.ml | 46 +++---- ocaml/typing/typedecl.ml | 4 +- ocaml/typing/typemode.ml | 15 +- 8 files changed, 227 insertions(+), 258 deletions(-) diff --git a/ocaml/lambda/translmode.ml b/ocaml/lambda/translmode.ml index 3d45f47f51d..860a069317c 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.proj_comonadic 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.proj_comonadic 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 48d89bd4e46..d0579a77163 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.proj_comonadic Locality m') locality; - Alloc.submode_exn m' (Alloc.join_with_comonadic Locality Locality.Const.max m); - Alloc.submode_exn (Alloc.meet_with_comonadic 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 = diff --git a/ocaml/typing/env.ml b/ocaml/typing/env.ml index a5cc4320a2f..608f03611fa 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.proj_comonadic Regionality vmode) + (Mode.Value.proj_comonadic Areality vmode) (Mode.Regionality.global) with | Ok () -> () @@ -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.proj_comonadic Regionality vmode) + (Mode.Value.proj_comonadic Areality vmode) Mode.Regionality.regional with | Ok () -> vmode |> Mode.value_to_alloc_r2l |> Mode.alloc_as_value @@ -3962,7 +3962,7 @@ let report_lookup_error _loc env ppf = function | Value_used_in_closure (lid, error, context) -> let e0, e1 = match error with - | Error (Regionality, _) -> "local", "might escape" + | Error (Areality, _) -> "local", "might escape" | Error (Linearity, _) -> "once", "is many" in fprintf ppf @@ -3970,7 +3970,7 @@ let report_lookup_error _loc env ppf = function inside a closure that %s.@]" !print_longident lid e0 e1; begin match error, context with - | Error (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 635d10f4259..1e0ca063b99 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,9 +1102,9 @@ let append_changes : (changes ref -> unit) ref = ref (fun _ -> assert false) let set_append_changes f = append_changes := f -type ('a, 'd) monadic = ('a, 'd) S.Negative.mode +type ('a, 'd) mode_monadic = ('a, 'd) S.Negative.mode -type ('a, 'd) comonadic = ('a, 'd) S.Positive.mode +type ('a, 'd) mode_comonadic = ('a, 'd) S.Positive.mode (** Representing a single object *) module type Obj = sig @@ -1325,28 +1318,13 @@ module Comonadic_with_regionality = struct include Common (Obj) - type 'a ax = - | Regionality : Regionality.Const.t ax - | Linearity : Linearity.Const.t ax - - let axis_of_ax : type a. a ax -> (Const.t, a) C.axis = function - | Regionality -> Areality - | Linearity -> Linearity - [@@inline] - - let obj_of_ax : type a. a ax -> a C.obj = function - | Regionality -> Regionality.Obj.obj - | Linearity -> Linearity.Obj.obj - [@@inline] - - type error = Error : 'a ax * 'a Solver.error -> error + type error = Error : (Const.t, 'a) C.Axis.t * 'a Solver.error -> error type equate_error = equate_step * error open Obj - let proj ax m = - Solver.via_monotone (obj_of_ax ax) (Proj (Obj.obj, axis_of_ax ax)) m + let proj ax m = Solver.via_monotone (C.proj_obj ax obj) (Proj (Obj.obj, ax)) m let meet_const c m = Solver.via_monotone obj (Meet_with c) (Solver.disallow_right m) @@ -1355,18 +1333,14 @@ module Comonadic_with_regionality = struct Solver.via_monotone obj (Join_with c) (Solver.disallow_left m) let min_with ax m = - Solver.via_monotone Obj.obj - (Min_with (axis_of_ax ax)) - (Solver.disallow_right m) + Solver.via_monotone Obj.obj (Min_with ax) (Solver.disallow_right m) let max_with ax m = - Solver.via_monotone Obj.obj - (Max_with (axis_of_ax ax)) - (Solver.disallow_left m) + Solver.via_monotone Obj.obj (Max_with ax) (Solver.disallow_left m) - let join_with ax c m = join_const (C.min_with Obj.obj (axis_of_ax ax) c) m + let join_with ax c m = join_const (C.min_with Obj.obj ax c) m - let meet_with ax c m = meet_const (C.max_with Obj.obj (axis_of_ax ax) c) 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) @@ -1382,7 +1356,7 @@ module Comonadic_with_regionality = struct if Linearity.Const.le lin0 lin1 then assert false else Error (Error (Linearity, { left = lin0; right = lin1 })) - else Error (Error (Regionality, { left = reg0; right = reg1 })) + else Error (Error (Areality, { left = reg0; right = reg1 })) let submode a b = try_with_log (submode_log a b) @@ -1407,27 +1381,13 @@ module Comonadic_with_locality = struct include Common (Obj) - type 'a ax = - | Locality : Locality.Const.t ax - | Linearity : Linearity.Const.t ax - - let axis_of_ax : type a. a ax -> (Const.t, a) C.axis = function - | Locality -> Areality - | Linearity -> Linearity - [@@inline] - - let obj_of_ax : type a. a ax -> a C.obj = function - | Locality -> Locality.Obj.obj - | Linearity -> Linearity.Obj.obj - - type error = Error : 'a ax * 'a Solver.error -> error + type error = Error : (Const.t, 'a) C.Axis.t * 'a Solver.error -> error type equate_error = equate_step * error open Obj - let proj ax m = - Solver.via_monotone (obj_of_ax ax) (Proj (Obj.obj, axis_of_ax ax)) m + let proj ax m = Solver.via_monotone (C.proj_obj ax obj) (Proj (Obj.obj, ax)) m let meet_const c m = Solver.via_monotone obj (Meet_with c) (Solver.disallow_right m) @@ -1436,21 +1396,17 @@ module Comonadic_with_locality = struct Solver.via_monotone obj (Join_with c) (Solver.disallow_left m) let min_with ax m = - Solver.via_monotone Obj.obj - (Min_with (axis_of_ax ax)) - (Solver.disallow_right m) + Solver.via_monotone Obj.obj (Min_with ax) (Solver.disallow_right m) let max_with ax m = - Solver.via_monotone Obj.obj - (Max_with (axis_of_ax ax)) - (Solver.disallow_left m) + Solver.via_monotone Obj.obj (Max_with ax) (Solver.disallow_left m) - let join_with ax c m = join_const (C.min_with Obj.obj (axis_of_ax ax) c) m + let join_with ax c m = join_const (C.min_with Obj.obj ax c) m - let meet_with ax c m = meet_const (C.max_with Obj.obj (axis_of_ax ax) c) m + let meet_with ax c m = meet_const (C.max_with Obj.obj ax c) m let zap_to_legacy m = - let locality = proj Locality m |> Locality.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 @@ -1468,7 +1424,7 @@ module Comonadic_with_locality = struct if Linearity.Const.le lin0 lin1 then assert false else Error (Error (Linearity, { left = lin0; right = lin1 })) - else Error (Error (Locality, { left = loc0; right = loc1 })) + else Error (Error (Areality, { left = loc0; right = loc1 })) let submode a b = try_with_log (submode_log a b) @@ -1477,7 +1433,7 @@ module Comonadic_with_locality = struct (** overriding to check per-axis *) let check_const m = - let locality = Locality.check_const (proj Locality m) in + let locality = Locality.check_const (proj Areality m) in let linearity = Linearity.check_const (proj Linearity m) in locality, linearity end @@ -1497,22 +1453,13 @@ module Monadic = struct include Common (Obj) - type 'a ax = Uniqueness : Uniqueness.Const.t ax - - let axis_of_ax : type a. a ax -> (Const.t, a) C.axis = function - | Uniqueness -> Uniqueness - - let obj_of_ax : type a. a ax -> a C.obj = function - | Uniqueness -> Uniqueness.Obj.obj - - type error = Error : 'a ax * 'a Solver.error -> error + type error = Error : (Const.t, 'a) C.Axis.t * 'a Solver.error -> error type equate_error = equate_step * error open Obj - let proj ax m = - Solver.via_monotone (obj_of_ax ax) (Proj (Obj.obj, axis_of_ax ax)) m + 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 @@ -1525,18 +1472,14 @@ module Monadic = struct Solver.via_monotone obj (Meet_with c) (Solver.disallow_left m) let max_with ax m = - Solver.via_monotone Obj.obj - (Min_with (axis_of_ax ax)) - (Solver.disallow_left m) + Solver.via_monotone Obj.obj (Min_with ax) (Solver.disallow_left m) let min_with ax m = - Solver.via_monotone Obj.obj - (Max_with (axis_of_ax ax)) - (Solver.disallow_right m) + Solver.via_monotone Obj.obj (Max_with ax) (Solver.disallow_right m) - let join_with ax c m = join_const (C.max_with Obj.obj (axis_of_ax ax) c) 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 (axis_of_ax 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) diff --git a/ocaml/typing/mode_intf.mli b/ocaml/typing/mode_intf.mli index 7aab806c672..a3c4e11eab4 100644 --- a/ocaml/typing/mode_intf.mli +++ b/ocaml/typing/mode_intf.mli @@ -93,16 +93,6 @@ module type Common = sig 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 @@ -123,9 +113,9 @@ module type S = sig type nonrec equate_step = equate_step - type ('a, 'd) monadic constraint 'd = 'l * 'r + type ('a, 'd) mode_monadic constraint 'd = 'l * 'r - type ('a, 'd) comonadic constraint 'd = 'l * 'r + type ('a, 'd) mode_comonadic constraint 'd = 'l * 'r type ('a, 'b) monadic_comonadic = { monadic : 'a; @@ -147,7 +137,7 @@ module type S = sig Common with module Const := Const and type error := error - and type 'd t = (Const.t, 'd) comonadic + and type 'd t = (Const.t, 'd) mode_comonadic val global : lr @@ -176,7 +166,7 @@ module type S = sig Common with module Const := Const and type error := error - and type 'd t = (Const.t, 'd) comonadic + and type 'd t = (Const.t, 'd) mode_comonadic val global : lr @@ -200,7 +190,7 @@ module type S = sig Common with module Const := Const and type error := error - and type 'd t = (Const.t, 'd) comonadic + and type 'd t = (Const.t, 'd) mode_comonadic val many : lr @@ -222,32 +212,45 @@ module type S = sig Common with module Const := Const and type error := error - and type 'd t = (Const.t, 'd) monadic + 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 + + 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 : sig - type 'a ax = Uniqueness : Uniqueness.Const.t ax + module Const : Lattice with type t = monadic - type error = Error : 'a ax * 'a Solver.error -> error + type error = Error : (Const.t, 'a) Axis.t * 'a Solver.error -> error - include Common with type error := error + include Common with type error := error and module Const := Const end module Comonadic : sig - type 'a ax = - | Regionality : Regionality.Const.t ax - | Linearity : Linearity.Const.t ax + module Const : Lattice with type t = Regionality.Const.t comonadic_with - type error = Error : 'a ax * 'a Solver.error -> error + type error = Error : (Const.t, 'a) Axis.t * 'a Solver.error -> error - include Common with type error := error + include Common with type error := error and module Const := Const end type ('a, 'b, 'c) modes = @@ -279,33 +282,44 @@ module type S = sig end val proj_comonadic : - 'a Comonadic.ax -> ('l * 'r) t -> ('a, 'l * 'r) comonadic + (Comonadic.Const.t, 'a) Axis.t -> + ('l * 'r) t -> + ('a, 'l * 'r) mode_comonadic - val proj_monadic : 'a Monadic.ax -> ('l * 'r) t -> ('a, 'l * 'r) monadic + val proj_monadic : + (Monadic.Const.t, 'a) Axis.t -> ('l * 'r) t -> ('a, 'l * 'r) mode_monadic val max_with_monadic : - 'a Monadic.ax -> ('a, 'l * 'r) monadic -> (disallowed * 'r) t + (Monadic.Const.t, 'a) Axis.t -> + ('a, 'l * 'r) mode_monadic -> + (disallowed * 'r) t val min_with_monadic : - 'a Monadic.ax -> ('a, 'l * 'r) monadic -> ('l * disallowed) t + (Monadic.Const.t, 'a) Axis.t -> + ('a, 'l * 'r) mode_monadic -> + ('l * disallowed) t val min_with_comonadic : - 'a Comonadic.ax -> ('a, 'l * 'r) comonadic -> ('l * disallowed) t + (Comonadic.Const.t, 'a) Axis.t -> + ('a, 'l * 'r) mode_comonadic -> + ('l * disallowed) t val max_with_comonadic : - 'a Comonadic.ax -> ('a, 'l * 'r) comonadic -> (disallowed * 'r) t + (Comonadic.Const.t, 'a) Axis.t -> + ('a, 'l * 'r) mode_comonadic -> + (disallowed * 'r) t val meet_with_comonadic : - 'a Comonadic.ax -> 'a -> ('l * 'r) t -> ('l * disallowed) t + (Comonadic.Const.t, 'a) Axis.t -> 'a -> ('l * 'r) t -> ('l * disallowed) t val join_with_comonadic : - 'a Comonadic.ax -> 'a -> ('l * 'r) t -> (disallowed * 'r) t + (Comonadic.Const.t, 'a) Axis.t -> 'a -> ('l * 'r) t -> (disallowed * 'r) t val meet_with_monadic : - 'a Monadic.ax -> 'a -> ('l * 'r) t -> ('l * disallowed) t + (Monadic.Const.t, 'a) Axis.t -> 'a -> ('l * 'r) t -> ('l * disallowed) t val join_with_monadic : - 'a Monadic.ax -> 'a -> ('l * 'r) t -> (disallowed * 'r) t + (Monadic.Const.t, 'a) Axis.t -> 'a -> ('l * 'r) t -> (disallowed * 'r) t val comonadic_to_monadic : ('l * 'r) Comonadic.t -> ('r * 'l) Monadic.t @@ -319,27 +333,23 @@ module type S = sig and would be hard to understand if it involves [Regionality]. *) module Alloc : sig module Monadic : sig - type 'a ax = Uniqueness : Uniqueness.Const.t ax + module Const : Lattice with type t = monadic - type error = Error : 'a ax * 'a Solver.error -> error + type error = Error : (Const.t, 'a) Axis.t * 'a Solver.error -> error - include Common with type error := error + include Common with type error := error and 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 - type 'a ax = - | Locality : Locality.Const.t ax - | Linearity : Linearity.Const.t ax - - type error = Error : 'a ax * 'a Solver.error -> error + type error = Error : (Const.t, 'a) Axis.t * 'a Solver.error -> error include Common with type error := error and module Const := Const @@ -398,33 +408,44 @@ module type S = sig val check_const : (allowed * allowed) t -> Const.Option.t val proj_comonadic : - 'a Comonadic.ax -> ('l * 'r) t -> ('a, 'l * 'r) comonadic + (Comonadic.Const.t, 'a) Axis.t -> + ('l * 'r) t -> + ('a, 'l * 'r) mode_comonadic - val proj_monadic : 'a Monadic.ax -> ('l * 'r) t -> ('a, 'l * 'r) monadic + val proj_monadic : + (Monadic.Const.t, 'a) Axis.t -> ('l * 'r) t -> ('a, 'l * 'r) mode_monadic val max_with_monadic : - 'a Monadic.ax -> ('a, 'l * 'r) monadic -> (disallowed * 'r) t + (Monadic.Const.t, 'a) Axis.t -> + ('a, 'l * 'r) mode_monadic -> + (disallowed * 'r) t val min_with_monadic : - 'a Monadic.ax -> ('a, 'l * 'r) monadic -> ('l * disallowed) t + (Monadic.Const.t, 'a) Axis.t -> + ('a, 'l * 'r) mode_monadic -> + ('l * disallowed) t val min_with_comonadic : - 'a Comonadic.ax -> ('a, 'l * 'r) comonadic -> ('l * disallowed) t + (Comonadic.Const.t, 'a) Axis.t -> + ('a, 'l * 'r) mode_comonadic -> + ('l * disallowed) t val max_with_comonadic : - 'a Comonadic.ax -> ('a, 'l * 'r) comonadic -> (disallowed * 'r) t + (Comonadic.Const.t, 'a) Axis.t -> + ('a, 'l * 'r) mode_comonadic -> + (disallowed * 'r) t val meet_with_comonadic : - 'a Comonadic.ax -> 'a -> ('l * 'r) t -> ('l * disallowed) t + (Comonadic.Const.t, 'a) Axis.t -> 'a -> ('l * 'r) t -> ('l * disallowed) t val join_with_comonadic : - 'a Comonadic.ax -> 'a -> ('l * 'r) t -> (disallowed * 'r) t + (Comonadic.Const.t, 'a) Axis.t -> 'a -> ('l * 'r) t -> (disallowed * 'r) t val meet_with_monadic : - 'a Monadic.ax -> 'a -> ('l * 'r) t -> ('l * disallowed) t + (Monadic.Const.t, 'a) Axis.t -> 'a -> ('l * 'r) t -> ('l * disallowed) t val join_with_monadic : - 'a Monadic.ax -> 'a -> ('l * 'r) t -> (disallowed * 'r) t + (Monadic.Const.t, 'a) Axis.t -> 'a -> ('l * 'r) t -> (disallowed * 'r) t val zap_to_legacy : lr -> Const.t diff --git a/ocaml/typing/typecore.ml b/ocaml/typing/typecore.ml index 620f40362ba..21d55c154a9 100644 --- a/ocaml/typing/typecore.ml +++ b/ocaml/typing/typecore.ml @@ -412,10 +412,10 @@ 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_comonadic Regionality Regionality.regional)] + Value.meet [mode; (Value.max_with_comonadic Areality Regionality.regional)] let meet_global mode = - Value.meet [mode; (Value.max_with_comonadic Regionality Regionality.global)] + Value.meet [mode; (Value.max_with_comonadic Areality Regionality.global)] let meet_many mode = Value.meet [mode; (Value.max_with_comonadic Linearity Linearity.many)] @@ -435,7 +435,7 @@ let modality_unbox_left global_flag mode = match global_flag with | Global_flag.Global -> mode - |> Value.meet_with_comonadic Regionality Regionality.Const.Global + |> Value.meet_with_comonadic Areality Regionality.Const.Global |> join_shared |> Value.meet_with_comonadic Linearity Linearity.Const.Many | Global_flag.Unrestricted -> mode @@ -465,7 +465,7 @@ mode is the mode of the function region *) let mode_return mode = { (mode_default (meet_regional mode)) with position = RTail (Regionality.disallow_left - (Value.proj_comonadic Regionality mode), FTail); + (Value.proj_comonadic Areality mode), FTail); closure_context = Some Return; } @@ -474,7 +474,7 @@ let mode_region mode = { (mode_default (meet_regional mode)) with position = RTail (Regionality.disallow_left - (Value.proj_comonadic Regionality mode), FNontail); + (Value.proj_comonadic Areality mode), FNontail); closure_context = None; } @@ -493,7 +493,7 @@ let mode_global expected_mode = let mode_exclave expected_mode = let mode = - Value.join_with_comonadic Regionality + Value.join_with_comonadic Areality Regionality.Const.Local expected_mode.mode in { (mode_default mode) @@ -555,7 +555,7 @@ let mode_argument ~funct ~index ~position_and_mode ~partial_app marg = | _, _, (Nontail | Default) -> mode_default vmode, vmode | _, _, Tail -> begin - Regionality.submode_exn (Value.proj_comonadic Regionality vmode) + Regionality.submode_exn (Value.proj_comonadic Areality vmode) Regionality.regional; mode_tailcall_argument vmode, vmode end @@ -4808,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.proj_comonadic 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 @@ -4873,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.proj_comonadic 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)) @@ -5276,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_comonadic Regionality Regionality.regional) expected_mode; + (Value.min_with_comonadic Areality Regionality.regional) expected_mode; { exp_desc = Texp_exclave exp; exp_loc = loc; exp_extra = []; @@ -5293,7 +5293,7 @@ and type_expect_ | Tail -> let mode, _ = Value.newvar_below - (Value.max_with_comonadic Regionality Regionality.regional) + (Value.max_with_comonadic Areality Regionality.regional) in mode, mode_tailcall_function mode | Nontail | Default -> @@ -5702,7 +5702,7 @@ and type_expect_ rue { exp_desc = Texp_setfield(record, Locality.disallow_right (regional_to_local - (Value.proj_comonadic Regionality rmode)), + (Value.proj_comonadic Areality rmode)), label_loc, label, newval); exp_loc = loc; exp_extra = []; exp_type = instance Predef.type_unit; @@ -6513,7 +6513,7 @@ 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_comonadic Locality mode; + (Alloc.meet [Alloc.max_with_comonadic Areality mode; Alloc.max_with_comonadic Linearity Linearity.many]) | _ -> () end; @@ -7372,7 +7372,7 @@ and type_argument ?explanation ?recarg env (mode : expected_mode) sarg in let eta_mode, _ = Value.newvar_below (alloc_as_value marg) in Regionality.submode_exn - (Value.proj_comonadic Regionality eta_mode) Regionality.regional; + (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 @@ -7394,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.proj_comonadic Regionality + |> Value.proj_comonadic Areality |> regional_to_global |> Locality.disallow_right)} in @@ -7542,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.proj_comonadic 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 @@ -7604,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.proj_comonadic 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 @@ -9390,7 +9390,7 @@ 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 - | Comonadic (Error (Regionality, e)), Some h -> + | Comonadic (Error (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 @@ -9424,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.proj_comonadic Locality res_mode) + Locality.check_const (Alloc.proj_comonadic Areality res_mode) with | Some Global -> Some (n+1, true) @@ -10054,12 +10054,12 @@ let report_error ~loc env = function match fail_reason with | Comonadic (Error (Linearity, _)) | Monadic (Error (Uniqueness, _)) -> sharedness_hint fail_reason submode_reason shared_context - | Comonadic (Error (Regionality, _)) -> + | Comonadic (Error (Areality, _)) -> escaping_hint fail_reason submode_reason closure_context in Location.errorf ~loc ~sub "%t" begin match fail_reason with - | Comonadic (Error (Regionality, _)) -> + | Comonadic (Error (Areality, _)) -> Format.dprintf "This value escapes its region" | Monadic (Error (Uniqueness, {left; right})) -> Format.dprintf "Found a %a value where a %a value was expected" @@ -10104,7 +10104,7 @@ let report_error ~loc env = function f actual f expected in begin match mkind with - | Comonadic (Error (Locality, e)) -> + | Comonadic (Error (Areality, e)) -> print_error Locality.Const.print (s, e) | Monadic (Error (Uniqueness, e)) -> print_error Uniqueness.Const.print (s, e) @@ -10113,7 +10113,7 @@ let report_error ~loc env = function end | Uncurried_function_escapes e -> begin match e with - | Comonadic (Error (Locality, _)) -> + | Comonadic (Error (Areality, _)) -> Location.errorf ~loc "This function or one of its parameters escape their region @ \ when it is partially applied." | Monadic (Error (Uniqueness, _)) -> assert false diff --git a/ocaml/typing/typedecl.ml b/ocaml/typing/typedecl.ml index 5eb29758411..1a754d2637b 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.proj_comonadic 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.proj_comonadic 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 From e036610ff240d53ed657fbad9085b1bf496a81a9 Mon Sep 17 00:00:00 2001 From: Zesen Qian Date: Wed, 3 Apr 2024 17:15:47 +0100 Subject: [PATCH 5/5] decompose monadic vs. comonadic --- ocaml/lambda/translmode.ml | 4 +- ocaml/typing/ctype.ml | 8 +- ocaml/typing/env.ml | 8 +- ocaml/typing/mode.ml | 174 ++++++++++++++++++++++++++----------- ocaml/typing/mode_intf.mli | 122 ++++++++------------------ ocaml/typing/typecore.ml | 78 ++++++++--------- ocaml/typing/typedecl.ml | 4 +- 7 files changed, 212 insertions(+), 186 deletions(-) diff --git a/ocaml/lambda/translmode.ml b/ocaml/lambda/translmode.ml index 860a069317c..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.proj_comonadic Areality 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.proj_comonadic Areality 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 d0579a77163..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.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'; + 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 608f03611fa..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.proj_comonadic Areality 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.proj_comonadic 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_monadic 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.proj_comonadic Areality vmode) + (Mode.Value.proj (Comonadic Areality) vmode) Mode.Regionality.regional with | Ok () -> vmode |> Mode.value_to_alloc_r2l |> Mode.alloc_as_value diff --git a/ocaml/typing/mode.ml b/ocaml/typing/mode.ml index 1e0ca063b99..6eff3ff6fcf 100644 --- a/ocaml/typing/mode.ml +++ b/ocaml/typing/mode.ml @@ -1526,6 +1526,14 @@ 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; @@ -1640,25 +1648,19 @@ module Value = struct let monadic, b1 = Monadic.newvar_below monadic in { monadic; comonadic }, b0 || b1 - let proj_monadic ax { monadic; _ } = Monadic.proj ax monadic - - let proj_comonadic ax { comonadic; _ } = Comonadic.proj ax comonadic - - type error = - | Monadic of Monadic.error - | Comonadic of Comonadic.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 (Comonadic e) + | Error (Error (ax, e)) -> Error (Error (Comonadic ax, e)) | Ok () -> ( match Monadic.submode_log monadic0 monadic1 ~log with - | Error e -> Error (Monadic e) + | Error (Error (ax, e)) -> Error (Error (Monadic ax, e)) | Ok () -> Ok ()) let submode a b = try_with_log (submode_log a b) @@ -1678,6 +1680,16 @@ module Value = struct let monadic = Monadic.legacy in { comonadic; monadic } + 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 @@ -1685,6 +1697,17 @@ module Value = struct 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 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 @@ -1692,35 +1715,50 @@ module Value = struct let monadic = Monadic.min_with ax m in { comonadic; monadic } + 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 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 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_comonadic ax c { monadic; comonadic } = + let monadic = Monadic.disallow_left monadic in + let comonadic = Comonadic.join_with ax c comonadic 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 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 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_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 meet_with_comonadic ax c { monadic; comonadic } = let monadic = Monadic.disallow_right monadic in let comonadic = Comonadic.meet_with ax c comonadic in { comonadic; monadic } - let join_with_comonadic ax c { monadic; comonadic } = - let monadic = Monadic.disallow_left monadic in - let comonadic = Comonadic.join_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 = @@ -1789,6 +1827,14 @@ 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; @@ -1848,23 +1894,17 @@ module Alloc = struct let monadic, b1 = Monadic.newvar_below monadic in { monadic; comonadic }, b0 || b1 - let proj_monadic ax { monadic; _ } = Monadic.proj ax monadic - - let proj_comonadic ax { comonadic; _ } = Comonadic.proj ax comonadic - - type error = - | Monadic of Monadic.error - | Comonadic of Comonadic.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 (Monadic e) + | Error (Error (ax, e)) -> Error (Error (Monadic ax, e)) | Ok () -> ( match Comonadic.submode_log comonadic0 comonadic1 ~log with - | Error e -> Error (Comonadic e) + | Error (Error (ax, e)) -> Error (Error (Comonadic ax, e)) | Ok () -> Ok ()) let submode a b = try_with_log (submode_log a b) @@ -1903,6 +1943,16 @@ module Alloc = struct on modes numerically, instead of defining symbolic functions *) (* type const = (LR.Const.t, Linearity.Const.t, Uniqueness.Const.t) modes *) + 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 @@ -1910,6 +1960,17 @@ module Alloc = struct 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 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 @@ -1917,35 +1978,50 @@ module Alloc = struct let monadic = Monadic.min_with ax m in { comonadic; monadic } + 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 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 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_comonadic ax c { monadic; comonadic } = + let monadic = Monadic.disallow_left monadic in + let comonadic = Comonadic.join_with ax c comonadic 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 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 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_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 meet_with_comonadic ax c { monadic; comonadic } = let monadic = Monadic.disallow_right monadic in let comonadic = Comonadic.meet_with ax c comonadic in { comonadic; monadic } - let join_with_comonadic ax c { monadic; comonadic } = - let monadic = Monadic.disallow_left monadic in - let comonadic = Comonadic.join_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 = @@ -2053,7 +2129,7 @@ module Alloc = struct let merge = merge end - let meet_with c { comonadic; monadic } = + 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 diff --git a/ocaml/typing/mode_intf.mli b/ocaml/typing/mode_intf.mli index a3c4e11eab4..52776ff3f50 100644 --- a/ocaml/typing/mode_intf.mli +++ b/ocaml/typing/mode_intf.mli @@ -240,9 +240,7 @@ module type S = sig module Monadic : sig module Const : Lattice with type t = monadic - type error = Error : (Const.t, 'a) Axis.t * 'a Solver.error -> error - - include Common with type error := error and module Const := Const + include Common with module Const := Const end module Comonadic : sig @@ -264,9 +262,17 @@ module type S = sig with type t = (Regionality.Const.t, Linearity.Const.t, Uniqueness.Const.t) modes - type error = - | Monadic of Monadic.error - | Comonadic of Comonadic.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 @@ -281,45 +287,15 @@ module type S = sig include Allow_disallow with type (_, _, 'd) sided = 'd t list end - val proj_comonadic : - (Comonadic.Const.t, 'a) Axis.t -> - ('l * 'r) t -> - ('a, 'l * 'r) mode_comonadic - - val proj_monadic : - (Monadic.Const.t, 'a) Axis.t -> ('l * 'r) t -> ('a, 'l * 'r) mode_monadic - - val max_with_monadic : - (Monadic.Const.t, 'a) Axis.t -> - ('a, 'l * 'r) mode_monadic -> - (disallowed * 'r) t + val proj : ('m, 'a, 'l * 'r) axis -> ('l * 'r) t -> 'm - val min_with_monadic : - (Monadic.Const.t, 'a) Axis.t -> - ('a, 'l * 'r) mode_monadic -> - ('l * disallowed) t + val max_with : ('m, 'a, 'l * 'r) axis -> 'm -> (disallowed * 'r) t - val min_with_comonadic : - (Comonadic.Const.t, 'a) Axis.t -> - ('a, 'l * 'r) mode_comonadic -> - ('l * disallowed) t + val min_with : ('m, 'a, 'l * 'r) axis -> 'm -> ('l * disallowed) t - val max_with_comonadic : - (Comonadic.Const.t, 'a) Axis.t -> - ('a, 'l * 'r) mode_comonadic -> - (disallowed * 'r) t + val meet_with : (_, 'a, _) axis -> 'a -> ('l * 'r) t -> ('l * disallowed) t - val meet_with_comonadic : - (Comonadic.Const.t, 'a) Axis.t -> 'a -> ('l * 'r) t -> ('l * disallowed) t - - val join_with_comonadic : - (Comonadic.Const.t, 'a) Axis.t -> 'a -> ('l * 'r) t -> (disallowed * 'r) t - - val meet_with_monadic : - (Monadic.Const.t, 'a) Axis.t -> 'a -> ('l * 'r) t -> ('l * disallowed) t - - val join_with_monadic : - (Monadic.Const.t, 'a) Axis.t -> 'a -> ('l * 'r) t -> (disallowed * 'r) 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 @@ -335,9 +311,7 @@ module type S = sig module Monadic : sig module Const : Lattice with type t = monadic - type error = Error : (Const.t, 'a) Axis.t * 'a Solver.error -> error - - include Common with type error := error and module Const := Const + include Common with module Const := Const val imply : Const.t -> ('l * 'r) t -> (disallowed * 'r) t end @@ -349,9 +323,7 @@ module type S = sig val eq : t -> t -> bool end - type error = Error : (Const.t, 'a) Axis.t * 'a Solver.error -> error - - include Common with type error := error and module Const := Const + include Common with module Const := Const val meet_const : Const.t -> ('l * 'r) t -> ('l * disallowed) t end @@ -393,9 +365,17 @@ module type S = sig val partial_apply : t -> t end - type error = - | Monadic of Monadic.error - | Comonadic of Comonadic.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 @@ -407,51 +387,21 @@ module type S = sig val check_const : (allowed * allowed) t -> Const.Option.t - val proj_comonadic : - (Comonadic.Const.t, 'a) Axis.t -> - ('l * 'r) t -> - ('a, 'l * 'r) mode_comonadic - - val proj_monadic : - (Monadic.Const.t, 'a) Axis.t -> ('l * 'r) t -> ('a, 'l * 'r) mode_monadic + val proj : ('m, 'a, 'l * 'r) axis -> ('l * 'r) t -> 'm - val max_with_monadic : - (Monadic.Const.t, 'a) Axis.t -> - ('a, 'l * 'r) mode_monadic -> - (disallowed * 'r) t + val max_with : ('m, 'a, 'l * 'r) axis -> 'm -> (disallowed * 'r) t - val min_with_monadic : - (Monadic.Const.t, 'a) Axis.t -> - ('a, 'l * 'r) mode_monadic -> - ('l * disallowed) t + val min_with : ('m, 'a, 'l * 'r) axis -> 'm -> ('l * disallowed) t - val min_with_comonadic : - (Comonadic.Const.t, 'a) Axis.t -> - ('a, 'l * 'r) mode_comonadic -> - ('l * disallowed) t + val meet_with : (_, 'a, _) axis -> 'a -> ('l * 'r) t -> ('l * disallowed) t - val max_with_comonadic : - (Comonadic.Const.t, 'a) Axis.t -> - ('a, 'l * 'r) mode_comonadic -> - (disallowed * 'r) t - - val meet_with_comonadic : - (Comonadic.Const.t, 'a) Axis.t -> 'a -> ('l * 'r) t -> ('l * disallowed) t - - val join_with_comonadic : - (Comonadic.Const.t, 'a) Axis.t -> 'a -> ('l * 'r) t -> (disallowed * 'r) t - - val meet_with_monadic : - (Monadic.Const.t, 'a) Axis.t -> 'a -> ('l * 'r) t -> ('l * disallowed) t - - val join_with_monadic : - (Monadic.Const.t, 'a) Axis.t -> 'a -> ('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 zap_to_ceil : ('l * allowed) t -> Const.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 diff --git a/ocaml/typing/typecore.ml b/ocaml/typing/typecore.ml index 21d55c154a9..465746eb2ae 100644 --- a/ocaml/typing/typecore.ml +++ b/ocaml/typing/typecore.ml @@ -412,16 +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_comonadic Areality Regionality.regional)] + Value.meet [mode; (Value.max_with (Comonadic Areality) Regionality.regional)] let meet_global mode = - Value.meet [mode; (Value.max_with_comonadic Areality Regionality.global)] + Value.meet [mode; (Value.max_with (Comonadic Areality) Regionality.global)] let meet_many mode = - Value.meet [mode; (Value.max_with_comonadic Linearity Linearity.many)] + Value.meet [mode; (Value.max_with (Comonadic Linearity) Linearity.many)] let join_shared mode = - Value.join [mode; Value.min_with_monadic Uniqueness Uniqueness.shared] + Value.join [mode; Value.min_with (Monadic Uniqueness) Uniqueness.shared] let value_regional_to_local mode = mode @@ -435,9 +435,9 @@ let modality_unbox_left global_flag mode = match global_flag with | Global_flag.Global -> mode - |> Value.meet_with_comonadic Areality Regionality.Const.Global + |> Value.meet_with (Comonadic Areality) Regionality.Const.Global |> join_shared - |> Value.meet_with_comonadic 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 @@ -447,7 +447,7 @@ let modality_box_right global_flag mode = | Global_flag.Global -> mode |> meet_global - |> Value.join_with_monadic Uniqueness Uniqueness.Const.max + |> Value.join_with (Monadic Uniqueness) Uniqueness.Const.max |> meet_many | Global_flag.Unrestricted -> mode @@ -465,7 +465,7 @@ mode is the mode of the function region *) let mode_return mode = { (mode_default (meet_regional mode)) with position = RTail (Regionality.disallow_left - (Value.proj_comonadic Areality mode), FTail); + (Value.proj (Comonadic Areality) mode), FTail); closure_context = Some Return; } @@ -474,7 +474,7 @@ let mode_region mode = { (mode_default (meet_regional mode)) with position = RTail (Regionality.disallow_left - (Value.proj_comonadic Areality mode), FNontail); + (Value.proj (Comonadic Areality) mode), FNontail); closure_context = None; } @@ -493,7 +493,7 @@ let mode_global expected_mode = let mode_exclave expected_mode = let mode = - Value.join_with_comonadic Areality + Value.join_with (Comonadic Areality) Regionality.Const.Local expected_mode.mode in { (mode_default mode) @@ -555,7 +555,7 @@ let mode_argument ~funct ~index ~position_and_mode ~partial_app marg = | _, _, (Nontail | Default) -> mode_default vmode, vmode | _, _, Tail -> begin - Regionality.submode_exn (Value.proj_comonadic Areality vmode) + Regionality.submode_exn (Value.proj (Comonadic Areality) vmode) Regionality.regional; mode_tailcall_argument vmode, vmode end @@ -4706,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.proj_monadic Uniqueness mode_r) in - let linearity = Linearity.disallow_right (Value.proj_comonadic 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 @@ -4715,13 +4715,13 @@ let unique_use ~loc ~env mode_l mode_r = (match Uniqueness.submode Uniqueness.shared uniqueness with | Ok () -> () | Error e -> - let e = Mode.Value.Monadic (Error (Uniqueness, e)) in + 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 -> - let e = Mode.Value.Comonadic (Error (Linearity, e)) in + 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, @@ -4808,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.proj_comonadic Areality 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 @@ -4873,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.proj_comonadic Areality 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)) @@ -5276,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_comonadic Areality Regionality.regional) expected_mode; + (Value.min_with (Comonadic Areality) Regionality.regional) expected_mode; { exp_desc = Texp_exclave exp; exp_loc = loc; exp_extra = []; @@ -5293,7 +5293,7 @@ and type_expect_ | Tail -> let mode, _ = Value.newvar_below - (Value.max_with_comonadic Areality Regionality.regional) + (Value.max_with (Comonadic Areality) Regionality.regional) in mode, mode_tailcall_function mode | Nontail | Default -> @@ -5702,7 +5702,7 @@ and type_expect_ rue { exp_desc = Texp_setfield(record, Locality.disallow_right (regional_to_local - (Value.proj_comonadic Areality rmode)), + (Value.proj (Comonadic Areality) rmode)), label_loc, label, newval); exp_loc = loc; exp_extra = []; exp_type = instance Predef.type_unit; @@ -6513,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_comonadic Areality mode; - Alloc.max_with_comonadic 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) @@ -7372,7 +7372,7 @@ and type_argument ?explanation ?recarg env (mode : expected_mode) sarg in let eta_mode, _ = Value.newvar_below (alloc_as_value marg) in Regionality.submode_exn - (Value.proj_comonadic Areality eta_mode) Regionality.regional; + (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 @@ -7394,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.proj_comonadic Areality + |> Value.proj (Comonadic Areality) |> regional_to_global |> Locality.disallow_right)} in @@ -7542,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.proj_comonadic Areality 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 @@ -7604,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.proj_comonadic Areality 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 @@ -9390,7 +9390,7 @@ 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 - | Comonadic (Error (Areality, e)), Some h -> + | 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 @@ -9424,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.proj_comonadic Areality res_mode) + Locality.check_const (Alloc.proj (Comonadic Areality) res_mode) with | Some Global -> Some (n+1, true) @@ -10052,19 +10052,19 @@ let report_error ~loc env = function -> let sub = match fail_reason with - | Comonadic (Error (Linearity, _)) | Monadic (Error (Uniqueness, _)) -> + | Error (Comonadic Linearity, _) | Error (Monadic Uniqueness, _) -> sharedness_hint fail_reason submode_reason shared_context - | Comonadic (Error (Areality, _)) -> + | Error (Comonadic Areality, _) -> escaping_hint fail_reason submode_reason closure_context in Location.errorf ~loc ~sub "%t" begin match fail_reason with - | Comonadic (Error (Areality, _)) -> + | Error (Comonadic Areality, _) -> Format.dprintf "This value escapes its region" - | Monadic (Error (Uniqueness, {left; right})) -> + | 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 - | Comonadic (Error (Linearity, {left; 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 @@ -10104,20 +10104,20 @@ let report_error ~loc env = function f actual f expected in begin match mkind with - | Comonadic (Error (Areality, e)) -> + | Error (Comonadic Areality, e) -> print_error Locality.Const.print (s, e) - | Monadic (Error (Uniqueness, e)) -> + | Error (Monadic Uniqueness, e) -> print_error Uniqueness.Const.print (s, e) - | Comonadic (Error (Linearity, e)) -> + | Error (Comonadic Linearity, e) -> print_error Linearity.Const.print (s, e) end | Uncurried_function_escapes e -> begin match e with - | Comonadic (Error (Areality, _)) -> + | Error (Comonadic Areality, _) -> Location.errorf ~loc "This function or one of its parameters escape their region @ \ when it is partially applied." - | Monadic (Error (Uniqueness, _)) -> assert false - | Comonadic (Error (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 1a754d2637b..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.proj_comonadic Areality 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.proj_comonadic Areality mret)) + (prim_const_mode (Mode.Alloc.proj (Comonadic Areality) mret)) ~global_repr ~is_layout_poly in ((mode, repr_arg) :: repr_args, repr_res)