content: -----------------------------------------------------------------------
  -- |
  -- Module           : Lang.Crucible.Simulator.SimError
  -- Description      : Data structure the execution state of the simulator
  -- Copyright        : (c) Galois, Inc 2014
  -- License          : BSD3
  -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
  -- Stability        : provisional
  ------------------------------------------------------------------------
  {-# LANGUAGE ConstraintKinds #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE DeriveDataTypeable #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  module Lang.Crucible.Simulator.SimError (
      SimErrorReason(..)
    , SimError(..)
    , simErrorReasonMsg
    , simErrorDetailsMsg
    , ppSimError
    ) where
  
  import GHC.Stack (CallStack)
  
  import Control.Exception
  import Data.String
  import Data.Typeable
  import Prettyprinter
  
  import What4.ProgramLoc
  
  ------------------------------------------------------------------------
  -- SimError
  
  -- | Class for exceptions generated by simulator.
  data SimErrorReason
     = GenericSimError !String
     | Unsupported !CallStack !String
        -- ^ We can't do that (yet?).  The call stack identifies where in the
        --   Haskell code the error occured.
     | ReadBeforeWriteSimError !String -- FIXME? include relevant data instead of a string?
     | AssertFailureSimError !String !String
       -- ^ An assertion failed. The first parameter is a short
       -- description. The second is a more detailed explanation.
     | ResourceExhausted String
        -- ^ A loop iteration count, or similar resource limit,
        --   was exceeded.
   deriving (Typeable)
  
  data SimError
     = SimError
     { simErrorLoc :: !ProgramLoc
     , simErrorReason :: !SimErrorReason
     }
   deriving (Typeable)
  
  simErrorReasonMsg :: SimErrorReason -> String
  simErrorReasonMsg (GenericSimError msg) = msg
  simErrorReasonMsg (Unsupported _ msg) = "Unsupported feature: " ++ msg
  simErrorReasonMsg (ReadBeforeWriteSimError msg) = msg
  simErrorReasonMsg (AssertFailureSimError msg _) = msg
  simErrorReasonMsg (ResourceExhausted msg) = "Resource exhausted: " ++ msg
  
  simErrorDetailsMsg :: SimErrorReason -> String
  simErrorDetailsMsg (AssertFailureSimError _ msg) = msg
  simErrorDetailsMsg (Unsupported stk _) = show stk
  simErrorDetailsMsg _ = ""
  
  instance IsString SimErrorReason where
    fromString = GenericSimError
  
  instance Show SimErrorReason where
    show = simErrorReasonMsg
  
  instance Show SimError where
    show = show . ppSimError
  
  ppSimError :: SimError -> Doc ann
  ppSimError er =
    vcat $ [ pretty (plSourceLoc loc) <> pretty ": error: in" <+> pretty (plFunction loc)
           , pretty (simErrorReasonMsg rsn)
           ] ++ if null details
                then []
                else [ pretty "Details:"
                     , indent 2 (vcat (pretty <$> lines details))
                     ]
   where loc = simErrorLoc er
         details = simErrorDetailsMsg rsn
         rsn = simErrorReason er
  
  instance Exception SimError
  