what4-1.1: 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

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

Instances details
TestEquality BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

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

TestEquality IndexLit Source # 
Instance details

Defined in What4.IndexLit

Methods

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

TestEquality OnlyIntRepr Source # 
Instance details

Defined in What4.Utils.OnlyIntRepr

Methods

testEquality :: forall (a :: k) (b :: k). OnlyIntRepr a -> OnlyIntRepr b -> Maybe (a :~: b) #

TestEquality ConcreteVal Source # 
Instance details

Defined in What4.Concrete

Methods

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

TestEquality TypeMap Source # 
Instance details

Defined in What4.Protocol.SMTWriter

Methods

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

OrdF BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

compareF :: forall (x :: k) (y :: k). BaseTypeRepr x -> BaseTypeRepr y -> OrderingF x y #

leqF :: forall (x :: k) (y :: k). BaseTypeRepr x -> BaseTypeRepr y -> Bool #

ltF :: forall (x :: k) (y :: k). BaseTypeRepr x -> BaseTypeRepr y -> Bool #

geqF :: forall (x :: k) (y :: k). BaseTypeRepr x -> BaseTypeRepr y -> Bool #

gtF :: forall (x :: k) (y :: k). BaseTypeRepr x -> BaseTypeRepr y -> Bool #

OrdF IndexLit Source # 
Instance details

Defined in What4.IndexLit

Methods

compareF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> OrderingF x y #

leqF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> Bool #

ltF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> Bool #

geqF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> Bool #

gtF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> Bool #

OrdF ConcreteVal Source # 
Instance details

Defined in What4.Concrete

Methods

compareF :: forall (x :: k) (y :: k). ConcreteVal x -> ConcreteVal y -> OrderingF x y #

leqF :: forall (x :: k) (y :: k). ConcreteVal x -> ConcreteVal y -> Bool #

ltF :: forall (x :: k) (y :: k). ConcreteVal x -> ConcreteVal y -> Bool #

geqF :: forall (x :: k) (y :: k). ConcreteVal x -> ConcreteVal y -> Bool #

gtF :: forall (x :: k) (y :: k). ConcreteVal x -> ConcreteVal y -> Bool #

ShowF BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

withShow :: forall p q (tp :: k) a. p BaseTypeRepr -> q tp -> (Show (BaseTypeRepr tp) => a) -> a #

showF :: forall (tp :: k). BaseTypeRepr tp -> String #

showsPrecF :: forall (tp :: k). Int -> BaseTypeRepr tp -> String -> String #

ShowF IndexLit Source # 
Instance details

Defined in What4.IndexLit

Methods

withShow :: forall p q (tp :: k) a. p IndexLit -> q tp -> (Show (IndexLit tp) => a) -> a #

showF :: forall (tp :: k). IndexLit tp -> String #

showsPrecF :: forall (tp :: k). Int -> IndexLit tp -> String -> String #

ShowF ConcreteVal Source # 
Instance details

Defined in What4.Concrete

Methods

withShow :: forall p q (tp :: k) a. p ConcreteVal -> q tp -> (Show (ConcreteVal tp) => a) -> a #

showF :: forall (tp :: k). ConcreteVal tp -> String #

showsPrecF :: forall (tp :: k). Int -> ConcreteVal tp -> String -> String #

ShowF TypeMap Source # 
Instance details

Defined in What4.Protocol.SMTWriter

Methods

withShow :: forall p q (tp :: k) a. p TypeMap -> q tp -> (Show (TypeMap tp) => a) -> a #

showF :: forall (tp :: k). TypeMap tp -> String #

showsPrecF :: forall (tp :: k). Int -> TypeMap tp -> String -> String #

HashableF BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

hashWithSaltF :: forall (tp :: k). Int -> BaseTypeRepr tp -> Int #

hashF :: forall (tp :: k). BaseTypeRepr tp -> Int #

HashableF IndexLit Source # 
Instance details

Defined in What4.IndexLit

Methods

hashWithSaltF :: forall (tp :: k). Int -> IndexLit tp -> Int #

hashF :: forall (tp :: k). IndexLit tp -> Int #

HashableF OnlyIntRepr Source # 
Instance details

Defined in What4.Utils.OnlyIntRepr

Methods

hashWithSaltF :: forall (tp :: k). Int -> OnlyIntRepr tp -> Int #

hashF :: forall (tp :: k). OnlyIntRepr tp -> Int #

FoldableFC App Source # 
Instance details

Defined in What4.Expr.App

Methods

