Compare commits
No commits in common. "7406739fcf4397da1ad17ee88ca352c55304615e" and "9d209fee178aa6b9468fd80edb2dd73c9b48f2e4" have entirely different histories.
7406739fcf
...
9d209fee17
7 changed files with 8 additions and 279 deletions
|
|
@ -5,11 +5,9 @@ A (very WIP) lambda expression evaluator and debugger.
|
||||||
I'd like to build the following:
|
I'd like to build the following:
|
||||||
|
|
||||||
- [X] parsing with parsec
|
- [X] parsing with parsec
|
||||||
|
- need to harden tests a bit more but existing tests pass
|
||||||
- [X] alpha/beta reduction to beta normal
|
- [X] alpha/beta reduction to beta normal
|
||||||
- [ ] substitutions for known abstractions (numbers can be written and are displayed as numbers rather than lambda terms)
|
- [ ] 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
|
- [ ] persisted variables
|
||||||
- [ ] display all steps in alpha/beta reductions until beta normal form is reached
|
- [ ] display all steps in alpha/beta reductions until beta normal form is reached
|
||||||
- [ ] online web-based lambda playground
|
- [ ] online web-based lambda playground
|
||||||
|
|
|
||||||
12
lamb.cabal
12
lamb.cabal
|
|
@ -14,9 +14,8 @@ executable lamb
|
||||||
main-is: Main.hs
|
main-is: Main.hs
|
||||||
other-modules: Parser,
|
other-modules: Parser,
|
||||||
Evaluation,
|
Evaluation,
|
||||||
Bruijn,
|
Bruijn
|
||||||
Niceties
|
build-depends: base, containers, parsec
|
||||||
build-depends: base, bimap, containers, parsec
|
|
||||||
hs-source-dirs: src
|
hs-source-dirs: src
|
||||||
default-language: Haskell2010
|
default-language: Haskell2010
|
||||||
|
|
||||||
|
|
@ -28,10 +27,7 @@ test-suite lamb-tests
|
||||||
ParserSpec,
|
ParserSpec,
|
||||||
Evaluation,
|
Evaluation,
|
||||||
EvaluationSpec,
|
EvaluationSpec,
|
||||||
Bruijn,
|
BruijnSpec
|
||||||
BruijnSpec,
|
build-depends: base, containers, hspec, parsec
|
||||||
Niceties,
|
|
||||||
NicetiesSpec
|
|
||||||
build-depends: base, bimap, containers, hspec, parsec
|
|
||||||
build-tool-depends: hspec-discover:hspec-discover
|
build-tool-depends: hspec-discover:hspec-discover
|
||||||
default-language: Haskell2010
|
default-language: Haskell2010
|
||||||
|
|
|
||||||
|
|
@ -1,7 +1,6 @@
|
||||||
module Main where
|
module Main where
|
||||||
|
|
||||||
import Evaluation (run)
|
import Evaluation (run)
|
||||||
import Niceties (replaceKnowns)
|
|
||||||
import Parser (parse)
|
import Parser (parse)
|
||||||
import System.Environment (getArgs)
|
import System.Environment (getArgs)
|
||||||
import System.IO (IOMode (ReadMode), hGetContents, openFile)
|
import System.IO (IOMode (ReadMode), hGetContents, openFile)
|
||||||
|
|
@ -16,5 +15,5 @@ main = do
|
||||||
case command of
|
case command of
|
||||||
"run" -> do
|
"run" -> do
|
||||||
content <- openFile path ReadMode >>= hGetContents
|
content <- openFile path ReadMode >>= hGetContents
|
||||||
either putStrLn putStrLn $ show . replaceKnowns . run <$> parse content
|
either putStrLn putStrLn $ show . run <$> parse content
|
||||||
_ -> putStrLn $ "Unrecognized command: " ++ command
|
_ -> putStrLn $ "Unrecognized command: " ++ command
|
||||||
|
|
|
||||||
245
src/Niceties.hs
245
src/Niceties.hs
|
|
@ -1,245 +0,0 @@
|
||||||
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")
|
|
||||||
)
|
|
||||||
)
|
|
||||||
]
|
|
||||||
|
|
@ -6,7 +6,7 @@ import Text.Parsec
|
||||||
import Text.Parsec.String (Parser)
|
import Text.Parsec.String (Parser)
|
||||||
|
|
||||||
data Expr = Variable String | Abstraction String Expr | Application Expr Expr
|
data Expr = Variable String | Abstraction String Expr | Application Expr Expr
|
||||||
deriving (Eq, Ord)
|
deriving (Eq)
|
||||||
|
|
||||||
instance Show Expr where
|
instance Show Expr where
|
||||||
show (Variable name) = name
|
show (Variable name) = name
|
||||||
|
|
|
||||||
2
test.lm
2
test.lm
|
|
@ -1 +1 @@
|
||||||
(λn. n (λx. λa. λb. b) (λa. λb. a)) (λf. λx. x)
|
(λx.λy.λz. x z (y z)) (λa.λb. a) (λa.λb. a)
|
||||||
|
|
|
||||||
|
|
@ -1,19 +0,0 @@
|
||||||
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")
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue