{-# LANGUAGE LambdaCase #-}
module Main where

import Control.Monad.IO.Class
import Control.Monad.Catch

import qualified Data.Map.Strict as Map
import Data.List

import Elab

import Eval (eval, UnifyError (..))

import Presyntax.Parser
import Presyntax

import Syntax

import System.Console.Haskeline (runInputT, defaultSettings, getInputLine)
import System.Exit

import Systems (formulaOfFace, Face)
import System.Environment

showTypeError :: Maybe [String] -> Elab.TypeError -> String
showTypeError lines (NotInScope l_c)       = "Variable not in scope: " ++ l_c

showTypeError lines (UnifyError (NotPiType vl)) = "Not a function type: " ++ show vl
showTypeError lines (UnifyError (NotSigmaType vl)) = "Not a sigma type: " ++ show vl
showTypeError lines (UnifyError (Mismatch a b)) =
  unlines [ "Types are not equal: "
          , "    " ++ show (quote a)
          , " vs "
          , "    " ++ show (quote b)
          ]

showTypeError lines (WrongFaces _ faces) = unlines (map face faces) where
  face :: ([Value], Value, Elab.TypeError) -> String
  face (ixs, rhs, err) =
    "When checking face described by " ++ show ixs ++ ":\n" ++ showTypeError Nothing err

showTypeError lines (InSpan start end err)
  | Just lines <- lines, fst start == fst end
  = makeRange (lines !! fst start) start end ++ '\n':showTypeError Nothing err
  | otherwise = showTypeError Nothing err

showTypeError lines (IncompleteSystem formula extent) =
  unlines $
    [ "Incomplete system: "
    , "it is defined by " ++ show formula
    , "but the context mandates extent " ++ show extent ]

showTypeError lines (IncompatibleFaces (fa, ta) (fb, tb) err) =
  unlines [ showTypeError lines err
          , "while checking that these overlapping faces are compatible:"
          , "* " ++ show fa ++ " -> " ++ show ta
          , "* " ++ show fb ++ " -> " ++ show tb
          ]

showTypeError _ x = show x

makeRange :: String -> (Int, Int) -> (Int, Int) -> String
makeRange line (_, sc) (_, ec) = line ++ "\n" ++ replicate (sc + 1) ' ' ++ replicate (ec - sc) '~'

main :: IO ()
main = do
  t <- getArgs
  case t of
    [file] -> Main.check file
    _ -> repl

check :: FilePath -> IO ()
check file = do
  code <- readFile file
  let
    ste e = do
      putStrLn $ showTypeError (Just (lines code)) e
      exitFailure
  case parseString body code of
    Left e -> print e
    Right x -> do
      (tm, _) <- infer (Env mempty) x `catch` ste `catch` (ste . UnifyError)
      print (eval (Env mempty) tm)

repl :: IO ()
repl = runInputT defaultSettings (go (Env mempty)) where
  go env = getInputLine "> " >>= \case
    Just i | ":sq " `isPrefixOf` i -> do
      case parseString body (replicate 4 ' ' ++ drop 4 i) of
        Right exp ->
          (do
            (tm, ty) <- liftIO $ infer env exp
            liftIO $ drawExtent ty (eval env tm)
          `catch` \e -> liftIO $ putStrLn (showTypeError (Just [i]) e))
          `catch` \e -> liftIO $ print (e :: SomeException)
        Left e -> liftIO (print e)
      go env
    Just i ->
      case parseString statement i of
        Left e -> liftIO (print e) *> go env
        Right (Assume vs) ->
          let
            loop env ((v, t):vs) = do
              tm <- liftIO $ Elab.check env t VTypeω
              let ty = eval env tm
              loop env{ names = Map.insert v (ty, VVar v) (names env) } vs
            loop env [] = go env
          in (loop env vs
              `catch` \e -> (liftIO $ putStrLn (showTypeError (Just [i]) e)) *> go env)
              `catch` \e -> (liftIO $ print (e :: SomeException)) *> go env
        Right (Eval v) -> do
          liftIO $
            (do
              (tm, ty) <- infer env v
              let v_nf = eval env tm
              putStrLn $ show v_nf ++ " : " ++ show ty
            `catch` \e -> putStrLn (showTypeError (Just [i]) e))
            `catch` \e -> print (e :: SomeException)
          go env
        Right (Declare n t e) -> do
          (do
            t <- liftIO $ Elab.check env t VTypeω
            let t' = eval env t
            b <- liftIO $ Elab.check env e t'
            let b' = eval env b
            go env{ names = Map.insert n (t', b') (names env) })
          `catch` \e -> (liftIO $ putStrLn (showTypeError (Just [i]) e)) *> go env
          `catch` \e -> (liftIO $ print (e :: SomeException)) *> go env
    Nothing -> pure ()

drawExtent :: Value -> Value -> IO ()
drawExtent ty vl = nicely $ getDirections ty vl where
  getDirections :: Value -> Value -> [([(String, Bool)], Value, Value)]
  getDirections (VPi _ VI r) (VLam s VI k) =
    let trues  = getDirections (r VI1) (k VI1)
        falses = getDirections (r VI0) (k VI0)
    in map (\(p, t, v) -> ((s, True):p, t, v))  trues
    ++ map (\(p, t, v) -> ((s, False):p, t, v)) falses
  getDirections ty t = [([], ty, t)]

  nicely :: [([(String, Bool)], Value, Value)] -> IO ()
  nicely [] = pure ()
  nicely ((bs, ty, el):fcs) = do
    putStr . unwords $ theFace bs
    putStrLn $ " => " ++ show el ++ " : " ++ show ty
    nicely fcs

  theFace = map (\(i, b) ->
    if b
      then "(" ++ i ++ "1)"
      else "(" ++ i ++ "0)")