module Main where
import AstTest
import Test.Hspec
main :: IO ()
main = hspec $ do
  evalSpec

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

module AST where
import Data.List.Safe ((!!))
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Text (Text)
import Prelude hiding ((!!))
type Name = Text
type Index = Int
data TermInf
  = Global Name
  | Local Index
  | Star
  | Ann TermChk TermChk
  | App TermChk TermInf
  | Pi TermChk TermChk
  deriving (Eq, Show)
data TermChk
  = Inf TermInf
  | Lam TermChk
  deriving (Eq, Show)
data Value
  = VStar
  | VLam TermChk
  | VPi TermChk TermChk
  deriving (Eq, Show)
type Env = Map Name Value
empty :: Env
empty = Map.empty
type Ctx = [Value]
type Eval t = Env -> Ctx -> t -> Maybe Value
evalInf :: Eval TermInf
evalInf env ctx (Global n) = Map.lookup n env
evalInf env ctx (Local idx) = ctx !! idx
evalInf env ctx Star = Just VStar
evalInf env ctx (Ann t _) = evalChk env ctx t
evalInf env ctx (App f a) = do
  a <- evalInf env ctx a
  case evalChk env ctx f of
    Just (VLam b) -> evalChk env (a : ctx) b
    Just (VPi _ b) -> evalChk env (a : ctx) b
    _ -> Nothing
evalInf env ctx (Pi dom t) = Just (VPi dom t)
evalChk :: Eval TermChk
evalChk env ctx (Inf term) = evalInf env ctx term
evalChk env ctx (Lam body) = Just (VLam body)

{ mkDerivation, base, lib, text }:

{ mkDerivation, base, containers, hspec, lib, listsafe, text }:

  libraryHaskellDepends = [ base text ];

  libraryHaskellDepends = [ base containers listsafe text ];

  testHaskellDepends = [ base ];

  testHaskellDepends = [ base hspec ];

module Main where
main :: IO ()
main = do
  putStrLn "Hello, Haskell!"

    exposed-modules:  MyLib

    exposed-modules:  AST

    other-modules: AbstractSyntax,
                   BidirectionalAbstractSyntax

    -- other-modules: 

                      text

                      text,
                      listsafe,
                      containers

    main-is:          MyLibTest.hs
    build-depends:    base ^>=4.14.3.0

    main-is:          Spec.hs
    other-modules:    AstTest
    build-depends:    base ^>=4.14.3.0,
                      hspec,
                      CoreTT