0b37d3f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1053 from ahmadsalim/improvement/parser-simplification

0b37d3fEdwin Brady13 years ago

src/Idris/ParseExpr.hs+101−120

compare with master

unifiedsplit

@@ -190,9 +190,7 @@ extension syn (Rule ssym ptm _)

190{- | Parses a (normal) built-in expression

191@

192InternalExpr ::=

193− App

194− | MatchApp

195− | UnifyLog

193+ UnifyLog

196 | RecordType

194 | RecordType

197 | SimpleExpr

195 | SimpleExpr

198 | Lambda

196 | Lambda

@@ -202,16 +200,15 @@ InternalExpr ::=

202 | Pi

200 | Pi

203 | CaseExpr

201 | CaseExpr

204 | DoBlock

202 | DoBlock

203+ | App

205 ;

204 ;

206@

205@

207-}

206-}

208internalExpr :: SyntaxInfo -> IdrisParser PTerm

207internalExpr :: SyntaxInfo -> IdrisParser PTerm

209internalExpr syn =

208internalExpr syn =

210− try (app syn)

211− <|> try (matchApp syn)

212− <|> try (unifyLog syn)

209+ unifyLog syn

213− <|> try (disamb syn)

210+ <|> disamb syn

214− <|> try (noImplicits syn)

211+ <|> noImplicits syn

215 <|> recordType syn

212 <|> recordType syn

216 <|> lambda syn

213 <|> lambda syn

217 <|> quoteGoal syn

214 <|> quoteGoal syn

@@ -220,7 +217,7 @@ internalExpr syn =

220 <|> try (pi syn)

217 <|> try (pi syn)

221 <|> doBlock syn

218 <|> doBlock syn

222 <|> caseExpr syn

219 <|> caseExpr syn

223− <|> simpleExpr syn

220+ <|> app syn

224 <?> "expression"

221 <?> "expression"

225

222

