@@ -190,9 +190,7 @@ extension syn (Rule ssym ptm _)
190190{- | Parses a (normal) built-in expression
191191@
192192InternalExpr ::=
193− App
194− | MatchApp
195− | UnifyLog
193+ UnifyLog
196194 | RecordType
197195 | SimpleExpr
198196 | Lambda
@@ -202,16 +200,15 @@ InternalExpr ::=
202200 | Pi
203201 | CaseExpr
204202 | DoBlock
203+ | App
205204 ;
206205@
207206-}
208207internalExpr :: SyntaxInfo -> IdrisParser PTerm
209208internalExpr syn =
210− try (app syn)
211− <|> try (matchApp syn)
212− <|> try (unifyLog syn)
213− <|> try (disamb syn)
214− <|> try (noImplicits syn)
209+ unifyLog syn
210+ <|> disamb syn
211+ <|> noImplicits syn
215212 <|> recordType syn
216213 <|> lambda syn
217214 <|> quoteGoal syn
@@ -220,7 +217,7 @@ internalExpr syn =
220217 <|> try (pi syn)
221218 <|> doBlock syn
222219 <|> caseExpr syn
223− <|> simpleExpr syn
220+ <|> app syn
224221 <?> "expression"
225222
226223{- | Parses a case expression
@@ -278,30 +275,28 @@ tacticsExpr syn = do reserved "tactics"
278275{- | Parses a simple expression
279276@
280277SimpleExpr ::=
281− '![' Term ']'
278+ {- External (User-defined) Simple Expression -}
282279 | '?' Name
283280 | % 'instance'
284281 | 'refl' ('{' Expr '}')?
285282 | ProofExpr
286283 | TacticsExpr
287284 | FnName
285+ | Idiom
288286 | List
289− | Comprehension
290287 | Alt
291− | Idiom
292− | '(' Bracketed
288+ | Bracketed
293289 | Constant
294290 | Type
295291 | '_|_'
296292 | '_'
297− | {- External (User-defined) Simple Expression -}
298293 ;
299294@
300295-}
301296simpleExpr :: SyntaxInfo -> IdrisParser PTerm
302297simpleExpr syn =
303− {-try (do symbol "!["; t <- term; lchar ']'; return $ PQuote t)
304− <|>-} do x <- try (lchar '?' *> name); return (PMetavar x)
298+ try (simpleExternalExpr syn)
299+ <|> do x <- try (lchar '?' *> name); return (PMetavar x)
305300 <|> do lchar '%'; fc <- getFC; reserved "instance"; return (PResolveTC fc)
306301 <|> do reserved "refl"; fc <- getFC;
307302 tm <- option Placeholder (do lchar '{'; t <- expr syn; lchar '}';
@@ -311,36 +306,39 @@ simpleExpr syn =
311306 <|> proofExpr syn
312307 <|> tacticsExpr syn
313308 <|> do reserved "Type"; return PType
314− <|> try (do c <- constant
315− fc <- getFC
316− return (modifyConst syn fc (PConstant c)))
317− <|> try (do symbol "'"; fc <- getFC; str <- name
318− return (PApp fc (PRef fc (sUN "Symbol_"))
319− [pexp (PConstant (Str (show str)))]))
309+ <|> do c <- constant
310+ fc <- getFC
311+ return (modifyConst syn fc (PConstant c))
312+ <|> do symbol "'"; fc <- getFC; str <- name
313+ return (PApp fc (PRef fc (sUN "Symbol_"))
314+ [pexp (PConstant (Str (show str)))])
320315 <|> do fc <- getFC
321316 x <- fnName
322317 return (PRef fc x)
323− <|> try (listExpr syn)
324− <|> try (comprehension syn)
325− <|> alt syn
326318 <|> idiom syn
319+ <|> listExpr syn
320+ <|> alt syn
327321 <|> do lchar '!'
328322 s <- simpleExpr syn
329323 fc <- getFC
330324 return (PAppBind fc s [])
331− <|> do lchar '('
332− bracketed (disallowImp syn)
325+ <|> bracketed (disallowImp syn)
333326 <|> do symbol "_|_"
334327 fc <- getFC
335328 return (PFalse fc)
336329 <|> do lchar '_'; return Placeholder
337− <|> simpleExternalExpr syn
338330 <?> "expression"
339331
340−
332+{- |Parses an expression in braces
333+@
334+Bracketed ::= '(' Bracketed'
335+ -}
336+bracketed :: SyntaxInfo -> IdrisParser PTerm
337+bracketed syn = do lchar '(' <?> "parenthesized expression"
338+ bracketed' syn
341339{- |Parses the rest of an expression in braces
342340@
343−Bracketed ::=
341+Bracketed' ::=
344342 ')'
345343 | Expr ')'
346344 | ExprList ')'
@@ -351,8 +349,8 @@ Bracketed ::=
351349 ;
352350@
353351-}
354−bracketed :: SyntaxInfo -> IdrisParser PTerm
355−bracketed syn =
352+bracketed' :: SyntaxInfo -> IdrisParser PTerm
353+bracketed' syn =
356354 do lchar ')'
357355 fc <- getFC
358356 return $ PTrue fc TypeOrTerm
@@ -425,29 +423,6 @@ modifyConst syn fc (PConstant (BI x))
425423 ]
426424modifyConst syn fc x = x
427425
428−{- | Parses a list literal expression e.g. [1,2,3]
429−@
430−ListExpr ::=
431− '[' ExprList? ']'
432−;
433−@
434−@
435−ExprList ::=
436− Expr
437− | Expr ',' ExprList
438− ;
439−@
440− -}
441−listExpr :: SyntaxInfo -> IdrisParser PTerm
442−listExpr syn = do lchar '['; fc <- getFC; xs <- sepBy (expr syn) (lchar ','); lchar ']'
443− return (mkList fc xs)
444− <?> "list expression"
445− where
446− mkList :: FC -> [PTerm] -> PTerm
447− mkList fc [] = PRef fc (sUN "Nil")
448− mkList fc (x : xs) = PApp fc (PRef fc (sUN "::")) [pexp x, pexp (mkList fc xs)]
449−
450−
451426{- | Parses an alternative expression
452427@
453428 Alt ::= '(|' Expr_List '|)';
@@ -478,31 +453,13 @@ hsimpleExpr syn =
478453 <|> simpleExpr syn
479454 <?> "expression"
480455
481−{- | Parses a matching application expression
482−@
483−MatchApp ::=
484− SimpleExpr '<==' FnName
485− ;
486−@
487−-}
488−matchApp :: SyntaxInfo -> IdrisParser PTerm
489−matchApp syn = do ty <- simpleExpr syn
490− symbol "<=="
491− fc <- getFC
492− f <- fnName
493− return (PLet (sMN 0 "match")
494− ty
495− (PMatchApp fc f)
496− (PRef fc (sMN 0 "match")))
497− <?> "matching application expression"
498−
499456{- | Parses a unification log expression
500457UnifyLog ::=
501458 '%' 'unifyLog' SimpleExpr
502459 ;
503460-}
504461unifyLog :: SyntaxInfo -> IdrisParser PTerm
505−unifyLog syn = do lchar '%'; reserved "unifyLog";
462+unifyLog syn = do try (lchar '%' *> reserved "unifyLog")
506463 tm <- simpleExpr syn
507464 return (PUnifyLog tm)
508465 <?> "unification log expression"
@@ -528,7 +485,7 @@ NoImplicits ::=
528485@
529486-}
530487noImplicits :: SyntaxInfo -> IdrisParser PTerm
531−noImplicits syn = do lchar '%'; reserved "noImplicits";
488+noImplicits syn = do try (lchar '%' *> reserved "noImplicits")
532489 tm <- simpleExpr syn
533490 return (PNoImplicits tm)
534491 <?> "no implicits expression"
@@ -537,7 +494,11 @@ noImplicits syn = do lchar '%'; reserved "noImplicits";
537494@
538495App ::=
539496 'mkForeign' Arg Arg*
540− | SimpleExpr Arg+
497+ | MatchApp
498+ | SimpleExpr Arg*
499+ ;
500+MatchApp ::=
501+ SimpleExpr '<==' FnName
541502 ;
542503@
543504-}
@@ -547,8 +508,6 @@ app syn = do f <- reserved "mkForeign"
547508 fn <- arg syn
548509 args <- many (do notEndApp; arg syn)
549510 i <- get
550− -- mkForeign f args ==>
551− -- liftPrimIO (\w => mkForeignPrim f args w)
552511 let ap = PApp fc (PRef fc (sUN "liftPrimIO"))
553512 [pexp (PLam (sMN 0 "w")
554513 Placeholder
@@ -558,13 +517,20 @@ app syn = do f <- reserved "mkForeign"
558517 return (dslify i ap)
559518
560519 <|> do f <- simpleExpr syn
520+ (do try $ symbol "<=="
521+ fc <- getFC
522+ ff <- fnName
523+ return (PLet (sMN 0 "match")
524+ f
525+ (PMatchApp fc ff)
526+ (PRef fc (sMN 0 "match")))
527+ <?> "matching application expression") <|> (do
561528 fc <- getFC
562− args <- some (do notEndApp; arg syn)
563529 i <- get
564−-- case f of
565−-- PAppBind fc ref [] ->
566−-- return (dslify i (PAppBind fc ref args))
567− return (dslify i (PApp fc f args))
530+ args <- many (do notEndApp; arg syn)
531+ case args of
532+ [] -> return f
533+ _ -> return (dslify i (PApp fc f args)))
568534 <?> "function application"
569535 where
570536 dslify :: IState -> PTerm -> PTerm
@@ -700,17 +666,17 @@ SimpleExprList ::=
700666@
701667-}
702668lambda :: SyntaxInfo -> IdrisParser PTerm
703−lambda syn = do lchar '\\'
704− try (do xt <- tyOptDeclList syn
705− symbol "=>"
706− sc <- expr syn
707− return (bindList PLam xt sc)
708− <|> (do ps <- sepBy (do fc <- getFC
709− e <- simpleExpr syn
710− return (fc, e)) (lchar ',')
711− symbol "=>"
712− sc <- expr syn
713− return (pmList (zip [0..] ps) sc)))
669+lambda syn = do lchar '\\' <?> "lambda expression"
670+ (do xt <- try $ tyOptDeclList syn
671+ symbol "=>"
672+ sc <- expr syn
673+ return (bindList PLam xt sc)) <|> do
674+ ps <- sepBy (do fc <- getFC
675+ e <- simpleExpr syn
676+ return (fc, e)) (lchar ',')
677+ symbol "=>"
678+ sc <- expr syn
679+ return (pmList (zip [0..] ps) sc)
714680 <?> "lambda expression"
715681 where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm
716682 pmList [] sc = sc
@@ -911,34 +877,49 @@ tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder
911877 return (sMN 0 "underscore")
912878 <?> "name or placeholder"
913879
914−{- | Parses a list comprehension
880+{- | Parses a list literal expression e.g. [1,2,3] or a comprehension [ (x, y) | x <- xs , y <- ys ]
915881@
916−Comprehension ::= '[' Expr '|' DoList ']';
882+ListExpr ::=
883+ '[' ']'
884+ | '[' Expr '|' DoList ']'
885+ | '[' ExprList ']'
886+;
917887@
918−
919888@
920889DoList ::=
921890 Do
922891 | Do ',' DoList
923892 ;
924893@
925−-}
926−comprehension :: SyntaxInfo -> IdrisParser PTerm
927−comprehension syn
928− = do lchar '['
929− fc <- getFC
930− pat <- expr syn
931− lchar '|'
932− qs <- sepBy1 (do_ syn) (lchar ',')
933− lchar ']'
934− return (PDoBlock (map addGuard qs ++
935− [DoExp fc (PApp fc (PRef fc (sUN "return"))
936− [pexp pat])]))
937− <?> "list comprehension"
938− where addGuard :: PDo -> PDo
939− addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (sUN "guard"))
940− [pexp e])
941− addGuard x = x
894+@
895+ExprList ::=
896+ Expr
897+ | Expr ',' ExprList
898+ ;
899+@
900+ -}
901+listExpr :: SyntaxInfo -> IdrisParser PTerm
902+listExpr syn = do lchar '['; fc <- getFC;
903+ try ((lchar ']' <?> "end of list expression") *> return (mkList fc [])) <|> (do
904+ x <- expr syn <?> "expression"
905+ (do try (lchar '|') <?> "list comprehension"
906+ qs <- sepBy1 (do_ syn) (lchar ',')
907+ lchar ']'
908+ return (PDoBlock (map addGuard qs ++
909+ [DoExp fc (PApp fc (PRef fc (sUN "return"))
910+ [pexp x])]))) <|> (do
911+ xs <- many ((lchar ',' <?> "list element") *> expr syn)
912+ lchar ']' <?> "end of list expression"
913+ return (mkList fc (x:xs))))
914+ <?> "list expression"
915+ where
916+ mkList :: FC -> [PTerm] -> PTerm
917+ mkList fc [] = PRef fc (sUN "Nil")
918+ mkList fc (x : xs) = PApp fc (PRef fc (sUN "::")) [pexp x, pexp (mkList fc xs)]
919+ addGuard :: PDo -> PDo
920+ addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (sUN "guard"))
921+ [pexp e])
922+ addGuard x = x
942923
943924{- | Parses a do-block
944925@
@@ -1070,11 +1051,11 @@ constant = do reserved "Integer"; return (AType (ATInt ITBig))
10701051 <|> do reserved "Bits16x8"; return (AType (ATInt (ITVec IT16 8)))
10711052 <|> do reserved "Bits32x4"; return (AType (ATInt (ITVec IT32 4)))
10721053 <|> do reserved "Bits64x2"; return (AType (ATInt (ITVec IT64 2)))
1073− <|> try (do f <- float; return $ Fl f)
1074− <|> try (do i <- natural; return $ BI i)
1075− <|> try (do s <- verbatimStringLiteral; return $ Str s)
1076− <|> try (do s <- stringLiteral; return $ Str s)
1077− <|> try (do c <- charLiteral; return $ Ch c)
1054+ <|> do f <- try float; return $ Fl f
1055+ <|> do i <- natural; return $ BI i
1056+ <|> do s <- verbatimStringLiteral; return $ Str s
1057+ <|> do s <- stringLiteral; return $ Str s
1058+ <|> do c <- try charLiteral; return $ Ch c --Currently ambigous with symbols
10781059 <?> "constant or literal"
10791060
10801061{- | Parses a verbatim multi-line string literal (triple-quoted)
@@ -1086,7 +1067,7 @@ VerbatimString_t ::=
10861067@
10871068 -}
10881069verbatimStringLiteral :: MonadicParsing m => m String
1089−verbatimStringLiteral = token $ do string "\"\"\""
1070+verbatimStringLiteral = token $ do try $ string "\"\"\""
10901071 manyTill anyChar $ try (string "\"\"\"")
10911072
10921073{- | Parses a static modifier