@@ -207,7 +207,7 @@ InternalExpr ::=
207207internalExpr :: SyntaxInfo -> IdrisParser PTerm
208208internalExpr syn =
209209 unifyLog syn
210− <|> try (disamb syn)
210+ <|> disamb syn
211211 <|> noImplicits syn
212212 <|> recordType syn
213213 <|> lambda syn
@@ -275,30 +275,28 @@ tacticsExpr syn = do reserved "tactics"
275275{- | Parses a simple expression
276276@
277277SimpleExpr ::=
278− '![' Term ']'
278+ {- External (User-defined) Simple Expression -}
279279 | '?' Name
280280 | % 'instance'
281281 | 'refl' ('{' Expr '}')?
282282 | ProofExpr
283283 | TacticsExpr
284284 | FnName
285+ | Idiom
285286 | List
286− | Comprehension
287287 | Alt
288− | Idiom
289288 | Bracketed
290289 | Constant
291290 | Type
292291 | '_|_'
293292 | '_'
294− | {- External (User-defined) Simple Expression -}
295293 ;
296294@
297295-}
298296simpleExpr :: SyntaxInfo -> IdrisParser PTerm
299297simpleExpr syn =
300− {-try (do symbol "!["; t <- term; lchar ']'; return $ PQuote t)
301− <|>-} do x <- try (lchar '?' *> name); return (PMetavar x)
298+ try (simpleExternalExpr syn)
299+ <|> do x <- try (lchar '?' *> name); return (PMetavar x)
302300 <|> do lchar '%'; fc <- getFC; reserved "instance"; return (PResolveTC fc)
303301 <|> do reserved "refl"; fc <- getFC;
304302 tm <- option Placeholder (do lchar '{'; t <- expr syn; lchar '}';
@@ -308,19 +306,18 @@ simpleExpr syn =
308306 <|> proofExpr syn
309307 <|> tacticsExpr syn
310308 <|> do reserved "Type"; return PType
311− <|> try (do c <- constant
312− fc <- getFC
313− return (modifyConst syn fc (PConstant c)))
314− <|> try (do symbol "'"; fc <- getFC; str <- name
315− return (PApp fc (PRef fc (sUN "Symbol_"))
316− [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)))])
317315 <|> do fc <- getFC
318316 x <- fnName
319317 return (PRef fc x)
320− <|> try (listExpr syn)
321− <|> try (comprehension syn)
322− <|> alt syn
323318 <|> idiom syn
319+ <|> listExpr syn
320+ <|> alt syn
324321 <|> do lchar '!'
325322 s <- simpleExpr syn
326323 fc <- getFC
@@ -330,7 +327,6 @@ simpleExpr syn =
330327 fc <- getFC
331328 return (PFalse fc)
332329 <|> do lchar '_'; return Placeholder
333− <|> simpleExternalExpr syn
334330 <?> "expression"
335331
336332{- |Parses an expression in braces
@@ -427,29 +423,6 @@ modifyConst syn fc (PConstant (BI x))
427423 ]
428424modifyConst syn fc x = x
429425
430−{- | Parses a list literal expression e.g. [1,2,3]
431−@
432−ListExpr ::=
433− '[' ExprList? ']'
434−;
435−@
436−@
437−ExprList ::=
438− Expr
439− | Expr ',' ExprList
440− ;
441−@
442− -}
443−listExpr :: SyntaxInfo -> IdrisParser PTerm
444−listExpr syn = do lchar '['; fc <- getFC; xs <- sepBy (expr syn) (lchar ','); lchar ']'
445− return (mkList fc xs)
446− <?> "list expression"
447− where
448− mkList :: FC -> [PTerm] -> PTerm
449− mkList fc [] = PRef fc (sUN "Nil")
450− mkList fc (x : xs) = PApp fc (PRef fc (sUN "::")) [pexp x, pexp (mkList fc xs)]
451−
452−
453426{- | Parses an alternative expression
454427@
455428 Alt ::= '(|' Expr_List '|)';
@@ -901,34 +874,49 @@ tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder
901874 return (sMN 0 "underscore")
902875 <?> "name or placeholder"
903876
904−{- | Parses a list comprehension
877+{- | Parses a list literal expression e.g. [1,2,3] or a comprehension [ (x, y) | x <- xs , y <- ys ]
905878@
906−Comprehension ::= '[' Expr '|' DoList ']';
879+ListExpr ::=
880+ '[' ']'
881+ | '[' Expr '|' DoList ']'
882+ | '[' ExprList ']'
883+;
907884@
908−
909885@
910886DoList ::=
911887 Do
912888 | Do ',' DoList
913889 ;
914890@
915−-}
916−comprehension :: SyntaxInfo -> IdrisParser PTerm
917−comprehension syn
918− = do lchar '['
919− fc <- getFC
920− pat <- expr syn
921− lchar '|'
922− qs <- sepBy1 (do_ syn) (lchar ',')
923− lchar ']'
924− return (PDoBlock (map addGuard qs ++
925− [DoExp fc (PApp fc (PRef fc (sUN "return"))
926− [pexp pat])]))
927− <?> "list comprehension"
928− where addGuard :: PDo -> PDo
929− addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (sUN "guard"))
930− [pexp e])
931− addGuard x = x
891+@
892+ExprList ::=
893+ Expr
894+ | Expr ',' ExprList
895+ ;
896+@
897+ -}
898+listExpr :: SyntaxInfo -> IdrisParser PTerm
899+listExpr syn = do lchar '['; fc <- getFC;
900+ try (lchar ']' *> return (mkList fc [])) <|> (do
901+ x <- expr syn
902+ (do try (lchar '|')
903+ qs <- sepBy1 (do_ syn) (lchar ',')
904+ lchar ']'
905+ return (PDoBlock (map addGuard qs ++
906+ [DoExp fc (PApp fc (PRef fc (sUN "return"))
907+ [pexp x])]))) <|> (do
908+ xs <- many (lchar ',' *> expr syn)
909+ lchar ']'
910+ return (mkList fc (x:xs))))
911+ <?> "list expression"
912+ where
913+ mkList :: FC -> [PTerm] -> PTerm
914+ mkList fc [] = PRef fc (sUN "Nil")
915+ mkList fc (x : xs) = PApp fc (PRef fc (sUN "::")) [pexp x, pexp (mkList fc xs)]
916+ addGuard :: PDo -> PDo
917+ addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (sUN "guard"))
918+ [pexp e])
919+ addGuard x = x
932920
933921{- | Parses a do-block
934922@
@@ -1060,11 +1048,11 @@ constant = do reserved "Integer"; return (AType (ATInt ITBig))
10601048 <|> do reserved "Bits16x8"; return (AType (ATInt (ITVec IT16 8)))
10611049 <|> do reserved "Bits32x4"; return (AType (ATInt (ITVec IT32 4)))
10621050 <|> do reserved "Bits64x2"; return (AType (ATInt (ITVec IT64 2)))
1063− <|> try (do f <- float; return $ Fl f)
1064− <|> try (do i <- natural; return $ BI i)
1065− <|> try (do s <- verbatimStringLiteral; return $ Str s)
1066− <|> try (do s <- stringLiteral; return $ Str s)
1067− <|> try (do c <- charLiteral; return $ Ch c)
1051+ <|> do f <- try float; return $ Fl f
1052+ <|> do i <- natural; return $ BI i
1053+ <|> do s <- verbatimStringLiteral; return $ Str s
1054+ <|> do s <- stringLiteral; return $ Str s
1055+ <|> do c <- try charLiteral; return $ Ch c --Currently ambigous with symbols
10681056 <?> "constant or literal"
10691057
10701058{- | Parses a verbatim multi-line string literal (triple-quoted)
@@ -1076,7 +1064,7 @@ VerbatimString_t ::=
10761064@
10771065 -}
10781066verbatimStringLiteral :: MonadicParsing m => m String
1079−verbatimStringLiteral = token $ do string "\"\"\""
1067+verbatimStringLiteral = token $ do try $ string "\"\"\""
10801068 manyTill anyChar $ try (string "\"\"\"")
10811069
10821070{- | Parses a static modifier