-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

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

module Morley.Michelson.Typed.Value
  ( Comparability (..)
  , CreateContract (..)
  , Operation' (..)
  , SetDelegate (..)
  , TransferTokens (..)
  , Emit(..)
  , Value' (..)
  , RemFail (..)
  , LambdaCode' (..)
  , mkVLam
  , mkVLamRec
  , rfMerge
  , rfAnyInstr
  , rfMapAnyInstr
  , addressToVContract
  , buildVContract
  , checkComparability
  , compileEpLiftSequence
  , liftCallArg
  , valueTypeSanity
  , withValueTypeSanity
  , eqValueExt
  ) where

import Control.Lens (At(..), Index, IxValue, Ixed(..))
import Data.Constraint (Dict(..), (\\))
import Data.GADT.Compare (GEq(..))
import Fmt (Buildable(build), Doc, (+|), (|+))

import Morley.Michelson.Text (MText)
import Morley.Michelson.Typed.Annotation (Notes)
import Morley.Michelson.Typed.Contract
import Morley.Michelson.Typed.Entrypoints
import Morley.Michelson.Typed.Scope
import Morley.Michelson.Typed.T (T(..))
import Morley.Tezos.Address
import Morley.Tezos.Core (ChainId, Mutez, Timestamp)
import Morley.Tezos.Crypto
  (Bls12381Fr, Bls12381G1, Bls12381G2, Chest, ChestKey, KeyHash, PublicKey, Signature)
import Morley.Util.Sing (eqParamMixed3, eqParamSing, geqI)
import Morley.Util.TH

-- | 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
    :: ( forall i o. Show (instr i o)
       , forall i o. NFData (instr i o)
       , Typeable instr, ParameterScope cp, StorageScope st)
    => CreateContract instr cp st
    -> Operation' instr
  OpEmit :: PackedValScope t => Emit instr t -> Operation' instr

instance (forall t. Buildable (Value' instr t)) => Buildable (Operation' instr) where
  build :: Operation' instr -> Doc
build =
    \case
      OpTransferTokens TransferTokens instr p
tt -> TransferTokens instr p -> Doc
forall a. Buildable a => a -> Doc
build TransferTokens instr p
tt
      OpSetDelegate SetDelegate
sd -> SetDelegate -> Doc
forall a. Buildable a => a -> Doc
build SetDelegate
sd
      OpCreateContract CreateContract instr cp st
cc -> CreateContract instr cp st -> Doc
forall a. Buildable a => a -> Doc
build CreateContract instr cp st
cc
      OpEmit Emit instr t
em -> Emit instr t -> Doc
forall a. Buildable a => a -> Doc
build Emit instr t
em

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
`eqParamMixed3` CreateContract instr cp st
cc2
    (OpCreateContract CreateContract instr cp st
_, Operation' instr
_) -> Bool
False
    (OpEmit Emit instr t
em1, OpEmit Emit instr t
em2) -> Emit instr t
em1 Emit instr t -> Emit instr t -> Bool
forall {k} (a1 :: k) (a2 :: k) (t :: k -> *).
(SingI a1, SingI a2, SDecide k, Eq (t a1)) =>
t a1 -> t a2 -> Bool
`eqParamSing` Emit instr t
em2
    (OpEmit Emit instr t
_, Operation' instr
_) -> Bool
False

data TransferTokens instr p = TransferTokens
  { forall (instr :: [T] -> [T] -> *) (p :: T).
TransferTokens instr p -> Value' instr p
ttTransferArgument :: Value' instr p
  , forall (instr :: [T] -> [T] -> *) (p :: T).
TransferTokens instr p -> Mutez
ttAmount :: Mutez
  , forall (instr :: [T] -> [T] -> *) (p :: T).
TransferTokens instr p -> Value' instr ('TContract p)
ttContract :: Value' instr ('TContract p)
  , forall (instr :: [T] -> [T] -> *) (p :: T).
TransferTokens instr p -> GlobalCounter
ttCounter :: GlobalCounter
  } 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
$cshowsPrec :: forall (instr :: [T] -> [T] -> *) (p :: T).
Int -> TransferTokens instr p -> ShowS
showsPrec :: Int -> TransferTokens instr p -> ShowS
$cshow :: forall (instr :: [T] -> [T] -> *) (p :: T).
TransferTokens instr p -> String
show :: TransferTokens instr p -> String
$cshowList :: forall (instr :: [T] -> [T] -> *) (p :: T).
[TransferTokens instr p] -> ShowS
showList :: [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
$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
/= :: 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
$cfrom :: forall (instr :: [T] -> [T] -> *) (p :: T) x.
TransferTokens instr p -> Rep (TransferTokens instr p) x
from :: forall 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
to :: forall x. Rep (TransferTokens instr p) x -> TransferTokens instr p
Generic)

