{-# 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.List                    (sort)
import           Data.Version                 (showVersion)
import           Options.Generic
import           System.Exit                  (exitFailure)
import           System.FilePath.Glob         (glob)

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 var a.
TypeCheck var a -> Either (TypeErrorInScopedContext var) 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

-- | Finds matches to the given pattern in the current working directory.
-- **NOTE:** throws exception when 'glob' returns an empty list.
globNonEmpty :: FilePath -> IO [FilePath]
globNonEmpty :: FilePath -> IO [FilePath]
globNonEmpty FilePath
path = do
  FilePath -> IO [FilePath]
glob FilePath
path forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    []    -> forall a. HasCallStack => FilePath -> a
error (FilePath
"File(s) not found at " forall a. Semigroup a => a -> a -> a
<> FilePath
path)
    [FilePath]
paths -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Ord a => [a] -> [a]
sort [FilePath]
paths)

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 -> do
    [FilePath]
expandedPaths <- forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap FilePath -> IO [FilePath]
globNonEmpty [FilePath]
paths
    forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [FilePath]
expandedPaths 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 var a.
TypeCheck var a -> Either (TypeErrorInScopedContext var) 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!"