d8a8fcf · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #506 from ahmadsalim/master

d8a8fcfEdwin Brady13 years ago

idris.cabal+1−1

compare with master

unifiedsplit

@@ -367,7 +367,7 @@ Executable idris

367 , text

368 , time >= 1.4

369 , transformers

370− , trifecta >= 1.1

370+ , trifecta == 1.1

371 , unordered-containers

372 , utf8-string

373 , vector

src/Idris/Parser.hs+177−191

@@ -4,7 +4,7 @@ module Idris.Parser where

4import Prelude hiding (pi)

6import 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)

8import Text.Parser.LookAhead

9import Text.Parser.Expression

10import qualified Text.Parser.Token as Tok

@@ -56,15 +56,18 @@ import System.FilePath

58-- | 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 ()

61-- | Generalized monadic parsing constraint type

67-- | Generalized monadic parsing constraint type

62type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)

68type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)

64{- * Space, comments and literals (token/lexing like parsers) -}

70{- * 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

69-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)

72-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)

70simpleWhiteSpace :: MonadicParsing m => m ()

73simpleWhiteSpace :: MonadicParsing m => m ()

@@ -73,9 +76,11 @@ simpleWhiteSpace = satisfy isSpace *> pure ()

73-- | Checks if a charcter is end of line

76-- | Checks if a charcter is end of line

74isEol :: Char -> Bool

77isEol :: Char -> Bool

75isEol '\n' = True

78isEol '\n' = True

76−isEol '\0' = True -- Check eof too

77isEol _ = False

79isEol _ = False

81+eol :: MonadicParsing m => m ()

82+eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"

83+

79-- | Checks if a character is a documentation comment marker

84-- | Checks if a character is a documentation comment marker

80isDocCommentMarker :: Char -> Bool

85isDocCommentMarker :: Char -> Bool

81isDocCommentMarker '|' = True

86isDocCommentMarker '|' = True

@@ -88,8 +93,8 @@ isDocCommentMarker _ = False

88 ;

93 ;

89 -}

94 -}

90singleLineComment :: MonadicParsing m => m ()

95singleLineComment :: MonadicParsing m => m ()

91−singleLineComment = try (string "--" *> satisfy isEol *> pure ())

96+singleLineComment = try (string "--" *> eol *> pure ())

92− <|> string "--" *> satisfy (not . isDocCommentMarker) *> many (satisfy (not . isEol)) *> (satisfy isEol <?> "end of line") *> pure ()

97+ <|> string "--" *> satisfy (not . isDocCommentMarker) *> many (satisfy (not . isEol)) *> eol *> pure ()

93 <?> ""

98 <?> ""

