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