foldMapFC :: forall f m. 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 f b. (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 f b. (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 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 :: forall f m. 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 f b. (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 f b. (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 :: forall f g m. 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 :: forall (a :: k) (b :: k). App e a -> App e b -> Maybe (a :~: b) #

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

Defined in What4.Expr.App

Methods

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

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

Defined in What4.Expr.App

Methods

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

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

Defined in What4.Expr.App

Methods

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

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

Defined in What4.Expr.App

Methods

compareF :: forall (x :: k) (y :: k). ExprBoundVar t x -> ExprBoundVar t y -> OrderingF x y #

leqF :: forall (x :: k) (y :: k). ExprBoundVar t x -> ExprBoundVar t y -> Bool #

ltF :: forall (x :: k) (y :: k). ExprBoundVar t x -> ExprBoundVar t y -> Bool #

geqF :: forall (x :: k) (y :: k). ExprBoundVar t x -> ExprBoundVar t y -> Bool #

gtF :: forall (x :: k) (y :: k). ExprBoundVar t x -> ExprBoundVar t y -> Bool #

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

Defined in What4.Expr.App

Methods

compareF :: forall (x :: k) (y :: k). Expr t x -> Expr t y -> OrderingF x y #

leqF :: forall (x :: k) (y :: k). Expr t x -> Expr t y -> Bool #

ltF :: forall (x :: k) (y :: k). Expr t x -> Expr t y -> Bool #

geqF :: forall (x :: k) (y :: k). Expr t x -> Expr t y -> Bool #

gtF :: forall (x :: k) (y :: k). Expr t x -> Expr t y -> Bool #

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

Defined in What4.Expr.App

Methods

compareF :: forall (x :: k) (y :: k). NonceAppExpr t x -> NonceAppExpr t y -> OrderingF x y #

leqF :: forall (x :: k) (y :: k). NonceAppExpr t x -> NonceAppExpr t y -> Bool #

ltF :: forall (x :: k) (y :: k). NonceAppExpr t x -> NonceAppExpr t y -> Bool #

geqF :: forall (x :: k) (y :: k). NonceAppExpr t x -> NonceAppExpr t y -> Bool #

gtF :: forall (x :: k) (y :: k). NonceAppExpr t x -> NonceAppExpr t y -> Bool #

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

Defined in What4.Expr.App

Methods

withShow :: forall p q (tp :: k) a. p (ExprBoundVar t) -> q tp -> (Show (ExprBoundVar t tp) => a) -> a #

showF :: forall (tp :: k). ExprBoundVar t tp -> String #

showsPrecF :: forall (tp :: k). Int -> ExprBoundVar t tp -> String -> String #

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

Defined in What4.Expr.App

Methods

withShow :: forall p q (tp :: k) a. p (Expr t) -> q tp -> (Show (Expr t tp) => a) -> a #

showF :: forall (tp :: k). Expr t tp -> String #

showsPrecF :: forall (tp :: k). 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 :: forall (tp :: k). Int -> App e tp -> Int #

hashF :: forall (tp :: k). App e tp -> Int #

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

Defined in What4.Expr.App

Methods

hashWithSaltF :: forall (tp :: k). Int -> ExprBoundVar t tp -> Int #

hashF :: forall (tp :: k). ExprBoundVar t tp -> Int #

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

Defined in What4.Expr.App

Methods

hashWithSaltF :: forall (tp :: k). Int -> Expr t tp -> Int #

hashF :: forall (tp :: k). Expr t tp -> Int #

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

Defined in What4.Interface

Methods

testEquality :: forall (a :: k) (b :: k). 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 :: forall (a :: k) (b :: k). 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 :: forall (tp :: k). Int -> ArrayResultWrapper e idx tp -> Int #

hashF :: forall (tp :: k). ArrayResultWrapper e idx tp -> Int #

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

Defined in What4.Expr.App

Methods

hashWithSaltF :: forall (tp :: k). Int -> NonceApp t e tp -> Int #

hashF :: forall (tp :: k). NonceApp t e tp -> Int #

HasAbsValue (Dummy :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

getAbsValue :: forall (tp :: BaseType). Dummy tp -> AbstractValue tp Source #

Constructors for kind BaseType

type BaseBoolType Source #

Arguments

 = 'BaseBoolType

:: BaseType.

type BaseIntegerType Source #

Arguments

 = 'BaseIntegerType

:: 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

Instances details
TestEquality StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

testEquality :: forall (a :: k) (b :: k). StringInfoRepr a -> StringInfoRepr b -> Maybe (a :~: b) #

TestEquality StringLiteral Source # 
Instance details

Defined in What4.Utils.StringLiteral

Methods

testEquality :: forall (a :: k) (b :: k). StringLiteral a -> StringLiteral b -> Maybe (a :~: b) #

OrdF StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

compareF :: forall (x :: k) (y :: k). StringInfoRepr x -> StringInfoRepr y -> OrderingF x y #

leqF :: forall (x :: k) (y :: k). StringInfoRepr x -> StringInfoRepr y -> Bool #

ltF :: forall (x :: k) (y :: k). StringInfoRepr x -> StringInfoRepr y -> Bool #

geqF :: forall (x :: k) (y :: k). StringInfoRepr x -> StringInfoRepr y -> Bool #

gtF :: forall (x :: k) (y :: k). StringInfoRepr x -> StringInfoRepr y -> Bool #

OrdF StringLiteral Source # 
Instance details

Defined in What4.Utils.StringLiteral

Methods

compareF :: forall (x :: k) (y :: k). StringLiteral x -> StringLiteral y -> OrderingF x y #

leqF :: forall (x :: k) (y :: k). StringLiteral x -> StringLiteral y -> Bool #

ltF :: forall (x :: k) (y :: k). StringLiteral x -> StringLiteral y -> Bool #

geqF :: forall (x :: k) (y :: k). StringLiteral x -> StringLiteral y -> Bool #

gtF :: forall (x :: k) (y :: k). StringLiteral x -> StringLiteral y -> Bool #

ShowF StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

withShow :: forall p q (tp :: k) a. p StringInfoRepr -> q tp -> (Show (StringInfoRepr tp) => a) -> a #

showF :: forall (tp :: k). StringInfoRepr tp -> String #

showsPrecF :: forall (tp :: k). Int -> StringInfoRepr tp -> String -> String #

ShowF StringLiteral Source # 
Instance details

Defined in What4.Utils.StringLiteral

Methods

withShow :: forall p q (tp :: k) a. p StringLiteral -> q tp -> (Show (StringLiteral tp) => a) -> a #

showF :: forall (tp :: k). StringLiteral tp -> String #

showsPrecF :: forall (tp :: k). Int -> StringLiteral tp -> String -> String #

HashableF StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

hashWithSaltF :: forall (tp :: k). Int -> StringInfoRepr tp -> Int #

hashF :: forall (tp :: k). StringInfoRepr tp -> Int #

HashableF StringLiteral Source # 
Instance details

Defined in What4.Utils.StringLiteral

Methods

hashWithSaltF :: forall (tp :: k). Int -> StringLiteral tp -> Int #

hashF :: forall (tp :: k). StringLiteral tp -> Int #

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 :: forall (a :: k) (b :: k). 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 :: forall (tp :: k). Int -> StringSeq e tp -> Int #

hashF :: forall (tp :: k). 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.

Instances

Instances details
TestEquality FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

testEquality :: forall (a :: k) (b :: k). FloatPrecisionRepr a -> FloatPrecisionRepr b -> Maybe (a :~: b) #

OrdF FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

compareF :: forall (x :: k) (y :: k). FloatPrecisionRepr x -> FloatPrecisionRepr y -> OrderingF x y #

leqF :: forall (x :: k) (y :: k). FloatPrecisionRepr x -> FloatPrecisionRepr y -> Bool #

ltF :: forall (x :: k) (y :: k). FloatPrecisionRepr x -> FloatPrecisionRepr y -> Bool #

geqF :: forall (x :: k) (y :: k). FloatPrecisionRepr x -> FloatPrecisionRepr y -> Bool #

gtF :: forall (x :: k) (y :: k). FloatPrecisionRepr x -> FloatPrecisionRepr y -> Bool #

ShowF FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

withShow :: forall p q (tp :: k) a. p FloatPrecisionRepr -> q tp -> (Show (FloatPrecisionRepr tp) => a) -> a #

showF :: forall (tp :: k). FloatPrecisionRepr tp -> String #

showsPrecF :: forall (tp :: k). Int -> FloatPrecisionRepr tp -> String -> String #

HashableF FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

hashWithSaltF :: forall (tp :: k). Int -> FloatPrecisionRepr tp -> Int #

hashF :: forall (tp :: k). FloatPrecisionRepr tp -> Int #

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

Defined in What4.BaseTypes

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

Instances details
TestEquality BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

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

OrdF BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

compareF :: forall (x :: k) (y :: k). BaseTypeRepr x -> BaseTypeRepr y -> OrderingF x y #

leqF :: forall (x :: k) (y :: k). BaseTypeRepr x -> BaseTypeRepr y -> Bool #

ltF :: forall (x :: k) (y :: k). BaseTypeRepr x -> BaseTypeRepr y -> Bool #

geqF :: forall (x :: k) (y :: k). BaseTypeRepr x -> BaseTypeRepr y -> Bool #

gtF :: forall (x :: k) (y :: k). BaseTypeRepr x -> BaseTypeRepr y -> Bool #

ShowF BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

withShow :: forall p q (tp :: k) a. p BaseTypeRepr -> q tp -> (Show (BaseTypeRepr tp) => a) -> a #

showF :: forall (tp :: k). BaseTypeRepr tp -> String #

showsPrecF :: forall (tp :: k). Int -> BaseTypeRepr tp -> String -> String #

HashableF BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

hashWithSaltF :: forall (tp :: k). Int -> BaseTypeRepr tp -> Int #

hashF :: forall (tp :: k). BaseTypeRepr tp -> Int #

KnownRepr BaseTypeRepr BaseComplexType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseRealType 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

Hashable (BaseTypeRepr bt) Source # 
Instance details

Defined in What4.BaseTypes

Methods

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

hash :: BaseTypeRepr bt -> Int #

Pretty (BaseTypeRepr bt) Source # 
Instance details

Defined in What4.BaseTypes

Methods

pretty :: BaseTypeRepr bt -> Doc ann #

prettyList :: [BaseTypeRepr bt] -> Doc ann #

data FloatPrecisionRepr (fpp :: FloatPrecision) where Source #

Constructors

FloatingPointPrecisionRepr :: (2 <= eb, 2 <= sb) => !(NatRepr eb) -> !(NatRepr sb) -> FloatPrecisionRepr (FloatingPointPrecision eb sb) 

Instances

Instances details
TestEquality FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

testEquality :: forall (a :: k) (b :: k). FloatPrecisionRepr a -> FloatPrecisionRepr b -> Maybe (a :~: b) #

OrdF FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

compareF :: forall (x :: k) (y :: k). FloatPrecisionRepr x -> FloatPrecisionRepr y -> OrderingF x y #

leqF :: forall (x :: k) (y :: k). FloatPrecisionRepr x -> FloatPrecisionRepr y -> Bool #

ltF :: forall (x :: k) (y :: k). FloatPrecisionRepr x -> FloatPrecisionRepr y -> Bool #

geqF :: forall (x :: k) (y :: k). FloatPrecisionRepr x -> FloatPrecisionRepr y -> Bool #

gtF :: forall (x :: k) (y :: k). FloatPrecisionRepr x -> FloatPrecisionRepr y -> Bool #

ShowF FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

withShow :: forall p q (tp :: k) a. p FloatPrecisionRepr -> q tp -> (Show (FloatPrecisionRepr tp) => a) -> a #

showF :: forall (tp :: k). FloatPrecisionRepr tp -> String #

showsPrecF :: forall (tp :: k). Int -> FloatPrecisionRepr tp -> String -> String #

HashableF FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

hashWithSaltF :: forall (tp :: k). Int -> FloatPrecisionRepr tp -> Int #

hashF :: forall (tp :: k). FloatPrecisionRepr tp -> Int #

(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

Hashable (FloatPrecisionRepr fpp) Source # 
Instance details

Defined in What4.BaseTypes

Pretty (FloatPrecisionRepr fpp) Source # 
Instance details

Defined in What4.BaseTypes

Methods

pretty :: FloatPrecisionRepr fpp -> Doc ann #

prettyList :: [FloatPrecisionRepr fpp] -> Doc ann #

data StringInfoRepr (si :: StringInfo) where Source #

Instances

Instances details
TestEquality StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

testEquality :: forall (a :: k) (b :: k). StringInfoRepr a -> StringInfoRepr b -> Maybe (a :~: b) #

OrdF StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

compareF :: forall (x :: k) (y :: k). StringInfoRepr x -> StringInfoRepr y -> OrderingF x y #

leqF :: forall (x :: k) (y :: k). StringInfoRepr x -> StringInfoRepr y -> Bool #

ltF :: forall (x :: k) (y :: k). StringInfoRepr x -> StringInfoRepr y -> Bool #

geqF :: forall (x :: k) (y :: k). StringInfoRepr x -> StringInfoRepr y -> Bool #

gtF :: forall (x :: k) (y :: k). StringInfoRepr x -> StringInfoRepr y -> Bool #

ShowF StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

withShow :: forall p q (tp :: k) a. p StringInfoRepr -> q tp -> (Show (StringInfoRepr tp) => a) -> a #

showF :: forall (tp :: k). StringInfoRepr tp -> String #

showsPrecF :: forall (tp :: k). Int -> StringInfoRepr tp -> String -> String #

HashableF StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

hashWithSaltF :: forall (tp :: k). Int -> StringInfoRepr tp -> Int #

hashF :: forall (tp :: k). StringInfoRepr tp -> Int #

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

Hashable (StringInfoRepr si) Source # 
Instance details

Defined in What4.BaseTypes

Pretty (StringInfoRepr si) Source # 
Instance details

Defined in What4.BaseTypes

Methods

pretty :: StringInfoRepr si -> Doc ann #

prettyList :: [StringInfoRepr si] -> Doc ann #

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

Instances details
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 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