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

Copyright(c) Galois Inc 2014-2020
LicenseBSD3
MaintainerJoe Hendrix <jhendrix@galois.com>
Stabilityprovisional
Safe HaskellNone
LanguageHaskell2010

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

BaseType data kind

data BaseType Source #

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

Instances
TestEquality BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

testEquality :: BaseTypeRepr a -> BaseTypeRepr b -> Maybe (a :~: b) #

TestEquality IndexLit Source # 
Instance details

Defined in What4.IndexLit

Methods

testEquality :: IndexLit a -> IndexLit b -> Maybe (a :~: b) #

TestEquality OnlyNatRepr Source # 
Instance details

Defined in What4.Utils.OnlyNatRepr

Methods

testEquality :: OnlyNatRepr a -> OnlyNatRepr b -> Maybe (a :~: b) #

TestEquality ConcreteVal Source # 
Instance details

Defined in What4.Concrete

Methods

testEquality :: ConcreteVal a -> ConcreteVal b -> Maybe (a :~: b) #

TestEquality TypeMap Source # 
Instance details

Defined in What4.Protocol.SMTWriter

Methods

testEquality :: TypeMap a -> TypeMap b -> Maybe (a :~: b) #

OrdF BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

compareF :: BaseTypeRepr x -> BaseTypeRepr y -> OrderingF x y #

leqF :: BaseTypeRepr x -> BaseTypeRepr y -> Bool #

ltF :: BaseTypeRepr x -> BaseTypeRepr y -> Bool #

geqF :: BaseTypeRepr x -> BaseTypeRepr y -> Bool #

gtF :: BaseTypeRepr x -> BaseTypeRepr y -> Bool #

OrdF IndexLit Source # 
Instance details

Defined in What4.IndexLit

Methods

compareF :: IndexLit x -> IndexLit y -> OrderingF x y #

leqF :: IndexLit x -> IndexLit y -> Bool #

ltF :: IndexLit x -> IndexLit y -> Bool #

geqF :: IndexLit x -> IndexLit y -> Bool #

gtF :: IndexLit x -> IndexLit y -> Bool #

OrdF ConcreteVal Source # 
Instance details

Defined in What4.Concrete

Methods

compareF :: ConcreteVal x -> ConcreteVal y -> OrderingF x y #

leqF :: ConcreteVal x -> ConcreteVal y -> Bool #

ltF :: ConcreteVal x -> ConcreteVal y -> Bool #

geqF :: ConcreteVal x -> ConcreteVal y -> Bool #

gtF :: ConcreteVal x -> ConcreteVal y -> Bool #

ShowF BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

withShow :: p BaseTypeRepr -> q tp -> (Show (BaseTypeRepr tp) -> a) -> a #

showF :: BaseTypeRepr tp -> String #

showsPrecF :: Int -> BaseTypeRepr tp -> String -> String #

ShowF IndexLit Source # 
Instance details

Defined in What4.IndexLit

Methods

withShow :: p IndexLit -> q tp -> (Show (IndexLit tp) -> a) -> a #

showF :: IndexLit tp -> String #

showsPrecF :: Int -> IndexLit tp -> String -> String #

ShowF ConcreteVal Source # 
Instance details

Defined in What4.Concrete

Methods

withShow :: p ConcreteVal -> q tp -> (Show (ConcreteVal tp) -> a) -> a #

showF :: ConcreteVal tp -> String #

showsPrecF :: Int -> ConcreteVal tp -> String -> String #

ShowF TypeMap Source # 
Instance details

Defined in What4.Protocol.SMTWriter

Methods

withShow :: p TypeMap -> q tp -> (Show (TypeMap tp) -> a) -> a #

showF :: TypeMap tp -> String #

showsPrecF :: Int -> TypeMap tp -> String -> String #

HashableF BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

hashWithSaltF :: Int -> BaseTypeRepr tp -> Int #

hashF :: BaseTypeRepr tp -> Int #

