module Main where

import qualified Data.Map.Strict as Map
import System.Exit (die)

import AST
import Parser
import TypeCheck


main :: IO ()
main = do
  source <- getContents

  uprog <- case parseProgram "<stdin>" source of
    Left err -> die (show err)
    Right term -> return term

  let env0 = Map.fromList
        [("Level", Nothing :| TLevelUniv)
        ,("One", Nothing :| TSet TIZero)
        ,("Unit", Nothing :| TOne)
        ,("lzero", Nothing :| TLevel)
        ,("lsuc", Nothing :| TPi "x" TLevel TLevel)]

  env <- case checkProgram env0 uprog of
    Left err -> die err
    Right env -> return env

  print env