95{- | Consumes a multi-line comment

100{- | Consumes a multi-line comment

@@ -129,33 +134,33 @@ docComment :: MonadicParsing m => Char -> m String

129docComment marker | isDocCommentMarker marker = do dc <- docComment' marker; return (T.unpack $ T.strip $ T.pack dc)

134docComment marker | isDocCommentMarker marker = do dc <- docComment' marker; return (T.unpack $ T.strip $ T.pack dc)

130 | otherwise = fail "internal error: tried to parse a documentation comment with invalid marker"

135 | otherwise = fail "internal error: tried to parse a documentation comment with invalid marker"

131 where docComment' :: MonadicParsing m => Char -> m String

136 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

133 <|> string "{-" *> char marker *> (manyTill anyChar (try (string "-}")) <?> "end of comment")

138 <|> string "{-" *> char marker *> (manyTill anyChar (try (string "-}")) <?> "end of comment")

134 <?> ""

139 <?> ""

135

140

136−-- | Consumes whitespace (and comments)

141+-- | Parses some white space

137whiteSpace :: MonadicParsing m => m ()

142whiteSpace :: MonadicParsing m => m ()

138−whiteSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

143+whiteSpace = Tok.whiteSpace

139

144

140-- | Parses a string literal

145-- | Parses a string literal

141stringLiteral :: MonadicParsing m => m String

146stringLiteral :: MonadicParsing m => m String

142−stringLiteral = lexeme $ Tok.stringLiteral

147+stringLiteral = Tok.stringLiteral

143

148

144-- | Parses a char literal

149-- | Parses a char literal

145charLiteral :: MonadicParsing m => m Char

150charLiteral :: MonadicParsing m => m Char

146−charLiteral = lexeme $ Tok.charLiteral

151+charLiteral = Tok.charLiteral

147

152

148-- | Parses a natural number

153-- | Parses a natural number

149natural :: MonadicParsing m => m Integer

154natural :: MonadicParsing m => m Integer

150−natural = lexeme $ Tok.natural

155+natural = Tok.natural

151

156

152-- | Parses an integral number

157-- | Parses an integral number

153integer :: MonadicParsing m => m Integer

158integer :: MonadicParsing m => m Integer

154−integer = lexeme $ Tok.integer

159+integer = Tok.integer

155

160

156-- | Parses a floating point number

161-- | Parses a floating point number

157float :: MonadicParsing m => m Double

162float :: MonadicParsing m => m Double

158−float = lexeme $ Tok.double

163+float = Tok.double

159

164

160{- * Symbols, identifiers, names and operators -}

165{- * Symbols, identifiers, names and operators -}

161

166

@@ -184,28 +189,28 @@ char = Chr.char

184string :: MonadicParsing m => String -> m String

189string :: MonadicParsing m => String -> m String

185string = Chr.string

190string = Chr.string

186

191

187−-- | Parses a character as a lexeme

192+-- | Parses a character as a token

188lchar :: MonadicParsing m => Char -> m Char

193lchar :: MonadicParsing m => Char -> m Char

189−lchar = lexeme . char

194+lchar = token . char

190

195

191−-- | Parses string as a lexeme

196+-- | Parses string as a token

192symbol :: MonadicParsing m => String -> m String

197symbol :: MonadicParsing m => String -> m String

193−symbol = lexeme . Tok.symbol

198+symbol = Tok.symbol

194

199

195-- | Parses a reserved identifier

200-- | Parses a reserved identifier

196reserved :: MonadicParsing m => String -> m ()

201reserved :: MonadicParsing m => String -> m ()

197−reserved = lexeme . Tok.reserve idrisStyle

202+reserved = Tok.reserve idrisStyle

198

203

199-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007

204-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007

200-- | Parses a reserved operator

205-- | Parses a reserved operator

201reservedOp :: MonadicParsing m => String -> m ()

206reservedOp :: MonadicParsing m => String -> m ()

202−reservedOp name = lexeme $ try $

207+reservedOp name = token $ try $

203 do string name

208 do string name

204 notFollowedBy (operatorLetter) <?> ("end of " ++ show name)

209 notFollowedBy (operatorLetter) <?> ("end of " ++ show name)

205

210

206−-- | Parses an identifier as a lexeme

211+-- | Parses an identifier as a token

207identifier :: MonadicParsing m => m String

212identifier :: MonadicParsing m => m String

208−identifier = lexeme $ Tok.ident idrisStyle

213+identifier = token $ Tok.ident idrisStyle

209

214

210-- | Parses an identifier with possible namespace as a name

215-- | Parses an identifier with possible namespace as a name

211iName :: MonadicParsing m => [String] -> m Name

216iName :: MonadicParsing m => [String] -> m Name

@@ -259,7 +264,9 @@ operatorLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"

259

264

260-- | Parses an operator

265-- | Parses an operator

261operator :: MonadicParsing m => m String

266operator :: 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

263

270

264{- * Position helpers -}

271{- * Position helpers -}

265{- | Get filename from position (returns "(interactive)" when no source file is given) -}

272{- | Get filename from position (returns "(interactive)" when no source file is given) -}

@@ -685,22 +692,25 @@ fnDecl syn

685 ;

692 ;

686-}

693-}

