content: {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE RecordWildCards #-}
  {-# LANGUAGE UndecidableInstances #-}
  {-# OPTIONS_HADDOCK show-extensions #-}
  
  -- |
  -- Module      :  Language.Spectacle.Model.ModelError
  -- Copyright   :  (c) Arista Networks, 2022-2023
  -- License     :  Apache License 2.0, see LICENSE
  --
  -- Stability   :  stable
  -- Portability :  non-portable (GHC extensions)
  --
  -- Model checker errors.
  --
  -- @since 1.0.0
  module Language.Spectacle.Model.ModelError
    ( -- * Model Errors
      ModelError (InitialError, RuntimeError, RefutedError),
  
      -- ** Pretty Printing
      ppModelError,
      ppInitialError,
      ppRuntimeError,
  
      -- * Property Errors
      TemporalError (TemporalError),
      errorModality,
      errorPropName,
      errorPrimes,
      errorPlains,
  
      -- ** Pretty Printing
      ppTemporalError,
    )
  where
  
  import Data.Kind (Type)
  import GHC.TypeLits (Symbol)
  import Prettyprinter (Doc, align, indent, line, viaShow, vsep, (<+>))
  import Prettyprinter.Render.Terminal (AnsiStyle)
  
  import Data.Type.Rec (Ascribe, HasDict)
  import Data.World (World, ppWorldListed)
  import Language.Spectacle.Exception.RuntimeException (RuntimeException)
  import Language.Spectacle.Specification.Prop (Modality, ppModality)
  
  -- ---------------------------------------------------------------------------------------------------------------------
  
  -- | 'TemporalError' captures information about a temporal property refutation.
  --
  -- @since 1.0.0
  data ModelError :: [Ascribe Symbol Type] -> Type where
    InitialError ::
      ModelError ctx
    RuntimeError ::
      RuntimeException ->
      ModelError ctx
    RefutedError ::
      TemporalError ctx ->
      ModelError ctx
  
  -- | @since 1.0.0
  deriving instance HasDict Show ctx => Show (ModelError ctx)
  
  ppModelError :: HasDict Show ctx => ModelError ctx -> Doc AnsiStyle
  ppModelError = \case
    InitialError -> ppInitialError
    RuntimeError exc -> ppRuntimeError exc
    RefutedError err -> ppTemporalError err
  
  ppInitialError :: Doc AnsiStyle
  ppInitialError = "no initial states resulted from evaluating the initial actions"
  
  ppRuntimeError :: RuntimeException -> Doc AnsiStyle
  ppRuntimeError exc = "runtime error:" <+> viaShow exc
  
  -- ---------------------------------------------------------------------------------------------------------------------
  
  -- | 'TemporalError' captures information about a temporal property refutation.
  --
  -- @since 1.0.0
  data TemporalError ctx = TemporalError
    { errorModality :: Modality
    , errorPropName :: String
    , errorPrimes :: Maybe (World ctx)
    , errorPlains :: Maybe (World ctx)
    }
  
  -- | @since 1.0.0
  deriving instance HasDict Show ctx => Show (TemporalError ctx)
  
  ppTemporalError :: HasDict Show ctx => TemporalError ctx -> Doc AnsiStyle
  ppTemporalError TemporalError {..} =
    "refuted property:"
      <+> ppModality errorModality
      <+> viaShow errorPropName
      <> line
      <> stateList
    where
      stateList =
        let plains = align . mappend "from: " . vsep . ppWorldListed <$> errorPlains
            primes = align . mappend "to: " . vsep . ppWorldListed <$> errorPrimes
            states = foldMap (maybe [] pure) [plains, primes]
         in vsep (map (indent 2 . mappend "* ") states)
  