instance Buildable (Value' instr p) => Buildable (TransferTokens instr p) where
  build :: TransferTokens instr p -> Doc
build TransferTokens {Mutez
GlobalCounter
Value' instr p
Value' instr ('TContract p)
ttTransferArgument :: forall (instr :: [T] -> [T] -> *) (p :: T).
TransferTokens instr p -> Value' instr p
ttAmount :: forall (instr :: [T] -> [T] -> *) (p :: T).
TransferTokens instr p -> Mutez
ttContract :: forall (instr :: [T] -> [T] -> *) (p :: T).
TransferTokens instr p -> Value' instr ('TContract p)
ttCounter :: forall (instr :: [T] -> [T] -> *) (p :: T).
TransferTokens instr p -> GlobalCounter
ttTransferArgument :: Value' instr p
ttAmount :: Mutez
ttContract :: Value' instr ('TContract p)
ttCounter :: GlobalCounter
..} =
    Doc
"Transfer " Doc -> Doc -> Doc
forall b. FromDoc b => Doc -> Doc -> b
+| Mutez
ttAmount Mutez -> Doc -> Doc
forall a b. (Buildable a, FromDoc b) => a -> Doc -> b
|+ Doc
" tokens to " Doc -> Doc -> Doc
forall b. FromDoc b => Doc -> Doc -> b
+| Value' instr ('TContract p) -> Doc
forall (instr :: [T] -> [T] -> *) (arg :: T).
Value' instr ('TContract arg) -> Doc
buildVContract Value' instr ('TContract p)
ttContract Doc -> Doc -> Doc
forall a b. (Buildable a, FromDoc b) => a -> Doc -> b
|+
      Doc
" with parameter " Doc -> Doc -> Doc
forall b. FromDoc b => Doc -> Doc -> b
+| Value' instr p
ttTransferArgument Value' instr p -> Doc -> Doc
forall a b. (Buildable a, FromDoc b) => a -> Doc -> b
|+ Doc
""

data SetDelegate = SetDelegate
  { SetDelegate -> Maybe KeyHash
sdMbKeyHash :: Maybe KeyHash
  , SetDelegate -> GlobalCounter
sdCounter :: GlobalCounter
  } 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
$cshowsPrec :: Int -> SetDelegate -> ShowS
showsPrec :: Int -> SetDelegate -> ShowS
$cshow :: SetDelegate -> String
show :: SetDelegate -> String
$cshowList :: [SetDelegate] -> ShowS
showList :: [SetDelegate] -> ShowS
Show, SetDelegate -> SetDelegate -> Bool
(SetDelegate -> SetDelegate -> Bool)
-> (SetDelegate -> SetDelegate -> Bool) -> Eq SetDelegate
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SetDelegate -> SetDelegate -> Bool
== :: SetDelegate -> SetDelegate -> Bool
$c/= :: SetDelegate -> SetDelegate -> Bool
/= :: 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
$cfrom :: forall x. SetDelegate -> Rep SetDelegate x
from :: forall x. SetDelegate -> Rep SetDelegate x
$cto :: forall x. Rep SetDelegate x -> SetDelegate
to :: forall x. Rep SetDelegate x -> SetDelegate
Generic)

instance NFData SetDelegate

instance Buildable SetDelegate where
  build :: SetDelegate -> Doc
build (SetDelegate Maybe KeyHash
mbDelegate GlobalCounter
_) =
    Doc
"Set delegate to " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> (KeyHash -> Doc) -> Maybe KeyHash -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
"<nobody>" KeyHash -> Doc
forall a. Buildable a => a -> Doc
build Maybe KeyHash
mbDelegate

data CreateContract instr cp st
  = ( forall i o. Show (instr i o)
    , forall i o. Eq (instr i o)
    )
  => CreateContract
  { forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
CreateContract instr cp st -> L1Address
ccOriginator :: L1Address
  , forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
CreateContract instr cp st -> Maybe KeyHash
ccDelegate :: Maybe KeyHash
  , forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
CreateContract instr cp st -> Mutez
ccBalance :: Mutez
  , forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
CreateContract instr cp st -> Value' instr st
ccStorageVal :: Value' instr st
  , forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
CreateContract instr cp st -> Contract' instr cp st
ccContract :: Contract' instr cp st
  , forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
CreateContract instr cp st -> GlobalCounter
ccCounter :: GlobalCounter
  }

