Skip to content

Generalize Uniqueness Analysis to arbitrary semirings #3280

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.

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

Draft
wants to merge 35 commits into
base: main
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
35 commits
Select commit Hold shift + click to select a range
df98cac
Use pull_request_target for compatibility with forks
goldfirere Oct 4, 2024
869f84f
Basic overwriting syntax (#3089)
anfelor Oct 7, 2024
480138b
Map unique_barrier information to Reads_vary (#3066)
anfelor Oct 7, 2024
cfe0418
First draft of type checking
anfelor Oct 11, 2024
d0faa26
Check in uniqueness analysis that tags stay the same during overwriting
anfelor Oct 14, 2024
876e636
Report a syntax error on overwriting anything except an allocation
anfelor Oct 14, 2024
f1ab518
Overwriting tests (#3123)
anfelor Oct 16, 2024
f93e692
Merge branch 'overwriting' into overwriting-typing
anfelor Oct 16, 2024
b48eb61
Full type-checking for tuples and records
anfelor Oct 16, 2024
70ead74
Type checking fully implemented
anfelor Oct 17, 2024
345fee9
Clean up type-checking and add ability to overwrite arbitrary express…
anfelor Oct 17, 2024
945fb76
Fix checking of tags
anfelor Oct 17, 2024
c0785a4
Test (labeled) tuples
anfelor Oct 18, 2024
0de2a80
Final tests and allow overwrite of inlined records
anfelor Oct 18, 2024
fbf6e1b
Review suggestion
anfelor Oct 21, 2024
432eade
Review suggestion
anfelor Oct 21, 2024
f984a60
Review feedback: add more tests
anfelor Oct 21, 2024
b261b06
Uniqueness analysis: Change grammar of error message to indicate para…
anfelor Oct 21, 2024
ac401e7
Merge remote-tracking branch 'origin/overwriting-typing' into overwri…
anfelor Oct 21, 2024
2d2ae0b
Review feedback: Fix typo
anfelor Oct 21, 2024
7bf5cf0
Review feedback: add comments and tests
anfelor Oct 21, 2024
3518596
Merge remote-tracking branch 'origin/overwriting-typing' into overwri…
anfelor Oct 21, 2024
a2ca9af
Prevent nested allocations in overwrite
anfelor Oct 21, 2024
399581b
Review feedback: Fix comment and improve readability
anfelor Oct 21, 2024
16d6739
Review feedback: add comments, tests and nicer error messages
anfelor Oct 23, 2024
d385037
Fix nested record bug
anfelor Oct 23, 2024
2d8afdb
Improve code quality
anfelor Oct 23, 2024
288800a
Disallow overwriting of unboxed records
anfelor Oct 23, 2024
eaa0c9f
Review feedback
anfelor Oct 24, 2024
33b3634
Clarify the overwriting state for type_label_exp
goldfirere Oct 25, 2024
fd050dc
Add debugging printers for uniqueness
goldfirere Oct 25, 2024
c29a7bb
Temporarily allow unique mutable fields for better tests of overwriti…
anfelor Oct 30, 2024
3e5023e
New scheme for checking that overwrite does not change tags
anfelor Nov 4, 2024
255f533
Generalize uniqueness analysis to work over arbitrary semirings and s…
anfelor Nov 7, 2024
4d69a80
Reshuffle uniqueness analysis
anfelor Nov 7, 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
Prev Previous commit
Next Next commit
Review feedback
  • Loading branch information
anfelor committed Oct 24, 2024
commit eaa0c9fcb465c02be187f74b124cef4e11c437de
77 changes: 61 additions & 16 deletions ocaml/testsuite/tests/typing-unique/overwriting.ml
Original file line number Diff line number Diff line change
Expand Up @@ -427,6 +427,65 @@ Uncaught exception: File "ocaml/parsing/location.ml", line 1106, characters 2-8:

|}]

(*****************************************)
(* Disallowing overwriting unboxed types *)

type unboxed_record = { x : int } [@@unboxed]
[%%expect{|
type unboxed_record = { x : int; } [@@unboxed]
|}]

let update (r : unboxed_record) =
overwrite_ r with { x = 4 }
[%%expect{|
Line 2, characters 20-29:
2 | overwrite_ r with { x = 4 }
^^^^^^^^^
Error: Overwriting is only supported on tuples, constructors and boxed records.
|}]

type unboxed_inlined_record = Mk of { x : int } [@@unboxed]
[%%expect{|
type unboxed_inlined_record = Mk of { x : int; } [@@unboxed]
|}]

let update (r : unboxed_inlined_record) = match r with
| Mk _ -> overwrite_ r with Mk { x = 4 }
[%%expect{|
Line 2, characters 30-42:
2 | | Mk _ -> overwrite_ r with Mk { x = 4 }
^^^^^^^^^^^^
Error: Overwriting is only supported on tuples, constructors and boxed records.
|}]

type unboxed_constructor = Mk of int [@@unboxed]
[%%expect{|
type unboxed_constructor = Mk of int [@@unboxed]
|}]

let update (r : unboxed_constructor) = match r with
| Mk _ -> overwrite_ r with Mk 4
[%%expect{|
Line 2, characters 30-34:
2 | | Mk _ -> overwrite_ r with Mk 4
^^^^
Error: Overwriting is only supported on tuples, constructors and boxed records.
|}]

type unboxed_tuple = #(int * int)
[%%expect{|
type unboxed_tuple = #(int * int)
|}]

let update (r : unboxed_tuple) =
overwrite_ r with #(_, 3)
[%%expect{|
Line 2, characters 20-27:
2 | overwrite_ r with #(_, 3)
^^^^^^^
Error: Overwriting is only supported on tuples, constructors and boxed records.
|}]

(*************************************)
(* Other edge-cases of type checking *)

Expand All @@ -446,20 +505,6 @@ Uncaught exception: File "ocaml/parsing/location.ml", line 1106, characters 2-8:

|}]

