Refactor modality logic (ocaml-flambda#2344)

ocaml/.depend

@@ -1002,6 +1002,7 @@ typing/includecore.cmi : \
     typing/types.cmi \
     typing/typedtree.cmi \
     typing/path.cmi \
+    typing/mode.cmi \
     parsing/location.cmi \
     typing/jkind.cmi \
     typing/ident.cmi \
@@ -1486,6 +1487,7 @@ typing/printtyp.cmi : \
     typing/shape.cmi \
     typing/path.cmi \
     typing/outcometree.cmi \
+    typing/mode.cmi \
     parsing/longident.cmi \
     parsing/location.cmi \
     typing/ident.cmi \
@@ -1943,6 +1945,7 @@ typing/typedecl.cmi : \
     typing/shape.cmi \
     typing/path.cmi \
     parsing/parsetree.cmi \
+    typing/mode.cmi \
     parsing/longident.cmi \
     parsing/location.cmi \
     utils/language_extension.cmi \
@@ -2185,21 +2188,20 @@ typing/typemod.cmi : \
     utils/compilation_unit.cmi \
     file_formats/cmi_format.cmi
 typing/typemode.cmo : \
-    utils/warnings.cmi \
     typing/mode.cmi \
     parsing/location.cmi \
     parsing/jane_syntax_parsing.cmi \
     parsing/jane_syntax.cmi \
     typing/typemode.cmi
 typing/typemode.cmx : \
-    utils/warnings.cmx \
     typing/mode.cmx \
     parsing/location.cmx \
     parsing/jane_syntax_parsing.cmx \
     parsing/jane_syntax.cmx \
     typing/typemode.cmi
 typing/typemode.cmi : \
     typing/mode.cmi \
+    parsing/location.cmi \
     parsing/jane_syntax.cmi
 typing/typeopt.cmo : \
     typing/types.cmi \

ocaml/ocamldoc/odoc_sig.ml

@@ -492,7 +492,7 @@ module Analyser =
       let record comments
           { Typedtree.ld_id; ld_mutable; ld_type; ld_loc; ld_attributes } =
         get_field env comments @@
-        {Types.ld_id; ld_mutable; ld_global = Unrestricted;
+        {Types.ld_id; ld_mutable; ld_modalities = Mode.Modality.Value.id;
          ld_jkind=Jkind.any ~why:Dummy_jkind (* ignored *);
          ld_type=ld_type.Typedtree.ctyp_type;
          ld_loc; ld_attributes; ld_uid=Types.Uid.internal_not_actually_unique} in

ocaml/otherlibs/dynlink/dune

@@ -91,7 +91,6 @@
     solver
     mode_intf
     mode
-    typemode
     jkind_intf
     jkind_types
     primitive
@@ -199,7 +198,6 @@
 (copy_files ../../typing/solver.ml)
 (copy_files ../../typing/shape_reduce.ml)
 (copy_files ../../typing/mode.ml)
-(copy_files ../../typing/typemode.ml)
 (copy_files ../../typing/types.ml)
 (copy_files ../../typing/btype.ml)
 (copy_files ../../typing/subst.ml)
@@ -269,7 +267,6 @@
 (copy_files ../../typing/solver.mli)
 (copy_files ../../typing/shape_reduce.mli)
 (copy_files ../../typing/mode.mli)
-(copy_files ../../typing/typemode.mli)
 (copy_files ../../typing/types.mli)
 (copy_files ../../typing/btype.mli)
 (copy_files ../../typing/subst.mli)
@@ -380,7 +377,6 @@
       .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Ast_mapper.cmo
       .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Solver.cmo
       .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Mode.cmo
-      .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Typemode.cmo
       .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Jkind_intf.cmo
       .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Jkind_types.cmo
       .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Types.cmo
@@ -464,7 +460,6 @@
       .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Ast_mapper.cmx
       .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Solver.cmx
       .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Mode.cmx
-      .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Typemode.cmx
       .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Jkind_intf.cmx
       .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Jkind_types.cmx
       .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Types.cmx

ocaml/testsuite/tests/typing-local/local.ml

@@ -1672,7 +1672,7 @@ Error: Signature mismatch:
          foo : string;
        is not the same as:
          global_ foo : string;
-       The second is global and the first is not.
+       The second is global_ and the first is not.
 |}]
 
 module M : sig
@@ -1698,7 +1698,7 @@ Error: Signature mismatch:
          global_ foo : string;
        is not the same as:
          foo : string;
