0 | module Text.Lexer.Tokenizer
  1 |
  2 | import Data.List
  3 |
  4 | import Text.Lexer.Core
  5 | import Text.Lexer
  6 | import Text.PrettyPrint.Prettyprinter
  7 |
  8 | import public Control.Delayed
  9 | import public Text.Bounded
 10 |
 11 | %default total
 12 |
 13 | ||| Description of a language's tokenization rule.
 14 | export
 15 | data Tokenizer : (tokenType : Type) -> Type where
 16 |      Match : Lexer -> (String -> tokenType) -> Tokenizer tokenType
 17 |      Compose : (begin : Lexer) ->
 18 |                (mapBegin : String -> tokenType) ->
 19 |                (tagger : String -> tag) ->
 20 |                (middle : Inf (tag -> Tokenizer tokenType)) ->
 21 |                (end : tag -> Lexer) ->
 22 |                (mapEnd : String -> tokenType) ->
 23 |                Tokenizer tokenType
 24 |      Alt : Tokenizer tokenType -> Lazy (Tokenizer tokenType) -> Tokenizer tokenType
 25 |
 26 | export
 27 | Functor Tokenizer where
 28 |   map f (Match lex fn) = Match lex (f . fn)
 29 |   map f (Compose {begin, mapBegin, tagger, middle, end, mapEnd})
 30 |     = Compose {
 31 |         mapBegin = f . mapBegin,
 32 |         middle   = map f . middle,
 33 |         mapEnd   = f . mapEnd,
 34 |         begin, tagger, end
 35 |       }
 36 |   map f (Alt t1 t2) = map f t1 `Alt` map f t2
 37 |
 38 | ||| Alternative tokenizer rules.
 39 | export
 40 | (<|>) : Tokenizer t -> Lazy (Tokenizer t) -> Tokenizer t
 41 | (<|>) = Alt
 42 |
 43 | ||| Match on a recogniser and cast the string to a token.
 44 | export
 45 | match : Lexer -> (String -> a) -> Tokenizer a
 46 | match = Match
 47 |
 48 | ||| Compose other tokenizer. Language composition should be quoted between
 49 | ||| a begin lexer and a end lexer. The begin token can be used to generate
 50 | ||| the composition tokenizer and the end lexer.
 51 | export
 52 | compose : (begin : Lexer) ->
 53 |           (mapBegin : String -> a) ->
 54 |           (tagger : String -> tag) ->
 55 |           (middle : Inf (tag -> Tokenizer a)) ->
 56 |           (end : tag -> Lexer) ->
 57 |           (mapEnd : String -> a) ->
 58 |           Tokenizer a
 59 | compose = Compose
 60 |
 61 | ||| Stop reason why tokenizer can't make more progress.
 62 | ||| @ ComposeNotClosing carries the span of composition begin token in the
 63 | |||                     form of `(startLine, startCol), (endLine, endCol)`.
 64 | public export
 65 | data StopReason = EndInput | NoRuleApply | ComposeNotClosing (Int, Int) (Int, Int)
 66 |
 67 | export
 68 | Show StopReason where
 69 |   show EndInput = "EndInput"
 70 |   show NoRuleApply = "NoRuleApply"
 71 |   show (ComposeNotClosing start end) = "ComposeNotClosing " ++ show start ++ " " ++ show end
 72 |
 73 | export
 74 | Pretty StopReason where
 75 |   pretty EndInput = pretty "EndInput"
 76 |   pretty NoRuleApply = pretty "NoRuleApply"
 77 |   pretty (ComposeNotClosing start end) = "ComposeNotClosing" <++> pretty start <++> pretty end
 78 |
 79 | tokenise : Lexer ->
 80 |            Tokenizer a ->
 81 |            (line, col : Int) -> List (WithBounds a) ->
 82 |            List Char ->
 83 |            (List (WithBounds a), (StopReason, Int, Int, List Char))
 84 | tokenise reject tokenizer line col acc [] = (reverse acc, EndInput, (line, col, []))
 85 | tokenise reject tokenizer line col acc str
 86 |     = case scan reject [] str of
 87 |            Just _ => (reverse acc, (EndInput, line, col, str))
 88 |            Nothing => case getFirstMatch tokenizer str of
 89 |                            Right (toks, line', col', rest) =>
 90 |                                -- assert total because getFirstMatch must consume something
 91 |                                assert_total (tokenise reject tokenizer line' col' (toks ++ acc) rest)
 92 |                            Left reason => (reverse acc, reason, (line, col, str))
 93 |   where
 94 |     countNLs : List Char -> Nat
 95 |     countNLs str = List.length (filter (== '\n') str)
 96 |
 97 |     getCols : List Char -> Int -> Int
 98 |     getCols x c
 99 |         = case span (/= '\n') x of
