Add support for short lambdas

Now, "\a b.a" is the same as "\a.\b.a".
This commit is contained in:
Joscha 2017-11-25 22:36:46 +00:00
parent 511ab62af5
commit 91fd370380

View file

@ -58,25 +58,19 @@ renameUniquely = rename_ []
in ELambda name (rename_ (name : c) e) in ELambda name (rename_ (name : c) e)
display :: (Show s) => Bool -> Expression s -> String display :: (Show s) => Bool -> Expression s -> String
display unicode = display_ [] . renameUniquely display unicode = d [] . renameUniquely
where display_ c (EReference n) where l = if unicode then "λ" else "\\"
d c (EReference n)
| n >= 0 && n < length c = c !! n | n >= 0 && n < length c = c !! n
| otherwise = "ERR" -- TODO: Deal with errors properly? | otherwise = "ERR"
display_ c (ESymbol s) = s d c (ESymbol s) = s
display_ c (ELambda s e) = d c (ELambda s e@(ELambda _ _)) = l ++ s ++ " " ++ (tail $ d (s:c) e)
(if unicode then "λ" else "\\") ++ s ++ "." ++ display_ (s : c) e d c (ELambda s e) = l ++ s ++ "." ++ d (s:c) e
display_ c (EExpr a@(ELambda _ _) b@(ELambda _ _)) = d c (EExpr a@(ELambda _ _) b@(ELambda _ _)) = "(" ++ d c a ++ ") (" ++ d c b ++ ")"
"(" ++ display_ c a ++ ") (" ++ display_ c b ++ ")" d c (EExpr a@(ELambda _ _) b@(EExpr _ _) ) = "(" ++ d c a ++ ") (" ++ d c b ++ ")"
display_ c (EExpr a@(ELambda _ _) b@(EExpr _ _)) = d c (EExpr a b@(ELambda _ _)) = d c a ++ " (" ++ d c b ++ ")"
"(" ++ display_ c a ++ ") (" ++ display_ c b ++ ")" d c (EExpr a b@(EExpr _ _) ) = d c a ++ " (" ++ d c b ++ ")"
display_ c (EExpr a@(ELambda _ _) b ) = d c (EExpr a b ) = d c a ++ " " ++ d c b
"(" ++ display_ c a ++ ") " ++ display_ c b
display_ c (EExpr a b@(ELambda _ _)) =
display_ c a ++ " (" ++ display_ c b ++ ")"
display_ c (EExpr a b@(EExpr _ _)) =
display_ c a ++ " (" ++ display_ c b ++ ")"
display_ c (EExpr a b) =
display_ c a ++ " " ++ display_ c b
{- {-
- Evaluating expressions - Evaluating expressions
@ -136,19 +130,22 @@ parenthesize parser = do
satisfy $ isClosingParen paren satisfy $ isClosingParen paren
return result return result
parseSymbol :: ReadP (Expression String) parseSymbolStr :: ReadP String
parseSymbol = do parseSymbolStr = do
a <- munch1 (`elem` ['a'..'z']) a <- munch1 (`elem` ['a'..'z'])
b <- munch (=='\'') b <- munch (== '\'')
return $ ESymbol (a ++ b) return $ a ++ b
parseSymbol :: ReadP (Expression String)
parseSymbol = parseSymbolStr >>= (return . ESymbol)
parseLambda :: ReadP (Expression String) parseLambda :: ReadP (Expression String)
parseLambda = do parseLambda = do
char '\\' +++ char 'λ' char '\\' +++ char 'λ'
(ESymbol s) <- parseSymbol symbols <- many1' $ between skipSpaces skipSpaces parseSymbolStr
char '.' char '.'
e <- parseExpr e <- parseExpr
return $ ELambda s e return $ foldr ELambda e symbols
parseExpr :: ReadP (Expression String) parseExpr :: ReadP (Expression String)
parseExpr = parseExpr =