what4-1.6.3: 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

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

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

TestEquality ConcreteVal Source # 
Instance details

Defined in What4.Concrete

Methods

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

TestEquality IndexLit Source # 
Instance details

Defined in What4.IndexLit

Methods

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

TestEquality TypeMap Source # 
Instance details

Defined in What4.Protocol.SMTWriter

Methods

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

TestEquality OnlyIntRepr Source # 
Instance details

Defined in What4.Utils.OnlyIntRepr

Methods

testEquality :: forall (a :: BaseType) (b :: BaseType). OnlyIntRepr a -> OnlyIntRepr b -> Maybe (a :~: b) #

HashableF BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

hashWithSaltF :: forall (tp :: BaseType). Int -> BaseTypeRepr tp -> Int

hashF :: forall (tp :: BaseType). BaseTypeRepr tp -> Int

HashableF IndexLit 
Instance details

Defined in What4.IndexLit

Methods

hashWithSaltF :: forall (tp :: BaseType). Int -> IndexLit tp -> Int

hashF :: forall (tp :: BaseType). IndexLit tp -> Int

HashableF OnlyIntRepr 
Instance details

Defined in What4.Utils.OnlyIntRepr

Methods

hashWithSaltF :: forall (tp :: BaseType). Int -> OnlyIntRepr tp -> Int

hashF :: forall (tp :: BaseType). OnlyIntRepr tp -> Int

OrdF BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

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

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

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

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

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

OrdF ConcreteVal 
Instance details

Defined in What4.Concrete

Methods

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

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

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

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

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

OrdF IndexLit 
Instance details

Defined in What4.IndexLit

Methods

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

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

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

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

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

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

showF :: forall (tp :: BaseType). BaseTypeRepr tp -> String

showsPrecF :: forall (tp :: BaseType). Int -> BaseTypeRepr tp -> String -> String

ShowF ConcreteVal 
Instance details

Defined in What4.Concrete

Methods

withShow :: forall p q (tp :: BaseType) a. p ConcreteVal -> q tp -> (Show (ConcreteVal tp) => a) -> a

showF :: forall (tp :: BaseType). ConcreteVal tp -> String

showsPrecF :: forall (tp :: BaseType). Int -> ConcreteVal tp -> String -> String

ShowF OptionSetting 
Instance details

Defined in What4.Config

Methods

withShow :: forall p q (tp :: BaseType) a. p OptionSetting -> q tp -> (Show (OptionSetting tp) => a) -> a

showF :: forall (tp :: BaseType). OptionSetting tp -> String

showsPrecF :: forall (tp :: BaseType). Int -> OptionSetting tp -> String -> String

ShowF IndexLit 
Instance details

Defined in What4.IndexLit

Methods

withShow :: forall p q (tp :: BaseType) a. p IndexLit -> q tp -> (Show (IndexLit tp) => a) -> a

showF :: forall (tp :: BaseType). IndexLit tp -> String

showsPrecF :: forall (tp :: BaseType). Int -> IndexLit tp -> String -> String

ShowF TypeMap 
Instance details

Defined in What4.Protocol.SMTWriter

Methods

withShow :: forall p q (tp :: BaseType) a. p TypeMap -> q tp -> (Show (TypeMap tp) => a) -> a

showF :: forall (tp :: BaseType). TypeMap tp -> String

showsPrecF :: forall (tp :: BaseType). Int -> TypeMap tp -> String -> String

KnownRepr BaseTypeRepr BaseBoolType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseComplexType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseIntegerType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseRealType Source # 
Instance details

Defined in What4.BaseTypes

FoldableFC App 
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

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

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

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

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

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

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

Defined in What4.BaseTypes

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

Defined in What4.BaseTypes

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

Defined in What4.BaseTypes

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

Defined in What4.BaseTypes

FoldableFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) 
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

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

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

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

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

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

FunctorFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) 
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

TraversableFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) 
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)

(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 :: BaseType) (b :: BaseType). 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 :: BaseType) (b :: BaseType). 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 :: BaseType) (b :: BaseType). 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 :: BaseType) (b :: BaseType). 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) 
Instance details

Defined in What4.Expr.App

Methods

hashWithSaltF :: forall (tp :: BaseType). Int -> App e tp -> Int

hashF :: forall (tp :: BaseType). App e tp -> Int

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

Defined in What4.Expr.App

Methods

hashWithSaltF :: forall (tp :: BaseType). Int -> Expr t tp -> Int

hashF :: forall (tp :: BaseType). Expr t tp -> Int

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

Defined in What4.Expr.App

Methods

hashWithSaltF :: forall (tp :: BaseType). Int -> ExprBoundVar t tp -> Int

hashF :: forall (tp :: BaseType). ExprBoundVar t tp -> Int

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

Defined in What4.Expr.App

Methods

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

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

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

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

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

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

Defined in What4.Expr.App

Methods

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

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

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

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

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

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

Defined in What4.Expr.App

Methods

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

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

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

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

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

ShowF (Expr t :: BaseType -> Type) 
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

showF :: forall (tp :: BaseType). Expr t tp -> String

showsPrecF :: forall (tp :: BaseType). Int -> Expr t tp -> String -> String

ShowF (ExprBoundVar t :: BaseType -> Type) 
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

