-----------------------------------------------------------------------
-- |
-- 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 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

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

-- | Compute the type representative for a concrete value.
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)

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

-- | Pretty-print a concrete value
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
")"