9560761 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Refactor and adjust doc comments

9560761Melvar Chen12 years ago

src/Idris/ParseExpr.hs+21−10

compare with master

unifiedsplit

@@ -234,6 +234,14 @@ internalExpr syn =

234 <|> app syn

235 <?> "expression"

236

237+{- | Parses the "impossible" keyword

238+@

239+Impossible ::= 'impossible'

240+@

241+-}

242+impossible :: IdrisParser PTerm

243+impossible = PImpossible <$ reserved "impossible"

244+

237{- | Parses a case expression

245{- | Parses a case expression

238@

246@

239CaseExpr ::=

247CaseExpr ::=

@@ -250,13 +258,13 @@ caseExpr syn = do reserved "case"; fc <- getFC

250{- | Parses a case in a case expression

258{- | Parses a case in a case expression

251@

259@

252CaseOption ::=

260CaseOption ::=

253− Expr '=>' Expr Terminator

261+ Expr (Impossible | '=>' Expr) Terminator

254 ;

262 ;

255@

263@

256-}

264-}

257caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)

265caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)

258caseOption syn = do lhs <- expr (syn { inPattern = True })

266caseOption syn = do lhs <- expr (syn { inPattern = True })

259− r <- PImpossible <$ reserved "impossible" <|> do symbol "=>"; expr syn

267+ r <- impossible <|> symbol "=>" *> expr syn

260 return (lhs, r)

268 return (lhs, r)

261 <?> "case option"

269 <?> "case option"

262

270

@@ -732,8 +740,8 @@ typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else retu

732{- | Parses a lambda expression

740{- | Parses a lambda expression

733@

741@

734Lambda ::=

742Lambda ::=

735− '\\' TypeOptDeclList '=>' Expr

743+ '\\' TypeOptDeclList LambdaTail

736− | '\\' SimpleExprList '=>' Expr

744+ | '\\' SimpleExprList LambdaTail

737 ;

745 ;

738@

746@

739@

747@

@@ -742,21 +750,22 @@ SimpleExprList ::=

742 | SimpleExpr ',' SimpleExprList

750 | SimpleExpr ',' SimpleExprList

743 ;

751 ;

744@

752@

753+@

754+LambdaTail ::=

755+ Impossible

756+ | '=>' Expr

757+@

745-}

758-}

746lambda :: SyntaxInfo -> IdrisParser PTerm

759lambda :: SyntaxInfo -> IdrisParser PTerm

747lambda syn = do lchar '\\' <?> "lambda expression"

760lambda syn = do lchar '\\' <?> "lambda expression"

748 (do xt <- try $ tyOptDeclList syn

761 (do xt <- try $ tyOptDeclList syn

749 fc <- getFC

762 fc <- getFC

750− sc <- PImpossible <$ reserved "impossible" <|> do

763+ sc <- lambdaTail

751− symbol "=>"

752− expr syn

753 return (bindList (PLam fc) xt sc)) <|> do

764 return (bindList (PLam fc) xt sc)) <|> do

754 ps <- sepBy (do fc <- getFC

765 ps <- sepBy (do fc <- getFC

755 e <- simpleExpr (syn { inPattern = True })

766 e <- simpleExpr (syn { inPattern = True })

756 return (fc, e)) (lchar ',')

767 return (fc, e)) (lchar ',')

757− sc <- PImpossible <$ reserved "impossible" <|> do

768+ sc <- lambdaTail

758− symbol "=>"

759− expr syn

760 return (pmList (zip [0..] ps) sc)

769 return (pmList (zip [0..] ps) sc)

761 <?> "lambda expression"

770 <?> "lambda expression"

762 where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm

771 where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm

@@ -765,6 +774,8 @@ lambda syn = do lchar '\\' <?> "lambda expression"

765 = PLam fc (sMN i "lamp") Placeholder

774 = PLam fc (sMN i "lamp") Placeholder

766 (PCase fc (PRef fc (sMN i "lamp"))

775 (PCase fc (PRef fc (sMN i "lamp"))

767 [(x, pmList xs sc)])

776 [(x, pmList xs sc)])

777+ lambdaTail :: IdrisParser PTerm

778+ lambdaTail = impossible <|> symbol "=>" *> expr syn

768

779

769{- | Parses a term rewrite expression

780{- | Parses a term rewrite expression

770@

781@

src/Idris/Parser.hs+2−2

@@ -811,7 +811,7 @@ argExpr syn = let syn' = syn { inPattern = True } in

811@

812RHS ::= '=' Expr

813 | '?=' RHSName? Expr

814− | 'impossible'

814+ | Impossible

815 ;

816@

817

@@ -827,7 +827,7 @@ rhs syn n = do lchar '='; expr syn

827 return n)

828 r <- expr syn

829 return (addLet fc name r)

830− <|> do reserved "impossible"; return PImpossible

830+ <|> impossible

831 <?> "function right hand side"

832 where mkN :: Name -> Name

833 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))