@@ -4,7 +4,7 @@ module Idris.Parser where
44import Prelude hiding (pi)
55
66import Text.Trifecta.Delta
7−import Text.Trifecta hiding (span, token, whiteSpace, stringLiteral, charLiteral, natural, symbol, char, string)
7+import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)
88import Text.Parser.LookAhead
99import Text.Parser.Expression
1010import qualified Text.Parser.Token as Tok
@@ -56,15 +56,18 @@ import System.FilePath
5656
5757
5858-- | Idris parser with state used during parsing
59−type IdrisParser = StateT IState Parser
59+type IdrisParser = StateT IState IdrisInnerParser
60+
61+newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }
62+ deriving (Monad, Functor, MonadPlus, Applicative, Alternative, CharParsing, LookAheadParsing, Parsing, DeltaParsing, MarkParsing Delta, Monoid)
63+
64+instance TokenParsing IdrisInnerParser where
65+ someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
6066
6167-- | Generalized monadic parsing constraint type
6268type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)
6369
6470{- * Space, comments and literals (token/lexing like parsers) -}
65−-- | Parses a token by applying parser and then consuming all following whiteSpace
66−lexeme :: MonadicParsing m => m a -> m a
67−lexeme p = p <* whiteSpace
6871
6972-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)
7073simpleWhiteSpace :: MonadicParsing m => m ()
@@ -73,9 +76,11 @@ simpleWhiteSpace = satisfy isSpace *> pure ()
7376-- | Checks if a charcter is end of line
7477isEol :: Char -> Bool
7578isEol '\n' = True
76−isEol '\0' = True -- Check eof too
7779isEol _ = False
7880
81+eol :: MonadicParsing m => m ()
82+eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"
83+
7984-- | Checks if a character is a documentation comment marker
8085isDocCommentMarker :: Char -> Bool
8186isDocCommentMarker '|' = True
@@ -88,8 +93,8 @@ isDocCommentMarker _ = False
8893 ;
8994 -}
9095singleLineComment :: MonadicParsing m => m ()
91−singleLineComment = try (string "--" *> satisfy isEol *> pure ())
92− <|> string "--" *> satisfy (not . isDocCommentMarker) *> many (satisfy (not . isEol)) *> (satisfy isEol <?> "end of line") *> pure ()
96+singleLineComment = try (string "--" *> eol *> pure ())
97+ <|> string "--" *> satisfy (not . isDocCommentMarker) *> many (satisfy (not . isEol)) *> eol *> pure ()
9398 <?> ""
9499
95100{- | Consumes a multi-line comment
@@ -129,33 +134,33 @@ docComment :: MonadicParsing m => Char -> m String
129134docComment marker | isDocCommentMarker marker = do dc <- docComment' marker; return (T.unpack $ T.strip $ T.pack dc)
130135 | otherwise = fail "internal error: tried to parse a documentation comment with invalid marker"
131136 where docComment' :: MonadicParsing m => Char -> m String
132− docComment' marker = string "--" *> char marker *> many (satisfy (not . isEol)) <* satisfy isEol
137+ docComment' marker = string "--" *> char marker *> many (satisfy (not . isEol)) <* eol
133138 <|> string "{-" *> char marker *> (manyTill anyChar (try (string "-}")) <?> "end of comment")
134139 <?> ""
135140
136−-- | Consumes whitespace (and comments)
141+-- | Parses some white space
137142whiteSpace :: MonadicParsing m => m ()
138−whiteSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
143+whiteSpace = Tok.whiteSpace
139144
140145-- | Parses a string literal
141146stringLiteral :: MonadicParsing m => m String
142−stringLiteral = lexeme $ Tok.stringLiteral
147+stringLiteral = Tok.stringLiteral
143148
144149-- | Parses a char literal
145150charLiteral :: MonadicParsing m => m Char
146−charLiteral = lexeme $ Tok.charLiteral
151+charLiteral = Tok.charLiteral
147152
148153-- | Parses a natural number
149154natural :: MonadicParsing m => m Integer
150−natural = lexeme $ Tok.natural
155+natural = Tok.natural
151156
152157-- | Parses an integral number
153158integer :: MonadicParsing m => m Integer
154−integer = lexeme $ Tok.integer
159+integer = Tok.integer
155160
156161-- | Parses a floating point number
157162float :: MonadicParsing m => m Double
158−float = lexeme $ Tok.double
163+float = Tok.double
159164
160165{- * Symbols, identifiers, names and operators -}
161166
@@ -184,28 +189,28 @@ char = Chr.char
184189string :: MonadicParsing m => String -> m String
185190string = Chr.string
186191
187−-- | Parses a character as a lexeme
192+-- | Parses a character as a token
188193lchar :: MonadicParsing m => Char -> m Char
189−lchar = lexeme . char
194+lchar = token . char
190195
191−-- | Parses string as a lexeme
196+-- | Parses string as a token
192197symbol :: MonadicParsing m => String -> m String
193−symbol = lexeme . Tok.symbol
198+symbol = Tok.symbol
194199
195200-- | Parses a reserved identifier
196201reserved :: MonadicParsing m => String -> m ()
197−reserved = lexeme . Tok.reserve idrisStyle
202+reserved = Tok.reserve idrisStyle
198203
199204-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007
200205-- | Parses a reserved operator
201206reservedOp :: MonadicParsing m => String -> m ()
202−reservedOp name = lexeme $ try $
207+reservedOp name = token $ try $
203208 do string name
204209 notFollowedBy (operatorLetter) <?> ("end of " ++ show name)
205210
206−-- | Parses an identifier as a lexeme
211+-- | Parses an identifier as a token
207212identifier :: MonadicParsing m => m String
208−identifier = lexeme $ Tok.ident idrisStyle
213+identifier = token $ Tok.ident idrisStyle
209214
210215-- | Parses an identifier with possible namespace as a name
211216iName :: MonadicParsing m => [String] -> m Name
@@ -259,7 +264,9 @@ operatorLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
259264
260265-- | Parses an operator
261266operator :: MonadicParsing m => m String
262−operator = lexeme . some $ operatorLetter
267+operator = do op <- token . some $ operatorLetter
268+ when (op == ":") $ fail "(:) is not a valid operator"
269+ return op
263270
264271{- * Position helpers -}
265272{- | Get filename from position (returns "(interactive)" when no source file is given) -}
@@ -685,22 +692,25 @@ fnDecl syn
685692 ;
686693-}
687694fnDecl' :: SyntaxInfo -> IdrisParser PDecl
688−fnDecl' syn = try (do doc <- option "" (docComment '|')
689− pushIndent
690− ist <- get
691− let initOpts = if default_total ist
692− then [TotalFn]
693− else []
694− opts <- fnOpts initOpts
695− acc <- optional accessibility
696− opts' <- fnOpts opts
697− n_in <- fnName
698− let n = expandNS syn n_in
699− fc <- getFC
700− ty <- typeSig (allowImp syn)
701− terminator
702− addAcc n acc
703− return (PTy doc syn fc opts' n ty))
695+fnDecl' syn = do (doc, fc, opts', n, acc) <- try (do
696+ doc <- option "" (docComment '|')
697+ pushIndent
698+ ist <- get
699+ let initOpts = if default_total ist
700+ then [TotalFn]
701+ else []
702+ opts <- fnOpts initOpts
703+ acc <- optional accessibility
704+ opts' <- fnOpts opts
705+ n_in <- fnName
706+ let n = expandNS syn n_in
707+ fc <- getFC
708+ lchar ':'
709+ return (doc, fc, opts', n, acc))
710+ ty <- typeExpr (allowImp syn)
711+ terminator
712+ addAcc n acc
713+ return (PTy doc syn fc opts' n ty)
704714 <|> postulate syn
705715 <|> caf syn
706716 <|> pattern syn
@@ -790,7 +800,8 @@ postulate syn = do doc <- try $ do doc <- option "" (docComment '|')
790800 opts' <- fnOpts opts
791801 n_in <- fnName
792802 let n = expandNS syn n_in
793− ty <- typeSig (allowImp syn)
803+ lchar ':'
804+ ty <- typeExpr (allowImp syn)
794805 fc <- getFC
795806 terminator
796807 addAcc n acc
@@ -1187,7 +1198,6 @@ SimpleExpr ::=
11871198 | '(' Bracketed
11881199 | Constant
11891200 | Type
1190− | '()'
11911201 | '_|_'
11921202 | '_'
11931203 | {- External (User-defined) Simple Expression -}
@@ -1212,15 +1222,12 @@ simpleExpr syn =
12121222 <|> try (comprehension syn)
12131223 <|> try (alt syn)
12141224 <|> try (idiom syn)
1215− <|> try (do lchar '('
1216− bracketed (disallowImp syn))
1225+ <|> do lchar '('
1226+ bracketed (disallowImp syn)
12171227 <|> try (do c <- constant
12181228 fc <- getFC
12191229 return (modifyConst syn fc (PConstant c)))
12201230 <|> do reserved "Type"; return PType
1221− <|> try (do symbol "()"
1222− fc <- getFC
1223− return (PTrue fc))
12241231 <|> try (do symbol "_|_"
12251232 fc <- getFC
12261233 return (PFalse fc))
@@ -1231,25 +1238,62 @@ simpleExpr syn =
12311238
12321239{- |Parses the rest of an expression in braces
12331240Bracketed ::=
1234− | Pair
1241+ ')'
12351242 | Expr ')'
1243+ | ExprList ')'
1244+ | Expr '**' Expr ')'
12361245 | Operator Expr ')'
12371246 | Expr Operator ')'
1247+ | Name ':' Expr '**' Expr ')'
12381248 ;
12391249-}
12401250bracketed :: SyntaxInfo -> IdrisParser PTerm
12411251bracketed syn =
1242− try (pair syn)
1243− <|> try (do e <- expr syn; lchar ')'; return e)
1244− <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
1245− return $ PLam (MN 1000 "ARG") Placeholder
1246− (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")),
1252+ do lchar ')'
1253+ fc <- getFC
1254+ return $ PTrue fc
1255+ <|>
1256+ try (do l <- expr syn
1257+ lchar ')'
1258+ return l)
1259+ <|> do (l, fc) <- try (do
1260+ l <- expr syn
1261+ fc <- getFC
1262+ lchar ','
1263+ return (l, fc))
1264+ rs <- sepBy1 (do fc' <- getFC; r <- expr syn; return (r, fc')) (lchar ',')
1265+ lchar ')'
1266+ return $ PPair fc l (mergePairs rs)
1267+ <|> do (l, fc) <- try (do
1268+ l <- expr syn
1269+ fc <- getFC
1270+ reservedOp "**"
1271+ return (l, fc))
1272+ r <- expr syn
1273+ lchar ')'
1274+ return (PDPair fc l Placeholder r)
1275+ <|> try(do fc0 <- getFC
1276+ l <- simpleExpr syn
1277+ o <- operator
1278+ lchar ')'
1279+ return $ PLam (MN 1000 "ARG") Placeholder
1280+ (PApp fc0 (PRef fc0 (UN o)) [pexp l,
1281+ pexp (PRef fc0 (MN 1000 "ARG"))]))
1282+ <|> try(do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
1283+ return $ PLam (MN 1000 "ARG") Placeholder
1284+ (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")),
12471285 pexp e]))
1248− <|> try (do fc <- getFC; e <- simpleExpr syn; o <- operator; lchar ')'
1249− return $ PLam (MN 1000 "ARG") Placeholder
1250− (PApp fc (PRef fc (UN o)) [pexp e,
1251− pexp (PRef fc (MN 1000 "ARG"))]))
1252− <?> "end of expression in braces"
1286+ <|> try (do ln <- name; lchar ':'
1287+ lty <- expr syn
1288+ reservedOp "**"
1289+ fc <- getFC
1290+ r <- expr syn
1291+ lchar ')'
1292+ return (PDPair fc (PRef fc ln) lty r))
1293+ <?> "end of braced expression"
1294+ where mergePairs :: [(PTerm, FC)] -> PTerm
1295+ mergePairs [(t, fc)] = t
1296+ mergePairs ((t, fc):rs) = PPair fc t (mergePairs rs)
12531297
12541298-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a
12551299-- big integer, otherwise try fromInteger and the constants as alternatives.
@@ -1293,62 +1337,6 @@ listExpr syn = do lchar '['; fc <- getFC; xs <- sepBy (expr syn) (lchar ','); lc
12931337 mkList fc [] = PRef fc (UN "Nil")
12941338 mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
12951339
1296−{- | Parses rest of pair expression
1297−Pair ::=
1298− Expr RestTuple? ')'
1299− | NTuple ')'
1300− | Name ':' Expr '**' 'Expr' ')'
1301− ;
1302−
1303−RestTuple ::=
1304− ',' Expr
1305− | '**' Expr
1306− ;
1307−
1308−NTuple ::=
1309− Expr ',' Expr
1310− | Expr ',' NTuple
1311− ;
1312−-}
1313−pair :: SyntaxInfo -> IdrisParser PTerm
1314−pair syn = try (do l <- expr syn
1315− fc <- getFC
1316− rest <- restTuple
1317− case rest of
1318− [] -> return l
1319− [Left r] -> return (PPair fc l r)
1320− [Right r] -> return (PDPair fc l Placeholder r))
1321− <|> try (do x <- ntuple
1322− lchar ')'
1323− return x)
1324− <|> do ln <- name; lchar ':'
1325− lty <- expr syn
1326− reservedOp "**"
1327− fc <- getFC
1328− r <- expr syn
1329− lchar ')'
1330− return (PDPair fc (PRef fc ln) lty r)
1331− <?> "pair expression"
1332− where
1333− restTuple :: IdrisParser [Either PTerm PTerm]
1334− restTuple = do lchar ')'; return []
1335− <|> do lchar ','
1336− r <- expr syn
1337− lchar ')'
1338− return [Left r]
1339− <|> do reservedOp "**"
1340− r <- expr syn
1341− lchar ')'
1342− return [Right r]
1343− <?> "end of pair expression"
1344− ntuple :: IdrisParser PTerm
1345− ntuple = try (do l <- expr syn; fc <- getFC; lchar ','
1346− rest <- ntuple
1347− return (PPair fc l rest))
1348− <|> (do l <- expr syn; fc <- getFC; lchar ','
1349− r <- expr syn
1350− return (PPair fc l r))
1351− <?> "tuple expression"
13521340
13531341{- | Parses an alternative expression
13541342 Alt ::= '(|' Expr_List '|)';
@@ -1524,15 +1512,10 @@ mkType (UN n) = UN ("set_" ++ n)
15241512mkType (MN 0 n) = MN 0 ("set_" ++ n)
15251513mkType (NS n s) = NS (mkType n) s
15261514
1527−{- |Parses a type for an expression
1515+{- |Parses a type signature
15281516TypeSig ::=
15291517 ':' Expr
15301518 ;
1531−-}
1532−typeSig :: SyntaxInfo -> IdrisParser PTerm
1533−typeSig syn = lchar ':' *> typeExpr syn <?> "type"
1534−
1535−{- |Parses a type signature
15361519TypeExpr ::= ConstraintList? Expr;
15371520 -}
15381521typeExpr :: SyntaxInfo -> IdrisParser PTerm
@@ -1633,50 +1616,48 @@ Pi ::=
16331616 | '{' 'static' '}' Expr' '->' Expr
16341617 ;
16351618 -}
1619+
1620+pi :: SyntaxInfo -> IdrisParser PTerm
16361621pi syn =
1637− try (do lazy <- if implicitAllowed syn -- laziness is top level only
1638− then option False (do lchar '|'; return True)
1639− else return False
1640− st <- static
1641− lchar '('; xt <- typeDeclList syn; lchar ')'
1642− doc <- option "" (docComment '^')
1643− symbol "->"
1644− sc <- expr syn
1645− return (bindList (PPi (Exp lazy st doc)) xt sc))
1646− <|> try (if implicitAllowed syn
1647− then do lazy <- option False (do lchar '|'
1648− return True)
1649− st <- static
1650− lchar '{'
1651− xt <- typeDeclList syn
1652− lchar '}'
1653− symbol "->"
1654− sc <- expr syn
1655− return (bindList (PPi (Imp lazy st "")) xt sc)
1656− else fail "no implicit arguments allowed here")
1657− <|> try (do lchar '{'
1658− reserved "auto"
1659− xt <- typeDeclList syn
1660− lchar '}'
1661− symbol "->"
1662− sc <- expr syn
1663− return (bindList (PPi
1664− (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))
1665− <|> try (do lchar '{'
1666− reserved "default"
1667− script <- simpleExpr syn
1668− xt <- typeDeclList syn
1669− lchar '}'
1670− symbol "->"
1671− sc <- expr syn
1672− return (bindList (PPi (TacImp False Dynamic script "")) xt sc))
1673− <|> do lchar '{'
1674− reserved "static"
1675− lchar '}'
1676− t <- expr' syn
1677− symbol "->"
1678− sc <- expr syn
1679− return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)
1622+ do lazy <- if implicitAllowed syn -- laziness is top level only
1623+ then option False (do lchar '|'; return True)
1624+ else return False
1625+ st <- static
1626+ (do try(lchar '('); xt <- typeDeclList syn; lchar ')'
1627+ doc <- option "" (docComment '^')
1628+ symbol "->"
1629+ sc <- expr syn
1630+ return (bindList (PPi (Exp lazy st doc)) xt sc)) <|> (do
1631+ lchar '{'
1632+ (do reserved "auto"
1633+ when (lazy || (st == Static)) $ fail "auto type constraints can not be lazy or static"
1634+ xt <- typeDeclList syn
1635+ lchar '}'
1636+ symbol "->"
1637+ sc <- expr syn
1638+ return (bindList (PPi
1639+ (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc)) <|> (do
1640+ reserved "default"
1641+ when (lazy || (st == Static)) $ fail "default tactic constraints can not be lazy or static"
1642+ script <- simpleExpr syn
1643+ xt <- typeDeclList syn
1644+ lchar '}'
1645+ symbol "->"
1646+ sc <- expr syn
1647+ return (bindList (PPi (TacImp False Dynamic script "")) xt sc)) <|> (do
1648+ reserved "static"
1649+ lchar '}'
1650+ t <- expr' syn
1651+ symbol "->"
1652+ sc <- expr syn
1653+ return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)) <|> (
1654+ if implicitAllowed syn then do
1655+ xt <- typeDeclList syn
1656+ lchar '}'
1657+ symbol "->"
1658+ sc <- expr syn
1659+ return (bindList (PPi (Imp lazy st "")) xt sc)
1660+ else do fail "no implicit arguments allowed here"))
16801661 <?> "dependent type signature"
16811662
16821663{- | Parses a type constraint list
@@ -1717,7 +1698,8 @@ usingDeclList :: SyntaxInfo -> IdrisParser [Using]
17171698usingDeclList syn
17181699 = try (sepBy1 (usingDecl syn) (lchar ','))
17191700 <|> do ns <- sepBy1 name (lchar ',')
1720− t <- typeSig (disallowImp syn)
1701+ lchar ':'
1702+ t <- typeExpr (disallowImp syn)
17211703 return (map (\x -> UImplicit x t) ns)
17221704 <?> "using declaration list"
17231705
@@ -1729,7 +1711,8 @@ UsingDecl ::=
17291711-}
17301712usingDecl :: SyntaxInfo -> IdrisParser Using
17311713usingDecl syn = try (do x <- fnName
1732− t <- typeSig (disallowImp syn)
1714+ lchar ':'
1715+ t <- typeExpr (disallowImp syn)
17331716 return (UImplicit x t))
17341717 <|> do c <- fnName
17351718 xs <- some fnName
@@ -1749,11 +1732,13 @@ FunctionSignatureList ::=
17491732-}
17501733typeDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
17511734typeDeclList syn = try (sepBy1 (do x <- fnName
1752− t <- typeSig (disallowImp syn)
1735+ lchar ':'
1736+ t <- typeExpr (disallowImp syn)
17531737 return (x,t))
17541738 (lchar ','))
17551739 <|> do ns <- sepBy1 name (lchar ',')
1756− t <- typeSig (disallowImp syn)
1740+ lchar ':'
1741+ t <- typeExpr (disallowImp syn)
17571742 return (map (\x -> (x, t)) ns)
17581743 <?> "type declaration list"
17591744
@@ -1934,7 +1919,8 @@ record syn = do (doc, acc) <- try (do
19341919 return (doc, acc))
19351920 fc <- getFC
19361921 tyn_in <- fnName
1937− ty <- typeSig (allowImp syn)
1922+ lchar ':'
1923+ ty <- typeExpr (allowImp syn)
19381924 let tyn = expandNS syn tyn_in
19391925 reserved "where"
19401926 (cdoc, cn, cty, _) <- indentedBlockS (constructor syn)
@@ -1978,24 +1964,23 @@ SimpleConstructorList ::=
19781964 ;
19791965-}
19801966data_ :: SyntaxInfo -> IdrisParser PDecl
1981−data_ syn = try (do doc <- option "" (docComment '|')
1982− acc <- optional accessibility
1983− co <- dataI
1984− fc <- getFC
1985− tyn_in <- fnName
1986− ty <- typeSig (allowImp syn)
1987− let tyn = expandNS syn tyn_in
1988− option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1989− reserved "where"
1990− cons <- indentedBlock (constructor syn)
1991− accData acc tyn (map (\ (_, n, _, _) -> n) cons)
1992− return $ PData doc syn fc co (PDatadecl tyn ty cons)))
1993− <|> try (do doc <- option "" (docComment '|')
1967+data_ syn = do (doc, acc, co) <- try (do
1968+ doc <- option "" (docComment '|')
19941969 pushIndent
19951970 acc <- optional accessibility
19961971 co <- dataI
1997− fc <- getFC
1998− tyn_in <- fnName
1972+ return (doc, acc, co))
1973+ fc <- getFC
1974+ tyn_in <- fnName
1975+ (do try (lchar ':')
1976+ popIndent
1977+ ty <- typeExpr (allowImp syn)
1978+ let tyn = expandNS syn tyn_in
1979+ option (PData doc syn fc co (PLaterdecl tyn ty)) (do
1980+ reserved "where"
1981+ cons <- indentedBlock (constructor syn)
1982+ accData acc tyn (map (\ (_, n, _, _) -> n) cons)
1983+ return $ PData doc syn fc co (PDatadecl tyn ty cons))) <|> (do
19991984 args <- many name
20001985 let ty = bindArgs (map (const PType) args) PType
20011986 let tyn = expandNS syn tyn_in
@@ -2019,7 +2004,7 @@ data_ syn = try (do doc <- option "" (docComment '|')
20192004 return (doc, x, cty, cfc)) cons
20202005 accData acc tyn (map (\ (_, n, _, _) -> n) cons')
20212006 return $ PData doc syn fc co (PDatadecl tyn ty cons')))
2022− <?> "data type declaration"
2007+ <?> "data type declaration"
20232008 where
20242009 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm
20252010 mkPApp fc t [] = t
@@ -2036,7 +2021,8 @@ constructor syn
20362021 = do doc <- option "" (docComment '|')
20372022 cn_in <- fnName; fc <- getFC
20382023 let cn = expandNS syn cn_in
2039− ty <- typeSig (allowImp syn)
2024+ lchar ':'
2025+ ty <- typeExpr (allowImp syn)
20402026 return (doc, cn, ty, fc)
20412027 <?> "constructor"
20422028
@@ -2414,7 +2400,7 @@ Provider ::= '%' 'provide' '(' FnName TypeSig ')' 'with' Expr;
24142400 -}
24152401provider :: SyntaxInfo -> IdrisParser [PDecl]
24162402provider syn = do try (lchar '%' *> reserved "provide");
2417− lchar '('; n <- fnName; t <- typeSig syn; lchar ')'
2403+ lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
24182404 fc <- getFC
24192405 reserved "with"
24202406 e <- expr syn
@@ -2553,17 +2539,17 @@ fullTactic syn = do t <- tactic syn
25532539{- * Loading and parsing -}
25542540{- | Parses an expression from input -}
25552541parseExpr :: IState -> String -> Result PTerm
2556−parseExpr st = parseString (evalStateT (fullExpr defaultSyntax) st) (Directed (UTF8.fromString "(input)") 0 0 0 0)
2542+parseExpr st = parseString (runInnerParser (evalStateT (fullExpr defaultSyntax) st)) (Directed (UTF8.fromString "(input)") 0 0 0 0)
25572543
25582544{- | Parses a tactic from input -}
25592545parseTactic :: IState -> String -> Result PTactic
2560−parseTactic st = parseString (evalStateT (fullTactic defaultSyntax) st) (Directed (UTF8.fromString "(input)") 0 0 0 0)
2546+parseTactic st = parseString (runInnerParser (evalStateT (fullTactic defaultSyntax) st)) (Directed (UTF8.fromString "(input)") 0 0 0 0)
25612547
25622548-- | Parse module header and imports
25632549parseImports :: FilePath -> String -> Idris ([String], [String], Maybe Delta)
25642550parseImports fname input
25652551 = do i <- getIState
2566− case parseString (evalStateT imports i) (Directed (UTF8.fromString fname) 0 0 0 0) input of
2552+ case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
25672553 Failure err -> fail (show err)
25682554 Success (x, i) -> do -- Discard state updates (there should be
25692555 -- none anyway)
@@ -2587,7 +2573,7 @@ parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
25872573 Idris [PDecl]
25882574parseProg syn fname input mrk
25892575 = do i <- getIState
2590− case parseString (evalStateT mainProg i) (Directed (UTF8.fromString fname) 0 0 0 0) input of
2576+ case parseString (runInnerParser (evalStateT mainProg i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
25912577 Failure doc -> do iputStrLn (show doc)
25922578 -- FIXME: Get error location from trifecta
25932579 --let errl = sourceLine (errorPos err)