894f664 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allowed multiple bindings in dependent pairs

894f664Ahmad Salim Al-Sibahi11 years ago

CHANGELOG+3

compare with master

unifiedsplit

@@ -9,6 +9,9 @@ Language updates

9 for defining new names. `{n} still quotes n to an existing name in scope.

10* A new primitive operator prim__strSubstr for more efficient extraction of

11 substrings. External code generators should implement this.

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

13+requirement of nesting, e.g. it is possible to now write (a : Type ** n : Nat

14+** Vect n a).

13Library updates

16Library updates

14---------------

17---------------

src/Idris/ParseExpr.hs+26−11

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

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

453 lchar ')'

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

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

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

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

457+ (ln, lnfc) <- name

456− colonFC <- lcharFC ':'

458+ colonFC <- lcharFC ':'

459+ return (ln, lnfc, colonFC)

457− lty <- expr syn

460+ lty <- expr syn

458− starsFC <- reservedOpFC "**"

461+ starsFC <- reservedOpFC "**"

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

459 fc <- getFC

463 fc <- getFC

460 r <- expr syn

464 r <- expr syn

461 close <- lcharFC ')'

465 close <- lcharFC ')'

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

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

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

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

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

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

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

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

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

@@ -470,7 +475,7 @@ bracketed' open syn =

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

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

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

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

472 lchar ')'

477 lchar ')'

473− return (Just o))

478+ return (Just o))

474 fc0 <- getFC

479 fc0 <- getFC

475 case op of

480 case op of

476 Nothing -> bracketedExpr syn open l

481 Nothing -> bracketedExpr syn open l

@@ -479,25 +484,35 @@ bracketed' open syn =

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

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

480 <|> do l <- expr syn

485 <|> do l <- expr syn

481 bracketedExpr syn open l

486 bracketedExpr syn open l

482−

487+ where mergePDPairs :: FC -> [(Name, FC, FC, PTerm, FC)] -> PTerm -> PTerm

488+ mergePDPairs starsFC' [] r = r

489+ mergePDPairs starsFC' ((ln, lnfc, colonFC, lty, starsFC):bnds) r =

490+ PDPair starsFC' [] TypeOrTerm (PRef lnfc [] ln) lty (mergePDPairs starsFC bnds r)

491+

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

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

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

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

485bracketedExpr syn openParenFC e =

494bracketedExpr syn openParenFC e =

486 do lchar ')'; return e

495 do lchar ')'; return e

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

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

488 r <- expr syn

497 r <- expr syn

489 return (r, comma))

498 return (r, comma))

490 closeParenFC <- lcharFC ')'

499 closeParenFC <- lcharFC ')'

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

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

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

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

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

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

503+ starsFC <- reservedOpFC "**"

494− r <- expr syn

504+ r <- expr syn

505+ return (r, starsFC)

495 closeParenFC <- lcharFC ')'

506 closeParenFC <- lcharFC ')'

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

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

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

497 <?> "end of bracketed expression"

509 <?> "end of bracketed expression"

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

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

499 mergePairs [(t, fc)] = t

511 mergePairs [(t, fc)] = t

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

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

513+ mergePDPairs :: [(PTerm, FC)] -> PTerm

514+ mergePDPairs [(t, fc)] = t

515+ mergePDPairs ((t, fc):rs) = PDPair fc [] TypeOrTerm t Placeholder (mergePDPairs rs)

501

516

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

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

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

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