October 2026 main drop: mirror from GitHub

a10b189 verified about 1 month ago

13.5 kB

{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}

{-|
Module      : Assertica.Verify.Report
Description : Verification report structures and serialization
Copyright   : (c) 2026 Ahmad Ali Parr
License     : BSL-1.0
The VerificationReport captures the complete result of verifying a file or module,
including the results at each pipeline stage, detailed errors, and the final verdict.
DESIGN PRINCIPLES:
1. Comprehensive: Captures all verification state at each stage
2. Deterministic: Same input produces identical report
3. Machine-readable: JSON serialization for CI consumption
4. Human-readable: Clear text format with explanations
5. Actionable: Every error includes source location and context
-}

module Assertica.Verify.Report
  ( -- * Main report types
    VerificationReport (..)
  , StageResult (..)
  , Verdict (..)
  , SourceLocation (..)

    -- * Error types
  , ErrorDetail (..)
  , ErrorCategory (..)

    -- * Report builders and serialization
  , mkReport
  , mkStageResult
  , toJSON
  , toHumanReadable
  , toCSV

    -- * Utility functions
  , isSuccess
  , allStagesSuccessful
  , stagesToList
  ) where

import Data.Text (Text)
import qualified Data.Text as T
import Data.List (intercalate)
import Data.Time (UTCTime)
import GHC.Generics (Generic)
import Data.Ord (comparing)

-- ============================================================================
-- SOURCE LOCATION
-- ============================================================================

{-| Source location with file and line information.
-}
data SourceLocation = SourceLocation
  { slFile   :: String
  , slLine   :: Int
  , slColumn :: Int
  }
  deriving (Eq, Show, Generic)

-- ============================================================================
-- ERROR TYPES
-- ============================================================================

{-| Error category for classification.
-}
data ErrorCategory
  = SyntaxError       -- ^ Parse failed (lexer/parser)
  | TypeError         -- ^ Type checker rejected
  | ProofObligation   -- ^ Proof missing or invalid
  | ModuleError       -- ^ Circular dependency, missing import
  | TerminationError  -- ^ Recursion not structurally decreasing
  | PositivityError   -- ^ Inductive type not strictly positive
  | CodeGenError      -- ^ Code generation failed
  | UnknownError      -- ^ Unexpected error
  deriving (Eq, Show, Ord, Generic)

{-| Detailed error information.
-}
data ErrorDetail = ErrorDetail
  { edCategory    :: ErrorCategory
  , edMessage     :: String
  , edLocation    :: Maybe SourceLocation
  , edContext     :: Maybe String    -- ^ Source code context
  , edSuggestedFix :: Maybe String   -- ^ Fix suggestion
  }
  deriving (Eq, Show, Generic)

-- ============================================================================
-- STAGE RESULTS
-- ============================================================================

{-| Result of a single verification stage.
-}
data StageResult
  = StageOK
      { srStageName :: String
      , srDuration :: Double   -- ^ Milliseconds
      }
  | StageFailed
      { srStageName :: String
      , srDuration :: Double
      , srError :: ErrorDetail
      }
  deriving (Eq, Show, Generic)

-- ============================================================================
-- FINAL VERDICT
-- ============================================================================

{-| Final verification verdict.
-}
data Verdict
  = Accept   -- ^ Module verified successfully
  | Reject   -- ^ Module failed verification
  deriving (Eq, Show, Ord, Generic)

-- ============================================================================
-- VERIFICATION REPORT
-- ============================================================================

{-| Complete verification report for a file/module.
-}
data VerificationReport = VerificationReport
  { vrFile              :: String              -- ^ Input file path
  , vrModule            :: Maybe String        -- ^ Module name (if applicable)
  , vrRevision          :: Maybe String        -- ^ Git revision or hash
  , vrTimestamp         :: String              -- ^ ISO 8601 timestamp
  , vrParseResult       :: StageResult         -- ^ Lexer/Parser stage
  , vrElaborationResult :: StageResult         -- ^ Elaboration stage
  , vrTypeCheckResult   :: StageResult         -- ^ Type checking stage
  , vrProofCheckResult  :: StageResult         -- ^ Proof verification stage
  , vrCodeGenResult     :: StageResult         -- ^ Code generation stage
  , vrVerdict           :: Verdict             -- ^ Final verdict
  , vrTotalDuration     :: Double              -- ^ Total time in milliseconds
  , vrAdditionalErrors  :: [ErrorDetail]       -- ^ Non-fatal errors or warnings
  }
  deriving (Eq, Show, Generic)

