{-# Language DeriveFunctor, RankNTypes, ConstraintKinds, TypeFamilies, ScopedTypeVariables, GADTs #-}
module Crux.Types where

import           Data.Functor.Const
import           Data.Parameterized.Map (MapF)
import           Data.Sequence (Seq)
import           Data.Text ( Text )
import           Data.Void
import           Prettyprinter

import           What4.Expr (GroundValue,GroundValueWrapper)
import           What4.Interface (Pred)
import           What4.ProgramLoc

import           Lang.Crucible.Backend
import           Lang.Crucible.Simulator
import           Lang.Crucible.Types

-- | A simulator context
type SimCtxt personality sym p = SimContext (personality sym) sym p

-- | The instance of the override monad we use,
-- when we don't care about the context of the surrounding function.
type OverM personality sym ext a =
  forall r args ret.
  OverrideSim
    (personality sym)  -- Extra data available in overrides (frontend-specific)
    sym                -- The symbolic backend (usually a what4 ExprBuilder in some form)
    ext                -- The Crucible syntax extension for the target language
    r
    args
    ret
    a

-- | This is the instance of the 'OverrideSim' monad that we use.
type Fun personality sym ext args ret =
  forall r.
  OverrideSim
    (personality sym)
    sym                                    -- the backend
    ext
    r
    args
    ret
    (RegValue sym ret)

data Result personality sym where
  Result :: (ExecResult (personality sym) sym ext (RegEntry sym UnitType)) -> Result personality sym


data ProcessedGoals =
  ProcessedGoals { ProcessedGoals -> Integer
totalProcessedGoals :: !Integer
                 , ProcessedGoals -> Integer
provedGoals :: !Integer
                 , ProcessedGoals -> Integer
disprovedGoals :: !Integer
                 , ProcessedGoals -> Integer
incompleteGoals :: !Integer
                 }

data ProofResult sym
   = Proved [Either (Assumption sym) (Assertion sym)]
   | NotProved (Doc Void) (Maybe (ModelView, [CrucibleEvent GroundValueWrapper])) [String]
     -- ^ The first argument is an explanation of the failure and
     -- counter example as provided by the Explainer (if any), the
     -- second maybe a model for the counter-example, and the third 
     -- is a list of abducts provided which may be empty

type LPred sym   = LabeledPred (Pred sym)

data ProvedGoals
  = Branch ProvedGoals ProvedGoals
  | NotProvedGoal
         [CrucibleAssumption (Const ())]
         SimError
         (Doc Void)
         [ProgramLoc]
         (Maybe (ModelView, [CrucibleEvent GroundValueWrapper]))
         [String]
  | ProvedGoal
         [CrucibleAssumption (Const ())]
         SimError
         [ProgramLoc]
         Bool
    -- ^ Keeps only the explanations for the relevant assumptions.
    --
    --   * The array of (AssumptionReason,String) is the set of
    --     assumptions for this Goal.
    --
    --   * The (SimError,String) is information about the failure,
    --     with the specific SimError (Lang.Crucible.Simulator) and a
    --     string representation of the Crucible term that encountered
    --     the error.
    --
    --   * The 'Bool' (third argument) indicates if the goal is
    --     trivial (i.e., the assumptions are inconsistent)


data ProgramCompleteness
 = ProgramComplete
 | ProgramIncomplete
 deriving (ProgramCompleteness -> ProgramCompleteness -> Bool
(ProgramCompleteness -> ProgramCompleteness -> Bool)
-> (ProgramCompleteness -> ProgramCompleteness -> Bool)
-> Eq ProgramCompleteness
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ProgramCompleteness -> ProgramCompleteness -> Bool
== :: ProgramCompleteness -> ProgramCompleteness -> Bool
$c/= :: ProgramCompleteness -> ProgramCompleteness -> Bool
/= :: ProgramCompleteness -> ProgramCompleteness -> Bool
Eq,Eq ProgramCompleteness
Eq ProgramCompleteness =>
(ProgramCompleteness -> ProgramCompleteness -> Ordering)
-> (ProgramCompleteness -> ProgramCompleteness -> Bool)
-> (ProgramCompleteness -> ProgramCompleteness -> Bool)
-> (ProgramCompleteness -> ProgramCompleteness -> Bool)
-> (ProgramCompleteness -> ProgramCompleteness -> Bool)
-> (ProgramCompleteness
    -> ProgramCompleteness -> ProgramCompleteness)
-> (ProgramCompleteness
    -> ProgramCompleteness -> ProgramCompleteness)
-> Ord ProgramCompleteness
ProgramCompleteness -> ProgramCompleteness -> Bool
ProgramCompleteness -> ProgramCompleteness -> Ordering
ProgramCompleteness -> ProgramCompleteness -> ProgramCompleteness
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ProgramCompleteness -> ProgramCompleteness -> Ordering
compare :: ProgramCompleteness -> ProgramCompleteness -> Ordering
$c< :: ProgramCompleteness -> ProgramCompleteness -> Bool
< :: ProgramCompleteness -> ProgramCompleteness -> Bool
$c<= :: ProgramCompleteness -> ProgramCompleteness -> Bool
<= :: ProgramCompleteness -> ProgramCompleteness -> Bool
$c> :: ProgramCompleteness -> ProgramCompleteness -> Bool
> :: ProgramCompleteness -> ProgramCompleteness -> Bool
$c>= :: ProgramCompleteness -> ProgramCompleteness -> Bool
>= :: ProgramCompleteness -> ProgramCompleteness -> Bool
$cmax :: ProgramCompleteness -> ProgramCompleteness -> ProgramCompleteness
max :: ProgramCompleteness -> ProgramCompleteness -> ProgramCompleteness
$cmin :: ProgramCompleteness -> ProgramCompleteness -> ProgramCompleteness
min :: ProgramCompleteness -> ProgramCompleteness -> ProgramCompleteness
Ord,Int -> ProgramCompleteness -> ShowS
[ProgramCompleteness] -> ShowS
ProgramCompleteness -> String
(Int -> ProgramCompleteness -> ShowS)
-> (ProgramCompleteness -> String)
-> ([ProgramCompleteness] -> ShowS)
-> Show ProgramCompleteness
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ProgramCompleteness -> ShowS
showsPrec :: Int -> ProgramCompleteness -> ShowS
$cshow :: ProgramCompleteness -> String
show :: ProgramCompleteness -> String
$cshowList :: [ProgramCompleteness] -> ShowS
showList :: [ProgramCompleteness] -> ShowS
Show)



data CruxSimulationResult =
  CruxSimulationResult
  { CruxSimulationResult -> ProgramCompleteness
cruxSimResultCompleteness :: ProgramCompleteness
  , CruxSimulationResult -> Seq (ProcessedGoals, ProvedGoals)
cruxSimResultGoals        :: Seq (ProcessedGoals, ProvedGoals)
  }


-- | A dummy datatype that can be used for the "personality"
--   type parameter.
data Crux sym = CruxPersonality


-- | A list of named GroundValues of the same type (used to
-- report SMT models in a portable way -- see the ModelView
-- datatype).
newtype Vals ty     = Vals [ Entry (GroundValue ty) ]

-- | A named value of type @a@ with a program
-- location. Used to describe and report models from SMT
-- queries (see Model and ModelView datatypes).
data Entry a        = Entry { forall a. Entry a -> String
entryName :: String
                            , forall a. Entry a -> ProgramLoc
entryLoc :: ProgramLoc
                            , forall a. Entry a -> a
entryValue :: a
                            }

-- | A portable/concrete view of a model's contents, organized by
-- crucible type. I.e., each crucible type is associated
-- with the list of entries (i.e. named GroundValues) at
-- that type for the given model, used to describe the
-- conditions under which an SMT query is satisfiable.
newtype ModelView = ModelView { ModelView -> MapF BaseTypeRepr Vals
modelVals :: MapF BaseTypeRepr Vals }

----------------------------------------------------------------------
-- Various things that can be logged/output

-- | Specify some general text that should be presented (to the user).
data SayWhat = SayWhat SayLevel Text Text  -- ^ fields are: Level From Message
             | SayMore SayWhat SayWhat
             | SayNothing

-- | Specify the verbosity/severity level of a message.  These are in
-- ordinal order for possible filtering, and higher levels may be sent
-- to a different location (e.g. stderr v.s. stdout).
data SayLevel = Noisily | Simply | OK | Warn | Fail deriving (SayLevel -> SayLevel -> Bool
(SayLevel -> SayLevel -> Bool)
-> (SayLevel -> SayLevel -> Bool) -> Eq SayLevel
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SayLevel -> SayLevel -> Bool
== :: SayLevel -> SayLevel -> Bool
$c/= :: SayLevel -> SayLevel -> Bool
/= :: SayLevel -> SayLevel -> Bool
Eq, Eq SayLevel
Eq SayLevel =>
(SayLevel -> SayLevel -> Ordering)
-> (SayLevel -> SayLevel -> Bool)
-> (SayLevel -> SayLevel -> Bool)
-> (SayLevel -> SayLevel -> Bool)
-> (SayLevel -> SayLevel -> Bool)
-> (SayLevel -> SayLevel -> SayLevel)
-> (SayLevel -> SayLevel -> SayLevel)
-> Ord SayLevel
SayLevel -> SayLevel -> Bool
SayLevel -> SayLevel -> Ordering
SayLevel -> SayLevel -> SayLevel
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SayLevel -> SayLevel -> Ordering
compare :: SayLevel -> SayLevel -> Ordering
$c< :: SayLevel -> SayLevel -> Bool
< :: SayLevel -> SayLevel -> Bool
$c<= :: SayLevel -> SayLevel -> Bool
<= :: SayLevel -> SayLevel -> Bool
$c> :: SayLevel -> SayLevel -> Bool
> :: SayLevel -> SayLevel -> Bool
$c>= :: SayLevel -> SayLevel -> Bool
>= :: SayLevel -> SayLevel -> Bool
$cmax :: SayLevel -> SayLevel -> SayLevel
max :: SayLevel -> SayLevel -> SayLevel
$cmin :: SayLevel -> SayLevel -> SayLevel
min :: SayLevel -> SayLevel -> SayLevel
Ord)