-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

{-# LANGUAGE QuantifiedConstraints #-}

-- | Module, containing data types for Michelson value.

module Michelson.Typed.Value
  ( SomeValue' (..)
  , SomeConstrainedValue' (..)
  , 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 qualified Data.Kind as Kind
import Data.Singletons (Sing, SingI(..))
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 (BadTypeForScope(..), CheckScope(..), ParameterScope, StorageScope)
import Michelson.Typed.Sing
import Michelson.Typed.T (T(..))
import Tezos.Address (Address)
import Tezos.Core (ChainId, Mutez, Timestamp)
import Tezos.Crypto (KeyHash, PublicKey, Signature)
import Util.TH
import Util.Typeable

-- | Data type, representing operation, list of which is returned
-- by Michelson contract (according to calling convention).
--
-- These operations are to be further executed against system state
-- after the contract execution.
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 tt :: TransferTokens instr p
tt -> TransferTokens instr p -> Builder
forall p. Buildable p => p -> Builder
build TransferTokens instr p
tt
      OpSetDelegate sd :: SetDelegate
sd -> SetDelegate -> Builder
forall p. Buildable p => p -> Builder
build SetDelegate
sd
      OpCreateContract cc :: 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
  op1 :: Operation' instr
op1 == :: Operation' instr -> Operation' instr -> Bool
== op2 :: Operation' instr
op2 = case (Operation' instr
op1, Operation' instr
op2) of
    (OpTransferTokens tt1 :: TransferTokens instr p
tt1, OpTransferTokens tt2 :: TransferTokens instr p
tt2) -> TransferTokens instr p -> TransferTokens instr p -> Bool
forall k (a1 :: k) (a2 :: k) (t :: k -> *).
(Typeable a1, Typeable a2, Eq (t a1)) =>
t a1 -> t a2 -> Bool
eqParam1 TransferTokens instr p
tt1 TransferTokens instr p
tt2
    (OpTransferTokens _, _) -> Bool
False
    (OpSetDelegate sd1 :: SetDelegate
sd1, OpSetDelegate sd2 :: SetDelegate
sd2) -> SetDelegate
sd1 SetDelegate -> SetDelegate -> Bool
forall a. Eq a => a -> a -> Bool
== SetDelegate
sd2
    (OpSetDelegate _, _) -> Bool
False
    (OpCreateContract cc1 :: CreateContract instr cp st
cc1, OpCreateContract cc2 :: CreateContract instr cp st
cc2) -> CreateContract instr cp st -> CreateContract instr cp st -> Bool
forall k1 k2 k3 (a1 :: k1) (a2 :: k1) (b1 :: k2) (b2 :: k2)
       (c1 :: k3) (c2 :: k3) (t :: k1 -> k2 -> k3 -> *).
(Typeable a1, Typeable a2, Typeable b1, Typeable b2, Typeable c1,
 Typeable c2, Eq (t a1 b1 c1)) =>
t a1 b1 c1 -> t a2 b2 c2 -> Bool
eqParam3 CreateContract instr cp st
cc1 CreateContract instr cp st
cc2
    (OpCreateContract _, _) -> 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 {..} =
    "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
|+ " 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
|+ ""

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 mbDelegate :: Maybe KeyHash
mbDelegate) =
    "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 "<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 a :: Address
a b :: Maybe KeyHash
b c :: Mutez
c d :: Value' instr st
d e :: 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 {..} =
    "Create a new contract with" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
    " 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 "<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
|+
    " 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
|+ ""

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 ]

