0 | module Idrall.ParserNew
  1 |
  2 | import Data.List
  3 | import Data.List1
  4 | import Data.String -- needed for pretty?
  5 | import Data.SortedMap
  6 |
  7 | import Text.Parser
  8 | import Text.Quantity
  9 | import Text.Token
 10 | import Text.Lexer
 11 | import Text.Bounded
 12 |
 13 | import Idrall.Parser.Lexer
 14 | import Idrall.Parser.Rule
 15 | import Idrall.FC
 16 | import Idrall.Expr
 17 | import Idrall.Path
 18 | import Idrall.Pretty
 19 |
 20 | import Debug.Trace
 21 |
 22 | %hide Prelude.(<|>)
 23 |
 24 | public export
 25 | RawExpr : Type
 26 | RawExpr = Expr ImportStatement
 27 |
 28 | both : (a -> b) -> (a, a) -> (b, b)
 29 | both f x = (f (fst x), f (snd x))
 30 |
 31 | boundToFC : OriginDesc -> WithBounds t -> FC
 32 | boundToFC mbModIdent b = MkFC mbModIdent (both cast $ start b) (both cast $ end b)
 33 |
 34 | boundToFC2 : OriginDesc -> WithBounds t -> WithBounds u -> FC
 35 | boundToFC2 mbModIdent s e = MkFC mbModIdent (both cast $ start s) (both cast $ end e)
 36 |
 37 | initBounds : OriginDesc
 38 | initBounds = Nothing
 39 |
 40 | mergeBounds : FC -> FC -> FC
 41 | mergeBounds (MkFC x start _) (MkFC y _ end) = (MkFC x start end)
 42 | mergeBounds (MkFC x start _) (MkVirtualFC y _ end) = (MkFC x start end)
 43 | mergeBounds f@(MkFC x start end) EmptyFC = f
 44 | mergeBounds (MkVirtualFC x start _) (MkFC y _ end) = (MkFC y start end)
 45 | mergeBounds (MkVirtualFC x start _) (MkVirtualFC y _ end) = (MkVirtualFC x start end)
 46 | mergeBounds f@(MkVirtualFC x start end) EmptyFC = f
 47 | mergeBounds EmptyFC f@(MkFC x start end) = f
 48 | mergeBounds EmptyFC f@(MkVirtualFC x start end) = f
 49 | mergeBounds EmptyFC EmptyFC = EmptyFC
 50 |
 51 | mkExprFC : OriginDesc -> WithBounds x -> (FC -> x -> Expr a) -> Expr a
 52 | mkExprFC od e mkE = mkE (boundToFC od e) (val e)
 53 |
 54 | mkExprFC0 : OriginDesc -> WithBounds x -> (FC -> Expr a) -> Expr a
 55 | mkExprFC0 od e mkE = mkE (boundToFC od e)
 56 |
 57 | updateBounds : FC -> Expr a -> Expr a
 58 | updateBounds fc (EConst _ z) = EConst fc z
 59 | updateBounds fc (EVar _ z n) = EVar fc z n
 60 | updateBounds fc (ELam _ z w v) = ELam fc z w v
 61 | updateBounds fc (EApp _ z w) = EApp fc z w
 62 | updateBounds fc (EPi _ n z w) = EPi fc n z w
 63 | updateBounds fc (ELet _ z t w v) = ELet fc z t w v
 64 | updateBounds fc (EAnnot _ z w) = EAnnot fc z w
 65 | updateBounds fc (EBool _) = EBool fc
 66 | updateBounds fc (EBoolLit _ z) = EBoolLit fc z
 67 | updateBounds fc (EBoolAnd _ z w) = EBoolAnd fc z w
 68 | updateBounds fc (EBoolOr _ z w) = EBoolOr fc z w
 69 | updateBounds fc (EBoolEQ _ z w) = EBoolEQ fc z w
 70 | updateBounds fc (EBoolNE _ z w) = EBoolNE fc z w
 71 | updateBounds fc (EBoolIf _ z w v) = EBoolIf fc z w v
 72 | updateBounds fc (ENatural _) = ENatural fc
 73 | updateBounds fc (ENaturalLit _ x) = ENaturalLit fc x
 74 | updateBounds fc (ENaturalBuild _) = ENaturalBuild fc
 75 | updateBounds fc (ENaturalFold _) = ENaturalFold fc
 76 | updateBounds fc (ENaturalIsZero _) = ENaturalIsZero fc
 77 | updateBounds fc (ENaturalEven _) = ENaturalEven fc
 78 | updateBounds fc (ENaturalOdd _) = ENaturalOdd fc
 79 | updateBounds fc (ENaturalSubtract _) = ENaturalSubtract fc
 80 | updateBounds fc (ENaturalToInteger _) = ENaturalToInteger fc
 81 | updateBounds fc (ENaturalShow _) = ENaturalShow fc
 82 | updateBounds fc (ENaturalPlus _ z w) = ENaturalPlus fc z w
 83 | updateBounds fc (ENaturalTimes _ z w) = ENaturalTimes fc z w
 84 | updateBounds fc (EInteger _) = EInteger fc
 85 | updateBounds fc (EIntegerLit _ x) = EIntegerLit fc x
 86 | updateBounds fc (EIntegerShow _) = EIntegerShow fc
 87 | updateBounds fc (EIntegerNegate _) = EIntegerNegate fc
 88 | updateBounds fc (EIntegerClamp _) = EIntegerClamp fc
 89 | updateBounds fc (EIntegerToDouble _) = EIntegerToDouble fc
 90 | updateBounds fc (EDouble _) = EDouble fc
 91 | updateBounds fc (EDoubleShow _) = EDoubleShow fc
 92 | updateBounds fc (EDoubleLit _ z) = EDoubleLit fc z
 93 | updateBounds fc (EList _) = EList fc
 94 | updateBounds fc (EListLit _ t z) = EListLit fc t z
 95 | updateBounds fc (EListAppend _ z w) = EListAppend fc z w
 96 | updateBounds fc (EListBuild _) = EListBuild fc
 97 | updateBounds fc (EListFold _) = EListFold fc
 98 | updateBounds fc (EListLength _) = EListLength fc
 99 | updateBounds fc (EListHead _) = EListHead fc
