{-# LANGUAGE DeriveDataTypeable #-}
{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
module Plutus.Contract.Test.ContractModel.Symbolics where

import Ledger.Ada qualified as Ada
import Ledger.Value (AssetClass, Value, assetClassValue, assetClassValueOf, isZero, leq)
import PlutusTx.Monoid qualified as PlutusTx

import Data.Aeson qualified as JSON
import Data.Data
import Data.Foldable
import Data.Map (Map)
import Data.Map qualified as Map

import Test.QuickCheck.StateModel hiding (Action, Actions, arbitraryAction, initialState, monitoring, nextState,
                                   perform, precondition, shrinkAction, stateAfter)

{- Note [Symbolic Tokens and Symbolic Values]
  Symbolic tokens represent tokens that are created during runtime of a `ContractModel` test.
  It is important that these tokens are *symbolic* as there needs to be a phase-separation
  between the generation and execution part of a `ContractModel` test in order to ensure that
  failing test cases can be shrunk - which is crucial for debugging.

  An important invariant of symbolic values is that different symbolic tokens represent
  different actual tokens. This is enforced by a uniqueness check in the `ContractModel`
  tests.

  A symbolic token is a Var Int. You might expect it to be a Var [AssetClass] but because the
  execution of test code is split between two monads we end up needing two indirections.

  See Note [The Env contract] on how to get the meaning of the symbolic tokens out of the
  inner monad.
-}

newtype AssetKey = AssetKey Int deriving (Eq AssetKey
Eq AssetKey
-> (AssetKey -> AssetKey -> Ordering)
-> (AssetKey -> AssetKey -> Bool)
-> (AssetKey -> AssetKey -> Bool)
-> (AssetKey -> AssetKey -> Bool)
-> (AssetKey -> AssetKey -> Bool)
-> (AssetKey -> AssetKey -> AssetKey)
-> (AssetKey -> AssetKey -> AssetKey)
-> Ord AssetKey
AssetKey -> AssetKey -> Bool
AssetKey -> AssetKey -> Ordering
AssetKey -> AssetKey -> AssetKey
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: AssetKey -> AssetKey -> AssetKey
$cmin :: AssetKey -> AssetKey -> AssetKey
max :: AssetKey -> AssetKey -> AssetKey
$cmax :: AssetKey -> AssetKey -> AssetKey
>= :: AssetKey -> AssetKey -> Bool
$c>= :: AssetKey -> AssetKey -> Bool
> :: AssetKey -> AssetKey -> Bool
$c> :: AssetKey -> AssetKey -> Bool
<= :: AssetKey -> AssetKey -> Bool
$c<= :: AssetKey -> AssetKey -> Bool
< :: AssetKey -> AssetKey -> Bool
$c< :: AssetKey -> AssetKey -> Bool
compare :: AssetKey -> AssetKey -> Ordering
$ccompare :: AssetKey -> AssetKey -> Ordering
$cp1Ord :: Eq AssetKey
Ord, AssetKey -> AssetKey -> Bool
(AssetKey -> AssetKey -> Bool)
-> (AssetKey -> AssetKey -> Bool) -> Eq AssetKey
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AssetKey -> AssetKey -> Bool
$c/= :: AssetKey -> AssetKey -> Bool
== :: AssetKey -> AssetKey -> Bool
$c== :: AssetKey -> AssetKey -> Bool
Eq, Int -> AssetKey -> ShowS
[AssetKey] -> ShowS
AssetKey -> String
(Int -> AssetKey -> ShowS)
-> (AssetKey -> String) -> ([AssetKey] -> ShowS) -> Show AssetKey
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AssetKey] -> ShowS
$cshowList :: [AssetKey] -> ShowS
show :: AssetKey -> String
$cshow :: AssetKey -> String
showsPrec :: Int -> AssetKey -> ShowS
$cshowsPrec :: Int -> AssetKey -> ShowS
Show, Integer -> AssetKey
AssetKey -> AssetKey
AssetKey -> AssetKey -> AssetKey
(AssetKey -> AssetKey -> AssetKey)
-> (AssetKey -> AssetKey -> AssetKey)
-> (AssetKey -> AssetKey -> AssetKey)
-> (AssetKey -> AssetKey)
-> (AssetKey -> AssetKey)
-> (AssetKey -> AssetKey)
-> (Integer -> AssetKey)
-> Num AssetKey
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> AssetKey
$cfromInteger :: Integer -> AssetKey
signum :: AssetKey -> AssetKey
$csignum :: AssetKey -> AssetKey
abs :: AssetKey -> AssetKey
$cabs :: AssetKey -> AssetKey
negate :: AssetKey -> AssetKey
$cnegate :: AssetKey -> AssetKey
* :: AssetKey -> AssetKey -> AssetKey
$c* :: AssetKey -> AssetKey -> AssetKey
- :: AssetKey -> AssetKey -> AssetKey
$c- :: AssetKey -> AssetKey -> AssetKey
+ :: AssetKey -> AssetKey -> AssetKey
$c+ :: AssetKey -> AssetKey -> AssetKey
Num, FromJSONKeyFunction [AssetKey]
FromJSONKeyFunction AssetKey
FromJSONKeyFunction AssetKey
-> FromJSONKeyFunction [AssetKey] -> FromJSONKey AssetKey
forall a.
FromJSONKeyFunction a -> FromJSONKeyFunction [a] -> FromJSONKey a
fromJSONKeyList :: FromJSONKeyFunction [AssetKey]
$cfromJSONKeyList :: FromJSONKeyFunction [AssetKey]
fromJSONKey :: FromJSONKeyFunction AssetKey
$cfromJSONKey :: FromJSONKeyFunction AssetKey
JSON.FromJSONKey, ToJSONKeyFunction [AssetKey]
ToJSONKeyFunction AssetKey
ToJSONKeyFunction AssetKey
-> ToJSONKeyFunction [AssetKey] -> ToJSONKey AssetKey
forall a.
ToJSONKeyFunction a -> ToJSONKeyFunction [a] -> ToJSONKey a
toJSONKeyList :: ToJSONKeyFunction [AssetKey]
$ctoJSONKeyList :: ToJSONKeyFunction [AssetKey]
toJSONKey :: ToJSONKeyFunction AssetKey
$ctoJSONKey :: ToJSONKeyFunction AssetKey
JSON.ToJSONKey, Typeable AssetKey
DataType
Constr
Typeable AssetKey
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> AssetKey -> c AssetKey)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c AssetKey)
-> (AssetKey -> Constr)
-> (AssetKey -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c AssetKey))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AssetKey))
-> ((forall b. Data b => b -> b) -> AssetKey -> AssetKey)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> AssetKey -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> AssetKey -> r)
-> (forall u. (forall d. Data d => d -> u) -> AssetKey -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> AssetKey -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> AssetKey -> m AssetKey)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> AssetKey -> m AssetKey)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> AssetKey -> m AssetKey)
-> Data AssetKey
AssetKey -> DataType
AssetKey -> Constr
(forall b. Data b => b -> b) -> AssetKey -> AssetKey
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AssetKey -> c AssetKey
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AssetKey
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> AssetKey -> u
forall u. (forall d. Data d => d -> u) -> AssetKey -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AssetKey -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AssetKey -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> AssetKey -> m AssetKey
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AssetKey -> m AssetKey
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AssetKey
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AssetKey -> c AssetKey
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AssetKey)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AssetKey)
$cAssetKey :: Constr
$tAssetKey :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> AssetKey -> m AssetKey
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AssetKey -> m AssetKey
gmapMp :: (forall d. Data d => d -> m d) -> AssetKey -> m AssetKey
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AssetKey -> m AssetKey
gmapM :: (forall d. Data d => d -> m d) -> AssetKey -> m AssetKey
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> AssetKey -> m AssetKey
gmapQi :: Int -> (forall d. Data d => d -> u) -> AssetKey -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> AssetKey -> u
gmapQ :: (forall d. Data d => d -> u) -> AssetKey -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> AssetKey -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AssetKey -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AssetKey -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AssetKey -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AssetKey -> r
gmapT :: (forall b. Data b => b -> b) -> AssetKey -> AssetKey
$cgmapT :: (forall b. Data b => b -> b) -> AssetKey -> AssetKey
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AssetKey)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AssetKey)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c AssetKey)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AssetKey)
dataTypeOf :: AssetKey -> DataType
$cdataTypeOf :: AssetKey -> DataType
toConstr :: AssetKey -> Constr
$ctoConstr :: AssetKey -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AssetKey
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AssetKey
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AssetKey -> c AssetKey
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AssetKey -> c AssetKey
$cp1Data :: Typeable AssetKey
Data)
-- | A symbolic token is a token that exists only during ContractModel generation time
data SymToken = SymToken { SymToken -> Var AssetKey
symVar :: Var AssetKey, SymToken -> String
symVarIdx :: String } deriving (Eq SymToken
Eq SymToken
-> (SymToken -> SymToken -> Ordering)
-> (SymToken -> SymToken -> Bool)
-> (SymToken -> SymToken -> Bool)
-> (SymToken -> SymToken -> Bool)
-> (SymToken -> SymToken -> Bool)
-> (SymToken -> SymToken -> SymToken)
-> (SymToken -> SymToken -> SymToken)
-> Ord SymToken
SymToken -> SymToken -> Bool
SymToken -> SymToken -> Ordering
SymToken -> SymToken -> SymToken
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SymToken -> SymToken -> SymToken
$cmin :: SymToken -> SymToken -> SymToken
max :: SymToken -> SymToken -> SymToken
$cmax :: SymToken -> SymToken -> SymToken
>= :: SymToken -> SymToken -> Bool
$c>= :: SymToken -> SymToken -> Bool
> :: SymToken -> SymToken -> Bool
$c> :: SymToken -> SymToken -> Bool
<= :: SymToken -> SymToken -> Bool
$c<= :: SymToken -> SymToken -> Bool
< :: SymToken -> SymToken -> Bool
$c< :: SymToken -> SymToken -> Bool
compare :: SymToken -> SymToken -> Ordering
$ccompare :: SymToken -> SymToken -> Ordering
$cp1Ord :: Eq SymToken
Ord, SymToken -> SymToken -> Bool
(SymToken -> SymToken -> Bool)
-> (SymToken -> SymToken -> Bool) -> Eq SymToken
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SymToken -> SymToken -> Bool
$c/= :: SymToken -> SymToken -> Bool
== :: SymToken -> SymToken -> Bool
$c== :: SymToken -> SymToken -> Bool
Eq, Typeable SymToken
DataType
Constr
Typeable SymToken
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> SymToken -> c SymToken)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SymToken)
-> (SymToken -> Constr)
-> (SymToken -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SymToken))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymToken))
-> ((forall b. Data b => b -> b) -> SymToken -> SymToken)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SymToken -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SymToken -> r)
-> (forall u. (forall d. Data d => d -> u) -> SymToken -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> SymToken -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SymToken -> m SymToken)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SymToken -> m SymToken)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SymToken -> m SymToken)
-> Data SymToken
SymToken -> DataType
SymToken -> Constr
(forall b. Data b => b -> b) -> SymToken -> SymToken
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymToken -> c SymToken
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymToken
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> SymToken -> u
forall u. (forall d. Data d => d -> u) -> SymToken -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SymToken -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SymToken -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SymToken -> m SymToken
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymToken -> m SymToken
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymToken
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymToken -> c SymToken
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SymToken)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymToken)
$cSymToken :: Constr
$tSymToken :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> SymToken -> m SymToken
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymToken -> m SymToken
gmapMp :: (forall d. Data d => d -> m d) -> SymToken -> m SymToken
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymToken -> m SymToken
gmapM :: (forall d. Data d => d -> m d) -> SymToken -> m SymToken
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SymToken -> m SymToken
gmapQi :: Int -> (forall d. Data d => d -> u) -> SymToken -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SymToken -> u
gmapQ :: (forall d. Data d => d -> u) -> SymToken -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SymToken -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SymToken -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SymToken -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SymToken -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SymToken -> r
gmapT :: (forall b. Data b => b -> b) -> SymToken -> SymToken
$cgmapT :: (forall b. Data b => b -> b) -> SymToken -> SymToken
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymToken)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymToken)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c SymToken)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SymToken)
dataTypeOf :: SymToken -> DataType
$cdataTypeOf :: SymToken -> DataType
toConstr :: SymToken -> Constr
$ctoConstr :: SymToken -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymToken
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymToken
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymToken -> c SymToken
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymToken -> c SymToken
$cp1Data :: Typeable SymToken
Data)
-- | A symbolic value is a combination of a real value and a value associating symbolic
-- tokens with an amount
data SymValue = SymValue { SymValue -> Map SymToken Integer
symValMap :: Map SymToken Integer, SymValue -> Value
actualValPart :: Value } deriving (Int -> SymValue -> ShowS
[SymValue] -> ShowS
SymValue -> String
(Int -> SymValue -> ShowS)
-> (SymValue -> String) -> ([SymValue] -> ShowS) -> Show SymValue
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SymValue] -> ShowS
$cshowList :: [SymValue] -> ShowS
show :: SymValue -> String
$cshow :: SymValue -> String
showsPrec :: Int -> SymValue -> ShowS
$cshowsPrec :: Int -> SymValue -> ShowS
Show)