showF :: forall (tp :: BaseType). ExprBoundVar t tp -> String

showsPrecF :: forall (tp :: BaseType). 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 :: BaseType) (b :: BaseType). 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 :: BaseType) (b :: BaseType). ArrayResultWrapper f idx a -> ArrayResultWrapper f idx b -> Maybe (a :~: b) #

(HashableF e, TestEquality e) => HashableF (NonceApp t e :: BaseType -> Type) 
Instance details

Defined in What4.Expr.App

Methods

hashWithSaltF :: forall (tp :: BaseType). Int -> NonceApp t e tp -> Int

hashF :: forall (tp :: BaseType). NonceApp t e tp -> Int

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

Defined in What4.Interface

Methods

hashWithSaltF :: forall (tp :: BaseType). Int -> ArrayResultWrapper e idx tp -> Int

hashF :: forall (tp :: BaseType). 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 :: Ctx BaseType) (b :: Ctx BaseType). SymFnWrapper sym a -> SymFnWrapper sym b -> Maybe (a :~: b) #

IsSymFn (SymFn sym) => OrdF (SymFnWrapper sym :: Ctx BaseType -> Type) 
Instance details

Defined in What4.Interface

Methods

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

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

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

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

gtF :: forall (x :: Ctx BaseType) (y :: Ctx BaseType). 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 :: StringInfo) (b :: StringInfo). StringInfoRepr a -> StringInfoRepr b -> Maybe (a :~: b) #

TestEquality StringLiteral Source # 
Instance details

Defined in What4.Utils.StringLiteral

Methods

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

HashableF StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

hashWithSaltF :: forall (tp :: StringInfo). Int -> StringInfoRepr tp -> Int

hashF :: forall (tp :: StringInfo). StringInfoRepr tp -> Int

HashableF StringLiteral 
Instance details

Defined in What4.Utils.StringLiteral

Methods

hashWithSaltF :: forall (tp :: StringInfo). Int -> StringLiteral tp -> Int

hashF :: forall (tp :: StringInfo). StringLiteral tp -> Int

OrdF StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

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

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

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

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

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

OrdF StringLiteral 
Instance details

Defined in What4.Utils.StringLiteral

Methods

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

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

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

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

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

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

showF :: forall (tp :: StringInfo). StringInfoRepr tp -> String

showsPrecF :: forall (tp :: StringInfo). Int -> StringInfoRepr tp -> String -> String

ShowF StringLiteral 
Instance details

Defined in What4.Utils.StringLiteral

Methods

withShow :: forall p q (tp :: StringInfo) a. p StringLiteral -> q tp -> (Show (StringLiteral tp) => a) -> a

showF :: forall (tp :: StringInfo). StringLiteral tp -> String

showsPrecF :: forall (tp :: StringInfo). Int -> StringLiteral tp -> String -> String

KnownRepr StringInfoRepr Char16 Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr StringInfoRepr Char8 Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr StringInfoRepr Unicode Source # 
Instance details

Defined in What4.BaseTypes

(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) #

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

Defined in What4.Expr.StringSeq

Methods

hashWithSaltF :: forall (tp :: StringInfo). Int -> StringSeq e tp -> Int

hashF :: forall (tp :: StringInfo). 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 :: FloatPrecision) (b :: FloatPrecision). FloatPrecisionRepr a -> FloatPrecisionRepr b -> Maybe (a :~: b) #

HashableF FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

hashWithSaltF :: forall (tp :: FloatPrecision). Int -> FloatPrecisionRepr tp -> Int

hashF :: forall (tp :: FloatPrecision). FloatPrecisionRepr tp -> Int

OrdF FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

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

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

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

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

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

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

showF :: forall (tp :: FloatPrecision). FloatPrecisionRepr tp -> String

showsPrecF :: forall (tp :: FloatPrecision). 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

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

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

HashableF BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

hashWithSaltF :: forall (tp :: BaseType). Int -> BaseTypeRepr tp -> Int

hashF :: forall (tp :: BaseType). BaseTypeRepr tp -> Int

OrdF BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

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

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

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

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

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

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

showF :: forall (tp :: BaseType). BaseTypeRepr tp -> String

showsPrecF :: forall (tp :: BaseType). Int -> BaseTypeRepr tp -> String -> String

KnownRepr BaseTypeRepr BaseBoolType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseComplexType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseIntegerType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseRealType Source # 
Instance details

Defined in What4.BaseTypes

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

Defined in What4.BaseTypes

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

Defined in What4.BaseTypes

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

Defined in What4.BaseTypes

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

Defined in What4.BaseTypes

(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 :: 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) #

HashableF FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

hashWithSaltF :: forall (tp :: FloatPrecision). Int -> FloatPrecisionRepr tp -> Int

hashF :: forall (tp :: FloatPrecision). FloatPrecisionRepr tp -> Int

OrdF FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

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

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

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

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

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

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

showF :: forall (tp :: FloatPrecision). FloatPrecisionRepr tp -> String

showsPrecF :: forall (tp :: FloatPrecision). 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

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 :: StringInfo) (b :: StringInfo). StringInfoRepr a -> StringInfoRepr b -> Maybe (a :~: b) #

HashableF StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

