{-# LANGUAGE QuantifiedConstraints #-}
module Michelson.Typed.Value
( Comparability (..)
, Comparable
, ComparabilityScope
, ContractInp1
, ContractInp
, ContractOut1
, ContractOut
, CreateContract (..)
, Operation' (..)
, SetDelegate (..)
, TransferTokens (..)
, Value' (..)
, RemFail (..)
, rfMerge
, rfAnyInstr
, rfMapAnyInstr
, addressToVContract
, buildVContract
, checkComparability
, compileEpLiftSequence
, comparabilityPresence
, getComparableProofS
, liftCallArg
, valueTypeSanity
, withValueTypeSanity
, eqValueExt
) where
import Data.Constraint (Dict(..), (\\))
import Data.Singletons (Sing)
import Data.Type.Bool (type (&&))
import Fmt (Buildable(build), Builder, (+|), (|+))
import GHC.TypeLits (ErrorMessage(..), TypeError)
import Michelson.Text (MText)
import Michelson.Typed.Entrypoints
import Michelson.Typed.Scope
import Michelson.Typed.Sing
import Michelson.Typed.T (T(..))
import Tezos.Address (Address)
import Tezos.Core (ChainId, Mutez, Timestamp)
import Tezos.Crypto (Bls12381Fr, Bls12381G1, Bls12381G2, KeyHash, PublicKey, Signature)
import Util.Sing (eqParamSing, eqParamSing3)
import Util.TH
data Operation' instr where
OpTransferTokens
:: (ParameterScope p)
=> TransferTokens instr p -> Operation' instr
OpSetDelegate :: SetDelegate -> Operation' instr
OpCreateContract
:: ( Show (instr (ContractInp cp st) (ContractOut st))
, NFData (instr (ContractInp cp st) (ContractOut st))
, Typeable instr, ParameterScope cp, StorageScope st)
=> CreateContract instr cp st
-> Operation' instr
instance Buildable (Operation' instr) where
build :: Operation' instr -> Builder
build =
\case
OpTransferTokens TransferTokens instr p
tt -> TransferTokens instr p -> Builder
forall p. Buildable p => p -> Builder
build TransferTokens instr p
tt
OpSetDelegate SetDelegate
sd -> SetDelegate -> Builder
forall p. Buildable p => p -> Builder
build SetDelegate
sd
OpCreateContract CreateContract instr cp st
cc -> CreateContract instr cp st -> Builder
forall p. Buildable p => p -> Builder
build CreateContract instr cp st
cc
deriving stock instance Show (Operation' instr)
instance Eq (Operation' instr) where
Operation' instr
op1 == :: Operation' instr -> Operation' instr -> Bool
== Operation' instr
op2 = case (Operation' instr
op1, Operation' instr
op2) of
(OpTransferTokens TransferTokens instr p
tt1, OpTransferTokens TransferTokens instr p
tt2) -> TransferTokens instr p
tt1 TransferTokens instr p -> TransferTokens instr p -> Bool
forall k (a1 :: k) (a2 :: k) (t :: k -> *).
(SingI a1, SingI a2, SDecide k, Eq (t a1)) =>
t a1 -> t a2 -> Bool
`eqParamSing` TransferTokens instr p
tt2
(OpTransferTokens TransferTokens instr p
_, Operation' instr
_) -> Bool
False
(OpSetDelegate SetDelegate
sd1, OpSetDelegate SetDelegate
sd2) -> SetDelegate
sd1 SetDelegate -> SetDelegate -> Bool
forall a. Eq a => a -> a -> Bool
== SetDelegate
sd2
(OpSetDelegate SetDelegate
_, Operation' instr
_) -> Bool
False
(OpCreateContract CreateContract instr cp st
cc1, OpCreateContract CreateContract instr cp st
cc2) -> CreateContract instr cp st
cc1 CreateContract instr cp st -> CreateContract instr cp st -> Bool
forall k1 k2 k3 (instr1 :: k1) (instr2 :: k1) (a1 :: k2) (a2 :: k2)
(b1 :: k3) (b2 :: k3) (t :: k1 -> k2 -> k3 -> *).
(Typeable instr1, Typeable instr2, SingI a1, SingI a2, SingI b1,
SingI b2, SDecide k2, SDecide k3, Eq (t instr1 a1 b1)) =>
t instr1 a1 b1 -> t instr2 a2 b2 -> Bool
`eqParamSing3` CreateContract instr cp st
cc2
(OpCreateContract CreateContract instr cp st
_, Operation' instr
_) -> Bool
False
data TransferTokens instr p = TransferTokens
{ TransferTokens instr p -> Value' instr p
ttTransferArgument :: Value' instr p
, TransferTokens instr p -> Mutez
ttAmount :: Mutez
, TransferTokens instr p -> Value' instr ('TContract p)
ttContract :: Value' instr ('TContract p)
} deriving stock (Int -> TransferTokens instr p -> ShowS
[TransferTokens instr p] -> ShowS
TransferTokens instr p -> String
(Int -> TransferTokens instr p -> ShowS)
-> (TransferTokens instr p -> String)
-> ([TransferTokens instr p] -> ShowS)
-> Show (TransferTokens instr p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (instr :: [T] -> [T] -> *) (p :: T).
Int -> TransferTokens instr p -> ShowS
forall (instr :: [T] -> [T] -> *) (p :: T).
[TransferTokens instr p] -> ShowS
forall (instr :: [T] -> [T] -> *) (p :: T).
TransferTokens instr p -> String
showList :: [TransferTokens instr p] -> ShowS
$cshowList :: forall (instr :: [T] -> [T] -> *) (p :: T).
[TransferTokens instr p] -> ShowS
show :: TransferTokens instr p -> String
$cshow :: forall (instr :: [T] -> [T] -> *) (p :: T).
TransferTokens instr p -> String
showsPrec :: Int -> TransferTokens instr p -> ShowS
$cshowsPrec :: forall (instr :: [T] -> [T] -> *) (p :: T).
Int -> TransferTokens instr p -> ShowS
Show, TransferTokens instr p -> TransferTokens instr p -> Bool
(TransferTokens instr p -> TransferTokens instr p -> Bool)
-> (TransferTokens instr p -> TransferTokens instr p -> Bool)
-> Eq (TransferTokens instr p)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (instr :: [T] -> [T] -> *) (p :: T).
TransferTokens instr p -> TransferTokens instr p -> Bool
/= :: TransferTokens instr p -> TransferTokens instr p -> Bool
$c/= :: forall (instr :: [T] -> [T] -> *) (p :: T).
TransferTokens instr p -> TransferTokens instr p -> Bool
== :: TransferTokens instr p -> TransferTokens instr p -> Bool
$c== :: forall (instr :: [T] -> [T] -> *) (p :: T).
TransferTokens instr p -> TransferTokens instr p -> Bool
Eq, (forall x.
TransferTokens instr p -> Rep (TransferTokens instr p) x)
-> (forall x.
Rep (TransferTokens instr p) x -> TransferTokens instr p)
-> Generic (TransferTokens instr p)
forall x. Rep (TransferTokens instr p) x -> TransferTokens instr p
forall x. TransferTokens instr p -> Rep (TransferTokens instr p) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (instr :: [T] -> [T] -> *) (p :: T) x.
Rep (TransferTokens instr p) x -> TransferTokens instr p
forall (instr :: [T] -> [T] -> *) (p :: T) x.
TransferTokens instr p -> Rep (TransferTokens instr p) x
$cto :: forall (instr :: [T] -> [T] -> *) (p :: T) x.
Rep (TransferTokens instr p) x -> TransferTokens instr p
$cfrom :: forall (instr :: [T] -> [T] -> *) (p :: T) x.
TransferTokens instr p -> Rep (TransferTokens instr p) x
Generic)
instance NFData (TransferTokens instr p)
instance Buildable (TransferTokens instr p) where
build :: TransferTokens instr p -> Builder
build TransferTokens {Mutez
Value' instr p
Value' instr ('TContract p)
ttContract :: Value' instr ('TContract p)
ttAmount :: Mutez
ttTransferArgument :: Value' instr p
ttContract :: forall (instr :: [T] -> [T] -> *) (p :: T).
TransferTokens instr p -> Value' instr ('TContract p)
ttAmount :: forall (instr :: [T] -> [T] -> *) (p :: T).
TransferTokens instr p -> Mutez
ttTransferArgument :: forall (instr :: [T] -> [T] -> *) (p :: T).
TransferTokens instr p -> Value' instr p
..} =
Builder
"Transfer " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Mutez
ttAmount Mutez -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
" tokens to " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Value' instr ('TContract p) -> Builder
forall (instr :: [T] -> [T] -> *) (arg :: T).
Value' instr ('TContract arg) -> Builder
buildVContract Value' instr ('TContract p)
ttContract Builder -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
""
data SetDelegate = SetDelegate
{ SetDelegate -> Maybe KeyHash
sdMbKeyHash :: Maybe KeyHash
} deriving stock (Int -> SetDelegate -> ShowS
[SetDelegate] -> ShowS
SetDelegate -> String
(Int -> SetDelegate -> ShowS)
-> (SetDelegate -> String)
-> ([SetDelegate] -> ShowS)
-> Show SetDelegate
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SetDelegate] -> ShowS
$cshowList :: [SetDelegate] -> ShowS
show :: SetDelegate -> String
$cshow :: SetDelegate -> String
showsPrec :: Int -> SetDelegate -> ShowS
$cshowsPrec :: Int -> SetDelegate -> ShowS
Show, SetDelegate -> SetDelegate -> Bool
(SetDelegate -> SetDelegate -> Bool)
-> (SetDelegate -> SetDelegate -> Bool) -> Eq SetDelegate
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SetDelegate -> SetDelegate -> Bool
$c/= :: SetDelegate -> SetDelegate -> Bool
== :: SetDelegate -> SetDelegate -> Bool
$c== :: SetDelegate -> SetDelegate -> Bool
Eq, (forall x. SetDelegate -> Rep SetDelegate x)
-> (forall x. Rep SetDelegate x -> SetDelegate)
-> Generic SetDelegate
forall x. Rep SetDelegate x -> SetDelegate
forall x. SetDelegate -> Rep SetDelegate x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SetDelegate x -> SetDelegate
$cfrom :: forall x. SetDelegate -> Rep SetDelegate x
Generic)
instance NFData SetDelegate
instance Buildable SetDelegate where
build :: SetDelegate -> Builder
build (SetDelegate Maybe KeyHash
mbDelegate) =
Builder
"Set delegate to " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder -> (KeyHash -> Builder) -> Maybe KeyHash -> Builder
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Builder
"<nobody>" KeyHash -> Builder
forall p. Buildable p => p -> Builder
build Maybe KeyHash
mbDelegate
data CreateContract instr cp st
= ( Show (instr (ContractInp cp st) (ContractOut st))
, Eq (instr (ContractInp cp st) (ContractOut st))
)
=> CreateContract
{ CreateContract instr cp st -> Address
ccOriginator :: Address
, CreateContract instr cp st -> Maybe KeyHash
ccDelegate :: Maybe KeyHash
, CreateContract instr cp st -> Mutez
ccBalance :: Mutez
, CreateContract instr cp st -> Value' instr st
ccStorageVal :: Value' instr st
, CreateContract instr cp st
-> instr (ContractInp cp st) (ContractOut st)
ccContractCode :: instr (ContractInp cp st) (ContractOut st)
}
instance NFData (instr (ContractInp cp st) (ContractOut st)) => NFData (CreateContract instr cp st) where
rnf :: CreateContract instr cp st -> ()
rnf (CreateContract Address
a Maybe KeyHash
b Mutez
c Value' instr st
d instr (ContractInp cp st) (ContractOut st)
e) = (Address, Maybe KeyHash, Mutez, Value' instr st,
instr (ContractInp cp st) (ContractOut st))
-> ()
forall a. NFData a => a -> ()
rnf (Address
a, Maybe KeyHash
b, Mutez
c, Value' instr st
d, instr (ContractInp cp st) (ContractOut st)
e)
instance Buildable (CreateContract instr cp st) where
build :: CreateContract instr cp st -> Builder
build CreateContract {instr (ContractInp cp st) (ContractOut st)
Maybe KeyHash
Mutez
Address
Value' instr st
ccContractCode :: instr (ContractInp cp st) (ContractOut st)
ccStorageVal :: Value' instr st
ccBalance :: Mutez
ccDelegate :: Maybe KeyHash
ccOriginator :: Address
ccContractCode :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
CreateContract instr cp st
-> instr (ContractInp cp st) (ContractOut st)
ccStorageVal :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
CreateContract instr cp st -> Value' instr st
ccBalance :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
CreateContract instr cp st -> Mutez
ccDelegate :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
CreateContract instr cp st -> Maybe KeyHash
ccOriginator :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
CreateContract instr cp st -> Address
..} =
Builder
"Create a new contract with" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
Builder
" delegate " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Builder -> (KeyHash -> Builder) -> Maybe KeyHash -> Builder
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Builder
"<nobody>" KeyHash -> Builder
forall p. Buildable p => p -> Builder
build Maybe KeyHash
ccDelegate Builder -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+
Builder
" and balance = " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Mutez
ccBalance Mutez -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
""
deriving stock instance Show (CreateContract instr cp st)
deriving stock instance Eq (CreateContract instr cp st)
type ContractInp1 param st = 'TPair param st
type ContractInp param st = '[ ContractInp1 param st ]
type ContractOut1 st = 'TPair ('TList 'TOperation) st
type ContractOut st = '[ ContractOut1 st ]
data RemFail (instr :: k -> k -> Type) (i :: k) (o :: k) where
RfNormal :: instr i o -> RemFail instr i o
RfAlwaysFails :: (forall o'. instr i o') -> RemFail instr i o
deriving stock instance (forall o'. Show (instr i o')) => Show (RemFail instr i o)
instance (forall o'. NFData (instr i o')) => NFData (RemFail instr i o) where
rnf :: RemFail instr i o -> ()
rnf (RfNormal instr i o
a) = instr i o -> ()
forall a. NFData a => a -> ()
rnf instr i o
a
rnf (RfAlwaysFails forall (o' :: k). instr i o'
a) = instr i Any -> ()
forall a. NFData a => a -> ()
rnf instr i Any
forall (o' :: k). instr i o'
a
instance Eq (instr i o) => Eq (RemFail instr i o) where
RfNormal instr i o
i1 == :: RemFail instr i o -> RemFail instr i o -> Bool
== RfNormal instr i o
i2 = instr i o
i1 instr i o -> instr i o -> Bool
forall a. Eq a => a -> a -> Bool
== instr i o
i2
RfAlwaysFails forall (o' :: k). instr i o'
i1 == RfNormal instr i o
i2 = instr i o
forall (o' :: k). instr i o'
i1 instr i o -> instr i o -> Bool
forall a. Eq a => a -> a -> Bool
== instr i o
i2
RfNormal instr i o
i1 == RfAlwaysFails forall (o' :: k). instr i o'
i2 = instr i o
i1 instr i o -> instr i o -> Bool
forall a. Eq a => a -> a -> Bool
== instr i o
forall (o' :: k). instr i o'
i2
RfAlwaysFails forall (o' :: k). instr i o'
i1 == RfAlwaysFails forall (o' :: k). instr i o'
i2 = instr i o
forall (o' :: k). instr i o'
i1 @o instr i o -> instr i o -> Bool
forall a. Eq a => a -> a -> Bool
== instr i o
forall (o' :: k). instr i o'
i2
rfMerge
:: (forall o'. instr i1 o' -> instr i2 o' -> instr i3 o')
-> RemFail instr i1 o -> RemFail instr i2 o -> RemFail instr i3 o
rfMerge :: (forall (o' :: k). instr i1 o' -> instr i2 o' -> instr i3 o')
-> RemFail instr i1 o -> RemFail instr i2 o -> RemFail instr i3 o
rfMerge forall (o' :: k). instr i1 o' -> instr i2 o' -> instr i3 o'
merger RemFail instr i1 o
instr1 RemFail instr i2 o
instr2 = case (RemFail instr i1 o
instr1, RemFail instr i2 o
instr2) of
(RfNormal instr i1 o
i1, RfNormal instr i2 o
i2) -> instr i3 o -> RemFail instr i3 o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal (instr i1 o -> instr i2 o -> instr i3 o
forall (o' :: k). instr i1 o' -> instr i2 o' -> instr i3 o'
merger instr i1 o
i1 instr i2 o
i2)
(RfAlwaysFails forall (o' :: k). instr i1 o'
i1, RfNormal instr i2 o
i2) -> instr i3 o -> RemFail instr i3 o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal (instr i1 o -> instr i2 o -> instr i3 o
forall (o' :: k). instr i1 o' -> instr i2 o' -> instr i3 o'
merger instr i1 o
forall (o' :: k). instr i1 o'
i1 instr i2 o
i2)
(RfNormal instr i1 o
i1, RfAlwaysFails forall (o' :: k). instr i2 o'
i2) -> instr i3 o -> RemFail instr i3 o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal (instr i1 o -> instr i2 o -> instr i3 o
forall (o' :: k). instr i1 o' -> instr i2 o' -> instr i3 o'
merger instr i1 o
i1 instr i2 o
forall (o' :: k). instr i2 o'
i2)
(RfAlwaysFails forall (o' :: k). instr i1 o'
i1, RfAlwaysFails forall (o' :: k). instr i2 o'
i2) -> (forall (o' :: k). instr i3 o') -> RemFail instr i3 o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
(forall (o' :: k). instr i o') -> RemFail instr i o
RfAlwaysFails (instr i1 o' -> instr i2 o' -> instr i3 o'
forall (o' :: k). instr i1 o' -> instr i2 o' -> instr i3 o'
merger instr i1 o'
forall (o' :: k). instr i1 o'
i1 instr i2 o'
forall (o' :: k). instr i2 o'
i2)
rfAnyInstr :: RemFail instr i o -> instr i o
rfAnyInstr :: RemFail instr i o -> instr i o
rfAnyInstr = \case
RfNormal instr i o
i -> instr i o
i
RfAlwaysFails forall (o' :: k). instr i o'
i -> instr i o
forall (o' :: k). instr i o'
i
rfMapAnyInstr
:: (forall o'. instr i1 o' -> instr i2 o')
-> RemFail instr i1 o
-> RemFail instr i2 o
rfMapAnyInstr :: (forall (o' :: k). instr i1 o' -> instr i2 o')
-> RemFail instr i1 o -> RemFail instr i2 o
rfMapAnyInstr forall (o' :: k). instr i1 o' -> instr i2 o'
f = \case
RfNormal instr i1 o
i -> instr i2 o -> RemFail instr i2 o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal (instr i2 o -> RemFail instr i2 o)
-> instr i2 o -> RemFail instr i2 o
forall a b. (a -> b) -> a -> b
$ instr i1 o -> instr i2 o
forall (o' :: k). instr i1 o' -> instr i2 o'
f instr i1 o
i
RfAlwaysFails forall (o' :: k). instr i1 o'
i -> (forall (o' :: k). instr i2 o') -> RemFail instr i2 o
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
(forall (o' :: k). instr i o') -> RemFail instr i o
RfAlwaysFails ((forall (o' :: k). instr i2 o') -> RemFail instr i2 o)
-> (forall (o' :: k). instr i2 o') -> RemFail instr i2 o
forall a b. (a -> b) -> a -> b
$ instr i1 o' -> instr i2 o'
forall (o' :: k). instr i1 o' -> instr i2 o'
f instr i1 o'
forall (o' :: k). instr i1 o'
i
getComparableProofS :: Sing (a :: T) -> Maybe (Dict (Comparable a))
getComparableProofS :: Sing a -> Maybe (Dict (Comparable a))
getComparableProofS Sing a
s = case Sing a -> Comparability a
forall (t :: T). Sing t -> Comparability t
checkComparability Sing a
s of
Comparability a
CanBeCompared -> Dict (Comparable a) -> Maybe (Dict (Comparable a))
forall a. a -> Maybe a
Just Dict (Comparable a)
forall (a :: Constraint). a => Dict a
Dict
Comparability a
CannotBeCompared -> Maybe (Dict (Comparable a))
forall a. Maybe a
Nothing
type family IsComparable (t :: T) :: Bool where
IsComparable ('TPair a b) = IsComparable a && IsComparable b
IsComparable ('TOption t) = IsComparable t
IsComparable 'TBls12381Fr = 'False
IsComparable 'TBls12381G1 = 'False
IsComparable 'TBls12381G2 = 'False
IsComparable ('TList _) = 'False
IsComparable ('TSet _) = 'False
IsComparable 'TOperation = 'False
IsComparable ('TContract _) = 'False
IsComparable ('TTicket _) = 'False
IsComparable ('TOr a b) = IsComparable a && IsComparable b
IsComparable ('TLambda _ _) = 'False
IsComparable ('TMap _ _) = 'False
IsComparable ('TBigMap _ _) = 'False
IsComparable _ = 'True
class (IsComparable t ~ 'True) => Comparable t where
tcompare :: (Value' instr t) -> (Value' instr t) -> Ordering
instance (Comparable e1, Comparable e2) => Comparable ('TPair e1 e2) where
tcompare :: Value' instr ('TPair e1 e2)
-> Value' instr ('TPair e1 e2) -> Ordering
tcompare (VPair (Value' instr l, Value' instr r)
a) (VPair (Value' instr l, Value' instr r)
b) = (Value' instr l, Value' instr r)
-> (Value' instr l, Value' instr r) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Value' instr l, Value' instr r)
a (Value' instr l, Value' instr r)
(Value' instr l, Value' instr r)
b
instance (Comparable e1, Comparable e2) => Comparable ('TOr e1 e2) where
tcompare :: Value' instr ('TOr e1 e2) -> Value' instr ('TOr e1 e2) -> Ordering
tcompare (VOr Either (Value' instr l) (Value' instr r)
a) (VOr Either (Value' instr l) (Value' instr r)
b) = Either (Value' instr l) (Value' instr r)
-> Either (Value' instr l) (Value' instr r) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Either (Value' instr l) (Value' instr r)
a Either (Value' instr l) (Value' instr r)
Either (Value' instr l) (Value' instr r)
b
instance Comparable e => Comparable ('TOption e) where
tcompare :: Value' instr ('TOption e) -> Value' instr ('TOption e) -> Ordering
tcompare (VOption Maybe (Value' instr t)
a) (VOption Maybe (Value' instr t)
b) = Maybe (Value' instr t) -> Maybe (Value' instr t) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Maybe (Value' instr t)
a Maybe (Value' instr t)
Maybe (Value' instr t)
b
instance Comparable 'TUnit where
tcompare :: Value' instr 'TUnit -> Value' instr 'TUnit -> Ordering
tcompare Value' instr 'TUnit
VUnit Value' instr 'TUnit
VUnit = Ordering
EQ
instance Comparable 'TInt where
tcompare :: Value' instr 'TInt -> Value' instr 'TInt -> Ordering
tcompare (VInt Integer
a) (VInt Integer
b) = Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Integer
a Integer
b
instance Comparable 'TNat where
tcompare :: Value' instr 'TNat -> Value' instr 'TNat -> Ordering
tcompare (VNat Natural
a) (VNat Natural
b) = Natural -> Natural -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Natural
a Natural
b
instance Comparable 'TString where
tcompare :: Value' instr 'TString -> Value' instr 'TString -> Ordering
tcompare (VString MText
a) (VString MText
b) = MText -> MText -> Ordering
forall a. Ord a => a -> a -> Ordering
compare MText
a MText
b
instance Comparable 'TBytes where
tcompare :: Value' instr 'TBytes -> Value' instr 'TBytes -> Ordering
tcompare (VBytes ByteString
a) (VBytes ByteString
b) = ByteString -> ByteString -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ByteString
a ByteString
b
instance Comparable 'TMutez where
tcompare :: Value' instr 'TMutez -> Value' instr 'TMutez -> Ordering
tcompare (VMutez Mutez
a) (VMutez Mutez
b) = Mutez -> Mutez -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Mutez
a Mutez
b
instance Comparable 'TBool where
tcompare :: Value' instr 'TBool -> Value' instr 'TBool -> Ordering
tcompare (VBool Bool
a) (VBool Bool
b) = Bool -> Bool -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Bool
a Bool
b
instance Comparable 'TKeyHash where
tcompare :: Value' instr 'TKeyHash -> Value' instr 'TKeyHash -> Ordering
tcompare (VKeyHash KeyHash
a) (VKeyHash KeyHash
b) = KeyHash -> KeyHash -> Ordering
forall a. Ord a => a -> a -> Ordering
compare KeyHash
a KeyHash
b
instance Comparable 'TTimestamp where
tcompare :: Value' instr 'TTimestamp -> Value' instr 'TTimestamp -> Ordering
tcompare (VTimestamp Timestamp
a) (VTimestamp Timestamp
b) = Timestamp -> Timestamp -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Timestamp
a Timestamp
b
instance Comparable 'TAddress where
tcompare :: Value' instr 'TAddress -> Value' instr 'TAddress -> Ordering
tcompare (VAddress EpAddress
a) (VAddress EpAddress
b) = EpAddress -> EpAddress -> Ordering
forall a. Ord a => a -> a -> Ordering
compare EpAddress
a EpAddress
b
instance Comparable 'TNever where
tcompare :: Value' instr 'TNever -> Value' instr 'TNever -> Ordering
tcompare = Value' instr 'TNever -> Value' instr 'TNever -> Ordering
\case
instance Comparable 'TChainId where
tcompare :: Value' instr 'TChainId -> Value' instr 'TChainId -> Ordering
tcompare (VChainId ChainId
a) (VChainId ChainId
b) = ChainId -> ChainId -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ChainId
a ChainId
b
instance Comparable 'TSignature where
tcompare :: Value' instr 'TSignature -> Value' instr 'TSignature -> Ordering
tcompare (VSignature Signature
a) (VSignature Signature
b) = Signature -> Signature -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Signature
a Signature
b
instance Comparable 'TKey where
tcompare :: Value' instr 'TKey -> Value' instr 'TKey -> Ordering
tcompare (VKey PublicKey
a) (VKey PublicKey
b) = PublicKey -> PublicKey -> Ordering
forall a. Ord a => a -> a -> Ordering
compare PublicKey
a PublicKey
b
instance (Comparable e) => Ord (Value' instr e) where
compare :: Value' instr e -> Value' instr e -> Ordering
compare = forall (instr :: [T] -> [T] -> *).
Comparable e =>
Value' instr e -> Value' instr e -> Ordering
forall (t :: T) (instr :: [T] -> [T] -> *).
Comparable t =>
Value' instr t -> Value' instr t -> Ordering
tcompare @e
type family FailOnNonComparable (isComparable :: Bool) :: Constraint where
FailOnNonComparable 'False =
TypeError ('Text "The type is not comparable")
FailOnNonComparable 'True = ()
type ComparabilityScope t =
(SingI t, Comparable t)
data Comparability t where
CanBeCompared :: (Comparable t) => Comparability t
CannotBeCompared :: (IsComparable t ~ 'False) => Comparability t
checkComparability :: Sing t -> Comparability t
checkComparability :: Sing t -> Comparability t
checkComparability = \case
STPair a b -> case (Sing n -> Comparability n
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n
a, Sing n -> Comparability n
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n
b) of
(Comparability n
CanBeCompared, Comparability n
CanBeCompared) -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
(Comparability n
CannotBeCompared, Comparability n
_) -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
(Comparability n
_, Comparability n
CannotBeCompared) -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
STOr a b -> case (Sing n -> Comparability n
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n
a, Sing n -> Comparability n
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n
b) of
(Comparability n
CanBeCompared, Comparability n
CanBeCompared) -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
(Comparability n
CannotBeCompared, Comparability n
_) -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
(Comparability n
_, Comparability n
CannotBeCompared) -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
STOption t -> case Sing n -> Comparability n
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n
t of
Comparability n
CanBeCompared -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Comparability n
CannotBeCompared -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
STList _ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
STSet _ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
Sing t
STOperation -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
STContract _ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
STTicket _ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
STLambda _ _ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
STMap _ _ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
STBigMap _ _ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
Sing t
STNever -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STUnit -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STInt -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STNat -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STString -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STBytes -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STMutez -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STBool -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STKeyHash -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STBls12381Fr -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
Sing t
STBls12381G1 -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
Sing t
STBls12381G2 -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
Sing t
STTimestamp -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STAddress -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STKey -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STSignature -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
Sing t
STChainId -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
comparabilityPresence :: Sing t -> Maybe (Dict $ (Comparable t))
comparabilityPresence :: Sing t -> Maybe (Dict $ Comparable t)
comparabilityPresence Sing t
s = case Sing t -> Comparability t
forall (t :: T). Sing t -> Comparability t
checkComparability Sing t
s of
Comparability t
CanBeCompared -> (Dict $ Comparable t) -> Maybe (Dict $ Comparable t)
forall a. a -> Maybe a
Just Dict $ Comparable t
forall (a :: Constraint). a => Dict a
Dict
Comparability t
CannotBeCompared -> Maybe (Dict $ Comparable t)
forall a. Maybe a
Nothing
instance SingI t => CheckScope (Comparable t) where
checkScope :: Either BadTypeForScope (Dict (Comparable t))
checkScope = BadTypeForScope
-> Maybe (Dict (Comparable t))
-> Either BadTypeForScope (Dict (Comparable t))
forall l r. l -> Maybe r -> Either l r
maybeToRight BadTypeForScope
BtNotComparable (Maybe (Dict (Comparable t))
-> Either BadTypeForScope (Dict (Comparable t)))
-> Maybe (Dict (Comparable t))
-> Either BadTypeForScope (Dict (Comparable t))
forall a b. (a -> b) -> a -> b
$ Sing t -> Maybe (Dict (Comparable t))
forall (t :: T). Sing t -> Maybe (Dict $ Comparable t)
comparabilityPresence Sing t
forall k (a :: k). SingI a => Sing a
sing
instance (SingI t) => CheckScope (ComparabilityScope t) where
checkScope :: Either BadTypeForScope (Dict (ComparabilityScope t))
checkScope =
(\Dict (Comparable t)
Dict -> Dict (ComparabilityScope t)
forall (a :: Constraint). a => Dict a
Dict) (Dict (Comparable t) -> Dict (ComparabilityScope t))
-> Either BadTypeForScope (Dict (Comparable t))
-> Either BadTypeForScope (Dict (ComparabilityScope t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CheckScope (Comparable t) =>
Either BadTypeForScope (Dict (Comparable t))
forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(Comparable t)
data Value' instr t where
VKey :: PublicKey -> Value' instr 'TKey
VUnit :: Value' instr 'TUnit
VSignature :: Signature -> Value' instr 'TSignature
VChainId :: ChainId -> Value' instr 'TChainId
VOption
:: forall t instr.
(SingI t)
=> Maybe (Value' instr t) -> Value' instr ('TOption t)
VList
:: forall t instr.
(SingI t)
=> [Value' instr t] -> Value' instr ('TList t)
VSet
:: forall t instr.
(SingI t, Comparable t)
=> Set (Value' instr t) -> Value' instr ('TSet t)
VOp
:: Operation' instr -> Value' instr 'TOperation
VContract
:: forall arg instr.
(SingI arg, HasNoOp arg)
=> Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg)
VTicket
:: forall arg instr.
(Comparable arg)
=> Address -> Value' instr arg -> Natural -> Value' instr ('TTicket arg)
VPair
:: forall l r instr.
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VOr
:: forall l r instr.
(SingI l, SingI r)
=> Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r)
VLam
:: forall inp out instr.
( SingI inp, SingI out
, forall i o. Show (instr i o)
, forall i o. Eq (instr i o)
, forall i o. NFData (instr i o)
)
=> RemFail instr (inp ': '[]) (out ': '[]) -> Value' instr ('TLambda inp out)
VMap
:: forall k v instr.
(SingI k, SingI v, Comparable k)
=> Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
VBigMap
:: forall k v instr.
(SingI k, SingI v, Comparable k, HasNoBigMap v)
=> Maybe Natural
-> Map (Value' instr k) (Value' instr v)
-> Value' instr ('TBigMap k v)
VInt :: Integer -> Value' instr 'TInt
VNat :: Natural -> Value' instr 'TNat
VString :: MText -> Value' instr 'TString
VBytes :: ByteString -> Value' instr 'TBytes
VMutez :: Mutez -> Value' instr 'TMutez
VBool :: Bool -> Value' instr 'TBool
VKeyHash :: KeyHash -> Value' instr 'TKeyHash
VTimestamp :: Timestamp -> Value' instr 'TTimestamp
VAddress :: EpAddress -> Value' instr 'TAddress
VBls12381Fr :: Bls12381Fr -> Value' instr 'TBls12381Fr
VBls12381G1 :: Bls12381G1 -> Value' instr 'TBls12381G1
VBls12381G2 :: Bls12381G2 -> Value' instr 'TBls12381G2
deriving stock instance Show (Value' instr t)
deriving stock instance Eq (Value' instr t)
addressToVContract
:: forall t instr.
(ParameterScope t, ForbidOr t)
=> Address -> Value' instr ('TContract t)
addressToVContract :: Address -> Value' instr ('TContract t)
addressToVContract Address
addr = Address -> SomeEntrypointCallT t -> Value' instr ('TContract t)
forall (arg :: T) (instr :: [T] -> [T] -> *).
(SingI arg, HasNoOp arg) =>
Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg)
VContract Address
addr SomeEntrypointCallT t
forall (t :: T).
(ParameterScope t, ForbidOr t) =>
SomeEntrypointCallT t
sepcPrimitive
buildVContract :: Value' instr ('TContract arg) -> Builder
buildVContract :: Value' instr ('TContract arg) -> Builder
buildVContract = \case
VContract Address
addr SomeEntrypointCallT arg
epc -> Builder
"Contract " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Address
addr Address -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
" call " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| SomeEntrypointCallT arg
epc SomeEntrypointCallT arg -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
""
compileEpLiftSequence
:: EpLiftSequence arg param
-> Value' instr arg
-> Value' instr param
compileEpLiftSequence :: EpLiftSequence arg param -> Value' instr arg -> Value' instr param
compileEpLiftSequence = \case
EpLiftSequence arg param
EplArgHere -> Value' instr arg -> Value' instr param
forall a. a -> a
id
EplWrapLeft EpLiftSequence arg subparam
els -> Either (Value' instr subparam) (Value' instr r)
-> Value' instr ('TOr subparam r)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(SingI l, SingI r) =>
Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r)
VOr (Either (Value' instr subparam) (Value' instr r)
-> Value' instr ('TOr subparam r))
-> (Value' instr arg
-> Either (Value' instr subparam) (Value' instr r))
-> Value' instr arg
-> Value' instr ('TOr subparam r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value' instr subparam
-> Either (Value' instr subparam) (Value' instr r)
forall a b. a -> Either a b
Left (Value' instr subparam
-> Either (Value' instr subparam) (Value' instr r))
-> (Value' instr arg -> Value' instr subparam)
-> Value' instr arg
-> Either (Value' instr subparam) (Value' instr r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpLiftSequence arg subparam
-> Value' instr arg -> Value' instr subparam
forall (arg :: T) (param :: T) (instr :: [T] -> [T] -> *).
EpLiftSequence arg param -> Value' instr arg -> Value' instr param
compileEpLiftSequence EpLiftSequence arg subparam
els
EplWrapRight EpLiftSequence arg subparam
els -> Either (Value' instr l) (Value' instr subparam)
-> Value' instr ('TOr l subparam)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(SingI l, SingI r) =>
Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r)
VOr (Either (Value' instr l) (Value' instr subparam)
-> Value' instr ('TOr l subparam))
-> (Value' instr arg
-> Either (Value' instr l) (Value' instr subparam))
-> Value' instr arg
-> Value' instr ('TOr l subparam)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value' instr subparam
-> Either (Value' instr l) (Value' instr subparam)
forall a b. b -> Either a b
Right (Value' instr subparam
-> Either (Value' instr l) (Value' instr subparam))
-> (Value' instr arg -> Value' instr subparam)
-> Value' instr arg
-> Either (Value' instr l) (Value' instr subparam)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpLiftSequence arg subparam
-> Value' instr arg -> Value' instr subparam
forall (arg :: T) (param :: T) (instr :: [T] -> [T] -> *).
EpLiftSequence arg param -> Value' instr arg -> Value' instr param
compileEpLiftSequence EpLiftSequence arg subparam
els
liftCallArg
:: EntrypointCallT param arg
-> Value' instr arg
-> Value' instr param
liftCallArg :: EntrypointCallT param arg -> Value' instr arg -> Value' instr param
liftCallArg EntrypointCallT param arg
epc = EpLiftSequence arg param -> Value' instr arg -> Value' instr param
forall (arg :: T) (param :: T) (instr :: [T] -> [T] -> *).
EpLiftSequence arg param -> Value' instr arg -> Value' instr param
compileEpLiftSequence (EntrypointCallT param arg -> EpLiftSequence arg param
forall (param :: T) (arg :: T).
EntrypointCallT param arg -> EpLiftSequence arg param
epcLiftSequence EntrypointCallT param arg
epc)
valueTypeSanity :: Value' instr t -> Dict (SingI t)
valueTypeSanity :: Value' instr t -> Dict (SingI t)
valueTypeSanity = \case
VKey{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VUnit{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VSignature{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VChainId{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VOption{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VList{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VSet{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VOp{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VContract Address
_ (SomeEpc EntrypointCall{}) -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VTicket Address
_ Value' instr arg
v Natural
_ -> case Value' instr arg -> Dict (SingI arg)
forall (instr :: [T] -> [T] -> *) (t :: T).
Value' instr t -> Dict (SingI t)
valueTypeSanity Value' instr arg
v of
Dict (SingI arg)
Dict -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VPair (Value' instr l
l, Value' instr r
r) -> case (Value' instr l -> Dict (SingI l)
forall (instr :: [T] -> [T] -> *) (t :: T).
Value' instr t -> Dict (SingI t)
valueTypeSanity Value' instr l
l, Value' instr r -> Dict (SingI r)
forall (instr :: [T] -> [T] -> *) (t :: T).
Value' instr t -> Dict (SingI t)
valueTypeSanity Value' instr r
r) of
(Dict (SingI l)
Dict, Dict (SingI r)
Dict) -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VOr{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VLam{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VMap{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VBigMap{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VInt{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VNat{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VString{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VBytes{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VMutez{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VBool{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VKeyHash{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VBls12381Fr{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VBls12381G1{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VBls12381G2{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VTimestamp{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
VAddress{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
withValueTypeSanity :: Value' instr t -> (SingI t => a) -> a
withValueTypeSanity :: Value' instr t -> (SingI t => a) -> a
withValueTypeSanity Value' instr t
v SingI t => a
a = case Value' instr t -> Dict (SingI t)
forall (instr :: [T] -> [T] -> *) (t :: T).
Value' instr t -> Dict (SingI t)
valueTypeSanity Value' instr t
v of Dict (SingI t)
Dict -> a
SingI t => a
a
eqValueExt :: Value' instr t1 -> Value' instr t2 -> Bool
eqValueExt :: Value' instr t1 -> Value' instr t2 -> Bool
eqValueExt Value' instr t1
v1 Value' instr t2
v2 =
Value' instr t1
v1 Value' instr t1 -> Value' instr t2 -> Bool
forall k (a1 :: k) (a2 :: k) (t :: k -> *).
(SingI a1, SingI a2, SDecide k, Eq (t a1)) =>
t a1 -> t a2 -> Bool
`eqParamSing` Value' instr t2
v2
(SingI t1 => Bool) -> Dict (SingI t1) -> Bool
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Value' instr t1 -> Dict (SingI t1)
forall (instr :: [T] -> [T] -> *) (t :: T).
Value' instr t -> Dict (SingI t)
valueTypeSanity Value' instr t1
v1
(SingI t2 => Bool) -> Dict (SingI t2) -> Bool
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Value' instr t2 -> Dict (SingI t2)
forall (instr :: [T] -> [T] -> *) (t :: T).
Value' instr t -> Dict (SingI t)
valueTypeSanity Value' instr t2
v2
$(deriveGADTNFData ''Operation')
$(deriveGADTNFData ''Value')