0 | module Parser.Lexer.Common
  1 |
  2 | import public Libraries.Text.Lexer
  3 |
  4 | %default total
  5 |
  6 | ||| In `comment` we are careful not to parse closing delimiters as
  7 | ||| valid comments. i.e. you may not write many dashes followed by
  8 | ||| a closing brace and call it a valid comment.
  9 | export
 10 | comment : Lexer
 11 | comment
 12 |    =  is '-' <+> is '-'                  -- comment opener
 13 |   <+> many (is '-') <+> reject (is '}')  -- not a closing delimiter
 14 |   <+> many (isNot '\n')                  -- till the end of line
 15 |
 16 | mutual
 17 |   ||| The mutually defined functions represent different states in a
 18 |   ||| small automaton.
 19 |   ||| `toEndComment` is the default state and it will munch through
 20 |   ||| the input until we detect a special character (a dash, an
 21 |   ||| opening brace, or a double quote) and then switch to the
 22 |   ||| appropriate state.
 23 |   toEndComment : (k : Nat) -> Recognise (k /= 0)
 24 |   toEndComment Z = empty
 25 |   toEndComment (S k)
 26 |                = some (pred (\c => c /= '-' && c /= '{' && c /= '"' && c /= '\''))
 27 |                         <+> (eof <|> toEndComment (S k))
 28 |              <|> is '{' <+> singleBrace k
 29 |              <|> is '-' <+> singleDash k
 30 |              <|> (charLit <|> pred (== '\'')) <+> toEndComment (S k)
 31 |              <|> stringLit <+> toEndComment (S k)
 32 |
 33 |   ||| After reading a single brace, we may either finish reading an
 34 |   ||| opening delimiter or ignore it (e.g. it could be an implicit
 35 |   ||| binder).
 36 |   singleBrace : (k : Nat) -> Lexer
 37 |   singleBrace k
 38 |      =  is '-' <+> many (is '-')              -- opening delimiter
 39 |                <+> (eof <|> singleDash (S k)) -- `singleDash` handles the {----} special case
 40 |                                               -- `eof` handles the file ending with {---
 41 |     <|> toEndComment (S k)                    -- not a valid comment
 42 |
 43 |   ||| After reading a single dash, we may either find another one,
 44 |   ||| meaning we may have started reading a line comment, or find
 45 |   ||| a closing brace meaning we have found a closing delimiter.
 46 |   singleDash : (k : Nat) -> Lexer
 47 |   singleDash k
 48 |      =  is '-' <+> doubleDash k    -- comment or closing delimiter
 49 |     <|> is '}' <+> toEndComment k  -- closing delimiter
 50 |     <|> toEndComment (S k)         -- not a valid comment
 51 |
 52 |   ||| After reading a double dash, we are potentially reading a line
 53 |   ||| comment unless the series of uninterrupted dashes is ended with
 54 |   ||| a closing brace in which case it is a closing delimiter.
 55 |   doubleDash : (k : Nat) -> Lexer
 56 |   doubleDash k = with Prelude.(::)
 57 |       many (is '-') <+> choice            -- absorb all dashes
 58 |         [ is '}' <+> toEndComment k                      -- closing delimiter
 59 |         , many (isNot '\n') <+> toEndComment (S k)       -- line comment
 60 |         ]
 61 |
 62 | export
 63 | blockComment : Lexer
 64 | blockComment = is '{' <+> is '-' <+> many (is '-') <+> (eof <|> toEndComment 1)
 65 |
 66 | -- Identifier Lexer
 67 | -- There are multiple variants.
 68 |
 69 | public export
 70 | data Flavour = AllowDashes | Capitalised | Normal
 71 |
 72 | isIdentStart : Flavour -> Char -> Bool
 73 | isIdentStart _           '_' = True
 74 | isIdentStart Capitalised  x  = isUpper x || x > chr 160
 75 | isIdentStart _            x  = isAlpha x || x > chr 160
 76 |
 77 | isIdentTrailing : Flavour -> Char -> Bool
 78 | isIdentTrailing AllowDashes '-'  = True
 79 | isIdentTrailing _           '\'' = True
 80 | isIdentTrailing _           '_'  = True
 81 | isIdentTrailing _            x   = isAlphaNum x || x > chr 160
 82 |
 83 | export %inline
 84 | isIdent : Flavour -> String -> Bool
 85 | isIdent flavour string =
 86 |   case unpack string of
 87 |     []      => False
 88 |     (x::xs) => isIdentStart flavour x && all (isIdentTrailing flavour) xs
 89 |
 90 | export %inline
 91 | ident : Flavour -> Lexer
 92 | ident flavour =
 93 |   (pred $ isIdentStart flavour) <+>
 94 |     (many . pred $ isIdentTrailing flavour)
 95 |
 96 | export
 97 | isIdentNormal : String -> Bool
 98 | isIdentNormal = isIdent Normal
 99 |
100 | export
101 | identNormal : Lexer
102 | identNormal = ident Normal
103 |
104 | export
105 | identAllowDashes : Lexer
106 | identAllowDashes = ident AllowDashes
107 |
108 | namespaceIdent : Lexer
109 | namespaceIdent = ident Capitalised <+> many (is '.' <+> ident Capitalised <+> expect (is '.'))
110 |
111 | export
112 | namespacedIdent : Lexer
113 | namespacedIdent = namespaceIdent <+> opt (is '.' <+> identNormal)
114 |
115 | export
116 | spacesOrNewlines : Lexer
117 | spacesOrNewlines = some (space <|> newline)
118 |