diff --git a/file_formats/cmt_format.ml b/file_formats/cmt_format.ml index 3e220fa7ab0..39f11d64d10 100644 --- a/file_formats/cmt_format.ml +++ b/file_formats/cmt_format.ml @@ -227,7 +227,7 @@ let iter_on_occurrences | Texp_object _ | Texp_pack _ | Texp_letop _ | Texp_unreachable | Texp_list_comprehension _ | Texp_array_comprehension _ | Texp_probe _ | Texp_probe_is_enabled _ | Texp_exclave _ - | Texp_open _ | Texp_src_pos -> ()); + | Texp_open _ | Texp_src_pos | Texp_overwrite _ | Texp_hole _ -> ()); default_iterator.expr sub e); (* Remark: some types get iterated over twice due to how constraints are diff --git a/lambda/translcore.ml b/lambda/translcore.ml index 5d5c9abff3e..ba10fad7160 100644 --- a/lambda/translcore.ml +++ b/lambda/translcore.ml @@ -1207,6 +1207,10 @@ and transl_exp0 ~in_new_scope ~scopes sort e = ] in Lconst(Const_block(0, cl)) + | Texp_overwrite (_, _) -> + Location.todo_overwrite_not_implemented ~kind:"Translcore" e.exp_loc + | Texp_hole _ -> + Location.todo_overwrite_not_implemented ~kind:"Translcore" e.exp_loc and pure_module m = match m.mod_desc with diff --git a/parsing/ast_helper.ml b/parsing/ast_helper.ml index 261c6bb9cc6..9d61c6e819e 100644 --- a/parsing/ast_helper.ml +++ b/parsing/ast_helper.ml @@ -245,7 +245,7 @@ module Exp = struct let unreachable ?loc ?attrs () = mk ?loc ?attrs Pexp_unreachable let stack ?loc ?attrs e = mk ?loc ?attrs (Pexp_stack e) let comprehension ?loc ?attrs e = mk ?loc ?attrs (Pexp_comprehension e) - let overwrite ?loc ?attrs x e = mk ?loc ?attrs (Pexp_overwrite (x, e)) + let overwrite ?loc ?attrs a b = mk ?loc ?attrs (Pexp_overwrite (a, b)) let hole ?loc ?attrs () = mk ?loc ?attrs Pexp_hole let case lhs ?guard rhs = diff --git a/parsing/ast_helper.mli b/parsing/ast_helper.mli index bdf72c2a4fc..74420b564f4 100644 --- a/parsing/ast_helper.mli +++ b/parsing/ast_helper.mli @@ -210,7 +210,7 @@ module Exp: val stack : ?loc:loc -> ?attrs:attrs -> expression -> expression val comprehension : ?loc:loc -> ?attrs:attrs -> comprehension_expression -> expression - val overwrite : ?loc:loc -> ?attrs:attrs -> lid -> expression -> expression + val overwrite : ?loc:loc -> ?attrs:attrs -> expression -> expression -> expression val hole : ?loc:loc -> ?attrs:attrs -> unit -> expression val case: pattern -> ?guard:expression -> expression -> case diff --git a/parsing/ast_iterator.ml b/parsing/ast_iterator.ml index 57d2a9e9eab..79147e5e556 100644 --- a/parsing/ast_iterator.ml +++ b/parsing/ast_iterator.ml @@ -532,7 +532,7 @@ module E = struct | Pexp_unreachable -> () | Pexp_stack e -> sub.expr sub e | Pexp_comprehension e -> iter_comp_exp sub e - | Pexp_overwrite (x, e) -> iter_loc sub x; sub.expr sub e + | Pexp_overwrite (e1, e2) -> sub.expr sub e1; sub.expr sub e2 | Pexp_hole -> () let iter_binding_op sub {pbop_op; pbop_pat; pbop_exp; pbop_loc} = diff --git a/parsing/ast_mapper.ml b/parsing/ast_mapper.ml index 0cd1fc53f17..61ee6a97e5e 100644 --- a/parsing/ast_mapper.ml +++ b/parsing/ast_mapper.ml @@ -605,7 +605,7 @@ module E = struct | Pexp_unreachable -> unreachable ~loc ~attrs () | Pexp_stack e -> stack ~loc ~attrs (sub.expr sub e) | Pexp_comprehension c -> comprehension ~loc ~attrs (map_cexp sub c) - | Pexp_overwrite (x, e) -> overwrite ~loc ~attrs (map_loc sub x) (sub.expr sub e) + | Pexp_overwrite (e1, e2) -> overwrite ~loc ~attrs (sub.expr sub e1) (sub.expr sub e2) | Pexp_hole -> hole ~loc ~attrs () let map_binding_op sub {pbop_op; pbop_pat; pbop_exp; pbop_loc} = diff --git a/parsing/depend.ml b/parsing/depend.ml index 2133140aed3..4dddf128bed 100644 --- a/parsing/depend.ml +++ b/parsing/depend.ml @@ -313,7 +313,7 @@ let rec add_expr bv exp = end | Pexp_extension e -> handle_extension e | Pexp_stack e -> add_expr bv e - | Pexp_overwrite (x, e) -> add bv x; add_expr bv e + | Pexp_overwrite (e1, e2) -> add_expr bv e1; add_expr bv e2 | Pexp_hole -> () | Pexp_unreachable -> () | Pexp_comprehension x -> add_comprehension_expr bv x diff --git a/parsing/location.ml b/parsing/location.ml index bbc9f8a747d..35c8faecfe4 100644 --- a/parsing/location.ml +++ b/parsing/location.ml @@ -1102,6 +1102,6 @@ let () = let raise_errorf ?(loc = none) ?(sub = []) = Format.kdprintf (fun txt -> raise (Error (mkerror loc sub txt))) -let todo_overwrite_not_implemented t = - alert ~kind:"" t "Overwrite not implemented."; +let todo_overwrite_not_implemented ?(kind = "") t = + alert ~kind t "Overwrite not implemented."; assert false diff --git a/parsing/location.mli b/parsing/location.mli index 883502ca857..6e53786e0f4 100644 --- a/parsing/location.mli +++ b/parsing/location.mli @@ -398,4 +398,4 @@ val report_exception: formatter -> exn -> unit (** Reraise the exception if it is unknown. *) (** CR uniqueness: remove this *) -val todo_overwrite_not_implemented : t -> 'a +val todo_overwrite_not_implemented : ?kind:string -> t -> 'a diff --git a/parsing/parser.mly b/parsing/parser.mly index e3d825413bf..89af876782b 100644 --- a/parsing/parser.mly +++ b/parsing/parser.mly @@ -2845,7 +2845,7 @@ fun_expr: { Pexp_try($3, $5), $2 } | TRY ext_attributes seq_expr WITH error { syntax_error() } - | OVERWRITE ext_attributes mkrhs(val_longident) WITH expr + | OVERWRITE ext_attributes seq_expr WITH expr { Pexp_overwrite($3, $5), $2 } | IF ext_attributes seq_expr THEN expr ELSE expr { Pexp_ifthenelse($3, $5, Some $7), $2 } diff --git a/parsing/parsetree.mli b/parsing/parsetree.mli index 3141885e072..be3ece493a4 100644 --- a/parsing/parsetree.mli +++ b/parsing/parsetree.mli @@ -491,7 +491,7 @@ and expression_desc = - [CLAUSES] is a series of [comprehension_clause]. *) (* CR uniqueness: allow arbitrary expressions instead of identifiers here *) - | Pexp_overwrite of Longident.t loc * expression (** overwrite_ x with exp *) + | Pexp_overwrite of expression * expression (** overwrite_ exp with exp *) | Pexp_hole (** _ *) and case = diff --git a/parsing/pprintast.ml b/parsing/pprintast.ml index 00b10f98b61..d621ad379bc 100644 --- a/parsing/pprintast.ml +++ b/parsing/pprintast.ml @@ -1090,11 +1090,11 @@ and expression ctxt f x = (expression ctxt) body | Pexp_extension e -> extension ctxt f e | Pexp_unreachable -> pp f "." - | Pexp_overwrite (x, e) -> + | Pexp_overwrite (e1, e2) -> (* Similar to the case of [Pexp_stack] *) pp f "@[overwrite_@ %a@ with@ %a@]" - longident_loc x - (expression2 reset_ctxt) e + (expression2 reset_ctxt) e1 + (expression2 reset_ctxt) e2 | Pexp_hole -> pp f "_" | _ -> expression1 ctxt f x diff --git a/parsing/printast.ml b/parsing/printast.ml index 391b825b185..7dba0d4b4a2 100644 --- a/parsing/printast.ml +++ b/parsing/printast.ml @@ -437,9 +437,10 @@ and expression i ppf x = | Pexp_comprehension c -> line i ppf "Pexp_comprehension\n"; comprehension_expression i ppf c - | Pexp_overwrite (x, e) -> - line i ppf "Pexp_overwrite %a\n" fmt_longident_loc x; - expression i ppf e + | Pexp_overwrite (e1, e2) -> + line i ppf "Pexp_overwrite\n"; + expression i ppf e1; + expression i ppf e2; | Pexp_hole -> line i ppf "Pexp_hole" diff --git a/printer/printast_with_mappings.ml b/printer/printast_with_mappings.ml index 67e41b4d764..f63b67e094a 100644 --- a/printer/printast_with_mappings.ml +++ b/printer/printast_with_mappings.ml @@ -461,9 +461,10 @@ and expression i ppf x = | Pexp_comprehension c -> line i ppf "Pexp_comprehension\n"; comprehension_expression i ppf c - | Pexp_overwrite (x, e) -> - line i ppf "Pexp_overwrite %a\n" fmt_longident_loc x; - expression i ppf e + | Pexp_overwrite (e1, e2) -> + line i ppf "Pexp_overwrite\n"; + expression i ppf e1; + expression i ppf e2 | Pexp_hole -> line i ppf "Pexp_hole" ) diff --git a/testsuite/tests/parsetree/source_jane_street.ml b/testsuite/tests/parsetree/source_jane_street.ml index c8c3b0c3941..d6ac1f8ea5f 100644 --- a/testsuite/tests/parsetree/source_jane_street.ml +++ b/testsuite/tests/parsetree/source_jane_street.ml @@ -1203,6 +1203,11 @@ let overwrite_record = function let overwrite_record = function { a; b } as t -> overwrite_ t with { b = a } +let ret_record () = { a = 1; b = 2 } + +let overwrite_record () = + overwrite_ (ret_record ()) with { b = a } + type constructor = C of { a : int; b : int } let overwrite_constructor = function @@ -1214,7 +1219,7 @@ let overwrite_constructor = function Line 2, characters 19-43: 2 | (a, b) as t -> overwrite_ t with (b, _) ^^^^^^^^^^^^^^^^^^^^^^^^ -Alert : Overwrite not implemented. +Alert Translcore: Overwrite not implemented. Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed |}] diff --git a/testsuite/tests/typing-modes/modes.ml b/testsuite/tests/typing-modes/modes.ml index af7c95803aa..f15bc1925b9 100644 --- a/testsuite/tests/typing-modes/modes.ml +++ b/testsuite/tests/typing-modes/modes.ml @@ -297,7 +297,7 @@ type r = { mutable x : string @@ global aliased many } [%%expect{| -type r = { mutable x : string; } +type r = { mutable x : string @@ aliased; } |}] diff --git a/testsuite/tests/typing-modes/mutable.ml b/testsuite/tests/typing-modes/mutable.ml index 9da90679c09..47af1368569 100644 --- a/testsuite/tests/typing-modes/mutable.ml +++ b/testsuite/tests/typing-modes/mutable.ml @@ -75,10 +75,7 @@ Error: This value escapes its region. portable record (ignoring mode-crossing). *) let foo (s @ portable) = ({s} : _ @@ portable) [%%expect{| -Line 1, characters 26-29: -1 | let foo (s @ portable) = ({s} : _ @@ portable) - ^^^ -Error: This value is "nonportable" but expected to be "portable". +val foo : 'a @ portable -> 'a r = |}] (* This attribute doesn't disable implied modalities on monadic axes. For @@ -92,15 +89,15 @@ val foo : 'a r -> 'a -> unit = let foo (s @ aliased) = ({s} : _ @@ unique) [%%expect{| -val foo : 'a -> 'a r = +Line 1, characters 26-27: +1 | let foo (s @ aliased) = ({s} : _ @@ unique) + ^ +Error: This value is "aliased" but expected to be "unique". |}] let foo (r @ unique) = (r.s : _ @@ unique) [%%expect{| -Line 1, characters 24-27: -1 | let foo (r @ unique) = (r.s : _ @@ unique) - ^^^ -Error: This value is "aliased" but expected to be "unique". +val foo : 'a r @ unique -> 'a = |}] module M : sig @@ -164,10 +161,7 @@ let r @ portable = (* CR mode-crossing: The [m0] in mutable should cross modes upon construction. *) [%%expect{| type r = { f : string -> string; mutable a : int; } -Lines 5-6, characters 2-12: -5 | ..{ f = (fun x -> x); -6 | a = 42 } -Error: This value is "nonportable" but expected to be "portable". +val r : r = {f = ; a = 42} |}] type r = @@ -180,8 +174,5 @@ let r @ portable = in modality; as a result, it enjoys mode crossing enabled by the modality. *) [%%expect{| type r = { f : string -> string; mutable g : string -> string @@ portable; } -Lines 5-6, characters 2-20: -5 | ..{ f = (fun x -> x); -6 | g = fun x -> x } -Error: This value is "nonportable" but expected to be "portable". +val r : r = {f = ; g = } |}] diff --git a/testsuite/tests/typing-modes/portable-contend.ml b/testsuite/tests/typing-modes/portable-contend.ml index 86bfcc797e7..74da6f93cf9 100644 --- a/testsuite/tests/typing-modes/portable-contend.ml +++ b/testsuite/tests/typing-modes/portable-contend.ml @@ -166,10 +166,7 @@ let foo () = and the above bar is closing over an nonportable record. Once we allow mutable() syntax, we can test this. *) [%%expect{| -Line 2, characters 23-61: -2 | let r @ portable = {a = best_bytes (); b = best_bytes ()} in - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: This value is "nonportable" but expected to be "portable". +val foo : unit -> unit = |}] diff --git a/testsuite/tests/typing-modes/val_modalities.ml b/testsuite/tests/typing-modes/val_modalities.ml index 91ea67dee38..5afd8b7eddb 100644 --- a/testsuite/tests/typing-modes/val_modalities.ml +++ b/testsuite/tests/typing-modes/val_modalities.ml @@ -34,7 +34,7 @@ module M = struct let foo = {x = "hello"} end [%%expect{| -module M : sig val foo : r @@ global many end +module M : sig val foo : r @@ global many portable end |}] module type S = sig diff --git a/testsuite/tests/typing-unique/overwriting.ml b/testsuite/tests/typing-unique/overwriting.ml index 07e3e079fed..4a06c41952d 100644 --- a/testsuite/tests/typing-unique/overwriting.ml +++ b/testsuite/tests/typing-unique/overwriting.ml @@ -3,49 +3,69 @@ expect; *) -(* CR uniqueness: More tests to consider adding here: - - overwriting tuples - - overwriting labeled tuples - - overwriting labeled tuples where only some labels are given - - overwriting tuples (and labeled ones) with the new .. syntax - - overwriting inline records (binding a variable to the whole constructor application, - like | (K { ... }) as v -> ...) - - overwriting inline records (binding a variable just to the inline record, - like | K r -> ...) - - overwriting constructor fields - - overwriting mutable fields (yes, this is a bit silly, but we should test it) - - overwriting immutable fields of records with mutable fields - - local variants of (some of) the above - - overwriting into a local record with a freshly-constructed bit of memory - (to make sure that inference does not locally allocate the new memory) -*) - type record_update = { x : string; y : string } [%%expect{| type record_update = { x : string; y : string; } |}] - let update (unique_ r : record_update) = - let x = overwrite_ r with { x = "foo" } - in x.x + let x = overwrite_ r with { x = "foo" } in + x.x [%%expect{| Line 2, characters 10-41: -2 | let x = overwrite_ r with { x = "foo" } +2 | let x = overwrite_ r with { x = "foo" } in ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Alert : Overwrite not implemented. +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let update (unique_ r : record_update) = + let x = overwrite_ r with ({ x = "foo" } : record_update) in + x.x +[%%expect{| +Line 2, characters 10-59: +2 | let x = overwrite_ r with ({ x = "foo" } : record_update) in + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed |}] -let update2 = update { x = "bar" } +(*************************************) +(* Checking uniqueness of overwrites *) + +let id = function x -> x + +let overwrite_shared (r : record_update) = + let r = id r in + let x = overwrite_ r with { x = "foo" } in + x.x +[%%expect{| +val id : ('a : value_or_null). 'a -> 'a @@ global many = +Line 5, characters 21-22: +5 | let x = overwrite_ r with { x = "foo" } in + ^ +Error: This value is "aliased" but expected to be "unique". +|}] + +let overwrite_shared (r : record_update) = + let x = overwrite_ r with { x = "foo" } in + x.x, r.x [%%expect{| -Line 1, characters 14-20: -1 | let update2 = update { x = "bar" } - ^^^^^^ -Error: Unbound value "update" +Line 3, characters 7-8: +3 | x.x, r.x + ^ +Error: This value is read from here, but it has already been used as unique: +Line 2, characters 21-22: +2 | let x = overwrite_ r with { x = "foo" } in + ^ + |}] +(**************************************) +(* Checking regionality of overwrites *) + (* Only global values may be written during overwrites, since the GC does not allow heap-to-stack pointers. However, it is fine if there are local values (like y here) @@ -57,45 +77,37 @@ Error: Unbound value "update" let gc_soundness_bug (local_ unique_ r) (local_ x) = exclave_ overwrite_ r with { x } [%%expect{| -Line 2, characters 11-34: +Line 2, characters 31-32: 2 | exclave_ overwrite_ r with { x } - ^^^^^^^^^^^^^^^^^^^^^^^ -Alert : Overwrite not implemented. -Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed - + ^ +Error: This value escapes its region. |}] let disallowed_by_locality (local_ unique_ r) (local_ x) = overwrite_ r with { x } [%%expect{| -Line 2, characters 2-25: +Line 2, characters 22-23: 2 | overwrite_ r with { x } - ^^^^^^^^^^^^^^^^^^^^^^^ -Alert : Overwrite not implemented. -Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed - + ^ +Error: This value escapes its region. |}] let gc_soundness_bug (unique_ r) (local_ x) = exclave_ overwrite_ r with { x } [%%expect{| -Line 2, characters 11-34: +Line 2, characters 31-32: 2 | exclave_ overwrite_ r with { x } - ^^^^^^^^^^^^^^^^^^^^^^^ -Alert : Overwrite not implemented. -Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed - + ^ +Error: This value escapes its region. |}] let disallowed_by_locality (unique_ r) (local_ x) = overwrite_ r with { x } [%%expect{| -Line 2, characters 2-25: +Line 2, characters 22-23: 2 | overwrite_ r with { x } - ^^^^^^^^^^^^^^^^^^^^^^^ -Alert : Overwrite not implemented. -Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed - + ^ +Error: This value escapes its region. |}] let gc_soundness_no_bug (local_ unique_ r) x = @@ -104,29 +116,76 @@ let gc_soundness_no_bug (local_ unique_ r) x = Line 2, characters 11-34: 2 | exclave_ overwrite_ r with { x } ^^^^^^^^^^^^^^^^^^^^^^^ -Alert : Overwrite not implemented. +Alert Translcore: Overwrite not implemented. Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed |}] -let disallowed_by_locality (local_ unique_ r) x = +(* This code should fail if we used a real allocation { r with x } here. + But we don't: the overwritten record may be regional in this case since + no allocation takes place. We check four related cases below. *) +let returning_regional (local_ unique_ r) x = overwrite_ r with { x } [%%expect{| Line 2, characters 2-25: 2 | overwrite_ r with { x } ^^^^^^^^^^^^^^^^^^^^^^^ -Alert : Overwrite not implemented. +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let disallowed_by_locality () x = + let r = stack_ { x = ""; y = "" } in + overwrite_ r with { x } +[%%expect{| +Line 3, characters 13-14: +3 | overwrite_ r with { x } + ^ +Error: This value escapes its region. +|}] + +let returning_regional () x = + exclave_ + let r = stack_ { x = ""; y = "" } in + overwrite_ r with { x } +[%%expect{| +Line 4, characters 4-27: +4 | overwrite_ r with { x } + ^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed |}] +let disallowed_by_locality () x = + let r = stack_ { x = ""; y = "" } in + exclave_ overwrite_ r with { x } +[%%expect{| +Line 3, characters 22-23: +3 | exclave_ overwrite_ r with { x } + ^ +Error: The value "r" is local, so it cannot be used inside an exclave_ +|}] + +let disallowed_by_regionality (local_ unique_ r) x = + let r = overwrite_ r with { x } in + let ref = ref r in + ref +[%%expect{| +Line 3, characters 16-17: +3 | let ref = ref r in + ^ +Error: This value escapes its region. +|}] + let gc_soundness_no_bug (unique_ r) x = exclave_ overwrite_ r with { x } [%%expect{| Line 2, characters 11-34: 2 | exclave_ overwrite_ r with { x } ^^^^^^^^^^^^^^^^^^^^^^^ -Alert : Overwrite not implemented. +Alert Translcore: Overwrite not implemented. Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed |}] @@ -137,7 +196,988 @@ let gc_soundness_no_bug (unique_ r) x = Line 2, characters 2-25: 2 | overwrite_ r with { x } ^^^^^^^^^^^^^^^^^^^^^^^ -Alert : Overwrite not implemented. +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +(*******************************) +(* Type-checking strong update *) + +type 'a eq = { eq0 : 'a; eq1 : 'a } +type 'a pair = 'a * 'a +[%%expect{| +type 'a eq = { eq0 : 'a; eq1 : 'a; } +type 'a pair = 'a * 'a +|}] + +let update eq = + overwrite_ eq with { eq0 = "foo" } +[%%expect{| +Line 2, characters 2-36: +2 | overwrite_ eq with { eq0 = "foo" } + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let update eq = + overwrite_ eq with { eq0 = "foo"; eq1 = 1 } +[%%expect{| +Line 2, characters 42-43: +2 | overwrite_ eq with { eq0 = "foo"; eq1 = 1 } + ^ +Error: This expression has type "int" but an expression was expected of type + "string" +|}] + +let update = + let eq = { eq0 = "foo" ; eq1 = "bar" } in + { eq with eq0 = 1 } +[%%expect{| +Line 3, characters 2-21: +3 | { eq with eq0 = 1 } + ^^^^^^^^^^^^^^^^^^^ +Error: This expression has type "int eq" but an expression was expected of type + "string eq" + Type "int" is not compatible with type "string" +|}] + +let update = + let eq = { eq0 = "foo" ; eq1 = "bar" } in + overwrite_ eq with { eq0 = 1 } +[%%expect{| +Line 3, characters 21-32: +3 | overwrite_ eq with { eq0 = 1 } + ^^^^^^^^^^^ +Error: This expression has type "int eq" but an expression was expected of type + "string eq" + Type "int" is not compatible with type "string" +|}] + +let update = + let eq = { eq0 = "foo" ; eq1 = "bar" } in + overwrite_ eq with { eq0 = 1; eq1 = 2 } +[%%expect{| +Line 3, characters 2-41: +3 | overwrite_ eq with { eq0 = 1; eq1 = 2 } + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let update : _ pair @ unique -> _ pair = function eq -> + overwrite_ eq with ("foo", _) +[%%expect{| +Line 2, characters 2-31: +2 | overwrite_ eq with ("foo", _) + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let update : _ pair @ unique -> _ pair = function eq -> + overwrite_ eq with ("foo", 1) +[%%expect{| +Line 2, characters 29-30: +2 | overwrite_ eq with ("foo", 1) + ^ +Error: This expression has type "int" but an expression was expected of type + "string" +|}] + +let update : unit -> _ pair = function eq -> + let eq : string pair = ("foo", "bar") in + overwrite_ eq with (1, _) +[%%expect{| +Line 3, characters 25-26: +3 | overwrite_ eq with (1, _) + ^ +Error: This expression has type "string" but an expression was expected of type + "int" +|}] + +let update : unit -> _ pair = function eq -> + let eq : string pair = ("foo", "bar") in + overwrite_ eq with (1, 2) +[%%expect{| +Line 3, characters 2-27: +3 | overwrite_ eq with (1, 2) + ^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +(*******************************) +(* Mode-checking strong update *) + +type moded_record = { a : (int -> int) option; b : int -> int @@ portable } +[%%expect{| +type moded_record = { a : (int -> int) option; b : int -> int @@ portable; } +|}] + +let update : moded_record @ unique once -> moded_record @ many = + function mr -> + let many_fun : int -> int @@ many = function x -> x in + overwrite_ mr with { a = None; b = many_fun } +[%%expect{| +Line 4, characters 4-49: +4 | overwrite_ mr with { a = None; b = many_fun } + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let update : moded_record @ unique once -> moded_record @ many = + function mr -> + let once_fun : int -> int @@ once = function x -> x in + overwrite_ mr with { a = None; b = once_fun } +[%%expect{| +Line 4, characters 39-47: +4 | overwrite_ mr with { a = None; b = once_fun } + ^^^^^^^^ +Error: This value is "once" but expected to be "many". +|}] + +let update : moded_record @ unique once -> moded_record @ many = + function mr -> + overwrite_ mr with { a = None; b = _ } +[%%expect{| +Line 3, characters 39-40: +3 | overwrite_ mr with { a = None; b = _ } + ^ +Error: This value is "once" but expected to be "many". +|}] + +(* Same as above, but omitting the [b = _]. *) +let update : moded_record @ unique once -> moded_record @ many = + function mr -> + overwrite_ mr with { a = None } +[%%expect{| +Line 3, characters 15-17: +3 | overwrite_ mr with { a = None } + ^^ +Error: This value is "once" but expected to be "many". +|}] + +let update : moded_record @ unique nonportable -> moded_record @ portable = + function mr -> + let portable_fun : int -> int @@ portable = function x -> x in + overwrite_ mr with { a = None; b = portable_fun } +[%%expect{| +Line 4, characters 4-53: +4 | overwrite_ mr with { a = None; b = portable_fun } + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let update : moded_record @ unique nonportable -> moded_record @ portable = + function mr -> + let nonportable_fun : int -> int @@ nonportable = function x -> x in + overwrite_ mr with { a = None; b = nonportable_fun } +[%%expect{| +Line 4, characters 39-54: +4 | overwrite_ mr with { a = None; b = nonportable_fun } + ^^^^^^^^^^^^^^^ +Error: This value is "nonportable" but expected to be "portable". +|}] + +let update : moded_record @ unique nonportable -> moded_record @ portable = + function mr -> + let portable_fun : int -> int @@ portable = function x -> x in + let nonportable_fun : int -> int @@ nonportable = function x -> x in + overwrite_ mr with { a = Some nonportable_fun; b = portable_fun } +[%%expect{| +Line 5, characters 34-49: +5 | overwrite_ mr with { a = Some nonportable_fun; b = portable_fun } + ^^^^^^^^^^^^^^^ +Error: This value is "nonportable" but expected to be "portable". +|}] + +(* This works since the kept field has the portable modality: *) +let update : moded_record @ unique nonportable -> moded_record @ portable = + function mr -> + overwrite_ mr with { a = None; b = _ } +[%%expect{| +Line 3, characters 4-42: +3 | overwrite_ mr with { a = None; b = _ } + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +(* Same as above, but omitting the [b = _]. *) +let update : moded_record @ unique nonportable -> moded_record @ portable = + function mr -> + overwrite_ mr with { a = None } +[%%expect{| +Line 3, characters 4-35: +3 | overwrite_ mr with { a = None } + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +(*****************************************) +(* 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 *) + +type constr = Constr1 of { x : string } | Constr2 of { x : int } + +let update c = + match c with + | Constr1 _ -> overwrite_ c with Constr1 { x = "" } + | Constr2 _ -> overwrite_ c with Constr2 { x = 2 } +[%%expect{| +type constr = Constr1 of { x : string; } | Constr2 of { x : int; } +Line 5, characters 17-53: +5 | | Constr1 _ -> overwrite_ c with Constr1 { x = "" } + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +type nested_record = Nested of { x : int } +[%%expect{| +type nested_record = Nested of { x : int; } +|}] + +let nested_update (t : int * (string * int)) = + overwrite_ t with (3, ("", _)) +[%%expect{| +Line 2, characters 29-30: +2 | overwrite_ t with (3, ("", _)) + ^ +Error: wildcard "_" not expected. +|}] + +let nested_update (t : int * record_update) = + overwrite_ t with (3, {x = _; y = _}) +[%%expect{| +Line 2, characters 29-30: +2 | overwrite_ t with (3, {x = _; y = _}) + ^ +Error: wildcard "_" not expected. +|}] + +let nested_update t = + overwrite_ t with Nested (_) +[%%expect{| +Line 2, characters 20-30: +2 | overwrite_ t with Nested (_) + ^^^^^^^^^^ +Error: This constructor expects an inlined record argument. +|}] + +let update_hole (t : int * (string * int)) = + overwrite_ t with _ +[%%expect{| +Line 2, characters 20-21: +2 | overwrite_ t with _ + ^ +Error: Overwriting is only supported on tuples, constructors and boxed records. +|}] + +(***********************************) +(* Checking that tags don't change *) + +type options = OptionA of string | OptionB of string +type options_record = { x : options } +[%%expect{| +type options = OptionA of string | OptionB of string +type options_record = { x : options; } +|}] + +let id = function + | OptionA s as v -> overwrite_ v with OptionA s + | OptionB s as v -> overwrite_ v with OptionB s +[%%expect{| +Line 2, characters 22-49: +2 | | OptionA s as v -> overwrite_ v with OptionA s + ^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let id v = + match v with + | OptionA s -> overwrite_ v with OptionA s + | OptionB s -> overwrite_ v with OptionB s +[%%expect{| +Line 3, characters 17-44: +3 | | OptionA s -> overwrite_ v with OptionA s + ^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let id v = + match v with + | OptionA _ -> + (match v with + | OptionA s -> overwrite_ v with OptionA s + | OptionB s -> overwrite_ v with OptionB s) + | OptionB s -> overwrite_ v with OptionB s +[%%expect{| +Line 5, characters 20-47: +5 | | OptionA s -> overwrite_ v with OptionA s + ^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let id v = + match v with + | OptionA s -> + (match v with + | OptionA _ -> overwrite_ v with OptionA s + | OptionB _ -> overwrite_ v with OptionA s) + | OptionB s -> overwrite_ v with OptionB s +[%%expect{| +Line 5, characters 20-47: +5 | | OptionA _ -> overwrite_ v with OptionA s + ^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let swap = function + | OptionA s as v -> overwrite_ v with OptionB s + | OptionB s as v -> overwrite_ v with OptionA s +[%%expect{| +Line 3, characters 40-47: +3 | | OptionB s as v -> overwrite_ v with OptionA s + ^^^^^^^ +Error: Overwrite may not change the tag to OptionA. +Hint: The old tag of this allocation is OptionB. +|}] + +let swap v = + match v with + | OptionA s -> overwrite_ v with OptionB s + | OptionB s -> overwrite_ v with OptionA s +[%%expect{| +Line 4, characters 35-42: +4 | | OptionB s -> overwrite_ v with OptionA s + ^^^^^^^ +Error: Overwrite may not change the tag to OptionA. +Hint: The old tag of this allocation is OptionB. +|}] + +let choose_in_branch v = + match v with + | OptionA s -> + if String.equal s "" + then overwrite_ v with OptionA s + else overwrite_ v with OptionB s + | OptionB _ -> v +[%%expect{| +Line 6, characters 29-36: +6 | else overwrite_ v with OptionB s + ^^^^^^^ +Error: Overwrite may not change the tag to OptionB. +Hint: The old tag of this allocation is OptionA. +|}] + +let or_patterns_good = function + | (OptionA "foo" | OptionA "bar") as v -> overwrite_ v with OptionA "baz" + | v -> v +[%%expect{| +Line 2, characters 44-75: +2 | | (OptionA "foo" | OptionA "bar") as v -> overwrite_ v with OptionA "baz" + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let or_patterns_good = function + | ((OptionA "foo" as v) | (OptionA "bar" as v)) -> overwrite_ v with OptionA "baz" + | v -> v +[%%expect{| +Line 2, characters 53-84: +2 | | ((OptionA "foo" as v) | (OptionA "bar" as v)) -> overwrite_ v with OptionA "baz" + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let or_patterns_bad = function + | (OptionA s | OptionB s) as v -> overwrite_ v with OptionA s +[%%expect{| +Line 2, characters 54-61: +2 | | (OptionA s | OptionB s) as v -> overwrite_ v with OptionA s + ^^^^^^^ +Error: Overwrite may not change the tag to OptionA. +Hint: The old tag of this allocation is unknown. +|}] + +let or_patterns_bad = function + | ((OptionA s as v) | (OptionB s as v)) -> overwrite_ v with OptionA s +[%%expect{| +Line 2, characters 63-70: +2 | | ((OptionA s as v) | (OptionB s as v)) -> overwrite_ v with OptionA s + ^^^^^^^ +Error: Overwrite may not change the tag to OptionA. +Hint: The old tag of this allocation is unknown. +|}] + +let or_patterns_bad = function + | ((OptionA _) | _) as v -> overwrite_ v with OptionA "" +[%%expect{| +Line 2, characters 48-55: +2 | | ((OptionA _) | _) as v -> overwrite_ v with OptionA "" + ^^^^^^^ +Error: Overwrite may not change the tag to OptionA. +Hint: The old tag of this allocation is unknown. +|}] + +let or_patterns_bad = function + | ({ x = (OptionA _) as v } | { x = v }) -> overwrite_ v with OptionA "" +[%%expect{| +Line 2, characters 64-71: +2 | | ({ x = (OptionA _) as v } | { x = v }) -> overwrite_ v with OptionA "" + ^^^^^^^ +Error: Overwrite may not change the tag to OptionA. +Hint: The old tag of this allocation is unknown. +|}] + +let is_option_a = function + | OptionA _ -> true + | OptionB _ -> false + +let guards_good = function + | OptionA _ as v -> + begin match Some "" with + | Some s when is_option_a (overwrite_ v with OptionA s) -> true + | _ -> false + end + | OptionB _ -> false +[%%expect{| +val is_option_a : options -> bool @@ global many = +Line 8, characters 30-59: +8 | | Some s when is_option_a (overwrite_ v with OptionA s) -> true + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let guards_bad = function + | OptionA _ as v when is_option_a (overwrite_ v with OptionA "") -> true + | _ -> false +[%%expect{| +Line 2, characters 4-13: +2 | | OptionA _ as v when is_option_a (overwrite_ v with OptionA "") -> true + ^^^^^^^^^ +Error: This value is read from here, but it is already being used as unique: +Line 2, characters 48-49: +2 | | OptionA _ as v when is_option_a (overwrite_ v with OptionA "") -> true + ^ + +|}] + +let nested_path_correct r = + match r with + | { x = OptionA s } -> overwrite_ r.x with OptionA s + | _ -> OptionB "" +[%%expect{| +Line 3, characters 25-54: +3 | | { x = OptionA s } -> overwrite_ r.x with OptionA s + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let nested_path_wrong r = + match r with + | { x = OptionA s } -> overwrite_ r.x with OptionB s + | _ -> OptionB "" +[%%expect{| +Line 3, characters 45-52: +3 | | { x = OptionA s } -> overwrite_ r.x with OptionB s + ^^^^^^^ +Error: Overwrite may not change the tag to OptionB. +Hint: The old tag of this allocation is OptionA. +|}] + +(* Unsupported *) +let let_bound_path = + let r = { x = OptionA "foo" } in + overwrite_ r.x with OptionA "bar" +[%%expect{| +Line 3, characters 22-29: +3 | overwrite_ r.x with OptionA "bar" + ^^^^^^^ +Error: Overwrite may not change the tag to OptionA. +Hint: The old tag of this allocation is unknown. +|}] + +type 'a mutable_record = { mutable m : 'a } + +let mutable_field_aliased r = + let y = OptionA "foo" in + r.m <- y; + (unique_ r), y +[%%expect{| +type 'a mutable_record = { mutable m : 'a; } +val mutable_field_aliased : + options mutable_record @ unique -> options mutable_record * options @@ + global many = +|}] + +let mutable_field_aliased r = + unique_ r.m +[%%expect{| +val mutable_field_aliased : 'a mutable_record @ unique -> 'a @@ global many = + +|}] + +let tag_of_mutable_field r = + match r with + | { m = OptionA s } -> + overwrite_ r.m with OptionA s + | _ -> OptionB "" +[%%expect{| +Line 4, characters 4-33: +4 | overwrite_ r.m with OptionA s + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let mutating_tag_seq r = + match r with + | { m = OptionA s } -> + r.m <- OptionB s; + overwrite_ r.m with OptionA s + | _ -> OptionB "" +[%%expect{| +Line 5, characters 24-31: +5 | overwrite_ r.m with OptionA s + ^^^^^^^ +Error: Overwrite may not change the tag to OptionA. +Hint: The old tag of this allocation was changed through mutation. +|}] + +let mutating_tag_seq_same r = + match r with + | { m = OptionA s } -> + r.m <- OptionA s; + overwrite_ r.m with OptionA s + | _ -> OptionB "" +[%%expect{| +Line 5, characters 24-31: +5 | overwrite_ r.m with OptionA s + ^^^^^^^ +Error: Overwrite may not change the tag to OptionA. +Hint: The old tag of this allocation was changed through mutation. +|}] + +let mutating_tag_seq_parent r = + match r with + | { m = { x = OptionA s } } -> + r.m <- { x = OptionB s }; + overwrite_ r.m.x with OptionA s + | _ -> OptionB "" +[%%expect{| +Line 5, characters 26-33: +5 | overwrite_ r.m.x with OptionA s + ^^^^^^^ +Error: Overwrite may not change the tag to OptionA. +Hint: The old tag of this allocation was changed through mutation. +|}] + +let mutating_tag_par r = + match r with + | { m = OptionA s } -> + (r.m <- OptionB s), overwrite_ r.m with OptionA s + | _ -> (), OptionB "" +[%%expect{| +Line 4, characters 44-51: +4 | (r.m <- OptionB s), overwrite_ r.m with OptionA s + ^^^^^^^ +Error: Overwrite may not change the tag to OptionA. +Hint: The old tag of this allocation is being changed through mutation. +|}] + +let mutating_tag_par_parent r = + match r with + | { m = { x = OptionA s } } -> + (r.m <- { x = OptionB s }), overwrite_ r.m.x with OptionA s + | _ -> (), OptionB "" +[%%expect{| +Line 4, characters 54-61: +4 | (r.m <- { x = OptionB s }), overwrite_ r.m.x with OptionA s + ^^^^^^^ +Error: Overwrite may not change the tag to OptionA. +Hint: The old tag of this allocation is being changed through mutation. +|}] + +let mutating_tag_choice r = + match r with + | { m = OptionA s } -> + if true then (r.m <- OptionB s; r.m) + else overwrite_ r.m with OptionA s + | _ -> OptionB "" +[%%expect{| +Line 5, characters 17-46: +5 | else overwrite_ r.m with OptionA s + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let mutating_tag_choice_parent r = + match r with + | { m = { x = OptionA s } } -> + if true then (r.m <- { x = OptionB s }; r.m.x) + else overwrite_ r.m.x with OptionA s + | _ -> OptionB "" +[%%expect{| +Line 5, characters 9-40: +5 | else overwrite_ r.m.x with OptionA s + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let mutating_tag_choice_seq r = + match r with + | { m = OptionA s } -> + (if true then r.m <- OptionB s else ()); + overwrite_ r.m with OptionA s + | _ -> OptionB "" +[%%expect{| +Line 5, characters 24-31: +5 | overwrite_ r.m with OptionA s + ^^^^^^^ +Error: Overwrite may not change the tag to OptionA. +Hint: The old tag of this allocation was changed through mutation. +|}] + +let mutating_tag_choice_seq_parent r = + match r with + | { m = { x = OptionA s } } -> + (if true then r.m <- { x = OptionB s } else ()); + overwrite_ r.m.x with OptionA s + | _ -> OptionB "" +[%%expect{| +Line 5, characters 26-33: +5 | overwrite_ r.m.x with OptionA s + ^^^^^^^ +Error: Overwrite may not change the tag to OptionA. +Hint: The old tag of this allocation was changed through mutation. +|}] + + +let mutating_tag_rematch r = + match r with + | { m = OptionA s } -> + r.m <- OptionB s; + begin match r with + | { m = OptionB s } -> + overwrite_ r.m with OptionB s + | _ -> OptionB "" + end + | _ -> OptionB "" +[%%expect{| +Line 7, characters 6-35: +7 | overwrite_ r.m with OptionB s + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +(********************************) +(* Overwriting (labeled) tuples *) + +type tuple_unlabeled = string * string +[%%expect{| +type tuple_unlabeled = string * string +|}] + +let update (unique_ r : tuple_unlabeled) : tuple_unlabeled = + let x = overwrite_ r with (_, _) in + x +[%%expect{| +Line 2, characters 10-34: +2 | let x = overwrite_ r with (_, _) in + ^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let update (unique_ r : tuple_unlabeled) : tuple_unlabeled = + let x = overwrite_ r with ("foo", _) in + x +[%%expect{| +Line 2, characters 10-38: +2 | let x = overwrite_ r with ("foo", _) in + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let update (unique_ r : tuple_unlabeled) : tuple_unlabeled = + let x = overwrite_ r with ("foo", "bar") in + x +[%%expect{| +Line 2, characters 10-42: +2 | let x = overwrite_ r with ("foo", "bar") in + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let update (unique_ r : tuple_unlabeled) : tuple_unlabeled = + let x = overwrite_ r with ("foo", "bar", "baz") in +x +[%%expect{| +Line 2, characters 28-49: +2 | let x = overwrite_ r with ("foo", "bar", "baz") in + ^^^^^^^^^^^^^^^^^^^^^ +Error: This expression has type "'a * 'b * 'c" + but an expression was expected of type + "tuple_unlabeled" = "string * string" +|}] + +type tuple_labeled = x:string * y:string +[%%expect{| +type tuple_labeled = x:string * y:string +|}] + +let update (unique_ r : tuple_labeled) : tuple_labeled = + let x = overwrite_ r with (~x:"foo", _) in + x +[%%expect{| +Line 2, characters 28-41: +2 | let x = overwrite_ r with (~x:"foo", _) in + ^^^^^^^^^^^^^ +Error: This expression has type "x:string * 'a" + but an expression was expected of type + "tuple_labeled" = "x:string * y:string" +|}] + +(* CR uniqueness: Would be good to support [~y:_], without the parentheses, if possible *) +let update (unique_ r : tuple_labeled) : tuple_labeled = + let x = overwrite_ r with (~x:(_), ~y:(_)) in + x +[%%expect{| +Line 2, characters 10-44: +2 | let x = overwrite_ r with (~x:(_), ~y:(_)) in + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let update (unique_ r : tuple_labeled) : tuple_labeled = + let x = overwrite_ r with (~x:"foo", ~y:(_)) in + x +[%%expect{| +Line 2, characters 10-46: +2 | let x = overwrite_ r with (~x:"foo", ~y:(_)) in + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let update (unique_ r : tuple_labeled) : tuple_labeled = + let x = overwrite_ r with (~x:"foo", ~y:"bar") in + x +[%%expect{| +Line 2, characters 10-48: +2 | let x = overwrite_ r with (~x:"foo", ~y:"bar") in + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +(***********************************) +(* Syntax to be supported later on *) + +(* CR uniqueness: It would be nice for one of these two pieces of syntax to work. + Currently these are syntax errors. *) + +(* +let update (unique_ r : tuple_labeled) : tuple_labeled = + let x = overwrite_ r with (~x:"foo", ..) in + x +[%%expect{| +|}] + +let update (unique_ r : tuple_labeled) : tuple_labeled = + let x = overwrite_ r with (~x:"foo") in + x +[%%expect{| +|}] +*) + +(*******************************) +(* Overwriting inlined records *) + +type constructor_update = Con of { x : string; y : string } +[%%expect{| +type constructor_update = Con of { x : string; y : string; } +|}] + +(* CR uniqueness: It would be nice if the analysis could figure out the tag + of a constructor_update from its type (which only has one possible tag). *) + +let update = function + | (Con _ as c) -> + let x = overwrite_ c with Con { x = "foo" } in + x +[%%expect{| +Line 3, characters 12-47: +3 | let x = overwrite_ c with Con { x = "foo" } in + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let update = function + | (Con c1 as c) -> + let x = overwrite_ c with Con { c1 with x = "foo" } in + x +[%%expect{| +Line 3, characters 12-55: +3 | let x = overwrite_ c with Con { c1 with x = "foo" } in + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let update = function + | (Con c) -> + let x = overwrite_ c with { x = "foo" } in + x +[%%expect{| +Line 3, characters 23-24: +3 | let x = overwrite_ c with { x = "foo" } in + ^ +Error: This form is not allowed as the type of the inlined record could escape. +|}] + +let update = function + | (Con c) -> + let x = overwrite_ c with { x = "foo" } in + Con x +[%%expect{| +Line 3, characters 23-24: +3 | let x = overwrite_ c with { x = "foo" } in + ^ +Error: This form is not allowed as the type of the inlined record could escape. +|}] + +let update = function + | (Con c) -> + let x = Con (overwrite_ c with { x = "foo" }) in + x +[%%expect{| +Line 3, characters 16-49: +3 | let x = Con (overwrite_ c with { x = "foo" }) in + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let update = function + | (Con c) -> + let x = Con (overwrite_ c with { c with x = "foo" }) in + x +[%%expect{| +Line 3, characters 16-56: +3 | let x = Con (overwrite_ c with { c with x = "foo" }) in + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed |}] diff --git a/testsuite/tests/typing-unique/overwriting_lift_constants.ml b/testsuite/tests/typing-unique/overwriting_lift_constants.ml index 6656e362e87..2018d2ed4af 100644 --- a/testsuite/tests/typing-unique/overwriting_lift_constants.ml +++ b/testsuite/tests/typing-unique/overwriting_lift_constants.ml @@ -77,7 +77,7 @@ val unsafe_dup : '_a @ unique -> '_a * '_a @ unique @@ global many = Line 9, characters 10-66: 9 | let p = overwrite_ p with { dim = 4; x = 1.0; y = 2.0; z = 3.0 } in ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Alert : Overwrite not implemented. +Alert Translcore: Overwrite not implemented. Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed |}] diff --git a/testsuite/tests/typing-unique/overwriting_lift_constants_bug.ml b/testsuite/tests/typing-unique/overwriting_lift_constants_bug.ml index 157227d8183..ae018fed287 100644 --- a/testsuite/tests/typing-unique/overwriting_lift_constants_bug.ml +++ b/testsuite/tests/typing-unique/overwriting_lift_constants_bug.ml @@ -64,7 +64,7 @@ type point = { dim : int; x : float; y : float; z : float; } Line 5, characters 19-48: 5 | if b then p else overwrite_ p with { x = 2.0 } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Alert : Overwrite not implemented. +Alert Translcore: Overwrite not implemented. Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed |}] diff --git a/testsuite/tests/typing-unique/overwriting_map.ml b/testsuite/tests/typing-unique/overwriting_map.ml index 748b359a1cf..1d412c3edd7 100644 --- a/testsuite/tests/typing-unique/overwriting_map.ml +++ b/testsuite/tests/typing-unique/overwriting_map.ml @@ -34,7 +34,7 @@ let () = Line 3, characters 22-57: 3 | | hd :: tl as xs -> overwrite_ xs with f hd :: map f tl ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Alert : Overwrite not implemented. +Alert Translcore: Overwrite not implemented. Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed |}] diff --git a/testsuite/tests/typing-unique/overwriting_proj_push_down_bug.ml b/testsuite/tests/typing-unique/overwriting_proj_push_down_bug.ml index acf1a7a4a12..6fed6b1c85d 100644 --- a/testsuite/tests/typing-unique/overwriting_proj_push_down_bug.ml +++ b/testsuite/tests/typing-unique/overwriting_proj_push_down_bug.ml @@ -328,15 +328,130 @@ let swap_inner (t : tree) = val swap_inner : tree -> tree @@ global many = |}] -(* TODO: Update this test once overwriting is fully implemented. -let swap_inner (t : tree) = - match t with - | Node { l = Node { r = lr } as l; r = Node { l = rl } as r } as t -> - overwrite_ t with - Node { l = overwrite_ l with Node { r = rl; }; - r = overwrite_ r with Node { l = lr; }} - | _ -> t +(* CR uniqueness: Update this test once overwriting is fully implemented. + let swap_inner (t : tree) = + match t with + | Node { l = Node { r = lr } as l; r = Node { l = rl } as r } as t -> + overwrite_ t with + Node { l = overwrite_ l with Node { r = rl; }; + r = overwrite_ r with Node { l = lr; }} + | _ -> t + [%%expect{| + + |}] +*) + +(***********************) +(* Barriers for guards *) + +let match_guard r = + match r with + | { y } when String.equal y "" -> + let r = aliased_use r in + (r, y) + | { y } -> + let r = unique_use r in + (r, y) +[%%expect{| +(let + (unique_use/283 = (apply (field_imm 0 (global Toploop!)) "unique_use") + aliased_use/280 = (apply (field_imm 0 (global Toploop!)) "aliased_use") + match_guard/376 = + (function {nlocal = 0} r/378[(consts ()) (non_consts ([0: *, *]))] + [(consts ()) + (non_consts ([0: [(consts ()) (non_consts ([0: *, *]))], *]))] + (let (y/379 =o (field_mut 1 r/378)) + (if (apply (field_imm 8 (global Stdlib__String!)) y/379 "") + (let + (r/450 =[(consts ()) (non_consts ([0: *, *]))] + (apply aliased_use/280 r/378)) + (makeblock 0 ([(consts ()) (non_consts ([0: *, *]))],*) r/450 + y/379)) + (let + (y/380 =o (field_mut 1 r/378) + r/451 =[(consts ()) (non_consts ([0: *, *]))] + (apply unique_use/283 r/378)) + (makeblock 0 ([(consts ()) (non_consts ([0: *, *]))],*) r/451 + y/380)))))) + (apply (field_imm 1 (global Toploop!)) "match_guard" match_guard/376)) +val match_guard : record @ unique -> record * string @@ global many = +|}] + +let match_guard_unique (unique_ r) = + match r with + | { y } when String.equal ((unique_use r).x) "" -> y + | _ -> "" [%%expect{| +Line 3, characters 4-9: +3 | | { y } when String.equal ((unique_use r).x) "" -> y + ^^^^^ +Error: This value is read from here, but it is already being used as unique: +Line 3, characters 41-42: +3 | | { y } when String.equal ((unique_use r).x) "" -> y + ^ + +|}] + +(********************************************) +(* Global allocations in overwritten fields *) + +type option_record = { x : string option; y : string option } +[%%expect{| +0 +type option_record = { x : string option; y : string option; } +|}] + +let check_heap_alloc_in_overwrite (unique_ r : option_record) = + overwrite_ r with { x = Some "" } +[%%expect{| +Line 2, characters 2-35: +2 | overwrite_ r with { x = Some "" } + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let check_heap_alloc_in_overwrite (local_ unique_ r : option_record) = + overwrite_ r with { x = Some "" } +[%%expect{| +Line 2, characters 2-35: +2 | overwrite_ r with { x = Some "" } + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +(*******************************) +(* Overwrite of mutable fields *) + +type mutable_record = { mutable x : string; y : string } +[%%expect{| +0 +type mutable_record = { mutable x : string; y : string; } +|}] + +let update (unique_ r : mutable_record) = + let x = overwrite_ r with { x = "foo" } in + x.x +[%%expect{| +Line 2, characters 10-41: +2 | let x = overwrite_ r with { x = "foo" } in + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let update (unique_ r : mutable_record) = + let x = overwrite_ r with { y = "foo" } in + x.x +[%%expect{| +Line 2, characters 10-41: +2 | let x = overwrite_ r with { y = "foo" } in + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed |}] -*) diff --git a/testsuite/tests/typing-unique/overwriting_syntax.ml b/testsuite/tests/typing-unique/overwriting_syntax.ml index bae29a0f679..8b2ff6eeb5f 100644 --- a/testsuite/tests/typing-unique/overwriting_syntax.ml +++ b/testsuite/tests/typing-unique/overwriting_syntax.ml @@ -3,6 +3,14 @@ expect; *) +(* CR uniqueness: It would be nice to also support the following syntactic forms: + overwrite_ e with (~x:5, ..) + overwrite_ e with { x = 4; _ } + + This would require us to allow general patterns as the top-level second argument to + overwrite_ with. However, all overwritten fields should continue to be expressions. +*) + (******************) (* Usage examples *) @@ -12,7 +20,7 @@ let overwrite_tuple = function Line 2, characters 17-41: 2 | (a, b) as t -> overwrite_ t with (b, _) ^^^^^^^^^^^^^^^^^^^^^^^^ -Alert : Overwrite not implemented. +Alert Translcore: Overwrite not implemented. Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed |}] @@ -26,18 +34,24 @@ type record = { a : int; b : int; } Line 4, characters 19-53: 4 | { a; b } as t -> overwrite_ t with { b = a; a = _ } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Alert : Overwrite not implemented. +Alert Translcore: Overwrite not implemented. Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed |}] +let with_record = function + { a; b } as t -> { t with b = a } +[%%expect{| +val with_record : record -> record @@ global many = +|}] + let overwrite_record = function { a; b } as t -> overwrite_ t with { b = a } [%%expect{| Line 2, characters 21-48: 2 | { a; b } as t -> overwrite_ t with { b = a } ^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Alert : Overwrite not implemented. +Alert Translcore: Overwrite not implemented. Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed |}] @@ -51,7 +65,7 @@ type constructor = C of { a : int; b : int; } Line 4, characters 21-57: 4 | C { a; b } as t -> overwrite_ t with C { b = a; a = _ } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Alert : Overwrite not implemented. +Alert Translcore: Overwrite not implemented. Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed |}] @@ -62,20 +76,18 @@ let overwrite_constructor = function Line 2, characters 23-52: 2 | C { a; b } as t -> overwrite_ t with C { b = a } ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Alert : Overwrite not implemented. +Alert Translcore: Overwrite not implemented. Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed |}] let overwrite_variant = function - `A (a, b) -> overwrite_ t with `A (b, _) + `A (a, b) as t -> overwrite_ t with `A (b, _) [%%expect{| -Line 2, characters 15-42: -2 | `A (a, b) -> overwrite_ t with `A (b, _) - ^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Alert : Overwrite not implemented. -Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed - +Line 2, characters 38-47: +2 | `A (a, b) as t -> overwrite_ t with `A (b, _) + ^^^^^^^^^ +Error: Overwriting is only supported on tuples, constructors and boxed records. |}] let overwrite_in_match = function @@ -86,7 +98,7 @@ let overwrite_in_match = function Line 3, characters 10-46: 3 | match overwrite_ t with C { b = a; a = _ } with ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Alert : Overwrite not implemented. +Alert Translcore: Overwrite not implemented. Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed |}] @@ -94,52 +106,51 @@ Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Asser (****************) (* Non-examples *) -let underscore () = _ +let underscore = _ [%%expect{| -Line 1, characters 20-21: -1 | let underscore () = _ - ^ -Alert : Overwrite not implemented. -Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed - +Line 1, characters 17-18: +1 | let underscore = _ + ^ +Error: wildcard "_" not expected. |}] -let underscore_tuple () = (_, 1) +let underscore_tuple = (_, 1) [%%expect{| -Line 1, characters 27-28: -1 | let underscore_tuple () = (_, 1) - ^ -Alert : Overwrite not implemented. -Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed - +Line 1, characters 24-25: +1 | let underscore_tuple = (_, 1) + ^ +Error: wildcard "_" not expected. |}] -let underscore_record () = { a = _; b = 1 } +let underscore_record = { a = _; b = 1 } [%%expect{| -Line 1, characters 33-34: -1 | let underscore_record () = { a = _; b = 1 } - ^ -Alert : Overwrite not implemented. -Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed - +Line 1, characters 30-31: +1 | let underscore_record = { a = _; b = 1 } + ^ +Error: wildcard "_" not expected. |}] -let overwrite_with_let t = overwrite_ t with let x = (a, b) in x +let overwrite_with_let t = overwrite_ t with let x = (1, 2) in x [%%expect{| -Line 1, characters 27-64: -1 | let overwrite_with_let t = overwrite_ t with let x = (a, b) in x - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Alert : Overwrite not implemented. -Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed - +Line 1, characters 45-64: +1 | let overwrite_with_let t = overwrite_ t with let x = (1, 2) in x + ^^^^^^^^^^^^^^^^^^^ +Error: Overwriting is only supported on tuples, constructors and boxed records. |}] let overwrite_with_match t = overwrite_ t with match t with C {a;b} -> C{a;b} [%%expect{| -Line 1, characters 29-77: +Line 1, characters 47-77: 1 | let overwrite_with_match t = overwrite_ t with match t with C {a;b} -> C{a;b} - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Alert : Overwrite not implemented. -Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: Overwriting is only supported on tuples, constructors and boxed records. +|}] +let overwrite_with_overwrite = function + { a; b } as t -> overwrite_ t with (overwrite_ t with { b = a }) +[%%expect{| +Line 2, characters 39-68: +2 | { a; b } as t -> overwrite_ t with (overwrite_ t with { b = a }) + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: Overwriting is only supported on tuples, constructors and boxed records. |}] diff --git a/testsuite/tests/typing-unique/overwriting_underscore.ml b/testsuite/tests/typing-unique/overwriting_underscore.ml index b0a9acd8910..01dddf98663 100644 --- a/testsuite/tests/typing-unique/overwriting_underscore.ml +++ b/testsuite/tests/typing-unique/overwriting_underscore.ml @@ -6,12 +6,12 @@ is not enabled and an underscore is detected outside of a pattern. Note, however, that the new implementation errors in the type checker rather than the parser. *) -let underscore () = _ +let underscore = _ [%%expect{| -Line 1, characters 20-21: -1 | let underscore () = _ - ^ -Error: Syntax error: "wildcard "_"" not expected. +Line 1, characters 17-18: +1 | let underscore = _ + ^ +Error: wildcard "_" not expected. |}] let overwriting t = overwrite_ t with (a, b) diff --git a/testsuite/tests/typing-unique/rbtree.ml b/testsuite/tests/typing-unique/rbtree.ml index 3887c9ac83c..dfc4f9ac938 100644 --- a/testsuite/tests/typing-unique/rbtree.ml +++ b/testsuite/tests/typing-unique/rbtree.ml @@ -114,24 +114,30 @@ module Make_Unique_Okasaki(Ord : Map.OrderedType) = struct let fold = fold + let set_color c t = + match t with + | Node _ -> overwrite_ t with Node { color = c } + | Leaf -> assert false + +let set_black = set_color Black +let set_red = set_color Red + (* t is black and its left child is red *) let balance_left t = match t with - | Node t -> - begin match t.left with - | Node { left = Node { color = Red } as ll } as l -> + | Node { left = l } -> + begin match l with + | Node { left = Node { color = Red } as ll; right = lr } -> overwrite_ l with Node { color = Red; left = overwrite_ ll with Node { color = Black }; - right = overwrite_ t with Node { color = Black; left = l.right } } - | Node { right = Node { color = Red } as lr } as l -> + right = overwrite_ t with Node { color = Black; left = lr } } + | Node { right = Node { color = Red; left = lrl; right = lrr } as lr } -> overwrite_ lr with Node { color = Red; - left = overwrite_ l with Node { color = Black; right = lr.left }; - right = overwrite_ t with Node { color = Black; left = lr.right } } - | Node l -> - overwrite_ t with - Node { color = Black; left = overwrite_ l with Node { color = Red } } + left = overwrite_ l with Node { color = Black; right = lrl }; + right = overwrite_ t with Node { color = Black; left = lrr } } + | Node _ -> overwrite_ t with Node { color = Black; left = set_red l } | Leaf -> assert false end | Leaf -> assert false @@ -139,21 +145,19 @@ module Make_Unique_Okasaki(Ord : Map.OrderedType) = struct (* t is black and its right child is red *) let balance_right t = match t with - | Node t -> - begin match t.right with - | Node { right = Node { color = Red } as rr } as r -> + | Node { right = r } -> + begin match r with + | Node { right = Node { color = Red } as rr; left = rl } -> overwrite_ r with Node { color = Red; - left = overwrite_ t with Node { color = Black; right = r.left }; + left = overwrite_ t with Node { color = Black; right = rl }; right = overwrite_ rr with Node { color = Black } } - | Node { left = Node { color = Red } as rl } as r -> + | Node { left = Node { color = Red; left = rll; right = rlr } as rl } as r -> overwrite_ rl with Node { color = Red; - left = overwrite_ t with Node { color = Black; right = rl.left }; - right = overwrite_ r with Node { color = Black; left = rl.right } } - | Node r -> - overwrite_ t with - Node { color = Black; right = overwrite_ r with Node { color = Red } } + left = overwrite_ t with Node { color = Black; right = rll }; + right = overwrite_ r with Node { color = Black; left = rlr } } + | Node _ -> overwrite_ t with Node { color = Black; right = set_red r } | Leaf -> assert false end | Leaf -> assert false @@ -161,24 +165,19 @@ module Make_Unique_Okasaki(Ord : Map.OrderedType) = struct let[@tail_mod_cons] rec ins k v t = match t with | Leaf -> Node { color = Red; left = Leaf; key = k; value = v; right = Leaf } - | Node t -> - match Ord.compare k t.key with + | Node { key; left; right } -> + match Ord.compare k key with | c when c < 0 -> begin - match t.left with + match left with | Node { color = Red } -> - balance_left (overwrite_ t with Node { left = ins k v t.left }) [@nontail] - | _ -> overwrite_ t with Node { left = ins k v t.left } end + balance_left (overwrite_ t with Node { left = ins k v left }) [@nontail] + | _ -> overwrite_ t with Node { left = ins k v left } end | c when c > 0 -> begin - match t.right with + match right with | Node { color = Red } -> - balance_right (overwrite_ t with Node { right = ins k v t.right }) [@nontail] - | _ -> overwrite_ t with Node { right = ins k v t.right } end - | _ (* k == t.key *) -> overwrite_ t with Node { value = v } - - let set_black t = - match t with - | Node _ as t -> overwrite_ t with Node { color = Black } - | Leaf -> assert false + balance_right (overwrite_ t with Node { right = ins k v right }) [@nontail] + | _ -> overwrite_ t with Node { right = ins k v right } end + | _ (* k == key *) -> overwrite_ t with Node { value = v } let insert k v t = set_black (ins k v t) end @@ -232,7 +231,7 @@ module Make_Tagged_Okasaki(Ord : Map.OrderedType) = struct (* t is black and its left child is red *) let balance_left t = match t with - | Node ({ color = Black } as t) -> + | Node { color = Black } as t -> begin match t.left with | Node { color = Red; left = Node { color = Red } as ll } as l -> overwrite_ l with @@ -254,7 +253,7 @@ module Make_Tagged_Okasaki(Ord : Map.OrderedType) = struct (* t is black and its right child is red *) let balance_right t = match t with - | Node ({ color = Black } as t) -> + | Node { color = Black } as t -> begin match t.right with | Node { color = Red; right = Node { color = Red } as rr } as r -> overwrite_ r with @@ -520,12 +519,10 @@ module Make_Okasaki : val insert : Ord.t -> 'a -> (Ord.t, 'a) tree -> (Ord.t, 'a) tree @@ global many end -Lines 114-117, characters 12-88: -114 | ............overwrite_ l with -115 | Node { color = Red; -116 | left = overwrite_ ll with Node { color = Black }; -117 | right = overwrite_ t with Node { color = Black; left = l.right } } -Alert : Overwrite not implemented. +Line 110, characters 16-52: +110 | | Node _ -> overwrite_ t with Node { color = c } + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed |}] diff --git a/testsuite/tests/typing-unique/unique.ml b/testsuite/tests/typing-unique/unique.ml index 69c489b0144..e160a12da46 100644 --- a/testsuite/tests/typing-unique/unique.ml +++ b/testsuite/tests/typing-unique/unique.ml @@ -9,7 +9,7 @@ let dup x = unique_ (x, x) Line 1, characters 24-25: 1 | let dup x = unique_ (x, x) ^ -Error: This value is used here, but it has already been used as unique: +Error: This value is used here, but it is already being used as unique: Line 1, characters 21-22: 1 | let dup x = unique_ (x, x) ^ @@ -29,7 +29,7 @@ Line 1, characters 24-25: 1 | let dup (once_ x) = (x, x) ^ Error: This value is used here, - but it is defined as once and has already been used: + but it is defined as once and is already being used: Line 1, characters 21-22: 1 | let dup (once_ x) = (x, x) ^ @@ -41,7 +41,7 @@ let dup (unique_ x) = (unique_ x, x, x) Line 1, characters 34-35: 1 | let dup (unique_ x) = (unique_ x, x, x) ^ -Error: This value is used here, but it has already been used as unique: +Error: This value is used here, but it is already being used as unique: Line 1, characters 31-32: 1 | let dup (unique_ x) = (unique_ x, x, x) ^ @@ -53,7 +53,7 @@ let dup (unique_ x) = (x, (unique_ x), x) Line 1, characters 26-37: 1 | let dup (unique_ x) = (x, (unique_ x), x) ^^^^^^^^^^^ -Error: This value is used here as unique, but it has already been used: +Error: This value is used here as unique, but it is already being used: Line 1, characters 23-24: 1 | let dup (unique_ x) = (x, (unique_ x), x) ^ @@ -66,7 +66,7 @@ let dup (unique_ x) = ((unique_ x), x) Line 1, characters 36-37: 1 | let dup (unique_ x) = ((unique_ x), x) ^ -Error: This value is used here, but it has already been used as unique: +Error: This value is used here, but it is already being used as unique: Line 1, characters 23-34: 1 | let dup (unique_ x) = ((unique_ x), x) ^^^^^^^^^^^ @@ -90,7 +90,7 @@ Line 4, characters 9-10: 4 | g () @ g () ^ Error: This value is used here, - but it is defined as once and has already been used: + but it is defined as once and is already being used: Line 4, characters 2-3: 4 | g () @ g () ^ @@ -449,7 +449,7 @@ Line 4, characters 13-16: 4 | (bar ~d:3, bar ~d:5) ^^^ Error: This value is used here, - but it is defined as once and has already been used: + but it is defined as once and is already being used: Line 4, characters 3-6: 4 | (bar ~d:3, bar ~d:5) ^^^ @@ -465,7 +465,7 @@ Line 4, characters 35-38: 4 | let baz = bar ~b:4 in (baz ~d:3, baz ~d:5) ^^^ Error: This value is used here, - but it is defined as once and has already been used: + but it is defined as once and is already being used: Line 4, characters 25-28: 4 | let baz = bar ~b:4 in (baz ~d:3, baz ~d:5) ^^^ @@ -481,7 +481,7 @@ Line 4, characters 11-14: 4 | (foo (), foo ()) ^^^ Error: This value is used here, - but it is defined as once and has already been used: + but it is defined as once and is already being used: Line 4, characters 3-6: 4 | (foo (), foo ()) ^^^ @@ -562,7 +562,7 @@ type tree = Leaf | Node of tree * tree Line 5, characters 19-20: 5 | in Node (x, x) ^ -Error: This value is used here, but it has already been used as unique: +Error: This value is used here, but it is already being used as unique: Line 5, characters 16-17: 5 | in Node (x, x) ^ @@ -586,7 +586,7 @@ let f ~(call_pos : [%call_pos]) () = Line 2, characters 21-29: 2 | unique_ (call_pos, call_pos) ^^^^^^^^ -Error: This value is used here, but it has already been used as unique: +Error: This value is used here, but it is already being used as unique: Line 2, characters 11-19: 2 | unique_ (call_pos, call_pos) ^^^^^^^^ @@ -598,7 +598,15 @@ let array_pats (arr : int option array) = | [| o |] -> let _ = unique_id arr in aliased_id o | _ -> None [%%expect{| -val array_pats : int option array @ unique -> int option = +Line 3, characters 51-52: +3 | | [| o |] -> let _ = unique_id arr in aliased_id o + ^ +Error: This value is used here, + but it is part of a value that has already been used as unique: +Line 3, characters 33-36: +3 | | [| o |] -> let _ = unique_id arr in aliased_id o + ^^^ + |}] let array_pats (arr : int option iarray) = @@ -616,3 +624,10 @@ Line 3, characters 33-36: ^^^ |}] + +(* Shadowing of unique variables *) +let shadow x = + x, (let x = (1, 2) in x) +[%%expect{| +val shadow : 'a -> 'a * (int * int) = +|}] diff --git a/testsuite/tests/typing-unique/unique_analysis.ml b/testsuite/tests/typing-unique/unique_analysis.ml index 5637afe3f83..e7a803d2c10 100644 --- a/testsuite/tests/typing-unique/unique_analysis.ml +++ b/testsuite/tests/typing-unique/unique_analysis.ml @@ -59,7 +59,7 @@ let sequence (unique_ x) = unique_ let y = x in (x, y) Line 1, characters 52-53: 1 | let sequence (unique_ x) = unique_ let y = x in (x, y) ^ -Error: This value is used here, but it has already been used as unique: +Error: This value is used here, but it is already being used as unique: Line 1, characters 49-50: 1 | let sequence (unique_ x) = unique_ let y = x in (x, y) ^ @@ -124,7 +124,7 @@ Line 4, characters 35-37: 4 | | x :: xs as gs -> (unique_ gs), xs ^^ Error: This value is used here, - but it is part of a value that has already been used as unique: + but it is part of a value that is already being used as unique: Line 4, characters 21-33: 4 | | x :: xs as gs -> (unique_ gs), xs ^^^^^^^^^^^^ @@ -140,7 +140,7 @@ Line 4, characters 25-35: 4 | | x :: xs as gs -> gs, unique_ xs ^^^^^^^^^^ Error: This value is used here as unique, - but it is part of a value that has already been used: + but it is part of a value that is already being used: Line 4, characters 21-23: 4 | | x :: xs as gs -> gs, unique_ xs ^^ @@ -155,7 +155,7 @@ Line 4, characters 35-37: 4 | | x :: xs as gs -> (unique_ xs), gs ^^ Error: This value is used here, - but part of it has already been used as unique: + but part of it is already being used as unique: Line 4, characters 21-33: 4 | | x :: xs as gs -> (unique_ xs), gs ^^^^^^^^^^^^ @@ -170,7 +170,7 @@ Line 4, characters 25-35: 4 | | x :: xs as gs -> xs, unique_ gs ^^^^^^^^^^ Error: This value is used here as unique, - but part of it has already been used: + but part of it is already being used: Line 4, characters 21-23: 4 | | x :: xs as gs -> xs, unique_ gs ^^ @@ -382,7 +382,7 @@ Line 3, characters 31-32: 3 | | (a, b) as t -> unique_ (a, t) ^ Error: This value is used here, - but part of it has already been used as unique: + but part of it is already being used as unique: Line 3, characters 28-29: 3 | | (a, b) as t -> unique_ (a, t) ^ @@ -397,7 +397,7 @@ Line 3, characters 36-37: 3 | | ((_, a), b) as t -> unique_ (a, t) ^ Error: This value is used here, - but part of it has already been used as unique: + but part of it is already being used as unique: Line 3, characters 33-34: 3 | | ((_, a), b) as t -> unique_ (a, t) ^ @@ -412,7 +412,7 @@ let or_patterns6 flag f x y = Line 3, characters 66-67: 3 | | true, a, (_, b) | false, b, (_, a) -> (unique_id a, unique_id b) ^ -Error: This value is used here, but it has already been used as unique: +Error: This value is used here, but it is already being used as unique: Line 3, characters 53-54: 3 | | true, a, (_, b) | false, b, (_, a) -> (unique_id a, unique_id b) ^ diff --git a/tools/debug_printers.ml b/tools/debug_printers.ml index 747df9dfae4..259c0c95fd1 100644 --- a/tools/debug_printers.ml +++ b/tools/debug_printers.ml @@ -7,3 +7,13 @@ let sort = Jkind.Sort.Debug_printers.t let sort_var = Jkind.Sort.Debug_printers.var let jkind = Jkind.Debug_printers.t let zero_alloc_var = Zero_alloc.debug_printer +let maybe_unique = Uniqueness_analysis.Maybe_unique.print +let maybe_aliased = Uniqueness_analysis.Maybe_aliased.print +let aliased = Uniqueness_analysis.Aliased.print +let tag = Uniqueness_analysis.Tag.print +let projection = Uniqueness_analysis.Projection.print +let usage_tree = Uniqueness_analysis.Usage_tree.print +let usage_forest = Uniqueness_analysis.Usage_forest.print +let paths = Uniqueness_analysis.Paths.print +let value = Uniqueness_analysis.Value.print +let ienv = Uniqueness_analysis.Ienv.print diff --git a/typing/ident.mli b/typing/ident.mli index dddbf68a60b..77c61b955de 100644 --- a/typing/ident.mli +++ b/typing/ident.mli @@ -24,6 +24,7 @@ include Identifiable.S with type t := t - [compare] compares identifiers by binding location *) +val print : Format.formatter -> t -> unit val print_with_scope : Format.formatter -> t -> unit (** Same as {!print} except that it will also add a "[n]" suffix if the scope of the argument is [n]. *) diff --git a/typing/printtyped.ml b/typing/printtyped.ml index 6e26099cd2f..6ec363c6dd6 100644 --- a/typing/printtyped.ml +++ b/typing/printtyped.ml @@ -626,7 +626,13 @@ and expression i ppf x = line i ppf "Texp_exclave"; expression i ppf e; | Texp_src_pos -> - line i ppf "Texp_src_pos" + line i ppf "Texp_src_pos" + | Texp_overwrite (e1, e2) -> + line i ppf "Texp_overwrite\n"; + expression i ppf e1; + expression i ppf e2 + | Texp_hole _ -> + line i ppf "Texp_hole" and value_description i ppf x = line i ppf "value_description %a %a\n" fmt_ident x.val_id fmt_location diff --git a/typing/tast_iterator.ml b/typing/tast_iterator.ml index e146df9b681..325d394905a 100644 --- a/typing/tast_iterator.ml +++ b/typing/tast_iterator.ml @@ -427,6 +427,10 @@ let expr sub {exp_loc; exp_extra; exp_desc; exp_env; exp_attributes; _} = | Texp_probe_is_enabled _ -> () | Texp_exclave exp -> sub.expr sub exp | Texp_src_pos -> () + | Texp_overwrite(exp1, exp2) -> + sub.expr sub exp1; + sub.expr sub exp2 + | Texp_hole _ -> () let package_type sub {pack_fields; pack_txt; _} = diff --git a/typing/tast_mapper.ml b/typing/tast_mapper.ml index 9eb5c868526..871c62be8fa 100644 --- a/typing/tast_mapper.ml +++ b/typing/tast_mapper.ml @@ -602,6 +602,9 @@ let expr sub x = | Texp_exclave exp -> Texp_exclave (sub.expr sub exp) | Texp_src_pos -> Texp_src_pos + | Texp_overwrite (exp1, exp2) -> + Texp_overwrite (sub.expr sub exp1, sub.expr sub exp2) + | Texp_hole use -> Texp_hole use in let exp_attributes = sub.attributes sub x.exp_attributes in {x with exp_loc; exp_extra; exp_desc; exp_env; exp_attributes} diff --git a/typing/typecore.ml b/typing/typecore.ml index 82e0ab1951d..775bb4818a9 100644 --- a/typing/typecore.ml +++ b/typing/typecore.ml @@ -26,7 +26,6 @@ open Mode open Typedtree open Btype open Ctype -open Uniqueness_analysis type comprehension_type = | List_comprehension @@ -263,6 +262,8 @@ type error = | Unsupported_stack_allocation of unsupported_stack_allocation | Not_allocation | Impossible_function_jkind of type_expr * jkind_lr + | Overwrite_of_invalid_term + | Unexpected_hole exception Error of Location.t * Env.t * error exception Error_forward of Location.error @@ -676,6 +677,49 @@ let optimise_allocations () = !allocations; reset_allocations () +(** 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 *) + | Assigning of + Types.type_expr * (* type of expression *) + Value.l (* mode of kept fields *) + +(** A version of [overwrite] for passing to [type_label_exp], which requires + the type of the *record* and the mode of the *label*. *) +type label_overwrite = + | No_overwrite_label + | Overwrite_label of + Types.type_expr * (* the type of the record *) + Value.l (* the mode of the label expression, already accounting + for modalities *) + +let assign_children ~no n f = function + | No_overwrite + | Assigning _ (* this is actually a type error, but it's caught elsewhere *) + -> List.init n (fun _ -> no) + | Overwriting(loc, typ, mode) -> f loc typ mode + +let assign_label_children = assign_children ~no:No_overwrite_label + +let assign_children = assign_children ~no:No_overwrite + +let rec can_be_overwritten = function + | Pexp_constraint (e, _, _) -> can_be_overwritten e.pexp_desc + | (Pexp_tuple _ | Pexp_construct _ | Pexp_record _) -> true + | _ -> false + (* Typing of constants *) let type_constant: Typedtree.constant -> type_expr = function @@ -927,13 +971,13 @@ let apply_mode_annots ~loc ~env (m : Alloc.Const.Option.t) mode = | Error e -> error (Right_le_left, e)) (** 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 - m0 |> Const.alloc_as_value |> Value.of_const +(* CR uniqueness: change back to old implementation *) +let mutable_mode _m0 rmode = + rmode + |> Value.meet_with (Comonadic Areality) (Regionality.Const.legacy) + |> Value.meet_with (Comonadic Linearity) (Linearity.Const.legacy) + |> Value.meet_with (Comonadic Portability) (Portability.Const.legacy) + |> Value.join_with (Monadic Contention) (Contention.Const.legacy) (** Takes the mutability on a field, and expected mode of the record (adjusted for allocation), check that the construction would be allowed. *) @@ -941,7 +985,7 @@ let check_construct_mutability ~loc ~env mutability argument_mode = match mutability with | Immutable -> () | Mutable m0 -> - let m0 = mutable_mode m0 in + let m0 = mutable_mode m0 (Value.newvar ()) in submode ~loc ~env m0 argument_mode (** The [expected_mode] of the record when projecting a mutable field. *) @@ -4044,6 +4088,14 @@ let rec is_nonexpansive exp = | Texp_extension_constructor _ -> false | Texp_exclave e -> is_nonexpansive e + (* The underlying mutation of exp1 can not be observed since we have the only reference + to it. In fact, a completely valid model for Texp_overwrite would be to ignore exp1 + and just allocate a new cell for exp2: *) + | Texp_overwrite (exp1, exp2) -> + is_nonexpansive exp1 && is_nonexpansive exp2 + (* Texp_hole can always be replaced by a field read from the old allocation, + which is non-expansive: *) + | Texp_hole _ -> true and is_nonexpansive_mod mexp = match mexp.mod_desc with @@ -4465,6 +4517,7 @@ let check_partial_application ~statement exp = | Texp_ident _ | Texp_constant _ | Texp_tuple _ | Texp_unboxed_tuple _ | Texp_construct _ | Texp_variant _ | Texp_record _ + | Texp_overwrite _ | Texp_hole _ | Texp_field _ | Texp_setfield _ | Texp_array _ | Texp_list_comprehension _ | Texp_array_comprehension _ | Texp_while _ | Texp_for _ | Texp_instvar _ @@ -5122,9 +5175,9 @@ let add_zero_alloc_attribute expr attributes = end | _ -> expr -let rec type_exp ?recarg env expected_mode sexp = +let rec type_exp ?recarg ?(overwrite=No_overwrite) env expected_mode sexp = (* We now delegate everything to type_expect *) - type_expect ?recarg env expected_mode sexp + type_expect ?recarg ~overwrite env expected_mode sexp (mk_expected (newvar (Jkind.Builtin.any ~why:Dummy_jkind))) (* Typing of an expression with an expected type. @@ -5134,13 +5187,13 @@ let rec type_exp ?recarg env expected_mode sexp = at [generic_level] (but its variables no higher than [!current_level]). *) -and type_expect ?recarg env +and type_expect ?recarg ?(overwrite=No_overwrite) env (expected_mode : expected_mode) sexp ty_expected_explained = let previous_saved_types = Cmt_format.get_saved_types () in let exp = Builtin_attributes.warning_scope sexp.pexp_attributes (fun () -> - type_expect_ ?recarg env expected_mode sexp ty_expected_explained + type_expect_ ?recarg ~overwrite env expected_mode sexp ty_expected_explained ) in Cmt_format.set_saved_types @@ -5148,7 +5201,7 @@ and type_expect ?recarg env exp and type_expect_ - ?(recarg=Rejected) + ?(recarg=Rejected) ?(overwrite=No_overwrite) env (expected_mode : expected_mode) sexp ty_expected_explained = let { ty = ty_expected; explanation } = ty_expected_explained in let loc = sexp.pexp_loc in @@ -5505,13 +5558,13 @@ and type_expect_ exp_attributes = sexp.pexp_attributes; exp_env = env } | Pexp_tuple sexpl -> - type_tuple ~loc ~env ~expected_mode ~ty_expected ~explanation + type_tuple ~overwrite ~loc ~env ~expected_mode ~ty_expected ~explanation ~attributes:sexp.pexp_attributes sexpl | Pexp_unboxed_tuple sexpl -> type_unboxed_tuple ~loc ~env ~expected_mode ~ty_expected ~explanation ~attributes:sexp.pexp_attributes sexpl | Pexp_construct(lid, sarg) -> - type_construct env expected_mode loc lid + type_construct ~overwrite env expected_mode loc lid sarg ty_expected_explained sexp.pexp_attributes | Pexp_variant(l, sarg) -> (* Keep sharing *) @@ -5528,7 +5581,9 @@ and type_expect_ with Rpresent (Some ty), Rpresent (Some ty0) -> let alloc_mode, argument_mode = register_allocation expected_mode in - let arg = type_argument env argument_mode sarg ty ty0 in + let arg = + type_argument ~overwrite:No_overwrite env argument_mode sarg ty ty0 + in re { exp_desc = Texp_variant(l, Some (arg, alloc_mode)); exp_loc = loc; exp_extra = []; exp_type = ty_expected0; @@ -5570,7 +5625,7 @@ and type_expect_ assert (lid_sexp_list <> []); let opt_exp = match opt_sexp with - None -> None + | None -> None | Some sexp -> let exp, mode = with_local_level_if_principal begin fun () -> @@ -5582,26 +5637,28 @@ and type_expect_ Some (exp, mode) in let ty_record, expected_type = - let expected_opath = - match extract_concrete_record env ty_expected with - | Record_type (p0, p, _, _) -> Some (p0, p, is_principal ty_expected) + let extract_record loc ty error = + match extract_concrete_record env ty with + | Record_type (p0, p, _, _) -> Some (p0, p, is_principal ty) | Maybe_a_record_type -> None | Not_a_record_type -> - let error = - Wrong_expected_kind(Record, Expression explanation, ty_expected) - in raise (Error (loc, env, error)) in + let expected_opath = + extract_record loc ty_expected + (Wrong_expected_kind(Record, Expression explanation, ty_expected)) + in let opt_exp_opath = match opt_exp with - | None -> None + | None -> + begin match overwrite with + | Overwriting (loc, ty, _) -> + extract_record loc ty (Expr_not_a_record_type ty) + | (No_overwrite | Assigning _) -> None + end | Some (exp, _) -> - match extract_concrete_record env exp.exp_type with - | Record_type (p0, p, _, _) -> Some (p0, p, is_principal exp.exp_type) - | Maybe_a_record_type -> None - | Not_a_record_type -> - let error = Expr_not_a_record_type exp.exp_type in - raise (Error (exp.exp_loc, env, error)) + extract_record exp.exp_loc exp.exp_type + (Expr_not_a_record_type exp.exp_type) in match expected_opath, opt_exp_opath with | None, None -> @@ -5616,31 +5673,49 @@ and type_expect_ in ty, opt_exp_opath in - let closed = (opt_sexp = None) in + let closed = (opt_sexp = None && overwrite = No_overwrite) in let lbl_a_list = wrap_disambiguate "This record expression is expected to have" (mk_expected ty_record) (disambiguate_sort_lid_a_list loc closed env Env.Construct expected_type) lid_sexp_list in + let is_unboxed = + List.exists + (fun (_, {lbl_repres; _}, _) -> + match lbl_repres with + | Record_unboxed | Record_inlined (_, _, Variant_unboxed) -> true + | _ -> false) + lbl_a_list + in + begin match overwrite with + | (No_overwrite | Assigning _) -> () + | Overwriting _ -> + if is_unboxed then + raise (Error (loc, env, Overwrite_of_invalid_term)); + end; let alloc_mode, argument_mode = - if List.exists - (fun (_, {lbl_repres; _}, _) -> - match lbl_repres with - | Record_unboxed | Record_inlined (_, _, Variant_unboxed) -> false - | _ -> true) - lbl_a_list then + if not is_unboxed then let alloc_mode, argument_mode = register_allocation expected_mode in Some alloc_mode, argument_mode else None, expected_mode in - let type_label_exp ((_, label, _) as x) = + let type_label_exp overwrite ((_, label, _) as x) = check_construct_mutability ~loc ~env label.lbl_mut argument_mode; let argument_mode = mode_modality label.lbl_modalities 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 + type_label_exp ~overwrite true env argument_mode loc ty_record x + in + let overwrites = + assign_label_children (List.length lbl_a_list) + (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 + Overwrite_label(ty, mode)) + lbl_a_list) + overwrite + in + let lbl_exp_list = List.map2 type_label_exp overwrites lbl_a_list in with_explanation (fun () -> unify_exp_types loc env (instance ty_record) (instance ty_expected)); (* note: check_duplicates would better be implemented in @@ -5660,8 +5735,32 @@ and type_expect_ (fun (_, lbl',_) -> lbl'.lbl_num = lbl.lbl_num) lbl_exp_list in - match opt_exp with - None -> + let unify_kept record_loc extended_expr_loc ty_exp mode lbl = + let _, ty_arg1, ty_res1 = instance_label ~fixed:false lbl in + unify_exp_types extended_expr_loc env ty_exp ty_res1; + match matching_label lbl with + | lid, _lbl, lbl_exp -> + (* do not connect result types for overridden labels *) + Overridden (lid, lbl_exp) + | exception Not_found -> begin + let _, ty_arg2, ty_res2 = instance_label ~fixed:false lbl in + unify_exp_types record_loc env ty_arg1 ty_arg2; + with_explanation (fun () -> + unify_exp_types record_loc env (instance ty_expected) ty_res2); + check_project_mutability ~loc:extended_expr_loc ~env lbl.lbl_mut mode; + let mode = Modality.Value.Const.apply lbl.lbl_modalities mode in + check_construct_mutability ~loc:record_loc ~env lbl.lbl_mut argument_mode; + let argument_mode = + mode_modality lbl.lbl_modalities argument_mode + in + submode ~loc:extended_expr_loc ~env mode argument_mode; + Kept (ty_arg1, lbl.lbl_mut, + unique_use ~loc:record_loc ~env mode + (as_single_mode argument_mode)) + end + in + match opt_exp, overwrite with + None, (No_overwrite | Assigning _) -> let label_definitions = Array.map (fun lbl -> match matching_label lbl with @@ -5684,33 +5783,17 @@ and type_expect_ lbl.lbl_all in None, label_definitions - | Some (exp, mode) -> + | 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 + | Some (exp, mode), _ -> let ty_exp = instance exp.exp_type in - let unify_kept lbl = - let _, ty_arg1, ty_res1 = instance_label ~fixed:false lbl in - unify_exp_types exp.exp_loc env ty_exp ty_res1; - match matching_label lbl with - | lid, _lbl, lbl_exp -> - (* do not connect result types for overridden labels *) - Overridden (lid, lbl_exp) - | exception Not_found -> begin - let _, ty_arg2, ty_res2 = instance_label ~fixed:false lbl in - unify_exp_types loc env ty_arg1 ty_arg2; - with_explanation (fun () -> - unify_exp_types loc env (instance ty_expected) ty_res2); - check_project_mutability ~loc:exp.exp_loc ~env lbl.lbl_mut mode; - let mode = Modality.Value.Const.apply lbl.lbl_modalities mode in - check_construct_mutability ~loc ~env lbl.lbl_mut argument_mode; - let argument_mode = - mode_modality lbl.lbl_modalities argument_mode - in - submode ~loc ~env mode argument_mode; - Kept (ty_arg1, lbl.lbl_mut, - unique_use ~loc ~env mode - (as_single_mode argument_mode)) - end + let label_definitions = + Array.map (unify_kept loc exp.exp_loc ty_exp mode) lbl.lbl_all in - let label_definitions = Array.map unify_kept lbl.lbl_all in let ubr = Unique_barrier.not_computed () in Some ({exp with exp_type = ty_exp}, ubr), label_definitions in @@ -5798,9 +5881,10 @@ and type_expect_ match label.lbl_mut with | Mutable m0 -> submode ~loc:record.exp_loc ~env rmode mode_mutate_mutable; - let mode = mutable_mode m0 |> mode_default in + let mode = mutable_mode m0 rmode |> mode_default in let mode = mode_modality label.lbl_modalities mode in - type_label_exp false env mode loc ty_record (lid, label, snewval) + type_label_exp ~overwrite:No_overwrite_label false env mode loc ty_record + (lid, label, snewval) | Immutable -> raise(Error(loc, env, Label_not_mutable lid.txt)) in @@ -5945,7 +6029,7 @@ and type_expect_ Builtin_attributes.error_message_attr sexp.pexp_attributes in let explanation = Option.map (fun msg -> Error_message_attr msg) error_message_attr_opt in - let arg = type_argument ?explanation env expected_mode sarg ty (instance ty) in + let arg = type_argument ~overwrite ?explanation env expected_mode sarg ty (instance ty) in rue { exp_desc = arg.exp_desc; exp_loc = arg.exp_loc; @@ -6507,15 +6591,68 @@ and type_expect_ ~ty_expected ~attributes:sexp.pexp_attributes comp - | Pexp_overwrite (_x, _e) -> + | Pexp_overwrite (exp1, exp2) -> if not (Language_extension.is_enabled Overwriting) then - raise (Typetexp.Error (loc, env, - Unsupported_extension Overwriting)) - else Location.todo_overwrite_not_implemented loc + raise (Typetexp.Error (loc, env, Unsupported_extension Overwriting)); + if not (can_be_overwritten exp2.pexp_desc) then + raise (Error (exp2.pexp_loc, env, Overwrite_of_invalid_term)); + let cell_mode, _ = + (* The overwritten cell has to be unique + and should have the areality expected here: *) + Value.newvar_below + (Value.meet_with (Monadic Uniqueness) Uniqueness.Const.Unique + (Value.max_with (Comonadic Areality) + (Value.proj (Comonadic Areality) expected_mode.mode))) + in + let cell_type = + (* CR uniqueness: this could be the jkind of exp2 *) + mk_expected (newvar (Jkind.Builtin.value ~why:Boxed_record)) + in + let exp1 = type_expect ~recarg env (mode_default cell_mode) exp1 cell_type in + let exp2 = + (* The newly-written fields have to be global to avoid heap-to-stack pointers. + We enforce that here, by asking the allocation to be global. + This makes the block alloc_heap, but we ignore that information anyway. *) + let exp2_mode = + mode_coerce + (Value.max_with (Comonadic Areality) Regionality.global) + expected_mode + in + (* When typing holes, we will enforce: fields_mode <= expected_mode. + But since we set the expected_mode to be global above, this would make + all holes global and thus prevent us from keeping any old values as holes + if the cell is local! However, it is sound for kept fields to be local, + since they don't involve a write and can't create heap-to-stack pointers. + And we have also checked above that for regionality cell_mode <= expected_mode. + Therefore, we can safely ignore regionality when checking the mode of holes. *) + let fields_mode = + Value.meet_with (Comonadic Areality) Regionality.Const.Global cell_mode + |> Value.disallow_right + in + let overwrite = + Overwriting (exp1.exp_loc, exp1.exp_type, fields_mode) + in + type_expect ~recarg ~overwrite env exp2_mode exp2 ty_expected_explained + in + re { exp_desc = Texp_overwrite(exp1, exp2); + exp_loc = loc; exp_extra = []; + exp_type = exp2.exp_type; + exp_attributes = sexp.pexp_attributes; + exp_env = env } | Pexp_hole -> - if not (Language_extension.is_enabled Overwriting) then - raise Syntaxerr.(Error(Not_expecting(loc, "wildcard \"_\""))) - else Location.todo_overwrite_not_implemented loc + begin match overwrite with + | 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; + let use = unique_use ~loc ~env fields_mode expected_mode.mode in + { exp_desc = Texp_hole use; + exp_loc = loc; exp_extra = []; + exp_type = ty_expected_explained.ty; + exp_attributes = sexp.pexp_attributes; + exp_env = env } + | _ -> raise (Error (loc, env, Unexpected_hole)); + end and expression_constraint pexp = { type_without_constraint = (fun env expected_mode -> @@ -6523,7 +6660,7 @@ and expression_constraint pexp = expr, expr.exp_type); type_with_constraint = (fun env expected_mode ty -> - type_argument env expected_mode pexp ty (instance ty)); + type_argument ~overwrite:No_overwrite env expected_mode pexp ty (instance ty)); is_self = (fun expr -> match expr.exp_desc with @@ -7315,7 +7452,7 @@ and type_option_some env expected_mode sarg ty ty0 = let ty' = extract_option_type env ty in let ty0' = extract_option_type env ty0 in let alloc_mode, argument_mode = register_allocation expected_mode in - let arg = type_argument env argument_mode sarg ty' ty0' in + let arg = type_argument ~overwrite:No_overwrite env argument_mode sarg ty' ty0' in let lid = Longident.Lident "Some" in let csome = Env.find_ident_constructor Predef.ident_some env in mkexp (Texp_construct(mknoloc lid , csome, [arg], Some alloc_mode)) @@ -7323,7 +7460,7 @@ and type_option_some env expected_mode sarg ty ty0 = (* [expected_mode] is the expected mode of the field. It's already adjusted for allocation, mutation and modalities. *) -and type_label_exp create env (arg_mode : expected_mode) loc ty_expected +and type_label_exp ~overwrite create env (arg_mode : expected_mode) loc ty_expected (lid, label, sarg) = (* Here also ty_expected may be at generic_level *) let separate = !Clflags.principal || Env.has_local_constraints env in @@ -7334,7 +7471,7 @@ and type_label_exp create env (arg_mode : expected_mode) loc ty_expected let (vars, ty_arg, snap, arg) = (* try the first approach *) with_local_level begin fun () -> - let (vars, ty_arg) = + let unify_as_label ty_expected = with_local_level_iter_if separate begin fun () -> let (vars, ty_arg, ty_res) = with_local_level_iter_if separate ~post:generalize_structure @@ -7355,13 +7492,22 @@ and type_label_exp create env (arg_mode : expected_mode) loc ty_expected end ~post:generalize_structure in + let (vars, ty_arg) = unify_as_label ty_expected in if label.lbl_private = Private then if create then raise (Error(loc, env, Private_type ty_expected)) else raise (Error(lid.loc, env, Private_label(lid.txt, ty_expected))); let snap = if vars = [] then None else Some (Btype.snapshot ()) in - let arg = type_argument env arg_mode sarg ty_arg (instance ty_arg) in + let overwrite = + match overwrite with + | No_overwrite_label -> No_overwrite + | Overwrite_label(ty, mode) -> + (* mode is correct already, like [arg_mode] *) + 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) end (* Note: there is no generalization logic here as could be expected, @@ -7381,7 +7527,9 @@ and type_label_exp create env (arg_mode : expected_mode) loc ty_expected with first_try_exn when maybe_expansive arg -> try (* backtrack and try the second approach *) Option.iter Btype.backtrack snap; - let arg = with_local_level (fun () -> type_exp env arg_mode sarg) + let arg = + with_local_level + (fun () -> type_exp ~overwrite:No_overwrite env arg_mode sarg) ~post:(fun arg -> lower_contravariant env arg.exp_type) in let arg = @@ -7400,7 +7548,7 @@ and type_label_exp create env (arg_mode : expected_mode) loc ty_expected in (lid, label, arg) -and type_argument ?explanation ?recarg env (mode : expected_mode) sarg +and type_argument ?explanation ?recarg ~overwrite env (mode : expected_mode) sarg ty_expected' ty_expected = (* ty_expected' may be generic *) let no_labels ty = @@ -7471,7 +7619,7 @@ and type_argument ?explanation ?recarg env (mode : expected_mode) sarg |> mode_morph (fun _mode -> exp_mode) |> expect_mode_cross env ty_expected' in - type_exp env expected_mode sarg) + type_exp ~overwrite env expected_mode sarg) in let rec make_args args ty_fun = match get_desc (expand_head env ty_fun) with @@ -7608,7 +7756,7 @@ and type_argument ?explanation ?recarg env (mode : expected_mode) sarg end | None -> let mode = expect_mode_cross env ty_expected' mode in - let texp = type_expect ?recarg env mode sarg + let texp = type_expect ?recarg ~overwrite env mode sarg (mk_expected ?explanation ty_expected') in unify_exp env texp ty_expected; texp @@ -7637,7 +7785,7 @@ and type_apply_arg env ~app_loc ~funct ~index ~position_and_mode ~partial_app (l if wrapped_in_some then begin type_option_some env expected_mode sarg ty_arg' ty_arg0' end else begin - type_argument env expected_mode sarg ty_arg' ty_arg0' + type_argument ~overwrite:No_overwrite env expected_mode sarg ty_arg' ty_arg0' end end else begin if !Clflags.principal @@ -7669,7 +7817,7 @@ and type_apply_arg env ~app_loc ~funct ~index ~position_and_mode ~partial_app (l let vars0, ty_arg0' = instance_poly ~fixed:false vars0 ty_arg0' in List.iter2 (fun ty ty' -> unify_var env ty ty') vars vars0; let arg = - type_argument env expected_mode sarg ty_arg' ty_arg0' + type_argument ~overwrite:No_overwrite env expected_mode sarg ty_arg' ty_arg0' in arg, ty_arg, vars end @@ -7787,7 +7935,7 @@ and type_application env app_loc expected_mode position_and_mode check_tail_call_local_returning app_loc env ap_mode position_and_mode; args, ty_ret, ap_mode, position_and_mode -and type_tuple ~loc ~env ~(expected_mode : expected_mode) ~ty_expected +and type_tuple ~overwrite ~loc ~env ~(expected_mode : expected_mode) ~ty_expected ~explanation ~attributes sexpl = (* CR layouts v5: consider sharing code with [type_unboxed_tuple] below when we allow non-values in boxed tuples. *) @@ -7799,14 +7947,18 @@ and type_tuple ~loc ~env ~(expected_mode : expected_mode) ~ty_expected locality_context = expected_mode.locality_context } in (* CR layouts v5: non-values in tuples *) - let labeled_subtypes = - List.map (fun (label, _) -> label, - newgenvar (Jkind.Builtin.value_or_null ~why:Tuple_element)) - sexpl + let unify_as_tuple ty_expected = + let labeled_subtypes = + List.map (fun (label, _) -> label, + newgenvar (Jkind.Builtin.value_or_null ~why:Tuple_element)) + sexpl + in + let to_unify = newgenty (Ttuple labeled_subtypes) in + with_explanation explanation (fun () -> + unify_exp_types loc env to_unify (generic_instance ty_expected)); + labeled_subtypes in - let to_unify = newgenty (Ttuple labeled_subtypes) in - with_explanation explanation (fun () -> - unify_exp_types loc env to_unify (generic_instance ty_expected)); + let labeled_subtypes = unify_as_tuple ty_expected in let argument_modes = match expected_mode.tuple_modes with (* CR zqian: improve the modes of opened labeled tuple pattern. *) @@ -7825,16 +7977,24 @@ and type_tuple ~loc ~env ~(expected_mode : expected_mode) ~ty_expected List.init arity (fun _ -> argument_mode) in let types_and_modes = List.combine labeled_subtypes argument_modes in + let overwrites = + assign_children arity (fun _loc typ mode -> + let labeled_subtypes = unify_as_tuple typ in + List.map + (fun (_, typ) -> Assigning(typ, mode)) + labeled_subtypes) + overwrite + in let expl = - List.map2 - (fun (label, body) ((_, ty), argument_mode) -> + Misc.Stdlib.List.map3 + (fun (label, body) ((_, ty), argument_mode) overwrite -> Option.iter (fun _ -> Language_extension.assert_enabled ~loc Labeled_tuples ()) label; let argument_mode = mode_default argument_mode in let argument_mode = expect_mode_cross env ty argument_mode in - (label, type_expect env argument_mode body (mk_expected ty))) - sexpl types_and_modes + (label, type_expect ~overwrite env argument_mode body (mk_expected ty))) + sexpl types_and_modes overwrites in re { exp_desc = Texp_tuple (expl, alloc_mode); @@ -7902,7 +8062,7 @@ and type_unboxed_tuple ~loc ~env ~(expected_mode : expected_mode) ~ty_expected exp_attributes = attributes; exp_env = env } -and type_construct env (expected_mode : expected_mode) loc lid sarg +and type_construct ~overwrite env (expected_mode : expected_mode) loc lid sarg ty_expected_explained attrs = let { ty = ty_expected; explanation } = ty_expected_explained in let expected_type = @@ -7943,7 +8103,7 @@ and type_construct env (expected_mode : expected_mode) loc lid sarg raise(Error(loc, env, Constructor_arity_mismatch (lid.txt, constr.cstr_arity, List.length sargs))); let separate = !Clflags.principal || Env.has_local_constraints env in - let ty_args, ty_res, texp = + let unify_as_construct ty_expected = with_local_level_if separate begin fun () -> let ty_args, ty_res, texp = with_local_level_if separate begin fun () -> @@ -7972,6 +8132,7 @@ and type_construct env (expected_mode : expected_mode) loc lid sarg generalize_structure ty_res; List.iter (fun {Types.ca_type=ty; _} -> generalize_structure ty) ty_args) in + let ty_args, ty_res, texp = unify_as_construct ty_expected in let ty_args0, ty_res = match instance_list (ty_res :: (List.map (fun ca -> ca.Types.ca_type) ty_args)) with t :: tl -> tl, t @@ -7986,7 +8147,9 @@ and type_construct env (expected_mode : expected_mode) loc lid sarg begin match sargs with | [{pexp_desc = Pexp_ident _ | - Pexp_record (_, (Some {pexp_desc = Pexp_ident _}| None))}] -> + Pexp_record (_, (Some {pexp_desc = Pexp_ident _}| None)) | + Pexp_overwrite (_, {pexp_desc = + Pexp_record (_, (Some {pexp_desc = Pexp_ident _}| None))})}] -> Required | _ -> raise (Error(loc, env, Inlined_record_expected)) @@ -8000,12 +8163,30 @@ and type_construct 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 + 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 let args = - List.map2 - (fun e ({Types.ca_type=ty; ca_modalities=gf; _},t0) -> + Misc.Stdlib.List.map3 + (fun e ({Types.ca_type=ty; ca_modalities=gf; _},t0) overwrite -> 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) + type_argument ~recarg ~overwrite env argument_mode e ty t0) + sargs (List.combine ty_args ty_args0) overwrites in if constr.cstr_private = Private then begin match constr.cstr_repr with @@ -9432,11 +9613,11 @@ and type_send env loc explanation e met = let maybe_check_uniqueness_exp exp = if Language_extension.is_enabled Unique then - check_uniqueness_exp exp + Uniqueness_analysis.check_uniqueness_exp exp let maybe_check_uniqueness_value_bindings vbl = if Language_extension.is_enabled Unique then - check_uniqueness_value_bindings vbl + Uniqueness_analysis.check_uniqueness_value_bindings vbl (* Typing of toplevel bindings *) @@ -10459,6 +10640,12 @@ let report_error ~loc env = function (Style.as_inline_code Printtyp.type_expr) ty (Style.as_inline_code Jkind.format) jkind (Style.as_inline_code Jkind.format) Jkind.for_arrow + | 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 @@ -10495,7 +10682,7 @@ let type_exp env e = maybe_check_uniqueness_exp exp; exp let type_argument env e t1 t2 = - let exp = type_argument env mode_legacy e t1 t2 in + let exp = type_argument ~overwrite:No_overwrite env mode_legacy e t1 t2 in maybe_check_uniqueness_exp exp; exp let type_option_some env e t1 t2 = diff --git a/typing/typecore.mli b/typing/typecore.mli index ec9cf902837..b0c016dece6 100644 --- a/typing/typecore.mli +++ b/typing/typecore.mli @@ -316,6 +316,8 @@ type error = | Unsupported_stack_allocation of unsupported_stack_allocation | Not_allocation | Impossible_function_jkind of type_expr * jkind_lr + | Overwrite_of_invalid_term + | Unexpected_hole exception Error of Location.t * Env.t * error exception Error_forward of Location.error diff --git a/typing/typedtree.ml b/typing/typedtree.ml index 160fc1165ee..81548f7081c 100644 --- a/typing/typedtree.ml +++ b/typing/typedtree.ml @@ -92,10 +92,26 @@ module Unique_barrier = struct not traversing the uniqueness analysis. This ensures that the unique barriers will stay sound for future extensions. *) Uniqueness.Const.legacy + + let print ppf t = + let open Format in + let print = function + | Enabled u -> fprintf ppf "Enabled(%a)" (Mode.Uniqueness.print ()) u + | Resolved uc -> + fprintf ppf "Resolved(%a)" Mode.Uniqueness.Const.print uc + | Not_computed -> fprintf ppf "Not_computed" + in + print !t end type unique_use = Mode.Uniqueness.r * Mode.Linearity.l +let print_unique_use ppf (u,l) = + let open Format in + fprintf ppf "@[(%a,@ %a)@]" + (Mode.Uniqueness.print ()) u + (Mode.Linearity.print ()) l + type alloc_mode = { mode : Mode.Alloc.r; locality_context : Env.locality_context option; @@ -269,6 +285,8 @@ and expression_desc = | Texp_probe_is_enabled of { name:string } | Texp_exclave of expression | Texp_src_pos + | Texp_overwrite of expression * expression + | Texp_hole of unique_use and ident_kind = | Id_value diff --git a/typing/typedtree.mli b/typing/typedtree.mli index 1bb9bf0898e..2415ada7c92 100644 --- a/typing/typedtree.mli +++ b/typing/typedtree.mli @@ -80,10 +80,28 @@ module Unique_barrier : sig (* Resolve the unique barrier once type-checking is complete. *) val resolve : t -> Mode.Uniqueness.Const.t + + val print : Format.formatter -> t -> unit end +(** A unique use annotates accesses to an allocation. + In the type checker we ensure that + actual_mode <= expected_mode + unique_use.uniqueness == expected_mode.uniqueness + unique_use.linearity == actual_mode.linearity + That is, if the user expects an access to be unique, + both the actual_mode and unique_use are also unique. + In the uniqueness analysis, we check whether a particular access + is the only lexically use in its branch and if not, we set + aliased /\ many <= unique_use + This means that an allocation's actual_mode can be unique, + while a particular access of the allocation is aliased. + Furthermore, if there is more than one access to an allocation, + its actual_mode will have to be many. *) type unique_use = Mode.Uniqueness.r * Mode.Linearity.l +val print_unique_use : Format.formatter -> unique_use -> unit + type alloc_mode = { mode : Mode.Alloc.r; locality_context : Env.locality_context option; @@ -454,6 +472,8 @@ and expression_desc = (* A source position value which has been automatically inferred, either as a result of [%call_pos] occuring in an expression, or omission of a Position argument in function application *) + | Texp_overwrite of expression * expression (** overwrite_ exp with exp *) + | Texp_hole of unique_use (** _ *) and function_curry = | More_args of { partial_mode : Mode.Alloc.l } diff --git a/typing/typemode.ml b/typing/typemode.ml index 8cbd18650c7..cd2a921a4a3 100644 --- a/typing/typemode.ml +++ b/typing/typemode.ml @@ -191,7 +191,8 @@ let mutable_implied_modalities (mut : Types.mutability) attrs = Atom (Comonadic Portability, Meet_with Portability.Const.legacy) ] in let monadic : Modality.t list = - [ Atom (Monadic Uniqueness, Join_with Uniqueness.Const.legacy); + (* CR uniqueness: change back to old implementation *) + [ Atom (Monadic Uniqueness, Join_with Uniqueness.Const.Unique); Atom (Monadic Contention, Join_with Contention.Const.legacy) ] in match mut with diff --git a/typing/types.ml b/typing/types.ml index 5364405ca1b..97442987059 100644 --- a/typing/types.ml +++ b/typing/types.ml @@ -602,6 +602,14 @@ let equal_tag t1 t2 = | Extension path1, Extension path2 -> Path.same path1 path2 | (Ordinary _ | Extension _), _ -> false +let compare_tag t1 t2 = + match (t1, t2) with + | Ordinary {src_index=i1}, Ordinary {src_index=i2} -> + Int.compare i1 i2 + | Extension path1, Extension path2 -> Path.compare path1 path2 + | Ordinary _, Extension _ -> -1 + | Extension _, Ordinary _ -> 1 + let equal_flat_element e1 e2 = match e1, e2 with | Imm, Imm | Float64, Float64 | Float32, Float32 | Float_boxed, Float_boxed diff --git a/typing/types.mli b/typing/types.mli index 137e33d1c1a..1c9ae0cc906 100644 --- a/typing/types.mli +++ b/typing/types.mli @@ -864,6 +864,9 @@ type constructor_description = (* Constructors are the same *) val equal_tag : tag -> tag -> bool +(* Comparison of tags to store them in sets. *) +val compare_tag : tag -> tag -> int + (* Constructors may be the same, given potential rebinding *) val may_equal_constr : constructor_description -> constructor_description -> bool diff --git a/typing/uniqueness_analysis.ml b/typing/uniqueness_analysis.ml index 4de43ff01f5..e92cbb9b9bf 100644 --- a/typing/uniqueness_analysis.ml +++ b/typing/uniqueness_analysis.ml @@ -22,12 +22,33 @@ open Typedtree module Uniqueness = Mode.Uniqueness module Linearity = Mode.Linearity +(* CR uniqueness: currently printing does not work. + The debugger just returns for all types. *) +module Print_utils = struct + open Format + + let list elem ppf l = + fprintf ppf "@[[%a]@]" + (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ";@ ") elem) + l + + module Map (M : Map.S) = struct + let print ~key ~value ppf map = + let open Format in + fprintf ppf "@[{:"; + M.iter (fun k v -> fprintf ppf "@[%a :->@ %a@]" key k value v) map; + fprintf ppf ":}@]" + end +end + module Occurrence = struct (** The occurrence of a potentially unique ident in the expression. Currently it's just the location; might add more things in the future *) type t = { loc : Location.t } let mk loc = { loc } + + let print ppf { loc } = Location.print_loc ppf loc end let rec iter_error f = function @@ -64,6 +85,8 @@ module Maybe_unique : sig expected to be unique in any branch, it will return unique. If the current usage is forced, it will return aliased. *) val uniqueness : t -> Uniqueness.r + + val print : Format.formatter -> t -> unit end = struct (** Occurrences with modes to be forced aliased and many in the future if needed. This is a list because of multiple control flows. For example, if @@ -105,6 +128,14 @@ end = struct let extract_occurrence = function [] -> assert false | (_, occ) :: _ -> occ let meet l0 l1 = l0 @ l1 + + let print ppf t = + let open Format in + Print_utils.list + (fun ppf (uu, occ) -> + fprintf ppf "@[(%a,@ %a)@]" Typedtree.print_unique_use uu + Occurrence.print occ) + ppf t end module Maybe_aliased : sig @@ -134,6 +165,10 @@ module Maybe_aliased : sig val meet : t -> t -> t val singleton : Occurrence.t -> access -> t + + val print_access : Format.formatter -> access -> unit + + val print : Format.formatter -> t -> unit end = struct type access = | Read of Unique_barrier.t @@ -169,6 +204,19 @@ end = struct | Read barrier -> Unique_barrier.add_upper_bound uniq barrier | _ -> ()) t + + let print_access ppf = + let open Format in + function + | Read ub -> fprintf ppf "Read(%a)" Unique_barrier.print ub + | Write -> fprintf ppf "Write" + + let print ppf t = + let open Format in + Print_utils.list + (fun ppf (occ, access) -> + fprintf ppf "(%a,%a)" Occurrence.print occ print_access access) + ppf t end module Aliased : sig @@ -188,6 +236,8 @@ module Aliased : sig val extract_occurrence : t -> Occurrence.t val reason : t -> reason + + val print : Format.formatter -> t -> unit end = struct type reason = | Forced @@ -201,8 +251,62 @@ end = struct let extract_occurrence (occ, _) = occ let reason (_, reason) = reason + + let print ppf (occ, reason) = + let open Format in + let print_reason ppf = function + | Forced -> fprintf ppf "Forced" + | Lazy -> fprintf ppf "Lazy" + | Lifted ma -> fprintf ppf "Lifted(%a)" Maybe_aliased.print_access ma + in + fprintf ppf "(%a,%a)" Occurrence.print occ print_reason reason end +(** For error messages, we keep track of whether an access was sequential or parallel *) +type access_order = + | Seq + | Par + +(** Usage algebra + + In this file we track the usage of variables and tags throughout a source file. + Information can be composed using three operators: + + - seq: sequential composition such as 'foo; bar' + - par: parallel composition such as '(foo, bar)' + where evaluation order is not specified. + - choose: non-deterministic choice such as 'if b then foo else bar' + + subject to the following laws: + + - seq, par, choose are associative + - par, choose are commutative + - seq and par both distribute over choose + - choose is idempotent (forall a. a `choose` a = a) + - seq and par have a common unit 'empty' + + Note: These laws do not apply regarding the concrete error messages reported + to the user if the analysis fails. However, the laws do determine whether + the analysis may fail in the first place. + + These operations form a semiring, where choose is '+', seq is '*' and empty + is '1'. In practice, our semirings also have an ordering that all operations + above preserve. We write 's1 > s2' if it is sound to return 's2' whenever + the analysis returns 's1'. + + Missing from a proper semiring is that we do not ask for a 'zero' which would + the unit of choose and annihilate seq and par. The reason for this is that + zero is not very useful in practice: it only applies to empty pattern matches + but not to exceptions or 'assert false'. If 'assert false' would map to zero, + the analysis would allow segfaulting code before an assertion failure. + Thus we only need zero for empty pattern matches, but to avoid the hassle of + defining it, we simply return 'empty' in that case, which is sound in every + semiring with '0 > 1'. + + CR uniqueness: we might want to have a law relating seq and par. + See eg. 'concurrent semiring' in Hoare, Möller, Struth, Wehrmann + "Concurrent Kleene Algebra and its Foundations". *) + module Usage : sig type t = | Unused (** empty usage *) @@ -230,12 +334,17 @@ module Usage : sig type error = { cannot_force : Maybe_unique.cannot_force; there : t; (** The other usage *) - first_or_second : first_or_second + first_or_second : first_or_second; (** Is it the first or second usage that's failing force? *) + access_order : access_order + (** Are the accesses in sequence or parallel? *) } exception Error of error + (** Unused *) + val empty : t + (** Sequential composition *) val seq : t -> t -> t @@ -244,6 +353,8 @@ module Usage : sig (** Parallel composition *) val par : t -> t -> t + + val print : Format.formatter -> t -> unit end = struct (* We have Unused (top) > Borrowed > Aliased > Unique > Error (bot). @@ -295,6 +406,10 @@ end = struct - error error is represented as exception which is just easier. + + We could additionally include a zero for our semiring that sits above unused. + However, this would have to suppress errors which prevents us from representing + Error as an exception. *) type t = @@ -316,6 +431,8 @@ end = struct | Aliased t -> Some (Aliased.extract_occurrence t) | Maybe_unique t -> Some (Maybe_unique.extract_occurrence t) + let empty = Unused + let choose m0 m1 = match m0, m1 with | Unused, m | m, Unused -> m @@ -336,16 +453,17 @@ end = struct type error = { cannot_force : Maybe_unique.cannot_force; there : t; - first_or_second : first_or_second + first_or_second : first_or_second; + access_order : access_order } exception Error of error - let force_aliased_multiuse t there first_or_second = + let force_aliased_multiuse t there first_or_second access_order = match Maybe_unique.mark_multi_use t with | Ok () -> () | Error cannot_force -> - raise (Error { cannot_force; there; first_or_second }) + raise (Error { cannot_force; there; first_or_second; access_order }) let par m0 m1 = match m0, m1 with @@ -355,7 +473,7 @@ end = struct Maybe_aliased t | Borrowed _, Aliased t | Aliased t, Borrowed _ -> Aliased t | Borrowed occ, Maybe_unique t | Maybe_unique t, Borrowed occ -> - force_aliased_multiuse t (Borrowed occ) First; + force_aliased_multiuse t (Borrowed occ) First Par; aliased (Maybe_unique.extract_occurrence t) Aliased.Forced | Maybe_aliased t0, Maybe_aliased t1 -> Maybe_aliased (Maybe_aliased.meet t0 t1) @@ -365,20 +483,20 @@ end = struct Aliased occ | Maybe_aliased t0, Maybe_unique t1 | Maybe_unique t1, Maybe_aliased t0 -> (* t1 must be aliased *) - force_aliased_multiuse t1 (Maybe_aliased t0) First; + force_aliased_multiuse t1 (Maybe_aliased t0) First Par; (* The barrier stays empty; if there is any unique after this, the analysis will error *) aliased (Maybe_unique.extract_occurrence t1) Aliased.Forced | Aliased t0, Aliased _ -> Aliased t0 | Aliased t0, Maybe_unique t1 -> - force_aliased_multiuse t1 (Aliased t0) Second; + force_aliased_multiuse t1 (Aliased t0) Second Par; Aliased t0 | Maybe_unique t1, Aliased t0 -> - force_aliased_multiuse t1 (Aliased t0) First; + force_aliased_multiuse t1 (Aliased t0) First Par; Aliased t0 | Maybe_unique t0, Maybe_unique t1 -> - force_aliased_multiuse t0 m1 First; - force_aliased_multiuse t1 m0 Second; + force_aliased_multiuse t0 m1 First Par; + force_aliased_multiuse t1 m0 Second Par; aliased (Maybe_unique.extract_occurrence t0) Aliased.Forced let seq m0 m1 = @@ -418,7 +536,7 @@ end = struct m1 | Aliased _, Borrowed _ -> m0 | Maybe_unique l, Borrowed occ -> - force_aliased_multiuse l m1 First; + force_aliased_multiuse l m1 First Seq; aliased occ Aliased.Forced | Aliased _, Maybe_aliased _ -> (* The barrier stays empty; if there is any unique after this, @@ -437,19 +555,360 @@ end = struct the analysis will error. *) let occ = Maybe_aliased.extract_occurrence l1 in - force_aliased_multiuse l0 m1 First; + force_aliased_multiuse l0 m1 First Seq; aliased occ Aliased.Forced | Aliased _, Aliased _ -> m0 | Maybe_unique l, Aliased _ -> - force_aliased_multiuse l m1 First; + force_aliased_multiuse l m1 First Seq; m1 | Aliased _, Maybe_unique l -> - force_aliased_multiuse l m0 Second; + force_aliased_multiuse l m0 Second Seq; m0 | Maybe_unique l0, Maybe_unique l1 -> - force_aliased_multiuse l0 m1 First; - force_aliased_multiuse l1 m0 Second; + force_aliased_multiuse l0 m1 First Seq; + force_aliased_multiuse l1 m0 Second Seq; aliased (Maybe_unique.extract_occurrence l0) Aliased.Forced + + let print ppf = + let open Format in + function + | Unused -> fprintf ppf "Unused" + | Borrowed occ -> fprintf ppf "Borrowed(%a)" Occurrence.print occ + | Maybe_aliased ma -> fprintf ppf "Maybe_aliased(%a)" Maybe_aliased.print ma + | Aliased a -> fprintf ppf "Aliased(%a)" Aliased.print a + | Maybe_unique mu -> fprintf ppf "Maybe_unique(%a)" Maybe_unique.print mu +end + +module Tag : sig + (** This module represents the tags of constructors at runtime. + When we overwrite a tag, we need to check that the + tag is equal to the old tag. This is to ensure that + the tag never changes during overwrites. Changing the + tag during overwrites is not supported by the multicore GC. *) + type t = + { tag : Types.tag; + name_for_error : Longident.t loc + } + + module Set : Set.S with type elt = t + + module Map : Map.S with type key = t + + val print : Format.formatter -> t -> unit +end = struct + type t = + { tag : Types.tag; + name_for_error : Longident.t loc + } + + type tags = t + + module Set = Set.Make (struct + type t = tags + + let compare t1 t2 = Types.compare_tag t1.tag t2.tag + end) + + module Map = Map.Make (struct + type t = tags + + let compare t1 t2 = Types.compare_tag t1.tag t2.tag + end) + + let print ppf { name_for_error; _ } = + Pprintast.longident ppf name_for_error.txt +end + +module Learned_tags : sig + (** This module collects the tags of allocations which we may learn from + pattern matches. It is always sound to forget tags we have learned + + [choose] is used to combine information in or-patterns and [par] + is used to combine information from several pattern matches on + the same variable. [seq] is not used (but may still be called + while checking expressions; then the arguments are [empty]). + + Perhaps surprisingly, we allow an allocation to have multiple + tags. This can only happen when there are two match-statements + and we enter branches of incompatible tags. Such code can never + run and so it does not matter which choice we make here. *) + + type t + + (** No known tag: eg. '()' pattern *) + val empty : t + + (** Sequential composition: This is not called for patterns in general + and we use the same implementation as for [par]. *) + val seq : t -> t -> t + + (** Non-deterministic choice: This is called for or-patterns like + '(TagA _ | TagB _) ->' where we learn the intersection of + the tags in the pattern. *) + val choose : t -> t -> t + + (** Parallel composition: If we match on the same memory cell twice + we learn the union of the patterns. For example, in + 'match (x, x) with (TagA _, TagB _) ->' we learn both tags. + This is a sound choice since 'x' can not possibly have two distinct + tags and also we are now aliasing 'x' which makes it impossible to + overwrite. Note that 'x' can have two distinct tags in the presence + of mutation but we track that in the Overwrites module below. *) + val par : t -> t -> t + + (** Register a tag we know (eg. from a pattern-match) *) + val learn_tag : Tag.t -> t + + (** Extract the tags that this cell may have *) + val extract_tags : t -> Tag.Set.t + + (** Assert that no tags were learned. *) + val assert_empty : t -> unit + + val print : Format.formatter -> t -> unit +end = struct + type t = Tag.Set.t + + (* If we were to define a zero for this semiring, it would be + the set of all possible tags. *) + + let empty = Tag.Set.empty + + let choose t0 t1 = Tag.Set.inter t0 t1 + + let par t0 t1 = Tag.Set.union t0 t1 + + let seq t0 t1 = par t0 t1 + + let learn_tag tag = Tag.Set.singleton tag + + let extract_tags t = t + + let assert_empty t = assert (Tag.Set.is_empty t) + + let print ppf t = + let open Format in + fprintf ppf "%a" (Format.pp_print_list Tag.print) (Tag.Set.elements t) +end + +module Overwrites : sig + (** This module collects the tags of overwrites. It is always sound + to assume we have overwritten with additional tags. + + However, it is in general unsound if the user mutates the tag + after we have learned its nature. Then all bets are off and we + always fail if there is an overwrite that follows a mutation. *) + + type t + + type old_tag = + | Old_tag_unknown + | Old_tag_was of Tag.t + | Old_tag_mutated of access_order + + type error = + | Changed_tag of + { old_tag : old_tag; + new_tag : Tag.t + } + + exception Error of error + + (** No overwrites as in eg. a constant expression '()'. *) + val empty : t + + (** Overwrite using a certain tag *) + val overwrite_tag : Tag.t -> t + + (** Indicate a mutation (which invalidates all tags we have learned + and will learn). If there is also an overwrite, we fail. *) + val mutate_tag : t + + (** Sequential composition: Union the overwrites that were collected + in either argument. Error if there was a mutation in one argument + and an overwrite in the second. Eg. + 'x <- TagA; overwrite_ x with TagB' fails + 'overwrite_ x with TagA; x <- TagB' fails + 'overwrite_ x with TagA; overwrite_ x with TagB' succeeds + *) + val seq : t -> t -> t + + (** Non-deterministic choice: Union the overwrites that were collected + in either argument. Record if there was a mutation in either + argument but do not error since the branches are independent. Eg. + 'if b then overwrite_ x with TagA else overwrite_ x with TagB' succeeds + 'if b then x <- TagA else overwrite_ x with TagB' succeeds and records + that 'x' was mutated in a branch. + *) + val choose : t -> t -> t + + (** Parallel composition: Same as [seq]. *) + val par : t -> t -> t + + (** If we find out that a tag was mutated, + we need to promote this information to its children. + This is because a write to a mutable field can change + any tag that is reachable from the mutable field. *) + val promote_mutation_to_children : t -> t + + (** We may not overwrite a tag we do not know. + At the end of the analysis, this function should + be called to ensure all overwrites are on known tags. *) + val check_no_remaining_overwritten_as : t -> unit + + (** Accept the overwrites using tags that we have learned + from a pattern-match. *) + val match_with_learned_tags : Tag.Set.t -> t -> t + + (** Assert that no overwrites were collected. *) + val assert_empty : t -> unit + + val print : Format.formatter -> t -> unit +end = struct + type tags = + { overwritten : Tag.Set.t Tag.Map.t; + (** The keys of the map are the tags of the overwrite. + When we learn new tags, we can remove keys from this map, + that correspond to the new tags. We then keep the learned + tags on the keys that did not match them to produce good + error messages. It is always sound to add elements to this map. + *) + was_mutated : bool + (** If a mutation occurs in a branch with no overwriting, we set this flag. + It is acceptable for overwrites to occur in a different branch or + earlier in the control flow, but it is not okay for an overwrite to + happen later in the control flow. + *) + } + + type t = + | Tags of tags + | Tag_was_mutated + (** We have discovered a mutable write. + This is dangerous: We might have accepted a overwrite based on the wrong tag. + If we detect this state, we reject all overwrites to this cell. *) + + type old_tag = + | Old_tag_unknown + | Old_tag_was of Tag.t + | Old_tag_mutated of access_order + + type error = + | Changed_tag of + { old_tag : old_tag; + new_tag : Tag.t + } + + exception Error of error + + let empty = Tags { overwritten = Tag.Map.empty; was_mutated = false } + + let overwrite_tag tag = + Tags + { overwritten = Tag.Map.singleton tag Tag.Set.empty; was_mutated = false } + + let mutate_tag = Tag_was_mutated + + (* We union the overwrites and either intersect or union the learned tags. + The distinction between these two functions only affects error messages. + *) + let union_with_inter_learned = + Tag.Map.union (fun _ t0 t1 -> Some (Tag.Set.inter t0 t1)) + + let union_with_union_learned = + Tag.Map.union (fun _ t0 t1 -> Some (Tag.Set.union t0 t1)) + + let choose t0 t1 = + match t0, t1 with + | Tags t0, Tags t1 -> + Tags + { overwritten = union_with_inter_learned t0.overwritten t1.overwritten; + was_mutated = t0.was_mutated || t1.was_mutated + } + | Tags { overwritten }, Tag_was_mutated + | Tag_was_mutated, Tags { overwritten } -> + Tags { overwritten; was_mutated = true } + | Tag_was_mutated, Tag_was_mutated -> Tag_was_mutated + + let seq_or_par access_order t0 t1 = + match t0, t1 with + | Tag_was_mutated, Tag_was_mutated -> Tag_was_mutated + | Tags t0, Tags t1 when (not t0.was_mutated) && not t1.was_mutated -> + Tags + { overwritten = union_with_union_learned t0.overwritten t1.overwritten; + was_mutated = false + } + | Tags { overwritten }, _ | _, Tags { overwritten } -> ( + match Tag.Map.choose_opt overwritten with + | None -> Tag_was_mutated + | Some (t, _) -> + raise + (Error + (Changed_tag + { old_tag = Old_tag_mutated access_order; new_tag = t }))) + + let par t0 t1 = seq_or_par Par t0 t1 + + let seq t0 t1 = seq_or_par Seq t0 t1 + + (* This is effectively the set difference [overwrite - learned]. + However, we also store the newly learned tags on the overwrites + that are not eliminated to give better error messages. *) + let match_with_learned_tags newly_learned t = + match t with + | Tag_was_mutated -> Tag_was_mutated + | Tags { overwritten; was_mutated } -> + Tags + { overwritten = + Tag.Map.filter_map + (fun tag learned_before -> + if Tag.Set.mem tag newly_learned + then None + else Some (Tag.Set.union learned_before newly_learned)) + overwritten; + was_mutated + } + + let promote_mutation_to_children t = + match t with + | Tag_was_mutated -> Tag_was_mutated + | Tags { was_mutated } -> if was_mutated then Tag_was_mutated else empty + + let check_no_remaining_overwritten_as t = + match t with + | Tags { overwritten } -> ( + match Tag.Map.choose_opt overwritten with + | None -> () + | Some (tag_overwritten, have_learned) -> + raise + (Error + (match Tag.Set.choose_opt have_learned with + | None -> + Changed_tag + { old_tag = Old_tag_unknown; new_tag = tag_overwritten } + | Some tag_learned -> + Changed_tag + { old_tag = Old_tag_was tag_learned; + new_tag = tag_overwritten + }))) + | Tag_was_mutated -> () + + let assert_empty t = + match t with + | Tags { overwritten; was_mutated } -> + assert (not was_mutated); + assert (Tag.Map.is_empty overwritten) + | _ -> assert false + + let print ppf = + let open Format in + function + | Tags tag -> + fprintf ppf "Tags { overwritten = %a; was_mutated = %a }" + (Format.pp_print_list Tag.print) + (List.map fst (Tag.Map.bindings tag.overwritten)) + Format.pp_print_bool tag.was_mutated + | Tag_was_mutated -> fprintf ppf "Tag_was_mutated" end module Projection : sig @@ -463,6 +922,11 @@ module Projection : sig | Memory_address (* this is rendered as clubsuit in the ICFP'24 paper *) module Map : Map.S with type key = t + + val print : Format.formatter -> t -> unit + + val print_map : + (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a Map.t -> unit end = struct module T = struct type t = @@ -509,6 +973,20 @@ end = struct include T module Map = Map.Make (T) + + let print ppf = + let open Format in + function + | Tuple_field n -> fprintf ppf "Tuple_field(%d)" n + | Record_field l -> fprintf ppf "Record_field(%s)" l + | Construct_field (s, n) -> fprintf ppf "Construct_field(%s,%d)" s n + | Variant_field l -> fprintf ppf "Variant_field(%s)" l + | Array_index n -> fprintf ppf "Array_index(%d)" n + | Memory_address -> fprintf ppf "Memory_address" + + let print_map print_value ppf map = + let module M = Print_utils.Map (Map) in + M.print ~key:print ~value:print_value ppf map end type boundary_reason = @@ -534,6 +1012,7 @@ type error = { cannot_force : Maybe_unique.cannot_force; reason : boundary_reason } + | Overwrite_changed_tag of Overwrites.error exception Error of error @@ -548,6 +1027,8 @@ module Usage_tree : sig (** The path representing the root node *) val root : t + + val print : Format.formatter -> t -> unit end (** Usage tree, lifted from [Usage.t] *) @@ -562,11 +1043,37 @@ module Usage_tree : sig (** Parallel composition lifted from [Usage.par] *) val par : t -> t -> t - (** A singleton tree containing only one leaf *) - val singleton : Usage.t -> Path.t -> t + (** An empty tree containing only the root with empty usage *) + val empty : t + + (** A singleton tree containing only one leaf. In patterns, the + 'Overwrites.t' should be empty and in expressions the 'Learned_tags.t' + should be empty. *) + val singleton : Usage.t -> Learned_tags.t -> Overwrites.t -> Path.t -> t (** Runs a function through the tree; the function must be monotone *) - val mapi : (Path.t -> Usage.t -> Usage.t) -> t -> t + val mapi : + (Path.t -> Usage.t -> Usage.t) -> + (Learned_tags.t -> Learned_tags.t) -> + (Overwrites.t -> Overwrites.t) -> + t -> + t + + (** Check that all overwrites are on known tags *) + val check_no_remaining_overwritten_as : t -> unit + + (** Split into usage and overwrites on the one side + and learned tags on the other. It is safe to throw + away the second component of the pair. *) + val split_usage_tags : t -> t * t + + (** Use the learned_tags from the first argument to match with + the overwrites of the second argument. + Danger: this throws away the usage in its first argument and should + only be called on the learned tags from [split_usage_tags]. *) + val match_with_learned_tags : t -> t -> t + + val print : Format.formatter -> t -> unit end = struct (** Represents a tree of usage. Each node records the choose on all possible execution paths. As a result, trees such as `S -> U` is valid, even though @@ -577,10 +1084,16 @@ end = struct INVARIANT: children >= parent. For example, having an aliased child under a unique parent is nonsense. The invariant is preserved because Usage.choose, Usage.par, and Usage.seq above are monotone, and Usage_tree.par and - Usage_tree.seq, Usage_tree.choose here are node-wise. *) + Usage_tree.seq, Usage_tree.choose here are node-wise. + + INVARIANT: Either the [learned] or the [overwrites] is [empty]. When + checking patterns the latter is empty while for expression the former is + empty. *) type t = { children : t Projection.Map.t; - usage : Usage.t + usage : Usage.t; + learned : Learned_tags.t; + overwrites : Overwrites.t } module Path = struct @@ -589,22 +1102,26 @@ end = struct let child (a : Projection.t) (p : t) : t = p @ [a] let root : t = [] + + let print ppf t = Print_utils.list Projection.print ppf t end - let mapi_aux projs f t = + let mapi_aux projs fu fl fo t = let rec loop projs t = - let usage = f projs t.usage in + let usage = fu projs t.usage in let children = Projection.Map.mapi (fun proj t -> loop (proj :: projs) t) t.children in - { usage; children } + let learned = fl t.learned in + let overwrites = fo t.overwrites in + { usage; children; learned; overwrites } in loop projs t let mapi f t = mapi_aux [] f t - let rec mapi2 f t0 t1 = - let usage = f Self t0.usage t1.usage in + let rec mapi2 fu fl fo t0 t1 = + let usage = fu Self t0.usage t1.usage in let children = Projection.Map.merge (fun proj c0 c1 -> @@ -613,38 +1130,117 @@ end = struct | None, Some c1 -> Some (mapi_aux [proj] - (fun projs r -> f (Ancestor projs) t0.usage r) + (fun projs r -> fu (Ancestor projs) t0.usage r) + (fun r -> fl r Learned_tags.empty) + (fun r -> + fo (Overwrites.promote_mutation_to_children t0.overwrites) r) c1) | Some c0, None -> Some (mapi_aux [proj] - (fun projs l -> f (Descendant projs) l t1.usage) + (fun projs l -> fu (Descendant projs) l t1.usage) + (fun l -> fl l Learned_tags.empty) + (fun l -> + fo l (Overwrites.promote_mutation_to_children t1.overwrites)) c0) - | Some c0, Some c1 -> Some (mapi2 f c0 c1)) + | Some c0, Some c1 -> Some (mapi2 fu fl fo c0 c1)) t0.children t1.children in - { usage; children } + let learned = fl t0.learned t1.learned in + let overwrites = fo t0.overwrites t1.overwrites in + { usage; children; learned; overwrites } - let lift f t0 t1 = + let lift fu fl fo t0 t1 = mapi2 (fun first_is_of_second t0 t1 -> - try f t0 t1 + try fu t0 t1 with Usage.Error error -> raise (Error (Usage { inner = error; first_is_of_second }))) + fl + (fun t0 t1 -> + try fo t0 t1 + with Overwrites.Error error -> + raise (Error (Overwrite_changed_tag error))) t0 t1 - let choose t0 t1 = lift Usage.choose t0 t1 + let choose t0 t1 = + lift Usage.choose Learned_tags.choose Overwrites.choose t0 t1 + + let seq t0 t1 = lift Usage.seq Learned_tags.seq Overwrites.seq t0 t1 - let seq t0 t1 = lift Usage.seq t0 t1 + let par t0 t1 = lift Usage.par Learned_tags.par Overwrites.par t0 t1 - let par t0 t1 = lift Usage.par t0 t1 + let empty = + { children = Projection.Map.empty; + usage = Usage.empty; + learned = Learned_tags.empty; + overwrites = Overwrites.empty + } - let rec singleton leaf = function - | [] -> { usage = leaf; children = Projection.Map.empty } + let rec singleton leaf learned overwrites = function + | [] -> + { usage = leaf; children = Projection.Map.empty; learned; overwrites } | proj :: path -> - { usage = Unused; - children = Projection.Map.singleton proj (singleton leaf path) + { usage = Usage.empty; + children = + Projection.Map.singleton proj (singleton leaf learned overwrites path); + learned = Learned_tags.empty; + overwrites = Overwrites.empty } + + let rec check_no_remaining_overwritten_as { children; overwrites } = + Projection.Map.iter + (fun _ t -> check_no_remaining_overwritten_as t) + children; + try Overwrites.check_no_remaining_overwritten_as overwrites + with Overwrites.Error error -> raise (Error (Overwrite_changed_tag error)) + + let rec split_usage_tags { children; usage; overwrites; learned } = + let split_children = Projection.Map.map split_usage_tags children in + let children_usages, children_tags = + ( Projection.Map.map fst split_children, + Projection.Map.map snd split_children ) + in + Overwrites.assert_empty overwrites; + ( { children = children_usages; + usage; + overwrites = Overwrites.empty; + learned = Learned_tags.empty + }, + { children = children_tags; + usage = Usage.empty; + overwrites = Overwrites.empty; + learned + } ) + + let rec match_with_learned_tags learned t = + let children = + Projection.Map.merge + (fun _ c0 c1 -> + match c0, c1 with + | None, None -> assert false + | None, Some c1 -> Some c1 + | Some _, None -> None + | Some c0, Some c1 -> Some (match_with_learned_tags c0 c1)) + learned.children t.children + in + Learned_tags.assert_empty t.learned; + { usage = t.usage; + children; + learned = Learned_tags.empty; + overwrites = + Overwrites.match_with_learned_tags + (Learned_tags.extract_tags learned.learned) + t.overwrites + } + + let rec print ppf { children; usage; learned; overwrites } = + let open Format in + fprintf ppf + "@[{ children = %a;@ usage = %a;@ learned = %a;@ overwrites = %a }@]" + (Projection.print_map print) + children Usage.print usage Learned_tags.print learned Overwrites.print + overwrites end (** Lift Usage_tree to forest *) @@ -657,6 +1253,8 @@ module Usage_forest : sig (** Create a fresh tree in the forest *) val fresh_root : unit -> t + + val print : Format.formatter -> t -> unit end (** Represents a forest of usage. *) @@ -681,10 +1279,31 @@ module Usage_forest : sig val unused : t (** The forest with only one usage, given by the path and the usage *) - val singleton : Usage.t -> Path.t -> t + val singleton : Usage.t -> Learned_tags.t -> Overwrites.t -> Path.t -> t (** Run a function through a forest. The function must be monotone *) - val map : (Usage.t -> Usage.t) -> t -> t + val map : + (Usage.t -> Usage.t) -> + (Learned_tags.t -> Learned_tags.t) -> + (Overwrites.t -> Overwrites.t) -> + t -> + t + + (** Check that all overwrites are on known tags *) + val check_no_remaining_overwritten_as : t -> unit + + (** Split into usage and overwrites on the one side + and learned tags on the other. It is safe to throw + away the second component of the pair. *) + val split_usage_tags : t -> t * t + + (** Use the learned_tags from the first argument to match with + the overwrites of the second argument. + Danger: this throws away the usage in its first argument and should + only be called on the learned tags from [split_usage_tags]. *) + val match_with_learned_tags : t -> t -> t + + val print : Format.formatter -> t -> unit end = struct module Root_id = struct module T = struct @@ -703,6 +1322,8 @@ end = struct let id = !stamp in stamp := id + 1; { id } + + let print ppf { id } = Format.fprintf ppf "{%d}" id end type t = Usage_tree.t Root_id.Map.t @@ -714,6 +1335,11 @@ end = struct rootid, Usage_tree.Path.child proj path let fresh_root () : t = Root_id.fresh (), Usage_tree.Path.root + + let print ppf (root_id, path) = + let open Format in + fprintf ppf "@[(%a,@ %a)@]" Root_id.print root_id Usage_tree.Path.print + path end let unused = Root_id.Map.empty @@ -724,8 +1350,8 @@ end = struct (fun _rootid t0 t1 -> match t0, t1 with | None, None -> assert false - | None, Some t1 -> Some t1 - | Some t0, None -> Some t0 + | None, Some t1 -> Some (f Usage_tree.empty t1) + | Some t0, None -> Some (f t0 Usage_tree.empty) | Some t0, Some t1 -> Some (f t0 t1)) t0 t1 @@ -735,19 +1361,54 @@ end = struct let par t0 t1 = map2 Usage_tree.par t0 t1 - let chooses l = List.fold_left choose unused l + (* For convenience, our semirings do not have a zero. + However, when we fold the [choose] operation we need to initialize the + accumulator with zero. We avoid doing this here by skipping the initial + accumulator altogether. When [chooses] gets passed an empty list, + we return the '1' of the semiring which is sound in all semirings + that have '0 > 1'. See the discussion about semirings above. *) + let fold_left1 f = function [] -> unused | x :: l -> List.fold_left f x l + + let chooses l = fold_left1 choose l - let seqs l = List.fold_left seq unused l + let seqs l = fold_left1 seq l - let pars l = List.fold_left par unused l + let pars l = fold_left1 par l - let singleton leaf ((rootid, path') : Path.t) = - Root_id.Map.singleton rootid (Usage_tree.singleton leaf path') + let singleton leaf learned overwrites ((rootid, path') : Path.t) = + Root_id.Map.singleton rootid + (Usage_tree.singleton leaf learned overwrites path') - (** f must be monotone *) - let map f = + (** 'fu fl fo' all must be monotone *) + let map fu fl fo = Root_id.Map.mapi (fun _root tree -> - Usage_tree.mapi (fun _projs usage -> f usage) tree) + Usage_tree.mapi (fun _projs usage -> fu usage) fl fo tree) + + let check_no_remaining_overwritten_as t = + Root_id.Map.iter + (fun _ t -> Usage_tree.check_no_remaining_overwritten_as t) + t + + let split_usage_tags t = + ( Root_id.Map.map (fun x -> fst (Usage_tree.split_usage_tags x)) t, + Root_id.Map.map (fun x -> snd (Usage_tree.split_usage_tags x)) t ) + + let match_with_learned_tags learned t = + Root_id.Map.merge + (fun _rootid t0 t1 -> + match t0, t1 with + | None, None -> assert false + | None, Some t1 -> Some t1 + | Some _, None -> None + | Some t0, Some t1 -> Some (Usage_tree.match_with_learned_tags t0 t1)) + learned t + + let print ppf t = + let open Format in + let module M = Print_utils.Map (Root_id.Map) in + M.print + ~key:(fun ppf { id } -> fprintf ppf "%d" id) + ~value:Usage_tree.print ppf t end module UF = Usage_forest @@ -790,7 +1451,7 @@ module Paths : sig (** [memory_address t] is [child Projection.Memory_address t]. *) val memory_address : t -> t - val mark : Usage.t -> t -> UF.t + val mark : Usage.t -> Learned_tags.t -> Overwrites.t -> t -> UF.t val fresh : unit -> t @@ -800,6 +1461,14 @@ module Paths : sig Occurrence.t -> Maybe_aliased.access -> t -> UF.t val mark_aliased : Occurrence.t -> Aliased.reason -> t -> UF.t + + val invalidate_tag : t -> UF.t + + val overwrite_tag : Tag.t -> t -> UF.t + + val learn_tag : Tag.t -> t -> UF.t + + val print : Format.formatter -> t -> unit end = struct type t = UF.Path.t list @@ -839,16 +1508,29 @@ end = struct let memory_address t = child Projection.Memory_address t - let mark usage t = UF.chooses (List.map (UF.singleton usage) t) + let mark usage learned overwrites t = + UF.chooses (List.map (UF.singleton usage learned overwrites) t) let fresh () = [UF.Path.fresh_root ()] let mark_implicit_borrow_memory_address occ access paths = mark (Maybe_aliased (Maybe_aliased.singleton occ access)) - (memory_address paths) + Learned_tags.empty Overwrites.empty (memory_address paths) + + let mark_aliased occ reason paths = + mark (Usage.aliased occ reason) Learned_tags.empty Overwrites.empty paths + + let invalidate_tag paths = + mark Usage.empty Learned_tags.empty Overwrites.mutate_tag paths + + let overwrite_tag tag paths = + mark Usage.empty Learned_tags.empty (Overwrites.overwrite_tag tag) paths + + let learn_tag tag paths = + mark Usage.empty (Learned_tags.learn_tag tag) Overwrites.empty paths - let mark_aliased occ reason paths = mark (Usage.aliased occ reason) paths + let print ppf t = Print_utils.list UF.Path.print ppf t end let force_aliased_boundary unique_use occ ~reason = @@ -887,11 +1569,20 @@ module Value : sig (** Mark the value as aliased_or_unique *) val mark_maybe_unique : t -> UF.t + (** Mark the value's memory address as aliased_or_unique *) + val mark_consumed_memory_address : t -> UF.t + (** Mark the memory_address of the value as implicitly borrowed (borrow_or_aliased). *) val mark_implicit_borrow_memory_address : Maybe_aliased.access -> t -> UF.t val mark_aliased : reason:boundary_reason -> t -> UF.t + + val invalidate_tag : t -> UF.t + + val overwrite_tag : Tag.t -> t -> UF.t + + val print : Format.formatter -> t -> unit end = struct type t = | Fresh @@ -924,14 +1615,40 @@ end = struct let mark_maybe_unique = function | Fresh -> UF.unused | Existing { paths; unique_use; occ } -> - Paths.mark (Usage.maybe_unique unique_use occ) paths + Paths.mark + (Usage.maybe_unique unique_use occ) + Learned_tags.empty Overwrites.empty paths + + let mark_consumed_memory_address = function + | Fresh -> UF.unused + | Existing { paths; unique_use; occ } -> + Paths.mark + (Usage.maybe_unique unique_use occ) + Learned_tags.empty Overwrites.empty + (Paths.memory_address paths) let mark_aliased ~reason = function | Fresh -> UF.unused | Existing { paths; unique_use; occ } -> force_aliased_boundary unique_use occ ~reason; let aliased = Usage.aliased occ Aliased.Forced in - Paths.mark aliased paths + Paths.mark aliased Learned_tags.empty Overwrites.empty paths + + let invalidate_tag = function + | Fresh -> UF.unused + | Existing { paths; _ } -> Paths.invalidate_tag paths + + let overwrite_tag tag = function + | Fresh -> UF.unused + | Existing { paths; _ } -> Paths.overwrite_tag tag paths + + let print ppf = + let open Format in + function + | Fresh -> fprintf ppf "Fresh" + | Existing { paths; unique_use; occ } -> + fprintf ppf "@[{ paths = %a;@ unique_use = %a;@ occ = %a }@]" Paths.print + paths Typedtree.print_unique_use unique_use Occurrence.print occ end module Ienv : sig @@ -954,10 +1671,12 @@ module Ienv : sig val singleton : Ident.t -> Paths.t -> t (* Constructing a mapping with only one mapping *) + + val print : Format.formatter -> t -> unit end (** Mapping from identifiers to a list of possible nodes, each represented by - a path into the forest, instead of directly ponting to the node. *) + a path into the forest, instead of directly pointing to the node. *) type t (** Extend a mapping with an extension *) @@ -968,6 +1687,8 @@ module Ienv : sig (** Find the list of paths corresponding to an identifier *) val find_opt : Ident.t -> t -> Paths.t option + + val print : Format.formatter -> t -> unit end = struct module Extension = struct type t = Paths.t Ident.Map.t @@ -994,6 +1715,10 @@ end = struct let conjuncts = List.fold_left conjunct empty let singleton id locs = Ident.Map.singleton id locs + + let print ppf t = + let module M = Print_utils.Map (Ident.Map) in + M.print ~key:Ident.print ~value:Paths.print ppf t end type t = Paths.t Ident.Map.t @@ -1007,6 +1732,10 @@ end = struct t ex let find_opt = Ident.Map.find_opt + + let print ppf t = + let module M = Print_utils.Map (Ident.Map) in + M.print ~key:Ident.print ~value:Paths.print ppf t end (* The fun algebraic stuff ends. Here comes the concrete mess *) @@ -1090,6 +1819,9 @@ and pattern_match_single pat paths : Ienv.Extension.t * UF.t = let uf_read = borrow_memory_address () in Ienv.Extension.empty, uf_read | Tpat_construct (lbl, cd, pats, _) -> + let uf_tag = + Paths.learn_tag { tag = cd.cstr_tag; name_for_error = lbl } paths + in let uf_read = borrow_memory_address () in let pats_args = List.combine pats cd.cstr_args in let ext, uf_pats = @@ -1101,7 +1833,7 @@ and pattern_match_single pat paths : Ienv.Extension.t * UF.t = pats_args |> conjuncts_pattern_match in - ext, UF.par uf_read uf_pats + ext, UF.pars [uf_tag; uf_read; uf_pats] | Tpat_variant (lbl, arg, _) -> let uf_read = borrow_memory_address () in let ext, uf_arg = @@ -1111,7 +1843,7 @@ and pattern_match_single pat paths : Ienv.Extension.t * UF.t = pattern_match_single arg paths | None -> Ienv.Extension.empty, UF.unused in - ext, UF.par uf_read uf_arg + ext, UF.pars [uf_read; uf_arg] | Tpat_record (pats, _) -> let uf_read = borrow_memory_address () in let ext, uf_pats = @@ -1254,8 +1986,15 @@ let lift_implicit_borrowing uf = | m -> (* other usage stays the same *) m) + (fun t -> t) + (fun t -> t) uf +let descend proj overwrite = + match overwrite with + | None -> None + | Some paths -> Some (Paths.child proj paths) + (* There are two modes our algorithm will work at. In the first mode, we care about if the expression can be considered as @@ -1268,7 +2007,7 @@ let lift_implicit_borrowing uf = using a.x.y. This mode is used in most occasions. *) (** Corresponds to the second mode *) -let rec check_uniqueness_exp (ienv : Ienv.t) exp : UF.t = +let rec check_uniqueness_exp ~overwrite (ienv : Ienv.t) exp : UF.t = match exp.exp_desc with | Texp_ident _ -> let value, uf = check_uniqueness_exp_as_value ienv exp in @@ -1276,7 +2015,9 @@ let rec check_uniqueness_exp (ienv : Ienv.t) exp : UF.t = | Texp_constant _ -> UF.unused | Texp_let (_, vbs, body) -> let ext, uf_vbs = check_uniqueness_value_bindings ienv vbs in - let uf_body = check_uniqueness_exp (Ienv.extend ienv ext) body in + let uf_body = + check_uniqueness_exp ~overwrite:None (Ienv.extend ienv ext) body + in UF.seq uf_vbs uf_body | Texp_function { params; body; _ } -> let ienv, uf_params = @@ -1288,37 +2029,44 @@ let rec check_uniqueness_exp (ienv : Ienv.t) exp : UF.t = match param.fp_kind with | Tparam_pat pat -> let value = Match_single (Paths.fresh ()) in - pattern_match pat value + let ext, uf_pat = pattern_match pat value in + ext, (UF.unused, uf_pat) | Tparam_optional_default (pat, default, _) -> let value, uf_default = check_uniqueness_exp_for_match ienv default in let ext, uf_pat = pattern_match pat value in - ext, UF.seq uf_default uf_pat + ext, (uf_default, uf_pat) in Ienv.extend ienv ext, uf_param) ienv params in let uf_body = match body with - | Tfunction_body body -> check_uniqueness_exp ienv body + | Tfunction_body body -> check_uniqueness_exp ~overwrite:None ienv body | Tfunction_cases { fc_cases; fc_param = _; _ } -> (* [param] is only a hint not a binder; actual binding done by the [c_lhs] field of each of the [cases]. *) let value = Match_single (Paths.fresh ()) in check_uniqueness_cases ienv value fc_cases in - let uf = UF.seq (UF.seqs uf_params) uf_body in + let uf = + List.fold_right + (fun (uf_default, uf_pat) uf_body -> + let uf_pat, tags = UF.split_usage_tags uf_pat in + UF.seqs [uf_default; uf_pat; UF.match_with_learned_tags tags uf_body]) + uf_params uf_body + in (* we are constructing a closure here, and therefore any implicit borrowing of free variables in the closure is in fact using aliased. *) lift_implicit_borrowing uf | Texp_apply (fn, args, _, _, _) -> - let uf_fn = check_uniqueness_exp ienv fn in + let uf_fn = check_uniqueness_exp ~overwrite:None ienv fn in let uf_args = List.map (fun (_, arg) -> match arg with - | Arg (e, _) -> check_uniqueness_exp ienv e + | Arg (e, _) -> check_uniqueness_exp ~overwrite:None ienv e | Omitted _ -> UF.unused) args in @@ -1328,19 +2076,37 @@ let rec check_uniqueness_exp (ienv : Ienv.t) exp : UF.t = let uf_cases = check_uniqueness_comp_cases ienv value cases in UF.seq uf_arg uf_cases | Texp_try (body, cases) -> - let uf_body = check_uniqueness_exp ienv body in + let uf_body = check_uniqueness_exp ~overwrite:None ienv body in let value = Match_single (Paths.fresh ()) in let uf_cases = check_uniqueness_cases ienv value cases in (* we don't know how much of e will be run; safe to assume all of them *) UF.seq uf_body uf_cases | Texp_tuple (es, _) -> - UF.pars (List.map (fun (_, e) -> check_uniqueness_exp ienv e) es) + UF.pars + (List.mapi + (fun i (_, e) -> + check_uniqueness_exp + ~overwrite:(descend (Projection.Tuple_field i) overwrite) + ienv e) + es) | Texp_unboxed_tuple es -> - UF.pars (List.map (fun (_, e, _) -> check_uniqueness_exp ienv e) es) - | Texp_construct (_, _, es, _) -> - UF.pars (List.map (fun e -> check_uniqueness_exp ienv e) es) + UF.pars + (List.map + (fun (_, e, _) -> check_uniqueness_exp ~overwrite:None ienv e) + es) + | Texp_construct (lbl, _, es, _) -> + let name = Longident.last lbl.txt in + UF.pars + (List.mapi + (fun i e -> + check_uniqueness_exp + ~overwrite: + (descend (Projection.Construct_field (name, i)) overwrite) + ienv e) + es) | Texp_variant (_, None) -> UF.unused - | Texp_variant (_, Some (arg, _)) -> check_uniqueness_exp ienv arg + | Texp_variant (_, Some (arg, _)) -> + check_uniqueness_exp ~overwrite:None ienv arg | Texp_record { fields; extended_expression } -> let value, uf_ext = match extended_expression with @@ -1363,7 +2129,11 @@ let rec check_uniqueness_exp (ienv : Ienv.t) exp : UF.t = unique_use in Value.mark_maybe_unique value - | _, Overridden (_, e) -> check_uniqueness_exp ienv e) + | l, Overridden (_, e) -> + check_uniqueness_exp + ~overwrite: + (descend (Projection.Record_field l.lbl_name) overwrite) + ienv e) fields in UF.par uf_ext (UF.pars (Array.to_list uf_fields)) @@ -1372,61 +2142,65 @@ let rec check_uniqueness_exp (ienv : Ienv.t) exp : UF.t = UF.seq uf (Value.mark_maybe_unique value) | Texp_setfield (rcd, _, _, _, arg) -> let value, uf_rcd = check_uniqueness_exp_as_value ienv rcd in - let uf_arg = check_uniqueness_exp ienv arg in + let uf_arg = check_uniqueness_exp ~overwrite:None ienv arg in let uf_write = Value.mark_implicit_borrow_memory_address Write value in - UF.pars [uf_rcd; uf_arg; uf_write] + let uf_tag = Value.invalidate_tag value in + UF.pars [uf_rcd; uf_arg; uf_write; uf_tag] | Texp_array (_, _, es, _) -> - UF.pars (List.map (fun e -> check_uniqueness_exp ienv e) es) + UF.pars (List.map (fun e -> check_uniqueness_exp ~overwrite:None ienv e) es) | Texp_ifthenelse (if_, then_, else_opt) -> (* if' is only borrowed, not used; but probably doesn't matter because of mode crossing *) - let uf_cond = check_uniqueness_exp ienv if_ in - let uf_then = check_uniqueness_exp ienv then_ in + let uf_cond = check_uniqueness_exp ~overwrite:None ienv if_ in + let uf_then = check_uniqueness_exp ~overwrite:None ienv then_ in let uf_else = match else_opt with - | Some else_ -> check_uniqueness_exp ienv else_ + | Some else_ -> check_uniqueness_exp ~overwrite:None ienv else_ | None -> UF.unused in UF.seq uf_cond (UF.choose uf_then uf_else) | Texp_sequence (e0, _, e1) -> - let uf0 = check_uniqueness_exp ienv e0 in - let uf1 = check_uniqueness_exp ienv e1 in + let uf0 = check_uniqueness_exp ~overwrite:None ienv e0 in + let uf1 = check_uniqueness_exp ~overwrite:None ienv e1 in UF.seq uf0 uf1 | Texp_while { wh_cond; wh_body; _ } -> - let uf_cond = check_uniqueness_exp ienv wh_cond in - let uf_body = check_uniqueness_exp ienv wh_body in + let uf_cond = check_uniqueness_exp ~overwrite:None ienv wh_cond in + let uf_body = check_uniqueness_exp ~overwrite:None ienv wh_body in UF.seq uf_cond uf_body | Texp_list_comprehension { comp_body; comp_clauses } -> - let uf_body = check_uniqueness_exp ienv comp_body in + let uf_body = check_uniqueness_exp ~overwrite:None ienv comp_body in let uf_clauses = check_uniqueness_comprehensions ienv comp_clauses in UF.par uf_body uf_clauses | Texp_array_comprehension (_, _, { comp_body; comp_clauses }) -> - let uf_body = check_uniqueness_exp ienv comp_body in + let uf_body = check_uniqueness_exp ~overwrite:None ienv comp_body in let uf_clauses = check_uniqueness_comprehensions ienv comp_clauses in UF.par uf_body uf_clauses | Texp_for { for_from; for_to; for_body; _ } -> - let uf_from = check_uniqueness_exp ienv for_from in - let uf_to = check_uniqueness_exp ienv for_to in - let uf_body = check_uniqueness_exp ienv for_body in + let uf_from = check_uniqueness_exp ~overwrite:None ienv for_from in + let uf_to = check_uniqueness_exp ~overwrite:None ienv for_to in + let uf_body = check_uniqueness_exp ~overwrite:None ienv for_body in UF.seq (UF.par uf_from uf_to) uf_body - | Texp_send (e, _, _) -> check_uniqueness_exp ienv e + | Texp_send (e, _, _) -> check_uniqueness_exp ~overwrite:None ienv e | Texp_new _ -> UF.unused | Texp_instvar _ -> UF.unused - | Texp_setinstvar (_, _, _, e) -> check_uniqueness_exp ienv e + | Texp_setinstvar (_, _, _, e) -> check_uniqueness_exp ~overwrite:None ienv e | Texp_override (_, ls) -> - UF.pars (List.map (fun (_, _, e) -> check_uniqueness_exp ienv e) ls) + UF.pars + (List.map + (fun (_, _, e) -> check_uniqueness_exp ~overwrite:None ienv e) + ls) | Texp_letmodule (_, _, _, mod_expr, body) -> let uf_mod = mark_aliased_open_variables ienv (fun iter -> iter.module_expr iter mod_expr) mod_expr.mod_loc in - let uf_body = check_uniqueness_exp ienv body in + let uf_body = check_uniqueness_exp ~overwrite:None ienv body in UF.seq uf_mod uf_body - | Texp_letexception (_, e) -> check_uniqueness_exp ienv e - | Texp_assert (e, _) -> check_uniqueness_exp ienv e + | Texp_letexception (_, e) -> check_uniqueness_exp ~overwrite:None ienv e + | Texp_assert (e, _) -> check_uniqueness_exp ~overwrite:None ienv e | Texp_lazy e -> - let uf = check_uniqueness_exp ienv e in + let uf = check_uniqueness_exp ~overwrite:None ienv e in lift_implicit_borrowing uf | Texp_object (cls_struc, _) -> (* the object (methods, values) will be type-checked by Typeclass, @@ -1458,11 +2232,32 @@ let rec check_uniqueness_exp (ienv : Ienv.t) exp : UF.t = (fun iter -> iter.open_declaration iter open_decl) open_decl.open_loc in - UF.seq uf (check_uniqueness_exp ienv e) - | Texp_probe { handler } -> check_uniqueness_exp ienv handler + UF.seq uf (check_uniqueness_exp ~overwrite:None ienv e) + | Texp_probe { handler } -> check_uniqueness_exp ~overwrite:None ienv handler | Texp_probe_is_enabled _ -> UF.unused - | Texp_exclave e -> check_uniqueness_exp ienv e + | Texp_exclave e -> check_uniqueness_exp ~overwrite:None ienv e | Texp_src_pos -> UF.unused + | Texp_overwrite (e1, e2) -> + let value, uf = check_uniqueness_exp_as_value ienv e1 in + let uf_tag = + match e2.exp_desc with + | Texp_construct (lbl, cd, _, _) -> + Value.overwrite_tag { tag = cd.cstr_tag; name_for_error = lbl } value + | Texp_record _ | Texp_tuple _ -> UF.unused + | _ -> + Misc.fatal_error "Uniqueness analysis: overwrite of unexpected term" + in + let uf_body = check_uniqueness_exp ~overwrite:(Value.paths value) ienv e2 in + (* We first evaluate the body and then perform the overwrite: *) + UF.seqs [uf; uf_tag; uf_body; Value.mark_consumed_memory_address value] + | Texp_hole use -> ( + match overwrite with + | None -> assert false + | Some p -> + let occ = Occurrence.mk exp.exp_loc in + Paths.mark + (Usage.maybe_unique use occ) + Learned_tags.empty Overwrites.empty p) (** Corresponds to the first mode. @@ -1504,11 +2299,14 @@ and check_uniqueness_exp_as_value ienv exp : Value.t * UF.t = | Non_boxing unique_use -> UF.unused, Value.existing paths unique_use occ | Boxing (_, unique_use) -> - Paths.mark (Usage.maybe_unique unique_use occ) paths, Value.fresh + ( Paths.mark + (Usage.maybe_unique unique_use occ) + Learned_tags.empty Overwrites.empty paths, + Value.fresh ) in value, UF.seqs [uf; uf_read; uf_boxing]) (* CR-someday anlorenzen: This could also support let-bindings. *) - | _ -> Value.fresh, check_uniqueness_exp ienv exp + | _ -> Value.fresh, check_uniqueness_exp ~overwrite:None ienv exp (** take typed expression, do some parsing and returns [value_to_match] *) and check_uniqueness_exp_for_match ienv exp : value_to_match * UF.t = @@ -1542,18 +2340,21 @@ and check_uniqueness_value_bindings ienv vbs = check_uniqueness_exp_for_match ienv vb.vb_expr in let ienv, uf_pat = pattern_match vb.vb_pat value in + (* We ignore the tags from value bindings *) + let uf_pat, _tags = UF.split_usage_tags uf_pat in ienv, UF.seq uf_value uf_pat) vbs) in Ienv.Extension.conjuncts exts, UF.pars uf_vbs -(* type signature needed because high-ranked *) +(* type signature needed because invoked on both value and computation patterns *) and check_uniqueness_cases_gen : 'a. ('a Typedtree.general_pattern -> _ -> _) -> _ -> _ -> 'a case list -> _ = fun pat_match ienv value cases -> - (* In the following we imitate how data are accessed at runtime for cases *) - (* we first evaluate all LHS including all the guards, in parallel *) + (* At first, we keep the information from patterns, guards and branches + separate. We only use the Ienv from the patterns in the guards and + branches. *) let exts, uf_pats = List.split (List.map @@ -1562,18 +2363,29 @@ and check_uniqueness_cases_gen : let uf_guard = match case.c_guard with | None -> UF.unused - | Some g -> check_uniqueness_exp (Ienv.extend ienv ext) g + | Some g -> + check_uniqueness_exp ~overwrite:None (Ienv.extend ienv ext) g in - ext, UF.par uf_lhs uf_guard) + ext, (uf_lhs, uf_guard)) cases) in - (* we then evaluate all RHS, in _parallel_ *) let uf_cases = List.map2 - (fun ext case -> check_uniqueness_exp (Ienv.extend ienv ext) case.c_rhs) + (fun ext case -> + check_uniqueness_exp ~overwrite:None (Ienv.extend ienv ext) case.c_rhs) exts cases in - UF.seq (UF.pars uf_pats) (UF.chooses uf_cases) + let uf_lhss, uf_guards = List.split uf_pats in + let uf_lhss_usages, uf_lhss_tags = + List.split (List.map UF.split_usage_tags uf_lhss) + in + (* We combine patterns as follows: We assume that the patterns and guards + could be evaluated in any order. This is necessary since the pattern-match + compiler might permute them. After this stage, only one of the branches is + evaluated. *) + UF.seq + (UF.pars (List.map2 UF.par uf_lhss_usages uf_guards)) + (UF.chooses (List.map2 UF.match_with_learned_tags uf_lhss_tags uf_cases)) and check_uniqueness_cases ienv value cases = check_uniqueness_cases_gen pattern_match ienv value cases @@ -1586,7 +2398,7 @@ and check_uniqueness_comprehensions ienv cs = (List.map (fun c -> match c with - | Texp_comp_when e -> check_uniqueness_exp ienv e + | Texp_comp_when e -> check_uniqueness_exp ~overwrite:None ienv e | Texp_comp_for cbs -> check_uniqueness_comprehension_clause_binding ienv cbs) cs) @@ -1597,10 +2409,11 @@ and check_uniqueness_comprehension_clause_binding ienv cbs = (fun cb -> match cb.comp_cb_iterator with | Texp_comp_range { start; stop; _ } -> - let uf_start = check_uniqueness_exp ienv start in - let uf_stop = check_uniqueness_exp ienv stop in + let uf_start = check_uniqueness_exp ~overwrite:None ienv start in + let uf_stop = check_uniqueness_exp ~overwrite:None ienv stop in UF.par uf_start uf_stop - | Texp_comp_in { sequence; _ } -> check_uniqueness_exp ienv sequence) + | Texp_comp_in { sequence; _ } -> + check_uniqueness_exp ~overwrite:None ienv sequence) cbs) and check_uniqueness_binding_op ienv bo = @@ -1610,19 +2423,27 @@ and check_uniqueness_binding_op ienv bo = | Some value -> Value.mark_maybe_unique value | None -> UF.unused in - let uf_exp = check_uniqueness_exp ienv bo.bop_exp in + let uf_exp = check_uniqueness_exp ~overwrite:None ienv bo.bop_exp in UF.par uf_path uf_exp let check_uniqueness_exp exp = - let _ = check_uniqueness_exp Ienv.empty exp in + let uf = check_uniqueness_exp ~overwrite:None Ienv.empty exp in + UF.check_no_remaining_overwritten_as uf; () let check_uniqueness_value_bindings vbs = - let _ = check_uniqueness_value_bindings Ienv.empty vbs in + let _, uf = check_uniqueness_value_bindings Ienv.empty vbs in + UF.check_no_remaining_overwritten_as uf; () let report_multi_use inner first_is_of_second = - let { Usage.cannot_force = { occ; axis }; there; first_or_second } = inner in + let { Usage.cannot_force = { occ; axis }; + there; + first_or_second; + access_order + } = + inner + in let here_usage = "used" in let there_usage = match there with @@ -1652,28 +2473,28 @@ let report_multi_use inner first_is_of_second = | Descendant _ -> "part of it" | Ancestor _ -> "it is part of a value that" in + let access_order = + match access_order with + | Par -> "is already being" + | Seq -> "has already been" + in (* English is sadly not very composible, we write out all four cases manually *) let error = match first_or_second, axis with | First, Uniqueness -> - Format.dprintf - "This value is %s here,@ but %s has already been %s as unique:" - second_usage first_is_of_second first_usage + Format.dprintf "This value is %s here,@ but %s %s %s as unique:" + second_usage first_is_of_second access_order first_usage | First, Linearity -> Format.dprintf - "This value is %s here,@ but %s is defined as once and has already \ - been %s:" - second_usage first_is_of_second first_usage + "This value is %s here,@ but %s is defined as once and %s %s:" + second_usage first_is_of_second access_order first_usage | Second, Uniqueness -> - Format.dprintf - "This value is %s here as unique,@ but %s has already been %s:" - second_usage first_is_of_second first_usage + Format.dprintf "This value is %s here as unique,@ but %s %s %s:" + second_usage first_is_of_second access_order first_usage | Second, Linearity -> - Format.dprintf - "This value is defined as once and %s here,@ but %s has already been \ - %s:" - second_usage first_is_of_second first_usage + Format.dprintf "This value is defined as once and %s here,@ but %s %s %s:" + second_usage first_is_of_second access_order first_usage in let sub = [Location.msg ~loc:first.loc ""] in Location.errorf ~loc:second.loc ~sub "@[%t@]" error @@ -1694,12 +2515,33 @@ let report_boundary cannot_force reason = Location.errorf ~loc:occ.loc "@[%s.\nHint: This value comes from %s.@]" error reason +let report_tag_change (err : Overwrites.error) = + match err with + | Changed_tag { old_tag; new_tag } -> + let new_tag_txt = + Format.dprintf "%a" Pprintast.longident new_tag.name_for_error.txt + in + let old_tag_txt = + match old_tag with + | Old_tag_unknown -> Format.dprintf "is unknown." + | Old_tag_was l -> + Format.dprintf "is %a." Pprintast.longident l.name_for_error.txt + | Old_tag_mutated access_order -> ( + match access_order with + | Par -> Format.dprintf "is being changed through mutation." + | Seq -> Format.dprintf "was changed through mutation.") + in + Location.errorf ~loc:new_tag.name_for_error.loc + "@[Overwrite may not change the tag to %t.\n\ + Hint: The old tag of this allocation %t@]" new_tag_txt old_tag_txt + let report_error err = Printtyp.wrap_printing_env ~error:true Env.empty (fun () -> match err with | Usage { inner; first_is_of_second } -> report_multi_use inner first_is_of_second - | Boundary { cannot_force; reason } -> report_boundary cannot_force reason) + | Boundary { cannot_force; reason } -> report_boundary cannot_force reason + | Overwrite_changed_tag err -> report_tag_change err) let () = Location.register_error_of_exn (function diff --git a/typing/uniqueness_analysis.mli b/typing/uniqueness_analysis.mli index 6a2f0892388..06a62504179 100644 --- a/typing/uniqueness_analysis.mli +++ b/typing/uniqueness_analysis.mli @@ -22,3 +22,36 @@ val check_uniqueness_exp : expression -> unit (* Check that idents which are used more than once, are not used with mode unique. *) val check_uniqueness_value_bindings : value_binding list -> unit + +(* These definitions are just to allow printing in the debugger *) +module type P := sig + type t + + val print : Format.formatter -> t -> unit +end + +module Maybe_unique : P + +module Maybe_aliased : P + +module Aliased : P + +module Usage : P + +module Tag : P + +module Projection : P + +module Usage_tree : P + +module Usage_forest : P + +module Paths : P + +module Value : P + +module Ienv : sig + include P + + module Extension : P +end diff --git a/typing/untypeast.ml b/typing/untypeast.ml index df7af0077cc..cc31f4ee5f4 100644 --- a/typing/untypeast.ml +++ b/typing/untypeast.ml @@ -696,6 +696,9 @@ let expression sub exp = pexp_attributes = []; }, [Nolabel, sub.expr sub exp]) | Texp_src_pos -> Pexp_extension ({ txt = "src_pos"; loc }, PStr []) + | Texp_overwrite (exp1, exp2) -> + Pexp_overwrite(sub.expr sub exp1, sub.expr sub exp2) + | Texp_hole _ -> Pexp_hole in List.fold_right (exp_extra sub) exp.exp_extra (Exp.mk ~loc ~attrs desc) diff --git a/typing/value_rec_check.ml b/typing/value_rec_check.ml index 32c742a2512..5ef1cd468cf 100644 --- a/typing/value_rec_check.ml +++ b/typing/value_rec_check.ml @@ -191,7 +191,11 @@ let classify_expression : Typedtree.expression -> sd = Static | Texp_unboxed_tuple _ -> - Dynamic + Dynamic + + | Texp_overwrite _ + | Texp_hole _ -> + Dynamic (* Disallowed for now *) | Texp_for _ | Texp_setfield _ @@ -989,6 +993,19 @@ let rec expression : Typedtree.expression -> term_judg = | Texp_probe_is_enabled _ -> empty | Texp_exclave e -> expression e | Texp_src_pos -> empty + | Texp_overwrite (exp1, exp2) -> + (* This is untested, since we currently mark Texp_overwrite as Dynamic and + the analysis always stops if there is an overwrite_ in a recursive expression. + We dereference the cell to be overwritten, since it would not be sound to + overwrite a cell that is not yet constructed. The new value to be written into + the cell may itself be recursive. We do not put a guard on here, but this is done + by the tuple/record/constructor that is contained in the overwritten expression. + *) + join [ + expression exp1 << Dereference; + expression exp2 + ] + | Texp_hole _ -> empty (* Function bodies. G |-{body} b : m