content: {- |
  Module           : Lang.Crucible.CFG.Expr
  Description      : Expression syntax definitions
  Copyright        : (c) Galois, Inc 2014-2016
  License          : BSD3
  Maintainer       : Joe Hendrix <jhendrix@galois.com>
  
  Define the syntax of Crucible expressions.  Expressions represent
  side-effect free computations that result in terms.  The same
  expression language is used both for registerized CFGs ("Lang.Crucible.CFG.Reg")
  and for the core SSA-form CFGs ("Lang.Crucible.CFG.Core").
  
  Evaluation of expressions is defined in module "Lang.Crucible.Simulator.Evaluation".
  -}
  
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE InstanceSigs #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE LambdaCase #-}
  {-# LANGUAGE PatternSynonyms #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TemplateHaskell #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE UndecidableInstances #-}
  
  -- This option is here because, without it, GHC takes an extremely
  -- long time (forever?) to compile this module with profiling enabled.
  -- The SpecConstr optimization appears to be the culprit, and this
  -- option disables it.  Perhaps we only need to disable this
  -- optimization on profiling builds?
  {-# OPTIONS_GHC -fno-spec-constr #-}
  
  module Lang.Crucible.CFG.Expr
    ( -- * App
      App(..)
    , mapApp
    , foldApp
    , traverseApp
    , pattern BoolEq
    , pattern IntEq
    , pattern RealEq
    , pattern BVEq
  
    , pattern BoolIte
    , pattern IntIte
    , pattern RealIte
    , pattern BVIte
      -- * Base terms
    , BaseTerm(..)
    , module Lang.Crucible.CFG.Extension
    , RoundingMode(..)
  
    , testVector
    , compareVector
    ) where
  
  import           Control.Monad.Identity
  import           Control.Monad.State.Strict
  import qualified Data.BitVector.Sized as BV
  import           Data.Kind (Type)
  import           Data.Vector (Vector)
  import           Numeric.Natural
  import           Prettyprinter
  import qualified Data.Vector as V
  import qualified GHC.Float as F
  
  import           Data.Parameterized.Classes
  import qualified Data.Parameterized.Context as Ctx
  import qualified Data.Parameterized.TH.GADT as U
  import           Data.Parameterized.TraversableFC
  
  import           What4.Interface (RoundingMode(..),StringLiteral(..), stringLiteralInfo)
  
  import           Lang.Crucible.CFG.Extension
  import           Lang.Crucible.FunctionHandle
  import           Lang.Crucible.Types
  import           Lang.Crucible.Utils.PrettyPrint
  import qualified Lang.Crucible.Utils.Structural as U
  
  ------------------------------------------------------------------------
  -- BaseTerm
  
  -- | Base terms represent the subset of expressions
  --   of base types, packaged together with a run-time
  --   representation of their type.
  data BaseTerm (f :: CrucibleType -> Type) tp
     = BaseTerm { baseTermType :: !(BaseTypeRepr tp)
                , baseTermVal  :: !(f (BaseToType tp))
                }
  
  instance TestEqualityFC BaseTerm where
    testEqualityFC testF (BaseTerm _ x) (BaseTerm _ y) = do
      Refl <- testF x y
      return Refl
  instance TestEquality f => TestEquality (BaseTerm f) where
    testEquality = testEqualityFC testEquality
  
  instance OrdFC BaseTerm where
    compareFC cmpF (BaseTerm _ x) (BaseTerm _ y) = do
      case cmpF x y of
        LTF -> LTF
        GTF -> GTF
        EQF -> EQF
  instance OrdF f => OrdF (BaseTerm f) where
    compareF = compareFC compareF
  
  instance FunctorFC BaseTerm where
    fmapFC = fmapFCDefault
  
  instance FoldableFC BaseTerm where
    foldMapFC = foldMapFCDefault
  
  instance TraversableFC BaseTerm where
    traverseFC f (BaseTerm tp x) = BaseTerm tp <$> f x
  
  ------------------------------------------------------------------------
  -- App
  
  -- | Equality on booleans
  pattern BoolEq :: () => (tp ~ BoolType) => f BoolType -> f BoolType -> App ext f tp
  pattern BoolEq x y = BaseIsEq BaseBoolRepr x y
  
  -- | Equality on integers
  pattern IntEq :: () => (tp ~ BoolType) => f IntegerType -> f IntegerType -> App ext f tp
  pattern IntEq x y = BaseIsEq BaseIntegerRepr x y
  
  -- | Equality on real numbers.
  pattern RealEq :: () => (tp ~ BoolType) => f RealValType -> f RealValType -> App ext f tp
  pattern RealEq x y = BaseIsEq BaseRealRepr x y
  
  -- | Equality on bitvectors
  pattern BVEq :: () => (1 <= w, tp ~ BoolType) => NatRepr w -> f (BVType w) -> f (BVType w) -> App ext f tp
  pattern BVEq w x y = BaseIsEq (BaseBVRepr w) x y
  
  
  -- | Return first or second value depending on condition.
  pattern BoolIte :: () => (tp ~ BoolType) => f BoolType -> f tp -> f tp -> App ext f tp
  pattern BoolIte c x y = BaseIte BaseBoolRepr c x y
  
  -- | Return first or second value depending on condition.
  pattern IntIte :: () => (tp ~ IntegerType) => f BoolType -> f tp -> f tp -> App ext f tp
  pattern IntIte c x y = BaseIte BaseIntegerRepr c x y
  
  -- | Return first or second number depending on condition.
  pattern RealIte :: () => (tp ~ RealValType) => f BoolType -> f tp -> f tp -> App ext f tp
  pattern RealIte c x y = BaseIte BaseRealRepr c x y
  
  -- | Return first or second value depending on condition.
  pattern BVIte :: () => (1 <= w, tp ~ BVType w) => f BoolType -> NatRepr w -> f tp -> f tp -> App ext f tp
  pattern BVIte c w x y = BaseIte (BaseBVRepr w) c x y
  
  -- | The main Crucible expression datastructure, defined as a
  -- multisorted algebra. Type @'App' ext f tp@ encodes the top-level
  -- application of a Crucible expression. The parameter @ext@ is used
  -- to indicate which syntax extension is being used via the
  -- @ExprExtension@ type family.  The type parameter @tp@ is a
  -- type index that indicates the Crucible type of the values denoted
  -- by the given expression form. Parameter @f@ is used everywhere a
  -- recursive sub-expression would go.  Uses of the 'App' type will
  -- tie the knot through this parameter.
  data App (ext :: Type) (f :: CrucibleType -> Type) (tp :: CrucibleType) where
  
    ----------------------------------------------------------------------
    -- Syntax Extension
  
    ExtensionApp :: !(ExprExtension ext f tp) -> App ext f tp
  
    ----------------------------------------------------------------------
    -- Polymorphic
  
    -- | Return true if two base types are equal.
    BaseIsEq :: !(BaseTypeRepr tp)
             -> !(f (BaseToType tp))
             -> !(f (BaseToType tp))
             -> App ext f BoolType
  
    -- | Select one or other
    BaseIte :: !(BaseTypeRepr tp)
            -> !(f BoolType)
            -> !(f (BaseToType tp))
            -> !(f (BaseToType tp))
            -> App ext f (BaseToType tp)
  
    ----------------------------------------------------------------------
    -- ()
  
    EmptyApp :: App ext f UnitType
  
    ----------------------------------------------------------------------
    -- Any
  
    -- Build an ANY type package.
    PackAny :: !(TypeRepr tp)
            -> !(f tp)
            -> App ext f AnyType
  
    -- Attempt to open an ANY type. Return the contained
    -- value if it has the given type; otherwise return Nothing.
    UnpackAny :: !(TypeRepr tp)
              -> !(f AnyType)
              -> App ext f (MaybeType tp)
  
    ---------------------------------------------------------------------
    -- Bool
  
    BoolLit :: !Bool -> App ext f BoolType
  
    Not :: !(f BoolType)
        -> App ext f BoolType
  
    And :: !(f BoolType)
        -> !(f BoolType)
        -> App ext f BoolType
    Or  :: !(f BoolType)
        -> !(f BoolType)
        -> App ext f BoolType
  
    -- Exclusive or of Boolean values.
    BoolXor :: !(f BoolType)
            -> !(f BoolType)
            -> App ext f BoolType
  
    ----------------------------------------------------------------------
    -- Nat
  
    -- @NatLit n@ returns the value n.
    NatLit :: !Natural -> App ext f NatType
    -- Equality for natural numbers
    NatEq :: !(f NatType) -> !(f NatType) -> App ext f BoolType
    -- If/Then/Else on natural numbers
    NatIte :: !(f BoolType) -> !(f NatType) -> !(f NatType) -> App ext f NatType
    -- Less than on natural numbers.
    NatLt :: !(f NatType) -> !(f NatType) -> App ext f BoolType
    -- Less than or equal on natural numbers.
    NatLe :: !(f NatType) -> !(f NatType) -> App ext f BoolType
    -- Add two natural numbers.
    NatAdd :: !(f NatType) -> !(f NatType) -> App ext f NatType
    -- @NatSub x y@ equals @x - y@.
    -- The result is undefined if the @x@ is less than @y@.
    NatSub :: !(f NatType) -> !(f NatType) -> App ext f NatType
    -- Multiply two natural numbers.
    NatMul :: !(f NatType) -> !(f NatType) -> App ext f NatType
    -- Divide two natural numbers.  Undefined if the divisor is 0.
    NatDiv :: !(f NatType) -> !(f NatType) -> App ext f NatType
    -- Modular reduction on natural numbers. Undefined if the modulus is 0.
    NatMod :: !(f NatType) -> !(f NatType) -> App ext f NatType
  
    ----------------------------------------------------------------------
    -- Integer
  
    -- Create a singleton real array from a numeric literal.
    IntLit :: !Integer -> App ext f IntegerType
    -- Less-than test on integers
    IntLt :: !(f IntegerType) -> !(f IntegerType) -> App ext f BoolType
    -- Less-than-or-equal test on integers
    IntLe :: !(f IntegerType) -> !(f IntegerType) -> App ext f BoolType
    -- Negation of an integer value
    IntNeg :: !(f IntegerType) -> App ext f IntegerType
    -- Add two integers.
    IntAdd :: !(f IntegerType) -> !(f IntegerType) -> App ext f IntegerType
    -- Subtract one integer from another.
    IntSub :: !(f IntegerType) -> !(f IntegerType) -> App ext f IntegerType
    -- Multiply two integers.
    IntMul :: !(f IntegerType) -> !(f IntegerType) -> App ext f IntegerType
    -- Divide two integers.  Undefined if the divisor is 0.
    IntDiv :: !(f IntegerType) -> !(f IntegerType) -> App ext f IntegerType
    -- Modular reduction on integers.  Undefined if the modulus is 0.
    IntMod :: !(f IntegerType) -> !(f IntegerType) -> App ext f IntegerType
    -- Integer absolute value
    IntAbs :: !(f IntegerType) -> App ext f IntegerType
  
    ----------------------------------------------------------------------
    -- RealVal
  
    -- A real constant
    RationalLit :: !Rational -> App ext f RealValType
  
    RealLt :: !(f RealValType) -> !(f RealValType) -> App ext f BoolType
    RealLe :: !(f RealValType) -> !(f RealValType) -> App ext f BoolType
    -- Negate a real number
    RealNeg :: !(f RealValType) -> App ext f RealValType
    -- Add two natural numbers.
    RealAdd :: !(f RealValType) -> !(f RealValType) -> App ext f RealValType
    -- Subtract one number from another.
    RealSub :: !(f RealValType) -> !(f RealValType) -> App ext f RealValType
    -- Multiple two numbers.
    RealMul :: !(f RealValType) -> !(f RealValType) -> App ext f RealValType
    -- Divide two numbers.
    RealDiv :: !(f RealValType) -> !(f RealValType) -> App ext f RealValType
    -- Compute the "real modulus", which is @x - y * floor(x ./ y)@ when
    -- @y@ is not zero and @x@ when @y@ is zero.
    RealMod :: !(f RealValType) -> !(f RealValType) -> App ext f RealValType
  
    -- Return true if real value is integer.
    RealIsInteger :: !(f RealValType) -> App ext f BoolType
  
    ----------------------------------------------------------------------
    -- Float
  
    -- | Generate an "undefined" float value. The semantics of this construct are
    -- still under discussion, see crucible#366.
    FloatUndef :: !(FloatInfoRepr fi) -> App ext f (FloatType fi)
  
    -- Floating point constants
    FloatLit :: !Float -> App ext f (FloatType SingleFloat)
    DoubleLit :: !Double -> App ext f (FloatType DoubleFloat)
    X86_80Lit :: !X86_80Val -> App ext f (FloatType X86_80Float)
    FloatNaN :: !(FloatInfoRepr fi) -> App ext f (FloatType fi)
    FloatPInf :: !(FloatInfoRepr fi) -> App ext f (FloatType fi)
    FloatNInf :: !(FloatInfoRepr fi) -> App ext f (FloatType fi)
    FloatPZero :: !(FloatInfoRepr fi) -> App ext f (FloatType fi)
    FloatNZero :: !(FloatInfoRepr fi) -> App ext f (FloatType fi)
  
    -- Arithmetic operations
    FloatNeg
      :: !(FloatInfoRepr fi)
      -> !(f (FloatType fi))
      -> App ext f (FloatType fi)
    FloatAbs
      :: !(FloatInfoRepr fi)
      -> !(f (FloatType fi))
      -> App ext f (FloatType fi)
    FloatSqrt
      :: !(FloatInfoRepr fi)
      -> !RoundingMode
      -> !(f (FloatType fi))
      -> App ext f (FloatType fi)
  
    FloatAdd
      :: !(FloatInfoRepr fi)
      -> !RoundingMode
      -> !(f (FloatType fi))
      -> !(f (FloatType fi))
      -> App ext f (FloatType fi)
    FloatSub
      :: !(FloatInfoRepr fi)
      -> !RoundingMode
      -> !(f (FloatType fi))
      -> !(f (FloatType fi))
      -> App ext f (FloatType fi)
    FloatMul
      :: !(FloatInfoRepr fi)
      -> !RoundingMode
      -> !(f (FloatType fi))
      -> !(f (FloatType fi))
      -> App ext f (FloatType fi)
    FloatDiv
      :: !(FloatInfoRepr fi)
      -> !RoundingMode
      -> !(f (FloatType fi))
      -> !(f (FloatType fi))
      -> App ext f (FloatType fi)
    -- Foating-point remainder of the two operands
    FloatRem
      :: !(FloatInfoRepr fi)
      -> !(f (FloatType fi))
      -> !(f (FloatType fi))
      -> App ext f (FloatType fi)
    FloatMin
      :: !(FloatInfoRepr fi)
      -> !(f (FloatType fi))
      -> !(f (FloatType fi))
      -> App ext f (FloatType fi)
    FloatMax
      :: !(FloatInfoRepr fi)
      -> !(f (FloatType fi))
      -> !(f (FloatType fi))
      -> App ext f (FloatType fi)
    FloatFMA
      :: !(FloatInfoRepr fi)
      -> !RoundingMode
      -> !(f (FloatType fi))
      -> !(f (FloatType fi))
      -> !(f (FloatType fi))
      -> App ext f (FloatType fi)
  
    -- Comparison operations
    FloatEq :: !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f BoolType
    FloatFpEq :: !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f BoolType
    FloatGt :: !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f BoolType
    FloatGe :: !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f BoolType
    FloatLt :: !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f BoolType
    FloatLe :: !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f BoolType
    FloatNe :: !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f BoolType
    FloatFpApart :: !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f BoolType
  
    FloatIte
      :: !(FloatInfoRepr fi)
      -> !(f BoolType)
      -> !(f (FloatType fi))
      -> !(f (FloatType fi))
      -> App ext f (FloatType fi)
  
    -- Conversion operations
    FloatCast
      :: !(FloatInfoRepr fi)
      -> !RoundingMode
      -> !(f (FloatType fi'))
      -> App ext f (FloatType fi)
    FloatFromBinary
      :: !(FloatInfoRepr fi)
      -> !(f (BVType (FloatInfoToBitWidth fi)))
      -> App ext f (FloatType fi)
    FloatToBinary
      :: (1 <= FloatInfoToBitWidth fi)
      => !(FloatInfoRepr fi)
      -> !(f (FloatType fi))
      -> App ext f (BVType (FloatInfoToBitWidth fi))
    FloatFromBV
      :: (1 <= w)
      => !(FloatInfoRepr fi)
      -> !RoundingMode
      -> !(f (BVType w))
      -> App ext f (FloatType fi)
    FloatFromSBV
      :: (1 <= w)
      => !(FloatInfoRepr fi)
      -> !RoundingMode
      -> !(f (BVType w))
      -> App ext f (FloatType fi)
    FloatFromReal
      :: !(FloatInfoRepr fi)
      -> !RoundingMode
      -> !(f RealValType)
      -> App ext f (FloatType fi)
    FloatToBV
      :: (1 <= w)
      => !(NatRepr w)
      -> !RoundingMode
      -> !(f (FloatType fi))
      -> App ext f (BVType w)
    FloatToSBV
      :: (1 <= w)
      => !(NatRepr w)
      -> !RoundingMode
      -> !(f (FloatType fi))
      -> App ext f (BVType w)
    FloatToReal :: !(f (FloatType fi)) -> App ext f RealValType
  
    -- Classification operations
    FloatIsNaN :: !(f (FloatType fi)) -> App ext f BoolType
    FloatIsInfinite :: !(f (FloatType fi)) -> App ext f BoolType
    FloatIsZero :: !(f (FloatType fi)) -> App ext f BoolType
    FloatIsPositive :: !(f (FloatType fi)) -> App ext f BoolType
    FloatIsNegative :: !(f (FloatType fi)) -> App ext f BoolType
    FloatIsSubnormal :: !(f (FloatType fi)) -> App ext f BoolType
    FloatIsNormal :: !(f (FloatType fi)) -> App ext f BoolType
  
    ----------------------------------------------------------------------
    -- Maybe
  
    JustValue :: !(TypeRepr tp)
              -> !(f tp)
              -> App ext f (MaybeType tp)
  
    NothingValue :: !(TypeRepr tp) -> App ext f (MaybeType tp)
  
    -- This is a partial operation with given a maybe value returns the
    -- value if is defined and otherwise fails with the given error message.
    --
    -- This operation should be used instead of pattern matching on a maybe
    -- when you do not want an explicit error message being printed, but rather
    -- want to assert that the value is defined.
    FromJustValue :: !(TypeRepr tp)
                  -> !(f (MaybeType tp))
                  -> !(f (StringType Unicode))
                  -> App ext f tp
  
    ----------------------------------------------------------------------
    -- Recursive Types
    RollRecursive :: IsRecursiveType nm
                  => !(SymbolRepr nm)
                  -> !(CtxRepr ctx)
                  -> !(f (UnrollType nm ctx))
                  -> App ext f (RecursiveType nm ctx)
  
    UnrollRecursive
                  :: IsRecursiveType nm
                  => !(SymbolRepr nm)
                  -> !(CtxRepr ctx)
                  -> !(f (RecursiveType nm ctx))
                  -> App ext f (UnrollType nm ctx)
  
    ----------------------------------------------------------------------
    -- Sequences
  
    -- Create an empty sequence
    SequenceNil :: !(TypeRepr tp) -> App ext f (SequenceType tp)
  
    -- Add a new value to the front of a sequence
    SequenceCons :: !(TypeRepr tp)
                 -> !(f tp)
                 -> !(f (SequenceType tp))
                 -> App ext f (SequenceType tp)
  
    -- Append two sequences
    SequenceAppend :: !(TypeRepr tp)
                   -> !(f (SequenceType tp))
                   -> !(f (SequenceType tp))
                   -> App ext f (SequenceType tp)
  
    -- Test if a sequence is nil
    SequenceIsNil :: !(TypeRepr tp)
                  -> !(f (SequenceType tp))
                  -> App ext f BoolType
  
    -- Return the length of a sequence
    SequenceLength :: !(TypeRepr tp)
                   -> !(f (SequenceType tp))
                   -> App ext f NatType
  
    -- Return the head of a sesquence, if it is non-nil.
    SequenceHead :: !(TypeRepr tp)
                 -> !(f (SequenceType tp))
                 -> App ext f (MaybeType tp)
  
    -- Return the tail of a sequence, if it is non-nil.
    SequenceTail :: !(TypeRepr tp)
                 -> !(f (SequenceType tp))
                 -> App ext f (MaybeType (SequenceType tp))
  
    -- Deconstruct a sequence.  Return nothing if nil,
    -- return the head and tail if non-nil.
    SequenceUncons :: !(TypeRepr tp)
                   -> !(f (SequenceType tp))
                   -> App ext f (MaybeType (StructType (EmptyCtx ::> tp ::> SequenceType tp)))
  
    ----------------------------------------------------------------------
    -- Vector
  
    -- Vector literal.
    VectorLit :: !(TypeRepr tp) -> !(Vector (f tp)) -> App ext f (VectorType tp)
  
    -- Create an vector of constants.
    VectorReplicate :: !(TypeRepr tp)
                    -> !(f NatType)
                    -> !(f tp)
                    -> App ext f (VectorType tp)
  
    -- Return true if vector is empty.
    VectorIsEmpty :: !(f (VectorType tp))
                  -> App ext f BoolType
  
    -- Size of vector
    VectorSize :: !(f (VectorType tp)) -> App ext f NatType
  
    -- Return value stored in given entry.
    VectorGetEntry :: !(TypeRepr tp)
                   -> !(f (VectorType tp))
                   -> !(f NatType)
                   -> App ext f tp
  
    -- Update vector at given entry.
    VectorSetEntry :: !(TypeRepr tp)
                   -> !(f (VectorType tp))
                   -> !(f NatType)
                   -> !(f tp)
                   -> App ext f (VectorType tp)
  
    -- Cons an element onto the front of the vector
    VectorCons :: !(TypeRepr tp)
               -> !(f tp)
               -> !(f (VectorType tp))
               -> App ext f (VectorType tp)
  
    ----------------------------------------------------------------------
    -- Handle
  
    HandleLit :: !(FnHandle args ret)
              -> App ext f (FunctionHandleType args ret)
  
    -- Create a closure that captures the last argument.
    Closure :: !(CtxRepr args)
            -> !(TypeRepr ret)
            -> !(f (FunctionHandleType (args::>tp) ret))
            -> !(TypeRepr tp)
            -> !(f tp)
            -> App ext f (FunctionHandleType args ret)
  
    ----------------------------------------------------------------------
    -- Conversions
  
    -- @NatToInteger@ convert a natural number to an integer.
    NatToInteger :: !(f NatType) -> App ext f IntegerType
  
    -- @IntegerToReal@ convert an integer to a real.
    IntegerToReal :: !(f IntegerType) -> App ext f RealValType
  
    -- @RealRound@ rounds the real number value toward the nearest integer.
    -- Ties are rounded away from 0.
    RealRound :: !(f RealValType) -> App ext f IntegerType
  
    -- @RealRound@ computes the largest integer less-or-equal to the given real number.
    RealFloor :: !(f RealValType) -> App ext f IntegerType
  
    -- @RealCeil@ computes the smallest integer greater-or-equal to the given real number.
    RealCeil :: !(f RealValType) -> App ext f IntegerType
  
    -- @IntegerToBV@ converts an integer value to a bitvector.  This operations computes
    -- the unique bitvector whose value is congruent to the input value modulo @2^w@.
    IntegerToBV :: (1 <= w) => NatRepr w -> !(f IntegerType) -> App ext f (BVType w)
  
    -- @RealToNat@ convert a non-negative real integer to natural number.
    -- This is partial, and requires that the input be a non-negative real
    -- integer.
    RealToNat :: !(f RealValType) -> App ext f NatType
  
    ----------------------------------------------------------------------
    -- ComplexReal
  
    -- Create complex number from two real numbers.
    Complex :: !(f RealValType) -> !(f RealValType) -> App ext f ComplexRealType
    RealPart :: !(f ComplexRealType) -> App ext f RealValType
    ImagPart :: !(f ComplexRealType) -> App ext f RealValType
  
    ----------------------------------------------------------------------
    -- BV
  
    -- | Generate an "undefined" bitvector value. The semantics of this construct
    -- are still under discussion, see crucible#366.
    BVUndef :: (1 <= w) => NatRepr w -> App ext f (BVType w)
  
    BVLit :: (1 <= w) => NatRepr w -> BV.BV w -> App ext f (BVType w)
  
    -- concatenate two bitvectors
    BVConcat :: (1 <= u, 1 <= v, 1 <= u+v)
             => !(NatRepr u)
             -> !(NatRepr v)
             -> !(f (BVType u))       -- Most significant bits
             -> !(f (BVType v))       -- Least significant bits
             -> App ext f (BVType (u+v))
  
    -- BVSelect idx n bv chooses bits [idx, .. , idx+n-1] from bitvector bv.
    -- The resulting bitvector will have width n.
    -- Index 0 denotes the least-significant bit.
    BVSelect :: (1 <= w, 1 <= len, idx + len <= w)
             => !(NatRepr idx)
             -> !(NatRepr len)
             -> !(NatRepr w)
             -> !(f (BVType w))
             -> App ext f (BVType len)
  
    BVTrunc :: (1 <= r, r+1 <= w)
            => !(NatRepr r)
            -> !(NatRepr w)
            -> !(f (BVType w))
            -> App ext f (BVType r)
  
    BVZext :: (1 <= w, 1 <= r, w+1 <= r)
           => !(NatRepr r)
           -> !(NatRepr w)
           -> !(f (BVType w))
           -> App ext f (BVType r)
  
    BVSext :: (1 <= w, 1 <= r, w+1 <= r)
           => !(NatRepr r)
           -> !(NatRepr w)
           -> !(f (BVType w))
           -> App ext f (BVType r)
  
    -- Complement bits in bitvector.
    BVNot :: (1 <= w)
          => !(NatRepr w)
          -> !(f (BVType w))
          -> App ext f (BVType w)
  
    BVAnd :: (1 <= w)
          => !(NatRepr w)
          -> !(f (BVType w))
          -> !(f (BVType w))
          -> App ext f (BVType w)
  
    BVOr  :: (1 <= w)
          => !(NatRepr w)
          -> !(f (BVType w))
          -> !(f (BVType w))
          -> App ext f (BVType w)
  
    BVXor :: (1 <= w)
          => !(NatRepr w)
          -> !(f (BVType w))
          -> !(f (BVType w))
          -> App ext f (BVType w)
  
    BVNeg :: (1 <= w)
          => !(NatRepr w)
          -> !(f (BVType w))
          -> App ext f (BVType w)
  
    BVAdd :: (1 <= w)
          => !(NatRepr w)
          -> !(f (BVType w))
          -> !(f (BVType w))
          -> App ext f (BVType w)
  
    BVSub :: (1 <= w)
          => !(NatRepr w)
          -> !(f (BVType w))
          -> !(f (BVType w))
          -> App ext f (BVType w)
  
    BVMul :: (1 <= w)
          => !(NatRepr w)
          -> !(f (BVType w))
          -> !(f (BVType w))
          -> App ext f (BVType w)
  
    BVUdiv :: (1 <= w)
           => !(NatRepr w)
           -> !(f (BVType w))
           -> !(f (BVType w))
           -> App ext f (BVType w)
  
    -- | This performs signed division.  The result is truncated to zero.
    --
    -- TODO: Document semantics when divisor is zero and case of
    -- minSigned w / -1 = minSigned w.
    BVSdiv :: (1 <= w)
           => !(NatRepr w)
           -> !(f (BVType w))
           -> !(f (BVType w))
           -> App ext f (BVType w)
  
    BVUrem :: (1 <= w)
           => !(NatRepr w)
           -> !(f (BVType w))
           -> !(f (BVType w))
           -> App ext f (BVType w)
  
    BVSrem :: (1 <= w)
           => !(NatRepr w)
           -> !(f (BVType w))
           -> !(f (BVType w))
           -> App ext f (BVType w)
  
    BVUle :: (1 <= w)
          => !(NatRepr w)
          -> !(f (BVType w))
          -> !(f (BVType w))
          -> App ext f BoolType
  
    BVUlt :: (1 <= w)
          => !(NatRepr w)
          -> !(f (BVType w))
          -> !(f (BVType w))
          -> App ext f BoolType
  
    BVSle :: (1 <= w)
          => !(NatRepr w)
          -> !(f (BVType w))
          -> !(f (BVType w))
          -> App ext f BoolType
  
    BVSlt :: (1 <= w)
          => !(NatRepr w)
          -> !(f (BVType w))
          -> !(f (BVType w))
          -> App ext f BoolType
  
    -- True if the unsigned addition of the two given bitvectors
    -- has a carry-out; that is, if the unsigned addition overflows.
    BVCarry :: (1 <= w)
            => !(NatRepr w)
            -> !(f (BVType w))
            -> !(f (BVType w))
            -> App ext f BoolType
  
    -- True if the signed addition of the two given bitvectors
    -- has a signed overflow condition.
    BVSCarry :: (1 <= w)
             => !(NatRepr w)
             -> !(f (BVType w))
             -> !(f (BVType w))
             -> App ext f BoolType
  
    -- True if the signed subtraction of the two given bitvectors
    -- has a signed overflow condition.
    BVSBorrow :: (1 <= w)
              => !(NatRepr w)
              -> !(f (BVType w))
              -> !(f (BVType w))
              -> App ext f BoolType
  
    -- Perform a left-shift
    BVShl :: (1 <= w)
          => !(NatRepr w)
          -> !(f (BVType w)) -- Value to shift
          -> !(f (BVType w)) -- The shift amount as an unsigned integer.
          -> App ext f (BVType w)
  
    -- Perform a logical shift right
    BVLshr :: (1 <= w)
           => !(NatRepr w)
           -> !(f (BVType w)) -- Value to shift
           -> !(f (BVType w)) -- The shift amount as an unsigned integer.
           -> App ext f (BVType w)
  
    -- Perform a signed shift right (if the
    BVAshr :: (1 <= w)
           => !(NatRepr w)
           -> !(f (BVType w)) -- Value to shift
           -> !(f (BVType w)) -- The shift amount as an unsigned integer.
           -> App ext f (BVType w)
  
    -- Rotate left
    BVRol :: (1 <= w)
          => !(NatRepr w)
          -> !(f (BVType w)) -- Value to rotate
          -> !(f (BVType w)) -- The rotate amount as an unsigned integer
          -> App ext f (BVType w)
  
    -- Rotate right
    BVRor :: (1 <= w)
          => !(NatRepr w)
          -> !(f (BVType w)) -- Value to rotate
          -> !(f (BVType w)) -- The rotate amount as an unsigned integer
          -> App ext f (BVType w)
  
    -- Return the number of consecutive 0 bits in the input, starting from
    -- the most significant bit position.  If the input is zero, all bits are counted
    -- as leading.
    BVCountLeadingZeros :: (1 <= w)
          => !(NatRepr w)
          -> !(f (BVType w))
          -> App ext f (BVType w)
  
    -- Return the number of consecutive 0 bits in the input, starting from
    -- the least significant bit position.  If the input is zero, all bits are counted
    -- as trailing.
    BVCountTrailingZeros :: (1 <= w)
          => !(NatRepr w)
          -> !(f (BVType w))
          -> App ext f (BVType w)
  
    -- popcount
    BVPopcount :: (1 <= w)
          => !(NatRepr w)
          -> !(f (BVType w))
          -> App ext f (BVType w)
  
    -- Return the minimum of the two arguments using unsigned comparisons
    BVUMin ::
      (1 <= w) =>
      !(NatRepr w) ->
      !(f (BVType w)) ->
      !(f (BVType w)) ->
      App ext f (BVType w)
  
    -- Return the maximum of the two arguments using unsigned comparisons
    BVUMax ::
      (1 <= w) =>
      !(NatRepr w) ->
      !(f (BVType w)) ->
      !(f (BVType w)) ->
      App ext f (BVType w)
  
    -- Return the minimum of the two arguments using signed comparisons
    BVSMin ::
      (1 <= w) =>
      !(NatRepr w) ->
      !(f (BVType w)) ->
      !(f (BVType w)) ->
      App ext f (BVType w)
  
    -- Return the maximum of the two arguments using signed comparisons
    BVSMax ::
      (1 <= w) =>
      !(NatRepr w) ->
      !(f (BVType w)) ->
      !(f (BVType w)) ->
      App ext f (BVType w)
  
    -- Given a Boolean, returns one if Boolean is True and zero otherwise.
    BoolToBV :: (1 <= w)
             => !(NatRepr w)
             -> !(f BoolType)
             -> App ext f (BVType w)
  
    -- Return the unsigned value of the given bitvector as an integer
    BvToInteger :: (1 <= w)
                => !(NatRepr w)
                -> !(f (BVType w))
                -> App ext f IntegerType
  
    -- Return the signed value of the given bitvector as an integer
    SbvToInteger :: (1 <= w)
                 => !(NatRepr w)
                 -> !(f (BVType w))
                 -> App ext f IntegerType
  
    -- Return the unsigned value of the given bitvector as a nat
    BvToNat :: (1 <= w)
            => !(NatRepr w)
            -> !(f (BVType w))
            -> App ext f NatType
  
    BVNonzero :: (1 <= w)
              => !(NatRepr w)
              -> !(f (BVType w))
              -> App ext f BoolType
  
    ----------------------------------------------------------------------
    -- WordMap
  
    EmptyWordMap :: (1 <= w)
                 => !(NatRepr w)
                 -> !(BaseTypeRepr tp)
                 -> App ext f (WordMapType w tp)
  
    InsertWordMap :: (1 <= w)
                  => !(NatRepr w)
                  -> !(BaseTypeRepr tp)
                  -> !(f (BVType w))
                  -> !(f (BaseToType tp))
                  -> !(f (WordMapType w tp))
                  -> App ext f (WordMapType w tp)
  
    LookupWordMap :: (1 <= w)
                  => !(BaseTypeRepr tp)
                  -> !(f (BVType w))
                  -> !(f (WordMapType w tp))
                  -> App ext f (BaseToType tp)
  
    LookupWordMapWithDefault
                  :: (1 <= w)
                  => !(BaseTypeRepr tp)
                  -> !(f (BVType w))
                  -> !(f (WordMapType w tp))
                  -> !(f (BaseToType tp))
                  -> App ext f (BaseToType tp)
  
    ----------------------------------------------------------------------
    -- Variants
  
    InjectVariant :: !(CtxRepr ctx)
              -> !(Ctx.Index ctx tp)
              -> !(f tp)
              -> App ext f (VariantType ctx)
  
    ProjectVariant :: !(CtxRepr ctx)
                   -> !(Ctx.Index ctx tp)
                   -> !(f (VariantType ctx))
                   -> App ext f (MaybeType tp)
  
    ----------------------------------------------------------------------
    -- Struct
  
    MkStruct :: !(CtxRepr ctx)
             -> !(Ctx.Assignment f ctx)
             -> App ext f (StructType ctx)
  
    GetStruct :: !(f (StructType ctx))
              -> !(Ctx.Index ctx tp)
              -> !(TypeRepr tp)
              -> App ext f tp
  
    SetStruct :: !(CtxRepr ctx)
              -> !(f (StructType ctx))
              -> !(Ctx.Index ctx tp)
              -> !(f tp)
              -> App ext f (StructType ctx)
  
    ----------------------------------------------------------------------
    -- StringMapType
  
    -- Initialize the ident value map to the given value.
    EmptyStringMap :: !(TypeRepr tp)
                   -> App ext f (StringMapType tp)
  
    -- Lookup the value of a string in a string map.
    LookupStringMapEntry :: !(TypeRepr tp)
                         -> !(f (StringMapType tp))
                         -> !(f (StringType Unicode))
                         -> App ext f (MaybeType tp)
  
    -- Update the name of the ident value map with the given value.
    InsertStringMapEntry :: !(TypeRepr tp)
                         -> !(f (StringMapType tp))
                         -> !(f (StringType Unicode))
                         -> !(f (MaybeType tp))
                         -> App ext f (StringMapType tp)
  
    ----------------------------------------------------------------------
    -- String
  
    -- Create a concrete string literal
    StringLit :: !(StringLiteral si)
              -> App ext f (StringType si)
  
    -- Create an empty string literal
    StringEmpty :: !(StringInfoRepr si)
                -> App ext f (StringType si)
  
    StringConcat :: !(StringInfoRepr si)
                 -> !(f (StringType si))
                 -> !(f (StringType si))
                 -> App ext f (StringType si)
  
    -- Compute the length of a string
    StringLength :: !(f (StringType si))
                 -> App ext f IntegerType
  
    -- Test if the first string contains the second string as a substring
    StringContains :: !(f (StringType si))
                   -> !(f (StringType si))
                   -> App ext f BoolType
  
    -- Test if the first string is a prefix of the second string
    StringIsPrefixOf :: !(f (StringType si))
                   -> !(f (StringType si))
                   -> App ext f BoolType
  
    -- Test if the first string is a suffix of the second string
    StringIsSuffixOf :: !(f (StringType si))
                   -> !(f (StringType si))
                   -> App ext f BoolType
  
    -- Return the first position at which the second string can be found as a substring
    -- in the first string, starting from the given index.
    -- If no such position exists, or if the index is out of range, return a negative value.
    StringIndexOf :: !(f (StringType si))
                  -> !(f (StringType si))
                  -> !(f IntegerType)
                  -> App ext f IntegerType
  
    -- @stringSubstring s off len@ extracts the substring of @s@ starting at index @off@ and
    -- having length no more than @len@.  This operation returns the empty string if
    -- @len@ is negative or if @off@ is not in range.
    StringSubstring :: !(StringInfoRepr si)
                    -> !(f (StringType si))
                    -> !(f IntegerType)
                    -> !(f IntegerType)
                    -> App ext f (StringType si)
  
    ShowValue :: !(BaseTypeRepr bt)
              -> !(f (BaseToType bt))
              -> App ext f (StringType Unicode)
  
    ShowFloat :: !(FloatInfoRepr fi)
              -> !(f (FloatType fi))
              -> App ext f (StringType Unicode)
  
    ----------------------------------------------------------------------
    -- Arrays (supporting symbolic operations)
  
    SymArrayLookup   :: !(BaseTypeRepr b)
                     -> !(f (SymbolicArrayType (idx ::> tp) b))
                     -> !(Ctx.Assignment (BaseTerm f) (idx ::> tp))
                     -> App ext f (BaseToType b)
  
    SymArrayUpdate   :: !(BaseTypeRepr b)
                     -> !(f (SymbolicArrayType (idx ::> itp) b))
                     -> !(Ctx.Assignment (BaseTerm f) (idx ::> itp))
                     -> !(f (BaseToType b))
                     -> App ext f (SymbolicArrayType (idx ::> itp) b)
  
    ------------------------------------------------------------------------
    -- Introspection
  
    -- Returns true if the given value is a concrete value, false otherwise.
    -- This is primarily intended to assist with issuing warnings and such
    -- when a value is expected to be concrete.  This primitive could be
    -- used for evil; try to avoid the temptation.
    IsConcrete :: !(BaseTypeRepr b)
               -> f (BaseToType b)
               -> App ext f BoolType
  
    ------------------------------------------------------------------------
    -- References
  
    -- Check whether two references are equal.
    ReferenceEq :: !(TypeRepr tp)
                -> !(f (ReferenceType tp))
                -> !(f (ReferenceType tp))
                -> App ext f BoolType
  
  
  -- | Compute a run-time representation of the type of an application.
  instance TypeApp (ExprExtension ext) => TypeApp (App ext) where
    -- appType :: App ext f tp -> TypeRepr tp
    appType a0 =
     case a0 of
      BaseIsEq{} -> knownRepr
      BaseIte tp _ _ _ -> baseToType tp
      ---------------------------------------------------------------------
      -- Extension
      ExtensionApp x -> appType x
  
      ----------------------------------------------------------------------
      -- ()
      EmptyApp -> knownRepr
      ----------------------------------------------------------------------
      -- Any
      PackAny{} -> knownRepr
      UnpackAny tp _ -> MaybeRepr tp
      ----------------------------------------------------------------------
      -- Bool
      BoolLit{} -> knownRepr
      Not{} -> knownRepr
      And{} -> knownRepr
      Or{} -> knownRepr
      BoolXor{} -> knownRepr
      ----------------------------------------------------------------------
      -- Nat
      NatLit{} -> knownRepr
      NatEq{} -> knownRepr
      NatIte{} -> knownRepr
      NatLt{} -> knownRepr
      NatLe{} -> knownRepr
      NatAdd{} -> knownRepr
      NatSub{} -> knownRepr
      NatMul{} -> knownRepr
      NatDiv{} -> knownRepr
      NatMod{} -> knownRepr
  
      ----------------------------------------------------------------------
      -- Integer
      IntLit{} -> knownRepr
      IntLt{} -> knownRepr
      IntLe{} -> knownRepr
      IntNeg{} -> knownRepr
      IntAdd{} -> knownRepr
      IntSub{} -> knownRepr
      IntMul{} -> knownRepr
      IntDiv{} -> knownRepr
      IntMod{} -> knownRepr
      IntAbs{} -> knownRepr
  
      ----------------------------------------------------------------------
      -- RealVal
      RationalLit{} -> knownRepr
      RealAdd{} -> knownRepr
      RealSub{} -> knownRepr
      RealMul{} -> knownRepr
      RealDiv{} -> knownRepr
      RealMod{} -> knownRepr
      RealNeg{} -> knownRepr
      RealLe{} -> knownRepr
      RealLt{} -> knownRepr
      RealIsInteger{} -> knownRepr
  
      ----------------------------------------------------------------------
      -- Float
      FloatUndef fi -> FloatRepr fi
      FloatLit{} -> knownRepr
      DoubleLit{} -> knownRepr
      X86_80Lit{} -> knownRepr
      FloatNaN fi -> FloatRepr fi
      FloatPInf fi -> FloatRepr fi
      FloatNInf fi -> FloatRepr fi
      FloatPZero fi -> FloatRepr fi
      FloatNZero fi -> FloatRepr fi
      FloatNeg fi _ -> FloatRepr fi
      FloatAbs fi _ -> FloatRepr fi
      FloatSqrt fi _ _ -> FloatRepr fi
      FloatAdd fi _ _ _ -> FloatRepr fi
      FloatSub fi _ _ _ -> FloatRepr fi
      FloatMul fi _ _ _ -> FloatRepr fi
      FloatDiv fi _ _ _ -> FloatRepr fi
      FloatRem fi _ _ -> FloatRepr fi
      FloatMin fi _ _ -> FloatRepr fi
      FloatMax fi _ _ -> FloatRepr fi
      FloatFMA fi _ _ _ _ -> FloatRepr fi
      FloatEq{} -> knownRepr
      FloatFpEq{} -> knownRepr
      FloatLt{} -> knownRepr
      FloatLe{} -> knownRepr
      FloatGt{} -> knownRepr
      FloatGe{} -> knownRepr
      FloatNe{} -> knownRepr
      FloatFpApart{} -> knownRepr
      FloatIte fi _ _ _ -> FloatRepr fi
      FloatCast fi _ _ -> FloatRepr fi
      FloatFromBinary fi _ -> FloatRepr fi
      FloatToBinary fi _ -> case floatInfoToBVTypeRepr fi of
        BaseBVRepr w -> BVRepr w
      FloatFromBV fi _ _ -> FloatRepr fi
      FloatFromSBV fi _ _ -> FloatRepr fi
      FloatFromReal fi _ _ -> FloatRepr fi
      FloatToBV w _ _ -> BVRepr w
      FloatToSBV w _ _ -> BVRepr w
      FloatToReal{} -> knownRepr
      FloatIsNaN{} -> knownRepr
      FloatIsInfinite{} -> knownRepr
      FloatIsZero{} -> knownRepr
      FloatIsPositive{} -> knownRepr
      FloatIsNegative{} -> knownRepr
      FloatIsSubnormal{} -> knownRepr
      FloatIsNormal{} -> knownRepr
  
      ----------------------------------------------------------------------
      -- Maybe
  
      JustValue tp _ -> MaybeRepr tp
      NothingValue tp -> MaybeRepr tp
      FromJustValue tp _ _ -> tp
  
      ----------------------------------------------------------------------
      -- Recursive Types
  
      RollRecursive nm ctx _ -> RecursiveRepr nm ctx
      UnrollRecursive nm ctx _ -> unrollType nm ctx
  
      ----------------------------------------------------------------------
      -- Vector
      VectorIsEmpty{}          -> knownRepr
      VectorSize{}             -> knownRepr
      VectorLit       tp _     -> VectorRepr tp
      VectorReplicate tp _ _   -> VectorRepr tp
      VectorGetEntry  tp _ _   -> tp
      VectorSetEntry  tp _ _ _ -> VectorRepr tp
      VectorCons      tp _ _   -> VectorRepr tp
  
      ----------------------------------------------------------------------
      -- Sequence
      SequenceNil tpr -> SequenceRepr tpr
      SequenceCons tpr _ _ -> SequenceRepr tpr
      SequenceAppend tpr _ _ -> SequenceRepr tpr
      SequenceIsNil _ _ -> knownRepr
      SequenceHead tpr _ -> MaybeRepr tpr
      SequenceUncons tpr _ ->
        MaybeRepr (StructRepr (Ctx.Empty Ctx.:> tpr Ctx.:> SequenceRepr tpr))
      SequenceLength{} -> knownRepr
      SequenceTail tpr _ -> MaybeRepr (SequenceRepr tpr)
  
      ----------------------------------------------------------------------
      -- SymbolicArrayType
  
      SymArrayLookup b _ _ -> baseToType b
      SymArrayUpdate b _ idx _ ->
        baseToType (BaseArrayRepr (fmapFC baseTermType idx) b)
  
      ----------------------------------------------------------------------
      -- WordMap
      EmptyWordMap w tp -> WordMapRepr w tp
      InsertWordMap w tp _ _ _ -> WordMapRepr w tp
      LookupWordMap tp _ _ -> baseToType tp
      LookupWordMapWithDefault tp _ _ _ -> baseToType tp
  
      ----------------------------------------------------------------------
      -- Handle
  
      HandleLit h -> handleType h
      Closure a r _ _ _ ->
        FunctionHandleRepr a r
  
      ----------------------------------------------------------------------
      -- Conversions
      NatToInteger{} -> knownRepr
      IntegerToReal{} -> knownRepr
      RealToNat{} -> knownRepr
      RealRound{} -> knownRepr
      RealFloor{} -> knownRepr
      RealCeil{} -> knownRepr
      IntegerToBV w _ -> BVRepr w
  
      ----------------------------------------------------------------------
      -- ComplexReal
      Complex{} -> knownRepr
      RealPart{} -> knownRepr
      ImagPart{} -> knownRepr
  
      ----------------------------------------------------------------------
      -- BV
      BVUndef w -> BVRepr w
      BVLit w _ -> BVRepr w
      BVTrunc w _ _ -> BVRepr w
      BVZext w _ _ -> BVRepr w
      BVSext w _ _ -> BVRepr w
  
      BVNot w _ -> BVRepr w
      BVAnd w _ _ -> BVRepr w
      BVOr  w _ _ -> BVRepr w
      BVXor  w _ _ -> BVRepr w
      BVNeg w _ -> BVRepr w
      BVAdd w _ _ -> BVRepr w
      BVSub w _ _ -> BVRepr w
      BVMul w _ _ -> BVRepr w
      BVUdiv w _ _ -> BVRepr w
      BVSdiv w _ _ -> BVRepr w
      BVUrem w _ _ -> BVRepr w
      BVSrem w _ _ -> BVRepr w
      BVUle{} -> knownRepr
      BVUlt{} -> knownRepr
      BVSle{} -> knownRepr
      BVSlt{} -> knownRepr
      BVCarry{} -> knownRepr
      BVSCarry{} -> knownRepr
      BVSBorrow{} -> knownRepr
      BVShl w _ _ -> BVRepr w
      BVLshr w _ _ -> BVRepr w
      BVAshr w _ _ -> BVRepr w
      BVRol w _ _ -> BVRepr w
      BVRor w _ _ -> BVRepr w
      BVCountTrailingZeros w _ -> BVRepr w
      BVCountLeadingZeros w _ -> BVRepr w
      BVPopcount w _ -> BVRepr w
      BVUMax w _ _ -> BVRepr w
      BVUMin w _ _ -> BVRepr w
      BVSMax w _ _ -> BVRepr w
      BVSMin w _ _ -> BVRepr w
  
      BoolToBV w _ -> BVRepr w
      BvToNat{} -> knownRepr
      BvToInteger{} -> knownRepr
      SbvToInteger{} -> knownRepr
      BVNonzero{} -> knownRepr
      BVSelect _ n _ _ -> BVRepr n
      BVConcat w1 w2 _ _ -> BVRepr (addNat w1 w2)
  
      ----------------------------------------------------------------------
      -- Struct
  
      MkStruct ctx _ -> StructRepr ctx
      GetStruct _ _ tp -> tp
      SetStruct ctx _ _ _ -> StructRepr ctx
  
      ----------------------------------------------------------------------
      -- Variants
  
      InjectVariant ctx _ _ -> VariantRepr ctx
      ProjectVariant ctx idx _ -> MaybeRepr (ctx Ctx.! idx)
  
      ----------------------------------------------------------------------
      -- StringMap
      EmptyStringMap tp             -> StringMapRepr tp
      LookupStringMapEntry tp _ _   -> MaybeRepr tp
      InsertStringMapEntry tp _ _ _ -> StringMapRepr tp
  
      ----------------------------------------------------------------------
      -- String
  
      StringLit s -> StringRepr (stringLiteralInfo s)
      ShowValue{} -> knownRepr
      ShowFloat{} -> knownRepr
      StringConcat si _ _ -> StringRepr si
      StringEmpty si -> StringRepr si
      StringLength _ -> knownRepr
      StringContains{} -> knownRepr
      StringIsPrefixOf{} -> knownRepr
      StringIsSuffixOf{} -> knownRepr
      StringIndexOf{} -> knownRepr
      StringSubstring si _ _ _ -> StringRepr si
  
      ------------------------------------------------------------------------
      -- Introspection
  
      IsConcrete _ _ -> knownRepr
  
      ------------------------------------------------------------------------
      -- References
  
      ReferenceEq{} -> knownRepr
  
  
  ----------------------------------------------------------------------------
  -- Utility operations
  
  testFnHandle :: FnHandle a1 r1 -> FnHandle a2 r2 -> Maybe (FnHandle a1 r1 :~: FnHandle a2 r2)
  testFnHandle x y = do
    Refl <- testEquality (handleID x) (handleID y)
    return Refl
  
  compareFnHandle :: FnHandle a1 r1
                  -> FnHandle a2 r2
                  -> OrderingF (FnHandle a1 r1) (FnHandle a2 r2)
  compareFnHandle x y = do
    case compareF (handleID x) (handleID y) of
      LTF -> LTF
      GTF -> GTF
      EQF -> EQF
  
  testVector :: (forall x y. f x -> f y -> Maybe (x :~: y))
             -> Vector (f tp) -> Vector (f tp) -> Maybe (Int :~: Int)
  testVector testF x y = do
    case V.zipWithM_ testF x y of
      Just () -> Just Refl
      Nothing -> Nothing
  
  compareVector :: forall f tp. (forall x y. f x -> f y -> OrderingF x y)
  
                -> Vector (f tp) -> Vector (f tp) -> OrderingF Int Int
  compareVector cmpF x y
      | V.length x < V.length y = LTF
      | V.length x > V.length y = GTF
      | otherwise = V.foldr go EQF (V.zip x y)
    where go :: forall z. (f z, f z) -> OrderingF Int Int -> OrderingF Int Int
          go (u,v) r =
            case cmpF u v of
              LTF -> LTF
              GTF -> GTF
              EQF -> r
  
  -- Force app to be in context.
  $(return [])
  
  ------------------------------------------------------------------------
  -- Pretty printing
  
  ppBaseTermAssignment :: (forall u . f u -> Doc ann)
                       -> Ctx.Assignment (BaseTerm f) ctx
                       -> Doc ann
  ppBaseTermAssignment pp v = brackets (commas (toListFC (pp . baseTermVal) v))
  
  instance PrettyApp (ExprExtension ext) => PrettyApp (App ext) where
    --ppApp :: (forall a . f a -> Doc ann) -> App ext f b -> Doc ann
    ppApp = $(U.structuralPretty [t|App|]
            [ ( U.ConType [t|Ctx.Assignment|]
                `U.TypeApp` (U.ConType [t|BaseTerm|] `U.TypeApp` U.DataArg 1)
                `U.TypeApp` U.AnyType
              , [| ppBaseTermAssignment |]
              )
            , (U.ConType [t|ExprExtension|] `U.TypeApp`
                    U.DataArg 0 `U.TypeApp` U.DataArg 1 `U.TypeApp` U.AnyType,
                [| ppApp |]
              )
            , ( U.ConType [t|Vector|] `U.TypeApp` U.AnyType
              , [| \pp v -> brackets (commas (fmap pp v)) |]
              )
            ])
  
  ------------------------------------------------------------------------
  -- TraverseApp (requires TemplateHaskell)
  
  traverseBaseTerm :: Applicative m
                    => (forall tp . f tp -> m (g tp))
                    -> Ctx.Assignment (BaseTerm f) x
                    -> m (Ctx.Assignment (BaseTerm g) x)
  traverseBaseTerm f = traverseFC (traverseFC f)
  
  -- | Traversal that performs the given action on each immediate
  -- subterm of an application. Used for the 'TraversableFC' instance.
  traverseApp :: forall ext m f g tp.
                 ( TraversableFC (ExprExtension ext)
                 , Applicative m
                 )
              => (forall u . f u -> m (g u))
              -> App ext f tp -> m (App ext g tp)
  traverseApp =
    $(U.structuralTraversal [t|App|]
       [
         ( U.ConType [t|Ctx.Assignment|] `U.TypeApp` (U.DataArg 1) `U.TypeApp` U.AnyType
         , [|traverseFC|]
         )
       , (U.ConType [t|ExprExtension|] `U.TypeApp`
               U.DataArg 0 `U.TypeApp` U.DataArg 1 `U.TypeApp` U.AnyType,
           [| traverseFC |]
         )
       , ( U.ConType [t|Ctx.Assignment|]
           `U.TypeApp` (U.ConType [t|BaseTerm|] `U.TypeApp` (U.DataArg 1))
           `U.TypeApp` U.AnyType
         , [| traverseBaseTerm |]
         )
       ])
  
  ------------------------------------------------------------------------------
  -- Parameterized Eq and Ord instances
  
  instance ( TestEqualityFC (ExprExtension ext)
           ) => TestEqualityFC (App ext) where
    testEqualityFC testSubterm =
      $(U.structuralTypeEquality [t|App|]
          [ (U.DataArg 1                   `U.TypeApp` U.AnyType, [|testSubterm|])
          , (U.ConType [t|Float|],
                [| \x y -> if F.castFloatToWord32 x == F.castFloatToWord32 y then Just Refl else Nothing |])
          , (U.ConType [t|Double|],
                [| \x y -> if F.castDoubleToWord64 x == F.castDoubleToWord64 y then Just Refl else Nothing |])
          , (U.ConType [t|ExprExtension|] `U.TypeApp`
                  U.DataArg 0 `U.TypeApp` U.DataArg 1 `U.TypeApp` U.AnyType,
              [|testEqualityFC testSubterm|]
            )
          , (U.ConType [t|NatRepr |]       `U.TypeApp` U.AnyType, [|testEquality|])
          , (U.ConType [t|SymbolRepr |]    `U.TypeApp` U.AnyType, [|testEquality|])
          , (U.ConType [t|TypeRepr|]       `U.TypeApp` U.AnyType, [|testEquality|])
          , (U.ConType [t|BaseTypeRepr|]  `U.TypeApp` U.AnyType, [|testEquality|])
          , (U.ConType [t|StringInfoRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
          , (U.ConType [t|FloatInfoRepr|]  `U.TypeApp` U.AnyType, [|testEquality|])
          , (U.ConType [t|StringLiteral|] `U.TypeApp` U.AnyType, [|testEquality|])
          , (U.ConType [t|Ctx.Assignment|] `U.TypeApp`
                (U.ConType [t|BaseTerm|] `U.TypeApp` U.AnyType) `U.TypeApp` U.AnyType
            , [| testEqualityFC (testEqualityFC testSubterm) |]
            )
          , (U.ConType [t|Ctx.Assignment|] `U.TypeApp` U.DataArg 1 `U.TypeApp` U.AnyType
            , [| testEqualityFC testSubterm |]
            )
          , (U.ConType [t|CtxRepr|] `U.TypeApp` U.AnyType
            , [| testEquality |]
            )
          , (U.ConType [t|Ctx.Index|] `U.TypeApp` U.AnyType `U.TypeApp` U.AnyType, [|testEquality|])
          , (U.ConType [t|FnHandle|]  `U.TypeApp` U.AnyType `U.TypeApp` U.AnyType, [|testFnHandle|])
          , (U.ConType [t|Vector|]    `U.TypeApp` U.AnyType, [|testVector testSubterm|])
          ])
  
  instance ( TestEqualityFC (ExprExtension ext)
           , TestEquality f
           ) => TestEquality (App ext f) where
    testEquality = testEqualityFC testEquality
  
  instance ( OrdFC (ExprExtension ext)
           ) => OrdFC (App ext) where
    compareFC compareSubterm
          = $(U.structuralTypeOrd [t|App|]
                     [ (U.DataArg 1            `U.TypeApp` U.AnyType, [|compareSubterm|])
                     , (U.ConType [t|Float|],
                           [| \x y -> fromOrdering (compare (F.castFloatToWord32 x) (F.castFloatToWord32 y)) |])
                     , (U.ConType [t|Double|],
                           [| \x y -> fromOrdering (compare (F.castDoubleToWord64 x) (F.castDoubleToWord64 y)) |])
                     , (U.ConType [t|ExprExtension|] `U.TypeApp`
                             U.DataArg 0 `U.TypeApp` U.DataArg 1 `U.TypeApp` U.AnyType,
                         [|compareFC compareSubterm|]
                       )
                     , (U.ConType [t|NatRepr |] `U.TypeApp` U.AnyType, [|compareF|])
                     , (U.ConType [t|SymbolRepr |] `U.TypeApp` U.AnyType, [|compareF|])
                     , (U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|compareF|])
                     , (U.ConType [t|BaseTypeRepr|] `U.TypeApp` U.AnyType, [|compareF|])
                     , (U.ConType [t|StringInfoRepr|] `U.TypeApp` U.AnyType, [|compareF|])
                     , (U.ConType [t|FloatInfoRepr|] `U.TypeApp` U.AnyType, [|compareF|])
                     , (U.ConType [t|StringLiteral|] `U.TypeApp` U.AnyType, [|compareF|])
                     , (U.ConType [t|Ctx.Assignment|] `U.TypeApp`
                           (U.ConType [t|BaseTerm|] `U.TypeApp` U.AnyType) `U.TypeApp` U.AnyType
                       , [| compareFC (compareFC compareSubterm) |]
                       )
                     , (U.ConType [t|Ctx.Assignment|] `U.TypeApp` U.DataArg 1 `U.TypeApp` U.AnyType
                       , [| compareFC compareSubterm |]
                       )
                     , ( U.ConType [t|CtxRepr|] `U.TypeApp` U.AnyType
                       , [| compareF |]
                       )
                     , (U.ConType [t|Ctx.Index|] `U.TypeApp` U.AnyType `U.TypeApp` U.AnyType, [|compareF|])
                     , (U.ConType [t|FnHandle|]  `U.TypeApp` U.AnyType `U.TypeApp` U.AnyType, [|compareFnHandle|])
                     , (U.ConType [t|Vector|]    `U.TypeApp` U.AnyType, [|compareVector compareSubterm|])
                     ]
                    )
  
  instance ( OrdFC (ExprExtension ext)
           , OrdF f
           ) => OrdF (App ext f) where
    compareF = compareFC compareF
  
  -------------------------------------------------------------------------------------
  -- Traversals and such
  
  instance ( TraversableFC (ExprExtension ext)
           ) => FunctorFC (App ext) where
    fmapFC = fmapFCDefault
  
  instance ( TraversableFC (ExprExtension ext)
           ) => FoldableFC (App ext) where
    foldMapFC = foldMapFCDefault
  
  instance ( TraversableFC (ExprExtension ext)
           ) => TraversableFC (App ext) where
    traverseFC f = traverseApp f
  
  -- | Fold over an application.
  foldApp :: ( TraversableFC (ExprExtension ext)
             )
          => (forall x . f x -> r -> r)
          -> r
          -> App ext f tp
          -> r
  foldApp f0 r0 a = execState (traverseApp (go f0) a) r0
    where go f v = v <$ modify (f v)
  
  -- | Map a Crucible-type-preserving function over the immediate
  -- subterms of an application.
  mapApp :: ( TraversableFC (ExprExtension ext)
            )
         => (forall u . f u -> g u) -> App ext f tp -> App ext g tp
  mapApp f a = runIdentity (traverseApp (pure . f) a)
  