fix: move cli code into app

rzk-lang · Dec 8, 2023 · 21c82b5 · 21c82b5
1 parent e9d12dc
commit 21c82b5
Show file tree

Hide file tree

Showing 2 changed files with 84 additions and 79 deletions.
diff --git a/rzk/app/Main.hs b/rzk/app/Main.hs
@@ -1,14 +1,92 @@
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP               #-}
+{-# LANGUAGE DeriveAnyClass    #-}
+{-# LANGUAGE DeriveGeneric     #-}
+{-# LANGUAGE LambdaCase        #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TupleSections     #-}
+
 module Main (main) where
 
 #ifndef __GHCJS__
 import           Main.Utf8 (withUtf8)
 #endif
-import qualified Rzk.Main
+
+import           Control.Monad           (forM, forM_, unless, when,
+                                          (>=>))
+import           Data.Version            (showVersion)
+
+#ifdef LSP
+import           Language.Rzk.VSCode.Lsp (runLsp)
+#endif
+
+import           Options.Generic
+import           System.Exit             (exitFailure, exitSuccess)
+
+import           Data.Functor            ((<&>))
+import           Paths_rzk               (version)
+import           Rzk.Format              (formatFile, formatFileWrite,
+                                          isWellFormattedFile)
+import           Rzk.TypeCheck
+import           Rzk.Main
+
+data FormatOptions = FormatOptions
+  { check :: Bool
+  , write :: Bool
+  } deriving (Generic, Show, ParseRecord, Read, ParseField)
+
+instance ParseFields FormatOptions where
+  parseFields _ _ _ _ = FormatOptions
+    <$> parseFields (Just "Check if the files are correctly formatted") (Just "check") (Just 'c') Nothing
+    <*> parseFields (Just "Write formatted file to disk") (Just "write") (Just 'w') Nothing
+
+data Command
+  = Typecheck [FilePath]
+  | Lsp
+  | Format FormatOptions [FilePath]
+  | Version
+  deriving (Generic, Show, ParseRecord)
 
 main :: IO ()
-main =
+main = do
 #ifndef __GHCJS__
-  withUtf8
+  withUtf8 $
+#endif
+    getRecord "rzk: an experimental proof assistant for synthetic ∞-categories" >>= \case
+    Typecheck paths -> do
+      modules <- parseRzkFilesOrStdin paths
+      case defaultTypeCheck (typecheckModulesWithLocation modules) of
+        Left err -> do
+          putStrLn "An error occurred when typechecking!"
+          putStrLn $ unlines
+            [ "Type Error:"
+            , ppTypeErrorInScopedContext' BottomUp err
+            ]
+          exitFailure
+        Right _decls -> putStrLn "Everything is ok!"
+
+    Lsp ->
+#ifdef LSP
+      void runLsp
+#else
+      error "rzk lsp is not supported with this build"
 #endif
-    Rzk.Main.main
+
+    Format (FormatOptions check write) paths -> do
+      when (check && write) (error "Options --check and --write are mutually exclusive")
+      expandedPaths <- expandRzkPathsOrYaml paths
+      case expandedPaths of
+        [] -> error "No files found"
+        filePaths -> do
+          when (not check && not write) $ forM_ filePaths (formatFile >=> putStrLn)
+          when write $ forM_ filePaths formatFileWrite
+          when check $ do
+            results <- forM filePaths $ \path -> isWellFormattedFile path <&> (path,)
+            let notFormatted = map fst $ filter (not . snd) results
+            unless (null notFormatted) $ do
+              putStrLn "Some files are not well formatted:"
+              forM_ notFormatted $ \path -> putStrLn ("  " <> path)
+              exitFailure
+            exitSuccess
+
+    Version -> putStrLn (showVersion version)
+
diff --git a/rzk/src/Rzk/Main.hs b/rzk/src/Rzk/Main.hs
@@ -1,93 +1,20 @@
-{-# LANGUAGE CPP               #-}
-{-# LANGUAGE DeriveAnyClass    #-}
-{-# LANGUAGE DeriveGeneric     #-}
 {-# LANGUAGE LambdaCase        #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RecordWildCards   #-}
-{-# LANGUAGE TupleSections     #-}
 {-# LANGUAGE TypeApplications  #-}
 
 module Rzk.Main where
 
-import           Control.Monad           (forM, forM_, unless, void, when,
-                                          (>=>))
+import           Control.Monad           (forM, when)
 import           Data.List               (sort)
-import           Data.Version            (showVersion)
-
-#ifdef LSP
-import           Language.Rzk.VSCode.Lsp (runLsp)
-#endif
-
 import qualified Data.Yaml               as Yaml
-import           Options.Generic
 import           System.Directory        (doesPathExist)
-import           System.Exit             (exitFailure, exitSuccess)
 import           System.FilePath.Glob    (glob)
-
-import           Data.Functor            ((<&>))
 import qualified Language.Rzk.Syntax     as Rzk
-import           Paths_rzk               (version)
-import           Rzk.Format              (formatFile, formatFileWrite,
-                                          isWellFormattedFile)
 import           Rzk.Project.Config
 import           Rzk.TypeCheck
 
-data FormatOptions = FormatOptions
-  { check :: Bool
-  , write :: Bool
-  } deriving (Generic, Show, ParseRecord, Read, ParseField)
-
-instance ParseFields FormatOptions where
-  parseFields _ _ _ _ = FormatOptions
-    <$> parseFields (Just "Check if the files are correctly formatted") (Just "check") (Just 'c') Nothing
-    <*> parseFields (Just "Write formatted file to disk") (Just "write") (Just 'w') Nothing
-
-data Command
-  = Typecheck [FilePath]
-  | Lsp
-  | Format FormatOptions [FilePath]
-  | Version
-  deriving (Generic, Show, ParseRecord)
-
-main :: IO ()
-main = getRecord "rzk: an experimental proof assistant for synthetic ∞-categories" >>= \case
-  Typecheck paths -> do
-    modules <- parseRzkFilesOrStdin paths
-    case defaultTypeCheck (typecheckModulesWithLocation modules) of
-      Left err -> do
-        putStrLn "An error occurred when typechecking!"
-        putStrLn $ unlines
-          [ "Type Error:"
-          , ppTypeErrorInScopedContext' BottomUp err
-          ]
-        exitFailure
-      Right _decls -> putStrLn "Everything is ok!"
-
-  Lsp ->
-#ifdef LSP
-    void runLsp
-#else
-    error "rzk lsp is not supported with this build"
-#endif
-
-  Format (FormatOptions check write) paths -> do
-    when (check && write) (error "Options --check and --write are mutually exclusive")
-    expandedPaths <- expandRzkPathsOrYaml paths
-    case expandedPaths of
-      [] -> error "No files found"
-      filePaths -> do
-        when (not check && not write) $ forM_ filePaths (formatFile >=> putStrLn)
-        when write $ forM_ filePaths formatFileWrite
-        when check $ do
-          results <- forM filePaths $ \path -> isWellFormattedFile path <&> (path,)
-          let notFormatted = map fst $ filter (not . snd) results
-          unless (null notFormatted) $ do
-            putStrLn "Some files are not well formatted:"
-            forM_ notFormatted $ \path -> putStrLn ("  " <> path)
-            exitFailure
-          exitSuccess
 
-  Version -> putStrLn (showVersion version)
 
 parseStdin :: IO Rzk.Module
 parseStdin = do