687fnDecl' :: SyntaxInfo -> IdrisParser PDecl

694fnDecl' :: SyntaxInfo -> IdrisParser PDecl

695+fnDecl' syn = do (doc, fc, opts', n, acc) <- try (do

688−fnDecl' syn = try (do doc <- option "" (docComment '|')

696+ doc <- option "" (docComment '|')

689− pushIndent

697+ pushIndent

690− ist <- get

698+ ist <- get

691− let initOpts = if default_total ist

699+ let initOpts = if default_total ist

692− then [TotalFn]

700+ then [TotalFn]

693− else []

701+ else []

694− opts <- fnOpts initOpts

702+ opts <- fnOpts initOpts

695− acc <- optional accessibility

703+ acc <- optional accessibility

696− opts' <- fnOpts opts

704+ opts' <- fnOpts opts

697− n_in <- fnName

705+ n_in <- fnName

698− let n = expandNS syn n_in

706+ let n = expandNS syn n_in

699− fc <- getFC

707+ fc <- getFC

708+ lchar ':'

709+ return (doc, fc, opts', n, acc))

700− ty <- typeSig (allowImp syn)

710+ ty <- typeExpr (allowImp syn)

701− terminator

711+ terminator

702− addAcc n acc

712+ addAcc n acc

703− return (PTy doc syn fc opts' n ty))

713+ return (PTy doc syn fc opts' n ty)

704 <|> postulate syn

714 <|> postulate syn

705 <|> caf syn

715 <|> caf syn

706 <|> pattern syn

716 <|> pattern syn

@@ -790,7 +800,8 @@ postulate syn = do doc <- try $ do doc <- option "" (docComment '|')

790 opts' <- fnOpts opts

800 opts' <- fnOpts opts

791 n_in <- fnName

801 n_in <- fnName

792 let n = expandNS syn n_in

802 let n = expandNS syn n_in

803+ lchar ':'

793− ty <- typeSig (allowImp syn)

804+ ty <- typeExpr (allowImp syn)

794 fc <- getFC

805 fc <- getFC

795 terminator

806 terminator

796 addAcc n acc

807 addAcc n acc

@@ -1187,7 +1198,6 @@ SimpleExpr ::=

1187 | '(' Bracketed

1198 | '(' Bracketed

1188 | Constant

1199 | Constant

1189 | Type

1200 | Type

1190− | '()'

1191 | '_|_'

1201 | '_|_'

1192 | '_'

1202 | '_'

1193 | {- External (User-defined) Simple Expression -}

1203 | {- External (User-defined) Simple Expression -}

@@ -1212,15 +1222,12 @@ simpleExpr syn =

1212 <|> try (comprehension syn)

1222 <|> try (comprehension syn)

1213 <|> try (alt syn)

1223 <|> try (alt syn)

1214 <|> try (idiom syn)

1224 <|> try (idiom syn)

1215− <|> try (do lchar '('

1225+ <|> do lchar '('

1216− bracketed (disallowImp syn))

1226+ bracketed (disallowImp syn)

1217 <|> try (do c <- constant

1227 <|> try (do c <- constant

1218 fc <- getFC

1228 fc <- getFC

1219 return (modifyConst syn fc (PConstant c)))

1229 return (modifyConst syn fc (PConstant c)))

1220 <|> do reserved "Type"; return PType

1230 <|> do reserved "Type"; return PType

1221− <|> try (do symbol "()"

1222− fc <- getFC

1223− return (PTrue fc))

1224 <|> try (do symbol "_|_"

1231 <|> try (do symbol "_|_"

1225 fc <- getFC

1232 fc <- getFC

1226 return (PFalse fc))

1233 return (PFalse fc))

@@ -1231,25 +1238,62 @@ simpleExpr syn =

1231

1238

1232{- |Parses the rest of an expression in braces

1239{- |Parses the rest of an expression in braces

1233Bracketed ::=

1240Bracketed ::=

1234− | Pair

1241+ ')'

1235 | Expr ')'

1242 | Expr ')'

1243+ | ExprList ')'

1244+ | Expr '**' Expr ')'

1236 | Operator Expr ')'

1245 | Operator Expr ')'

1237 | Expr Operator ')'

1246 | Expr Operator ')'

1247+ | Name ':' Expr '**' Expr ')'

1238 ;

1248 ;

1239-}

1249-}

1240bracketed :: SyntaxInfo -> IdrisParser PTerm

1250bracketed :: SyntaxInfo -> IdrisParser PTerm

1241bracketed syn =

1251bracketed syn =

1252+ do lchar ')'

1253+ fc <- getFC

1254+ return $ PTrue fc

1255+ <|>

1242− try (pair syn)

1256+ try (do l <- expr syn

1243− <|> try (do e <- expr syn; lchar ')'; return e)

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"))]))

1244− <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'

1282+ <|> try(do fc <- getFC; o <- operator; e <- expr syn; lchar ')'

1245− return $ PLam (MN 1000 "ARG") Placeholder

1283+ return $ PLam (MN 1000 "ARG") Placeholder

1246− (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")),

1284+ (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")),

1247 pexp e]))

1285 pexp e]))

1248− <|> try (do fc <- getFC; e <- simpleExpr syn; o <- operator; lchar ')'

1286+ <|> try (do ln <- name; lchar ':'

1249− return $ PLam (MN 1000 "ARG") Placeholder

1287+ lty <- expr syn

1250− (PApp fc (PRef fc (UN o)) [pexp e,

1288+ reservedOp "**"

1251− pexp (PRef fc (MN 1000 "ARG"))]))

1289+ fc <- getFC

1290+ r <- expr syn

1291+ lchar ')'

1292+ return (PDPair fc (PRef fc ln) lty r))

1252− <?> "end of expression in braces"

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)

1253

1297

1254-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a

1298-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a

1255-- big integer, otherwise try fromInteger and the constants as alternatives.

1299-- 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

1293 mkList fc [] = PRef fc (UN "Nil")

1337 mkList fc [] = PRef fc (UN "Nil")

1294 mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]