-       The first is global and the second is not.
+       The first is global_ and the second is not.
 |}]
 
 (* Special handling of tuples in matches and let bindings *)
@@ -2523,7 +2523,8 @@ Error: Signature mismatch:
          Bar of int * string
        is not the same as:
          Bar of int * global_ string
-       Locality mismatch at argument position 2 : The second is global and the first is not.
+       Modality mismatch at argument position 2:
+       The second is global_ and the first is not.
 |}]
 
 
@@ -2550,7 +2551,8 @@ Error: Signature mismatch:
          Bar of int * global_ string
        is not the same as:
          Bar of int * string
-       Locality mismatch at argument position 2 : The first is global and the second is not.
+       Modality mismatch at argument position 2:
+       The first is global_ and the second is not.
 |}]
 
 (* global_ binds closer than star *)

ocaml/testsuite/tests/typing-modes/modes.ml

@@ -231,12 +231,8 @@ Error: Unrecognized modality foo.
 |}]
 
 type t = Foo of global_ string @@ global
+(* CR reduced-modality: this should warn. *)
 [%%expect{|
-Line 1, characters 34-40:
-1 | type t = Foo of global_ string @@ global
-                                      ^^^^^^
-Warning 250 [redundant-modality]: This global modality is redundant.
-
 type t = Foo of global_ string
 |}]
 
@@ -260,15 +256,49 @@ Error: Unrecognized modality foo.
 type r = {
   global_ x : string @@ global
 }
+(* CR reduced-modality: this should warn. *)
 [%%expect{|
-Line 2, characters 24-30:
-2 |   global_ x : string @@ global
-                            ^^^^^^
-Warning 250 [redundant-modality]: This global modality is redundant.
-
 type r = { global_ x : string; }
 |}]
 
+(* Modalities don't imply each other; this will change as we add borrowing. *)
+type r = {
+  global_ x : string @@ shared
+}
+[%%expect{|
+type r = { global_ x : string @@ shared; }
+|}]
+
+type r = {
+  x : string @@ shared global many
+}
+[%%expect{|
+type r = { global_ x : string @@ many shared; }
+|}]
+
+type r = {
+  x : string @@ shared global many shared
+}
+(* CR reduced-modality: this should warn. *)
+[%%expect{|
+type r = { global_ x : string @@ many shared; }
+|}]
+
+type r = Foo of string @@ global shared many
+[%%expect{|
+type r = Foo of global_ string @@ many shared
+|}]
+
+(* mutable implies global shared many. No warnings are given since we imagine
+   that the coupling will be removed soon. *)
+type r = {
+  mutable x : string @@ global shared many
+}
+[%%expect{|
+type r = { mutable x : string; }
+|}]
+
+
 (* patterns *)
 
 let foo ?(local_ x @ unique once = 42) () = ()

ocaml/testsuite/tests/typing-modes/mutable.ml

@@ -3,9 +3,10 @@
  expect;
 *)
 
-(* Since [mutable] implies [global] modality, which in turns implies [shared]
-   and [many] modalities, the effect of mutable in isolation is not testable
-   yet. *)
+(* This file tests the typing around mutable() logic. *)
+
+(* For legacy compatibility, [mutable] implies [global] [shared] and [many].
+   Therefore, the effect of mutable in isolation is not testable yet. *)
 
 (* CR zqian: add test for mutable when mutable is decoupled from modalities. *)
 

ocaml/testsuite/tests/typing-unique/unique.ml

@@ -241,12 +241,11 @@ Error: This value is shared but expected to be unique.
 |}]
 
 
-(* global modality entails shared modality;
-this is crucial once we introduce borrowing whose scope is controlled
-by locality *)
-type 'a glob = { global_ glob: 'a } [@@unboxed]
+(* CR zqian: [global] should imply [shared]/[many], once we introduce borrowing whose
+scope is controlled by locality *)
+type 'a glob = { glob: 'a @@ shared many } [@@unboxed]
 [%%expect{|
-type 'a glob = { global_ glob : 'a; } [@@unboxed]
+type 'a glob = { glob : 'a @@ many shared; } [@@unboxed]
 |}]
 let dup (glob : 'a) : 'a glob * 'a glob = unique_ ({glob}, {glob})
 [%%expect{|
@@ -655,4 +654,3 @@ Line 2, characters 11-19:
                ^^^^^^^^
 
 |}]
-

ocaml/testsuite/tests/typing-unique/unique_analysis.ml

@@ -612,9 +612,9 @@ val foo : unit -> unit = <fun>
 |}]
 
 (* Testing modalities in records *)
