Skip to content

clean up mutable() logic as commented #2467

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Apr 21, 2024
Merged

clean up mutable() logic as commented #2467

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
3a3580a
clean up mutable() logic as commented
riaqn Apr 18, 2024
1541fde
address comment
riaqn Apr 21, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 21 additions & 0 deletions ocaml/testsuite/tests/typing-modes/mutable.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,3 +8,24 @@
yet. *)

(* CR zqian: add test for mutable when mutable is decoupled from modalities. *)

(* CR mode-crossing: Uncomment the following examples once portability is added. *)

(* The [m0] in mutable should cross modes upon construction. *)
(*
type r =
{ f : string -> string;
mutable a : int }
let r @ portable =
{ f = fun x -> x;
a = 42 } *)

(* The [m0] in mutable corresponds to the field type wrapped in modality; as a
result, it enjoys mode crossing enabled by the modality. *)
(*
type r =
{ f : string -> string;
mutable g : string -> string @@ portable }
let r @ portable =
{ f = fun x -> x;
g = fun x -> x } *)
94 changes: 38 additions & 56 deletions ocaml/typing/typecore.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -460,6 +460,11 @@ let mode_default mode =

let mode_legacy = mode_default Value.legacy

let mode_modality modality expected_mode =
expected_mode.mode
|> modality_box_right modality
|> mode_default

(* used when entering a function;
mode is the mode of the function region *)
let mode_return mode =
Expand Down Expand Up @@ -861,55 +866,28 @@ let apply_mode_annots ~loc ~env (m : Alloc.Const.Option.t) mode =
| 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
projected field. *)
let project_field mutability modalities (m : (allowed * _) Value.t) =
ignore mutability;
modality_unbox_left modalities m

(** Takes [m0] which is the parameter on mutable, and [m] which is a right mode
on the record being constructed, returns the right mode for the mutable
field used for construction. *)
let construct_mutable m0 m =
let m0 =
Alloc.Const.merge
{comonadic = m0;
monadic = Alloc.Monadic.Const.min}
in
let m0 = Const.alloc_as_value m0 in
(* We require [join m0 ret <= m], which is equivalent to [m0 <= m] and [ret <=
m]. *)
(match Value.submode (Value.of_const m0) m with
| Ok () -> ()
| Error _ -> Misc.fatal_error
"mutable defaults to Comonadic.legacy, \
which is min, so this call cannot fail."
);
m |> Value.disallow_left

(** Takes [m0] which is the parameter on mutable, returns the right mode for the
new value of the mutable field. *)
let mutate_mutable m0 =
(** Given the parameter [m0] on mutable, return the mode of future writes. *)
let mutable_mode m0 =
let m0 =
Alloc.Const.merge
{comonadic = m0;
monadic = Alloc.Monadic.Const.min}
in
let m0 = Const.alloc_as_value m0 in
m0 |> Value.of_const |> Value.disallow_left
m0 |> Const.alloc_as_value |> Value.of_const

(** Takes the mutability and modalities on the field, and expected mode of the
record (adjusted for allocation), returns the expected mode for the field.
*)
let construct_field mutability modalities (argument_mode : expected_mode) =
let mode =
match mutability with
| Immutable -> argument_mode.mode
| Mutable m0 -> construct_mutable m0 argument_mode.mode
in
let mode = modality_box_right modalities mode in
mode_default mode
(** Takes the mutability on a field, and expected mode of the record (adjusted
for allocation), check that the construction would be allowed. *)
let check_construct_mutability mutability (argument_mode : expected_mode) =
match mutability with
| Immutable -> ()
| Mutable m0 ->
let m0 = mutable_mode m0 in
match Value.submode m0 argument_mode.mode with
| Ok () -> ()
| Error _ ->
Misc.fatal_error
"mutable defaults to Comonadic.legacy, \
which is min, so this call cannot fail."

(* Typing of patterns *)