100 | updateBounds fc (EListLast _) = EListLast fc
101 | updateBounds fc (EListIndexed _) = EListIndexed fc
102 | updateBounds fc (EListReverse _) = EListReverse fc
103 | updateBounds fc (EText _) = EText fc
104 | updateBounds fc (ETextLit _ z) = ETextLit fc z
105 | updateBounds fc (ETextAppend _ z w) = ETextAppend fc z w
106 | updateBounds fc (ETextShow _) = ETextShow fc
107 | updateBounds fc (ETextReplace _) = ETextReplace fc
108 | updateBounds fc (EOptional _) = EOptional fc
109 | updateBounds fc (ESome _ x) = ESome fc x
110 | updateBounds fc (ENone _) = ENone fc
111 | updateBounds fc (EField _ z s) = EField fc z s
112 | updateBounds fc (EWith _ z s y) = EWith fc z s y
113 | updateBounds fc (EEquivalent _ z w) = EEquivalent fc z w
114 | updateBounds fc (EAssert _ z) = EAssert fc z
115 | updateBounds fc (ERecord _ z) = ERecord fc z
116 | updateBounds fc (ERecordLit _ z) = ERecordLit fc z
117 | updateBounds fc (EUnion _ z) = EUnion fc z
118 | updateBounds fc (ECombine _ x y) = ECombine fc x y
119 | updateBounds fc (ECombineTypes _ x y) = ECombineTypes fc x y
120 | updateBounds fc (EPrefer _ x y) = EPrefer fc x y
121 | updateBounds fc (ERecordCompletion _ x y) = ERecordCompletion fc x y
122 | updateBounds fc (EMerge _ x y z) = EMerge fc x y z
123 | updateBounds fc (EToMap _ x y) = EToMap fc x y
124 | updateBounds fc (EProject _ x y) = EProject fc x y
125 | updateBounds fc (EImportAlt _ x y) = EImportAlt fc x y
126 | updateBounds fc (EEmbed _ z) = EEmbed fc z
127 |
128 | Rule : Type -> Type -> Type
129 | Rule state ty = Grammar state RawToken True ty
130 |
131 | EmptyRule : Type -> Type -> Type
132 | EmptyRule state ty = Grammar state RawToken False ty
133 |
134 | chainr1 : Grammar state t True (a)
135 |        -> Grammar state t True (a -> a -> a)
136 |        -> Grammar state t True (a)
137 | chainr1 p op = p >>= rest
138 | where
139 |   rest : a -> Grammar state t False (a)
140 |   rest a1 = (do f <- op
141 |                 a2 <- p >>= rest
142 |                 rest (f a1 a2)) <|> pure a1
143 |
144 | ||| Parse first expression, then attempt to parse
145 | ||| an operation and a second argument to that operation
146 | ||| and apply the operation to the first expression and the
147 | ||| newly parsed argument. If the operation or argument fail
148 | ||| to parse, produce the first expression successfully.
149 | |||
150 | ||| In short, parse an expression and optionally parse and apply
151 | ||| an operation following it.
152 | hchainl : Grammar state t True (a)
153 |         -> Grammar state t True (a -> b -> a)
154 |         -> Grammar state t True (b)
155 |         -> Grammar state t True (a)
156 | hchainl pini pop parg = pini >>= go
157 |   where
158 |   covering
159 |   go : a -> Grammar state t False (a)
160 |   go x = (do op <- pop
161 |              arg <- parg
162 |              go $ op x arg) <|> pure x
163 |
164 | chainl1 : Grammar state t True (a)
165 |        -> Grammar state t True (a -> a -> a)
166 |        -> Grammar state t True (a)
167 | chainl1 p op = do
168 |   x <- p
169 |   rest x
170 | where
171 |   rest : a -> Grammar state t False (a)
172 |   rest a1 = (do
173 |     f <- op
174 |     a2 <- p
175 |     rest (f a1 a2)) <|> pure a1
176 |
177 | infixOp : Grammar state t True ()
178 |         -> (a -> a -> a)
179 |         -> Grammar state t True (a -> a -> a)
180 | infixOp l ctor = do
181 |   l
182 |   Text.Parser.Core.pure ctor
183 |
184 | boundedOp : (FC -> Expr a -> Expr a -> Expr a)
185 |           -> Expr a
186 |           -> Expr a
187 |           -> Expr a
188 | boundedOp op x y =
189 |   let xB = getFC x
190 |       yB = getFC y
191 |       mB = mergeBounds xB yB in
192 |       op mB x y
193 |
194 | builtinTerm : OriginDesc -> WithBounds String -> Grammar state (TokenRawToken) False (RawExpr)
195 | builtinTerm od str =
196 |   case val str of
197 |      "Natural/build" => pure $ cons ENaturalBuild
198 |      "Natural/fold" => pure $ cons ENaturalFold
199 |      "Natural/isZero" => pure $ cons ENaturalIsZero
200 |      "Natural/even" => pure $ cons ENaturalEven
201 |      "Natural/odd" => pure $ cons ENaturalOdd
202 |      "Natural/subtract" => pure $ cons ENaturalSubtract
203 |      "Natural/toInteger" => pure $ cons ENaturalToInteger
204 |      "Natural/show" => pure $ cons ENaturalShow
205 |      "Integer/show" => pure $ cons EIntegerShow
206 |      "Integer/negate" => pure $ cons EIntegerNegate
207 |      "Integer/clamp" => pure $ cons EIntegerClamp
208 |      "Integer/toDouble" => pure $ cons EIntegerToDouble
209 |      "Double/show" => pure $ cons EDoubleShow
210 |      "List/build" => pure $ cons EListBuild
211 |      "List/fold" => pure $ cons EListFold
212 |      "List/length" => pure $ cons EListLength
213 |      "List/head" => pure $ cons EListHead
214 |      "List/last" => pure $ cons EListLast
215 |      "List/indexed" => pure $ cons EListIndexed
216 |      "List/reverse" => pure $ cons EListReverse
217 |      "List" => pure $ cons EList
218 |      "Text/show" => pure $ cons ETextShow
219 |      "Text/replace" => pure $ cons ETextReplace
220 |      "Optional" => pure $ cons EOptional
221 |      "None" => pure $ cons ENone
222 |      "NaN" => pure $ EDoubleLit (boundToFC od str) (0.0/0.0)
223 |      "True" => pure $ EBoolLit (boundToFC od str) True
224 |      "False" => pure $ EBoolLit (boundToFC od str) False
225 |      "Bool" => pure $ EBool (boundToFC od str)
226 |      "Text" => pure $ EText (boundToFC od str)
227 |      "Natural" => pure $ ENatural (boundToFC od str)
228 |      "Integer" => pure $ EInteger (boundToFC od str)
229 |      "Double" => pure $ EDouble (boundToFC od str)
230 |      "Type" => pure $ EConst (boundToFC od str) CType
231 |      "Kind" => pure $ EConst (boundToFC od str) Kind
232 |      "Sort" => pure $ EConst (boundToFC od str) Sort
233 |      x => fail "Expected builtin name"
234 |   where
235 |     cons : (FC -> RawExpr) -> RawExpr
236 |     cons = mkExprFC0 od str
237 |
238 | precedingComma :  Grammar state (RawToken) True (Maybe ())
239 | precedingComma = do
240 |   _ <- symbol ","
241 |   optional whitespace
242 |
243 | mutual
244 |   dhallImport : Grammar state (TokenRawToken) True (ImportStatement)
245 |   dhallImport = httpImport <|> envImport <|> pathImport <|> missingImport
246 |   where
247 |     httpImport : Grammar state (TokenRawToken) True (ImportStatement)
248 |     httpImport = do
249 |       h <- Rule.httpImport
250 |       pure $ Http h
251 |     envImport : Grammar state (TokenRawToken) True (ImportStatement)
252 |     envImport = do
253 |       e <- Rule.envImport
254 |       pure $ EnvVar e
255 |     pathImport : Grammar state (TokenRawToken) True (ImportStatement)
256 |     pathImport = do
257 |       p <- Rule.filePath
258 |       pure $ LocalFile $ filePathFromPath p
259 |     missingImport : Grammar state (TokenRawToken) True (ImportStatement)
260 |     missingImport = Rule.missingImport *> pure Missing
261 |
262 |   embed : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
263 |   embed od = do
264 |     i <- bounds (shaAndAsImport <|> asImport <|> shaImport <|> bareImport)
265 |     pure $ EEmbed (boundToFC od i) (val i)
266 |   where
267 |     asType : Grammar state (TokenRawToken) True (a -> Import a)
268 |     asType = do
269 |       (tokenW $ keyword "as Text" *> pure Text)
270 |         <|> (tokenW $ keyword "as Location" *> pure Location)
271 |     asImport : Grammar state (TokenRawToken) True (Import ImportStatement)
272 |     asImport = do
273 |       i <- dhallImport
274 |       con <- asType
275 |       pure $ con i
276 |     shaImport : Grammar state (TokenRawToken) True (Import ImportStatement)
277 |     shaImport = do
278 |       i <- dhallImport
279 |       _ <- tokenW $ Rule.shaImport
280 |       pure $ Raw i
281 |     shaAndAsImport : Grammar state (TokenRawToken) True (Import ImportStatement)
282 |     shaAndAsImport = do
283 |       i <- dhallImport
284 |       _ <- tokenW $ Rule.shaImport
285 |       con <- asType
286 |       pure $ con i
287 |     bareImport : Grammar state (TokenRawToken) True (Import ImportStatement)
288 |     bareImport = do
289 |       i <- dhallImport
290 |       pure $ Raw i
291 |
292 |   naturalLit : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
293 |   naturalLit od = do
294 |     s <- bounds $ Rule.naturalLit
295 |     pure $ mkExprFC od s ENaturalLit
296 |
297 |   integerLit : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
298 |   integerLit od = do
299 |     s <- bounds $ Rule.integerLit
300 |     pure $ mkExprFC od s EIntegerLit
301 |
302 |   doubleLit : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
303 |   doubleLit od = do
304 |     s <- bounds $ Rule.doubleLit
305 |     pure $ mkExprFC od s EDoubleLit
306 |
307 |   someLit : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
308 |   someLit od = do
309 |     start <- bounds $ tokenW $ someBuiltin
310 |     e <- bounds $ exprTerm od
311 |     pure $ ESome (mergeBounds (boundToFC od start) (boundToFC od e)) $ val e
312 |
313 |   emptyTextLit : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
314 |   emptyTextLit od = do
315 |     start <- bounds $ textBoundary
316 |     end <- bounds $ textBoundary
317 |     pure $ ETextLit (boundToFC2 od start end) neutral
318 |
319 |   textLit : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
320 |   textLit od = do
321 |     start <- bounds $ textBegin
322 |     chunks <- some (interpLit <|> chunkLit (val start))
323 |     end <- bounds $ textBoundary
324 |     pure $ ETextLit (boundToFC2 od start end) (foldl (<+>) neutral chunks)
325 |   where
326 |     interpLit : Rule (Chunks ImportStatement)
327 |     interpLit = do
328 |       e <- between interpBegin interpEnd $ exprTerm od
329 |       pure $ MkChunks [("", e)] ""
330 |
331 |     chunkLit : IsMultiline -> Rule (Chunks ImportStatement)
332 |     chunkLit x = do
333 |       str <- Parser.Rule.textLit x
334 |       pure (MkChunks [] str)
335 |
336 |   builtin : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
337 |   builtin od = do
338 |       name <- bounds $ Rule.builtin
339 |       builtinTerm od name
340 |
341 |   varTerm : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
342 |   varTerm od = do
343 |       name <- bounds $ identPart
344 |       pure $ EVar (boundToFC od name) (val name) 0
345 |
346 |   varAtTerm : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
347 |   varAtTerm od = do
348 |       name <- bounds $ identPart
349 |       symbol "@"
350 |       end <- bounds $ naturalLit
351 |       pure $ EVar (mergeBounds (boundToFC od name) (boundToFC od end)) (val name) (cast $ val end)
352 |
353 |   variable : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
354 |   variable od = varAtTerm od <|> varTerm od
355 |
356 |   postFix : OriginDesc -> WithBounds RawExpr -> Grammar state (TokenRawToken) True (RawExpr)
357 |   postFix od x = do
358 |     tokenW $ symbol "."
359 |     commit
360 |     rightProject <|> leftProject
361 |   where
362 |     rightProject : Grammar state (TokenRawToken) True (RawExpr)
363 |     rightProject = do
364 |       e <- bounds $ (between (symbol "(") (symbol ")") $ exprTerm od)
365 |       pure $ EProject (mergeBounds (boundToFC od x) (boundToFC od e)) (val x) (Right $ val e)
366 |     leftProject : Grammar state (TokenRawToken) True (RawExpr)
367 |     leftProject = do
368 |       l <- bounds $ (between (symbol "{") (symbol "}") (sepBy (symbol ",") fieldName))
369 |       pure $ EProject (mergeBounds (boundToFC od x) (boundToFC od l)) (val x) (Left $ map MkFieldName $ val l)
370 |       {-
371 |       pure $ case l of
372 |            (MkBounded Nothing isIrrelevant bounds) =>
373 |               EProject (mergeBounds (boundToFC od x) (boundToFC od l)) (val x) (Left $ [])
374 |            (MkBounded (Just y) isIrrelevant bounds) =>
375 |               EProject (mergeBounds (boundToFC od x) (boundToFC od l)) (val x) (Left $ forget $ y)
376 |               -}
377 |
378 |   atom : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
379 |   atom od = do
380 |     builtin od <|> variable od
381 |       <|> (textLit od) <|> emptyTextLit od
382 |       <|> naturalLit od <|> integerLit od <|> doubleLit od
383 |       <|> someLit od
384 |       <|> piTermLong od
385 |       <|> recordType od <|> recordLit od
386 |       <|> union od
387 |       <|> embed od
388 |       <|> listLit od <|> (between (symbol "(") (symbol ")") $ exprTerm od)
389 |
390 |   recordParser : OriginDesc
391 |                -> Grammar state (TokenRawToken) True ()
392 |                -> Grammar state (TokenRawToken) True ()
393 |                -> (FC -> (SortedMap FieldName (RawExpr)) -> RawExpr)
394 |                -> Grammar state (TokenRawToken) True (RawExpr)
395 |   recordParser od sep empty cons = do
396 |     start <- bounds $ tokenW $ symbol "{"
397 |     let fc' = boundToFC od start
398 |     emptyRecord fc' empty <|> populatedRecord fc'
399 |   where
400 |     emptyRecord : FC
401 |                 -> Grammar state (TokenRawToken) True ()
402 |                 -> Grammar state (TokenRawToken) True (RawExpr)
403 |     emptyRecord fc empty = do
404 |       end <- bounds empty
405 |       pure $ cons (mergeBounds fc (boundToFC initBounds end)) $ SortedMap.fromList []
406 |     recordField : Grammar state (TokenRawToken) True (FieldName, RawExpr)
407 |     recordField = do
408 |       i <- fieldName
409 |       _ <- optional whitespace
410 |       tokenW $ sep
411 |       e <- exprTerm od
412 |       pure (MkFieldName i, e)
413 |     populatedRecord : FC -> Grammar state (TokenRawToken) True (RawExpr)
414 |     populatedRecord fc = do
415 |       _ <- optional precedingComma
416 |       es <- sepBy (tokenW $ symbol ",") recordField
417 |       _ <- optional whitespace
418 |       end <- bounds $ symbol "}"
419 |       pure $ cons (mergeBounds fc (boundToFC od end)) $ SortedMap.fromList (es)
420 |
421 |   recordType : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
422 |   recordType od = recordParser od (symbol ":") (symbol "}") ERecord
423 |
424 |   recordLit : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
425 |   recordLit od = do
426 |     start <- bounds $ tokenW $ symbol "{"
427 |     commit
428 |     let fc' = boundToFC od start
429 |     emptyRecord fc' <|> populatedRecord fc'
430 |   where
431 |     emptyRecord : FC
432 |                 -> Grammar state (TokenRawToken) True (RawExpr)
433 |     emptyRecord fc = do
434 |       end <- bounds $ symbol "=" *> symbol "}"
435 |       pure $ ERecordLit (mergeBounds fc (boundToFC initBounds end)) $ SortedMap.fromList []
436 |     RecordElem : Type
437 |     RecordElem = SortedMap FieldName (Expr ImportStatement)
438 |     mkNestedRecord : List1 FieldName -> RawExpr -> RecordElem
439 |     mkNestedRecord ks e =
440 |       let (k ::: ks') = reverse ks in
441 |       foldl (\ms,k' => fromList [(k', ERecordLit initFC ms)]) (fromList [(k, e)]) ks'
442 |     dottedField : FC -> Grammar state (TokenRawToken) True RecordElem
443 |     dottedField fc = do
444 |       ls <- bounds dottedListRec
445 |       symbol "="
446 |       commit
447 |       e <- exprTerm od
448 |       pure $ mkNestedRecord (val ls) e
449 |     punField : FC -> Grammar state (TokenRawToken) True RecordElem
450 |     punField fc = do
451 |       i <- bounds fieldName
452 |       pure $ SortedMap.fromList [(MkFieldName (val i), EVar fc (val i) 0)] -- TODO check 0 here
453 |     recordField : FC -> Grammar state (TokenRawToken) True RecordElem
454 |     recordField fc = dottedField fc <|> punField fc
455 |     populatedRecord : FC -> Grammar state (TokenRawToken) True (RawExpr)
456 |     populatedRecord fc = do
457 |       _ <- optional precedingComma
458 |       es <- sepBy1 (symbol ",") (recordField fc)
459 |       end <- bounds $ symbol "}"
460 |       pure $ ERecordLit (mergeBounds fc (boundToFC od end)) $ foldl1 (mergeWith (ECombine initFC)) es
461 |
462 |   union : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
463 |   union od = do
464 |     start <- bounds $ tokenW $ symbol "<"
465 |     commit
466 |     es <- sepBy (tokenW $ symbol "|") (unionComplex <|> unionSimple)
467 |     _ <- optional whitespace
468 |     end <- bounds $ symbol ">"
469 |     pure $ EUnion (mergeBounds (boundToFC od start) (boundToFC od end)) $ SortedMap.fromList es
470 |   where
471 |     unionSimple : Grammar state (TokenRawToken) True (FieldName, Maybe (RawExpr))
472 |     unionSimple = do
473 |       name <- tokenW $ fieldName
474 |       pure (MkFieldName name, Nothing)
475 |     unionComplex : Grammar state (TokenRawToken) True (FieldName, Maybe (RawExpr))
476 |     unionComplex = do
477 |       name <- tokenW $ fieldName
478 |       start <- bounds $ tokenW $ symbol ":"
479 |       e <- exprTerm od
480 |       _ <- optional whitespace
481 |       pure (MkFieldName name, Just e)
482 |
483 |   listLit : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
484 |   listLit od = do
485 |     start <- bounds $ tokenW $ symbol "["
486 |     commit
487 |     let fc' = boundToFC od start
488 |     (populatedList fc') <|> (emptyList fc')
489 |   where
490 |     listType : Grammar state (TokenRawToken) True (WithBounds RawExpr)
491 |     listType = do
492 |       tokenW $ symbol ":"
493 |       bounds $ exprTerm od
494 |     emptyList : FC -> Grammar state (TokenRawToken) True (RawExpr)
495 |     emptyList fc = do
496 |       tokenW $ symbol "]"
497 |       ty <- listType
498 |       pure $ EListLit (mergeBounds fc (boundToFC od ty)) (Just (val ty)) []
499 |     populatedList : FC -> Grammar state (TokenRawToken) True (RawExpr)
500 |     populatedList fc = do
501 |       _ <- optional precedingComma
502 |       es <- sepBy1 (tokenW $ symbol ",") $ exprTerm od
503 |       _ <- optional whitespace
504 |       end <- bounds $ symbol "]"
505 |       ty <- optional listType
506 |       pure $ case ty of
507 |                   Nothing =>
508 |                     EListLit (mergeBounds fc (boundToFC od end)) Nothing (forget es)
509 |                   (Just ty') =>
510 |                     EListLit (mergeBounds fc (boundToFC initBounds ty')) (Just $ val ty') (forget es)
511 |
512 |   opParser : Grammar state (TokenRawToken) True ()
513 |            -> (FC -> RawExpr -> RawExpr -> RawExpr)
514 |            -> Grammar state (TokenRawToken) True (RawExpr -> RawExpr -> RawExpr)
515 |   opParser op cons = infixOp (do
516 |       _ <- optional whitespace
517 |       tokenW op) (boundedOp cons)
518 |
519 |   mulOp : Grammar state (TokenRawToken) True (RawExpr -> RawExpr -> RawExpr)
520 |   mulOp = (opParser (symbol "*") ENaturalTimes)
521 |
522 |   withOp : Grammar state (TokenRawToken) True (RawExpr -> RawExpr -> RawExpr)
523 |   withOp =
524 |     do
525 |       -- TODO find a better solution than just `match White` at the start of
526 |       -- every operator
527 |       _ <- optional $ whitespace
528 |       tokenW $ keyword "with"
529 |       commit
530 |       dl <- dottedList
531 |       _ <- optional $ whitespace
532 |       tokenW $ symbol "="
533 |       pure (boundedOp (with' dl))
534 |   where
535 |     with' : List1 FieldName -> FC -> Expr a -> Expr a -> Expr a
536 |     with' xs fc x y = EWith fc x xs y
537 |
538 |   projTermLeft : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
539 |   projTermLeft od = hchainl (fieldTerm od) projOp listFieldName
540 |   where
541 |     proj' : RawExpr -> WithBounds (List String) -> RawExpr
542 |     proj' e ls =
543 |       let start = getFC e
544 |           end = boundToFC od ls
545 |           fc' = mergeBounds start end
546 |       in EProject fc' e $ Left $ map MkFieldName (val ls)
547 |     projOp : Grammar state (TokenRawToken) True (RawExpr -> WithBounds (List String) -> RawExpr)
548 |     projOp = do
549 |       symbol ".{"
550 |       commit
551 |       pure proj'
552 |     listFieldName : Grammar state (TokenRawToken) True (WithBounds (List String))
553 |     listFieldName = do
554 |       ls <- bounds $ (sepBy (symbol ",") fieldName) <* symbol "}"
555 |       pure ls
556 |
557 |   projTermRight : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
558 |   projTermRight od = hchainl (projTermLeft od) projOp (bounds $ exprTerm od <* symbol ")")
559 |   where
560 |     proj' : RawExpr -> WithBounds RawExpr -> RawExpr
561 |     proj' e e' =
562 |       let start = getFC e
563 |           fc' = mergeBounds start (boundToFC od e')
564 |       in EProject fc' e $ Right $ val e'
565 |     projOp : Grammar state (TokenRawToken) True (RawExpr -> WithBounds RawExpr -> RawExpr)
566 |     projOp = do
567 |       symbol ".("
568 |       commit
569 |       pure proj'
570 |
571 |   fieldTerm : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
572 |   fieldTerm od = hchainl (atom od) fieldOp (bounds fieldName)
573 |   where
574 |     field' : RawExpr -> WithBounds String -> RawExpr
575 |     field' e s =
576 |       let start = getFC e
577 |           end = boundToFC od $ s
578 |           fc' = mergeBounds start end
579 |       in EField fc' e (MkFieldName (val s))
580 |     fieldOp : Grammar state (TokenRawToken) True (RawExpr -> WithBounds String -> RawExpr)
581 |     fieldOp = do
582 |       _ <- optional whitespace
583 |       _ <- tokenW $ symbol "."
584 |       pure $ field'
585 |
586 |   recordCompletion : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
587 |   recordCompletion od = hchainl (projTermRight od) recordCompletionOp (projTermRight od)
588 |     where
589 |       recordCompletionOp : Grammar state (TokenRawToken) True (RawExpr -> RawExpr -> RawExpr)
590 |       recordCompletionOp = (opParser (symbol "::") ERecordCompletion)
591 |
592 |   appTerm : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
593 |   appTerm od = (do
594 |                 x <- some $ recordCompletion od
595 |                 pure $ List1.foldl1 (EApp EmptyFC) x) -- (appOp)
596 |
597 |   mulTerm : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
598 |   mulTerm od = chainl1 (appTerm od) (mulOp)
599 |
600 |   boolTerm : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
601 |   boolTerm od = chainl1 (mulTerm od) (boolOp)
602 |   where
603 |     boolOp : Grammar state (TokenRawToken) True (RawExpr -> RawExpr -> RawExpr)
604 |     boolOp =
605 |       (opParser (symbol "&&") EBoolAnd) <|> (opParser (symbol "||") EBoolOr)
606 |       <|> (opParser (symbol "==") EBoolEQ) <|> (opParser (symbol "!=") EBoolNE)
607 |
608 |   piTerm : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
609 |   piTerm od = chainr1 (boolTerm od) (piOp)
610 |   where
611 |     epi' : String -> FC -> Expr a -> Expr a -> Expr a
612 |     epi' n fc y z = EPi fc n y z
613 |     piOp : Grammar state (TokenRawToken) True (RawExpr -> RawExpr -> RawExpr)
614 |     piOp =
615 |         infixOp (do
616 |           _ <- optional whitespace
617 |           arrow)
618 |           (boundedOp $ epi' "_")
619 |
620 |   annotTerm : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
621 |   annotTerm od = chainr1 (piTerm od) (annotOp)
622 |   where
623 |     annotOp : Grammar state (TokenRawToken) True (RawExpr -> RawExpr -> RawExpr)
624 |     annotOp = (opParser (symbol ":") EAnnot)
625 |
626 |   plusTerm : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
627 |   plusTerm od = chainl1 (annotTerm od) (plusOp)
628 |   where
629 |     plusOp : Grammar state (TokenRawToken) True (RawExpr -> RawExpr -> RawExpr)
630 |     plusOp = (opParser (symbol "+") ENaturalPlus)
631 |
632 |   otherTerm : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
633 |   otherTerm od = chainl1 (annotTerm od) (otherOp)
634 |   where
635 |     otherOp : Grammar state (TokenRawToken) True (RawExpr -> RawExpr -> RawExpr)
636 |     otherOp =
637 |       (opParser (symbol "++") ETextAppend) <|> (opParser (symbol "#") EListAppend)
638 |         <|> (opParser (symbol "&&") EBoolAnd) <|> (opParser (symbol "||") EBoolOr)
639 |         <|> (opParser (symbol "==") EBoolEQ) <|> (opParser (symbol "!=") EBoolNE)
640 |         <|> (opParser (symbol "+") ENaturalPlus)
641 |         <|> (opParser (symbol "/\\" <|> symbol "∧") ECombine)
642 |         <|> (opParser (symbol "//\\\\" <|> symbol "⩓") ECombineTypes)
643 |         <|> (opParser (symbol "//" <|> symbol "⫽") EPrefer)
644 |         <|> (opParser (symbol "===" <|> symbol "≡") EEquivalent)
645 |         <|> (opParser (symbol "?") EImportAlt)
646 |
647 |   exprTerm : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
648 |   exprTerm od = do
649 |     piTermLong od <|>
650 |     chainl1 (otherTerm od) (withOp) <|>
651 |     letBinding od <|>
652 |     lamTerm od <|>
653 |     assertTerm od <|>
654 |     ifTerm od <|>
655 |     mergeTerm od <|>
656 |     toMapTerm od
657 |
658 |   letBinding : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
659 |   letBinding od = do
660 |     start <- bounds $ tokenW $ keyword "let"
661 |     commit
662 |     name <- tokenW $ identPart
663 |     ty <- optional (tokenW $ symbol ":" *> exprTerm od)
664 |     _ <- tokenW $ symbol "="
665 |     e <- bounds $ exprTerm od
666 |     _ <- optional whitespace
667 |     _ <- optional $ tokenW $ keyword "in"
668 |     e' <- exprTerm od
669 |     pure $ ELet (mergeBounds (boundToFC od start) (boundToFC od e)) name ty (val e) e'
670 |
671 |   piTermLong : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
672 |   piTermLong od = do
673 |     start <- bounds $ piStart
674 |     commit
675 |     name <- identPart
676 |     _ <- symbol ":"
677 |     t <- bounds $ exprTerm od
678 |     _ <- symbol ")"
679 |     _ <- arrow
680 |     body <- bounds $ exprTerm od
681 |     pure $ EPi (mergeBounds (boundToFC od start) (boundToFC od body))
682 |             name (val t) (val body)
683 |   where
684 |     piStart : Grammar state (TokenRawToken) True ()
685 |     piStart = ((symbol "∀" <|> keyword "forall") *> symbol "(")
686 |
687 |   lamTerm : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
688 |   lamTerm od = do
689 |     start <- bounds $ lamStart
690 |     commit
691 |     name <- tokenW $ identPart
692 |     _ <- symbol ":"
693 |     _ <- optional whitespace
694 |     t <- bounds $ exprTerm od
695 |     _ <- tokenW $ symbol ")"
696 |     _ <- arrow
697 |     body <- bounds $ exprTerm od
698 |     pure $ ELam (mergeBounds (boundToFC od start) (boundToFC od body))
699 |             name (val t) (val body)
700 |   where
701 |     lamStart : Grammar state (TokenRawToken) True ()
702 |     lamStart = tokenW $ ((symbol "\\" <|> symbol "λ") *> symbol "(")
703 |
704 |   assertTerm : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
705 |   assertTerm od = do
706 |     start <- bounds $ tokenW $ keyword "assert"
707 |     commit
708 |     _ <- symbol ":"
709 |     _ <- optional whitespace
710 |     e <- bounds $ exprTerm od
711 |     pure $ EAssert (mergeBounds (boundToFC od start) (boundToFC od e)) (val e)
712 |
713 |   mergeTerm : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
714 |   mergeTerm od = Text.Parser.Core.do
715 |     start <- bounds $ tokenW $ keyword "merge"
716 |     commit
717 |     e1 <- bounds $ exprTerm od
718 |     the (Grammar state TokenRawToken _ (RawExpr)) $
719 |       case go (boundToFC od start) (val e1) of
720 |            (Right x) => pure x
721 |            (Left _) => fail "TODO implement better merge parse"
722 |   where
723 |     go : FC -> RawExpr -> Either () (RawExpr)
724 |     go start (EApp fc x y) =
725 |       pure $ EMerge (mergeBounds start fc) x y Nothing
726 |     go start (EAnnot fc (EApp _ x y) t) =
727 |       pure $ EMerge (mergeBounds start fc) x y (Just t)
728 |     go _ _ = Left ()
729 |
730 |   toMapTerm : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
731 |   toMapTerm od = Text.Parser.Core.do
732 |     start <- bounds $ tokenW $ keyword "toMap"
733 |     commit
734 |     e <- bounds $ exprTerm od
735 |     pure $ case val e of -- TODO find out why pure must be here?
736 |          (EAnnot fc x y) =>
737 |             EToMap (mergeBounds (boundToFC od start) (boundToFC od e)) x (Just y)
738 |          x =>
739 |             EToMap (mergeBounds (boundToFC od start) (boundToFC od e)) x Nothing
740 |
741 |   ifTerm : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
742 |   ifTerm od = do
743 |     start <- bounds $ tokenW $ keyword "if"
744 |     commit
745 |     i <- bounds $ exprTerm od
746 |     _ <- optional whitespace
747 |     _ <- bounds $ tokenW $ keyword "then"
748 |     t <- bounds $ exprTerm od
749 |     _ <- optional whitespace
750 |     _ <- bounds $ tokenW $ keyword "else"
751 |     e <- bounds $ exprTerm od
752 |     pure $ EBoolIf (mergeBounds (boundToFC od start) (boundToFC od e))
753 |             (val i) (val t) (val e)
754 |
755 | finalParser : OriginDesc -> Grammar state (TokenRawToken) True (RawExpr)
756 | finalParser od = do
757 |   e <- exprTerm od
758 |   -- _ <- optional $ many whitespace
759 |   endOfInput
760 |   pure e
761 |
762 | [PERROR] Show (ParsingError TokenRawToken) where
763 |   show (Error x xs) =
764 |     """
765 |     error: \{x}
766 |     tokens: \{show xs}
767 |     """
768 |
769 | removeComments : List (WithBounds TokenRawToken) -> List (WithBounds TokenRawToken)
770 | removeComments xs = filter pred xs
771 | where
772 |   pred : WithBounds RawToken -> Bool
773 |   pred bounds = let tok = val bounds in
774 |     case tok of
775 |          Comment _ => False
776 |          _ => True
777 |
778 | combineWhite : List (WithBounds TokenRawToken) -> List (WithBounds TokenRawToken)
779 | combineWhite [] = []
780 | combineWhite [x] = [x]
781 | combineWhite (x :: y :: xs) =
782 |   case (val x, val y) of
783 |        (White, White) => combineWhite (y :: xs)
784 |        (t, u) => x :: combineWhite (y :: xs)
785 |
786 | doLex : String -> Either (StopReason, Int, Int, String) (List (WithBounds TokenRawToken))
787 | doLex input = Idrall.Parser.Lexer.lex input
788 |
789 | doParse' : OriginDesc -> List (WithBounds TokenRawToken) -> Either (List1 (ParsingError RawToken)) (RawExpr, List (WithBounds TokenRawToken))
790 | doParse' od tokens =
791 |   let processedTokens = (combineWhite . removeComments) tokens
792 |   in parse (finalParser od) $ processedTokens
793 |
794 | public export
795 | parseExprNew : {default Nothing od : OriginDesc} -> String -> Either String (RawExpr, Int)
796 | parseExprNew input = do
797 |     Right tokens <- pure $ doLex input
798 |       | Left e => Left $ show e
799 |
800 |     Right (expr, x) <- pure $ doParse' od tokens
801 |       | Left e => Left $ let %hint perror : ?; perror = PERROR in "\{show od} \{show e}"
802 |     pure (expr, 0)
803 |
804 | doParse : String -> IO ()
805 | doParse input = do
806 |   Right tokens <- pure $ doLex input
807 |     | Left e => printLn $ show e
808 |   putStrLn $ "tokens: " ++ show tokens
809 |
810 |   let processedTokens = (combineWhite . removeComments) tokens
811 |   putStrLn $ "processedTokens: " ++ show processedTokens
812 |   Right (expr, x) <- pure $ doParse' Nothing tokens
813 |     | Left e => printLn $ let %hint perror : ?; perror = PERROR in show e
814 |
815 |   let doc = the (Doc (RawExpr)) $ pretty expr
816 |   putStrLn $
817 |     """
818 |     expr: \{show expr}
819 |     x: \{show x}
820 |     pretty: \{show doc}
821 |     """
822 |
823 | normalString : String
824 | normalString = "\"f\noo\""
825 |
826 | interpString : String
827 | interpString = "\"fo ${True && \"ba ${False} r\"} o\""
828 |