hashWithSaltF :: forall (tp :: StringInfo). Int -> StringInfoRepr tp -> Int

hashF :: forall (tp :: StringInfo). StringInfoRepr tp -> Int

OrdF StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

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

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

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

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

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

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

showF :: forall (tp :: StringInfo). StringInfoRepr tp -> String

showsPrecF :: forall (tp :: StringInfo). Int -> StringInfoRepr tp -> String -> String

KnownRepr StringInfoRepr Char16 Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr StringInfoRepr Char8 Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr StringInfoRepr Unicode Source # 
Instance details

Defined in What4.BaseTypes

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

type family (a :: Natural) - (b :: Natural) :: Natural where ... #

type family (a :: Natural) * (b :: Natural) :: Natural where ... #

data NatRepr (n :: Nat) #

Instances

Instances details
TestEquality NatRepr 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

testEquality :: forall (a :: Nat) (b :: Nat). NatRepr a -> NatRepr b -> Maybe (a :~: b) #

EqF NatRepr 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

eqF :: forall (a :: Nat). NatRepr a -> NatRepr a -> Bool

HashableF NatRepr 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

hashWithSaltF :: forall (tp :: Nat). Int -> NatRepr tp -> Int

hashF :: forall (tp :: Nat). NatRepr tp -> Int

OrdF NatRepr 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

compareF :: forall (x :: Nat) (y :: Nat). NatRepr x -> NatRepr y -> OrderingF x y

leqF :: forall (x :: Nat) (y :: Nat). NatRepr x -> NatRepr y -> Bool

ltF :: forall (x :: Nat) (y :: Nat). NatRepr x -> NatRepr y -> Bool

geqF :: forall (x :: Nat) (y :: Nat). NatRepr x -> NatRepr y -> Bool

gtF :: forall (x :: Nat) (y :: Nat). NatRepr x -> NatRepr y -> Bool

ShowF NatRepr 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

withShow :: forall p q (tp :: Nat) a. p NatRepr -> q tp -> (Show (NatRepr tp) => a) -> a

showF :: forall (tp :: Nat). NatRepr tp -> String

showsPrecF :: forall (tp :: Nat). Int -> NatRepr tp -> String -> String

DecidableEq NatRepr 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

decEq :: forall (a :: Nat) (b :: Nat). NatRepr a -> NatRepr b -> Either (a :~: b) ((a :~: b) -> Void)

IsRepr NatRepr 
Instance details

Defined in Data.Parameterized.WithRepr

Methods

withRepr :: forall (a :: Nat) r. NatRepr a -> (KnownRepr NatRepr a => r) -> r

KnownNat n => KnownRepr NatRepr (n :: Nat) 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

knownRepr :: NatRepr n #

KnownNat n => Data (NatRepr n) 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NatRepr n -> c (NatRepr n)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (NatRepr n)

toConstr :: NatRepr n -> Constr

dataTypeOf :: NatRepr n -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (NatRepr n))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (NatRepr n))

gmapT :: (forall b. Data b => b -> b) -> NatRepr n -> NatRepr n

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NatRepr n -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NatRepr n -> r

gmapQ :: (forall d. Data d => d -> u) -> NatRepr n -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> NatRepr n -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n)

Show (NatRepr n) 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

showsPrec :: Int -> NatRepr n -> ShowS

show :: NatRepr n -> String

showList :: [NatRepr n] -> ShowS

Eq (NatRepr m) 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

(==) :: NatRepr m -> NatRepr m -> Bool

(/=) :: NatRepr m -> NatRepr m -> Bool

Hashable (NatRepr n) 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

hashWithSalt :: Int -> NatRepr n -> Int

hash :: NatRepr n -> Int

PolyEq (NatRepr m) (NatRepr n) 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

polyEqF :: NatRepr m -> NatRepr n -> Maybe (NatRepr m :~: NatRepr n)

polyEq :: NatRepr m -> NatRepr n -> Bool

data Some (f :: k -> Type) #

Instances

Instances details
OrdC (Some :: (k -> Type) -> Type) 
Instance details

Defined in Data.Parameterized.ClassesC

Methods

compareC :: (forall (x :: k) (y :: k). f x -> g y -> OrderingF x y) -> Some f -> Some g -> Ordering

TestEqualityC (Some :: (k -> Type) -> Type) 
Instance details

Defined in Data.Parameterized.ClassesC

Methods

