{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module What4.Concrete
(
ConcreteVal(..)
, concreteType
, ppConcrete
, fromConcreteBool
, fromConcreteInteger
, fromConcreteReal
, fromConcreteString
, fromConcreteBV
, fromConcreteComplex
) where
import qualified Data.List as List
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import LibBF (BigFloat)
import qualified Numeric as N
import qualified Prettyprinter as PP
import qualified Data.BitVector.Sized as BV
import Data.Parameterized.Classes
import Data.Parameterized.Ctx
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.TH.GADT
import Data.Parameterized.TraversableFC
import What4.BaseTypes
import What4.Utils.Complex
import What4.Utils.StringLiteral
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.BV w ->
ConcreteVal (BaseBVType w)
ConcreteStruct :: Ctx.Assignment ConcreteVal ctx -> ConcreteVal (BaseStructType ctx)
ConcreteArray ::
Ctx.Assignment BaseTypeRepr (idx ::> i) ->
ConcreteVal b ->
Map (Ctx.Assignment ConcreteVal (idx ::> i)) (ConcreteVal b) ->
ConcreteVal (BaseArrayType (idx ::> i) b)
deriving instance ShowF ConcreteVal
deriving instance Show (ConcreteVal tp)
fromConcreteBool :: ConcreteVal BaseBoolType -> Bool
fromConcreteBool :: ConcreteVal 'BaseBoolType -> Bool
fromConcreteBool (ConcreteBool Bool
x) = Bool
x
fromConcreteInteger :: ConcreteVal BaseIntegerType -> Integer
fromConcreteInteger :: ConcreteVal 'BaseIntegerType -> Integer
fromConcreteInteger (ConcreteInteger Integer
x) = Integer
x
fromConcreteReal :: ConcreteVal BaseRealType -> Rational
fromConcreteReal :: ConcreteVal 'BaseRealType -> Rational
fromConcreteReal (ConcreteReal Rational
x) = Rational
x
fromConcreteComplex :: ConcreteVal BaseComplexType -> Complex Rational
fromConcreteComplex :: ConcreteVal 'BaseComplexType -> Complex Rational
fromConcreteComplex (ConcreteComplex Complex Rational
x) = Complex Rational
x
fromConcreteString :: ConcreteVal (BaseStringType si) -> StringLiteral si
fromConcreteString :: forall (si :: StringInfo).
ConcreteVal (BaseStringType si) -> StringLiteral si
fromConcreteString (ConcreteString StringLiteral si
x) = StringLiteral si
x
fromConcreteBV :: ConcreteVal (BaseBVType w) -> BV.BV w
fromConcreteBV :: forall (w :: Natural). ConcreteVal (BaseBVType w) -> BV w
fromConcreteBV (ConcreteBV NatRepr w
_w BV w
x) = BV w
x
concreteType :: ConcreteVal tp -> BaseTypeRepr tp
concreteType :: forall (tp :: BaseType). ConcreteVal tp -> BaseTypeRepr tp
concreteType = \case
ConcreteBool{} -> BaseTypeRepr 'BaseBoolType
BaseBoolRepr
ConcreteInteger{} -> BaseTypeRepr 'BaseIntegerType
BaseIntegerRepr
ConcreteReal{} -> BaseTypeRepr 'BaseRealType
BaseRealRepr
ConcreteFloat FloatPrecisionRepr fpp
fpp BigFloat
_ -> forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr ('BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr fpp
fpp
ConcreteString StringLiteral si
s -> forall (si :: StringInfo).
StringInfoRepr si -> BaseTypeRepr ('BaseStringType si)
BaseStringRepr (forall (si :: StringInfo). StringLiteral si -> StringInfoRepr si
stringLiteralInfo StringLiteral si
s)
ConcreteComplex{} -> BaseTypeRepr 'BaseComplexType
BaseComplexRepr
ConcreteBV NatRepr w
w BV w
_ -> forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w
ConcreteStruct Assignment ConcreteVal ctx
xs -> forall (ctx :: Ctx BaseType).
Assignment BaseTypeRepr ctx -> BaseTypeRepr ('BaseStructType ctx)
BaseStructRepr (forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
fmapFC forall (tp :: BaseType). ConcreteVal tp -> BaseTypeRepr tp
concreteType Assignment ConcreteVal ctx
xs)
ConcreteArray Assignment BaseTypeRepr (idx ::> i)
idxTy ConcreteVal b
def Map (Assignment ConcreteVal (idx ::> i)) (ConcreteVal b)
_ -> forall (idx :: Ctx BaseType) (tp :: BaseType) (xs :: BaseType).
Assignment BaseTypeRepr (idx ::> tp)
-> BaseTypeRepr xs -> BaseTypeRepr ('BaseArrayType (idx ::> tp) xs)
BaseArrayRepr Assignment BaseTypeRepr (idx ::> i)
idxTy (forall (tp :: BaseType). ConcreteVal tp -> BaseTypeRepr tp
concreteType ConcreteVal b
def)
$(return [])
instance TestEquality ConcreteVal where
testEquality :: forall (a :: BaseType) (b :: BaseType).
ConcreteVal a -> ConcreteVal b -> Maybe (a :~: b)
testEquality = $(structuralTypeEquality [t|ConcreteVal|]
[ (ConType [t|NatRepr|] `TypeApp` AnyType, [|testEquality|])
, (ConType [t|Ctx.Assignment|] `TypeApp` AnyType `TypeApp` AnyType, [|testEqualityFC testEquality|])
, (ConType [t|ConcreteVal|] `TypeApp` AnyType, [|testEquality|])
, (ConType [t|StringLiteral|] `TypeApp` AnyType, [|testEquality|])
, (ConType [t|FloatPrecisionRepr|] `TypeApp` AnyType, [|testEquality|])
, (ConType [t|Map|] `TypeApp` AnyType `TypeApp` AnyType, [|\x y -> if x == y then Just Refl else Nothing|])
])
instance Eq (ConcreteVal tp) where
ConcreteVal tp
x== :: ConcreteVal tp -> ConcreteVal tp -> Bool
==ConcreteVal tp
y = forall a. Maybe a -> Bool
isJust (forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality ConcreteVal tp
x ConcreteVal tp
y)
instance OrdF ConcreteVal where
compareF :: forall (x :: BaseType) (y :: BaseType).
ConcreteVal x -> ConcreteVal y -> OrderingF x y
compareF = $(structuralTypeOrd [t|ConcreteVal|]
[ (ConType [t|NatRepr|] `TypeApp` AnyType, [|compareF|])
, (ConType [t|Ctx.Assignment|] `TypeApp` AnyType `TypeApp` AnyType, [|compareFC compareF|])
, (ConType [t|ConcreteVal|] `TypeApp` AnyType, [|compareF|])
, (ConType [t|StringLiteral|] `TypeApp` AnyType, [|compareF|])
, (ConType [t|FloatPrecisionRepr|] `TypeApp` AnyType, [|compareF|])
, (ConType [t|Map|] `TypeApp` AnyType `TypeApp` AnyType, [|\x y -> fromOrdering (compare x y)|])
])
instance Ord (ConcreteVal tp) where
compare :: ConcreteVal tp -> ConcreteVal tp -> Ordering
compare ConcreteVal tp
x ConcreteVal tp
y = forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF ConcreteVal tp
x ConcreteVal tp
y)
ppRational :: Rational -> PP.Doc ann
ppRational :: forall ann. Rational -> Doc ann
ppRational = forall a ann. Show a => a -> Doc ann
PP.viaShow
ppConcrete :: ConcreteVal tp -> PP.Doc ann
ppConcrete :: forall (tp :: BaseType) ann. ConcreteVal tp -> Doc ann
ppConcrete = \case
ConcreteBool Bool
x -> forall a ann. Pretty a => a -> Doc ann
PP.pretty Bool
x
ConcreteInteger Integer
x -> forall a ann. Pretty a => a -> Doc ann
PP.pretty Integer
x
ConcreteReal Rational
x -> forall ann. Rational -> Doc ann
ppRational Rational
x
ConcreteFloat FloatPrecisionRepr fpp
_fpp BigFloat
bf -> forall a ann. Show a => a -> Doc ann
PP.viaShow BigFloat
bf
ConcreteString StringLiteral si
x -> forall a ann. Show a => a -> Doc ann
PP.viaShow StringLiteral si
x
ConcreteBV NatRepr w
w BV w
x -> forall a ann. Pretty a => a -> Doc ann
PP.pretty (String
"0x" forall a. [a] -> [a] -> [a]
++ (forall a. (Integral a, Show a) => a -> String -> String
N.showHex (forall (w :: Natural). BV w -> Integer
BV.asUnsigned BV w
x) (String
":[" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show NatRepr w
w forall a. [a] -> [a] -> [a]
++ String
"]")))
ConcreteComplex (Rational
r :+ Rational
i) -> forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"complex(" forall a. Semigroup a => a -> a -> a
PP.<> forall ann. Rational -> Doc ann
ppRational Rational
r forall a. Semigroup a => a -> a -> a
PP.<> forall a ann. Pretty a => a -> Doc ann
PP.pretty String
", " forall a. Semigroup a => a -> a -> a
PP.<> forall ann. Rational -> Doc ann
ppRational Rational
i forall a. Semigroup a => a -> a -> a
PP.<> forall a ann. Pretty a => a -> Doc ann
PP.pretty String
")"
ConcreteStruct Assignment ConcreteVal ctx
xs -> forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"struct(" forall a. Semigroup a => a -> a -> a
PP.<> forall ann. [Doc ann] -> Doc ann
PP.cat (forall a. a -> [a] -> [a]
List.intersperse forall ann. Doc ann
PP.comma (forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
toListFC forall (tp :: BaseType) ann. ConcreteVal tp -> Doc ann
ppConcrete Assignment ConcreteVal ctx
xs)) forall a. Semigroup a => a -> a -> a
PP.<> forall a ann. Pretty a => a -> Doc ann
PP.pretty String
")"
ConcreteArray Assignment BaseTypeRepr (idx ::> i)
_ ConcreteVal b
def Map (Assignment ConcreteVal (idx ::> i)) (ConcreteVal b)
xs0 -> forall {l} {t :: (BaseType -> Type) -> l -> Type} {x :: l}
{tp :: BaseType} {ann}.
FoldableFC t =>
[(t ConcreteVal x, ConcreteVal tp)] -> Doc ann -> Doc ann
go (forall k a. Map k a -> [(k, a)]
Map.toAscList Map (Assignment ConcreteVal (idx ::> i)) (ConcreteVal b)
xs0) (forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"constArray(" forall a. Semigroup a => a -> a -> a
PP.<> forall (tp :: BaseType) ann. ConcreteVal tp -> Doc ann
ppConcrete ConcreteVal b
def forall a. Semigroup a => a -> a -> a
PP.<> forall a ann. Pretty a => a -> Doc ann
PP.pretty String
")")
where
go :: [(t ConcreteVal x, ConcreteVal tp)] -> Doc ann -> Doc ann
go [] Doc ann
doc = Doc ann
doc
go ((t ConcreteVal x
i,ConcreteVal tp
x):[(t ConcreteVal x, ConcreteVal tp)]
xs) Doc ann
doc = forall {l} {t :: (BaseType -> Type) -> l -> Type} {x :: l}
{tp :: BaseType} {ann}.
FoldableFC t =>
t ConcreteVal x -> ConcreteVal tp -> Doc ann -> Doc ann
ppUpd t ConcreteVal x
i ConcreteVal tp
x ([(t ConcreteVal x, ConcreteVal tp)] -> Doc ann -> Doc ann
go [(t ConcreteVal x, ConcreteVal tp)]
xs Doc ann
doc)
ppUpd :: t ConcreteVal x -> ConcreteVal tp -> Doc ann -> Doc ann
ppUpd t ConcreteVal x
i ConcreteVal tp
x Doc ann
doc =
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"update(" forall a. Semigroup a => a -> a -> a
PP.<> forall ann. [Doc ann] -> Doc ann
PP.cat (forall a. a -> [a] -> [a]
List.intersperse forall ann. Doc ann
PP.comma (forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
toListFC forall (tp :: BaseType) ann. ConcreteVal tp -> Doc ann
ppConcrete t ConcreteVal x
i))
forall a. Semigroup a => a -> a -> a
PP.<> forall ann. Doc ann
PP.comma
forall a. Semigroup a => a -> a -> a
PP.<> forall (tp :: BaseType) ann. ConcreteVal tp -> Doc ann
ppConcrete ConcreteVal tp
x
forall a. Semigroup a => a -> a -> a
PP.<> forall ann. Doc ann
PP.comma
forall a. Semigroup a => a -> a -> a
PP.<> Doc ann
doc
forall a. Semigroup a => a -> a -> a
PP.<> forall a ann. Pretty a => a -> Doc ann
PP.pretty String
")"