
  0 | module Data.Finite
  1 | 
  2 | import Data.Vect
  3 | 
  4 | %default total
  5 | 
  6 | ||| An interface for listing all values of a type with a
  7 | ||| finite number of inhabitants.
  8 | public export
  9 | interface Finite a where
 10 |   constructor MkFinite
 11 |   values : List a
 12 | 
 13 | public export %inline
 14 | valuesOf : (0 a : Type) -> Finite a => List a
 15 | valuesOf _ = values
 16 | 
 17 | public export
 18 | Finite () where values = [()]
 19 | 
 20 | public export
 21 | Finite Void where values = []
 22 | 
 23 | public export
 24 | Finite Bool where values = [False,True]
 25 | 
 26 | public export
 27 | Finite Ordering where values = [LT,EQ,GT]
 28 | 
 29 | public export
 30 | Finite a => Finite (Maybe a) where values = Nothing :: map Just values
 31 | 
 32 | public export
 33 | Finite a => Finite b => Finite (Either a b) where
 34 |   values = map Left values ++ map Right values
 35 | 
 36 | public export
 37 | Finite a => Finite b => Finite (a,b) where
 38 |   values = [| MkPair values values |]
 39 | 
 40 | public export
 41 | {n : _} -> Finite a => Finite (Vect n a) where
 42 |   values {n = 0}   = [[]]
 43 |   values {n = S k} = [| values :: values |]
 44 | 
 45 | weaken : List (Fin k) -> List (Fin $ S k)
 46 | weaken []        = []
 47 | weaken (x :: xs) = weaken x :: weaken xs
 48 | 
 49 | fins : {n : _} -> List (Fin n)
 50 | fins {n = 0}   = []
 51 | fins {n = S k} = last :: weaken (fins {n = k})
 52 | 
 53 | public export %inline
 54 | {n : _} -> Finite (Fin n) where
 55 |   values = fins
 56 |