fix parse issue for typed lamda arguments
This commit is contained in:
@@ -285,28 +285,16 @@ letExpr = do
|
|||||||
pure (name,fc,ty,t)
|
pure (name,fc,ty,t)
|
||||||
|
|
||||||
pLamArg : Parser (Icit × String × Maybe Raw)
|
pLamArg : Parser (Icit × String × Maybe Raw)
|
||||||
pLamArg = impArg <|> autoArg <|> expArg
|
pLamArg = impArg <|> expArg
|
||||||
<|> (\ x => (Explicit, x, Nothing)) <$> (ident <|> uident)
|
<|> (\ x => (Explicit, x, Nothing)) <$> (ident <|> uident)
|
||||||
<|> keyword "_" *> pure (Explicit, "_", Nothing)
|
<|> keyword "_" *> pure (Explicit, "_", Nothing)
|
||||||
where
|
where
|
||||||
|
-- TODO - we're moving away from uppercase variables, but a test uses them
|
||||||
impArg : Parser (Icit × String × Maybe Raw)
|
impArg : Parser (Icit × String × Maybe Raw)
|
||||||
impArg = do
|
impArg = (Implicit, ) <$> braces (_,_ <$> (ident <|> uident) <*> optional (symbol ":" >> typeExpr))
|
||||||
nm <- braces (ident <|> uident)
|
|
||||||
ty <- optional (symbol ":" >> typeExpr)
|
|
||||||
pure (Implicit, nm, ty)
|
|
||||||
|
|
||||||
autoArg : Parser (Icit × String × Maybe Raw)
|
|
||||||
autoArg = do
|
|
||||||
nm <- dbraces (ident <|> uident)
|
|
||||||
ty <- optional (symbol ":" >> typeExpr)
|
|
||||||
pure (Auto, nm, ty)
|
|
||||||
|
|
||||||
expArg : Parser (Icit × String × Maybe Raw)
|
expArg : Parser (Icit × String × Maybe Raw)
|
||||||
expArg = do
|
expArg = (Explicit , ) <$> parenWrap (_,_ <$> ident <*> optional (symbol ":" >> typeExpr))
|
||||||
nm <- parenWrap (ident <|> uident)
|
|
||||||
-- FIXME - this is broken, outside parenWrap, guess I never used it?
|
|
||||||
ty <- optional (symbol ":" >> typeExpr)
|
|
||||||
pure (Explicit, nm, ty)
|
|
||||||
|
|
||||||
lamExpr : Parser Raw
|
lamExpr : Parser Raw
|
||||||
lamExpr = do
|
lamExpr = do
|
||||||
|
|||||||
7
tests/LambdaArg.newt
Normal file
7
tests/LambdaArg.newt
Normal file
@@ -0,0 +1,7 @@
|
|||||||
|
module LambdaArg
|
||||||
|
|
||||||
|
import Prelude
|
||||||
|
|
||||||
|
-- Parsing of typed arguments on lambda
|
||||||
|
foo : Nat -> ({_ : U} -> Nat -> Nat)
|
||||||
|
foo x = \ {x : U} (x : Nat) => x
|
||||||
Reference in New Issue
Block a user