    -----------------------------------------------------------------------
    -- |
    -- 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
    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
    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 tp
    BaseTypeRepr 'BaseBoolType
    BaseBoolRepr
      ConcreteInteger{}         -> BaseTypeRepr tp
    BaseTypeRepr 'BaseIntegerType
    BaseIntegerRepr
      ConcreteReal{}            -> BaseTypeRepr tp
    BaseTypeRepr 'BaseRealType
    BaseRealRepr
      ConcreteFloat FloatPrecisionRepr fpp
    fpp BigFloat
    _       -> FloatPrecisionRepr fpp -> BaseTypeRepr ('BaseFloatType fpp)
    forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp -> BaseTypeRepr ('BaseFloatType fpp)
    BaseFloatRepr FloatPrecisionRepr fpp
    fpp
      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 :: Natural).
    (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 (tp :: BaseType). ConcreteVal tp -> BaseTypeRepr tp)
    -> forall (x :: Ctx BaseType).
       Assignment ConcreteVal x -> Assignment BaseTypeRepr x
    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
    forall (f :: BaseType -> Type) (g :: BaseType -> Type).
    (forall (x :: BaseType). f x -> g x)
    -> forall (x :: Ctx BaseType). Assignment f x -> Assignment g x
    fmapFC ConcreteVal x -> BaseTypeRepr x
    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)
    _ -> 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 (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 = 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)
    forall (a :: BaseType) (b :: BaseType).
    ConcreteVal a -> ConcreteVal 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 = 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
    forall (x :: BaseType) (y :: BaseType).
    ConcreteVal x -> ConcreteVal 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 = 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 :: forall (tp :: BaseType) ann. ConcreteVal tp -> Doc ann
    ppConcrete = \case
      ConcreteBool Bool
    x -> Bool -> Doc ann
    forall ann. Bool -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    PP.pretty Bool
    x
      ConcreteInteger Integer
    x -> Integer -> Doc ann
    forall ann. 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
      ConcreteFloat FloatPrecisionRepr fpp
    _fpp BigFloat
    bf -> BigFloat -> Doc ann
    forall a ann. Show a => a -> Doc ann
    PP.viaShow BigFloat
    bf
      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 ann. 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 => a -> String -> String
    N.showHex (BV w -> Integer
    forall (w :: Natural). 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 ann. 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 ann. 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 ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    PP.pretty String
    ")"
      ConcreteStruct Assignment ConcreteVal ctx
    xs -> String -> Doc ann
    forall ann. 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]
    List.intersperse Doc ann
    forall ann. Doc ann
    PP.comma ((forall (x :: BaseType). ConcreteVal x -> Doc ann)
    -> forall (x :: Ctx BaseType).
       Assignment 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]
    forall (f :: BaseType -> Type) a.
    (forall (x :: BaseType). f x -> a)
    -> forall (x :: Ctx BaseType). Assignment f x -> [a]
    toListFC ConcreteVal x -> Doc ann
    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 ann. 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 ann. 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 ann. 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 ann. 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]
    List.intersperse Doc ann
    forall ann. Doc ann
    PP.comma ((forall (x :: BaseType). ConcreteVal x -> Doc ann)
    -> forall (x :: l). 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]
    forall (f :: BaseType -> Type) a.
    (forall (x :: BaseType). f x -> a) -> forall (x :: l). t f x -> [a]
    toListFC ConcreteVal x -> Doc ann
    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 ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    PP.pretty String
    ")"