-- ============================================================================
-- REPORT CONSTRUCTION
-- ============================================================================

{-| Create a successful stage result.
-}
mkStageResult :: String -> Double -> StageResult
mkStageResult name duration = StageOK name duration

{-| Create a failed stage result.
-}
mkFailedStageResult :: String -> Double -> ErrorDetail -> StageResult
mkFailedStageResult name duration err = StageFailed name duration err

{-| Create a verification report.
-}
mkReport
  :: String              -- ^ File path
  -> Maybe String        -- ^ Module name
  -> Maybe String        -- ^ Revision
  -> String              -- ^ Timestamp
  -> StageResult         -- ^ Parse result
  -> StageResult         -- ^ Elaboration result
  -> StageResult         -- ^ Type check result
  -> StageResult         -- ^ Proof check result
  -> StageResult         -- ^ Code gen result
  -> VerificationReport
mkReport file modName rev ts pr er tr pcr cg =
  let stages = [pr, er, tr, pcr, cg]
      verdict = if all isSuccess stages then Accept else Reject
      totalDuration = sum [stageDuration s | s <- stages]
  in VerificationReport
       { vrFile = file
       , vrModule = modName
       , vrRevision = rev
       , vrTimestamp = ts
       , vrParseResult = pr
       , vrElaborationResult = er
       , vrTypeCheckResult = tr
       , vrProofCheckResult = pcr
       , vrCodeGenResult = cg
       , vrVerdict = verdict
       , vrTotalDuration = totalDuration
       , vrAdditionalErrors = []
       }

-- ============================================================================
-- QUERY FUNCTIONS
-- ============================================================================

{-| Check if a stage result is successful.
-}
isSuccess :: StageResult -> Bool
isSuccess StageOK{} = True
isSuccess StageFailed{} = False

{-| Check if all stages in a report were successful.
-}
allStagesSuccessful :: VerificationReport -> Bool
allStagesSuccessful vr =
  all isSuccess
    [ vrParseResult vr
    , vrElaborationResult vr
    , vrTypeCheckResult vr
    , vrProofCheckResult vr
    , vrCodeGenResult vr
    ]

{-| Get the duration of a stage result.
-}
stageDuration :: StageResult -> Double
stageDuration StageOK{srDuration=d} = d
stageDuration StageFailed{srDuration=d} = d

{-| Get stage name.
-}
stageName :: StageResult -> String
stageName StageOK{srStageName=n} = n
stageName StageFailed{srStageName=n} = n

{-| Convert report to list of stages.
-}
stagesToList :: VerificationReport -> [StageResult]
stagesToList vr =
  [ vrParseResult vr
  , vrElaborationResult vr
  , vrTypeCheckResult vr
  , vrProofCheckResult vr
  , vrCodeGenResult vr
  ]

-- ============================================================================
-- SERIALIZATION: JSON
-- ============================================================================

{-| Serialize report to JSON format.
Deterministic ordering ensures identical input produces identical JSON.
-}
toJSON :: VerificationReport -> String
toJSON vr =
  "{\n"
  ++ "  \"file\": \"" ++ escapeJSON (vrFile vr) ++ "\",\n"
  ++ "  \"module\": " ++ maybe "null" (\m -> "\"" ++ escapeJSON m ++ "\"") (vrModule vr) ++ ",\n"
  ++ "  \"revision\": " ++ maybe "null" (\r -> "\"" ++ escapeJSON r ++ "\"") (vrRevision vr) ++ ",\n"
  ++ "  \"timestamp\": \"" ++ escapeJSON (vrTimestamp vr) ++ "\",\n"
  ++ "  \"verdict\": \"" ++ show (vrVerdict vr) ++ "\",\n"
  ++ "  \"totalDuration\": " ++ show (vrTotalDuration vr) ++ ",\n"
  ++ "  \"stages\": [\n"
  ++ intercalate ",\n" (map stageToJSON (stagesToList vr))
  ++ "\n  ],\n"
  ++ "  \"additionalErrors\": [\n"
  ++ intercalate ",\n" (map errorToJSON (vrAdditionalErrors vr))
  ++ "\n  ]\n"
  ++ "}"