100 |                (incol, []) => c + cast (length incol)
101 |                (incol, _) => cast (length incol)
102 |
103 |     -- get the next lexeme using the `Lexer` in argument, its position and the input
104 |     -- Returns the new position, the lexeme parsed and the rest of the input
105 |     -- If parsing the lexer fails, this returns `Nothing`
106 |     getNext : (lexer : Lexer) ->  (line, col : Int) -> (input : List Char) -> Maybe (String, Int, Int, List Char)
107 |     getNext lexer line col str =
108 |       let Just (token, rest) = scan lexer [] str
109 |             | _ => Nothing
110 |           line' = line + cast (countNLs token)
111 |           col' = getCols token col
112 |           tokenStr = pack $ reverse token
113 |        in pure (tokenStr, line', col', rest)
114 |
115 |     getFirstMatch : Tokenizer a -> List Char ->
116 |                     Either StopReason (List (WithBounds a), Int, Int, List Char)
117 |     getFirstMatch (Match lex fn) str
118 |         = let Just (tok, line', col', rest) = getNext lex line col str
119 |                 | _ => Left NoRuleApply
120 |               tok' = MkBounded (fn tok) False (MkBounds line col line' col')
121 |            in Right ([tok'], line', col', rest)
122 |     getFirstMatch (Compose begin mapBegin tagger middleFn endFn mapEnd) str
123 |         = let Just (beginTok', line', col' , rest) = getNext begin line col str
124 |                 | Nothing => Left NoRuleApply
125 |               tag = tagger beginTok'
126 |               middle = middleFn tag
127 |               end = endFn tag
128 |               beginTok'' = MkBounded (mapBegin beginTok') False (MkBounds line col line' col')
129 |               (midToks, (reason, line'', col'', rest'')) =
130 |                     assert_total (tokenise end middle line' col' [] rest)
131 |            in case reason of
132 |                    (ComposeNotClosing _ _) => Left reason
133 |                    _ => let Just (endTok', lineEnd, colEnd, restEnd) =
134 |                                 getNext end line'' col'' rest''
135 |                               | _ => Left $ ComposeNotClosing (line, col) (line', col')
136 |                             endTok'' = MkBounded (mapEnd endTok') False (MkBounds line'' col'' lineEnd colEnd)
137 |                          in Right ([endTok''] ++ reverse midToks ++ [beginTok''], lineEnd, colEnd, restEnd)
138 |     getFirstMatch (Alt t1 t2) str
139 |         = case getFirstMatch t1 str of
140 |                Right result => Right result
141 |                Left reason@(ComposeNotClosing _ _) => Left reason
142 |                Left _ => getFirstMatch t2 str
143 |
144 | export
145 | lexTo : Lexer ->
146 |         Tokenizer a ->
147 |         String ->
148 |         (List (WithBounds a), (StopReason, Int, Int, String))
149 | lexTo reject tokenizer str
150 |     = let (ts, reason, (l, c, str')) =
151 |               tokenise reject tokenizer 0 0 [] (unpack str) in
152 |           (ts, reason, (l, c, pack str'))
153 |
154 | ||| Given a tokenizer and an input string, return a list of recognised tokens,
155 | ||| and the line, column, and remainder of the input at the first point in the string
156 | ||| where there are no recognised tokens.
157 | export
158 | lex : Tokenizer a -> String -> (List (WithBounds a), (StopReason, Int, Int, String))
159 | lex tokenizer str = lexTo (pred $ const False) tokenizer str
160 |