{-# LANGUAGE DeriveAnyClass    #-}
{-# LANGUAGE DeriveGeneric     #-}
{-# LANGUAGE LambdaCase        #-}
{-# LANGUAGE OverloadedStrings #-}
module Rzk.Main where

import           Control.Monad                (forM)
import qualified Data.Aeson                   as JSON
import qualified Data.ByteString.Lazy.Char8   as ByteString
import           Data.Version                 (showVersion)
import           Options.Generic
import           System.Exit                  (exitFailure)

import qualified Language.Rzk.Syntax          as Rzk
import           Language.Rzk.VSCode.Tokenize (tokenizeModule)
import           Paths_rzk                    (version)
import           Rzk.TypeCheck

data Command
  = Typecheck [FilePath]
  | Tokenize
  | Version
  deriving (forall x. Rep Command x -> Command
forall x. Command -> Rep Command x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Command x -> Command
$cfrom :: forall x. Command -> Rep Command x
Generic, Int -> Command -> ShowS
[Command] -> ShowS
Command -> FilePath
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [Command] -> ShowS
$cshowList :: [Command] -> ShowS
show :: Command -> FilePath
$cshow :: Command -> FilePath
showsPrec :: Int -> Command -> ShowS
$cshowsPrec :: Int -> Command -> ShowS
Show, Parser Command
forall a. Parser a -> ParseRecord a
parseRecord :: Parser Command
$cparseRecord :: Parser Command
ParseRecord)

main :: IO ()
main :: IO ()
main = forall (io :: * -> *) a.
(MonadIO io, ParseRecord a) =>
Text -> io a
getRecord Text
"rzk: an experimental proof assistant for synthetic ∞-categories" forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Typecheck [FilePath]
paths -> do
    [(FilePath, Module)]
modules <- [FilePath] -> IO [(FilePath, Module)]
parseRzkFilesOrStdin [FilePath]
paths
    case forall a.
TypeCheck VarIdent a
-> Either (TypeErrorInScopedContext VarIdent) a
defaultTypeCheck ([(FilePath, Module)] -> TypeCheck VarIdent ()
typecheckModulesWithLocation [(FilePath, Module)]
modules) of
      Left TypeErrorInScopedContext VarIdent
err -> do
        FilePath -> IO ()
putStrLn FilePath
"An error occurred when typechecking!"
        FilePath -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines
          [ FilePath
"Type Error:"
          , TypeErrorInScopedContext VarIdent -> FilePath
ppTypeErrorInScopedContext' TypeErrorInScopedContext VarIdent
err
          ]
        forall a. IO a
exitFailure
      Right () -> FilePath -> IO ()
putStrLn FilePath
"Everything is ok!"

  Command
Tokenize -> do
    Module
rzkModule <- IO Module
parseStdin
    ByteString -> IO ()
ByteString.putStrLn (forall a. ToJSON a => a -> ByteString
JSON.encode (Module -> [VSToken]
tokenizeModule Module
rzkModule))

  Command
Version -> FilePath -> IO ()
putStrLn (Version -> FilePath
showVersion Version
version)

parseStdin :: IO Rzk.Module
parseStdin :: IO Module
parseStdin = do
  Either FilePath Module
result <- FilePath -> Either FilePath Module
Rzk.parseModule forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO FilePath
getContents
  case Either FilePath Module
result of
    Left FilePath
err -> do
      FilePath -> IO ()
putStrLn (FilePath
"An error occurred when parsing stdin")
      forall a. HasCallStack => FilePath -> a
error FilePath
err
    Right Module
rzkModule -> forall (m :: * -> *) a. Monad m => a -> m a
return Module
rzkModule

parseRzkFilesOrStdin :: [FilePath] -> IO [(FilePath, Rzk.Module)]
parseRzkFilesOrStdin :: [FilePath] -> IO [(FilePath, Module)]
parseRzkFilesOrStdin = \case
  -- if no paths are given — read from stdin
  [] -> do
    Module
rzkModule <- IO Module
parseStdin
    forall (m :: * -> *) a. Monad m => a -> m a
return [(FilePath
"<stdin>", Module
rzkModule)]
  -- otherwise — parse all given files in given order
  [FilePath]
paths -> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [FilePath]
paths forall a b. (a -> b) -> a -> b
$ \FilePath
path -> do
    FilePath -> IO ()
putStrLn (FilePath
"Loading file " forall a. Semigroup a => a -> a -> a
<> FilePath
path)
    Either FilePath Module
result <- FilePath -> Either FilePath Module
Rzk.parseModule forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> IO FilePath
readFile FilePath
path
    case Either FilePath Module
result of
      Left FilePath
err -> do
        FilePath -> IO ()
putStrLn (FilePath
"An error occurred when parsing file " forall a. Semigroup a => a -> a -> a
<> FilePath
path)
        forall a. HasCallStack => FilePath -> a
error FilePath
err
      Right Module
rzkModule -> forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath
path, Module
rzkModule)

typecheckString :: String -> Either String String
typecheckString :: FilePath -> Either FilePath FilePath
typecheckString FilePath
moduleString = do
  Module
rzkModule <- FilePath -> Either FilePath Module
Rzk.parseModule FilePath
moduleString
  case forall a.
TypeCheck VarIdent a
-> Either (TypeErrorInScopedContext VarIdent) a
defaultTypeCheck (Maybe FilePath -> Module -> TypeCheck VarIdent [Decl']
typecheckModule forall a. Maybe a
Nothing Module
rzkModule) of
    Left TypeErrorInScopedContext VarIdent
err -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines
      [ FilePath
"An error occurred when typechecking!"
      , FilePath
"Rendering type error... (this may take a few seconds)"
      , [FilePath] -> FilePath
unlines
        [ FilePath
"Type Error:"
        , TypeErrorInScopedContext VarIdent -> FilePath
ppTypeErrorInScopedContext' TypeErrorInScopedContext VarIdent
err
        ]
      ]
    Right [Decl']
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure FilePath
"Everything is ok!"