| Copyright | (c) Galois Inc 2014-2020 |
|---|---|
| License | BSD3 |
| Maintainer | Joe Hendrix <jhendrix@galois.com> |
| Stability | provisional |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
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
- 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
- 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')
- class KnownRepr (f :: k -> Type) (ctx :: k) where
- knownRepr :: f ctx
- type KnownCtx f = KnownRepr (Assignment f)
BaseType data kind
This data kind enumerates the Crucible solver interface types, which are types that may be represented symbolically.
Instances
| TestEquality BaseTypeRepr Source # | |
Defined in What4.BaseTypes Methods testEquality :: forall (a :: k) (b :: k). BaseTypeRepr a -> BaseTypeRepr 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 IndexLit | |
Defined in What4.IndexLit Methods testEquality :: forall (a :: k) (b :: k). IndexLit a -> IndexLit 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) | |
| TestEquality OnlyIntRepr | |
Defined in What4.Utils.OnlyIntRepr Methods testEquality :: forall (a :: k) (b :: k). OnlyIntRepr a -> OnlyIntRepr b -> Maybe (a :~: b) | |
| HashableF BaseTypeRepr Source # | |
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 | |
| HashableF OnlyIntRepr | |
Defined in What4.Utils.OnlyIntRepr Methods hashWithSaltF :: forall (tp :: k). Int -> OnlyIntRepr tp -> Int hashF :: forall (tp :: k). OnlyIntRepr tp -> Int | |
| OrdF BaseTypeRepr Source # | |
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 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 | |
| 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 | |
| ShowF BaseTypeRepr Source # | |
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 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 OptionSetting | |
Defined in What4.Config Methods withShow :: forall p q (tp :: k) a. p OptionSetting -> q tp -> (Show (OptionSetting tp) => a) -> a showF :: forall (tp :: k). OptionSetting tp -> String showsPrecF :: forall (tp :: k). Int -> OptionSetting tp -> String -> String | |
| ShowF IndexLit | |
Defined in What4.IndexLit | |
| ShowF TypeMap | |
Defined in What4.Protocol.SMTWriter | |
| KnownRepr BaseTypeRepr BaseBoolType Source # | |
Defined in What4.BaseTypes Methods | |
| KnownRepr BaseTypeRepr BaseComplexType Source # | |
Defined in What4.BaseTypes Methods | |
| KnownRepr BaseTypeRepr BaseIntegerType Source # | |
Defined in What4.BaseTypes Methods | |
| KnownRepr BaseTypeRepr BaseRealType Source # | |
Defined in What4.BaseTypes Methods | |
| 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] | |
| (1 <= w, KnownNat w) => KnownRepr BaseTypeRepr (BaseBVType w :: BaseType) Source # | |
Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseBVType w) # | |
| KnownRepr FloatPrecisionRepr fpp => KnownRepr BaseTypeRepr (BaseFloatType fpp :: BaseType) Source # | |
Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseFloatType fpp) # | |
| KnownRepr StringInfoRepr si => KnownRepr BaseTypeRepr (BaseStringType si :: BaseType) Source # | |
Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseStringType si) # | |
| KnownRepr (Assignment BaseTypeRepr) ctx => KnownRepr BaseTypeRepr (BaseStructType ctx :: BaseType) Source # | |
Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseStructType ctx) # | |
| 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] | |
| FunctorFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) | |
Defined in What4.Expr.App | |
| 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) idx, KnownRepr BaseTypeRepr tp, KnownRepr BaseTypeRepr t) => KnownRepr BaseTypeRepr (BaseArrayType (idx ::> tp) t :: BaseType) Source # | |
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 (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 (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 (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 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 | |
| HashableF (Expr t :: BaseType -> Type) | |
Defined in What4.Expr.App Methods hashWithSaltF :: forall (tp :: k). Int -> Expr t 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 | |
| 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 (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 (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 (Expr t :: BaseType -> Type) | |
Defined in What4.Expr.App | |
| 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 | |
| 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) | |
| 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) | |
| (HashableF e, TestEquality e) => HashableF (NonceApp t e :: BaseType -> Type) | |
Defined in What4.Expr.App Methods hashWithSaltF :: forall (tp :: k). Int -> NonceApp t e tp -> Int | |
| 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 | |
| HasAbsValue (Dummy :: BaseType -> Type) Source # | |
Defined in What4.Expr.App Methods getAbsValue :: forall (tp :: BaseType). Dummy tp -> AbstractValue tp Source # | |
| IsSymFn (SymFn sym) => TestEquality (SymFnWrapper sym :: Ctx BaseType -> Type) | |
Defined in What4.Interface Methods testEquality :: forall (a :: k) (b :: k). SymFnWrapper sym a -> SymFnWrapper sym b -> Maybe (a :~: b) | |
| IsSymFn (SymFn sym) => OrdF (SymFnWrapper sym :: Ctx BaseType -> Type) | |
Defined in What4.Interface Methods compareF :: forall (x :: k) (y :: k). SymFnWrapper sym x -> SymFnWrapper sym y -> OrderingF x y leqF :: forall (x :: k) (y :: k). SymFnWrapper sym x -> SymFnWrapper sym y -> Bool ltF :: forall (x :: k) (y :: k). SymFnWrapper sym x -> SymFnWrapper sym y -> Bool geqF :: forall (x :: k) (y :: k). SymFnWrapper sym x -> SymFnWrapper sym y -> Bool gtF :: forall (x :: k) (y :: k). SymFnWrapper sym x -> SymFnWrapper sym y -> Bool | |
Constructors for kind BaseType
type BaseBoolType Source #
Arguments
| = 'BaseBoolType |
|
type BaseIntegerType Source #
Arguments
| = 'BaseIntegerType |
|
type BaseRealType Source #
Arguments
| = 'BaseRealType |
|
type BaseStringType Source #
Arguments
| = 'BaseStringType |
|
type BaseBVType Source #
Arguments
| = 'BaseBVType |
|
type BaseFloatType Source #
Arguments
| = 'BaseFloatType |
|
type BaseComplexType Source #
Arguments
| = 'BaseComplexType |
|
type BaseStructType Source #
StringInfo data kind
data StringInfo Source #
Instances
| TestEquality StringInfoRepr Source # | |
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) | |
| HashableF StringInfoRepr Source # | |
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 | |
| OrdF StringInfoRepr Source # | |
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 Source # | |
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 | |
| KnownRepr StringInfoRepr Char16 Source # | |
Defined in What4.BaseTypes Methods | |
| KnownRepr StringInfoRepr Char8 Source # | |
Defined in What4.BaseTypes Methods | |
| KnownRepr StringInfoRepr Unicode Source # | |
Defined in What4.BaseTypes Methods | |
| (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 | |
Constructors for StringInfo
Arguments
| = 'Char8 |
|
Arguments
| = 'Char16 |
|
Arguments
| = 'Unicode |
|
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
| TestEquality FloatPrecisionRepr Source # | |
Defined in What4.BaseTypes Methods testEquality :: forall (a :: k) (b :: k). FloatPrecisionRepr a -> FloatPrecisionRepr b -> Maybe (a :~: b) | |
| HashableF FloatPrecisionRepr Source # | |
Defined in What4.BaseTypes Methods hashWithSaltF :: forall (tp :: k). Int -> FloatPrecisionRepr tp -> Int hashF :: forall (tp :: k). FloatPrecisionRepr tp -> Int | |
| OrdF FloatPrecisionRepr Source # | |
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 # | |
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 | |
| (2 <= eb, 2 <= es, KnownNat eb, KnownNat es) => KnownRepr FloatPrecisionRepr (FloatingPointPrecision eb es :: FloatPrecision) Source # | |
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 |
|
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
data FloatPrecisionRepr (fpp :: FloatPrecision) where Source #
Constructors
| FloatingPointPrecisionRepr :: (2 <= eb, 2 <= sb) => !(NatRepr eb) -> !(NatRepr sb) -> FloatPrecisionRepr (FloatingPointPrecision eb sb) |
Instances
data StringInfoRepr (si :: StringInfo) where Source #
Constructors
| Char8Repr :: StringInfoRepr Char8 | |
| Char16Repr :: StringInfoRepr Char16 | |
| UnicodeRepr :: StringInfoRepr Unicode |
Instances
| TestEquality StringInfoRepr Source # | |
Defined in What4.BaseTypes Methods testEquality :: forall (a :: k) (b :: k). StringInfoRepr a -> StringInfoRepr b -> Maybe (a :~: b) | |
| HashableF StringInfoRepr Source # | |
Defined in What4.BaseTypes Methods hashWithSaltF :: forall (tp :: k). Int -> StringInfoRepr tp -> Int hashF :: forall (tp :: k). StringInfoRepr tp -> Int | |
| OrdF StringInfoRepr Source # | |
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 # | |
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 | |
| KnownRepr StringInfoRepr Char16 Source # | |
Defined in What4.BaseTypes Methods | |
| KnownRepr StringInfoRepr Char8 Source # | |
Defined in What4.BaseTypes Methods | |
| KnownRepr StringInfoRepr Unicode Source # | |
Defined in What4.BaseTypes Methods | |
| Show (StringInfoRepr si) Source # | |
Defined in What4.BaseTypes Methods showsPrec :: Int -> StringInfoRepr si -> ShowS show :: StringInfoRepr si -> String showList :: [StringInfoRepr si] -> ShowS | |
| Eq (StringInfoRepr si) Source # | |
Defined in What4.BaseTypes Methods (==) :: StringInfoRepr si -> StringInfoRepr si -> Bool (/=) :: StringInfoRepr si -> StringInfoRepr si -> Bool | |
| Hashable (StringInfoRepr si) Source # | |
Defined in What4.BaseTypes | |
| Pretty (StringInfoRepr si) Source # | |
Defined in What4.BaseTypes | |
arrayTypeIndices :: BaseTypeRepr (BaseArrayType idx tp) -> Assignment BaseTypeRepr idx Source #
Return the type of the indices for an array type.
arrayTypeResult :: BaseTypeRepr (BaseArrayType idx tp) -> BaseTypeRepr tp Source #
Return the result type of an array type.
floatPrecisionToBVType :: FloatPrecisionRepr (FloatingPointPrecision eb sb) -> BaseTypeRepr (BaseBVType (eb + sb)) Source #
lemmaFloatPrecisionIsPos :: forall eb' sb'. FloatPrecisionRepr (FloatingPointPrecision eb' sb') -> LeqProof 1 (eb' + sb') Source #
KnownRepr
class KnownRepr (f :: k -> Type) (ctx :: k) where #