From f1709dc70379e0329daaca025930a6e68bddf561 Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Fri, 16 Jun 2023 00:32:53 +0300
Subject: [PATCH] Add rzk version command

---
 rzk/package.yaml    |  1 +
 rzk/rzk.cabal       |  7 +++--
 rzk/src/Rzk/Main.hs | 77 ++++++++++++++++++++++++---------------------
 3 files changed, 47 insertions(+), 38 deletions(-)

diff --git a/rzk/package.yaml b/rzk/package.yaml
index 399e6c6b3..f4c799e65 100644
--- a/rzk/package.yaml
+++ b/rzk/package.yaml
@@ -24,6 +24,7 @@ dependencies:
 - bifunctors
 - mtl
 - template-haskell
+- optparse-generic
 
 ghc-options:
 - -Wall
diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal
index 7ab52c146..595b18153 100644
--- a/rzk/rzk.cabal
+++ b/rzk/rzk.cabal
@@ -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
@@ -51,6 +49,7 @@ library
     , base >=4.7 && <5
     , bifunctors
     , mtl
+    , optparse-generic
     , template-haskell
   default-language: Haskell2010
 
@@ -66,6 +65,7 @@ executable rzk
     , base >=4.7 && <5
     , bifunctors
     , mtl
+    , optparse-generic
     , rzk
     , template-haskell
   default-language: Haskell2010
@@ -83,6 +83,7 @@ test-suite rzk-test
     , base >=4.7 && <5
     , bifunctors
     , mtl
+    , optparse-generic
     , rzk
     , template-haskell
   default-language: Haskell2010
diff --git a/rzk/src/Rzk/Main.hs b/rzk/src/Rzk/Main.hs
index 6ab73b8b7..33f65b832 100644
--- a/rzk/src/Rzk/Main.hs
+++ b/rzk/src/Rzk/Main.hs
@@ -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