
  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 | -- Denotationally equivalent to `Data.Fin.allFins`, but runs in linear, instead
 46 | -- of quadratic time. This is done by leveraging the runtime optimisation of
 47 | -- natural-number shaped datatypes as described here:
 48 | -- https://idris2.readthedocs.io/en/latest/reference/builtins.html
 49 | -- Similar function also appears in `Data.Array.Index.allFinsFast` in the
 50 | -- `idris2-array` library.
 51 | allFinsLinear : (n : Nat) -> List (Fin n)
 52 | allFinsLinear 0 = []
 53 | allFinsLinear (S n) = go [] last
 54 |   where
 55 |     go : List (Fin k) -> Fin k -> List (Fin k)
 56 |     go xs FZ     = FZ :: xs
 57 |     go xs (FS x) = go (FS x :: xs) (assert_smaller (FS x) $ weaken x)
 58 | 
 59 | public export %inline
 60 | {n : _} -> Finite (Fin n) where
 61 |   values = allFinsLinear n
 62 |