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

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) where
  - BaseBoolRepr :: BaseTypeRepr 'BaseBoolType
  - BaseBVRepr :: forall (w :: Natural). 1 <= w => !(NatRepr w) -> BaseTypeRepr ('BaseBVType w)
  - BaseIntegerRepr :: BaseTypeRepr 'BaseIntegerType
  - BaseRealRepr :: BaseTypeRepr 'BaseRealType
  - BaseFloatRepr :: forall (fpp :: FloatPrecision). !(FloatPrecisionRepr fpp) -> BaseTypeRepr ('BaseFloatType fpp)
  - BaseStringRepr :: forall (si :: StringInfo). StringInfoRepr si -> BaseTypeRepr ('BaseStringType si)
  - BaseComplexRepr :: BaseTypeRepr 'BaseComplexType
  - BaseStructRepr :: forall (ctx :: Ctx BaseType). !(Assignment BaseTypeRepr ctx) -> BaseTypeRepr ('BaseStructType ctx)
  - BaseArrayRepr :: forall (idx :: Ctx BaseType) (tp :: BaseType) (xs :: BaseType). !(Assignment BaseTypeRepr (idx ::> tp)) -> !(BaseTypeRepr xs) -> BaseTypeRepr ('BaseArrayType (idx ::> tp) xs)
- data FloatPrecisionRepr (fpp :: FloatPrecision) where
  - FloatingPointPrecisionRepr :: forall (eb :: Natural) (sb :: Natural). (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 :: forall (idx :: Ctx BaseType) (tp :: BaseType). BaseTypeRepr (BaseArrayType idx tp) -> Assignment BaseTypeRepr idx
- arrayTypeResult :: forall (idx :: Ctx BaseType) (tp :: BaseType). BaseTypeRepr (BaseArrayType idx tp) -> BaseTypeRepr tp
- floatPrecisionToBVType :: forall (eb :: Nat) (sb :: Nat). FloatPrecisionRepr (FloatingPointPrecision eb sb) -> BaseTypeRepr (BaseBVType (eb + sb))
- lemmaFloatPrecisionIsPos :: forall (eb' :: Nat) (sb' :: Nat). 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 :: k -> Type) = 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 :: BaseType) (b :: BaseType). BaseTypeRepr a -> BaseTypeRepr b -> Maybe (a :~: b) Source #
TestEquality ConcreteVal Source # |
Instance details Defined in What4.Concrete Methods testEquality :: forall (a :: BaseType) (b :: BaseType). ConcreteVal a -> ConcreteVal b -> Maybe (a :~: b) Source #
TestEquality IndexLit Source # |
Instance details Defined in What4.IndexLit Methods testEquality :: forall (a :: BaseType) (b :: BaseType). IndexLit a -> IndexLit b -> Maybe (a :~: b) Source #
TestEquality TypeMap Source # |
Instance details Defined in What4.Protocol.SMTWriter Methods testEquality :: forall (a :: BaseType) (b :: BaseType). TypeMap a -> TypeMap b -> Maybe (a :~: b) Source #
TestEquality OnlyIntRepr Source # |
Instance details Defined in What4.Utils.OnlyIntRepr Methods testEquality :: forall (a :: BaseType) (b :: BaseType). OnlyIntRepr a -> OnlyIntRepr b -> Maybe (a :~: b) Source #
HashableF BaseTypeRepr Source # |
Instance details Defined in What4.BaseTypes Methods hashWithSaltF :: forall (tp :: BaseType). Int -> BaseTypeRepr tp -> Int Source # hashF :: forall (tp :: BaseType). BaseTypeRepr tp -> Int Source #
HashableF IndexLit Source # |
Instance details Defined in What4.IndexLit Methods hashWithSaltF :: forall (tp :: BaseType). Int -> IndexLit tp -> Int Source # hashF :: forall (tp :: BaseType). IndexLit tp -> Int Source #
HashableF OnlyIntRepr Source # |
Instance details Defined in What4.Utils.OnlyIntRepr Methods hashWithSaltF :: forall (tp :: BaseType). Int -> OnlyIntRepr tp -> Int Source # hashF :: forall (tp :: BaseType). OnlyIntRepr tp -> Int Source #
OrdF BaseTypeRepr Source # |

Instance details

Defined in What4.BaseTypes

Methods

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

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

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

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

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

OrdF ConcreteVal Source # |

Instance details

Defined in What4.Concrete

Methods

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

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

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

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

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

OrdF IndexLit Source # |

Instance details

Defined in What4.IndexLit

Methods

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

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

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

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

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

ShowF BaseTypeRepr Source # |
Instance details Defined in What4.BaseTypes Methods withShow :: forall p q (tp :: BaseType) a. p BaseTypeRepr -> q tp -> (Show (BaseTypeRepr tp) => a) -> a Source # showF :: forall (tp :: BaseType). BaseTypeRepr tp -> String Source # showsPrecF :: forall (tp :: BaseType). Int -> BaseTypeRepr tp -> String -> String Source #
ShowF ConcreteVal Source # |
Instance details Defined in What4.Concrete Methods withShow :: forall p q (tp :: BaseType) a. p ConcreteVal -> q tp -> (Show (ConcreteVal tp) => a) -> a Source # showF :: forall (tp :: BaseType). ConcreteVal tp -> String Source # showsPrecF :: forall (tp :: BaseType). Int -> ConcreteVal tp -> String -> String Source #
ShowF OptionSetting Source # |
Instance details Defined in What4.Config Methods withShow :: forall p q (tp :: BaseType) a. p OptionSetting -> q tp -> (Show (OptionSetting tp) => a) -> a Source # showF :: forall (tp :: BaseType). OptionSetting tp -> String Source # showsPrecF :: forall (tp :: BaseType). Int -> OptionSetting tp -> String -> String Source #
ShowF IndexLit Source # |
Instance details Defined in What4.IndexLit Methods withShow :: forall p q (tp :: BaseType) a. p IndexLit -> q tp -> (Show (IndexLit tp) => a) -> a Source # showF :: forall (tp :: BaseType). IndexLit tp -> String Source # showsPrecF :: forall (tp :: BaseType). Int -> IndexLit tp -> String -> String Source #
ShowF TypeMap Source # |
Instance details Defined in What4.Protocol.SMTWriter Methods withShow :: forall p q (tp :: BaseType) a. p TypeMap -> q tp -> (Show (TypeMap tp) => a) -> a Source # showF :: forall (tp :: BaseType). TypeMap tp -> String Source # showsPrecF :: forall (tp :: BaseType). Int -> TypeMap tp -> String -> String Source #
KnownRepr BaseTypeRepr BaseBoolType Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseBoolType Source #
KnownRepr BaseTypeRepr BaseComplexType Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseComplexType Source #
KnownRepr BaseTypeRepr BaseIntegerType Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseIntegerType Source #
KnownRepr BaseTypeRepr BaseRealType Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseRealType Source #
FoldableFC App Source # |

Instance details

Defined in What4.Expr.App

Methods

foldMapFC :: forall f m. Monoid m => (forall (x :: BaseType). f x -> m) -> forall (x :: BaseType). App f x -> m Source #

foldrFC :: (forall (x :: BaseType). f x -> b -> b) -> forall (x :: BaseType). b -> App f x -> b Source #

foldlFC :: forall f b. (forall (x :: BaseType). b -> f x -> b) -> forall (x :: BaseType). b -> App f x -> b Source #

foldrFC' :: (forall (x :: BaseType). f x -> b -> b) -> forall (x :: BaseType). b -> App f x -> b Source #

foldlFC' :: forall f b. (forall (x :: BaseType). b -> f x -> b) -> forall (x :: BaseType). b -> App f x -> b Source #

toListFC :: (forall (x :: BaseType). f x -> a) -> forall (x :: BaseType). App f x -> [a] Source #

(1 <= w, KnownNat w) => KnownRepr BaseTypeRepr (BaseBVType w :: BaseType) Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseBVType w) Source #
KnownRepr FloatPrecisionRepr fpp => KnownRepr BaseTypeRepr (BaseFloatType fpp :: BaseType) Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseFloatType fpp) Source #
KnownRepr StringInfoRepr si => KnownRepr BaseTypeRepr (BaseStringType si :: BaseType) Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseStringType si) Source #
KnownRepr (Assignment BaseTypeRepr) ctx => KnownRepr BaseTypeRepr (BaseStructType ctx :: BaseType) Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseStructType ctx) Source #
FoldableFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) Source # |