1338 mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]

1295

1339

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"

1352

1340

1353{- | Parses an alternative expression

1341{- | Parses an alternative expression

1354 Alt ::= '(|' Expr_List '|)';

1342 Alt ::= '(|' Expr_List '|)';

@@ -1524,15 +1512,10 @@ mkType (UN n) = UN ("set_" ++ n)

1524mkType (MN 0 n) = MN 0 ("set_" ++ n)

1512mkType (MN 0 n) = MN 0 ("set_" ++ n)

1525mkType (NS n s) = NS (mkType n) s

1513mkType (NS n s) = NS (mkType n) s

1526

1514

1527−{- |Parses a type for an expression

1515+{- |Parses a type signature

1528TypeSig ::=

1516TypeSig ::=

1529 ':' Expr

1517 ':' Expr

1530 ;

1518 ;

1531−-}

1532−typeSig :: SyntaxInfo -> IdrisParser PTerm

1533−typeSig syn = lchar ':' *> typeExpr syn <?> "type"

1534−

1535−{- |Parses a type signature

1536TypeExpr ::= ConstraintList? Expr;

1519TypeExpr ::= ConstraintList? Expr;

1537 -}

1520 -}

1538typeExpr :: SyntaxInfo -> IdrisParser PTerm

1521typeExpr :: SyntaxInfo -> IdrisParser PTerm

@@ -1633,50 +1616,48 @@ Pi ::=

1633 | '{' 'static' '}' Expr' '->' Expr

1616 | '{' 'static' '}' Expr' '->' Expr

1634 ;

1617 ;

1635 -}

1618 -}

