module AstTest where

import AST
import Test.Hspec

evalSpec :: Spec
evalSpec =
  describe "CoreTT.AST" $ do
    it "evaluates Star as VStar" $ do
      evalInf empty [] Star `shouldBe` Just VStar

    it "evaluates a lambda abstraction Lam b as VLam b" $ do
      evalChk empty [] (Lam (Inf (Local 0))) `shouldBe` Just (VLam (Inf (Local 0)))

    it "evaluates a local variable as its value in the context" $ do
      evalInf empty [VStar] (Local 0) `shouldBe` Just VStar

    it "raises an error when variable out of range" $ do
      evalInf empty [] (Local 3) `shouldBe` Nothing

    it "raises an error when we apply something not to a function" $ do
      evalInf empty [] (App (Inf Star) Star) `shouldBe` Nothing