type unboxed_record = { x : int } [@@unboxed]
[%%expect{|
type unboxed_record = { x : int; } [@@unboxed]
|}]

let update (r : unboxed_record) =
overwrite_ r with { x = 4 }
[%%expect{|
Line 2, characters 20-29:
2 | overwrite_ r with { x = 4 }
^^^^^^^^^
Error: Overwriting is only supported on tuples, constructors and boxed records.
|}]

type nested_record = Nested of { x : int }
[%%expect{|
type nested_record = Nested of { x : int; }
Expand All @@ -471,7 +516,7 @@ let nested_update (t : int * (string * int)) =
Line 2, characters 29-30:
2 | overwrite_ t with (3, ("", _))
^
Error: Syntax error: "wildcard "_"" not expected.
Error: wildcard "_" not expected.
|}]

let nested_update (t : int * record_update) =
Expand All @@ -480,7 +525,7 @@ let nested_update (t : int * record_update) =
Line 2, characters 29-30:
2 | overwrite_ t with (3, {x = _; y = _})
^
Error: Syntax error: "wildcard "_"" not expected.
Error: wildcard "_" not expected.
|}]

let nested_update t =
Expand Down
6 changes: 3 additions & 3 deletions ocaml/testsuite/tests/typing-unique/overwriting_syntax.ml
Original file line number Diff line number Diff line change
Expand Up @@ -111,23 +111,23 @@ let underscore = _
Line 1, characters 17-18:
1 | let underscore = _
^
Error: Syntax error: "wildcard "_"" not expected.
Error: wildcard "_" not expected.
|}]

let underscore_tuple = (_, 1)
[%%expect{|
Line 1, characters 24-25:
1 | let underscore_tuple = (_, 1)
^
Error: Syntax error: "wildcard "_"" not expected.
Error: wildcard "_" not expected.
|}]

let underscore_record = { a = _; b = 1 }
[%%expect{|
Line 1, characters 30-31:
1 | let underscore_record = { a = _; b = 1 }
^
Error: Syntax error: "wildcard "_"" not expected.
Error: wildcard "_" not expected.
|}]

let overwrite_with_let t = overwrite_ t with let x = (1, 2) in x
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ let underscore = _
Line 1, characters 17-18:
1 | let underscore = _
^
Error: Syntax error: "wildcard "_"" not expected.
Error: wildcard "_" not expected.
|}]

let overwriting t = overwrite_ t with (a, b)
Expand Down
98 changes: 52 additions & 46 deletions ocaml/typing/typecore.ml
Original file line number Diff line number Diff line change
Expand Up @@ -263,6 +263,7 @@ type error =
| Unsupported_stack_allocation of unsupported_stack_allocation
| Not_allocation
| Overwrite_of_invalid_term
| Unexpected_hole

exception Error of Location.t * Env.t * error
exception Error_forward of Location.error
Expand Down Expand Up @@ -676,29 +677,29 @@ let optimise_allocations () =
!allocations;
reset_allocations ()

(** The state of the overwrite determines if we have already checked the
allocation to be overwritten. The complexity arises here because the
allocation can consist of both a constructor and an inlined record. *)
type overwrite_state =
| Expect_allocation (* we expect a tuple/constructor/record/inlined record *)
| Expect_field_assignment (* we expect a concrete value or hole *)