instance Buildable (Value' instr st) => Buildable (CreateContract instr cp st) where
  build :: CreateContract instr cp st -> Doc
build CreateContract {Maybe KeyHash
L1Address
Mutez
GlobalCounter
Contract' instr cp st
Value' instr st
ccOriginator :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
CreateContract instr cp st -> L1Address
ccDelegate :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
CreateContract instr cp st -> Maybe KeyHash
ccBalance :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
CreateContract instr cp st -> Mutez
ccStorageVal :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
CreateContract instr cp st -> Value' instr st
ccContract :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
CreateContract instr cp st -> Contract' instr cp st
ccCounter :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
CreateContract instr cp st -> GlobalCounter
ccOriginator :: L1Address
ccDelegate :: Maybe KeyHash
ccBalance :: Mutez
ccStorageVal :: Value' instr st
ccContract :: Contract' instr cp st
ccCounter :: GlobalCounter
..} =
    Doc
"Create a new contract with" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>
    Doc
" delegate " Doc -> Doc -> Doc
forall b. FromDoc b => Doc -> Doc -> b
+| Doc -> (KeyHash -> Doc) -> Maybe KeyHash -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
"<nobody>" KeyHash -> Doc
forall a. Buildable a => a -> Doc
build Maybe KeyHash
ccDelegate Doc -> Doc -> Doc
forall a b. (Buildable a, FromDoc b) => a -> Doc -> b
|+
    Doc
", balance = " Doc -> Doc -> Doc
forall b. FromDoc b => Doc -> Doc -> b
+| Mutez
ccBalance Mutez -> Doc -> Doc
forall a b. (Buildable a, FromDoc b) => a -> Doc -> b
|+
    Doc
" and storage =" Doc -> Doc -> Doc
forall b. FromDoc b => Doc -> Doc -> b
+| Value' instr st
ccStorageVal Value' instr st -> Doc -> Doc
forall a b. (Buildable a, FromDoc b) => a -> Doc -> b
|+ Doc
""

deriving stock instance Show (CreateContract instr cp st)
deriving stock instance Eq (CreateContract instr cp st)

data Emit instr t = PackedValScope t => Emit
  { forall (instr :: [T] -> [T] -> *) (t :: T). Emit instr t -> Text
emTag :: Text
  , forall (instr :: [T] -> [T] -> *) (t :: T). Emit instr t -> Notes t
emNotes :: Notes t
  , forall (instr :: [T] -> [T] -> *) (t :: T).
Emit instr t -> Value' instr t
emValue :: Value' instr t
  , forall (instr :: [T] -> [T] -> *) (t :: T).
Emit instr t -> GlobalCounter
emCounter :: GlobalCounter
  }

deriving stock instance Show (Emit instr t)
deriving stock instance Eq (Emit instr t)

instance Buildable (Value' instr t) => Buildable (Emit instr t) where
  build :: Emit instr t -> Doc
build Emit{Text
GlobalCounter
Notes t
Value' instr t
emTag :: forall (instr :: [T] -> [T] -> *) (t :: T). Emit instr t -> Text
emNotes :: forall (instr :: [T] -> [T] -> *) (t :: T). Emit instr t -> Notes t
emValue :: forall (instr :: [T] -> [T] -> *) (t :: T).
Emit instr t -> Value' instr t
emCounter :: forall (instr :: [T] -> [T] -> *) (t :: T).
Emit instr t -> GlobalCounter
emTag :: Text
emNotes :: Notes t
emValue :: Value' instr t
emCounter :: GlobalCounter
..} = Doc
"Emit contract event with tag " Doc -> Doc -> Doc
forall b. FromDoc b => Doc -> Doc -> b
+| Text
emTag Text -> Doc -> Doc
forall a b. (Buildable a, FromDoc b) => a -> Doc -> b
|+ Doc
", type " Doc -> Doc -> Doc
forall b. FromDoc b => Doc -> Doc -> b
+| Notes t
emNotes Notes t -> Doc -> Doc
forall a b. (Buildable a, FromDoc b) => a -> Doc -> b
|+
    Doc
" and payload " Doc -> Doc -> Doc
forall b. FromDoc b => Doc -> Doc -> b
+| Value' instr t
emValue Value' instr t -> Doc -> Doc
forall a b. (Buildable a, FromDoc b) => a -> Doc -> b
|+ Doc
""

-- | Wrapper over instruction which remembers whether this instruction
-- always fails or not.
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

-- | Ignoring distinction between constructors here, comparing only semantics.
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 = 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 {k} (instr :: k -> k -> *) (i1 :: k) (i2 :: k) (i3 :: k)
       (o :: k).
(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)

-- | Get code disregard whether it always fails or not.
rfAnyInstr :: RemFail instr i o -> instr i o
rfAnyInstr :: forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
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

-- | Modify inner code.
rfMapAnyInstr
  :: (forall o'. instr i1 o' -> instr i2 o')
  -> RemFail instr i1 o
  -> RemFail instr i2 o
rfMapAnyInstr :: forall {k} (instr :: k -> k -> *) (i1 :: k) (i2 :: k) (o :: k).
(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

tcompare :: forall t instr. Comparable t => (Value' instr t) -> (Value' instr t) -> Ordering
tcompare :: forall (t :: T) (instr :: [T] -> [T] -> *).
Comparable t =>
Value' instr t -> Value' instr t -> 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
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
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
tcompare Value' instr t
VUnit Value' instr t
VUnit = Ordering
EQ
tcompare (VInt Integer
a) (VInt Integer
b) = Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Integer
a Integer
b
tcompare (VNat Natural
a) (VNat Natural
b) = Natural -> Natural -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Natural
a Natural
b
tcompare (VString MText
a) (VString MText
b) = MText -> MText -> Ordering
forall a. Ord a => a -> a -> Ordering
compare MText
a MText
b
tcompare (VBytes ByteString
a) (VBytes ByteString
b) = ByteString -> ByteString -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ByteString
a ByteString
b
tcompare (VMutez Mutez
a) (VMutez Mutez
b) = Mutez -> Mutez -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Mutez
a Mutez
b
tcompare (VBool Bool
a) (VBool Bool
b) = Bool -> Bool -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Bool
a Bool
b
tcompare (VKeyHash KeyHash
a) (VKeyHash KeyHash
b) = KeyHash -> KeyHash -> Ordering
forall a. Ord a => a -> a -> Ordering
compare KeyHash
a KeyHash
b
tcompare (VTimestamp Timestamp
a) (VTimestamp Timestamp
b) = Timestamp -> Timestamp -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Timestamp
a Timestamp
b
tcompare (VAddress EpAddress
a) (VAddress EpAddress
b) = EpAddress -> EpAddress -> Ordering
forall a. Ord a => a -> a -> Ordering
compare EpAddress
a EpAddress
b
tcompare (VChainId ChainId
a) (VChainId ChainId
b) = ChainId -> ChainId -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ChainId
a ChainId
b
tcompare (VSignature Signature
a) (VSignature Signature
b) = Signature -> Signature -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Signature
a Signature
b
tcompare (VKey PublicKey
a) (VKey PublicKey
b) = PublicKey -> PublicKey -> Ordering
forall a. Ord a => a -> a -> Ordering
compare PublicKey
a PublicKey
b

instance (Comparable t) => Ord (Value' instr t) where
  compare :: Value' instr t -> Value' instr t -> Ordering
compare = forall (t :: T) (instr :: [T] -> [T] -> *).
Comparable t =>
Value' instr t -> Value' instr t -> Ordering
tcompare @t

{- | Representation of a Michelson value.

Since values (i.e. lambdas, operations) can include instructions, this type
depends on the type used to represent instructions, which is the parameter
@instr@. It is itself a polymorphic type, parametrized by the Michelson types of
its input and output stacks.

The primary motivator for polymorphism is breaking cyclic dependencies between
this module and "Morley.Michelson.Typed.Instr". In principle @instr@ can also be
used as an extension point, but at the time of writing it isn't used as such, it
is always eventually unified with @Instr@.

@t@ is the value's Michelson type.
-}
type Value' :: ([T] -> [T] -> Type) -> T -> Type
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.
       Comparable t
    => Set (Value' instr t) -> Value' instr ('TSet t)
  VOp
    :: Operation' instr -> Value' instr 'TOperation
  VContract
    :: forall arg instr.
       (SingI arg, ForbidOp 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)
    => LambdaCode' instr inp out
    -> Value' instr ('TLambda inp out)
  VMap
    :: forall k v instr.
       (SingI v, Comparable k)
    => Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
  VBigMap
    :: forall k v instr.
       (SingI v, Comparable k, ForbidBigMap v)
    => Maybe Natural -- ^ The big_map's ID. This is only used in the interpreter.
    -> 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
  VChest      :: Chest -> Value' instr 'TChest
  VChestKey   :: ChestKey -> Value' instr 'TChestKey

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

{- | Code of a lambda value, either recursive or non-recursive.

Note the quantified constraints on the constructors. We opt to carry those here
and not on the respective instances for the sake of simplifying downstream
instance definitions. Constraining each instance with quantified constraints
gets very long-winded very fast, and it wouldn't work with 'deriveGADTNFData'.
-}
data LambdaCode' instr inp out where
  LambdaCode
    :: ( 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 ': '[])
    -> LambdaCode' instr inp out
  LambdaCodeRec
    :: ( forall i o. Show (instr i o)
       , forall i o. Eq (instr i o)
       , forall i o. NFData (instr i o))
    => RemFail instr (inp ': 'TLambda inp out ': '[]) (out ': '[])
    -> LambdaCode' instr inp out

deriving stock instance Show (LambdaCode' instr inp out)
deriving stock instance Eq (LambdaCode' instr inp out)

instance GEq (Value' instr) where
  geq :: forall (a :: T) (b :: T).
Value' instr a -> Value' instr b -> Maybe (a :~: b)
geq Value' instr a
l Value' instr b
r = Value' instr a -> Value' instr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing, Eq (f b)) =>
f a -> f b -> Maybe (a :~: b)
geqI Value' instr a
l Value' instr b
r (SingI a => Maybe (a :~: b)) -> Dict (SingI a) -> Maybe (a :~: b)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Value' instr a -> Dict (SingI a)
forall (instr :: [T] -> [T] -> *) (t :: T).
Value' instr t -> Dict (SingI t)
valueTypeSanity Value' instr a
l (SingI b => Maybe (a :~: b)) -> Dict (SingI b) -> Maybe (a :~: b)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Value' instr b -> Dict (SingI b)
forall (instr :: [T] -> [T] -> *) (t :: T).
Value' instr t -> Dict (SingI t)
valueTypeSanity Value' instr b
r

-- | Make value of @contract@ type which refers to the given address and
-- does not call any entrypoint.
addressToVContract
  :: forall t instr kind.
      (ParameterScope t, ForbidOr t)
  => KindedAddress kind -> Value' instr ('TContract t)
addressToVContract :: forall (t :: T) (instr :: [T] -> [T] -> *) (kind :: AddressKind).
(ParameterScope t, ForbidOr t) =>
KindedAddress kind -> Value' instr ('TContract t)
addressToVContract KindedAddress kind
addr = Address -> SomeEntrypointCallT t -> Value' instr ('TContract t)
forall (t :: T) (instr :: [T] -> [T] -> *).
(SingI t, ForbidOp t) =>
Address -> SomeEntrypointCallT t -> Value' instr ('TContract t)
VContract (KindedAddress kind -> Address
forall (kind :: AddressKind). KindedAddress kind -> Address
MkAddress KindedAddress kind
addr) SomeEntrypointCallT t
forall (t :: T).
(ParameterScope t, ForbidOr t) =>
SomeEntrypointCallT t
sepcPrimitive

buildVContract :: Value' instr ('TContract arg) -> Doc
buildVContract :: forall (instr :: [T] -> [T] -> *) (arg :: T).
Value' instr ('TContract arg) -> Doc
buildVContract = \case
  VContract Address
addr SomeEntrypointCallT arg
epc -> Doc
"Contract " Doc -> Doc -> Doc
forall b. FromDoc b => Doc -> Doc -> b
+| Address
addr Address -> Doc -> Doc
forall a b. (Buildable a, FromDoc b) => a -> Doc -> b
|+ Doc
" call " Doc -> Doc -> Doc
forall b. FromDoc b => Doc -> Doc -> b
+| SomeEntrypointCallT arg
epc SomeEntrypointCallT arg -> Doc -> Doc
forall a b. (Buildable a, FromDoc b) => a -> Doc -> b
|+ Doc
""

-- | Turn 'EpLiftSequence' into actual function on t'Morley.Michelson.Typed.Aliases.Value's.
compileEpLiftSequence
  :: EpLiftSequence arg param
  -> Value' instr arg
  -> Value' instr param
compileEpLiftSequence :: forall (arg :: T) (param :: T) (instr :: [T] -> [T] -> *).
EpLiftSequence arg param -> Value' instr arg -> Value' instr param
compileEpLiftSequence = \case
  EpLiftSequence arg param
EplArgHere -> Value' instr arg -> Value' instr arg
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 param
Either (Value' instr subparam) (Value' instr r)
-> Value' instr ('TOr subparam r)
forall (t :: T) (v :: T) (instr :: [T] -> [T] -> *).
(SingI t, SingI v) =>
Either (Value' instr t) (Value' instr v) -> Value' instr ('TOr t v)
VOr (Either (Value' instr subparam) (Value' instr r)
 -> Value' instr param)
-> (Value' instr arg
    -> Either (Value' instr subparam) (Value' instr r))
-> Value' instr arg
-> Value' instr param
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 param
Either (Value' instr l) (Value' instr subparam)
-> Value' instr ('TOr l subparam)
forall (t :: T) (v :: T) (instr :: [T] -> [T] -> *).
(SingI t, SingI v) =>
Either (Value' instr t) (Value' instr v) -> Value' instr ('TOr t v)
VOr (Either (Value' instr l) (Value' instr subparam)
 -> Value' instr param)
-> (Value' instr arg
    -> Either (Value' instr l) (Value' instr subparam))
-> Value' instr arg
-> Value' instr param
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 :: forall (param :: T) (arg :: T) (instr :: [T] -> [T] -> *).
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)