1619+

1620+pi :: SyntaxInfo -> IdrisParser PTerm

1636pi syn =

1621pi syn =

1637− try (do lazy <- if implicitAllowed syn -- laziness is top level only

1622+ do lazy <- if implicitAllowed syn -- laziness is top level only

1638− then option False (do lchar '|'; return True)

1623+ then option False (do lchar '|'; return True)

1639− else return False

1624+ else return False

1640− st <- static

1625+ st <- static

1641− lchar '('; xt <- typeDeclList syn; lchar ')'

1626+ (do try(lchar '('); xt <- typeDeclList syn; lchar ')'

1642− doc <- option "" (docComment '^')

1627+ doc <- option "" (docComment '^')

1643− symbol "->"

1628+ symbol "->"

1644− sc <- expr syn

1629+ sc <- expr syn

1645− return (bindList (PPi (Exp lazy st doc)) xt sc))

1630+ return (bindList (PPi (Exp lazy st doc)) xt sc)) <|> (do

1646− <|> try (if implicitAllowed syn

1647− then do lazy <- option False (do lchar '|'

1648− return True)

1649− st <- static

1650− lchar '{'

1631+ lchar '{'

1651− xt <- typeDeclList syn

1632+ (do reserved "auto"

1652− lchar '}'

1633+ when (lazy || (st == Static)) $ fail "auto type constraints can not be lazy or static"

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

1634+ xt <- typeDeclList syn

1660− lchar '}'

1635+ lchar '}'

1661− symbol "->"

1636+ symbol "->"

1662− sc <- expr syn

1637+ sc <- expr syn

1663− return (bindList (PPi

1638+ return (bindList (PPi

1664− (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))

1639+ (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc)) <|> (do

1665− <|> try (do lchar '{'

1640+ reserved "default"

1666− reserved "default"

1641+ when (lazy || (st == Static)) $ fail "default tactic constraints can not be lazy or static"

1667− script <- simpleExpr syn

1642+ script <- simpleExpr syn

1668− xt <- typeDeclList syn

1643+ xt <- typeDeclList syn

1669− lchar '}'

1644+ lchar '}'

1670− symbol "->"

1645+ symbol "->"

1671− sc <- expr syn

1646+ sc <- expr syn

1672− return (bindList (PPi (TacImp False Dynamic script "")) xt sc))

1647+ return (bindList (PPi (TacImp False Dynamic script "")) xt sc)) <|> (do

1673− <|> do lchar '{'

1674− reserved "static"

1648+ reserved "static"

1675− lchar '}'

1649+ lchar '}'

1676− t <- expr' syn

1650+ t <- expr' syn

1677− symbol "->"

1651+ symbol "->"

1678− sc <- expr syn

1652+ sc <- expr syn

1679− return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)

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"))

1680 <?> "dependent type signature"

1661 <?> "dependent type signature"

1681

1662

1682{- | Parses a type constraint list

1663{- | Parses a type constraint list

@@ -1717,7 +1698,8 @@ usingDeclList :: SyntaxInfo -> IdrisParser [Using]

1717usingDeclList syn

1698usingDeclList syn

1718 = try (sepBy1 (usingDecl syn) (lchar ','))

1699 = try (sepBy1 (usingDecl syn) (lchar ','))

1719 <|> do ns <- sepBy1 name (lchar ',')

1700 <|> do ns <- sepBy1 name (lchar ',')

1701+ lchar ':'

1720− t <- typeSig (disallowImp syn)

1702+ t <- typeExpr (disallowImp syn)

1721 return (map (\x -> UImplicit x t) ns)

1703 return (map (\x -> UImplicit x t) ns)

1722 <?> "using declaration list"

1704 <?> "using declaration list"

1723

1705

@@ -1729,7 +1711,8 @@ UsingDecl ::=

1729-}

1711-}

1730usingDecl :: SyntaxInfo -> IdrisParser Using

1712usingDecl :: SyntaxInfo -> IdrisParser Using

1731usingDecl syn = try (do x <- fnName

1713usingDecl syn = try (do x <- fnName

1714+ lchar ':'

1732− t <- typeSig (disallowImp syn)

1715+ t <- typeExpr (disallowImp syn)

1733 return (UImplicit x t))

1716 return (UImplicit x t))

1734 <|> do c <- fnName

1717 <|> do c <- fnName

1735 xs <- some fnName

1718 xs <- some fnName

@@ -1749,11 +1732,13 @@ FunctionSignatureList ::=

1749-}

1732-}

1750typeDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]

1733typeDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]

1751typeDeclList syn = try (sepBy1 (do x <- fnName

1734typeDeclList syn = try (sepBy1 (do x <- fnName

1735+ lchar ':'

1752− t <- typeSig (disallowImp syn)

1736+ t <- typeExpr (disallowImp syn)

1753 return (x,t))

1737 return (x,t))

1754 (lchar ','))

1738 (lchar ','))

1755 <|> do ns <- sepBy1 name (lchar ',')

1739 <|> do ns <- sepBy1 name (lchar ',')

1740+ lchar ':'

1756− t <- typeSig (disallowImp syn)

1741+ t <- typeExpr (disallowImp syn)

1757 return (map (\x -> (x, t)) ns)

1742 return (map (\x -> (x, t)) ns)

1758 <?> "type declaration list"

1743 <?> "type declaration list"

1759

1744

@@ -1934,7 +1919,8 @@ record syn = do (doc, acc) <- try (do

1934 return (doc, acc))

1919 return (doc, acc))

