0 | module Data.Enum
  1 |
  2 | import Derive.Prelude
  3 | import public Data.Finite
  4 | import public Data.List.Elem
  5 | import public Data.Prim.Bits32
  6 | import public Decidable.HDecEq
  7 |
  8 | %default total
  9 | %language ElabReflection
 10 |
 11 | --------------------------------------------------------------------------------
 12 | -- Primitive Indices
 13 | --------------------------------------------------------------------------------
 14 |
 15 | public export
 16 | record Index (n : Bits32) where
 17 |   constructor I
 18 |   val : Bits32
 19 |   {auto 0 prf : val < n}
 20 |
 21 | %runElab deriveIndexed "Index" [Show,Eq,Ord]
 22 |
 23 | export
 24 | tryIndex : {r : _} -> Bits32 -> Maybe (Index r)
 25 | tryIndex n =
 26 |   case lt n r of
 27 |     Nothing0 => Nothing
 28 |     Just0 v  => Just (I n)
 29 |
 30 | public export
 31 | fromInteger : (n : Integer) -> (0 p : cast n < r) => Index r
 32 | fromInteger n = I (cast n)
 33 |
 34 | public export
 35 | Zero : (0 prf : 0 < n) => Index n
 36 | Zero = I 0
 37 |
 38 | export
 39 | 0 ltProof : (v : Bits32) -> (0 prf : v < n) => lt (cast v) (cast n) === True
 40 | ltProof v = believe_me $ Builtin.Refl {x = True}
 41 |
 42 | export %inline
 43 | toFin : Index n -> Fin (cast n)
 44 | toFin (I v) = bits32ToFin v n
 45 |
 46 | export %inline
 47 | Cast (Index n) Integer where
 48 |   cast (I v) = cast v
 49 |
 50 | export %inline
 51 | Cast (Index n) Bits32 where
 52 |   cast (I v) = v
 53 |
 54 | --------------------------------------------------------------------------------
 55 | -- Enum Interface
 56 | --------------------------------------------------------------------------------
 57 |
 58 | ||| Verified enumerations.
 59 | |||
 60 | ||| Provides a function for converting a value of the given type to an
 61 | ||| `Index n` of the given size.
 62 | |||
 63 | ||| In addition, proves that `Finite.value` holds every value there is and
 64 | ||| that `toIndex` is injective.
 65 | |||
 66 | ||| With these proofs we can use a value of type `t` as an index into a
 67 | ||| (potentially dependent) array.
 68 | public export
 69 | interface Finite t => Enum (0 t : Type) (0 n : Bits32) | t where
 70 |   constructor MkEnum
 71 |   toIndex : t -> Index n
 72 |
 73 |   0 toIndexInjective : (x,y : t) -> toIndex x === toIndex y -> x === y
 74 |
 75 |   0 valuesComplete : (x : t) -> Elem x Finite.values
 76 |
 77 | export %inline
 78 | enumToFin : Enum t n => t -> Fin (cast n)
 79 | enumToFin = toFin . toIndex
 80 |
 81 | export %inline
 82 | enumToBits32 : Enum t n => t -> Bits32
 83 | enumToBits32 = cast . toIndex
 84 |
 85 | export %inline
 86 | enumToInteger : Enum t n => t -> Integer
 87 | enumToInteger = cast . toIndex
 88 |
 89 | export
 90 | Enum Bool 2 where
 91 |   toIndex False = 0
 92 |   toIndex True  = 1
 93 |
 94 |   toIndexInjective False False Refl = Refl
 95 |   toIndexInjective True True Refl = Refl
 96 |
 97 |   valuesComplete False = Here
 98 |   valuesComplete True = There Here
 99 |
100 | export
101 | Enum Ordering 3 where
102 |   toIndex LT = 0
103 |   toIndex EQ = 1
104 |   toIndex GT = 2
105 |
106 |   toIndexInjective LT LT Refl = Refl
107 |   toIndexInjective EQ EQ Refl = Refl
108 |   toIndexInjective GT GT Refl = Refl
109 |
110 |   valuesComplete LT = Here
111 |   valuesComplete EQ = There Here
112 |   valuesComplete GT = There $ There Here
113 |
114 | --------------------------------------------------------------------------------
115 | -- Utilities
116 | --------------------------------------------------------------------------------
117 |
118 | public export
119 | inList : HDecEq i => (v : i) -> List i -> Bool
120 | inList v []        = False
121 | inList v (x :: xs) =
122 |   case hdecEq v x of
123 |     Nothing0 => inList v xs
124 |     Just0 _  => True
125 |
126 | export
127 | 0 inListImpliesElem : HDecEq i => (v : i) -> inList v is === True -> Elem v is
128 | inListImpliesElem v prf {is = []}    = absurd prf
129 | inListImpliesElem v prf {is = x::xs} with (hdecEq v x)
130 |   _ | Nothing0  = There $ inListImpliesElem v prf {is = xs}
131 |   _ | Just0 p   = rewrite p in Here
132 |