
   0 | module Data.Prim.Bits32
   1 | 
   2 | import Data.Fin
   3 | import public Algebra.Ring
   4 | import public Control.Order
   5 | import public Control.Relation
   6 | import public Control.Relation.ReflexiveClosure
   7 | import public Control.Relation.Trichotomy
   8 | import public Control.WellFounded
   9 | import public Data.Maybe0
  10 | 
  11 | %default total
  12 | 
  13 | unsafeRefl : a === b
  14 | unsafeRefl = believe_me (Builtin.Refl {x = a})
  15 | 
  16 | ||| Witness that `m < n === True`.
  17 | export
  18 | data (<) : (m,n : Bits32) -> Type where
  19 |   LT : {0 m,n : Bits32} -> (0 prf : (m < n) === True) -> m < n
  20 | 
  21 | ||| Makes a compile-time proof of `x < y` available at runtime.
  22 | |||
  23 | ||| Heads up: `(<)` is not supposed to be used or even needed at runtime,
  24 | ||| as it will be erased anymay. However, this function is sometimes
  25 | ||| required, for instance when implementing interface `Connex`.
  26 | export
  27 | unerase : (0 p : m < n) -> m < n
  28 | unerase (LT p) = LT p
  29 | 
  30 | ||| Contructor for `(<)`.
  31 | |||
  32 | ||| This can only be used in an erased context.
  33 | export %hint
  34 | 0 mkLT : (0 prf : (m < n) === True) -> m < n
  35 | mkLT = LT
  36 | 
  37 | ||| Extractor for `(<)`.
  38 | |||
  39 | ||| This can only be used in an erased context.
  40 | export
  41 | 0 runLT : m < n -> (m < n) === True
  42 | runLT (LT prf) = prf
  43 | 
  44 | ||| We don't trust values of type `(<)` too much,
  45 | ||| so we use this when creating magical results.
  46 | export
  47 | strictLT : (0 p : m < n) -> Lazy c -> c
  48 | strictLT (LT prf) x = x
  49 | 
  50 | --------------------------------------------------------------------------------
  51 | --          Aliases
  52 | --------------------------------------------------------------------------------
  53 | 
  54 | ||| Flipped version of `(<)`.
  55 | public export
  56 | 0 (>) : (m,n : Bits32) -> Type
  57 | m > n = n < m
  58 | 
  59 | ||| Alias for `ReflexiveClosure (<) m n`
  60 | public export
  61 | 0 (<=) : (m,n : Bits32) -> Type
  62 | (<=) = ReflexiveClosure (<)
  63 | 
  64 | --------------------------------------------------------------------------------
  65 | --          Tests
  66 | --------------------------------------------------------------------------------
  67 | 
  68 | 0 ltNotEQ : m < n -> Not (m === n)
  69 | ltNotEQ x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and EQ")
  70 | 
  71 | 0 ltNotGT : m < n -> Not (n < m)
  72 | ltNotGT x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and GT")
  73 | 
  74 | 0 eqNotLT : m === n -> Not (m < n)
  75 | eqNotLT = flip ltNotEQ
  76 | 
  77 | public export %inline
  78 | lt : (x,y : Bits32) -> Maybe0 (x < y)
  79 | lt x y = case prim__lt_Bits32 x y of
  80 |   0 => Nothing0
  81 |   _ => Just0 (mkLT unsafeRefl)
  82 | 
  83 | public export %inline
  84 | lte : (x,y : Bits32) -> Maybe0 (x <= y)
  85 | lte x y = case prim__lte_Bits32 x y of
  86 |   0 => Nothing0
  87 |   _ => Just0 (if x < y then (Rel $ mkLT unsafeRefl) else (fromEq unsafeRefl))
  88 | 
  89 | export
  90 | comp : (m,n : Bits32) -> Trichotomy (<) m n
  91 | comp m n = case prim__lt_Bits32 m n of
  92 |   0 => case prim__eq_Bits32 m n of
  93 |     0 => GT (ltNotGT $ LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (LT unsafeRefl)
  94 |     x => EQ (eqNotLT unsafeRefl) (unsafeRefl) (eqNotLT unsafeRefl)
  95 |   x => LT (LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (ltNotGT $ LT unsafeRefl)
  96 | 
  97 | --------------------------------------------------------------------------------
  98 | --          Interfaces
  99 | --------------------------------------------------------------------------------
 100 | 
 101 | export %inline
 102 | Transitive Bits32 (<) where
 103 |   transitive _ _ = LT unsafeRefl
 104 | 
 105 | export %inline
 106 | Trichotomous Bits32 (<) where
 107 |   trichotomy m n = comp m n
 108 | 
 109 | --------------------------------------------------------------------------------
 110 | --          Bounds and Well-Foundedness
 111 | --------------------------------------------------------------------------------
 112 | 
 113 | ||| Lower bound of `Bits32`
 114 | public export
 115 | MinBits32 : Bits32
 116 | MinBits32 = 0
 117 | 
 118 | ||| Upper bound of `Bits32`
 119 | public export
 120 | MaxBits32 : Bits32
 121 | MaxBits32 = 0xffff_ffff
 122 | 
 123 | ||| `m >= 0` for all `m` of type `Bits32`.
 124 | export
 125 | 0 GTE_MinBits32 : (m : Bits32) -> MinBits32 <= m
 126 | GTE_MinBits32 m = case comp MinBits32 m of
 127 |   LT x f g => Rel x
 128 |   EQ f x g => fromEq x
 129 |   GT f g x => assert_total $ idris_crash "IMPOSSIBLE: Bits32 smaller than 0"
 130 | 
 131 | ||| Not value of type `Bits32` is less than zero.
 132 | export
 133 | 0 Not_LT_MinBits32 : m < 0 -> Void
 134 | Not_LT_MinBits32 p = Not_LT_and_GTE p (GTE_MinBits32 m)
 135 | 
 136 | ||| `m <= MaxBits32` for all `m` of type `Bits32`.
 137 | export
 138 | 0 LTE_MaxBits32 : (m : Bits32) -> m <= MaxBits32
 139 | LTE_MaxBits32 m = case comp m MaxBits32 of
 140 |   LT x f g => Rel x
 141 |   EQ f x g => fromEq x
 142 |   GT f g x => assert_total
 143 |             $ idris_crash "IMPOSSIBLE: Bits32 greater than \{show MaxBits32}"
 144 | 
 145 | ||| Not value of type `Bits32` is greater than `MaxBits32`.
 146 | export
 147 | 0 Not_GT_MaxBits32 : m > MaxBits32 -> Void
 148 | Not_GT_MaxBits32 p = Not_LT_and_GTE p (LTE_MaxBits32 m)
 149 | 
 150 | ||| Every value of type `Bits32` is accessible with relation
 151 | ||| to `(<)`.
 152 | export
 153 | accessLT : (m : Bits32) -> Accessible (<) m
 154 | accessLT m = Access $ \n,lt => accessLT (assert_smaller m n)
 155 | 
 156 | namespace WellFounded
 157 |   ||| `(<)` is well founded.
 158 |   export %inline
 159 |   [LT] WellFounded Bits32 (<) where
 160 |     wellFounded = accessLT
 161 | 
 162 |   ||| Every value of type `Bits32` is accessible with relation
 163 |   ||| to `(>)`.
 164 |   export
 165 |   accessGT : (m : Bits32) -> Accessible (>) m
 166 |   accessGT m = Access $ \n,gt => accessGT (assert_smaller m n)
 167 | 
 168 |   ||| `(>)` is well founded.
 169 |   export %inline
 170 |   [GT] WellFounded Bits32 (>) where
 171 |     wellFounded = accessGT
 172 | 
 173 | --------------------------------------------------------------------------------
 174 | --          Conversions
 175 | --------------------------------------------------------------------------------
 176 | 
 177 | export
 178 | 0 ltImpliesNatLT : (x,y : Bits32) -> x < y => Nat.lt (cast x) (cast y) === True
 179 | ltImpliesNatLT x y = unsafeRefl
 180 | 
 181 | export
 182 | 0 lteImpliesNatLT : (x,y : Bits32) -> x <= y => Nat.lt (cast x) (S $ cast y) === True
 183 | lteImpliesNatLT x y = unsafeRefl
 184 | 
 185 | export
 186 | 0 gtImpliesNatGT : (x,y : Bits32) -> x > y => Nat.gt (cast x) (cast y) === True
 187 | gtImpliesNatGT x y = ltImpliesNatLT y x
 188 | 
 189 | export %inline
 190 | bits32ToFin : (x : Bits32) -> (0 y : Bits32) -> (0 lt : x < y) => Fin (cast y)
 191 | bits32ToFin x y = natToFinLT (cast x) @{ltReflectsLT _ _ $ ltImpliesNatLT x y}
 192 | 
 193 | export %inline
 194 | bits32ToFinLTE : (x : Bits32) -> (0 y : Bits32) -> (0 lte : x <= y) => Fin (S $ cast y)
 195 | bits32ToFinLTE x y = natToFinLT (cast x) @{ltReflectsLT _ _ $ lteImpliesNatLT x y}
 196 | 
 197 | export %inline
 198 | Cast Bits32 (Fin 0x1_0000_0000) where
 199 |   cast x = bits32ToFinLTE x 0xffff_ffff @{LTE_MaxBits32 x}
 200 |