{-| Serialize a stage result to JSON.
-}
stageToJSON :: StageResult -> String
stageToJSON (StageOK name duration) =
  "    {\n"
  ++ "      \"name\": \"" ++ escapeJSON name ++ "\",\n"
  ++ "      \"status\": \"OK\",\n"
  ++ "      \"duration\": " ++ show duration ++ "\n"
  ++ "    }"
stageToJSON (StageFailed name duration err) =
  "    {\n"
  ++ "      \"name\": \"" ++ escapeJSON name ++ "\",\n"
  ++ "      \"status\": \"FAILED\",\n"
  ++ "      \"duration\": " ++ show duration ++ ",\n"
  ++ "      \"error\": " ++ errorToJSON err ++ "\n"
  ++ "    }"

{-| Serialize an error to JSON.
-}
errorToJSON :: ErrorDetail -> String
errorToJSON err =
  "{\n"
  ++ "        \"category\": \"" ++ show (edCategory err) ++ "\",\n"
  ++ "        \"message\": \"" ++ escapeJSON (edMessage err) ++ "\",\n"
  ++ "        \"location\": " ++ locationToJSON (edLocation err) ++ ",\n"
  ++ "        \"context\": " ++ maybe "null" (\c -> "\"" ++ escapeJSON c ++ "\"") (edContext err) ++ ",\n"
  ++ "        \"suggestedFix\": " ++ maybe "null" (\f -> "\"" ++ escapeJSON f ++ "\"") (edSuggestedFix err) ++ "\n"
  ++ "      }"

{-| Serialize source location to JSON.
-}
locationToJSON :: Maybe SourceLocation -> String
locationToJSON Nothing = "null"
locationToJSON (Just sl) =
  "{\n"
  ++ "          \"file\": \"" ++ escapeJSON (slFile sl) ++ "\",\n"
  ++ "          \"line\": " ++ show (slLine sl) ++ ",\n"
  ++ "          \"column\": " ++ show (slColumn sl) ++ "\n"
  ++ "        }"

{-| Escape special JSON characters.
-}
escapeJSON :: String -> String
escapeJSON = concatMap escapeChar
  where
    escapeChar '"' = "\\\""
    escapeChar '\\' = "\\\\"
    escapeChar '\n' = "\\n"
    escapeChar '\r' = "\\r"
    escapeChar '\t' = "\\t"
    escapeChar c = [c]

-- ============================================================================
-- SERIALIZATION: HUMAN-READABLE TEXT
-- ============================================================================

{-| Serialize report to human-readable text format.
-}
toHumanReadable :: VerificationReport -> String
toHumanReadable vr =
  unlines
    [ "=========================================="
    , "VERIFICATION REPORT"
    , "=========================================="
    , ""
    , "File:      " ++ vrFile vr
    , "Module:    " ++ maybe "(none)" id (vrModule vr)
    , "Revision:  " ++ maybe "(unknown)" id (vrRevision vr)
    , "Timestamp: " ++ vrTimestamp vr
    , ""
    , "=========================================="
    , "VERIFICATION STAGES"
    , "=========================================="
    , ""
    , formatStages (stagesToList vr)
    , ""
    , "=========================================="
    , "FINAL VERDICT: " ++ show (vrVerdict vr)
    , "TOTAL TIME: " ++ show (vrTotalDuration vr) ++ " ms"
    , "=========================================="
    ] ++ (if null (vrAdditionalErrors vr) then "" else "\nADDITIONAL MESSAGES:\n" ++ formatErrors (vrAdditionalErrors vr))

{-| Format stages for human-readable output.
-}
formatStages :: [StageResult] -> String
formatStages = unlines . zipWith formatStage [1..]
  where
    formatStage i (StageOK name duration) =
      "  [" ++ show i ++ "] " ++ padTo 20 name ++ " : OK (" ++ show duration ++ " ms)"
    formatStage i (StageFailed name duration err) =
      "  [" ++ show i ++ "] " ++ padTo 20 name ++ " : FAILED (" ++ show duration ++ " ms)\n" ++
      "      Error: " ++ edMessage err ++ "\n" ++
      locString (edLocation err)

