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