Fixed a very rare solver/evaluator disagreement on map key order

cozy/evaluation.py

@@ -679,7 +679,7 @@ def loop(stk):
         default = mkval(e.type.v)
         def make_map(stk):
             res = Map(e.type, default)
-            for (k, v) in reversed(list(stk.pop())):
+            for (k, v) in list(stk.pop()):
                 res[k] = v
             stk.append(res)
         out.append(make_map)

cozy/value_types.py

@@ -52,10 +52,10 @@ def __getitem__(self, k):
     def items(self):
         yield from self._items
     def keys(self):
-        for (k, v) in reversed(self._items):
+        for (k, v) in self.items():
             yield k
     def values(self):
-        for (k, v) in self._items:
+        for (k, v) in self.items():
             yield v
     def _hashable(self):
         return (self.default,) + tuple(sorted(self._items))

tests/evaluation.py

@@ -72,3 +72,20 @@ def test_bag_equality_with_tuple(self):
     def test_makerecord(self):
         e = EMakeRecord((('orderkey', ENum(0).with_type(TInt())), ('custkey', ENum(0).with_type(TInt())), ('orderstatus', ENative(ENum(0).with_type(TInt())).with_type(TNative('char'))), ('totalprice', ENum(0).with_type(TFloat())), ('orderdate', ENative(ENum(0).with_type(TInt())).with_type(TNative('uint64_t'))), ('orderpriority', EStr('').with_type(TString())), ('clerk', EStr('').with_type(TString())), ('shippriority', ENum(0).with_type(TInt())), ('comment', EStr('').with_type(TString())))).with_type(TRecord((('orderkey', TInt()), ('custkey', TInt()), ('orderstatus', TNative('char')), ('totalprice', TFloat()), ('orderdate', TNative('uint64_t')), ('orderpriority', TString()), ('clerk', TString()), ('shippriority', TInt()), ('comment', TString()))))
         uneval(e.type, eval(e, {}))
+
+    def test_distinct_order(self):
+        env = {
+            "xs": Bag([0, 1, 0]),
+        }
+        e = EUnaryOp(UOp.Distinct, EVar("xs").with_type(INT_BAG)).with_type(INT_BAG)
+        self.assertEqual(eval(e, env), Bag([0, 1]))
+
+    def test_map_keys1(self):
+        m = Map(TMap(INT, INT), 0, [(0, 1), (1, 2)])
+        ks = list(m.keys())
+        self.assertEqual(ks, [0, 1])
+
+    def test_map_keys2(self):
+        m = Map(TMap(INT, INT), 0, [(0, 1), (1, 2), (0, 3)])
+        ks = list(m.keys())
+        self.assertEqual(ks, [0, 1])

tests/semantics.py

@@ -25,7 +25,7 @@ def dbg(model):
             print(" ---> {!r}".format(r2))
         assert satisfy(EAll([
             assumptions,
-            ENot(EBinOp(e1, op, e2).with_type(BOOL))]), model_callback=dbg) is None
+            ENot(EBinOp(e1, op, e2).with_type(BOOL))]), model_callback=dbg, validate_model=True) is None
 
     def test_distinct_mapkeys(self):
         xs = EVar("xs").with_type(INT_BAG)