testEqualityC :: (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> Some f -> Some f -> Bool

FoldableF (Some :: (k -> Type) -> Type) 
Instance details

Defined in Data.Parameterized.Some

Methods

foldMapF :: Monoid m => (forall (s :: k). e s -> m) -> Some e -> m

foldrF :: (forall (s :: k). e s -> b -> b) -> b -> Some e -> b

foldlF :: (forall (s :: k). b -> e s -> b) -> b -> Some e -> b

foldrF' :: (forall (s :: k). e s -> b -> b) -> b -> Some e -> b

foldlF' :: (forall (s :: k). b -> e s -> b) -> b -> Some e -> b

toListF :: (forall (tp :: k). f tp -> a) -> Some f -> [a]

FunctorF (Some :: (k -> Type) -> Type) 
Instance details

Defined in Data.Parameterized.Some

Methods

fmapF :: (forall (x :: k). f x -> g x) -> Some f -> Some g

TraversableF (Some :: (k -> Type) -> Type) 
Instance details

Defined in Data.Parameterized.Some

Methods

traverseF :: Applicative m => (forall (s :: k). e s -> m (f s)) -> Some e -> m (Some f)

ShowF f => Show (Some f) 
Instance details

Defined in Data.Parameterized.Some

Methods

showsPrec :: Int -> Some f -> ShowS

show :: Some f -> String

showList :: [Some f] -> ShowS

TestEquality f => Eq (Some f) 
Instance details

Defined in Data.Parameterized.Some

Methods

(==) :: Some f -> Some f -> Bool

(/=) :: Some f -> Some f -> Bool

OrdF f => Ord (Some f) 
Instance details

Defined in Data.Parameterized.Some

Methods

compare :: Some f -> Some f -> Ordering

(<) :: Some f -> Some f -> Bool

(<=) :: Some f -> Some f -> Bool

(>) :: Some f -> Some f -> Bool

(>=) :: Some f -> Some f -> Bool

max :: Some f -> Some f -> Some f

min :: Some f -> Some f -> Some f

(HashableF f, TestEquality f) => Hashable (Some f) 
Instance details

Defined in Data.Parameterized.Some

Methods

hashWithSalt :: Int -> Some f -> Int

hash :: Some f -> Int

type (<=) (x :: t) (y :: t) = Assert (x <=? y) (LeErrMsg x y :: Constraint) #

type family (a :: Natural) + (b :: Natural) :: Natural where ... #

data LeqProof (m :: Nat) (n :: Nat) where #

Constructors

LeqProof :: forall (m :: Nat) (n :: Nat). m <= n => LeqProof m n 

addNat :: forall (m :: Nat) (n :: Nat). NatRepr m -> NatRepr n -> NatRepr (m + n) #

leqTrans :: forall (m :: Nat) (n :: Nat) (p :: Nat). LeqProof m n -> LeqProof n p -> LeqProof m p #

leqAddPos :: forall (m :: Natural) (n :: Natural) p q. (1 <= m, 1 <= n) => p m -> q n -> LeqProof 1 (m + n) #

knownNat :: forall (n :: Nat). KnownNat n => NatRepr n #

class TestEquality (f :: k -> Type) where #

Methods

testEquality :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b) #

Instances

Instances details
TestEquality SNat 
Instance details

Defined in GHC.TypeNats

Methods

testEquality :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b) #

TestEquality NatRepr 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

testEquality :: forall (a :: Nat) (b :: Nat). NatRepr a -> NatRepr b -> Maybe (a :~: b) #

TestEquality PeanoRepr 
Instance details

Defined in Data.Parameterized.Peano

Methods

testEquality :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> Maybe (a :~: b) #

TestEquality BaseTypeRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

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

TestEquality ConcreteVal Source # 
Instance details

Defined in What4.Concrete

Methods

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

TestEquality IndexLit Source # 
Instance details

Defined in What4.IndexLit

Methods

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

TestEquality TypeMap Source # 
Instance details

Defined in What4.Protocol.SMTWriter

Methods

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

TestEquality OnlyIntRepr Source # 
Instance details

Defined in What4.Utils.OnlyIntRepr

Methods

testEquality :: forall (a :: BaseType) (b :: BaseType). OnlyIntRepr a -> OnlyIntRepr b -> Maybe (a :~: b) #

TestEquality FloatPrecisionRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

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

TestEquality StringInfoRepr Source # 
Instance details

Defined in What4.BaseTypes

Methods

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

TestEquality StringLiteral Source # 
Instance details

Defined in What4.Utils.StringLiteral

Methods

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

TestEquality FloatModeRepr Source # 
Instance details

Defined in What4.FloatMode

Methods

testEquality :: forall (a :: FloatMode) (b :: FloatMode). FloatModeRepr a -> FloatModeRepr b -> Maybe (a :~: b) #

TestEquality FloatInfoRepr Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

Methods

testEquality :: forall (a :: FloatInfo) (b :: FloatInfo). FloatInfoRepr a -> FloatInfoRepr b -> Maybe (a :~: b) #

TestEquality BVFlavorRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

testEquality :: forall (a :: BVFlavor) (b :: BVFlavor). BVFlavorRepr a -> BVFlavorRepr b -> Maybe (a :~: b) #

TestEquality OrderedSemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

testEquality :: forall (a :: SemiRing) (b :: SemiRing). OrderedSemiRingRepr a -> OrderedSemiRingRepr b -> Maybe (a :~: b) #

TestEquality SemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

testEquality :: forall (a :: SemiRing) (b :: SemiRing). SemiRingRepr a -> SemiRingRepr b -> Maybe (a :~: b) #

TestEquality BoolRepr 
Instance details

Defined in Data.Parameterized.BoolRepr

Methods

testEquality :: forall (a :: Bool) (b :: Bool). BoolRepr a -> BoolRepr b -> Maybe (a :~: b) #

TestEquality SChar 
Instance details

Defined in GHC.TypeLits

Methods

testEquality :: forall (a :: Char) (b :: Char). SChar a -> SChar b -> Maybe (a :~: b) #

TestEquality SSymbol 
Instance details

Defined in GHC.TypeLits

