a7f75c5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'feature/deppairparsing' of https://github.com/ahmadsalim/Idris-dev into ahmadsalim-feature/deppairparsing

a7f75c5Edwin Brady11 years ago

CHANGELOG+3

compare with master

unifiedsplit

@@ -101,6 +101,9 @@ New in 0.10:

101 Where `CATS` is a whitespace separated list of categoriese. Default is for

102 all categories to be logged.

103* New flag `--listlogcats` to list logging categories.`

104+* Dependent pairs now can be specified using a telescope-style syntax, without

105+ requirement of nesting, e.g. it is possible to now write the following:

106+ (a : Type ** n : Nat ** Vect n a)

104

107

105New in 0.9.20:

108New in 0.9.20:

106==============

109==============

src/Idris/AbsSyntaxTree.hs+34−14

@@ -1879,23 +1879,38 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1879 align . group . vsep . punctuate (ann comma) $

1880 map (prettySe (decD d) startPrec bnd) elts

1881 where ann = case pun of

1882− TypeOrTerm -> id

1882+ TypeOrTerm -> id

1883− IsType -> annName pairTy

1883+ IsType -> annName pairTy

1884− IsTerm -> annName pairCon

1884+ IsTerm -> annName pairCon

1885− prettySe d p bnd (PDPair _ _ pun l t r) =

1885+ prettySe d p bnd dpair@(PDPair _ _ pun l t r)

1886− depth d $

1886+ | Just elts <- dPairElts dpair

1887+ = depth d . enclose (annotated lparen) (annotated rparen) .

1888+ align . group . vsep . punctuate (space <> annotated (text "**")) $

1889+ ppElts elts bnd

1890+ | otherwise

1891+ = depth d $

1887− annotated lparen <>

1892+ annotated lparen <>

1888− left <+>

1893+ left <+>

1889− annotated (text "**") <+>

1894+ annotated (text "**") <+>

1890− prettySe (decD d) startPrec (addBinding bnd) r <>

1895+ prettySe (decD d) startPrec (addBinding bnd) r <>

1891− annotated rparen

1896+ annotated rparen

1892 where annotated = case pun of

1897 where annotated = case pun of

1893− IsType -> annName sigmaTy

1898+ IsType -> annName sigmaTy

1894− IsTerm -> annName sigmaCon

1899+ IsTerm -> annName sigmaCon

1895− TypeOrTerm -> id

1900+ TypeOrTerm -> id

1901+

1896 (left, addBinding) = case (l, pun) of

1902 (left, addBinding) = case (l, pun) of

1897 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))

1903 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))

1898− _ -> (prettySe (decD d) startPrec bnd l, id)

1904+ _ -> (prettySe (decD d) startPrec bnd l, id)

1905+

1906+ ppElts [] bs = []

1907+ ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]

1908+ ppElts ((PRef _ _ n, t):rs) bs

1909+ | IsType <- pun

1910+ = (bindingOf n False <+> colon <+>

1911+ prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)

1912+ ppElts ((l, t):rs) bs

1913+ = (prettySe (decD d) startPrec bs l) : ppElts rs bs

1899 prettySe d p bnd (PAlternative ns a as) =

1914 prettySe d p bnd (PAlternative ns a as) =

1900 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1915 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1901 where

1916 where

@@ -2014,6 +2029,11 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

2014 | otherwise = Just [x, y]

2029 | otherwise = Just [x, y]

2015 pairElts _ = Nothing

2030 pairElts _ = Nothing

2016

2031

2032+ dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]

2033+ dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)

2034+ | otherwise = Just [(l, t), (Placeholder, r)]

2035+ dPairElts _ = Nothing

2036+

2017 natns = "Prelude.Nat."

2037 natns = "Prelude.Nat."

2018

2038

2019 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer

2039 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer

src/Idris/Parser/Expr.hs+47−15

@@ -398,7 +398,7 @@ simpleExpr syn =

398 <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc [] (SN $ ElimN t))

399 <|> proofExpr syn

400 <|> tacticsExpr syn

401− <|> try (do reserved "Type"; symbol "*"; return $ PUniverse AllTypes)

401+ <|> try (do reserved "Type*"; return $ PUniverse AllTypes)

402 <|> do reserved "AnyType"; return $ PUniverse AllTypes

403 <|> PType <$> reservedFC "Type"

404 <|> do reserved "UniqueType"; return $ PUniverse UniqueType

@@ -440,16 +440,16 @@ bracketed :: SyntaxInfo -> IdrisParser PTerm

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

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

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

443+

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

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

444@

445@

445Bracketed' ::=

446Bracketed' ::=

446 ')'

447 ')'

447 | Expr ')'

448 | Expr ')'

448 | ExprList ')'

449 | ExprList ')'

449− | Expr '**' Expr ')'

450+ | DependentPair ')'

450 | Operator Expr ')'

451 | Operator Expr ')'

451 | Expr Operator ')'

452 | Expr Operator ')'

452− | Name ':' Expr '**' Expr ')'

453 ;

454@

455-}

@@ -458,14 +458,7 @@ bracketed' open syn =

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

459 lchar ')'

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

461− <|> try (do (ln, lnfc) <- name

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

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

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

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

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

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

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

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

@@ -486,20 +479,59 @@ bracketed' open syn =

486 <|> do l <- expr syn

479 <|> do l <- expr syn

487 bracketedExpr syn open l

480 bracketedExpr syn open l

488

481

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+

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

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

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

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

491bracketedExpr syn openParenFC e =

525bracketedExpr syn openParenFC e =

492 do lchar ')'; return e

526 do lchar ')'; return e

493− <|> do exprs <- many (do comma <- lcharFC ','

527+ <|> do exprs <- some (do comma <- lcharFC ','

494 r <- expr syn

528 r <- expr syn

495 return (r, comma))

529 return (r, comma))

496 closeParenFC <- lcharFC ')'

530 closeParenFC <- lcharFC ')'

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

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

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

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

499 <|> do starsFC <- reservedOpFC "**"

533 <|> do starsFC <- reservedOpFC "**"

500− r <- expr syn

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

501− closeParenFC <- lcharFC ')'

502− return (PDPair starsFC [openParenFC, starsFC, closeParenFC] TypeOrTerm e Placeholder r)

503 <?> "end of bracketed expression"

535 <?> "end of bracketed expression"

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

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

505 mergePairs [(t, fc)] = t

537 mergePairs [(t, fc)] = t

test/proof003/test015.idr+3−3

@@ -44,11 +44,11 @@ natToBin (S w) (S k) with (parity k)

44testBin : Maybe (Binary 8 42)

45testBin = natToBin _ _

47−pattern syntax bitpair [x] [y] = (_ ** (_ ** (x, y, _)))

47+pattern syntax bitpair [x] [y] = (_ ** _ ** (x, y, _))

48−term syntax bitpair [x] [y] = (_ ** (_ ** (x, y, Refl)))

48+term syntax bitpair [x] [y] = (_ ** _ ** (x, y, Refl))

50addBit : Bit x -> Bit y -> Bit c ->

51− (bX ** (bY ** (Bit bX, Bit bY, c + x + y = bY + 2 * bX)))

51+ (bX ** bY ** (Bit bX, Bit bY, c + x + y = bY + 2 * bX))

52addBit B0 B0 B0 = bitpair B0 B0

53addBit B0 B0 B1 = bitpair B0 B1

54addBit B0 B1 B0 = bitpair B0 B1