From 998020263cda1930135f63e47b3ffbc05a7228dd Mon Sep 17 00:00:00 2001
From: David Duvenaud <duvenaud@gmail.com>
Date: Mon, 6 May 2024 17:24:49 -0400
Subject: [PATCH] Got sets working with new syntax and fixed tests.

---
 lib/set.dx         | 17 ++++++++---------
 tests/set-tests.dx |  8 ++++----
 2 files changed, 12 insertions(+), 13 deletions(-)

diff --git a/lib/set.dx b/lib/set.dx
index c92c6229f..3ed72e788 100644
--- a/lib/set.dx
+++ b/lib/set.dx
@@ -4,22 +4,22 @@ import sort
 
 '## Monoidal enforcement of uniqueness in sorted lists
 
-def last(xs:n=>a) -> Maybe a given (n|Ix, a) =
+def last(xs:n=>a) -> Maybe a given (n|Ix, a:Type) =
   s = size n
   case s == 0 of
     True -> Nothing
     False -> Just xs[unsafe_from_ordinal (unsafe_nat_diff s 1)]
 
-def first(xs:n=>a) -> Maybe a given (n|Ix, a) =
+def first(xs:n=>a) -> Maybe a given (n|Ix, a:Type) =
   s = size n
   case s == 0 of
     True -> Nothing
     False -> Just xs[unsafe_from_ordinal 0]
 
-def all_except_last(xs:n=>a) -> List a given (n|Ix, a) =
-  shortSize = Fin (size n -| 1)
-  allButLast = for i:shortSize. xs[unsafe_from_ordinal (ordinal i)]
-  AsList _ allButLast
+def all_except_last(xs:n=>a) -> List a given (n|Ix, a:Type) =
+  newlen = size n -| 1
+  allButLast = for i:(Fin newlen). xs[unsafe_from_ordinal (ordinal i)]
+  AsList newlen allButLast
 
 def merge_unique_sorted_lists(xlist:List a, ylist:List a) -> List a given (a|Eq) =
   # This function is associative, for use in a monoidal reduction.
@@ -39,8 +39,7 @@ def merge_unique_sorted_lists(xlist:List a, ylist:List a) -> List a given (a|Eq)
 
 def remove_duplicates_from_sorted(xs:n=>a) -> List a given (n|Ix, a|Eq) =
   xlists = for i:n. (AsList 1 [xs[i]])
-  reduce (AsList 0 []) merge_unique_sorted_lists xlists
-
+  reduce xlists (AsList 0 []) merge_unique_sorted_lists
 
 '## Sets
 
@@ -82,7 +81,7 @@ def set_intersect(
   UnsafeAsSet(nx, xs) = sx
   UnsafeAsSet(ny, ys) = sy
   # This could be done in O(nx + ny) instead of O(nx log ny).
-  isInYs = \x. case search_sorted_exact ys x of
+  isInYs = \x:a. case search_sorted_exact ys x of
     Just x -> True
     Nothing -> False
   AsList(n', intersection) = filter xs isInYs
diff --git a/tests/set-tests.dx b/tests/set-tests.dx
index dd40db9d3..da0cd5c52 100644
--- a/tests/set-tests.dx
+++ b/tests/set-tests.dx
@@ -1,10 +1,10 @@
 import set
 
--- check order invariance.
+# check order invariance.
 :p (to_set ["Bob", "Alice", "Charlie"]) == (to_set ["Charlie", "Bob", "Alice"])
 > True
 
--- check uniqueness.
+# check uniqueness.
 :p (to_set ["Bob", "Alice", "Alice", "Charlie"]) == (to_set ["Charlie", "Charlie", "Bob", "Alice"])
 > True
 
@@ -57,13 +57,13 @@ Person : Type = Element names2
 :p size Person
 > 3
 
--- Check that ordinal and unsafeFromOrdinal are inverses.
+# Check that ordinal and unsafeFromOrdinal are inverses.
 roundTrip = for i:Person.
   i == (unsafe_from_ordinal (ordinal i))
 :p all roundTrip
 > True
 
--- Check that member and value are inverses.
+# Check that member and value are inverses.
 roundTrip2 = for i:Person.
   s = value i
   ix = member s names2