using NoStdLib
using Primitives

import list
import product

||| The size of a set, i.e. the number of (distinct) elements it contains.

!!! setSize({}) == 0
!!! setSize({1,2,3}) == 3
!!! forall s1 : Set(N), s2 : Set(N). setSize(s1 union s2) <= setSize(s1) + setSize(s2)
!!! ∀ S : Set(N). setSize S == setSize (S ∪ S)
setSize : Set(a) -> N
setSize(s) = length(list(s))

||| Cartesian product of two sets, i.e. the set of all possible ordered pairs
||| with one element from each set.

!!! setCP({1,2}, {'a','b'}) == {(1,'a'), (1,'b'), (2,'a'), (2,'b')}
!!! setCP({}, {1,2,3}) == {}
!!! ∀ A : Set(N), B : Set(N). setSize(setCP(A, B)) == setSize(A) * setSize(B)
setCP : Set(a) * Set(b) -> Set(a * b)
setCP (A,B) = unions(each(\a. each(\b. (a,b), B), A))

||| The size of a bag, i.e. the number of elements it contains (counting multiplicity).
!!! bagSize(bag([])) == 0
!!! bagSize(bag([1,2,3])) == 3
!!! bagSize(bag([1,1,2,3,3,3])) == 6
!!! bagSize(⟅1 # 1000000, 2 # 990482⟆) == 1990482
bagSize : Bag(a) -> N
bagSize(b) = foldr(\((_,n), s). n + s, 0, list(bagCounts(b)))

||| Cartesian product of two bags, i.e. the bag of all possible
||| ordered pairs with one element taken from each bag.  Note that if
||| there are multiple copies of an element, they are considered
||| distinct for the purposes of counting how many ways there are to
||| form a given pair.

!!! bagCounts(bagCP(bag [1,1,1], bag ['x'])) == {((1,'x'), 3)}
!!! bagCP(bag [1,1,2], bag "hello") == ⟅(1, 'e') # 2, (1, 'h') # 2, (1, 'l') # 4, (1, 'o') # 2, (2, 'e'), (2, 'h'), (2, 'l') # 2, (2, 'o')⟆
!!! ∀ A : List(N), B : List(N). bag(listCP(A,B)) == bagCP(bag(A), bag(B))
!!! ∀ A : List(N), B : List(N). bagSize(bagCP(bag(A), bag(B))) == bagSize(bag(A)) * bagSize(bag(B))

bagCP : Bag(a) * Bag(b) -> Bag(a * b)
bagCP (A,B) = $unsafeBagFromCounts(each(\((a,m),(b,n)). ((a,b), m*n), setCP(bagCounts(A), bagCounts(B))))

reducebag : (a × a → a) × a × Bag(a) → a
reducebag(f,z,b) = foldr(f,z,list(b))

reduceset : (a × a → a) × a × Set(a) → a
reduceset(f,z,s) = foldr(f,z,list(s))

unions : Set(Set(a)) → Set(a)
unions(ss) = foldr(~∪~, {}, list(ss))