-- | Wrapper over instruction which remembers whether this instruction
-- always fails or not.
data RemFail (instr :: k -> k -> Kind.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 a :: instr i o
a) = instr i o -> ()
forall a. NFData a => a -> ()
rnf instr i o
a
  rnf (RfAlwaysFails a :: 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

-- | Ignoring distinction between constructors here, comparing only semantics.
instance Eq (instr i o) => Eq (RemFail instr i o) where
  RfNormal i1 :: instr i o
i1 == :: RemFail instr i o -> RemFail instr i o -> Bool
== RfNormal i2 :: 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 i1 :: forall (o' :: k). instr i o'
i1 == RfNormal i2 :: 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 i1 :: instr i o
i1 == RfAlwaysFails i2 :: 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 i1 :: forall (o' :: k). instr i o'
i1 == RfAlwaysFails i2 :: 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

-- | Merge two execution branches.
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 merger :: forall (o' :: k). instr i1 o' -> instr i2 o' -> instr i3 o'
merger instr1 :: RemFail instr i1 o
instr1 instr2 :: RemFail instr i2 o
instr2 = case (RemFail instr i1 o
instr1, RemFail instr i2 o
instr2) of
  (RfNormal i1 :: instr i1 o
i1, RfNormal i2 :: 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 i1 :: forall (o' :: k). instr i1 o'
i1, RfNormal i2 :: 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 i1 :: instr i1 o
i1, RfAlwaysFails i2 :: 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 i1 :: forall (o' :: k). instr i1 o'
i1, RfAlwaysFails i2 :: 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)

-- | Get code disregard whether it always fails or not.
rfAnyInstr :: RemFail instr i o -> instr i o
rfAnyInstr :: RemFail instr i o -> instr i o
rfAnyInstr = \case
  RfNormal i :: instr i o
i -> instr i o
i
  RfAlwaysFails i :: forall (o' :: k). instr i o'
i -> instr i o
forall (o' :: k). instr i o'
i

-- | Modify inner code.
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 f :: forall (o' :: k). instr i1 o' -> instr i2 o'
f = \case
  RfNormal i :: 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 i :: 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 s :: Sing a
s = case Sing a -> Comparability a
forall (t :: T). Sing t -> Comparability t
checkComparability Sing a
s of
  CanBeCompared -> Dict (Comparable a) -> Maybe (Dict (Comparable a))
forall a. a -> Maybe a
Just Dict (Comparable a)
forall (a :: Constraint). a => Dict a
Dict
  CannotBeCompared -> Maybe (Dict (Comparable a))
forall a. Maybe a
Nothing

-- | Constraint which ensures that type is comparable.
type family IsComparable (t :: T) :: Bool where
  IsComparable ('TPair a b) =  IsComparable a && IsComparable b
  IsComparable 'TKey = 'False
  IsComparable 'TUnit = 'False
  IsComparable 'TSignature = 'False
  IsComparable 'TChainId = 'False
  IsComparable ('TOption _) = 'False
  IsComparable ('TList _) = 'False
  IsComparable ('TSet _) = 'False
  IsComparable 'TOperation = 'False
  IsComparable ('TContract _) = 'False
  IsComparable ('TOr _ _) = 'False
  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 a :: (Value' instr l, Value' instr r)
a) (VPair b :: (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 'TInt where
  tcompare :: Value' instr 'TInt -> Value' instr 'TInt -> Ordering
tcompare (VInt a :: Integer
a) (VInt b :: 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 a :: Natural
a) (VNat b :: 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 a :: MText
a) (VString b :: 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 a :: ByteString
a) (VBytes b :: 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 a :: Mutez
a) (VMutez b :: 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 a :: Bool
a) (VBool b :: 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 a :: KeyHash
a) (VKeyHash b :: 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 a :: Timestamp
a) (VTimestamp b :: 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 a :: EpAddress
a) (VAddress b :: EpAddress
b) = EpAddress -> EpAddress -> Ordering
forall a. Ord a => a -> a -> Ordering
compare EpAddress
a EpAddress
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

-- | Report a human-readable error that 'TBigMap' contains another 'TBigMap'
type family FailOnNonComparable (isComparable :: Bool) :: Constraint where
  FailOnNonComparable 'False =
    TypeError ('Text "The type is not comparable")
  FailOnNonComparable 'True = ()

-- | Alias for comparable types.
type ComparabilityScope t =
  (KnownT 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 a -> Comparability a
forall (t :: T). Sing t -> Comparability t
checkComparability Sing a
a, Sing b -> Comparability b
forall (t :: T). Sing t -> Comparability t
checkComparability Sing b
b) of
    (CanBeCompared, CanBeCompared) -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
    (CannotBeCompared, _) -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
    (_, CannotBeCompared) -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  STKey -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  STUnit -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  STSignature -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  STChainId -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  STOption _ -> 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
  STOperation -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  STContract _ -> Comparability t
forall (t :: T). (IsComparable t ~ 'False) => Comparability t
CannotBeCompared
  STOr _ _ -> 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
  STInt -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  STNat -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  STString -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  STBytes -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  STMutez -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  STBool -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  STKeyHash -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  STTimestamp -> Comparability t
forall (t :: T). Comparable t => Comparability t
CanBeCompared
  STAddress -> 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 s :: Sing t
s = case Sing t -> Comparability t
forall (t :: T). Sing t -> Comparability t
checkComparability Sing t
s of
  CanBeCompared -> (Dict $ Comparable t) -> Maybe (Dict $ Comparable t)
forall a. a -> Maybe a
Just Dict $ Comparable t
forall (a :: Constraint). a => Dict a
Dict
  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 (KnownT t) => CheckScope (ComparabilityScope t) where
  checkScope :: Either BadTypeForScope (Dict (ComparabilityScope t))
checkScope =
    (\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)

-- | Representation of Michelson value.
--
-- Type parameter @instr@ stands for Michelson instruction
-- type, i.e. data type to represent an instruction of language.

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.
       (KnownT t)
    => Maybe (Value' instr t) -> Value' instr ('TOption t)
  VList
    :: forall t instr.
       (KnownT t)
    => [Value' instr t] -> Value' instr ('TList t)
  VSet
    :: forall t instr.
       (KnownT t, Comparable t)
    => Set (Value' instr t) -> Value' instr ('TSet t)
  VOp
    :: Operation' instr -> Value' instr 'TOperation
  VContract
    :: forall arg instr.
       Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg)
  VPair
    :: forall l r instr.
       (Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
  VOr
    :: forall l r instr.
       (KnownT l, KnownT r)
    => Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r)
  VLam
    :: forall inp out instr.
       ( KnownT inp, KnownT 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.
       (KnownT k, KnownT v, Comparable k)
    => Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
  VBigMap
    :: forall k v instr.
       (KnownT k, KnownT v, Comparable k)
    => 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

deriving stock instance Show (Value' instr t)
deriving stock instance Eq (Value' instr t)

-- | Make value of 'contract' type which refers to the given address and
-- does not call any entrypoint.
addressToVContract
  :: forall t instr.
      (ParameterScope t, ForbidOr t)
  => Address -> Value' instr ('TContract t)
addressToVContract :: Address -> Value' instr ('TContract t)
addressToVContract addr :: Address
addr = Address -> SomeEntrypointCallT t -> Value' instr ('TContract t)
forall (arg :: T) (instr :: [T] -> [T] -> *).
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 addr :: Address
addr epc :: SomeEntrypointCallT arg
epc -> "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
|+ " 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
|+ ""

data SomeValue' instr where
  SomeValue :: KnownT t => Value' instr t -> SomeValue' instr

deriving stock instance Show (SomeValue' instr)

instance Eq (SomeValue' instr) where
  SomeValue v1 :: Value' instr t
v1 == :: SomeValue' instr -> SomeValue' instr -> Bool
== SomeValue v2 :: Value' instr t
v2 = Value' instr t
v1 Value' instr t -> Value' instr t -> Bool
forall k (a1 :: k) (a2 :: k) (t :: k -> *).
(Typeable a1, Typeable a2, Eq (t a1)) =>
t a1 -> t a2 -> Bool
`eqParam1` Value' instr t
v2

data SomeConstrainedValue' instr (c :: T -> Constraint) where
  SomeConstrainedValue
    :: forall (t :: T) (c :: T -> Constraint) instr
    . (c t)
    => Value' instr t
    -> SomeConstrainedValue' instr c

deriving stock instance Show (SomeConstrainedValue' instr c)

-- TODO
-- @gromak: perhaps we should implement `SomeValue'` in terms of
-- `SomeConstrainedValue'`, but it will require changing quite a lot of code,
-- so it is postponed.

-- | Turn 'EpLiftSequence' into actual function on 'Value's.
compileEpLiftSequence
  :: EpLiftSequence arg param
  -> Value' instr arg
  -> Value' instr param
compileEpLiftSequence :: EpLiftSequence arg param -> Value' instr arg -> Value' instr param
compileEpLiftSequence = \case
  EplArgHere -> Value' instr arg -> Value' instr param
forall a. a -> a
id
  EplWrapLeft els :: EpLiftSequence arg subparam
els -> Either (Value' instr subparam) (Value' instr r)
-> Value' instr ('TOr subparam r)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(KnownT l, KnownT 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 els :: EpLiftSequence arg subparam
els -> Either (Value' instr l) (Value' instr subparam)
-> Value' instr ('TOr l subparam)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(KnownT l, KnownT 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

-- | Lift entrypoint argument to full parameter.
liftCallArg
  :: EntrypointCallT param arg
  -> Value' instr arg
  -> Value' instr param
liftCallArg :: EntrypointCallT param arg -> Value' instr arg -> Value' instr param
liftCallArg epc :: 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)

-- | Get a witness of that value's type is known.
--
-- Note that we cannot pick such witness out of nowhere as not all types
-- of kind 'T' have 'Typeable' and 'SingI' instances; example:
--
-- @
-- type family Any :: T where
--   -- nothing here
-- @
valueTypeSanity :: Value' instr t -> Dict (KnownT t)
valueTypeSanity :: Value' instr t -> Dict (KnownT t)
valueTypeSanity = \case
  VKey{} -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict
  VUnit{} -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict
  VSignature{} -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict
  VChainId{} -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict
  VOption{} -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict
  VList{} -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict
  VSet{} -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict
  VOp{} -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict
  VContract _ (SomeEpc EntrypointCall{}) -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict
  VPair (l :: Value' instr l
l, r :: Value' instr r
r) -> case (Value' instr l -> Dict (KnownT l)
forall (instr :: [T] -> [T] -> *) (t :: T).
Value' instr t -> Dict (KnownT t)
valueTypeSanity Value' instr l
l, Value' instr r -> Dict (KnownT r)
forall (instr :: [T] -> [T] -> *) (t :: T).
Value' instr t -> Dict (KnownT t)
valueTypeSanity Value' instr r
r) of
    (Dict, Dict) -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict
  VOr{} -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict
  VLam{} -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict
  VMap{} -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict
  VBigMap{} -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict
  VInt{} -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict
  VNat{} -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict
  VString{} -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict
  VBytes{} -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict
  VMutez{} -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict
  VBool{} -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict
  VKeyHash{} -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict
  VTimestamp{} -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict
  VAddress{} -> Dict (KnownT t)
forall (a :: Constraint). a => Dict a
Dict

-- | Provide a witness of that value's type is known.
withValueTypeSanity :: Value' instr t -> (KnownT t => a) -> a
withValueTypeSanity :: Value' instr t -> (KnownT t => a) -> a
withValueTypeSanity v :: Value' instr t
v a :: KnownT t => a
a = case Value' instr t -> Dict (KnownT t)
forall (instr :: [T] -> [T] -> *) (t :: T).
Value' instr t -> Dict (KnownT t)
valueTypeSanity Value' instr t
v of Dict -> a
KnownT t => a
a

-- | Extended values comparison - it does not require 'Value's to be
-- of the same type, only their content to match.
eqValueExt :: Value' instr t1 -> Value' instr t2 -> Bool
eqValueExt :: Value' instr t1 -> Value' instr t2 -> Bool
eqValueExt v1 :: Value' instr t1
v1 v2 :: Value' instr t2
v2 =
  Value' instr t1
v1 Value' instr t1 -> Value' instr t2 -> Bool
forall k (a1 :: k) (a2 :: k) (t :: k -> *).
(Typeable a1, Typeable a2, Eq (t a1)) =>
t a1 -> t a2 -> Bool
`eqParam1` Value' instr t2
v2
    (KnownT t1 => Bool) -> Dict (KnownT t1) -> Bool
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Value' instr t1 -> Dict (KnownT t1)
forall (instr :: [T] -> [T] -> *) (t :: T).
Value' instr t -> Dict (KnownT t)
valueTypeSanity Value' instr t1
v1
    (KnownT t2 => Bool) -> Dict (KnownT t2) -> Bool
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Value' instr t2 -> Dict (KnownT t2)
forall (instr :: [T] -> [T] -> *) (t :: T).
Value' instr t -> Dict (KnownT t)
valueTypeSanity Value' instr t2
v2

-- TODO: actually we should handle big maps with something close
-- to following:
--
--  VBigMap :: BigMap op ref k v -> Value' cp ('TBigMap k v)
--
-- data Value'Op v
--     = New v
--     | Upd v
--     | Rem
--     | NotExisted
--
-- data BigMap op ref k v = BigMap
--  { bmRef :: ref k v, bmChanges :: Map (CValue k) (Value'Op (Value' cp v)) }

$(deriveGADTNFData ''Operation')
$(deriveGADTNFData ''Value')