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
- 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 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
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) #
OrdF ConcreteVal Source #
Instance details Defined in What4.Concrete Methods compareF :: forall (x :: k) (y :: k). ConcreteVal x -> ConcreteVal y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). ConcreteVal x -> ConcreteVal y -> Bool # ltF :: forall (x :: k) (y :: k). ConcreteVal x -> ConcreteVal y -> Bool # geqF :: forall (x :: k) (y :: k). ConcreteVal x -> ConcreteVal y -> Bool # gtF :: forall (x :: k) (y :: k). ConcreteVal x -> ConcreteVal y -> Bool #
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 # showF :: forall (tp :: k). ConcreteVal tp -> String # showsPrecF :: forall (tp :: k). 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 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 #