336f5da · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Some refactoring of bracketed expressions (centralizing most of the

336f5daAhmad Salim Al-Sibahi13 years ago

src/Idris/Parser.hs+90−105

compare with master

unifiedsplit

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

261

262-- | Parses an operator

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

265

267

266{- * Position helpers -}

268{- * Position helpers -}

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

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

@@ -687,22 +689,25 @@ fnDecl syn

687 ;

689 ;

688-}

690-}

689fnDecl' :: SyntaxInfo -> IdrisParser PDecl

691fnDecl' :: SyntaxInfo -> IdrisParser PDecl

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

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

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

691− pushIndent

694+ pushIndent

692− ist <- get

695+ ist <- get

693− let initOpts = if default_total ist

696+ let initOpts = if default_total ist

694− then [TotalFn]

697+ then [TotalFn]

695− else []

698+ else []

696− opts <- fnOpts initOpts

699+ opts <- fnOpts initOpts

697− acc <- optional accessibility

700+ acc <- optional accessibility

698− opts' <- fnOpts opts

701+ opts' <- fnOpts opts

699− n_in <- fnName

702+ n_in <- fnName

700− let n = expandNS syn n_in

703+ let n = expandNS syn n_in

701− fc <- getFC

704+ fc <- getFC

705+ lchar ':'

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

702− ty <- typeSig (allowImp syn)

707+ ty <- typeExpr (allowImp syn)

703− terminator

708+ terminator

704− addAcc n acc

709+ addAcc n acc

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

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

706 <|> postulate syn

711 <|> postulate syn

707 <|> caf syn

712 <|> caf syn

708 <|> pattern syn

713 <|> pattern syn

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

792 opts' <- fnOpts opts

797 opts' <- fnOpts opts

793 n_in <- fnName

798 n_in <- fnName

794 let n = expandNS syn n_in

799 let n = expandNS syn n_in

800+ lchar ':'

795− ty <- typeSig (allowImp syn)

801+ ty <- typeExpr (allowImp syn)

796 fc <- getFC

802 fc <- getFC

797 terminator

803 terminator

798 addAcc n acc

804 addAcc n acc

@@ -1189,7 +1195,6 @@ SimpleExpr ::=

1189 | '(' Bracketed

1195 | '(' Bracketed

1190 | Constant

1196 | Constant

1191 | Type

1197 | Type

1192− | '()'

1193 | '_|_'

1198 | '_|_'

1194 | '_'

1199 | '_'

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

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

@@ -1214,15 +1219,12 @@ simpleExpr syn =

1214 <|> try (comprehension syn)

1219 <|> try (comprehension syn)

1215 <|> try (alt syn)

1220 <|> try (alt syn)

1216 <|> try (idiom syn)

1221 <|> try (idiom syn)

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

1222+ <|> do lchar '('

1218− bracketed (disallowImp syn))

1223+ bracketed (disallowImp syn)

1219 <|> try (do c <- constant

1224 <|> try (do c <- constant

1220 fc <- getFC

1225 fc <- getFC

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

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

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

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

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

1224− fc <- getFC

1225− return (PTrue fc))

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

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

1227 fc <- getFC

1229 fc <- getFC

1228 return (PFalse fc))

1230 return (PFalse fc))

@@ -1233,25 +1235,62 @@ simpleExpr syn =

1233

1235

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

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

1235Bracketed ::=

1237Bracketed ::=

1236− | Pair

1238+ ')'

1237 | Expr ')'

1239 | Expr ')'

1240+ | ExprList ')'

1241+ | Expr '**' Expr ')'

1238 | Operator Expr ')'

1242 | Operator Expr ')'

1239 | Expr Operator ')'

1243 | Expr Operator ')'

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

1240 ;

1245 ;

1241-}

1246-}

1242bracketed :: SyntaxInfo -> IdrisParser PTerm

1247bracketed :: SyntaxInfo -> IdrisParser PTerm

1243bracketed syn =

1248bracketed syn =

1249+ do lchar ')'

1250+ fc <- getFC

1251+ return $ PTrue fc

1252+ <|>

1244− try (pair syn)

1253+ try (do l <- expr syn

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

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

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

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

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

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

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

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

1249 pexp e]))

1282 pexp e]))

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

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

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

1284+ lty <- expr syn

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

1285+ reservedOp "**"

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

1286+ fc <- getFC

1287+ r <- expr syn

1288+ lchar ')'

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

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

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)

1255

1294

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

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

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

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

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

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

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

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

1297

1336

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"

1354

1337