instance Show SymToken where
  show :: SymToken -> String
show (SymToken (Var Int
i) String
n) = String
"tok" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"." String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
n
instance Semigroup SymValue where
  (SymValue Map SymToken Integer
m Value
v) <> :: SymValue -> SymValue -> SymValue
<> (SymValue Map SymToken Integer
m' Value
v') = Map SymToken Integer -> Value -> SymValue
SymValue ((Integer -> Integer -> Integer)
-> Map SymToken Integer
-> Map SymToken Integer
-> Map SymToken Integer
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) Map SymToken Integer
m Map SymToken Integer
m') (Value
v Value -> Value -> Value
forall a. Semigroup a => a -> a -> a
<> Value
v')
instance Monoid SymValue where
  mempty :: SymValue
mempty = Map SymToken Integer -> Value -> SymValue
SymValue Map SymToken Integer
forall a. Monoid a => a
mempty Value
forall a. Monoid a => a
mempty
instance Eq SymValue where
  (SymValue Map SymToken Integer
m Value
v) == :: SymValue -> SymValue -> Bool
== (SymValue Map SymToken Integer
m' Value
v') = (Integer -> Bool) -> Map SymToken Integer -> Map SymToken Integer
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0) Map SymToken Integer
m Map SymToken Integer -> Map SymToken Integer -> Bool
forall a. Eq a => a -> a -> Bool
== (Integer -> Bool) -> Map SymToken Integer -> Map SymToken Integer
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0) Map SymToken Integer
m'
                                     Bool -> Bool -> Bool
