0 | module Data.Prim.String
  1 |
  2 | import public Data.DPair
  3 | import public Data.Prim.Ord
  4 |
  5 | %default total
  6 |
  7 | unsafeRefl : a === b
  8 | unsafeRefl = believe_me (Refl {x = a})
  9 |
 10 | --------------------------------------------------------------------------------
 11 | --          (<)
 12 | --------------------------------------------------------------------------------
 13 |
 14 | ||| Witness that `m < n === True`.
 15 | export
 16 | data (<) : (m,n : String) -> Type where
 17 |   LT : {0 m,n : String} -> (0 prf : (m < n) === True) -> m < n
 18 |
 19 | ||| Contructor for `(<)`.
 20 | |||
 21 | ||| This can only be used in an erased context.
 22 | export %hint
 23 | 0 mkLT : (0 prf : (m < n) === True) -> m < n
 24 | mkLT = LT
 25 |
 26 | ||| Extractor for `(<)`.
 27 | |||
 28 | ||| This can only be used in an erased context.
 29 | export
 30 | 0 runLT : m < n -> (m < n) === True
 31 | runLT (LT prf) = prf
 32 |
 33 | ||| We don't trust values of type `(<)` too much,
 34 | ||| so we use this when creating magical results.
 35 | export
 36 | strictLT : (0 p : m < n) -> Lazy c -> c
 37 | strictLT (LT prf) x = x
 38 |
 39 | --------------------------------------------------------------------------------
 40 | --          Aliases
 41 | --------------------------------------------------------------------------------
 42 |
 43 | ||| Flipped version of `(<)`.
 44 | public export
 45 | 0 (>) : (m,n : String) -> Type
 46 | m > n = n < m
 47 |
 48 | ||| `m <= n` mean that either `m < n` or `m === n` holds.
 49 | public export
 50 | 0 (<=) : (m,n : String) -> Type
 51 | m <= n = Either (m < n) (m === n)
 52 |
 53 | ||| Flipped version of `(<=)`.
 54 | public export
 55 | 0 (>=) : (m,n : String) -> Type
 56 | m >= n = n <= m
 57 |
 58 | ||| `m /= n` mean that either `m < n` or `m > n` holds.
 59 | public export
 60 | 0 (/=) : (m,n : String) -> Type
 61 | m /= n = Either (m < n) (m > n)
 62 |
 63 | --------------------------------------------------------------------------------
 64 | --          Order
 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 | export
 77 | comp : (m,n : String) -> Trichotomy (<) m n
 78 | comp m n = case prim__lt_String m n of
 79 |   0 => case prim__eq_String m n of
 80 |     0 => GT (ltNotGT $ LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (LT unsafeRefl)
 81 |     x => EQ (eqNotLT unsafeRefl) (unsafeRefl) (eqNotLT unsafeRefl)
 82 |   x => LT (LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (ltNotGT $ LT unsafeRefl)
 83 |
 84 | export
 85 | Total String (<) where
 86 |   trichotomy   = comp
 87 |   transLT p q  = strictLT p $ strictLT q $ LT unsafeRefl
 88 |
 89 | --------------------------------------------------------------------------------
 90 | --          Bounds and Well-Foundedness
 91 | --------------------------------------------------------------------------------
 92 |
 93 | ||| Lower bound of `String`
 94 | public export
 95 | MinString : String
 96 | MinString = ""
 97 |
 98 | ||| `m >= MinString` for all `m` of type `String`.
 99 | export
100 | 0 GTE_MinString : (m : String) -> m >= MinString
101 | GTE_MinString m = case comp MinString m of
102 |   LT x f g => %search
103 |   EQ f x g => %search
104 |   GT f g x => assert_total $ idris_crash #"IMPOSSIBLE: String smaller than """#
105 |
106 | ||| Not value of type `String` is less than `MinString`.
107 | export
108 | 0 Not_LT_MinString : m < MinString -> Void
109 | Not_LT_MinString = GTE_not_LT (GTE_MinString m)
110 |