From 3046beaef22620fdf679396e1c5184427c6fcc3d Mon Sep 17 00:00:00 2001 From: jackjohn7 <70782491+jackjohn7@users.noreply.github.com> Date: Sun, 17 May 2026 00:21:54 -0500 Subject: [PATCH 1/3] replacing known values in output now (pretty sick) --- lamb.cabal | 12 ++- src/Main.hs | 3 +- src/Niceties.hs | 245 +++++++++++++++++++++++++++++++++++++++++++ src/Parser.hs | 2 +- test.lm | 2 +- test/NicetiesSpec.hs | 19 ++++ 6 files changed, 276 insertions(+), 7 deletions(-) create mode 100644 src/Niceties.hs create mode 100644 test/NicetiesSpec.hs diff --git a/lamb.cabal b/lamb.cabal index 88ff50e..0a65674 100644 --- a/lamb.cabal +++ b/lamb.cabal @@ -14,8 +14,9 @@ executable lamb main-is: Main.hs other-modules: Parser, Evaluation, - Bruijn - build-depends: base, containers, parsec + Bruijn, + Niceties + build-depends: base, bimap, containers, parsec hs-source-dirs: src default-language: Haskell2010 @@ -27,7 +28,10 @@ test-suite lamb-tests ParserSpec, Evaluation, EvaluationSpec, - BruijnSpec - build-depends: base, containers, hspec, parsec + Bruijn, + BruijnSpec, + Niceties, + NicetiesSpec + build-depends: base, bimap, containers, hspec, parsec build-tool-depends: hspec-discover:hspec-discover default-language: Haskell2010 diff --git a/src/Main.hs b/src/Main.hs index 6490c7c..bd04634 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -1,6 +1,7 @@ module Main where import Evaluation (run) +import Niceties (replaceKnowns) import Parser (parse) import System.Environment (getArgs) import System.IO (IOMode (ReadMode), hGetContents, openFile) @@ -15,5 +16,5 @@ main = do case command of "run" -> do content <- openFile path ReadMode >>= hGetContents - either putStrLn putStrLn $ show . run <$> parse content + either putStrLn putStrLn $ show . replaceKnowns . run <$> parse content _ -> putStrLn $ "Unrecognized command: " ++ command diff --git a/src/Niceties.hs b/src/Niceties.hs new file mode 100644 index 0000000..b2d9233 --- /dev/null +++ b/src/Niceties.hs @@ -0,0 +1,245 @@ +module Niceties where + +import Bruijn (toDeBruijn) +import Data.Bimap (Bimap, fromList, lookupR) +import Parser (Expr (Abstraction, Application, Variable)) + +findKnown :: Expr -> Maybe String +findKnown e = lookupR (toDeBruijn e) knownValues + +-- | Replace known values in expression with proper names +replaceKnowns :: Expr -> Expr +replaceKnowns a@(Abstraction name body) = case findKnown a of + Just name' -> Variable name' + Nothing -> Abstraction name $ replaceKnowns body +replaceKnowns (Application f arg) = Application (replaceKnowns f) (replaceKnowns arg) +replaceKnowns v = v + +knownValues :: Bimap String Expr +knownValues = + Data.Bimap.fromList + [ ( "I", + toDeBruijn $ Abstraction "x" (Variable "x") + ), + ( "true", + -- same as K + toDeBruijn $ + Abstraction "x" (Abstraction "y" (Variable "x")) + ), + ( "false", + -- same as K*, `0`, `nil` + toDeBruijn $ + Abstraction "x" (Abstraction "y" (Variable "y")) + ), + ( "S", + toDeBruijn $ + Abstraction "x" $ + Abstraction "y" $ + Abstraction "z" $ + Application + (Application (Variable "x") (Variable "z")) + (Application (Variable "y") (Variable "z")) + ), + ( "B", + toDeBruijn $ + Abstraction "x" $ + Abstraction "y" $ + Abstraction "z" $ + Application + (Variable "x") + (Application (Variable "y") (Variable "z")) + ), + ( "C", + toDeBruijn $ + Abstraction "x" $ + Abstraction "y" $ + Abstraction "z" $ + Application + (Application (Variable "x") (Variable "z")) + (Variable "y") + ), + ( "W", + toDeBruijn $ + Abstraction "x" $ + Abstraction "y" $ + Application + (Application (Variable "x") (Variable "y")) + (Variable "y") + ), + ( "ω", + toDeBruijn $ + Abstraction "x" $ + Application (Variable "x") (Variable "x") + ), + -- Fixed points + ( "Y", + toDeBruijn $ + Abstraction "f" $ + Application + ( Abstraction "x" $ + Application + (Variable "f") + (Application (Variable "x") (Variable "x")) + ) + ( Abstraction "x" $ + Application + (Variable "f") + (Application (Variable "x") (Variable "x")) + ) + ), + ( "Z", + toDeBruijn $ + Abstraction "f" $ + Application + ( Abstraction "x" $ + Application (Variable "f") $ + Abstraction "v" $ + Application + (Application (Variable "x") (Variable "x")) + (Variable "v") + ) + ( Abstraction "x" $ + Application (Variable "f") $ + Abstraction "v" $ + Application + (Application (Variable "x") (Variable "x")) + (Variable "v") + ) + ), + -- Church numerals + -- Note: if you use the Church numeral recognition algorithm, + -- you may not need these in the Bimap at all. + ( "succ", + toDeBruijn $ + Abstraction "n" $ + Abstraction "f" $ + Abstraction "x" $ + Application + (Variable "f") + ( Application + (Application (Variable "n") (Variable "f")) + (Variable "x") + ) + ), + ( "plus", + toDeBruijn $ + Abstraction "m" $ + Abstraction "n" $ + Abstraction "f" $ + Abstraction "x" $ + Application + (Application (Variable "m") (Variable "f")) + ( Application + (Application (Variable "n") (Variable "f")) + (Variable "x") + ) + ), + ( "mult", + toDeBruijn $ + Abstraction "m" $ + Abstraction "n" $ + Abstraction "f" $ + Application + (Variable "m") + (Application (Variable "n") (Variable "f")) + ), + ( "exp", + toDeBruijn $ + Abstraction "m" $ + Abstraction "n" $ + Application (Variable "n") (Variable "m") + ), + ( "pred", + toDeBruijn $ + Abstraction "n" $ + Abstraction "f" $ + Abstraction "x" $ + Application + ( Application + ( Application (Variable "n") $ + Abstraction "g" $ + Abstraction "h" $ + Application + (Variable "h") + (Application (Variable "g") (Variable "f")) + ) + (Abstraction "u" (Variable "x")) + ) + (Abstraction "u" (Variable "u")) + ), + ( "isZero", + toDeBruijn $ + Abstraction "n" $ + Application + ( Application (Variable "n") $ + Abstraction "x" $ + Abstraction "a" $ + Abstraction "b" (Variable "b") + ) + (Abstraction "a" $ Abstraction "b" (Variable "a")) + ), + -- Church booleans + ( "and", + toDeBruijn $ + Abstraction "p" $ + Abstraction "q" $ + Application + (Application (Variable "p") (Variable "q")) + (Variable "p") + ), + ( "or", + toDeBruijn $ + Abstraction "p" $ + Abstraction "q" $ + Application + (Application (Variable "p") (Variable "p")) + (Variable "q") + ), + ( "not", + toDeBruijn $ + Abstraction "p" $ + Abstraction "a" $ + Abstraction "b" $ + Application + (Application (Variable "p") (Variable "b")) + (Variable "a") + ), + -- Pairs + ( "pair", + toDeBruijn $ + Abstraction "x" $ + Abstraction "y" $ + Abstraction "f" $ + Application + (Application (Variable "f") (Variable "x")) + (Variable "y") + ), + ( "fst", + toDeBruijn $ + Abstraction "p" $ + Application (Variable "p") $ + Abstraction "x" $ + Abstraction "y" (Variable "x") + ), + ( "snd", + toDeBruijn $ + Abstraction "p" $ + Application (Variable "p") $ + Abstraction "x" $ + Abstraction "y" (Variable "y") + ), + -- Lists + ( "cons", + toDeBruijn $ + Abstraction "h" $ + Abstraction "t" $ + Abstraction "f" $ + Abstraction "x" $ + Application + (Application (Variable "f") (Variable "h")) + ( Application + (Application (Variable "t") (Variable "f")) + (Variable "x") + ) + ) + ] diff --git a/src/Parser.hs b/src/Parser.hs index de8028c..3cd4d7c 100644 --- a/src/Parser.hs +++ b/src/Parser.hs @@ -6,7 +6,7 @@ import Text.Parsec import Text.Parsec.String (Parser) data Expr = Variable String | Abstraction String Expr | Application Expr Expr - deriving (Eq) + deriving (Eq, Ord) instance Show Expr where show (Variable name) = name diff --git a/test.lm b/test.lm index 3be6e04..1496ac5 100644 --- a/test.lm +++ b/test.lm @@ -1 +1 @@ -(λx.λy.λz. x z (y z)) (λa.λb. a) (λa.λb. a) +(λn. n (λx. λa. λb. b) (λa. λb. a)) (λf. λx. x) diff --git a/test/NicetiesSpec.hs b/test/NicetiesSpec.hs new file mode 100644 index 0000000..59ad76f --- /dev/null +++ b/test/NicetiesSpec.hs @@ -0,0 +1,19 @@ +module NicetiesSpec (spec) where + +import Bruijn (toDeBruijn) +import Niceties (findKnown, replaceKnowns) +import Parser (Expr (Abstraction, Application, Variable)) +import Test.Hspec + +spec :: Spec +spec = do + describe "can find knowns" $ do + it "can find identity" $ + findKnown identity `shouldBe` Just "I" + describe "replaceKnowns" $ do + it "can replace identity" $ + replaceKnowns identity `shouldBe` Variable "I" + it "can replace identity of identity" $ + replaceKnowns (Application identity identity) `shouldBe` Application (Variable "I") (Variable "I") + where + identity = toDeBruijn $ Abstraction "x" (Variable "x") From 54d147b95493098cc3bc02976cf35275f436ca46 Mon Sep 17 00:00:00 2001 From: jackjohn7 <70782491+jackjohn7@users.noreply.github.com> Date: Sun, 17 May 2026 00:26:30 -0500 Subject: [PATCH 2/3] update readme --- README.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index bdc771d..afc9ae5 100644 --- a/README.md +++ b/README.md @@ -5,9 +5,10 @@ A (very WIP) lambda expression evaluator and debugger. I'd like to build the following: - [X] parsing with parsec - - need to harden tests a bit more but existing tests pass - [X] alpha/beta reduction to beta normal - [ ] substitutions for known abstractions (numbers can be written and are displayed as numbers rather than lambda terms) + - [ ] replace known terms in input + - [X] replace known terms in output - [ ] persisted variables - [ ] display all steps in alpha/beta reductions until beta normal form is reached - [ ] online web-based lambda playground From 7406739fcf4397da1ad17ee88ca352c55304615e Mon Sep 17 00:00:00 2001 From: jackjohn7 <70782491+jackjohn7@users.noreply.github.com> Date: Sun, 17 May 2026 00:30:29 -0500 Subject: [PATCH 3/3] update README --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index afc9ae5..b5d4a03 100644 --- a/README.md +++ b/README.md @@ -9,6 +9,7 @@ I'd like to build the following: - [ ] substitutions for known abstractions (numbers can be written and are displayed as numbers rather than lambda terms) - [ ] replace known terms in input - [X] replace known terms in output + - [ ] support detection and replacement for generic church numerals (not just 1 and 0 (false)) - [ ] persisted variables - [ ] display all steps in alpha/beta reductions until beta normal form is reached - [ ] online web-based lambda playground