@@ -444,6 +444,7 @@ bracketed :: SyntaxInfo -> IdrisParser PTerm
444444bracketed syn = do (FC fn (sl, sc) _) <- getFC
445445 lchar '(' <?> "parenthesized expression"
446446 bracketed' (FC fn (sl, sc) (sl, sc+1)) syn
447+
447448{- |Parses the rest of an expression in braces
448449@
449450Bracketed' ::=
@@ -462,19 +463,7 @@ bracketed' open syn =
462463 do (FC f start (l, c)) <- getFC
463464 lchar ')'
464465 return $ PTrue (spanFC open (FC f start (l, c+1))) TypeOrTerm
465− <|> try (do (ln, lnfc, colonFC, lty, starsFC):bnds <- some $ do
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)))
466+ <|> try (dependentPair TypeOrTerm [] open syn)
478467 <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
479468 -- No prefix operators! (bit of a hack here...)
480469 if (o == "-" || o == "!")
@@ -494,11 +483,45 @@ bracketed' open syn =
494483 pexp (PRef fc0 [] (sMN 1000 "ARG"))]))
495484 <|> do l <- expr syn
496485 bracketedExpr syn open l
497− where mergePDPairs :: FC -> [(Name, FC, FC, PTerm, FC)] -> PTerm -> PTerm
498− mergePDPairs starsFC' [] r = r
499− mergePDPairs starsFC' ((ln, lnfc, colonFC, lty, starsFC):bnds) r =
500− PDPair starsFC' [] TypeOrTerm (PRef lnfc [] ln) lty (mergePDPairs starsFC bnds r)
501−
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)
520+ pun e (maybe Placeholder snd cfclty) (mergePDPairs pun starsFC bnds r))
521+ mergePDPairs pun starsFC' [] r = r
522+ mergePDPairs pun starsFC' ((e, cfclty, starsFC):bnds) r =
523+ PDPair starsFC' [] pun e (maybe Placeholder snd cfclty) (mergePDPairs pun starsFC bnds r)
524+
502525-- | Parse the contents of parentheses, after an expression has been parsed.
503526bracketedExpr :: SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm
504527bracketedExpr syn openParenFC e =
@@ -509,20 +532,12 @@ bracketedExpr syn openParenFC e =
509532 closeParenFC <- lcharFC ')'
510533 let hilite = [openParenFC, closeParenFC] ++ map snd exprs
511534 return $ PPair openParenFC hilite TypeOrTerm e (mergePairs exprs)
512− <|> do exprs <- some $ do
513− starsFC <- reservedOpFC "**"
514− r <- expr 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))
535+ <|> do starsFC <- reservedOpFC "**"
536+ dependentPair IsTerm [(e, Nothing, starsFC)] openParenFC syn
519537 <?> "end of bracketed expression"
520538 where mergePairs :: [(PTerm, FC)] -> PTerm
521539 mergePairs [(t, fc)] = t
522540 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)
526541
527542-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a
528543-- big integer, otherwise try fromInteger and the constants as alternatives.