module Main

import Core.Check
import Core.Term
import Core.Value
import Core.Normalize
import Core.Misc
import Parser.Parse

import Control.Monad.Either
import Data.Vect
import Data.String
import Data.IORef
import Data.IOArray
import System
import System.File

smartPrint : {a : Type} -> Show a => a -> IO ()
smartPrint {a = String} = putStrLn
smartPrint {a = _}      = printLn

isTrue : String -> Bool -> IO ()
isTrue _   True  = pure ()
isTrue str False = putStrLn str >> exitFailure

unwrapCC : {a : Type} -> Show a => IO b -> Either a b -> IO b
unwrapCC {a = a} iob = \case 
                 Left e  => do
                   smartPrint e
                   iob
                 Right s => pure s

unwrap : {a : Type} -> Show a => Either a b -> IO b
unwrap = unwrapCC exitFailure

createNST : IO (Ref NST Nat)
createNST = do
  nstIoRef <- newIORef 0
  pure (MkRefP NST nstIoRef)

createDTX : (label : Type) -> Int -> IO (RefA label Value)
createDTX label n = do
  arr <- newArray n
  pure (MkRefP label arr)

typeCheck : {auto deftrs    : RefA DTR Value}
            -> {auto deftys : RefA DTY Value}
            -> {auto frst   : Ref  NST Nat}
            -> Int -> List (Term 0, Term 0) -> IO ()
typeCheck i []                 = pure ()
typeCheck i ((ty, tr) :: defs) = do
  vty <- unwrap =<< resolve (eval [] ty)
  vtr <- unwrap =<< resolve (eval [] tr)
  isTrue "putArr DTY" =<< putArr DTY i vty
  isTrue "putArr DTR" =<< putArr DTR i vtr
  typeCheck (i+1) defs

replRead : IO String
replRead = do
  line <- getLine
  if null (trim line)
     then replRead
     else case line of
               ":exit" => exitSuccess
               _       => pure line

repl : {auto deftrs    : RefA DTR Value}
       -> {auto deftys : RefA DTY Value}
       -> {auto frst   : Ref  NST Nat}
       -> List String -> IO a
repl strs = do
  line <- replRead
  term <- unwrapCC (repl strs) (parseEnv strs line)
  type <- unwrapCC (repl strs) =<< resolve (whnf =<< infer [] [] term)
  val  <- unwrapCC (repl strs) =<< resolve (whnf =<< eval  [] term)
  putStr "inferred type: "
  printLn type
  putStr "weak head normal form: "
  printLn val
  repl strs

main : IO ()
main = getArgs >>= \case
          (_ :: x :: xs) => do
            putStrLn (x ++ ": ")
            putStr "Parsing: "
            (strs, res) <- readFile x >>= unwrap >>= unwrap . toplevel
            putStrLn " OK!"
            let rlen = cast (length res)
            nst <- createNST
            dtr <- createDTX DTR rlen
            dty <- createDTX DTY rlen
            putStr "Typechecking: "
            typeCheck 0 res
            putStrLn "OK!"
            case xs of
                 ("repl" :: _) => repl strs
                 _             => exitSuccess
          _ => do
            nst <- createNST
            dtr <- createDTX DTR 0
            dty <- createDTX DTY 0
            repl []