Copyright	(c) Galois Inc 2018-2020
License	BSD3
Maintainer	Rob Dockins <[email protected]>
Stability	provisional
Safe Haskell	None
Language	Haskell2010

What4.Concrete

Contents

Concrete values
Concrete projections

Description

This module defines a representation of concrete values of base types. These are values in fully-evaluated form that do not depend on any symbolic constants.

Synopsis

data ConcreteVal (tp :: BaseType) where
- ConcreteBool :: Bool -> ConcreteVal 'BaseBoolType
- ConcreteInteger :: Integer -> ConcreteVal 'BaseIntegerType
- ConcreteReal :: Rational -> ConcreteVal 'BaseRealType
- ConcreteFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> BigFloat -> ConcreteVal ('BaseFloatType fpp)
- ConcreteString :: forall (si :: StringInfo). StringLiteral si -> ConcreteVal ('BaseStringType si)
- ConcreteComplex :: Complex Rational -> ConcreteVal 'BaseComplexType
- ConcreteBV :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> ConcreteVal ('BaseBVType w)
- ConcreteStruct :: forall (ctx :: Ctx BaseType). Assignment ConcreteVal ctx -> ConcreteVal ('BaseStructType ctx)
- ConcreteArray :: forall (idx :: Ctx BaseType) (i :: BaseType) (b :: BaseType). Assignment BaseTypeRepr (idx ::> i) -> ConcreteVal b -> Map (Assignment ConcreteVal (idx ::> i)) (ConcreteVal b) -> ConcreteVal ('BaseArrayType (idx ::> i) b)
concreteType :: forall (tp :: BaseType). ConcreteVal tp -> BaseTypeRepr tp
ppConcrete :: forall (tp :: BaseType) ann. ConcreteVal tp -> Doc ann
fromConcreteBool :: ConcreteVal BaseBoolType -> Bool
fromConcreteInteger :: ConcreteVal BaseIntegerType -> Integer
fromConcreteReal :: ConcreteVal BaseRealType -> Rational
fromConcreteString :: forall (si :: StringInfo). ConcreteVal (BaseStringType si) -> StringLiteral si
fromConcreteBV :: forall (w :: Nat). ConcreteVal (BaseBVType w) -> BV w
fromConcreteComplex :: ConcreteVal BaseComplexType -> Complex Rational

Concrete values

data ConcreteVal (tp :: BaseType) where Source #

A data type for representing the concrete values of base types.

Constructors

ConcreteBool :: Bool -> ConcreteVal 'BaseBoolType
ConcreteInteger :: Integer -> ConcreteVal 'BaseIntegerType
ConcreteReal :: Rational -> ConcreteVal 'BaseRealType
ConcreteFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> BigFloat -> ConcreteVal ('BaseFloatType fpp)
ConcreteString :: forall (si :: StringInfo). StringLiteral si -> ConcreteVal ('BaseStringType si)
ConcreteComplex :: Complex Rational -> ConcreteVal 'BaseComplexType
ConcreteBV :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> ConcreteVal ('BaseBVType w)
ConcreteStruct :: forall (ctx :: Ctx BaseType). Assignment ConcreteVal ctx -> ConcreteVal ('BaseStructType ctx)
ConcreteArray :: forall (idx :: Ctx BaseType) (i :: BaseType) (b :: BaseType). Assignment BaseTypeRepr (idx ::> i) -> ConcreteVal b -> Map (Assignment ConcreteVal (idx ::> i)) (ConcreteVal b) -> ConcreteVal ('BaseArrayType (idx ::> i) b)

Instances

Instances details

TestEquality ConcreteVal Source #
Instance details Defined in What4.Concrete Methods testEquality :: forall (a :: BaseType) (b :: BaseType). ConcreteVal a -> ConcreteVal b -> Maybe (a :~: b) #
OrdF ConcreteVal Source #
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 #
ShowF ConcreteVal Source #
Instance details Defined in What4.Concrete Methods withShow :: forall p q (tp :: BaseType) a. p ConcreteVal -> q tp -> (Show (ConcreteVal tp) => a) -> a # showF :: forall (tp :: BaseType). ConcreteVal tp -> String # showsPrecF :: forall (tp :: BaseType). Int -> ConcreteVal tp -> String -> String #
Show (ConcreteVal tp) Source #
Instance details Defined in What4.Concrete Methods showsPrec :: Int -> ConcreteVal tp -> ShowS # show :: ConcreteVal tp -> String # showList :: [ConcreteVal tp] -> ShowS #
Eq (ConcreteVal tp) Source #
Instance details Defined in What4.Concrete Methods (==) :: ConcreteVal tp -> ConcreteVal tp -> Bool # (/=) :: ConcreteVal tp -> ConcreteVal tp -> Bool #
Ord (ConcreteVal tp) Source #
Instance details Defined in What4.Concrete Methods compare :: ConcreteVal tp -> ConcreteVal tp -> Ordering # (<) :: ConcreteVal tp -> ConcreteVal tp -> Bool # (<=) :: ConcreteVal tp -> ConcreteVal tp -> Bool # (>) :: ConcreteVal tp -> ConcreteVal tp -> Bool # (>=) :: ConcreteVal tp -> ConcreteVal tp -> Bool # max :: ConcreteVal tp -> ConcreteVal tp -> ConcreteVal tp # min :: ConcreteVal tp -> ConcreteVal tp -> ConcreteVal tp #

concreteType :: forall (tp :: BaseType). ConcreteVal tp -> BaseTypeRepr tp Source #

Compute the type representative for a concrete value.

ppConcrete :: forall (tp :: BaseType) ann. ConcreteVal tp -> Doc ann Source #

Pretty-print a concrete value

Concrete projections

fromConcreteBool :: ConcreteVal BaseBoolType -> Bool Source #

fromConcreteInteger :: ConcreteVal BaseIntegerType -> Integer Source #

fromConcreteReal :: ConcreteVal BaseRealType -> Rational Source #

fromConcreteString :: forall (si :: StringInfo). ConcreteVal (BaseStringType si) -> StringLiteral si Source #

fromConcreteBV :: forall (w :: Nat). ConcreteVal (BaseBVType w) -> BV w Source #

fromConcreteComplex :: ConcreteVal BaseComplexType -> Complex Rational Source #