{-| Format errors for human-readable output.
-}
formatErrors :: [ErrorDetail] -> String
formatErrors = unlines . map formatError
  where
    formatError err =
      "  - [" ++ show (edCategory err) ++ "] " ++ edMessage err
      ++ locString (edLocation err)
      ++ case edSuggestedFix err of
           Just fix -> "\n    Suggestion: " ++ fix
           Nothing -> ""

{-| Format location string.
-}
locString :: Maybe SourceLocation -> String
locString Nothing = ""
locString (Just sl) =
  " (at " ++ slFile sl ++ ":" ++ show (slLine sl) ++ ":" ++ show (slColumn sl) ++ ")"

{-| Pad string to specified width.
-}
padTo :: Int -> String -> String
padTo n s = s ++ replicate (max 0 (n - length s)) ' '

-- ============================================================================
-- SERIALIZATION: CSV (for batch reporting)
-- ============================================================================

{-| Serialize report to CSV format (single row per file).
-}
toCSV :: VerificationReport -> String
toCSV vr =
  escapeCSV (vrFile vr) ++ ","
  ++ escapeCSV (maybe "" id (vrModule vr)) ++ ","
  ++ escapeCSV (maybe "" id (vrRevision vr)) ++ ","
  ++ show (vrVerdict vr) ++ ","
  ++ show (vrTotalDuration vr)

{-| CSV header for batch reports.
-}
csvHeader :: String
csvHeader = "File,Module,Revision,Verdict,Duration"

