{-# 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
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
[] -> do
Module
rzkModule <- IO Module
parseStdin
forall (m :: * -> *) a. Monad m => a -> m a
return [(FilePath
"<stdin>", Module
rzkModule)]
[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!"