Copyright | (c) Galois Inc 2014-2020 |
---|---|
License | BSD3 |
Maintainer | Joe Hendrix <jhendrix@galois.com> |
Stability | provisional |
Safe Haskell | None |
Language | Haskell2010 |
What4.BaseTypes
Description
This module exports the types used in solver expressions.
These types are largely used as indexes to various GADTs and type families as a way to let the GHC typechecker help us keep expressions used by solvers apart.
In addition, we provide a value-level reification of the type
indices that can be examined by pattern matching, called BaseTypeRepr
.
Synopsis
- data BaseType
- type BaseBoolType = 'BaseBoolType
- type BaseIntegerType = 'BaseIntegerType
- type BaseRealType = 'BaseRealType
- type BaseStringType = 'BaseStringType
- type BaseBVType = 'BaseBVType
- type BaseFloatType = 'BaseFloatType
- type BaseComplexType = 'BaseComplexType
- type BaseStructType = 'BaseStructType
- type BaseArrayType = 'BaseArrayType
- data StringInfo
- type Char8 = 'Char8
- type Char16 = 'Char16
- type Unicode = 'Unicode
- data FloatPrecision
- type family FloatPrecisionBits (fpp :: FloatPrecision) :: Nat where ...
- type FloatingPointPrecision = 'FloatingPointPrecision
- type Prec16 = FloatingPointPrecision 5 11
- type Prec32 = FloatingPointPrecision 8 24
- type Prec64 = FloatingPointPrecision 11 53
- type Prec80 = FloatingPointPrecision 15 65
- type Prec128 = FloatingPointPrecision 15 113
- data BaseTypeRepr (bt :: BaseType) where
- BaseBoolRepr :: BaseTypeRepr 'BaseBoolType
- BaseBVRepr :: forall (w :: Natural). 1 <= w => !(NatRepr w) -> BaseTypeRepr ('BaseBVType w)
- BaseIntegerRepr :: BaseTypeRepr 'BaseIntegerType
- BaseRealRepr :: BaseTypeRepr 'BaseRealType
- BaseFloatRepr :: forall (fpp :: FloatPrecision). !(FloatPrecisionRepr fpp) -> BaseTypeRepr ('BaseFloatType fpp)
- BaseStringRepr :: forall (si :: StringInfo). StringInfoRepr si -> BaseTypeRepr ('BaseStringType si)
- BaseComplexRepr :: BaseTypeRepr 'BaseComplexType
- BaseStructRepr :: forall (ctx :: Ctx BaseType). !(Assignment BaseTypeRepr ctx) -> BaseTypeRepr ('BaseStructType ctx)
- BaseArrayRepr :: forall (idx :: Ctx BaseType) (tp :: BaseType) (xs :: BaseType). !(Assignment BaseTypeRepr (idx ::> tp)) -> !(BaseTypeRepr xs) -> BaseTypeRepr ('BaseArrayType (idx ::> tp) xs)
- data FloatPrecisionRepr (fpp :: FloatPrecision) where
- FloatingPointPrecisionRepr :: forall (eb :: Natural) (sb :: Natural). (2 <= eb, 2 <= sb) => !(NatRepr eb) -> !(NatRepr sb) -> FloatPrecisionRepr ('FloatingPointPrecision eb sb)
- data StringInfoRepr (si :: StringInfo) where
- Char8Repr :: StringInfoRepr 'Char8
- Char16Repr :: StringInfoRepr 'Char16
- UnicodeRepr :: StringInfoRepr 'Unicode
- arrayTypeIndices :: forall (idx :: Ctx BaseType) (tp :: BaseType). BaseTypeRepr (BaseArrayType idx tp) -> Assignment BaseTypeRepr idx
- arrayTypeResult :: forall (idx :: Ctx BaseType) (tp :: BaseType). BaseTypeRepr (BaseArrayType idx tp) -> BaseTypeRepr tp
- floatPrecisionToBVType :: forall (eb :: Nat) (sb :: Nat). FloatPrecisionRepr (FloatingPointPrecision eb sb) -> BaseTypeRepr (BaseBVType (eb + sb))
- lemmaFloatPrecisionIsPos :: forall (eb' :: Nat) (sb' :: Nat). FloatPrecisionRepr (FloatingPointPrecision eb' sb') -> LeqProof 1 (eb' + sb')
- type family (a :: Natural) - (b :: Natural) :: Natural where ...
- type family (a :: Natural) * (b :: Natural) :: Natural where ...
- data NatRepr (n :: Nat)
- data Some (f :: k -> Type)
- 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
- 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
- testEquality :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
- data (a :: k) :~: (b :: k) where
- data NatComparison (m :: Natural) (n :: Natural) where
- 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
- ZeroNat :: IsZeroNat 0
- NonZeroNat :: forall (n1 :: Natural). IsZeroNat (n1 + 1)
- data NatCases (m :: Natural) (n :: Nat) where
- class KnownRepr (f :: k -> Type) (ctx :: k) where
- knownRepr :: f ctx
- type KnownCtx (f :: k -> Type) = KnownRepr (Assignment f)
BaseType data kind
This data kind enumerates the Crucible solver interface types, which are types that may be represented symbolically.
Instances
TestEquality BaseTypeRepr Source # | |
Defined in What4.BaseTypes Methods testEquality :: forall (a :: BaseType) (b :: BaseType). BaseTypeRepr a -> BaseTypeRepr b -> Maybe (a :~: b) # | |
TestEquality ConcreteVal Source # | |
Defined in What4.Concrete Methods testEquality :: forall (a :: BaseType) (b :: BaseType). ConcreteVal a -> ConcreteVal b -> Maybe (a :~: b) # | |
TestEquality IndexLit Source # | |
Defined in What4.IndexLit | |
TestEquality TypeMap Source # | |
Defined in What4.Protocol.SMTWriter | |
TestEquality OnlyIntRepr Source # | |
Defined in What4.Utils.OnlyIntRepr Methods testEquality :: forall (a :: BaseType) (b :: BaseType). OnlyIntRepr a -> OnlyIntRepr b -> Maybe (a :~: b) # | |
HashableF BaseTypeRepr Source # | |
Defined in What4.BaseTypes Methods hashWithSaltF :: forall (tp :: BaseType). Int -> BaseTypeRepr tp -> Int hashF :: forall (tp :: BaseType). BaseTypeRepr tp -> Int | |
HashableF IndexLit | |
Defined in What4.IndexLit | |
HashableF OnlyIntRepr | |
Defined in What4.Utils.OnlyIntRepr Methods hashWithSaltF :: forall (tp :: BaseType). Int -> OnlyIntRepr tp -> Int hashF :: forall (tp :: BaseType). OnlyIntRepr tp -> Int | |
OrdF BaseTypeRepr Source # | |
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 | |
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 | |
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 # | |
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 | |
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 | |
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 | |
ShowF TypeMap | |
KnownRepr BaseTypeRepr BaseBoolType Source # | |
Defined in What4.BaseTypes Methods | |
KnownRepr BaseTypeRepr BaseComplexType Source # | |
Defined in What4.BaseTypes Methods | |
KnownRepr BaseTypeRepr BaseIntegerType Source # | |
Defined in What4.BaseTypes Methods | |
KnownRepr BaseTypeRepr BaseRealType Source # | |
Defined in What4.BaseTypes Methods | |
FoldableFC App | |
Defined in What4.Expr.App Methods foldMapFC :: forall f m. Monoid m => (forall (x :: 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 # | |
Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseBVType w) # | |
KnownRepr FloatPrecisionRepr fpp => KnownRepr BaseTypeRepr (BaseFloatType fpp :: BaseType) Source # | |
Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseFloatType fpp) # | |
KnownRepr StringInfoRepr si => KnownRepr BaseTypeRepr (BaseStringType si :: BaseType) Source # | |
Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseStringType si) # | |
KnownRepr (Assignment BaseTypeRepr) ctx => KnownRepr BaseTypeRepr (BaseStructType ctx :: BaseType) Source # | |
Defined in What4.BaseTypes Methods knownRepr :: BaseTypeRepr (BaseStructType ctx) # | |
FoldableFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) | |
Defined in What4.Expr.App Methods foldMapFC :: forall f m. Monoid m => (forall (x :: 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) | |
TraversableFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) | |
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 # | |
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 # | |
Defined in What4.Expr.App | |
TestEquality (Expr t :: BaseType -> Type) Source # | |
Defined in What4.Expr.App | |
TestEquality (ExprBoundVar t :: BaseType -> Type) Source # | |
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 # | |
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) | |
Defined in What4.Expr.App | |
HashableF (Expr t :: BaseType -> Type) | |
Defined in What4.Expr.App | |
HashableF (ExprBoundVar t :: BaseType -> Type) | |
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) | |
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) | |
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) | |
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) | |
ShowF (ExprBoundVar t :: BaseType -> Type) | |
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 # | |
Defined in What4.Expr.App | |
TestEquality f => TestEquality (ArrayResultWrapper f idx :: BaseType -> Type) Source # | |
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) | |
Defined in What4.Expr.App | |
HashableF e => HashableF (ArrayResultWrapper e idx :: BaseType -> Type) | |
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 # | |
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 # | |
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) | |
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 |
|
type BaseIntegerType Source #
Arguments
= 'BaseIntegerType |
|
type BaseRealType Source #
Arguments
= 'BaseRealType |
|
type BaseStringType Source #
Arguments
= 'BaseStringType |
|
type BaseBVType Source #
type BaseFloatType Source #
Arguments
= 'BaseFloatType |
|
type BaseComplexType Source #
Arguments
= 'BaseComplexType |
|
StringInfo data kind
data StringInfo Source #
Instances
Constructors for StringInfo
Arguments
= 'Char8 |
|
Arguments
= 'Char16 |
|
Arguments
= 'Unicode |
|
FloatPrecision data kind
data FloatPrecision Source #
This data kind describes the types of floating-point formats. This consist of the standard IEEE 754-2008 binary floating point formats.
Instances
type family FloatPrecisionBits (fpp :: FloatPrecision) :: Nat where ... Source #
This computes the number of bits occupied by a floating-point format.
Equations
FloatPrecisionBits (FloatingPointPrecision eb sb) = eb + sb |
Constructors for kind FloatPrecision
type FloatingPointPrecision Source #
Arguments
= 'FloatingPointPrecision |
|
FloatingPointPrecision aliases
type Prec16 = FloatingPointPrecision 5 11 Source #
Floating-point precision aliases
type Prec32 = FloatingPointPrecision 8 24 Source #
type Prec64 = FloatingPointPrecision 11 53 Source #
type Prec80 = FloatingPointPrecision 15 65 Source #
type Prec128 = FloatingPointPrecision 15 113 Source #
Representations of base types
data BaseTypeRepr (bt :: BaseType) 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
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
data StringInfoRepr (si :: StringInfo) where Source #
Constructors
Char8Repr :: StringInfoRepr 'Char8 | |
Char16Repr :: StringInfoRepr 'Char16 | |
UnicodeRepr :: StringInfoRepr 'Unicode |
Instances
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 #
Instances
TestEquality NatRepr | |
Defined in Data.Parameterized.NatRepr.Internal Methods testEquality :: forall (a :: Nat) (b :: Nat). NatRepr a -> NatRepr b -> Maybe (a :~: b) # | |
EqF NatRepr | |
Defined in Data.Parameterized.NatRepr.Internal | |
HashableF NatRepr | |
Defined in Data.Parameterized.NatRepr.Internal Methods hashWithSaltF :: forall (tp :: Nat). Int -> NatRepr tp -> Int | |
OrdF NatRepr | |
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 | |
Defined in Data.Parameterized.NatRepr.Internal | |
DecidableEq NatRepr | |
IsRepr NatRepr | |
Defined in Data.Parameterized.WithRepr | |
KnownNat n => KnownRepr NatRepr (n :: Nat) | |
Defined in Data.Parameterized.NatRepr.Internal | |
KnownNat n => Data (NatRepr n) | |
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) | |
Eq (NatRepr m) | |
Hashable (NatRepr n) | |
Defined in Data.Parameterized.NatRepr.Internal | |
PolyEq (NatRepr m) (NatRepr n) | |
Instances
OrdC (Some :: (k -> Type) -> Type) | |
Defined in Data.Parameterized.ClassesC | |
TestEqualityC (Some :: (k -> Type) -> Type) | |
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) | |
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 | |
FunctorF (Some :: (k -> Type) -> Type) | |
Defined in Data.Parameterized.Some | |
TraversableF (Some :: (k -> Type) -> Type) | |
Defined in Data.Parameterized.Some | |
ShowF f => Show (Some f) | |
TestEquality f => Eq (Some f) | |
OrdF f => Ord (Some f) | |
(HashableF f, TestEquality f) => Hashable (Some f) | |
Defined in Data.Parameterized.Some |
leqAddPos :: forall (m :: Natural) (n :: Natural) p q. (1 <= m, 1 <= n) => p m -> q n -> LeqProof 1 (m + n) #
class TestEquality (f :: k -> Type) where #
Methods
testEquality :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b) #
Instances
TestEquality SNat | |
Defined in GHC.TypeNats Methods testEquality :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b) # | |
TestEquality NatRepr | |
Defined in Data.Parameterized.NatRepr.Internal Methods testEquality :: forall (a :: Nat) (b :: Nat). NatRepr a -> NatRepr b -> Maybe (a :~: b) # | |
TestEquality PeanoRepr | |
Defined in Data.Parameterized.Peano Methods testEquality :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> Maybe (a :~: b) # | |
TestEquality BaseTypeRepr Source # | |
Defined in What4.BaseTypes Methods testEquality :: forall (a :: BaseType) (b :: BaseType). BaseTypeRepr a -> BaseTypeRepr b -> Maybe (a :~: b) # | |
TestEquality ConcreteVal Source # | |
Defined in What4.Concrete Methods testEquality :: forall (a :: BaseType) (b :: BaseType). ConcreteVal a -> ConcreteVal b -> Maybe (a :~: b) # | |
TestEquality IndexLit Source # | |
Defined in What4.IndexLit | |
TestEquality TypeMap Source # | |
Defined in What4.Protocol.SMTWriter | |
TestEquality OnlyIntRepr Source # | |
Defined in What4.Utils.OnlyIntRepr Methods testEquality :: forall (a :: BaseType) (b :: BaseType). OnlyIntRepr a -> OnlyIntRepr b -> Maybe (a :~: b) # | |
TestEquality FloatPrecisionRepr Source # | |
Defined in What4.BaseTypes Methods testEquality :: forall (a :: FloatPrecision) (b :: FloatPrecision). FloatPrecisionRepr a -> FloatPrecisionRepr b -> Maybe (a :~: b) # | |
TestEquality StringInfoRepr Source # | |
Defined in What4.BaseTypes Methods testEquality :: forall (a :: StringInfo) (b :: StringInfo). StringInfoRepr a -> StringInfoRepr b -> Maybe (a :~: b) # | |
TestEquality StringLiteral Source # | |
Defined in What4.Utils.StringLiteral Methods testEquality :: forall (a :: StringInfo) (b :: StringInfo). StringLiteral a -> StringLiteral b -> Maybe (a :~: b) # | |
TestEquality FloatModeRepr Source # | |
Defined in What4.FloatMode Methods testEquality :: forall (a :: FloatMode) (b :: FloatMode). FloatModeRepr a -> FloatModeRepr b -> Maybe (a :~: b) # | |
TestEquality FloatInfoRepr Source # | |
Defined in What4.InterpretedFloatingPoint Methods testEquality :: forall (a :: FloatInfo) (b :: FloatInfo). FloatInfoRepr a -> FloatInfoRepr b -> Maybe (a :~: b) # | |
TestEquality BVFlavorRepr Source # | |
Defined in What4.SemiRing Methods testEquality :: forall (a :: BVFlavor) (b :: BVFlavor). BVFlavorRepr a -> BVFlavorRepr b -> Maybe (a :~: b) # | |
TestEquality OrderedSemiRingRepr Source # | |
Defined in What4.SemiRing Methods testEquality :: forall (a :: SemiRing) (b :: SemiRing). OrderedSemiRingRepr a -> OrderedSemiRingRepr b -> Maybe (a :~: b) # | |
TestEquality SemiRingRepr Source # | |
Defined in What4.SemiRing Methods testEquality :: forall (a :: SemiRing) (b :: SemiRing). SemiRingRepr a -> SemiRingRepr b -> Maybe (a :~: b) # | |
TestEquality BoolRepr | |
Defined in Data.Parameterized.BoolRepr Methods testEquality :: forall (a :: Bool) (b :: Bool). BoolRepr a -> BoolRepr b -> Maybe (a :~: b) # | |
TestEquality SChar | |
Defined in GHC.TypeLits Methods testEquality :: forall (a :: Char) (b :: Char). SChar a -> SChar b -> Maybe (a :~: b) # | |
TestEquality SSymbol | |
Defined in GHC.TypeLits Methods testEquality :: forall (a :: Symbol) (b :: Symbol). SSymbol a -> SSymbol b -> Maybe (a :~: b) # | |
TestEquality SymbolRepr | |
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 # | |
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 # | |
Defined in What4.Expr.App | |
TestEquality (Expr t :: BaseType -> Type) Source # | |
Defined in What4.Expr.App | |
TestEquality (ExprBoundVar t :: BaseType -> Type) Source # | |
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 # | |
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 # | |
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 # | |
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 # | |
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) | |
Defined in Data.Typeable.Internal Methods testEquality :: forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a :~: b) # | |
TestEquality (Nonce :: k -> Type) | |
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 # | |
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 # | |
Defined in What4.Expr.App | |
TestEquality f => TestEquality (ArrayResultWrapper f idx :: BaseType -> Type) Source # | |
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) | |
Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) # | |
TestEquality (Index ctx :: k -> Type) | |
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) | |
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) | |
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) | |
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 # | |
Defined in What4.SpecialFunctions Methods testEquality :: SpecialFnArg e tp a -> SpecialFnArg e tp b -> Maybe (a :~: b) # | |
TestEquality ((:~~:) a :: k -> Type) | |
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) | |
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 # | |
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 # | |
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) | |
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) | |
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) | |
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) | |
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 #
Instances
Category ((:~:) :: k -> k -> Type) | |
TestCoercion ((:~:) a :: k -> Type) | |
Defined in Data.Type.Coercion Methods testCoercion :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b) | |
TestEquality ((:~:) a :: k -> Type) | |
Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) # | |
NFData2 ((:~:) :: Type -> Type -> Type) | |
Defined in Control.DeepSeq | |
NFData1 ((:~:) a) | |
Defined in Control.DeepSeq | |
(a ~ b, Data a) => Data (a :~: b) | |
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) | |
Defined in Data.Type.Equality | |
a ~ b => Enum (a :~: b) | |
Defined in Data.Type.Equality | |
a ~ b => Read (a :~: b) | |
Defined in Data.Type.Equality | |
Show (a :~: b) | |
NFData (a :~: b) | |
Defined in Control.DeepSeq | |
Eq (a :~: b) | |
Ord (a :~: b) | |
Defined in Data.Type.Equality |
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 #
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) #
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 #
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) #
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) #
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 #
maxUnsigned :: forall (w :: Nat). 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 #
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 #
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] #
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) #
plusMinusCancel :: forall f (m :: Natural) g (n :: Natural). f m -> g n -> ((m + n) - n) :~: m #
signedClamp :: forall (w :: Natural). 1 <= w => NatRepr w -> Integer -> Integer #
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) #
toUnsigned :: forall (w :: Nat). NatRepr w -> Integer -> Integer #
unsignedClamp :: forall (w :: Nat). NatRepr w -> Integer -> Integer #
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) |
KnownRepr
class KnownRepr (f :: k -> Type) (ctx :: k) where #