    ------------------------------------------------------------------------
    -- |
    -- Module      : What4.Expr.AppTheory
    -- Description : Identifying the solver theory required by a core expression
    -- Copyright   : (c) Galois, Inc 2016-2020
    -- License     : BSD3
    -- Maintainer  : Joe Hendrix <jhendrix@galois.com>
    -- Stability   : provisional
    ------------------------------------------------------------------------

    {-# LANGUAGE GADTs #-}
    module What4.Expr.AppTheory
      ( AppTheory(..)
      , quantTheory
      , appTheory
      , typeTheory
      ) where

    import           What4.Expr.App
    import           What4.BaseTypes
    import qualified What4.SemiRing as SR
    import qualified What4.Expr.WeightedSum as WSum

    -- | The theory that a symbol belongs to.
    data AppTheory
       = BoolTheory
       | LinearArithTheory
       | NonlinearArithTheory
       | ComputableArithTheory
       | BitvectorTheory
       | QuantifierTheory
       | StringTheory
       | FloatingPointTheory
       | ArrayTheory
       | StructTheory
         -- ^ Theory attributed to structs (equivalent to records in CVC4/CVC5/Z3, tuples in Yices)
       | FnTheory
         -- ^ Theory attributed application functions.
       deriving (AppTheory -> AppTheory -> Bool
    (AppTheory -> AppTheory -> Bool)
    -> (AppTheory -> AppTheory -> Bool) -> Eq AppTheory
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: AppTheory -> AppTheory -> Bool
    == :: AppTheory -> AppTheory -> Bool
    $c/= :: AppTheory -> AppTheory -> Bool
    /= :: AppTheory -> AppTheory -> Bool
    Eq, Eq AppTheory
    Eq AppTheory
    -> (AppTheory -> AppTheory -> Ordering)
    -> (AppTheory -> AppTheory -> Bool)
    -> (AppTheory -> AppTheory -> Bool)
    -> (AppTheory -> AppTheory -> Bool)
    -> (AppTheory -> AppTheory -> Bool)
    -> (AppTheory -> AppTheory -> AppTheory)
    -> (AppTheory -> AppTheory -> AppTheory)
    -> Ord AppTheory
    AppTheory -> AppTheory -> Bool
    AppTheory -> AppTheory -> Ordering
    AppTheory -> AppTheory -> AppTheory
    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 :: AppTheory -> AppTheory -> Ordering
    compare :: AppTheory -> AppTheory -> Ordering
    $c< :: AppTheory -> AppTheory -> Bool
    < :: AppTheory -> AppTheory -> Bool
    $c<= :: AppTheory -> AppTheory -> Bool
    <= :: AppTheory -> AppTheory -> Bool
    $c> :: AppTheory -> AppTheory -> Bool
    > :: AppTheory -> AppTheory -> Bool
    $c>= :: AppTheory -> AppTheory -> Bool
    >= :: AppTheory -> AppTheory -> Bool
    $cmax :: AppTheory -> AppTheory -> AppTheory
    max :: AppTheory -> AppTheory -> AppTheory
    $cmin :: AppTheory -> AppTheory -> AppTheory
    min :: AppTheory -> AppTheory -> AppTheory
    Ord)

    quantTheory :: NonceApp t (Expr t) tp -> AppTheory
    quantTheory :: forall t (tp :: BaseType). NonceApp t (Expr t) tp -> AppTheory
    quantTheory NonceApp t (Expr t) tp
    a0 =
      case NonceApp t (Expr t) tp
    a0 of
        Annotation BaseTypeRepr tp
    tpr Nonce t tp
    _ Expr t tp
    _ -> BaseTypeRepr tp -> AppTheory
    forall (tp :: BaseType). BaseTypeRepr tp -> AppTheory
    typeTheory BaseTypeRepr tp
    tpr
        Forall{} -> AppTheory
    QuantifierTheory
        Exists{} -> AppTheory
    QuantifierTheory
        ArrayFromFn{}   -> AppTheory
    FnTheory
        MapOverArrays{} -> AppTheory
    ArrayTheory
        ArrayTrueOnEntries{} -> AppTheory
    ArrayTheory
        FnApp{} -> AppTheory
    FnTheory

    typeTheory :: BaseTypeRepr tp -> AppTheory
    typeTheory :: forall (tp :: BaseType). BaseTypeRepr tp -> AppTheory
    typeTheory BaseTypeRepr tp
    tp = case BaseTypeRepr tp
    tp of
      BaseTypeRepr tp
    BaseBoolRepr      -> AppTheory
    BoolTheory
      BaseBVRepr NatRepr w
    _      -> AppTheory
    BitvectorTheory
      BaseTypeRepr tp
    BaseIntegerRepr   -> AppTheory
    LinearArithTheory
      BaseTypeRepr tp
    BaseRealRepr      -> AppTheory
    LinearArithTheory
      BaseFloatRepr FloatPrecisionRepr fpp
    _   -> AppTheory
    FloatingPointTheory
      BaseStringRepr{}  -> AppTheory
    StringTheory
      BaseTypeRepr tp
    BaseComplexRepr   -> AppTheory
    LinearArithTheory
      BaseStructRepr Assignment BaseTypeRepr ctx
    _  -> AppTheory
    StructTheory
      BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
    _ BaseTypeRepr xs
    _ -> AppTheory
    ArrayTheory

    appTheory :: App (Expr t) tp -> AppTheory
    appTheory :: forall t (tp :: BaseType). App (Expr t) tp -> AppTheory
    appTheory App (Expr t) tp
    a0 =
      case App (Expr t) tp
    a0 of
        ----------------------------
        -- Boolean operations

        BaseIte BaseTypeRepr tp
    tp Integer
    _ Expr t 'BaseBoolType
    _ Expr t tp
    _ Expr t tp
    _ -> BaseTypeRepr tp -> AppTheory
    forall (tp :: BaseType). BaseTypeRepr tp -> AppTheory
    typeTheory BaseTypeRepr tp
    tp
        BaseEq BaseTypeRepr tp1
    tp Expr t tp1
    _ Expr t tp1
    _ -> BaseTypeRepr tp1 -> AppTheory
    forall (tp :: BaseType). BaseTypeRepr tp -> AppTheory
    typeTheory BaseTypeRepr tp1
    tp

        NotPred{} -> AppTheory
    BoolTheory
        ConjPred{} -> AppTheory
    BoolTheory

        RealIsInteger{} -> AppTheory
    LinearArithTheory

        BVTestBit{} -> AppTheory
    BitvectorTheory
        BVSlt{} -> AppTheory
    BitvectorTheory
        BVUlt{} -> AppTheory
    BitvectorTheory
        BVOrBits{} -> AppTheory
    BitvectorTheory

        ----------------------------
        -- Semiring operations
        SemiRingProd SemiRingProduct (Expr t) sr
    pd ->
          case SemiRingProduct (Expr t) sr -> SemiRingRepr sr
    forall (f :: BaseType -> Type) (sr :: SemiRing).
    SemiRingProduct f sr -> SemiRingRepr sr
    WSum.prodRepr SemiRingProduct (Expr t) sr
    pd of
            SR.SemiRingBVRepr BVFlavorRepr fv
    _ NatRepr w
    _ -> AppTheory
    BitvectorTheory
            SemiRingRepr sr
    SR.SemiRingIntegerRepr -> AppTheory
    NonlinearArithTheory
            SemiRingRepr sr
    SR.SemiRingRealRepr -> AppTheory
    NonlinearArithTheory

        SemiRingSum WeightedSum (Expr t) sr
    sm ->
          case WeightedSum (Expr t) sr -> SemiRingRepr sr
    forall (f :: BaseType -> Type) (sr :: SemiRing).
    WeightedSum f sr -> SemiRingRepr sr
    WSum.sumRepr WeightedSum (Expr t) sr
    sm of
            SR.SemiRingBVRepr BVFlavorRepr fv
    _ NatRepr w
    _ -> AppTheory
    BitvectorTheory
            SemiRingRepr sr
    SR.SemiRingIntegerRepr -> AppTheory
    LinearArithTheory
            SemiRingRepr sr
    SR.SemiRingRealRepr -> AppTheory
    LinearArithTheory

        SemiRingLe{} -> AppTheory
    LinearArithTheory

        ----------------------------
        -- Integer operations

        IntMod Expr t 'BaseIntegerType
    _ SemiRingLiteral{} -> AppTheory
    LinearArithTheory
        IntMod{} -> AppTheory
    NonlinearArithTheory

        IntDiv Expr t 'BaseIntegerType
    _ SemiRingLiteral{} -> AppTheory
    LinearArithTheory
        IntDiv{} -> AppTheory
    NonlinearArithTheory

        IntAbs{} -> AppTheory
    LinearArithTheory
        IntDivisible{} -> AppTheory
    LinearArithTheory

        ----------------------------
        -- Real operations

        RealDiv{} -> AppTheory
    NonlinearArithTheory
        RealSqrt{} -> AppTheory
    NonlinearArithTheory

        ----------------------------
        -- Computable number operations
        RealSpecialFunction{} -> AppTheory
    ComputableArithTheory

        ----------------------------
        -- Bitvector operations
        BVUnaryTerm{} -> AppTheory
    BoolTheory
        BVConcat{} -> AppTheory
    BitvectorTheory
        BVSelect{} -> AppTheory
    BitvectorTheory
        BVUdiv{} -> AppTheory
    BitvectorTheory
        BVUrem{} -> AppTheory
    BitvectorTheory
        BVSdiv{} -> AppTheory
    BitvectorTheory
        BVSrem{} -> AppTheory
    BitvectorTheory
        BVShl{}   -> AppTheory
    BitvectorTheory
        BVLshr{}  -> AppTheory
    BitvectorTheory
        BVRol{}   -> AppTheory
    BitvectorTheory
        BVRor{}   -> AppTheory
    BitvectorTheory
        BVAshr{}  -> AppTheory
    BitvectorTheory
        BVZext{}  -> AppTheory
    BitvectorTheory
        BVSext{}  -> AppTheory
    BitvectorTheory
        BVPopcount{} -> AppTheory
    BitvectorTheory
        BVCountLeadingZeros{} -> AppTheory
    BitvectorTheory
        BVCountTrailingZeros{} -> AppTheory
    BitvectorTheory
        BVFill{} -> AppTheory
    BitvectorTheory

        ----------------------------
        -- Float operations

        FloatNeg{}        -> AppTheory
    FloatingPointTheory
        FloatAbs{}        -> AppTheory
    FloatingPointTheory
        FloatSqrt{}       -> AppTheory
    FloatingPointTheory
        FloatAdd{}        -> AppTheory
    FloatingPointTheory
        FloatSub{}        -> AppTheory
    FloatingPointTheory
        FloatMul{}        -> AppTheory
    FloatingPointTheory
        FloatDiv{}        -> AppTheory
    FloatingPointTheory
        FloatRem{}        -> AppTheory
    FloatingPointTheory
        FloatFMA{}        -> AppTheory
    FloatingPointTheory
        FloatFpEq{}       -> AppTheory
    FloatingPointTheory
        FloatLe{}         -> AppTheory
    FloatingPointTheory
        FloatLt{}         -> AppTheory
    FloatingPointTheory
        FloatIsNaN{}      -> AppTheory
    FloatingPointTheory
        FloatIsInf{}      -> AppTheory
    FloatingPointTheory
        FloatIsZero{}     -> AppTheory
    FloatingPointTheory
        FloatIsPos{}      -> AppTheory
    FloatingPointTheory
        FloatIsNeg{}      -> AppTheory
    FloatingPointTheory
        FloatIsSubnorm{}  -> AppTheory
    FloatingPointTheory
        FloatIsNorm{}     -> AppTheory
    FloatingPointTheory
        FloatCast{}       -> AppTheory
    FloatingPointTheory
        FloatRound{}      -> AppTheory
    FloatingPointTheory
        FloatFromBinary{} -> AppTheory
    FloatingPointTheory
        FloatToBinary{}   -> AppTheory
    FloatingPointTheory
        BVToFloat{}       -> AppTheory
    FloatingPointTheory
        SBVToFloat{}      -> AppTheory
    FloatingPointTheory
        RealToFloat{}     -> AppTheory
    FloatingPointTheory
        FloatToBV{}       -> AppTheory
    FloatingPointTheory
        FloatToSBV{}      -> AppTheory
    FloatingPointTheory
        FloatToReal{}     -> AppTheory
    FloatingPointTheory

        FloatSpecialFunction{} -> AppTheory
    ComputableArithTheory -- TODO? is this right?

        --------------------------------
        -- Conversions.

        IntegerToReal{} -> AppTheory
    LinearArithTheory
        BVToInteger{}   -> AppTheory
    LinearArithTheory
        SBVToInteger{}  -> AppTheory
    LinearArithTheory

        RoundReal{} -> AppTheory
    LinearArithTheory
        RoundEvenReal{} -> AppTheory
    LinearArithTheory
        FloorReal{} -> AppTheory
    LinearArithTheory
        CeilReal{}  -> AppTheory
    LinearArithTheory
        RealToInteger{} -> AppTheory
    LinearArithTheory

        IntegerToBV{}  -> AppTheory
    BitvectorTheory

        ---------------------
        -- Array operations

        ArrayMap{} -> AppTheory
    ArrayTheory
        ConstantArray{} -> AppTheory
    ArrayTheory
        SelectArray{} -> AppTheory
    ArrayTheory
        UpdateArray{} -> AppTheory
    ArrayTheory
        CopyArray{} -> AppTheory
    ArrayTheory
        SetArray{} -> AppTheory
    ArrayTheory
        EqualArrayRange{} -> AppTheory
    ArrayTheory

        ---------------------
        -- String operations
        StringAppend{} -> AppTheory
    StringTheory
        StringLength{} -> AppTheory
    StringTheory
        StringContains{} -> AppTheory
    StringTheory
        StringIndexOf{} -> AppTheory
    StringTheory
        StringIsPrefixOf{} -> AppTheory
    StringTheory
        StringIsSuffixOf{} -> AppTheory
    StringTheory
        StringSubstring{} -> AppTheory
    StringTheory

        ---------------------
        -- Complex operations

        Cplx{} -> AppTheory
    LinearArithTheory
        RealPart{} -> AppTheory
    LinearArithTheory
        ImagPart{} -> AppTheory
    LinearArithTheory

        ---------------------
        -- Struct operations

        -- A struct with its fields.
        StructCtor{}  -> AppTheory
    StructTheory
        StructField{} -> AppTheory
    StructTheory