content: {- pi-forall language -}
  
  -- | The command line interface to the pi type checker.
  -- Also provides functions for type checking individual terms
  -- and files.
  module Main (goFilename, go, main) where
  
  import Control.Monad.Except (runExceptT)
  import Environment (emptyEnv, runTcMonad)
  import Modules (getModules)
  import Parser (parseExpr)
  import PrettyPrint (Disp (..), render)
  import System.Environment (getArgs)
  import System.Exit (exitFailure, exitSuccess)
  import System.FilePath (splitFileName)
  import Text.ParserCombinators.Parsec.Error (ParseError, errorPos)
  import TypeCheck (inferType, tcModules)
  
  exitWith :: Either a b -> (a -> IO ()) -> IO b
  exitWith res f =
    case res of
      Left x -> f x >> exitFailure
      Right y -> return y
  
  -- | Type check the given string in the empty environment
  go :: String -> IO ()
  go str = do
    case parseExpr str of
      Left parseError -> putParseError parseError
      Right term -> do
        putStrLn "parsed as"
        putStrLn $ render $ disp term
        res <- runTcMonad emptyEnv (inferType term)
        case res of
          Left typeError -> putTypeError typeError
          Right ty -> do
            putStrLn "typed with type"
            putStrLn $ render $ disp ty
  
  -- | Display a parse error to the user
  putParseError :: ParseError -> IO ()
  putParseError parseError = do
    putStrLn $ render $ disp $ errorPos parseError
    print parseError
  
  -- | Display a type error to the user
  putTypeError :: Disp d => d -> IO ()
  putTypeError typeError = do
    putStrLn "Type Error:"
    putStrLn $ render $ disp typeError
  
  -- | Type check the given file
  goFilename :: String -> IO ()
  goFilename pathToMainFile = do
    let prefixes = [currentDir, mainFilePrefix]
        (mainFilePrefix, name) = splitFileName pathToMainFile
        currentDir = ""
    putStrLn $ "processing " ++ name ++ "..."
    v <- runExceptT (getModules prefixes name)
    val <- v `exitWith` putParseError
    putStrLn "type checking..."
    d <- runTcMonad emptyEnv (tcModules val)
    defs <- d `exitWith` putTypeError
    putStrLn $ render $ disp (last defs)
  
  -- | 'pi <filename>' invokes the type checker on the given
  -- file and either prints the types of all definitions in the module
  -- or prints an error message.
  main :: IO ()
  main = do
    [pathToMainFile] <- getArgs
    goFilename pathToMainFile
    exitSuccess
  