What4.BaseTypes

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.

BaseType data kind

data BaseType

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

Instances

TestEquality BaseTypeRepr

Defined in What4.BaseTypes

Methods

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

TestEquality IndexLit

Defined in What4.IndexLit

Methods

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

TestEquality OnlyIntRepr

Defined in What4.Utils.OnlyIntRepr

Methods

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

TestEquality ConcreteVal

Defined in What4.Concrete

Methods

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

TestEquality TypeMap

Defined in What4.Protocol.SMTWriter

Methods

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

OrdF BaseTypeRepr

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

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

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

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

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

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

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

Defined in What4.BaseTypes

Methods

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

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

HashableF IndexLit

Defined in What4.IndexLit

Methods

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

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

HashableF OnlyIntRepr

Defined in What4.Utils.OnlyIntRepr

Methods

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

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

FoldableFC App

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

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseComplexType

KnownRepr BaseTypeRepr BaseRealType

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseRealType

KnownRepr BaseTypeRepr BaseIntegerType

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseIntegerType

KnownRepr BaseTypeRepr BaseBoolType

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseBoolType

FunctorFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type)

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)

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)

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)

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseStructType ctx)

KnownRepr StringInfoRepr si => KnownRepr BaseTypeRepr (BaseStringType si :: BaseType)

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseStringType si)

KnownRepr FloatPrecisionRepr fpp => KnownRepr BaseTypeRepr (BaseFloatType fpp :: BaseType)

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseFloatType fpp)

(1 <= w, KnownNat w) => KnownRepr BaseTypeRepr (BaseBVType w :: BaseType)

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseBVType w)

(KnownRepr (Assignment BaseTypeRepr) idx, KnownRepr BaseTypeRepr tp, KnownRepr BaseTypeRepr t) => KnownRepr BaseTypeRepr (BaseArrayType (idx ::> tp) t :: BaseType)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

Defined in What4.Expr.App

Methods

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

Constructors for kind BaseType

type BaseBoolType

Arguments

 = 'BaseBoolType

:: BaseType.

type BaseIntegerType

Arguments

 = 'BaseIntegerType

:: BaseType.

type BaseRealType

Arguments

 = 'BaseRealType

:: BaseType.

type BaseStringType

Arguments

 = 'BaseStringType

:: BaseType.

type BaseBVType

Arguments

 = 'BaseBVType

:: Nat -> BaseType.

type BaseFloatType

Arguments

 = 'BaseFloatType

:: FloatPrecision -> BaseType.

type BaseComplexType

Arguments

 = 'BaseComplexType

:: BaseType.

type BaseStructType

Arguments

 = 'BaseStructType

:: Ctx BaseType -> BaseType.

type BaseArrayType

Arguments

 = 'BaseArrayType

:: Ctx BaseType -> BaseType -> BaseType.

StringInfo data kind

data StringInfo

Instances

TestEquality StringInfoRepr

Defined in What4.BaseTypes

Methods

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

TestEquality StringLiteral

Defined in What4.Utils.StringLiteral

Methods

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

OrdF StringInfoRepr

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

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

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

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

Defined in What4.BaseTypes

Methods

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

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

HashableF StringLiteral

Defined in What4.Utils.StringLiteral

Methods

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

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

KnownRepr StringInfoRepr Unicode

Defined in What4.BaseTypes

Methods

knownRepr :: StringInfoRepr Unicode

KnownRepr StringInfoRepr Char16

Defined in What4.BaseTypes

Methods

knownRepr :: StringInfoRepr Char16

KnownRepr StringInfoRepr Char8

Defined in What4.BaseTypes

Methods

knownRepr :: StringInfoRepr Char8

(TestEquality e, HasAbsValue e, HashableF e) => TestEquality (StringSeq e :: StringInfo -> Type)

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)

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

Arguments

 = 'Char8

:: StringInfo.

type Char16

Arguments

 = 'Char16

:: StringInfo.

type Unicode

Arguments

 = 'Unicode

:: StringInfo.

FloatPrecision data kind

data FloatPrecision

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

Instances

TestEquality FloatPrecisionRepr

Defined in What4.BaseTypes

Methods

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

OrdF FloatPrecisionRepr

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

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

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)

Defined in What4.BaseTypes

Methods

knownRepr :: FloatPrecisionRepr (FloatingPointPrecision eb es)

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

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

Arguments

 = 'FloatingPointPrecision

:: Nat -> Nat -> FloatPrecision.

FloatingPointPrecision aliases

type Prec16 = FloatingPointPrecision 5 11

Floating-point precision aliases

type Prec32 = FloatingPointPrecision 8 24

type Prec64 = FloatingPointPrecision 11 53

type Prec80 = FloatingPointPrecision 15 65

type Prec128 = FloatingPointPrecision 15 113