Methods

testEquality :: forall (a :: Symbol) (b :: Symbol). SSymbol a -> SSymbol b -> Maybe (a :~: b) #

TestEquality SymbolRepr 
Instance details

Defined in Data.Parameterized.SymbolRepr

Methods

testEquality :: forall (a :: Symbol) (b :: Symbol). SymbolRepr a -> SymbolRepr b -> Maybe (a :~: b) #

Eq p => TestEquality (UnaryBV p :: Nat -> Type) Source # 
Instance details

Defined in What4.Expr.UnaryBV

Methods

testEquality :: forall (a :: Nat) (b :: Nat). UnaryBV p a -> UnaryBV p b -> Maybe (a :~: b) #

(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) #

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

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

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

(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) #

OrdF f => TestEquality (SemiRingProduct f :: SemiRing -> Type) Source # 
Instance details

Defined in What4.Expr.WeightedSum

Methods

testEquality :: forall (a :: SemiRing) (b :: SemiRing). SemiRingProduct f a -> SemiRingProduct f b -> Maybe (a :~: b) #

OrdF f => TestEquality (WeightedSum f :: SemiRing -> Type) Source # 
Instance details

Defined in What4.Expr.WeightedSum

Methods

testEquality :: forall (a :: SemiRing) (b :: SemiRing). WeightedSum f a -> WeightedSum f b -> Maybe (a :~: b) #

TestEquality (TypeRep :: k -> Type) 
Instance details

Defined in Data.Typeable.Internal

Methods

testEquality :: forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a :~: b) #

TestEquality (Nonce :: k -> Type) 
Instance details

Defined in Data.Parameterized.Nonce.Unsafe

Methods

testEquality :: forall (a :: k) (b :: k). Nonce a -> Nonce b -> Maybe (a :~: b) #

TestEquality (Dummy :: k -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

testEquality :: forall (a :: k) (b :: k). Dummy a -> Dummy b -> Maybe (a :~: b) #

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

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

TestEquality ((:~:) a :: k -> Type) 
Instance details

Defined in Data.Type.Equality

Methods

testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) #

TestEquality (Index ctx :: k -> Type) 
Instance details

Defined in Data.Parameterized.Context.Safe

Methods

testEquality :: forall (a :: k) (b :: k). Index ctx a -> Index ctx b -> Maybe (a :~: b) #

TestEquality (Index ctx :: k -> Type) 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

testEquality :: forall (a :: k) (b :: k). Index ctx a -> Index ctx b -> Maybe (a :~: b) #

TestEquality (Index l :: k -> Type) 
Instance details

Defined in Data.Parameterized.List

Methods

testEquality :: forall (a :: k) (b :: k). Index l a -> Index l b -> Maybe (a :~: b) #

TestEquality (Nonce s :: k -> Type) 
Instance details

Defined in Data.Parameterized.Nonce

Methods

testEquality :: forall (a :: k) (b :: k). Nonce s a -> Nonce s b -> Maybe (a :~: b) #

OrdF e => TestEquality (SpecialFnArg e tp :: Type -> Type) Source # 
Instance details

Defined in What4.SpecialFunctions

Methods

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

TestEquality ((:~~:) a :: k -> Type) 
Instance details

Defined in Data.Type.Equality

Methods

testEquality :: forall (a0 :: k) (b :: k). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) #

TestEquality f => TestEquality (Compose f g :: k2 -> Type) 
Instance details

Defined in Data.Functor.Compose

Methods

testEquality :: forall (a :: k2) (b :: k2). Compose f g a -> Compose f g b -> Maybe (a :~: b) #

TestEquality SpecialFunction Source # 
Instance details

Defined in What4.SpecialFunctions

Methods

testEquality :: forall (a :: Ctx Type) (b :: Ctx Type). SpecialFunction a -> SpecialFunction b -> Maybe (a :~: b) #

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

TestEquality f => TestEquality (Assignment f :: Ctx k -> Type) 
Instance details

Defined in Data.Parameterized.Context.Safe

Methods

testEquality :: forall (a :: Ctx k) (b :: Ctx k). Assignment f a -> Assignment f b -> Maybe (a :~: b) #

TestEquality f => TestEquality (Assignment f :: Ctx k -> Type) 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

testEquality :: forall (a :: Ctx k) (b :: Ctx k). Assignment f a -> Assignment f b -> Maybe (a :~: b) #

TestEquality f => TestEquality (List f :: [k] -> Type) 
Instance details

Defined in Data.Parameterized.List

Methods

testEquality :: forall (a :: [k]) (b :: [k]). List f a -> List f b -> Maybe (a :~: b) #

(TestEquality f, TestEquality g) => TestEquality (PairRepr f g :: (k1, k2) -> Type) 
Instance details

Defined in Data.Parameterized.DataKind

Methods

testEquality :: forall (a :: (k1, k2)) (b :: (k1, k2)). PairRepr f g a -> PairRepr f g b -> Maybe (a :~: b) #

data (a :: k) :~: (b :: k) where #

Constructors

Refl :: forall {k} (a :: k). a :~: a 

Instances

Instances details
Category ((:~:) :: k -> k -> Type) 
Instance details

Defined in Control.Category

Methods

id :: forall (a :: k). a :~: a

