{-# LANGUAGE TypeApplications #-}
module Minilang.Lambda.DeBruijnSpec where

import Minilang.Lambda.DeBruijn (DeBruijn (..), Env, builtinDeBruijnEnv, eval, toDeBruijn, eval')
import qualified Minilang.Lambda.Eval as Eval
import Test.Hspec (Spec, describe, 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' env term `shouldBe` FV "t"

  describe "built-in arithmetic" $ do
    let benv = builtinDeBruijnEnv :: Env Text

    it "(+ 3 4) reduces to FNum 7" $
      eval' benv (App (App (FBuiltin "+") (FNum 3)) (FNum 4))
        `shouldBe` FNum 7

    it "(- 10 3) reduces to FNum 7" $
      eval' benv (App (App (FBuiltin "-") (FNum 10)) (FNum 3))
        `shouldBe` FNum 7

    it "(* 2 5) reduces to FNum 10" $
      eval' benv (App (App (FBuiltin "*") (FNum 2)) (FNum 5))
        `shouldBe` FNum 10

    it "(div 10 3) reduces to FNum 3" $
      eval' benv (App (App (FBuiltin "div") (FNum 10)) (FNum 3))
        `shouldBe` FNum 3

    it "(mod 10 3) reduces to FNum 1" $
      eval' benv (App (App (FBuiltin "mod") (FNum 10)) (FNum 3))
        `shouldBe` FNum 1

    it "(= 3 3) reduces to Church True" $
      eval' benv (App (App (FBuiltin "=") (FNum 3)) (FNum 3))
        `shouldBe` Lam "f" (Lam "t" (Var "t" 0))

    it "(= 3 4) reduces to Church False" $
      eval' benv (App (App (FBuiltin "=") (FNum 3)) (FNum 4))
        `shouldBe` Lam "f" (Lam "t" (Var "f" 1))

    it "(< 2 5) reduces to Church True" $
      eval' benv (App (App (FBuiltin "<") (FNum 2)) (FNum 5))
        `shouldBe` Lam "f" (Lam "t" (Var "t" 0))

    it "(< 5 2) reduces to Church False" $
      eval' benv (App (App (FBuiltin "<") (FNum 5)) (FNum 2))
        `shouldBe` Lam "f" (Lam "t" (Var "f" 1))

    it "(neg 7) reduces to FNum -7" $
      eval' benv (App (FBuiltin "neg") (FNum 7))
        `shouldBe` FNum (-7)

    it "(+ 1) partial: stays as a spine without reducing" $
      eval' benv (App (FBuiltin "+") (FNum 1))
        `shouldBe` App (FBuiltin "+") (FNum 1)

    it "(div 1 0) stays stuck" $
      eval' benv (App (App (FBuiltin "div") (FNum 1)) (FNum 0))
        `shouldBe` App (App (FBuiltin "div") (FNum 1)) (FNum 0)

    it "(+ x 1) with free x stays stuck" $
      eval' benv (App (App (FBuiltin "+") (FV "x")) (FNum 1))
        `shouldBe` App (App (FBuiltin "+") (FV "x")) (FNum 1)

    it "lookup of '+' in builtin env yields FBuiltin" $
      eval' benv (FV "+") `shouldBe` FBuiltin "+"