{-# LANGUAGE TypeApplications #-} module Minilang.Lambda.DeBruijnSpec where 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) spec :: Spec spec = do it "convert term to deBruijn representation" $ do let term = Eval.Lam "x" (Eval.Lam "y" (Eval.Var "x")) deBruijn = toDeBruijn term deBruijn `shouldBe` Lam "x" (Lam "y" (Var "x" 1)) it "evaluates deBruijn term" $ 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"