what4-1.0: Solver-agnostic symbolic values support for issuing queries

Copyright(c) Galois Inc 2014-2020
LicenseBSD3
MaintainerJoe Hendrix <jhendrix@galois.com>
Stabilityprovisional
Safe HaskellNone
LanguageHaskell2010

What4.BaseTypes

Contents

Description

This module exports the types used in solver expressions.

These types are largely used as indexes to various GADTs and type families as a way to let the GHC typechecker help us keep expressions used by solvers apart.

In addition, we provide a value-level reification of the type indices that can be examined by pattern matching, called BaseTypeRepr.

Synopsis

BaseType data kind

data BaseType Source #

This data kind enumerates the Crucible solver interface types, which are types that may be represented symbolically.

Instances
TestEquality BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

testEquality :: BaseTypeRepr a -> BaseTypeRepr b -> Maybe (a :~: b) #

TestEquality IndexLit Source # 
Instance details

Defined in What4.IndexLit

Methods

testEquality :: IndexLit a -> IndexLit b -> Maybe (a :~: b) #

TestEquality OnlyNatRepr Source # 
Instance details

Defined in What4.Utils.OnlyNatRepr

Methods

testEquality :: OnlyNatRepr a -> OnlyNatRepr b -> Maybe (a :~: b) #

TestEquality ConcreteVal Source # 
Instance details

Defined in What4.Concrete

Methods

testEquality :: ConcreteVal a -> ConcreteVal b -> Maybe (a :~: b) #

TestEquality TypeMap Source # 
Instance details

Defined in What4.Protocol.SMTWriter

Methods

testEquality :: TypeMap a -> TypeMap b -> Maybe (a :~: b) #

OrdF BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

OrdF IndexLit Source # 
Instance details

Defined in What4.IndexLit

Methods

compareF :: IndexLit x -> IndexLit y -> OrderingF x y #

leqF :: IndexLit x -> IndexLit y -> Bool #

ltF :: IndexLit x -> IndexLit y -> Bool #

geqF :: IndexLit x -> IndexLit y -> Bool #

gtF :: IndexLit x -> IndexLit y -> Bool #

OrdF ConcreteVal Source # 
Instance details

Defined in What4.Concrete

ShowF BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

withShow :: p BaseTypeRepr -> q tp -> (Show (BaseTypeRepr tp) -> a) -> a #

showF :: BaseTypeRepr tp -> String #

showsPrecF :: Int -> BaseTypeRepr tp -> String -> String #

ShowF IndexLit Source # 
Instance details

Defined in What4.IndexLit

Methods

withShow :: p IndexLit -> q tp -> (Show (IndexLit tp) -> a) -> a #

showF :: IndexLit tp -> String #

showsPrecF :: Int -> IndexLit tp -> String -> String #

ShowF ConcreteVal Source # 
Instance details

Defined in What4.Concrete

Methods

withShow :: p ConcreteVal -> q tp -> (Show (ConcreteVal tp) -> a) -> a #

showF :: ConcreteVal tp -> String #

showsPrecF :: Int -> ConcreteVal tp -> String -> String #

ShowF TypeMap Source # 
Instance details

Defined in What4.Protocol.SMTWriter

Methods

withShow :: p TypeMap -> q tp -> (Show (TypeMap tp) -> a) -> a #

showF :: TypeMap tp -> String #

showsPrecF :: Int -> TypeMap tp -> String -> String #

HashableF BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

HashableF IndexLit Source # 
Instance details

Defined in What4.IndexLit

Methods

hashWithSaltF :: Int -> IndexLit tp -> Int #

hashF :: IndexLit tp -> Int #

HashableF OnlyNatRepr Source # 
Instance details

Defined in What4.Utils.OnlyNatRepr

Methods

hashWithSaltF :: Int -> OnlyNatRepr tp -> Int #

hashF :: OnlyNatRepr tp -> Int #

FoldableFC App Source # 
Instance details

Defined in What4.Expr.App

Methods

foldMapFC :: Monoid m => (forall (x :: k). f x -> m) -> forall (x :: l). App f x -> m #

foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> App f x -> b #