HashableF IndexLit Source # 
Instance details

Defined in What4.IndexLit

Methods

hashWithSaltF :: Int -> IndexLit tp -> Int #

hashF :: IndexLit tp -> Int #

HashableF OnlyNatRepr Source # 
Instance details

Defined in What4.Utils.OnlyNatRepr

Methods

hashWithSaltF :: Int -> OnlyNatRepr tp -> Int #

hashF :: OnlyNatRepr tp -> Int #

FoldableFC App Source # 
Instance details

Defined in What4.Expr.App

Methods

foldMapFC :: 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 (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 (x :: k). b -> f x -> b) -> forall (x :: l). b -> App f x -> b #

toListFC :: (forall (x :: k). f x -> a) -> forall (x :: l). App f x -> [a] #

KnownRepr BaseTypeRepr BaseComplexType Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseComplexType #

KnownRepr BaseTypeRepr BaseRealType Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseRealType #

KnownRepr BaseTypeRepr BaseNatType Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseNatType #

KnownRepr BaseTypeRepr BaseIntegerType Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseIntegerType #

KnownRepr BaseTypeRepr BaseBoolType Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseBoolType #

FunctorFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

fmapFC :: (forall (x :: k). f x -> g x) -> forall (x :: l). NonceApp t f x -> NonceApp t g x #

FoldableFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

foldMapFC :: 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 (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 (x :: k). b -> f x -> b) -> forall (x :: l). b -> NonceApp t f x -> b #

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

TraversableFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

traverseFC :: Applicative m => (forall (x :: k). f x -> m (g x)) -> forall (x :: l). NonceApp t f x -> m (NonceApp t g x) #

KnownRepr (Assignment BaseTypeRepr) ctx => KnownRepr BaseTypeRepr (BaseStructType ctx :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseStructType ctx) #

KnownRepr StringInfoRepr si => KnownRepr BaseTypeRepr (BaseStringType si :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseStringType si) #

KnownRepr FloatPrecisionRepr fpp => KnownRepr BaseTypeRepr (BaseFloatType fpp :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseFloatType fpp) #

(1 <= w, KnownNat w) => KnownRepr BaseTypeRepr (BaseBVType w :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseBVType w) #

