dcacfea · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

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

dcacfeaAhmad Salim Al-Sibahi11 years ago

CHANGELOG+4

compare with master

unifiedsplit

@@ -16,6 +16,10 @@ Language updates

16 valid unbound implicit is now *always* an unbound implicit. This is much

17 more resilient to changes in inputs, but does require that function names

18 be explicitly qualified when in argument position.

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

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

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

22+

20Library updates

24Library updates

21---------------

25---------------

src/Idris/AbsSyntaxTree.hs+27−7

@@ -1820,20 +1820,35 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1820 TypeOrTerm -> id

1821 IsType -> annName pairTy

1822 IsTerm -> annName pairCon

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

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

1824− depth d $

1824+ | Just elts <- dPairElts dpair

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

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

1827+ ppElts elts bnd

1828+ | otherwise

1829+ = depth d $

1825− annotated lparen <>

1830+ annotated lparen <>

1826− left <+>

1831+ left <+>

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

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

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

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

1829− annotated rparen

1834+ annotated rparen

1830 where annotated = case pun of

1835 where annotated = case pun of

1831 IsType -> annName sigmaTy

1836 IsType -> annName sigmaTy

1832 IsTerm -> annName sigmaCon

1837 IsTerm -> annName sigmaCon

1833 TypeOrTerm -> id

1838 TypeOrTerm -> id

1839+

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

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

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

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

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

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

1843+

1844+ ppElts [] bs = []

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

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

1847+ | IsType <- pun

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

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

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

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

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

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

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

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

1839 where

1854 where

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

1951 | otherwise = Just [x, y]

1966 | otherwise = Just [x, y]

1952 pairElts _ = Nothing

1967 pairElts _ = Nothing

1953

1968

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

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

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

1972+ dPairElts _ = Nothing

1973+

1954 natns = "Prelude.Nat."

1974 natns = "Prelude.Nat."

1955

1975

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

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

src/Idris/ParseExpr.hs+27−12

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

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

403 <|> proofExpr syn

404 <|> tacticsExpr syn

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

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

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

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

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

@@ -462,14 +462,19 @@ bracketed' open syn =

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

463 lchar ')'

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

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

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

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

467+ (ln, lnfc) <- name

466− colonFC <- lcharFC ':'

468+ colonFC <- lcharFC ':'

469+ return (ln, lnfc, colonFC)

467− lty <- expr syn

470+ lty <- expr' syn

468− starsFC <- reservedOpFC "**"

471+ starsFC <- reservedOpFC "**"

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

469 fc <- getFC

473 fc <- getFC

470 r <- expr syn

474 r <- expr syn

471 close <- lcharFC ')'

475 close <- lcharFC ')'

472− return (PDPair fc [open, colonFC, starsFC, close] TypeOrTerm (PRef lnfc [] ln) lty r))

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

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

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

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

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

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

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

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

@@ -480,7 +485,7 @@ bracketed' open syn =

480 <|> try (do l <- simpleExpr syn

485 <|> try (do l <- simpleExpr syn

481 op <- option Nothing (do o <- operator

486 op <- option Nothing (do o <- operator

482 lchar ')'

487 lchar ')'

483− return (Just o))

488+ return (Just o))

484 fc0 <- getFC

489 fc0 <- getFC

485 case op of

490 case op of

486 Nothing -> bracketedExpr syn open l

491 Nothing -> bracketedExpr syn open l

@@ -489,25 +494,35 @@ bracketed' open syn =

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

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

490 <|> do l <- expr syn

495 <|> do l <- expr syn

491 bracketedExpr syn open l

496 bracketedExpr syn open l

492−

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+

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

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

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

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

495bracketedExpr syn openParenFC e =

504bracketedExpr syn openParenFC e =

496 do lchar ')'; return e

505 do lchar ')'; return e

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

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

498 r <- expr syn

507 r <- expr syn

499 return (r, comma))

508 return (r, comma))

500 closeParenFC <- lcharFC ')'

509 closeParenFC <- lcharFC ')'

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

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

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

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

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

503− <|> do starsFC <- reservedOpFC "**"

513+ starsFC <- reservedOpFC "**"

504− r <- expr syn

514+ r <- expr syn

515+ return (r, starsFC)

505 closeParenFC <- lcharFC ')'

516 closeParenFC <- lcharFC ')'

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

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

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

507 <?> "end of bracketed expression"

519 <?> "end of bracketed expression"

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

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

509 mergePairs [(t, fc)] = t

521 mergePairs [(t, fc)] = t

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

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

511

526

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

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

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

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

test/proof003/expected−12

@@ -1,15 +1,3 @@

1−Parity.idr:15:18-23:

2−This style of tactic proof is deprecated. See %runElab for the replacement.

3−Parity.idr:22:18-23:

4−This style of tactic proof is deprecated. See %runElab for the replacement.

5−test015.idr:88:15-20:

6−This style of tactic proof is deprecated. See %runElab for the replacement.

7−test015.idr:97:16-21:

8−This style of tactic proof is deprecated. See %runElab for the replacement.

9−test015.idr:108:20-25:

10−This style of tactic proof is deprecated. See %runElab for the replacement.

11−test015.idr:136:20-25:

12−This style of tactic proof is deprecated. See %runElab for the replacement.

1300101010

100101010

1401011001

201011001

15010000011

3010000011

test/proof003/run+1−1

@@ -1,4 +1,4 @@

1#!/usr/bin/env bash

2−idris $@ test015.idr --nocolour --consolewidth 80 -o test015

2+idris $@ test015.idr --nocolour --consolewidth 80 --no-tactic-deprecation-warnings -o test015

3./test015

4rm -f test015 Parity.ibc test015.ibc

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