diff --git a/doc/tutorial/tutorial.md b/doc/tutorial/tutorial.md index 6d2bd3620..8ab7252ba 100644 --- a/doc/tutorial/tutorial.md +++ b/doc/tutorial/tutorial.md @@ -1348,6 +1348,104 @@ multiple times for different input/output relations). Several useful graph transformers are declared in `lib/graph.dl` and implemented in `lib/graph.rs` +### Variable mutability + +We summarize variable mutability rules in DDlog. Variables declared in the +context of a rule are immutable: they are bound once and do not change their +value within the rule. Mutability of variables in an expression is determined +according to the following rules: + +* Local variables declared using `var v` are mutable. + +* Function arguments with `mut` qualifier are mutable. + +* Other function arguments are immutable. + +* Loop variables are automatically modified at each iteration of the loop, but + cannot be modified in the body of the loop. + +* Variables declared in the rule scope and used inside an expression (e.g., in + an assignment clause) are immutable. + +* Variables declared inside a match pattern are mutable if and only if the expression + being matched is mutable: + +Mutable variables and their fields can be assigned to or passed as mutable +arguments to functions. + +``` +function f(x: mut string, y: u32) { + var z = 0; + + // ok: z is a local variable. + z = y; + + // ok: x is a `mut` argument. + x = "foo" + + // error: y is a read-only argument. + y = 0; + + var vec = [0, 1, 2]; + for (val in vec) { + // error: loop variable cannot be modified in the body of the loop. + val = y + }; + + var opt: Option = Some{0}; + + match (opt) { + Some{u} -> { + // ok: `opt` is mutable; hence it components are mutable. + u = 5 + }, + _ -> () + } +} +``` + +There are several exceptions to the above rules: + +* Field of variables of type `Ref<>` or `Intern<>` are immutable. + +* Variables used in the expression that the loop iterates over cannot be modified + in the body of the loop. + +* In addition, to prevent errors, DDlog disallows modifying any variables inside + `if`-conditions, or inside operands of binary or unary operators. + +``` +typedef TestStruct = TestStruct { + f1: string, + f2: bool +} + +function f() { + var test: TestStruct = TestStruct{"foo", false}; + var interned: Intern = TestStruct{"foo", false}.intern(); + + // ok: modifying field of a local variable. + test.f1 = "bar"; + + // ok: overwriting the entire interned variable. + interned = TestStruct{"bar", true}.intern(); + + // error: cannot modify the contents of an interned value. + interned.f1 = "bar"; + + var vec = [0, 1, 2]; + for (val in vec) { + // error: cannot modify a variable while iterating over it. + vec.push(val) + }; + + // error: attempt to modify a variable inside an if-condition. + if ({vec.push(3); vec.len()} > 5) { + ... + } +} +``` + ## Multisets and streams All DDlog relations considered so far implement set semantics. A set can contain diff --git a/test/datalog_tests/function.fail.ast.expected b/test/datalog_tests/function.fail.ast.expected index 9172c9e8b..21fcbf504 100644 --- a/test/datalog_tests/function.fail.ast.expected +++ b/test/datalog_tests/function.fail.ast.expected @@ -111,3 +111,23 @@ extern function foo(x: u32): () error: ./test/datalog_tests/function.fail.dl:8:21-8:38: expression 'std::nth(components, 1)' must be of type 'Result<>', but its type is 'std::Option<'a>' var last_name = components.nth(1)?; ^^^^^^^^^^^^^^^^^ + +error: ./test/datalog_tests/function.fail.dl:13:5-13:7: Expression is not an l-value + y = 0 + ^^ + +error: ./test/datalog_tests/function.fail.dl:7:9-7:13: Expression is not an l-value + val = y + ^^^^ + +error: ./test/datalog_tests/function.fail.dl:15:5-15:17: Expression is not an l-value + interned.f1 = "bar" + ^^^^^^^^^^^^ + +error: ./test/datalog_tests/function.fail.dl:13:9-13:12: Expression is not an l-value + vec.push(val) + ^^^ + +error: ./test/datalog_tests/function.fail.dl:13:10-13:13: Expression is not an l-value + if ({vec.push(3); vec.len()} > 5) { () } + ^^^ diff --git a/test/datalog_tests/function.fail.dl b/test/datalog_tests/function.fail.dl index 84c6267f2..5d01bd2be 100644 --- a/test/datalog_tests/function.fail.dl +++ b/test/datalog_tests/function.fail.dl @@ -192,3 +192,76 @@ function try1(name: string): Result<(string, string), string> { var last_name = components.nth(1)?; Some{(first_name, last_name)} } + +//--- + +function f(x: mut string, y: u32) { + var z = 0; + + // ok: z is a local variable. + z = y; + + // ok: x is a `mut` argument. + x = "foo"; + + // error: y is a read-only argument. + y = 0 +} + +//--- + +function f(x: mut string, y: u32) { + var vec = [0, 1, 2]; + for (val in vec) { + // error: loop variable cannot be modified in the body of the loop. + val = y + } +} + +//--- + +typedef TestStruct = TestStruct { + f1: string, + f2: bool +} + +function f() { + var interned: Intern = TestStruct{"foo", false}.intern(); + + // ok: overwriting the entire interned variable. + interned = TestStruct{"bar", true}.intern(); + + // error: cannot modify the contents of an interned value. + interned.f1 = "bar" +} + +//--- +typedef TestStruct = TestStruct { + f1: string, + f2: bool +} + +function f() { + var interned: Intern = TestStruct{"foo", false}.intern(); + + var vec = [0, 1, 2]; + for (val in vec) { + // error: cannot modify a variable while iterating over it. + vec.push(val) + } +} + +//--- + +typedef TestStruct = TestStruct { + f1: string, + f2: bool +} + +function f() { + var interned: Intern = TestStruct{"foo", false}.intern(); + + var vec = [0, 1, 2]; + // error: attempt to modify a variable inside an if-condition. + if ({vec.push(3); vec.len()} > 5) { () } +} diff --git a/test/datalog_tests/simple2.debug.ast.expected b/test/datalog_tests/simple2.debug.ast.expected index 6353f09c0..8b267031f 100644 --- a/test/datalog_tests/simple2.debug.ast.expected +++ b/test/datalog_tests/simple2.debug.ast.expected @@ -22,6 +22,8 @@ typedef Ints = Ints{x: bigint} typedef MapOfMaps = MapOfMaps{m: std::Map>} typedef MapOfVecs = MapOfVecs{m: std::Map<(std::u32, bigint),std::Vec>} typedef ModifyMe = ModifyMe{x: string, y: std::s128} +typedef Nested = Nested{descr: string, n: NestedStruct} +typedef NestedStruct = NestedStruct{x: std::Option} typedef Object = Object{field: std::u128} typedef Objects = Objects{chunk: Object} typedef Opt<'X> = std::Option<'X> @@ -449,6 +451,22 @@ extern function json::to_json_string (x: 'T): std::Result extern function json::to_json_value (x: 'T): std::Result #[has_side_effects = true] extern function log::log (module: log::module_t, level: log::log_level_t, msg: string): () +function mutable_match (): () +{ + ((var m: ModifyMe) = (ModifyMe{.x="foo", .y=128'sd123456789}: ModifyMe); + match (m) { + (ModifyMe{.x=(var x: string), .y=128'sd123456789}: ModifyMe) -> x = "bar", + (_: ModifyMe) -> () + }) +} +function mutable_match_field (n: mut NestedStruct): () +{ + match (n.x) { + (std::Some{.x=(ModifyMe{.x=(var x: string), .y=128'sd123456789}: ModifyMe)}: std::Option) -> x = "bar", + (std::Some{.x=(var m: ModifyMe)}: std::Option) -> m.x = "bar", + (var x: std::Option) -> x = (std::Some{.x=(ModifyMe{.x="buzz", .y=128'sd0}: ModifyMe)}: std::Option) + } +} function myfunc (x: string): string { x @@ -1096,6 +1114,7 @@ output relation InspectSimpleSum [InspectSimpleSum] input relation Ints [Ints] output relation MapOfMaps [MapOfMaps] output relation MapOfVecs [MapOfVecs] +output relation Nested [Nested] relation Objects [Objects] output relation OutputInspectNot [OutputInspectNot] relation ParsedChunk [ParsedChunk] @@ -1148,10 +1167,19 @@ OutputInspectNot[(OutputInspectNot{.x=x, .y=y}: OutputInspectNot)] :- InputInspe "delete" }) ++ ": x=") ++ (std::__builtin_2string(y): string)) ++ " y=") ++ (std::__builtin_2string(y): string))), Inspect debug::debug_event((32'd10, 32'd2, 32'd0), ddlog_weight, ddlog_timestamp, "Inspect", (x, y), (OutputInspectNot{.x=x, .y=y}: OutputInspectNot)). TI_R[(TI_R{.a=a}: TI_R)] :- TI_R[(__ti_r0@ (TI_R{.a=(a: std::Set)}: TI_R))], (std::set_size(a) > 64'd1), Inspect debug::debug_event((32'd11, 32'd1, 32'd0), ddlog_weight, ddlog_timestamp, "Condition", __ti_r0, (TI_R{.a=a}: TI_R)). -ChunkParseError[(ChunkParseError{.err=err}: ChunkParseError)] :- ParsedChunk[(__parsedchunk0@ (ParsedChunk{.data=(std::Err{.err=(err: string)}: std::Result)}: ParsedChunk))], Inspect debug::debug_event((32'd12, 32'd0, 32'd0), ddlog_weight, ddlog_timestamp, "Map", __parsedchunk0, (ChunkParseError{.err=err}: ChunkParseError)). -ParsedChunk[(ParsedChunk{.data=(json::from_json_string(json): std::Result)}: ParsedChunk)] :- Chunk[(__chunk0@ (Chunk{.json=(json: string)}: Chunk))], Inspect debug::debug_event((32'd13, 32'd0, 32'd0), ddlog_weight, ddlog_timestamp, "Map", __chunk0, (ParsedChunk{.data=(json::from_json_string(json): std::Result)}: ParsedChunk)). -Objects[(Objects{.chunk=objs}: Objects)] :- ParsedChunk[(__parsedchunk0@ (ParsedChunk{.data=(std::Ok{.res=(objs: Object)}: std::Result)}: ParsedChunk))], Inspect debug::debug_event((32'd14, 32'd0, 32'd0), ddlog_weight, ddlog_timestamp, "Map", __parsedchunk0, (Objects{.chunk=objs}: Objects)). -CompressedChunk[(CompressedChunk{.json=json}: CompressedChunk)] :- Objects[(__objects0@ (Objects{.chunk=(objs: Object)}: Objects))], (std::Ok{.res=(var json: string)}: std::Result) = json::to_json_string(objs), Inspect debug::debug_event((32'd15, 32'd1, 32'd0), ddlog_weight, ddlog_timestamp, "Condition", __objects0, (CompressedChunk{.json=json}: CompressedChunk)). +Nested[(Nested{.descr="1", .n=((var n: NestedStruct) = (NestedStruct{.x=(std::Some{.x=(ModifyMe{.x="foo", .y=128'sd123456789}: ModifyMe)}: std::Option)}: NestedStruct); + (mutable_match_field(n); + n))}: Nested)]. +Nested[(Nested{.descr="2", .n=((var n: NestedStruct) = (NestedStruct{.x=(std::Some{.x=(ModifyMe{.x="", .y=128'sd0}: ModifyMe)}: std::Option)}: NestedStruct); + (mutable_match_field(n); + n))}: Nested)]. +Nested[(Nested{.descr="3", .n=((var n: NestedStruct) = (NestedStruct{.x=(std::None{}: std::Option)}: NestedStruct); + (mutable_match_field(n); + n))}: Nested)]. +ChunkParseError[(ChunkParseError{.err=err}: ChunkParseError)] :- ParsedChunk[(__parsedchunk0@ (ParsedChunk{.data=(std::Err{.err=(err: string)}: std::Result)}: ParsedChunk))], Inspect debug::debug_event((32'd15, 32'd0, 32'd0), ddlog_weight, ddlog_timestamp, "Map", __parsedchunk0, (ChunkParseError{.err=err}: ChunkParseError)). +ParsedChunk[(ParsedChunk{.data=(json::from_json_string(json): std::Result)}: ParsedChunk)] :- Chunk[(__chunk0@ (Chunk{.json=(json: string)}: Chunk))], Inspect debug::debug_event((32'd16, 32'd0, 32'd0), ddlog_weight, ddlog_timestamp, "Map", __chunk0, (ParsedChunk{.data=(json::from_json_string(json): std::Result)}: ParsedChunk)). +Objects[(Objects{.chunk=objs}: Objects)] :- ParsedChunk[(__parsedchunk0@ (ParsedChunk{.data=(std::Ok{.res=(objs: Object)}: std::Result)}: ParsedChunk))], Inspect debug::debug_event((32'd17, 32'd0, 32'd0), ddlog_weight, ddlog_timestamp, "Map", __parsedchunk0, (Objects{.chunk=objs}: Objects)). +CompressedChunk[(CompressedChunk{.json=json}: CompressedChunk)] :- Objects[(__objects0@ (Objects{.chunk=(objs: Object)}: Objects))], (std::Ok{.res=(var json: string)}: std::Result) = json::to_json_string(objs), Inspect debug::debug_event((32'd18, 32'd1, 32'd0), ddlog_weight, ddlog_timestamp, "Condition", __objects0, (CompressedChunk{.json=json}: CompressedChunk)). Fib[(Fib{.x=64'd0, .f=fib(64'd0)}: Fib)]. Fib[(Fib{.x=64'd1, .f=fib(64'd1)}: Fib)]. Fib[(Fib{.x=64'd2, .f=fib(64'd2)}: Fib)]. @@ -1161,7 +1189,7 @@ Fib[(Fib{.x=64'd10, .f=fib(64'd10)}: Fib)]. Fib[(Fib{.x=64'd20, .f=fib(64'd20)}: Fib)]. Ack[(Ack{.m=64'd2, .n=64'd1, .a=ack(64'd2, 64'd1)}: Ack)]. Strings[(Strings{.descr="x={10:bit<12>}, y={10:float}, z={-4:signed<125>}", .str=((((("x=" ++ (std::__builtin_2string((12'd10: bit<12>)): string)) ++ ", y=") ++ (std::__builtin_2string((32'f10.0: float)): string)) ++ ", z=") ++ (std::__builtin_2string((- (128'sd4: signed<128>))): string))}: Strings)]. -Rseq[(Rseq{._s=(TSeq1{.x=(_l, (std::ref_new(_s): std::Ref))}: TSeq)}: Rseq)] :- Rletter[(__rletter0@ (Rletter{._l=(_l: string)}: Rletter))], Rseqs[(__rseqs1@ (Rseqs{._s=(_s: TSeq)}: Rseqs))], Inspect debug::debug_event_join((32'd25, 32'd1, 32'd0), ddlog_weight, ddlog_timestamp, __rletter0, __rseqs1, (Rseq{._s=(TSeq1{.x=(_l, (std::ref_new(_s): std::Ref))}: TSeq)}: Rseq)). +Rseq[(Rseq{._s=(TSeq1{.x=(_l, (std::ref_new(_s): std::Ref))}: TSeq)}: Rseq)] :- Rletter[(__rletter0@ (Rletter{._l=(_l: string)}: Rletter))], Rseqs[(__rseqs1@ (Rseqs{._s=(_s: TSeq)}: Rseqs))], Inspect debug::debug_event_join((32'd28, 32'd1, 32'd0), ddlog_weight, ddlog_timestamp, __rletter0, __rseqs1, (Rseq{._s=(TSeq1{.x=(_l, (std::ref_new(_s): std::Ref))}: TSeq)}: Rseq)). Try1[(Try1{.description="Isaac Newton", .result=try1("Isaac Newton")}: Try1)]. Try1[(Try1{.description="", .result=try1("")}: Try1)]. Try1[(Try1{.description="Albert_Einstein", .result=try1("Albert_Einstein")}: Try1)]. diff --git a/test/datalog_tests/simple2.dl b/test/datalog_tests/simple2.dl index 37a841395..24b6b8610 100644 --- a/test/datalog_tests/simple2.dl +++ b/test/datalog_tests/simple2.dl @@ -176,6 +176,44 @@ function write_to_tuple_field(): (string, u64) { m } +function mutable_match() { + var m = ModifyMe{"foo", 123456789}; + match (m) { + ModifyMe{x, 123456789} -> x = "bar", + _ -> () + } +} + +typedef NestedStruct = NestedStruct { + x: Option +} + +function mutable_match_field(n: mut NestedStruct) { + match (n.x) { + Some{ModifyMe{x, 123456789}} -> x = "bar", + Some{m} -> m.x = "bar", + x -> x = Some{ModifyMe{"buzz", 0}} + } +} + +output relation Nested(descr: string, n: NestedStruct) +Nested("1",{ + var n = NestedStruct{Some{ModifyMe{"foo", 123456789}}}; + n.mutable_match_field(); + n +}). +Nested("2",{ + var n = NestedStruct{Some{ModifyMe{"", 0}}}; + n.mutable_match_field(); + n +}). +Nested("3",{ + var n = NestedStruct{None}; + n.mutable_match_field(); + n +}). + + /* Test "multiset" relations. */ import json @@ -375,5 +413,3 @@ function shadow2(): () = { var v = "foo" } - - diff --git a/test/datalog_tests/simple2.dump.expected b/test/datalog_tests/simple2.dump.expected index 9c2f23907..1e4d85c01 100644 --- a/test/datalog_tests/simple2.dump.expected +++ b/test/datalog_tests/simple2.dump.expected @@ -18,6 +18,10 @@ MapOfMaps: MapOfMaps{.m = [("bar", [(-10, (10000, true)), (200, (2, false))]), ("foo", [(1, (1, true)), (2, (4, false))]), ("foobar", [])]}: +1 MapOfVecs: MapOfVecs{.m = [((0, 0), [0.1, -100, 0, 1000000]), ((100, -100), []), ((100, 100), [0.1, -100, 0, 1000000])]}: +1 +Nested: +Nested{.descr = "1", .n = NestedStruct{.x = std::Some{.x = ModifyMe{.x = "bar", .y = 123456789}}}}: +1 +Nested{.descr = "2", .n = NestedStruct{.x = std::Some{.x = ModifyMe{.x = "bar", .y = 0}}}}: +1 +Nested{.descr = "3", .n = NestedStruct{.x = std::Some{.x = ModifyMe{.x = "buzz", .y = 0}}}}: +1 RFloatToInt: RFloatToInt{._x = -333}: +1 StringMaps: