{-|
Module      : What4.Expr.App
Copyright   : (c) Galois Inc, 2015-2020
License     : BSD3
Maintainer  : jhendrix@galois.com

This module defines datastructures that encode the basic
syntax formers used in What4.ExprBuilder.
-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module What4.Expr.App where

import qualified Control.Exception as Ex
import           Control.Lens hiding (asIndex, (:>), Empty)
import           Control.Monad
import           Control.Monad.ST
import qualified Data.BitVector.Sized as BV
import           Data.Foldable
import           Data.Hashable
import qualified Data.HashTable.Class as H (toList)
import qualified Data.HashTable.ST.Basic as H
import           Data.Kind
import           Data.List.NonEmpty (NonEmpty(..))
import qualified Data.Map.Strict as Map
import           Data.Maybe
import           Data.Parameterized.Classes
import           Data.Parameterized.Context as Ctx
import qualified Data.Parameterized.HashTable as PH
import           Data.Parameterized.NatRepr
import           Data.Parameterized.Nonce
import           Data.Parameterized.Some
import           Data.Parameterized.TH.GADT
import           Data.Parameterized.TraversableFC
import           Data.Ratio (numerator, denominator)
import qualified Data.Sequence as Seq
import           Data.Set (Set)
import qualified Data.Set as Set
import           Data.STRef
import           Data.String
import           Data.Text (Text)
import qualified Data.Text as Text
import           Data.Word (Word64)
import           GHC.Generics (Generic)
import           LibBF (BigFloat)
import qualified LibBF as BF
import           Numeric.Natural
import           Prettyprinter hiding (Unbounded)

import           What4.BaseTypes
import           What4.Concrete
import           What4.Interface
import           What4.ProgramLoc
import qualified What4.SemiRing as SR
import qualified What4.SpecialFunctions as SFn
import qualified What4.Expr.ArrayUpdateMap as AUM
import           What4.Expr.BoolMap (BoolMap, Polarity(..), BoolMapView(..), Wrap(..))
import qualified What4.Expr.BoolMap as BM
import           What4.Expr.MATLAB
import           What4.Expr.WeightedSum (WeightedSum, SemiRingProduct)
import qualified What4.Expr.WeightedSum as WSum
import qualified What4.Expr.StringSeq as SSeq
import           What4.Expr.UnaryBV (UnaryBV)
import qualified What4.Expr.UnaryBV as UnaryBV

import           What4.Utils.AbstractDomains
import           What4.Utils.Arithmetic
import qualified What4.Utils.BVDomain as BVD
import           What4.Utils.Complex
import           What4.Utils.IncrHash
import qualified What4.Utils.AnnotatedMap as AM

------------------------------------------------------------------------
-- Data types

-- | This type represents 'Expr' values that were built from a
-- 'NonceApp'.
--
-- Parameter @t@ is a phantom type brand used to track nonces.
--
-- Selector functions are provided to destruct 'NonceAppExpr' values,
-- but the constructor is kept hidden. The preferred way to construct
-- an 'Expr' from a 'NonceApp' is to use 'sbNonceExpr'.
data NonceAppExpr t (tp :: BaseType)
   = NonceAppExprCtor { forall t (tp :: BaseType). NonceAppExpr t tp -> Nonce t tp
nonceExprId  :: {-# UNPACK #-} !(Nonce t tp)
                     , forall t (tp :: BaseType). NonceAppExpr t tp -> ProgramLoc
nonceExprLoc :: !ProgramLoc
                     , forall t (tp :: BaseType).
NonceAppExpr t tp -> NonceApp t (Expr t) tp
nonceExprApp :: !(NonceApp t (Expr t) tp)
                     , forall t (tp :: BaseType). NonceAppExpr t tp -> AbstractValue tp
nonceExprAbsValue :: !(AbstractValue tp)
                     }

-- | This type represents 'Expr' values that were built from an 'App'.
--
-- Parameter @t@ is a phantom type brand used to track nonces.
--
-- Selector functions are provided to destruct 'AppExpr' values, but
-- the constructor is kept hidden. The preferred way to construct an
-- 'Expr' from an 'App' is to use 'sbMakeExpr'.
data AppExpr t (tp :: BaseType)
   = AppExprCtor { forall t (tp :: BaseType). AppExpr t tp -> Nonce t tp
appExprId  :: {-# UNPACK #-} !(Nonce t tp)
                , forall t (tp :: BaseType). AppExpr t tp -> ProgramLoc
appExprLoc :: !ProgramLoc
                , forall t (tp :: BaseType). AppExpr t tp -> App (Expr t) tp
appExprApp :: !(App (Expr t) tp)
                , forall t (tp :: BaseType). AppExpr t tp -> AbstractValue tp
appExprAbsValue :: !(AbstractValue tp)
                }

-- | The main ExprBuilder expression datastructure.  The non-trivial @Expr@
-- values constructed by this module are uniquely identified by a
-- nonce value that is used to explicitly represent sub-term sharing.
-- When traversing the structure of an @Expr@ it is usually very important
-- to memoize computations based on the values of these identifiers to avoid
-- exponential blowups due to shared term structure.
--
-- Type parameter @t@ is a phantom type brand used to relate nonces to
-- a specific nonce generator (similar to the @s@ parameter of the
-- @ST@ monad). The type index @tp@ of kind 'BaseType' indicates the
-- type of the values denoted by the given expression.
--
-- Type @'Expr' t@ instantiates the type family @'SymExpr'
-- ('ExprBuilder' t st)@.
data Expr t (tp :: BaseType) where
  SemiRingLiteral :: !(SR.SemiRingRepr sr) -> !(SR.Coefficient sr) -> !ProgramLoc -> Expr t (SR.SemiRingBase sr)
  BoolExpr :: !Bool -> !ProgramLoc -> Expr t BaseBoolType
  FloatExpr :: !(FloatPrecisionRepr fpp) -> !BigFloat -> !ProgramLoc -> Expr t (BaseFloatType fpp)
  StringExpr :: !(StringLiteral si) -> !ProgramLoc -> Expr t (BaseStringType si)
  -- Application
  AppExpr :: {-# UNPACK #-} !(AppExpr t tp) -> Expr t tp
  -- An atomic predicate
  NonceAppExpr :: {-# UNPACK #-} !(NonceAppExpr t tp) -> Expr t tp
  -- A bound variable
  BoundVarExpr :: !(ExprBoundVar t tp) -> Expr t tp

data BVOrNote w = BVOrNote !IncrHash !(BVD.BVDomain w)

newtype BVOrSet e w = BVOrSet (AM.AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ())


-- | Type @'App' e tp@ encodes the top-level application of an 'Expr'
-- expression. It includes first-order expression forms that do not
-- bind variables (contrast with 'NonceApp').
--
-- Parameter @e@ is used everywhere a recursive sub-expression would
-- go. Uses of the 'App' type will tie the knot through this
-- parameter. Parameter @tp@ indicates the type of the expression.
data App (e :: BaseType -> Type) (tp :: BaseType) where

  ------------------------------------------------------------------------
  -- Generic operations

  BaseIte ::
    !(BaseTypeRepr tp) ->
    !Integer {- Total number of predicates in this ite tree -} ->
    !(e BaseBoolType) ->
    !(e tp) ->
    !(e tp) ->
    App e tp

  BaseEq ::
    !(BaseTypeRepr tp) ->
    !(e tp) ->
    !(e tp) ->
    App e BaseBoolType

  ------------------------------------------------------------------------
  -- Boolean operations

  -- Invariant: The argument to a NotPred must not be another NotPred.
  NotPred :: !(e BaseBoolType) -> App e BaseBoolType

  -- Invariant: The BoolMap must contain at least two elements. No
  -- element may be a NotPred; negated elements must be represented
  -- with Negative element polarity.
  ConjPred :: !(BoolMap e) -> App e BaseBoolType

  ------------------------------------------------------------------------
  -- Semiring operations

  SemiRingSum ::
    {-# UNPACK #-} !(WeightedSum e sr) ->
    App e (SR.SemiRingBase sr)

  -- A product of semiring values
  --
  -- The ExprBuilder should maintain the invariant that none of the values is
  -- a constant, and hence this denotes a non-linear expression.
  -- Multiplications by scalars should use the 'SemiRingSum' constructor.
  SemiRingProd ::
     {-# UNPACK #-} !(SemiRingProduct e sr) ->
     App e (SR.SemiRingBase sr)

  SemiRingLe
     :: !(SR.OrderedSemiRingRepr sr)
     -> !(e (SR.SemiRingBase sr))
     -> !(e (SR.SemiRingBase sr))
     -> App e BaseBoolType

  ------------------------------------------------------------------------
  -- Basic arithmetic operations

  RealIsInteger :: !(e BaseRealType) -> App e BaseBoolType

  IntDiv :: !(e BaseIntegerType)  -> !(e BaseIntegerType) -> App e BaseIntegerType
  IntMod :: !(e BaseIntegerType)  -> !(e BaseIntegerType) -> App e BaseIntegerType
  IntAbs :: !(e BaseIntegerType)  -> App e BaseIntegerType
  IntDivisible :: !(e BaseIntegerType) -> Natural -> App e BaseBoolType

  RealDiv :: !(e BaseRealType) -> !(e BaseRealType) -> App e BaseRealType

  -- Returns @sqrt(x)@, result is not defined if @x@ is negative.
  RealSqrt :: !(e BaseRealType) -> App e BaseRealType

  ------------------------------------------------------------------------
  -- Operations that introduce irrational numbers.

  RealSpecialFunction ::
    !(SFn.SpecialFunction args) ->
    !(SFn.SpecialFnArgs e BaseRealType args) ->
    App e (BaseRealType)

  --------------------------------
  -- Bitvector operations

  -- Return value of bit at given index.
  BVTestBit :: (1 <= w)
            => !Natural -- Index of bit to test
                        -- (least-significant bit has index 0)
            -> !(e (BaseBVType w))
            -> App e BaseBoolType
  BVSlt :: (1 <= w)
        => !(e (BaseBVType w))
        -> !(e (BaseBVType w))
        -> App e BaseBoolType
  BVUlt :: (1 <= w)
        => !(e (BaseBVType w))
        -> !(e (BaseBVType w))
        -> App e BaseBoolType

  BVOrBits :: (1 <= w) => !(NatRepr w) -> !(BVOrSet e w) -> App e (BaseBVType w)

  -- A unary representation of terms where an integer @i@ is mapped to a
  -- predicate that is true if the unsigned encoding of the value is greater
  -- than or equal to @i@.
  --
  -- The map contains a binding (i -> p_i) when the predicate
  --
  -- As an example, we can encode the value @1@ with the assignment:
  --   { 0 => true ; 2 => false }
  BVUnaryTerm :: (1 <= n)
              => !(UnaryBV (e BaseBoolType) n)
              -> App e (BaseBVType n)

  BVConcat :: (1 <= u, 1 <= v, 1 <= (u+v))
           => !(NatRepr (u+v))
           -> !(e (BaseBVType u))
           -> !(e (BaseBVType v))
           -> App e (BaseBVType (u+v))

  BVSelect :: (1 <= n, idx + n <= w)
              -- First bit to select from (least-significant bit has index 0)
           => !(NatRepr idx)
              -- Number of bits to select, counting up toward more significant bits
           -> !(NatRepr n)
              -- Bitvector to select from.
           -> !(e (BaseBVType w))
           -> App e (BaseBVType n)

  BVFill :: (1 <= w)
         => !(NatRepr w)
         -> !(e BaseBoolType)
         -> App e (BaseBVType w)

  BVUdiv :: (1 <= w)
         => !(NatRepr w)
         -> !(e (BaseBVType w))
         -> !(e (BaseBVType w))
         -> App e (BaseBVType w)
  BVUrem :: (1 <= w)
         => !(NatRepr w)
         -> !(e (BaseBVType w))
         -> !(e (BaseBVType w))
         -> App e (BaseBVType w)
  BVSdiv :: (1 <= w)
         => !(NatRepr w)
         -> !(e (BaseBVType w))
         -> !(e (BaseBVType w))
         -> App e (BaseBVType w)
  BVSrem :: (1 <= w)
         => !(NatRepr w)
         -> !(e (BaseBVType w))
         -> !(e (BaseBVType w))
         -> App e (BaseBVType w)

  BVShl :: (1 <= w)
        => !(NatRepr w)
        -> !(e (BaseBVType w))
        -> !(e (BaseBVType w))
        -> App e (BaseBVType w)

  BVLshr :: (1 <= w)
         => !(NatRepr w)
         -> !(e (BaseBVType w))
         -> !(e (BaseBVType w))
         -> App e (BaseBVType w)

  BVAshr :: (1 <= w)
         => !(NatRepr w)
         -> !(e (BaseBVType w))
         -> !(e (BaseBVType w))
         -> App e (BaseBVType w)

  BVRol :: (1 <= w)
        => !(NatRepr w)
        -> !(e (BaseBVType w)) -- bitvector to rotate
        -> !(e (BaseBVType w)) -- rotate amount
        -> App e (BaseBVType w)

  BVRor :: (1 <= w)
        => !(NatRepr w)
        -> !(e (BaseBVType w))   -- bitvector to rotate
        -> !(e (BaseBVType w))   -- rotate amount
        -> App e (BaseBVType w)

  BVZext :: (1 <= w, w+1 <= r, 1 <= r)
         => !(NatRepr r)
         -> !(e (BaseBVType w))
         -> App e (BaseBVType r)

  BVSext :: (1 <= w, w+1 <= r, 1 <= r)
         => !(NatRepr r)
         -> !(e (BaseBVType w))
         -> App e (BaseBVType r)

  BVPopcount ::
    (1 <= w) =>
    !(NatRepr w) ->
    !(e (BaseBVType w)) ->
    App e (BaseBVType w)

  BVCountTrailingZeros ::
    (1 <= w) =>
    !(NatRepr w) ->
    !(e (BaseBVType w)) ->
    App e (BaseBVType w)

  BVCountLeadingZeros ::
    (1 <= w) =>
    !(NatRepr w) ->
    !(e (BaseBVType w)) ->
    App e (BaseBVType w)

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

  FloatNeg
    :: !(FloatPrecisionRepr fpp)
    -> !(e (BaseFloatType fpp))
    -> App e (BaseFloatType fpp)
  FloatAbs
    :: !(FloatPrecisionRepr fpp)
    -> !(e (BaseFloatType fpp))
    -> App e (BaseFloatType fpp)
  FloatSqrt
    :: !(FloatPrecisionRepr fpp)
    -> !RoundingMode
    -> !(e (BaseFloatType fpp))
    -> App e (BaseFloatType fpp)
  FloatAdd
    :: !(FloatPrecisionRepr fpp)
    -> !RoundingMode
    -> !(e (BaseFloatType fpp))
    -> !(e (BaseFloatType fpp))
    -> App e (BaseFloatType fpp)
  FloatSub
    :: !(FloatPrecisionRepr fpp)
    -> !RoundingMode
    -> !(e (BaseFloatType fpp))
    -> !(e (BaseFloatType fpp))
    -> App e (BaseFloatType fpp)
  FloatMul
    :: !(FloatPrecisionRepr fpp)
    -> !RoundingMode
    -> !(e (BaseFloatType fpp))
    -> !(e (BaseFloatType fpp))
    -> App e (BaseFloatType fpp)
  FloatDiv
    :: !(FloatPrecisionRepr fpp)
    -> !RoundingMode
    -> !(e (BaseFloatType fpp))
    -> !(e (BaseFloatType fpp))
    -> App e (BaseFloatType fpp)
  FloatRem
    :: !(FloatPrecisionRepr fpp)
    -> !(e (BaseFloatType fpp))
    -> !(e (BaseFloatType fpp))
    -> App e (BaseFloatType fpp)
  FloatFMA
    :: !(FloatPrecisionRepr fpp)
    -> !RoundingMode
    -> !(e (BaseFloatType fpp))
    -> !(e (BaseFloatType fpp))
    -> !(e (BaseFloatType fpp))
    -> App e (BaseFloatType fpp)
  FloatFpEq
    :: !(e (BaseFloatType fpp))
    -> !(e (BaseFloatType fpp))
    -> App e BaseBoolType
  FloatLe
    :: !(e (BaseFloatType fpp))
    -> !(e (BaseFloatType fpp))
    -> App e BaseBoolType
  FloatLt
    :: !(e (BaseFloatType fpp))
    -> !(e (BaseFloatType fpp))
    -> App e BaseBoolType
  FloatIsNaN :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
  FloatIsInf :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
  FloatIsZero :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
  FloatIsPos :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
  FloatIsNeg :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
  FloatIsSubnorm :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
  FloatIsNorm :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
  FloatCast
    :: !(FloatPrecisionRepr fpp)
    -> !RoundingMode
    -> !(e (BaseFloatType fpp'))
    -> App e (BaseFloatType fpp)
  FloatRound
    :: !(FloatPrecisionRepr fpp)
    -> !RoundingMode
    -> !(e (BaseFloatType fpp))
    -> App e (BaseFloatType fpp)
  FloatFromBinary
    :: (2 <= eb, 2 <= sb)
    => !(FloatPrecisionRepr (FloatingPointPrecision eb sb))
    -> !(e (BaseBVType (eb + sb)))
    -> App e (BaseFloatType (FloatingPointPrecision eb sb))
  FloatToBinary
    :: (2 <= eb, 2 <= sb, 1 <= eb + sb)
    => !(FloatPrecisionRepr (FloatingPointPrecision eb sb))
    -> !(e (BaseFloatType (FloatingPointPrecision eb sb)))
    -> App e (BaseBVType (eb + sb))
  BVToFloat
    :: (1 <= w)
    => !(FloatPrecisionRepr fpp)
    -> !RoundingMode
    -> !(e (BaseBVType w))
    -> App e (BaseFloatType fpp)
  SBVToFloat
    :: (1 <= w)
    => !(FloatPrecisionRepr fpp)
    -> !RoundingMode
    -> !(e (BaseBVType w))
    -> App e (BaseFloatType fpp)
  RealToFloat
    :: !(FloatPrecisionRepr fpp)
    -> !RoundingMode
    -> !(e BaseRealType)
    -> App e (BaseFloatType fpp)
  FloatToBV
    :: (1 <= w)
    => !(NatRepr w)
    -> !RoundingMode
    -> !(e (BaseFloatType fpp))
    -> App e (BaseBVType w)
  FloatToSBV
    :: (1 <= w)
    => !(NatRepr w)
    -> !RoundingMode
    -> !(e (BaseFloatType fpp))
    -> App e (BaseBVType w)
  FloatToReal :: !(e (BaseFloatType fpp)) -> App e BaseRealType

  FloatSpecialFunction ::
    !(FloatPrecisionRepr fpp) ->
    !(SFn.SpecialFunction args) ->
    !(SFn.SpecialFnArgs e (BaseFloatType fpp) args) ->
    App e (BaseFloatType fpp)

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

  -- Partial map from concrete indices to array values over another array.
  ArrayMap :: !(Ctx.Assignment BaseTypeRepr (i ::> itp))
           -> !(BaseTypeRepr tp)
                -- /\ The type of the array.
           -> !(AUM.ArrayUpdateMap e (i ::> itp) tp)
              -- /\ Maps indices that are updated to the associated value.
           -> !(e (BaseArrayType (i::> itp) tp))
              -- /\ The underlying array that has been updated.
           -> App e (BaseArrayType (i ::> itp) tp)

  -- Constant array
  ConstantArray :: !(Ctx.Assignment BaseTypeRepr (i ::> tp))
                -> !(BaseTypeRepr b)
                -> !(e b)
                -> App e (BaseArrayType (i::>tp) b)

  UpdateArray :: !(BaseTypeRepr b)
              -> !(Ctx.Assignment BaseTypeRepr (i::>tp))
              -> !(e (BaseArrayType (i::>tp) b))
              -> !(Ctx.Assignment e (i::>tp))
              -> !(e b)
              -> App e (BaseArrayType (i::>tp) b)

  SelectArray :: !(BaseTypeRepr b)
              -> !(e (BaseArrayType (i::>tp) b))
              -> !(Ctx.Assignment e (i::>tp))
              -> App e b

  CopyArray ::
    (1 <= w) =>
    !(NatRepr w) ->
    !(BaseTypeRepr a) ->
    !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) {- @dest_arr@ -} ->
    !(e (BaseBVType w)) {- @dest_idx@ -} ->
    !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) {- @src_arr@ -} ->
    !(e (BaseBVType w)) {- @src_idx@ -} ->
    !(e (BaseBVType w)) {- @len@ -} ->
    !(e (BaseBVType w)) {- @dest_idx + len@ -} ->
    !(e (BaseBVType w)) {- @src_idx + len@ -} ->
    App e (BaseArrayType (SingleCtx (BaseBVType w)) a)

  SetArray ::
    (1 <= w) =>
    !(NatRepr w) ->
    !(BaseTypeRepr a) ->
    !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) {- @arr@ -} ->
    !(e (BaseBVType w)) {- @idx@ -} ->
    !(e a) {- @val@ -}->
    !(e (BaseBVType w)) {- @len@ -} ->
    !(e (BaseBVType w)) {- @idx + len@ -} ->
    App e (BaseArrayType (SingleCtx (BaseBVType w)) a)

  EqualArrayRange ::
    (1 <= w) =>
    !(NatRepr w) ->
    !(BaseTypeRepr a) ->
    !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) {- @lhs_arr@ -} ->
    !(e (BaseBVType w)) {- @lhs_idx@ -} ->
    !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) {- @rhs_arr@ -} ->
    !(e (BaseBVType w)) {- @rhs_idx@ -} ->
    !(e (BaseBVType w)) {- @len@ -} ->
    !(e (BaseBVType w)) {- @lhs_idx + len@ -} ->
    !(e (BaseBVType w)) {- @rhs_idx + len@ -} ->
    App e BaseBoolType

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

  IntegerToReal :: !(e BaseIntegerType) -> App e BaseRealType

  -- Convert a real value to an integer
  --
  -- Not defined on non-integral reals.
  RealToInteger :: !(e BaseRealType) -> App e BaseIntegerType

  BVToInteger   :: (1 <= w) => !(e (BaseBVType w)) -> App e BaseIntegerType
  SBVToInteger  :: (1 <= w) => !(e (BaseBVType w)) -> App e BaseIntegerType

  -- Converts integer to a bitvector.  The number is interpreted modulo 2^n.
  IntegerToBV  :: (1 <= w) => !(e BaseIntegerType) -> NatRepr w -> App e (BaseBVType w)

  RoundReal :: !(e BaseRealType) -> App e BaseIntegerType
  RoundEvenReal :: !(e BaseRealType) -> App e BaseIntegerType
  FloorReal :: !(e BaseRealType) -> App e BaseIntegerType
  CeilReal  :: !(e BaseRealType) -> App e BaseIntegerType

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

  Cplx  :: {-# UNPACK #-} !(Complex (e BaseRealType)) -> App e BaseComplexType
  RealPart :: !(e BaseComplexType) -> App e BaseRealType
  ImagPart :: !(e BaseComplexType) -> App e BaseRealType

  ------------------------------------------------------------------------
  -- Strings

  StringContains :: !(e (BaseStringType si))
                 -> !(e (BaseStringType si))
                 -> App e BaseBoolType

  StringIsPrefixOf :: !(e (BaseStringType si))
                 -> !(e (BaseStringType si))
                 -> App e BaseBoolType

  StringIsSuffixOf :: !(e (BaseStringType si))
                 -> !(e (BaseStringType si))
                 -> App e BaseBoolType

  StringIndexOf :: !(e (BaseStringType si))
                -> !(e (BaseStringType si))
                -> !(e BaseIntegerType)
                -> App e BaseIntegerType

  StringSubstring :: !(StringInfoRepr si)
                  -> !(e (BaseStringType si))
                  -> !(e BaseIntegerType)
                  -> !(e BaseIntegerType)
                  -> App e (BaseStringType si)

  StringAppend :: !(StringInfoRepr si)
               -> !(SSeq.StringSeq e si)
               -> App e (BaseStringType si)

  StringLength :: !(e (BaseStringType si))
               -> App e BaseIntegerType

  ------------------------------------------------------------------------
  -- Structs

  -- A struct with its fields.
  StructCtor :: !(Ctx.Assignment BaseTypeRepr flds)
             -> !(Ctx.Assignment e flds)
             -> App e (BaseStructType flds)

  StructField :: !(e (BaseStructType flds))
              -> !(Ctx.Index flds tp)
              -> !(BaseTypeRepr tp)
              -> App e tp

-- | The Kind of a bound variable.
data VarKind
  = QuantifierVarKind
    -- ^ A variable appearing in a quantifier.
  | LatchVarKind
    -- ^ A variable appearing as a latch input.
  | UninterpVarKind
    -- ^ A variable appearing in a uninterpreted constant

-- | Information about bound variables.
-- Parameter @t@ is a phantom type brand used to track nonces.
--
-- Type @'ExprBoundVar' t@ instantiates the type family
-- @'BoundVar' ('ExprBuilder' t st)@.
--
-- Selector functions are provided to destruct 'ExprBoundVar'
-- values, but the constructor is kept hidden. The preferred way to
-- construct a 'ExprBoundVar' is to use 'freshBoundVar'.
data ExprBoundVar t (tp :: BaseType) =
  BVar { forall t (tp :: BaseType). ExprBoundVar t tp -> Nonce t tp
bvarId  :: {-# UNPACK #-} !(Nonce t tp)
       , forall t (tp :: BaseType). ExprBoundVar t tp -> ProgramLoc
bvarLoc :: !ProgramLoc
       , forall t (tp :: BaseType). ExprBoundVar t tp -> SolverSymbol
bvarName :: !SolverSymbol
       , forall t (tp :: BaseType). ExprBoundVar t tp -> BaseTypeRepr tp
bvarType :: !(