Copyright	(c) Galois Inc 2014-2020
License	BSD3
Maintainer	Joe Hendrix <[email protected]>
Stability	provisional
Safe Haskell	Safe-Inferred
Language	Haskell2010

What4.BaseTypes

Contents

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 ConcreteVal Source #
Instance details Defined in What4.Concrete Methods testEquality :: forall (a :: k) (b :: k). ConcreteVal a -> ConcreteVal 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 TypeMap Source #
Instance details Defined in What4.Protocol.SMTWriter Methods testEquality :: forall (a :: k) (b :: k). TypeMap a -> TypeMap 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) #
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 #
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 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 #
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 #
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 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 OptionSetting Source #
Instance details 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 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 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 #
FoldableF BoolMap Source #	Specialized version of `foldMapVars`
Instance details Defined in What4.Expr.BoolMap Methods foldMapF :: Monoid m => (forall (s :: k). e s -> m) -> BoolMap e -> m # foldrF :: (forall (s :: k). e s -> b -> b) -> b -> BoolMap e -> b # foldlF :: (forall (s :: k). b -> e s -> b) -> b -> BoolMap e -> b # foldrF' :: (forall (s :: k). e s -> b -> b) -> b -> BoolMap e -> b # foldlF' :: (forall (s :: k). b -> e s -> b) -> b -> BoolMap e -> b # toListF :: (forall (tp :: k). f tp -> a) -> BoolMap f -> [a] #
FoldableF ConjMap Source #
Instance details Defined in What4.Expr.BoolMap Methods foldMapF :: Monoid m => (forall (s :: k). e s -> m) -> ConjMap e -> m # foldrF :: (forall (s :: k). e s -> b -> b) -> b -> ConjMap e -> b # foldlF :: (forall (s :: k). b -> e s -> b) -> b -> ConjMap e -> b # foldrF' :: (forall (s :: k). e s -> b -> b) -> b -> ConjMap e -> b # foldlF' :: (forall (s :: k). b -> e s -> b) -> b -> ConjMap e -> b # toListF :: (forall (tp :: k). f tp -> a) -> ConjMap f -> [a] #
KnownRepr BaseTypeRepr BaseBoolType Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseBoolType #
KnownRepr BaseTypeRepr BaseComplexType Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseComplexType #
KnownRepr BaseTypeRepr BaseIntegerType Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseIntegerType #
KnownRepr BaseTypeRepr BaseRealType Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseRealType #
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] #
(1 <= w, KnownNat w) => KnownRepr BaseTypeRepr (BaseBVType w :: BaseType) Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseBVType w) #
KnownRepr FloatPrecisionRepr fpp => KnownRepr BaseTypeRepr (BaseFloatType fpp :: BaseType) Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseFloatType fpp) #
KnownRepr StringInfoRepr si => KnownRepr BaseTypeRepr (BaseStringType si :: BaseType) Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseStringType si) #
KnownRepr (Assignment BaseTypeRepr) ctx => KnownRepr BaseTypeRepr (BaseStructType ctx :: BaseType) Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseStructType ctx) #
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] #
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 #
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) 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 (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 (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 (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 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 (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 #
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 #
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 (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 (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 (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 #
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 #
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) #
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) #
(HashableF e, TestEquality 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 #
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 #
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 :: k) (b :: k). SymFnWrapper sym a -> SymFnWrapper sym b -> Maybe (a :~: b) #
IsSymFn (SymFn sym) => OrdF (SymFnWrapper sym :: Ctx BaseType -> Type) Source #
Instance details 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

:: 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) #
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 #
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 #
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 StringInfoRepr Unicode Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: StringInfoRepr Unicode #
(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) #
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 #
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 #
(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) #
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 #
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 #
KnownRepr BaseTypeRepr BaseBoolType Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseBoolType #
KnownRepr BaseTypeRepr BaseComplexType Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseComplexType #
KnownRepr BaseTypeRepr BaseIntegerType Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseIntegerType #
KnownRepr BaseTypeRepr BaseRealType Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseRealType #
(1 <= w, KnownNat w) => KnownRepr BaseTypeRepr (BaseBVType w :: BaseType) Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseBVType w) #
KnownRepr FloatPrecisionRepr fpp => KnownRepr BaseTypeRepr (BaseFloatType fpp :: BaseType) Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseFloatType fpp) #
KnownRepr StringInfoRepr si => KnownRepr BaseTypeRepr (BaseStringType si :: BaseType) Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseStringType si) #
KnownRepr (Assignment BaseTypeRepr) ctx => KnownRepr BaseTypeRepr (BaseStructType ctx :: BaseType) Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseStructType ctx) #
(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 #
Eq (BaseTypeRepr bt) Source #
Instance details Defined in What4.BaseTypes Methods (==) :: BaseTypeRepr bt -> BaseTypeRepr bt -> Bool # (/=) :: BaseTypeRepr bt -> BaseTypeRepr bt -> Bool #
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) #
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 #
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 #
(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 #
Eq (FloatPrecisionRepr fpp) Source #
Instance details Defined in What4.BaseTypes Methods (==) :: FloatPrecisionRepr fpp -> FloatPrecisionRepr fpp -> Bool # (/=) :: FloatPrecisionRepr fpp -> FloatPrecisionRepr fpp -> Bool #
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) #
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 #
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 #
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 StringInfoRepr Unicode Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: StringInfoRepr Unicode #
Show (StringInfoRepr si) Source #
Instance details Defined in What4.BaseTypes Methods showsPrec :: Int -> StringInfoRepr si -> ShowS # show :: StringInfoRepr si -> String # showList :: [StringInfoRepr si] -> ShowS #
Eq (StringInfoRepr si) Source #
Instance details Defined in What4.BaseTypes Methods (==) :: StringInfoRepr si -> StringInfoRepr si -> Bool # (/=) :: StringInfoRepr si -> StringInfoRepr si -> Bool #
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 BaseBoolType Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseBoolType #
KnownRepr BaseTypeRepr BaseComplexType Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseComplexType #
KnownRepr BaseTypeRepr BaseIntegerType Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseIntegerType #
KnownRepr BaseTypeRepr BaseRealType Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr BaseRealType #
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 StringInfoRepr Unicode Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: StringInfoRepr Unicode #
KnownRepr FloatModeRepr FloatIEEE Source #
Instance details Defined in What4.FloatMode Methods knownRepr :: FloatModeRepr FloatIEEE #
KnownRepr FloatModeRepr FloatReal Source #
Instance details Defined in What4.FloatMode Methods knownRepr :: FloatModeRepr FloatReal #
KnownRepr FloatModeRepr FloatUninterpreted Source #
Instance details Defined in What4.FloatMode Methods knownRepr :: FloatModeRepr FloatUninterpreted #
KnownRepr FloatInfoRepr DoubleDoubleFloat Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr DoubleDoubleFloat #
KnownRepr FloatInfoRepr DoubleFloat Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr DoubleFloat #
KnownRepr FloatInfoRepr HalfFloat Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr HalfFloat #
KnownRepr FloatInfoRepr QuadFloat Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr QuadFloat #
KnownRepr FloatInfoRepr SingleFloat Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr SingleFloat #
KnownRepr FloatInfoRepr X86_80Float Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr X86_80Float #
(1 <= w, KnownNat w) => KnownRepr BaseTypeRepr (BaseBVType w :: BaseType) Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseBVType w) #
KnownRepr FloatPrecisionRepr fpp => KnownRepr BaseTypeRepr (BaseFloatType fpp :: BaseType) Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseFloatType fpp) #
KnownRepr StringInfoRepr si => KnownRepr BaseTypeRepr (BaseStringType si :: BaseType) Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseStringType si) #
KnownRepr (Assignment BaseTypeRepr) ctx => KnownRepr BaseTypeRepr (BaseStructType ctx :: BaseType) Source #
Instance details Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseStructType ctx) #
(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) #
(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 (Proxy :: k -> Type) (ctx :: k)
Instance details Defined in Data.Parameterized.Classes Methods knownRepr :: Proxy ctx #
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