(KnownRepr (Assignment BaseTypeRepr) idx, KnownRepr BaseTypeRepr tp, KnownRepr BaseTypeRepr t) => KnownRepr BaseTypeRepr (BaseArrayType (idx ::> tp) t :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

Methods

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

(Eq (e BaseBoolType), Eq (e BaseRealType), HashableF e, HasAbsValue e, OrdF e) => TestEquality (App e :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

testEquality :: App e a -> App e b -> Maybe (a :~: b) #

TestEquality (ExprBoundVar t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

testEquality :: ExprBoundVar t a -> ExprBoundVar t b -> Maybe (a :~: b) #

TestEquality (Expr t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.Builder

Methods

testEquality :: Expr t a -> Expr t b -> Maybe (a :~: b) #

TestEquality (NonceAppExpr t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.Builder

Methods

testEquality :: NonceAppExpr t a -> NonceAppExpr t b -> Maybe (a :~: b) #

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

Defined in What4.Expr.App

Methods

compareF :: ExprBoundVar t x -> ExprBoundVar t y -> OrderingF x y #

leqF :: ExprBoundVar t x -> ExprBoundVar t y -> Bool #

ltF :: ExprBoundVar t x -> ExprBoundVar t y -> Bool #

geqF :: ExprBoundVar t x -> ExprBoundVar t y -> Bool #

gtF :: ExprBoundVar t x -> ExprBoundVar t y -> Bool #

OrdF (Expr t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.Builder

Methods

compareF :: Expr t x -> Expr t y -> OrderingF x y #

leqF :: Expr t x -> Expr t y -> Bool #

ltF :: Expr t x -> Expr t y -> Bool #

geqF :: Expr t x -> Expr t y -> Bool #

gtF :: Expr t x -> Expr t y -> Bool #

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

Defined in What4.Expr.Builder

Methods

compareF :: NonceAppExpr t x -> NonceAppExpr t y -> OrderingF x y #

leqF :: NonceAppExpr t x -> NonceAppExpr t y -> Bool #

ltF :: NonceAppExpr t x -> NonceAppExpr t y -> Bool #

geqF :: NonceAppExpr t x -> NonceAppExpr t y -> Bool #

gtF :: NonceAppExpr t x -> NonceAppExpr t y -> Bool #

ShowF (ExprBoundVar t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

withShow :: p (ExprBoundVar t) -> q tp -> (Show (ExprBoundVar t tp) -> a) -> a #

showF :: ExprBoundVar t tp -> String #

showsPrecF :: Int -> ExprBoundVar t tp -> String -> String #

ShowF (Expr t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.Builder

Methods

withShow :: p (Expr t) -> q tp -> (Show (Expr t tp) -> a) -> a #

showF :: Expr t tp -> String #

showsPrecF :: Int -> Expr t tp -> String -> String #

(OrdF e, HashableF e, HasAbsValue e, Hashable (e BaseBoolType), Hashable (e BaseRealType)) => HashableF (App e :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

hashWithSaltF :: Int -> App e tp -> Int #

hashF :: App e tp -> Int #

HashableF (ExprBoundVar t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

hashWithSaltF :: Int -> ExprBoundVar t tp -> Int #

hashF :: ExprBoundVar t tp -> Int #

HashableF (Expr t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.Builder

Methods

hashWithSaltF :: Int -> Expr t tp -> Int #

hashF :: Expr t tp -> Int #

TestEquality f => TestEquality (ArrayResultWrapper f idx :: BaseType -> Type) Source # 
Instance details

Defined in What4.Interface

Methods

testEquality :: ArrayResultWrapper f idx a -> ArrayResultWrapper f idx b -> Maybe (a :~: b) #

TestEquality e => TestEquality (NonceApp t e :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

testEquality :: NonceApp t e a -> NonceApp t e b -> Maybe (a :~: b) #

HashableF e => HashableF (ArrayResultWrapper e idx :: BaseType -> Type) Source # 
Instance details

Defined in What4.Interface

Methods

hashWithSaltF :: Int -> ArrayResultWrapper e idx tp -> Int #

hashF :: ArrayResultWrapper e idx tp -> Int #

HashableF e => HashableF (NonceApp t e :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

hashWithSaltF :: Int -> NonceApp t e tp -> Int #

hashF :: NonceApp t e tp -> Int #

Constructors for kind BaseType

type BaseBoolType Source #

Arguments

 = BaseBoolType

:: BaseType.

type BaseIntegerType Source #

Arguments

 = BaseIntegerType

:: BaseType.

type BaseNatType Source #

Arguments

 = BaseNatType

:: 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
TestEquality StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

testEquality :: StringInfoRepr a -> StringInfoRepr b -> Maybe (a :~: b) #

TestEquality StringLiteral Source # 
Instance details

Defined in What4.Utils.StringLiteral

Methods

testEquality :: StringLiteral a -> StringLiteral b -> Maybe (a :~: b) #

OrdF StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

compareF :: StringInfoRepr x -> StringInfoRepr y -> OrderingF x y #

leqF :: StringInfoRepr x -> StringInfoRepr y -> Bool #

ltF :: StringInfoRepr x -> StringInfoRepr y -> Bool #

geqF :: StringInfoRepr x -> StringInfoRepr y -> Bool #

gtF :: StringInfoRepr x -> StringInfoRepr y -> Bool #

OrdF StringLiteral Source # 
Instance details

Defined in What4.Utils.StringLiteral

Methods

compareF :: StringLiteral x -> StringLiteral y -> OrderingF x y #

leqF :: StringLiteral x -> StringLiteral y -> Bool #

ltF :: StringLiteral x -> StringLiteral y -> Bool #

geqF :: StringLiteral x -> StringLiteral y -> Bool #

gtF :: StringLiteral x -> StringLiteral y -> Bool #

ShowF StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

withShow :: p StringInfoRepr -> q tp -> (Show (StringInfoRepr tp) -> a) -> a #

showF :: StringInfoRepr tp -> String #

showsPrecF :: Int -> StringInfoRepr tp -> String -> String #

ShowF StringLiteral Source # 
Instance details

Defined in What4.Utils.StringLiteral

Methods

withShow :: p StringLiteral -> q tp -> (Show (StringLiteral tp) -> a) -> a #

showF :: StringLiteral tp -> String #

showsPrecF :: Int -> StringLiteral tp -> String -> String #

HashableF StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

hashWithSaltF :: Int -> StringInfoRepr tp -> Int #

hashF :: StringInfoRepr tp -> Int #

HashableF StringLiteral Source # 
Instance details

Defined in What4.Utils.StringLiteral

Methods

hashWithSaltF :: Int -> StringLiteral tp -> Int #

hashF :: StringLiteral tp -> Int #

KnownRepr StringInfoRepr Unicode Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: StringInfoRepr Unicode #

KnownRepr StringInfoRepr Char16 Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: StringInfoRepr Char16 #

KnownRepr StringInfoRepr Char8 Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: StringInfoRepr Char8 #

(TestEquality e, HasAbsValue e, HashableF e) => TestEquality (StringSeq e :: StringInfo -> Type) Source # 
Instance details

Defined in What4.Expr.StringSeq

Methods

testEquality :: 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 :: Int -> StringSeq e tp -> Int #

hashF :: 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
TestEquality FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

testEquality :: FloatPrecisionRepr a -> FloatPrecisionRepr b -> Maybe (a :~: b) #

OrdF FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

compareF :: FloatPrecisionRepr x -> FloatPrecisionRepr y -> OrderingF x y #

leqF :: FloatPrecisionRepr x -> FloatPrecisionRepr y -> Bool #

ltF :: FloatPrecisionRepr x -> FloatPrecisionRepr y -> Bool #

geqF :: FloatPrecisionRepr x -> FloatPrecisionRepr y -> Bool #

gtF :: FloatPrecisionRepr x -> FloatPrecisionRepr y -> Bool #

ShowF FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

withShow :: p FloatPrecisionRepr -> q tp -> (Show (FloatPrecisionRepr tp) -> a) -> a #

showF :: FloatPrecisionRepr tp -> String #

showsPrecF :: Int -> FloatPrecisionRepr tp -> String -> String #

HashableF FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

hashWithSaltF :: Int -> FloatPrecisionRepr tp -> Int #

hashF :: FloatPrecisionRepr tp -> Int #

(2 <= eb, 2 <= es, KnownNat eb, KnownNat es) => KnownRepr FloatPrecisionRepr (FloatingPointPrecision eb es :: FloatPrecision) Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: FloatPrecisionRepr (FloatingPointPrecision eb es) #

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

This computes the number of bits occupied by a floating-point format.

Equations

FloatPrecisionBits (FloatingPointPrecision eb sb) = eb + sb 

Constructors for kind FloatPrecision

type FloatingPointPrecision Source #

Arguments

 = FloatingPointPrecision

:: Nat -> Nat -> FloatPrecision.

FloatingPointPrecision aliases

type Prec16 = FloatingPointPrecision 5 11 Source #

Floating-point precision aliases

type Prec32 = FloatingPointPrecision 8 24 Source #

type Prec64 = FloatingPointPrecision 11 53 Source #

type Prec80 = FloatingPointPrecision 15 65 Source #

type Prec128 = FloatingPointPrecision 15 113 Source #

Representations of base types

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

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

Constructors

BaseBoolRepr :: BaseTypeRepr BaseBoolType 
BaseBVRepr :: 1 <= w => !(NatRepr w) -> BaseTypeRepr (BaseBVType w) 
BaseNatRepr :: BaseTypeRepr BaseNatType 
BaseIntegerRepr :: BaseTypeRepr BaseIntegerType 
BaseRealRepr :: BaseTypeRepr BaseRealType 
BaseFloatRepr :: !(FloatPrecisionRepr fpp) -> BaseTypeRepr (BaseFloatType fpp) 
BaseStringRepr :: StringInfoRepr si -> BaseTypeRepr (BaseStringType si) 
BaseComplexRepr :: BaseTypeRepr BaseComplexType 
BaseStructRepr :: !(Assignment BaseTypeRepr ctx) -> BaseTypeRepr (BaseStructType ctx) 
BaseArrayRepr :: !(Assignment BaseTypeRepr (idx ::> tp)) -> !(BaseTypeRepr xs) -> BaseTypeRepr (BaseArrayType (idx ::> tp) xs) 
Instances
TestEquality BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

testEquality :: BaseTypeRepr a -> BaseTypeRepr b -> Maybe (a :~: b) #

OrdF BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

compareF :: BaseTypeRepr x -> BaseTypeRepr y -> OrderingF x y #

leqF :: BaseTypeRepr x -> BaseTypeRepr y -> Bool #

ltF :: BaseTypeRepr x -> BaseTypeRepr y -> Bool #

geqF :: BaseTypeRepr x -> BaseTypeRepr y -> Bool #

gtF :: BaseTypeRepr x -> BaseTypeRepr y -> Bool #

ShowF BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

withShow :: p BaseTypeRepr -> q tp -> (Show (BaseTypeRepr tp) -> a) -> a #

showF :: BaseTypeRepr tp -> String #

showsPrecF :: Int -> BaseTypeRepr tp -> String -> String #

HashableF BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

hashWithSaltF :: Int -> BaseTypeRepr tp -> Int #

hashF :: BaseTypeRepr tp -> Int #

KnownRepr BaseTypeRepr BaseComplexType Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseComplexType #

KnownRepr BaseTypeRepr BaseRealType Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseRealType #

KnownRepr BaseTypeRepr BaseNatType Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseNatType #

KnownRepr BaseTypeRepr BaseIntegerType Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseIntegerType #

KnownRepr BaseTypeRepr BaseBoolType Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseBoolType #

KnownRepr (Assignment BaseTypeRepr) ctx => KnownRepr BaseTypeRepr (BaseStructType ctx :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseStructType ctx) #

KnownRepr StringInfoRepr si => KnownRepr BaseTypeRepr (BaseStringType si :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseStringType si) #

KnownRepr FloatPrecisionRepr fpp => KnownRepr BaseTypeRepr (BaseFloatType fpp :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseFloatType fpp) #

(1 <= w, KnownNat w) => KnownRepr BaseTypeRepr (BaseBVType w :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseBVType w) #

(KnownRepr (Assignment BaseTypeRepr) idx, KnownRepr BaseTypeRepr tp, KnownRepr BaseTypeRepr t) => KnownRepr BaseTypeRepr (BaseArrayType (idx ::> tp) t :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

Methods

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

Show (BaseTypeRepr bt) Source # 
Instance details

Defined in What4.BaseTypes

Methods

showsPrec :: Int -> BaseTypeRepr bt -> ShowS #

show :: BaseTypeRepr bt -> String #

showList :: [BaseTypeRepr bt] -> ShowS #

Pretty (BaseTypeRepr bt) Source # 
Instance details

Defined in What4.BaseTypes

Methods

pretty :: BaseTypeRepr bt -> Doc #

prettyList :: [BaseTypeRepr bt] -> Doc #

Hashable (BaseTypeRepr bt) Source # 
Instance details

Defined in What4.BaseTypes

Methods

hashWithSalt :: Int -> BaseTypeRepr bt -> Int #

hash :: BaseTypeRepr bt -> Int #

data FloatPrecisionRepr (fpp :: FloatPrecision) where Source #

Constructors

FloatingPointPrecisionRepr :: (2 <= eb, 2 <= sb) => !(NatRepr eb) -> !(NatRepr sb) -> FloatPrecisionRepr (FloatingPointPrecision eb sb) 
Instances
TestEquality FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

testEquality :: FloatPrecisionRepr a -> FloatPrecisionRepr b -> Maybe (a :~: b) #

OrdF FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

compareF :: FloatPrecisionRepr x -> FloatPrecisionRepr y -> OrderingF x y #

leqF :: FloatPrecisionRepr x -> FloatPrecisionRepr y -> Bool #

ltF :: FloatPrecisionRepr x -> FloatPrecisionRepr y -> Bool #

geqF :: FloatPrecisionRepr x -> FloatPrecisionRepr y -> Bool #

gtF :: FloatPrecisionRepr x -> FloatPrecisionRepr y -> Bool #

ShowF FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

withShow :: p FloatPrecisionRepr -> q tp -> (Show (FloatPrecisionRepr tp) -> a) -> a #

showF :: FloatPrecisionRepr tp -> String #

showsPrecF :: Int -> FloatPrecisionRepr tp -> String -> String #

HashableF FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

hashWithSaltF :: Int -> FloatPrecisionRepr tp -> Int #

hashF :: FloatPrecisionRepr tp -> Int #

(2 <= eb, 2 <= es, KnownNat eb, KnownNat es) => KnownRepr FloatPrecisionRepr (FloatingPointPrecision eb es :: FloatPrecision) Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: FloatPrecisionRepr (FloatingPointPrecision eb es) #

Show (FloatPrecisionRepr fpp) Source # 
Instance details

Defined in What4.BaseTypes

Methods

showsPrec :: Int -> FloatPrecisionRepr fpp -> ShowS #

show :: FloatPrecisionRepr fpp -> String #

showList :: [FloatPrecisionRepr fpp] -> ShowS #

Pretty (FloatPrecisionRepr fpp) Source # 
Instance details

Defined in What4.BaseTypes

Methods

pretty :: FloatPrecisionRepr fpp -> Doc #

prettyList :: [FloatPrecisionRepr fpp] -> Doc #

Hashable (FloatPrecisionRepr fpp) Source # 
Instance details

Defined in What4.BaseTypes

Methods

hashWithSalt :: Int -> FloatPrecisionRepr fpp -> Int #

hash :: FloatPrecisionRepr fpp -> Int #

data StringInfoRepr (si :: StringInfo) where Source #

Constructors

Char8Repr :: StringInfoRepr Char8 
Char16Repr :: StringInfoRepr Char16 
UnicodeRepr :: StringInfoRepr Unicode 
Instances
TestEquality StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

testEquality :: StringInfoRepr a -> StringInfoRepr b -> Maybe (a :~: b) #

OrdF StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

compareF :: StringInfoRepr x -> StringInfoRepr y -> OrderingF x y #

leqF :: StringInfoRepr x -> StringInfoRepr y -> Bool #

ltF :: StringInfoRepr x -> StringInfoRepr y -> Bool #

geqF :: StringInfoRepr x -> StringInfoRepr y -> Bool #

gtF :: StringInfoRepr x -> StringInfoRepr y -> Bool #

ShowF StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

withShow :: p StringInfoRepr -> q tp -> (Show (StringInfoRepr tp) -> a) -> a #

showF :: StringInfoRepr tp -> String #

showsPrecF :: Int -> StringInfoRepr tp -> String -> String #

HashableF StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

hashWithSaltF :: Int -> StringInfoRepr tp -> Int #

hashF :: StringInfoRepr tp -> Int #

KnownRepr StringInfoRepr Unicode Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: StringInfoRepr Unicode #

KnownRepr StringInfoRepr Char16 Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: StringInfoRepr Char16 #

KnownRepr StringInfoRepr Char8 Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: StringInfoRepr Char8 #

Show (StringInfoRepr si) Source # 
Instance details

Defined in What4.BaseTypes

Methods

showsPrec :: Int -> StringInfoRepr si -> ShowS #

show :: StringInfoRepr si -> String #

showList :: [StringInfoRepr si] -> ShowS #

Pretty (StringInfoRepr si) Source # 
Instance details

Defined in What4.BaseTypes

Methods

pretty :: StringInfoRepr si -> Doc #

prettyList :: [StringInfoRepr si] -> Doc #

Hashable (StringInfoRepr si) Source # 
Instance details

Defined in What4.BaseTypes

Methods

hashWithSalt :: Int -> StringInfoRepr si -> Int #

hash :: StringInfoRepr si -> Int #

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
KnownNat n => KnownRepr NatRepr (n :: Nat) 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

knownRepr :: NatRepr n #

KnownRepr BaseTypeRepr BaseComplexType Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseComplexType #

KnownRepr BaseTypeRepr BaseRealType Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseRealType #

KnownRepr BaseTypeRepr BaseNatType Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseNatType #

KnownRepr BaseTypeRepr BaseIntegerType Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseIntegerType #

KnownRepr BaseTypeRepr BaseBoolType Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr BaseBoolType #

KnownRepr StringInfoRepr Unicode Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: StringInfoRepr Unicode #

KnownRepr StringInfoRepr Char16 Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: StringInfoRepr Char16 #

KnownRepr StringInfoRepr Char8 Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: StringInfoRepr Char8 #

KnownRepr FloatInfoRepr DoubleDoubleFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr DoubleDoubleFloat #

KnownRepr FloatInfoRepr X86_80Float Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr X86_80Float #

KnownRepr FloatInfoRepr QuadFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr QuadFloat #

KnownRepr FloatInfoRepr DoubleFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr DoubleFloat #

KnownRepr FloatInfoRepr SingleFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr SingleFloat #

KnownRepr FloatInfoRepr HalfFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr HalfFloat #

KnownRepr FloatModeRepr FloatReal Source # 
Instance details

Defined in What4.Expr.Builder

Methods

knownRepr :: FloatModeRepr FloatReal #

KnownRepr FloatModeRepr FloatUninterpreted Source # 
Instance details

Defined in What4.Expr.Builder

Methods

knownRepr :: FloatModeRepr FloatUninterpreted #

KnownRepr FloatModeRepr FloatIEEE Source # 
Instance details

Defined in What4.Expr.Builder

Methods

knownRepr :: FloatModeRepr FloatIEEE #

KnownRepr (Assignment BaseTypeRepr) ctx => KnownRepr BaseTypeRepr (BaseStructType ctx :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseStructType ctx) #

KnownRepr StringInfoRepr si => KnownRepr BaseTypeRepr (BaseStringType si :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseStringType si) #

KnownRepr FloatPrecisionRepr fpp => KnownRepr BaseTypeRepr (BaseFloatType fpp :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseFloatType fpp) #

(1 <= w, KnownNat w) => KnownRepr BaseTypeRepr (BaseBVType w :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: BaseTypeRepr (BaseBVType w) #

(2 <= eb, 2 <= es, KnownNat eb, KnownNat es) => KnownRepr FloatPrecisionRepr (FloatingPointPrecision eb es :: FloatPrecision) Source # 
Instance details

Defined in What4.BaseTypes

Methods

knownRepr :: FloatPrecisionRepr (FloatingPointPrecision eb es) #

(KnownRepr (Assignment BaseTypeRepr) idx, KnownRepr BaseTypeRepr tp, KnownRepr BaseTypeRepr t) => KnownRepr BaseTypeRepr (BaseArrayType (idx ::> tp) t :: BaseType) Source # 
Instance details

Defined in What4.BaseTypes

Methods

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

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

Defined in Data.Parameterized.Context.Unsafe

Methods

knownRepr :: Assignment f EmptyCtx #

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

Defined in Data.Parameterized.Context.Unsafe

Methods

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

type KnownCtx f = KnownRepr (Assignment f) Source #

A Context where all the argument types are KnownRepr instances