-----------------------------------------------------------------------
-- |
-- Module           : What4.Concrete
-- Description      : Concrete values of base types
-- Copyright        : (c) Galois, Inc 2018-2020
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
--
-- 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.
-----------------------------------------------------------------------

{-# 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
  (
    -- * Concrete values
    ConcreteVal(..)
  , concreteType
  , ppConcrete

    -- * Concrete projections
  , fromConcreteBool
  , fromConcreteInteger
  , fromConcreteReal
  , fromConcreteString
  , fromConcreteBV
  , fromConcreteComplex
  ) where

import           Data.List
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
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

-- | A data type for representing the concrete values of base types.
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 {- Width of the bitvector -} ->
    BV.BV w   {- Unsigned value of the bitvector -} ->
    ConcreteVal (BaseBVType w)
  ConcreteStruct  :: Ctx.Assignment ConcreteVal ctx -> ConcreteVal (BaseStructType ctx)
  ConcreteArray   ::
    Ctx.Assignment BaseTypeRepr (idx ::> i) {- Type representatives for the index tuple -} ->
    ConcreteVal b {- A default value -} ->
    Map (Ctx.Assignment ConcreteVal (idx ::> i)) (ConcreteVal b) {- A collection of point-updates -} ->
    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 :: ConcreteVal (BaseStringType si) -> StringLiteral si
fromConcreteString (ConcreteString StringLiteral si
x) = StringLiteral si
StringLiteral si
x

fromConcreteBV :: ConcreteVal (BaseBVType w) -> BV.BV w
fromConcreteBV :: ConcreteVal (BaseBVType w) -> BV w
fromConcreteBV (ConcreteBV NatRepr w
_w BV w
x) = BV w
BV w
x

-- | Compute the type representative for a concrete value.
concreteType :: ConcreteVal tp -> BaseTypeRepr tp
concreteType :: ConcreteVal tp -> BaseTypeRepr tp
concreteType = \case
  ConcreteBool{}     -> BaseTypeRepr tp
BaseTypeRepr BaseBoolType
BaseBoolRepr
  ConcreteInteger{}  -> BaseTypeRepr tp
BaseTypeRepr BaseIntegerType
BaseIntegerRepr
  ConcreteReal{}     -> BaseTypeRepr tp
BaseTypeRepr BaseRealType
BaseRealRepr
  ConcreteString StringLiteral si
s   -> StringInfoRepr si -> BaseTypeRepr (BaseStringType si)
forall (si :: StringInfo).
StringInfoRepr si -> BaseTypeRepr (BaseStringType si)
BaseStringRepr (StringLiteral si -> StringInfoRepr si
forall (si :: StringInfo). StringLiteral si -> StringInfoRepr si
stringLiteralInfo StringLiteral si
s)
  ConcreteComplex{}  -> BaseTypeRepr tp
BaseTypeRepr BaseComplexType
BaseComplexRepr
  ConcreteBV NatRepr w
w BV w
_     -> NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr NatRepr w
w
  ConcreteStruct Assignment ConcreteVal ctx
xs  -> Assignment BaseTypeRepr ctx -> BaseTypeRepr (BaseStructType ctx)
forall (ctx :: Ctx BaseType).
Assignment BaseTypeRepr ctx -> BaseTypeRepr (BaseStructType ctx)
BaseStructRepr ((forall (x :: BaseType). ConcreteVal x -> BaseTypeRepr x)
-> Assignment ConcreteVal ctx -> Assignment BaseTypeRepr ctx
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 (x :: BaseType). ConcreteVal x -> BaseTypeRepr x
concreteType Assignment ConcreteVal ctx
xs)
  ConcreteArray Assignment BaseTypeRepr (idx ::> i)
idxTy ConcreteVal b
def Map (Assignment ConcreteVal (idx ::> i)) (ConcreteVal b)
_ -> Assignment BaseTypeRepr (idx ::> i)
-> BaseTypeRepr b -> BaseTypeRepr (BaseArrayType (idx ::> i) 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 (ConcreteVal b -> BaseTypeRepr b
forall (x :: BaseType). ConcreteVal x -> BaseTypeRepr x
concreteType ConcreteVal b
def)

$(return [])

instance TestEquality ConcreteVal where
  testEquality :: 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|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 = Maybe (tp :~: tp) -> Bool
forall a. Maybe a -> Bool
isJust (ConcreteVal tp -> ConcreteVal tp -> Maybe (tp :~: tp)
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 :: 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|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 = OrderingF tp tp -> Ordering
forall k (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (ConcreteVal tp -> ConcreteVal tp -> OrderingF tp tp
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)

-- | Pretty-print a rational number.
ppRational :: Rational -> PP.Doc ann
ppRational :: Rational -> Doc ann
ppRational = Rational -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow

-- | Pretty-print a concrete value
ppConcrete :: ConcreteVal tp -> PP.Doc ann
ppConcrete :: ConcreteVal tp -> Doc ann
ppConcrete = \case
  ConcreteBool Bool
x -> Bool -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty Bool
x
  ConcreteInteger Integer
x -> Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty Integer
x
  ConcreteReal Rational
x -> Rational -> Doc ann
forall ann. Rational -> Doc ann
ppRational Rational
x
  ConcreteString StringLiteral si
x -> StringLiteral si -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow StringLiteral si
x
  ConcreteBV NatRepr w
w BV w
x -> String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (String
"0x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Integer -> String -> String
forall a. (Integral a, Show a) => a -> String -> String
N.showHex (BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
x) (String
":[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NatRepr w -> String
forall a. Show a => a -> String
show NatRepr w
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]")))
  ConcreteComplex (Rational
r :+ Rational
i) -> String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"complex(" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Rational -> Doc ann
forall ann. Rational -> Doc ann
ppRational Rational
r Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
", " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Rational -> Doc ann
forall ann. Rational -> Doc ann
ppRational Rational
i Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
")"
  ConcreteStruct Assignment ConcreteVal ctx
xs -> String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"struct(" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.cat (Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
intersperse Doc ann
forall ann. Doc ann
PP.comma ((forall (x :: BaseType). ConcreteVal x -> Doc ann)
-> Assignment ConcreteVal ctx -> [Doc ann]
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 (x :: BaseType). ConcreteVal x -> Doc ann
forall (tp :: BaseType) ann. ConcreteVal tp -> Doc ann
ppConcrete Assignment ConcreteVal ctx
xs)) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> String -> Doc ann
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 -> [(Assignment ConcreteVal (idx ::> i), ConcreteVal b)]
-> Doc ann -> Doc ann
forall l (t :: (BaseType -> Type) -> l -> Type) (x :: l)
       (tp :: BaseType) ann.
FoldableFC t =>
[(t ConcreteVal x, ConcreteVal tp)] -> Doc ann -> Doc ann
go (Map (Assignment ConcreteVal (idx ::> i)) (ConcreteVal b)
-> [(Assignment ConcreteVal (idx ::> i), ConcreteVal b)]
forall k a. Map k a -> [(k, a)]
Map.toAscList Map (Assignment ConcreteVal (idx ::> i)) (ConcreteVal b)
xs0) (String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"constArray(" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> ConcreteVal b -> Doc ann
forall (tp :: BaseType) ann. ConcreteVal tp -> Doc ann
ppConcrete ConcreteVal b
def Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> String -> Doc ann
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 = t ConcreteVal x -> ConcreteVal tp -> Doc ann -> Doc ann
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 =
       String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"update(" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.cat (Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
intersperse Doc ann
forall ann. Doc ann
PP.comma ((forall (x :: BaseType). ConcreteVal x -> Doc ann)
-> t ConcreteVal x -> [Doc ann]
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 (x :: BaseType). ConcreteVal x -> Doc ann
forall (tp :: BaseType) ann. ConcreteVal tp -> Doc ann
ppConcrete t ConcreteVal x
i))
                         Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Doc ann
forall ann. Doc ann
PP.comma
                         Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> ConcreteVal tp -> Doc ann
forall (tp :: BaseType) ann. ConcreteVal tp -> Doc ann
ppConcrete ConcreteVal tp
x
                         Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Doc ann
forall ann. Doc ann
PP.comma
                         Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Doc ann
doc
                         Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
")"