(.) :: forall (b :: k) (c :: k) (a :: k). (b :~: c) -> (a :~: b) -> a :~: c

TestCoercion ((:~:) a :: k -> Type) 
Instance details

Defined in Data.Type.Coercion

Methods

testCoercion :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b)

TestEquality ((:~:) a :: k -> Type) 
Instance details

Defined in Data.Type.Equality

Methods

testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) #

NFData2 ((:~:) :: Type -> Type -> Type) 
Instance details

Defined in Control.DeepSeq

Methods

liftRnf2 :: (a -> ()) -> (b -> ()) -> (a :~: b) -> ()

NFData1 ((:~:) a) 
Instance details

Defined in Control.DeepSeq

Methods

liftRnf :: (a0 -> ()) -> (a :~: a0) -> ()

(a ~ b, Data a) => Data (a :~: b) 
Instance details

Defined in Data.Data

Methods

gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b)

gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b)

toConstr :: (a :~: b) -> Constr

dataTypeOf :: (a :~: b) -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b))

gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r

gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b)

a ~ b => Bounded (a :~: b) 
Instance details

Defined in Data.Type.Equality

Methods

minBound :: a :~: b

maxBound :: a :~: b

a ~ b => Enum (a :~: b) 
Instance details

Defined in Data.Type.Equality

Methods

succ :: (a :~: b) -> a :~: b

pred :: (a :~: b) -> a :~: b

toEnum :: Int -> a :~: b

fromEnum :: (a :~: b) -> Int

enumFrom :: (a :~: b) -> [a :~: b]

enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b]

enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b]

enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b]

a ~ b => Read (a :~: b) 
Instance details

Defined in Data.Type.Equality

Methods

readsPrec :: Int -> ReadS (a :~: b)

readList :: ReadS [a :~: b]

readPrec :: ReadPrec (a :~: b)

readListPrec :: ReadPrec [a :~: b]

Show (a :~: b) 
Instance details

Defined in Data.Type.Equality

Methods

showsPrec :: Int -> (a :~: b) -> ShowS

show :: (a :~: b) -> String

showList :: [a :~: b] -> ShowS

NFData (a :~: b) 
Instance details

Defined in Control.DeepSeq

Methods

rnf :: (a :~: b) -> ()

Eq (a :~: b) 
Instance details

Defined in Data.Type.Equality

Methods

(==) :: (a :~: b) -> (a :~: b) -> Bool

(/=) :: (a :~: b) -> (a :~: b) -> Bool

Ord (a :~: b) 
Instance details

Defined in Data.Type.Equality

Methods

compare :: (a :~: b) -> (a :~: b) -> Ordering

(<) :: (a :~: b) -> (a :~: b) -> Bool

(<=) :: (a :~: b) -> (a :~: b) -> Bool

(>) :: (a :~: b) -> (a :~: b) -> Bool

(>=) :: (a :~: b) -> (a :~: b) -> Bool

max :: (a :~: b) -> (a :~: b) -> a :~: b

min :: (a :~: b) -> (a :~: b) -> a :~: b

data NatComparison (m :: Natural) (n :: Natural) where #

Constructors

NatLT :: forall (m :: Natural) (y :: Natural). (m + 1) <= (m + (y + 1)) => !(NatRepr y) -> NatComparison m (m + (y + 1)) 
NatEQ :: forall (m :: Natural). NatComparison m m 
NatGT :: forall (n :: Natural) (y :: Natural). (n + 1) <= (n + (y + 1)) => !(NatRepr y) -> NatComparison (n + (y + 1)) n 

compareNat :: forall (m :: Nat) (n :: Nat). NatRepr m -> NatRepr n -> NatComparison m n #

addIsLeq :: forall f (n :: Nat) g (m :: Natural). f n -> g m -> LeqProof n (n + m) #

addIsLeqLeft1 :: forall (n :: Natural) (n' :: Natural) (m :: Nat). LeqProof (n + n') m -> LeqProof n m #

addMulDistribRight :: forall (n :: Natural) (m :: Natural) (p :: Natural) f g h. f n -> g m -> h p -> ((n * p) + (m * p)) :~: ((n + m) * p) #

addPrefixIsLeq :: forall f (m :: Natural) g (n :: Nat). f m -> g n -> LeqProof n (m + n) #

dblPosIsPos :: forall (n :: Nat). LeqProof 1 n -> LeqProof 1 (n + n) #

decNat :: forall (n :: Natural). 1 <= n => NatRepr n -> NatRepr (n - 1) #

decideLeq :: forall (a :: Nat) (b :: Nat). NatRepr a -> NatRepr b -> Either (LeqProof a b) (LeqProof a b -> Void) #

divNat :: forall (n :: Natural) (m :: Natural). 1 <= n => NatRepr (m * n) -> NatRepr n -> NatRepr m #

halfNat :: forall (n :: Natural). NatRepr (n + n) -> NatRepr n #

incNat :: forall (n :: Nat). NatRepr n -> NatRepr (n + 1) #

intValue :: forall (n :: Nat). NatRepr n -> Integer #

isPosNat :: forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n) #

isZeroNat :: forall (n :: Nat). NatRepr n -> IsZeroNat n #

