
   0 | module TyRE.StringRE
   1 | 
   2 | import public Data.Maybe
   3 | 
   4 | import public TyRE.Codes
   5 | import public TyRE.Core
   6 | import public TyRE.RE
   7 | import public TyRE.Text.Lexer
   8 | import public TyRE.Text.Parser
   9 | 
  10 | public export
  11 | data Token =
  12 |               OParQ -- [
  13 |             | CParQ -- ]
  14 |             | OPar -- (
  15 |             | CPar -- )
  16 |             | Dot -- .
  17 |             | BackTic -- `
  18 |             | Dash -- -
  19 |             | Star -- *
  20 |             | Plus -- +
  21 |             | QMark -- ?
  22 |             | Alt -- |
  23 |             | Exclamation
  24 |             | CharLit String
  25 |             | End -- end of input
  26 | 
  27 | ||| character literal:
  28 | |||   c -- for non special characters
  29 | |||   \c -- can be for both special and non special characters
  30 | public export
  31 | reCharLit : Lexer
  32 | reCharLit = (non $ some $ oneOf specialChars) <|> (is '\\' <+> any)
  33 | 
  34 | public export
  35 | reTokenMap : TokenMap Token
  36 | reTokenMap = [
  37 |               (is '[',    \x => OParQ),
  38 |               (is ']',    \x => CParQ),
  39 |               (is '(',    \x => OPar),
  40 |               (is ')',    \x => CPar),
  41 |               (is '.',    \x => Dot),
  42 |               (is '`',    \x => BackTic),
  43 |               (is '-',    \x => Dash),
  44 |               (is '*',    \x => Star),
  45 |               (is '+',    \x => Plus),
  46 |               (is '?',    \x => QMark),
  47 |               (is '|',    \x => Alt),
  48 |               (is '!',    \x => Exclamation),
  49 |               (reCharLit, \x => CharLit x)
  50 |               ]
  51 | 
  52 | public export
  53 | Rule : Type -> Type
  54 | Rule ty = Grammar (TokenData Token) True ty
  55 | 
  56 | ----- terminals -----
  57 | public export
  58 | openParQ : Rule ()
  59 | openParQ = terminal "[" (\case {(MkToken _ _  OParQ) => Just (); _ => Nothing})
  60 | 
  61 | public export
  62 | closedParQ : Rule ()
  63 | closedParQ = terminal "]" (\case {(MkToken _ _  CParQ) => Just (); _ => Nothing})
  64 | 
  65 | public export
  66 | openPar : Rule ()
  67 | openPar = terminal "(" (\case {(MkToken _ _  OPar) => Just (); _ => Nothing})
  68 | 
  69 | public export
  70 | closedPar : Rule ()
  71 | closedPar = terminal ")" (\case {(MkToken _ _  CPar) => Just (); _ => Nothing})
  72 | 
  73 | public export
  74 | backTic : Rule ()
  75 | backTic = terminal "`" (\case {(MkToken _ _  BackTic) => Just (); _ => Nothing})
  76 | 
  77 | public export
  78 | dash : Rule ()
  79 | dash = terminal "-" (\case {(MkToken _ _  Dash) => Just (); _ => Nothing})
  80 | 
  81 | public export
  82 | dot : Rule ()
  83 | dot = terminal "." (\case {(MkToken _ _  Dot) => Just (); _ => Nothing})
  84 | 
  85 | public export
  86 | star : Rule ()
  87 | star = terminal "*" (\case {(MkToken _ _  Star) => Just (); _ => Nothing})
  88 | 
  89 | public export
  90 | plus : Rule ()
  91 | plus = terminal "+" (\case {(MkToken _ _  Plus) => Just (); _ => Nothing})
  92 | 
  93 | public export
  94 | qMark : Rule ()
  95 | qMark = terminal "?" (\case {(MkToken _ _  QMark) => Just (); _ => Nothing})
  96 | 
  97 | public export
  98 | alt : Rule ()
  99 | alt = terminal "|" (\case {(MkToken _ _  Alt) => Just (); _ => Nothing})
 100 | 
 101 | public export
 102 | end : Rule ()
 103 | end = terminal "" (\case {(MkToken _ _  End) => Just (); _ => Nothing})
 104 | 
 105 | public export
 106 | exclamation : Rule ()
 107 | exclamation = terminal "!" (\case {(MkToken _ _  Exclamation) => Just (); _ => Nothing})
 108 | 
 109 | public export
 110 | getCharLit : (TokenData Token) -> Maybe Char
 111 | getCharLit (MkToken _ _ (CharLit str)) with (unpack str)
 112 |   getCharLit (MkToken _ _ (CharLit str)) | [] = Nothing --should not happen
 113 |   getCharLit (MkToken _ _ (CharLit str)) | (c :: []) = Just c
 114 |   getCharLit (MkToken _ _ (CharLit str)) | ('\\' :: (c :: [])) = Just c
 115 |   getCharLit (MkToken _ _ (CharLit str)) | ('\\' :: (c :: (c' :: cs))) = Nothing --should not happen
 116 |   getCharLit (MkToken _ _ (CharLit str)) | (c :: (c' :: cs)) = Nothing --should not happen
 117 | getCharLit _ = Nothing
 118 | 
 119 | public export
 120 | charLit : Rule Char
 121 | charLit = terminal "char" getCharLit
 122 | 
 123 | ----- grammar -----
 124 | public export
 125 | charLitsRep : Rule (List Char)
 126 | charLitsRep = (map (::) charLit <*> charLitsRep) <|> (map (\x => [x]) charLit)
 127 | 
 128 | public export
 129 | oneOf : Rule RE
 130 | oneOf = map OneOf $ openParQ *> charLitsRep <* closedParQ
 131 | 
 132 | public export
 133 | range : Rule RE
 134 | range = (map To ((openParQ *> charLit) <* dash) <*> charLit) <* closedParQ
 135 | 
 136 | public export
 137 | exactly : Rule RE
 138 | exactly = map Exactly charLit
 139 | 
 140 | public export
 141 | any : Rule RE
 142 | any = map (\_ => Any) dot
 143 | 
 144 | public export
 145 | mapRE : RE -> Maybe (RE -> RE) -> RE
 146 | mapRE re Nothing = re
 147 | mapRE re (Just f) = f re
 148 | 
 149 | mutual
 150 |   public export
 151 |   unit  : Rule RE
 152 |   unit  = exactly <|> any <|> oneOf <|> range -- single character patterns
 153 |         <|> (map Group $ backTic *> fullRE <* backTic) -- group
 154 |         <|> (openPar *> fullRE <* closedPar) -- with paranthesis
 155 | 
 156 |   public export
 157 |   postUnit  : Rule (RE -> RE)
 158 |   postUnit  = (map (\_ => Maybe) qMark) -- ...?
 159 |             <|> (map (\_ => Rep1) plus) -- ...+
 160 |             <|> (map (\_ => Rep0) star) -- ...*
 161 |             <|> (map (\_ => Keep) exclamation) -- ...!
 162 | 
 163 |   public export
 164 |   semiUnit : Rule RE
 165 |   semiUnit = map mapRE unit <*> optional (postUnit)
 166 | 
 167 |   public export
 168 |   postSemiUnit : Rule (RE -> RE)
 169 |   postSemiUnit =  (map (\y => \x => Alt x y) (alt *> semiUnit)) -- ...|A
 170 |               <|> (map (\y => \x => Concat x y) fullRE) -- ...ABC
 171 | 
 172 |   public export
 173 |   fullRE : Rule RE
 174 |   fullRE =  map mapRE semiUnit <*> optional (postSemiUnit)
 175 | 
 176 | public export
 177 | reWithEnd : Rule RE
 178 | reWithEnd = fullRE <* end
 179 | 
 180 | --- parsing ---
 181 | 
 182 | public export
 183 | mapTokens : (List (TokenData Token), (Int, Int, String))
 184 |           -> List (TokenData Token)
 185 | mapTokens (tokens, (f, l, _)) = tokens ++ [MkToken f l End]
 186 | 
 187 | public export
 188 | rAux : String -> Maybe RE
 189 | rAux str = case (parse reWithEnd (mapTokens (lex reTokenMap str))) of
 190 |                     Right (reg, _) => Just reg
 191 |                     Left _ => Nothing
 192 | 
 193 | public export
 194 | toRE : (str : String) -> {auto isJust : IsJust (rAux str)} -> RE
 195 | toRE str {isJust} = fromJust (rAux str) @{isJust}
 196 | 
 197 | public export
 198 | r : (str : String) -> {auto isJust : IsJust (rAux str)} -> TyRE (TypeRE $ toRE str {isJust})
 199 | r str {isJust} = compile (toRE str {isJust})