From 46d94d86705a7fd0a7c5d0d7c6a74f11669641ca Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Mon, 27 Oct 2025 16:26:55 +0100 Subject: Add more tests and references --- .../haskell/test/Minilang/Lambda/EvalSpec.hs | 24 ++++++++++++++++------ 1 file changed, 18 insertions(+), 6 deletions(-) (limited to 'lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs') 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 = -- cgit v1.2.3