-- | 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 (SingI t)
valueTypeSanity :: forall (instr :: [T] -> [T] -> *) (t :: T).
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
  VChest{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict
  VChestKey{} -> Dict (SingI t)
forall (a :: Constraint). a => Dict a
Dict

mkVLam
  :: ( 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)
     )
  => (IsNotInView => RemFail instr '[inp] '[out])
  -> Value' instr ('TLambda inp out)
mkVLam :: forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(SingI inp, SingI out,
 forall (i :: [T]) (o :: [T]). Show (instr i o),
 forall (i :: [T]) (o :: [T]). Eq (instr i o),
 forall (i :: [T]) (o :: [T]). NFData (instr i o)) =>
(IsNotInView => RemFail instr '[inp] '[out])
-> Value' instr ('TLambda inp out)
mkVLam IsNotInView => RemFail instr '[inp] '[out]
rf = LambdaCode' instr inp out -> Value' instr ('TLambda inp out)
forall (t :: T) (v :: T) (instr :: [T] -> [T] -> *).
(SingI t, SingI v) =>
LambdaCode' instr t v -> Value' instr ('TLambda t v)
VLam (LambdaCode' instr inp out -> Value' instr ('TLambda inp out))
-> (RemFail instr '[inp] '[out] -> LambdaCode' instr inp out)
-> RemFail instr '[inp] '[out]
-> Value' instr ('TLambda inp out)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RemFail instr '[inp] '[out] -> LambdaCode' instr inp out
forall (instr :: [T] -> [T] -> *) (inp :: T) (out :: T).
(forall (i :: [T]) (o :: [T]). Show (instr i o),
 forall (i :: [T]) (o :: [T]). Eq (instr i o),
 forall (i :: [T]) (o :: [T]). NFData (instr i o)) =>
RemFail instr '[inp] '[out] -> LambdaCode' instr inp out
LambdaCode (RemFail instr '[inp] '[out] -> Value' instr ('TLambda inp out))
-> RemFail instr '[inp] '[out] -> Value' instr ('TLambda inp out)
forall a b. (a -> b) -> a -> b
$ (IsNotInView => RemFail instr '[inp] '[out])
-> RemFail instr '[inp] '[out]
forall r. (IsNotInView => r) -> r
giveNotInView RemFail instr '[inp] '[out]
IsNotInView => RemFail instr '[inp] '[out]
rf

mkVLamRec
  :: ( 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)
     )
  => (IsNotInView => RemFail instr '[inp, 'TLambda inp out] '[out])
  -> Value' instr ('TLambda inp out)
