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