summaryrefslogtreecommitdiff
path: root/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs
blob: 85c9d6b2a61f656556f5b74f7e7288fe25141a07 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
{-# 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"