
   0 | module Data.Prim.Bits8
   1 | 
   2 | import public Control.WellFounded
   3 | import public Data.DPair
   4 | import public Data.Prim.Ord
   5 | import public Algebra.Solver.Ring
   6 | import Syntax.PreorderReasoning
   7 | 
   8 | %default total
   9 | 
  10 | unsafeRefl : a === b
  11 | unsafeRefl = believe_me (Refl {x = a})
  12 | 
  13 | --------------------------------------------------------------------------------
  14 | --          (<)
  15 | --------------------------------------------------------------------------------
  16 | 
  17 | ||| Witness that `m < n === True`.
  18 | export
  19 | data (<) : (m,n : Bits8) -> Type where
  20 |   LT : {0 m,n : Bits8} -> (0 prf : (m < n) === True) -> m < n
  21 | 
  22 | ||| Contructor for `(<)`.
  23 | |||
  24 | ||| This can only be used in an erased context.
  25 | export %hint
  26 | 0 mkLT : (0 prf : (m < n) === True) -> m < n
  27 | mkLT = LT
  28 | 
  29 | ||| Extractor for `(<)`.
  30 | |||
  31 | ||| This can only be used in an erased context.
  32 | export
  33 | 0 runLT : m < n -> (m < n) === True
  34 | runLT (LT prf) = prf
  35 | 
  36 | ||| We don't trust values of type `(<)` too much,
  37 | ||| so we use this when creating magical results.
  38 | export
  39 | strictLT : (0 p : m < n) -> Lazy c -> c
  40 | strictLT (LT prf) x = x
  41 | 
  42 | --------------------------------------------------------------------------------
  43 | --          Aliases
  44 | --------------------------------------------------------------------------------
  45 | 
  46 | ||| Flipped version of `(<)`.
  47 | public export
  48 | 0 (>) : (m,n : Bits8) -> Type
  49 | m > n = n < m
  50 | 
  51 | ||| `m <= n` mean that either `m < n` or `m === n` holds.
  52 | public export
  53 | 0 (<=) : (m,n : Bits8) -> Type
  54 | m <= n = Either (m < n) (m === n)
  55 | 
  56 | ||| Flipped version of `(<=)`.
  57 | public export
  58 | 0 (>=) : (m,n : Bits8) -> Type
  59 | m >= n = n <= m
  60 | 
  61 | ||| `m /= n` mean that either `m < n` or `m > n` holds.
  62 | public export
  63 | 0 (/=) : (m,n : Bits8) -> Type
  64 | m /= n = Either (m < n) (m > n)
  65 | 
  66 | --------------------------------------------------------------------------------
  67 | --          Order
  68 | --------------------------------------------------------------------------------
  69 | 
  70 | 0 ltNotEQ : m < n -> Not (m === n)
  71 | ltNotEQ x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and EQ")
  72 | 
  73 | 0 ltNotGT : m < n -> Not (n < m)
  74 | ltNotGT x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and GT")
  75 | 
  76 | 0 eqNotLT : m === n -> Not (m < n)
  77 | eqNotLT = flip ltNotEQ
  78 | 
  79 | export
  80 | comp : (m,n : Bits8) -> Trichotomy (<) m n
  81 | comp m n = case prim__lt_Bits8 m n of
  82 |   0 => case prim__eq_Bits8 m n of
  83 |     0 => GT (ltNotGT $ LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (LT unsafeRefl)
  84 |     x => EQ (eqNotLT unsafeRefl) (unsafeRefl) (eqNotLT unsafeRefl)
  85 |   x => LT (LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (ltNotGT $ LT unsafeRefl)
  86 | 
  87 | export
  88 | Total Bits8 (<) where
  89 |   trichotomy   = comp
  90 |   transLT p q  = strictLT p $ strictLT q $ LT unsafeRefl
  91 | 
  92 | --------------------------------------------------------------------------------
  93 | --          Bounds and Well-Foundedness
  94 | --------------------------------------------------------------------------------
  95 | 
  96 | ||| Lower bound of `Bits8`
  97 | public export
  98 | MinBits8 : Bits8
  99 | MinBits8 = 0
 100 | 
 101 | ||| Upper bound of `Bits8`
 102 | public export
 103 | MaxBits8 : Bits8
 104 | MaxBits8 = 0xff
 105 | 
 106 | ||| `m >= 0` for all `m` of type `Bits8`.
 107 | export
 108 | 0 GTE_MinBits8 : (m : Bits8) -> m >= MinBits8
 109 | GTE_MinBits8 m = case comp MinBits8 m of
 110 |   LT x f g => %search
 111 |   EQ f x g => %search
 112 |   GT f g x => assert_total $ idris_crash "IMPOSSIBLE: Bits8 smaller than 0"
 113 | 
 114 | ||| Not value of type `Bits8` is less than zero.
 115 | export
 116 | 0 Not_LT_MinBits8 : m < 0 -> Void
 117 | Not_LT_MinBits8 = GTE_not_LT (GTE_MinBits8 m)
 118 | 
 119 | ||| `m <= MaxBits8` for all `m` of type `Bits8`.
 120 | export
 121 | 0 LTE_MaxBits8 : (m : Bits8) -> m <= MaxBits8
 122 | LTE_MaxBits8 m = case comp m MaxBits8 of
 123 |   LT x f g => %search
 124 |   EQ f x g => %search
 125 |   GT f g x =>
 126 |     assert_total $
 127 |     idris_crash "IMPOSSIBLE: Bits8 greater than \{show MaxBits8}"
 128 | 
 129 | ||| Not value of type `Bits8` is greater than `MaxBits8`.
 130 | export
 131 | 0 Not_GT_MaxBits8 : m > MaxBits8 -> Void
 132 | Not_GT_MaxBits8 = LTE_not_GT (LTE_MaxBits8 m)
 133 | 
 134 | ||| Every value of type `Bits8` is accessible with relation
 135 | ||| to `(<)`.
 136 | export
 137 | accessLT : (m : Bits8) -> Accessible (<) m
 138 | accessLT m = Access $ \n,lt => accessLT (assert_smaller m n)
 139 | 
 140 | ||| `(<)` is well founded.
 141 | export %inline
 142 | WellFounded Bits8 (<) where
 143 |   wellFounded = accessLT
 144 | 
 145 | ||| Every value of type `Bits8` is accessible with relation
 146 | ||| to `(>)`.
 147 | export
 148 | accessGT : (m : Bits8) -> Accessible (>) m
 149 | accessGT m = Access $ \n,gt => accessGT (assert_smaller m n)
 150 | 
 151 | ||| `(>)` is well founded.
 152 | export %inline
 153 | [GT] WellFounded Bits8 (>) where
 154 |   wellFounded = accessGT
 155 | 
 156 | --------------------------------------------------------------------------------
 157 | --          Arithmetics
 158 | --------------------------------------------------------------------------------
 159 | 
 160 | ||| Safe division.
 161 | |||
 162 | ||| This uses `0 < d` as a constraint instead
 163 | ||| of `0 /= d`, because in my experience, the former
 164 | ||| is much more useful.
 165 | export %inline
 166 | sdiv : (n,d : Bits8) -> (0 prf : 0 < d) => Bits8
 167 | sdiv n d = n `div` d
 168 | 
 169 | ||| Refined division.
 170 | |||
 171 | ||| This comes with a proof that the result is
 172 | ||| strictly smaller than `n`.
 173 | |||
 174 | ||| This uses `0 < n` as a constraint instead
 175 | ||| of `0 /= n`, because in my experience, the former
 176 | ||| is much more useful.
 177 | export %inline
 178 | rdiv :
 179 |      (n,d : Bits8)
 180 |   -> {auto 0 dgt1 : 1 < d}
 181 |   -> {auto 0 ngt0 : 0 < n}
 182 |   -> Subset Bits8 (< n)
 183 | rdiv n d = Element (n `div` d) (LT unsafeRefl)
 184 | 
 185 | ||| Safe modulo.
 186 | |||
 187 | ||| This uses `0 < d` as a constraint instead
 188 | ||| of `0 /= d`, because in my experience, the former
 189 | ||| is much more useful.
 190 | |||
 191 | ||| If you need the postcondition that the result is strictly
 192 | ||| smaller than `d`, use `rmod` instead.
 193 | export %inline
 194 | smod : (n,d : Bits8) -> (0 prf : 0 < d) => Bits8
 195 | smod n d = n `mod` d
 196 | 
 197 | ||| Refined modulo.
 198 | |||
 199 | ||| This comes with a proof that the result is strictly smaller
 200 | ||| than `d`.
 201 | |||
 202 | ||| It uses `0 < d` as a constraint instead
 203 | ||| of `0 /= d`, because in my experience, the former
 204 | ||| is much more useful.
 205 | export %inline
 206 | rmod : (n,d : Bits8) -> (0 prf : 0 < d) => Subset Bits8 (< d)
 207 | rmod n d = Element (n `mod` d) (LT unsafeRefl)
 208 |