Copyright	(c) Galois Inc 2014-2020
License	BSD3
Maintainer	Joe Hendrix <jhendrix@galois.com>
Stability	provisional
Safe Haskell	None
Language	Haskell2010

What4.BaseTypes

Contents

BaseType data kind
- Constructors for kind BaseType
StringInfo data kind
- Constructors for StringInfo
FloatPrecision data kind
- Constructors for kind FloatPrecision
- FloatingPointPrecision aliases
Representations of base types
KnownRepr

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

data BaseType
type BaseBoolType = 'BaseBoolType
type BaseIntegerType = 'BaseIntegerType
type BaseRealType = 'BaseRealType
type BaseStringType = 'BaseStringType
type BaseBVType = 'BaseBVType
type BaseFloatType = 'BaseFloatType
type BaseComplexType = 'BaseComplexType
type BaseStructType = 'BaseStructType
type BaseArrayType = 'BaseArrayType
data StringInfo
type Char8 = 'Char8
type Char16 = 'Char16
type Unicode = 'Unicode
data FloatPrecision
type family FloatPrecisionBits (fpp :: FloatPrecision) :: Nat where ...
type FloatingPointPrecision = 'FloatingPointPrecision
type Prec16 = FloatingPointPrecision 5 11
type Prec32 = FloatingPointPrecision 8 24
type Prec64 = FloatingPointPrecision 11 53
type Prec80 = FloatingPointPrecision 15 65
type Prec128 = FloatingPointPrecision 15 113
data BaseTypeRepr (bt :: BaseType) :: Type where
- 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)
data FloatPrecisionRepr (fpp :: FloatPrecision) where
- FloatingPointPrecisionRepr :: (2 <= eb, 2 <= sb) => !(NatRepr eb) -> !(NatRepr sb) -> FloatPrecisionRepr (FloatingPointPrecision eb sb)
data StringInfoRepr (si :: StringInfo) where
- Char8Repr :: StringInfoRepr Char8
- Char16Repr :: StringInfoRepr Char16
- UnicodeRepr :: StringInfoRepr Unicode
arrayTypeIndices :: BaseTypeRepr (BaseArrayType idx tp) -> Assignment BaseTypeRepr idx
arrayTypeResult :: BaseTypeRepr (BaseArrayType idx tp) -> BaseTypeRepr tp
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
class KnownRepr (f :: k -> Type) (ctx :: k) where
- knownRepr :: f ctx
type KnownCtx f = KnownRepr (Assignment f)

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 Methods knownRepr :: BaseTypeRepr BaseComplexType #
KnownRepr BaseTypeRepr BaseRealType Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseRealType #
KnownRepr BaseTypeRepr BaseIntegerType Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseIntegerType #
KnownRepr BaseTypeRepr BaseBoolType Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseBoolType #
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 Methods knownRepr :: BaseTypeRepr (BaseStructType ctx) #
KnownRepr StringInfoRepr si => KnownRepr BaseTypeRepr (BaseStringType si :: BaseType) Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseStringType si) #
KnownRepr FloatPrecisionRepr fpp => KnownRepr BaseTypeRepr (BaseFloatType fpp :: BaseType) Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseFloatType fpp) #
(1 <= w, KnownNat w) => KnownRepr BaseTypeRepr (BaseBVType w :: BaseType) Source #
Instance details 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) 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 Methods knownRepr :: StringInfoRepr Unicode #
KnownRepr StringInfoRepr Char16 Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: StringInfoRepr Char16 #
KnownRepr StringInfoRepr Char8 Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: StringInfoRepr Char8 #
(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 Methods knownRepr :: FloatPrecisionRepr (FloatingPointPrecision eb es) #

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

type Prec32 = FloatingPointPrecision 8 24 Source #

type Prec64 = FloatingPointPrecision 11 53 Source #

type Prec80 = FloatingPointPrecision 15 65 Source #

type Prec128 = FloatingPointPrecision 15 113 Source #

Representations of base types

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

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

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 Methods knownRepr :: BaseTypeRepr BaseComplexType #
KnownRepr BaseTypeRepr BaseRealType Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseRealType #
KnownRepr BaseTypeRepr BaseIntegerType Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseIntegerType #
KnownRepr BaseTypeRepr BaseBoolType Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseBoolType #
KnownRepr (Assignment BaseTypeRepr) ctx => KnownRepr BaseTypeRepr (BaseStructType ctx :: BaseType) Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseStructType ctx) #
KnownRepr StringInfoRepr si => KnownRepr BaseTypeRepr (BaseStringType si :: BaseType) Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseStringType si) #
KnownRepr FloatPrecisionRepr fpp => KnownRepr BaseTypeRepr (BaseFloatType fpp :: BaseType) Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseFloatType fpp) #
(1 <= w, KnownNat w) => KnownRepr BaseTypeRepr (BaseBVType w :: BaseType) Source #
Instance details 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) Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseArrayType (idx ::> tp) t) #
Show (BaseTypeRepr bt) Source #
Instance details Defined in What4.BaseTypes Methods showsPrec :: Int -> BaseTypeRepr bt -> ShowS # show :: BaseTypeRepr bt -> String # showList :: [BaseTypeRepr bt] -> ShowS #
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 Methods knownRepr :: FloatPrecisionRepr (FloatingPointPrecision eb es) #
Show (FloatPrecisionRepr fpp) Source #
Instance details Defined in What4.BaseTypes Methods showsPrec :: Int -> FloatPrecisionRepr fpp -> ShowS # show :: FloatPrecisionRepr fpp -> String # showList :: [FloatPrecisionRepr fpp] -> ShowS #
Hashable (FloatPrecisionRepr fpp) Source #
Instance details Defined in What4.BaseTypes Methods hashWithSalt :: Int -> FloatPrecisionRepr fpp -> Int # hash :: FloatPrecisionRepr fpp -> Int #
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 #