1935 fc <- getFC

1920 fc <- getFC

1936 tyn_in <- fnName

1921 tyn_in <- fnName

1922+ lchar ':'

1937− ty <- typeSig (allowImp syn)

1923+ ty <- typeExpr (allowImp syn)

1938 let tyn = expandNS syn tyn_in

1924 let tyn = expandNS syn tyn_in

1939 reserved "where"

1925 reserved "where"

1940 (cdoc, cn, cty, _) <- indentedBlockS (constructor syn)

1926 (cdoc, cn, cty, _) <- indentedBlockS (constructor syn)

@@ -1978,24 +1964,23 @@ SimpleConstructorList ::=

1978 ;

1964 ;

1979-}

1965-}

1980data_ :: SyntaxInfo -> IdrisParser PDecl

1966data_ :: SyntaxInfo -> IdrisParser PDecl

1981−data_ syn = try (do doc <- option "" (docComment '|')

1967+data_ syn = do (doc, acc, co) <- try (do

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 '|')

1968+ doc <- option "" (docComment '|')

1994 pushIndent

1969 pushIndent

1995 acc <- optional accessibility

1970 acc <- optional accessibility

1996 co <- dataI

1971 co <- dataI

1972+ return (doc, acc, co))

1997− fc <- getFC

1973+ fc <- getFC

1998− tyn_in <- fnName

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

1999 args <- many name

1984 args <- many name

2000 let ty = bindArgs (map (const PType) args) PType

1985 let ty = bindArgs (map (const PType) args) PType

2001 let tyn = expandNS syn tyn_in

1986 let tyn = expandNS syn tyn_in

@@ -2019,7 +2004,7 @@ data_ syn = try (do doc <- option "" (docComment '|')

2019 return (doc, x, cty, cfc)) cons

2004 return (doc, x, cty, cfc)) cons

