Refactor new mode syntax (#3522)

Author: riaqn

Diff for: jane/doc/extensions/modes/syntax.md

@@ -1,12 +1,3 @@
-# Motivation
-Previously we have a fixed set of mode names in the parser. Everytime we want to
-add more modes we need to update the parser (and correspondingly ocamlformat).
-This is too costy in the long term.
-
-We introduce a new mode syntax that allows mode names (and mode expressions in
-the future) to enjoy a dedicated name space. As a result, any identifier can be
-used as a mode name.
-
 # Modes and modalities
 Currently a mode expression is simply a space-delimited list of modes.
 
@@ -23,112 +14,120 @@ local
 local unique
 ```
 
-Currently modalities have  the same syntax as modes:
+Modes are in a dedicated namespace separated from variable names or type names,
+which means you can continue to use `local` or `unique` as variable or type
+names.
+
+Currently a modality expression is simply a space-delimited list of modalities.
 
 ```
 modality := local | global | ..
 modalities := separated_nonempty_list(SPACE, modality)
 ```
+Similarly, modalities are in a dedicated namespace.
 
 # Where can they appear
 
-Mode expressions and modalities can appear after either `@` or `@@`. The former
-is used in most cases, while the latter is used for disambiguition. For example,
-in `val f : a -> b @ global`, the `@ global` could be annotating either `b` or
-`f`. To avoid the ambiguity, we will write `val f : a -> b @ local @@ global`
-where `local` is the mode of `b` and `global` is the modality on `f`.
+To write a mode expression in program, it has to be prefixed by an `@` symbol.
+Similarly, a modality expression has to be prefixed by an `@@` symbol. They can
+appear in several places in a program as described below.
 
-## Function parameter
-```ocaml
-let foo ?(label_let_pattern = default) = ..
-let foo ~(label_let_pattern) = ..
-let foo (x @ modes) = ..
-let foo (x : ty @@ modes) = ..
-```
-where `label_let_pattern` could be
+## Arrow types
 ```ocaml
-x @ modes
-x : ty @@ modes
-x : a b c. a -> b -> c @@ modes
-```
-Patterns that are not directly function parameters can’t have modes. For
-example:
-```
-let foo ((x, y) @ modes) = .. (error)
+a * b @ modes -> b @ modes
+foo:a * b @ modes -> b @ modes
+?foo:a * b @ modes -> b @ modes
 ```
 
-## Let bindings
+One should be careful about the precedence of `@`. In the following example,
+`modes` annotates `c`.
 ```ocaml
-let x @ modes = ..
-let x : ty @@ modes = ..
-let x : type a b. ty @@ modes = ..
+a -> b -> c @ modes
 ```
 
-## Functions and their return
+You can use parentheses to override precedence. In the
+following example, `modes` annotates `b -> c`.
 ```ocaml
-let (foo @ modes) x y = ..
-let foo x y @ modes = ..
-let foo x y : ty @@ modes = ..
-fun foo x y @ modes -> ..
-fun foo x y : ty @@ modes -> ..
+a -> (b -> c) @ modes
 ```
 
-## Arrow types
+## Function parameter
+The rule of thumb is: wherever a type constraint `x : ty` is allowed, a similar
+mode constraint `x @ modes` or type-and-mode constraint `x : ty @ modes` will be
+allowed.
 ```ocaml
-a * b @ modes -> b @ modes
-foo:a * b @ modes -> b @ modes
-?foo:a * b @ modes -> b @ modes
+let foo ?(x : int @ modes = default) = ..
+let foo ?x:((a, b) : int @ modes = default)
+let foo ~(x : int @ modes) = ..
+let foo ~x:((a, b) : int @ modes) = ..
+let foo ((a, b) : int @ modes) = ..
 ```
-
-## Record fields & Value descriptions
-The two are similar in both semantics and syntax, so we will consider them
-together.
+Patterns that are not directly function parameters can’t have modes. For
+example, the following is not allowed, because `x @ local` is not a function
+parameter (but the first component of one).
 ```ocaml
-type r = {x : string @@ global}
-type r = {x : string @ local -> string @ local @@ global}
-
-val foo : string -> string @ local @@ portable
+let foo ((x @ local), y) = ..
 ```
 
-## Expressions
+Again, one should pay attention to the precedences. In the following example, the first
+`modes` annotates `'b`, while the second annotates `x`.
 ```ocaml
-(expression : _ @@ local)
+let foo (x : 'a -> 'b @ modes) = ..
+let foo (x : ('a -> 'b) @ modes) = ..
 ```
 
-# Future works
-## Unzipped syntax
-In the future we will support
-```ocaml
-type r = string -> string @@ local unique -> unique local
-```
-which corresponds to
+## Let bindings
+The rule of thumb is: wherever a type constraint `pat : ty` is allowed, a similar
+mode constraint `pat @ modes` and type-and-mode constraint `pat : ty @ modes` will be
+allowed.
 ```ocaml
-type r = string @@ local unique -> string @@ unique local
+  let a : int @ modes = 42 in
+  let (a, b) : int @ once portable = 42 in
 ```
-This gets more complex when modalities are involved:
+
+## Functions and their body
+You can specify the mode of the function itself:
 ```ocaml
-type r = { x : string -> string @@ (local -> unique) global}
+let (foo @ modes) x y = ..
 ```
-which is equivalent to
+You can also specify the mode of the function body:
 ```ocaml
-type r = {x : string @ local -> string @ unique @@ global}
+let foo x y @ modes = ..
+let foo x y : ty @ modes = ..
+fun foo x y @ modes -> ..
 ```
-where `global` is a modality on the `x` field.
+We don't support `fun foo x y : ty @ modes -> 42` due to a limitation in the
+parser.
 
-## Syntax sugar
-Similar to
+## Expressions
 ```ocaml
-let foo x y : int = exp in
+(expression : ty @ local)
 ```
-which unfolds to
+We don't support `(expression @ modes)` because `@` is already parsed as a binary operator.
+
+## Record fields
+Record fields can have modalities, for example:
 ```ocaml
-let foo x y = exp : int in
+type r = {x : string @@ modalities}
+type r = {x : string @ modes -> string @ modes @@ modalities}
 ```
-We should allow
+
+## Signature items
+Signature items such as values can have modalities; for example:
 ```ocaml
-let foo x y @ local = exp in
+val foo : string @@ modalities
+val bar : string @ modes -> string @ modes @@ modalities
 ```
-unfold to
+
+A signature can have default modalities that each item can override; for example:
 ```ocaml
-let foo x y = exp : _ @@ local in
+sig @@ portable
+val foo : string (* have portable modality *)
+val bar : string -> string @@ nonportable (* not have portable modality *)
+end
 ```
+
+## Modules
+Support for modules with modes is being worked on and not ready for company-wide adoption.
+For the few use sites, the syntax should be self-explanatory. More documentation will come
+as it becomes ready.

Diff for: otherlibs/stdlib_alpha/capsule.ml

@@ -107,7 +107,7 @@ end = struct
 
   type 'k t = A.t
 
-  let[@inline] unsafe_mk () : _ @@ local = A.make Id.uninitialized
+  let[@inline] unsafe_mk () : _ @ local = A.make Id.uninitialized
   let[@inline] id t =
     (* Safe since [Password.t] is only ever accessible by 1 fiber. *)
     match A.get_unsync t with
@@ -131,7 +131,7 @@ end = struct
          | already_set_id -> already_set_id)
       | set_id -> set_id
 