isZeroOrGT1 :: forall (n :: Nat). NatRepr n -> Either (n :~: 0) (LeqProof 1 n) #

lemmaMul :: forall (n :: Natural) p (w :: Natural) q. 1 <= n => p w -> q n -> (w + ((n - 1) * w)) :~: (n * w) #

leqAdd :: forall f (m :: Nat) (n :: Nat) (p :: Natural). LeqProof m n -> f p -> LeqProof m (n + p) #

leqAdd2 :: forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat). LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h) #

leqMulCongr :: forall (a :: Nat) (x :: Nat) (b :: Nat) (y :: Nat). LeqProof a x -> LeqProof b y -> LeqProof (a * b) (x * y) #

leqMulMono :: forall (x :: Natural) p q (y :: Nat). 1 <= x => p x -> q y -> LeqProof y (x * y) #

leqMulPos :: forall p q (x :: Natural) (y :: Natural). (1 <= x, 1 <= y) => p x -> q y -> LeqProof 1 (x * y) #

leqProof :: forall (m :: Nat) (n :: Nat) f g. m <= n => f m -> g n -> LeqProof m n #

leqRefl :: forall f (n :: Nat). f n -> LeqProof n n #

leqSub :: forall (m :: Nat) (n :: Nat) (p :: Nat). LeqProof m n -> LeqProof p m -> LeqProof (m - p) n #

leqSub2 :: forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat). LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l - y_h) (x_h - y_l) #

leqSucc :: forall f (z :: Nat). f z -> LeqProof z (z + 1) #

leqZero :: forall (n :: Nat). LeqProof 0 n #

lessThanAsymmetric :: forall (m :: Nat) f (n :: Natural). LeqProof (n + 1) m -> LeqProof (m + 1) n -> f n -> Void #

lessThanIrreflexive :: forall f (a :: Nat). f a -> LeqProof (1 + a) a -> Void #

maxNat :: forall (m :: Nat) (n :: Nat). NatRepr m -> NatRepr n -> Some NatRepr #

maxSigned :: forall (w :: Natural). 1 <= w => NatRepr w -> Integer #

maxUnsigned :: forall (w :: Nat). NatRepr w -> Integer #

minSigned :: forall (w :: Natural). 1 <= w => NatRepr w -> Integer #

minUnsigned :: forall (w :: Nat). NatRepr w -> Integer #

minusPlusCancel :: forall f (m :: Natural) g (n :: Natural). n <= m => f m -> g n -> ((m - n) + n) :~: m #

mkNatRepr :: Natural -> Some NatRepr #

mul2Plus :: forall f (n :: Natural). f n -> (n + n) :~: (2 * n) #

mulCancelR :: forall (c :: Natural) (n1 :: Natural) (n2 :: Natural) f1 f2 f3. (1 <= c, (n1 * c) ~ (n2 * c)) => f1 n1 -> f2 n2 -> f3 c -> n1 :~: n2 #

mulComm :: forall f (m :: Natural) g (n :: Natural). f m -> g n -> (m * n) :~: (n * m) #

natForEach :: forall (l :: Nat) (h :: Nat) a. NatRepr l -> NatRepr h -> (forall (n :: Nat). (l <= n, n <= h) => NatRepr n -> a) -> [a] #

natFromZero :: forall (h :: Nat) a. NatRepr h -> (forall (n :: Nat). n <= h => NatRepr n -> a) -> [a] #

natMultiply :: forall (n :: Nat) (m :: Nat). NatRepr n -> NatRepr m -> NatRepr (n * m) #

natRec :: forall (p :: Nat) f. NatRepr p -> f 0 -> (forall (n :: Nat). NatRepr n -> f n -> f (n + 1)) -> f p #

natRecBounded :: forall (m :: Nat) (h :: Nat) f. m <= h => NatRepr m -> NatRepr h -> f 0 -> (forall (n :: Nat). n <= h => NatRepr n -> f n -> f (n + 1)) -> f (m + 1) #

natRecStrictlyBounded :: forall (m :: Nat) f. NatRepr m -> f 0 -> (forall (n :: Natural). (n + 1) <= m => NatRepr n -> f n -> f (n + 1)) -> f m #

natRecStrong :: forall (p :: Nat) f. NatRepr p -> f 0 -> (forall (n :: Nat). NatRepr n -> (forall (m :: Nat). m <= n => NatRepr m -> f m) -> f (n + 1)) -> f p #

plusAssoc :: forall f (m :: Natural) g (n :: Natural) h (o :: Natural). f m -> g n -> h o -> (m + (n + o)) :~: ((m + n) + o) #

plusComm :: forall f (m :: Natural) g (n :: Natural). f m -> g n -> (m + n) :~: (n + m) #

plusMinusCancel :: forall f (m :: Natural) g (n :: Natural). f m -> g n -> ((m + n) - n) :~: m #

predNat :: forall (n :: Natural). NatRepr (n + 1) -> NatRepr n #

signedClamp :: forall (w :: Natural). 1 <= w => NatRepr w -> Integer -> Integer #

someNat :: Integral a => a -> Maybe (Some NatRepr) #

subNat :: forall (n :: Nat) (m :: Nat). n <= m => NatRepr m -> NatRepr n -> NatRepr (m - n) #