1355{- | Parses an alternative expression

1338{- | Parses an alternative expression

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

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

@@ -1526,15 +1509,10 @@ mkType (UN n) = UN ("set_" ++ n)

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

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

1527mkType (NS n s) = NS (mkType n) s

1510mkType (NS n s) = NS (mkType n) s

1528

1511

1529−{- |Parses a type for an expression

1512+{- |Parses a type signature

1530TypeSig ::=

1513TypeSig ::=

1531 ':' Expr

1514 ':' Expr

1532 ;

1515 ;

1533−-}

1534−typeSig :: SyntaxInfo -> IdrisParser PTerm

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

1536−

1537−{- |Parses a type signature

1538TypeExpr ::= ConstraintList? Expr;

1516TypeExpr ::= ConstraintList? Expr;

1539 -}

1517 -}

1540typeExpr :: SyntaxInfo -> IdrisParser PTerm

1518typeExpr :: SyntaxInfo -> IdrisParser PTerm

@@ -1719,7 +1697,8 @@ usingDeclList :: SyntaxInfo -> IdrisParser [Using]

1719usingDeclList syn

1697usingDeclList syn

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

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

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

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

1700+ lchar ':'

1722− t <- typeSig (disallowImp syn)

1701+ t <- typeExpr (disallowImp syn)

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

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

1724 <?> "using declaration list"

1703 <?> "using declaration list"

1725

1704

@@ -1731,7 +1710,8 @@ UsingDecl ::=

1731-}

1710-}

1732usingDecl :: SyntaxInfo -> IdrisParser Using

1711usingDecl :: SyntaxInfo -> IdrisParser Using

1733usingDecl syn = try (do x <- fnName

1712usingDecl syn = try (do x <- fnName

1713+ lchar ':'

1734− t <- typeSig (disallowImp syn)

1714+ t <- typeExpr (disallowImp syn)

1735 return (UImplicit x t))

1715 return (UImplicit x t))

1736 <|> do c <- fnName

1716 <|> do c <- fnName

1737 xs <- some fnName

1717 xs <- some fnName

@@ -1751,11 +1731,13 @@ FunctionSignatureList ::=

1751-}

1731-}

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

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

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

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

1734+ lchar ':'

1754− t <- typeSig (disallowImp syn)

1735+ t <- typeExpr (disallowImp syn)

1755 return (x,t))

1736 return (x,t))

1756 (lchar ','))

1737 (lchar ','))

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

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

1739+ lchar ':'

1758− t <- typeSig (disallowImp syn)

1740+ t <- typeExpr (disallowImp syn)

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

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

1760 <?> "type declaration list"

1742 <?> "type declaration list"

1761

1743

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

1936 return (doc, acc))

1918 return (doc, acc))

1937 fc <- getFC

1919 fc <- getFC

1938 tyn_in <- fnName

1920 tyn_in <- fnName

1921+ lchar ':'

1939− ty <- typeSig (allowImp syn)

1922+ ty <- typeExpr (allowImp syn)

1940 let tyn = expandNS syn tyn_in

1923 let tyn = expandNS syn tyn_in

1941 reserved "where"

1924 reserved "where"

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

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

@@ -1985,7 +1968,8 @@ data_ syn = try (do doc <- option "" (docComment '|')

1985 co <- dataI

1968 co <- dataI

1986 fc <- getFC

1969 fc <- getFC

1987 tyn_in <- fnName

1970 tyn_in <- fnName

1971+ lchar ':'

1988− ty <- typeSig (allowImp syn)

1972+ ty <- typeExpr (allowImp syn)

1989 let tyn = expandNS syn tyn_in

1973 let tyn = expandNS syn tyn_in

1990 option (PData doc syn fc co (PLaterdecl tyn ty)) (do

1974 option (PData doc syn fc co (PLaterdecl tyn ty)) (do

1991 reserved "where"

1975 reserved "where"

@@ -2038,7 +2022,8 @@ constructor syn

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

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

2039 cn_in <- fnName; fc <- getFC

2023 cn_in <- fnName; fc <- getFC

2040 let cn = expandNS syn cn_in

2024 let cn = expandNS syn cn_in

2025+ lchar ':'

2041− ty <- typeSig (allowImp syn)

2026+ ty <- typeExpr (allowImp syn)

2042 return (doc, cn, ty, fc)

2027 return (doc, cn, ty, fc)

2043 <?> "constructor"

2028 <?> "constructor"

2044

2029

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

2416 -}

2401 -}

2417provider :: SyntaxInfo -> IdrisParser [PDecl]

2402provider :: SyntaxInfo -> IdrisParser [PDecl]

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

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

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

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

2420 fc <- getFC

2405 fc <- getFC

2421 reserved "with"

2406 reserved "with"

2422 e <- expr syn

2407 e <- expr syn