-    let unsafe_mk () : _ @@ local unyielding = A.make Id.uninitialized
+    let unsafe_mk () : _ @ local unyielding = A.make Id.uninitialized
   end
 
   let[@inline] shared t = t
@@ -585,10 +585,10 @@ module Mutex = struct
 
   let[@inline] with_lock :
     type k.
-    k t
+    (k t
     -> (k Password.t @ local -> 'a) @ local
-    -> 'a
-    @@ portable
+    -> 'a)
+    @ portable
     = fun t f ->
       M.lock t.mutex;
       match t.poisoned with
@@ -647,10 +647,10 @@ module Rwlock = struct
 
   let[@inline] with_write_lock :
     type k.
-    k t
+    (k t
     -> (k Password.t @ local -> 'a) @ local
-    -> 'a
-    @@ portable
+    -> 'a)
+    @ portable
     = fun t f ->
       Rw.lock_write t.rwlock;
       match t.state with
@@ -679,10 +679,10 @@ module Rwlock = struct
 
   let[@inline] with_read_lock :
     type k.
-    k t
+    (k t
     -> (k Password.Shared.t @ local unyielding -> 'a) @ local
-    -> 'a
-    @@ portable
+    -> 'a)
+    @ portable
     = fun t f ->
       Rw.lock_read t.rwlock;
       match t.state with

Diff for: otherlibs/stdlib_alpha/effect.ml

@@ -390,8 +390,8 @@ type last_fiber : immediate
 type (-'a, +'b) cont
 
 (* CR borrowing: implement [borrow] without magic. *)
-let borrow (f : ('a, 'b) cont @ local -> 'c @ unique) (k : ('a, 'b) cont @@ unique)
-  : 'c * ('a, 'b) cont @@ unique = f k, Obj.magic_unique k
+let borrow (f : ('a, 'b) cont @ local -> 'c @ unique) (k : ('a, 'b) cont @ unique)
+  : 'c * ('a, 'b) cont @ unique = f k, Obj.magic_unique k
 
 external get_cont_callstack :
   ('a, 'b) cont @ local -> int -> Printexc.raw_backtrace @@ portable =
@@ -456,11 +456,11 @@ external reperform :
 let alloc_cont
     (type a b h e es)
     (module H : Handler.Create with type e = e and type es = es)
-    (f : local_ h -> a -> b @@ once)
+    (f : (local_ h -> a -> b) @ once)
     (h : h) : (a, (b, e * es) r) cont =
   let exception Ready__ of (a, (b, e * es) r) cont in
   let effc (type o eh) ((op, h) as perf : (o, eh) perform)
-      (k : (o, (b, e * es) r) cont) last_fiber : _ @@ unique =
+      (k : (o, (b, e * es) r) cont) last_fiber : _ @ unique =
     match h with
     | H.C h ->
       Op(op, h, k, last_fiber)
@@ -483,7 +483,7 @@ let alloc_cont
 let run_stack
     (type a h e es)
     (module H : Handler.Create with type e = e and type es = es)
-     (f : local_ h -> a @@ once) (h : h) : (a, e * es) r =
+     (f : (local_ h -> a) @ once) (h : h) : (a, e * es) r =
   let effc ((op, h) as perf) k last_fiber =
     match h with
     | H.C h ->
@@ -541,7 +541,7 @@ let discontinue_with_backtrace k e bt (local_ hs) =
   resume k (fun e -> Printexc.raise_with_backtrace e bt) e hs
 
 let fiber (type a b e)
-    (f : local_ e Handler.t -> a -> b @@ once)=
+    (f : (local_ e Handler.t -> a -> b) @ once)=
   let module H = (val (Handler.create ()) :
     Handler.Create with type e = e and type es = unit)
   in
@@ -552,7 +552,7 @@ let fiber (type a b e)
   Cont { cont; mapping }
 
 let fiber_with (type a b e es) (local_ l : es Handler.List.Length.t)
-    (f : local_ (e * es) Handler.List.t -> a -> b @@ once) =
+    (f : (local_ (e * es) Handler.List.t -> a -> b) @ once) =
   let module H = (val (Handler.create ()) :
     Handler.Create with type e = e and type es = es)
   in
@@ -564,7 +564,7 @@ let fiber_with (type a b e es) (local_ l : es Handler.List.Length.t)
   let cont = alloc_cont (module H) f handlers in
   Cont { cont; mapping }
 
-let run (type a e) (f : local_ e Handler.t -> a @@ once) =
+let run (type a e) (f : (local_ e Handler.t -> a) @ once) =
   let module H = (val (Handler.create ()) :
     Handler.Create with type e = e and type es = unit)
   in
@@ -574,7 +574,7 @@ let run (type a e) (f : local_ e Handler.t -> a @@ once) =
   handle (Mapping.empty ()) res
 
 let run_with (type a e es) (local_ hs : es Handler.List.t)
-    (f : local_ (e * es) Handler.List.t -> a @@ once) =
+    (f : (local_ (e * es) Handler.List.t -> a) @ once) =
   let module H = (val (Handler.create ()) :
     Handler.Create with type e = e and type es = es)
   in