diff --git a/.editorconfig b/.editorconfig new file mode 100644 index 0000000..e2139a6 --- /dev/null +++ b/.editorconfig @@ -0,0 +1,11 @@ +root = true + +[*] +charset = utf-8 +indent_style = space +indent_size = 4 +trim_trailing_whitespace = true +insert_final_newline = true + +[*.yml] +indent_size = 2 diff --git a/README.md b/README.md index 4f3526f..d3f8c7d 100644 --- a/README.md +++ b/README.md @@ -9,7 +9,7 @@ Exit the prompt with `Ctrl-c` (or equivalent). ### Example session ``` ->> let D = (\x. x x) in let F = (\f. f (f y)) in D (F (\x. x)) +>> let D = (\x. x x); F = (\f. f (f y)) in D (F (\x. x)) (y y) >> let T = (\f x. f (f x)) in (\f x. T (T (T (T T))) f x) (\x. x) y y @@ -29,4 +29,5 @@ and spaces are used to separate variables rather than commas. * Applications are left-associative: `M N P` may be written instead of `((M N) P)`. * The body of an abstraction or let expression extends as far right as possible: `\x. M N` means `\x.(M N)` and not `(\x. M) N`. * A sequence of abstractions may be contracted: `\foo. \bar. \baz. N` may be abbreviated as `\foo bar baz. N`. -* Variables may be bound using let expressions: `let x = N in M` is syntactic sugar for `(\x. N) M`. \ No newline at end of file +* Variables may be bound using let expressions: `let x = N in M` is syntactic sugar for `(\x. N) M`. +* Multiple variables may be defined in one let expression: `let x = N; y = O in M` diff --git a/src/LambdaCalculus/Expression.hs b/src/LambdaCalculus/Expression.hs index 1e06ce0..c0b8770 100644 --- a/src/LambdaCalculus/Expression.hs +++ b/src/LambdaCalculus/Expression.hs @@ -19,7 +19,7 @@ data Expression instance TextShow Expression where showb (Variable var) = fromText var showb (Application ef ex) = "(" <> showb ef <> " " <> showb ex <> ")" - showb (Abstraction var body) = "(\\" <> fromText var <> ". " <> showb body <> ")" + showb (Abstraction var body) = "(λ" <> fromText var <> ". " <> showb body <> ")" instance Show Expression where show = T.unpack . showt diff --git a/src/LambdaCalculus/Parser.hs b/src/LambdaCalculus/Parser.hs index e14e455..02d67a0 100644 --- a/src/LambdaCalculus/Parser.hs +++ b/src/LambdaCalculus/Parser.hs @@ -8,52 +8,58 @@ import LambdaCalculus.Expression import Text.Parsec hiding (spaces) import Text.Parsec.Text -spaces :: Parser () -spaces = void $ many1 space +keywords :: [Text] +keywords = ["let", "in"] -variableName :: Parser Text -variableName = do - notFollowedBy anyKeyword - T.pack <$> many1 letter - where anyKeyword = choice $ map keyword keywords - keywords = ["let", "in"] - --- | Match an exact string which is not just a substring --- of a larger variable name. +-- | A keyword is an exact string which is not part of an identifier. keyword :: Text -> Parser () -keyword kwd = try $ do - void $ string (T.unpack kwd) - notFollowedBy letter +keyword kwd = do + void $ string (T.unpack kwd) + notFollowedBy letter + +-- | An identifier is a sequence of letters which is not a keyword. +identifier :: Parser Text +identifier = do + notFollowedBy anyKeyword + T.pack <$> many1 letter + where anyKeyword = choice $ map (try . keyword) keywords variable :: Parser Expression -variable = Variable <$> variableName +variable = Variable <$> identifier + +spaces :: Parser () +spaces = skipMany1 space application :: Parser Expression application = foldl1 Application <$> sepEndBy1 applicationTerm spaces where applicationTerm :: Parser Expression - applicationTerm = variable <|> abstraction <|> let_ <|> grouping + applicationTerm = abstraction <|> grouping <|> let_ <|> variable where grouping :: Parser Expression grouping = between (char '(') (char ')') expression abstraction :: Parser Expression abstraction = do - char '\\' - optional spaces - names <- sepEndBy1 variableName spaces - char '.' - optional spaces - body <- expression - pure $ foldr Abstraction body names + char '\\' <|> char 'λ' ; optional spaces + names <- sepEndBy1 identifier spaces + char '.' + body <- expression + pure $ foldr Abstraction body names let_ :: Parser Expression let_ = do - keyword "let" - name <- between spaces (optional spaces) variableName - char '=' - value <- expression - keyword "in" - body <- expression - pure $ Application (Abstraction name body) value + try (keyword "let") ; spaces + defs <- sepBy1 definition (char ';' *> optional spaces) + keyword "in" + body <- expression + pure $ foldr (uncurry letExpr) body defs + where definition :: Parser (Text, Expression) + definition = do + name <- identifier ; optional spaces + char '=' + value <- expression + pure (name, value) + letExpr :: Text -> Expression -> Expression -> Expression + letExpr name value body = Application (Abstraction name body) value expression :: Parser Expression expression = optional spaces *> (abstraction <|> let_ <|> application <|> variable) <* optional spaces diff --git a/test/Spec.hs b/test/Spec.hs index bd54d52..0ec4a7f 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -60,6 +60,7 @@ main = defaultMain $ , testCase "unary application" $ parseExpression "(x)" @?= Right (Variable "x") , testCase "application shorthand" $ parseExpression "a b c d" @?= Right (Application (Application (Application (Variable "a") (Variable "b")) (Variable "c")) (Variable "d")) , testCase "let" $ parseExpression "let x = \\y.y in x" @?= Right (Application (Abstraction "x" (Variable "x")) (Abstraction "y" (Variable "y"))) + , testCase "multi-let" $ parseExpression "let x = y; y = z in x y" @?= Right (Application (Abstraction "x" (Application (Abstraction "y" (Application (Variable "x") (Variable "y"))) (Variable "z"))) (Variable "y")) , testCase "ttttt" $ parseExpression "(\\T f x.(T (T (T (T T)))) f x) (\\f x.f (f x)) (\\x.x) y" @?= Right ttttt , testGroup "Redundant whitespace"