foldlFC :: (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> App f x -> b #

foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> App f x -> b #

foldlFC' :: (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> App f x -> b #

toListFC :: (forall (x :: k). f x -> a) -> forall (x :: l). App f x -> [a] #

KnownRepr BaseTypeRepr BaseComplexType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseRealType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseNatType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseIntegerType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseBoolType Source # 
Instance details

Defined in What4.BaseTypes

FunctorFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

fmapFC :: (forall (x :: k). f x -> g x) -> forall (x :: l). NonceApp t f x -> NonceApp t g x #

FoldableFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

foldMapFC :: Monoid m => (forall (x :: k). f x -> m) -> forall (x :: l). NonceApp t f x -> m #

foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> NonceApp t f x -> b #

foldlFC :: (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> NonceApp t f x -> b #

foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> NonceApp t f x -> b #

foldlFC' :: (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> NonceApp t f x -> b #

toListFC :: (forall (x :: k). f x -> a) -> forall (x :: l). NonceApp t f x -> [a] #

TraversableFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

traverseFC :: Applicative m => (forall (x :: k). f x -> m (g x)) -> forall (x :: l). NonceApp t f x -> m (NonceApp t g x) #

KnownRepr (Assignment BaseTypeRepr) ctx => KnownRepr BaseTypeRepr (BaseStructType ctx :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr StringInfoRepr si => KnownRepr BaseTypeRepr (BaseStringType si :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr FloatPrecisionRepr fpp => KnownRepr BaseTypeRepr (BaseFloatType fpp :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

(1 <= w, KnownNat w) => KnownRepr BaseTypeRepr (BaseBVType w :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

(KnownRepr (Assignment BaseTypeRepr) idx, KnownRepr BaseTypeRepr tp, KnownRepr BaseTypeRepr t) => KnownRepr BaseTypeRepr (BaseArrayType (idx ::> tp) t :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseArrayType (idx ::> tp) t) #

(Eq (e BaseBoolType), Eq (e BaseRealType), HashableF e, HasAbsValue e, OrdF e) => TestEquality (App e :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

testEquality :: App e a -> App e b -> Maybe (a :~: b) #

TestEquality (ExprBoundVar t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

testEquality :: ExprBoundVar t a -> ExprBoundVar t b -> Maybe (a :~: b) #

TestEquality (Expr t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.Builder

Methods

testEquality :: Expr t a -> Expr t b -> Maybe (a :~: b) #

TestEquality (NonceAppExpr t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.Builder

Methods

testEquality :: NonceAppExpr t a -> NonceAppExpr t b -> Maybe (a :~: b) #

OrdF (ExprBoundVar t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

compareF :: ExprBoundVar t x -> ExprBoundVar t y -> OrderingF x y #

leqF :: ExprBoundVar t x -> ExprBoundVar t y -> Bool #

ltF :: ExprBoundVar t x -> ExprBoundVar t y -> Bool #

geqF :: ExprBoundVar t x -> ExprBoundVar t y -> Bool #

gtF :: ExprBoundVar t x -> ExprBoundVar t y -> Bool #

OrdF (Expr t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.Builder

Methods

compareF :: Expr t x -> Expr t y -> OrderingF x y #

leqF :: Expr t x -> Expr t y -> Bool #

ltF :: Expr t x -> Expr t y -> Bool #

geqF :: Expr t x -> Expr t y -> Bool #

gtF :: Expr t x -> Expr t y -> Bool #

OrdF (NonceAppExpr t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.Builder

Methods

compareF :: NonceAppExpr t x -> NonceAppExpr t y -> OrderingF x y #

leqF :: NonceAppExpr t x -> NonceAppExpr t y -> Bool #

ltF :: NonceAppExpr t x -> NonceAppExpr t y -> Bool #

geqF :: NonceAppExpr t x -> NonceAppExpr t y -> Bool #

gtF :: NonceAppExpr t x -> NonceAppExpr t y -> Bool #

ShowF (ExprBoundVar t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

withShow :: p (ExprBoundVar t) -> q tp -> (Show (ExprBoundVar t tp) -> a) -> a #

showF :: ExprBoundVar t tp -> String #

showsPrecF :: Int -> ExprBoundVar t tp -> String -> String #

ShowF (Expr t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.Builder

Methods

withShow :: p (Expr t) -> q tp -> (Show (Expr t tp) -> a) -> a #

showF :: Expr t tp -> String #

showsPrecF :: Int -> Expr t tp -> String -> String #

(OrdF e, HashableF e, HasAbsValue e, Hashable (e BaseBoolType), Hashable (e BaseRealType)) => HashableF (App e :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

hashWithSaltF :: Int -> App e tp -> Int #

hashF :: App e tp -> Int #

HashableF (ExprBoundVar t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

hashWithSaltF :: Int -> ExprBoundVar t tp -> Int #

hashF :: ExprBoundVar t tp -> Int #

HashableF (Expr t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.Builder

Methods

hashWithSaltF :: Int -> Expr t tp -> Int #

hashF :: Expr t tp -> Int #

TestEquality f => TestEquality (ArrayResultWrapper f idx :: BaseType -> Type) Source # 
Instance details

Defined in What4.Interface

Methods

testEquality :: ArrayResultWrapper f idx a -> ArrayResultWrapper f idx b -> Maybe (a :~: b) #

TestEquality e => TestEquality (NonceApp t e :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

testEquality :: NonceApp t e a -> NonceApp t e b -> Maybe (a :~: b) #

HashableF e => HashableF (ArrayResultWrapper e idx :: BaseType -> Type) Source # 
Instance details

Defined in What4.Interface

Methods

hashWithSaltF :: Int -> ArrayResultWrapper e idx tp -> Int #

hashF :: ArrayResultWrapper e idx tp -> Int #

HashableF e => HashableF (NonceApp t e :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

hashWithSaltF :: Int -> NonceApp t e tp -> Int #

hashF :: NonceApp t e tp -> Int #

Constructors for kind BaseType

type BaseBoolType Source #

Arguments

 = BaseBoolType

:: BaseType.

type BaseIntegerType Source #

Arguments

 = BaseIntegerType

:: BaseType.

type BaseNatType Source #

Arguments

 = BaseNatType

:: BaseType.

type BaseRealType Source #

Arguments

 = BaseRealType

:: BaseType.

type BaseStringType Source #

Arguments

 = BaseStringType

:: BaseType.

type BaseBVType Source #

Arguments

 = BaseBVType

:: Nat -> BaseType.

type BaseFloatType Source #

Arguments

 = BaseFloatType

:: FloatPrecision -> BaseType.

type BaseComplexType Source #

Arguments

 = BaseComplexType

:: BaseType.

type BaseStructType Source #

Arguments

 = BaseStructType

:: Ctx BaseType -> BaseType.

type BaseArrayType Source #

Arguments

 = BaseArrayType

:: Ctx BaseType -> BaseType -> BaseType.

StringInfo data kind

data StringInfo Source #

Instances
TestEquality StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

TestEquality StringLiteral Source # 
Instance details

Defined in What4.Utils.StringLiteral

OrdF StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

OrdF StringLiteral Source # 
Instance details

Defined in What4.Utils.StringLiteral

ShowF StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

withShow :: p StringInfoRepr -> q tp -> (Show (StringInfoRepr tp) -> a) -> a #

showF :: StringInfoRepr tp -> String #

showsPrecF :: Int -> StringInfoRepr tp -> String -> String #

ShowF StringLiteral Source # 
Instance details

Defined in What4.Utils.StringLiteral

Methods

withShow :: p StringLiteral -> q tp -> (Show (StringLiteral tp) -> a) -> a #

showF :: StringLiteral tp -> String #

showsPrecF :: Int -> StringLiteral tp -> String -> String #

HashableF StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

HashableF StringLiteral Source # 
Instance details

Defined in What4.Utils.StringLiteral

KnownRepr StringInfoRepr Unicode Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr StringInfoRepr Char16 Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr StringInfoRepr Char8 Source # 
Instance details

Defined in What4.BaseTypes

(TestEquality e, HasAbsValue e, HashableF e) => TestEquality (StringSeq e :: StringInfo -> Type) Source # 
Instance details

Defined in What4.Expr.StringSeq

Methods

testEquality :: StringSeq e a -> StringSeq e b -> Maybe (a :~: b) #

(HasAbsValue e, HashableF e) => HashableF (StringSeq e :: StringInfo -> Type) Source # 
Instance details

Defined in What4.Expr.StringSeq

Methods

hashWithSaltF :: Int -> StringSeq e tp -> Int #

hashF :: StringSeq e tp -> Int #

Constructors for StringInfo

type Char8 Source #

Arguments

 = Char8

:: StringInfo.

type Char16 Source #

Arguments

 = Char16

:: StringInfo.

type Unicode Source #

Arguments

 = Unicode

:: StringInfo.

FloatPrecision data kind

data FloatPrecision Source #

This data kind describes the types of floating-point formats. This consist of the standard IEEE 754-2008 binary floating point formats.

type family FloatPrecisionBits (fpp :: FloatPrecision) :: Nat where ... Source #

This computes the number of bits occupied by a floating-point format.

Equations

FloatPrecisionBits (FloatingPointPrecision eb sb) = eb + sb 

Constructors for kind FloatPrecision

type FloatingPointPrecision Source #

Arguments

 = FloatingPointPrecision

:: Nat -> Nat -> FloatPrecision.

FloatingPointPrecision aliases

type Prec16 = FloatingPointPrecision 5 11 Source #

Floating-point precision aliases

Representations of base types

data BaseTypeRepr (bt :: BaseType) :: Type where Source #

A runtime representation of a solver interface type. Parameter bt has kind BaseType.

Instances
TestEquality BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

testEquality :: BaseTypeRepr a -> BaseTypeRepr b -> Maybe (a :~: b) #

OrdF BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

ShowF BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

withShow :: p BaseTypeRepr -> q tp -> (Show (BaseTypeRepr tp) -> a) -> a #

showF :: BaseTypeRepr tp -> String #

showsPrecF :: Int -> BaseTypeRepr tp -> String -> String #

HashableF BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseComplexType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseRealType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseNatType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseIntegerType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseBoolType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr (Assignment BaseTypeRepr) ctx => KnownRepr BaseTypeRepr (BaseStructType ctx :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr StringInfoRepr si => KnownRepr BaseTypeRepr (BaseStringType si :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr FloatPrecisionRepr fpp => KnownRepr BaseTypeRepr (BaseFloatType fpp :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

(1 <= w, KnownNat w) => KnownRepr BaseTypeRepr (BaseBVType w :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

(KnownRepr (Assignment BaseTypeRepr) idx, KnownRepr BaseTypeRepr tp, KnownRepr BaseTypeRepr t) => KnownRepr BaseTypeRepr (BaseArrayType (idx ::> tp) t :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseArrayType (idx ::> tp) t) #

Show (BaseTypeRepr bt) Source # 
Instance details

Defined in What4.BaseTypes

Pretty (BaseTypeRepr bt) Source # 
Instance details

Defined in What4.BaseTypes

Methods

pretty :: BaseTypeRepr bt -> Doc #

prettyList :: [BaseTypeRepr bt] -> Doc #

Hashable (BaseTypeRepr bt) Source # 
Instance details

Defined in What4.BaseTypes

Methods

hashWithSalt :: Int -> BaseTypeRepr bt -> Int #

hash :: BaseTypeRepr bt -> Int #

data FloatPrecisionRepr (fpp :: FloatPrecision) where Source #

Constructors

FloatingPointPrecisionRepr :: (2 <= eb, 2 <= sb) => !(NatRepr eb) -> !(NatRepr sb) -> FloatPrecisionRepr (FloatingPointPrecision eb sb) 
Instances
TestEquality FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

OrdF FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

ShowF FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

HashableF FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

(2 <= eb, 2 <= es, KnownNat eb, KnownNat es) => KnownRepr FloatPrecisionRepr (FloatingPointPrecision eb es :: FloatPrecision) Source # 
Instance details

Defined in What4.BaseTypes

Show (FloatPrecisionRepr fpp) Source # 
Instance details

Defined in What4.BaseTypes

Pretty (FloatPrecisionRepr fpp) Source # 
Instance details

Defined in What4.BaseTypes

Hashable (FloatPrecisionRepr fpp) Source # 
Instance details

Defined in What4.BaseTypes

data StringInfoRepr (si :: StringInfo) where Source #

Instances
TestEquality StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

OrdF StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

ShowF StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

withShow :: p StringInfoRepr -> q tp -> (Show (StringInfoRepr tp) -> a) -> a #

showF :: StringInfoRepr tp -> String #

showsPrecF :: Int -> StringInfoRepr tp -> String -> String #

HashableF StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr StringInfoRepr Unicode Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr StringInfoRepr Char16 Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr StringInfoRepr Char8 Source # 
Instance details

Defined in What4.BaseTypes

Show (StringInfoRepr si) Source # 
Instance details

Defined in What4.BaseTypes

Pretty (StringInfoRepr si) Source # 
Instance details

Defined in What4.BaseTypes

Hashable (StringInfoRepr si) Source # 
Instance details

Defined in What4.BaseTypes

arrayTypeIndices :: BaseTypeRepr (BaseArrayType idx tp) -> Assignment BaseTypeRepr idx Source #

Return the type of the indices for an array type.

arrayTypeResult :: BaseTypeRepr (BaseArrayType idx tp) -> BaseTypeRepr tp Source #

Return the result type of an array type.

KnownRepr

class KnownRepr (f :: k -> Type) (ctx :: k) where #

This class is parameterized by a kind k (typically a data kind), a type constructor f of kind k -> * (typically a GADT of singleton types indexed by k), and an index parameter ctx of kind k.

Methods

knownRepr :: f ctx #

Instances
KnownNat n => KnownRepr NatRepr (n :: Nat) 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

knownRepr :: NatRepr n #

KnownRepr BaseTypeRepr BaseComplexType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseRealType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseNatType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseIntegerType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseBoolType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr StringInfoRepr Unicode Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr StringInfoRepr Char16 Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr StringInfoRepr Char8 Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr FloatInfoRepr DoubleDoubleFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

KnownRepr FloatInfoRepr X86_80Float Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

KnownRepr FloatInfoRepr QuadFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

KnownRepr FloatInfoRepr DoubleFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

KnownRepr FloatInfoRepr SingleFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

KnownRepr FloatInfoRepr HalfFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

KnownRepr FloatModeRepr FloatReal Source # 
Instance details

Defined in What4.Expr.Builder

KnownRepr FloatModeRepr FloatUninterpreted Source # 
Instance details

Defined in What4.Expr.Builder

KnownRepr FloatModeRepr FloatIEEE Source # 
Instance details

Defined in What4.Expr.Builder

KnownRepr (Assignment BaseTypeRepr) ctx => KnownRepr BaseTypeRepr (BaseStructType ctx :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr StringInfoRepr si => KnownRepr BaseTypeRepr (BaseStringType si :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr FloatPrecisionRepr fpp => KnownRepr BaseTypeRepr (BaseFloatType fpp :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

(1 <= w, KnownNat w) => KnownRepr BaseTypeRepr (BaseBVType w :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

(2 <= eb, 2 <= es, KnownNat eb, KnownNat es) => KnownRepr FloatPrecisionRepr (FloatingPointPrecision eb es :: FloatPrecision) Source # 
Instance details

Defined in What4.BaseTypes

(KnownRepr (Assignment BaseTypeRepr) idx, KnownRepr BaseTypeRepr tp, KnownRepr BaseTypeRepr t) => KnownRepr BaseTypeRepr (BaseArrayType (idx ::> tp) t :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseArrayType (idx ::> tp) t) #

KnownRepr (Assignment f :: Ctx k -> Type) (EmptyCtx :: Ctx k) 
Instance details

Defined in Data.Parameterized.Context.Unsafe

(KnownRepr (Assignment f) ctx, KnownRepr f bt) => KnownRepr (Assignment f :: Ctx k -> Type) (ctx ::> bt :: Ctx k) 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

knownRepr :: Assignment f (ctx ::> bt) #

type KnownCtx f = KnownRepr (Assignment f) Source #

A Context where all the argument types are KnownRepr instances