0 | module Protocol.SExp.Parser
  1 |
  2 | import Protocol.SExp
  3 |
  4 | import Parser.Lexer.Common
  5 | import Libraries.Text.Token
  6 | import Libraries.Text.Lexer.Tokenizer
  7 | import Libraries.Text.Parser
  8 | import Libraries.Text.PrettyPrint.Prettyprinter.Symbols
  9 | import Libraries.Text.PrettyPrint.Prettyprinter.Util
 10 | import Libraries.Text.PrettyPrint.Prettyprinter.Doc
 11 |
 12 | import Parser.Support.Escaping
 13 |
 14 | %default total
 15 |
 16 | {- To decouple parsing of S-expressions, we reproduce some
 17 |    functionality from the source-file parser. We duplicate it since we
 18 |    don't need the full blown functionality of the source-code token.
 19 | -}
 20 |
 21 | public export
 22 | data SExpToken
 23 |   = StringLit String
 24 |   | IntegerLit Integer
 25 |   | Symbol String
 26 |   | Ident String
 27 |   | StringBegin Nat
 28 |   | StringEnd
 29 |   | Whitespace
 30 |   | EndInput
 31 |
 32 | export
 33 | Show SExpToken where
 34 |   -- Literals
 35 |   show (IntegerLit x) = "literal " ++ show x
 36 |   -- String
 37 |   show (StringBegin hashtag) = "string begin"
 38 |   show StringEnd = "string end"
 39 |   show (StringLit x) = "string " ++ show x
 40 |   -- Identifiers
 41 |   show (Ident x) = "identifier " ++ x
 42 |   show (Symbol x) = "symbol " ++ x
 43 |   show Whitespace = " "
 44 |   show EndInput = "end of input"
 45 |
 46 | export
 47 | Pretty Void SExpToken where
 48 |   -- Literals
 49 |   pretty (IntegerLit x) = pretty "literal" <++> pretty (show x)
 50 |   -- String
 51 |   pretty (StringBegin hashtag) = reflow "string begin"
 52 |   pretty StringEnd = reflow "string end"
 53 |   pretty (StringLit x) = pretty "string" <++> dquotes (pretty x)
 54 |   -- Identifiers
 55 |   pretty (Ident x) = pretty "identifier" <++> pretty x
 56 |   pretty (Symbol x) = pretty "symbol" <++> pretty x
 57 |   -- Special
 58 |   pretty Whitespace = pretty "space"
 59 |   pretty EndInput = reflow "end of input"
 60 |
 61 | SExpRule : Type -> Type
 62 | SExpRule = Grammar () SExpToken True
 63 |
 64 | EmptySExpRule : Type -> Type
 65 | EmptySExpRule = Grammar () SExpToken False
 66 |
 67 | symbols : List String
 68 | symbols = ["(", ":", ")"]
 69 |
 70 | symbol : String -> SExpRule ()
 71 | symbol req
 72 |     = terminal ("Expected '" ++ req ++ "'") $
 73 |                \case
 74 |                  Symbol s => guard (s == req)
 75 |                  _ => Nothing
 76 |
 77 | space : SExpRule ()
 78 | space = terminal ("Expected a space") $
 79 |                \case
 80 |                  Whitespace => Just ()
 81 |                  _ => Nothing
 82 |
 83 | exactIdent : String -> SExpRule ()
 84 | exactIdent req
 85 |     = terminal ("Expected " ++ req) $
 86 |                \case
 87 |                  Ident s => guard (s == req)
 88 |                  _ => Nothing
 89 |
 90 | simpleStrLit : SExpRule String
 91 | simpleStrLit
 92 |     = terminal "Expected string literal" $
 93 |                \case
 94 |                  StringLit s => unescape 0 s
 95 |                  _ => Nothing
 96 |
 97 | strBegin : SExpRule Nat
 98 | strBegin = terminal "Expected string begin" $
 99 |                     \case
