0 | module Data.Prim.Integer
  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 Data.Maybe0
  8 |
  9 | %default total
 10 |
 11 | unsafeRefl : a === b
 12 | unsafeRefl = believe_me (Builtin.Refl {x = a})
 13 |
 14 | ||| Witness that `m < n === True`.
 15 | export
 16 | data (<) : (m,n : Integer) -> Type where
 17 |   LT : {0 m,n : Integer} -> (0 prf : (m < n) === True) -> m < n
 18 |
 19 | ||| Makes a compile-time proof of `x < y` available at runtime.
 20 | |||
 21 | ||| Heads up: `(<)` is not supposed to be used or even needed at runtime,
 22 | ||| as it will be erased anymay. However, this function is sometimes
 23 | ||| required, for instance when implementing interface `Connex`.
 24 | export
 25 | unerase : (0 p : m < n) -> m < n
 26 | unerase (LT p) = LT p
 27 |
 28 | ||| Contructor for `(<)`.
 29 | |||
 30 | ||| This can only be used in an erased context.
 31 | export %hint
 32 | 0 mkLT : (0 prf : (m < n) === True) -> m < n
 33 | mkLT = LT
 34 |
 35 | ||| Extractor for `(<)`.
 36 | |||
 37 | ||| This can only be used in an erased context.
 38 | export
 39 | 0 runLT : m < n -> (m < n) === True
 40 | runLT (LT prf) = prf
 41 |
 42 | ||| We don't trust values of type `(<)` too much,
 43 | ||| so we use this when creating magical results.
 44 | export
 45 | strictLT : (0 p : m < n) -> Lazy c -> c
 46 | strictLT (LT prf) x = x
 47 |
 48 | --------------------------------------------------------------------------------
 49 | --          Aliases
 50 | --------------------------------------------------------------------------------
 51 |
 52 | ||| Flipped version of `(<)`.
 53 | public export
 54 | 0 (>) : (m,n : Integer) -> Type
 55 | m > n = n < m
 56 |
 57 | ||| Alias for `ReflexiveClosure (<) m n`
 58 | public export
 59 | 0 (<=) : (m,n : Integer) -> Type
 60 | (<=) = ReflexiveClosure (<)
 61 |
 62 | --------------------------------------------------------------------------------
 63 | --          Tests
 64 | --------------------------------------------------------------------------------
 65 |
 66 | 0 ltNotEQ : m < n -> Not (m === n)
 67 | ltNotEQ x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and EQ")
 68 |
 69 | 0 ltNotGT : m < n -> Not (n < m)
 70 | ltNotGT x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and GT")
 71 |
 72 | 0 eqNotLT : m === n -> Not (m < n)
 73 | eqNotLT = flip ltNotEQ
 74 |
 75 | public export %inline
 76 | lt : (x,y : Integer) -> Maybe0 (x < y)
 77 | lt x y = case prim__lt_Integer x y of
 78 |   0 => Nothing0
 79 |   _ => Just0 (mkLT unsafeRefl)
 80 |
 81 | public export %inline
 82 | lte : (x,y : Integer) -> Maybe0 (x <= y)
 83 | lte x y = case prim__lte_Integer x y of
 84 |   0 => Nothing0
 85 |   _ => Just0 (if x < y then (Rel $ mkLT unsafeRefl) else (fromEq unsafeRefl))
 86 |
 87 | export
 88 | comp : (m,n : Integer) -> Trichotomy (<) m n
 89 | comp m n = case prim__lt_Integer m n of
 90 |   0 => case prim__eq_Integer m n of
 91 |     0 => GT (ltNotGT $ LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (LT unsafeRefl)
 92 |     x => EQ (eqNotLT unsafeRefl) (unsafeRefl) (eqNotLT unsafeRefl)
 93 |   x => LT (LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (ltNotGT $ LT unsafeRefl)
 94 |
 95 | --------------------------------------------------------------------------------
 96 | --          Interfaces
 97 | --------------------------------------------------------------------------------
 98 |
 99 | export %inline
100 | Transitive Integer (<) where
101 |   transitive _ _ = LT unsafeRefl
102 |
103 | export %inline
104 | Trichotomous Integer (<) where
105 |   trichotomy m n = comp m n
106 |
107 | --------------------------------------------------------------------------------
108 | --          Axioms
109 | --------------------------------------------------------------------------------
110 |
111 | ||| This axiom, which only holds for unbounded integers, relates
112 | ||| addition and the ordering of integers:
113 | |||
114 | ||| From `k < m` follows `n + k < n + m` for all integers `k`, `m`, and `n`.
115 | export
116 | 0 plusGT : (k,m,n : Integer) -> k < m -> n + k < n + m
117 | plusGT k m n x = strictLT x $ mkLT unsafeRefl
118 |
119 | ||| This axiom, which only holds for unbounded integers, relates
120 | ||| multiplication and the ordering of integers:
121 | |||
122 | ||| From `0 < m` and `0 < n` follows `0 < m * n` for all integers `m` and `n`.
123 | export
124 | 0 multPosPosGT0 : (m,n : Integer) -> 0 < m -> 0 < n -> 0 < m * n
125 | multPosPosGT0 _ _ p1 p2 = strictLT p1 $ strictLT p2 $ mkLT unsafeRefl
126 |