0 | module Data.Refined.Char
  1 |
  2 | import Control.Relation.ReflexiveClosure
  3 | import Control.Relation
  4 | import public Data.Prim.Char
  5 | import public Data.Refined.Core
  6 |
  7 | public export %inline
  8 | {x : Char} -> HDec0 Char (< x) where
  9 |   hdec0 v = lt v x
 10 |
 11 | public export %inline
 12 | {x : Char} -> HDec0 Char (x <) where
 13 |   hdec0 v = lt x v
 14 |
 15 | public export %inline
 16 | {x : Char} -> HDec0 Char (<= x) where
 17 |   hdec0 v = lte v x
 18 |
 19 | public export %inline
 20 | {x : Char} -> HDec0 Char (x <=) where
 21 |   hdec0 v = lte x v
 22 |
 23 | --------------------------------------------------------------------------------
 24 | --          Non-operators
 25 | --------------------------------------------------------------------------------
 26 |
 27 | ||| `LessThan m n` is an alias for `n < m`.
 28 | |||
 29 | ||| This is useful when defining ranges such as
 30 | ||| `From 2 && LessThan 10`, but it gives the wrong idea when used in
 31 | ||| infix notation. So, don't do this: ```x `LessThan` 10```.
 32 | public export
 33 | 0 LessThan : Char -> Char -> Type
 34 | LessThan m n = n < m
 35 |
 36 | ||| `From m n` is an alias for `n <= m`.
 37 | public export
 38 | 0 To : Char -> Char -> Type
 39 | To m n = ReflexiveClosure (<) n m
 40 |
 41 | ||| `GreaterThan m n` is an alias for `m < n`.
 42 | |||
 43 | ||| This is useful when defining ranges such as
 44 | ||| `From 2 && LessThan 10`, but it gives the wrong idea when used in
 45 | ||| infix notation. So, don't do this: ```x `GreaterThan` 10```.
 46 | public export
 47 | 0 GreaterThan : Char -> Char -> Type
 48 | GreaterThan = (<)
 49 |
 50 | ||| `From m n` is an alias for `m <= n`.
 51 | public export
 52 | 0 From : Char -> Char -> Type
 53 | From = ReflexiveClosure (<)
 54 |
 55 | ||| `FromTo m n` is an alias for `From m && To n`.
 56 | public export
 57 | 0 FromTo : Char -> Char -> Char -> Type
 58 | FromTo m n = From m && To n
 59 |
 60 | ||| `Between m n` is an alias for `GreaterThan m && LessThan n`.
 61 | public export
 62 | 0 Between : Char -> Char -> Char -> Type
 63 | Between m n = GreaterThan m && LessThan n
 64 |
 65 | --------------------------------------------------------------------------------
 66 | --          Widenings
 67 | --------------------------------------------------------------------------------
 68 |
 69 | export
 70 | 0 widen :
 71 |      FromTo m n x
 72 |   -> {auto 0 p1 : m2 <= m}
 73 |   -> {auto 0 p2 : n  <= n2}
 74 |   -> FromTo m2 n2 x
 75 | widen (And y z) = And (transitive p1 y) (transitive z p2)
 76 |
 77 | export
 78 | 0 widen' :
 79 |      Between m n x
 80 |   -> {auto 0 p1 : m2 <= m}
 81 |   -> {auto 0 p2 : n  <= n2}
 82 |   -> Between m2 n2 x
 83 | widen' (And y z) = And (strictRight p1 y) (strictLeft z p2)
 84 |
 85 | --------------------------------------------------------------------------------
 86 | --          Classes
 87 | --------------------------------------------------------------------------------
 88 |
 89 | public export
 90 | 0 Ascii : Char -> Type
 91 | Ascii = (< '\128')
 92 |
 93 | public export
 94 | 0 Printable : Char -> Type
 95 | Printable = Holds (not . isControl)
 96 |
 97 | public export
 98 | 0 PrintableAscii : Char -> Type
 99 | PrintableAscii = Ascii && Printable
100 |
101 | public export
102 | 0 Upper : Char -> Type
103 | Upper = FromTo 'A' 'Z'
104 |
105 | public export
106 | 0 Lower : Char -> Type
107 | Lower = FromTo 'a' 'z'
108 |
109 | public export
110 | 0 Binit : Char -> Type
111 | Binit = FromTo '0' '1'
112 |
113 | public export
114 | 0 Octit : Char -> Type
115 | Octit = FromTo '0' '9'
116 |
117 | public export
118 | 0 Digit : Char -> Type
119 | Digit = FromTo '0' '9'
120 |
121 | public export
122 | 0 Hexit : Char -> Type
123 | Hexit = Digit || FromTo 'a' 'f' || FromTo 'A' 'F'
124 |
125 | public export
126 | 0 Alpha : Char -> Type
127 | Alpha = Lower || Upper
128 |
129 | public export
130 | 0 AlphaNum : Char -> Type
131 | AlphaNum = Alpha || Digit
132 |