226{- | Parses a case expression

223{- | Parses a case expression

@@ -278,30 +275,28 @@ tacticsExpr syn = do reserved "tactics"

278{- | Parses a simple expression

275{- | Parses a simple expression

279@

276@

280SimpleExpr ::=

277SimpleExpr ::=

281− '![' Term ']'

278+ {- External (User-defined) Simple Expression -}

282 | '?' Name

279 | '?' Name

283 | % 'instance'

280 | % 'instance'

284 | 'refl' ('{' Expr '}')?

281 | 'refl' ('{' Expr '}')?

285 | ProofExpr

282 | ProofExpr

286 | TacticsExpr

283 | TacticsExpr

287 | FnName

284 | FnName

285+ | Idiom

288 | List

286 | List

289− | Comprehension

290 | Alt

287 | Alt

291− | Idiom

292− | '(' Bracketed

288+ | Bracketed

293 | Constant

289 | Constant

294 | Type

290 | Type

295 | '_|_'

291 | '_|_'

296 | '_'

292 | '_'

297− | {- External (User-defined) Simple Expression -}

298 ;

293 ;

299@

294@

300-}

295-}

301simpleExpr :: SyntaxInfo -> IdrisParser PTerm

296simpleExpr :: SyntaxInfo -> IdrisParser PTerm

302simpleExpr syn =

297simpleExpr syn =

303− {-try (do symbol "!["; t <- term; lchar ']'; return $ PQuote t)

298+ try (simpleExternalExpr syn)

304− <|>-} do x <- try (lchar '?' *> name); return (PMetavar x)

299+ <|> do x <- try (lchar '?' *> name); return (PMetavar x)

305 <|> do lchar '%'; fc <- getFC; reserved "instance"; return (PResolveTC fc)

300 <|> do lchar '%'; fc <- getFC; reserved "instance"; return (PResolveTC fc)

306 <|> do reserved "refl"; fc <- getFC;

301 <|> do reserved "refl"; fc <- getFC;

307 tm <- option Placeholder (do lchar '{'; t <- expr syn; lchar '}';

302 tm <- option Placeholder (do lchar '{'; t <- expr syn; lchar '}';

@@ -311,36 +306,39 @@ simpleExpr syn =

311 <|> proofExpr syn

306 <|> proofExpr syn

312 <|> tacticsExpr syn

307 <|> tacticsExpr syn

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

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

314− <|> try (do c <- constant

309+ <|> do c <- constant

315− fc <- getFC

310+ fc <- getFC

316− return (modifyConst syn fc (PConstant c)))

311+ return (modifyConst syn fc (PConstant c))

317− <|> try (do symbol "'"; fc <- getFC; str <- name

312+ <|> do symbol "'"; fc <- getFC; str <- name

318− return (PApp fc (PRef fc (sUN "Symbol_"))

313+ return (PApp fc (PRef fc (sUN "Symbol_"))

319− [pexp (PConstant (Str (show str)))]))

314+ [pexp (PConstant (Str (show str)))])

320 <|> do fc <- getFC

315 <|> do fc <- getFC

321 x <- fnName

316 x <- fnName

322 return (PRef fc x)

317 return (PRef fc x)

323− <|> try (listExpr syn)

324− <|> try (comprehension syn)

325− <|> alt syn

326 <|> idiom syn

318 <|> idiom syn

319+ <|> listExpr syn

320+ <|> alt syn

327 <|> do lchar '!'

321 <|> do lchar '!'

328 s <- simpleExpr syn

322 s <- simpleExpr syn

329 fc <- getFC

323 fc <- getFC

330 return (PAppBind fc s [])

324 return (PAppBind fc s [])

331− <|> do lchar '('

332− bracketed (disallowImp syn)

325+ <|> bracketed (disallowImp syn)

333 <|> do symbol "_|_"

326 <|> do symbol "_|_"

334 fc <- getFC

327 fc <- getFC

335 return (PFalse fc)

328 return (PFalse fc)

336 <|> do lchar '_'; return Placeholder

329 <|> do lchar '_'; return Placeholder

337− <|> simpleExternalExpr syn

338 <?> "expression"

330 <?> "expression"

339

331

340−

332+{- |Parses an expression in braces

333+@

334+Bracketed ::= '(' Bracketed'

335+ -}

336+bracketed :: SyntaxInfo -> IdrisParser PTerm

337+bracketed syn = do lchar '(' <?> "parenthesized expression"

338+ bracketed' syn

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

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

342@

340@

343−Bracketed ::=

341+Bracketed' ::=

344 ')'

342 ')'

345 | Expr ')'

343 | Expr ')'

346 | ExprList ')'

344 | ExprList ')'

@@ -351,8 +349,8 @@ Bracketed ::=

351 ;

349 ;

352@

350@

353-}

351-}

354−bracketed :: SyntaxInfo -> IdrisParser PTerm

352+bracketed' :: SyntaxInfo -> IdrisParser PTerm

355−bracketed syn =

353+bracketed' syn =

356 do lchar ')'

354 do lchar ')'

357 fc <- getFC

355 fc <- getFC

358 return $ PTrue fc TypeOrTerm

356 return $ PTrue fc TypeOrTerm

@@ -425,29 +423,6 @@ modifyConst syn fc (PConstant (BI x))

425 ]

423 ]

426modifyConst syn fc x = x

424modifyConst syn fc x = x

427

425

428−{- | Parses a list literal expression e.g. [1,2,3]

429−@

430−ListExpr ::=

431− '[' ExprList? ']'

432−;

433−@

434−@

435−ExprList ::=

436− Expr

437− | Expr ',' ExprList

438− ;

439−@

440− -}

441−listExpr :: SyntaxInfo -> IdrisParser PTerm

442−listExpr syn = do lchar '['; fc <- getFC; xs <- sepBy (expr syn) (lchar ','); lchar ']'

443− return (mkList fc xs)

444− <?> "list expression"

445− where

446− mkList :: FC -> [PTerm] -> PTerm

447− mkList fc [] = PRef fc (sUN "Nil")

448− mkList fc (x : xs) = PApp fc (PRef fc (sUN "::")) [pexp x, pexp (mkList fc xs)]

449−

450−