Constructors

Char8Repr :: StringInfoRepr Char8
Char16Repr :: StringInfoRepr Char16
UnicodeRepr :: StringInfoRepr Unicode

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 Methods knownRepr :: StringInfoRepr Unicode #
KnownRepr StringInfoRepr Char16 Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: StringInfoRepr Char16 #
KnownRepr StringInfoRepr Char8 Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: StringInfoRepr Char8 #
Show (StringInfoRepr si) Source #
Instance details Defined in What4.BaseTypes Methods showsPrec :: Int -> StringInfoRepr si -> ShowS # show :: StringInfoRepr si -> String # showList :: [StringInfoRepr si] -> ShowS #
Hashable (StringInfoRepr si) Source #
Instance details Defined in What4.BaseTypes Methods hashWithSalt :: Int -> StringInfoRepr si -> Int # hash :: StringInfoRepr si -> Int #
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.

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

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

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

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 Methods knownRepr :: BaseTypeRepr BaseComplexType #
KnownRepr BaseTypeRepr BaseRealType Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseRealType #
KnownRepr BaseTypeRepr BaseIntegerType Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseIntegerType #
KnownRepr BaseTypeRepr BaseBoolType Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseBoolType #
KnownRepr StringInfoRepr Unicode Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: StringInfoRepr Unicode #
KnownRepr StringInfoRepr Char16 Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: StringInfoRepr Char16 #
KnownRepr StringInfoRepr Char8 Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: StringInfoRepr Char8 #
KnownRepr FloatInfoRepr DoubleDoubleFloat Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr DoubleDoubleFloat #
KnownRepr FloatInfoRepr X86_80Float Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr X86_80Float #
KnownRepr FloatInfoRepr QuadFloat Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr QuadFloat #
KnownRepr FloatInfoRepr DoubleFloat Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr DoubleFloat #
KnownRepr FloatInfoRepr SingleFloat Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr SingleFloat #
KnownRepr FloatInfoRepr HalfFloat Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr HalfFloat #
KnownRepr FloatModeRepr FloatReal Source #
Instance details Defined in What4.Expr.Builder Methods knownRepr :: FloatModeRepr FloatReal #
KnownRepr FloatModeRepr FloatUninterpreted Source #
Instance details Defined in What4.Expr.Builder Methods knownRepr :: FloatModeRepr FloatUninterpreted #
KnownRepr FloatModeRepr FloatIEEE Source #
Instance details Defined in What4.Expr.Builder Methods knownRepr :: FloatModeRepr FloatIEEE #
KnownRepr (Assignment BaseTypeRepr) ctx => KnownRepr BaseTypeRepr (BaseStructType ctx :: BaseType) Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseStructType ctx) #
KnownRepr StringInfoRepr si => KnownRepr BaseTypeRepr (BaseStringType si :: BaseType) Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseStringType si) #
KnownRepr FloatPrecisionRepr fpp => KnownRepr BaseTypeRepr (BaseFloatType fpp :: BaseType) Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseFloatType fpp) #
(1 <= w, KnownNat w) => KnownRepr BaseTypeRepr (BaseBVType w :: BaseType) Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseBVType w) #
(2 <= eb, 2 <= es, KnownNat eb, KnownNat es) => KnownRepr FloatPrecisionRepr (FloatingPointPrecision eb es :: FloatPrecision) Source #
Instance details 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) 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 Methods knownRepr :: Assignment f EmptyCtx #
(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