0 | module Text.ILex.Char.Range
  1 |
  2 | import Derive.Prelude
  3 |
  4 | %default total
  5 | %language ElabReflection
  6 |
  7 | --------------------------------------------------------------------------------
  8 | --- WithBounds Interface
  9 | --------------------------------------------------------------------------------
 10 |
 11 | public export
 12 | interface Ord a => WithBounds a where
 13 |   minBound : a
 14 |   maxBound : a
 15 |
 16 | export %inline
 17 | WithBounds Bits8 where
 18 |   minBound = 0
 19 |   maxBound = 0xff
 20 |
 21 | export %inline
 22 | WithBounds Bits16 where
 23 |   minBound = 0
 24 |   maxBound = 0xffff
 25 |
 26 | export %inline
 27 | WithBounds Bits32 where
 28 |   minBound = 0
 29 |   maxBound = 0xffff_ffff
 30 |
 31 | export %inline
 32 | WithBounds Bits64 where
 33 |   minBound = 0
 34 |   maxBound = 0xffff_ffff_ffff_ffff
 35 |
 36 | --------------------------------------------------------------------------------
 37 | --- Range
 38 | --------------------------------------------------------------------------------
 39 |
 40 | ||| A range of unicode code points.
 41 | |||
 42 | ||| Actually, it's a range of 32-bit numbers, but we use it for describing
 43 | ||| ranges of codepoints in this library.
 44 | export
 45 | data RangeOf : (t : Type) -> Type where
 46 |   Empty : RangeOf t
 47 |   Rng   : (low,up : t) -> RangeOf t
 48 |
 49 | %runElab derive "RangeOf" [Show,Eq,Ord]
 50 |
 51 | public export
 52 | 0 Range8 : Type
 53 | Range8 = RangeOf Bits8
 54 |
 55 | public export
 56 | 0 Range32 : Type
 57 | Range32 = RangeOf Bits32
 58 |
 59 | ||| The empty range of codepoints.
 60 | export %inline
 61 | empty : RangeOf t
 62 | empty = Empty
 63 |
 64 | ||| A range containing a single value
 65 | export %inline
 66 | singleton : t -> RangeOf t
 67 | singleton v = Rng v v
 68 |
 69 | export %inline
 70 | isEmpty : RangeOf t -> Bool
 71 | isEmpty Empty = True
 72 | isEmpty _     = False
 73 |
 74 | ||| Generates a new range from `x` to `y` if `x` is strictly
 75 | ||| smaller than `y`. Otherwise, the empty range is returned.
 76 | export %inline
 77 | range : Ord t => (x,y : t) -> RangeOf t
 78 | range x y =
 79 |   case x <= y of
 80 |     True  => Rng x y
 81 |     False => Empty
 82 |
 83 | ||| True if the value is within the range.
 84 | export
 85 | has : Ord t => RangeOf t -> t -> Bool
 86 | has Empty     _ = False
 87 | has (Rng x y) v = x <= v && v <= y
 88 |
 89 | ||| True if the two ranges overlap
 90 | export
 91 | overlap : Ord t => RangeOf t -> RangeOf t -> Bool
 92 | overlap r1@(Rng l1 u1) r2@(Rng l2 u2) = has r1 l2 || has r2 l1
 93 | overlap _              _              = False
 94 |
 95 | ||| Spans the range from the lowest to the largest bound of the two ranges.
 96 | export
 97 | span : Ord t => RangeOf t -> RangeOf t -> RangeOf t
 98 | span r1@(Rng l1 u1) r2@(Rng l2 u2) = Rng (min l1 l2) (max u1 u2)
 99 | span Empty          r              = r
