{- |
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 { forall (f :: CrucibleType -> Type) (tp :: BaseType).
BaseTerm f tp -> BaseTypeRepr tp
baseTermType :: !(BaseTypeRepr tp)
              , forall (f :: CrucibleType -> Type) (tp :: BaseType).
BaseTerm f tp -> f (BaseToType tp)
baseTermVal  :: !(f (BaseToType tp))
              }

instance TestEqualityFC BaseTerm where
  testEqualityFC :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
 f x -> f y -> Maybe (x :~: y))
-> forall (x :: BaseType) (y :: BaseType).
   BaseTerm f x -> BaseTerm f y -> Maybe (x :~: y)
testEqualityFC forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y)
testF (BaseTerm BaseTypeRepr x
_ f (BaseToType x)
x) (BaseTerm BaseTypeRepr y
_ f (BaseToType y)
y) = do
    BaseToType x :~: BaseToType y
Refl <- f (BaseToType x)
-> f (BaseToType y) -> Maybe (BaseToType x :~: BaseToType y)
forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y)
testF f (BaseToType x)
x f (BaseToType y)
y
    (x :~: y) -> Maybe (x :~: y)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return x :~: x
x :~: y
forall {k} (a :: k). a :~: a
Refl
instance TestEquality f => TestEquality (BaseTerm f) where
  testEquality :: forall (a :: BaseType) (b :: BaseType).
BaseTerm f a -> BaseTerm f b -> Maybe (a :~: b)
testEquality = (forall (x :: CrucibleType) (y :: CrucibleType).
 f x -> f y -> Maybe (x :~: y))
-> forall (a :: BaseType) (b :: BaseType).
   BaseTerm f a -> BaseTerm f b -> Maybe (a :~: b)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type).
TestEqualityFC t =>
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> forall (x :: l) (y :: l). t f x -> t f y -> Maybe (x :~: y)
forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
 f x -> f y -> Maybe (x :~: y))
-> forall (x :: BaseType) (y :: BaseType).
   BaseTerm f x -> BaseTerm f y -> Maybe (x :~: y)
testEqualityFC f x -> f y -> Maybe (x :~: y)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y)
testEquality

instance OrdFC BaseTerm where
  compareFC :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
 f x -> f y -> OrderingF x y)
-> forall (x :: BaseType) (y :: BaseType).
   BaseTerm f x -> BaseTerm f y -> OrderingF x y
compareFC forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> OrderingF x y
cmpF (BaseTerm BaseTypeRepr x
_ f (BaseToType x)
x) (BaseTerm BaseTypeRepr y
_ f (BaseToType y)
y) = do
    case f (BaseToType x)
-> f (BaseToType y) -> OrderingF (BaseToType x) (BaseToType y)
forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> OrderingF x y
cmpF f (BaseToType x)
x f (BaseToType y)
y of
      OrderingF (BaseToType x) (BaseToType y)
LTF -> OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
      OrderingF (BaseToType x) (BaseToType y)
GTF -> OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF
      OrderingF (BaseToType x) (BaseToType y)
EQF -> OrderingF x x
OrderingF x y
forall {k} (x :: k). OrderingF x x
EQF
instance OrdF f => OrdF (BaseTerm f) where
  compareF :: forall (x :: BaseType) (y :: BaseType).
BaseTerm f x -> BaseTerm f y -> OrderingF x y
compareF = (forall (x :: CrucibleType) (y :: CrucibleType).
 f x -> f y -> OrderingF x y)
-> forall (x :: BaseType) (y :: BaseType).
   BaseTerm f x -> BaseTerm f y -> OrderingF x y
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type).
OrdFC t =>
(forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> forall (x :: l) (y :: l). t f x -> t f y -> OrderingF x y
forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
 f x -> f y -> OrderingF x y)
-> forall (x :: BaseType) (y :: BaseType).
   BaseTerm f x -> BaseTerm f y -> OrderingF x y
compareFC f x -> f y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> OrderingF x y
compareF

instance FunctorFC BaseTerm where
  fmapFC :: forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: BaseType). BaseTerm f x -> BaseTerm g x
fmapFC = (forall (x :: CrucibleType). f x -> g x)
-> BaseTerm f x -> BaseTerm g x
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: BaseType). BaseTerm f x -> BaseTerm g x
forall {k} {l} (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
TraversableFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: BaseType). BaseTerm f x -> BaseTerm g x
fmapFCDefault

instance FoldableFC BaseTerm where
  foldMapFC :: forall (f :: CrucibleType -> Type) m.
Monoid m =>
(forall (x :: CrucibleType). f x -> m)
-> forall (x :: BaseType). BaseTerm f x -> m
foldMapFC = (forall (x :: CrucibleType). f x -> m) -> BaseTerm f x -> m
(forall (x :: CrucibleType). f x -> m)
-> forall (x :: BaseType). BaseTerm f x -> m
forall {k} {l} (t :: (k -> Type) -> l -> Type) m (f :: k -> Type).
(TraversableFC t, Monoid m) =>
(forall (x :: k). f x -> m) -> forall (x :: l). t f x -> m
foldMapFCDefault

instance TraversableFC BaseTerm where
  traverseFC :: forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: BaseType). BaseTerm f x -> m (BaseTerm g x)
traverseFC forall (x :: CrucibleType). f x -> m (g x)
f (BaseTerm BaseTypeRepr x
tp f (BaseToType x)
x) = BaseTypeRepr x -> g (BaseToType x) -> BaseTerm g x
forall (f :: CrucibleType -> Type) (tp :: BaseType).
BaseTypeRepr tp -> f (BaseToType tp) -> BaseTerm f tp
BaseTerm BaseTypeRepr x
tp (g (BaseToType x) -> BaseTerm g x)
-> m (g (BaseToType x)) -> m (BaseTerm g x)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f (BaseToType x) -> m (g (BaseToType x))
forall (x :: CrucibleType). f x -> m (g x)
f f (BaseToType x)
x

------------------------------------------------------------------------
-- App

