Skip to content

Commit

Permalink
Add rzk version command
Browse files Browse the repository at this point in the history
  • Loading branch information
fizruk committed Jun 15, 2023
1 parent 9286afa commit f1709dc
Show file tree
Hide file tree
Showing 3 changed files with 47 additions and 38 deletions.
1 change: 1 addition & 0 deletions rzk/package.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ dependencies:
- bifunctors
- mtl
- template-haskell
- optparse-generic

ghc-options:
- -Wall
Expand Down
7 changes: 4 additions & 3 deletions rzk/rzk.cabal
Original file line number Diff line number Diff line change
@@ -1,10 +1,8 @@
cabal-version: 1.12

-- This file has been generated from package.yaml by hpack version 0.35.2.
-- This file has been generated from package.yaml by hpack version 0.35.1.
--
-- see: https://github.com/sol/hpack
--
-- hash: 7855530fcdfd2a28c4ea3654677ed2d18f83d419f5d1c173f4bb44a915464c06

name: rzk
version: 0.4.0
Expand Down Expand Up @@ -51,6 +49,7 @@ library
, base >=4.7 && <5
, bifunctors
, mtl
, optparse-generic
, template-haskell
default-language: Haskell2010

Expand All @@ -66,6 +65,7 @@ executable rzk
, base >=4.7 && <5
, bifunctors
, mtl
, optparse-generic
, rzk
, template-haskell
default-language: Haskell2010
Expand All @@ -83,6 +83,7 @@ test-suite rzk-test
, base >=4.7 && <5
, bifunctors
, mtl
, optparse-generic
, rzk
, template-haskell
default-language: Haskell2010
77 changes: 42 additions & 35 deletions rzk/src/Rzk/Main.hs
Original file line number Diff line number Diff line change
@@ -1,48 +1,55 @@
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
module Rzk.Main where

import Control.Monad (forM)
import System.Environment (getArgs)
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 (Generic, Show, ParseRecord)

main :: IO ()
main = do
args <- getArgs
case args of
"typecheck" : paths -> do
modules <- case paths of
-- if no paths are given — read from stdin
[] -> do
result <- Rzk.parseModule <$> getContents
case result of
Left err -> do
putStrLn ("An error occurred when parsing stdin")
error err
Right rzkModule -> return [("<stdin>", rzkModule)]
-- otherwise — parse all given files in given order
_ -> forM paths $ \path -> do
putStrLn ("Loading file " <> path)
result <- Rzk.parseModule <$> readFile path
case result of
Left err -> do
putStrLn ("An error occurred when parsing file " <> path)
error err
Right rzkModule -> return (path, rzkModule)
case defaultTypeCheck (typecheckModulesWithLocation modules) of
Left err -> do
putStrLn "An error occurred when typechecking!"
putStrLn $ unlines
[ "Type Error:"
, ppTypeErrorInScopedContext' err
]
exitFailure
Right () -> putStrLn "Everything is ok!"
_ -> ppUsage
main = getRecord "rzk: an experimental proof assistant for synthetic ∞-categories" >>= \case
Typecheck paths -> do
modules <- case paths of
-- if no paths are given — read from stdin
[] -> do
result <- Rzk.parseModule <$> getContents
case result of
Left err -> do
putStrLn ("An error occurred when parsing stdin")
error err
Right rzkModule -> return [("<stdin>", rzkModule)]
-- otherwise — parse all given files in given order
_ -> forM paths $ \path -> do
putStrLn ("Loading file " <> path)
result <- Rzk.parseModule <$> readFile path
case result of
Left err -> do
putStrLn ("An error occurred when parsing file " <> path)
error err
Right rzkModule -> return (path, rzkModule)
case defaultTypeCheck (typecheckModulesWithLocation modules) of
Left err -> do
putStrLn "An error occurred when typechecking!"
putStrLn $ unlines
[ "Type Error:"
, ppTypeErrorInScopedContext' err
]
exitFailure
Right () -> putStrLn "Everything is ok!"

ppUsage :: IO ()
ppUsage = putStrLn "rzk typecheck FILE"
Version -> putStrLn (showVersion version)

typecheckString :: String -> Either String String
typecheckString moduleString = do
Expand Down

0 comments on commit f1709dc

Please sign in to comment.