diff --git a/hackett-lib/hackett/data/ord.rkt b/hackett-lib/hackett/data/ord.rkt new file mode 100644 index 0000000..baadbd1 --- /dev/null +++ b/hackett-lib/hackett/data/ord.rkt @@ -0,0 +1,76 @@ +#lang hackett + +(provide (data Ordering) + (class Ord)) + +(require hackett/data/identity) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Ord typeclass +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(data Ordering + lt + eq + gt) + + +(class (Eq A) => (Ord A) + [compare : {A -> A -> Ordering} + (λ [x y] (case* [{x le? y} {y le? x}] + [[True True] eq] + [[True False] lt] + [[False True] gt] + [[False False] (error! "Ord instance not totally ordered")]))] + ;; <=, >=, <, and > are defined by Hackett as functions on integers and I'm not confident that I + ;; can still write the Ord instance for integers if I shadow them here + [le? : {A -> A -> Bool} + (λ* [[x y] (case (compare x y) [gt False] [_ True])])] + [ge? : {A -> A -> Bool} (λ* [[x y] (case (compare x y) [lt False] [_ True])])] + [lt? : {A -> A -> Bool} (λ* [[x y] (case (compare x y) [lt True] [_ False])])] + [gt? : {A -> A -> Bool} (λ* [[x y] (case (compare x y) [gt True] [_ False])])]) + +(instance (Ord Integer) + [le? <=]) + +(instance (Ord Bool) + [compare (λ* [[False False] eq] + [[False True] lt] + [[True False] gt] + [[Tre True] eq])]) + +;; I couldn't find the actual implementation in Haskell but this seems to be what GHC does +(instance (∀ [A] (Ord A) => (Ord (List A))) + [compare + (λ* [[Nil Nil] eq] + [[Nil _] lt] + [[_ Nil] gt] + [[{x :: xs} {y :: ys}] + (case (compare x y) + [eq (compare xs ys)] + [ans ans])])]) + +(instance (∀ [A B] (Ord A) (Ord B) => (Ord (Tuple A B))) + [compare + (λ* [[(Tuple a1 b1) (Tuple a2 b2)] + (case (compare a1 a2) + [lt lt] + [gt gt] + [eq (compare b1 b2)])])]) + +(instance (∀ [A] (Ord A) => (Ord (Maybe A))) + [le? + (λ* [[Nothing _] True] + [[_ Nothing] False] + [[(Just x) (Just y)] (le? x y)])]) + +(instance (∀ [A B] (Ord A) (Ord B) => (Ord (Either A B))) + [le? + (λ* [[(Left x) (Left y)] (le? x y)] + [[(Left _) _] True] + [[_ (Left _)] False] + [[(Right x) (Right y)] (le? x y)])]) + +(instance (∀ [A] (Ord A) => (Ord (Identity A))) + [compare + (λ* [[(Identity x) (Identity y)] (compare x y)])]) \ No newline at end of file diff --git a/hackett-lib/hackett/data/set.rkt b/hackett-lib/hackett/data/set.rkt new file mode 100644 index 0000000..1ff3fef --- /dev/null +++ b/hackett-lib/hackett/data/set.rkt @@ -0,0 +1,1547 @@ +#lang hackett + +(require hackett/data/ord) + +(provide (data Set) ;; should put this in an internal thing but providing it for writing instances + (data Triple) + ;; query + null + size + member + not-member + lookupLT + lookupGT + lookupLE + lookupGE + ;; construction + empty + singleton + ;; insertion, deletion + insert + insertR + delete + ;; subset + isProperSubsetOf? + isSubsetOf? + ;; disjoint + disjoint + ;; minimal, maximal + lookupMin + findMin + lookupMax + findMax + deleteMin + deleteMax + ;; union + unions + union + ;; difference + difference + ;; intersection + intersection + ;; filter + set-filter + partition + ;; map + set-map + mapMonotonic + ;; fold + set-foldr + set-foldl + ;; lists + toAscList + toList + fromList + toDescList + fromAscList + fromDescList + fromDistinctAscList + fromDistinctDescList + ;; list variations + elems + ;; split + split + splitS + splitMember + ;; indexing + findIndex + lookupIndex + elemAt + deleteAt + take + drop + splitAt + takeWhileAntitone + dropWhileAntitone + spanAntitone + ;; + deleteFindMin + deleteFindMax + minView + maxView + ;; link + link + insertMax + insertMin + ;; merge + merge + ;; utilities + splitRoot + powerSet + cartesianProduct + (data MergeSet) + disjointUnion + ;; debugging + showTree + ;; assertions + valid + ordered + balanced + validsize) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Utilities +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; I believe these are a part of the `Bits` typeclass in Haskell + +(defn shiftL : {Integer -> Integer -> Integer} + [[x n] + (if {n == 0} + x + (shiftL {x * 2} {n - 1}))]) + +(defn shiftR : {Integer -> Integer -> Integer} + [[x n] + (if {n == 0} + x + (shiftR (quotient! x 2) {n - 1}))]) + +(def concat (foldr ++ "")) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Triples +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(data (Triple A B C) + (Triple A B C)) + +(instance (∀ [A B C] (Eq A) (Eq B) (Eq C) => (Eq (Triple A B C))) + [== (λ* [[(Triple a1 b1 c1) (Triple a2 b2 c2)] + {{a1 == a2} && {b1 == b2} && {c1 == c2}}])]) + +(instance (∀ [A B C] (Show A) (Show B) (Show C) => (Show (Triple A B C))) + [show (λ* [[(Triple a b c)] + {"Triple " ++ (show a) ++ " " ++ (show b) ++ " " ++ (show c)}])]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Set Datatype and Instances + +(data (Set A) + (Bin Integer A (Set A) (Set A)) + Tip) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Eq converts the set to a list. In a lazy setting, this +;; actually seems one of the faster methods to compare two trees +;; and it is certainly the simplest :-) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(instance (∀ [A] (Eq A) => (Eq (Set A))) + [== (λ* [[t1 t2] + {{(size t1) == (size t2)} && {(toAscList t1) == (toAscList t2)}}])]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Ord +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(instance (∀ [A] (Ord A) => (Ord (Set A))) + [compare (λ [s1 s2] (compare (toAscList s1) (toAscList s2)))]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Show +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(instance (∀ [A] (Show A) => (Show (Set A))) + [show (λ [s] {"fromList " ++ (show (toList s))})]) + +(instance (∀ [A] (Ord A) => (Semigroup (Set A))) + [++ union]) + +(instance (∀ [A] (Ord A) => (Monoid (Set A))) + [mempty empty]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Query +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; /O(1)/. Is this the empty set? +(defn null : (∀ [A] {(Set A) -> Bool}) + [[Tip] True] + [[(Bin _ _ _ _)] False]) + +;; /O(1)/. The number of elements in the set. +(defn size : (∀ [A] {(Set A) -> Integer}) + [[Tip] 0] + [[(Bin sz _ _ _)] sz]) + +;; apparently hackett can't infer typeclass constraints +;; explicitly quantifying these types is a PITA + +;; /O(log n)/. Is the element in the set? +(def member : (∀ [A] (Ord A) => {A -> (Set A) -> Bool}) + (letrec ([go + (λ* [[_ Tip] False] + [[x (Bin _ y l r)] + (case (compare x y) + [lt (go x l)] + [gt (go x r)] + [eq True])])]) + go)) + +;; /O(log n)/. Is the element not in the set? +(defn not-member : (∀ [A] (Ord A) => {A -> (Set A) -> Bool}) + [[a t] (not (member a t))]) + +;; /O(log n)/. Find largest element smaller than the given one. +;; +;; > lookupLT 3 (fromList [3, 5]) == Nothing +;; > lookupLT 5 (fromList [3, 5]) == Just 3 +(def lookupLT : (∀ [A] (Ord A) => {A -> (Set A) -> (Maybe A)}) + (letrec ([go-nothing + (λ* [[_ Tip] Nothing] + [[x (Bin _ y l r)] + (if {x le? y} + (go-nothing x l) + (go-just x y r))])] + [go-just + (λ* [[_ best Tip] (Just best)] + [[x best (Bin _ y l r)] + (if {x le? y} + (go-just x best l) + (go-just x y r))])]) + go-nothing)) + +;; /O(log n)/. Find smallest element greater than the given one. +;; +;; > lookupGT 4 (fromList [3, 5]) == Just 5 +;; > lookupGT 5 (fromList [3, 5]) == Nothing +(def lookupGT : (∀ [A] (Ord A) => {A -> (Set A) -> (Maybe A)}) + (letrec ([go-nothing + (λ* [[_ Tip] Nothing] + [[x (Bin _ y l r)] + (if {x lt? y} + (go-just x y l) + (go-nothing x r))])] + [go-just + (λ* [[_ best Tip] (Just best)] + [[x best (Bin _ y l r)] + (if {x lt? y} + (go-just x y l) + (go-just x best r))])]) + go-nothing)) + +;; | /O(log n)/. Find largest element smaller or equal to the given one. +;; +;; > lookupLE 2 (fromList [3, 5]) == Nothing +;; > lookupLE 4 (fromList [3, 5]) == Just 3 +;; > lookupLE 5 (fromList [3, 5]) == Just 5 +(def lookupLE : (∀ [A] (Ord A) => {A -> (Set A) -> (Maybe A)}) + (letrec ([go-nothing + (λ* [[_ Tip] Nothing] + [[x (Bin _ y l r)] + (case (compare x y) + [lt (go-nothing x l)] + [eq (Just y)] + [gt (go-just x y r)])])] + [go-just + (λ* [[_ best Tip] (Just best)] + [[x best (Bin _ y l r)] + (case (compare x y) + [lt (go-just x best l)] + [eq (Just y)] + [gt (go-just x y r)])])]) + go-nothing)) + +;; | /O(log n)/. Find smallest element greater or equal to the given one. +;; +;; > lookupGE 3 (fromList [3, 5]) == Just 3 +;; > lookupGE 4 (fromList [3, 5]) == Just 5 +;; > lookupGE 6 (fromList [3, 5]) == Nothing +(def lookupGE : (∀ [A] (Ord A) => {A -> (Set A) -> (Maybe A)}) + (letrec ([go-nothing + (λ* [[_ Tip] Nothing] + [[x (Bin _ y l r)] + (case (compare x y) + [lt (go-just x y l)] + [eq (Just y)] + [gt (go-nothing x r)])])] + [go-just + (λ* [[_ best Tip] (Just best)] + [[x best (Bin _ y l r)] + (case (compare x y) + [lt (go-just x y l)] + [eq (Just y)] + [gt (go-just x best r)])])]) + go-nothing)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; CONSTRUCTION +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; | /O(1)/. The empty set. +(def empty : (∀ [A] (Set A)) + Tip) + +;; | /O(1)/. Create a singleton set. +(defn singleton : (∀ [A] {A -> (Set A)}) + [[x] (Bin 1 x Tip Tip)]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Insertion, Deletion +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; /O(log n)/. Insert an element in a set. +;; If the set already contains an element equal to the given value, +;; it is replaced with the new value. +(defn insert : (∀ [A] (Ord A) => {A -> (Set A) -> (Set A)}) + [[x0] + (letrec ([go : (∀ [A] (Ord A) => {A -> A -> (Set A) -> (Set A)}) + (λ* [[orig _ Tip] (singleton (lazy orig))] + [[orig x (Bin sz y l r)] + (case (compare x y) + [lt (let ([l2 (go orig x l)]) + (if (ptr-eq? l2 l) + (Bin sz y l r) ;; this used an @ pattern originally + (balanceL y l2 r)))] + [gt (let ([r2 (go orig x r)]) + (if (ptr-eq? r2 r) + (Bin sz y l r) ;; this used an @ pattern originally + (balanceR y l r2)))] + [eq + (Bin sz (lazy orig) l r) + ;; since the desired semantics of this actually relies on ptr-eq, default to + ;; always reconstructing the node with the original argument + #;(if (ptr-eq? orig y) + (Bin sz y l r) ;; this used an @ pattern originally + (Bin sz (lazy orig) l r))])])]) + (go x0 x0))]) + +;; I don't know what this is for. +(defn lazy + [[x] x]) + +;; stand-in in case Hackett ever provides this +(defn ptr-eq? : (∀ [A] (Eq A) => {A -> A -> Bool}) + [[x y] {x == y}]) + +;; Insert an element to the set only if it is not in the set. +;; Used by `union`. +(defn insertR : (∀ [A] (Ord A) => {A -> (Set A) -> (Set A)}) + [[x0] + (letrec ([go : (∀ [A] (Ord A) => {A -> A -> (Set A) -> (Set A)}) + (λ* [[orig _ Tip] (singleton (lazy orig))] + [[orig x t] ;; @ pattern used + (case t + [(Bin _ y l r) + (case (compare x y) + [lt (let ([ll (go orig x l)]) + (if (ptr-eq? ll l) + t + (balanceL y ll r)))] + [gt (let ([rr (go orig x r)]) + (if (ptr-eq? rr r) + t + (balanceR y l rr)))] + [eq t])] + [_ undefined!])])]) + (go x0 x0))]) + +;; /O(log n)/. Delete an element from a set. +(def delete : (∀ [A] (Ord A) => {A -> (Set A) -> (Set A)}) + (letrec ([go : (∀ [A] (Ord A) => {A -> (Set A) -> (Set A)}) + (λ* [[_ Tip] Tip] + [[x (Bin s y l r)] ;; @ pattern used + (case (compare x y) + [lt (let ([ll (go x l)]) + (if (ptr-eq? ll l) + (Bin s y l r) + (balanceR y ll r)))] + [gt (let ([rr (go x r)]) + (if (ptr-eq? rr r) + (Bin s y l r) + (balanceL y l rr)))] + [eq (glue l r)])])]) + go)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Subset +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; /O(n+m)/. Is this a proper subset? (ie. a subset but not equal). +(defn isProperSubsetOf? : (∀ [A] (Ord A) => {(Set A) -> (Set A) -> Bool}) + [[s1 s2] {{(size s1) < (size s2)} && {s1 isSubsetOf? s2}}]) + +;; /O(n+m)/. Is this a subset? +;; @(s1 `isSubsetOf` s2)@ tells whether @s1@ is a subset of @s2@. +(defn isSubsetOf? : (∀ [A] (Ord A) => {(Set A) -> (Set A) -> Bool}) + [[t1 t2] {{(size t1) <= (size t2)} && {t1 isSubsetOfX? t2}}]) + +(defn isSubsetOfX? : (∀ [A] (Ord A) => {(Set A) -> (Set A) -> Bool}) + [[Tip _] True] + [[_ Tip] False] + [[(Bin _ x l r) t] + (case (splitMember x t) + [(Triple ls found gs) + {found && {l isSubsetOfX? ls} && {r isSubsetOfX? gs}}])]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Disjoint +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; /O(n+m)/. Check whether two sets are disjoint (i.e. their intersection +;; is empty). +;; +;; > disjoint (fromList [2,4,6]) (fromList [1,3]) == True +;; > disjoint (fromList [2,4,6,8]) (fromList [2,3,5,7]) == False +;; > disjoint (fromList [1,2]) (fromList [1,2,3,4]) == False +;; > disjoint (fromList []) (fromList []) == True +;; +(defn disjoint : (∀ [A] (Ord A) => {(Set A) -> (Set A) -> Bool}) + [[Tip _] True] + [[_ Tip] True] + [[(Bin _ x l r) t] + (case (splitMember x t) + [(Triple ls found gs) + {(not found) && (disjoint l ls) && (disjoint r gs)}])]) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Minimal, Maximal +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defn lookupMinSure : (∀ [A] {A -> (Set A) -> A}) + [[x Tip] x] + [[_ (Bin _ x l _)] (lookupMinSure x l)]) + +;; /O(log n)/. The minimal element of a set. +(defn lookupMin : (∀ [A] {(Set A) -> (Maybe A)}) + [[Tip] Nothing] + [[(Bin _ x l _)] (Just (lookupMinSure x l))]) + +;; /O(log n)/. The minimal element of a set. +(defn findMin : (∀ [A] {(Set A) -> A}) + [[t] (case (lookupMin t) + [(Just r) r] + [_ (error! "Set.findMin: empty set has no minimal element")])]) + +(defn lookupMaxSure : (∀ [A] {A -> (Set A) -> A}) + [[x Tip] x] + [[_ (Bin _ x _ r)] (lookupMaxSure x r)]) + +;; /O(log n)/. The maximal element of a set. +(defn lookupMax : (∀ [A] {(Set A) -> (Maybe A)}) + [[Tip] Nothing] + [[(Bin _ x _ r)] (Just (lookupMaxSure x r))]) + +;; /O(log n)/. The maximal element of a set. +(defn findMax : (∀ [A] {(Set A) -> A}) + [[t] (case (lookupMax t) + [(Just r) r] + [_ (error! "Set.findMin: empty set has no minimal element")])]) + +;; /O(log n)/. Delete the minimal element. Returns an empty set if the set is empty. +(defn deleteMin : (∀ [A] {(Set A) -> (Set A)}) + [[(Bin _ _ Tip r)] r] + [[(Bin _ x l r)] (balanceR x (deleteMin l) r)] + [[Tip] Tip]) + +;; /O(log n)/. Delete the maximal element. Returns an empty set if the set is empty. +(defn deleteMax : (∀ [A] {(Set A) -> (Set A)}) + [[(Bin _ _ l Tip)] l] + [[(Bin _ x l r)] (balanceL x l (deleteMax r))] + [[Tip] Tip]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Union +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; The union of a list of sets: (@'unions' == 'foldl' 'union' 'empty'@). +(def unions : (∀ [A] (Ord A) => {(List (Set A)) -> (Set A)}) + (foldl union empty)) + +;; /O(m*log(n\/m + 1)), m <= n/. The union of two sets, preferring the first set when +;; equal elements are encountered. +(defn union : (∀ [A] (Ord A) => {(Set A) -> (Set A) -> (Set A)}) + [[t1 Tip] t1] + [[t1 (Bin _ x Tip Tip)] (insertR x t1)] + [[(Bin _ x Tip Tip) t2] (insert x t2)] + [[Tip t2] t2] + [[(Bin s1 x l1 r1) t2] ;; @ pattern used + (case (splitS x t2) + [(Tuple l2 r2) + (let ([l1l2 (union l1 l2)] + [r1r2 (union r1 r2)]) + (if {(ptr-eq? l1l2 l1) && (ptr-eq? r1r2 r1)} + (Bin s1 x l1 r1) + (link x l1l2 r1r2)))])]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Difference +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; /O(m*log(n\/m + 1)), m <= n/. Difference of two sets. +(defn difference : (∀ [A] (Ord A) => {(Set A) -> (Set A) -> (Set A)}) + [[Tip _] Tip] + [[t1 Tip] t1] + [[t1 (Bin _ x l2 r2)] + (case (split x t1) + [(Tuple l1 r1) + (let ([l1l2 (difference l1 l2)] + [r1r2 (difference r1 r2)]) + (if {(size l1l2) + (size r1r2) == (size t1)} + t1 + (merge l1l2 r1r2)))])]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Intersection +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; /O(m*log(n\/m + 1)), m <= n/. The intersection of two sets. +;; Elements of the result come from the first set, so for example +;; +;; > import qualified Data.Set as S +;; > data AB = A | B deriving Show +;; > instance Ord AB where compare _ _ = EQ +;; > instance Eq AB where _ == _ = True +;; > main = print (S.singleton A `S.intersection` S.singleton B, +;; > S.singleton B `S.intersection` S.singleton A) +;; +;; prints @(fromList [A],fromList [B])@. +(defn intersection : (∀ [A] (Ord A) => {(Set A) -> (Set A) -> (Set A)}) + [[Tip _] Tip] + [[_ Tip] Tip] + [[t1 t2] ;; @ pattern used + (case t1 + [(Bin _ x l1 r1) + (case (splitMember x t2) + [(Triple l2 b r2) + (let ([l1l2 (intersection l1 l2)] + [r1r2 (intersection r1 r2)]) + (if b + (if {(ptr-eq? l1l2 l1) && (ptr-eq? r1r2 r1)} + t1 + (link x l1l2 r1r2)) + (merge l1l2 r1r2)))])] + [_ (error! ":'(")])]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Filter and partition +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; /O(n)/. Filter all elements that satisfy the predicate. +(defn set-filter : (∀ [A] (Eq A) => {{A -> Bool} -> (Set A) -> (Set A)}) + [[_ Tip] Tip] + [[p (Bin s x l r)] ;; @ pattern used + (let ([l2 (set-filter p l)] + [r2 (set-filter p r)]) + (if (p x) + (if {(ptr-eq? l l2) && (ptr-eq? r r2)} + (Bin s x l r) + (link x l2 r2)) + (merge l2 r2)))]) + +;; /O(n)/. Partition the set into two sets, one with all elements that satisfy +;; the predicate and one with all elements that don't satisfy the predicate. +;; See also 'split'. +(defn partition : (∀ [A] (Eq A) => {{A -> Bool} -> (Set A) -> (Tuple (Set A) (Set A))}) + [[p0 t0] + (letrec ([go (λ* [[_ Tip] (Tuple Tip Tip)] + [[p (Bin s x l r)] ;; @ pattern used + (case* [(go p l) (go p r)] + [[(Tuple l1 l2) (Tuple r1 r2)] + (if (p x) + (Tuple (if {(ptr-eq? l1 l) && (ptr-eq? r1 r)} + (Bin s x l r) + (link x l1 r1)) + (merge l2 r2)) + (Tuple (merge l1 r1) + (if {(ptr-eq? l2 l) && (ptr-eq? r2 r)} + (Bin s x l r) + (link x l2 r2))))])])]) + (go p0 t0))]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Map +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; /O(n*log n)/. +;; @'map' f s@ is the set obtained by applying @f@ to each element of @s@. +;; +;; It's worth noting that the size of the result may be smaller if, +; for some @(x,y)@, @x \/= y && f x == f y@ +(defn set-map : (∀ [A B] (Ord B) => {{A -> B} -> (Set A) -> (Set B)}) + [[f s] (fromList (map f (toList s)))]) + +;; | /O(n)/. The +;; +;; @'mapMonotonic' f s == 'map' f s@, but works only when @f@ is strictly increasing. +;; /The precondition is not checked./ +;; Semi-formally, we have: +;; +;; > and [x < y ==> f x < f y | x <- ls, y <- ls] +;; > ==> mapMonotonic f s == map f s +;; > where ls = toList s +(defn mapMonotonic : (∀ [A B] {{A -> B} -> (Set A) -> (Set B)}) + [[_ Tip] Tip] + [[f (Bin sz x l r)] (Bin sz (f x) (mapMonotonic f l) (mapMonotonic f r))]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Fold +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; /O(n)/. Fold the elements in the set using the given right-associative +;; binary operator, such that @'foldr' f z == 'Prelude.foldr' f z . 'toAscList'@. +;; +;; For example, +;; +;; > toAscList set = foldr (:) [] set +(defn set-foldr : (∀ [A B] {{A -> B -> B} -> B -> (Set A) -> B}) + [[f z] + (letrec [(go + (λ* [[zz Tip] zz] + [[zz (Bin _ x l r)] (go (f x (go zz r)) l)]))] + (go z))]) + +;; /O(n)/. Fold the elements in the set using the given left-associative +;; binary operator, such that @'foldl' f z == 'Prelude.foldl' f z . 'toAscList'@. +;; +;; For example, +;; +;; > toDescList set = foldl (flip (:)) [] set +(defn set-foldl : (∀ [A B] {{A -> B -> A} -> A -> (Set B) -> A}) + [[f z] + (letrec ([go (λ* [[z2 Tip] z2] + [[z2 (Bin _ x l r)] (go (f (go z2 l) x) r)])]) + (go z))]) + +;; currently doesn't typecheck, likely due to a bug in hackett +#;(defn foldMap : (∀ [A B] (Monoid B) => {{A -> B} -> (Set A) -> B}) + [[f t] + (letrec ([go (λ* [[Tip] mempty] + [[(Bin s k l r)] + (if {s == 1} + (f k) + {(go l) ++ {(f k) ++ (go r)}})])]) + (go t))]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Lists +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; /O(n)/. Convert the set to an ascending list of elements. Subject to list fusion. +(def toAscList : (∀ [A] {(Set A) -> (List A)}) + (set-foldr :: Nil)) + +;; /O(n)/. Convert the set to a list of elements. Subject to list fusion. +(def toList : (∀ [A] {(Set A) -> (List A)}) + toAscList) + +;; /O(n*log n)/. Create a set from a list of elements. +;; +;; If the elements are ordered, a linear-time implementation is used, +;; with the performance equal to 'fromDistinctAscList'. + +;; For some reason, when 'singleton' is used in fromList or in +;; create, it is not inlined, so we inline it manually. +(def fromList : (∀ [A] (Ord A) => {(List A) -> (Set A)}) + (letrec ([not-ordered? (λ* [[_ Nil] False] + [[x {y :: _}] {x ge? y}])] + [fromList2 (λ [t0 xs] (foldl (flip insert) t0 xs))] + [go (λ* [[_ t Nil] t] + [[_ t {x :: Nil}] (insertMax x t)] + [[s l {x :: xss}] ;; @ pattern used + (let ([xs {x :: xss}]) + (if (not-ordered? x xss) + (fromList2 l xs) + (case (create s xss) + [(Triple r ys Nil) (go (shiftL s 1) (link x l r) ys)] + [(Triple r _ ys) (fromList2 (link x l r) ys)])))])] + ;; The create is returning a triple (tree, xs, ys). Both xs and ys + ;; represent not yet processed elements and only one of them can be nonempty. + ;; If ys is nonempty, the keys in ys are not ordered with respect to tree + ;; and must be inserted using fromList'. Otherwise the keys have been + ;; ordered so far. + [create (λ* [[_ Nil] (Triple Tip Nil Nil)] + [[s {x :: xss}] ;; @ pattern used + (let ([xs {x :: xss}]) + (if {s == 1} + (if (not-ordered? x xss) + (Triple (Bin 1 x Tip Tip) Nil xss) + (Triple (Bin 1 x Tip Tip) xss Nil)) + (case (create (shiftR s 1) xs) + [(Triple a Nil b) (Triple a Nil b)] ;; @ pattern used + [(Triple l {y :: Nil} zs) (Triple (insertMax y l) Nil zs)] + [(Triple l {y :: yss} _) ;; @ pattern used + (let ([ys {y :: yss}]) + (if (not-ordered? y yss) + (Triple l Nil ys) + (case (create (shiftR s 1) yss) + [(Triple r zs ws) (Triple (link y l r) zs ws)])))] + [_ (error! "See above note about invariant")])))])]) + (λ* [[Nil] Tip] + [[{x :: Nil}] (Bin 1 x Tip Tip)] + [[{x0 :: xs0}] + (if (not-ordered? x0 xs0) + (fromList2 (Bin 1 x0 Tip Tip) xs0) + (go 1 (Bin 1 x0 Tip Tip) xs0))]))) + +;; /O(n)/. Convert the set to a descending list of elements. Subject to list +;; fusion. +(def toDescList : (∀ [A] {(Set A) -> (List A)}) + (set-foldl (flip ::) Nil)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Building trees from ascending/descending lists can be done in linear time. +;; +;; Note that if [xs] is ascending that: +;; fromAscList xs == fromList xs +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; /O(n)/. Build a set from an ascending list in linear time. +;; /The precondition (input list is ascending) is not checked./ +(defn fromAscList : (∀ [A] (Eq A) => {(List A) -> (Set A)}) + [[xs] (fromDistinctAscList (combineEq xs))]) + +;; /O(n)/. Build a set from a descending list in linear time. +;; /The precondition (input list is descending) is not checked./ +(defn fromDescList : (∀ [A] (Eq A) => {(List A) -> (Set A)}) + [[xs] (fromDistinctDescList (combineEq xs))]) + +;; [combineEq xs] combines equal elements with [const] in an ordered list [xs] +;; +;; TODO: combineEq allocates an intermediate list. It *should* be better to +;; make fromAscListBy and fromDescListBy the fundamental operations, and to +;; implement the rest using those. +(defn combineEq : (∀ [A] (Eq A) => {(List A) -> (List A)}) + [[Nil] Nil] + [[{x :: xs}] + (letrec ([combineEq2 (λ* [[z Nil] {z :: Nil}] + [[z {y :: ys}] + (if {z == y} + (combineEq2 z ys) + {z :: (combineEq2 y ys)})])]) + (combineEq2 x xs))]) + +;; | /O(n)/. Build a set from an ascending list of distinct elements in linear time. +;; /The precondition (input list is strictly ascending) is not checked./ + +;; For some reason, when 'singleton' is used in fromDistinctAscList or in +;; create, it is not inlined, so we inline it manually. +(defn fromDistinctAscList : (∀ [A] {(List A) -> (Set A)}) + [[Nil] Tip] + [[{x0 :: xs0}] + (letrec ([go (λ* [[_ t Nil] t] + [[s l {x :: xs}] + (case (create s xs) + [(Tuple r ys) (let ([t2 (link x l r)]) + (go (shiftL s 1) t2 ys))])])] + [create (λ* [[_ Nil] (Tuple Tip Nil)] + [[s {x :: xs2}] ;; @ pattern used + (let ([xs {x :: xs2}]) + (if {s == 1} + (Tuple (Bin 1 x Tip Tip) xs2) + (case (create (shiftR s 1) xs) + [(Tuple x Nil) (Tuple x Nil)] ;; @ pattern used + [(Tuple l {y :: ys}) + (case (create (shiftR s 1) ys) + [(Tuple r zs) (Tuple (link y l r) zs)])])))])]) + (go 1 (Bin 1 x0 Tip Tip) xs0))]) + +;; /O(n)/. Build a set from a descending list of distinct elements in linear time. +;; /The precondition (input list is strictly descending) is not checked./ + +;; For some reason, when 'singleton' is used in fromDistinctDescList or in +;; create, it is not inlined, so we inline it manually. +(defn fromDistinctDescList : (∀ [A] {(List A) -> (Set A)}) + [[Nil] Tip] + [[{x0 :: xs0}] + (letrec ([go (λ* [[_ t Nil] t] + [[s r {x :: xs}] + (case (create s xs) + [(Tuple l ys) (let ([t2 (link x l r)]) + (go (shiftL s 1) t2 ys))])])] + [create (λ* [[_ Nil] (Tuple Tip Nil)] + [[s {x :: xs2}] ;; @ pattern used + (let ([xs {x :: xs2}]) + (if {s == 1} + (Tuple (Bin 1 x Tip Tip) xs2) + (case (create (shiftR s 1) xs) + [(Tuple x Nil) (Tuple x Nil)] ;; @ pattern used + [(Tuple r {y :: ys}) + (case (create (shiftR s 1) ys) + [(Tuple l zs) (Tuple (link y l r) zs)])])))])]) + (go 1 (Bin 1 x0 Tip Tip) xs0))]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; List variations +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; /O(n)/. An alias of 'toAscList'. The elements of a set in ascending order. +;; Subject to list fusion. +(def elems : (∀ [A] {(Set A) -> (List A)}) + toAscList) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Split +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; /O(log n)/. The expression (@'split' x set@) is a pair @(set1,set2)@ +;; where @set1@ comprises the elements of @set@ less than @x@ and @set2@ +;; comprises the elements of @set@ greater than @x@. +(defn split : (∀ [A] (Ord A) => {A -> (Set A) -> (Tuple (Set A) (Set A))}) + [[x t] (splitS x t)]) + +;; originally returned a `StrictPair` +(defn splitS : (∀ [A] (Ord A) => {A -> (Set A) -> (Tuple (Set A) (Set A))}) + [[_ Tip] (Tuple Tip Tip)] + [[x (Bin _ y l r)] + (case (compare x y) + [lt (case (splitS x l) + [(Tuple ls gs) (Tuple ls (link y gs r))])] + [gt (case (splitS x r) + [(Tuple ls gs) (Tuple (link y l ls) gs)])] + [eq (Tuple l r)])]) + +(defn splitMember : (∀ [A] (Ord A) => {A -> (Set A) -> (Triple (Set A) Bool (Set A))}) + [[_ Tip] (Triple Tip False Tip)] + [[x (Bin _ y l r)] + (case (compare x y) + [lt (case (splitMember x l) + [(Triple ls found gs) + (let ([gs2 (link y gs r)]) + (Triple ls found gs2))])] + [gt (case (splitMember x r) + [(Triple ls found gs) + (let ([ls2 (link y l ls)]) + (Triple ls2 found gs))])] + [eq (Triple l True r)])]) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Indexing +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; /O(log n)/. Return the /index/ of an element, which is its zero-based +;; index in the sorted sequence of elements. The index is a number from /0/ up +;; to, but not including, the 'size' of the set. Calls 'error' when the element +;; is not a 'member' of the set. +;; +;; > findIndex 2 (fromList [5,3]) Error: element is not in the set +;; > findIndex 3 (fromList [5,3]) == 0 +;; > findIndex 5 (fromList [5,3]) == 1 +;; > findIndex 6 (fromList [5,3]) Error: element is not in the set + +(def findIndex : (∀ [A] (Ord A) => {A -> (Set A) -> Integer}) + (letrec ([go : (∀ [A] (Ord A) => {Integer -> A -> (Set A) -> Integer}) + (λ* [[_ _ Tip] (error! "Set.findIndex: element is not in the set")] + [[idx x (Bin _ kx l r)] + (case (compare x kx) + [lt (go idx x l)] + [gt (go {idx + (size l) + 1} x r)] + [eq {idx + (size l)}])])]) + (go 0))) + +;; /O(log n)/. Lookup the /index/ of an element, which is its zero-based index in +;; the sorted sequence of elements. The index is a number from /0/ up to, but not +;; including, the 'size' of the set. +;; +;; > isJust (lookupIndex 2 (fromList [5,3])) == False +;; > fromJust (lookupIndex 3 (fromList [5,3])) == 0 +;; > fromJust (lookupIndex 5 (fromList [5,3])) == 1 +;; > isJust (lookupIndex 6 (fromList [5,3])) == False +(def lookupIndex : (∀ [A] (Ord A) => {A -> (Set A) -> (Maybe Integer)}) + (letrec ([go : (∀ [A] (Ord A) => {Integer -> A -> (Set A) -> (Maybe Integer)}) + (λ* [[_ _ Tip] Nothing] + [[idx x (Bin _ kx l r)] + (case (compare x kx) + [lt (go idx x l)] + [gt (go {idx + (size l) + 1} x r)] + [eq (Just {idx + (size l)})])])]) + (go 0))) + +;; /O(log n)/. Retrieve an element by its /index/, i.e. by its zero-based +;; index in the sorted sequence of elements. If the /index/ is out of range (less +;; than zero, greater or equal to 'size' of the set), 'error' is called. +;; +;; > elemAt 0 (fromList [5,3]) == 3 +; > elemAt 1 (fromList [5,3]) == 5 +;; > elemAt 2 (fromList [5,3]) Error: index out of range +(defn elemAt : (∀ [A] {Integer -> (Set A) -> A}) + [[_ Tip] (error! "Set.elemAt: index out of range")] + [[i (Bin _ x l r)] + (let ([sizeL (size l)]) + (case (compare i sizeL) + [lt (elemAt i l)] + [gt (elemAt {i - sizeL - 1} r)] + [eq x]))]) + +;; /O(log n)/. Delete the element at /index/, i.e. by its zero-based index in +;; the sorted sequence of elements. If the /index/ is out of range (less than zero, +;; greater or equal to 'size' of the set), 'error' is called. +;; +;; > deleteAt 0 (fromList [5,3]) == singleton 5 +;; > deleteAt 1 (fromList [5,3]) == singleton 3 +;; > deleteAt 2 (fromList [5,3]) Error: index out of range +;; > deleteAt (-1) (fromList [5,3]) Error: index out of range +(defn deleteAt : (∀ [A] {Integer -> (Set A) -> (Set A)}) + [[i t] + (case t + [Tip (error! "Set.deleteAt: index out of range")] + [(Bin _ x l r) + (let ([sizeL (size l)]) + (case (compare i sizeL) + [lt (balanceR x (deleteAt i l) r)] + [gt (balanceL x l (deleteAt {i - sizeL - 1} r))] + [eq (glue l r)]))])]) + +;; Take a given number of elements in order, beginning +;; with the smallest ones. +;; +;; +;; take n = 'fromDistinctAscList' . 'Prelude.take' n . 'toAscList' +(defn take : (∀ [A] {Integer -> (Set A) -> (Set A)}) + [[i m] + (if {i > (size m)} + m + (if {i <= 0} + Tip + (letrec ([go (λ* [[i Tip] Tip] + [[i (Bin _ x l r)] + (let ([sizeL (size l)]) + (case (compare i sizeL) + [lt (go i l)] + [gt (link x l (go {i - sizeL - i} r))] + [eq l]))])]) + (go i m))))]) + +;; Drop a given number of elements in order, beginning +;; with the smallest ones. +;; +;; drop n = 'fromDistinctAscList' . 'Prelude.drop' n . 'toAscList' +(defn drop : (∀ [A] {Integer -> (Set A) -> (Set A)}) + [[i m] + (if {i >= (size m)} + Tip + (letrec ([go (λ* [[_ Tip] Tip] + [[i (Bin s x l r)] + (if {i < 0} + (Bin s x l r) + (let ([sizeL (size l)]) + (case (compare i sizeL) + [lt (link x (go i l) r)] + [gt (go {i - sizeL - 1} r)] + [eq (insertMin x r)])))])]) + (go i m)))]) + +(defn splitAt : (∀ [A] {Integer -> (Set A) -> (Tuple (Set A) (Set A))}) + [[i0 m0] + (if {i0 >= (size m0)} + (Tuple m0 Tip) + (letrec ([go (λ* [[_ Tip] (Tuple Tip Tip)] + [[i (Bin s x l r)] + (if {i <= 0} + (Tuple Tip (Bin s x l r)) + (let ([sizeL (size l)]) + (case (compare i sizeL) + [lt (case (go i l) + [(Tuple ll lr) (Tuple ll (link x lr r))])] + [gt (case (go {i - sizeL - 1} r) + [(Tuple rl rr) (Tuple (link x l rl) rr)])] + [eq (Tuple l (insertMin x r))])))])]) + (go i0 m0)))]) + +;; /O(log n)/. Take while a predicate on the elements holds. +;; The user is responsible for ensuring that for all elements @j@ and @k@ in the set, +;; @j \< k ==\> p j \>= p k@. See note at 'spanAntitone'. +;; +;; @ +;; takeWhileAntitone p = 'fromDistinctAscList' . 'Data.List.takeWhile' p . 'toList' +;; takeWhileAntitone p = 'set-filter' p +;; @ +(defn takeWhileAntitone : (∀ [A] {{A -> Bool} -> (Set A) -> (Set A)}) + [[_ Tip] Tip] + [[p (Bin _ x l r)] + (if (p x) + (link x l (takeWhileAntitone p r)) + (takeWhileAntitone p l))]) + +;; /O(log n)/. Drop while a predicate on the elements holds. +;; The user is responsible for ensuring that for all elements @j@ and @k@ in the set, +;; @j \< k ==\> p j \>= p k@. See note at 'spanAntitone'. +;; +;; @ +;; dropWhileAntitone p = 'fromDistinctAscList' . 'Data.List.dropWhile' p . 'toList' +;; dropWhileAntitone p = 'set-filter' (not . p) +;; @ +(defn dropWhileAntitone : (∀ [A] {{A -> Bool} -> (Set A) -> (Set A)}) + [[_ Tip] Tip] + [[p (Bin _ x l r)] + (if (p x) + (dropWhileAntitone p r) + (link x (dropWhileAntitone p l) r))]) + +;; | /O(log n)/. Divide a set at the point where a predicate on the elements stops holding. +;; The user is responsible for ensuring that for all elements @j@ and @k@ in the set, +;; @j \< k ==\> p j \>= p k@. +;; +;; @ +;; spanAntitone p xs = ('takeWhileAntitone' p xs, 'dropWhileAntitone' p xs) +;; spanAntitone p xs = partition p xs +;; @ +;; +;; Note: if @p@ is not actually antitone, then @spanAntitone@ will split the set +;; at some /unspecified/ point where the predicate switches from holding to not +;; holding (where the predicate is seen to hold before the first element and to fail +;; after the last element). +(defn spanAntitone : (∀ [A] {{A -> Bool} -> (Set A) -> (Tuple (Set A) (Set A))}) + [[p0 m] + (letrec ([go (λ* [[_ Tip] (Tuple Tip Tip)] + [[p (Bin _ x l r)] + (if (p x) + (case (go p r) + [(Tuple u v) (Tuple (link x l u) v)]) + (case (go p l) + [(Tuple u v) (Tuple u (link x v r))]))])]) + (go p0 m))]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +#| + [balance x l r] balances two trees with value x. + The sizes of the trees should balance after decreasing the + size of one of them. (a rotation). + + [delta] is the maximal relative difference between the sizes of + two trees, it corresponds with the [w] in Adams' paper. + [ratio] is the ratio between an outer and inner sibling of the + heavier subtree in an unbalanced setting. It determines + whether a double or single rotation should be performed + to restore balance. It is correspondes with the inverse + of $\alpha$ in Adam's article. + + Note that according to the Adam's paper: + - [delta] should be larger than 4.646 with a [ratio] of 2. + - [delta] should be larger than 3.745 with a [ratio] of 1.534. + + But the Adam's paper is errorneous: + - it can be proved that for delta=2 and delta>=5 there does + not exist any ratio that would work + - delta=4.5 and ratio=2 does not work + + That leaves two reasonable variants, delta=3 and delta=4, + both with ratio=2. + + - A lower [delta] leads to a more 'perfectly' balanced tree. + - A higher [delta] performs less rebalancing. + + In the benchmarks, delta=3 is faster on insert operations, + and delta=4 has slightly better deletes. As the insert speedup + is larger, we currently use delta=3. +|# +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(def delta 3) +(def ratio 2) + +#| +-- The balance function is equivalent to the following: +-- +-- balance :: a -> Set a -> Set a -> Set a +-- balance x l r +-- | sizeL + sizeR <= 1 = Bin sizeX x l r +-- | sizeR > delta*sizeL = rotateL x l r +-- | sizeL > delta*sizeR = rotateR x l r +-- | otherwise = Bin sizeX x l r +-- where +-- sizeL = size l +-- sizeR = size r +-- sizeX = sizeL + sizeR + 1 +-- +-- rotateL :: a -> Set a -> Set a -> Set a +-- rotateL x l r@(Bin _ _ ly ry) | size ly < ratio*size ry = singleL x l r +-- | otherwise = doubleL x l r +-- rotateR :: a -> Set a -> Set a -> Set a +-- rotateR x l@(Bin _ _ ly ry) r | size ry < ratio*size ly = singleR x l r +-- | otherwise = doubleR x l r +-- +-- singleL, singleR :: a -> Set a -> Set a -> Set a +-- singleL x1 t1 (Bin _ x2 t2 t3) = bin x2 (bin x1 t1 t2) t3 +-- singleR x1 (Bin _ x2 t1 t2) t3 = bin x2 t1 (bin x1 t2 t3) +-- +-- doubleL, doubleR :: a -> Set a -> Set a -> Set a +-- doubleL x1 t1 (Bin _ x2 (Bin _ x3 t2 t3) t4) = bin x3 (bin x1 t1 t2) (bin x2 t3 t4) +-- doubleR x1 (Bin _ x2 t1 (Bin _ x3 t2 t3)) t4 = bin x3 (bin x2 t1 t2) (bin x1 t3 t4) +-- +-- It is only written in such a way that every node is pattern-matched only once. +-- +-- Only balanceL and balanceR are needed at the moment, so balance is not here anymore. +-- In case it is needed, it can be found in Data.Map. + +-- Functions balanceL and balanceR are specialised versions of balance. +-- balanceL only checks whether the left subtree is too big, +-- balanceR only checks whether the right subtree is too big. +|# + +;; balanceL is called when left subtree might have been inserted to or when +;; right subtree might have been deleted from. +(defn balanceL : (∀ [A] {A -> (Set A) -> (Set A) -> (Set A)}) + [[x l r] + (case r + [Tip + (case l + [Tip (Bin 1 x Tip Tip)] + [(Bin _ _ Tip Tip) (Bin 2 x l Tip)] + [(Bin _ lx Tip (Bin _ lrx _ _)) + (Bin 3 lrx (Bin 1 lx Tip Tip) (Bin 1 x Tip Tip))] + [(Bin _ lx (Bin a b c d) Tip) (Bin 3 lx (Bin a b c d) (Bin 1 x Tip Tip))] ;; @ pattern + [(Bin ls lx (Bin lls a b c) (Bin lrs lrx lrl lrr)) + (if {lrs lt? {ratio * lls}} + (Bin {1 + ls} lx (Bin lls a b c) (Bin {1 + lrs} x (Bin lrs lrx lrl lrr) Tip)) + (Bin {1 + ls} lrx (Bin {1 + lls + (size lrl)} lx (Bin lls a b c) lrl) (Bin {1 + (size lrr)} x lrr Tip)))])] + [(Bin rs _ _ _) + (case l + [Tip (Bin {1 + rs} x Tip r)] + [(Bin ls lx ll lr) + (if {ls gt? {delta * rs}} + (case* [ll lr] + [[(Bin lls _ _ _) (Bin lrs lrx lrl lrr)] + (if {lrs lt? {ratio * lls}} + (Bin {1 + ls + rs} lx ll (Bin {1 + rs + lrs} x lr r)) + (Bin {1 + ls + rs} lrx (Bin {1 + lls + (size lrl)} lx ll lrl) (Bin {1 + rs + (size lrr)} x lrr r)))] + [[_ _] (error! "Failure in balanceL")]) + (Bin {1 + ls + rs} x l r))])])]) + + +;; balanceR is called when right subtree might have been inserted to or when +;; left subtree might have been deleted from. +(defn balanceR : (∀ [A] {A -> (Set A) -> (Set A) -> (Set A)}) + [[x l r] + (case l + [Tip + (case r + [Tip (Bin 1 x Tip Tip)] + [(Bin _ _ Tip Tip) (Bin 2 x Tip r)] + [(Bin _ rx Tip (Bin a b c d)) (Bin 3 rx (Bin 1 x Tip Tip) (Bin a b c d))] ;; @ pattern used + [(Bin _ rx (Bin _ rlx _ _) Tip) (Bin 3 rlx (Bin 1 x Tip Tip) (Bin 1 rx Tip Tip))] + [(Bin rs rx (Bin rls rlx rll rlr) (Bin rrs a b c)) + (if {rls lt? {ratio * rrs}} + (Bin {1 + rs} rx (Bin {1 + rls} x Tip (Bin rls rlx rll rlr)) (Bin rrs a b c)) + (Bin {1 + rs} rlx (Bin {1 + (size rll)} x Tip rll) (Bin {1 + rrs + (size rlr)} rx rlr (Bin rrs a b c))))])] + [(Bin ls _ _ _) + (case r + [Tip (Bin {1 + ls} x l Tip)] + [(Bin rs rx rl rr) + (if {rs gt? {delta * ls}} + (case* [rl rr] + [[(Bin rls rlx rll rlr) (Bin rrs _ _ _)] + (if {rls lt? {ratio * rrs}} + (Bin {1 + ls + rs} rx (Bin {1 + ls + rls} x l rl) rr) + (Bin {1 + ls + rs} rlx (Bin {1 + ls + (size rll)} x l rll) (Bin {1 + rrs + (size rlr)} rx rlr rr)))] + [[_ _] (error! "Failure in balanceR")]) + (Bin {1 + ls + rs} x l r))])])]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; The bin constructor maintains the size of the tree +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(defn bin : (∀ [A] {A -> (Set A) -> (Set A) -> (Set A)}) + [[x l r] (Bin {(size l) + (size r) + 1} x l r)]) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +#| + Utility functions that maintain the balance properties of the tree. + All constructors assume that all values in [l] < [x] and all values + in [r] > [x], and that [l] and [r] are valid trees. + + In order of sophistication: + [Bin sz x l r] The type constructor. + [bin x l r] Maintains the correct size, assumes that both [l] + and [r] are balanced with respect to each other. + [balance x l r] Restores the balance and size. + Assumes that the original tree was balanced and + that [l] or [r] has changed by at most one element. + [link x l r] Restores balance and size. + + Furthermore, we can construct a new tree from two trees. Both operations + assume that all values in [l] < all values in [r] and that [l] and [r] + are valid: + [glue l r] Glues [l] and [r] together. Assumes that [l] and + [r] are already balanced with respect to each other. + [merge l r] Merges two trees and restores balance. +|# +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; [glue l r]: glues two trees together. +;; Assumes that [l] and [r] are already balanced with respect to each other. +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(defn glue : (∀ [A] {(Set A) -> (Set A) -> (Set A)}) + [[Tip r] r] + [[l Tip] l] + [[(Bin sl xl ll lr) (Bin sr xr rl rr)] ;; @ patterns used + (if {sl > sr} + (case (maxViewSure xl ll lr) ;; pattern-matching `let` used originally + [(Tuple m ll) (balanceR m ll (Bin sr xr rl rr))]) + (case (minViewSure xr rl rr) + [(Tuple m rr) (balanceL m (Bin sl xl ll lr) rr)]))]) + +;; originially returned a `StrictPair` +(def minViewSure : (∀ [A] {A -> (Set A) -> (Set A) -> (Tuple A (Set A))}) + (letrec ([go (λ* [[x Tip r] (Tuple x r)] + [[x (Bin _ xl ll lr) r] + (case (go xl ll lr) + [(Tuple xm lll) (Tuple xm (balanceR x lll r))])])]) + go)) + +;; originially returned a `StrictPair` +(def maxViewSure : (∀ [A] {A -> (Set A) -> (Set A) -> (Tuple A (Set A))}) + (letrec ([go (λ* [[x l Tip] (Tuple x l)] + [[x l (Bin _ xr rl rr)] + (case (go xr rl rr) + [(Tuple xm rrr) (Tuple xm (balanceL x l rrr))])])]) + go)) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Link +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defn link : (∀ [A] {A -> (Set A) -> (Set A) -> (Set A)}) + [[x Tip r] (insertMin x r)] + [[x l Tip] (insertMax x l)] + [[x (Bin sizeL y ly ry) (Bin sizeR z lz rz)] ;; @ patterns used + (if {{delta * sizeL} < sizeR} + (balanceL z (link x (Bin sizeL y ly ry) lz) rz) + (if {{delta * sizeR} < sizeL} + (balanceR y ly (link x ry (Bin sizeR z lz rz))) + (bin x (Bin sizeL y ly ry) (Bin sizeR z lz rz))))]) +;; insertMin and insertMax don't perform potentially expensive comparisons. +(defn insertMax : (∀ [A] {A -> (Set A) -> (Set A)}) + [[x Tip] (singleton x)] + [[x (Bin _ y l r)] (balanceR y l (insertMax x r))]) + +(defn insertMin : (∀ [A] {A -> (Set A) -> (Set A)}) + [[x Tip] (singleton x)] + [[x (Bin _ y l r)] (balanceL y (insertMin x l) r)]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; [merge l r]: merges two trees. +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defn merge : (∀ [A] {(Set A) -> (Set A) -> (Set A)}) + [[Tip r] r] + [[l Tip] l] + [[l r] ;; @ pattern used + (case* [l r] + [[(Bin sizeL x lx rx) (Bin sizeR y ly ry)] + (if {{delta * sizeL} < sizeR} + (balanceL y (merge l ly) ry) + (if {{delta * sizeR} < sizeL} + (balanceR x lx (merge rx r)) + (glue l r)))] + [[_ _] (error! ":'(")])]) + +;; /O(log n)/. Delete and find the minimal element. +;; +;; > deleteFindMin set = (findMin set, deleteMin set) +(defn deleteFindMin : (∀ [A] {(Set A) -> (Tuple A (Set A))}) + [[t] (case (minView t) + [(Just r) r] + [_ (Tuple (error! "Set.deleteFindMin: can not return the minimal element of an empty set") + Tip)])]) + +;; /O(log n)/. Delete and find the maximal element. +;; +;; > deleteFindMax set = (findMax set, deleteMax set) +(defn deleteFindMax : (∀ [A] {(Set A) -> (Tuple A (Set A))}) + [[t] (case (maxView t) + [(Just r) r] + [_ (Tuple (error! "Set.deleteFindMax: can not return the maximal element of an empty set") + Tip)])]) + +;; /O(log n)/. Retrieves the minimal key of the set, and the set +;; stripped of that element, or 'Nothing' if passed an empty set. +(defn minView : (∀ [A] {(Set A) -> (Maybe (Tuple A (Set A)))}) + [[Tip] Nothing] + [[(Bin _ x l r)] (Just (minViewSure x l r))]) + +;; /O(log n)/. Retrieves the maximal key of the set, and the set +;; stripped of that element, or 'Nothing' if passed an empty set. +(defn maxView : (∀ [A] {(Set A) -> (Maybe (Tuple A (Set A)))}) + [[Tip] Nothing] + [[(Bin _ x l r)] (Just (maxViewSure x l r))]) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Utilities +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; /O(1)/. Decompose a set into pieces based on the structure of the underlying +;; tree. This function is useful for consuming a set in parallel. +;; +;; No guarantee is made as to the sizes of the pieces; an internal, but +;; deterministic process determines this. However, it is guaranteed that the pieces +;; returned will be in ascending order (all elements in the first subset less than all +;; elements in the second, and so on). +;; +;; Examples: +;; +;; > splitRoot (fromList [1..6]) == +;; > [fromList [1,2,3],fromList [4],fromList [5,6]] +;; +;; > splitRoot empty == [] +;; +;; Note that the current implementation does not return more than three subsets, +;; but you should not depend on this behaviour because it can change in the +;; future without notice. +(defn splitRoot : (∀ [A] {(Set A) -> (List (Set A))}) + [[Tip] Nil] + [[(Bin _ v l r)] {l :: (singleton v) :: r :: Nil}]) + +;; Calculate the power set of a set: the set of all its subsets. +;; +;; @ +;; t `member` powerSet s == t `isSubsetOf` s +;; @ +;; +;; Example: +;; +;; @ +;; powerSet (fromList [1,2,3]) = +;; fromList [[], [1], [2], [3], [1,2], [1,3], [2,3], [1,2,3]] +;; @ +(defn powerSet : (∀ [A] {(Set A) -> (Set (Set A))}) + [[xs0] + (letrec ([step (λ [x pxs] (glue (insertMin (singleton x) + (mapMonotonic (insertMin x) pxs)) + pxs))]) + (insertMin empty (set-foldr step Tip xs0)))]) + +;; Calculate the Cartesian product of two sets. +;; +;; @ +;; cartesianProduct xs ys = fromList $ liftA2 (,) (toList xs) (toList ys) +;; @ +;; +;; Example: +;; +;; @ +;; cartesianProduct (fromList [1,2]) (fromList ['a','b']) = +;; fromList [(1,'a'), (1,'b'), (2,'a'), (2,'b')] +;; @ +(defn cartesianProduct : (∀ [A B] (Ord A) (Ord B) => {(Set A) -> (Set B) -> (Set (Tuple A B))}) + [[as bs] + (fromList {(pure Tuple) <*> (toList as) <*> (toList bs)}) + ;; currently `foldMap` doesn't typecheck so don't use this implementation + #;(getMergeSet (foldMap (λ [a] (MergeSet (mapMonotonic (Tuple a) bs))) as))]) + +;; A version of Set with peculiar Semigroup and Monoid instances. +;; The result of xs <> ys will only be a valid set if the greatest +;; element of xs is strictly less than the least element of ys. +;; This is used to define cartesianProduct. +(data (MergeSet A) + (MergeSet (Set A))) + +(instance (∀ [A] (Semigroup (MergeSet A))) + [++ (λ* [[(MergeSet xs) (MergeSet ys)] (MergeSet (merge xs ys))])]) + +(instance (∀ [A] (Monoid (MergeSet A))) + [mempty (MergeSet empty)]) + +;; Calculate the disjoin union of two sets. +;; +;; @ disjointUnion xs ys = map Left xs `union` map Right ys @ +;; +;; Example: +;; +;; @ +;; disjointUnion (fromList [1,2]) (fromList ["hi", "bye"]) = +;; fromList [Left 1, Left 2, Right "hi", Right "bye"] +;; @ +(defn disjointUnion : (∀ [A B] {(Set A) -> (Set B) -> (Set (Either A B))}) + [[as bs] + (merge (mapMonotonic Left as) (mapMonotonic Right bs))]) + +#| +{-------------------------------------------------------------------- + Debugging +--------------------------------------------------------------------} +-- | /O(n)/. Show the tree that implements the set. The tree is shown +-- in a compressed, hanging format. +showTree :: Show a => Set a -> String +showTree s + = showTreeWith True False s + + +{- | /O(n)/. The expression (@showTreeWith hang wide map@) shows + the tree that implements the set. If @hang@ is + @True@, a /hanging/ tree is shown otherwise a rotated tree is shown. If + @wide@ is 'True', an extra wide version is shown. + +> Set> putStrLn $ showTreeWith True False $ fromDistinctAscList [1..5] +> 4 +> +--2 +> | +--1 +> | +--3 +> +--5 +> +> Set> putStrLn $ showTreeWith True True $ fromDistinctAscList [1..5] +> 4 +> | +> +--2 +> | | +> | +--1 +> | | +> | +--3 +> | +> +--5 +> +> Set> putStrLn $ showTreeWith False True $ fromDistinctAscList [1..5] +> +--5 +> | +> 4 +> | +> | +--3 +> | | +> +--2 +> | +> +--1 + +-} +showTreeWith :: Show a => Bool -> Bool -> Set a -> String +showTreeWith hang wide t + | hang = (showsTreeHang wide [] t) "" + | otherwise = (showsTree wide [] [] t) "" + +showsTree :: Show a => Bool -> [String] -> [String] -> Set a -> ShowS +showsTree wide lbars rbars t + = case t of + Tip -> showsBars lbars . showString "|\n" + Bin _ x Tip Tip + -> showsBars lbars . shows x . showString "\n" + Bin _ x l r + -> showsTree wide (withBar rbars) (withEmpty rbars) r . + showWide wide rbars . + showsBars lbars . shows x . showString "\n" . + showWide wide lbars . + showsTree wide (withEmpty lbars) (withBar lbars) l + +showsTreeHang :: Show a => Bool -> [String] -> Set a -> ShowS +showsTreeHang wide bars t + = case t of + Tip -> showsBars bars . showString "|\n" + Bin _ x Tip Tip + -> showsBars bars . shows x . showString "\n" + Bin _ x l r + -> showsBars bars . shows x . showString "\n" . + showWide wide bars . + showsTreeHang wide (withBar bars) l . + showWide wide bars . + showsTreeHang wide (withEmpty bars) r + +showWide :: Bool -> [String] -> String -> String +showWide wide bars + | wide = showString (concat (reverse bars)) . showString "|\n" + | otherwise = id + +showsBars :: [String] -> ShowS +showsBars bars + = case bars of + [] -> id + _ -> showString (concat (reverse (tail bars))) . showString node + +|# + +;; /O(n)/. Show the tree that implements the set. The tree is shown +;; in a compressed, hanging format. +(defn showTree : (∀ [A] (Show A) => {(Set A) -> String}) + [[s] (showTreeWith True False s)]) + +(defn showTreeWith : (∀ [A] (Show A) => {Bool -> Bool -> (Set A) -> String}) + [[hang wide t] + (if hang + (showsTreeHang wide Nil t) + (showsTree wide Nil Nil t))]) + +(defn showsTree : (∀ [A] (Show A) => {Bool -> (List String) -> (List String) -> (Set A) -> String}) + [[wide lbars rbars t] + (case t + [Tip {(showBars lbars) ++ "|\n"}] + [(Bin _ x Tip Tip) + {(showBars lbars) ++ (show x) ++ "\n"}] + [(Bin _ x l r) + {(showsTree wide (withBar rbars) (withEmpty rbars) r) + ++ (showWide wide rbars) + ++ (showBars lbars) ++ (show x) ++ "\n" + ++ (showWide wide lbars) + ++ (showsTree wide (withEmpty lbars) (withBar lbars) l)}])]) + + +(defn showsTreeHang : (∀ [A] (Show A) => {Bool -> (List String) -> (Set A) -> String}) + [[wide bars t] + (case t + [Tip {(showBars bars) ++ "|\n"}] + [(Bin _ x Tip Tip) {(showBars bars) ++ (show x) ++ "\n"}] + [(Bin _ x l r) + {(showBars bars) ++ (show x) ++ "\n" + ++ (showWide wide bars) + ++ (showsTreeHang wide (withBar bars) l) + ++ (showWide wide bars) + ++ (showsTreeHang wide (withEmpty bars) r)}])]) + +(defn showWide : {Bool -> (List String) -> String} + [[wide bars] + (if wide + {(concat (reverse bars)) ++ "|\n"} + "")]) + +(defn showBars : {(List String) -> String} + [[Nil] ""] + [[bars] {(concat (reverse (tail! bars))) ++ node}]) + +(def node : String + "+--") + +(defn withBar : {(List String) -> (List String)} + [[bars] {"| " :: bars}]) +(defn withEmpty : {(List String) -> (List String)} + [[bars] {" " :: bars}]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Assertions +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; /O(n)/. Test if the internal set structure is valid. +(defn valid : (∀ [A] (Ord A) => {(Set A) -> Bool}) + [[t] {(balanced t) && (ordered t) && (validsize t)}]) + +(defn ordered : (∀ [A] (Ord A) => {(Set A) -> Bool}) + [[t] + (letrec ([bounded (λ* [[lo hi t2] + (case t2 + [Tip True] + [(Bin _ x l r) {(lo x) + && (hi x) + && (bounded lo (λ [y] (lt? y x)) l) + && (bounded (λ [y] (gt? y x)) hi r)}])])]) + (bounded (const True) (const True) t))]) + +(defn balanced : (∀ [A] {(Set A) -> Bool}) + [[Tip] True] + [[(Bin _ _ l r)] + {{{(size l) + (size r) <= 1} || {{(size l) <= {delta * (size r)}} && {(size r) <= {delta * (size l)}}}} + && (balanced l) && (balanced r)}]) + +(def validsize : (∀ [A] {(Set A) -> Bool}) + (letrec ([realsize (λ* [[Tip] (Just 0)] + [[(Bin sz _ l r)] + (case (Tuple (realsize l) (realsize r)) + [(Tuple (Just n) (Just m)) + (if {sz == {n + m + 1}} + (Just sz) + Nothing)] + [_ Nothing])])]) + (λ [t] {(realsize t) == (Just (size t))}))) \ No newline at end of file diff --git a/hackett-lib/hackett/monad/state.rkt b/hackett-lib/hackett/monad/state.rkt new file mode 100644 index 0000000..e114dc8 --- /dev/null +++ b/hackett-lib/hackett/monad/state.rkt @@ -0,0 +1,321 @@ +#lang hackett + +(require hackett/monad/trans) + +(provide (for-type StateT) + runStateT + state + evalStateT + execStateT + mapStateT + withStateT + get + put + modify + gets) + + +;; adapted from +;; https://github.com/ghc/packages-transformers/blob/master/Control/Monad/Trans/State/Lazy.hs + +;; Lazy state monads, passing an updatable state through a computation. +;; See below for examples. +;; +;; Some computations may not require the full power of state transformers: +;; +;; * For a read-only state, see "Control.Monad.Trans.Reader". +;; +;; * To accumulate a value without using it on the way, see +;; "Control.Monad.Trans.Writer". +;; +;; In this version, sequencing of computations is lazy, so that for +;; example the following produces a usable result: +;; +;; > evalState (sequence $ repeat $ do { n <- get; put (n*2); return n }) 1 +;; +;; For a strict version with the same interface, see +;; "Control.Monad.Trans.State.Strict". + +;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; A state monad parameterized by the type @s@ of the state to carry. +;; +;; The 'return' function leaves the state unchanged, while @>>=@ uses +;; the final state of the first computation as the initial state of +;; the second. +;; type State s = StateT s Identity + +#| + + +-- | Unwrap a state monad computation as a function. +-- (The inverse of 'state'.) +runState :: State s a -- ^state-passing computation to execute + -> s -- ^initial state + -> (a, s) -- ^return value and final state +runState m = runIdentity . runStateT m +{-# INLINE runState #-} + +-- | Evaluate a state computation with the given initial state +-- and return the final value, discarding the final state. +-- +-- * @'evalState' m s = 'fst' ('runState' m s)@ +evalState :: State s a -- ^state-passing computation to execute + -> s -- ^initial value + -> a -- ^return value of the state computation +evalState m s = fst (runState m s) +{-# INLINE evalState #-} + +-- | Evaluate a state computation with the given initial state +-- and return the final state, discarding the final value. +-- +-- * @'execState' m s = 'snd' ('runState' m s)@ +execState :: State s a -- ^state-passing computation to execute + -> s -- ^initial value + -> s -- ^final state +execState m s = snd (runState m s) +{-# INLINE execState #-} + +-- | Map both the return value and final state of a computation using +-- the given function. +-- +-- * @'runState' ('mapState' f m) = f . 'runState' m@ +mapState :: ((a, s) -> (b, s)) -> State s a -> State s b +mapState f = mapStateT (Identity . f . runIdentity) +{-# INLINE mapState #-} + +-- | @'withState' f m@ executes action @m@ on a state modified by +-- applying @f@. +-- +-- * @'withState' f m = 'modify' f >> m@ +withState :: (s -> s) -> State s a -> State s a +withState = withStateT +{-# INLINE withState #-} +|# + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; this doesn't belong here +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(instance (∀ [a b] (Semigroup a) (Semigroup b) => (Semigroup (Tuple a b))) + [++ (λ* [[(Tuple a1 b1) (Tuple a2 b2)] + (Tuple {a1 ++ a2} {b1 ++ b2})])]) + +(instance (∀ [a b] (Monoid a) (Monoid b) => (Monoid (Tuple a b))) + [mempty (Tuple mempty mempty)]) + +;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; A state transformer monad parameterized by: +;; +;; * @s@ - The state. +;; +;; * @m@ - The inner monad. +;; +;; The 'return' function leaves the state unchanged, while @>>=@ uses +;; the final state of the first computation as the initial state of +;; the second. + +(data (StateT s m a) + (StateT {s -> (m (Tuple a s))})) + +(defn runStateT + [[(StateT f)] f]) + +;; Construct a state monad computation from a function. +;; (The inverse of 'runState'.) +(defn state : (∀ [m s a] (Monad m) => + {{s -> (Tuple a s)} -> (StateT s m a)}) + [[f] (StateT {pure . f})]) + +;; Evaluate a state computation with the given initial state +;; and return the final value, discarding the final state. +;; +;; * @'evalStateT' m s = 'liftM' 'fst' ('runStateT' m s)@ +(defn evalStateT : (∀ [m s a] (Monad m) => {(StateT s m a) -> s -> (m a)}) + [[m s] + (do [t <- (runStateT m s)] ;; this originally used a lazy pattern + (case t + [(Tuple a _) + (pure a)]))]) + +;; Evaluate a state computation with the given initial state +;; and return the final state, discarding the final value. +;; +;; * @'execStateT' m s = 'liftM' 'snd' ('runStateT' m s)@ +(defn execStateT : (∀ [m s a] (Monad m) => {(StateT s m a) -> s -> (m s)}) + [[m s] + (do [t <- (runStateT m s)] ;; this originally used a lazy pattern + (case t + [(Tuple _ s2) + (pure s2)]))]) + +;; Map both the return value and final state of a computation using +;; the given function. +;; +;; * @'runStateT' ('mapStateT' f m) = f . 'runStateT' m@ +(defn mapStateT : (∀ [m n s a b] {{(m (Tuple a s)) -> (n (Tuple b s))} + -> (StateT s m a) + -> (StateT s n b)}) + [[f m] (StateT {f . (runStateT m)})]) + +;; @'withStateT' f m@ executes action @m@ on a state modified by +;; applying @f@. +;; +;; * @'withStateT' f m = 'modify' f >> m@ +(defn withStateT : (∀ [s m a] {{s -> s} -> (StateT s m a) -> (StateT s m a)}) + [[f m] (StateT {(runStateT m) . f})]) + +(instance (∀ [m s] (Functor m) => (Functor (StateT s m))) + [map + (λ [f m] + (StateT (λ [s] + (map (λ [t] (case t + [(Tuple a sp) (Tuple (f a) sp)])) + (runStateT m s)))))]) + +(instance (∀ [m s] (Monad m) => (Applicative (StateT s m))) + [pure (λ [a] (StateT (λ [s] (pure (Tuple a s)))))] + [<*> + (λ* [[(StateT mf) (StateT mx)] + (StateT (λ [s] (do [t1 <- (mf s)] + [t2 <- (case t1 + [(Tuple f sp) (mx sp)])] + ;; because binding positions aren't patterns we have to match on t1 again to + ;; get f (or use a nested `do`) + (case* [t1 t2] + [[(Tuple f _) (Tuple x spp)] (pure (Tuple (f x) spp))]))))])]) + +;; not sure where this goes wrong + +;; this was originally an Alternative instance in terms of MonadPlus but I'm going to venture to say +;; Monoid subsumes both those classes in Hackett +#;(instance (∀ [m s a] (Monad m) (Monoid m) => (Semigroup (StateT s m a))) + [++ + (λ* [[(StateT m) (StateT n)] + (StateT (λ [s] {(m s) ++ (n s)}))])]) + + +#;(instance (∀ [m s] (Monad m) (Monoid m) => (Monoid (StateT s m))) + [mempty (StateT (λ [_] mempty))]) + +(instance (∀ [m s] (Monad m) => (Monad (StateT s m))) + [=<< + (λ* [[k m] + (StateT (λ [s] (do [t <- (runStateT m s)] + (case t + [(Tuple a sp) + (runStateT (k a) sp)]))))])]) + +(instance (∀ [s] (MonadTrans (StateT s))) + [lift + (λ [m] (StateT (λ [s] (do [a <- m] + (pure (Tuple a s))))))]) + +;; Fetch the current value of the state within the monad. +(def get : (∀ [m s] (Monad m) => (StateT s m s)) + (state (λ [s] (Tuple s s)))) + +;; @'put' s@ sets the state within the monad to @s@. +(defn put : (∀ [m s] (Monad m) => {s -> (StateT s m Unit)}) + [[s] (state (λ [_] (Tuple Unit s)))]) + +;; @'modify' f@ is an action that updates the state to the result of +;; applying @f@ to the current state. +;; +;; * @'modify' f = 'get' >>= ('put' . f)@ +(defn modify : (∀ [m s] (Monad m) => {{s -> s} -> (StateT s m Unit)}) + [[f] (state (λ [s] (Tuple Unit (f s))))]) + +;; Get a specific component of the state, using a projection function +;; supplied. +;; +;; * @'gets' f = 'liftM' f 'get'@ +(defn gets : (∀ [m s a] (Monad m) => {{s -> a} -> (StateT s m a)}) + [[f] (state (λ [s] (Tuple (f s) s)))]) + +#| + +instance (Functor m, MonadPlus m) => Alternative (StateT s m) where + empty = StateT $ \ _ -> mzero + {-# INLINE empty #-} + StateT m <|> StateT n = StateT $ \ s -> m s `mplus` n s + {-# INLINE (<|>) #-} + + +#if MIN_VERSION_base(4,9,0) +instance (Fail.MonadFail m) => Fail.MonadFail (StateT s m) where + fail str = StateT $ \ _ -> Fail.fail str + {-# INLINE fail #-} +#endif + +instance (MonadPlus m) => MonadPlus (StateT s m) where + mzero = StateT $ \ _ -> mzero + {-# INLINE mzero #-} + StateT m `mplus` StateT n = StateT $ \ s -> m s `mplus` n s + {-# INLINE mplus #-} + +instance (MonadFix m) => MonadFix (StateT s m) where + mfix f = StateT $ \ s -> mfix $ \ ~(a, _) -> runStateT (f a) s + {-# INLINE mfix #-} + +instance MonadTrans (StateT s) where + lift m = StateT $ \ s -> do + a <- m + return (a, s) + {-# INLINE lift #-} + +instance (MonadIO m) => MonadIO (StateT s m) where + liftIO = lift . liftIO + {-# INLINE liftIO #-} + + + +-- | A variant of 'modify' in which the computation is strict in the +-- new state. +-- +-- * @'modify'' f = 'get' >>= (('$!') 'put' . f)@ +modify' :: (Monad m) => (s -> s) -> StateT s m () +modify' f = do + s <- get + put $! f s +{-# INLINE modify' #-} + + + +-- | Uniform lifting of a @callCC@ operation to the new monad. +-- This version rolls back to the original state on entering the +-- continuation. +liftCallCC :: CallCC m (a,s) (b,s) -> CallCC (StateT s m) a b +liftCallCC callCC f = StateT $ \ s -> + callCC $ \ c -> + runStateT (f (\ a -> StateT $ \ _ -> c (a, s))) s +{-# INLINE liftCallCC #-} + +-- | In-situ lifting of a @callCC@ operation to the new monad. +-- This version uses the current state on entering the continuation. +-- It does not satisfy the uniformity property (see "Control.Monad.Signatures"). +liftCallCC' :: CallCC m (a,s) (b,s) -> CallCC (StateT s m) a b +liftCallCC' callCC f = StateT $ \ s -> + callCC $ \ c -> + runStateT (f (\ a -> StateT $ \ s' -> c (a, s'))) s +{-# INLINE liftCallCC' #-} + +-- | Lift a @catchE@ operation to the new monad. +liftCatch :: Catch e m (a,s) -> Catch e (StateT s m) a +liftCatch catchE m h = + StateT $ \ s -> runStateT m s `catchE` \ e -> runStateT (h e) s +{-# INLINE liftCatch #-} + +-- | Lift a @listen@ operation to the new monad. +liftListen :: (Monad m) => Listen w m (a,s) -> Listen w (StateT s m) a +liftListen listen m = StateT $ \ s -> do + ~((a, s'), w) <- listen (runStateT m s) + return ((a, w), s') +{-# INLINE liftListen #-} + +-- | Lift a @pass@ operation to the new monad. +liftPass :: (Monad m) => Pass w m (a,s) -> Pass w (StateT s m) a +liftPass pass m = StateT $ \ s -> pass $ do + ~((a, f), s') <- runStateT m s + return ((a, s'), f) +{-# INLINE liftPass #-} +|# \ No newline at end of file diff --git a/hackett-lib/hackett/system/random.rkt b/hackett-lib/hackett/system/random.rkt new file mode 100644 index 0000000..bc3c13f --- /dev/null +++ b/hackett-lib/hackett/system/random.rkt @@ -0,0 +1,200 @@ +#lang hackett + +(provide (class RandomGen) + (class Random) + (data StdGen)) + +;; stand in since there are no bounded integers +(def intMinBound -12345) +(def intMaxBound 12345) + +;; Minimal complete definition: 'next' and 'split'. + +(class (RandomGen G) + ;; The 'next' operation returns an 'Int' that is uniformly distributed + ;; in the range returned by 'genRange' (including both end points), + ;; and a new generator. + [next : {G -> (Tuple Integer G)}] + + ;; The 'split' operation allows one to obtain two distinct random number + ;; generators. This is very useful in functional programs (for example, when + ;; passing a random number generator down to recursive calls), but very + ;; little work has been done on statistically robust implementations of + ;; 'split' (["System.Random\#Burton", "System.Random\#Hellekalek"] + ;; are the only examples we know of). + [split : {G -> (Tuple G G)}] + + + ;; The 'genRange' operation yields the range of values returned by + ;; the generator. + + ;; It is required that: + ;; + ;; * If @(a,b) = 'genRange' g@, then @a < b@. + ;; + ;; * 'genRange' always returns a pair of defined 'Int's. + ;; + ;; The second condition ensures that 'genRange' cannot examine its + ;; argument, and hence the value it returns can be determined only by the + ;; instance of 'RandomGen'. That in turn allows an implementation to make + ;; a single call to 'genRange' to establish a generator's range, without + ;; being concerned that the generator returned by (say) 'next' might have + ;; a different range to the generator passed to 'next'. + ;; + ;; The default definition spans the full range of 'Int'. + [genRange : {G -> (Tuple Integer Integer)} + (λ [_] (Tuple intMinBound intMaxBound))]) + + +#| +The 'StdGen' instance of 'RandomGen' has a 'genRange' of at least 30 bits. + +The result of repeatedly using 'next' should be at least as statistically +robust as the /Minimal Standard Random Number Generator/ described by +["System.Random\#Park", "System.Random\#Carta"]. +Until more is known about implementations of 'split', all we require is +that 'split' deliver generators that are (a) not identical and +(b) independently robust in the sense just given. + +The 'Show' and 'Read' instances of 'StdGen' provide a primitive way to save the +state of a random number generator. +It is required that @'read' ('show' g) == g@. + +In addition, 'reads' may be used to map an arbitrary string (not necessarily one +produced by 'show') onto a value of type 'StdGen'. In general, the 'Read' +instance of 'StdGen' has the following properties: + +* It guarantees to succeed on any string. + +* It guarantees to consume only a finite portion of the string. + +* Different argument strings are likely to result in different results. + +|# + +(data StdGen + (StdGen Integer Integer)) + +(def stdRange : (Tuple Integer Integer) + (Tuple 1 2147483562)) + +(defn stdNext : {StdGen -> (Tuple Integer StdGen)} + [[(StdGen s1 s2)] + (letrec ([zp (if {z < 1} + {z + 2147483562} + z)] + [z {s1pp - s2pp}] + [k (quotient! s1 53668)] + [s1p {40014 * {s1 - {k * 53668}} - {k * 12211}}] + [s1pp (if {s1p < 0} + {s1p + 2147483563} + s1p)] + [kp (quotient! s2 52774)] + [s2p {40692 * {s2 - {kp * 52774}} - {kp * 3791}}] + [s2pp (if {s2p < 0} + {s2p + 2147483399} + s2p)]) + (Tuple zp (StdGen s1pp s2pp)))]) + +(defn stdSplit : {StdGen -> (Tuple StdGen StdGen)} + [[(StdGen s1 s2)] ;; @ pattern used + (let ([std (StdGen s1 s2)]) + (case (snd (next std)) + [(StdGen t1 t2) + ;; no statistical foundation for this! + (letrec ([left (StdGen new_s1 t2)] + [right (StdGen t1 new_s2)] + [new_s1 (if {s1 == 2147483562} + 1 + {s1 + 1})] + [new_s2 (if {s2 == 1} + 2147483398 + {s2 - 1})]) + (Tuple left right))]))]) + +(instance (RandomGen StdGen) + [next stdNext] + #;[genRange (λ [_] stdRange)] + [split stdSplit]) + +(instance (Show StdGen) + [show (λ* [[(StdGen s1 s2)] {(show s1) ++ " " ++ (show s2)}])]) + +;; With a source of random number supply in hand, the 'Random' class allows the +;; programmer to extract random values of a variety of types. +;; +;; Minimal complete definition: 'randomR' and 'random'. + +(class (Random A) + ;; Takes a range /(lo,hi)/ and a random number generator + ;; /g/, and returns a random value uniformly distributed in the closed + ;; interval /[lo,hi]/, together with a new generator. It is unspecified + ;; what happens if /lo>hi/. For continuous types there is no requirement + ;; that the values /lo/ and /hi/ are ever produced, but they may be, + ;; depending on the implementation and the interval. + [randomR : (∀ [G] (RandomGen G) => {(Tuple A A) -> G -> (Tuple A G)})] + ;; The same as 'randomR', but using a default range determined by the type: + ;; + ;; * For bounded types (instances of 'Bounded', such as 'Char'), + ;; the range is normally the whole type. + ;; + ;; * For fractional types, the range is normally the semi-closed interval + ;; @[0,1)@. + ;; + ;; * For 'Integer', the range is (arbitrarily) the range of 'Int'. + [random : (∀ [G] (RandomGen G) => {G -> (Tuple A G)})] + + ;; Plural variant of 'randomR', producing an infinite list of + ;; random values instead of returning a new generator. + ;; think more lib functions are needed for this default impl + #;[randomRs : (∀ [G] (RandomGen G) => {(Tuple A A) -> G -> (List A)})] + ;; randomRs ival g = build (\cons _nil -> buildRandoms cons (randomR ival) g) + + ;; Plural variant of 'random', producing an infinite list of + ;; random values instead of returning a new generator. + #;[randoms : (∀ [G] (RandomGen G) => {G -> (List a)})] + ;; randoms g = build (\cons _nil -> buildRandoms cons random g) + + ;; A variant of 'randomR' that uses the global random number generator + ;; (see "System.Random#globalrng"). + ;; randomRIO :: (a,a) -> IO a + ;; randomRIO range = getStdRandom (randomR range) + + ;; A variant of 'random' that uses the global random number generator + ;; (see "System.Random#globalrng"). + ;; randomIO :: IO a + ;; randomIO = getStdRandom random + ) + +(instance (Random Integer) + [randomR + (λ [ival g] (randomIvalInteger ival g))] + [random + (λ [g] (randomR (Tuple intMinBound intMaxBound) g))]) + +(defn randomIvalInteger : (∀ [G] (RandomGen G) => {(Tuple Integer Integer) -> G -> (Tuple Integer G)}) + [[(Tuple l h) rng] + (if {l > h} + (randomIvalInteger (Tuple h l) rng) + (case (genRange rng) + [(Tuple genlo genhi) + (letrec ([b {genhi - genlo + 1}] + ;; Probabilities of the most likely and least likely result + ;; will differ at most by a factor of (1 +- 1/q). Assuming the RandomGen + ;; is uniform, of course + + ;; On average, log q / log b more random values will be generated + ;; than the minimum + [q 1000] + [k {h - l + 1}] + [magtgt {k * q}] + [f (λ [mag v g] + (if {mag >= magtgt} + (Tuple v g) + (case (next g) + [(Tuple x gp) + (let ([vp {v * b + {x - genlo}}]) + {vp seq (f {mag * b} vp gp)})])))]) + (case (f 1 0 rng) + [(Tuple v rngp) + (Tuple {l + {v remainder! k}} rngp)]))]))]) \ No newline at end of file diff --git a/hackett-lib/hackett/test/quickcheck.rkt b/hackett-lib/hackett/test/quickcheck.rkt new file mode 100644 index 0000000..657af31 --- /dev/null +++ b/hackett-lib/hackett/test/quickcheck.rkt @@ -0,0 +1,326 @@ +#lang hackett + +;; minimal quickcheck implementation following Claessen, Hughes ICFP'00 +;; http://www.eecs.northwestern.edu/~robby/courses/395-495-2009-fall/quick.pdf + +(require hackett/system/random) + +(provide (for-type Gen) + (class Arbitrary) + (class Coarbitrary) + (class Testable) + choose + variant + promote + sized + elements + vector + oneof + frequency + (for-type Result) + ok + stamp + arguments + nothing + result + (data Property) + evaluate + forAll + ==> + label + classify + collect + quickCheck + generate) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Utilties +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(defn !! : (∀ [A] {(List A) -> Integer -> A}) + [[{x :: xs} n] + (if {n == 0} + x + {xs !! {n - 1}})] + [[_ _] (error! "!! index out of range")]) + +(defn length : (∀ [A] {(List A) -> Integer}) + [[Nil] 0] + [[{_ :: xs}] {1 + (length xs)}]) + +(defn repeat : (∀ [A] {Integer -> A -> (List A)}) + [[n x] + (if {n == 0} + Nil + {x :: (repeat {n - 1} x)})]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Implementation +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(data (Gen A) + (Gen {Integer -> StdGen -> A})) + +(defn choose : (∀ [A] (Random A) => {(Tuple A A) -> (Gen A)}) + [[bounds] (Gen (λ [n r] (fst (randomR bounds r))))]) + +(defn variant : (∀ [A] {Integer -> (Gen A) -> (Gen A)}) + [[v (Gen m)] + (letrec ([rands (λ [r0] + (case (split r0) + [(Tuple r1 r2) + {r1 :: (rands r2)}]))]) + (Gen (λ [n r] + (m n {(rands r) !! {v + 1}}))))]) + +(defn promote : (∀ [A B] {{A -> (Gen B)} -> (Gen {A -> B})}) + [[f] (Gen (λ [n r] + (λ [a] + (case (f a) + [(Gen m) (m n r)]))))]) + +(defn sized : (∀ [A] {{Integer -> (Gen A)} -> (Gen A)}) + [[fgen] (Gen (λ [n r] + (case (fgen n) + [(Gen m) (m n r)])))]) + +(defn gen-bind : (∀ [A B] {(Gen A) -> {A -> (Gen B)} -> (Gen B)}) + [[(Gen m1) k] + (Gen (λ [n r0] + (case (split r0) + [(Tuple r1 r2) + (case (k (m1 n r1)) + [(Gen m2) + (m2 n r2)])])))]) + +(instance (Functor Gen) + [map + (λ [f x] + (do [xp <- x] + (pure (f xp))))]) + +(instance (Applicative Gen) + [pure (λ [a] (Gen (λ [n r] a)))] + [<*> + (λ [f x] + (do [fp <- f] + [xp <- x] + (pure (fp xp))))]) + +(instance (Monad Gen) + [=<< (flip gen-bind)]) + +(defn elements : (∀ [A] {(List A) -> (Gen A)}) + [[xs] + (map (!! xs) (choose (Tuple 0 {(length xs) - 1})))]) + +;; Arbitrary ; Coarbitrary + +(class (Arbitrary A) + [arbitrary : (Gen A)] + [shrink : {A -> A} + id]) + +(class (Coarbitrary A) + [coarbitrary : (∀ [B] {A -> (Gen B) -> (Gen B)})]) + +(instance (Arbitrary Bool) + [arbitrary (elements {True :: False :: Nil})]) + +(instance (Arbitrary Integer) + [arbitrary (sized (λ [n] (choose (Tuple {0 - n} n))))] + [shrink (λ [x] (quotient! x 2))]) + +(instance (∀ [A B] (Arbitrary A) (Arbitrary B) => (Arbitrary (Tuple A B))) + [arbitrary (do [a <- arbitrary] + [b <- arbitrary] + (pure (Tuple a b)))] + [shrink (λ* [[(Tuple a b)] (Tuple (shrink a) (shrink b))])]) + +(instance (∀ [A] (Arbitrary A) => (Arbitrary (List A))) + [arbitrary (sized (λ [n] {(choose (Tuple 0 n)) >>= vector}))] + [shrink + (λ [xs] (map shrink (take (quotient! (length xs) 2) xs)))]) + +(instance (∀ [A B] (Coarbitrary A) (Arbitrary B) => (Arbitrary {A -> B})) + [arbitrary (promote (λ [x] (coarbitrary x arbitrary)))]) + +(instance (Coarbitrary Bool) + [coarbitrary (λ [b] (variant (if b 0 1)))]) + +(instance (Coarbitrary Integer) + [coarbitrary + (λ [n] (if {n == 0} + (variant 0) + (if {n < 0} + {(variant 2) . (coarbitrary (- n))} + {(variant 1) . (coarbitrary (quotient! n 2))})))]) + +(instance (∀ [A B] (Coarbitrary A) (Coarbitrary B) => (Coarbitrary (Tuple A B))) + [coarbitrary + (λ* [[(Tuple a b)] + {(coarbitrary a) . (coarbitrary b)}])]) + +(instance (∀ [A B] (Coarbitrary A) => (Coarbitrary (List A))) + [coarbitrary + (λ* [[Nil] (variant 0)] + [[{a :: as}] {(variant 1) . (coarbitrary a) . (coarbitrary as)}])]) + +(instance (∀ [A B] (Arbitrary A) (Coarbitrary B) => (Coarbitrary {A -> B})) + [coarbitrary + (λ [f gen] + {arbitrary >>= {(λ [x] (coarbitrary x gen)) . f}})]) + +;; back to regular programming + +(defn vector : (∀ [A] (Arbitrary A) => {Integer -> (Gen (List A))}) + [[n] + (sequence (map (const arbitrary) (repeat n 1)))]) + +(defn oneof : (∀ [A] {(List (Gen A)) -> (Gen A)}) + [[gens] {(elements gens) >>= id}]) + +(defn frequency : (∀ [A] {(List (Tuple Integer (Gen A))) -> (Gen A)}) + [[xs] + (letrec ([pick + (λ* [[n {(Tuple k x) :: xs}] + (if {n <= k} + x + (pick {n - k} xs))] + [[_ _] undefined!])]) + (do [idx <- (choose (Tuple 1 (sum (map fst xs))))] + (pick idx xs)))]) + +;; Property + +(data Result + (Result (Maybe Bool) (List String) (List String))) + +(defn ok : {Result -> (Maybe Bool)} + [[(Result m _ _)] m]) + +(defn stamp : {Result -> (List String)} + [[(Result _ s _)] s]) + +(defn arguments : {Result -> (List String)} + [[(Result _ _ as)] as]) + +(data Property + (Prop (Gen Result))) + +(def nothing : Result + (Result Nothing Nil Nil)) + +(defn result : {Result -> Property} + [[res] (Prop (pure res))]) + +(class (Testable A) + [property : {A -> Property}]) + +(instance (Testable Bool) + [property + (λ [b] (result (Result (Just b) Nil Nil)))]) + +(instance (Testable Property) + [property + (λ [prop] prop)]) + +(instance (∀ [A B] (Arbitrary A) (Show A) (Testable B) => (Testable {A -> B})) + [property (λ [f] (forAll arbitrary f))]) + +(defn evaluate : (∀ [A] (Testable A) => {A -> (Gen Result)}) + [[a] (case (property a) + [(Prop gen) gen])]) + +(defn forAll : (∀ [A B] (Show A) (Testable B) => {(Gen A) -> {A -> B} -> Property}) + [[gen body] + (letrec ([arg + (λ [a res] (Result (ok res) (stamp res) {(show a) :: (arguments res)}))]) + (Prop (do [a <- gen] + [res <- (evaluate (body a))] + (pure (arg a res)))))]) + +(defn ==> : (∀ [A] (Testable A) => {Bool -> A -> Property}) + [[True a] (property a)] + [[False a] (result nothing)]) + +(defn label : (∀ [A] (Testable A) => {String -> A -> Property}) + [[s a] + (let ([add + (λ [res] (Result (ok res) {s :: (stamp res)} (arguments res)))]) + (Prop (map add (evaluate a))))]) + +(defn classify : (∀ [A] (Testable A) => {Bool -> String -> A -> Property}) + [[True name] (label name)] + ;; this didn't typecheck without the eta expansion + [[False _] (λ [a] (property a))]) + +(defn collect : (∀ [A B] (Show A) (Testable B) => {A -> B -> Property}) + [[v] (label (show v))]) + +(defn quickCheck : (∀ [A] (Testable A) => {A -> (IO Unit)}) + [[a] + (case (property a) + [(Prop g) + (let ([results (generate 20 g)]) + (reportResults results))])]) + +(defn generate : (∀ [A] {Integer -> (Gen A) -> (List A)}) + [[n (Gen g)] + (let ([sg (StdGen -1234 1234)] + [size 10]) + (letrec ([go + (λ [sg n] + (if {n == 0} + Nil + (case (split sg) + [(Tuple sg1 sg2) + {(g size sg1) :: (go sg2 {n - 1})}])))]) + (go sg n)))]) + +(defn reportResults : {(List Result) -> (IO Unit)} + [[Nil] (println "All tests passed!")] + [[{(Result Nothing _ _) :: rs}] + (reportResults rs)] + [[{(Result (Just True) _ _) :: rs}] + (reportResults rs)] + [[{(Result (Just False) s a) :: _}] + (println {"Test Failed: " ++ (show s) ++ " " ++ (show a)})]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Tests +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(def prop_RevUnit : {Integer -> Bool} + (λ [x] {(reverse {x :: Nil}) == {x :: Nil}})) + +(defn prop_RevApp : {(List Integer) -> (List Integer) -> Bool} + [[xs ys] + {(reverse {xs ++ ys}) == {(reverse ys) ++ (reverse xs)}}]) + +(defn prop_RevRev : {(List Integer) -> Bool} + [[xs] {(reverse (reverse xs)) == xs}]) + +(defn prop_CompAssoc : {{Integer -> Integer} -> + {Integer -> Integer} -> + {Integer -> Integer} -> + Integer -> Bool} + [[f g h x] + {({f . {g . h}} x) == ({{f . g} . h} x)}]) + +(defn max : {Integer -> Integer -> Integer} + [[x y] (if {x > y} + x + y)]) + +(defn prop_MaxLe : {Integer -> Integer -> Property} + [[x y] {{x <= y} ==> {(max x y) == y}}]) + +(instance (Show {Integer -> Integer}) + [show (const " Integer>")]) + +(main (do (quickCheck prop_RevUnit) + (quickCheck prop_RevApp) + (quickCheck prop_RevRev) + (quickCheck prop_CompAssoc) + (quickCheck prop_MaxLe))) \ No newline at end of file diff --git a/hackett-test/tests/hackett/data/set-tests.rkt b/hackett-test/tests/hackett/data/set-tests.rkt new file mode 100644 index 0000000..2fc7d44 --- /dev/null +++ b/hackett-test/tests/hackett/data/set-tests.rkt @@ -0,0 +1,649 @@ +#lang hackett + +(require hackett/data/set) +(require hackett/data/ord) +(require hackett/data/identity) +(require hackett/test/quickcheck) +(require hackett/monad/trans) +(require hackett/monad/state) + +(require hackett/private/test) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Utilities +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defn length : (∀ [A] {(List A) -> Integer}) + [[Nil] 0] + [[{_ :: xs}] {1 + (length xs)}]) + +(defn elem : (∀ [A] (Eq A) => {A -> (List A) -> Bool}) + [[_ Nil] False] + [[x {y :: ys}] (if {x == y} + True + (elem x ys))]) + +(defn notElem? : (∀ [A] (Eq A) => {A -> (List A) -> Bool}) + [[x ys] (not (elem x ys))]) + +(defn all : (∀ [A] {{A -> Bool} -> (List A) -> Bool}) + [[_ Nil] True] + [[p {x :: xs}] {(p x) && (all p xs)}]) + +(defn any : (∀ [A] {{A -> Bool} -> (List A) -> Bool}) + [[_ Nil] False] + [[p {x :: xs}] {(p x) || (any p xs)}]) + +(defn fromUpToBy : {Integer -> Integer -> Integer -> (List Integer)} + [[base ceil step] + (if {base > ceil} + Nil + {base :: (fromUpToBy {base + step} ceil step)})]) + +(defn fromDownToBy : {Integer -> Integer -> Integer -> (List Integer)} + [[base floor step] + (if {base < floor} + Nil + {base :: (fromDownToBy {base - step} floor step)})]) + +(defn sort : (∀ [A] (Ord A) => {(List A) -> (List A)}) + [[Nil] Nil] + [[{x :: xs}] + (let ([before (filter (λ [y] (le? y x)) xs)] + [after (filter (λ [y] (gt? y x)) xs)]) + {(sort before) ++ {x :: (sort after)}})]) + +(def nub : (∀ [A] (Eq A) => {(List A) -> (List A)}) + (letrec ([insertUnique + (λ* [[x Nil] {x :: Nil}] + [[x {y :: ys}] + (if {x == y} + {y :: ys} + {y :: (insertUnique x ys)})])] + [nubp + (λ* [[Nil xs] xs] + [[{x :: xs} ys] + (nubp xs (insertUnique x ys))])]) + (λ [xs] (nubp xs Nil)))) + +(defn set-all : (∀ [a] {{a -> Bool} -> (Set a) -> Bool}) + [[p s] (set-foldr (λ [x acc] {acc && (p x)}) True s)]) + +(defn last! : (∀ [a] {(List a) -> a}) + [[{x :: Nil}] x] + [[{x :: xs}] (last! xs)] + [[Nil] (error! "last! given empty list")]) + +;; The 'group' function takes a list and returns a list of lists such +;; that the concatenation of the result is equal to the argument. Moreover, +;; each sublist in the result contains only equal elements. For example, +;; +;; > group "Mississippi" = ["M","i","ss","i","ss","i","pp","i"] +;; +;; It is a special case of 'groupBy', which allows the programmer to supply +;; their own equality test. +(def group : (∀ [A] (Eq A) => {(List A) -> (List (List A))}) + (groupBy ==)) + + +;; The 'groupBy' function is the non-overloaded version of 'group'. +(defn groupBy : (∀ [a] {{a -> a -> Bool} -> (List a) -> (List (List a))}) + [[_ Nil] Nil] + [[p {x :: xs}] + (case (span (p x) xs) + [(Tuple ys zs) + {{x :: ys} :: (groupBy p zs)}])]) + +;; 'span', applied to a predicate @p@ and a list @xs@, returns a tuple where +;; first element is longest prefix (possibly empty) of @xs@ of elements that +;; satisfy @p@ and second element is the remainder of the list: +;; +;; > span (< 3) [1,2,3,4,1,2,3,4] == ([1,2],[3,4,1,2,3,4]) +;; > span (< 9) [1,2,3] == ([1,2,3],[]) +;; > span (< 0) [1,2,3] == ([],[1,2,3]) +;; +;; 'span' @p xs@ is equivalent to @('takeWhile' p xs, 'dropWhile' p xs)@ +(defn span : (∀ [a] {{a -> Bool} -> (List a) -> (Tuple (List a) (List a))}) + [[_ Nil] (Tuple Nil Nil)] + [[p {x :: xsp}] ;; @ pattern used + (if (p x) + (case (span p xsp) + [(Tuple ys zs) (Tuple {x :: ys} zs)]) + (Tuple Nil {x :: xsp}))]) + +;; The 'deleteBy' function behaves like 'delete', but takes a +;; user-supplied equality predicate. +;; +;; >>> deleteBy (<=) 4 [1..10] +;; [1,2,3,5,6,7,8,9,10] +(defn List.deleteBy : (∀ [a] {{a -> a -> Bool} -> a -> (List a) -> (List a)}) + [[_ _ Nil] Nil] + [[p x {y :: ys}] + (if (p x y) + ys + {y :: (List.deleteBy p x ys)})]) + +;; 'delete' @x@ removes the first occurrence of @x@ from its list argument. +;; For example, +;; +;; >>> delete 'a' "banana" +;; "bnana" +;; +;; It is a special case of 'deleteBy', which allows the programmer to +;; supply their own equality test. +(def List.delete : (∀ [a] (Eq a) => {a -> (List a) -> (List a)}) + (List.deleteBy ==)) + +;; The '\\' function is list difference (non-associative). +;; In the result of @xs@ '\\' @ys@, the first occurrence of each element of +;; @ys@ in turn (if any) has been removed from @xs@. Thus +;; +;; > (xs ++ ys) \\ xs == ys. +;; +;; >>> "Hello World!" \\ "ell W" +;; "Hoorld!" +;; +;; It is a special case of 'deleteFirstsBy', which allows the programmer +;; to supply their own equality test. +(def \\ : (∀ [a] (Eq a) => {(List a) -> (List a) -> (List a)}) + (foldl (flip List.delete))) + +;; The 'intersectBy' function is the non-overloaded version of 'intersect'. +(defn List.intersectBy : (∀ [a] {{a -> a -> Bool} -> (List a) -> (List a) -> (List a)}) + [[_ Nil _] Nil] + [[_ _ Nil] Nil] + [[p xs ys] + (filter (λ [x] (any (p x) ys)) xs)]) + +;; | The 'intersect' function takes the list intersection of two lists. +;; For example, +;; +;; >>> [1,2,3,4] `intersect` [2,4,6,8] +;; [2,4] +;; +;; If the first list contains duplicates, so will the result. +;; +;; >>> [1,2,2,3,4] `intersect` [6,4,4,2] +;; [2,2,4] +;; +;; It is a special case of 'intersectBy', which allows the programmer to +;; supply their own equality test. If the element is found in both the first +;; and the second list, the element from the first list will be used. +(def List.intersect : (∀ [a] (Eq a) => {(List a) -> (List a) -> (List a)}) + (List.intersectBy ==)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; A type with a peculiar Eq instance designed to make sure keys +;; come from where they're supposed to. + +(data (OddEq A) + (OddEq A Bool)) + +(instance (∀ [A] (Show A) => (Show (OddEq A))) + [show (λ* [[(OddEq a b)] {"OddEq " ++ (show a) ++ " " ++ (show b)}])]) + +(defn getOddEq : (∀ [A] {(OddEq A) -> (Tuple A Bool)}) + [[(OddEq a b)] (Tuple a b)]) + +(instance (∀ [A] (Arbitrary A) => (Arbitrary (OddEq A))) + [arbitrary {OddEq <$> arbitrary <*> arbitrary}]) + +(instance (∀ [A] (Eq A) => (Eq (OddEq A))) + [== (λ* [[(OddEq x _) (OddEq y _)] {x == y}])]) + +(instance (∀ [A] (Ord A) => (Ord (OddEq A))) + [compare (λ* [[(OddEq x _) (OddEq y _)] (compare x y)])]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Unit tests +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; test_lookupLT +(test {(lookupLT 3 (fromList {3 :: 5 :: Nil})) ==! Nothing}) +(test {(lookupLT 5 (fromList {3 :: 5 :: Nil})) ==! (Just 3)}) + +;; test_lookupGT +(test {(lookupGT 4 (fromList {3 :: 5 :: Nil})) ==! (Just 5)}) +(test {(lookupGT 5 (fromList {3 :: 5 :: Nil})) ==! Nothing}) + +;; test_lookupLE +(test {(lookupLE 2 (fromList {3 :: 5 :: Nil})) ==! Nothing}) +(test {(lookupLE 4 (fromList {3 :: 5 :: Nil})) ==! (Just 3)}) +(test {(lookupLE 5 (fromList {3 :: 5 :: Nil})) ==! (Just 5)}) + +;; test_lookupGE +(test {(lookupGE 3 (fromList {3 :: 5 :: Nil})) ==! (Just 3)}) +(test {(lookupGE 4 (fromList {3 :: 5 :: Nil})) ==! (Just 5)}) +(test {(lookupGE 6 (fromList {3 :: 5 :: Nil})) ==! Nothing}) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Indexed +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defn isJust + [[(Just _)] True] + [[Nothing] False]) + +(defn fromJust + [[(Just x)] x] + [[_] (error! "fromJust")]) + +;; test_lookupIndex +(test {(isJust (lookupIndex 2 (fromList {5 :: 3 :: Nil}))) ==! False}) +(test {(fromJust (lookupIndex 3 (fromList {5 :: 3 :: Nil}))) ==! 0}) +(test {(fromJust (lookupIndex 5 (fromList {5 :: 3 :: Nil}))) ==! 1}) +(test {(isJust (lookupIndex 6 (fromList {5 :: 3 :: Nil}))) ==! False}) + +;; test_findIndex +(test {(findIndex 3 (fromList {5 :: 3 :: Nil})) ==! 0}) +(test {(findIndex 5 (fromList {5 :: 3 :: Nil})) ==! 1}) + +;; test_elemAt +(test {(elemAt 0 (fromList {5 :: 3 :: Nil})) ==! 3}) +(test {(elemAt 1 (fromList {5 :: 3 :: Nil})) ==! 5}) + +;; test_deleteAt +(test {(deleteAt 0 (fromList {5 :: 3 :: Nil})) ==! (singleton 5)}) +(test {(deleteAt 1 (fromList {5 :: 3 :: Nil})) ==! (singleton 3)}) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Arbitrary, reasonably balanced trees +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; The IsInt class lets us constrain a type variable to be Int in an entirely +;; standard way. The constraint @ IsInt a @ is essentially equivalent to the +;; GHC-only constraint @ a ~ Int @, but @ IsInt @ requires manual intervention +;; to use. If ~ is ever standardized, we should certainly use it instead. +;; Earlier versions used an Enum constraint, but this is confusing because +;; not all Enum instances will work properly for the Arbitrary instance here. + +(class (Show A) (Arbitrary A) => (IsInt A) + [fromIntF : (∀ [F] {(F Integer) -> (F A)})]) + +(instance (IsInt Integer) + [fromIntF id]) + +(def fromInt : (∀ [A] (IsInt A) => {Integer -> A}) + {run-identity . fromIntF . Identity}) + +(data (F G A B) + (F {(G B) -> A})) +(defn unf + [[(F f)] f]) + +(def toIntF : (∀ [G A] (IsInt A) => {(G A) -> (G Integer)}) + {unf . fromIntF . F $ id}) + + +;; How much the minimum value of an arbitrary set should vary +(def positionFactor : Integer + 1) + +;; How much the gap between consecutive elements in an arbitrary +;; set should vary +(def gapRange : Integer + 5) + +(instance (∀ [A] (IsInt A) => (Arbitrary (Set A))) + [arbitrary + (let ([step (do [i <- get] + [diff <- (lift (choose (Tuple 1 gapRange)))] + (let [ip {i + diff}]) + (put ip) + (pure ip))]) + (sized (λ [sz0] + (do [sz <- (choose (Tuple 0 sz0))] + [middle <- (choose (Tuple {(- 0 positionFactor) * {sz + 1}} {positionFactor * {sz + 1}}))] + [t <- (let ([shift {{sz * gapRange + 1} quotient! 2}] + [start {middle - shift}]) + (evalStateT (mkArb step sz) start))] + (if (valid t) + (pure (fromIntF t)) + (error! "Test generated invalid tree!"))))))] + [shrink + {fromIntF . fromList . toIntF . shrink . toList}]) + +(class (Monad m) => (MonadGen m) + [liftGen : (∀ [a] {(Gen a) -> (m a)})]) + +(instance (MonadGen Gen) + [liftGen id]) + +(instance (∀ [m s] (MonadGen m) => (MonadGen (StateT s m))) + [liftGen {lift . liftGen}]) + +;; Given an action that produces successively larger elements and +;; a size, produce a set of arbitrary shape with exactly that size. +(defn mkArb : (∀ [m a] (MonadGen m) => {(m a) -> Integer -> (m (Set a))}) + [[step n] + (if {n <= 0} + (pure Tip) + (if {n == 1} + {singleton <$> step} + (if {n == 2} + (do [dir <- (liftGen arbitrary)] + [p <- step] + [q <- step] + (if dir + (pure (Bin 2 q (singleton p) Tip)) + (pure (Bin 2 p Tip (singleton q))))) + (let ([upper {{3 * {n - 1}} quotient! 4}] + ;; this assumes a balnce factor of delta = 3 + [lower {{n + 2} quotient! 4}]) + (do [ln <- (liftGen (choose (Tuple lower upper)))] + (let [rn {n - ln - 1}]) + {(λ [l x r] (Bin n x l r)) + <$> (mkArb step ln) + <*> step + <*> (mkArb step rn)})))))]) + +;; Given a strictly increasing list of elements, produce an arbitrarily +;; shaped set with exactly those elements. +(defn setFromList : (∀ [A] {(List A) -> (Gen (Set A))}) + [[xs] + (let ([step (do [xxs <- get] + (case xxs + [{x :: xs} + (do (put xs) + (pure x))] + [_ (error! "setFromList case not covered")]))]) + (evalStateT (mkArb step (length xs)) xs))]) + +(data TwoSets + (TwoSets (Set Integer) (Set Integer))) + +(instance (Show TwoSets) + [show (λ* [[(TwoSets t1 t2)] + {"TwoSets " ++ (show t1) ++ " " ++ (show t2)}])]) + +(data (TwoLists A) + (TwoLists (List A) (List A))) + +(instance (Functor TwoLists) + [map (λ* [[f (TwoLists l1 l2)] + (TwoLists (map f l1) (map f l2))])]) + +(data Options2 + One2 + Two2 + Both2) ;; deriving (Bounded, Enum) + +(instance (Arbitrary Options2) + [arbitrary (elements {One2 :: Two2 :: Both2 :: Nil})]) + +;; We produce two lists from a simple "universe". This instance +;; is intended to give good results when the two lists are then +;; combined with each other; if other elements are used with them, +;; they may or may not behave particularly well. +(instance (∀ [A] (IsInt A) => (Arbitrary (TwoLists A))) + [arbitrary (sized (λ [sz0] (do [sz <- (choose (Tuple 0 sz0))] + (let [universe (fromUpToBy 0 {3 * {sz - 1}} 3)]) + (divide2Gen (fromIntF universe)))))]) + +(instance (Arbitrary TwoSets) + [arbitrary (do [tl <- arbitrary] + (case tl + [(TwoLists l r) + {TwoSets <$> (setFromList l) <*> (setFromList r)}]))]) + +(defn divide2Gen : (∀ [A] {(List A) -> (Gen (TwoLists A))}) + [[Nil] (pure (TwoLists Nil Nil))] + [[{x :: xs}] + (do [way <- arbitrary] + [tl <- (divide2Gen xs)] + (case tl + [(TwoLists ls rs) + (case way + [One2 (pure (TwoLists {x :: ls} rs))] + [Two2 (pure (TwoLists ls {x :: rs}))] + [Both2 (pure (TwoLists {x :: ls} {x :: rs}))])]))]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Valid trees +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defn forValid : (∀ [A B] (IsInt A) (Testable B) => {{(Set A) -> B} -> Property}) + [[f] + (forAll arbitrary + (λ [t] + (classify {(size t) == 0} "empty" + (classify {{(size t) > 0} && {(size t) <= 10}} "small" + (classify {{(size t) > 10} && {(size t) <= 64}} "medium" + (classify {(size t) > 64} "large" + (f t)))))))]) + +(defn forValidUnitTree : (∀ [A] (Testable A) => {{(Set Integer) -> A} -> Property}) + [[f] (forValid f)]) + +(def prop_Valid : Property + (forValidUnitTree valid)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Single, Member, Insert, Delete +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defn prop_Single : {Integer -> Bool} + [[x] {(insert x empty) == (singleton x)}]) + +(defn prop_Member : {(List Integer) -> Integer -> Bool} + [[xs n] + (let ([m (fromList xs)]) + (all (λ [k] {(member k m) == (elem k xs)}) {n :: xs}))]) + +(defn prop_NotMember : {(List Integer) -> Integer -> Bool} + [[xs n] + (let ([m (fromList xs)]) + (all (λ [k] {(not-member k m) == (notElem? k xs)}) {n :: xs}))]) + +(defn test_LookupSomething : {{Integer -> (Set Integer) -> (Maybe Integer)} + -> {Integer -> Integer -> Bool} + -> (List Integer) + -> Bool} + [[lookupp cmp xs] + (letrec ([filter_odd + (λ* [[Nil] Nil] + [[{_ :: Nil}] Nil] + [[{_ :: o :: xs}] {o :: (filter_odd xs)}])]) + (let ([odd_sorted_xs (filter_odd (nub (sort xs)))] + [t (fromList odd_sorted_xs)] + [test : {Integer -> Bool} + (λ [x] (case (filter (λ [y] (cmp y x)) odd_sorted_xs) + [Nil {(lookupp x t) == Nothing}] + [cs + (if (cmp 0 1) + {(lookupp x t) == (Just (last! cs))} ;; we want largest such element + {(lookupp x t) == (Just (head! cs))})]))]) ;; we want smallest such element + (all test xs)))]) + +(def prop_LookupLT : {(List Integer) -> Bool} + (test_LookupSomething lookupLT <)) + +(def prop_LookupGT : {(List Integer) -> Bool} + (test_LookupSomething lookupGT >)) + +(def prop_LookupLE : {(List Integer) -> Bool} + (test_LookupSomething lookupLE <=)) + +(def prop_LookupGE : {(List Integer) -> Bool} + (test_LookupSomething lookupGE >=)) + +(defn prop_InsertValid : {Integer -> Property} + [[k] (forValidUnitTree (λ [t] (valid (insert k t))))]) + +(defn prop_InsertDelete : {Integer -> (Set Integer) -> Property} + [[k t] {(not (member k t)) ==> {(delete k (insert k t)) == t}}]) + +(defn prop_InsertBiased : {Integer -> (Set Integer) -> Bool} + [[k t] + (let ([tp (mapMonotonic (λ [x] (OddEq x False)) t)] + [ktp (insert (OddEq k True) tp)] + [kt (mapMonotonic getOddEq ktp)]) + (member (Tuple k True) kt))]) + +(defn prop_DeleteValid : {Integer -> Property} + [[k] (forValidUnitTree (λ [t] (valid (delete k (insert k t)))))]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Balance +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defn prop_Link : {Integer -> Property} + [[x] + (forValidUnitTree (λ [t] + (case (split x t) + [(Tuple l r) (valid (link x l r))])))]) + +(defn prop_Merge : {Integer -> Property} + [[x] + (forValidUnitTree (λ [t] + (case (split x t) + [(Tuple l r) (valid (merge l r))])))]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Union +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(def prop_UnionValid : Property + (forValidUnitTree + (λ [t1] + (forValidUnitTree + (λ [t2] + (valid (union t1 t2))))))) + +(defn prop_UnionInsert : {Integer -> (Set Integer) -> Bool} + [[x t] {(union t (singleton x)) == (insert x t)}]) + +(defn prop_UnionAssoc : {(Set Integer) -> (Set Integer) -> (Set Integer) -> Bool} + [[t1 t2 t3] {(union t1 (union t2 t3)) == (union (union t1 t2) t3)}]) + +(defn prop_UnionComm : {TwoSets -> Bool} + [[(TwoSets t1 t2)] {(union t1 t2) == (union t2 t1)}]) + +(defn prop_UnionBiased : {TwoSets -> Bool} + [[(TwoSets l r)] + (let ([lp (mapMonotonic (λ [x] (OddEq x False)) l)] + [rp (mapMonotonic (λ [x] (OddEq x True)) l)]) + {(union lp rp) == (union lp (difference rp lp))})]) + +(defn prop_IntBiased : {TwoSets -> Bool} + [[(TwoSets l r)] + (let ([lp (mapMonotonic (λ [x] (OddEq x False)) l)] + [rp (mapMonotonic (λ [x] (OddEq x True)) l)] + [lprp (intersection lp rp)]) + (set-all (λ* [[(OddEq _ b)] (not b)]) lprp))]) + +(def prop_DiffValid : Property + (forValidUnitTree(λ [t1] (forValidUnitTree (λ [t2] (valid (difference t1 t2))))))) + +(defn prop_Diff : {(List Integer) -> (List Integer) -> Bool} + [[xs ys] + {(toAscList (difference (fromList xs) (fromList ys))) + == (sort (\\ (nub xs) (nub ys)))}]) + +(def prop_IntValid : Property + (forValidUnitTree (λ [t1] (forValidUnitTree (λ [t2] (valid (intersection t1 t2))))))) + +(defn prop_Int : {(List Integer) -> (List Integer) -> Bool} + [[xs ys] + {(toAscList (intersection (fromList xs) (fromList ys))) + == (sort (nub (List.intersect xs ys)))}]) + +(defn prop_disjoint : {(Set Integer) -> (Set Integer) -> Bool} + [[a b] {(disjoint a b) == (null (intersection a b))}]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Lists +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(def prop_Ordered : Property + (forAll (choose (Tuple 5 100)) + (λ [n] (let ([xs (fromUpToBy 0 n 1)]) + ;; the haskell source uses `===` but I don't know what that is + {(fromAscList xs) == (fromList xs)})))) + +(def prop_DescendingOrdered : Property + (forAll (choose (Tuple 5 100)) + (λ [n] (let ([xs (fromDownToBy n 0 1)]) + ;; the haskell source uses `===` but I don't know what that is + {(fromDescList xs) == (fromList xs)})))) + +(defn prop_List : {(List Integer) -> Bool} + [[xs] {(sort (nub xs)) == (toList (fromList xs))}]) + +(defn prop_DescList : {(List Integer) -> Bool} + [[xs] {(reverse (sort (nub xs))) == (toDescList (fromList xs))}]) + +(defn prop_AscDescList : {(List Integer) -> Bool} + [[xs] (let ([s (fromList xs)]) + {(toAscList s) == (reverse (toDescList s))})]) + +(defn prop_fromList : {(List Integer) -> Bool} + [[xs] + (let ([t (fromList xs)] + [sort_xs (sort xs)] + [nub_sort_xs (map head! (group sort_xs))]) + {{t == (fromAscList sort_xs)} + && {t == (fromDistinctAscList nub_sort_xs)} + && {t == (foldr insert empty xs)}})]) + +(defn prop_fromListDesc : {(List Integer) -> Bool} + [[xs] + (let ([t (fromList xs)] + [sort_xs (reverse (sort xs))] + [nub_sort_xs (map head! (group sort_xs))]) + {{t == (fromDescList sort_xs)} + && {t == (fromDistinctDescList nub_sort_xs)} + && {t == (foldr insert empty xs)}})]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Set operations are like IntSet operations +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; ... a bunch of tests making use of IntSet which doesn't exist for us ... + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Main +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(main (do (quickCheck prop_Valid) + (quickCheck prop_Single) + (quickCheck prop_Member) + (quickCheck prop_NotMember) + (quickCheck prop_InsertValid) + (quickCheck prop_InsertDelete) + ;; prop_InsertBiased is failing + (quickCheck prop_InsertBiased) + (quickCheck prop_DeleteValid) + (quickCheck prop_Link) + (quickCheck prop_Merge) + (quickCheck prop_UnionValid) + (quickCheck prop_UnionInsert) + (quickCheck prop_UnionAssoc) + (quickCheck prop_DiffValid) + (quickCheck prop_IntValid) + (quickCheck prop_disjoint) + (quickCheck prop_Ordered) + (quickCheck prop_DescendingOrdered) + (quickCheck prop_List) + (quickCheck prop_DescList) + (quickCheck prop_AscDescList) + (quickCheck prop_UnionComm) + (quickCheck prop_UnionBiased) + (quickCheck prop_IntBiased) + (quickCheck prop_LookupLT) + (quickCheck prop_LookupGT) + (quickCheck prop_LookupLE) + (quickCheck prop_LookupGE) + (quickCheck prop_fromList) + (quickCheck prop_fromListDesc) + (quickCheck prop_Diff) + (quickCheck prop_Int))) + +#| +(def k 1) + (def t (fromList {1 :: 3 :: Nil})) +(def tp (mapMonotonic (λ [x] (OddEq x False)) t)) +(def ktp (insert (OddEq k True) tp)) +(def kt (mapMonotonic getOddEq ktp)) +|# \ No newline at end of file