diff --git a/testsuite/tests/formatting/test_locations.dlocations.ocamlc.reference b/testsuite/tests/formatting/test_locations.dlocations.ocamlc.reference index aa772792501..4532bd6680e 100644 --- a/testsuite/tests/formatting/test_locations.dlocations.ocamlc.reference +++ b/testsuite/tests/formatting/test_locations.dlocations.ocamlc.reference @@ -88,14 +88,14 @@ let rec fib = function | 0 | 1 -> 1 | n -> (fib (n - 1)) + (fib (n - 2)) pattern (test_locations.ml[17,534+8]..test_locations.ml[17,534+11]) Tpat_var "fib" - value_mode meet_local,once(0[global,many,global,many]),join_shared(1[shared,shared]) + value_mode global,many,shared expression (test_locations.ml[17,534+14]..test_locations.ml[19,572+34]) Texp_function region true - alloc_mode map_comonadic(regional_to_global)(6[global,many,global,many]),id(7[shared,shared]) + alloc_mode global,many,shared [] Tfunction_cases (test_locations.ml[17,534+14]..test_locations.ml[19,572+34]) - alloc_mode id(2[global,many,global,many]),id(3[shared,shared]) + alloc_mode global,many,shared value [ @@ -110,11 +110,11 @@ let rec fib = function | 0 | 1 -> 1 | n -> (fib (n - 1)) + (fib (n - 2)) pattern (test_locations.ml[19,572+4]..test_locations.ml[19,572+5]) Tpat_var "n" - value_mode meet_global,many ∘ map_comonadic(local_to_regional)(2[global,many,global,many]),join_unique(3[shared,shared]) + value_mode global,many,unique expression (test_locations.ml[19,572+9]..test_locations.ml[19,572+34]) Texp_apply apply_mode Tail - locality_mode proj_areality(10[global,many,global,many]) + locality_mode global expression (test_locations.ml[19,572+21]..test_locations.ml[19,572+22]) Texp_ident "Stdlib!.+" [ @@ -123,7 +123,7 @@ let rec fib = function | 0 | 1 -> 1 | n -> (fib (n - 1)) + (fib (n - 2)) expression (test_locations.ml[19,572+9]..test_locations.ml[19,572+20]) Texp_apply apply_mode Default - locality_mode proj_areality(4[global,many,global,many]) + locality_mode global expression (test_locations.ml[19,572+9]..test_locations.ml[19,572+12]) Texp_ident "fib" [ @@ -132,7 +132,7 @@ let rec fib = function | 0 | 1 -> 1 | n -> (fib (n - 1)) + (fib (n - 2)) expression (test_locations.ml[19,572+13]..test_locations.ml[19,572+20]) Texp_apply apply_mode Default - locality_mode proj_areality(20[global,many,global,many]) + locality_mode global expression (test_locations.ml[19,572+16]..test_locations.ml[19,572+17]) Texp_ident "Stdlib!.-" [ @@ -151,7 +151,7 @@ let rec fib = function | 0 | 1 -> 1 | n -> (fib (n - 1)) + (fib (n - 2)) expression (test_locations.ml[19,572+23]..test_locations.ml[19,572+34]) Texp_apply apply_mode Default - locality_mode proj_areality(4[global,many,global,many]) + locality_mode global expression (test_locations.ml[19,572+23]..test_locations.ml[19,572+26]) Texp_ident "fib" [ @@ -160,7 +160,7 @@ let rec fib = function | 0 | 1 -> 1 | n -> (fib (n - 1)) + (fib (n - 2)) expression (test_locations.ml[19,572+27]..test_locations.ml[19,572+34]) Texp_apply apply_mode Default - locality_mode proj_areality(34[global,many,global,many]) + locality_mode global expression (test_locations.ml[19,572+30]..test_locations.ml[19,572+31]) Texp_ident "Stdlib!.-" [ diff --git a/testsuite/tests/formatting/test_locations.dno-locations.ocamlc.reference b/testsuite/tests/formatting/test_locations.dno-locations.ocamlc.reference index 03e872fa7e9..db71a9ab1f5 100644 --- a/testsuite/tests/formatting/test_locations.dno-locations.ocamlc.reference +++ b/testsuite/tests/formatting/test_locations.dno-locations.ocamlc.reference @@ -88,14 +88,14 @@ let rec fib = function | 0 | 1 -> 1 | n -> (fib (n - 1)) + (fib (n - 2)) pattern Tpat_var "fib" - value_mode meet_local,once(0[global,many,global,many]),join_shared(1[shared,shared]) + value_mode global,many,shared expression Texp_function region true - alloc_mode map_comonadic(regional_to_global)(6[global,many,global,many]),id(7[shared,shared]) + alloc_mode global,many,shared [] Tfunction_cases - alloc_mode id(2[global,many,global,many]),id(3[shared,shared]) + alloc_mode global,many,shared value [ @@ -110,11 +110,11 @@ let rec fib = function | 0 | 1 -> 1 | n -> (fib (n - 1)) + (fib (n - 2)) pattern Tpat_var "n" - value_mode meet_global,many ∘ map_comonadic(local_to_regional)(2[global,many,global,many]),join_unique(3[shared,shared]) + value_mode global,many,unique expression Texp_apply apply_mode Tail - locality_mode proj_areality(10[global,many,global,many]) + locality_mode global expression Texp_ident "Stdlib!.+" [ @@ -123,7 +123,7 @@ let rec fib = function | 0 | 1 -> 1 | n -> (fib (n - 1)) + (fib (n - 2)) expression Texp_apply apply_mode Default - locality_mode proj_areality(4[global,many,global,many]) + locality_mode global expression Texp_ident "fib" [ @@ -132,7 +132,7 @@ let rec fib = function | 0 | 1 -> 1 | n -> (fib (n - 1)) + (fib (n - 2)) expression Texp_apply apply_mode Default - locality_mode proj_areality(20[global,many,global,many]) + locality_mode global expression Texp_ident "Stdlib!.-" [ @@ -151,7 +151,7 @@ let rec fib = function | 0 | 1 -> 1 | n -> (fib (n - 1)) + (fib (n - 2)) expression Texp_apply apply_mode Default - locality_mode proj_areality(4[global,many,global,many]) + locality_mode global expression Texp_ident "fib" [ @@ -160,7 +160,7 @@ let rec fib = function | 0 | 1 -> 1 | n -> (fib (n - 1)) + (fib (n - 2)) expression Texp_apply apply_mode Default - locality_mode proj_areality(34[global,many,global,many]) + locality_mode global expression Texp_ident "Stdlib!.-" [ diff --git a/typing/mode.ml b/typing/mode.ml index 015364c0fe5..0a85013d335 100644 --- a/typing/mode.ml +++ b/typing/mode.ml @@ -1195,15 +1195,21 @@ module Common (Obj : Obj) = struct let print ?verbose () ppf m = Solver.print ?verbose obj ppf m - let print_raw ?verbose () ppf m = Solver.print_raw ?verbose obj ppf m - let zap_to_ceil m = with_log (Solver.zap_to_ceil obj m) let zap_to_floor m = with_log (Solver.zap_to_floor obj m) let of_const : type l r. const -> (l * r) t = fun a -> Solver.of_const obj a - let check_const m = Solver.check_const obj m + module Guts = struct + let get_floor m = Solver.get_floor obj m + + let get_ceil m = Solver.get_ceil obj m + + let get_conservative_floor m = Solver.get_conservative_floor obj m + + let get_conservative_ceil m = Solver.get_conservative_ceil obj m + end end [@@inline] @@ -1227,6 +1233,18 @@ module Locality = struct let legacy = of_const Const.legacy let zap_to_legacy = zap_to_floor + + module Guts = struct + let check_const m = + let floor = Guts.get_floor m in + let ceil = Guts.get_ceil m in + if Const.le ceil floor then Some ceil else None + + let check_const_conservative m = + let floor = Guts.get_conservative_floor m in + let ceil = Guts.get_conservative_ceil m in + if Const.le ceil floor then Some ceil else None + end end module Regionality = struct @@ -1430,12 +1448,6 @@ module Comonadic_with_locality = struct (* override to report the offending axis *) let equate a b = try_with_log (equate_from_submode submode_log a b) - - (** overriding to check per-axis *) - let check_const m = - let locality = Locality.check_const (proj Areality m) in - let linearity = Linearity.check_const (proj Linearity m) in - locality, linearity end module Monadic = struct @@ -1502,11 +1514,6 @@ module Monadic = struct (* override to report the offending axis *) let equate a b = try_with_log (equate_from_submode submode_log a b) - - (** overriding to check per-axis *) - let check_const m = - let uniqueness = Uniqueness.check_const (proj Uniqueness m) in - uniqueness, () end type ('mo, 'como) monadic_comonadic = @@ -1550,13 +1557,6 @@ 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 ()) @@ -1585,7 +1585,9 @@ module Value = struct 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 print ppf m = + let { monadic; comonadic } = split m in + Format.fprintf ppf "%a,%a" Comonadic.print comonadic Monadic.print monadic let legacy = merge { comonadic = Comonadic.legacy; monadic = Monadic.legacy } @@ -1919,13 +1921,6 @@ module Alloc = 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 ()) @@ -2069,7 +2064,9 @@ module Alloc = struct 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 print ppf m = + let { monadic; comonadic } = split m in + Format.fprintf ppf "%a,%a" Comonadic.print comonadic Monadic.print monadic let legacy = merge { comonadic = Comonadic.legacy; monadic = Monadic.legacy } @@ -2158,11 +2155,6 @@ module Alloc = struct 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 give the lower bound mode of [B -> C]. *) diff --git a/typing/mode_intf.mli b/typing/mode_intf.mli index af181c71459..ef0a8ff2a81 100644 --- a/typing/mode_intf.mli +++ b/typing/mode_intf.mli @@ -83,11 +83,7 @@ module type Common = sig val newvar_below : ('l * allowed) t -> ('l_ * 'r) t * bool - val print_raw : - ?verbose:bool -> unit -> Format.formatter -> ('l * 'r) t -> unit - - val print : - ?verbose:bool -> unit -> Format.formatter -> (allowed * allowed) t -> unit + val print : ?verbose:bool -> unit -> Format.formatter -> ('l * 'r) t -> unit val of_const : Const.t -> ('l * 'r) t end @@ -147,7 +143,21 @@ module type S = sig val zap_to_ceil : ('l * allowed) t -> Const.t - val check_const : (allowed * allowed) t -> Const.t option + module Guts : sig + (** This module exposes some functions that allow callers to inspect modes + directly, which could be useful for error printing and dev tools (such as + merlin). Any usage of this in type checking should be pondered. *) + + (** Returns [Some c] if the given mode has been constrained to constant + [c]. see notes on [get_floor] in [solver_intf.mli] for cautions. *) + val check_const : (allowed * allowed) t -> Const.t option + + (** Similar to [check_const] but doesn't run the further constraining + needed for precise bounds. As a result, it is inexpensive and returns + a conservative result. I.e., it might return [None] for + fully-constrained modes. *) + val check_const_conservative : (l * 'r) t -> Const.t option + end end module Regionality : sig @@ -389,8 +399,6 @@ module type S = sig and type error := error and type 'd t := 'd t - val check_const : (allowed * allowed) t -> Const.Option.t - val proj : ('m, 'a, 'l * 'r) axis -> ('l * 'r) t -> 'm val max_with : ('m, 'a, 'l * 'r) axis -> 'm -> (disallowed * 'r) t diff --git a/typing/printtyped.ml b/typing/printtyped.ml index ec68a5f45ef..eedaac2c332 100644 --- a/typing/printtyped.ml +++ b/typing/printtyped.ml @@ -404,16 +404,16 @@ and expression_extra i ppf x attrs = attributes i ppf attrs; and alloc_mode: type l r. _ -> _ -> (l * r) Mode.Alloc.t -> _ - = fun i ppf m -> line i ppf "alloc_mode %a\n" (Mode.Alloc.print_raw ()) m + = fun i ppf m -> line i ppf "alloc_mode %a\n" (Mode.Alloc.print ()) m and alloc_mode_option i ppf m = Option.iter (alloc_mode i ppf) m and locality_mode i ppf m = line i ppf "locality_mode %a\n" - (Mode.Locality.print_raw ()) m + (Mode.Locality.print ()) m and value_mode i ppf m = - line i ppf "value_mode %a\n" (Mode.Value.print_raw ()) m + line i ppf "value_mode %a\n" (Mode.Value.print ()) m and expression_alloc_mode i ppf (expr, am) = alloc_mode i ppf am; diff --git a/typing/solver.ml b/typing/solver.ml index dda6e7d330f..2e388329cde 100644 --- a/typing/solver.ml +++ b/typing/solver.ml @@ -628,24 +628,49 @@ module Solver_mono (C : Lattices_mono) = struct C.join obj acc (zap_to_floor_morphvar obj mv ~commit:log)) a mvs - let check_const : type a. a C.obj -> (a, allowed * allowed) mode -> a option = + let get_conservative_ceil : type a l r. a C.obj -> (a, l * r) mode -> a = fun obj m -> match m with - | Amode a -> Some a - | Amodevar mv -> - let lower = zap_to_floor_morphvar obj mv ~commit:None in - if C.le obj (mupper obj mv) lower then Some lower else None + | Amode a -> a + | Amodevar mv -> mupper obj mv + | Amodemeet (a, mvs) -> + List.fold_left (fun acc mv -> C.meet obj acc (mupper obj mv)) a mvs + | Amodejoin (a, mvs) -> + List.fold_left (fun acc mv -> C.join obj acc (mupper obj mv)) a mvs + + let get_conservative_floor : type a l r. a C.obj -> (a, l * r) mode -> a = + fun obj m -> + match m with + | Amode a -> a + | Amodevar mv -> mlower obj mv + | Amodejoin (a, mvs) -> + List.fold_left (fun acc mv -> C.join obj acc (mupper obj mv)) a mvs + | Amodemeet (a, mvs) -> + List.fold_left (fun acc mv -> C.meet obj acc (mlower obj mv)) a mvs + + (* Due to our biased implementation, the ceil is precise. *) + let get_ceil = get_conservative_ceil + + let get_floor : type a r. a C.obj -> (a, allowed * r) mode -> a = + fun obj m -> + match m with + | Amode a -> a + | Amodevar mv -> zap_to_floor_morphvar obj mv ~commit:None + | Amodejoin (a, mvs) -> + List.fold_left + (fun acc mv -> + C.join obj acc (zap_to_floor_morphvar obj mv ~commit:None)) + a mvs let print : - type a. - ?verbose:bool -> - a C.obj -> - Format.formatter -> - (a, allowed * allowed) mode -> - unit = - fun ?(verbose = false) obj ppf m -> - print_raw obj ~verbose ppf - (match check_const obj m with None -> m | Some a -> Amode a) + type a l r. + ?verbose:bool -> a C.obj -> Format.formatter -> (a, l * r) mode -> unit = + fun ?verbose (obj : a C.obj) ppf m -> + let ceil = get_conservative_ceil obj m in + let floor = get_conservative_floor obj m in + if C.le obj ceil floor + then C.print obj ppf ceil + else print_raw ?verbose obj ppf m let newvar obj = Amodevar (Amorphvar (fresh obj, C.id)) @@ -737,11 +762,15 @@ module Solvers_polarized (C : Lattices_mono) = struct let newvar_below = S.newvar_below - let check_const = S.check_const + let get_ceil = S.get_ceil - let print ?(verbose = false) = S.print ~verbose + let get_floor = S.get_floor - let print_raw ?(verbose = false) = S.print_raw ~verbose + let get_conservative_ceil = S.get_conservative_ceil + + let get_conservative_floor = S.get_conservative_floor + + let print ?(verbose = false) = S.print ~verbose let via_monotone = S.apply @@ -795,11 +824,15 @@ module Solvers_polarized (C : Lattices_mono) = struct let newvar_below = S.newvar_above - let check_const = S.check_const + let get_ceil = S.get_floor - let print ?(verbose = false) = S.print ~verbose + let get_floor = S.get_ceil - let print_raw ?(verbose = false) = S.print_raw ~verbose + let get_conservative_ceil = S.get_conservative_floor + + let get_conservative_floor = S.get_conservative_ceil + + let print ?(verbose = false) = S.print ~verbose let via_monotone = S.apply diff --git a/typing/solver_intf.mli b/typing/solver_intf.mli index 4b8d3dbc65f..fe3c60b29ef 100644 --- a/typing/solver_intf.mli +++ b/typing/solver_intf.mli @@ -271,24 +271,28 @@ module type Solver_polarized = sig (** Return the meet of the list of modes. *) val meet : 'a obj -> ('a, 'l * allowed) mode list -> ('a, right_only) mode - (** Checks if a mode has been constrained sufficiently to a constant. Because - our internal representation is conservative, further constraint is run to - decide the bounds. This operation is therefore expensive and requires the - mode to be allowed on both sides. - WARNING: the lattice must be finite for this to terminate.*) - val check_const : 'a obj -> ('a, allowed * allowed) mode -> 'a option - - (** Print a mode. Calls [check_const] for cleaner printing; caveats there - apply here too. *) + (** Returns the lower bound of the mode. Because of our conservative internal + representation, further constraining is needed for precise bound. + This operation is therefore expensive and requires the mode to be allowed + on the left. + WARNING: the lattice must be finite for this to terminate. *) + val get_floor : 'a obj -> ('a, allowed * 'r) mode -> 'a + + (** Returns the upper bound of the mode. Notes for [get_floor] applies. *) + val get_ceil : 'a obj -> ('a, 'l * allowed) mode -> 'a + + (** Similar to [get_floor] but does not run the further constraining needed + for a precise bound. As a result, the returned bound is conservative; + i.e., it might be lower than the real floor. *) + val get_conservative_floor : 'a obj -> ('a, 'l * 'r) mode -> 'a + + (** Similar to [get_ceil] but does not run the further constraining needed + for a precise bound. As a result, the returned bound is conservative; + i.e., it might be higher than the real ceil. *) + val get_conservative_ceil : 'a obj -> ('a, 'l * 'r) mode -> 'a + + (** Printing a mode for debugging. *) val print : - ?verbose:bool -> - 'a obj -> - Format.formatter -> - ('a, allowed * allowed) mode -> - unit - - (** Print a mode without calling [check_const]. *) - val print_raw : ?verbose:bool -> 'a obj -> Format.formatter -> ('a, 'l * 'r) mode -> unit (** Apply a monotone morphism whose source and target modes are of the diff --git a/typing/typecore.ml b/typing/typecore.ml index c90551daa20..e03ecf3c2be 100644 --- a/typing/typecore.ml +++ b/typing/typecore.ml @@ -9488,7 +9488,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.Guts.check_const (Alloc.proj (Comonadic Areality) res_mode) with | Some Global -> Some (n+1, true) diff --git a/typing/typedecl.ml b/typing/typedecl.ml index 1e402324711..b9e292b66d6 100644 --- a/typing/typedecl.ml +++ b/typing/typedecl.ml @@ -2467,7 +2467,7 @@ let make_native_repr env core_type ty ~global_repr ~is_layout_poly ~why = Same_as_ocaml_repr sort let prim_const_mode m = - match Mode.Locality.check_const m with + match Mode.Locality.Guts.check_const m with | Some Global -> Prim_global | Some Local -> Prim_local | None -> assert false