Representations of base types

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

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

Constructors

BaseBoolRepr :: BaseTypeRepr BaseBoolType

BaseBVRepr :: 1 <= w => !(NatRepr w) -> BaseTypeRepr (BaseBVType w)

BaseIntegerRepr :: BaseTypeRepr BaseIntegerType

BaseRealRepr :: BaseTypeRepr BaseRealType

BaseFloatRepr :: !(FloatPrecisionRepr fpp) -> BaseTypeRepr (BaseFloatType fpp)

BaseStringRepr :: StringInfoRepr si -> BaseTypeRepr (BaseStringType si)

BaseComplexRepr :: BaseTypeRepr BaseComplexType

BaseStructRepr :: !(Assignment BaseTypeRepr ctx) -> BaseTypeRepr (BaseStructType ctx)

BaseArrayRepr :: !(Assignment BaseTypeRepr (idx ::> tp)) -> !(BaseTypeRepr xs) -> BaseTypeRepr (BaseArrayType (idx ::> tp) xs)

Instances

TestEquality BaseTypeRepr

Defined in What4.BaseTypes

Methods

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

OrdF BaseTypeRepr

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

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

Defined in What4.BaseTypes

Methods

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

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

KnownRepr BaseTypeRepr BaseComplexType

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseComplexType

KnownRepr BaseTypeRepr BaseRealType

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseRealType

KnownRepr BaseTypeRepr BaseIntegerType

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseIntegerType

KnownRepr BaseTypeRepr BaseBoolType

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseBoolType

KnownRepr (Assignment BaseTypeRepr) ctx => KnownRepr BaseTypeRepr (BaseStructType ctx :: BaseType)

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseStructType ctx)

KnownRepr StringInfoRepr si => KnownRepr BaseTypeRepr (BaseStringType si :: BaseType)

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseStringType si)

KnownRepr FloatPrecisionRepr fpp => KnownRepr BaseTypeRepr (BaseFloatType fpp :: BaseType)

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseFloatType fpp)

(1 <= w, KnownNat w) => KnownRepr BaseTypeRepr (BaseBVType w :: BaseType)

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseBVType w)

(KnownRepr (Assignment BaseTypeRepr) idx, KnownRepr BaseTypeRepr tp, KnownRepr BaseTypeRepr t) => KnownRepr BaseTypeRepr (BaseArrayType (idx ::> tp) t :: BaseType)

Defined in What4.BaseTypes

Methods

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

Show (BaseTypeRepr bt)

Defined in What4.BaseTypes

Methods

showsPrec :: Int -> BaseTypeRepr bt -> ShowS

show :: BaseTypeRepr bt -> String

showList :: [BaseTypeRepr bt] -> ShowS

Hashable (BaseTypeRepr bt)

Defined in What4.BaseTypes

Methods

hashWithSalt :: Int -> BaseTypeRepr bt -> Int

hash :: BaseTypeRepr bt -> Int

Pretty (BaseTypeRepr bt)

Defined in What4.BaseTypes

Methods

pretty :: BaseTypeRepr bt -> Doc ann

prettyList :: [BaseTypeRepr bt] -> Doc ann

data FloatPrecisionRepr (fpp :: FloatPrecision) where

Constructors

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

Instances

TestEquality FloatPrecisionRepr

Defined in What4.BaseTypes

Methods

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

OrdF FloatPrecisionRepr

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

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

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)

Defined in What4.BaseTypes

Methods

knownRepr :: FloatPrecisionRepr (FloatingPointPrecision eb es)

Show (FloatPrecisionRepr fpp)

Defined in What4.BaseTypes

Methods

showsPrec :: Int -> FloatPrecisionRepr fpp -> ShowS

show :: FloatPrecisionRepr fpp -> String

showList :: [FloatPrecisionRepr fpp] -> ShowS

Hashable (FloatPrecisionRepr fpp)

Defined in What4.BaseTypes

Methods

hashWithSalt :: Int -> FloatPrecisionRepr fpp -> Int

hash :: FloatPrecisionRepr fpp -> Int

Pretty (FloatPrecisionRepr fpp)

Defined in What4.BaseTypes

Methods

pretty :: FloatPrecisionRepr fpp -> Doc ann

prettyList :: [FloatPrecisionRepr fpp] -> Doc ann

data StringInfoRepr (si :: StringInfo) where

Constructors

Char8Repr :: StringInfoRepr Char8

Char16Repr :: StringInfoRepr Char16

UnicodeRepr :: StringInfoRepr Unicode

Instances

TestEquality StringInfoRepr

Defined in What4.BaseTypes

Methods

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

OrdF StringInfoRepr

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

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

Defined in What4.BaseTypes

Methods

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

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

KnownRepr StringInfoRepr Unicode

