Skip to content

Commit

Permalink
mode_alpha controls val_modalities
Browse files Browse the repository at this point in the history
  • Loading branch information
riaqn committed Jun 28, 2024
1 parent 9e890a8 commit a3a08ed
Show file tree
Hide file tree
Showing 18 changed files with 109 additions and 60 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,7 @@ let rec fib = function | 0 | 1 -> 1 | n -> (fib (n - 1)) + (fib (n - 2))
<def_rec>
pattern (test_locations.ml[17,534+8]..test_locations.ml[17,534+11])
Tpat_var "fib"
value_mode global,many,nonportable;unique,uncontended
value_mode global,many,nonportable;join(shared,contended)(modevar#1[shared,uncontended ... unique,uncontended])
expression (test_locations.ml[17,534+14]..test_locations.ml[19,572+34])
Texp_function
region true
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,7 @@ let rec fib = function | 0 | 1 -> 1 | n -> (fib (n - 1)) + (fib (n - 2))
<def_rec>
pattern
Tpat_var "fib"
value_mode global,many,nonportable;unique,uncontended
value_mode global,many,nonportable;join(shared,contended)(modevar#1[shared,uncontended ... unique,uncontended])
expression
Texp_function
region true
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ File "bad_arg_impl.ml", line 1:
Error: The argument module bad_arg_impl.ml
does not match the parameter signature monoid.cmi:
Values do not match:
val append : unit -> unit -> [> `Banana ] @@ global many portable
val append : unit -> unit -> [> `Banana ]
is not included in
val append : t -> t -> t
The type unit -> unit -> [> `Banana ] is not compatible with the type
Expand Down
11 changes: 11 additions & 0 deletions ocaml/testsuite/tests/typing-modes/modes.ml
Original file line number Diff line number Diff line change
Expand Up @@ -396,3 +396,14 @@ Line 2, characters 43-46:
^^^
Error: Modality on primitive is not supported yet.
|}]

(* modalities on normal values requires [-extension mode_alpha] *)
module type S = sig
val x : string -> string @ local @@ foo bar
end
[%%expect{|
Line 2, characters 38-41:
2 | val x : string -> string @ local @@ foo bar
^^^
Error: The extension "mode" is disabled and cannot be used
|}]
37 changes: 21 additions & 16 deletions ocaml/testsuite/tests/typing-modes/val_modalities.ml
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
(* TEST
flags = "-extension unique";
flags = "-extension unique -extension mode_alpha";
expect;
*)

Expand All @@ -10,17 +10,17 @@ type r = {
let uncontended_use (_ @ uncontended) = ()
[%%expect{|
type r = { mutable x : string; }
val uncontended_use : 'a -> unit = <fun>
val uncontended_use : 'a -> unit @@ global many = <fun>
|}]

let share_use : 'a -> unit @@ portable = fun _ -> ()
[%%expect{|
val share_use : 'a -> unit = <fun>
val share_use : 'a -> unit @@ global many = <fun>
|}]

let (portable_use @ portable) (_ @ portable) = ()
[%%expect{|
val portable_use : 'a @ portable -> unit = <fun>
val portable_use : 'a @ portable -> unit @@ global many = <fun>
|}]

(* The compiler building itself is a comprehensive test of legacy modules/values.
Expand All @@ -30,7 +30,7 @@ module M = struct
let foo = {x = "hello"}
end
[%%expect{|
module M : sig val foo : r end
module M : sig val foo : r @@ global many end
|}]

module type S = sig
Expand Down Expand Up @@ -58,7 +58,7 @@ module M = struct
let x @ contended = "hello"
end
[%%expect{|
module M : sig val x : string @@ contended end
module M : sig val x : string @@ global many portable contended end
|}]

(* Testing the defaulting behaviour.
Expand Down Expand Up @@ -105,11 +105,11 @@ Lines 8-10, characters 35-7:
10 | end
Error: Signature mismatch:
Modules do not match:
sig val x : string @@ contended end
sig val x : string @@ global many portable contended end
is not included in
sig val x : string end
Values do not match:
val x : string @@ contended
val x : string @@ global many portable contended
is not included in
val x : string
The second is empty and the first is contended.
Expand Down Expand Up @@ -140,8 +140,9 @@ Lines 8-13, characters 35-7:
Error: Signature mismatch:
Modules do not match:
sig
val x : string
module N : sig val y : string @@ contended end
val x : string @@ global many portable
module N :
sig val y : string @@ global many portable contended end
end
is not included in
sig
Expand All @@ -150,12 +151,12 @@ Error: Signature mismatch:
end
In module N:
Modules do not match:
sig val y : string @@ contended end
sig val y : string @@ global many portable contended end
is not included in
sig val y : string end
In module N:
Values do not match:
val y : string @@ contended
val y : string @@ global many portable contended
is not included in
val y : string
The second is empty and the first is contended.
Expand All @@ -173,7 +174,8 @@ module Without_inclusion = struct
let () = portable_use M.x
end
[%%expect{|
module Without_inclusion : sig module M : sig val x : string end end
module Without_inclusion :
sig module M : sig val x : string @@ global many portable end end
|}]

module Without_inclusion = struct
Expand Down Expand Up @@ -203,11 +205,11 @@ Lines 4-6, characters 10-7:
6 | end
Error: Signature mismatch:
Modules do not match:
sig val x : string @@ contended end
sig val x : string @@ global many portable contended end
is not included in
sig val x : string end
Values do not match:
val x : string @@ contended
val x : string @@ global many portable contended
is not included in
val x : string
The second is empty and the first is contended.
Expand Down Expand Up @@ -266,7 +268,10 @@ module Close_over_value = struct
end
[%%expect{|
module Close_over_value :
sig module M : sig val x : string end val foo : unit -> unit end
sig
module M : sig val x : string @@ global many portable end
val foo : unit -> unit @@ global many portable
end
|}]

module Close_over_value_monadic = struct
Expand Down
1 change: 1 addition & 0 deletions ocaml/testsuite/tests/typing-modes/val_modalities_floor.ml
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ strongest instead of legacy *)
";
{
setup-ocamlopt.byte-build-env;
flags = "-extension mode_alpha";
{
src = "def_portable.ml";
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,10 @@ Line 3, characters 2-51:
3 | struct type t = int let f (x : int) = (x : t) end;; (* must fail *)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Signature mismatch:
...
Modules do not match:
sig type t = int val f : int -> t end
is not included in
sig type t = private Foobar.t val f : int -> t end
Type declarations do not match:
type t = int
is not included in
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,10 @@ Line 3, characters 2-51:
3 | struct type t = int let f (x : int) = (x : t) end;; (* must fail *)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Signature mismatch:
...
Modules do not match:
sig type t = int val f : int -> t end
is not included in
sig type t = private Foobar.t val f : int -> t end
Type declarations do not match:
type t = int
is not included in
Expand Down
2 changes: 1 addition & 1 deletion ocaml/typing/printtyp.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2027,7 +2027,7 @@ let tree_of_value_description id decl =
(* Important: process the fvs *after* the type; tree_of_type_scheme
resets the naming context *)
let snap = Btype.snapshot () in
let moda = Mode.Modality.Value.zap_to_id decl.val_modalities in
let moda = Mode.Modality.Value.zap_to_floor decl.val_modalities in
let qtvs = extract_qtvs [decl.val_type] in
let apparent_arity =
let rec count n typ =
Expand Down
15 changes: 11 additions & 4 deletions ocaml/typing/typedecl.ml
Original file line number Diff line number Diff line change
Expand Up @@ -426,7 +426,9 @@ let transl_labels ~new_var_jkind ~allow_unboxed env univars closed lbls kloc =
| Immutable -> Immutable
| Mutable -> Mutable Mode.Alloc.Comonadic.Const.legacy
in
let modalities = Typemode.transl_modalities mut modalities in
let modalities =
Typemode.transl_modalities ~maturity:Stable mut modalities
in
let arg = Ast_helper.Typ.force_poly arg in
let cty = transl_simple_type ~new_var_jkind env ?univars ~closed Mode.Alloc.Const.legacy arg in
{ld_id = Ident.create_local name.txt;
Expand Down Expand Up @@ -462,8 +464,13 @@ let transl_labels ~new_var_jkind ~allow_unboxed env univars closed lbls kloc =
let transl_types_gf ~new_var_jkind ~allow_unboxed
env loc univars closed cal kloc =
let mk arg =
let cty = transl_simple_type ~new_var_jkind env ?univars ~closed Mode.Alloc.Const.legacy arg.pca_type in
let gf = Typemode.transl_modalities Immutable arg.pca_modalities in
let cty =
transl_simple_type ~new_var_jkind env ?univars ~closed
Mode.Alloc.Const.legacy arg.pca_type
in
let gf =
Typemode.transl_modalities ~maturity:Stable Immutable arg.pca_modalities
in
{ca_modalities = gf; ca_type = cty; ca_loc = arg.pca_loc}
in
let tyl_gfl = List.map mk cal in
Expand Down Expand Up @@ -2875,7 +2882,7 @@ let transl_value_decl env loc valdecl =
[] when Env.is_in_signature env ->
let modalities =
valdecl.pval_modalities
|> Typemode.transl_modalities Immutable
|> Typemode.transl_modalities ~maturity:Alpha Immutable
|> Mode.Modality.Value.of_const
in
let default_arity =
Expand Down
49 changes: 31 additions & 18 deletions ocaml/typing/typemod.ml
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,7 @@ type error =
old_arg_type : Compilation_unit.Name.t option;
old_source_file : Misc.filepath;
}
| Submode_failed of Mode.Value.Comonadic.error
| Submode_failed of Mode.Value.error

exception Error of Location.t * Env.t * error
exception Error_forward of Location.error
Expand Down Expand Up @@ -2425,6 +2425,31 @@ let simplify_app_summary app_view = match app_view.arg with
| false, Some p -> Includemod.Error.Named p, mty
| false, None -> Includemod.Error.Anonymous, mty

let maybe_infer_modalities ~loc ~env ~md_mode ~mode =
if Language_extension.(is_at_least Mode Alpha) then begin
(* Upon construction, for comonadic (prescriptive) axes, module
must be weaker than the values therein, for otherwise operations
would be allowed to performed on the module (and extended to the
values) that's disallowed for the values.
For monadic (descriptive) axes, the restriction is not on the
construction but on the projection, which is modelled by the
[Diff] modality in [mode.ml]. *)
begin match Mode.Value.Comonadic.submode
mode.Mode.comonadic
md_mode.Mode.comonadic with
| Ok () -> ()
| Error (Error (ax, e)) -> raise (Error (loc, env, Submode_failed (Error (Comonadic ax, e))))
end;
Mode.Modality.Value.infer ~md_mode ~mode
end else begin
begin match Mode.Value.submode mode md_mode with
| Ok () -> ()
| Error e -> raise (Error (loc, env, Submode_failed e))
end;
Mode.Modality.Value.id
end

let rec type_module ?(alias=false) sttn funct_body anchor env smod =
Builtin_attributes.warning_scope smod.pmod_attributes
(fun () -> type_module_aux ~alias sttn funct_body anchor env smod)
Expand Down Expand Up @@ -2885,21 +2910,9 @@ and type_structure ?(toplevel = None) funct_body anchor env sstr =
Signature_names.check_value names first_loc id;
let vd, mode = Env.find_value_no_locks_exn id newenv in
let vd = Subst.Lazy.force_value_description vd in
(* Upon construction, for comonadic (prescriptive) axes, module
must be weaker than the values therein, for otherwise operations
would be allowed to performed on the module (and extended to the
values) that's disallowed for the values.
For monadic (descriptive) axes, the restriction is not on the
construction but on the projection, which is modelled by the
[Diff] modality in [mode.ml]. *)
begin match Mode.Value.Comonadic.submode
mode.Mode.comonadic
md_mode.Mode.comonadic with
| Ok () -> ()
| Error e -> raise (Error (first_loc, env, Submode_failed e))
end;
let modalities = Mode.Modality.Value.infer ~md_mode ~mode in
let modalities =
maybe_infer_modalities ~loc:first_loc ~env ~md_mode ~mode
in
let vd =
{ vd with
val_zero_alloc = zero_alloc;
Expand Down Expand Up @@ -4073,8 +4086,8 @@ let report_error ~loc _env = function
| Submode_failed (Error (ax, {left; right})) ->
Location.errorf ~loc
"This value is %a, but expected to be %a because it is inside a module."
(Mode.Value.Comonadic.Const.print_axis ax) left
(Mode.Value.Comonadic.Const.print_axis ax) right
(Mode.Value.Const.print_axis ax) left
(Mode.Value.Const.print_axis ax) right

let report_error env ~loc err =
Printtyp.wrap_printing_env_error env
Expand Down
2 changes: 1 addition & 1 deletion ocaml/typing/typemod.mli
Original file line number Diff line number Diff line change
Expand Up @@ -160,7 +160,7 @@ type error =
old_arg_type: Compilation_unit.Name.t option;
old_source_file: Misc.filepath;
}
| Submode_failed of Mode.Value.Comonadic.error
| Submode_failed of Mode.Value.error

exception Error of Location.t * Env.t * error
exception Error_forward of Location.error
Expand Down
11 changes: 6 additions & 5 deletions ocaml/typing/typemode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,8 @@ let transl_mode_annots modes =
| [] -> acc
| m :: rest ->
let { txt; loc } = (m : Mode_expr.Const.t :> _ Location.loc) in
Jane_syntax_parsing.assert_extension_enabled ~loc Mode ();
Jane_syntax_parsing.assert_extension_enabled ~loc Mode
Language_extension.Stable;
let acc : Alloc.Const.Option.t =
match txt with
(* CR zqian: We should interpret other mode names (global, shared, once)
Expand Down Expand Up @@ -53,10 +54,10 @@ let transl_mode_annots modes =
in
loop Alloc.Const.Option.none modes.txt

let transl_modality m : Modality.t =
let transl_modality ~maturity m : Modality.t =
let { txt; loc } = m in
let (Parsetree.Modality s) = txt in
Jane_syntax_parsing.assert_extension_enabled ~loc Mode ();
Jane_syntax_parsing.assert_extension_enabled ~loc Mode maturity;
match s with
| "global" -> Atom (Comonadic Areality, Meet_with Regionality.Const.Global)
| "local" -> Atom (Comonadic Areality, Meet_with Regionality.Const.Local)
Expand Down Expand Up @@ -117,8 +118,8 @@ let is_mutable_implied_modality m =
(* polymorphic equality suffices for now. *)
List.mem m mutable_implied_modalities

let transl_modalities mut modalities =
let modalities = List.map transl_modality modalities in
let transl_modalities ~maturity mut modalities =
let modalities = List.map (transl_modality ~maturity) modalities in
let modalities =
if Types.is_mutable mut
then modalities @ mutable_implied_modalities
Expand Down
4 changes: 3 additions & 1 deletion ocaml/typing/typemode.mli
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,10 @@ val transl_mode_annots : Jane_syntax.Mode_expr.t -> Mode.Alloc.Const.Option.t
legacy if unspecified *)
val transl_alloc_mode : Jane_syntax.Mode_expr.t -> Mode.Alloc.Const.t

(** Interpret mode syntax as modalities *)
(** Interpret mode syntax as modalities. Modalities occuring at different places
requires different levels of maturity. *)
val transl_modalities :
maturity:Language_extension.maturity ->
Types.mutability ->
Parsetree.modality Location.loc list ->
Mode.Modality.Value.Const.t
Expand Down
Loading

0 comments on commit a3a08ed

Please sign in to comment.