What4.Concrete

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.

Concrete values

data ConcreteVal tp where

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

Constructors

ConcreteBool :: Bool -> ConcreteVal BaseBoolType

ConcreteNat :: Natural -> ConcreteVal BaseNatType

ConcreteInteger :: Integer -> ConcreteVal BaseIntegerType

ConcreteReal :: Rational -> ConcreteVal BaseRealType

ConcreteString :: StringLiteral si -> ConcreteVal (BaseStringType si)

ConcreteComplex :: Complex Rational -> ConcreteVal BaseComplexType

ConcreteBV :: 1 <= w => NatRepr w -> BV w -> ConcreteVal (BaseBVType w)

ConcreteStruct :: Assignment ConcreteVal ctx -> ConcreteVal (BaseStructType ctx)

ConcreteArray :: Assignment BaseTypeRepr (idx ::> i) -> ConcreteVal b -> Map (Assignment ConcreteVal (idx ::> i)) (ConcreteVal b) -> ConcreteVal (BaseArrayType (idx ::> i) b)

Instances

TestEquality ConcreteVal

Defined in What4.Concrete

Methods

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

OrdF ConcreteVal

Defined in What4.Concrete

Methods

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

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

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

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

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

ShowF ConcreteVal

Defined in What4.Concrete

Methods

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

showF :: ConcreteVal tp -> String

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

Eq (ConcreteVal tp)

Defined in What4.Concrete

Methods

(==) :: ConcreteVal tp -> ConcreteVal tp -> Bool

(/=) :: ConcreteVal tp -> ConcreteVal tp -> Bool

Ord (ConcreteVal tp)

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

Show (ConcreteVal tp)

Defined in What4.Concrete

Methods

showsPrec :: Int -> ConcreteVal tp -> ShowS

show :: ConcreteVal tp -> String

showList :: [ConcreteVal tp] -> ShowS

concreteType :: ConcreteVal tp -> BaseTypeRepr tp

Compute the type representative for a concrete value.

ppConcrete :: ConcreteVal tp -> Doc

Pretty-print a concrete value

Concrete projections

fromConcreteBool :: ConcreteVal BaseBoolType -> Bool

fromConcreteNat :: ConcreteVal BaseNatType -> Natural

fromConcreteInteger :: ConcreteVal BaseIntegerType -> Integer

fromConcreteReal :: ConcreteVal BaseRealType -> Rational

fromConcreteString :: ConcreteVal (BaseStringType si) -> StringLiteral si

fromConcreteBV :: ConcreteVal (BaseBVType w) -> BV w

fromConcreteComplex :: ConcreteVal BaseComplexType -> Complex Rational