0 | module Data.Prim.String
  1 |
  2 | import public Control.Order
  3 | import public Control.Relation
  4 | import public Control.Relation.ReflexiveClosure
  5 | import public Control.Relation.Trichotomy
  6 | import public Data.Maybe0
  7 |
  8 | %default total
  9 |
 10 | unsafeRefl : a === b
 11 | unsafeRefl = believe_me (Builtin.Refl {x = a})
 12 |
 13 | --------------------------------------------------------------------------------
 14 | --          (<)
 15 | --------------------------------------------------------------------------------
 16 |
 17 | ||| Witness that `m < n === True`.
 18 | export
 19 | data (<) : (m,n : String) -> Type where
 20 |   LT : {0 m,n : String} -> (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 : String) -> 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 : String) -> Type
 54 | (<=) = ReflexiveClosure (<)
 55 |
 56 | --------------------------------------------------------------------------------
 57 | --          Order
 58 | --------------------------------------------------------------------------------
 59 |
 60 | 0 ltNotEQ : m < n -> Not (m === n)
 61 | ltNotEQ x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and EQ")
 62 |
 63 | 0 ltNotGT : m < n -> Not (n < m)
 64 | ltNotGT x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and GT")
 65 |
 66 | 0 eqNotLT : m === n -> Not (m < n)
 67 | eqNotLT = flip ltNotEQ
 68 |
 69 | public export %inline
 70 | lt : (x,y : String) -> Maybe0 (x < y)
 71 | lt x y = case prim__lt_String x y of
 72 |   0 => Nothing0
 73 |   _ => Just0 (mkLT unsafeRefl)
 74 |
 75 | public export %inline
 76 | lte : (x,y : String) -> Maybe0 (x <= y)
 77 | lte x y = case prim__lte_String x y of
 78 |   0 => Nothing0
 79 |   _ => Just0 (if x < y then (Rel $ mkLT unsafeRefl) else (fromEq unsafeRefl))
 80 |
 81 | export
 82 | comp : (m,n : String) -> Trichotomy (<) m n
 83 | comp m n = case prim__lt_String m n of
 84 |   0 => case prim__eq_String m n of
 85 |     0 => GT (ltNotGT $ LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (LT unsafeRefl)
 86 |     x => EQ (eqNotLT unsafeRefl) (unsafeRefl) (eqNotLT unsafeRefl)
 87 |   x => LT (LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (ltNotGT $ LT unsafeRefl)
 88 |
 89 | --------------------------------------------------------------------------------
 90 | --          Interfaces
 91 | --------------------------------------------------------------------------------
 92 |
 93 | export %inline
 94 | Transitive String (<) where
 95 |   transitive _ _ = LT unsafeRefl
 96 |
 97 | export %inline
 98 | Trichotomous String (<) where
 99 |   trichotomy m n = comp m n
100 |
101 | --------------------------------------------------------------------------------
102 | --          Bounds and Well-Foundedness
103 | --------------------------------------------------------------------------------
104 |
105 | ||| Lower bound of `String`
106 | public export
107 | MinString : String
108 | MinString = ""
109 |
110 | ||| `m >= MinString` for all `m` of type `String`.
111 | export
112 | 0 GTE_MinString : (m : String) -> MinString <= m
113 | GTE_MinString m = case comp MinString m of
114 |   LT x f g => %search
115 |   EQ f x g => fromEq x
116 |   GT f g x => assert_total $ idris_crash #"IMPOSSIBLE: String smaller than """#
117 |
118 | ||| Not value of type `String` is less than `MinString`.
119 | export
120 | 0 Not_LT_MinString : m < MinString -> Void
121 | Not_LT_MinString p = Not_LT_and_GTE p (GTE_MinString m)
122 |