(** We keep this state which is passed as an optional argument throughout
the typechecker. It goes through the following life-cycle:
- It starts as No_overwrite
- Once we find an Texp_overwrite, we create an Overwriting()
- If we find a constructor with inlined record, we specialize
the Overwriting to the type/mode of the inlined record
- Once we find an allocation, we pass an Assigning() to the fields
- If the fields are a Texp_hole, we use the stored type/mode.
- We reset the state to No_overwrite *)
type overwrite =
| No_overwrite
| Overwriting of
Location.t * (* location of expression being overwritten *)
Types.type_expr * (* type of expression *)
Value.l * (* mode of kept fields *)
overwrite_state (* state in the overwrite *)
Value.l (* mode of kept fields *)
| Assigning of
Types.type_expr * (* type of expression *)
Value.l (* mode of kept fields *)

let assign_children n f = function
| Overwriting(loc, typ, mode, Expect_allocation) -> f loc typ mode
| Overwriting(loc, typ, mode) -> f loc typ mode
| _ -> List.init n (fun _ -> No_overwrite)

let assign_non_hole = function
| (No_overwrite | Overwriting(_, _, _, Expect_field_assignment)) -> No_overwrite
| Overwriting(_, _, _, Expect_allocation) as overwrite -> overwrite

let rec can_be_overwritten = function
| Pexp_constraint (e, _, _) -> can_be_overwritten e.pexp_desc
| (Pexp_tuple _ | Pexp_construct _ | Pexp_record _) -> true
Expand Down Expand Up @@ -5681,7 +5682,6 @@ and type_expect_
in
Some (exp, mode)
in
let overwrite = assign_non_hole overwrite in
let ty_record, expected_type =
let extract_record loc ty error =
match extract_concrete_record env ty with
Expand All @@ -5698,10 +5698,9 @@ and type_expect_
match opt_exp with
| None ->
begin match overwrite with
| Overwriting (loc, ty, _, Expect_allocation) ->
| Overwriting (loc, ty, _) ->
extract_record loc ty (Expr_not_a_record_type ty)
| Overwriting (_, _, _, Expect_field_assignment) -> assert false
| No_overwrite -> None
| (No_overwrite | Assigning _) -> None
end
| Some (exp, _) ->
extract_record exp.exp_loc exp.exp_type
Expand Down Expand Up @@ -5735,14 +5734,12 @@ and type_expect_
| _ -> false)
lbl_a_list
in
let _check_overwrite_unboxed_record =
match overwrite with
| No_overwrite -> ()
| Overwriting(_, _, _, Expect_field_assignment) -> assert false
| Overwriting(_, _, _, Expect_allocation) ->
begin match overwrite with
| (No_overwrite | Assigning _) -> ()
| Overwriting _ ->
if is_unboxed then
raise (Error (loc, env, Overwrite_of_invalid_term));
in
end;
let alloc_mode, argument_mode =
if not is_unboxed then
let alloc_mode, argument_mode = register_allocation expected_mode in
Expand All @@ -5757,12 +5754,10 @@ and type_expect_
in
let overwrites =
assign_children (List.length lbl_a_list)
(fun loc ty mode -> (* only change mode here, see type_label_exp *)
(fun _loc ty mode -> (* only change mode here, see type_label_exp *)
List.map (fun (_, label, _) ->
let mode = Modality.Value.Const.apply label.lbl_modalities mode in
(* We pass Expect_allocation to allow type_label_exp
to specialize the overwrite again *)
Overwriting(loc, ty, mode, Expect_allocation))
Assigning(ty, mode))
lbl_a_list)
overwrite
in
Expand Down Expand Up @@ -5811,7 +5806,7 @@ and type_expect_
end
in
match opt_exp, overwrite with
None, No_overwrite ->
None, (No_overwrite | Assigning _) ->
let label_definitions =
Array.map (fun lbl ->
match matching_label lbl with
Expand All @@ -5834,13 +5829,12 @@ and type_expect_
lbl.lbl_all
in
None, label_definitions
| None, Overwriting (exp_loc, exp_type, mode, Expect_allocation) ->
| None, Overwriting (exp_loc, exp_type, mode) ->
let ty_exp = instance exp_type in
let label_definitions =
Array.map (unify_kept loc exp_loc ty_exp mode) lbl.lbl_all
in
None, label_definitions
| None, Overwriting (_, _, _, Expect_field_assignment) -> assert false
| Some (exp, mode), _ ->
let ty_exp = instance exp.exp_type in
let label_definitions =
Expand Down Expand Up @@ -6661,7 +6655,7 @@ and type_expect_
|> Value.disallow_right
in
let overwrite =
Overwriting (exp1.exp_loc, exp1.exp_type, fields_mode, Expect_allocation)
Overwriting (exp1.exp_loc, exp1.exp_type, fields_mode)
in
type_expect ~recarg ~overwrite env exp2_mode exp2 ty_expected_explained
in
Expand All @@ -6672,7 +6666,7 @@ and type_expect_
exp_env = env }
| Pexp_hole ->
begin match overwrite with
| Overwriting(_loc, typ, fields_mode, Expect_field_assignment) ->
| Assigning(typ, fields_mode) ->
assert (Language_extension.is_enabled Overwriting);
with_explanation (fun () -> unify_exp_types loc env typ (instance ty_expected));
submode ~loc ~env fields_mode expected_mode;
Expand All @@ -6682,7 +6676,7 @@ and type_expect_
exp_type = ty_expected_explained.ty;
exp_attributes = sexp.pexp_attributes;
exp_env = env }
| _ -> raise Syntaxerr.(Error(Not_expecting(loc, "wildcard \"_\"")))
| _ -> raise (Error (loc, env, Unexpected_hole));
end

