
   0 | module Text.ILex.RExp
   1 | 
   2 | import Data.Bool
   3 | import Data.ByteString
   4 | import Data.DPair
   5 | import Decidable.HDecEq
   6 | import public Text.ILex.Char.Set
   7 | import Derive.Prelude
   8 | 
   9 | %default total
  10 | %language ElabReflection
  11 | 
  12 | --------------------------------------------------------------------------------
  13 | -- Regular Expressions
  14 | --------------------------------------------------------------------------------
  15 | 
  16 | ||| A data type for regular expressions.
  17 | |||
  18 | ||| The `Bool` flag indicates, if the regular expression consumes
  19 | ||| at least one character of input or not.
  20 | public export
  21 | data RExpOf : Bool -> Type -> Type where
  22 |   Eps  : RExpOf False t
  23 |   Ch   : SetOf t -> RExpOf True t
  24 |   And  : RExpOf b1 t -> RExpOf b2 t -> RExpOf (b1 || b2) t
  25 |   Or   : RExpOf b1 t -> RExpOf b2 t -> RExpOf (b1 && b2) t
  26 |   Star : RExpOf True t -> RExpOf False t
  27 | 
  28 | %runElab derivePattern "RExpOf" [I,P] [Show]
  29 | 
  30 | public export
  31 | 0 RExp : Bool -> Type
  32 | RExp b = RExpOf b Bits32
  33 | 
  34 | public export
  35 | 0 RExp8 : Bool -> Type
  36 | RExp8 b = RExpOf b Bits8
  37 | 
  38 | public export
  39 | data IsCh : RExpOf b t -> Type where
  40 |   ItIsCh : IsCh (Ch s)
  41 | 
  42 | export
  43 | adjRanges : (SetOf t -> RExpOf True s) -> RExpOf b t -> RExpOf b s
  44 | adjRanges f Eps       = Eps
  45 | adjRanges f (Ch x)    = f x
  46 | adjRanges f (And x y) = And (adjRanges f x) (adjRanges f y)
  47 | adjRanges f (Or x y)  = Or (adjRanges f x) (adjRanges f y)
  48 | adjRanges f (Star x)  = Star (adjRanges f x)
  49 | 
  50 | --------------------------------------------------------------------------------
  51 | -- Token Maps
  52 | --------------------------------------------------------------------------------
  53 | 
  54 | public export
  55 | 0 TokenMap : Type -> Type
  56 | TokenMap a = List (RExp True, a)
  57 | 
  58 | public export
  59 | 0 TokenMap8 : Type -> Type
  60 | TokenMap8 a = List (RExp8 True, a)
  61 | 
  62 | --------------------------------------------------------------------------------
  63 | -- Utilities
  64 | --------------------------------------------------------------------------------
  65 | 
  66 | public export
  67 | orF : RExpOf (b || False) t -> RExpOf b t
  68 | orF x = replace {p = \b => RExpOf b t} (orFalseNeutral b) x
  69 | 
  70 | public export
  71 | orT : RExpOf (b || True) t -> RExpOf True t
  72 | orT x = replace {p = \b => RExpOf b t} (orTrueTrue b) x
  73 | 
  74 | public export
  75 | toOrF : RExpOf b t -> RExpOf (b || False) t
  76 | toOrF x = replace {p = \b => RExpOf b t} (sym $ orFalseNeutral b) x
  77 | 
  78 | --------------------------------------------------------------------------------
  79 | -- Combinators
  80 | --------------------------------------------------------------------------------
  81 | 
  82 | ||| Accepts the given single character
  83 | public export %inline
  84 | chr : Char -> RExp True
  85 | chr = Ch . fromChar
  86 | 
  87 | public export %inline
  88 | fromChar : Char -> RExp True
  89 | fromChar = chr
  90 | 
  91 | ||| Case insensitive version of `chr`.
  92 | public export
  93 | charLike : Char -> RExp True
  94 | charLike c =
  95 |   case isLower c of
  96 |     True  => Or (chr c) (chr $ toUpper c)
  97 |     False => case isUpper c of
  98 |       True  => Or (chr c) (chr $ toLower c)
  99 |       False => chr c
 100 | 
 101 | parameters {auto bnd : WithBounds t}
 102 |            {auto neg : Neg t}
 103 | 
 104 |   public export %inline
 105 |   not : (r : RExpOf b t) -> (0 p : IsCh r) => RExpOf True t
 106 |   not (Ch s) = Ch $ negation s
 107 | 
 108 |   public export %inline
 109 |   (&&) : (x,y : RExpOf b t) -> (0 p : IsCh x) => (0 q : IsCh y) => RExpOf True t
 110 |   (&&) (Ch s) (Ch t) = Ch (intersection s t)
 111 | 
 112 |   public export %inline
 113 |   (||) : (x,y : RExpOf b t) -> (0 p : IsCh x) => (0 q : IsCh y) => RExpOf  True t
 114 |   (||) (Ch s) (Ch t) = Ch (union s t)
 115 | 
 116 |   public export
 117 |   (<|>) : RExpOf b1 t -> RExpOf b2 t -> RExpOf (b1 && b2) t
 118 |   Ch x <|> Ch y = Ch (union x y)
 119 |   x <|> y       = Or x y
 120 | 
 121 |   public export
 122 |   oneof : (rs : List (RExpOf True t)) -> (0 p : NonEmpty rs) => RExpOf True t
 123 |   oneof [r]           = r
 124 |   oneof (r::t@(_::_)) = r <|> oneof t
 125 | 
 126 | public export %inline
 127 | (>>) : RExpOf b1 t -> RExpOf b2 t -> RExpOf (b1 || b2) t
 128 | (>>) = And
 129 | 
 130 | public export %inline
 131 | eps : RExpOf False t
 132 | eps = Eps
 133 | 
 134 | public export %inline
 135 | opt : RExpOf True t -> RExpOf False t
 136 | opt = (`Or` eps)
 137 | 
 138 | ||| Exactly matches the given sequence of characters
 139 | public export
 140 | chars : (cs : List Char) -> (0 p : NonEmpty cs) => RExp True
 141 | chars [c]            = chr c
 142 | chars (c::cs@(_::_)) = chr c >> chars cs
 143 | 
 144 | ||| Case-insensitive version of `chars`
 145 | public export
 146 | charsLike : (cs : List Char) -> (0 p : NonEmpty cs) => RExp True
 147 | charsLike [c]            = charLike c
 148 | charsLike (c::cs@(_::_)) = charLike c >> charsLike cs
 149 | 
 150 | ||| Exactly matches the given string.
 151 | public export
 152 | str : (s : String) -> (0 p : NonEmpty (unpack s)) => RExp True
 153 | str s = chars (unpack s)
 154 | 
 155 | ||| Utility for using string literals with regular expressions.
 156 | public export %inline
 157 | fromString : (s : String) -> (0 p : NonEmpty (unpack s)) => RExp True
 158 | fromString = str
 159 | 
 160 | ||| Case-insensitive version of `str`
 161 | public export
 162 | like : (s : String) -> (0 p : NonEmpty (unpack s)) => RExp True
 163 | like s = charsLike (unpack s)
 164 | 
 165 | public export
 166 | pre : (s : String) -> (0 p : NonEmpty (unpack s)) => RExp b -> RExp True
 167 | pre s r = str s >> r
 168 | 
 169 | public export %inline
 170 | star : RExpOf True t -> RExpOf False t
 171 | star = Star
 172 | 
 173 | public export %inline
 174 | plus : RExpOf True t -> RExpOf True t
 175 | plus x = x >> star x
 176 | 
 177 | public export
 178 | sep1 : (sep : RExpOf True t) -> RExpOf True t -> RExpOf True t
 179 | sep1 sep x = x >> star (sep >> x)
 180 | 
 181 | public export
 182 | sep : (sep : RExpOf True t) -> RExpOf True t -> RExpOf False t
 183 | sep s x = opt (sep1 s x)
 184 | 
 185 | --------------------------------------------------------------------------------
 186 | -- Repetitions
 187 | --------------------------------------------------------------------------------
 188 | 
 189 | public export
 190 | rep : Nat -> Bool
 191 | rep (S _) = True
 192 | rep _     = False
 193 | 
 194 | ||| Repeats the given expression exactly `n` times
 195 | export
 196 | repeat : (n : Nat) -> RExpOf True t -> RExpOf (rep n) t
 197 | repeat 0     x = Eps
 198 | repeat (S k) x = x >> repeat k x
 199 | 
 200 | ||| Repeats the given expression exactly at most `n` times
 201 | export %inline
 202 | atmost : (n : Nat) -> RExpOf True t -> RExpOf False t
 203 | atmost 0     x = eps
 204 | atmost (S k) x = opt (x >> atmost k x)
 205 | 
 206 | ||| Repeats the given expression between `m` and `n`  times
 207 | export
 208 | repeatRange : (m,n : Nat) -> RExpOf True t -> RExpOf (rep m) t
 209 | repeatRange m n x = orF $ repeat m x >> atmost (n `minus` m) x
 210 | 
 211 | ||| Repeats the given expression at least `n` times
 212 | export %inline
 213 | atleast : (n : Nat) -> RExpOf True t -> RExpOf (rep n) t
 214 | atleast n x = orF $ repeat n x >> star x
 215 | 
 216 | --------------------------------------------------------------------------------
 217 | -- Character Classes
 218 | --------------------------------------------------------------------------------
 219 | 
 220 | ||| Accepts only the newline character
 221 | public export %inline
 222 | nl : RExp True
 223 | nl = '\n'
 224 | 
 225 | ||| Accepts any character in the given range of unicode
 226 | ||| code points.
 227 | |||
 228 | ||| Please note that even if the given range exceeds the given
 229 | ||| set of valid codepoints (0x000 - 0xD7FF || 0xE000 - 0x10FFFF),
 230 | ||| it will be intersected with the valid set during generation
 231 | ||| of the state machine.
 232 | public export %inline
 233 | range32 : Bits32 -> Bits32 -> RExp True
 234 | range32 x y = Ch (range $ range x y)
 235 | 
 236 | ||| Accepts any character in the given range
 237 | public export %inline
 238 | range : Char -> Char -> RExp True
 239 | range x y = Ch (range $ charRange x y)
 240 | 
 241 | ||| Accepts any character in the given range
 242 | public export %inline
 243 | digit : RExp True
 244 | digit = Ch digit
 245 | 
 246 | public export
 247 | posdigit : RExp True
 248 | posdigit = Ch posdigit
 249 | 
 250 | ||| Accepts any upper case character
 251 | public export %inline
 252 | upper : RExp True
 253 | upper = Ch upper
 254 | 
 255 | ||| Accepts any lower case character
 256 | public export %inline
 257 | lower : RExp True
 258 | lower = Ch lower
 259 | 
 260 | ||| Accepts any alphabetic character
 261 | public export %inline
 262 | alpha : RExp True
 263 | alpha = Ch alpha
 264 | 
 265 | ||| Accepts any alpha-numeric character
 266 | public export %inline
 267 | alphaNum : RExp True
 268 | alphaNum = Ch alphaNum
 269 | 
 270 | ||| Accepts a binary digit ('0' or '1').
 271 | public export
 272 | bindigit : RExp True
 273 | bindigit = chr '0' <|> chr '1'
 274 | 
 275 | ||| Accepts an octal digit.
 276 | public export
 277 | octdigit : RExp True
 278 | octdigit = range '0' '7'
 279 | 
 280 | ||| Accepts a hexadecimal digit.
 281 | |||
 282 | ||| Letters can be upper or lower case.
 283 | public export
 284 | hexdigit : RExp True
 285 | hexdigit = range '0' '9' <|> range 'a' 'f' <|> range 'A' 'F'
 286 | 
 287 | ||| Accepts a single unicode control codepoint.
 288 | |||
 289 | ||| Control characters are unicode codepoints in the ranges
 290 | ||| 0x00 to 0x1f (`'\NUL'` to `'\US'`) and
 291 | ||| 0x71 to 0x9f (`'\DEL'` to `'\159'`).
 292 | |||
 293 | ||| Among these, the most commonly used are tab (`'\t'`, 0x09),
 294 | ||| line feed (`'\r'`, 0x0d) and carriage return (`'\n'`, 0x0a).
 295 | public export %inline
 296 | control : RExp True
 297 | control = Ch control
 298 | 
 299 | ||| Accepts a non-control unicode codepoint.
 300 | public export %inline
 301 | dot : RExp True
 302 | dot = Ch printable
 303 | 
 304 | ||| Accepts an arbitrary number of printable unicode codepoints.
 305 | public export %inline
 306 | dots : RExp False
 307 | dots = star dot
 308 | 
 309 | ||| Accepts a non-empty number of printable unicode codepoints.
 310 | public export %inline
 311 | dots1 : RExp True
 312 | dots1 = plus dot
 313 | 
 314 | --------------------------------------------------------------------------------
 315 | -- Integers
 316 | --------------------------------------------------------------------------------
 317 | 
 318 | ||| Recognizes a non-empty string of binary digits.
 319 | public export
 320 | binary : RExp True
 321 | binary = plus bindigit
 322 | 
 323 | ||| Recognizes a non-empty string of octal digits.
 324 | public export
 325 | octal : RExp True
 326 | octal = plus octdigit
 327 | 
 328 | ||| Recognizes a non-empty string of decimal digits.
 329 | |||
 330 | ||| In this case, no leading zeroes are allowed: "0" is recognized
 331 | ||| but "01" is not.
 332 | public export
 333 | decimal : RExp True
 334 | decimal = chr '0' <|> (posdigit >> star digit)
 335 | 
 336 | ||| Recognizes a non-empty string of hexadecimal digits.
 337 | |||
 338 | ||| Letters can be upper or lower case.
 339 | public export
 340 | hexadecimal : RExp True
 341 | hexadecimal = plus hexdigit
 342 | 
 343 | ||| Accepts a decimal number (like `decimal`: no leading zeroes)
 344 | ||| prefixed with an optional "minus" sign.
 345 | public export
 346 | integer : RExp True
 347 | integer = opt '-' >> decimal
 348 | 
 349 | ||| Accepts a natural number in binary, octal, decimal (no leading zeroes),
 350 | ||| or hexadecimal form.
 351 | |||
 352 | ||| Non-decimal forms must be prefixed with "0b" (binary), "0o" (octal), or
 353 | ||| "0x" (hexadecimal), just like in Idris.
 354 | public export
 355 | natural : RExp True
 356 | natural =
 357 |   (like "0b" >> binary)      <|>
 358 |   (like "0o" >> octal)       <|>
 359 |   (like "0x" >> hexadecimal) <|>
 360 |   decimal
 361 | 
 362 | --------------------------------------------------------------------------------
 363 | -- Constant Size Expressions
 364 | --------------------------------------------------------------------------------
 365 | 
 366 | ||| Proof that regular expression `x` consists of a constant number
 367 | ||| (`n`) of characters.
 368 | public export
 369 | data ConstSize : (n : Nat) -> (x : RExpOf b t) -> Type where
 370 |   [search x]
 371 |   ||| The epsilon expression trivially matches zero characters.
 372 |   CS0   : ConstSize 0 Eps
 373 | 
 374 |   ||| A single character trivially matches one character.
 375 |   CSC   : ConstSize 1 (Ch x)
 376 | 
 377 |   ||| Sequencing two constant size expressions of `m` and `n` characters
 378 |   ||| yields an expression matching `m+n` characters.
 379 |   CSAnd : ConstSize m x -> ConstSize n y -> ConstSize (m+n) (And x y)
 380 | 
 381 |   ||| A choice of constant size expressions all matching the same number of
 382 |   ||| characters yields again an expression matching the same number of
 383 |   ||| characters.
 384 |   CSOr  : ConstSize n x -> ConstSize n y -> ConstSize n (Or x y)
 385 | 
 386 | ||| Decides if the given expression matches a constant number of
 387 | ||| characters.
 388 | export
 389 | constSize : (x : RExpOf b t) -> Maybe (Subset Nat (`ConstSize` x))
 390 | constSize Eps       = Just (Element 0 CS0)
 391 | constSize (Ch x)    = Just (Element 1 CSC)
 392 | constSize (And x y) = do
 393 |   Element m p1 <- constSize x
 394 |   Element n p2 <- constSize y
 395 |   pure (Element (m+n) (CSAnd p1 p2))
 396 | constSize (Or x y)  = do
 397 |   Element m p1 <- constSize x
 398 |   Element n p2 <- constSize y
 399 |   case hdecEq m n of
 400 |     Just0 prf => pure (Element m (CSOr p1 (rewrite prf in p2)))
 401 |     Nothing0  => Nothing
 402 | constSize (Star x)  = Nothing
 403 | 
 404 | ||| Proof that the `chars cs` combinator returns an expression
 405 | ||| that matches a constant number of `length cs` characters.
 406 | export
 407 | 0 charsConstSize :
 408 |      (cs : List Char)
 409 |   -> {auto 0 prf : NonEmpty cs}
 410 |   -> ConstSize (length cs) (chars cs)
 411 | charsConstSize [c]              = CSC
 412 | charsConstSize (c :: cs@(_::_)) = CSAnd CSC (charsConstSize cs)
 413 |