{-| Escape special CSV characters.
-}
escapeCSV :: String -> String
escapeCSV s
  | any (`elem` s) ",\"\n" = "\"" ++ concatMap escapeChar s ++ "\""
  | otherwise = s
  where
    escapeChar '"' = "\"\""
    escapeChar c = [c]

	{-# LANGUAGE DeriveGeneric #-}
	{-# LANGUAGE OverloadedStrings #-}

	{-\|
	Module : Assertica.Verify.Report
	Description : Verification report structures and serialization
	Copyright : (c) 2026 Ahmad Ali Parr
	License : BSL-1.0

	The VerificationReport captures the complete result of verifying a file or module,
	including the results at each pipeline stage, detailed errors, and the final verdict.

	DESIGN PRINCIPLES:
	1. Comprehensive: Captures all verification state at each stage
	2. Deterministic: Same input produces identical report
	3. Machine-readable: JSON serialization for CI consumption
	4. Human-readable: Clear text format with explanations
	5. Actionable: Every error includes source location and context
	-}

	module Assertica.Verify.Report
	( -- * Main report types
	VerificationReport (..)
	, StageResult (..)
	, Verdict (..)
	, SourceLocation (..)

	-- * Error types
	, ErrorDetail (..)
	, ErrorCategory (..)

	-- * Report builders and serialization
	, mkReport
	, mkStageResult
	, toJSON
	, toHumanReadable
	, toCSV

	-- * Utility functions
	, isSuccess
	, allStagesSuccessful
	, stagesToList
	) where

	import Data.Text (Text)
	import qualified Data.Text as T
	import Data.List (intercalate)
	import Data.Time (UTCTime)
	import GHC.Generics (Generic)
	import Data.Ord (comparing)

	-- ============================================================================
	-- SOURCE LOCATION
	-- ============================================================================

	{-\| Source location with file and line information.
	-}
	data SourceLocation = SourceLocation
	{ slFile :: String
	, slLine :: Int
	, slColumn :: Int
	}
	deriving (Eq, Show, Generic)

	-- ============================================================================
	-- ERROR TYPES
	-- ============================================================================

	{-\| Error category for classification.
	-}
	data ErrorCategory
	= SyntaxError -- ^ Parse failed (lexer/parser)
	\| TypeError -- ^ Type checker rejected
	\| ProofObligation -- ^ Proof missing or invalid
	\| ModuleError -- ^ Circular dependency, missing import
	\| TerminationError -- ^ Recursion not structurally decreasing
	\| PositivityError -- ^ Inductive type not strictly positive
	\| CodeGenError -- ^ Code generation failed
	\| UnknownError -- ^ Unexpected error
	deriving (Eq, Show, Ord, Generic)

	{-\| Detailed error information.
	-}
	data ErrorDetail = ErrorDetail
	{ edCategory :: ErrorCategory
	, edMessage :: String
	, edLocation :: Maybe SourceLocation
	, edContext :: Maybe String -- ^ Source code context
	, edSuggestedFix :: Maybe String -- ^ Fix suggestion
	}
	deriving (Eq, Show, Generic)

	-- ============================================================================
	-- STAGE RESULTS
	-- ============================================================================

	{-\| Result of a single verification stage.
	-}
	data StageResult
	= StageOK
	{ srStageName :: String
	, srDuration :: Double -- ^ Milliseconds
	}
	\| StageFailed
	{ srStageName :: String
	, srDuration :: Double
	, srError :: ErrorDetail
	}
	deriving (Eq, Show, Generic)

	-- ============================================================================
	-- FINAL VERDICT
	-- ============================================================================

	{-\| Final verification verdict.
	-}
	data Verdict
	= Accept -- ^ Module verified successfully
	\| Reject -- ^ Module failed verification
	deriving (Eq, Show, Ord, Generic)

	-- ============================================================================
	-- VERIFICATION REPORT
	-- ============================================================================

	{-\| Complete verification report for a file/module.
	-}
	data VerificationReport = VerificationReport
	{ vrFile :: String -- ^ Input file path
	, vrModule :: Maybe String -- ^ Module name (if applicable)
	, vrRevision :: Maybe String -- ^ Git revision or hash
	, vrTimestamp :: String -- ^ ISO 8601 timestamp
	, vrParseResult :: StageResult -- ^ Lexer/Parser stage
	, vrElaborationResult :: StageResult -- ^ Elaboration stage
	, vrTypeCheckResult :: StageResult -- ^ Type checking stage
	, vrProofCheckResult :: StageResult -- ^ Proof verification stage
	, vrCodeGenResult :: StageResult -- ^ Code generation stage
	, vrVerdict :: Verdict -- ^ Final verdict
	, vrTotalDuration :: Double -- ^ Total time in milliseconds
	, vrAdditionalErrors :: [ErrorDetail] -- ^ Non-fatal errors or warnings
	}
	deriving (Eq, Show, Generic)

	-- ============================================================================
	-- REPORT CONSTRUCTION
	-- ============================================================================

	{-\| Create a successful stage result.
	-}
	mkStageResult :: String -> Double -> StageResult
	mkStageResult name duration = StageOK name duration

	{-\| Create a failed stage result.
	-}
	mkFailedStageResult :: String -> Double -> ErrorDetail -> StageResult
	mkFailedStageResult name duration err = StageFailed name duration err

	{-\| Create a verification report.
	-}
	mkReport
	:: String -- ^ File path
	-> Maybe String -- ^ Module name
	-> Maybe String -- ^ Revision
	-> String -- ^ Timestamp
	-> StageResult -- ^ Parse result
	-> StageResult -- ^ Elaboration result
	-> StageResult -- ^ Type check result
	-> StageResult -- ^ Proof check result
	-> StageResult -- ^ Code gen result
	-> VerificationReport
	mkReport file modName rev ts pr er tr pcr cg =
	let stages = [pr, er, tr, pcr, cg]
	verdict = if all isSuccess stages then Accept else Reject
	totalDuration = sum [stageDuration s \| s <- stages]
	in VerificationReport
	{ vrFile = file
	, vrModule = modName
	, vrRevision = rev
	, vrTimestamp = ts
	, vrParseResult = pr
	, vrElaborationResult = er
	, vrTypeCheckResult = tr
	, vrProofCheckResult = pcr
	, vrCodeGenResult = cg
	, vrVerdict = verdict
	, vrTotalDuration = totalDuration
	, vrAdditionalErrors = []
	}

	-- ============================================================================
	-- QUERY FUNCTIONS
	-- ============================================================================

	{-\| Check if a stage result is successful.
	-}
	isSuccess :: StageResult -> Bool
	isSuccess StageOK{} = True
	isSuccess StageFailed{} = False

	{-\| Check if all stages in a report were successful.
	-}
	allStagesSuccessful :: VerificationReport -> Bool
	allStagesSuccessful vr =
	all isSuccess
	[ vrParseResult vr
	, vrElaborationResult vr
	, vrTypeCheckResult vr
	, vrProofCheckResult vr
	, vrCodeGenResult vr
	]

	{-\| Get the duration of a stage result.
	-}
	stageDuration :: StageResult -> Double
	stageDuration StageOK{srDuration=d} = d
	stageDuration StageFailed{srDuration=d} = d

	{-\| Get stage name.
	-}
	stageName :: StageResult -> String
	stageName StageOK{srStageName=n} = n
	stageName StageFailed{srStageName=n} = n

	{-\| Convert report to list of stages.
	-}
	stagesToList :: VerificationReport -> [StageResult]
	stagesToList vr =
	[ vrParseResult vr
	, vrElaborationResult vr
	, vrTypeCheckResult vr
	, vrProofCheckResult vr
	, vrCodeGenResult vr
	]

	-- ============================================================================
	-- SERIALIZATION: JSON
	-- ============================================================================

	{-\| Serialize report to JSON format.
	Deterministic ordering ensures identical input produces identical JSON.
	-}
	toJSON :: VerificationReport -> String
	toJSON vr =
	"{\n"
	++ " \"file\": \"" ++ escapeJSON (vrFile vr) ++ "\",\n"
	++ " \"module\": " ++ maybe "null" (\m -> "\"" ++ escapeJSON m ++ "\"") (vrModule vr) ++ ",\n"
	++ " \"revision\": " ++ maybe "null" (\r -> "\"" ++ escapeJSON r ++ "\"") (vrRevision vr) ++ ",\n"
	++ " \"timestamp\": \"" ++ escapeJSON (vrTimestamp vr) ++ "\",\n"
	++ " \"verdict\": \"" ++ show (vrVerdict vr) ++ "\",\n"
	++ " \"totalDuration\": " ++ show (vrTotalDuration vr) ++ ",\n"
	++ " \"stages\": [\n"
	++ intercalate ",\n" (map stageToJSON (stagesToList vr))
	++ "\n ],\n"
	++ " \"additionalErrors\": [\n"
	++ intercalate ",\n" (map errorToJSON (vrAdditionalErrors vr))
	++ "\n ]\n"
	++ "}"

	{-\| Serialize a stage result to JSON.
	-}
	stageToJSON :: StageResult -> String
	stageToJSON (StageOK name duration) =
	" {\n"
	++ " \"name\": \"" ++ escapeJSON name ++ "\",\n"
	++ " \"status\": \"OK\",\n"
	++ " \"duration\": " ++ show duration ++ "\n"
	++ " }"
	stageToJSON (StageFailed name duration err) =
	" {\n"
	++ " \"name\": \"" ++ escapeJSON name ++ "\",\n"
	++ " \"status\": \"FAILED\",\n"
	++ " \"duration\": " ++ show duration ++ ",\n"
	++ " \"error\": " ++ errorToJSON err ++ "\n"
	++ " }"

	{-\| Serialize an error to JSON.
	-}
	errorToJSON :: ErrorDetail -> String
	errorToJSON err =
	"{\n"
	++ " \"category\": \"" ++ show (edCategory err) ++ "\",\n"
	++ " \"message\": \"" ++ escapeJSON (edMessage err) ++ "\",\n"
	++ " \"location\": " ++ locationToJSON (edLocation err) ++ ",\n"
	++ " \"context\": " ++ maybe "null" (\c -> "\"" ++ escapeJSON c ++ "\"") (edContext err) ++ ",\n"
	++ " \"suggestedFix\": " ++ maybe "null" (\f -> "\"" ++ escapeJSON f ++ "\"") (edSuggestedFix err) ++ "\n"
	++ " }"

	{-\| Serialize source location to JSON.
	-}
	locationToJSON :: Maybe SourceLocation -> String
	locationToJSON Nothing = "null"
	locationToJSON (Just sl) =
	"{\n"
	++ " \"file\": \"" ++ escapeJSON (slFile sl) ++ "\",\n"
	++ " \"line\": " ++ show (slLine sl) ++ ",\n"
	++ " \"column\": " ++ show (slColumn sl) ++ "\n"
	++ " }"

	{-\| Escape special JSON characters.
	-}
	escapeJSON :: String -> String
	escapeJSON = concatMap escapeChar
	where
	escapeChar '"' = "\\\""
	escapeChar '\\' = "\\\\"
	escapeChar '\n' = "\\n"
	escapeChar '\r' = "\\r"
	escapeChar '\t' = "\\t"
	escapeChar c = [c]

	-- ============================================================================
	-- SERIALIZATION: HUMAN-READABLE TEXT
	-- ============================================================================

	{-\| Serialize report to human-readable text format.
	-}
	toHumanReadable :: VerificationReport -> String
	toHumanReadable vr =
	unlines
	[ "=========================================="
	, "VERIFICATION REPORT"
	, "=========================================="
	, ""
	, "File: " ++ vrFile vr
	, "Module: " ++ maybe "(none)" id (vrModule vr)
	, "Revision: " ++ maybe "(unknown)" id (vrRevision vr)
	, "Timestamp: " ++ vrTimestamp vr
	, ""
	, "=========================================="
	, "VERIFICATION STAGES"
	, "=========================================="
	, ""
	, formatStages (stagesToList vr)
	, ""
	, "=========================================="
	, "FINAL VERDICT: " ++ show (vrVerdict vr)
	, "TOTAL TIME: " ++ show (vrTotalDuration vr) ++ " ms"
	, "=========================================="
	] ++ (if null (vrAdditionalErrors vr) then "" else "\nADDITIONAL MESSAGES:\n" ++ formatErrors (vrAdditionalErrors vr))

	{-\| Format stages for human-readable output.
	-}
	formatStages :: [StageResult] -> String
	formatStages = unlines . zipWith formatStage [1..]
	where
	formatStage i (StageOK name duration) =
	" [" ++ show i ++ "] " ++ padTo 20 name ++ " : OK (" ++ show duration ++ " ms)"
	formatStage i (StageFailed name duration err) =
	" [" ++ show i ++ "] " ++ padTo 20 name ++ " : FAILED (" ++ show duration ++ " ms)\n" ++
	" Error: " ++ edMessage err ++ "\n" ++
	locString (edLocation err)

	{-\| Format errors for human-readable output.
	-}
	formatErrors :: [ErrorDetail] -> String
	formatErrors = unlines . map formatError
	where
	formatError err =
	" - [" ++ show (edCategory err) ++ "] " ++ edMessage err
	++ locString (edLocation err)
	++ case edSuggestedFix err of
	Just fix -> "\n Suggestion: " ++ fix
	Nothing -> ""

	{-\| Format location string.
	-}
	locString :: Maybe SourceLocation -> String
	locString Nothing = ""
	locString (Just sl) =
	" (at " ++ slFile sl ++ ":" ++ show (slLine sl) ++ ":" ++ show (slColumn sl) ++ ")"

	{-\| Pad string to specified width.
	-}
	padTo :: Int -> String -> String
	padTo n s = s ++ replicate (max 0 (n - length s)) ' '

	-- ============================================================================
	-- SERIALIZATION: CSV (for batch reporting)
	-- ============================================================================

	{-\| Serialize report to CSV format (single row per file).
	-}
	toCSV :: VerificationReport -> String
	toCSV vr =
	escapeCSV (vrFile vr) ++ ","
	++ escapeCSV (maybe "" id (vrModule vr)) ++ ","
	++ escapeCSV (maybe "" id (vrRevision vr)) ++ ","
	++ show (vrVerdict vr) ++ ","
	++ show (vrTotalDuration vr)

	{-\| CSV header for batch reports.
	-}
	csvHeader :: String
	csvHeader = "File,Module,Revision,Verdict,Duration"

	{-\| Escape special CSV characters.
	-}
	escapeCSV :: String -> String
	escapeCSV s
	\| any (`elem` s) ",\"\n" = "\"" ++ concatMap escapeChar s ++ "\""
	\| otherwise = s
	where
	escapeChar '"' = "\"\""
	escapeChar c = [c]