content: module Main where
  
  import Data.Either
  import System.IO ( stdin, hGetContents )
  import System.Environment ( getArgs )
  import Options 
  import Terms
  
  import RawSyntax
  import AbsSynToTerm
  import TypeChecker
  import Basics
  import Display
  import Text.PrettyPrint.HughesPJ (render)
  import qualified Data.Sequence as S
  import System.FilePath
  import System.Directory
  import Control.Monad.Error
  
  import Language.LBNF.Runtime (ParseMonad(..))
  
  instance Error Doc where
    noMsg = "nanoAgda: unknown error"
    strMsg = text
  
  myLLexer = tokens 
  
  type Verbosity = Int
  
  putStrV :: Verbosity -> Doc -> Checker ()
  putStrV v s = if verb options >= v then liftIO $ putStrLn (render s) else return ()
  
  -- | The file containing the type of the term contained in file @f@
  typeFile f = replaceExtension f "type.na"
  
  runFile :: FilePath -> Checker Value
  runFile f = do
    putStrV 1 $ "Processing file:" <+> text f
    contents <- liftIO $ readFile f
    run contents f
  
  instance Pretty Token where
      pretty = text . show
  
  type Checker a = (ErrorT Doc IO) a
  
  run :: String -> FilePath -> Checker Value
  run s fname = let ts = myLLexer s in case pExp ts of
     Bad err -> do 
       putStrV 1 $ "Tokens:" <+> pretty ts
       throwError $ text $ fname ++ ": parse failed: " ++ err
     Ok tree -> do
       process fname tree
  
  getType :: FilePath -> Checker Value
  getType fname = do
    let t = typeFile fname
    putStrV 10 $ "typeFile = " <> text t
    ex <- liftIO $ doesFileExist t
    if ex  
      then do putStrV 2 $ "Using type from file: " <> text t
              runFile t 
      else do putStrV 2 "Using default type" 
              return (Star dummyPosition 1)
  
  process :: FilePath -> Exp -> Checker Value
  process fname modul = do
    typ <- getType fname
    let resolved = runResolver $ resolveTerm modul
    putStrV 4 $ "[Resolved into]" $$ pretty resolved
    let (checked,info) = runChecker (resolved,typ) $ cType mempty resolved typ
    mapM (putStrV 0) info  -- display constraints, etc.
    case checked of
      Right a -> do 
         putStrV 0 $ "nf =" <+> pretty a
         return a
      Left (e,err) -> do let (line,col) = termPosition e 
                         throwError $ (text fname <> ":" <> pretty line <> ":" <> pretty (col - 1) <> ": " <> err)
                         
        
  main :: IO ()
  main = do 
    results <- forM (files options) $ \f -> runErrorT $ runFile f
    let (errs,oks) = partitionEithers results
    mapM (putStrLn . render) errs               
    putStrLn $ show (length oks) ++ "/" ++ show (length results) ++ " files typecheck."
  
  