@@ -261,7 +261,9 @@ operatorLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
261261
262262-- | Parses an operator
263263operator :: MonadicParsing m => m String
264−operator = lexeme . some $ operatorLetter
264+operator = do op <- lexeme . some $ operatorLetter
265+ when (op == ":") $ fail "(:) is not a valid operator"
266+ return op
265267
266268{- * Position helpers -}
267269{- | Get filename from position (returns "(interactive)" when no source file is given) -}
@@ -687,22 +689,25 @@ fnDecl syn
687689 ;
688690-}
689691fnDecl' :: SyntaxInfo -> IdrisParser PDecl
690−fnDecl' syn = try (do doc <- option "" (docComment '|')
691− pushIndent
692− ist <- get
693− let initOpts = if default_total ist
694− then [TotalFn]
695− else []
696− opts <- fnOpts initOpts
697− acc <- optional accessibility
698− opts' <- fnOpts opts
699− n_in <- fnName
700− let n = expandNS syn n_in
701− fc <- getFC
702− ty <- typeSig (allowImp syn)
703− terminator
704− addAcc n acc
705− return (PTy doc syn fc opts' n ty))
692+fnDecl' syn = do (doc, fc, opts', n, acc) <- try (do
693+ doc <- option "" (docComment '|')
694+ pushIndent
695+ ist <- get
696+ let initOpts = if default_total ist
697+ then [TotalFn]
698+ else []
699+ opts <- fnOpts initOpts
700+ acc <- optional accessibility
701+ opts' <- fnOpts opts
702+ n_in <- fnName
703+ let n = expandNS syn n_in
704+ fc <- getFC
705+ lchar ':'
706+ return (doc, fc, opts', n, acc))
707+ ty <- typeExpr (allowImp syn)
708+ terminator
709+ addAcc n acc
710+ return (PTy doc syn fc opts' n ty)
706711 <|> postulate syn
707712 <|> caf syn
708713 <|> pattern syn
@@ -792,7 +797,8 @@ postulate syn = do doc <- try $ do doc <- option "" (docComment '|')
792797 opts' <- fnOpts opts
793798 n_in <- fnName
794799 let n = expandNS syn n_in
795− ty <- typeSig (allowImp syn)
800+ lchar ':'
801+ ty <- typeExpr (allowImp syn)
796802 fc <- getFC
797803 terminator
798804 addAcc n acc
@@ -1189,7 +1195,6 @@ SimpleExpr ::=
11891195 | '(' Bracketed
11901196 | Constant
11911197 | Type
1192− | '()'
11931198 | '_|_'
11941199 | '_'
11951200 | {- External (User-defined) Simple Expression -}
@@ -1214,15 +1219,12 @@ simpleExpr syn =
12141219 <|> try (comprehension syn)
12151220 <|> try (alt syn)
12161221 <|> try (idiom syn)
1217− <|> try (do lchar '('
1218− bracketed (disallowImp syn))
1222+ <|> do lchar '('
1223+ bracketed (disallowImp syn)
12191224 <|> try (do c <- constant
12201225 fc <- getFC
12211226 return (modifyConst syn fc (PConstant c)))
12221227 <|> do reserved "Type"; return PType
1223− <|> try (do symbol "()"
1224− fc <- getFC
1225− return (PTrue fc))
12261228 <|> try (do symbol "_|_"
12271229 fc <- getFC
12281230 return (PFalse fc))
@@ -1233,25 +1235,62 @@ simpleExpr syn =
12331235
12341236{- |Parses the rest of an expression in braces
12351237Bracketed ::=
1236− | Pair
1238+ ')'
12371239 | Expr ')'
1240+ | ExprList ')'
1241+ | Expr '**' Expr ')'
12381242 | Operator Expr ')'
12391243 | Expr Operator ')'
1244+ | Name ':' Expr '**' Expr ')'
12401245 ;
12411246-}
12421247bracketed :: SyntaxInfo -> IdrisParser PTerm
12431248bracketed syn =
1244− try (pair syn)
1245− <|> try (do e <- expr syn; lchar ')'; return e)
1246− <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
1247− return $ PLam (MN 1000 "ARG") Placeholder
1248− (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")),
1249+ do lchar ')'
1250+ fc <- getFC
1251+ return $ PTrue fc
1252+ <|>
1253+ try (do l <- expr syn
1254+ lchar ')'
1255+ return l)
1256+ <|> do (l, fc) <- try (do
1257+ l <- expr syn
1258+ fc <- getFC
1259+ lchar ','
1260+ return (l, fc))
1261+ rs <- sepBy1 (do fc' <- getFC; r <- expr syn; return (r, fc')) (lchar ',')
1262+ lchar ')'
1263+ return $ PPair fc l (mergePairs rs)
1264+ <|> do (l, fc) <- try (do
1265+ l <- expr syn
1266+ fc <- getFC
1267+ reservedOp "**"
1268+ return (l, fc))
1269+ r <- expr syn
1270+ lchar ')'
1271+ return (PDPair fc l Placeholder r)
1272+ <|> try(do fc0 <- getFC
1273+ l <- simpleExpr syn
1274+ o <- operator
1275+ lchar ')'
1276+ return $ PLam (MN 1000 "ARG") Placeholder
1277+ (PApp fc0 (PRef fc0 (UN o)) [pexp l,
1278+ pexp (PRef fc0 (MN 1000 "ARG"))]))
1279+ <|> try(do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
1280+ return $ PLam (MN 1000 "ARG") Placeholder
1281+ (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")),
12491282 pexp e]))
1250− <|> try (do fc <- getFC; e <- simpleExpr syn; o <- operator; lchar ')'
1251− return $ PLam (MN 1000 "ARG") Placeholder
1252− (PApp fc (PRef fc (UN o)) [pexp e,
1253− pexp (PRef fc (MN 1000 "ARG"))]))
1254− <?> "end of expression in braces"
1283+ <|> try (do ln <- name; lchar ':'
1284+ lty <- expr syn
1285+ reservedOp "**"
1286+ fc <- getFC
1287+ r <- expr syn
1288+ lchar ')'
1289+ return (PDPair fc (PRef fc ln) lty r))
1290+ <?> "end of braced expression"
1291+ where mergePairs :: [(PTerm, FC)] -> PTerm
1292+ mergePairs [(t, fc)] = t
1293+ mergePairs ((t, fc):rs) = PPair fc t (mergePairs rs)
12551294
12561295-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a
12571296-- big integer, otherwise try fromInteger and the constants as alternatives.
@@ -1295,62 +1334,6 @@ listExpr syn = do lchar '['; fc <- getFC; xs <- sepBy (expr syn) (lchar ','); lc
12951334 mkList fc [] = PRef fc (UN "Nil")
12961335 mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
12971336
1298−{- | Parses rest of pair expression
1299−Pair ::=
1300− Expr RestTuple? ')'
1301− | NTuple ')'
1302− | Name ':' Expr '**' 'Expr' ')'
1303− ;
1304−
1305−RestTuple ::=
1306− ',' Expr
1307− | '**' Expr
1308− ;
1309−
1310−NTuple ::=
1311− Expr ',' Expr
1312− | Expr ',' NTuple
1313− ;
1314−-}
1315−pair :: SyntaxInfo -> IdrisParser PTerm
1316−pair syn = try (do l <- expr syn
1317− fc <- getFC
1318− rest <- restTuple
1319− case rest of
1320− [] -> return l
1321− [Left r] -> return (PPair fc l r)
1322− [Right r] -> return (PDPair fc l Placeholder r))
1323− <|> try (do x <- ntuple
1324− lchar ')'
1325− return x)
1326− <|> do ln <- name; lchar ':'
1327− lty <- expr syn
1328− reservedOp "**"
1329− fc <- getFC
1330− r <- expr syn
1331− lchar ')'
1332− return (PDPair fc (PRef fc ln) lty r)
1333− <?> "pair expression"
1334− where
1335− restTuple :: IdrisParser [Either PTerm PTerm]
1336− restTuple = do lchar ')'; return []
1337− <|> do lchar ','
1338− r <- expr syn
1339− lchar ')'
1340− return [Left r]
1341− <|> do reservedOp "**"
1342− r <- expr syn
1343− lchar ')'
1344− return [Right r]
1345− <?> "end of pair expression"
1346− ntuple :: IdrisParser PTerm
1347− ntuple = try (do l <- expr syn; fc <- getFC; lchar ','
1348− rest <- ntuple
1349− return (PPair fc l rest))
1350− <|> (do l <- expr syn; fc <- getFC; lchar ','
1351− r <- expr syn
1352− return (PPair fc l r))
1353− <?> "tuple expression"
13541337
13551338{- | Parses an alternative expression
13561339 Alt ::= '(|' Expr_List '|)';
@@ -1526,15 +1509,10 @@ mkType (UN n) = UN ("set_" ++ n)
15261509mkType (MN 0 n) = MN 0 ("set_" ++ n)
15271510mkType (NS n s) = NS (mkType n) s
15281511
1529−{- |Parses a type for an expression
1512+{- |Parses a type signature
15301513TypeSig ::=
15311514 ':' Expr
15321515 ;
1533−-}
1534−typeSig :: SyntaxInfo -> IdrisParser PTerm
1535−typeSig syn = lchar ':' *> typeExpr syn <?> "type"
1536−
1537−{- |Parses a type signature
15381516TypeExpr ::= ConstraintList? Expr;
15391517 -}
15401518typeExpr :: SyntaxInfo -> IdrisParser PTerm
@@ -1719,7 +1697,8 @@ usingDeclList :: SyntaxInfo -> IdrisParser [Using]
17191697usingDeclList syn
17201698 = try (sepBy1 (usingDecl syn) (lchar ','))
17211699 <|> do ns <- sepBy1 name (lchar ',')
1722− t <- typeSig (disallowImp syn)
1700+ lchar ':'
1701+ t <- typeExpr (disallowImp syn)
17231702 return (map (\x -> UImplicit x t) ns)
17241703 <?> "using declaration list"
17251704
@@ -1731,7 +1710,8 @@ UsingDecl ::=
17311710-}
17321711usingDecl :: SyntaxInfo -> IdrisParser Using
17331712usingDecl syn = try (do x <- fnName
1734− t <- typeSig (disallowImp syn)
1713+ lchar ':'
1714+ t <- typeExpr (disallowImp syn)
17351715 return (UImplicit x t))
17361716 <|> do c <- fnName
17371717 xs <- some fnName
@@ -1751,11 +1731,13 @@ FunctionSignatureList ::=
17511731-}
17521732typeDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
17531733typeDeclList syn = try (sepBy1 (do x <- fnName
1754− t <- typeSig (disallowImp syn)
1734+ lchar ':'
1735+ t <- typeExpr (disallowImp syn)
17551736 return (x,t))
17561737 (lchar ','))
17571738 <|> do ns <- sepBy1 name (lchar ',')
1758− t <- typeSig (disallowImp syn)
1739+ lchar ':'
1740+ t <- typeExpr (disallowImp syn)
17591741 return (map (\x -> (x, t)) ns)
17601742 <?> "type declaration list"
17611743
@@ -1936,7 +1918,8 @@ record syn = do (doc, acc) <- try (do
19361918 return (doc, acc))
19371919 fc <- getFC
19381920 tyn_in <- fnName
1939− ty <- typeSig (allowImp syn)
1921+ lchar ':'
1922+ ty <- typeExpr (allowImp syn)
19401923 let tyn = expandNS syn tyn_in
19411924 reserved "where"
19421925 (cdoc, cn, cty, _) <- indentedBlockS (constructor syn)
@@ -1985,7 +1968,8 @@ data_ syn = try (do doc <- option "" (docComment '|')
19851968 co <- dataI
19861969 fc <- getFC
19871970 tyn_in <- fnName
1988− ty <- typeSig (allowImp syn)
1971+ lchar ':'
1972+ ty <- typeExpr (allowImp syn)
19891973 let tyn = expandNS syn tyn_in
19901974 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
19911975 reserved "where"
@@ -2038,7 +2022,8 @@ constructor syn
20382022 = do doc <- option "" (docComment '|')
20392023 cn_in <- fnName; fc <- getFC
20402024 let cn = expandNS syn cn_in
2041− ty <- typeSig (allowImp syn)
2025+ lchar ':'
2026+ ty <- typeExpr (allowImp syn)
20422027 return (doc, cn, ty, fc)
20432028 <?> "constructor"
20442029
@@ -2416,7 +2401,7 @@ Provider ::= '%' 'provide' '(' FnName TypeSig ')' 'with' Expr;
24162401 -}
24172402provider :: SyntaxInfo -> IdrisParser [PDecl]
24182403provider syn = do try (lchar '%' *> reserved "provide");
2419− lchar '('; n <- fnName; t <- typeSig syn; lchar ')'
2404+ lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
24202405 fc <- getFC
24212406 reserved "with"
24222407 e <- expr syn