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