451{- | Parses an alternative expression

426{- | Parses an alternative expression

452@

427@

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

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

@@ -478,31 +453,13 @@ hsimpleExpr syn =

478 <|> simpleExpr syn

453 <|> simpleExpr syn

479 <?> "expression"

454 <?> "expression"

480

455

481−{- | Parses a matching application expression

482−@

483−MatchApp ::=

484− SimpleExpr '<==' FnName

485− ;

486−@

487−-}

488−matchApp :: SyntaxInfo -> IdrisParser PTerm

489−matchApp syn = do ty <- simpleExpr syn

490− symbol "<=="

491− fc <- getFC

492− f <- fnName

493− return (PLet (sMN 0 "match")

494− ty

495− (PMatchApp fc f)

496− (PRef fc (sMN 0 "match")))

497− <?> "matching application expression"

498−

499{- | Parses a unification log expression

456{- | Parses a unification log expression

500UnifyLog ::=

457UnifyLog ::=

501 '%' 'unifyLog' SimpleExpr

458 '%' 'unifyLog' SimpleExpr

502 ;

459 ;

503-}

460-}

504unifyLog :: SyntaxInfo -> IdrisParser PTerm

461unifyLog :: SyntaxInfo -> IdrisParser PTerm

505−unifyLog syn = do lchar '%'; reserved "unifyLog";

462+unifyLog syn = do try (lchar '%' *> reserved "unifyLog")

506 tm <- simpleExpr syn

463 tm <- simpleExpr syn

507 return (PUnifyLog tm)

464 return (PUnifyLog tm)

508 <?> "unification log expression"

465 <?> "unification log expression"

@@ -528,7 +485,7 @@ NoImplicits ::=

528@

485@

529-}

486-}

530noImplicits :: SyntaxInfo -> IdrisParser PTerm

487noImplicits :: SyntaxInfo -> IdrisParser PTerm

531−noImplicits syn = do lchar '%'; reserved "noImplicits";

488+noImplicits syn = do try (lchar '%' *> reserved "noImplicits")

532 tm <- simpleExpr syn

489 tm <- simpleExpr syn

533 return (PNoImplicits tm)

490 return (PNoImplicits tm)

534 <?> "no implicits expression"

491 <?> "no implicits expression"

@@ -537,7 +494,11 @@ noImplicits syn = do lchar '%'; reserved "noImplicits";

537@

494@

538App ::=

495App ::=

539 'mkForeign' Arg Arg*

496 'mkForeign' Arg Arg*

497+ | MatchApp

540− | SimpleExpr Arg+

498+ | SimpleExpr Arg*

499+ ;

500+MatchApp ::=

501+ SimpleExpr '<==' FnName

541 ;

502 ;

542@

503@

543-}

504-}

@@ -547,8 +508,6 @@ app syn = do f <- reserved "mkForeign"

547 fn <- arg syn

508 fn <- arg syn

548 args <- many (do notEndApp; arg syn)

509 args <- many (do notEndApp; arg syn)

549 i <- get

510 i <- get

550− -- mkForeign f args ==>

551− -- liftPrimIO (\w => mkForeignPrim f args w)

552 let ap = PApp fc (PRef fc (sUN "liftPrimIO"))

511 let ap = PApp fc (PRef fc (sUN "liftPrimIO"))

