0 | module Data.Prim.Char
  1 |
  2 | import public Control.WellFounded
  3 | import public Data.DPair
  4 | import public Data.Prim.Ord
  5 |
  6 | %default total
  7 |
  8 | unsafeRefl : a === b
  9 | unsafeRefl = believe_me (Refl {x = a})
 10 |
 11 | --------------------------------------------------------------------------------
 12 | --          (<)
 13 | --------------------------------------------------------------------------------
 14 |
 15 | ||| Witness that `m < n === True`.
 16 | export
 17 | data (<) : (m,n : Char) -> Type where
 18 |   LT : {0 m,n : Char} -> (0 prf : (m < n) === True) -> m < n
 19 |
 20 | ||| Contructor for `(<)`.
 21 | |||
 22 | ||| This can only be used in an erased context.
 23 | export %hint
 24 | 0 mkLT : (0 prf : (m < n) === True) -> m < n
 25 | mkLT = LT
 26 |
 27 | ||| Extractor for `(<)`.
 28 | |||
 29 | ||| This can only be used in an erased context.
 30 | export
 31 | 0 runLT : m < n -> (m < n) === True
 32 | runLT (LT prf) = prf
 33 |
 34 | ||| We don't trust values of type `(<)` too much,
 35 | ||| so we use this when creating magical results.
 36 | export
 37 | strictLT : (0 p : m < n) -> Lazy c -> c
 38 | strictLT (LT prf) x = x
 39 |
 40 | --------------------------------------------------------------------------------
 41 | --          Aliases
 42 | --------------------------------------------------------------------------------
 43 |
 44 | ||| Flipped version of `(<)`.
 45 | public export
 46 | 0 (>) : (m,n : Char) -> Type
 47 | m > n = n < m
 48 |
 49 | ||| `m <= n` mean that either `m < n` or `m === n` holds.
 50 | public export
 51 | 0 (<=) : (m,n : Char) -> Type
 52 | m <= n = Either (m < n) (m === n)
 53 |
 54 | ||| Flipped version of `(<=)`.
 55 | public export
 56 | 0 (>=) : (m,n : Char) -> Type
 57 | m >= n = n <= m
 58 |
 59 | ||| `m /= n` mean that either `m < n` or `m > n` holds.
 60 | public export
 61 | 0 (/=) : (m,n : Char) -> Type
 62 | m /= n = Either (m < n) (m > n)
 63 |
 64 | --------------------------------------------------------------------------------
 65 | --          Order
 66 | --------------------------------------------------------------------------------
 67 |
 68 | 0 ltNotEQ : m < n -> Not (m === n)
 69 | ltNotEQ x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and EQ")
 70 |
 71 | 0 ltNotGT : m < n -> Not (n < m)
 72 | ltNotGT x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and GT")
 73 |
 74 | 0 eqNotLT : m === n -> Not (m < n)
 75 | eqNotLT = flip ltNotEQ
 76 |
 77 | export
 78 | comp : (m,n : Char) -> Trichotomy (<) m n
 79 | comp m n = case prim__lt_Char m n of
 80 |   0 => case prim__eq_Char m n of
 81 |     0 => GT (ltNotGT $ LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (LT unsafeRefl)
 82 |     x => EQ (eqNotLT unsafeRefl) (unsafeRefl) (eqNotLT unsafeRefl)
 83 |   x => LT (LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (ltNotGT $ LT unsafeRefl)
 84 |
 85 | export
 86 | Total Char (<) where
 87 |   trichotomy   = comp
 88 |   transLT p q  = strictLT p $ strictLT q $ LT unsafeRefl
 89 |
 90 | --------------------------------------------------------------------------------
 91 | --          Bounds and Well-Foundedness
 92 | --------------------------------------------------------------------------------
 93 |
 94 | ||| Lower bound of `Char`
 95 | public export
 96 | MinChar : Char
 97 | MinChar = '\x0000'
 98 |
 99 | ||| `m >= MinChar` for all `m` of type `Char`.
100 | export
101 | 0 GTE_MinChar : (m : Char) -> m >= MinChar
102 | GTE_MinChar m = case comp MinChar m of
103 |   LT x f g => %search
104 |   EQ f x g => %search
105 |   GT f g x => assert_total $ idris_crash "IMPOSSIBLE: Char smaller than 0"
106 |
107 | ||| Not value of type `Char` is less than `MinChar`.
108 | export
109 | 0 Not_LT_MinChar : m < MinChar -> Void
110 | Not_LT_MinChar = GTE_not_LT (GTE_MinChar m)
111 |
112 | ||| Every value of type `Char` is accessible with relation
113 | ||| to `(<)`.
114 | export
115 | accessLT : (m : Char) -> Accessible (<) m
116 | accessLT m = Access $ \n,lt => accessLT (assert_smaller m n)
117 |
118 | ||| `(<)` is well founded.
119 | export %inline
120 | WellFounded Char (<) where
121 |   wellFounded = accessLT
122 |