ecb9da6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Support multiple let bindings

This sort of thing now works: test : Nat -> Nat test n = let foo = n S k = plus foo foo in k The bindings must be aligned, and the keyword 'in' (indented however you like within the 'test' block) terminates the list. Pattern match alternatives are also supported, for quickly catching failures: test2 : Nat -> Nat test2 n = let foo = n S k = plus foo foo | Z => 42 in k Fixes #1362

commitecb9da6d767d4e8ef778f6e2da9b0e1a2e46117d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 9 Jul 2014, 21:54 (12 years ago) parent1269791

2 files changed+28−17

compare with master

unifiedsplit

src/Idris/ParseExpr.hs+24−15 src/Idris/ParseHelpers.hs+4−2

src/Idris/ParseExpr.hs+24−15

@@ -780,23 +780,32 @@ TypeSig' ::=

780780@

781781 -}

782782let_ :: SyntaxInfo -> IdrisParser PTerm

783−let_ syn = try (do reserved "let"; fc <- getFC; n <- name;

784− ty <- option Placeholder (do lchar ':'; expr' syn)

785− lchar '='

786− v <- expr syn

787− ts <- option [] (do lchar '|'

788− sepBy1 (do_alt syn) (lchar '|'))

783+let_ syn = try (do reserved "let"

784+ ls <- indentedBlock (let_binding syn)

789785 reserved "in"; sc <- expr syn

790− case ts of

791− [] -> return (PLet n ty v sc)

792− alts -> return (PCase fc v ((PRef fc n, sc) : ts)))

793− <|> (do reserved "let"; fc <- getFC; pat <- expr' (syn { inPattern = True } )

794− symbol "="; v <- expr syn

795− ts <- option [] (do lchar '|'

796− sepBy1 (do_alt syn) (lchar '|'))

797− reserved "in"; sc <- expr syn

798− return (PCase fc v ((pat, sc) : ts)))

786+ return (buildLets ls sc))

787+-- <|> (do reserved "let"; fc <- getFC; pat <- expr' (syn { inPattern = True } )

788+-- symbol "="; v <- expr syn

789+-- ts <- option [] (do lchar '|'

790+-- sepBy1 (do_alt syn) (lchar '|'))

791+-- reserved "in"; sc <- expr syn

792+-- return (PCase fc v ((pat, sc) : ts)))

799793 <?> "let binding"

794+ where buildLets [] sc = sc

795+ buildLets ((fc,PRef _ n,ty,v,[]):ls) sc

796+ = PLet n ty v (buildLets ls sc)

797+ buildLets ((fc,pat,ty,v,alts):ls) sc

798+ = PCase fc v ((pat, buildLets ls sc) : alts)

799+

800+let_binding syn = do fc <- getFC;

801+ pat <- expr' (syn { inPattern = True })

802+ ty <- option Placeholder (do lchar ':'; expr' syn)

803+ lchar '='

804+ v <- expr syn

805+ ts <- option [] (do lchar '|'

806+ sepBy1 (do_alt syn) (lchar '|'))

807+ return (fc,pat,ty,v,ts)

808+

800809

801810{- | Parses a quote goal

802811

src/Idris/ParseHelpers.hs+4−2

@@ -439,7 +439,8 @@ closeBlock = do ist <- get

439439 Nothing : xs -> lchar '}' >> return xs <?> "end of block"

440440 Just lvl : xs -> (do i <- indent

441441 isParen <- lookAheadMatches (char ')')

442− if i >= lvl && not isParen

442+ isIn <- lookAheadMatches (reserved "in")

443+ if i >= lvl && not (isParen || isIn)

443444 then fail "not end of block"

444445 else return xs)

445446 <|> (do notOpenBraces

@@ -462,7 +463,8 @@ keepTerminator = do lchar ';'; return ()

462463 <|> do c <- indent; l <- lastIndent

463464 unless (c <= l) $ fail "not a terminator"

464465 <|> do isParen <- lookAheadMatches (oneOf ")}|")

465− unless isParen $ fail "not a terminator"

466+ isIn <- lookAheadMatches (reserved "in")

467+ unless (isIn || isParen) $ fail "not a terminator"

466468 <|> lookAhead eof

467469

468470-- | Checks if application expression does not end