
   0 | module Text.Regex.Interface
   1 | 
   2 | import public Data.Alternative
   3 | import Data.List
   4 | import public Data.List.Quantifiers
   5 | import public Data.List1
   6 | import public Data.Vect
   7 | 
   8 | import Deriving.Show
   9 | 
  10 | %default total
  11 | %language ElabReflection
  12 | 
  13 | ----------------------
  14 | --- Regex building ---
  15 | ----------------------
  16 | 
  17 | public export
  18 | data EdgeSide = Start | End
  19 | ||| `Line` line mode means "depends on the matching mode", `Text` means "literally, independent on matching mode".
  20 | public export
  21 | data LineMode = Line | Text
  22 | 
  23 | export %hint ShowEdgeSide : Show EdgeSide; ShowEdgeSide = %runElab derive
  24 | export %hint ShowLineMode : Show LineMode; ShowLineMode = %runElab derive
  25 | 
  26 | public export
  27 | interface Alternative rx => Regex rx where
  28 |   ||| Matches a symbol if the given function returns `Just`, and returns the contents of this `Just`.
  29 |   sym' : (Char -> Maybe a) -> rx a
  30 |   ||| Matches a symbol satisfying the given predicate, and returns the matched char, or fails.
  31 |   sym : (Char -> Bool) -> rx Char
  32 |   sym f = sym' $ \c => whenT (f c) c
  33 |   ||| Matches the given symbol and returns it, or fails.
  34 |   char : Char -> rx Char
  35 |   char = sym . (==)
  36 | 
  37 |   ||| Matches any single char in line (i.e. without newlines depending on the mode) or in text (i.e. literally any character).
  38 |   anyChar : LineMode -> rx Char
  39 | 
  40 |   ||| Matches the start/end of the line/text.
  41 |   edge : LineMode -> EdgeSide -> rx ()
  42 | 
  43 |   ||| Zero-width boundary between a word-class char and a non-word class char or an edge.
  44 |   |||
  45 |   ||| For left or right boundary, set corresponding bool parameter to `True`,
  46 |   ||| for any set both to `True`, for non-boundary set both to `False`.
  47 |   wordBoundary : (left : Bool) -> (right : Bool) -> rx ()
  48 | 
  49 |   ||| Matches the given string.
  50 |   string : String -> rx String
  51 |   string = map pack . sequence . map char . unpack
  52 | 
  53 |   ||| Regex having an original matched string along with the original value.
  54 |   withMatch : rx a -> rx (String, a)
  55 |   ||| Regex having only the original matched string as a contained resulting value.
  56 |   matchOf : rx a -> rx String
  57 |   matchOf = map fst . withMatch
  58 | 
  59 |   ||| Matches all of given sub-regexes, sequentially.
  60 |   all : All rx tys -> rx $ HList tys
  61 |   all = pushOut
  62 | 
  63 |   ||| Matches is there exists at least one sub-regex that matches.
  64 |   exists : All rx tys -> rx $ Any Prelude.id tys
  65 |   exists = altAll
  66 | 
  67 |   ||| Optional application of a given regex.
  68 |   opt : rx a -> rx $ Maybe a
  69 |   opt = optional
  70 | 
  71 |   rep1 : rx a -> rx $ List1 a
  72 |   rep1 r = [| r ::: rep r |]
  73 |   rep : rx a -> rx $ List a
  74 |   rep r = toList <$> rep1 r <|> pure []
  75 | 
  76 |   repeatN : (n : Nat) -> rx a -> rx $ Vect n a
  77 |   repeatN n = sequence . replicate n
  78 | 
  79 |   repeatNOrMore : (n : Nat) -> rx a -> rx $ List a
  80 |   repeatNOrMore n r = [| map toList (repeatN n r) ++ rep r |]
  81 | 
  82 |   repeatNOrLess : (n : Nat) -> rx a -> rx $ List a
  83 |   repeatNOrLess Z     _ = pure []
  84 |   repeatNOrLess (S n) r = [| r :: repeatNOrLess n r |] <|> pure []
  85 | 
  86 |   repeatNM : (n, m : Nat) -> (0 nm : n `LTE` m) => rx a -> rx $ List a
  87 |   repeatNM n m r = [| map toList (repeatN n r) ++ repeatNOrLess (m `minus` n) r |]
  88 | 
  89 | --- Special general cases ---
  90 | 
  91 | ||| Always matches without consuming any symbol.
  92 | public export %inline
  93 | omega : Regex rx => rx ()
  94 | omega = pure ()
  95 | 
  96 | export infixr 7 `thenGoes`
  97 | ||| Simple consequent composition
  98 | public export %inline
  99 | thenGoes : Regex rx => rx a -> rx b -> rx (a, b)
 100 | thenGoes x y = [| (x, y) |]
 101 | 
 102 | --- Special chars ---
 103 | 
 104 | public export %inline
 105 | anyOf : Regex rx => List Char -> rx Char
 106 | anyOf cs = sym (`elem` cs)
 107 | 
 108 | public export %inline
 109 | noneOf : Regex rx => List Char -> rx Char
 110 | noneOf cs = sym $ not . (`elem` cs)
 111 | 
 112 | public export %inline
 113 | between : Regex rx => Char -> Char -> rx Char
 114 | between l r = sym $ \k => l <= k && k <= r
 115 | 
 116 | ||| Either "\r\n" or any of '\n', '\r' or '\v'
 117 | public export
 118 | genericNL : Regex rx => rx String
 119 | genericNL = string "\x0d\x0a" <|> map singleton (anyOf ['\n', '\r', '\v'])
 120 | 
 121 | public export
 122 | data CharClass
 123 |   = Alpha | Digit | XDigit | Alnum | Upper | Lower | Word
 124 |   | Cntrl | Space | Blank | Graph | Print | Ascii | Punct
 125 | 
 126 | public export %tcinline
 127 | charClass : CharClass -> Char -> Bool
 128 | charClass Alpha    = isAlpha
 129 | charClass Digit    = isDigit
 130 | charClass XDigit   = isHexDigit
 131 | charClass Alnum    = isAlphaNum
 132 | charClass Upper    = isUpper
 133 | charClass Lower    = isLower
 134 | charClass Word     = \c => isAlphaNum c || c == '_'
 135 | charClass Cntrl    = isControl
 136 | charClass Space    = isSpace
 137 | charClass Blank    = \c => c == ' ' || c == '\t'
 138 | charClass Graph    = \c => chr 0x21 <= c && c <= chr 0x7E
 139 | charClass Print    = \c => c == ' ' || charClass Graph c
 140 | charClass Ascii    = \c => chr 0x00 <= c && c <= chr 0x7F
 141 | charClass Punct    = \c => charClass Graph c && not (isSpace c) && not (isAlphaNum c)
 142 | 
 143 | --- Special combinations ---
 144 | 
 145 | public export
 146 | parseDigit : (base : Nat) -> (0 _ : So (2 <= base && base <= 36)) => Char -> Maybe $ Fin base
 147 | parseDigit base@(S _) c = do
 148 |   let tofin = \n => fromMaybe FZ {- must never happen -} $ integerToFin (cast n) base
 149 |   let ord0 = ord '0'
 150 |   let ordA = ord 'a'
 151 |   let c = if isUpper c then chr (ord c - ord 'A' + ordA) else c
 152 |   let pred = if base <= 10
 153 |                then let upDig = chr $ ord0 + cast base              in '0' <= c && c <= upDig
 154 |                else let upLet = chr $ ordA + cast (base `minus` 10) in '0' <= c && c <= '9' || 'a' <= c && c <= upLet
 155 |   whenT pred $ tofin $ if c <= '9' then ord c - ord0 else ord c - ordA + 10
 156 | 
 157 | ||| A digit of given base
 158 | public export
 159 | digit' : Regex rx => (base : Nat) -> (0 _ : So (2 <= base && base <= 36)) => rx $ Fin base
 160 | digit' base = sym' $ parseDigit base
 161 | 
 162 | ||| A 10-base digit
 163 | public export %inline
 164 | digit : Regex rx => rx $ Fin 10
 165 | digit = digit' 10
 166 | 
 167 | ||| A natural number regex without any sign
 168 | public export
 169 | naturalNumber' : Regex rx => (base : Nat) ->  (0 _ : So (2 <= base && base <= 36)) => rx Nat
 170 | naturalNumber' base = rep1 (digit' base) <&> \(h:::tl) => go (cast h) tl where
 171 |   go : Nat -> List (Fin base) -> Nat
 172 |   go acc []      = acc
 173 |   go acc (x::xs) = go (acc * base + cast x) xs
 174 | 
 175 | public export %inline
 176 | naturalNumber : Regex rx => rx Nat
 177 | naturalNumber = naturalNumber' 10
 178 |