mkVLamRec :: forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(SingI inp, SingI out,
 forall (i :: [T]) (o :: [T]). Show (instr i o),
 forall (i :: [T]) (o :: [T]). Eq (instr i o),
 forall (i :: [T]) (o :: [T]). NFData (instr i o)) =>
(IsNotInView => RemFail instr '[inp, 'TLambda inp out] '[out])
-> Value' instr ('TLambda inp out)
mkVLamRec IsNotInView => RemFail instr '[inp, 'TLambda inp out] '[out]
rf = LambdaCode' instr inp out -> Value' instr ('TLambda inp out)
forall (t :: T) (v :: T) (instr :: [T] -> [T] -> *).
(SingI t, SingI v) =>
LambdaCode' instr t v -> Value' instr ('TLambda t v)
VLam (LambdaCode' instr inp out -> Value' instr ('TLambda inp out))
-> (RemFail instr '[inp, 'TLambda inp out] '[out]
    -> LambdaCode' instr inp out)
-> RemFail instr '[inp, 'TLambda inp out] '[out]
-> Value' instr ('TLambda inp out)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RemFail instr '[inp, 'TLambda inp out] '[out]
-> LambdaCode' instr inp out
forall (instr :: [T] -> [T] -> *) (inp :: T) (out :: T).
(forall (i :: [T]) (o :: [T]). Show (instr i o),
 forall (i :: [T]) (o :: [T]). Eq (instr i o),
 forall (i :: [T]) (o :: [T]). NFData (instr i o)) =>
RemFail instr '[inp, 'TLambda inp out] '[out]
-> LambdaCode' instr inp out
LambdaCodeRec (RemFail instr '[inp, 'TLambda inp out] '[out]
 -> Value' instr ('TLambda inp out))
