rzk-0.7.0: app/Main.hs

{-# 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
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 = 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
      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)