content: {-# LANGUAGE CPP               #-}
  {-# LANGUAGE DeriveAnyClass    #-}
  {-# LANGUAGE DeriveGeneric     #-}
  {-# LANGUAGE LambdaCase        #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE TupleSections     #-}
  {-# LANGUAGE NamedFieldPuns #-}
  
  module Main (main) where
  
  #ifndef __GHCJS__
  import           Main.Utf8 (withUtf8)
  #endif
  
  import           Control.Monad           (forM, forM_, unless, when,
                                            (>=>))
  import           Data.Version            (showVersion)
  
  #ifdef LSP_ENABLED
  import           Language.Rzk.VSCode.Lsp (runLsp)
  #endif
  
  import           Options.Generic
  import           System.Exit             (exitFailure, exitSuccess)
  
  import           Data.Functor            (void, (<&>))
  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 = do
  #ifndef __GHCJS__
    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_ENABLED
        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)
  