0 | module Text.ILex.Char.Set
3 | import Derive.Prelude
4 | import public Text.ILex.Char.Range
6 | %language ElabReflection
17 | record SetOf t where
20 | ranges_ : List (RangeOf t)
22 | %runElab derive "SetOf" [Show,Eq,Ord]
30 | Set32 = SetOf Bits32
37 | ranges : SetOf t -> List (RangeOf t)
47 | singleton : t -> SetOf t
48 | singleton x = S [singleton x]
52 | range : RangeOf t -> SetOf t
53 | range r = if isEmpty r then empty else S [r]
57 | isEmpty : SetOf t -> Bool
58 | isEmpty (S []) = True
63 | has : Ord t => SetOf t -> t -> Bool
64 | has (S rs) v = any (`has` v) rs
66 | parameters {0 t : Type}
67 | {auto ord : WithBounds t}
71 | normalise : SnocList (RangeOf t) -> Vect n (RangeOf t) -> List (RangeOf t)
72 | normalise sc [] = sc <>> []
73 | normalise sc [r] = if isEmpty r then [] else sc <>> [r]
74 | normalise sc (r1 :: r2 :: t) =
76 | Left r => if isEmpty r then normalise sc t else normalise sc (r::t)
77 | Right (x,y) => normalise (sc:<x) (y::t)
84 | rangeSet : List (RangeOf t) -> SetOf t
85 | rangeSet rs = S . normalise [<] $
fromList (sort rs)
89 | union : SetOf t -> SetOf t -> SetOf t
90 | union (S rs) (S ss) = rangeSet (rs ++ ss)
92 | appendNonEmpty : SnocList (RangeOf t) -> RangeOf t -> SnocList (RangeOf t)
93 | appendNonEmpty sr r = if isEmpty r then sr else sr :< r
96 | SnocList (RangeOf t)
100 | inters sr l@(x::xs) r@(y::ys) =
101 | let sr2 := appendNonEmpty sr (intersection x y)
102 | in case upperBound x < upperBound y of
103 | True => inters sr2 xs r
104 | False => inters sr2 l ys
105 | inters sr _ _ = sr <>> []
109 | intersection : SetOf t -> SetOf t -> SetOf t
110 | intersection (S rs) (S ss) = S (inters [<] rs ss)
114 | negation : SetOf t -> SetOf t
115 | negation (S rs) = S $
go [<] 0 rs
117 | go : SnocList (RangeOf t) -> t -> List (RangeOf t) -> List (RangeOf t)
118 | go sx m [] = sx <>> [range m maxBound]
119 | go sx m (x :: xs) =
123 | let l := lowerBound x
125 | sx2 := if l > m then sx :< range m (l-1) else sx
126 | in if u == maxBound then sx2 <>> [] else go sx2 (u+1) xs
130 | difference : SetOf t -> SetOf t -> SetOf t
131 | difference x y = intersection x (negation y)
134 | FromChar Set32 where
135 | fromChar = singleton . cast
140 | chars : String -> Set32
141 | chars = rangeSet . map (singleton . cast) . unpack
145 | fullSet : WithBounds t => SetOf t
146 | fullSet = range fullRange
150 | isFull : WithBounds t => SetOf t -> Bool
151 | isFull = (== fullSet)
159 | charRange : Char -> Char -> Set32
160 | charRange x y = range $
charRange x y
165 | lower = charRange 'a' 'z'
170 | upper = charRange 'A' 'Z'
175 | alpha = union lower upper
180 | digit = charRange '0' '9'
185 | posdigit = charRange '1' '9'
190 | alphaNum = union alpha digit
195 | control = charRange '\NUL' '\US' `union` charRange '\DEL' '\159'
202 | printable = negation control
207 | ascii = range $
range 0 127
211 | printableAscii : Set32
212 | printableAscii = intersection ascii printable
222 | unicode = difference (range codepoint) (range surrogate)