
   0 | module Data.Prim.Int32
   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 : Int32) -> Type where
  20 |   LT : {0 m,n : Int32} -> (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 : Int32) -> 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 : Int32) -> Type
  54 | m <= n = Either (m < n) (m === n)
  55 | 
  56 | ||| Flipped version of `(<=)`.
  57 | public export
  58 | 0 (>=) : (m,n : Int32) -> 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 : Int32) -> 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 : Int32) -> Trichotomy (<) m n
  81 | comp m n = case prim__lt_Int32 m n of
  82 |   0 => case prim__eq_Int32 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 Int32 (<) 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 `Int32`
  97 | public export
  98 | MinInt32 : Int32
  99 | MinInt32 = -0x80000000
 100 | 
 101 | ||| Upper bound of `Int32`
 102 | public export
 103 | MaxInt32 : Int32
 104 | MaxInt32 = 0x7fffffff
 105 | 
 106 | ||| `m >= MinInt32` for all `m` of type `Int32`.
 107 | export
 108 | 0 GTE_MinInt32 : (m : Int32) -> m >= MinInt32
 109 | GTE_MinInt32 m = case comp MinInt32 m of
 110 |   LT x f g => %search
 111 |   EQ f x g => %search
 112 |   GT f g x =>
 113 |     assert_total $
 114 |     idris_crash "IMPOSSIBLE: Int32 smaller than \{show MinInt32}"
 115 | 
 116 | ||| Not value of type `Int32` is less than zero.
 117 | export
 118 | 0 Not_LT_MinInt32 : m < MinInt32 -> Void
 119 | Not_LT_MinInt32 = GTE_not_LT (GTE_MinInt32 m)
 120 | 
 121 | ||| `m <= MaxInt32` for all `m` of type `Int32`.
 122 | export
 123 | 0 LTE_MaxInt32 : (m : Int32) -> m <= MaxInt32
 124 | LTE_MaxInt32 m = case comp m MaxInt32 of
 125 |   LT x f g => %search
 126 |   EQ f x g => %search
 127 |   GT f g x =>
 128 |     assert_total $
 129 |     idris_crash "IMPOSSIBLE: Int32 greater than \{show MaxInt32}"
 130 | 
 131 | ||| Not value of type `Int32` is greater than `MaxInt32`.
 132 | export
 133 | 0 Not_GT_MaxInt32 : m > MaxInt32 -> Void
 134 | Not_GT_MaxInt32 = LTE_not_GT (LTE_MaxInt32 m)
 135 | 
 136 | ||| Every value of type `Int32` is accessible with relation
 137 | ||| to `(<)`.
 138 | export
 139 | accessLT : (m : Int32) -> Accessible (<) m
 140 | accessLT m = Access $ \n,lt => accessLT (assert_smaller m n)
 141 | 
 142 | ||| `(<)` is well founded.
 143 | export %inline
 144 | WellFounded Int32 (<) where
 145 |   wellFounded = accessLT
 146 | 
 147 | ||| Every value of type `Int32` is accessible with relation
 148 | ||| to `(>)`.
 149 | export
 150 | accessGT : (m : Int32) -> Accessible (>) m
 151 | accessGT m = Access $ \n,gt => accessGT (assert_smaller m n)
 152 | 
 153 | ||| `(>)` is well founded.
 154 | export %inline
 155 | [GT] WellFounded Int32 (>) where
 156 |   wellFounded = accessGT
 157 | 
 158 | --------------------------------------------------------------------------------
 159 | --          Arithmetics
 160 | --------------------------------------------------------------------------------
 161 | 
 162 | ||| Safe division.
 163 | export %inline
 164 | sdiv : (n,d : Int32) -> (0 prf : d /= 0) => Int32
 165 | sdiv n d = n `div` d
 166 | 
 167 | ||| Safe modulo.
 168 | export %inline
 169 | smod : (n,d : Int32) -> (0 prf : d /= 0) => Int32
 170 | smod n d = n `mod` d
 171 |