100 | span l              Empty          = l
101 |
102 | ||| Intersection of two ranges, if any.
103 | export
104 | intersection : Ord t => RangeOf t -> RangeOf t -> RangeOf t
105 | intersection (Rng l1 u1) (Rng l2 u2) =
106 |   if l1 <= l2 then range l2 (min u1 u2) else range l1 (min u2 u1)
107 | intersection _           _           = Empty
108 |
109 | parameters {0 t : Type}
110 |            {auto ord : Ord t}
111 |            {auto ng  : Neg t}
112 |
113 |
114 |   fromTill : (x,y : t) -> RangeOf t
115 |   fromTill x y =
116 |     case x < y of
117 |       True  => range x (y-1)
118 |       False => Empty
119 |
120 |   afterTo : (x,y : t) -> RangeOf t
121 |   afterTo x y =
122 |     case x < y of
123 |       True  => range (x+1) y
124 |       False => Empty
125 |
126 |   ||| True if the two ranges are adjacent, that is, the upper bound
127 |   ||| of one range is one less than the lower bound of the other.
128 |   export
129 |   adjacent : RangeOf t -> RangeOf t -> Bool
130 |   adjacent (Rng l1 u1) (Rng l2 u2) =
131 |     (u1 < l2 && (u1+1) == l2) || (u2 < l1 && (u2+1) == l1)
132 |   adjacent _           _           = False
133 |
134 |   ||| Union of the ranges.
135 |   |||
136 |   ||| If there are two results then they are guaranteed to be non-empty,
137 |   ||| have a non-empty gap in between, and are in ascending order
138 |   export
139 |   union : RangeOf t -> RangeOf t -> Either (RangeOf t) (RangeOf t,RangeOf t)
140 |   union r1@(Rng l1 u1) r2@(Rng l2 u2) =
141 |     if overlap r1 r2 || adjacent r1 r2
142 |        then Left (span r1 r2)
143 |        else Right (min r1 r2, max r1 r2)
144 |   union Empty       r           = Left r
145 |   union l           Empty       = Left l
146 |
147 |   ||| Returns the result of subtracting the second range from the first.
148 |   |||
149 |   ||| If there are two results then they are guaranteed to be non-empty,
150 |   ||| have a non-empty gap in between, and are in ascending order
151 |   export
152 |   difference : RangeOf t -> RangeOf t -> Either (RangeOf t) (RangeOf t,RangeOf t)
153 |   difference r1@(Rng l1 u1) r2@(Rng l2 u2) =
154 |     case overlap r1 r2 of
155 |       True  =>
156 |         let x@(Rng _ _) := fromTill l1 l2 | Empty => Left (afterTo u2 u1)
157 |             y@(Rng _ _) := afterTo u2 u1 | Empty => Left x
158 |          in Right (min x y, max x y)
159 |       False => Left r1
160 |   difference Empty       r           = Left Empty
161 |   difference l           Empty       = Left l
162 |
163 | ||| The range of all unicode code points.
164 | export
165 | codepoint : Range32
166 | codepoint = Rng 0 0x10ffff
167 |
168 | ||| The range of surrogate pairs.
169 | export
170 | surrogate : Range32
171 | surrogate = Rng 0xd800 0xdfff
172 |
173 | ||| A range corresponding to a pair of characters.
174 | export %inline
175 | charRange : (x,y : Char) -> Range32
176 | charRange x y = range (cast x) (cast y)
177 |
178 | ||| The full range.  All 32 bit values are within it.
179 | export %inline
180 | fullRange : WithBounds t => RangeOf t
181 | fullRange = Rng minBound maxBound
182 |
183 | ||| A range is full if it contains every possible value.
184 | export %inline
185 | isFull : WithBounds t => RangeOf t -> Bool
186 | isFull = (== fullRange)
187 |
188 | export
189 | lowerBound : WithBounds t => RangeOf t -> t
190 | lowerBound (Rng l _) = l
191 | lowerBound Empty     = maxBound
192 |
193 | export
194 | upperBound : WithBounds t => RangeOf t -> t
195 | upperBound (Rng _ u) = u
196 | upperBound Empty     = minBound
197 |