diff --git a/file_formats/cmt_format.ml b/file_formats/cmt_format.ml index cc98af65a38..7829264ebc0 100644 --- a/file_formats/cmt_format.ml +++ b/file_formats/cmt_format.ml @@ -247,7 +247,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 d9c4237e5b1..0d59d0d0647 100644 --- a/lambda/translcore.ml +++ b/lambda/translcore.ml @@ -1226,6 +1226,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 d92d3835a1e..458c71f2a8a 100644 --- a/parsing/ast_helper.ml +++ b/parsing/ast_helper.ml @@ -250,6 +250,8 @@ 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 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 b660b633101..7c82178c063 100644 --- a/parsing/ast_helper.mli +++ b/parsing/ast_helper.mli @@ -215,6 +215,8 @@ 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 -> expression -> expression -> expression + val hole : ?loc:loc -> ?attrs:attrs -> unit -> expression val case: pattern -> ?guard:expression -> expression -> case val binding_op: str -> pattern -> expression -> loc -> binding_op diff --git a/parsing/ast_iterator.ml b/parsing/ast_iterator.ml index 1752b365fec..08c6581aea5 100644 --- a/parsing/ast_iterator.ml +++ b/parsing/ast_iterator.ml @@ -535,6 +535,8 @@ module E = struct | Pexp_unreachable -> () | Pexp_stack e -> sub.expr sub e | Pexp_comprehension e -> iter_comp_exp 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} = iter_loc sub pbop_op; diff --git a/parsing/ast_mapper.ml b/parsing/ast_mapper.ml index b04728903bd..5bbedf1be5e 100644 --- a/parsing/ast_mapper.ml +++ b/parsing/ast_mapper.ml @@ -613,6 +613,8 @@ 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 (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} = let open Exp in diff --git a/parsing/depend.ml b/parsing/depend.ml index 69fba756745..f975418baed 100644 --- a/parsing/depend.ml +++ b/parsing/depend.ml @@ -316,6 +316,8 @@ let rec add_expr bv exp = end | Pexp_extension e -> handle_extension e | Pexp_stack e -> 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/language_extension.ml b/parsing/language_extension.ml index 50b504256fc..691d24cd0fe 100644 --- a/parsing/language_extension.ml +++ b/parsing/language_extension.ml @@ -63,6 +63,7 @@ let get_level_ops : type a. a t -> (module Extension_level with type t = a) = | Comprehensions -> (module Unit) | Mode -> (module Maturity) | Unique -> (module Maturity) + | Overwriting -> (module Unit) | Include_functor -> (module Unit) | Polymorphic_parameters -> (module Unit) | Immutable_arrays -> (module Unit) @@ -82,7 +83,7 @@ let get_level_ops : type a. a t -> (module Extension_level with type t = a) = But we've decided to punt on this issue in the short term. *) let is_erasable : type a. a t -> bool = function - | Mode | Unique | Layouts -> true + | Mode | Unique | Overwriting | Layouts -> true | Comprehensions | Include_functor | Polymorphic_parameters | Immutable_arrays | Module_strengthening | SIMD | Labeled_tuples | Small_numbers | Instances -> false @@ -98,6 +99,7 @@ module Exist_pair = struct | Pair (Comprehensions, ()) -> Beta | Pair (Mode, m) -> m | Pair (Unique, m) -> m + | Pair (Overwriting, ()) -> Alpha | Pair (Include_functor, ()) -> Stable | Pair (Polymorphic_parameters, ()) -> Stable | Pair (Immutable_arrays, ()) -> Stable @@ -120,7 +122,7 @@ module Exist_pair = struct | Pair ( (( Comprehensions | Include_functor | Polymorphic_parameters | Immutable_arrays | Module_strengthening | Labeled_tuples - | Instances ) as ext), + | Instances | Overwriting ) as ext), _ ) -> to_string ext @@ -137,6 +139,7 @@ module Exist_pair = struct | "unique" -> Some (Pair (Unique, Stable)) | "unique_beta" -> Some (Pair (Unique, Beta)) | "unique_alpha" -> Some (Pair (Unique, Alpha)) + | "overwriting" -> Some (Pair (Overwriting, ())) | "include_functor" -> Some (Pair (Include_functor, ())) | "polymorphic_parameters" -> Some (Pair (Polymorphic_parameters, ())) | "immutable_arrays" -> Some (Pair (Immutable_arrays, ())) @@ -161,6 +164,7 @@ let all_extensions = [ Pack Comprehensions; Pack Mode; Pack Unique; + Pack Overwriting; Pack Include_functor; Pack Polymorphic_parameters; Pack Immutable_arrays; @@ -198,6 +202,7 @@ let equal_t (type a b) (a : a t) (b : b t) : (a, b) Misc.eq option = | Comprehensions, Comprehensions -> Some Refl | Mode, Mode -> Some Refl | Unique, Unique -> Some Refl + | Overwriting, Overwriting -> Some Refl | Include_functor, Include_functor -> Some Refl | Polymorphic_parameters, Polymorphic_parameters -> Some Refl | Immutable_arrays, Immutable_arrays -> Some Refl @@ -207,7 +212,7 @@ let equal_t (type a b) (a : a t) (b : b t) : (a, b) Misc.eq option = | Labeled_tuples, Labeled_tuples -> Some Refl | Small_numbers, Small_numbers -> Some Refl | Instances, Instances -> Some Refl - | ( ( Comprehensions | Mode | Unique | Include_functor + | ( ( Comprehensions | Mode | Unique | Overwriting | Include_functor | Polymorphic_parameters | Immutable_arrays | Module_strengthening | Layouts | SIMD | Labeled_tuples | Small_numbers | Instances ), _ ) -> diff --git a/parsing/language_extension.mli b/parsing/language_extension.mli index 1282e251cb8..5ce88e276f2 100644 --- a/parsing/language_extension.mli +++ b/parsing/language_extension.mli @@ -21,6 +21,7 @@ type 'a t = 'a Language_extension_kernel.t = | Comprehensions : unit t | Mode : maturity t | Unique : maturity t + | Overwriting : unit t | Include_functor : unit t | Polymorphic_parameters : unit t | Immutable_arrays : unit t diff --git a/parsing/lexer.mll b/parsing/lexer.mll index 0252e0c33dd..4cfada207e6 100644 --- a/parsing/lexer.mll +++ b/parsing/lexer.mll @@ -80,6 +80,7 @@ let keyword_table = "once_", ONCE; "open", OPEN; "or", OR; + "overwrite_", OVERWRITE; (* "parser", PARSER; *) "private", PRIVATE; "rec", REC; diff --git a/parsing/location.ml b/parsing/location.ml index a6a0271c421..35c8faecfe4 100644 --- a/parsing/location.ml +++ b/parsing/location.ml @@ -1101,3 +1101,7 @@ let () = let raise_errorf ?(loc = none) ?(sub = []) = Format.kdprintf (fun txt -> raise (Error (mkerror loc sub txt))) + +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 ff4373462fa..abe9cf8d4e7 100644 --- a/parsing/location.mli +++ b/parsing/location.mli @@ -396,3 +396,6 @@ val raise_errorf: ?loc:t -> ?sub:msg list -> val report_exception: formatter -> exn -> unit (** Reraise the exception if it is unknown. *) + +(** CR uniqueness: remove this once overwriting is fully implemented *) +val todo_overwrite_not_implemented : ?kind:string -> t -> 'a diff --git a/parsing/parser.mly b/parsing/parser.mly index 6976ac419e4..d6cf9bd64e0 100644 --- a/parsing/parser.mly +++ b/parsing/parser.mly @@ -1016,6 +1016,7 @@ let maybe_pmod_constraint mode expr = %token OPEN "open" %token OPTLABEL "?label:" (* just an example *) %token OR "or" +%token OVERWRITE "overwrite_" /* %token PARSER "parser" */ %token PERCENT "%" %token PLUS "+" @@ -2818,10 +2819,8 @@ fun_expr: { mk_indexop_expr user_indexing_operators ~loc:$sloc $1 } | fun_expr attribute { Exp.attr $1 $2 } -/* BEGIN AVOID */ | UNDERSCORE - { not_expecting $loc($1) "wildcard \"_\"" } -/* END AVOID */ + { mkexp ~loc:$sloc Pexp_hole } | mode=mode_legacy exp=seq_expr { mkexp_with_modes ~loc:$sloc ~exp ~cty:None ~modes:[mode] } | EXCLAVE seq_expr @@ -2848,6 +2847,8 @@ fun_expr: { Pexp_try($3, $5), $2 } | TRY ext_attributes seq_expr WITH error { syntax_error() } + | 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 } | IF ext_attributes seq_expr THEN expr diff --git a/parsing/parsetree.mli b/parsing/parsetree.mli index 53e2809ce61..d00cb264a6c 100644 --- a/parsing/parsetree.mli +++ b/parsing/parsetree.mli @@ -507,6 +507,8 @@ and expression_desc = - [BODY] is an expression. - [CLAUSES] is a series of [comprehension_clause]. *) + | Pexp_overwrite of expression * expression (** overwrite_ exp with exp *) + | Pexp_hole (** _ *) and case = { diff --git a/parsing/pprintast.ml b/parsing/pprintast.ml index 4f09fe078e1..4705108989a 100644 --- a/parsing/pprintast.ml +++ b/parsing/pprintast.ml @@ -1095,6 +1095,12 @@ and expression ctxt f x = (expression ctxt) body | Pexp_extension e -> extension ctxt f e | Pexp_unreachable -> pp f "." + | Pexp_overwrite (e1, e2) -> + (* Similar to the case of [Pexp_stack] *) + pp f "@[overwrite_@ %a@ with@ %a@]" + (expression2 reset_ctxt) e1 + (expression2 reset_ctxt) e2 + | Pexp_hole -> pp f "_" | _ -> expression1 ctxt f x and expression1 ctxt f x = diff --git a/parsing/printast.ml b/parsing/printast.ml index ca734e1ced4..ba4bf6b2964 100644 --- a/parsing/printast.ml +++ b/parsing/printast.ml @@ -448,6 +448,12 @@ and expression i ppf x = | Pexp_comprehension c -> line i ppf "Pexp_comprehension\n"; comprehension_expression i ppf c + | 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" and comprehension_expression i ppf = function | Pcomp_array_comprehension (m, c) -> diff --git a/printer/printast_with_mappings.ml b/printer/printast_with_mappings.ml index 8fd16dfcc82..d40def98a8a 100644 --- a/printer/printast_with_mappings.ml +++ b/printer/printast_with_mappings.ml @@ -472,6 +472,12 @@ and expression i ppf x = | Pexp_comprehension c -> line i ppf "Pexp_comprehension\n"; comprehension_expression i ppf c + | 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" ) and comprehension_expression i ppf = function diff --git a/testsuite/tests/parsetree/source_jane_street.ml b/testsuite/tests/parsetree/source_jane_street.ml index 5c232c039af..e42376e9372 100644 --- a/testsuite/tests/parsetree/source_jane_street.ml +++ b/testsuite/tests/parsetree/source_jane_street.ml @@ -1201,3 +1201,39 @@ Line 2, characters 18-26: ^^^^^^^^ Error: Mode annotations on modules are not supported yet. |}] + +(***************) +(* Overwriting *) + + +let overwrite_tuple = function + (a, b) as t -> overwrite_ t with (b, _) + +type record = { a : int; b : int } + +let overwrite_record = function + { a; b } as t -> overwrite_ t with { b = a; a = _ } + +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 + C { a; b } as t -> overwrite_ t with C { b = a; a = _ } + +let overwrite_constructor = function + C { a; b } as t -> overwrite_ t with C { b = a } +[%%expect{| +Line 2, characters 19-43: +2 | (a, b) as t -> overwrite_ t with (b, _) + ^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] diff --git a/testsuite/tests/typing-layouts-unboxed-records/typing_misc_unboxed_records.ml b/testsuite/tests/typing-layouts-unboxed-records/typing_misc_unboxed_records.ml index 5837a2fdf85..a15c7fddaa4 100644 --- a/testsuite/tests/typing-layouts-unboxed-records/typing_misc_unboxed_records.ml +++ b/testsuite/tests/typing-layouts-unboxed-records/typing_misc_unboxed_records.ml @@ -125,9 +125,9 @@ Error: Unbound record field "Complex.z" (* PR#6608 *) #{ true with contents = 0 };; [%%expect{| -Line 1, characters 3-7: +Line 1, characters 0-27: 1 | #{ true with contents = 0 };; - ^^^^ + ^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: This expression has type "bool" which is not a unboxed record type. |}];; diff --git a/testsuite/tests/typing-misc/records.ml b/testsuite/tests/typing-misc/records.ml index 9c277848df6..100d287f12f 100644 --- a/testsuite/tests/typing-misc/records.ml +++ b/testsuite/tests/typing-misc/records.ml @@ -134,9 +134,9 @@ Error: Unbound record field "Complex.z" (* PR#6608 *) { true with contents = 0 };; [%%expect{| -Line 1, characters 2-6: +Line 1, characters 0-26: 1 | { true with contents = 0 };; - ^^^^ + ^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: This expression has type "bool" which is not a record type. |}];; diff --git a/testsuite/tests/typing-misc/wrong_kind.ml b/testsuite/tests/typing-misc/wrong_kind.ml index 2c9c70200e2..958b5c932e3 100644 --- a/testsuite/tests/typing-misc/wrong_kind.ml +++ b/testsuite/tests/typing-misc/wrong_kind.ml @@ -232,9 +232,9 @@ Error: This expression has type "'a -> Record.t" which is not a record type. let () = ignore { (Record.get ()) with a = 5 };; [%%expect{| -Line 2, characters 11-26: +Line 2, characters 9-39: 2 | ignore { (Record.get ()) with a = 5 };; - ^^^^^^^^^^^^^^^ + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: This expression has type "'a -> Record.t" which is not a record type. |}] diff --git a/testsuite/tests/typing-unique/overwriting.ml b/testsuite/tests/typing-unique/overwriting.ml new file mode 100644 index 00000000000..a653ad412c8 --- /dev/null +++ b/testsuite/tests/typing-unique/overwriting.ml @@ -0,0 +1,1181 @@ +(* TEST + flags += "-extension-universe alpha"; + expect; +*) + +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 +[%%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 : 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 + +|}] + +(*************************************) +(* 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 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) + that are not overwritten. We test 2^3 configurations: + - the overwritten value can be local/global + - the resulting value can be local/global + - the value written in the record can be local/global *) + +let gc_soundness_bug (local_ unique_ r) (local_ x) = + exclave_ overwrite_ r with { x } +[%%expect{| +Line 2, characters 31-32: +2 | exclave_ overwrite_ r with { x } + ^ +Error: This value escapes its region. +|}] + +let disallowed_by_locality (local_ unique_ r) (local_ x) = + overwrite_ r with { x } +[%%expect{| +Line 2, characters 22-23: +2 | overwrite_ r with { x } + ^ +Error: This value escapes its region. +|}] + +let gc_soundness_bug (unique_ r) (local_ x) = + exclave_ overwrite_ r with { x } +[%%expect{| +Line 2, characters 31-32: +2 | exclave_ overwrite_ r with { x } + ^ +Error: This value escapes its region. +|}] + +let disallowed_by_locality (unique_ r) (local_ x) = + overwrite_ r with { x } +[%%expect{| +Line 2, characters 22-23: +2 | overwrite_ r with { x } + ^ +Error: This value escapes its region. +|}] + +let gc_soundness_no_bug (local_ unique_ r) x = + exclave_ overwrite_ r with { x } +[%%expect{| +Line 2, characters 11-34: +2 | exclave_ overwrite_ r with { x } + ^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +(* 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 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 Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let gc_soundness_no_bug (unique_ r) x = + overwrite_ r with { x } +[%%expect{| +Line 2, characters 2-25: +2 | overwrite_ r with { x } + ^^^^^^^^^^^^^^^^^^^^^^^ +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. +|}] + +(*****************************) +(* Overwriting with mutation *) + +(* Currently all tests in this section fail because mutable record fields + are always aliased. But in the future, this will change! + When mutable record fields can be unique, we have to ensure that users + cannot change the tag using mutation before overwriting a cell with the + knowledge of the old tag. We took that into account when designing this + feature and all tests here should work correctly in that case. + You can find the expected test outputs at PR3157. *) + +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{| +Line 2, characters 10-13: +2 | unique_ r.m + ^^^ +Error: This value is "aliased" but expected to be "unique". +|}] + +let tag_of_mutable_field r = + match r with + | { m = OptionA s } -> + overwrite_ r.m with OptionA s + | _ -> OptionB "" +[%%expect{| +Line 4, characters 15-18: +4 | overwrite_ r.m with OptionA s + ^^^ +Error: This value is "aliased" but expected to be "unique". +|}] + +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 15-18: +5 | overwrite_ r.m with OptionA s + ^^^ +Error: This value is "aliased" but expected to be "unique". +|}] + +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 15-18: +5 | overwrite_ r.m with OptionA s + ^^^ +Error: This value is "aliased" but expected to be "unique". +|}] + +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 15-20: +5 | overwrite_ r.m.x with OptionA s + ^^^^^ +Error: This value is "aliased" but expected to be "unique". +|}] + +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 35-38: +4 | (r.m <- OptionB s), overwrite_ r.m with OptionA s + ^^^ +Error: This value is "aliased" but expected to be "unique". +|}] + +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 43-48: +4 | (r.m <- { x = OptionB s }), overwrite_ r.m.x with OptionA s + ^^^^^ +Error: This value is "aliased" but expected to be "unique". +|}] + +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 28-31: +5 | else overwrite_ r.m with OptionA s + ^^^ +Error: This value is "aliased" but expected to be "unique". +|}] + +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 20-25: +5 | else overwrite_ r.m.x with OptionA s + ^^^^^ +Error: This value is "aliased" but expected to be "unique". +|}] + +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 15-18: +5 | overwrite_ r.m with OptionA s + ^^^ +Error: This value is "aliased" but expected to be "unique". +|}] + +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 15-20: +5 | overwrite_ r.m.x with OptionA s + ^^^^^ +Error: This value is "aliased" but expected to be "unique". +|}] + + +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 17-20: +7 | overwrite_ r.m with OptionB s + ^^^ +Error: This value is "aliased" but expected to be "unique". +|}] + +(********************************) +(* 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 new file mode 100644 index 00000000000..2018d2ed4af --- /dev/null +++ b/testsuite/tests/typing-unique/overwriting_lift_constants.ml @@ -0,0 +1,83 @@ +(* TEST + flags += "-extension-universe alpha"; + expect; + reference = "${test_source_directory}/overwriting_lift_constants.reference"; +*) + +(* CR uniqueness: To run this test replace 'expect' above by 'native' + and delete the expect block. *) + +type point = { mutable dim : int; x : float; y : float; z : float } + +(* First: check that overwriting happens at all *) +let unsafe_dup : 'a @ unique -> 'a * 'a @ unique = + Obj.magic (fun x -> (x, x)) + +let check_overwriting_enabled () = + let (p, q) = unsafe_dup { dim = 3; x = 1.0; y = 2.0; z = 3.0 } in + let p = overwrite_ p with { dim = 4; x = 1.0; y = 2.0; z = 3.0 } in + p == q + +(* This file tests how constants are lifted out. + Unique constants can not be lifted out since they + might be overwritten but all other constants should still + be lifted out. + Since this pass is not yet implemented, I have added the + expected result from the prototype in a comment to each test. +*) + +(* Same test for float blocks *) +type fpoint = { x : float; y : float; z : float } + +let fupdate_with_constant (p : fpoint) = + let q = overwrite_ p with { x = 2.0; y = 3.0; z = 4.0 } in + q + +let test2 () = + let p = { x = 1.0; y = 2.0; z = 3.0 } in + let q = { x = 1.0; y = 2.0; z = 3.0 } in + fupdate_with_constant p == fupdate_with_constant q + +(* The tail of the list should be lifted out *) +let constant_list x = + x :: 2 :: [] + +(* While the head is different, the tails are the same *) +let test3 () = + List.hd (constant_list 1) == List.hd (constant_list 2), + List.tl (constant_list 1) == List.tl (constant_list 2) + +(* Since the tail was marked unique, it can not be lifted out *) +let constant_list_unique x = + let unique_ y = 2 :: [] in x :: y + +let test4 () = + List.hd (constant_list_unique 1) == List.hd (constant_list_unique 2), + List.tl (constant_list_unique 1) == List.tl (constant_list_unique 2) + +(* Since the tail was marked unique, it can not be lifted out *) +let constant_list_unique2 x = + let unique_ z = [] in + let unique_ y = 2 :: z in x :: y + +let test5 () = + List.hd (constant_list_unique2 1) == List.hd (constant_list_unique2 2), + List.tl (constant_list_unique2 1) == List.tl (constant_list_unique2 2) + +let () = + Printf.printf "%B\n" (check_overwriting_enabled ()); + Printf.printf "%B\n" (test2 ()); + Printf.printf "(%B, %B)\n" (test3 ()); + Printf.printf "(%B, %B)\n" (test4 ()); + Printf.printf "(%B, %B)\n" (test5 ()); + +[%%expect{| +type point = { mutable dim : int; x : float; y : float; z : float; } +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 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.reference b/testsuite/tests/typing-unique/overwriting_lift_constants.reference new file mode 100644 index 00000000000..7d564accdeb --- /dev/null +++ b/testsuite/tests/typing-unique/overwriting_lift_constants.reference @@ -0,0 +1,5 @@ +true +true +(false, true) +(false, false) +(false, false) diff --git a/testsuite/tests/typing-unique/overwriting_lift_constants_bug.ml b/testsuite/tests/typing-unique/overwriting_lift_constants_bug.ml new file mode 100644 index 00000000000..ae018fed287 --- /dev/null +++ b/testsuite/tests/typing-unique/overwriting_lift_constants_bug.ml @@ -0,0 +1,70 @@ +(* TEST + flags += "-extension-universe alpha"; + expect; + reference = "${test_source_directory}/overwriting_lift_constants_bug.reference"; +*) + +(* CR uniqueness: To run this test replace 'expect' above by 'native' + and delete the expect block. *) + +type point = { dim : int; x : float; y : float; z : float } + +let constant_lift b = + let unique_ p = { dim = 3; x = 1.0; y = 2.0; z = 3.0 } in + if b then p else overwrite_ p with { x = 2.0 } + +type fpoint = { x : float; y : float; z : float } + +let fconstant_lift b = + let unique_ p = { x = 1.0; y = 2.0; z = 3.0 } in + if b then p else overwrite_ p with { x = 2.0 } + +type mpoint = { dim : int option; x : float#; y : float#; z : float# } + +let mconstant_lift b = + let unique_ p = { dim = Some 3; x = #1.0; y = #2.0; z = #3.0 } in + if b then p else overwrite_ p with { x = #2.0 } + +type ufpoint = { x : float#; y : float#; z : float# } + +let ufconstant_lift b = + let unique_ p = { x = #1.0; y = #2.0; z = #3.0 } in + if b then p else overwrite_ p with { x = #2.0 } + +type utpoint = { xy : #(float * float); z : float } + +let ufconstant_lift b = + let unique_ p = { xy = #(1.0, 2.0); z = 3.0 } in + if b then p else overwrite_ p with { xy = #(2.0, 2.0) } + +let () = + let x = (constant_lift true).x in + let y = (constant_lift false).x in + let z = (constant_lift true).x in + Printf.printf "%f %f %f\n" x y z; + let x = (fconstant_lift true).x in + let y = (fconstant_lift false).x in + let z = (fconstant_lift true).x in + Printf.printf "%f %f %f\n" x y z; + let x = Float_u.to_float (mconstant_lift true).x in + let y = Float_u.to_float (mconstant_lift false).x in + let z = Float_u.to_float (mconstant_lift true).x in + Printf.printf "%f %f %f\n" x y z; + let x = Float_u.to_float (ufconstant_lift true).x in + let y = Float_u.to_float (ufconstant_lift false).x in + let z = Float_u.to_float (ufconstant_lift true).x in + Printf.printf "%f %f %f\n" x y z; + let x = Float_u.to_float (fst (ufconstant_lift true).xy) in + let y = Float_u.to_float (fst (ufconstant_lift false).xy) in + let z = Float_u.to_float (fst (ufconstant_lift true).xy) in + Printf.printf "%f %f %f\n" x y z + +[%%expect{| +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 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.reference b/testsuite/tests/typing-unique/overwriting_lift_constants_bug.reference new file mode 100644 index 00000000000..0e4f622cc78 --- /dev/null +++ b/testsuite/tests/typing-unique/overwriting_lift_constants_bug.reference @@ -0,0 +1,5 @@ +1.000000 2.000000 1.000000 +1.000000 2.000000 1.000000 +1.000000 2.000000 1.000000 +1.000000 2.000000 1.000000 +1.000000 2.000000 1.000000 diff --git a/testsuite/tests/typing-unique/overwriting_map.ml b/testsuite/tests/typing-unique/overwriting_map.ml new file mode 100644 index 00000000000..1d412c3edd7 --- /dev/null +++ b/testsuite/tests/typing-unique/overwriting_map.ml @@ -0,0 +1,40 @@ +(* TEST + flags += "-extension-universe alpha"; + expect; + reference = "${test_source_directory}/overwriting_map.reference"; +*) + +(* CR uniqueness: To run this test replace 'expect' above by 'native' + and delete the expect block. *) + +let rec map f xs = + match xs with + | hd :: tl as xs -> overwrite_ xs with f hd :: map f tl + | [] -> [] + +let () = + let xs = [1;2;3] in + + let baseline_allocation = Gc.allocated_bytes() -. Gc.allocated_bytes() in + let before = Gc.allocated_bytes () in + let _ = Sys.opaque_identity (map (fun x -> x + 1) xs) in + let after = Gc.allocated_bytes () in + let bytes_per_word = Sys.word_size / 8 in + let delta = + int_of_float ((after -. before) -. baseline_allocation) / bytes_per_word + in + let msg = + match delta with + | 0 -> "No Allocation" + | n -> "Allocated " ^ string_of_int n ^ " words" + in + Printf.printf "%15s: %s\n" "List.map" msg + +[%%expect{| +Line 3, characters 22-57: +3 | | hd :: tl as xs -> overwrite_ xs with f hd :: map f tl + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +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.reference b/testsuite/tests/typing-unique/overwriting_map.reference new file mode 100644 index 00000000000..4106527cffb --- /dev/null +++ b/testsuite/tests/typing-unique/overwriting_map.reference @@ -0,0 +1 @@ + List.map: No Allocation 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 e8891c0bc9c..6fed6b1c85d 100644 --- a/testsuite/tests/typing-unique/overwriting_proj_push_down_bug.ml +++ b/testsuite/tests/typing-unique/overwriting_proj_push_down_bug.ml @@ -1,5 +1,5 @@ (* TEST - flags += "-extension unique_alpha "; + flags += "-extension-universe alpha "; flags += "-dlambda"; expect; *) @@ -19,14 +19,15 @@ let aliased_use x = x [%%expect{| (let (aliased_use/280 = (function {nlocal = 0} x/282 x/282)) (apply (field_imm 1 (global Toploop!)) "aliased_use" aliased_use/280)) -val aliased_use : 'a -> 'a = +val aliased_use : ('a : value_or_null). 'a -> 'a @@ global many = |}] let unique_use (unique_ x) = x [%%expect{| (let (unique_use/283 = (function {nlocal = 0} x/285 x/285)) (apply (field_imm 1 (global Toploop!)) "unique_use" unique_use/283)) -val unique_use : 'a @ unique -> 'a = +val unique_use : ('a : value_or_null). 'a @ unique -> 'a @@ global many = + |}] (* This output is fine with overwriting: The [r.y] is not pushed down. *) @@ -47,7 +48,7 @@ let proj_aliased r = (apply aliased_use/280 r/288)) (makeblock 0 ([(consts ()) (non_consts ([0: *, *]))],*) r/290 y/289)))) (apply (field_imm 1 (global Toploop!)) "proj_aliased" proj_aliased/286)) -val proj_aliased : record -> record * string = +val proj_aliased : record -> record * string @@ global many = |}] let proj_unique r = @@ -67,7 +68,7 @@ let proj_unique r = (apply unique_use/283 r/293)) (makeblock 0 ([(consts ()) (non_consts ([0: *, *]))],*) r/295 y/294)))) (apply (field_imm 1 (global Toploop!)) "proj_unique" proj_unique/291)) -val proj_unique : record @ unique -> record * string = +val proj_unique : record @ unique -> record * string @@ global many = |}] (* This output would be unsound if [aliased_use] was able to overwrite [r] @@ -90,7 +91,7 @@ let match_aliased r = (makeblock 0 ([(consts ()) (non_consts ([0: *, *]))],*) r/300 (field_imm 1 r/298))))) (apply (field_imm 1 (global Toploop!)) "match_aliased" match_aliased/296)) -val match_aliased : record -> record * string = +val match_aliased : record -> record * string @@ global many = |}] (* This is sound since we bind [y] before the [unique_use] *) @@ -112,7 +113,7 @@ let match_unique r = (apply unique_use/283 r/304)) (makeblock 0 ([(consts ()) (non_consts ([0: *, *]))],*) r/306 y/305)))) (apply (field_imm 1 (global Toploop!)) "match_unique" match_unique/302)) -val match_unique : record @ unique -> record * string = +val match_unique : record @ unique -> record * string @@ global many = |}] (* Similarly, this would be unsound since Lambda performs a mini ANF pass. *) @@ -138,7 +139,7 @@ let match_mini_anf_aliased r = (field_imm 1 r/310))))) (apply (field_imm 1 (global Toploop!)) "match_mini_anf_aliased" match_mini_anf_aliased/308)) -val match_mini_anf_aliased : record -> record * string = +val match_mini_anf_aliased : record -> record * string @@ global many = |}] (* This is sound since we bind [y] before the [unique_use] *) @@ -164,7 +165,8 @@ let match_mini_anf_unique r = (makeblock 0 ([(consts ()) (non_consts ([0: *, *]))],*) r/323 y/322)))) (apply (field_imm 1 (global Toploop!)) "match_mini_anf_unique" match_mini_anf_unique/318)) -val match_mini_anf_unique : record @ unique -> record * string = +val match_mini_anf_unique : record @ unique -> record * string @@ global many = + |}] let match_anf_aliased r = @@ -194,7 +196,7 @@ let match_anf_aliased r = y/331))))) (apply (field_imm 1 (global Toploop!)) "match_anf_aliased" match_anf_aliased/328)) -val match_anf_aliased : record -> record * string = +val match_anf_aliased : record -> record * string @@ global many = |}] (* This is sound since we bind [y] using [field_mut] *) @@ -226,7 +228,8 @@ let match_anf_unique r = y/343))))) (apply (field_imm 1 (global Toploop!)) "match_anf_unique" match_anf_unique/340)) -val match_anf_unique : record @ unique -> record * string = +val match_anf_unique : record @ unique -> record * string @@ global many = + |}] type tree = @@ -322,18 +325,133 @@ let swap_inner (t : tree) = (exit 19)) with (19) t/360))) (apply (field_imm 1 (global Toploop!)) "swap_inner" swap_inner/358)) -val swap_inner : tree -> 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 new file mode 100644 index 00000000000..8b2ff6eeb5f --- /dev/null +++ b/testsuite/tests/typing-unique/overwriting_syntax.ml @@ -0,0 +1,156 @@ +(* TEST + flags += "-extension-universe alpha"; + 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 *) + +let overwrite_tuple = function + (a, b) as t -> overwrite_ t with (b, _) +[%%expect{| +Line 2, characters 17-41: +2 | (a, b) as t -> overwrite_ t with (b, _) + ^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +type record = { a : int; b : int } + +let overwrite_record = function + { a; b } as t -> overwrite_ t with { b = a; a = _ } +[%%expect{| +type record = { a : int; b : int; } +Line 4, characters 19-53: +4 | { a; b } as t -> overwrite_ t with { b = a; a = _ } + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +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 Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +type constructor = C of { a : int; b : int } + +let overwrite_constructor = function + C { a; b } as t -> overwrite_ t with C { b = a; a = _ } +[%%expect{| +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 Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +let overwrite_constructor = function + C { a; b } as t -> overwrite_ t with C { b = a } +[%%expect{| +Line 2, characters 23-52: +2 | C { a; b } as t -> overwrite_ t with C { b = a } + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +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) as t -> overwrite_ t with `A (b, _) +[%%expect{| +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 + C { a; b } as t -> + match overwrite_ t with C { b = a; a = _ } with + | C {a; b} -> C {a; b} +[%%expect{| +Line 3, characters 10-46: +3 | match overwrite_ t with C { b = a; a = _ } with + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Alert Translcore: Overwrite not implemented. +Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed + +|}] + +(****************) +(* Non-examples *) + +let underscore = _ +[%%expect{| +Line 1, characters 17-18: +1 | let underscore = _ + ^ +Error: wildcard "_" not expected. +|}] + +let underscore_tuple = (_, 1) +[%%expect{| +Line 1, characters 24-25: +1 | let underscore_tuple = (_, 1) + ^ +Error: wildcard "_" not expected. +|}] + +let underscore_record = { a = _; b = 1 } +[%%expect{| +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 = (1, 2) in x +[%%expect{| +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 47-77: +1 | let overwrite_with_match t = overwrite_ t with match t with C {a;b} -> C{a;b} + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +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 new file mode 100644 index 00000000000..01dddf98663 --- /dev/null +++ b/testsuite/tests/typing-unique/overwriting_underscore.ml @@ -0,0 +1,24 @@ +(* TEST + expect; +*) + +(* For backwards-compatibility, we want to keep the same error message when the extension + 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 = _ +[%%expect{| +Line 1, characters 17-18: +1 | let underscore = _ + ^ +Error: wildcard "_" not expected. +|}] + +let overwriting t = overwrite_ t with (a, b) +[%%expect{| +Line 1, characters 20-44: +1 | let overwriting t = overwrite_ t with (a, b) + ^^^^^^^^^^^^^^^^^^^^^^^^ +Error: The overwriting extension is disabled + To enable it, pass the '-extension overwriting' flag +|}] diff --git a/testsuite/tests/typing-unique/rbtree.byte.reference b/testsuite/tests/typing-unique/rbtree.byte.reference new file mode 100644 index 00000000000..ca1ee52b2cb --- /dev/null +++ b/testsuite/tests/typing-unique/rbtree.byte.reference @@ -0,0 +1,4 @@ +4200 +4200 42000 +4200 42000 +4200 42000 diff --git a/testsuite/tests/typing-unique/rbtree.ml b/testsuite/tests/typing-unique/rbtree.ml new file mode 100644 index 00000000000..dfc4f9ac938 --- /dev/null +++ b/testsuite/tests/typing-unique/rbtree.ml @@ -0,0 +1,528 @@ +(* TEST + flags += "-extension-universe alpha"; + expect; + reference = "${test_source_directory}/rbtree.byte.reference"; +*) + +(* CR uniqueness: To run this test replace 'expect' above by 'native' + and delete the expect block. *) + +type color = Red | Black + +type ('k, 'v) tree = + | Node of { color : color; + left : ('k, 'v) tree; + key : 'k @@ aliased many; + value : 'v @@ aliased many; + right : ('k, 'v) tree } + | Leaf + +let rec fold f b t = + match t with + | Node { left; key; value; right } -> + fold f (f key value (fold f b left)) right + | Leaf -> b + +let work ~insert ~fold ~empty = + let rec loop n t = + if n <= 0 then t + else loop (n - 1) (insert n (n mod 10 = 0) t) + in + let tree = loop 42000 empty in + fold (fun _ v acc -> if v then acc + 1 else acc) 0 tree + +(************************************************************************* + Okasaki-style red-black trees + *************************************************************************) + +module Make_Okasaki(Ord : Map.OrderedType) = struct + type 'a t = (Ord.t, 'a) tree + + let fold = fold + + (* 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 { l with color = Red; + left = Node { ll with color = Black }; + right = Node { t with color = Black; left = l.right } } + | Node ({ right = Node ({ color = Red } as lr) } as l) -> + Node { lr with color = Red; + left = Node { l with color = Black; right = lr.left }; + right = Node { t with color = Black; left = lr.right } } + | Node l -> + Node { t with color = Black; left = Node { l with color = Red } } + | Leaf -> assert false + end + | Leaf -> assert false + + (* 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 { r with color = Red; + left = Node { t with color = Black; right = r.left }; + right = Node { rr with color = Black } } + | Node ({ left = Node ({ color = Red } as rl) } as r) -> + Node { rl with color = Red; + left = Node { t with color = Black; right = rl.left }; + right = Node { r with color = Black; left = rl.right } } + | Node r -> + Node { t with color = Black; right = Node { r with color = Red } } + | Leaf -> assert false + end + | Leaf -> assert false + + 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 + | c when c < 0 -> begin + match t.left with + | Node { color = Red } -> + balance_left (Node { t with left = ins k v t.left }) [@nontail] + | _ -> Node { t with left = ins k v t.left } end + | c when c > 0 -> begin + match t.right with + | Node { color = Red } -> + balance_right (Node { t with right = ins k v t.right }) [@nontail] + | _ -> Node { t with right = ins k v t.right } end + | _ (* k == t.key *) -> Node { t with value = v } + + let set_black t = + match t with + | Node { color = Black } -> t + | Node t -> Node { t with color = Black } + | Leaf -> Leaf + + let insert k v t = set_black (ins k v t) +end + + +(************************************************************************* + Okasaki-style red-black trees with uniqueness + *************************************************************************) + +module Make_Unique_Okasaki(Ord : Map.OrderedType) = struct + type 'a t = (Ord.t, 'a) tree + + 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 { 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 = 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 = 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 + + (* t is black and its right child is red *) + let balance_right t = + match t with + | 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 = rl }; + right = overwrite_ rr with Node { color = Black } } + | 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 = 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 + + 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 { key; left; right } -> + match Ord.compare k key with + | c when c < 0 -> begin + match left with + | Node { color = Red } -> + 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 right with + | Node { color = Red } -> + 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 + +(************************************************************************* + Tree with explicit tags + *************************************************************************) + +type tree_tag = private Tree +type zipper_tag = private Zipper + +type ('left, 'right, 'kind) tag = + | Red : (tree_tag, tree_tag, tree_tag) tag + | Black : (tree_tag, tree_tag, tree_tag) tag + | Right_red : (tree_tag, zipper_tag, zipper_tag) tag + | Right_black : (tree_tag, zipper_tag, zipper_tag) tag + | Left_red : (zipper_tag, tree_tag, zipper_tag) tag + | Left_black : (zipper_tag, tree_tag, zipper_tag) tag + +type ('k, 'v, 'kind) tagged_tree = + | Node : { color : ('left, 'right, 'kind) tag; + left : ('k, 'v, 'left) tagged_tree; + key : 'k; + value : 'v; + right : ('k, 'v, 'right) tagged_tree } + -> ('k, 'v, 'kind) tagged_tree + | Leaf : ('k, 'v, 'kind) tagged_tree + +let rec tagged_fold : 'k 'v 'kind 'a. ('k -> 'v -> 'a -> 'a) -> 'a -> ('k, 'v, 'kind) tagged_tree -> 'a = fun f a t -> + match t with + | Node { left; key; value; right } -> + tagged_fold f (f key value (tagged_fold f a left)) right + | Leaf -> a + +let unique_work ~insert ~fold ~empty = + let rec loop n (t) = + if n <= 0 then t + else loop (n - 1) (insert n (n mod 10 = 0) t) in + let tree = loop 42000 empty in + fold (fun _ v acc -> if v then acc + 1 else acc) 0 tree + + +(************************************************************************* + Okasaki-style red-black trees with uniqueness and explicit tags + *************************************************************************) +module Make_Tagged_Okasaki(Ord : Map.OrderedType) = struct + type 'a t = (Ord.t, 'a, tree_tag) tagged_tree + + let fold = tagged_fold + + (* t is black and its left child is red *) + let balance_left t = + match t with + | Node { color = Black } as t -> + begin match t.left with + | Node { color = Red; left = Node { color = Red } as ll } as l -> + overwrite_ l with + Node { color = Red; + left = overwrite_ ll with Node { color = Black }; + right = overwrite_ t with Node { color = Black; left = l.right } } + | Node { color = Red; right = Node { color = Red } as lr } as l -> + 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 { color = Red } as l -> + overwrite_ t with + Node { color = Black; left = overwrite_ l with Node { color = Red } } + | _ -> assert false + end + | _ -> assert false + + (* t is black and its right child is red *) + let balance_right t = + match t with + | Node { color = Black } as t -> + begin match t.right with + | Node { color = Red; right = Node { color = Red } as rr } as r -> + overwrite_ r with + Node { color = Red; + left = overwrite_ t with Node { color = Black; right = r.left }; + right = overwrite_ rr with Node { color = Black } } + | Node { color = Red; left = Node { color = Red } 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 { color = Red } as r -> + overwrite_ t with + Node { color = Black; right = overwrite_ r with Node { color = Red } } + | _ -> assert false + end + | _ -> assert false + + let rec ins : 'a. Ord.t -> 'a -> 'a t -> 'a t = fun k v t -> + match t with + | Node { color = Black } as t -> begin + match Ord.compare k t.key with + | c when c < 0 -> begin + match t.left with + | Node { color = Red } -> + balance_left (overwrite_ t with Node { left = ins k v t.left }) + | _ -> overwrite_ t with Node { left = ins k v t.left } end + | c when c > 0 -> begin + match t.right with + | Node { color = Red } -> + balance_right (overwrite_ t with Node { right = ins k v t.right }) + | _ -> overwrite_ t with Node { right = ins k v t.right } end + | _ (* k == t.key *) -> overwrite_ t with Node { value = v } end + (* next case exactly as above; copied due to GADT inference *) + | Node { color = Red } as t -> begin + match Ord.compare k t.key with + | c when c < 0 -> begin + match t.left with + | Node { color = Red } -> + balance_left (overwrite_ t with Node { left = ins k v t.left }) + | _ -> overwrite_ t with Node { left = ins k v t.left } end + | c when c > 0 -> begin + match t.right with + | Node { color = Red } -> + balance_right (overwrite_ t with Node { right = ins k v t.right }) + | _ -> overwrite_ t with Node { right = ins k v t.right } end + | _ (* k == t.key *) -> overwrite_ t with Node { value = v } end + | Leaf -> Node { color = Red; left = Leaf; key = k; value = v; right = Leaf } + + let set_black t = + match t with + | Node { color = Red } as t -> overwrite_ t with Node { color = Black } + | t -> t + + let insert k v t = set_black (ins k v t) +end + +(************************************************************************* + Bottom-up red-black trees + *************************************************************************) + +module Make_Tagged_Bottom_Up(Ord : Map.OrderedType) = struct + type 'a t = (Ord.t, 'a, tree_tag) tagged_tree + type 'a z = (Ord.t, 'a, zipper_tag) tagged_tree + + let fold = tagged_fold + + let rec move_up : 'a. 'a z -> 'a t -> 'a t = fun z t -> + match z with + | Node { color = Left_red; left = z' } as z -> + move_up z' (overwrite_ z with Node { color = Red; left = t }) + | Node { color = Left_black; left = z' } as z -> + move_up z' (overwrite_ z with Node { color = Black; left = t }) + | Node { color = Right_red; right = z' } as z -> + move_up z' (overwrite_ z with Node { color = Red; right = t }) + | Node { color = Right_black; right = z' } as z -> + move_up z' (overwrite_ z with Node { color = Black; right = t }) + | Leaf -> t + + let rec fixup : 'a. 'a z -> 'a t -> 'a t = fun z t -> + match z with + | Node { color = Left_red; left = z'; right = zright } as z -> begin + match z' with + | Node { color = Left_black; left = z''; right = y } as z' -> begin + match y with + | Node { color = Red } as y -> + fixup z'' (overwrite_ z' with + Node { color = Red; + left = overwrite_ z with Node { color = Black; left = t }; + right = overwrite_ y with Node { color = Black } }) + | Node { color = Black } | Leaf -> + move_up z'' (overwrite_ z with + Node { color = Black; + right = overwrite_ z' with Node { color = Red; left = zright }; + left = t }) end + | Node { color = Right_black; right = z''; left = y } as z' -> begin + match y with + | Node { color = Red } as y -> + fixup z'' (overwrite_ z' with + Node { color = Red; + right = overwrite_ z with Node { color = Black; left = t }; + left = overwrite_ y with Node { color = Black } }) + | Node { color = Black } | Leaf -> + match t with + | Node ({ color = Red; left = tl; right = tr } as t) -> + move_up z'' (overwrite_ t with + Node { color = Black; + left = overwrite_ z' with Node { color = Red; right = tl }; + right = overwrite_ z with Node { color = Red; left = tr } }) + | _ -> assert false end + | _ -> assert false end + | Node { color = Right_red; right = z'; left = zleft } as z -> begin + match z' with + | Node { color = Right_black; right = z''; left = y } as z' -> begin + match y with + | Node { color = Red } as y -> + fixup z'' (overwrite_ z' with + Node { color = Red; + right = overwrite_ z with Node { color = Black; right = t }; + left = overwrite_ y with Node { color = Black } }) + | Node { color = Black } | Leaf -> + move_up z'' (overwrite_ z with + Node { color = Black; + left = overwrite_ z' with Node { color = Red; right = zleft }; + right = t }) end + | Node { color = Left_black; left = z''; right = y } as z' -> begin + match y with + | Node { color = Red } as y -> + fixup z'' (overwrite_ z' with + Node { color = Red; + left = overwrite_ z with Node { color = Black; right = t }; + right = overwrite_ y with Node { color = Black } }) + | Node { color = Black } | Leaf -> + match t with + | Node { color = Red; left = tl; right = tr } as t -> + move_up z'' (overwrite_ t with + Node { color = Black; + left = overwrite_ z with Node { color = Red; right = tl }; + right = overwrite_ z' with Node { color = Red; left = tr } }) + | _ -> assert false end + | _ -> assert false end + | _ -> move_up z t + + let rec ins : 'a. Ord.t -> 'a -> 'a z -> 'a t -> 'a t = fun k v z t -> + match t with + | Node { color = Black; left; right } as t -> begin + match Ord.compare k t.key with + | c when c < 0 -> + ins k v (overwrite_ t with Node { color = Left_black; left = z }) left + | c when c > 0 -> + ins k v (overwrite_ t with Node { color = Right_black; right = z }) right + | _ (* k == t.key *) -> move_up z (overwrite_ t with Node { value = v }) end + | Node { color = Red; left; right } as t -> begin + match Ord.compare k t.key with + | c when c < 0 -> + ins k v (overwrite_ t with Node { color = Left_red; left = z }) left + | c when c > 0 -> + ins k v (overwrite_ t with Node { color = Right_red; right = z }) right + | _ (* k == t.key *) -> move_up z (overwrite_ t with Node { value = v }) end + | Leaf -> fixup z (Node { color = Red; left = Leaf; key = k; value = v; right = Leaf }) + + let set_black t = + match t with + | Node { color = Red } as t -> overwrite_ t with Node { color = Black } + | _ -> t + + let insert k v t = set_black (ins k v Leaf t) +end + +module IntOrder = struct + type t = int + + let compare t1 t2 = t1 - t2 +end + +let () = + let module Ord = IntOrder in + let module M1 = Make_Okasaki(Ord) in + let module M2 = Make_Unique_Okasaki(Ord) in + let module M3 = Make_Tagged_Okasaki(Ord) in + let module M4 = Make_Tagged_Bottom_Up(Ord) in + + let baseline_allocation = Gc.allocated_bytes() -. Gc.allocated_bytes() in + let bytes_per_word = Sys.word_size / 8 in + let node_size = 6 in + let compute_delta before after = + int_of_float ((after -. before) -. baseline_allocation) / bytes_per_word / node_size + in + + let r1 = work ~insert:M1.insert ~fold ~empty:Leaf in + + let before_r2 = Gc.allocated_bytes () in + let r2 = unique_work ~insert:M2.insert ~fold ~empty:Leaf in + let after_r2 = Gc.allocated_bytes () in + let delta_r2 = compute_delta before_r2 after_r2 in + + let before_r3 = Gc.allocated_bytes () in + let r3 = unique_work ~insert:M3.insert ~fold:tagged_fold ~empty:Leaf in + let after_r3 = Gc.allocated_bytes () in + let delta_r3 = compute_delta before_r3 after_r3 in + + let before_r4 = Gc.allocated_bytes () in + let r4 = unique_work ~insert:M4.insert ~fold:tagged_fold ~empty:Leaf in + let after_r4 = Gc.allocated_bytes () in + let delta_r4 = compute_delta before_r4 after_r4 in + + Printf.printf "%d\n%d %d\n%d %d\n%d %d\n" + r1 r2 delta_r2 r3 delta_r3 r4 delta_r4 + +[%%expect{| +type color = Red | Black +type ('k, 'v) tree = + Node of { color : color; left : ('k, 'v) tree; key : 'k @@ many aliased; + value : 'v @@ many aliased; right : ('k, 'v) tree; + } + | Leaf +val fold : + 'a 'b ('c : value_or_null). + ('a -> 'b -> 'c -> 'c) -> 'c -> ('a, 'b) tree -> 'c + @@ global many = +val work : + ('a : value_or_null) ('b : value_or_null) ('c : value_or_null). + insert:(int -> bool -> 'a -> 'a) -> + fold:(('b -> bool -> int -> int) -> int -> 'a -> 'c) -> empty:'a -> 'c + @@ global many = +Line 85, characters 16-71: +85 | balance_right (Node { t with right = ins k v t.right }) [@nontail] + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Warning 72 [tmc-breaks-tailcall]: This call +is in tail-modulo-cons position in a TMC function, +but the function called is not itself specialized for TMC, +so the call will not be transformed into a tail call. +Please either mark the called function with the [@tail_mod_cons] +attribute, or mark this call with the [@tailcall false] attribute +to make its non-tailness explicit. + +Line 80, characters 16-68: +80 | balance_left (Node { t with left = ins k v t.left }) [@nontail] + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Warning 72 [tmc-breaks-tailcall]: This call +is in tail-modulo-cons position in a TMC function, +but the function called is not itself specialized for TMC, +so the call will not be transformed into a tail call. +Please either mark the called function with the [@tail_mod_cons] +attribute, or mark this call with the [@tailcall false] attribute +to make its non-tailness explicit. + +module Make_Okasaki : + functor (Ord : Map.OrderedType) -> + sig + type 'a t = (Ord.t, 'a) tree + val fold : + 'a 'b ('c : value_or_null). + ('a -> 'b -> 'c -> 'c) -> 'c -> ('a, 'b) tree -> 'c + @@ global many + val balance_left : ('a, 'b) tree -> ('a, 'b) tree @@ global many + portable + val balance_right : ('a, 'b) tree -> ('a, 'b) tree @@ global many + portable + val ins : Ord.t -> 'a -> (Ord.t, 'a) tree -> (Ord.t, 'a) tree @@ global + many + val set_black : ('a, 'b) tree -> ('a, 'b) tree @@ global many portable + val insert : Ord.t -> 'a -> (Ord.t, 'a) tree -> (Ord.t, 'a) tree @@ + global many + end +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 f99b4293bc3..46a1b0ef9c7 100644 --- a/testsuite/tests/typing-unique/unique.ml +++ b/testsuite/tests/typing-unique/unique.ml @@ -8,7 +8,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) ^ @@ -28,7 +28,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) ^ @@ -40,7 +40,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) ^ @@ -52,7 +52,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) ^ @@ -65,7 +65,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) ^^^^^^^^^^^ @@ -81,28 +81,42 @@ val dup : 'a -> 'a * 'a @ once = (* closing over unique values gives once closure *) let f () = - let unique_ k = "foo" in - let g () = (unique_ k) ^ (unique_ k) in - g () ^ g () + let unique_ k = [1;2;3] in + let g () = (unique_ k) @ [1;2;3] in + g () @ g () [%%expect{| -Line 3, characters 27-38: -3 | let g () = (unique_ k) ^ (unique_ k) in - ^^^^^^^^^^^ -Error: This value is used here, but it has already been used as unique: -Line 3, characters 13-24: -3 | let g () = (unique_ k) ^ (unique_ k) in - ^^^^^^^^^^^ +Line 4, characters 9-10: +4 | g () @ g () + ^ +Error: This value is used here, + but it is defined as once and is already being used: +Line 4, characters 2-3: +4 | g () @ g () + ^ |}] (* but if the closure doesn't utilize the uniqueness, then it's not once *) let f () = - let unique_ k = "foo" in - let g () = k ^ k in - g () ^ g () + let unique_ k = [1;2;3] in + let g () = k @ [1;2;3] in + g () @ g () [%%expect{| -val f : unit -> string = +val f : unit -> int list = +|}] + +(* closing over once values gives once closure *) +(* note that in g we don't annotate k; because once_ is already the most relaxed mode *) +let f () = + let once_ k = [(fun x -> x)] in + let g () = k @ [(fun x -> x)] in + g () @ g () +[%%expect{| +Line 3, characters 13-14: +3 | let g () = k @ [(fun x -> x)] in + ^ +Error: This value is "once" but expected to be "many". |}] (* variables inside loops will be made both aliased and many *) @@ -172,37 +186,6 @@ let f = val f : unit = () |}] -(* the following is howerver fine, because g doesn't use the uniqueness of k; -in fact, the k inside g is just aliased. - *) -let f () = - let unique_ k = "foo" in - let g () = k ^ k in - (* k is unique, and thus g is once *) - g () ^ g () -[%%expect{| -val f : unit -> string = -|}] - -(* closing over once values gives once closure *) -(* note that in g we don't annotate k; becaue once_ is already the most relaxed mode - *) -let f () = - let once_ k = "foo" in - let g () = k in - (g (), g () ) -[%%expect{| -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: -Line 4, characters 3-4: -4 | (g (), g () ) - ^ - -|}] - let x = "foo" [%%expect{| val x : string = "foo" @@ -218,9 +201,9 @@ Error: This value is "once" but expected to be "many". |}] (* the following is fine - we relax many to once *) -let foo y = once_ x +let foo () = once_ x [%%expect{| -val foo : 'a -> string @ once = +val foo : unit -> string @ once = |}] (* top-level must be aliased; the following unique is weakened to aliased *) @@ -231,11 +214,11 @@ val foo : string = "foo" (* the following is bad - trying to tighten aliased to unique *) -let foo y = unique_ x +let foo () = unique_ x [%%expect{| -Line 1, characters 20-21: -1 | let foo y = unique_ x - ^ +Line 1, characters 21-22: +1 | let foo () = unique_ x + ^ Error: This value is "aliased" but expected to be "unique". |}] @@ -263,7 +246,7 @@ module M : sig val drop : 'a @ unique -> unit @ unique end (* In the following we won't use module *) (* printed modes are imprecise *) -let unique_id : 'a. unique_ 'a -> unique_ 'a = fun x -> x +let unique_id : unique_ 'a -> unique_ 'a = fun x -> x [%%expect{| val unique_id : 'a @ unique -> 'a @ unique = |}] @@ -326,19 +309,6 @@ Error: This expression has type "'a @ unique -> 'a" but an expression was expected of type "'b -> 'c @ unique" |}] -type record_update = { x : string } -[%%expect{| -type record_update = { x : string; } -|}] - -let update2 = update { x = "bar" } -[%%expect{| -Line 1, characters 14-20: -1 | let update2 = update { x = "bar" } - ^^^^^^ -Error: Unbound value "update" -|}] - let inf1 (unique_ x : float) = unique_ let y = x in y [%%expect{| val inf1 : float @ unique -> float = @@ -400,24 +370,6 @@ let ul_ret x = exclave_ unique_ x val ul_ret : 'a @ unique -> local_ 'a = |}] -type point = { x : float; y : float } -[%%expect{| -type point = { x : float; y : float; } -|}] - -let overwrite_point t = - unique_ ({t with y = 0.5}, {t with x = 0.5}) -[%%expect{| -val overwrite_point : point @ unique -> point * point = -|}] - -let gc_soundness_nobug (local_ unique_ p) (local_ f) = - exclave_ { p with x = f } -[%%expect{| -val gc_soundness_nobug : - local_ point @ unique -> local_ float -> local_ point = -|}] - let rec foo = fun (local_ o) -> match (unique_ o) with @@ -496,7 +448,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) ^^^ @@ -512,7 +464,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) ^^^ @@ -521,16 +473,16 @@ Line 4, characters 25-28: let curry = let unique_ x = "foo" in - let foo y = unique_ x in - (foo 1, foo 2) + let foo () = unique_ x in + (foo (), foo ()) [%%expect{| -Line 4, characters 10-13: -4 | (foo 1, foo 2) - ^^^ +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 1, foo 2) +4 | (foo (), foo ()) ^^^ |}] @@ -609,7 +561,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) ^ @@ -633,7 +585,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) ^^^^^^^^ @@ -663,3 +615,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 057d616ca2e..d80e53fc044 100644 --- a/testsuite/tests/typing-unique/unique_analysis.ml +++ b/testsuite/tests/typing-unique/unique_analysis.ml @@ -8,7 +8,7 @@ -extension layouts_beta *) (* First some helper functions *) -let unique_id : 'a. unique_ 'a -> unique_ 'a = fun x -> x +let unique_id : unique_ 'a -> unique_ 'a = fun x -> x [%%expect{| val unique_id : 'a @ unique -> 'a @ unique = |}] @@ -39,9 +39,8 @@ let branching (unique_ x) = unique_ if true then x else x val branching : 'a @ unique -> 'a = |}] -(* whether we constrain uniqueness or linearity is irrelavant - for testing uniqueness analysis. Therefore, in the rest we - will only constrain uniqueness *) +(* Uniqueness and linearity have similar restrictions on control-flow. + Therefore, in the rest we will only constrain uniqueness *) let branching (once_ x) = if true then x else x [%%expect{| val branching : 'a @ once -> 'a @ once = @@ -60,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) ^ @@ -125,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 ^^^^^^^^^^^^ @@ -141,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 ^^ @@ -156,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 ^^^^^^^^^^^^ @@ -171,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 ^^ @@ -240,8 +239,6 @@ Line 4, characters 50-51: |}] -(* for some reason the following error message is missing "another use". Don't -know what's wrong *) let mark_top_aliased = let unique_ xs = 2 :: 3 :: [] in match xs with @@ -385,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) ^ @@ -400,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) ^ @@ -415,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) ^ @@ -578,7 +575,7 @@ type r_aliased = { x : Value.t; y : Value.t @@ many aliased; } let foo () = let r = {x = Value.mk (); y = Value.mk ()} in ignore (aliased_id r.y); - (* the following is allowed, because using r uniquely implies using r.x + (* the following is allowed, because using r uniquely implies using r.y aliased *) ignore (unique_id r) [%%expect{| @@ -664,7 +661,7 @@ let foo () = let r = R_aliased (Value.mk (), Value.mk ()) in let R_aliased (_, y) = r in ignore (aliased_id y); - (* the following is allowed, because using r uniquely implies using r.x + (* the following is allowed, because using r uniquely implies using r.y aliased *) ignore (unique_id r) [%%expect{| @@ -743,7 +740,7 @@ Line 4, characters 20-21: type r = {x : float; y : float} (* CR zqian: The following should pass but doesn't, because the uniqueness - analysis doesn't support mode crossing. The following involes sequencing the + analysis doesn't support mode crossing. The following involves sequencing the maybe_unique usage of [r.x] and the maybe_unique usage of [r] as a whole. Sequencing them will force both to be aliased and many. The [unique_use] in [r.x] is mode-crossed (being an unboxed float) so is fine. The [unique_use] 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 e89b6e3dcda..a71891ec1a4 100644 --- a/typing/printtyped.ml +++ b/typing/printtyped.ml @@ -647,7 +647,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 c31881fe92d..a2d8dbec1f1 100644 --- a/typing/tast_iterator.ml +++ b/typing/tast_iterator.ml @@ -439,6 +439,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 2ce51ae48dc..bc7dd19b6dc 100644 --- a/typing/tast_mapper.ml +++ b/typing/tast_mapper.ml @@ -618,6 +618,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 3c402295b11..e5a7948cb17 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 @@ -278,6 +277,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 @@ -691,6 +692,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 @@ -4163,6 +4207,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 @@ -4585,6 +4637,7 @@ let check_partial_application ~statement exp = | Texp_unboxed_tuple _ | Texp_construct _ | Texp_variant _ | Texp_record _ | Texp_record_unboxed_product _ | Texp_unboxed_field _ + | Texp_overwrite _ | Texp_hole _ | Texp_field _ | Texp_setfield _ | Texp_array _ | Texp_list_comprehension _ | Texp_array_comprehension _ | Texp_while _ | Texp_for _ | Texp_instvar _ @@ -5244,9 +5297,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. @@ -5256,13 +5309,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 @@ -5270,7 +5323,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 @@ -5283,13 +5336,13 @@ and type_expect_ unify_exp ~sdesc_for_hint:desc env (re exp) (instance ty_expected)); exp in - let type_expect_record (type rep) (record_form : rep record_form) + let type_expect_record (type rep) ~overwrite (record_form : rep record_form) (lid_sexp_list: (Longident.t loc * Parsetree.expression) list) (opt_sexp : Parsetree.expression option) = 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 () -> @@ -5301,40 +5354,36 @@ and type_expect_ Some (exp, mode) in let ty_record, expected_type = - let expected_opath = - match extract_concrete_record record_form env ty_expected with - | Record_type (p0, p, _, _) -> Some (p0, p, is_principal ty_expected) + let extract_record loc ty other_form_error not_a_record_error = + match extract_concrete_record record_form env ty with + | Record_type (p0, p, _, _) -> Some (p0, p, is_principal ty) | Record_type_of_other_form -> - let error = - Wrong_expected_record_boxing - (Expression explanation, P record_form, ty_expected) - in - raise (Error (loc, env, error)) + raise (Error (loc, env, other_form_error)) | Maybe_a_record_type -> None | Not_a_record_type -> - let wks = record_form_to_wrong_kind_sort record_form in - let error = - Wrong_expected_kind(wks, Expression explanation, ty_expected) - in - raise (Error (loc, env, error)) + raise (Error (loc, env, not_a_record_error)) + in + let expected_opath = + let wks = record_form_to_wrong_kind_sort record_form in + extract_record loc ty_expected + (Wrong_expected_record_boxing + (Expression explanation, P record_form, ty_expected)) + (Wrong_expected_kind(wks, 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_record_type_has_wrong_boxing (P record_form, ty)) + (Expr_not_a_record_type (P record_form, ty)) + | (No_overwrite | Assigning _) -> None + end | Some (exp, _) -> - match extract_concrete_record record_form env exp.exp_type with - | Record_type (p0, p, _, _) -> - Some (p0, p, is_principal exp.exp_type) - | Maybe_a_record_type -> None - | Record_type_of_other_form -> - let error = - Expr_record_type_has_wrong_boxing (P record_form, exp.exp_type) - in - raise (Error (exp.exp_loc, env, error)) - | Not_a_record_type -> - let error = - Expr_not_a_record_type (P record_form, exp.exp_type) in - raise (Error (exp.exp_loc, env, error)) + extract_record loc exp.exp_type + (Expr_record_type_has_wrong_boxing (P record_form, exp.exp_type)) + (Expr_not_a_record_type (P record_form, exp.exp_type)) in match expected_opath, opt_exp_opath with | None, None -> @@ -5349,7 +5398,7 @@ 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_form_to_string record_form) @@ -5372,22 +5421,40 @@ and type_expect_ | Record_unboxed_product -> false end in + let is_boxed = + List.exists + (fun (_, {lbl_repres; _}, _) -> + repres_might_allocate record_form lbl_repres) + lbl_a_list + in + begin match overwrite with + | (No_overwrite | Assigning _) -> () + | Overwriting _ -> + if not is_boxed then + raise (Error (loc, env, Overwrite_of_invalid_term)); + end; let alloc_mode, argument_mode = - if List.exists - (fun (_, {lbl_repres; _}, _) -> - repres_might_allocate record_form lbl_repres) - lbl_a_list then + if is_boxed 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 record_form - 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 record_form + 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 @@ -5407,8 +5474,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 @@ -5434,33 +5525,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 @@ -5855,13 +5930,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 *) @@ -5878,7 +5953,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; @@ -5917,10 +5994,10 @@ and type_expect_ exp_env = env } end | Pexp_record(lid_sexp_list, opt_sexp) -> - type_expect_record Legacy lid_sexp_list opt_sexp + type_expect_record ~overwrite Legacy lid_sexp_list opt_sexp | Pexp_record_unboxed_product(lid_sexp_list, opt_sexp) -> Language_extension.assert_enabled ~loc Layouts Language_extension.Beta; - type_expect_record Unboxed_product lid_sexp_list opt_sexp + type_expect_record ~overwrite Unboxed_product lid_sexp_list opt_sexp | Pexp_field(srecord, lid) -> let (record, rmode, label, _) = type_label_access Legacy env srecord Env.Projection lid @@ -6021,8 +6098,8 @@ and type_expect_ submode ~loc:record.exp_loc ~env rmode mode_mutate_mutable; let mode = mutable_mode m0 |> mode_default in let mode = mode_modality label.lbl_modalities mode in - type_label_exp false env mode loc ty_record (lid, label, snewval) - Legacy + type_label_exp ~overwrite:No_overwrite_label false env mode loc ty_record + (lid, label, snewval) Legacy | Immutable -> raise(Error(loc, env, Label_not_mutable lid.txt)) in @@ -6167,7 +6244,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; @@ -6729,6 +6806,68 @@ and type_expect_ ~ty_expected ~attributes:sexp.pexp_attributes comp + | Pexp_overwrite (exp1, exp2) -> + if not (Language_extension.is_enabled Overwriting) then + 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 -> + 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 -> @@ -6736,7 +6875,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 @@ -7535,7 +7674,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)) @@ -7545,10 +7684,10 @@ and type_option_some env expected_mode sarg ty ty0 = allocation, mutation and modalities. *) and type_label_exp : type rep. - _ -> _ -> _ -> _ -> _ -> + overwrite:_ -> _ -> _ -> _ -> _ -> _ -> _ * rep gen_label_description * _ -> rep record_form -> _ * rep gen_label_description * _ - = fun create env arg_mode loc ty_expected (lid, label, sarg) record_form -> + = fun ~overwrite create env arg_mode loc ty_expected (lid, label, sarg) record_form -> (* Here also ty_expected may be at generic_level *) let separate = !Clflags.principal || Env.has_local_constraints env in (* #4682: we try two type-checking approaches for [arg] using backtracking: @@ -7558,7 +7697,7 @@ and type_label_exp 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 @@ -7580,13 +7719,22 @@ and type_label_exp 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, @@ -7606,7 +7754,9 @@ and type_label_exp 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 = @@ -7625,7 +7775,7 @@ and type_label_exp 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 = @@ -7696,7 +7846,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 @@ -7833,7 +7983,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 @@ -7862,7 +8012,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 @@ -7894,7 +8044,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 @@ -8012,7 +8162,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. *) @@ -8024,14 +8174,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. *) @@ -8050,16 +8204,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); @@ -8127,7 +8289,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 = @@ -8168,7 +8330,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 () -> @@ -8197,6 +8359,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 @@ -8211,7 +8374,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)) @@ -8225,12 +8390,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 @@ -9658,12 +9841,12 @@ and type_send env loc explanation e met = let maybe_check_uniqueness_exp exp = if Language_extension.is_at_least Unique Language_extension.maturity_of_unique_for_drf then - check_uniqueness_exp exp + Uniqueness_analysis.check_uniqueness_exp exp let maybe_check_uniqueness_value_bindings vbl = if Language_extension.is_at_least Unique Language_extension.maturity_of_unique_for_drf then - check_uniqueness_value_bindings vbl + Uniqueness_analysis.check_uniqueness_value_bindings vbl (* Typing of toplevel bindings *) @@ -10726,6 +10909,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 @@ -10762,7 +10951,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 09347fd38fd..36c34591889 100644 --- a/typing/typecore.mli +++ b/typing/typecore.mli @@ -321,6 +321,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 bd35e8fb8d5..c1fc87d38f0 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; @@ -282,6 +298,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 52f9b6a9e3c..faa5efea45d 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; @@ -482,6 +500,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/types.ml b/typing/types.ml index b6e7839a902..4f4337d67f5 100644 --- a/typing/types.ml +++ b/typing/types.ml @@ -608,6 +608,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 f2dbc5bdb16..3ae4afb2ae5 100644 --- a/typing/types.mli +++ b/typing/types.mli @@ -871,6 +871,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 bfcf37796c9..39a41173c71 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 @@ -173,6 +208,19 @@ end = struct | _ -> ()) t else () + + 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 @@ -192,6 +240,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 @@ -205,8 +255,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 *) @@ -234,12 +338,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 @@ -248,6 +357,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). @@ -299,6 +410,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 = @@ -320,6 +435,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 @@ -340,16 +457,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 @@ -359,7 +477,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) @@ -369,20 +487,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 = @@ -422,7 +540,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, @@ -441,19 +559,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 @@ -468,6 +927,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 = @@ -525,6 +989,22 @@ 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 + | Record_unboxed_product_field l -> + fprintf ppf "Record_unboxed_product_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 = @@ -550,6 +1030,7 @@ type error = { cannot_force : Maybe_unique.cannot_force; reason : boundary_reason } + | Overwrite_changed_tag of Overwrites.error exception Error of error @@ -564,6 +1045,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] *) @@ -578,11 +1061,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 @@ -593,10 +1102,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 @@ -605,22 +1120,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 -> @@ -629,38 +1148,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 *) @@ -673,6 +1271,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. *) @@ -697,10 +1297,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 @@ -719,6 +1340,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 @@ -730,6 +1353,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 @@ -740,8 +1368,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 @@ -751,19 +1379,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 @@ -810,7 +1473,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 @@ -820,6 +1483,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 @@ -862,16 +1533,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 = @@ -914,11 +1598,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 @@ -958,14 +1651,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 @@ -988,10 +1707,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 *) @@ -1002,6 +1723,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 @@ -1028,6 +1751,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 @@ -1041,6 +1768,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 *) @@ -1124,6 +1855,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 = @@ -1135,7 +1869,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 = @@ -1145,7 +1879,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 = @@ -1302,8 +2036,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 @@ -1316,7 +2057,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 @@ -1324,7 +2065,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 = @@ -1336,37 +2079,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 @@ -1376,19 +2126,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 @@ -1411,7 +2179,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)) @@ -1431,7 +2203,7 @@ let rec check_uniqueness_exp (ienv : Ienv.t) exp : UF.t = l.lbl_name value unique_use in Value.mark_maybe_unique value - | _, Overridden (_, e) -> check_uniqueness_exp ienv e) + | _, Overridden (_, e) -> check_uniqueness_exp ~overwrite:None ienv e) fields in UF.par uf_ext (UF.pars (Array.to_list uf_fields)) @@ -1443,61 +2215,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, @@ -1529,11 +2305,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. @@ -1575,7 +2372,10 @@ 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]) | Texp_unboxed_field (e, _, _, l, unique_use) -> ( @@ -1590,7 +2390,7 @@ and check_uniqueness_exp_as_value ienv exp : Value.t * UF.t = let value = Value.existing paths unique_use occ in value, uf) (* 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 = @@ -1624,18 +2424,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 @@ -1644,18 +2447,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 @@ -1668,7 +2482,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) @@ -1679,10 +2493,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 = @@ -1692,19 +2507,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 @@ -1734,28 +2557,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 @@ -1776,12 +2599,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 5a272200c9d..63d9e580766 100644 --- a/typing/untypeast.ml +++ b/typing/untypeast.ml @@ -712,6 +712,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 a7713fb5d8b..4d9c86904e6 100644 --- a/typing/value_rec_check.ml +++ b/typing/value_rec_check.ml @@ -197,7 +197,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 _ @@ -1015,6 +1019,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 diff --git a/utils/language_extension_kernel.ml b/utils/language_extension_kernel.ml index ce60165f1ae..7e8ac8dadce 100644 --- a/utils/language_extension_kernel.ml +++ b/utils/language_extension_kernel.ml @@ -8,6 +8,7 @@ type _ t = | Comprehensions : unit t | Mode : maturity t | Unique : maturity t + | Overwriting : unit t | Include_functor : unit t | Polymorphic_parameters : unit t | Immutable_arrays : unit t @@ -23,6 +24,7 @@ let to_string : type a. a t -> string = function | Comprehensions -> "comprehensions" | Mode -> "mode" | Unique -> "unique" + | Overwriting -> "overwriting" | Include_functor -> "include_functor" | Polymorphic_parameters -> "polymorphic_parameters" | Immutable_arrays -> "immutable_arrays" diff --git a/utils/language_extension_kernel.mli b/utils/language_extension_kernel.mli index 7dc4c0b2f38..1fdd1c17b02 100644 --- a/utils/language_extension_kernel.mli +++ b/utils/language_extension_kernel.mli @@ -19,6 +19,7 @@ type _ t = | Comprehensions : unit t | Mode : maturity t | Unique : maturity t + | Overwriting : unit t | Include_functor : unit t | Polymorphic_parameters : unit t | Immutable_arrays : unit t diff --git a/utils/profile_counters_functions.ml b/utils/profile_counters_functions.ml index 8320d6edb4f..e590a2c4cc9 100644 --- a/utils/profile_counters_functions.ml +++ b/utils/profile_counters_functions.ml @@ -11,7 +11,7 @@ let count_language_extensions typing_input = | Labeled_tuples -> Language_extension_kernel.to_string lang_ext | Mode | Unique | Polymorphic_parameters | Layouts | SIMD | Small_numbers - | Instances -> + | Instances | Overwriting -> let error_msg = Format.sprintf "No counters supported for language extension : %s." (Language_extension_kernel.to_string lang_ext)