and expression_constraint pexp =
Expand Down Expand Up @@ -7531,11 +7525,16 @@ and type_label_exp ~overwrite create env (arg_mode : expected_mode) loc ty_expec
raise (Error(lid.loc, env, Private_label(lid.txt, ty_expected)));
let snap = if vars = [] then None else Some (Btype.snapshot ()) in
let overwrite =
List.hd (assign_children 1
(fun loc ty mode -> (* mode is correct already, see Pexp_record *)
let (_, ty_arg) = unify_as_label ty in
[Overwriting(loc, ty_arg, mode, Expect_field_assignment)])
overwrite)
match overwrite with
| No_overwrite -> No_overwrite
| Overwriting(loc, ty, mode) ->
(* mode is correct already, see Pexp_record *)
let (_, ty_arg) = unify_as_label ty in
Overwriting(loc, ty_arg, mode)
| Assigning(ty, mode) ->
(* mode is correct already, see Pexp_record *)
let (_, ty_arg) = unify_as_label ty in
Assigning(ty_arg, mode)
in
let arg = type_argument ~overwrite env arg_mode sarg ty_arg (instance ty_arg) in
(vars, ty_arg, snap, arg)
Expand Down Expand Up @@ -8007,10 +8006,10 @@ and type_tuple ~overwrite ~loc ~env ~(expected_mode : expected_mode) ~ty_expecte
in
let types_and_modes = List.combine labeled_subtypes argument_modes in
let overwrites =
assign_children arity (fun loc typ mode ->
assign_children arity (fun _loc typ mode ->
let labeled_subtypes = unify_as_tuple typ in
List.map
(fun (_, typ) -> Overwriting(loc, typ, mode, Expect_field_assignment))
(fun (_, typ) -> Assigning(typ, mode))
labeled_subtypes)
overwrite
in
Expand Down Expand Up @@ -8195,17 +8194,21 @@ and type_construct ~overwrite env (expected_mode : expected_mode) loc lid sarg
let alloc_mode, argument_mode = register_allocation expected_mode in
argument_mode, Some alloc_mode
in
begin match overwrite, constr.cstr_repr with
| Overwriting(_, _, _), Variant_unboxed ->
raise (Error (loc, env, Overwrite_of_invalid_term));
| _, _ -> ()
end;
let overwrites =
assign_children constr.cstr_arity
(fun loc ty mode ->
let ty_args, _, _ = unify_as_construct ty in
List.map (fun ty_arg ->
let mode = Modality.Value.Const.apply ty_arg.Types.ca_modalities mode in
let status = match recarg with
| Required -> Expect_allocation
| Allowed | Rejected -> Expect_field_assignment
in
Overwriting(loc, ty_arg.Types.ca_type, mode, status))
match recarg with
| Required -> Overwriting(loc, ty_arg.Types.ca_type, mode)
| Allowed | Rejected -> Assigning(ty_arg.Types.ca_type, mode)
)
ty_args)
overwrite
in
Expand Down Expand Up @@ -10710,6 +10713,9 @@ let report_error ~loc env = function
| Overwrite_of_invalid_term ->
Location.errorf ~loc
"Overwriting is only supported on tuples, constructors and boxed records."
| Unexpected_hole ->
Location.errorf ~loc
"wildcard \"_\" not expected."

let report_error ~loc env err =
Printtyp.wrap_printing_env_error env
Expand Down
1 change: 1 addition & 0 deletions ocaml/typing/typecore.mli
Original file line number Diff line number Diff line change
Expand Up @@ -316,6 +316,7 @@ type error =
| Unsupported_stack_allocation of unsupported_stack_allocation
| Not_allocation
| Overwrite_of_invalid_term
| Unexpected_hole

exception Error of Location.t * Env.t * error
exception Error_forward of Location.error
Expand Down
Loading
Loading