@@ -398,7 +398,7 @@ simpleExpr syn =
398398 <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc [] (SN $ ElimN t))
399399 <|> proofExpr syn
400400 <|> tacticsExpr syn
401− <|> try (do reserved "Type"; symbol "*"; return $ PUniverse AllTypes)
401+ <|> try (do reserved "Type*"; return $ PUniverse AllTypes)
402402 <|> do reserved "AnyType"; return $ PUniverse AllTypes
403403 <|> PType <$> reservedFC "Type"
404404 <|> do reserved "UniqueType"; return $ PUniverse UniqueType
@@ -440,16 +440,16 @@ bracketed :: SyntaxInfo -> IdrisParser PTerm
440440bracketed syn = do (FC fn (sl, sc) _) <- getFC
441441 lchar '(' <?> "parenthesized expression"
442442 bracketed' (FC fn (sl, sc) (sl, sc+1)) syn
443+
443444{- |Parses the rest of an expression in braces
444445@
445446Bracketed' ::=
446447 ')'
447448 | Expr ')'
448449 | ExprList ')'
449− | Expr '**' Expr ')'
450+ | DependentPair ')'
450451 | Operator Expr ')'
451452 | Expr Operator ')'
452− | Name ':' Expr '**' Expr ')'
453453 ;
454454@
455455-}
@@ -458,14 +458,7 @@ bracketed' open syn =
458458 do (FC f start (l, c)) <- getFC
459459 lchar ')'
460460 return $ PTrue (spanFC open (FC f start (l, c+1))) TypeOrTerm
461− <|> try (do (ln, lnfc) <- name
462− colonFC <- lcharFC ':'
463− lty <- expr syn
464− starsFC <- reservedOpFC "**"
465− fc <- getFC
466− r <- expr syn
467− close <- lcharFC ')'
468− return (PDPair fc [open, colonFC, starsFC, close] TypeOrTerm (PRef lnfc [] ln) lty r))
461+ <|> try (dependentPair TypeOrTerm [] open syn)
469462 <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
470463 -- No prefix operators! (bit of a hack here...)
471464 if (o == "-" || o == "!")
@@ -486,20 +479,59 @@ bracketed' open syn =
486479 <|> do l <- expr syn
487480 bracketedExpr syn open l
488481
482+
483+
484+{-| Parses the rest of a dependent pair after '(' or '(Expr **' -}
485+dependentPair :: PunInfo -> [(PTerm, Maybe (FC, PTerm), FC)] -> FC -> SyntaxInfo -> IdrisParser PTerm
486+dependentPair pun prev openFC syn =
487+ if prev == [] then
488+ nametypePart <|> namePart
489+ else
490+ case pun of
491+ IsType -> nametypePart <|> namePart <|> exprPart True
492+ IsTerm -> exprPart False
493+ TypeOrTerm -> nametypePart <|> namePart <|> exprPart False
494+ where nametypePart = do
495+ (ln, lnfc, colonFC) <- try $ do
496+ (ln, lnfc) <- name
497+ colonFC <- lcharFC ':'
498+ return (ln, lnfc, colonFC)
499+ lty <- expr' syn
500+ starsFC <- reservedOpFC "**"
501+ dependentPair IsType ((PRef lnfc [] ln, Just (colonFC, lty), starsFC):prev) openFC syn
502+ namePart = try $ do
503+ (ln, lnfc) <- name
504+ starsFC <- reservedOpFC "**"
505+ dependentPair pun ((PRef lnfc [] ln, Nothing, starsFC):prev) openFC syn
506+ exprPart isEnd = do
507+ e <- expr syn
508+ sepFCE <-
509+ let stars = (Left <$> reservedOpFC "**")
510+ ending = (Right <$> lcharFC ')')
511+ in if isEnd then ending else stars <|> ending
512+ case sepFCE of
513+ Left starsFC -> dependentPair IsTerm ((e, Nothing, starsFC):prev) openFC syn
514+ Right closeFC ->
515+ return (mkPDPairs pun openFC closeFC (reverse prev) e)
516+ mkPDPairs pun openFC closeFC ((e, cfclty, starsFC):bnds) r =
517+ (PDPair openFC ([openFC] ++ maybe [] ((: []) . fst) cfclty ++ [starsFC, closeFC] ++ (=<<) (\(_,cfclty,sfc) -> maybe [] ((: []) . fst) cfclty ++ [sfc]) bnds)
518+ pun e (maybe Placeholder snd cfclty) (mergePDPairs pun starsFC bnds r))
519+ mergePDPairs pun starsFC' [] r = r
520+ mergePDPairs pun starsFC' ((e, cfclty, starsFC):bnds) r =
521+ PDPair starsFC' [] pun e (maybe Placeholder snd cfclty) (mergePDPairs pun starsFC bnds r)
522+
489523-- | Parse the contents of parentheses, after an expression has been parsed.
490524bracketedExpr :: SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm
491525bracketedExpr syn openParenFC e =
492526 do lchar ')'; return e
493− <|> do exprs <- many (do comma <- lcharFC ','
527+ <|> do exprs <- some (do comma <- lcharFC ','
494528 r <- expr syn
495529 return (r, comma))
496530 closeParenFC <- lcharFC ')'
497531 let hilite = [openParenFC, closeParenFC] ++ map snd exprs
498532 return $ PPair openParenFC hilite TypeOrTerm e (mergePairs exprs)
499533 <|> do starsFC <- reservedOpFC "**"
500− r <- expr syn
501− closeParenFC <- lcharFC ')'
502− return (PDPair starsFC [openParenFC, starsFC, closeParenFC] TypeOrTerm e Placeholder r)
534+ dependentPair IsTerm [(e, Nothing, starsFC)] openParenFC syn
503535 <?> "end of bracketed expression"
504536 where mergePairs :: [(PTerm, FC)] -> PTerm
505537 mergePairs [(t, fc)] = t