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