Address review comments.

lib/std.dl

@@ -513,14 +513,16 @@ function resize(v: mut Vec<'X>, new_len: usize, value: 'X) {
 
 /* Swap value at index `idx` for `value`.
  * Stores the old value at this index in `value` unless `idx` exceeds
- * the size of the vector (in which case the vector remains unmodified). */
-function swap_nth(v: mut Vec<'X>, idx: usize, value: mut 'X) {
+ * the size of the vector (in which case the vector remains unmodified).
+ * Returns true if the swap happened and false otherwise. */
+function swap_nth(v: mut Vec<'X>, idx: usize, value: mut 'X): bool {
     vec_swap_nth(v, idx, value)
 }
 
 /* Set value at index `idx` to `value`.
- * If `idx` exceeds the size of the vector (in which case the vector remains unmodified). */
-function update_nth(v: mut Vec<'X>, idx: usize, value: 'X) {
+ * If `idx` exceeds the size of the vector (in which case the vector remains unmodified).
+ * Returns true if updated happened and false otherwise. */
+function update_nth(v: mut Vec<'X>, idx: usize, value: 'X): bool {
     vec_update_nth(v, idx, value)
 }
 
@@ -565,6 +567,10 @@ function union(m1: Map<'K, 'V>, m2: Map<'K,'V>): Map<'K, 'V> {
     map_union(m1, m2)
 }
 
+function keys(m: Map<'K, 'V>): Vec<'K> {
+    map_keys(m)
+}
+
 /*
  * Set
  */
@@ -664,8 +670,8 @@ extern function vec_to_set(s: Vec<'A>): Set<'A>
 extern function vec_sort(v: mut Vec<'X>)
 extern function vec_sort_imm(v: Vec<'X>): Vec<'X>
 extern function vec_resize(v: mut Vec<'X>, new_len: usize, value: 'X)
-extern function vec_swap_nth(v: mut Vec<'X>, idx: usize, value: mut 'X)
-extern function vec_update_nth(v: mut Vec<'X>, idx: usize, value: 'X)
+extern function vec_swap_nth(v: mut Vec<'X>, idx: usize, value: mut 'X): bool
+extern function vec_update_nth(v: mut Vec<'X>, idx: usize, value: 'X): bool
 
 extern function map_size(m: Map<'K, 'V>): usize
 extern function map_insert(m: mut Map<'K,'V>, k: 'K, v: 'V)
@@ -675,6 +681,7 @@ extern function map_get(m: Map<'K,'V>, k:'K): Option<'V>
 extern function map_contains_key(m: Map<'K,'V>, k: 'K): bool
 extern function map_is_empty(m: Map<'K,'V>): bool
 extern function map_union(m1: Map<'K, 'V>, m2: Map<'K,'V>): Map<'K, 'V>
+extern function map_keys(m: Map<'K, 'V>): Vec<'K>
 
 extern function set_size(s: Set<'X>): usize
 extern function set_insert(s: mut Set<'X>, v: 'X)

lib/std.rs

@@ -524,16 +524,20 @@ pub fn std_vec_resize<X: Clone>(v: &mut std_Vec<X>, new_len: &std_usize, value:
     v.resize(*new_len as usize, value)
 }
 
-pub fn std_vec_swap_nth<X: Clone>(v: &mut std_Vec<X>, idx: &std_usize, value: &mut X) {
+pub fn std_vec_swap_nth<X: Clone>(v: &mut std_Vec<X>, idx: &std_usize, value: &mut X) -> bool {
     if (*idx as usize) < v.x.len() {
         std::mem::swap(&mut v.x[*idx as usize], value);
+        return true;
     };
+    return false;
 }
 
-pub fn std_vec_update_nth<X: Clone>(v: &mut std_Vec<X>, idx: &std_usize, value: &X) {
+pub fn std_vec_update_nth<X: Clone>(v: &mut std_Vec<X>, idx: &std_usize, value: &X) -> bool {
     if (*idx as usize) < v.x.len() {
         v.x[*idx as usize] = value.clone();
-    }
+        return true;
+    };
+    return false;
 }
 
 // Set
@@ -1001,6 +1005,12 @@ pub fn std_map_union<K: Ord + Clone, V: Clone>(
     m
 }
 
+pub fn std_map_keys<K: Ord + Clone, V>(m: &std_Map<K, V>) -> std_Vec<K> {
+    std_Vec {
+        x: m.x.keys().cloned().collect(),
+    }
+}
+
 // strings
 
 pub fn std___builtin_2string<T: Display>(x: &T) -> String {

src/Language/DifferentialDatalog/NS.hs

@@ -147,8 +147,8 @@ arg2v f a = ArgVar f (name a)
 ctxAllVars :: DatalogProgram -> ECtx -> [Var]
 ctxAllVars d ctx = let (lvs, rvs) = ctxVars' d ctx False in lvs ++ rvs
 
--- All variables visible in the 'ctx', classified into (writable, read-only
--- varables).
+-- All variables visible in 'ctx', classified into (writable, read-only)
+-- variables.
 -- This function is _unsafe_ to use before type inference.
 ctxVars :: DatalogProgram -> ECtx -> ([Var], [Var])
 ctxVars d ctx = ctxVars' d ctx True
@@ -157,7 +157,8 @@ ctxVars d ctx = ctxVars' d ctx True
 --
 -- The 'with_types' flag is true if 'd' contains enough type information
 -- to determine variable types (i.e., it has been through type inference).
--- When false, `ctxVars` may misclassify
+-- When false, `ctxVars` may misclassify variables, so it should only be
+-- invoked this way in situations where variable mutability does not matter.
 ctxVars' :: DatalogProgram -> ECtx -> Bool -> ([Var], [Var])
 ctxVars' d ctx with_types =
     case ctx of

test/datalog_tests/lib_test.debug.ast.expected

@@ -844,6 +844,10 @@ function std::key (g: std::Group<'K,'V>): 'K
 {
     (std::group_key(g): 'K)
 }
+function std::keys (m: std::Map<'K,'V>): std::Vec<'K>
+{
+    (std::map_keys(m): std::Vec<'K>)
+}
 function std::len (s: string): std::usize
 {
     std::string_len(s)
@@ -858,6 +862,7 @@ extern function std::map_get (m: std::Map<'K,'V>, k: 'K): std::Option<'V>
 extern function std::map_insert (m: mut std::Map<'K,'V>, k: 'K, v: 'V): ()
 extern function std::map_insert_imm (m: std::Map<'K,'V>, k: 'K, v: 'V): std::Map<'K,'V>
 extern function std::map_is_empty (m: std::Map<'K,'V>): bool
+extern function std::map_keys (m: std::Map<'K,'V>): std::Vec<'K>
 extern function std::map_remove (m: mut std::Map<'K,'V>, k: 'K): std::Option<'V>
 extern function std::map_singleton (k: 'K, v: 'V): std::Map<'K,'V>
 extern function std::map_size (m: std::Map<'K,'V>): std::usize
@@ -1038,7 +1043,7 @@ function std::substr (s: string, start: std::usize, end: std::usize): string
 {
     std::string_substr(s, start, end)
 }
-function std::swap_nth (v: mut std::Vec<'X>, idx: std::usize, value: mut 'X): ()
+function std::swap_nth (v: mut std::Vec<'X>, idx: std::usize, value: mut 'X): bool
 {
     std::vec_swap_nth(v, idx, value)
 }
@@ -1199,7 +1204,7 @@ function std::unwrap_or_default (res: std::Result<'V,'E>): 'V
 {
     (std::result_unwrap_or_default(res): 'V)
 }
-function std::update_nth (v: mut std::Vec<'X>, idx: std::usize, value: 'X): ()
+function std::update_nth (v: mut std::Vec<'X>, idx: std::usize, value: 'X): bool
 {
     std::vec_update_nth(v, idx, value)
 }
@@ -1216,9 +1221,9 @@ extern function std::vec_set_nth (v: std::Vec<'X>, n: std::usize, value: 'X): ()
 extern function std::vec_singleton (x: 'X): std::Vec<'X>
 extern function std::vec_sort (v: mut std::Vec<'X>): ()
 extern function std::vec_sort_imm (v: std::Vec<'X>): std::Vec<'X>
-extern function std::vec_swap_nth (v: mut std::Vec<'X>, idx: std::usize, value: mut 'X): ()
+extern function std::vec_swap_nth (v: mut std::Vec<'X>, idx: std::usize, value: mut 'X): bool
 extern function std::vec_to_set (s: std::Vec<'A>): std::Set<'A>
-extern function std::vec_update_nth (v: mut std::Vec<'X>, idx: std::usize, value: 'X): ()
+extern function std::vec_update_nth (v: mut std::Vec<'X>, idx: std::usize, value: 'X): bool
 extern function std::vec_with_capacity (len: std::usize): std::Vec<'A>
 extern function std::vec_with_length (len: std::usize, x: 'A): std::Vec<'A>
 function std_test::alphabet_map (): std::Map<std::usize,string>
@@ -1358,9 +1363,9 @@ std_test::SortedVectorInPlace[(std_test::SortedVectorInPlace{.v=sorted}: std_tes
                                                                                                                                                                                                                                                       (std::sort(v2);
                                                                                                                                                                                                                                                        v2)), Inspect debug::debug_event((32'd1, 32'd1, 32'd0), ddlog_weight, ddlog_timestamp, "Condition", __std_test_vector0, (std_test::SortedVectorInPlace{.v=sorted}: std_test::SortedVectorInPlace)).
 std_test::IntVecTest[(std_test::IntVecTest{.descr="vec0", .vec=std_test::vec0()}: std_test::IntVecTest)].
-std_test::IntVecTest[(std_test::IntVecTest{.descr="vec0.resize(10)", .vec=((var v: std::Vec<std::s64>) = std_test::vec0();
-                                                                           (std::resize(v, 64'd10, (- 64'sd100));
-                                                                            v))}: std_test::IntVecTest)].
+std_test::IntVecTest[(std_test::IntVecTest{.descr="vec0.resize(10,-100)", .vec=((var v: std::Vec<std::s64>) = std_test::vec0();
+                                                                                (std::resize(v, 64'd10, (- 64'sd100));
+                                                                                 v))}: std_test::IntVecTest)].
 std_test::IntVecTest[(std_test::IntVecTest{.descr="vec0.update_nth(10, -1)", .vec=((var v: std::Vec<std::s64>) = std_test::vec0();
                                                                                    (std::update_nth(v, 64'd10, (- 64'sd1));
                                                                                     v))}: std_test::IntVecTest)].

test/datalog_tests/simple.debug.ast.expected

@@ -1154,6 +1154,10 @@ function std::key (g: std::Group<'K,'V>): 'K
 {
     (std::group_key(g): 'K)
 }
+function std::keys (m: std::Map<'K,'V>): std::Vec<'K>
+{
+    (std::map_keys(m): std::Vec<'K>)
+}
 function std::len (s: string): std::usize
 {
     std::string_len(s)
@@ -1168,6 +1172,7 @@ extern function std::map_get (m: std::Map<'K,'V>, k: 'K): std::Option<'V>
 extern function std::map_insert (m: mut std::Map<'K,'V>, k: 'K, v: 'V): ()
 extern function std::map_insert_imm (m: std::Map<'K,'V>, k: 'K, v: 'V): std::Map<'K,'V>
 extern function std::map_is_empty (m: std::Map<'K,'V>): bool
+extern function std::map_keys (m: std::Map<'K,'V>): std::Vec<'K>
 extern function std::map_remove (m: mut std::Map<'K,'V>, k: 'K): std::Option<'V>
 extern function std::map_singleton (k: 'K, v: 'V): std::Map<'K,'V>
 extern function std::map_size (m: std::Map<'K,'V>): std::usize
@@ -1348,7 +1353,7 @@ function std::substr (s: string, start: std::usize, end: std::usize): string
 {
     std::string_substr(s, start, end)
 }
-function std::swap_nth (v: mut std::Vec<'X>, idx: std::usize, value: mut 'X): ()
+function std::swap_nth (v: mut std::Vec<'X>, idx: std::usize, value: mut 'X): bool
 {
     std::vec_swap_nth(v, idx, value)
 }
@@ -1509,7 +1514,7 @@ function std::unwrap_or_default (res: std::Result<'V,'E>): 'V
 {
     (std::result_unwrap_or_default(res): 'V)
 }
-function std::update_nth (v: mut std::Vec<'X>, idx: std::usize, value: 'X): ()
+function std::update_nth (v: mut std::Vec<'X>, idx: std::usize, value: 'X): bool
 {
     std::vec_update_nth(v, idx, value)
 }
@@ -1526,9 +1531,9 @@ extern function std::vec_set_nth (v: std::Vec<'X>, n: std::usize, value: 'X): ()
 extern function std::vec_singleton (x: 'X): std::Vec<'X>
 extern function std::vec_sort (v: mut std::Vec<'X>): ()
 extern function std::vec_sort_imm (v: std::Vec<'X>): std::Vec<'X>
-extern function std::vec_swap_nth (v: mut std::Vec<'X>, idx: std::usize, value: mut 'X): ()
+extern function std::vec_swap_nth (v: mut std::Vec<'X>, idx: std::usize, value: mut 'X): bool
 extern function std::vec_to_set (s: std::Vec<'A>): std::Set<'A>
-extern function std::vec_update_nth (v: mut std::Vec<'X>, idx: std::usize, value: 'X): ()
+extern function std::vec_update_nth (v: mut std::Vec<'X>, idx: std::usize, value: 'X): bool
 extern function std::vec_with_capacity (len: std::usize): std::Vec<'A>
 extern function std::vec_with_length (len: std::usize, x: 'A): std::Vec<'A>
 function strings (): ()

test/datalog_tests/simple2.debug.ast.expected

@@ -608,6 +608,10 @@ function std::key (g: std::Group<'K,'V>): 'K
 {
     (std::group_key(g): 'K)
 }
+function std::keys (m: std::Map<'K,'V>): std::Vec<'K>
+{
+    (std::map_keys(m): std::Vec<'K>)
+}
 function std::len (s: string): std::usize
 {
     std::string_len(s)
@@ -622,6 +626,7 @@ extern function std::map_get (m: std::Map<'K,'V>, k: 'K): std::Option<'V>
 extern function std::map_insert (m: mut std::Map<'K,'V>, k: 'K, v: 'V): ()
 extern function std::map_insert_imm (m: std::Map<'K,'V>, k: 'K, v: 'V): std::Map<'K,'V>
 extern function std::map_is_empty (m: std::Map<'K,'V>): bool
+extern function std::map_keys (m: std::Map<'K,'V>): std::Vec<'K>
 extern function std::map_remove (m: mut std::Map<'K,'V>, k: 'K): std::Option<'V>
 extern function std::map_singleton (k: 'K, v: 'V): std::Map<'K,'V>
 extern function std::map_size (m: std::Map<'K,'V>): std::usize
@@ -802,7 +807,7 @@ function std::substr (s: string, start: std::usize, end: std::usize): string
 {
     std::string_substr(s, start, end)
 }
-function std::swap_nth (v: mut std::Vec<'X>, idx: std::usize, value: mut 'X): ()
+function std::swap_nth (v: mut std::Vec<'X>, idx: std::usize, value: mut 'X): bool
 {
     std::vec_swap_nth(v, idx, value)
 }
@@ -963,7 +968,7 @@ function std::unwrap_or_default (res: std::Result<'V,'E>): 'V
 {
     (std::result_unwrap_or_default(res): 'V)
 }
-function std::update_nth (v: mut std::Vec<'X>, idx: std::usize, value: 'X): ()
+function std::update_nth (v: mut std::Vec<'X>, idx: std::usize, value: 'X): bool
 {
     std::vec_update_nth(v, idx, value)
 }
@@ -980,9 +985,9 @@ extern function std::vec_set_nth (v: std::Vec<'X>, n: std::usize, value: 'X): ()
 extern function std::vec_singleton (x: 'X): std::Vec<'X>
 extern function std::vec_sort (v: mut std::Vec<'X>): ()
 extern function std::vec_sort_imm (v: std::Vec<'X>): std::Vec<'X>
-extern function std::vec_swap_nth (v: mut std::Vec<'X>, idx: std::usize, value: mut 'X): ()
+extern function std::vec_swap_nth (v: mut std::Vec<'X>, idx: std::usize, value: mut 'X): bool
 extern function std::vec_to_set (s: std::Vec<'A>): std::Set<'A>
-extern function std::vec_update_nth (v: mut std::Vec<'X>, idx: std::usize, value: 'X): ()
+extern function std::vec_update_nth (v: mut std::Vec<'X>, idx: std::usize, value: 'X): bool
 extern function std::vec_with_capacity (len: std::usize): std::Vec<'A>
 extern function std::vec_with_length (len: std::usize, x: 'A): std::Vec<'A>
 function ti_f (value: std::Option<string>): std::Option<(string, string)>

test/datalog_tests/std_test.dl

@@ -17,7 +17,7 @@ SortedVectorInPlace(sorted) :-
 output relation IntVecTest(descr: string, vec: Vec<s64>)
 
 IntVecTest("vec0", vec0()).
-IntVecTest("vec0.resize(10)", {var v = vec0(); v.resize(10, -100); v}).
+IntVecTest("vec0.resize(10,-100)", {var v = vec0(); v.resize(10, -100); v}).
 IntVecTest("vec0.update_nth(10, -1)", {var v = vec0(); v.update_nth(10, -1); v}).
 IntVecTest("vec0.update_nth(1, -1)", {var v = vec0(); v.update_nth(1, -1); v}).
 IntVecTest("vec0.swap_nth(10, -1)", {

test/datalog_tests/std_test.dump.expected

@@ -29,7 +29,7 @@ std_test::MapDelete{.descr = "alphabet\\4\\3\\2", .m = [(0, "a"), (1, "b")], .s
 std_test::MapDelete{.descr = "alphabet\\4\\3\\2\\1", .m = [(0, "a")], .s = std::Some{.x = "b"}}
 std_test::MapDelete{.descr = "alphabet\\4\\3\\2\\1\\0", .m = [], .s = std::Some{.x = "a"}}
 std_test::IntVecTest{.descr = "vec0", .vec = [0, 1, 2, 3, 4, 5]}
-std_test::IntVecTest{.descr = "vec0.resize(10)", .vec = [0, 1, 2, 3, 4, 5, -100, -100, -100, -100]}
+std_test::IntVecTest{.descr = "vec0.resize(10,-100)", .vec = [0, 1, 2, 3, 4, 5, -100, -100, -100, -100]}
 std_test::IntVecTest{.descr = "vec0.swap_nth(10, -1)", .vec = [0, 1, 2, 3, 4, 5, -1]}
 std_test::IntVecTest{.descr = "vec0.swap_nth(5, -1)", .vec = [0, 1, 2, 3, 4, -1, 5]}
 std_test::IntVecTest{.descr = "vec0.update_nth(1, -1)", .vec = [0, -1, 2, 3, 4, 5]}

test/datalog_tests/tutorial.debug.ast.expected

@@ -525,6 +525,10 @@ function std::key (g: std::Group<'K,'V>): 'K
 {
     (std::group_key(g): 'K)
 }
+function std::keys (m: std::Map<'K,'V>): std::Vec<'K>
+{
+    (std::map_keys(m): std::Vec<'K>)
+}
 function std::len (s: string): std::usize
 {
     std::string_len(s)
@@ -539,6 +543,7 @@ extern function std::map_get (m: std::Map<'K,'V>, k: 'K): std::Option<'V>
 extern function std::map_insert (m: mut std::Map<'K,'V>, k: 'K, v: 'V): ()
 extern function std::map_insert_imm (m: std::Map<'K,'V>, k: 'K, v: 'V): std::Map<'K,'V>
 extern function std::map_is_empty (m: std::Map<'K,'V>): bool
+extern function std::map_keys (m: std::Map<'K,'V>): std::Vec<'K>
 extern function std::map_remove (m: mut std::Map<'K,'V>, k: 'K): std::Option<'V>
 extern function std::map_singleton (k: 'K, v: 'V): std::Map<'K,'V>
 extern function std::map_size (m: std::Map<'K,'V>): std::usize
@@ -719,7 +724,7 @@ function std::substr (s: string, start: std::usize, end: std::usize): string
 {
     std::string_substr(s, start, end)
 }
-function std::swap_nth (v: mut std::Vec<'X>, idx: std::usize, value: mut 'X): ()
+function std::swap_nth (v: mut std::Vec<'X>, idx: std::usize, value: mut 'X): bool
 {
     std::vec_swap_nth(v, idx, value)
 }
@@ -880,7 +885,7 @@ function std::unwrap_or_default (res: std::Result<'V,'E>): 'V
 {
     (std::result_unwrap_or_default(res): 'V)
 }
-function std::update_nth (v: mut std::Vec<'X>, idx: std::usize, value: 'X): ()
+function std::update_nth (v: mut std::Vec<'X>, idx: std::usize, value: 'X): bool
 {
     std::vec_update_nth(v, idx, value)
 }
@@ -897,9 +902,9 @@ extern function std::vec_set_nth (v: std::Vec<'X>, n: std::usize, value: 'X): ()
 extern function std::vec_singleton (x: 'X): std::Vec<'X>
 extern function std::vec_sort (v: mut std::Vec<'X>): ()
 extern function std::vec_sort_imm (v: std::Vec<'X>): std::Vec<'X>
-extern function std::vec_swap_nth (v: mut std::Vec<'X>, idx: std::usize, value: mut 'X): ()
+extern function std::vec_swap_nth (v: mut std::Vec<'X>, idx: std::usize, value: mut 'X): bool
 extern function std::vec_to_set (s: std::Vec<'A>): std::Set<'A>
-extern function std::vec_update_nth (v: mut std::Vec<'X>, idx: std::usize, value: 'X): ()
+extern function std::vec_update_nth (v: mut std::Vec<'X>, idx: std::usize, value: 'X): bool
 extern function std::vec_with_capacity (len: std::usize): std::Vec<'A>
 extern function std::vec_with_length (len: std::usize, x: 'A): std::Vec<'A>
 extern function string_slice_unsafe (x: string, from: bit<64>, to: bit<64>): string