|
1 | | -{-# LANGUAGE CPP #-} |
| 1 | +{-# LANGUAGE CPP #-} |
| 2 | +{-# LANGUAGE DeriveAnyClass #-} |
| 3 | +{-# LANGUAGE DeriveGeneric #-} |
| 4 | +{-# LANGUAGE LambdaCase #-} |
| 5 | +{-# LANGUAGE OverloadedStrings #-} |
| 6 | +{-# LANGUAGE TupleSections #-} |
| 7 | +{-# LANGUAGE NamedFieldPuns #-} |
| 8 | + |
2 | 9 | module Main (main) where |
3 | 10 |
|
4 | 11 | #ifndef __GHCJS__ |
5 | 12 | import Main.Utf8 (withUtf8) |
6 | 13 | #endif |
7 | | -import qualified Rzk.Main |
| 14 | + |
| 15 | +import Control.Monad (forM, forM_, unless, when, |
| 16 | + (>=>)) |
| 17 | +import Data.Version (showVersion) |
| 18 | + |
| 19 | +#ifdef LSP |
| 20 | +import Language.Rzk.VSCode.Lsp (runLsp) |
| 21 | +#endif |
| 22 | + |
| 23 | +import Options.Generic |
| 24 | +import System.Exit (exitFailure, exitSuccess) |
| 25 | + |
| 26 | +import Data.Functor ((<&>)) |
| 27 | +import Paths_rzk (version) |
| 28 | +import Rzk.Format (formatFile, formatFileWrite, |
| 29 | + isWellFormattedFile) |
| 30 | +import Rzk.TypeCheck |
| 31 | +import Rzk.Main |
| 32 | + |
| 33 | +data FormatOptions = FormatOptions |
| 34 | + { check :: Bool |
| 35 | + , write :: Bool |
| 36 | + } deriving (Generic, Show, ParseRecord, Read, ParseField) |
| 37 | + |
| 38 | +instance ParseFields FormatOptions where |
| 39 | + parseFields _ _ _ _ = FormatOptions |
| 40 | + <$> parseFields (Just "Check if the files are correctly formatted") (Just "check") (Just 'c') Nothing |
| 41 | + <*> parseFields (Just "Write formatted file to disk") (Just "write") (Just 'w') Nothing |
| 42 | + |
| 43 | +data Command |
| 44 | + = Typecheck [FilePath] |
| 45 | + | Lsp |
| 46 | + | Format FormatOptions [FilePath] |
| 47 | + | Version |
| 48 | + deriving (Generic, Show, ParseRecord) |
8 | 49 |
|
9 | 50 | main :: IO () |
10 | | -main = |
| 51 | +main = do |
11 | 52 | #ifndef __GHCJS__ |
12 | | - withUtf8 |
| 53 | + withUtf8 $ |
| 54 | +#endif |
| 55 | + getRecord "rzk: an experimental proof assistant for synthetic ∞-categories" >>= \case |
| 56 | + Typecheck paths -> do |
| 57 | + modules <- parseRzkFilesOrStdin paths |
| 58 | + case defaultTypeCheck (typecheckModulesWithLocation modules) of |
| 59 | + Left err -> do |
| 60 | + putStrLn "An error occurred when typechecking!" |
| 61 | + putStrLn $ unlines |
| 62 | + [ "Type Error:" |
| 63 | + , ppTypeErrorInScopedContext' BottomUp err |
| 64 | + ] |
| 65 | + exitFailure |
| 66 | + Right _decls -> putStrLn "Everything is ok!" |
| 67 | + |
| 68 | + Lsp -> |
| 69 | +#ifdef LSP |
| 70 | + void runLsp |
| 71 | +#else |
| 72 | + error "rzk lsp is not supported with this build" |
13 | 73 | #endif |
14 | | - Rzk.Main.main |
| 74 | + |
| 75 | + Format (FormatOptions {check, write}) paths -> do |
| 76 | + when (check && write) (error "Options --check and --write are mutually exclusive") |
| 77 | + expandedPaths <- expandRzkPathsOrYaml paths |
| 78 | + case expandedPaths of |
| 79 | + [] -> error "No files found" |
| 80 | + filePaths -> do |
| 81 | + when (not check && not write) $ forM_ filePaths (formatFile >=> putStrLn) |
| 82 | + when write $ forM_ filePaths formatFileWrite |
| 83 | + when check $ do |
| 84 | + results <- forM filePaths $ \path -> isWellFormattedFile path <&> (path,) |
| 85 | + let notFormatted = map fst $ filter (not . snd) results |
| 86 | + unless (null notFormatted) $ do |
| 87 | + putStrLn "Some files are not well formatted:" |
| 88 | + forM_ notFormatted $ \path -> putStrLn (" " <> path) |
| 89 | + exitFailure |
| 90 | + exitSuccess |
| 91 | + |
| 92 | + Version -> putStrLn (showVersion version) |
| 93 | + |
0 commit comments