100 |                       StringBegin hashtag => Just hashtag
101 |                       _ => Nothing
102 |
103 | strEnd : SExpRule ()
104 | strEnd = terminal "Expected string end" $
105 |                   \case
106 |                     StringEnd => Just ()
107 |                     _ => Nothing
108 |
109 | simpleStr : SExpRule String
110 | simpleStr = strBegin *> commit *> (option "" simpleStrLit) <* strEnd
111 |
112 | stringTokens : Tokenizer SExpToken
113 | stringTokens
114 |     = match (someUntil (is '"') (escape (is '\\') any <|> any)) StringLit
115 |
116 | ideTokens : Tokenizer SExpToken
117 | ideTokens =
118 |       match (choice $ exact <$> symbols) Symbol
119 |   <|> match digits (IntegerLit . cast)
120 |   <|> compose (is '"')
121 |               (const $ StringBegin 0)
122 |               (const ())
123 |               (const stringTokens)
124 |               (const $ is '"')
125 |               (const StringEnd)
126 |   <|> match (some $ pred isSpace) (const Whitespace)
127 |   <|> match identAllowDashes Ident
128 |
129 | notWhitespace : WithBounds SExpToken -> Bool
130 | notWhitespace btok = case btok.val of
131 |   Whitespace => False
132 |   _ => True
133 |
134 | idelex : String ->
135 |   Either (StopReason, Int, Int, String)
136 |          (List (WithBounds SExpToken))
137 | idelex str = case lex ideTokens str of
138 |   -- Add the EndInput token so that we'll have a line and column
139 |   -- number to read when storing spans in the file
140 |   (tok, (EndInput, l, c, _)) => Right (filter notWhitespace tok ++
141 |                                       [MkBounded EndInput False (MkBounds l c l c)])
142 |   (_, fail) => Left fail
143 |
144 |
145 | identifierSExp : SExpRule String
146 | identifierSExp
147 |     = terminal "Expected name" $
148 |                \case
149 |                  Ident str => Just str
150 |                  _ => Nothing
151 |
152 | intLit : SExpRule Integer
153 | intLit
154 |     = terminal "Expected integer literal" $
155 |                \case
156 |                  IntegerLit i => Just i
157 |                  _ => Nothing
158 |
159 |
160 | eoi : EmptySExpRule ()
161 | eoi = ignore $ nextIs "Expected end of input" isEOI
162 |   where
163 |     isEOI : SExpToken -> Bool
164 |     isEOI EndInput = True
165 |     isEOI _ = False
166 |
167 | covering
168 | sexp : SExpRule SExp
169 | sexp
170 |     = do symbol ":"; exactIdent "True"
171 |          pure (BoolAtom True)
172 |   <|> do symbol ":"; exactIdent "False"
173 |          pure (BoolAtom False)
174 |   <|> do i <- intLit
175 |          pure (IntegerAtom i)
176 |   <|> do str <- simpleStr
177 |          pure (StringAtom str)
178 |   <|> do symbol ":"; x <- identifierSExp
179 |          pure (SymbolAtom x)
180 |   <|> do Parser.symbol "("
181 |          xs <- many sexp
182 |          symbol ")"
183 |          pure (SExpList xs)
184 |
185 | public export
186 | data SExpError =
187 |     LexError (StopReason, Int, Int, String)
188 |   | ParseErrors (List1 $ ParsingError SExpToken)
189 |
190 | ideParser : {e : _} ->
191 |             String -> Grammar () SExpToken e ty -> Either SExpError ty
192 | ideParser str p
193 |     = do toks   <- mapFst LexError $ idelex str
194 |          (_, _, (parsed, _)) <- mapFst ParseErrors $ parseWith p toks
195 |          Right parsed
196 |
197 | export
198 | covering
199 | parseSExp : String -> Either SExpError SExp
200 | parseSExp inp
201 |     = ideParser inp (do c <- sexp; eoi; pure c)
202 |