-- | Equality on booleans
pattern BoolEq :: () => (tp ~ BoolType) => f BoolType -> f BoolType -> App ext f tp
pattern $mBoolEq :: forall {r} {tp :: CrucibleType} {f :: CrucibleType -> Type} {ext}.
App ext f tp
-> ((tp ~ BoolType) => f BoolType -> f BoolType -> r)
-> ((# #) -> r)
-> r
$bBoolEq :: forall (tp :: CrucibleType) (f :: CrucibleType -> Type) ext.
(tp ~ BoolType) =>
f BoolType -> f BoolType -> App ext f tp
BoolEq x y = BaseIsEq BaseBoolRepr x y

-- | Equality on integers
pattern IntEq :: () => (tp ~ BoolType) => f IntegerType -> f IntegerType -> App ext f tp
pattern $mIntEq :: forall {r} {tp :: CrucibleType} {f :: CrucibleType -> Type} {ext}.
App ext f tp
-> ((tp ~ BoolType) => f IntegerType -> f IntegerType -> r)
-> ((# #) -> r)
-> r
$bIntEq :: forall (tp :: CrucibleType) (f :: CrucibleType -> Type) ext.
(tp ~ BoolType) =>
f IntegerType -> f IntegerType -> App ext f tp
IntEq x y = BaseIsEq BaseIntegerRepr x y

-- | Equality on real numbers.
pattern RealEq :: () => (tp ~ BoolType) => f RealValType -> f RealValType -> App ext f tp
pattern $mRealEq :: forall {r} {tp :: CrucibleType} {f :: CrucibleType -> Type} {ext}.
App ext f tp
-> ((tp ~ BoolType) => f RealValType -> f RealValType -> r)
-> ((# #) -> r)
-> r
$bRealEq :: forall (tp :: CrucibleType) (f :: CrucibleType -> Type) ext.
(tp ~ BoolType) =>
f RealValType -> f RealValType -> App ext f tp
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 $mBVEq :: forall {r} {tp :: CrucibleType} {f :: CrucibleType -> Type} {ext}.
App ext f tp
-> (forall {w :: Natural}.
    (1 <= w, tp ~ BoolType) =>
    NatRepr w -> f (BVType w) -> f (BVType w) -> r)
-> ((# #) -> r)
-> r
$bBVEq :: forall (tp :: CrucibleType) (f :: CrucibleType -> Type) ext
       (w :: Natural).
(1 <= w, tp ~ BoolType) =>
NatRepr w -> f (BVType w) -> f (BVType w) -> App ext f tp
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 $mBoolIte :: forall {r} {tp :: CrucibleType} {f :: CrucibleType -> Type} {ext}.
App ext f tp
-> ((tp ~ BoolType) => f BoolType -> f tp -> f tp -> r)
-> ((# #) -> r)
-> r
$bBoolIte :: forall (tp :: CrucibleType) (f :: CrucibleType -> Type) ext.
(tp ~ BoolType) =>
f BoolType -> f tp -> f tp -> App ext f tp
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 $mIntIte :: forall {r} {tp :: CrucibleType} {f :: CrucibleType -> Type} {ext}.
App ext f tp
-> ((tp ~ IntegerType) => f BoolType -> f tp -> f tp -> r)
-> ((# #) -> r)
-> r
$bIntIte :: forall (tp :: CrucibleType) (f :: CrucibleType -> Type) ext.
(tp ~ IntegerType) =>
f BoolType -> f tp -> f tp -> App ext f tp
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 $mRealIte :: forall {r} {tp :: CrucibleType} {f :: CrucibleType -> Type} {ext}.
App ext f tp
-> ((tp ~ RealValType) => f BoolType -> f tp -> f tp -> r)
-> ((# #) -> r)
-> r
$bRealIte :: forall (tp :: CrucibleType) (f :: CrucibleType -> Type) ext.
(tp ~ RealValType) =>
f BoolType -> f tp -> f tp -> App ext f tp
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 $mBVIte :: forall {r} {tp :: CrucibleType} {f :: CrucibleType -> Type} {ext}.
App ext f tp
-> (forall {w :: Natural}.
    (1 <= w, tp ~ BVType w) =>
    f BoolType -> NatRepr w -> f tp -> f tp -> r)
-> ((# #) -> r)
-> r
$bBVIte :: forall (tp :: CrucibleType) (f :: CrucibleType -> Type) ext
       (w :: Natural).
(1 <= w, tp ~ BVType w) =>
f BoolType -> NatRepr w -> f tp -> f tp -> App ext f tp
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 :: forall (f :: CrucibleType -> Type) (x :: CrucibleType).
App ext f x -> TypeRepr x
appType App ext f x
a0 =
   case App ext f x
a0 of
    BaseIsEq{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    BaseIte BaseTypeRepr tp
tp f BoolType
_ f ('BaseToType tp)
_ f ('BaseToType tp)
_ -> BaseTypeRepr tp -> TypeRepr ('BaseToType tp)
forall (bt :: BaseType).
BaseTypeRepr bt -> TypeRepr (BaseToType bt)
baseToType BaseTypeRepr tp
tp
    ---------------------------------------------------------------------
    -- Extension
    ExtensionApp ExprExtension ext f x
x -> ExprExtension ext f x -> TypeRepr x
forall (f :: CrucibleType -> Type) (x :: CrucibleType).
ExprExtension ext f x -> TypeRepr x
forall (app :: (CrucibleType -> Type) -> CrucibleType -> Type)
       (f :: CrucibleType -> Type) (x :: CrucibleType).
TypeApp app =>
app f x -> TypeRepr x
appType ExprExtension ext f x
x

    ----------------------------------------------------------------------
    -- ()
    App ext f x
EmptyApp -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    ----------------------------------------------------------------------
    -- Any
    PackAny{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    UnpackAny TypeRepr tp
tp f 'AnyType
_ -> TypeRepr tp -> TypeRepr ('MaybeType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('MaybeType tp1)
MaybeRepr TypeRepr tp
tp
    ----------------------------------------------------------------------
    -- Bool
    BoolLit{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    Not{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    And{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    Or{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    BoolXor{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    ----------------------------------------------------------------------
    -- Nat
    NatLit{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    NatEq{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    NatIte{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    NatLt{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    NatLe{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    NatAdd{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    NatSub{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    NatMul{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    NatDiv{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    NatMod{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

    ----------------------------------------------------------------------
    -- Integer
    IntLit{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    IntLt{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    IntLe{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    IntNeg{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    IntAdd{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    IntSub{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    IntMul{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    IntDiv{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    IntMod{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    IntAbs{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

    ----------------------------------------------------------------------
    -- RealVal
    RationalLit{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealAdd{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealSub{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealMul{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealDiv{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealMod{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealNeg{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealLe{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealLt{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealIsInteger{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

    ----------------------------------------------------------------------
    -- Float
    FloatUndef FloatInfoRepr fi
fi -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatLit{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    DoubleLit{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    X86_80Lit{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatNaN FloatInfoRepr fi
fi -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatPInf FloatInfoRepr fi
fi -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatNInf FloatInfoRepr fi
fi -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatPZero FloatInfoRepr fi
fi -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatNZero FloatInfoRepr fi
fi -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatNeg FloatInfoRepr fi
fi f ('FloatType fi)
_ -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatAbs FloatInfoRepr fi
fi f ('FloatType fi)
_ -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatSqrt FloatInfoRepr fi
fi RoundingMode
_ f ('FloatType fi)
_ -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatAdd FloatInfoRepr fi
fi RoundingMode
_ f ('FloatType fi)
_ f ('FloatType fi)
_ -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatSub FloatInfoRepr fi
fi RoundingMode
_ f ('FloatType fi)
_ f ('FloatType fi)
_ -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatMul FloatInfoRepr fi
fi RoundingMode
_ f ('FloatType fi)
_ f ('FloatType fi)
_ -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatDiv FloatInfoRepr fi
fi RoundingMode
_ f ('FloatType fi)
_ f ('FloatType fi)
_ -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatRem FloatInfoRepr fi
fi f ('FloatType fi)
_ f ('FloatType fi)
_ -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatMin FloatInfoRepr fi
fi f ('FloatType fi)
_ f ('FloatType fi)
_ -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatMax FloatInfoRepr fi
fi f ('FloatType fi)
_ f ('FloatType fi)
_ -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatFMA FloatInfoRepr fi
fi RoundingMode
_ f ('FloatType fi)
_ f ('FloatType fi)
_ f ('FloatType fi)
_ -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatEq{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatFpEq{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatLt{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatLe{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatGt{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatGe{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatNe{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatFpApart{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatIte FloatInfoRepr fi
fi f BoolType
_ f ('FloatType fi)
_ f ('FloatType fi)
_ -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatCast FloatInfoRepr fi
fi RoundingMode
_ f (FloatType fi')
_ -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatFromBinary FloatInfoRepr fi
fi f (BVType (FloatInfoToBitWidth fi))
_ -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatToBinary FloatInfoRepr fi
fi f (FloatType fi)
_ -> case FloatInfoRepr fi
-> BaseTypeRepr (BaseBVType (FloatInfoToBitWidth fi))
forall (fi :: FloatInfo).
FloatInfoRepr fi
-> BaseTypeRepr (BaseBVType (FloatInfoToBitWidth fi))
floatInfoToBVTypeRepr FloatInfoRepr fi
fi of
      BaseBVRepr NatRepr w
w -> NatRepr w -> TypeRepr ('BaseToType ('BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    FloatFromBV FloatInfoRepr fi
fi RoundingMode
_ f (BVType w)
_ -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatFromSBV FloatInfoRepr fi
fi RoundingMode
_ f (BVType w)
_ -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatFromReal FloatInfoRepr fi
fi RoundingMode
_ f RealValType
_ -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FloatToBV NatRepr w
w RoundingMode
_ f (FloatType fi)
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    FloatToSBV NatRepr w
w RoundingMode
_ f (FloatType fi)
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    FloatToReal{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatIsNaN{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatIsInfinite{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatIsZero{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatIsPositive{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatIsNegative{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatIsSubnormal{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatIsNormal{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

    ----------------------------------------------------------------------
    -- Maybe

    JustValue TypeRepr tp
tp f tp
_ -> TypeRepr tp -> TypeRepr ('MaybeType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('MaybeType tp1)
MaybeRepr TypeRepr tp
tp
    NothingValue TypeRepr tp
tp -> TypeRepr tp -> TypeRepr ('MaybeType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('MaybeType tp1)
MaybeRepr TypeRepr tp
tp
    FromJustValue TypeRepr x
tp f (MaybeType x)
_ f (StringType Unicode)
_ -> TypeRepr x
tp

    ----------------------------------------------------------------------
    -- Recursive Types

    RollRecursive SymbolRepr nm
nm CtxRepr ctx
ctx f (UnrollType nm ctx)
_ -> SymbolRepr nm -> CtxRepr ctx -> TypeRepr ('RecursiveType nm ctx)
forall (nm :: Symbol) (ctx :: Ctx CrucibleType).
IsRecursiveType nm =>
SymbolRepr nm -> CtxRepr ctx -> TypeRepr ('RecursiveType nm ctx)
RecursiveRepr SymbolRepr nm
nm CtxRepr ctx
ctx
    UnrollRecursive SymbolRepr nm
nm CtxRepr ctx
ctx f (RecursiveType nm ctx)
_ -> SymbolRepr nm -> CtxRepr ctx -> TypeRepr (UnrollType nm ctx)
forall (nm :: Symbol) (ctx :: Ctx CrucibleType).
IsRecursiveType nm =>
SymbolRepr nm -> CtxRepr ctx -> TypeRepr (UnrollType nm ctx)
forall (ctx :: Ctx CrucibleType).
SymbolRepr nm -> CtxRepr ctx -> TypeRepr (UnrollType nm ctx)
unrollType SymbolRepr nm
nm CtxRepr ctx
ctx

    ----------------------------------------------------------------------
    -- Vector
    VectorIsEmpty{}          -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    VectorSize{}             -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    VectorLit       TypeRepr tp
tp Vector (f tp)
_     -> TypeRepr tp -> TypeRepr ('VectorType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('VectorType tp1)
VectorRepr TypeRepr tp
tp
    VectorReplicate TypeRepr tp
tp f 'NatType
_ f tp
_   -> TypeRepr tp -> TypeRepr ('VectorType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('VectorType tp1)
VectorRepr TypeRepr tp
tp
    VectorGetEntry  TypeRepr x
tp f (VectorType x)
_ f 'NatType
_   -> TypeRepr x
tp
    VectorSetEntry  TypeRepr tp
tp f ('VectorType tp)
_ f 'NatType
_ f tp
_ -> TypeRepr tp -> TypeRepr ('VectorType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('VectorType tp1)
VectorRepr TypeRepr tp
tp
    VectorCons      TypeRepr tp
tp f tp
_ f ('VectorType tp)
_   -> TypeRepr tp -> TypeRepr ('VectorType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('VectorType tp1)
VectorRepr TypeRepr tp
tp

    ----------------------------------------------------------------------
    -- Sequence
    SequenceNil TypeRepr tp
tpr -> TypeRepr tp -> TypeRepr ('SequenceType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('SequenceType tp1)
SequenceRepr TypeRepr tp
tpr
    SequenceCons TypeRepr tp
tpr f tp
_ f ('SequenceType tp)
_ -> TypeRepr tp -> TypeRepr ('SequenceType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('SequenceType tp1)
SequenceRepr TypeRepr tp
tpr
    SequenceAppend TypeRepr tp
tpr f ('SequenceType tp)
_ f ('SequenceType tp)
_ -> TypeRepr tp -> TypeRepr ('SequenceType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('SequenceType tp1)
SequenceRepr TypeRepr tp
tpr
    SequenceIsNil TypeRepr tp
_ f (SequenceType tp)
_ -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    SequenceHead TypeRepr tp
tpr f (SequenceType tp)
_ -> TypeRepr tp -> TypeRepr ('MaybeType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('MaybeType tp1)
MaybeRepr TypeRepr tp
tpr
    SequenceUncons TypeRepr tp
tpr f (SequenceType tp)
_ ->
      TypeRepr (StructType ((EmptyCtx ::> tp) ::> SequenceType tp))
-> TypeRepr
     ('MaybeType (StructType ((EmptyCtx ::> tp) ::> SequenceType tp)))
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('MaybeType tp1)
MaybeRepr (CtxRepr ((EmptyCtx ::> tp) ::> SequenceType tp)
-> TypeRepr (StructType ((EmptyCtx ::> tp) ::> SequenceType tp))
forall (ctx :: Ctx CrucibleType).
CtxRepr ctx -> TypeRepr ('StructType ctx)
StructRepr (Assignment TypeRepr EmptyCtx
forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment TypeRepr EmptyCtx
-> TypeRepr tp -> Assignment TypeRepr (EmptyCtx ::> tp)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> TypeRepr tp
tpr Assignment TypeRepr (EmptyCtx ::> tp)
-> TypeRepr (SequenceType tp)
-> CtxRepr ((EmptyCtx ::> tp) ::> SequenceType tp)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> TypeRepr tp -> TypeRepr (SequenceType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('SequenceType tp1)
SequenceRepr TypeRepr tp
tpr))
    SequenceLength{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    SequenceTail TypeRepr tp
tpr f (SequenceType tp)
_ -> TypeRepr (SequenceType tp)
-> TypeRepr ('MaybeType (SequenceType tp))
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('MaybeType tp1)
MaybeRepr (TypeRepr tp -> TypeRepr (SequenceType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('SequenceType tp1)
SequenceRepr TypeRepr tp
tpr)

    ----------------------------------------------------------------------
    -- SymbolicArrayType

    SymArrayLookup BaseTypeRepr b
b f (SymbolicArrayType (idx ::> tp) b)
_ Assignment (BaseTerm f) (idx ::> tp)
_ -> BaseTypeRepr b -> TypeRepr ('BaseToType b)
forall (bt :: BaseType).
BaseTypeRepr bt -> TypeRepr (BaseToType bt)
baseToType BaseTypeRepr b
b
    SymArrayUpdate BaseTypeRepr b
b f ('BaseToType (BaseArrayType (idx ::> itp) b))
_ Assignment (BaseTerm f) (idx ::> itp)
idx f (BaseToType b)
_ ->
      BaseTypeRepr (BaseArrayType (idx ::> itp) b)
-> TypeRepr ('BaseToType (BaseArrayType (idx ::> itp) b))
forall (bt :: BaseType).
BaseTypeRepr bt -> TypeRepr (BaseToType bt)
baseToType (Assignment BaseTypeRepr (idx ::> itp)
-> BaseTypeRepr b -> BaseTypeRepr (BaseArrayType (idx ::> itp) b)
forall (idx :: Ctx BaseType) (tp :: BaseType) (xs :: BaseType).
Assignment BaseTypeRepr (idx ::> tp)
-> BaseTypeRepr xs -> BaseTypeRepr ('BaseArrayType (idx ::> tp) xs)
BaseArrayRepr ((forall (x :: BaseType). BaseTerm f x -> BaseTypeRepr x)
-> forall (x :: Ctx BaseType).
   Assignment (BaseTerm f) x -> Assignment BaseTypeRepr x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: BaseType -> Type) (g :: BaseType -> Type).
(forall (x :: BaseType). f x -> g x)
-> forall (x :: Ctx BaseType). Assignment f x -> Assignment g x
fmapFC BaseTerm f x -> BaseTypeRepr x
forall (x :: BaseType). BaseTerm f x -> BaseTypeRepr x
forall (f :: CrucibleType -> Type) (tp :: BaseType).
BaseTerm f tp -> BaseTypeRepr tp
baseTermType Assignment (BaseTerm f) (idx ::> itp)
idx) BaseTypeRepr b
b)

    ----------------------------------------------------------------------
    -- WordMap
    EmptyWordMap NatRepr w
w BaseTypeRepr tp
tp -> NatRepr w -> BaseTypeRepr tp -> TypeRepr ('WordMapType w tp)
forall (n :: Natural) (tp1 :: BaseType).
(1 <= n) =>
NatRepr n -> BaseTypeRepr tp1 -> TypeRepr ('WordMapType n tp1)
WordMapRepr NatRepr w
w BaseTypeRepr tp
tp
    InsertWordMap NatRepr w
w BaseTypeRepr tp
tp f (BVType w)
_ f (BaseToType tp)
_ f ('WordMapType w tp)
_ -> NatRepr w -> BaseTypeRepr tp -> TypeRepr ('WordMapType w tp)
forall (n :: Natural) (tp1 :: BaseType).
(1 <= n) =>
NatRepr n -> BaseTypeRepr tp1 -> TypeRepr ('WordMapType n tp1)
WordMapRepr NatRepr w
w BaseTypeRepr tp
tp
    LookupWordMap BaseTypeRepr tp
tp f (BVType w)
_ f (WordMapType w tp)
_ -> BaseTypeRepr tp -> TypeRepr ('BaseToType tp)
forall (bt :: BaseType).
BaseTypeRepr bt -> TypeRepr (BaseToType bt)
baseToType BaseTypeRepr tp
tp
    LookupWordMapWithDefault BaseTypeRepr tp
tp f (BVType w)
_ f (WordMapType w tp)
_ f ('BaseToType tp)
_ -> BaseTypeRepr tp -> TypeRepr ('BaseToType tp)
forall (bt :: BaseType).
BaseTypeRepr bt -> TypeRepr (BaseToType bt)
baseToType BaseTypeRepr tp
tp

    ----------------------------------------------------------------------
    -- Handle

    HandleLit FnHandle args ret
h -> FnHandle args ret -> TypeRepr ('FunctionHandleType args ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> TypeRepr (FunctionHandleType args ret)
handleType FnHandle args ret
h
    Closure CtxRepr args
a TypeRepr ret
r f (FunctionHandleType (args ::> tp) ret)
_ TypeRepr tp
_ f tp
_ ->
      CtxRepr args
-> TypeRepr ret -> TypeRepr ('FunctionHandleType args ret)
forall (ctx :: Ctx CrucibleType) (ret :: CrucibleType).
CtxRepr ctx
-> TypeRepr ret -> TypeRepr ('FunctionHandleType ctx ret)
FunctionHandleRepr CtxRepr args
a TypeRepr ret
r

    ----------------------------------------------------------------------
    -- Conversions
    NatToInteger{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    IntegerToReal{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealToNat{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealRound{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealFloor{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealCeil{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    IntegerToBV NatRepr w
w f IntegerType
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w

    ----------------------------------------------------------------------
    -- ComplexReal
    Complex{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealPart{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    ImagPart{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

    ----------------------------------------------------------------------
    -- BV
    BVUndef NatRepr w
w -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVLit NatRepr w
w BV w
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVTrunc NatRepr r
w NatRepr w
_ f (BVType w)
_ -> NatRepr r -> TypeRepr ('BaseToType (BaseBVType r))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr r
w
    BVZext NatRepr r
w NatRepr w
_ f (BVType w)
_ -> NatRepr r -> TypeRepr ('BaseToType (BaseBVType r))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr r
w
    BVSext NatRepr r
w NatRepr w
_ f (BVType w)
_ -> NatRepr r -> TypeRepr ('BaseToType (BaseBVType r))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr r
w

    BVNot NatRepr w
w f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVAnd NatRepr w
w f ('BaseToType (BaseBVType w))
_ f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVOr  NatRepr w
w f ('BaseToType (BaseBVType w))
_ f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVXor  NatRepr w
w f ('BaseToType (BaseBVType w))
_ f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVNeg NatRepr w
w f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVAdd NatRepr w
w f ('BaseToType (BaseBVType w))
_ f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVSub NatRepr w
w f ('BaseToType (BaseBVType w))
_ f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVMul NatRepr w
w f ('BaseToType (BaseBVType w))
_ f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVUdiv NatRepr w
w f ('BaseToType (BaseBVType w))
_ f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVSdiv NatRepr w
w f ('BaseToType (BaseBVType w))
_ f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVUrem NatRepr w
w f ('BaseToType (BaseBVType w))
_ f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVSrem NatRepr w
w f ('BaseToType (BaseBVType w))
_ f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVUle{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    BVUlt{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    BVSle{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    BVSlt{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    BVCarry{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    BVSCarry{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    BVSBorrow{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    BVShl NatRepr w
w f ('BaseToType (BaseBVType w))
_ f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVLshr NatRepr w
w f ('BaseToType (BaseBVType w))
_ f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVAshr NatRepr w
w f ('BaseToType (BaseBVType w))
_ f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVRol NatRepr w
w f ('BaseToType (BaseBVType w))
_ f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVRor NatRepr w
w f ('BaseToType (BaseBVType w))
_ f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVCountTrailingZeros NatRepr w
w f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVCountLeadingZeros NatRepr w
w f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVPopcount NatRepr w
w f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVUMax NatRepr w
w f ('BaseToType (BaseBVType w))
_ f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVUMin NatRepr w
w f ('BaseToType (BaseBVType w))
_ f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVSMax NatRepr w
w f ('BaseToType (BaseBVType w))
_ f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BVSMin NatRepr w
w f ('BaseToType (BaseBVType w))
_ f ('BaseToType (BaseBVType w))
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w

    BoolToBV NatRepr w
w f BoolType
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
    BvToNat{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    BvToInteger{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    SbvToInteger{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    BVNonzero{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    BVSelect NatRepr idx
_ NatRepr len
n NatRepr w
_ f (BVType w)
_ -> NatRepr len -> TypeRepr ('BaseToType (BaseBVType len))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr len
n
    BVConcat NatRepr u
w1 NatRepr v
w2 f (BVType u)
_ f (BVType v)
_ -> NatRepr (u + v) -> TypeRepr ('BaseToType (BaseBVType (u + v)))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr (NatRepr u -> NatRepr v -> NatRepr (u + v)
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr u
w1 NatRepr v
w2)

    ----------------------------------------------------------------------
    -- Struct

    MkStruct CtxRepr ctx
ctx Assignment f ctx
_ -> CtxRepr ctx -> TypeRepr ('StructType ctx)
forall (ctx :: Ctx CrucibleType).
CtxRepr ctx -> TypeRepr ('StructType ctx)
StructRepr CtxRepr ctx
ctx
    GetStruct f (StructType ctx)
_ Index ctx x
_ TypeRepr x
tp -> TypeRepr x
tp
    SetStruct CtxRepr ctx
ctx f ('StructType ctx)
_ Index ctx tp
_ f tp
_ -> CtxRepr ctx -> TypeRepr ('StructType ctx)
forall (ctx :: Ctx CrucibleType).
CtxRepr ctx -> TypeRepr ('StructType ctx)
StructRepr CtxRepr ctx
ctx

    ----------------------------------------------------------------------
    -- Variants

    InjectVariant CtxRepr ctx
ctx Index ctx tp
_ f tp
_ -> CtxRepr ctx -> TypeRepr ('VariantType ctx)
forall (ctx :: Ctx CrucibleType).
CtxRepr ctx -> TypeRepr ('VariantType ctx)
VariantRepr CtxRepr ctx
ctx
    ProjectVariant CtxRepr ctx
ctx Index ctx tp
idx f (VariantType ctx)
_ -> TypeRepr tp -> TypeRepr ('MaybeType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('MaybeType tp1)
MaybeRepr (CtxRepr ctx
ctx CtxRepr ctx -> Index ctx tp -> TypeRepr tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
idx)

    ----------------------------------------------------------------------
    -- StringMap
    EmptyStringMap TypeRepr tp
tp             -> TypeRepr tp -> TypeRepr ('StringMapType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('StringMapType tp1)
StringMapRepr TypeRepr tp
tp
    LookupStringMapEntry TypeRepr tp
tp f (StringMapType tp)
_ f (StringType Unicode)
_   -> TypeRepr tp -> TypeRepr ('MaybeType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('MaybeType tp1)
MaybeRepr TypeRepr tp
tp
    InsertStringMapEntry TypeRepr tp
tp f ('StringMapType tp)
_ f (StringType Unicode)
_ f (MaybeType tp)
_ -> TypeRepr tp -> TypeRepr ('StringMapType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('StringMapType tp1)
StringMapRepr TypeRepr tp
tp

    ----------------------------------------------------------------------
    -- String

    StringLit StringLiteral si
s -> StringInfoRepr si -> TypeRepr ('BaseToType (BaseStringType si))
forall (si :: StringInfo).
StringInfoRepr si -> TypeRepr ('BaseToType (BaseStringType si))
StringRepr (StringLiteral si -> StringInfoRepr si
forall (si :: StringInfo). StringLiteral si -> StringInfoRepr si
stringLiteralInfo StringLiteral si
s)
    ShowValue{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    ShowFloat{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    StringConcat StringInfoRepr si
si f ('BaseToType (BaseStringType si))
_ f ('BaseToType (BaseStringType si))
_ -> StringInfoRepr si -> TypeRepr ('BaseToType (BaseStringType si))
forall (si :: StringInfo).
StringInfoRepr si -> TypeRepr ('BaseToType (BaseStringType si))
StringRepr StringInfoRepr si
si
    StringEmpty StringInfoRepr si
si -> StringInfoRepr si -> TypeRepr ('BaseToType (BaseStringType si))
forall (si :: StringInfo).
StringInfoRepr si -> TypeRepr ('BaseToType (BaseStringType si))
StringRepr StringInfoRepr si
si
    StringLength f (StringType si)
_ -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    StringContains{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    StringIsPrefixOf{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    StringIsSuffixOf{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    StringIndexOf{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    StringSubstring StringInfoRepr si
si f ('BaseToType (BaseStringType si))
_ f IntegerType
_ f IntegerType
_ -> StringInfoRepr si -> TypeRepr ('BaseToType (BaseStringType si))
forall (si :: StringInfo).
StringInfoRepr si -> TypeRepr ('BaseToType (BaseStringType si))
StringRepr StringInfoRepr si
si

    ------------------------------------------------------------------------
    -- Introspection

    IsConcrete BaseTypeRepr b
_ f (BaseToType b)
_ -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

    ------------------------------------------------------------------------
    -- References

    ReferenceEq{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr


----------------------------------------------------------------------------
-- Utility operations

testFnHandle :: FnHandle a1 r1 -> FnHandle a2 r2 -> Maybe (FnHandle a1 r1 :~: FnHandle a2 r2)
testFnHandle :: forall (a1 :: Ctx CrucibleType) (r1 :: CrucibleType)
       (a2 :: Ctx CrucibleType) (r2 :: CrucibleType).
FnHandle a1 r1
-> FnHandle a2 r2 -> Maybe (FnHandle a1 r1 :~: FnHandle a2 r2)
testFnHandle FnHandle a1 r1
x FnHandle a2 r2
y = do
  (a1 ::> r1) :~: (a2 ::> r2)
Refl <- Nonce GlobalNonceGenerator (a1 ::> r1)
-> Nonce GlobalNonceGenerator (a2 ::> r2)
-> Maybe ((a1 ::> r1) :~: (a2 ::> r2))
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Ctx CrucibleType) (b :: Ctx CrucibleType).
Nonce GlobalNonceGenerator a
-> Nonce GlobalNonceGenerator b -> Maybe (a :~: b)
testEquality (FnHandle a1 r1 -> Nonce GlobalNonceGenerator (a1 ::> r1)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
handleID FnHandle a1 r1
x) (FnHandle a2 r2 -> Nonce GlobalNonceGenerator (a2 ::> r2)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
handleID FnHandle a2 r2
y)
  (FnHandle a1 r1 :~: FnHandle a2 r2)
-> Maybe (FnHandle a1 r1 :~: FnHandle a2 r2)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return FnHandle a1 r1 :~: FnHandle a1 r1
FnHandle a1 r1 :~: FnHandle a2 r2
forall {k} (a :: k). a :~: a
Refl

compareFnHandle :: FnHandle a1 r1
                -> FnHandle a2 r2
                -> OrderingF (FnHandle a1 r1) (FnHandle a2 r2)
compareFnHandle :: forall (a1 :: Ctx CrucibleType) (r1 :: CrucibleType)
       (a2 :: Ctx CrucibleType) (r2 :: CrucibleType).
FnHandle a1 r1
-> FnHandle a2 r2 -> OrderingF (FnHandle a1 r1) (FnHandle a2 r2)
compareFnHandle FnHandle a1 r1
x FnHandle a2 r2
y = do
  case Nonce GlobalNonceGenerator (a1 ::> r1)
-> Nonce GlobalNonceGenerator (a2 ::> r2)
-> OrderingF (a1 ::> r1) (a2 ::> r2)
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: Ctx CrucibleType) (y :: Ctx CrucibleType).
Nonce GlobalNonceGenerator x
-> Nonce GlobalNonceGenerator y -> OrderingF x y
compareF (FnHandle a1 r1 -> Nonce GlobalNonceGenerator (a1 ::> r1)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
handleID FnHandle a1 r1
x) (FnHandle a2 r2 -> Nonce GlobalNonceGenerator (a2 ::> r2)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
handleID FnHandle a2 r2
y) of
    OrderingF (a1 ::> r1) (a2 ::> r2)
LTF -> OrderingF (FnHandle a1 r1) (FnHandle a2 r2)
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
    OrderingF (a1 ::> r1) (a2 ::> r2)
GTF -> OrderingF (FnHandle a1 r1) (FnHandle a2 r2)
forall {k} (x :: k) (y :: k). OrderingF x y
GTF
    OrderingF (a1 ::> r1) (a2 ::> r2)
EQF -> OrderingF (FnHandle a1 r1) (FnHandle a1 r1)
OrderingF (FnHandle a1 r1) (FnHandle a2 r2)
forall {k} (x :: k). OrderingF x x
EQF

testVector :: (forall x y. f x -> f y -> Maybe (x :~: y))
           -> Vector (f tp) -> Vector (f tp) -> Maybe (Int :~: Int)
testVector :: forall {k} (f :: k -> Type) (tp :: k).
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> Vector (f tp) -> Vector (f tp) -> Maybe (Int :~: Int)
testVector forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
testF Vector (f tp)
x Vector (f tp)
y = do
  case (f tp -> f tp -> Maybe (tp :~: tp))
-> Vector (f tp) -> Vector (f tp) -> Maybe ()
forall (m :: Type -> Type) a b c.
Monad m =>
(a -> b -> m c) -> Vector a -> Vector b -> m ()
V.zipWithM_ f tp -> f tp -> Maybe (tp :~: tp)
forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
testF Vector (f tp)
x Vector (f tp)
y of
    Just () -> (Int :~: Int) -> Maybe (Int :~: Int)
forall a. a -> Maybe a
Just Int :~: Int
forall {k} (a :: k). a :~: a
Refl
    Maybe ()
Nothing -> Maybe (Int :~: Int)
forall a. Maybe a
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 :: forall {k} (f :: k -> Type) (tp :: k).
(forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> Vector (f tp) -> Vector (f tp) -> OrderingF Int Int
compareVector forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
cmpF Vector (f tp)
x Vector (f tp)
y
    | Vector (f tp) -> Int
forall a. Vector a -> Int
V.length Vector (f tp)
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Vector (f tp) -> Int
forall a. Vector a -> Int
V.length Vector (f tp)
y = OrderingF Int Int
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
    | Vector (f tp) -> Int
forall a. Vector a -> Int
V.length Vector (f tp)
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Vector (f tp) -> Int
forall a. Vector a -> Int
V.length Vector (f tp)
y = OrderingF Int Int
forall {k} (x :: k) (y :: k). OrderingF x y
GTF
    | Bool
otherwise = ((f tp, f tp) -> OrderingF Int Int -> OrderingF Int Int)
-> OrderingF Int Int -> Vector (f tp, f tp) -> OrderingF Int Int
forall a b. (a -> b -> b) -> b -> Vector a -> b
V.foldr (f tp, f tp) -> OrderingF Int Int -> OrderingF Int Int
forall (z :: k).
(f z, f z) -> OrderingF Int Int -> OrderingF Int Int
go OrderingF Int Int
forall {k} (x :: k). OrderingF x x
EQF (Vector (f tp) -> Vector (f tp) -> Vector (f tp, f tp)
forall a b. Vector a -> Vector b -> Vector (a, b)
V.zip Vector (f tp)
x Vector (f tp)
y)
  where go :: forall z. (f z, f z) -> OrderingF Int Int -> OrderingF Int Int
        go :: forall (z :: k).
(f z, f z) -> OrderingF Int Int -> OrderingF Int Int
go (f z
u,f z
v) OrderingF Int Int
r =
          case f z -> f z -> OrderingF z z
forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
cmpF f z
u f z
v of
            OrderingF z z
LTF -> OrderingF Int Int
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
            OrderingF z z
GTF -> OrderingF Int Int
forall {k} (x :: k) (y :: k). OrderingF x y
GTF
            OrderingF z z
EQF -> OrderingF Int Int
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 :: forall (f :: CrucibleType -> Type) ann (ctx :: Ctx BaseType).
(forall (u :: CrucibleType). f u -> Doc ann)
-> Assignment (BaseTerm f) ctx -> Doc ann
ppBaseTermAssignment forall (u :: CrucibleType). f u -> Doc ann
pp Assignment (BaseTerm f) ctx
v = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
brackets ([Doc ann] -> Doc ann
forall (f :: Type -> Type) ann.
Foldable f =>
f (Doc ann) -> Doc ann
commas ((forall (x :: BaseType). BaseTerm f x -> Doc ann)
-> forall (x :: Ctx BaseType).
   Assignment (BaseTerm f) x -> [Doc ann]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
forall (f :: BaseType -> Type) a.
(forall (x :: BaseType). f x -> a)
-> forall (x :: Ctx BaseType). Assignment f x -> [a]
toListFC (f (BaseToType x) -> Doc ann
forall (u :: CrucibleType). f u -> Doc ann
pp (f (BaseToType x) -> Doc ann)
-> (BaseTerm f x -> f (BaseToType x)) -> BaseTerm f x -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BaseTerm f x -> f (BaseToType x)
forall (f :: CrucibleType -> Type) (tp :: BaseType).
BaseTerm f tp -> f (BaseToType tp)
baseTermVal) Assignment (BaseTerm f) ctx
v))

instance PrettyApp (ExprExtension ext) => PrettyApp (App ext) where
  --ppApp :: (forall a . f a -> Doc ann) -> App ext f b -> Doc ann
  ppApp :: forall (f :: CrucibleType -> Type) ann.
(forall (x :: CrucibleType). f x -> Doc ann)
-> forall (x :: CrucibleType). App ext f x -> 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 :: forall (m :: Type -> Type) (f :: CrucibleType -> Type)
       (g :: CrucibleType -> Type) (x :: Ctx BaseType).
Applicative m =>
(forall (tp :: CrucibleType). f tp -> m (g tp))
-> Assignment (BaseTerm f) x -> m (Assignment (BaseTerm g) x)
traverseBaseTerm forall (tp :: CrucibleType). f tp -> m (g tp)
f = (forall (x :: BaseType). BaseTerm f x -> m (BaseTerm g x))
-> forall (x :: Ctx BaseType).
   Assignment (BaseTerm f) x -> m (Assignment (BaseTerm g) x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: BaseType -> Type) (g :: BaseType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: BaseType). f x -> m (g x))
-> forall (x :: Ctx BaseType). Assignment f x -> m (Assignment g x)
traverseFC ((forall (tp :: CrucibleType). f tp -> m (g tp))
-> forall (x :: BaseType). BaseTerm f x -> m (BaseTerm g x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: BaseType). BaseTerm f x -> m (BaseTerm g x)
traverseFC f x -> m (g x)
forall (tp :: CrucibleType). f tp -> m (g tp)
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 :: forall ext (m :: Type -> Type) (f :: CrucibleType -> Type)
       (g :: CrucibleType -> Type) (tp :: CrucibleType).
(TraversableFC (ExprExtension ext), Applicative m) =>
(forall (u :: CrucibleType). 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 :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
 f x -> f y -> Maybe (x :~: y))
-> forall (x :: CrucibleType) (y :: CrucibleType).
   App ext f x -> App ext f y -> Maybe (x :~: y)
testEqualityFC forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y)
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 :: forall (a :: CrucibleType) (b :: CrucibleType).
App ext f a -> App ext f b -> Maybe (a :~: b)
testEquality = (forall (x :: CrucibleType) (y :: CrucibleType).
 f x -> f y -> Maybe (x :~: y))
-> forall (a :: CrucibleType) (b :: CrucibleType).
   App ext f a -> App ext f b -> Maybe (a :~: b)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type).
TestEqualityFC t =>
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> forall (x :: l) (y :: l). t f x -> t f y -> Maybe (x :~: y)
forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
 f x -> f y -> Maybe (x :~: y))
-> forall (x :: CrucibleType) (y :: CrucibleType).
   App ext f x -> App ext f y -> Maybe (x :~: y)
testEqualityFC f x -> f y -> Maybe (x :~: y)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y)
testEquality

instance ( OrdFC (ExprExtension ext)
         ) => OrdFC (App ext) where
  compareFC :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
 f x -> f y -> OrderingF x y)
-> forall (x :: CrucibleType) (y :: CrucibleType).
   App ext f x -> App ext f y -> OrderingF x y
compareFC forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> OrderingF x y
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 :: forall (x :: CrucibleType) (y :: CrucibleType).
App ext f x -> App ext f y -> OrderingF x y
compareF = (forall (x :: CrucibleType) (y :: CrucibleType).
 f x -> f y -> OrderingF x y)
-> forall (x :: CrucibleType) (y :: CrucibleType).
   App ext f x -> App ext f y -> OrderingF x y
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type).
OrdFC t =>
(forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> forall (x :: l) (y :: l). t f x -> t f y -> OrderingF x y
forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
 f x -> f y -> OrderingF x y)
-> forall (x :: CrucibleType) (y :: CrucibleType).
   App ext f x -> App ext f y -> OrderingF x y
compareFC f x -> f y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> OrderingF x y
compareF

-------------------------------------------------------------------------------------
-- Traversals and such

instance ( TraversableFC (ExprExtension ext)
         ) => FunctorFC (App ext) where
  fmapFC :: forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: CrucibleType). App ext f x -> App ext g x
fmapFC = (forall (x :: CrucibleType). f x -> g x)
-> App ext f x -> App ext g x
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: CrucibleType). App ext f x -> App ext g x
forall {k} {l} (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
TraversableFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: CrucibleType). App ext f x -> App ext g x
fmapFCDefault

instance ( TraversableFC (ExprExtension ext)
         ) => FoldableFC (App ext) where
  foldMapFC :: forall (f :: CrucibleType -> Type) m.
Monoid m =>
(forall (x :: CrucibleType). f x -> m)
-> forall (x :: CrucibleType). App ext f x -> m
foldMapFC = (forall (x :: CrucibleType). f x -> m) -> App ext f x -> m
(forall (x :: CrucibleType). f x -> m)
-> forall (x :: CrucibleType). App ext f x -> m
forall {k} {l} (t :: (k -> Type) -> l -> Type) m (f :: k -> Type).
(TraversableFC t, Monoid m) =>
(forall (x :: k). f x -> m) -> forall (x :: l). t f x -> m
foldMapFCDefault

instance ( TraversableFC (ExprExtension ext)
         ) => TraversableFC (App ext) where
  traverseFC :: forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: CrucibleType). App ext f x -> m (App ext g x)
traverseFC forall (x :: CrucibleType). f x -> m (g x)
f = (forall (x :: CrucibleType). f x -> m (g x))
-> App ext f x -> m (App ext g x)
forall ext (m :: Type -> Type) (f :: CrucibleType -> Type)
       (g :: CrucibleType -> Type) (tp :: CrucibleType).
(TraversableFC (ExprExtension ext), Applicative m) =>
(forall (u :: CrucibleType). f u -> m (g u))
-> App ext f tp -> m (App ext g tp)
traverseApp f u -> m (g u)
forall (x :: CrucibleType). f x -> m (g x)
f

-- | Fold over an application.
foldApp :: ( TraversableFC (ExprExtension ext)
           )
        => (forall x . f x -> r -> r)
        -> r
        -> App ext f tp
        -> r
foldApp :: forall ext (f :: CrucibleType -> Type) r (tp :: CrucibleType).
TraversableFC (ExprExtension ext) =>
(forall (x :: CrucibleType). f x -> r -> r)
-> r -> App ext f tp -> r
foldApp forall (x :: CrucibleType). f x -> r -> r
f0 r
r0 App ext f tp
a = State r (App ext f tp) -> r -> r
forall s a. State s a -> s -> s
execState ((forall (u :: CrucibleType). f u -> StateT r Identity (f u))
-> App ext f tp -> State r (App ext f tp)
forall ext (m :: Type -> Type) (f :: CrucibleType -> Type)
       (g :: CrucibleType -> Type) (tp :: CrucibleType).
(TraversableFC (ExprExtension ext), Applicative m) =>
(forall (u :: CrucibleType). f u -> m (g u))
-> App ext f tp -> m (App ext g tp)
traverseApp ((f u -> r -> r) -> f u -> StateT r Identity (f u)
forall {f :: Type -> Type} {s} {t}.
MonadState s f =>
(t -> s -> s) -> t -> f t
go f u -> r -> r
forall (x :: CrucibleType). f x -> r -> r
f0) App ext f tp
a) r
r0
  where go :: (t -> s -> s) -> t -> f t
go t -> s -> s
f t
v = t
v t -> f () -> f t
forall a b. a -> f b -> f a
forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
<$ (s -> s) -> f ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify (t -> s -> s
f t
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 :: forall ext (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (tp :: CrucibleType).
TraversableFC (ExprExtension ext) =>
(forall (u :: CrucibleType). f u -> g u)
-> App ext f tp -> App ext g tp
mapApp forall (u :: CrucibleType). f u -> g u
f App ext f tp
a = Identity (App ext g tp) -> App ext g tp
forall a. Identity a -> a
runIdentity ((forall (u :: CrucibleType). f u -> Identity (g u))
-> App ext f tp -> Identity (App ext g tp)
forall ext (m :: Type -> Type) (f :: CrucibleType -> Type)
       (g :: CrucibleType -> Type) (tp :: CrucibleType).
(TraversableFC (ExprExtension ext), Applicative m) =>
(forall (u :: CrucibleType). f u -> m (g u))
-> App ext f tp -> m (App ext g tp)
traverseApp (g u -> Identity (g u)
forall a. a -> Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (g u -> Identity (g u)) -> (f u -> g u) -> f u -> Identity (g u)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f u -> g u
forall (u :: CrucibleType). f u -> g u
f) App ext f tp
a)