Defined in What4.BaseTypes

Methods

knownRepr :: StringInfoRepr Unicode

KnownRepr StringInfoRepr Char16

Defined in What4.BaseTypes

Methods

knownRepr :: StringInfoRepr Char16

KnownRepr StringInfoRepr Char8

Defined in What4.BaseTypes

Methods

knownRepr :: StringInfoRepr Char8

Show (StringInfoRepr si)

Defined in What4.BaseTypes

Methods

showsPrec :: Int -> StringInfoRepr si -> ShowS

show :: StringInfoRepr si -> String

showList :: [StringInfoRepr si] -> ShowS

Hashable (StringInfoRepr si)

Defined in What4.BaseTypes

Methods

hashWithSalt :: Int -> StringInfoRepr si -> Int

hash :: StringInfoRepr si -> Int

Pretty (StringInfoRepr si)

Defined in What4.BaseTypes

Methods

pretty :: StringInfoRepr si -> Doc ann

prettyList :: [StringInfoRepr si] -> Doc ann

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

Return the type of the indices for an array type.

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

Return the result type of an array type.

floatPrecisionToBVType :: FloatPrecisionRepr (FloatingPointPrecision eb sb) -> BaseTypeRepr (BaseBVType (eb + sb))

lemmaFloatPrecisionIsPos :: forall eb' sb'. FloatPrecisionRepr (FloatingPointPrecision eb' sb') -> LeqProof 1 (eb' + sb')

module Data.Parameterized.NatRepr

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)

Defined in Data.Parameterized.NatRepr.Internal

Methods

knownRepr :: NatRepr n

KnownRepr BaseTypeRepr BaseComplexType

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseComplexType

KnownRepr BaseTypeRepr BaseRealType

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseRealType

KnownRepr BaseTypeRepr BaseIntegerType

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseIntegerType

KnownRepr BaseTypeRepr BaseBoolType

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseBoolType

KnownRepr StringInfoRepr Unicode

Defined in What4.BaseTypes

Methods

knownRepr :: StringInfoRepr Unicode

KnownRepr StringInfoRepr Char16

Defined in What4.BaseTypes

Methods

knownRepr :: StringInfoRepr Char16

KnownRepr StringInfoRepr Char8

Defined in What4.BaseTypes

Methods

knownRepr :: StringInfoRepr Char8

KnownRepr FloatInfoRepr DoubleDoubleFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr DoubleDoubleFloat

KnownRepr FloatInfoRepr X86_80Float

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr X86_80Float

KnownRepr FloatInfoRepr QuadFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr QuadFloat

KnownRepr FloatInfoRepr DoubleFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr DoubleFloat

KnownRepr FloatInfoRepr SingleFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr SingleFloat

KnownRepr FloatInfoRepr HalfFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr HalfFloat

KnownRepr FloatModeRepr FloatReal

Defined in What4.Expr.Builder

Methods

knownRepr :: FloatModeRepr FloatReal

KnownRepr FloatModeRepr FloatUninterpreted

Defined in What4.Expr.Builder

Methods

knownRepr :: FloatModeRepr FloatUninterpreted

KnownRepr FloatModeRepr FloatIEEE

Defined in What4.Expr.Builder

Methods

knownRepr :: FloatModeRepr FloatIEEE

KnownRepr (Assignment BaseTypeRepr) ctx => KnownRepr BaseTypeRepr (BaseStructType ctx :: BaseType)

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseStructType ctx)

KnownRepr StringInfoRepr si => KnownRepr BaseTypeRepr (BaseStringType si :: BaseType)

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseStringType si)

KnownRepr FloatPrecisionRepr fpp => KnownRepr BaseTypeRepr (BaseFloatType fpp :: BaseType)

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseFloatType fpp)

(1 <= w, KnownNat w) => KnownRepr BaseTypeRepr (BaseBVType w :: BaseType)

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseBVType w)

(2 <= eb, 2 <= es, KnownNat eb, KnownNat es) => KnownRepr FloatPrecisionRepr (FloatingPointPrecision eb es :: FloatPrecision)

Defined in What4.BaseTypes

Methods

knownRepr :: FloatPrecisionRepr (FloatingPointPrecision eb es)

(KnownRepr (Assignment BaseTypeRepr) idx, KnownRepr BaseTypeRepr tp, KnownRepr BaseTypeRepr t) => KnownRepr BaseTypeRepr (BaseArrayType (idx ::> tp) t :: BaseType)

Defined in What4.BaseTypes

Methods

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

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

Defined in Data.Parameterized.Context.Unsafe

Methods

knownRepr :: Assignment f EmptyCtx

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

Defined in Data.Parameterized.Context.Unsafe

Methods

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

type KnownCtx f = KnownRepr (Assignment f)

A Context where all the argument types are KnownRepr instances