{-# LANGUAGE CPP               #-}
{-# LANGUAGE DeriveAnyClass    #-}
{-# LANGUAGE DeriveGeneric     #-}
{-# LANGUAGE LambdaCase        #-}
{-# LANGUAGE OverloadedStrings #-}

module Rzk.Main where

import           Control.Monad           (forM, void)
import           Data.List               (sort)
import           Data.Version            (showVersion)
#ifndef __GHCJS__
import           Language.Rzk.VSCode.Lsp (runLsp)
#endif
import           Options.Generic
import           System.Exit             (exitFailure)
import           System.FilePath.Glob    (glob)

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

data Command
  = Typecheck [FilePath]
  | Lsp
  | 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 [(FilePath, [Decl'])]
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:"
          , OutputDirection -> TypeErrorInScopedContext VarIdent -> FilePath
ppTypeErrorInScopedContext' OutputDirection
BottomUp TypeErrorInScopedContext VarIdent
err
          ]
        forall a. IO a
exitFailure
      Right [(FilePath, [Decl'])]
_decls -> FilePath -> IO ()
putStrLn FilePath
"Everything is ok!"

  Command
Lsp ->
#ifndef __GHCJS__
    forall (f :: * -> *) a. Functor f => f a -> f ()
void IO Int
runLsp
#else
    error "rzk lsp is not supported with a GHCJS build"
#endif

  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'], [TypeErrorInScopedContext VarIdent])
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:"
        , OutputDirection -> TypeErrorInScopedContext VarIdent -> FilePath
ppTypeErrorInScopedContext' OutputDirection
BottomUp TypeErrorInScopedContext VarIdent
err
        ]
      ]
    Right ([Decl'], [TypeErrorInScopedContext VarIdent])
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure FilePath
"Everything is ok!"