Expand Down Expand Up @@ -2414,7 +2392,7 @@ and type_pat_aux
(* CR zqian: decouple mutable and global modality *)
if Types.is_mutable mutability then Global else Unrestricted
in
let alloc_mode = project_field mutability modalities alloc_mode.mode in
let alloc_mode = modality_unbox_left modalities alloc_mode.mode in
let alloc_mode = simple_pat_mode alloc_mode in
let pl = List.map (fun p -> type_pat ~alloc_mode tps Value p ty_elt) spl in
rvp {
Expand Down Expand Up @@ -2657,7 +2635,7 @@ and type_pat_aux
let args =
List.map2
(fun p (ty, gf) ->
let alloc_mode = project_field Immutable gf alloc_mode.mode in
let alloc_mode = modality_unbox_left gf alloc_mode.mode in
let alloc_mode = simple_pat_mode alloc_mode in
type_pat ~alloc_mode tps Value p ty)
sargs (List.combine ty_args_ty ty_args_gf)
Expand Down Expand Up @@ -2700,7 +2678,7 @@ and type_pat_aux
let type_label_pat (label_lid, label, sarg) =
let ty_arg =
solve_Ppat_record_field ~refine loc env label label_lid record_ty in
let mode = project_field label.lbl_mut label.lbl_global alloc_mode.mode in
let mode = modality_unbox_left label.lbl_global alloc_mode.mode in
let alloc_mode = simple_pat_mode mode in
(label_lid, label, type_pat tps Value ~alloc_mode sarg ty_arg)
in
Expand Down Expand Up @@ -5594,7 +5572,8 @@ and type_expect_
None, expected_mode
in
let type_label_exp ((_, label, _) as x) =
let argument_mode = construct_field label.lbl_mut label.lbl_global argument_mode in
check_construct_mutability label.lbl_mut argument_mode;
let argument_mode = mode_modality label.lbl_global argument_mode in
type_label_exp true env argument_mode loc ty_record x
in
let lbl_exp_list = List.map type_label_exp lbl_a_list in
Expand Down Expand Up @@ -5655,8 +5634,11 @@ and type_expect_
unify_exp_types loc env ty_arg1 ty_arg2;
with_explanation (fun () ->
unify_exp_types loc env (instance ty_expected) ty_res2);
let mode = project_field lbl.lbl_mut lbl.lbl_global mode in
let argument_mode = construct_field lbl.lbl_mut lbl.lbl_global argument_mode in
let mode = modality_unbox_left lbl.lbl_global mode in
check_construct_mutability lbl.lbl_mut argument_mode;
let argument_mode =
mode_modality lbl.lbl_global argument_mode
in
submode ~loc ~env mode argument_mode;
Kept (ty_arg1, lbl.lbl_mut,
unique_use ~loc ~env mode argument_mode.mode)
Expand Down Expand Up @@ -5702,7 +5684,7 @@ and type_expect_
ty_arg
end ~post:generalize_structure
in
let mode = project_field label.lbl_mut label.lbl_global rmode in
let mode = modality_unbox_left label.lbl_global rmode in
let boxing : texp_field_boxing =
let is_float_boxing =
match label.lbl_repres with
Expand Down Expand Up @@ -5745,10 +5727,9 @@ and type_expect_
let (label_loc, label, newval) =
match label.lbl_mut with
| Mutable m0 ->
let mode = mutate_mutable m0 in
let mode = modality_box_right label.lbl_global mode in
type_label_exp false env (mode_default mode) loc
ty_record (lid, label, snewval)
let mode = mutable_mode m0 |> mode_default in
let mode = mode_modality label.lbl_global mode in
type_label_exp false env mode loc ty_record (lid, label, snewval)
| Immutable ->
raise(Error(loc, env, Label_not_mutable lid.txt))
in
Expand Down Expand Up @@ -7814,7 +7795,7 @@ and type_construct env (expected_mode : expected_mode) loc lid sarg
let args =
List.map2
(fun e ((ty, gf),t0) ->
let argument_mode = construct_field Immutable gf argument_mode in
let argument_mode = mode_modality gf argument_mode in
type_argument ~recarg env argument_mode e ty t0)
sargs (List.combine ty_args ty_args0)
in
Expand Down Expand Up @@ -8700,7 +8681,8 @@ and type_generic_array
else
Predef.type_iarray, Global_flag.Unrestricted
in
let argument_mode = construct_field mutability modalities argument_mode in
check_construct_mutability mutability argument_mode;
let argument_mode = mode_modality modalities argument_mode in
let jkind, elt_sort = Jkind.of_new_sort_var ~why:Array_element in
let ty = newgenvar jkind in
let to_unify = type_ ty in
Expand Down