f3ce68e · 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

f3ce68eDavid Raymond Christiansen11 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/ParseExpr.hs+26−11

@@ -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/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