&& Value
v Value -> Value -> Bool
forall a. Eq a => a -> a -> Bool
== Value
v'
-- | Check if a symbolic value is zero
symIsZero :: SymValue -> Bool
symIsZero :: SymValue -> Bool
symIsZero (SymValue Map SymToken Integer
m Value
v) = (Integer -> Bool) -> Map SymToken Integer -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
==Integer
0) Map SymToken Integer
m Bool -> Bool -> Bool
&& Value -> Bool
isZero Value
v

-- | Check if one symbolic value is less than or equal to another
symLeq :: SymValue -> SymValue -> Bool
symLeq :: SymValue -> SymValue -> Bool
symLeq (SymValue Map SymToken Integer
m Value
v) (SymValue Map SymToken Integer
m' Value
v') = Value
v Value -> Value -> Bool
`leq` Value
v' Bool -> Bool -> Bool
&& (Integer -> Bool) -> Map SymToken Integer -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<=Integer
0) ((Integer -> Integer -> Integer)
-> Map SymToken Integer
-> Map SymToken Integer
-> Map SymToken Integer
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) Map SymToken Integer
m (Integer -> Integer
forall a. Num a => a -> a
negate (Integer -> Integer)
-> Map SymToken Integer -> Map SymToken Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map SymToken Integer
m'))

-- | Using a semantics function for symbolic tokens, convert a SymValue to a Value
toValue :: (SymToken -> AssetClass) -> SymValue -> Value
toValue :: (SymToken -> AssetClass) -> SymValue -> Value
toValue SymToken -> AssetClass
symTokenMap (SymValue Map SymToken Integer
m Value
v) = Value
v Value -> Value -> Value
forall a. Semigroup a => a -> a -> a
<> [Value] -> Value
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold [ AssetClass -> Integer -> Value
assetClassValue (SymToken -> AssetClass
symTokenMap SymToken
t) Integer
v | (SymToken
t, Integer
v) <- Map SymToken Integer -> [(SymToken, Integer)]
forall k a. Map k a -> [(k, a)]
Map.toList Map SymToken Integer
m ]

-- Negate a symbolic value
inv :: SymValue -> SymValue
inv :: SymValue -> SymValue
inv (SymValue Map SymToken Integer
m Value
v) = Map SymToken Integer -> Value -> SymValue
SymValue (Integer -> Integer
forall a. Num a => a -> a
negate (Integer -> Integer)
-> Map SymToken Integer -> Map SymToken Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map SymToken Integer
m) (Value -> Value
forall a. Group a => a -> a
PlutusTx.inv Value
v)

class SymValueLike v where
  toSymValue :: v -> SymValue

class TokenLike t where
  -- | Get the value of a specific token in a `SymValue`
  symAssetClassValueOf :: SymValue -> t -> Integer
  -- | Convert a token and an amount to a `SymValue`
  symAssetClassValue :: t -> Integer -> SymValue

instance SymValueLike Value where
  toSymValue :: Value -> SymValue
toSymValue = Map SymToken Integer -> Value -> SymValue
SymValue Map SymToken Integer
forall a. Monoid a => a
mempty

instance SymValueLike SymValue where
  toSymValue :: SymValue -> SymValue
toSymValue = SymValue -> SymValue
forall a. a -> a
id

instance SymValueLike Ada.Ada where
  toSymValue :: Ada -> SymValue
toSymValue = Value -> SymValue
forall v. SymValueLike v => v -> SymValue
toSymValue (Value -> SymValue) -> (Ada -> Value) -> Ada -> SymValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ada -> Value
Ada.toValue

instance TokenLike SymToken where
  symAssetClassValueOf :: SymValue -> SymToken -> Integer
symAssetClassValueOf (SymValue Map SymToken Integer
svm Value
_) SymToken
t = Maybe Integer -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (Maybe Integer -> Integer) -> Maybe Integer -> Integer
forall a b. (a -> b) -> a -> b
$ SymToken -> Map SymToken Integer -> Maybe Integer
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SymToken
t Map SymToken Integer
svm

  symAssetClassValue :: SymToken -> Integer -> SymValue
symAssetClassValue SymToken
_ Integer
0 = Map SymToken Integer -> Value -> SymValue
SymValue Map SymToken Integer
forall a. Monoid a => a
mempty Value
forall a. Monoid a => a
mempty
  symAssetClassValue SymToken
t Integer
i = Map SymToken Integer -> Value -> SymValue
SymValue (SymToken -> Integer -> Map SymToken Integer
forall k a. k -> a -> Map k a
Map.singleton SymToken
t Integer
i) Value
forall a. Monoid a => a
mempty

instance TokenLike AssetClass where
  symAssetClassValueOf :: SymValue -> AssetClass -> Integer
symAssetClassValueOf (SymValue Map SymToken Integer
_ Value
v) AssetClass
t = Value -> AssetClass -> Integer
assetClassValueOf Value
v AssetClass
t
  symAssetClassValue :: AssetClass -> Integer -> SymValue
symAssetClassValue AssetClass
t Integer
i = Value -> SymValue
forall v. SymValueLike v => v -> SymValue
toSymValue (Value -> SymValue) -> Value -> SymValue
forall a b. (a -> b) -> a -> b
$ AssetClass -> Integer -> Value
assetClassValue AssetClass
t Integer
i