File size: 6,422 Bytes
a10b189 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 | {-# LANGUAGE OverloadedStrings #-}
{-|
Module : Assertica.Verify.CLI
Description : Command-line interface for verification
Copyright : (c) 2026 Ahmad Ali Parr
License : BSL-1.0
Provides a command-line interface for running verification from the shell.
Usage:
assertica-verify --file FILE [--output FORMAT] [--generate-haskell] [--strict]
assertica-verify --dir DIR [--output FORMAT] [--generate-haskell] [--strict]
Options:
--file FILE Verify single file (required if --dir not given)
--dir DIR Verify all .as files in directory (required if --file not given)
--output FORMAT Output format: json, text, csv (default: text)
--generate-haskell Generate Haskell code for verified modules
--strict Treat warnings as errors
--help Show this help message
Exit codes:
0 All verifications passed
N N verifications failed
-}
module Assertica.Verify.CLI
( -- * Main CLI entry point
main
-- * CLI argument parsing
, CLIArgs (..)
, OutputFormat (..)
, parseCLIArgs
, defaultCLIArgs
-- * CLI execution
, runCLI
) where
import System.Environment (getArgs, getProgName)
import System.Exit (exitFailure, exitSuccess, exitWith, ExitCode(..))
import System.IO (hPutStrLn, stderr)
import Assertica.Verify.Pipeline (verifyFile, verifyDirectory)
import Assertica.Verify.CI (ciVerify, generateBatchJSON, generateBatchCSV, getExitCode, generateBatchHumanReadable)
import Assertica.Verify.Report (toJSON, toHumanReadable, toCSV, Verdict(..))
-- ============================================================================
-- CLI TYPES
-- ============================================================================
{-| Output format specification.
-}
data OutputFormat
= JSON
| Text
| CSV
deriving (Eq, Show)
{-| Parsed command-line arguments.
-}
data CLIArgs = CLIArgs
{ argFile :: Maybe FilePath -- ^ File to verify
, argDir :: Maybe FilePath -- ^ Directory to verify
, argOutputFormat :: OutputFormat -- ^ Output format
, argGenerateHS :: Bool -- ^ Generate Haskell code
, argStrict :: Bool -- ^ Strict mode (warnings as errors)
, argHelp :: Bool -- ^ Show help
}
deriving (Show)
{-| Default CLI arguments.
-}
defaultCLIArgs :: CLIArgs
defaultCLIArgs = CLIArgs
{ argFile = Nothing
, argDir = Nothing
, argOutputFormat = Text
, argGenerateHS = False
, argStrict = False
, argHelp = False
}
-- ============================================================================
-- ARGUMENT PARSING
-- ============================================================================
{-| Parse command-line arguments.
Deterministic: Same arguments always produce same CLIArgs.
-}
parseCLIArgs :: [String] -> Either String CLIArgs
parseCLIArgs args = go args defaultCLIArgs
where
go :: [String] -> CLIArgs -> Either String CLIArgs
go [] acc = Right acc
go ("--file":path:rest) acc = go rest (acc { argFile = Just path })
go ("--dir":path:rest) acc = go rest (acc { argDir = Just path })
go ("--output":"json":rest) acc = go rest (acc { argOutputFormat = JSON })
go ("--output":"text":rest) acc = go rest (acc { argOutputFormat = Text })
go ("--output":"csv":rest) acc = go rest (acc { argOutputFormat = CSV })
go ("--generate-haskell":rest) acc = go rest (acc { argGenerateHS = True })
go ("--strict":rest) acc = go rest (acc { argStrict = True })
go ("--help":rest) acc = go rest (acc { argHelp = True })
go ("-h":rest) acc = go rest (acc { argHelp = True })
go (unknown:_) _ = Left $ "Unknown argument: " ++ unknown
-- ============================================================================
-- MAIN CLI ENTRY POINT
-- ============================================================================
{-| Main CLI entry point.
Parse arguments and dispatch to appropriate action.
-}
main :: IO ()
main = do
args <- getArgs
case parseCLIArgs args of
Left err -> do
hPutStrLn stderr $ "Error: " ++ err
exitFailure
Right opts
| argHelp opts -> showHelp
| otherwise -> runCLI opts
{-| Run CLI with parsed arguments.
-}
runCLI :: CLIArgs -> IO ()
runCLI opts
| argHelp opts = showHelp
| maybe False (not . null) (argFile opts) = do
let file = case argFile opts of
Just f -> f
Nothing -> error "File not provided"
report <- verifyFile file
case argOutputFormat opts of
JSON -> putStrLn (toJSON report)
Text -> putStrLn (toHumanReadable report)
CSV -> putStrLn (toCSV report)
let exitCode = if vrVerdict report == Reject then ExitFailure 1 else ExitSuccess
exitWith exitCode
| maybe False (not . null) (argDir opts) = do
let dir = case argDir opts of
Just d -> d
Nothing -> error "Directory not provided"
batchReport <- ciVerify dir
case argOutputFormat opts of
JSON -> putStrLn (generateBatchJSON batchReport)
Text -> putStrLn (generateBatchHumanReadable batchReport)
CSV -> putStrLn (generateBatchCSV batchReport)
exitWith (getExitCode batchReport)
| otherwise = do
hPutStrLn stderr "Error: Must provide either --file or --dir"
exitFailure
where
vrVerdict r = Assertica.Verify.Report.vrVerdict r
{-| Show help message.
-}
showHelp :: IO ()
showHelp = do
progName <- getProgName
putStrLn $ unlines
[ "Usage: " ++ progName ++ " [options]"
, ""
, "Options:"
, " --file FILE Verify single file"
, " --dir DIR Verify all .as files in directory"
, " --output FORMAT Output format: json, text, csv (default: text)"
, " --generate-haskell Generate Haskell code for verified modules"
, " --strict Treat warnings as errors"
, " --help, -h Show this help message"
, ""
, "Examples:"
, " " ++ progName ++ " --file example.as"
, " " ++ progName ++ " --dir ./proofs --output json"
, " " ++ progName ++ " --dir ./proofs --generate-haskell --output text"
, ""
, "Exit codes:"
, " 0 All verifications passed"
, " N > 0 N verifications failed"
]
exitSuccess
|