|
| 1 | +import sort |
| 2 | + |
| 3 | + |
| 4 | +'### Monoidal enforcement of uniqueness in sorted lists |
| 5 | + |
| 6 | +def last {n a} (xs:n=>a) : Maybe a = |
| 7 | + s = size n |
| 8 | + case s == 0 of |
| 9 | + True -> Nothing |
| 10 | + False -> Just xs.(unsafeFromOrdinal n (s - 1)) |
| 11 | + |
| 12 | +def first {n a} (xs:n=>a) : Maybe a = |
| 13 | + s = size n |
| 14 | + case s == 0 of |
| 15 | + True -> Nothing |
| 16 | + False -> Just xs.(unsafeFromOrdinal n 0) |
| 17 | + |
| 18 | +def allExceptLast {n a} (xs:n=>a) : List a = |
| 19 | + shortSize = Fin (max 0 ((size n) - 1)) |
| 20 | + allButLast = view i:shortSize. xs.(unsafeFromOrdinal _ (ordinal i)) |
| 21 | + (AsList _ allButLast) |
| 22 | + |
| 23 | +def mergeUniqueSortedLists {a} [Eq a] (xlist:List a) (ylist:List a) : List a = |
| 24 | + -- This function is associative, for use in a monoidal reduction. |
| 25 | + -- Assumes all xs are <= all ys. |
| 26 | + -- The element at the end of xs might equal the |
| 27 | + -- element at the beginning of ys. If so, this |
| 28 | + -- function removes the duplicate when concatenating the lists. |
| 29 | + (AsList nx xs) = xlist |
| 30 | + (AsList _ ys) = ylist |
| 31 | + case last xs of |
| 32 | + Nothing -> ylist |
| 33 | + Just last_x -> case first ys of |
| 34 | + Nothing -> xlist |
| 35 | + Just first_y -> case last_x == first_y of |
| 36 | + False -> concat [xlist, ylist] |
| 37 | + True -> concat [allExceptLast xs, ylist] |
| 38 | + |
| 39 | +def removeDuplicatesFromSorted {n a} [Eq a] (xs:n=>a) : List a = |
| 40 | + xlists = for i:n. (AsList 1 [xs.i]) |
| 41 | + reduce (AsList 0 []) mergeUniqueSortedLists xlists |
| 42 | + |
| 43 | + |
| 44 | +'### Sets |
| 45 | + |
| 46 | +data Set a [Ord a] = |
| 47 | + -- Guaranteed to be in sorted order with unique elements, |
| 48 | + -- as long as no one else uses this constructor. |
| 49 | + -- Instead use the "toSet" function below. |
| 50 | + UnsafeAsSet n:Int elements:(Fin n => a) |
| 51 | + |
| 52 | +def toSet {n a} [Ord a] (xs:n=>a) : Set a = |
| 53 | + sorted_xs = sort xs |
| 54 | + (AsList n' sorted_unique_xs) = removeDuplicatesFromSorted sorted_xs |
| 55 | + UnsafeAsSet n' sorted_unique_xs |
| 56 | + |
| 57 | +def setSize {a} ((UnsafeAsSet n _):Set a) : Int = n |
| 58 | + |
| 59 | +instance {a} [Eq a] Eq (Set a) |
| 60 | + (==) = \(UnsafeAsSet _ xs) (UnsafeAsSet _ ys). |
| 61 | + (AsList _ xs) == (AsList _ ys) |
| 62 | + |
| 63 | +def setUnion {a} |
| 64 | + ((UnsafeAsSet nx xs):Set a) |
| 65 | + ((UnsafeAsSet ny ys):Set a) : Set a = |
| 66 | + combined = mergeSortedTables xs ys |
| 67 | + (AsList n' sorted_unique_xs) = removeDuplicatesFromSorted combined |
| 68 | + UnsafeAsSet _ sorted_unique_xs |
| 69 | + |
| 70 | +def setIntersect {a} |
| 71 | + ((UnsafeAsSet nx xs):Set a) |
| 72 | + ((UnsafeAsSet ny ys):Set a) : Set a = |
| 73 | + -- This could be done in O(nx + ny) instead of O(nx log ny). |
| 74 | + isInYs = \x. case searchSorted ys x of |
| 75 | + Just x -> True |
| 76 | + Nothing -> False |
| 77 | + (AsList n' intersection) = filter isInYs xs |
| 78 | + UnsafeAsSet _ intersection |
| 79 | + |
| 80 | + |
| 81 | +'### Index set for sets of strings |
| 82 | + |
| 83 | +-- Todo: Make polymorphic in type. Waiting on a bugfix. |
| 84 | +-- data SetIx a l:(Set a) [Ord a] = |
| 85 | + |
| 86 | +data StringSetIx l:(Set String) = |
| 87 | + MkSetIx Int -- TODO: Use (Fin (setSize l)) instead. |
| 88 | + |
| 89 | +instance {set} Ix (StringSetIx set) |
| 90 | + getSize = \(). setSize set |
| 91 | + ordinal = \(MkSetIx i). i |
| 92 | + unsafeFromOrdinal = \k. MkSetIx k |
| 93 | + |
| 94 | +instance {set} Eq (StringSetIx set) |
| 95 | + (==) = \ix1 ix2. ordinal ix1 == ordinal ix2 |
| 96 | + |
| 97 | +-- Todo: Add an interface for converting to and from integer indices. |
| 98 | +-- Compiler can't handle the associated type yet. |
| 99 | +-- interface AssocIx n -- index sets where indices have data associated with them |
| 100 | +-- IxValueType : Type |
| 101 | +-- ixValue : n -> IxValueType n |
| 102 | +-- lookupIx : IxValueType n -> n |
| 103 | + |
| 104 | +def stringToSetIx {set:Set String} (s:String) : Maybe (StringSetIx set) = |
| 105 | + (UnsafeAsSet n elements) = set |
| 106 | + maybeIx = searchSorted elements s |
| 107 | + case maybeIx of |
| 108 | + Nothing -> Nothing |
| 109 | + Just i -> Just $ MkSetIx (ordinal i) |
| 110 | + |
| 111 | +def setIxToString {set:Set String} (ix:StringSetIx set) : String = |
| 112 | + (UnsafeAsSet n elements) = set |
| 113 | + elements.(unsafeFromOrdinal _ (ordinal ix)) |
| 114 | + |
0 commit comments