{-# 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 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
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 [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 (forall a. [a] -> [a]
reverse [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!"