-type r_global = {x : string; global_ y : string}
+type r_shared = {x : string; y : string @@ shared many}
 [%%expect{|
-type r_global = { x : string; global_ y : string; }
+type r_shared = { x : string; y : string @@ many shared; }
 |}]
 
 let foo () =
@@ -697,14 +697,14 @@ Line 3, characters 19-20:
 |}]
 
 (* testing modalities in constructors *)
-type r_global = R_global of string * global_ string
+type r_shared = R_shared of string * string @@ shared many
 [%%expect{|
-type r_global = R_global of string * global_ string
+type r_shared = R_shared of string * string @@ many shared
 |}]
 
 let foo () =
-  let r = R_global ("hello", "world") in
-  let R_global (_, y) = r in
+  let r = R_shared ("hello", "world") in
+  let R_shared (_, y) = r in
   ignore (shared_id y);
   (* the following is allowed, because using r uniquely implies using r.x
      shared *)
@@ -715,17 +715,17 @@ val foo : unit -> unit = <fun>
 
  (* Similarly for linearity *)
 let foo () =
-  let r = once_ (R_global ("hello", "world")) in
-  let R_global (_, y) = r in
+  let r = once_ (R_shared ("hello", "world")) in
+  let R_shared (_, y) = r in
   ignore_once y;
   ignore_once r;
 [%%expect{|
 val foo : unit -> unit = <fun>
 |}]
 
 let foo () =
-  let r = once_ (R_global ("hello", "world")) in
-  let R_global (x, _) = r in
+  let r = once_ (R_shared ("hello", "world")) in
+  let R_shared (x, _) = r in
   ignore_once x;
   ignore_once r;
 [%%expect{|
@@ -741,8 +741,8 @@ Line 4, characters 14-15:
 |}]
 
 let foo () =
-  let r = R_global ("hello", "world") in
-  let R_global (x, _) = r in
+  let r = R_shared ("hello", "world") in
+  let R_shared (x, _) = r in
   ignore (shared_id x);
   (* doesn't work for normal fields *)
   ignore (unique_id r)

ocaml/typing/ctype.ml

@@ -3144,7 +3144,7 @@ and mcomp_record_description type_pairs env =
         mcomp type_pairs env l1.ld_type l2.ld_type;
         if Ident.name l1.ld_id = Ident.name l2.ld_id &&
            l1.ld_mutable = l2.ld_mutable &&
-           l1.ld_global = l2.ld_global
+           l1.ld_modalities = l2.ld_modalities
         then iter xs ys
         else raise Incompatible
     | [], [] -> ()

ocaml/typing/ctype.mli

@@ -186,7 +186,7 @@ type existential_treatment =
 
 val instance_constructor: existential_treatment ->
         constructor_description ->
-        (type_expr * Global_flag.t) list * type_expr * type_expr list
+        (type_expr * Modality.Value.t) list * type_expr * type_expr list
         (* Same, for a constructor. Also returns existentials. *)
 val instance_parameterized_type:
         ?keep_names:bool ->

ocaml/typing/datarepr.ml

@@ -95,7 +95,7 @@ let constructor_args ~current_unit priv cd_args cd_res path rep =
         }
       in
       existentials,
-      [ newgenconstr path type_params, Global_flag.Unrestricted ],
+      [ newgenconstr path type_params, Modality.Value.id ],
       Some tdecl
 
 let constructor_descrs ~current_unit ty_path decl cstrs rep =
@@ -201,7 +201,7 @@ let none =
 
 let dummy_label =
   { lbl_name = ""; lbl_res = none; lbl_arg = none;
-    lbl_mut = Immutable; lbl_global = Unrestricted;
+    lbl_mut = Immutable; lbl_modalities = Modality.Value.id;
     lbl_jkind = Jkind.any ~why:Dummy_jkind;
     lbl_num = -1; lbl_pos = -1; lbl_all = [||];
     lbl_repres = Record_unboxed;
@@ -222,7 +222,7 @@ let label_descrs ty_res lbls repres priv =
             lbl_res = ty_res;
             lbl_arg = l.ld_type;
             lbl_mut = l.ld_mutable;
-            lbl_global = l.ld_global;
+            lbl_modalities = l.ld_modalities;
             lbl_jkind = l.ld_jkind;
             lbl_pos = if is_void then lbl_pos_void else pos;
             lbl_num = num;