-> RemFail instr '[inp, 'TLambda inp out] '[out]
-> Value' instr ('TLambda inp out)
forall a b. (a -> b) -> a -> b
$ (IsNotInView => RemFail instr '[inp, 'TLambda inp out] '[out])
-> RemFail instr '[inp, 'TLambda inp out] '[out]
forall r. (IsNotInView => r) -> r
giveNotInView RemFail instr '[inp, 'TLambda inp out] '[out]
IsNotInView => RemFail instr '[inp, 'TLambda inp out] '[out]
rf

-- | Provide a witness of that value's type is known.
withValueTypeSanity :: Value' instr t -> (SingI t => a) -> a
withValueTypeSanity :: forall (instr :: [T] -> [T] -> *) (t :: T) a.
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

-- | Extended values comparison - it does not require t'Morley.Michelson.Typed.Aliases.Value's to be
-- of the same type, only their content to match.
eqValueExt :: Value' instr t1 -> Value' instr t2 -> Bool
eqValueExt :: forall (instr :: [T] -> [T] -> *) (t1 :: T) (t2 :: T).
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

mconcat [[d|
  instance
    ( forall i o. NFData (instr i o)
    ) => NFData (CreateContract instr cp st) where
    rnf (CreateContract a b c d e f) = rnf (a, b, c, d, e, f)
  |]
  , deriveGADTNFData ''Operation'
  , deriveGADTNFData ''Value'
  , deriveGADTNFData ''LambdaCode'
  ]

