what4-1.6.3: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2018-2020
LicenseBSD3
MaintainerRob Dockins <rdockins@galois.com>
Stabilityprovisional
Safe HaskellNone
LanguageHaskell2010

What4.Concrete

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

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

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