553 [pexp (PLam (sMN 0 "w")

512 [pexp (PLam (sMN 0 "w")

554 Placeholder

513 Placeholder

@@ -558,13 +517,20 @@ app syn = do f <- reserved "mkForeign"

558 return (dslify i ap)

517 return (dslify i ap)

559

518

560 <|> do f <- simpleExpr syn

519 <|> do f <- simpleExpr syn

520+ (do try $ symbol "<=="

521+ fc <- getFC

522+ ff <- fnName

523+ return (PLet (sMN 0 "match")

524+ f

525+ (PMatchApp fc ff)

526+ (PRef fc (sMN 0 "match")))

527+ <?> "matching application expression") <|> (do

561 fc <- getFC

528 fc <- getFC

562− args <- some (do notEndApp; arg syn)

563 i <- get

529 i <- get

530+ args <- many (do notEndApp; arg syn)

564−-- case f of

531+ case args of

565−-- PAppBind fc ref [] ->

532+ [] -> return f

566−-- return (dslify i (PAppBind fc ref args))

567− return (dslify i (PApp fc f args))

533+ _ -> return (dslify i (PApp fc f args)))

568 <?> "function application"

534 <?> "function application"

569 where

535 where

570 dslify :: IState -> PTerm -> PTerm

536 dslify :: IState -> PTerm -> PTerm

@@ -700,17 +666,17 @@ SimpleExprList ::=

700@

666@

701-}

667-}

702lambda :: SyntaxInfo -> IdrisParser PTerm

668lambda :: SyntaxInfo -> IdrisParser PTerm

703−lambda syn = do lchar '\\'

669+lambda syn = do lchar '\\' <?> "lambda expression"

704− try (do xt <- tyOptDeclList syn

670+ (do xt <- try $ tyOptDeclList syn

705− symbol "=>"

671+ symbol "=>"

706− sc <- expr syn

672+ sc <- expr syn

707− return (bindList PLam xt sc)

673+ return (bindList PLam xt sc)) <|> do

708− <|> (do ps <- sepBy (do fc <- getFC

674+ ps <- sepBy (do fc <- getFC

709− e <- simpleExpr syn

675+ e <- simpleExpr syn

710− return (fc, e)) (lchar ',')

676+ return (fc, e)) (lchar ',')

711− symbol "=>"

677+ symbol "=>"

712− sc <- expr syn

678+ sc <- expr syn

713− return (pmList (zip [0..] ps) sc)))

679+ return (pmList (zip [0..] ps) sc)

714 <?> "lambda expression"

680 <?> "lambda expression"

715 where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm

681 where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm

716 pmList [] sc = sc

682 pmList [] sc = sc

@@ -911,34 +877,49 @@ tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder

911 return (sMN 0 "underscore")

877 return (sMN 0 "underscore")

912 <?> "name or placeholder"

878 <?> "name or placeholder"

913

879

914−{- | Parses a list comprehension

880+{- | Parses a list literal expression e.g. [1,2,3] or a comprehension [ (x, y) | x <- xs , y <- ys ]

915@

881@

882+ListExpr ::=

883+ '[' ']'

916−Comprehension ::= '[' Expr '|' DoList ']';

884+ | '[' Expr '|' DoList ']'

885+ | '[' ExprList ']'

886+;

917@

887@

918−

919@

888@

920DoList ::=

889DoList ::=

921 Do

890 Do

922 | Do ',' DoList

891 | Do ',' DoList

923 ;

892 ;

924@

893@

894+@

895+ExprList ::=

896+ Expr

897+ | Expr ',' ExprList

898+ ;

899+@

925−-}

900+ -}

926−comprehension :: SyntaxInfo -> IdrisParser PTerm

901+listExpr :: SyntaxInfo -> IdrisParser PTerm

927−comprehension syn

928− = do lchar '['

902+listExpr syn = do lchar '['; fc <- getFC;

929− fc <- getFC

903+ try ((lchar ']' <?> "end of list expression") *> return (mkList fc [])) <|> (do

930− pat <- expr syn

904+ x <- expr syn <?> "expression"

931− lchar '|'

905+ (do try (lchar '|') <?> "list comprehension"

932− qs <- sepBy1 (do_ syn) (lchar ',')

906+ qs <- sepBy1 (do_ syn) (lchar ',')

933− lchar ']'

907+ lchar ']'

934− return (PDoBlock (map addGuard qs ++

908+ return (PDoBlock (map addGuard qs ++

935− [DoExp fc (PApp fc (PRef fc (sUN "return"))

909+ [DoExp fc (PApp fc (PRef fc (sUN "return"))

936− [pexp pat])]))

910+ [pexp x])]))) <|> (do

937− <?> "list comprehension"

911+ xs <- many ((lchar ',' <?> "list element") *> expr syn)

912+ lchar ']' <?> "end of list expression"

913+ return (mkList fc (x:xs))))

914+ <?> "list expression"

915+ where

916+ mkList :: FC -> [PTerm] -> PTerm

917+ mkList fc [] = PRef fc (sUN "Nil")

918+ mkList fc (x : xs) = PApp fc (PRef fc (sUN "::")) [pexp x, pexp (mkList fc xs)]

938− where addGuard :: PDo -> PDo

919+ addGuard :: PDo -> PDo

939− addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (sUN "guard"))

920+ addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (sUN "guard"))

