Copyright	(c) Galois Inc 2018-2020
License	BSD3
Maintainer	Rob Dockins <rdockins@galois.com>
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 where
- 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)
concreteType :: ConcreteVal tp -> BaseTypeRepr tp
ppConcrete :: ConcreteVal tp -> Doc
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

Concrete values

data ConcreteVal tp where Source #

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 Source #
Instance details Defined in What4.Concrete Methods testEquality :: ConcreteVal a -> ConcreteVal b -> Maybe (a :~: b) #
OrdF ConcreteVal Source #
Instance details 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 Source #
Instance details 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) 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 #
Show (ConcreteVal tp) Source #
Instance details Defined in What4.Concrete Methods showsPrec :: Int -> ConcreteVal tp -> ShowS # show :: ConcreteVal tp -> String # showList :: [ConcreteVal tp] -> ShowS #

concreteType :: ConcreteVal tp -> BaseTypeRepr tp Source #

Compute the type representative for a concrete value.

ppConcrete :: ConcreteVal tp -> Doc Source #

Pretty-print a concrete value

Concrete projections

fromConcreteBool :: ConcreteVal BaseBoolType -> Bool Source #

fromConcreteNat :: ConcreteVal BaseNatType -> Natural 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 #