summaryrefslogtreecommitdiff
path: root/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
diff options
context:
space:
mode:
authorArnaud Bailly <arnaud@pankzsoft.com>2025-10-27 16:26:55 +0100
committerArnaud Bailly <arnaud@pankzsoft.com>2025-10-27 16:26:55 +0100
commit46d94d86705a7fd0a7c5d0d7c6a74f11669641ca (patch)
treea5739cde5488fccc77249f6d803efa6b460a1642 /lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
parent5cba53dd054222ce3319a1efe6803952c9675889 (diff)
downloadlambda-nantes-46d94d86705a7fd0a7c5d0d7c6a74f11669641ca.tar.gz
Add more tests and references
Diffstat (limited to 'lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs')
-rw-r--r--lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs24
1 files changed, 18 insertions, 6 deletions
diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
index df933a4..11cf394 100644
--- a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
@@ -7,9 +7,16 @@ import Test.Hspec (Spec, describe, it, shouldBe)
spec :: Spec
spec = do
- let fix = Lam "x" (App (Var "x") (Var "x"))
+ let fix =
+ Lam
+ "f"
+ ( App
+ (Lam "x" (App (Var "f") (App (Var "x") (Var "x"))))
+ (Lam "x" (App (Var "f") (App (Var "x") (Var "x"))))
+ )
let omega = App fix fix
let term = App (App (Lam "x" (Lam "y" (Var "y"))) omega) (Var "z")
+ let fst' = Lam "x" (Lam "y" (Var "x"))
describe "call-by-value eval" $ do
it "evaluates 'x' as itself" $ do
@@ -18,12 +25,16 @@ spec = do
it "evaluates '((λ x. x) y)' as 'y'" $ do
let term = App (Lam "x" (Var "x")) (Var "y")
eval term [] `shouldBe` Var "y"
- it "evaluates '((λ x y. y) y z t)' as '(z t)'" $ do
+ it "evaluates '((λ x y. y) z t y)' as '(t y)'" $ do
let snd' = Lam "x" (Lam "y" (Var "y"))
- let term = App (App (App snd' (Var "y")) (Var "z")) (Var "t")
- eval term [] `shouldBe` App (Var "z") (Var "t")
+ let term = App (App (App snd' (Var "z")) (Var "t")) (Var "y")
+ eval term [] `shouldBe` App (Var "t") (Var "y")
+ it "evaluates '((λ x y. x) z t)' as 'z'" $ do
+ let term = App (App fst' (Var "z")) (Var "t")
+ eval term [] `shouldBe` Var "z"
it "diverges on evaluating argument bound to ω" $
- shouldDiverge $ eval term []
+ shouldDiverge $
+ eval term []
describe "call-by-need eval" $ do
it "evaluates 'x' as itself" $ do
@@ -31,7 +42,8 @@ spec = do
it "evaluates '(λ x y . y) ⊥ z' as 'z'" $ do
evalNeed term [] `shouldBe` Var "z"
it "diverges on evaluating ω" $
- shouldDiverge $ evalNeed omega []
+ shouldDiverge $
+ evalNeed omega []
shouldDiverge :: Term -> IO ()
shouldDiverge t =