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

import           Control.Monad       (forM)
import           Data.Version        (showVersion)
import           Options.Generic
import           System.Exit         (exitFailure)

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

data Command
  = Typecheck [FilePath]
  | 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 <- case [FilePath]
paths of
      -- if no paths are given — read from stdin
      [] -> 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 [(FilePath
"<stdin>", Module
rzkModule)]
      -- otherwise — parse all given files in given order
      [FilePath]
_ -> 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)
    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
Version -> FilePath -> IO ()
putStrLn (Version -> FilePath
showVersion Version
version)

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 (Module -> TypeCheck VarIdent [Decl']
typecheckModule 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!"