Instance details

Defined in What4.Expr.App

Methods

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

foldrFC :: (forall (x :: BaseType). f x -> b -> b) -> forall (x :: BaseType). b -> NonceApp t f x -> b Source #

foldlFC :: forall f b. (forall (x :: BaseType). b -> f x -> b) -> forall (x :: BaseType). b -> NonceApp t f x -> b Source #

foldrFC' :: (forall (x :: BaseType). f x -> b -> b) -> forall (x :: BaseType). b -> NonceApp t f x -> b Source #

foldlFC' :: forall f b. (forall (x :: BaseType). b -> f x -> b) -> forall (x :: BaseType). b -> NonceApp t f x -> b Source #

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

FunctorFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods fmapFC :: (forall (x :: BaseType). f x -> g x) -> forall (x :: BaseType). NonceApp t f x -> NonceApp t g x Source #
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 :: BaseType). f x -> m (g x)) -> forall (x :: BaseType). NonceApp t f x -> m (NonceApp t g x) Source #
(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) Source #
(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 :: BaseType) (b :: BaseType). App e a -> App e b -> Maybe (a :~: b) Source #
TestEquality (Expr t :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods testEquality :: forall (a :: BaseType) (b :: BaseType). Expr t a -> Expr t b -> Maybe (a :~: b) Source #
TestEquality (ExprBoundVar t :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods testEquality :: forall (a :: BaseType) (b :: BaseType). ExprBoundVar t a -> ExprBoundVar t b -> Maybe (a :~: b) Source #
TestEquality (NonceAppExpr t :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods testEquality :: forall (a :: BaseType) (b :: BaseType). NonceAppExpr t a -> NonceAppExpr t b -> Maybe (a :~: b) Source #
(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 :: BaseType). Int -> App e tp -> Int Source # hashF :: forall (tp :: BaseType). App e tp -> Int Source #
HashableF (Expr t :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods hashWithSaltF :: forall (tp :: BaseType). Int -> Expr t tp -> Int Source # hashF :: forall (tp :: BaseType). Expr t tp -> Int Source #
HashableF (ExprBoundVar t :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods hashWithSaltF :: forall (tp :: BaseType). Int -> ExprBoundVar t tp -> Int Source # hashF :: forall (tp :: BaseType). ExprBoundVar t tp -> Int Source #
OrdF (Expr t :: BaseType -> Type) Source # |

Instance details

Defined in What4.Expr.App

Methods

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

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

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

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

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

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

Instance details

Defined in What4.Expr.App

Methods

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

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

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

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

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

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

Instance details

Defined in What4.Expr.App

Methods

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

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

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

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

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

ShowF (Expr t :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods withShow :: forall p q (tp :: BaseType) a. p (Expr t) -> q tp -> (Show (Expr t tp) => a) -> a Source # showF :: forall (tp :: BaseType). Expr t tp -> String Source # showsPrecF :: forall (tp :: BaseType). Int -> Expr t tp -> String -> String Source #
ShowF (ExprBoundVar t :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods withShow :: forall p q (tp :: BaseType) a. p (ExprBoundVar t) -> q tp -> (Show (ExprBoundVar t tp) => a) -> a Source # showF :: forall (tp :: BaseType). ExprBoundVar t tp -> String Source # showsPrecF :: forall (tp :: BaseType). Int -> ExprBoundVar t tp -> String -> String Source #
TestEquality e => TestEquality (NonceApp t e :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods testEquality :: forall (a :: BaseType) (b :: BaseType). NonceApp t e a -> NonceApp t e b -> Maybe (a :~: b) Source #
TestEquality f => TestEquality (ArrayResultWrapper f idx :: BaseType -> Type) Source # |
Instance details Defined in What4.Interface Methods testEquality :: forall (a :: BaseType) (b :: BaseType). ArrayResultWrapper f idx a -> ArrayResultWrapper f idx b -> Maybe (a :~: b) Source #
(HashableF e, TestEquality e) => HashableF (NonceApp t e :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods hashWithSaltF :: forall (tp :: BaseType). Int -> NonceApp t e tp -> Int Source # hashF :: forall (tp :: BaseType). NonceApp t e tp -> Int Source #
HashableF e => HashableF (ArrayResultWrapper e idx :: BaseType -> Type) Source # |
Instance details Defined in What4.Interface Methods hashWithSaltF :: forall (tp :: BaseType). Int -> ArrayResultWrapper e idx tp -> Int Source # hashF :: forall (tp :: BaseType). ArrayResultWrapper e idx tp -> Int Source #
HasAbsValue (Dummy :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods getAbsValue :: forall (tp :: BaseType). Dummy tp -> AbstractValue tp Source #
IsSymFn (SymFn sym) => TestEquality (SymFnWrapper sym :: Ctx BaseType -> Type) Source # |
Instance details Defined in What4.Interface Methods testEquality :: forall (a :: Ctx BaseType) (b :: Ctx BaseType). SymFnWrapper sym a -> SymFnWrapper sym b -> Maybe (a :~: b) Source #
IsSymFn (SymFn sym) => OrdF (SymFnWrapper sym :: Ctx BaseType -> Type) Source # |

Instance details

Defined in What4.Interface

Methods

compareF :: forall (x :: Ctx BaseType) (y :: Ctx BaseType). SymFnWrapper sym x -> SymFnWrapper sym y -> OrderingF x y Source #

leqF :: forall (x :: Ctx BaseType) (y :: Ctx BaseType). SymFnWrapper sym x -> SymFnWrapper sym y -> Bool Source #

ltF :: forall (x :: Ctx BaseType) (y :: Ctx BaseType). SymFnWrapper sym x -> SymFnWrapper sym y -> Bool Source #

geqF :: forall (x :: Ctx BaseType) (y :: Ctx BaseType). SymFnWrapper sym x -> SymFnWrapper sym y -> Bool Source #

gtF :: forall (x :: Ctx BaseType) (y :: Ctx BaseType). SymFnWrapper sym x -> SymFnWrapper sym y -> Bool 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 :: StringInfo) (b :: StringInfo). StringInfoRepr a -> StringInfoRepr b -> Maybe (a :~: b) Source #
TestEquality StringLiteral Source # |
Instance details Defined in What4.Utils.StringLiteral Methods testEquality :: forall (a :: StringInfo) (b :: StringInfo). StringLiteral a -> StringLiteral b -> Maybe (a :~: b) Source #
HashableF StringInfoRepr Source # |
Instance details Defined in What4.BaseTypes Methods hashWithSaltF :: forall (tp :: StringInfo). Int -> StringInfoRepr tp -> Int Source # hashF :: forall (tp :: StringInfo). StringInfoRepr tp -> Int Source #
HashableF StringLiteral Source # |
Instance details Defined in What4.Utils.StringLiteral Methods hashWithSaltF :: forall (tp :: StringInfo). Int -> StringLiteral tp -> Int Source # hashF :: forall (tp :: StringInfo). StringLiteral tp -> Int Source #
OrdF StringInfoRepr Source # |

Instance details

Defined in What4.BaseTypes

Methods

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

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

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

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

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

OrdF StringLiteral Source # |

Instance details

Defined in What4.Utils.StringLiteral

Methods

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

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

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

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

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

ShowF StringInfoRepr Source # |
Instance details Defined in What4.BaseTypes Methods withShow :: forall p q (tp :: StringInfo) a. p StringInfoRepr -> q tp -> (Show (StringInfoRepr tp) => a) -> a Source # showF :: forall (tp :: StringInfo). StringInfoRepr tp -> String Source # showsPrecF :: forall (tp :: StringInfo). Int -> StringInfoRepr tp -> String -> String Source #
ShowF StringLiteral Source # |
Instance details Defined in What4.Utils.StringLiteral Methods withShow :: forall p q (tp :: StringInfo) a. p StringLiteral -> q tp -> (Show (StringLiteral tp) => a) -> a Source # showF :: forall (tp :: StringInfo). StringLiteral tp -> String Source # showsPrecF :: forall (tp :: StringInfo). Int -> StringLiteral tp -> String -> String Source #
KnownRepr StringInfoRepr Char16 Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: StringInfoRepr Char16 Source #
KnownRepr StringInfoRepr Char8 Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: StringInfoRepr Char8 Source #
KnownRepr StringInfoRepr Unicode Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: StringInfoRepr Unicode Source #
(TestEquality e, HasAbsValue e, HashableF e) => TestEquality (StringSeq e :: StringInfo -> Type) Source # |
Instance details Defined in What4.Expr.StringSeq Methods testEquality :: forall (a :: StringInfo) (b :: StringInfo). StringSeq e a -> StringSeq e b -> Maybe (a :~: b) Source #
(HasAbsValue e, HashableF e) => HashableF (StringSeq e :: StringInfo -> Type) Source # |
Instance details Defined in What4.Expr.StringSeq Methods hashWithSaltF :: forall (tp :: StringInfo). Int -> StringSeq e tp -> Int Source # hashF :: forall (tp :: StringInfo). StringSeq e tp -> Int Source #

## 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 :: FloatPrecision) (b :: FloatPrecision). FloatPrecisionRepr a -> FloatPrecisionRepr b -> Maybe (a :~: b) Source #
HashableF FloatPrecisionRepr Source # |
Instance details Defined in What4.BaseTypes Methods hashWithSaltF :: forall (tp :: FloatPrecision). Int -> FloatPrecisionRepr tp -> Int Source # hashF :: forall (tp :: FloatPrecision). FloatPrecisionRepr tp -> Int Source #
OrdF FloatPrecisionRepr Source # |

Instance details

Defined in What4.BaseTypes

Methods

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

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

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

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

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

ShowF FloatPrecisionRepr Source # |
Instance details Defined in What4.BaseTypes Methods withShow :: forall p q (tp :: FloatPrecision) a. p FloatPrecisionRepr -> q tp -> (Show (FloatPrecisionRepr tp) => a) -> a Source # showF :: forall (tp :: FloatPrecision). FloatPrecisionRepr tp -> String Source # showsPrecF :: forall (tp :: FloatPrecision). Int -> FloatPrecisionRepr tp -> String -> String Source #
(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) Source #

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) where Source #

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

Constructors

BaseBoolRepr :: BaseTypeRepr 'BaseBoolType |
BaseBVRepr :: forall (w :: Natural). 1 <= w => !(NatRepr w) -> BaseTypeRepr ('BaseBVType w) |
BaseIntegerRepr :: BaseTypeRepr 'BaseIntegerType |
BaseRealRepr :: BaseTypeRepr 'BaseRealType |
BaseFloatRepr :: forall (fpp :: FloatPrecision). !(FloatPrecisionRepr fpp) -> BaseTypeRepr ('BaseFloatType fpp) |
BaseStringRepr :: forall (si :: StringInfo). StringInfoRepr si -> BaseTypeRepr ('BaseStringType si) |
BaseComplexRepr :: BaseTypeRepr 'BaseComplexType |
BaseStructRepr :: forall (ctx :: Ctx BaseType). !(Assignment BaseTypeRepr ctx) -> BaseTypeRepr ('BaseStructType ctx) |
BaseArrayRepr :: forall (idx :: Ctx BaseType) (tp :: BaseType) (xs :: BaseType). !(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 :: BaseType) (b :: BaseType). BaseTypeRepr a -> BaseTypeRepr b -> Maybe (a :~: b) Source #
HashableF BaseTypeRepr Source # |
Instance details Defined in What4.BaseTypes Methods hashWithSaltF :: forall (tp :: BaseType). Int -> BaseTypeRepr tp -> Int Source # hashF :: forall (tp :: BaseType). BaseTypeRepr tp -> Int Source #
OrdF BaseTypeRepr Source # |

Instance details

Defined in What4.BaseTypes

Methods

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

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

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

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

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

ShowF BaseTypeRepr Source # |
Instance details Defined in What4.BaseTypes Methods withShow :: forall p q (tp :: BaseType) a. p BaseTypeRepr -> q tp -> (Show (BaseTypeRepr tp) => a) -> a Source # showF :: forall (tp :: BaseType). BaseTypeRepr tp -> String Source # showsPrecF :: forall (tp :: BaseType). Int -> BaseTypeRepr tp -> String -> String Source #
KnownRepr BaseTypeRepr BaseBoolType Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseBoolType Source #
KnownRepr BaseTypeRepr BaseComplexType Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseComplexType Source #
KnownRepr BaseTypeRepr BaseIntegerType Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseIntegerType Source #
KnownRepr BaseTypeRepr BaseRealType Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseRealType Source #
(1 <= w, KnownNat w) => KnownRepr BaseTypeRepr (BaseBVType w :: BaseType) Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseBVType w) Source #
KnownRepr FloatPrecisionRepr fpp => KnownRepr BaseTypeRepr (BaseFloatType fpp :: BaseType) Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseFloatType fpp) Source #
KnownRepr StringInfoRepr si => KnownRepr BaseTypeRepr (BaseStringType si :: BaseType) Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseStringType si) Source #
KnownRepr (Assignment BaseTypeRepr) ctx => KnownRepr BaseTypeRepr (BaseStructType ctx :: BaseType) Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseStructType ctx) Source #
(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) Source #
Show (BaseTypeRepr bt) Source # |
Instance details Defined in What4.BaseTypes Methods showsPrec :: Int -> BaseTypeRepr bt -> ShowS Source # show :: BaseTypeRepr bt -> String Source # showList :: [BaseTypeRepr bt] -> ShowS Source #
Eq (BaseTypeRepr bt) Source # |
Instance details Defined in What4.BaseTypes Methods (==) :: BaseTypeRepr bt -> BaseTypeRepr bt -> Bool Source # (/=) :: BaseTypeRepr bt -> BaseTypeRepr bt -> Bool Source #
Hashable (BaseTypeRepr bt) Source # |
Instance details Defined in What4.BaseTypes Methods hashWithSalt :: Int -> BaseTypeRepr bt -> Int Source # hash :: BaseTypeRepr bt -> Int Source #
Pretty (BaseTypeRepr bt) Source # |
Instance details Defined in What4.BaseTypes Methods pretty :: BaseTypeRepr bt -> Doc ann Source # prettyList :: [BaseTypeRepr bt] -> Doc ann Source #

data FloatPrecisionRepr (fpp :: FloatPrecision) where Source #

Constructors

FloatingPointPrecisionRepr :: forall (eb :: Natural) (sb :: Natural). (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 :: FloatPrecision) (b :: FloatPrecision). FloatPrecisionRepr a -> FloatPrecisionRepr b -> Maybe (a :~: b) Source #
HashableF FloatPrecisionRepr Source # |
Instance details Defined in What4.BaseTypes Methods hashWithSaltF :: forall (tp :: FloatPrecision). Int -> FloatPrecisionRepr tp -> Int Source # hashF :: forall (tp :: FloatPrecision). FloatPrecisionRepr tp -> Int Source #
OrdF FloatPrecisionRepr Source # |

Instance details

Defined in What4.BaseTypes

Methods

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

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

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

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

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

ShowF FloatPrecisionRepr Source # |
Instance details Defined in What4.BaseTypes Methods withShow :: forall p q (tp :: FloatPrecision) a. p FloatPrecisionRepr -> q tp -> (Show (FloatPrecisionRepr tp) => a) -> a Source # showF :: forall (tp :: FloatPrecision). FloatPrecisionRepr tp -> String Source # showsPrecF :: forall (tp :: FloatPrecision). Int -> FloatPrecisionRepr tp -> String -> String Source #
(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) Source #
Show (FloatPrecisionRepr fpp) Source # |
Instance details Defined in What4.BaseTypes Methods showsPrec :: Int -> FloatPrecisionRepr fpp -> ShowS Source # show :: FloatPrecisionRepr fpp -> String Source # showList :: [FloatPrecisionRepr fpp] -> ShowS Source #
Eq (FloatPrecisionRepr fpp) Source # |
Instance details Defined in What4.BaseTypes Methods (==) :: FloatPrecisionRepr fpp -> FloatPrecisionRepr fpp -> Bool Source # (/=) :: FloatPrecisionRepr fpp -> FloatPrecisionRepr fpp -> Bool Source #
Hashable (FloatPrecisionRepr fpp) Source # |
Instance details Defined in What4.BaseTypes Methods hashWithSalt :: Int -> FloatPrecisionRepr fpp -> Int Source # hash :: FloatPrecisionRepr fpp -> Int Source #
Pretty (FloatPrecisionRepr fpp) Source # |
Instance details Defined in What4.BaseTypes Methods pretty :: FloatPrecisionRepr fpp -> Doc ann Source # prettyList :: [FloatPrecisionRepr fpp] -> Doc ann Source #

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 :: StringInfo) (b :: StringInfo). StringInfoRepr a -> StringInfoRepr b -> Maybe (a :~: b) Source #
HashableF StringInfoRepr Source # |
Instance details Defined in What4.BaseTypes Methods hashWithSaltF :: forall (tp :: StringInfo). Int -> StringInfoRepr tp -> Int Source # hashF :: forall (tp :: StringInfo). StringInfoRepr tp -> Int Source #
OrdF StringInfoRepr Source # |

Instance details

Defined in What4.BaseTypes

Methods

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

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

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

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

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

ShowF StringInfoRepr Source # |
Instance details Defined in What4.BaseTypes Methods withShow :: forall p q (tp :: StringInfo) a. p StringInfoRepr -> q tp -> (Show (StringInfoRepr tp) => a) -> a Source # showF :: forall (tp :: StringInfo). StringInfoRepr tp -> String Source # showsPrecF :: forall (tp :: StringInfo). Int -> StringInfoRepr tp -> String -> String Source #
KnownRepr StringInfoRepr Char16 Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: StringInfoRepr Char16 Source #
KnownRepr StringInfoRepr Char8 Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: StringInfoRepr Char8 Source #
KnownRepr StringInfoRepr Unicode Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: StringInfoRepr Unicode Source #
Show (StringInfoRepr si) Source # |
Instance details Defined in What4.BaseTypes Methods showsPrec :: Int -> StringInfoRepr si -> ShowS Source # show :: StringInfoRepr si -> String Source # showList :: [StringInfoRepr si] -> ShowS Source #
Eq (StringInfoRepr si) Source # |
Instance details Defined in What4.BaseTypes Methods (==) :: StringInfoRepr si -> StringInfoRepr si -> Bool Source # (/=) :: StringInfoRepr si -> StringInfoRepr si -> Bool Source #
Hashable (StringInfoRepr si) Source # |
Instance details Defined in What4.BaseTypes Methods hashWithSalt :: Int -> StringInfoRepr si -> Int Source # hash :: StringInfoRepr si -> Int Source #
Pretty (StringInfoRepr si) Source # |
Instance details Defined in What4.BaseTypes Methods pretty :: StringInfoRepr si -> Doc ann Source # prettyList :: [StringInfoRepr si] -> Doc ann Source #

arrayTypeIndices :: forall (idx :: Ctx BaseType) (tp :: BaseType). BaseTypeRepr (BaseArrayType idx tp) -> Assignment BaseTypeRepr idx Source #

Return the type of the indices for an array type.

arrayTypeResult :: forall (idx :: Ctx BaseType) (tp :: BaseType). BaseTypeRepr (BaseArrayType idx tp) -> BaseTypeRepr tp Source #

Return the result type of an array type.

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

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

module Data.Parameterized.NatRepr

# KnownRepr

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

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 Source #

#### Instances

Instances details

KnownNat n => KnownRepr NatRepr (n :: Nat) |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods knownRepr :: NatRepr n Source #
KnownRepr PeanoRepr Z |
Instance details Defined in Data.Parameterized.Peano Methods knownRepr :: PeanoRepr Z Source #
KnownRepr BaseTypeRepr BaseBoolType Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseBoolType Source #
KnownRepr BaseTypeRepr BaseComplexType Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseComplexType Source #
KnownRepr BaseTypeRepr BaseIntegerType Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseIntegerType Source #
KnownRepr BaseTypeRepr BaseRealType Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseRealType Source #
KnownRepr StringInfoRepr Char16 Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: StringInfoRepr Char16 Source #
KnownRepr StringInfoRepr Char8 Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: StringInfoRepr Char8 Source #
KnownRepr StringInfoRepr Unicode Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: StringInfoRepr Unicode Source #
KnownRepr FloatModeRepr FloatIEEE Source # |
Instance details Defined in What4.FloatMode Methods knownRepr :: FloatModeRepr FloatIEEE Source #
KnownRepr FloatModeRepr FloatReal Source # |
Instance details Defined in What4.FloatMode Methods knownRepr :: FloatModeRepr FloatReal Source #
KnownRepr FloatModeRepr FloatUninterpreted Source # |
Instance details Defined in What4.FloatMode Methods knownRepr :: FloatModeRepr FloatUninterpreted Source #
KnownRepr FloatInfoRepr DoubleDoubleFloat Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr DoubleDoubleFloat Source #
KnownRepr FloatInfoRepr DoubleFloat Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr DoubleFloat Source #
KnownRepr FloatInfoRepr HalfFloat Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr HalfFloat Source #
KnownRepr FloatInfoRepr QuadFloat Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr QuadFloat Source #
KnownRepr FloatInfoRepr SingleFloat Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr SingleFloat Source #
KnownRepr FloatInfoRepr X86_80Float Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr X86_80Float Source #
KnownRepr BoolRepr 'False |
Instance details Defined in Data.Parameterized.BoolRepr Methods knownRepr :: BoolRepr 'False Source #
KnownRepr BoolRepr 'True |
Instance details Defined in Data.Parameterized.BoolRepr Methods knownRepr :: BoolRepr 'True Source #
KnownSymbol s => KnownRepr SymbolRepr (s :: Symbol) |
Instance details Defined in Data.Parameterized.SymbolRepr Methods knownRepr :: SymbolRepr s Source #
KnownRepr PeanoRepr n => KnownRepr PeanoRepr (S n :: Peano) |
Instance details Defined in Data.Parameterized.Peano Methods knownRepr :: PeanoRepr (S n) Source #
(1 <= w, KnownNat w) => KnownRepr BaseTypeRepr (BaseBVType w :: BaseType) Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseBVType w) Source #
KnownRepr FloatPrecisionRepr fpp => KnownRepr BaseTypeRepr (BaseFloatType fpp :: BaseType) Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseFloatType fpp) Source #
KnownRepr StringInfoRepr si => KnownRepr BaseTypeRepr (BaseStringType si :: BaseType) Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseStringType si) Source #
KnownRepr (Assignment BaseTypeRepr) ctx => KnownRepr BaseTypeRepr (BaseStructType ctx :: BaseType) Source # |
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseStructType ctx) Source #
(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) Source #
(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) Source #
KnownRepr (Proxy :: k -> Type) (ctx :: k) |
Instance details Defined in Data.Parameterized.Classes Methods knownRepr :: Proxy ctx Source #
KnownRepr (Assignment f :: Ctx k -> Type) (EmptyCtx :: Ctx k) |
Instance details Defined in Data.Parameterized.Context.Safe Methods knownRepr :: Assignment f (EmptyCtx :: Ctx k) Source #
KnownRepr (Assignment f :: Ctx k -> Type) (EmptyCtx :: Ctx k) |
Instance details Defined in Data.Parameterized.Context.Unsafe Methods knownRepr :: Assignment f (EmptyCtx :: Ctx k) Source #
KnownRepr (List f :: [k] -> Type) ('[] :: [k]) |
Instance details Defined in Data.Parameterized.List Methods knownRepr :: List f ('[] :: [k]) Source #
(KnownRepr (Assignment f) ctx, KnownRepr f bt) => KnownRepr (Assignment f :: Ctx k -> Type) (ctx ::> bt :: Ctx k) |
Instance details Defined in Data.Parameterized.Context.Safe Methods knownRepr :: Assignment f (ctx ::> bt) Source #
(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) Source #
(KnownRepr f s, KnownRepr (List f) sh) => KnownRepr (List f :: [a] -> Type) (s ': sh :: [a]) |
Instance details Defined in Data.Parameterized.List Methods knownRepr :: List f (s ': sh) Source #

type KnownCtx (f :: k -> Type) = KnownRepr (Assignment f) Source #

A Context where all the argument types are `KnownRepr` instances