940− [pexp e])

921+ [pexp e])

941− addGuard x = x

922+ addGuard x = x

942

923

943{- | Parses a do-block

924{- | Parses a do-block

944@

925@

@@ -1070,11 +1051,11 @@ constant = do reserved "Integer"; return (AType (ATInt ITBig))

1070 <|> do reserved "Bits16x8"; return (AType (ATInt (ITVec IT16 8)))

1051 <|> do reserved "Bits16x8"; return (AType (ATInt (ITVec IT16 8)))

1071 <|> do reserved "Bits32x4"; return (AType (ATInt (ITVec IT32 4)))

1052 <|> do reserved "Bits32x4"; return (AType (ATInt (ITVec IT32 4)))

1072 <|> do reserved "Bits64x2"; return (AType (ATInt (ITVec IT64 2)))

1053 <|> do reserved "Bits64x2"; return (AType (ATInt (ITVec IT64 2)))

1073− <|> try (do f <- float; return $ Fl f)

1054+ <|> do f <- try float; return $ Fl f

1074− <|> try (do i <- natural; return $ BI i)

1055+ <|> do i <- natural; return $ BI i

1075− <|> try (do s <- verbatimStringLiteral; return $ Str s)

1056+ <|> do s <- verbatimStringLiteral; return $ Str s

1076− <|> try (do s <- stringLiteral; return $ Str s)

1057+ <|> do s <- stringLiteral; return $ Str s

1077− <|> try (do c <- charLiteral; return $ Ch c)

1058+ <|> do c <- try charLiteral; return $ Ch c --Currently ambigous with symbols

1078 <?> "constant or literal"

1059 <?> "constant or literal"

1079

1060

1080{- | Parses a verbatim multi-line string literal (triple-quoted)

1061{- | Parses a verbatim multi-line string literal (triple-quoted)

@@ -1086,7 +1067,7 @@ VerbatimString_t ::=

1086@

1067@

1087 -}

1068 -}

1088verbatimStringLiteral :: MonadicParsing m => m String

1069verbatimStringLiteral :: MonadicParsing m => m String

1089−verbatimStringLiteral = token $ do string "\"\"\""

1070+verbatimStringLiteral = token $ do try $ string "\"\"\""

1090 manyTill anyChar $ try (string "\"\"\"")

1071 manyTill anyChar $ try (string "\"\"\"")

1091

1072

1092{- | Parses a static modifier

1073{- | Parses a static modifier

src/Idris/ParseHelpers.hs+1−1

@@ -214,7 +214,7 @@ idrisStyle :: MonadicParsing m => IdentifierStyle m

214idrisStyle = IdentifierStyle _styleName _styleStart _styleLetter _styleReserved Hi.Identifier Hi.ReservedIdentifier

215 where _styleName = "Idris"

216 _styleStart = satisfy isAlpha

217− _styleLetter = satisfy isAlphaNum <|> oneOf "_'" <|> (lchar '.')

217+ _styleLetter = satisfy isAlphaNum <|> oneOf "_'."

218 _styleReserved = HS.fromList ["let", "in", "data", "codata", "record", "Type",

219 "do", "dsl", "import", "impossible",

220 "case", "of", "total", "partial", "mutual",

src/Idris/Parser.hs−2

@@ -831,7 +831,6 @@ clause syn

831 return $ PClause fc n capp wargs rs wheres) <|> (do

832 popIndent

833 reserved "with"

834− lchar '(' <?> "parenthesized expression"

835 wval <- bracketed syn

834 wval <- bracketed syn

836 openBlock

835 openBlock

837 ds <- some $ fnDecl syn

836 ds <- some $ fnDecl syn

@@ -865,7 +864,6 @@ clause syn

865 reserved "with"

864 reserved "with"

866 ist <- get

865 ist <- get

867 put (ist { lastParse = Just n })

866 put (ist { lastParse = Just n })

868− lchar '(' <?> "parenthesized expression"

869 wval <- bracketed syn

867 wval <- bracketed syn

870 openBlock

868 openBlock

871 ds <- some $ fnDecl syn

869 ds <- some $ fnDecl syn