tutorial.md: Document variable mutability.

- Added tutorial section summarizing variable mutability rules.
- Added several positive and negative variable mutability tests.

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<u32> = 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> = 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

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) { () }
+         ^^^

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> = 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> = 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> = 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) { () }
+}

test/datalog_tests/simple2.debug.ast.expected

@@ -22,6 +22,8 @@ typedef Ints = Ints{x: bigint}
 typedef MapOfMaps = MapOfMaps{m: std::Map<string,std::Map<double,(std::usize, bool)>>}
 typedef MapOfVecs = MapOfVecs{m: std::Map<(std::u32, bigint),std::Vec<double>>}
 typedef ModifyMe = ModifyMe{x: string, y: std::s128}
+typedef Nested = Nested{descr: string, n: NestedStruct}
+typedef NestedStruct = NestedStruct{x: std::Option<ModifyMe>}
 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<string,string>
 extern function json::to_json_value (x: 'T): std::Result<json::JsonValue,string>
 #[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<ModifyMe>) -> x = "bar",
+        (std::Some{.x=(var m: ModifyMe)}: std::Option<ModifyMe>) -> m.x = "bar",
+        (var x: std::Option<ModifyMe>) -> x = (std::Some{.x=(ModifyMe{.x="buzz", .y=128'sd0}: ModifyMe)}: std::Option<ModifyMe>)
+    }
+}
 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<string>)}: 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<Object,string>)}: 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<Object,string>)}: 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<Object,string>)}: ParsedChunk)).
-Objects[(Objects{.chunk=objs}: Objects)] :- ParsedChunk[(__parsedchunk0@ (ParsedChunk{.data=(std::Ok{.res=(objs: Object)}: std::Result<Object,string>)}: 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<string,string>) = 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<ModifyMe>)}: 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<ModifyMe>)}: NestedStruct);
+                               (mutable_match_field(n);
+                                n))}: Nested)].
+Nested[(Nested{.descr="3", .n=((var n: NestedStruct) = (NestedStruct{.x=(std::None{}: std::Option<ModifyMe>)}: NestedStruct);
+                               (mutable_match_field(n);
+                                n))}: Nested)].
+ChunkParseError[(ChunkParseError{.err=err}: ChunkParseError)] :- ParsedChunk[(__parsedchunk0@ (ParsedChunk{.data=(std::Err{.err=(err: string)}: std::Result<Object,string>)}: 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<Object,string>)}: 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<Object,string>)}: ParsedChunk)).
+Objects[(Objects{.chunk=objs}: Objects)] :- ParsedChunk[(__parsedchunk0@ (ParsedChunk{.data=(std::Ok{.res=(objs: Object)}: std::Result<Object,string>)}: 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<string,string>) = 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>))}: 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>))}: TSeq)}: Rseq)).
+Rseq[(Rseq{._s=(TSeq1{.x=(_l, (std::ref_new(_s): std::Ref<TSeq>))}: 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>))}: 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)].

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<ModifyMe>
+}
+
+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"
 }
-
-

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: