what4-1.5.1: Solver-agnostic symbolic values support for issuing queries

Copyright | (c) Galois Inc 2018-2020
License | BSD3
Maintainer | Rob Dockins <rdockins@galois.com>
Stability | provisional
Safe Haskell | Safe-Inferred
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 where
  - ConcreteBool :: Bool -> ConcreteVal BaseBoolType
  - ConcreteInteger :: Integer -> ConcreteVal BaseIntegerType
  - ConcreteReal :: Rational -> ConcreteVal BaseRealType
  - ConcreteFloat :: FloatPrecisionRepr fpp -> BigFloat -> ConcreteVal (BaseFloatType fpp)
  - 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)
- concreteType :: ConcreteVal tp -> BaseTypeRepr tp
- ppConcrete :: ConcreteVal tp -> Doc ann
- fromConcreteBool :: ConcreteVal BaseBoolType -> Bool
- 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

# Concrete values

data ConcreteVal tp 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 :: FloatPrecisionRepr fpp -> BigFloat -> ConcreteVal (BaseFloatType fpp) |
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

Instances details

TestEquality ConcreteVal Source # |
Instance details Defined in What4.Concrete Methods testEquality :: forall (a :: k) (b :: k). ConcreteVal a -> ConcreteVal b -> Maybe (a :~: b) Source #
OrdF ConcreteVal Source # |

Instance details

Defined in What4.Concrete

Methods

compareF :: forall (x :: k) (y :: k). ConcreteVal x -> ConcreteVal y -> OrderingF x y Source #

leqF :: forall (x :: k) (y :: k). ConcreteVal x -> ConcreteVal y -> Bool Source #

ltF :: forall (x :: k) (y :: k). ConcreteVal x -> ConcreteVal y -> Bool Source #

geqF :: forall (x :: k) (y :: k). ConcreteVal x -> ConcreteVal y -> Bool Source #

gtF :: forall (x :: k) (y :: k). ConcreteVal x -> ConcreteVal y -> Bool Source #

ShowF ConcreteVal Source # |
Instance details Defined in What4.Concrete Methods withShow :: forall p q (tp :: k) a. p ConcreteVal -> q tp -> (Show (ConcreteVal tp) => a) -> a Source # showF :: forall (tp :: k). ConcreteVal tp -> String Source # showsPrecF :: forall (tp :: k). Int -> ConcreteVal tp -> String -> String Source #
Show (ConcreteVal tp) Source # |
Instance details Defined in What4.Concrete Methods showsPrec :: Int -> ConcreteVal tp -> ShowS Source # show :: ConcreteVal tp -> String Source # showList :: [ConcreteVal tp] -> ShowS Source #
Eq (ConcreteVal tp) Source # |
Instance details Defined in What4.Concrete Methods (==) :: ConcreteVal tp -> ConcreteVal tp -> Bool Source # (/=) :: ConcreteVal tp -> ConcreteVal tp -> Bool Source #
Ord (ConcreteVal tp) Source # |

Instance details

Defined in What4.Concrete

Methods

compare :: ConcreteVal tp -> ConcreteVal tp -> Ordering Source #

(<) :: ConcreteVal tp -> ConcreteVal tp -> Bool Source #

(<=) :: ConcreteVal tp -> ConcreteVal tp -> Bool Source #

(>) :: ConcreteVal tp -> ConcreteVal tp -> Bool Source #

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

max :: ConcreteVal tp -> ConcreteVal tp -> ConcreteVal tp Source #

min :: ConcreteVal tp -> ConcreteVal tp -> ConcreteVal tp Source #

concreteType :: ConcreteVal tp -> BaseTypeRepr tp Source #

Compute the type representative for a concrete value.

ppConcrete :: 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 :: ConcreteVal (BaseStringType si) -> StringLiteral si Source #

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

fromConcreteComplex :: ConcreteVal BaseComplexType -> Complex Rational Source #