on master help sign in
Merge branch 'feature/deppairparsing' of https://github.com/ahmadsalim/Idris-dev into ahmadsalim-feature/deppairparsing

Conflicts: CHANGELOG

commitf3ce68ea69c20fe9f395e8dde32762194709408f authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSun 27 Sep 2015, 10:30 (11 years ago) parent2f7d8c2894f664
3 files changed+33−14
CHANGELOG+4 src/Idris/ParseExpr.hs+26−11 test/proof003/test015.idr+3−3
CHANGELOG+4
@@ -16,6 +16,10 @@ Language updates
1616 valid unbound implicit is now *always* an unbound implicit. This is much
1717 more resilient to changes in inputs, but does require that function names
1818 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+
1923
2024Library updates
2125---------------
src/Idris/ParseExpr.hs+26−11
@@ -462,14 +462,19 @@ bracketed' open syn =
462462 do (FC f start (l, c)) <- getFC
463463 lchar ')'
464464 return $ PTrue (spanFC open (FC f start (l, c+1))) TypeOrTerm
465− <|> try (do (ln, lnfc) <- name
466− colonFC <- lcharFC ':'
467− lty <- expr syn
468− starsFC <- reservedOpFC "**"
465+ <|> try (do (ln, lnfc, colonFC, lty, starsFC):bnds <- some $ do
466+ (ln, lnfc, colonFC) <- try $ do
467+ (ln, lnfc) <- name
468+ colonFC <- lcharFC ':'
469+ return (ln, lnfc, colonFC)
470+ lty <- expr syn
471+ starsFC <- reservedOpFC "**"
472+ return (ln, lnfc, colonFC, lty, starsFC)
469473 fc <- getFC
470474 r <- expr syn
471475 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)))
473478 <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
474479 -- No prefix operators! (bit of a hack here...)
475480 if (o == "-" || o == "!")
@@ -480,7 +485,7 @@ bracketed' open syn =
480485 <|> try (do l <- simpleExpr syn
481486 op <- option Nothing (do o <- operator
482487 lchar ')'
483− return (Just o))
488+ return (Just o))
484489 fc0 <- getFC
485490 case op of
486491 Nothing -> bracketedExpr syn open l
@@ -489,25 +494,35 @@ bracketed' open syn =
489494 pexp (PRef fc0 [] (sMN 1000 "ARG"))]))
490495 <|> do l <- expr syn
491496 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+
493502-- | Parse the contents of parentheses, after an expression has been parsed.
494503bracketedExpr :: SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm
495504bracketedExpr syn openParenFC e =
496505 do lchar ')'; return e
497− <|> do exprs <- many (do comma <- lcharFC ','
506+ <|> do exprs <- some (do comma <- lcharFC ','
498507 r <- expr syn
499508 return (r, comma))
500509 closeParenFC <- lcharFC ')'
501510 let hilite = [openParenFC, closeParenFC] ++ map snd exprs
502511 return $ PPair openParenFC hilite TypeOrTerm e (mergePairs exprs)
503− <|> do starsFC <- reservedOpFC "**"
504− r <- expr syn
512+ <|> do exprs <- some $ do
513+ starsFC <- reservedOpFC "**"
514+ r <- expr syn
515+ return (r, starsFC)
505516 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))
507519 <?> "end of bracketed expression"
508520 where mergePairs :: [(PTerm, FC)] -> PTerm
509521 mergePairs [(t, fc)] = t
510522 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)
511526
512527-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a
513528-- 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)
4444testBin : Maybe (Binary 8 42)
4545testBin = natToBin _ _
4646
47−pattern syntax bitpair [x] [y] = (_ ** (_ ** (x, y, _)))
48−term syntax bitpair [x] [y] = (_ ** (_ ** (x, y, Refl)))
47+pattern syntax bitpair [x] [y] = (_ ** _ ** (x, y, _))
48+term syntax bitpair [x] [y] = (_ ** _ ** (x, y, Refl))
4949
5050addBit : 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))
5252addBit b0 b0 b0 = bitpair b0 b0
5353addBit b0 b0 b1 = bitpair b0 b1
5454addBit b0 b1 b0 = bitpair b0 b1