instance NFData (Emit instr t) where
  rnf :: Emit instr t -> ()
rnf (Emit Text
a Notes t
b Value' instr t
c GlobalCounter
d) =
    Text -> ()
forall a. NFData a => a -> ()
rnf Text
a () -> () -> ()
forall a b. a -> b -> b
`seq` Notes t -> ()
forall a. NFData a => a -> ()
rnf Notes t
b () -> () -> ()
forall a b. a -> b -> b
`seq` Value' instr t -> ()
forall a. NFData a => a -> ()
rnf Value' instr t
c () -> () -> ()
forall a b. a -> b -> b
`seq` GlobalCounter -> ()
forall a. NFData a => a -> ()
rnf GlobalCounter
d

instance NFData (TransferTokens instr p)

type instance Index (Value' _ ('TList _)) = Int
type instance IxValue (Value' instr ('TList elem)) = Value' instr elem
instance Ixed (Value' instr ('TList elem)) where
  ix :: Index (Value' instr ('TList elem))
-> Traversal'
     (Value' instr ('TList elem)) (IxValue (Value' instr ('TList elem)))
ix Index (Value' instr ('TList elem))
idx IxValue (Value' instr ('TList elem))
-> f (IxValue (Value' instr ('TList elem)))
handler (VList [Value' instr t]
xs) = [Value' instr elem] -> Value' instr ('TList elem)
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
[Value' instr t] -> Value' instr ('TList t)
VList ([Value' instr elem] -> Value' instr ('TList elem))
-> f [Value' instr elem] -> f (Value' instr ('TList elem))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Index [Value' instr elem]
-> Traversal' [Value' instr elem] (IxValue [Value' instr elem])
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index [Value' instr elem]
Index (Value' instr ('TList elem))
idx IxValue [Value' instr elem] -> f (IxValue [Value' instr elem])
IxValue (Value' instr ('TList elem))
-> f (IxValue (Value' instr ('TList elem)))
handler [Value' instr elem]
[Value' instr t]
xs

type instance Index (Value' instr ('TMap k _)) = Value' instr k
type instance IxValue (Value' instr ('TMap _ v)) = Value' instr v
instance Ixed (Value' instr ('TMap k v))
instance At (Value' instr ('TMap k v)) where
  at :: Index (Value' instr ('TMap k v))
-> Lens'
     (Value' instr ('TMap k v))
     (Maybe (IxValue (Value' instr ('TMap k v))))
at Index (Value' instr ('TMap k v))
key Maybe (IxValue (Value' instr ('TMap k v)))
-> f (Maybe (IxValue (Value' instr ('TMap k v))))
handler (VMap Map (Value' instr k) (Value' instr v)
vmap) = Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
forall (t :: T) (v :: T) (instr :: [T] -> [T] -> *).
(SingI v, Comparable t) =>
Map (Value' instr t) (Value' instr v) -> Value' instr ('TMap t v)
VMap (Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v))
-> f (Map (Value' instr k) (Value' instr v))
-> f (Value' instr ('TMap k v))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Index (Map (Value' instr k) (Value' instr v))
-> Lens'
     (Map (Value' instr k) (Value' instr v))
     (Maybe (IxValue (Map (Value' instr k) (Value' instr v))))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index (Map (Value' instr k) (Value' instr v))