2020 accData acc tyn (map (\ (_, n, _, _) -> n) cons')

2005 accData acc tyn (map (\ (_, n, _, _) -> n) cons')

2021 return $ PData doc syn fc co (PDatadecl tyn ty cons')))

2006 return $ PData doc syn fc co (PDatadecl tyn ty cons')))

2022− <?> "data type declaration"

2007+ <?> "data type declaration"

2023 where

2008 where

2024 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm

2009 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm

2025 mkPApp fc t [] = t

2010 mkPApp fc t [] = t

@@ -2036,7 +2021,8 @@ constructor syn

2036 = do doc <- option "" (docComment '|')

2021 = do doc <- option "" (docComment '|')

2037 cn_in <- fnName; fc <- getFC

2022 cn_in <- fnName; fc <- getFC

2038 let cn = expandNS syn cn_in

2023 let cn = expandNS syn cn_in

2024+ lchar ':'

2039− ty <- typeSig (allowImp syn)

2025+ ty <- typeExpr (allowImp syn)

2040 return (doc, cn, ty, fc)

2026 return (doc, cn, ty, fc)

2041 <?> "constructor"

2027 <?> "constructor"

2042

2028

@@ -2414,7 +2400,7 @@ Provider ::= '%' 'provide' '(' FnName TypeSig ')' 'with' Expr;

2414 -}

2400 -}

2415provider :: SyntaxInfo -> IdrisParser [PDecl]

2401provider :: SyntaxInfo -> IdrisParser [PDecl]

2416provider syn = do try (lchar '%' *> reserved "provide");

2402provider syn = do try (lchar '%' *> reserved "provide");

2417− lchar '('; n <- fnName; t <- typeSig syn; lchar ')'

2403+ lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

2418 fc <- getFC

2404 fc <- getFC

2419 reserved "with"

2405 reserved "with"

2420 e <- expr syn

2406 e <- expr syn

@@ -2553,17 +2539,17 @@ fullTactic syn = do t <- tactic syn

2553{- * Loading and parsing -}

2539{- * Loading and parsing -}

2554{- | Parses an expression from input -}

2540{- | Parses an expression from input -}

2555parseExpr :: IState -> String -> Result PTerm

2541parseExpr :: 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)

2557

2543

2558{- | Parses a tactic from input -}

2544{- | Parses a tactic from input -}

2559parseTactic :: IState -> String -> Result PTactic

2545parseTactic :: 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)

2561

2547

2562-- | Parse module header and imports

2548-- | Parse module header and imports

2563parseImports :: FilePath -> String -> Idris ([String], [String], Maybe Delta)

2549parseImports :: FilePath -> String -> Idris ([String], [String], Maybe Delta)

2564parseImports fname input

2550parseImports fname input

2565 = do i <- getIState

2551 = 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

2567 Failure err -> fail (show err)

2553 Failure err -> fail (show err)

2568 Success (x, i) -> do -- Discard state updates (there should be

2554 Success (x, i) -> do -- Discard state updates (there should be

2569 -- none anyway)

2555 -- none anyway)

@@ -2587,7 +2573,7 @@ parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->

2587 Idris [PDecl]

2573 Idris [PDecl]

2588parseProg syn fname input mrk

2574parseProg syn fname input mrk

2589 = do i <- getIState

2575 = 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

2591 Failure doc -> do iputStrLn (show doc)

2577 Failure doc -> do iputStrLn (show doc)

2592 -- FIXME: Get error location from trifecta

2578 -- FIXME: Get error location from trifecta

2593 --let errl = sourceLine (errorPos err)

2579 --let errl = sourceLine (errorPos err)

src/Idris/REPLParser.hs+1−1

@@ -23,7 +23,7 @@ import Data.Char(toLower)

23import qualified Data.ByteString.UTF8 as UTF8

25parseCmd :: IState -> String -> String -> Result Command

26−parseCmd i inputname = parseString (evalStateT pCmd i) (Directed (UTF8.fromString inputname) 0 0 0 0)

26+parseCmd i inputname = parseString (P.runInnerParser (evalStateT pCmd i)) (Directed (UTF8.fromString inputname) 0 0 0 0)

28cmd :: [String] -> P.IdrisParser ()

29cmd xs = do P.lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs)