diff options
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs | 19 | ||||
| -rw-r--r-- | lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs | 7 |
2 files changed, 24 insertions, 2 deletions
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs b/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs index 290839e..8b24f8b 100644 --- a/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs +++ b/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs @@ -1,8 +1,9 @@ {-# LANGUAGE LambdaCase #-} + module Minilang.Lambda.DeBruijn where import Data.List (elemIndex) -import Data.Text (Text, unpack, pack) +import Data.Text (Text) import Minilang.Lambda.Eval (Term) import qualified Minilang.Lambda.Eval as Eval @@ -13,6 +14,12 @@ data DeBruijn ann | App (DeBruijn ann) (DeBruijn ann) deriving (Show, Read, Eq) +type Env ann = [(Text, DeBruijn ann)] + +newEnv :: Env ann +newEnv = [] + + fromDeBruijn :: DeBruijn Text -> Term fromDeBruijn = \case FV x -> Eval.Var x @@ -40,6 +47,16 @@ eval (App f a) = f' -> App f' a eval term = term +eval' :: Env ann -> DeBruijn ann -> DeBruijn ann +eval' env (FV v) = case lookup v env of + Just term -> term + Nothing -> FV v +eval' env (App f a) = + case eval' env f of + Lam _ body -> eval' env (substitute 0 a body) + f' -> App f' a +eval' _ term = term + substitute :: Int -> DeBruijn ann -> DeBruijn ann -> DeBruijn ann substitute n arg term = case term of FV x -> FV x diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs index cff047d..85c9d6b 100644 --- a/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs @@ -1,7 +1,7 @@ {-# LANGUAGE TypeApplications #-} module Minilang.Lambda.DeBruijnSpec where -import Minilang.Lambda.DeBruijn (DeBruijn (..), eval, toDeBruijn) +import Minilang.Lambda.DeBruijn (DeBruijn (..), eval, toDeBruijn, eval') import qualified Minilang.Lambda.Eval as Eval import Test.Hspec (Spec, it, shouldBe) import Data.Text (Text) @@ -18,3 +18,8 @@ spec = do let term = App (App (Lam "x" (Lam "y" (Var "x" 1))) (FV "z")) (FV "t") eval @Text term `shouldBe` FV "z" + + it "evaluates deBruijn term in env" $ do + let term = App (FV "z") (FV "t") + env = [("z", toDeBruijn $ Eval.Lam "x" (Eval.Var "x"))] + eval' @Text env term `shouldBe` FV "t" |