testLeq :: forall (m :: Nat) (n :: Nat). NatRepr m -> NatRepr n -> Maybe (LeqProof m n) #

testNatCases :: forall (m :: Nat) (n :: Nat). NatRepr m -> NatRepr n -> NatCases m n #

testStrictLeq :: forall (m :: Nat) (n :: Nat). m <= n => NatRepr m -> NatRepr n -> Either (LeqProof (m + 1) n) (m :~: n) #

toSigned :: forall (w :: Natural). 1 <= w => NatRepr w -> Integer -> Integer #

toUnsigned :: forall (w :: Nat). NatRepr w -> Integer -> Integer #

unsignedClamp :: forall (w :: Nat). NatRepr w -> Integer -> Integer #

widthVal :: forall (n :: Nat). NatRepr n -> Int #

withAddLeq :: forall (n :: Nat) (m :: Nat) a. NatRepr n -> NatRepr m -> (n <= (n + m) => NatRepr (n + m) -> a) -> a #

withAddMulDistribRight :: forall (n :: Natural) (m :: Natural) (p :: Natural) f g h a. f n -> g m -> h p -> (((n * p) + (m * p)) ~ ((n + m) * p) => a) -> a #

withAddPrefixLeq :: forall (n :: Nat) (m :: Nat) a. NatRepr n -> NatRepr m -> (m <= (n + m) => a) -> a #

withDivModNat :: forall (n :: Nat) (m :: Nat) a. NatRepr n -> NatRepr m -> (forall (div :: Natural) (mod :: Natural). n ~ ((div * m) + mod) => NatRepr div -> NatRepr mod -> a) -> a #

withKnownNat :: forall (n :: Nat) r. NatRepr n -> (KnownNat n => r) -> r #

withLeqProof :: forall (m :: Nat) (n :: Nat) a. LeqProof m n -> (m <= n => a) -> a #

withSubMulDistribRight :: forall (n :: Natural) (m :: Natural) (p :: Natural) f g h a. m <= n => f n -> g m -> h p -> (((n * p) - (m * p)) ~ ((n - m) * p) => a) -> a #

data IsZeroNat (n :: Natural) where #

Constructors

ZeroNat :: IsZeroNat 0 
NonZeroNat :: forall (n1 :: Natural). IsZeroNat (n1 + 1) 

data NatCases (m :: Natural) (n :: Nat) where #

Constructors

NatCaseLT :: forall (m :: Natural) (n :: Nat). LeqProof (m + 1) n -> NatCases m n 
NatCaseEQ :: forall (m :: Natural). NatCases m m 
NatCaseGT :: forall (n :: Nat) (m :: Natural). LeqProof (n + 1) m -> NatCases m n 

KnownRepr

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

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 PeanoRepr Z 
Instance details

Defined in Data.Parameterized.Peano

Methods

knownRepr :: PeanoRepr Z #

KnownRepr BaseTypeRepr BaseBoolType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseComplexType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseIntegerType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr BaseTypeRepr BaseRealType Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr StringInfoRepr Char16 Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr StringInfoRepr Char8 Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr StringInfoRepr Unicode Source # 
Instance details

Defined in What4.BaseTypes

KnownRepr FloatModeRepr FloatIEEE Source # 
Instance details

Defined in What4.FloatMode

KnownRepr FloatModeRepr FloatReal Source # 
Instance details

Defined in What4.FloatMode

KnownRepr FloatModeRepr FloatUninterpreted Source # 
Instance details

Defined in What4.FloatMode

KnownRepr FloatInfoRepr DoubleDoubleFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

KnownRepr FloatInfoRepr DoubleFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

KnownRepr FloatInfoRepr HalfFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

KnownRepr FloatInfoRepr QuadFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

KnownRepr FloatInfoRepr SingleFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

KnownRepr FloatInfoRepr X86_80Float Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

KnownRepr BoolRepr 'False 
Instance details

Defined in Data.Parameterized.BoolRepr

Methods

knownRepr :: BoolRepr 'False #

KnownRepr BoolRepr 'True 
Instance details

Defined in Data.Parameterized.BoolRepr

Methods

knownRepr :: BoolRepr 'True #

KnownSymbol s => KnownRepr SymbolRepr (s :: Symbol) 
Instance details

Defined in Data.Parameterized.SymbolRepr

Methods

knownRepr :: SymbolRepr s #

KnownRepr PeanoRepr n => KnownRepr PeanoRepr (S n :: Peano) 
Instance details

Defined in Data.Parameterized.Peano

Methods

knownRepr :: PeanoRepr (S n) #

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

Defined in What4.BaseTypes

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

Defined in What4.BaseTypes

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

Defined in What4.BaseTypes

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

Defined in What4.BaseTypes

(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

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.Safe

Methods

knownRepr :: Assignment f (EmptyCtx :: Ctx k) #

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

Defined in Data.Parameterized.Context.Unsafe

Methods

knownRepr :: Assignment f (EmptyCtx :: Ctx k) #

KnownRepr (List f :: [k] -> Type) ('[] :: [k]) 
Instance details

Defined in Data.Parameterized.List

Methods

knownRepr :: List f ('[] :: [k]) #

(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) #

(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) #

(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) #

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

A Context where all the argument types are KnownRepr instances