diff options
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs | 36 | ||||
| -rw-r--r-- | lambda-calcul/haskell/test/Minilang/IOSpec.hs | 2 | ||||
| -rw-r--r-- | lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs | 16 |
3 files changed, 31 insertions, 23 deletions
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs index 0829186..a15d3f9 100644 --- a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs +++ b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs @@ -1,6 +1,7 @@ module Minilang.Lambda.Eval where -import Data.Text (Text) +import Data.Text (Text, unpack) +import Debug.Trace (trace) data Term = Var Text @@ -8,29 +9,36 @@ data Term | App Term Term deriving (Show, Read, Eq) -type Env = [(Text, Term)] +type Env = [(Text, Value)] + +data Value + = V Text + | Abs Text Term Env + | Ap Value Value + deriving (Show, Read, Eq) -- call-by-value evaluator -eval :: Term -> Env -> Term +eval :: Term -> Env -> Value eval (Var x) env = case lookup x env of Just v -> v -- we do not need to eval v again - Nothing -> Var x -eval (Lam x body) _env = Lam x body + Nothing -> V x -- x is not bound in env +eval (Lam x body) env = Abs x body env eval (App f a) env = -- we need to force evaluation of the argument -- because haskell's default semantics is non-strict -- so if a' is never used, it will not be evaluated! let a' = eval a env in seq a' $ case eval f env of - Lam x body -> eval body ((x, a') : env) - f' -> App f' a' + Abs x body env' -> eval body ((x, a') : env') + f' -> Ap f' a' -evalNeed :: Term -> Env -> Term +evalNeed :: Term -> Env -> Value evalNeed (Var x) env = case lookup x env of - Just v -> evalNeed v env -- we need to eval v because it might be a redex - Nothing -> Var x -evalNeed (Lam x body) _env = Lam x body + Just v -> v + Nothing -> V x +evalNeed (Lam x body) env = Abs x body env evalNeed (App f a) env = - case evalNeed f env of - Lam x body -> evalNeed body ((x, a) : env) - f' -> App f' a + let a' = eval a env + in case evalNeed f env of + Abs x body env' -> evalNeed body ((x, a') : env') + f' -> Ap f' a' diff --git a/lambda-calcul/haskell/test/Minilang/IOSpec.hs b/lambda-calcul/haskell/test/Minilang/IOSpec.hs index 14d279d..80cda6c 100644 --- a/lambda-calcul/haskell/test/Minilang/IOSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/IOSpec.hs @@ -27,7 +27,7 @@ spec = parallel $ out <- readFile outputFileName - out `shouldBe` "Var \"z\"\n" + out `shouldBe` "V \"z\"\n" withTempFile :: (String -> IO ()) -> IO () withTempFile = diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs index 11cf394..718b46d 100644 --- a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs @@ -2,7 +2,7 @@ module Minilang.Lambda.EvalSpec (spec) where import Control.Concurrent (threadDelay) import Control.Concurrent.Async (race_) -import Minilang.Lambda.Eval (Term (..), eval, evalNeed) +import Minilang.Lambda.Eval (Term (..), Value (..), eval, evalNeed) import Test.Hspec (Spec, describe, it, shouldBe) spec :: Spec @@ -21,31 +21,31 @@ spec = do describe "call-by-value eval" $ do it "evaluates 'x' as itself" $ do let term = Var "x" - eval term [] `shouldBe` Var "x" + eval term [] `shouldBe` V "x" it "evaluates '((λ x. x) y)' as 'y'" $ do let term = App (Lam "x" (Var "x")) (Var "y") - eval term [] `shouldBe` Var "y" + eval term [] `shouldBe` V "y" 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 "z")) (Var "t")) (Var "y") - eval term [] `shouldBe` App (Var "t") (Var "y") + eval term [] `shouldBe` Ap (V "t") (V "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" + eval term [] `shouldBe` V "z" it "diverges on evaluating argument bound to ω" $ shouldDiverge $ eval term [] describe "call-by-need eval" $ do it "evaluates 'x' as itself" $ do - evalNeed (Var "x") [] `shouldBe` Var "x" + evalNeed (Var "x") [] `shouldBe` V "x" it "evaluates '(λ x y . y) ⊥ z' as 'z'" $ do - evalNeed term [] `shouldBe` Var "z" + evalNeed term [] `shouldBe` V "z" it "diverges on evaluating ω" $ shouldDiverge $ evalNeed omega [] -shouldDiverge :: Term -> IO () +shouldDiverge :: Value -> IO () shouldDiverge t = race_ (t `seq` fail "Did not diverge") |