git.iko.soy/Idris-dev
on master help sign in
Support multiple let bindings
ecb9da6Edwin Brady
src/Idris/ParseExpr.hs+24−15
compare with master
unifiedsplit
@@ -780,23 +780,32 @@ TypeSig' ::=
780@
780@
781 -}
781 -}
782let_ :: SyntaxInfo -> IdrisParser PTerm
782let_ :: SyntaxInfo -> IdrisParser PTerm
783−let_ syn = try (do reserved "let"; fc <- getFC; n <- name;
783+let_ syn = try (do reserved "let"
784− ty <- option Placeholder (do lchar ':'; expr' syn)
784+ ls <- indentedBlock (let_binding syn)
785− lchar '='
786− v <- expr syn
787− ts <- option [] (do lchar '|'
788− sepBy1 (do_alt syn) (lchar '|'))
789 reserved "in"; sc <- expr syn
785 reserved "in"; sc <- expr syn
790− case ts of
786+ return (buildLets ls sc))
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 } )
787+-- <|> (do reserved "let"; fc <- getFC; pat <- expr' (syn { inPattern = True } )
794− symbol "="; v <- expr syn
788+-- symbol "="; v <- expr syn
795− ts <- option [] (do lchar '|'
789+-- ts <- option [] (do lchar '|'
796− sepBy1 (do_alt syn) (lchar '|'))
790+-- sepBy1 (do_alt syn) (lchar '|'))
797− reserved "in"; sc <- expr syn
791+-- reserved "in"; sc <- expr syn
798− return (PCase fc v ((pat, sc) : ts)))
792+-- return (PCase fc v ((pat, sc) : ts)))
799 <?> "let binding"
793 <?> "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+
800
809
801{- | Parses a quote goal
810{- | Parses a quote goal
802
811
src/Idris/ParseHelpers.hs+4−2
@@ -439,7 +439,8 @@ closeBlock = do ist <- get
439 Nothing : xs -> lchar '}' >> return xs <?> "end of block"
439 Nothing : xs -> lchar '}' >> return xs <?> "end of block"
440 Just lvl : xs -> (do i <- indent
440 Just lvl : xs -> (do i <- indent
441 isParen <- lookAheadMatches (char ')')
441 isParen <- lookAheadMatches (char ')')
442+ isIn <- lookAheadMatches (reserved "in")
442− if i >= lvl && not isParen
443+ if i >= lvl && not (isParen || isIn)
443 then fail "not end of block"
444 then fail "not end of block"
444 else return xs)
445 else return xs)
445 <|> (do notOpenBraces
446 <|> (do notOpenBraces
@@ -462,7 +463,8 @@ keepTerminator = do lchar ';'; return ()
462 <|> do c <- indent; l <- lastIndent
463 <|> do c <- indent; l <- lastIndent
463 unless (c <= l) $ fail "not a terminator"
464 unless (c <= l) $ fail "not a terminator"
464 <|> do isParen <- lookAheadMatches (oneOf ")}|")
465 <|> do isParen <- lookAheadMatches (oneOf ")}|")
466+ isIn <- lookAheadMatches (reserved "in")
465− unless isParen $ fail "not a terminator"
467+ unless (isIn || isParen) $ fail "not a terminator"
466 <|> lookAhead eof
468 <|> lookAhead eof
467
469
468-- | Checks if application expression does not end
470-- | Checks if application expression does not end