Index (Value' instr ('TMap k v))
key Maybe (IxValue (Map (Value' instr k) (Value' instr v)))
-> f (Maybe (IxValue (Map (Value' instr k) (Value' instr v))))
Maybe (IxValue (Value' instr ('TMap k v)))
-> f (Maybe (IxValue (Value' instr ('TMap k v))))
handler Map (Value' instr k) (Value' instr v)
Map (Value' instr k) (Value' instr v)
vmap

type instance Index (Value' instr ('TBigMap k _)) = Value' instr k
type instance IxValue (Value' instr ('TBigMap _ v)) = Value' instr v
instance Ixed (Value' instr ('TBigMap k v))
instance At (Value' instr ('TBigMap k v)) where
  at :: Index (Value' instr ('TBigMap k v))
-> Lens'
     (Value' instr ('TBigMap k v))
     (Maybe (IxValue (Value' instr ('TBigMap k v))))
at Index (Value' instr ('TBigMap k v))
key Maybe (IxValue (Value' instr ('TBigMap k v)))
-> f (Maybe (IxValue (Value' instr ('TBigMap k v))))
handler (VBigMap Maybe Natural
bmid Map (Value' instr k) (Value' instr v)
bmap) = Maybe Natural
-> Map (Value' instr k) (Value' instr v)
-> Value' instr ('TBigMap k v)
forall (t :: T) (v :: T) (instr :: [T] -> [T] -> *).
(SingI v, Comparable t, ForbidBigMap v) =>
Maybe Natural
-> Map (Value' instr t) (Value' instr v)
-> Value' instr ('TBigMap t v)
VBigMap Maybe Natural
bmid (Map (Value' instr k) (Value' instr v)
 -> Value' instr ('TBigMap k v))
-> f (Map (Value' instr k) (Value' instr v))
-> f (Value' instr ('TBigMap k v))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Index (Map (Value' instr k) (Value' instr v))
-> Lens'
     (Map (Value' instr k) (Value' instr v))
     (Maybe (IxValue (Map (Value' instr k) (Value' instr v))))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index (Map (Value' instr k) (Value' instr v))
Index (Value' instr ('TBigMap k v))
key Maybe (IxValue (Map (Value' instr k) (Value' instr v)))
-> f (Maybe (IxValue (Map (Value' instr k) (Value' instr v))))
Maybe (IxValue (Value' instr ('TBigMap k v)))
-> f (Maybe (IxValue (Value' instr ('TBigMap k v))))
handler Map (Value' instr k) (Value' instr v)
Map (Value' instr k) (Value' instr v)
bmap

type instance Index (Value' instr ('TSet a)) = Value' instr a
type instance IxValue (Value' _ ('TSet _)) = ()
instance Ixed (Value' instr ('TSet a))
instance At (Value' instr ('TSet a)) where
  at :: Index (Value' instr ('TSet a))
-> Lens'
     (Value' instr ('TSet a)) (Maybe (IxValue (Value' instr ('TSet a))))
at Index (Value' instr ('TSet a))
key Maybe (IxValue (Value' instr ('TSet a)))
-> f (Maybe (IxValue (Value' instr ('TSet a))))
handler (VSet Set (Value' instr t)
vset) = Set (Value' instr a) -> Value' instr ('TSet a)
forall (t :: T) (instr :: [T] -> [T] -> *).
Comparable t =>
Set (Value' instr t) -> Value' instr ('TSet t)
VSet (Set (Value' instr a) -> Value' instr ('TSet a))
-> f (Set (Value' instr a)) -> f (Value' instr ('TSet a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Index (Set (Value' instr a))
-> Lens'
     (Set (Value' instr a)) (Maybe (IxValue (Set (Value' instr a))))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index (Set (Value' instr a))
Index (Value' instr ('TSet a))
key Maybe (IxValue (Set (Value' instr a)))
-> f (Maybe (IxValue (Set (Value' instr a))))
Maybe (IxValue (Value' instr ('TSet a)))
-> f (Maybe (IxValue (Value' instr ('TSet a))))
handler Set (Value' instr a)
Set (Value' instr t)
vset