101a2e9 · Idris-dev · git.iko.soy

444bracketed syn = do (FC fn (sl, sc) _) <- getFC

445 lchar '(' <?> "parenthesized expression"

446 bracketed' (FC fn (sl, sc) (sl, sc+1)) syn

447+

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

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

448@

449@

449Bracketed' ::=

450Bracketed' ::=

462 do (FC f start (l, c)) <- getFC

463 do (FC f start (l, c)) <- getFC

463 lchar ')'

464 lchar ')'

464 return $ PTrue (spanFC open (FC f start (l, c+1))) TypeOrTerm

465 return $ PTrue (spanFC open (FC f start (l, c+1))) TypeOrTerm

465− <|> try (do (ln, lnfc, colonFC, lty, starsFC):bnds <- some $ do

466+ <|> try (dependentPair TypeOrTerm [] open syn)

466− (ln, lnfc, colonFC) <- try $ do

467− (ln, lnfc) <- name

468− colonFC <- lcharFC ':'

469− return (ln, lnfc, colonFC)

470− lty <- expr' syn

471− starsFC <- reservedOpFC "**"

472− return (ln, lnfc, colonFC, lty, starsFC)

473− fc <- getFC

474− r <- expr syn

475− close <- lcharFC ')'

476− return (PDPair fc ([open, colonFC, starsFC, close] ++ (=<<) (\(_,_,cfc,_,sfc) -> [cfc, sfc]) bnds)

477− TypeOrTerm (PRef lnfc [] ln) lty (mergePDPairs starsFC bnds r)))

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

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

479 -- No prefix operators! (bit of a hack here...)

468 -- No prefix operators! (bit of a hack here...)

480 if (o == "-" || o == "!")

469 if (o == "-" || o == "!")

494 pexp (PRef fc0 [] (sMN 1000 "ARG"))]))

483 pexp (PRef fc0 [] (sMN 1000 "ARG"))]))

495 <|> do l <- expr syn

484 <|> do l <- expr syn

496 bracketedExpr syn open l

485 bracketedExpr syn open l

497− where mergePDPairs :: FC -> [(Name, FC, FC, PTerm, FC)] -> PTerm -> PTerm

486+

487+

488+

489+dependentPair :: PunInfo -> [(PTerm, Maybe (FC, PTerm), FC)] -> FC -> SyntaxInfo -> IdrisParser PTerm

490+dependentPair pun prev openFC syn =

491+ case pun of

492+ IsType -> nametypePart <|> namePart

493+ IsTerm -> exprPart

494+ TypeOrTerm ->

495+ if prev /= [] then -- To avoid ambiguity with later parsing

496+ nametypePart <|> namePart

497+ else

498+ nametypePart <|> namePart <|> exprPart

499+ where nametypePart = do

500+ (ln, lnfc, colonFC) <- try $ do

501+ (ln, lnfc) <- name

502+ colonFC <- lcharFC ':'

503+ return (ln, lnfc, colonFC)

504+ lty <- expr' syn

505+ starsFC <- reservedOpFC "**"

506+ dependentPair IsType ((PRef lnfc [] ln, Just (colonFC, lty), starsFC):prev) openFC syn

507+ namePart = try $ do

508+ (ln, lnfc) <- name

509+ starsFC <- reservedOpFC "**"

510+ dependentPair pun ((PRef lnfc [] ln, Nothing, starsFC):prev) openFC syn

511+ exprPart = do

512+ e <- expr syn

513+ sepFCE <- (Left <$> reservedOpFC "**") <|> (Right <$> lcharFC ')')

514+ case sepFCE of

515+ Left starsFC -> dependentPair IsTerm ((e, Nothing, starsFC):prev) openFC syn

516+ Right closeFC ->

517+ return (mkPDPairs pun openFC closeFC (reverse prev) e)

518+ mkPDPairs pun openFC closeFC ((e, cfclty, starsFC):bnds) r =

519+ (PDPair openFC ([openFC] ++ maybe [] ((: []) . fst) cfclty ++ [starsFC, closeFC] ++ (=<<) (\(_,cfclty,sfc) -> maybe [] ((: []) . fst) cfclty ++ [sfc]) bnds)

498− mergePDPairs starsFC' [] r = r

520+ pun e (maybe Placeholder snd cfclty) (mergePDPairs pun starsFC bnds r))

521+ mergePDPairs pun starsFC' [] r = r

499− mergePDPairs starsFC' ((ln, lnfc, colonFC, lty, starsFC):bnds) r =

522+ mergePDPairs pun starsFC' ((e, cfclty, starsFC):bnds) r =

500− PDPair starsFC' [] TypeOrTerm (PRef lnfc [] ln) lty (mergePDPairs starsFC bnds r)

523+ PDPair starsFC' [] pun e (maybe Placeholder snd cfclty) (mergePDPairs pun starsFC bnds r)

501−

524+

502-- | Parse the contents of parentheses, after an expression has been parsed.

525-- | Parse the contents of parentheses, after an expression has been parsed.

503bracketedExpr :: SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm

526bracketedExpr :: SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm

504bracketedExpr syn openParenFC e =

527bracketedExpr syn openParenFC e =

509 closeParenFC <- lcharFC ')'

532 closeParenFC <- lcharFC ')'

510 let hilite = [openParenFC, closeParenFC] ++ map snd exprs

533 let hilite = [openParenFC, closeParenFC] ++ map snd exprs

511 return $ PPair openParenFC hilite TypeOrTerm e (mergePairs exprs)

534 return $ PPair openParenFC hilite TypeOrTerm e (mergePairs exprs)

512− <|> do exprs <- some $ do

513− starsFC <- reservedOpFC "**"

535+ <|> do starsFC <- reservedOpFC "**"

514− r <- expr syn

536+ dependentPair IsTerm [(e, Nothing, starsFC)] openParenFC syn

515− return (r, starsFC)

516− closeParenFC <- lcharFC ')'

517− let hilite = [openParenFC, closeParenFC] ++ map snd exprs

518− return (PDPair openParenFC hilite TypeOrTerm e Placeholder (mergePDPairs exprs))

519 <?> "end of bracketed expression"

537 <?> "end of bracketed expression"

520 where mergePairs :: [(PTerm, FC)] -> PTerm

538 where mergePairs :: [(PTerm, FC)] -> PTerm

521 mergePairs [(t, fc)] = t

539 mergePairs [(t, fc)] = t

522 mergePairs ((t, fc):rs) = PPair fc [] TypeOrTerm t (mergePairs rs)

540 mergePairs ((t, fc):rs) = PPair fc [] TypeOrTerm t (mergePairs rs)

523− mergePDPairs :: [(PTerm, FC)] -> PTerm

524− mergePDPairs [(t, fc)] = t

525− mergePDPairs ((t, fc):rs) = PDPair fc [] TypeOrTerm t Placeholder (mergePDPairs rs)

526

541

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

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

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

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