{-# 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, assetClass, assetClassValue, assetClassValueOf, flattenValue, 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 Data.Maybe

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, Typeable SymValue
DataType
Constr
Typeable SymValue
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> SymValue -> c SymValue)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SymValue)
-> (SymValue -> Constr)
-> (SymValue -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SymValue))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymValue))
-> ((forall b. Data b => b -> b) -> SymValue -> SymValue)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SymValue -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SymValue -> r)
-> (forall u. (forall d. Data d => d -> u) -> SymValue -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> SymValue -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SymValue -> m SymValue)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SymValue -> m SymValue)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SymValue -> m SymValue)
-> Data SymValue
SymValue -> DataType
SymValue -> Constr
(forall b. Data b => b -> b) -> SymValue -> SymValue
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymValue -> c SymValue
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymValue
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) -> SymValue -> u
forall u. (forall d. Data d => d -> u) -> SymValue -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SymValue -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SymValue -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SymValue -> m SymValue
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymValue -> m SymValue
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymValue
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymValue -> c SymValue
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SymValue)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymValue)
$cSymValue :: Constr
$tSymValue :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> SymValue -> m SymValue
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymValue -> m SymValue
gmapMp :: (forall d. Data d => d -> m d) -> SymValue -> m SymValue
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymValue -> m SymValue
gmapM :: (forall d. Data d => d -> m d) -> SymValue -> m SymValue
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SymValue -> m SymValue
gmapQi :: Int -> (forall d. Data d => d -> u) -> SymValue -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SymValue -> u
gmapQ :: (forall d. Data d => d -> u) -> SymValue -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SymValue -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SymValue -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SymValue -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SymValue -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SymValue -> r
gmapT :: (forall b. Data b => b -> b) -> SymValue -> SymValue
$cgmapT :: (forall b. Data b => b -> b) -> SymValue -> SymValue
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymValue)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymValue)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c SymValue)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SymValue)
dataTypeOf :: SymValue -> DataType
$cdataTypeOf :: SymValue -> DataType
toConstr :: SymValue -> Constr
$ctoConstr :: SymValue -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymValue
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymValue
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymValue -> c SymValue
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymValue -> c SymValue
$cp1Data :: Typeable SymValue
Data)

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 ]

-- | Invert a sym token mapping to turn a Value into a SymValue,
-- useful for error reporting
toSymVal :: (AssetClass -> Maybe SymToken) -> Value -> SymValue
toSymVal :: (AssetClass -> Maybe SymToken) -> Value -> SymValue
toSymVal AssetClass -> Maybe SymToken
invSymTokenMap Value
v =
  let acMap :: [(AssetClass, Integer)]
acMap = [ (CurrencySymbol -> TokenName -> AssetClass
assetClass CurrencySymbol
cs TokenName
tn, Integer
i) | (CurrencySymbol
cs, TokenName
tn, Integer
i) <- Value -> [(CurrencySymbol, TokenName, Integer)]
flattenValue Value
v ]
  in Map SymToken Integer -> Value -> SymValue
SymValue ([(SymToken, Integer)] -> Map SymToken Integer
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (SymToken
tn, Integer
i) | (AssetClass
ac, Integer
i) <- [(AssetClass, Integer)]
acMap, SymToken
tn <- Maybe SymToken -> [SymToken]
forall a. Maybe a -> [a]
maybeToList (Maybe SymToken -> [SymToken]) -> Maybe SymToken -> [SymToken]
forall a b. (a -> b) -> a -> b
$ AssetClass -> Maybe SymToken
invSymTokenMap AssetClass
ac ])
              ([Value] -> Value
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold [ AssetClass -> Integer -> Value
assetClassValue AssetClass
ac Integer
i | (AssetClass
ac, Integer
i) <- [(AssetClass, Integer)]
acMap, AssetClass -> Maybe SymToken
invSymTokenMap AssetClass
ac Maybe SymToken -> Maybe SymToken -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe SymToken
forall a. Maybe a
Nothing ])

-- 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`
  symAssetIdValueOf :: SymValue -> t -> Integer
  -- | Convert a token and an amount to a `SymValue`
  symAssetIdValue :: 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
  symAssetIdValueOf :: SymValue -> SymToken -> Integer
symAssetIdValueOf (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

  symAssetIdValue :: SymToken -> Integer -> SymValue
symAssetIdValue 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
  symAssetIdValue 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
  symAssetIdValueOf :: SymValue -> AssetClass -> Integer
symAssetIdValueOf (SymValue Map SymToken Integer
_ Value
v) AssetClass
t = Value -> AssetClass -> Integer
assetClassValueOf Value
v AssetClass
t
  symAssetIdValue :: AssetClass -> Integer -> SymValue
symAssetIdValue 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