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

{-# OPTIONS_GHC -Wno-orphans #-}

module Morley.Michelson.Typed.Convert
  ( convertParamNotes
  , convertView
  , convertSomeView
  , convertContractCode
  , convertContractCodeOptimized
  , convertContract
  , convertContractOptimized
  , instrToOps
  , instrToOpsOptimized
  , untypeDemoteT
  , untypeValue
  , untypeValueHashable
  , untypeValueOptimized

  -- Helper for generating documentation
  , sampleTypedValue

  -- * Misc
  , flattenEntrypoints
  , U.HandleImplicitDefaultEp(..)
  , eqInstrExt
  ) where

import Data.ByteArray qualified as ByteArray
import Data.Constraint (Dict(..), (\\))
import Data.Default (def)
import Data.List.NonEmpty ((<|))
import Data.Map qualified as Map
import Data.Singletons (Sing, demote)
import Fmt (Buildable(..), Doc, fmt, listF, pretty)
import Unsafe qualified (fromIntegral)

import Morley.Michelson.Printer.Util
import Morley.Michelson.Text
import Morley.Michelson.Typed.Aliases
import Morley.Michelson.Typed.Annotation (annotateInstr, mkUType)
import Morley.Michelson.Typed.Contract
import Morley.Michelson.Typed.Entrypoints
import Morley.Michelson.Typed.Extract (toUType)
import Morley.Michelson.Typed.Instr as Instr
import Morley.Michelson.Typed.Scope
import Morley.Michelson.Typed.Sing (SingT(..))
import Morley.Michelson.Typed.T (T(..))
import Morley.Michelson.Typed.Value
import Morley.Michelson.Typed.View
import Morley.Michelson.Untyped qualified as U
import Morley.Michelson.Untyped.Annotation (Annotation(unAnnotation))
import Morley.Tezos.Address
import Morley.Tezos.Core
  (ChainId(unChainId), mformatChainId, parseChainId, timestampFromSeconds, timestampToSeconds, tz,
  unMutez)
import Morley.Tezos.Crypto
import Morley.Tezos.Crypto.BLS12381 qualified as BLS
import Morley.Tezos.Crypto.Timelock (chestBytes, chestKeyBytes)
import Morley.Util.PeanoNatural (fromPeanoNatural, singPeanoVal)
import Morley.Util.Sing (eqParamSing)

-- | Convert typed parameter annotations to an untyped 'U.ParameterType'.
convertParamNotes :: ParamNotes cp -> U.ParameterType
convertParamNotes :: forall (cp :: T). ParamNotes cp -> ParameterType
convertParamNotes (ParamNotes Notes cp
notes RootAnn
rootAnn) =
  Ty -> RootAnn -> ParameterType
U.ParameterType (Notes cp -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes cp
notes) RootAnn
rootAnn

-- | Convert typed t'ContractCode' to an untyped t'U.Contract'.
convertContractCode
  :: forall param store . (SingI param, SingI store)
  => ContractCode param store -> U.Contract
convertContractCode :: forall (param :: T) (store :: T).
(SingI param, SingI store) =>
ContractCode param store -> Contract
convertContractCode = UntypingOptions -> ContractCode param store -> Contract
forall (param :: T) (store :: T).
(SingI param, SingI store) =>
UntypingOptions -> ContractCode param store -> Contract
convertContractCode' UntypingOptions
Readable

-- | Convert typed t'ContractCode' to an untyped t'U.Contract' using optimized
-- representation.
convertContractCodeOptimized
  :: forall param store . (SingI param, SingI store)
  => ContractCode param store -> U.Contract
convertContractCodeOptimized :: forall (param :: T) (store :: T).
(SingI param, SingI store) =>
ContractCode param store -> Contract
convertContractCodeOptimized = UntypingOptions -> ContractCode param store -> Contract
forall (param :: T) (store :: T).
(SingI param, SingI store) =>
UntypingOptions -> ContractCode param store -> Contract
convertContractCode' UntypingOptions
Optimized

convertContractCode'
  :: forall param store . (SingI param, SingI store)
  => UntypingOptions -> ContractCode param store -> U.Contract
convertContractCode' :: forall (param :: T) (store :: T).
(SingI param, SingI store) =>
UntypingOptions -> ContractCode param store -> Contract
convertContractCode' UntypingOptions
opts ContractCode param store
contract =
  U.Contract
    { contractParameter :: ParameterType
contractParameter = Ty -> RootAnn -> ParameterType
U.ParameterType (forall (t :: T). SingI t => Ty
untypeDemoteT @param) RootAnn
forall {k} (a :: k). Annotation a
U.noAnn
    , contractStorage :: Ty
contractStorage = forall (t :: T). SingI t => Ty
untypeDemoteT @store
    , contractCode :: ExpandedOp
contractCode = [ExpandedOp] -> ExpandedOp
seqOrSingleOp ([ExpandedOp] -> ExpandedOp) -> [ExpandedOp] -> ExpandedOp
forall a b. (a -> b) -> a -> b
$ UntypingOptions
-> Instr (ContractInp param store) (ContractOut store)
-> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts (Instr (ContractInp param store) (ContractOut store)
 -> [ExpandedOp])
-> Instr (ContractInp param store) (ContractOut store)
-> [ExpandedOp]
forall a b. (a -> b) -> a -> b
$ ContractCode param store
-> Instr (ContractInp param store) (ContractOut store)
forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
ContractCode' instr cp st
-> instr (ContractInp cp st) (ContractOut st)
unContractCode ContractCode param store
contract
    , entriesOrder :: EntriesOrder
entriesOrder = EntriesOrder
U.canonicalEntriesOrder
    , contractViews :: ViewsSet ExpandedOp
contractViews = ViewsSet ExpandedOp
forall a. Default a => a
def
    }

convertView :: forall arg store ret. View arg store ret -> U.View
convertView :: forall (arg :: T) (store :: T) (ret :: T).
View arg store ret -> View
convertView = UntypingOptions -> View arg store ret -> View
forall (arg :: T) (store :: T) (ret :: T).
UntypingOptions -> View arg store ret -> View
convertView' UntypingOptions
Readable

convertView' :: forall arg store ret. UntypingOptions -> View arg store ret -> U.View
convertView' :: forall (arg :: T) (store :: T) (ret :: T).
UntypingOptions -> View arg store ret -> View
convertView' UntypingOptions
opts View{ViewName
Notes arg
Notes ret
ViewCode' Instr arg store ret
vName :: ViewName
vArgument :: Notes arg
vReturn :: Notes ret
vCode :: ViewCode' Instr arg store ret
vName :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> ViewName
vArgument :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> Notes arg
vReturn :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> Notes ret
vCode :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> ViewCode' instr arg st ret
..} =
  U.View
    { viewName :: ViewName
viewName = ViewName
vName
    , viewArgument :: Ty
viewArgument = forall (t :: T). SingI t => Ty
untypeDemoteT @arg
    , viewReturn :: Ty
viewReturn = forall (t :: T). SingI t => Ty
untypeDemoteT @ret
    , viewCode :: ExpandedOp
viewCode = [ExpandedOp] -> ExpandedOp
seqOrSingleOp ([ExpandedOp] -> ExpandedOp) -> [ExpandedOp] -> ExpandedOp
forall a b. (a -> b) -> a -> b
$ UntypingOptions -> ViewCode' Instr arg store ret -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts ViewCode' Instr arg store ret
vCode
    }

seqOrSingleOp :: [U.ExpandedOp] -> U.ExpandedOp
seqOrSingleOp :: [ExpandedOp] -> ExpandedOp
seqOrSingleOp = \case
  [ExpandedOp
x] -> ExpandedOp
x
  [ExpandedOp]
xs -> [ExpandedOp] -> ExpandedOp
U.SeqEx [ExpandedOp]
xs

convertSomeView :: SomeView st -> U.View
convertSomeView :: forall (st :: T). SomeView st -> View
convertSomeView = UntypingOptions -> SomeView st -> View
forall (st :: T). UntypingOptions -> SomeView st -> View
convertSomeView' UntypingOptions
Readable

convertSomeView' :: UntypingOptions -> SomeView st -> U.View
convertSomeView' :: forall (st :: T). UntypingOptions -> SomeView st -> View
convertSomeView' UntypingOptions
opts (SomeView View' Instr arg st ret
v) = UntypingOptions -> View' Instr arg st ret -> View
forall (arg :: T) (store :: T) (ret :: T).
UntypingOptions -> View arg store ret -> View
convertView' UntypingOptions
opts View' Instr arg st ret
v

-- | Convert typed t'Contract' to an untyped t'U.Contract'.
convertContract :: Contract param store -> U.Contract
convertContract :: forall (param :: T) (store :: T). Contract param store -> Contract
convertContract = UntypingOptions -> Contract param store -> Contract
forall (param :: T) (store :: T).
UntypingOptions -> Contract param store -> Contract
convertContract' UntypingOptions
Readable

-- | Convert typed t'Contract' to untyped t'U.Contract' using optimized
-- representation.
convertContractOptimized :: Contract param store -> U.Contract
convertContractOptimized :: forall (param :: T) (store :: T). Contract param store -> Contract
convertContractOptimized = UntypingOptions -> Contract param store -> Contract
forall (param :: T) (store :: T).
UntypingOptions -> Contract param store -> Contract
convertContract' UntypingOptions
Optimized

convertContract' :: UntypingOptions -> Contract param store -> U.Contract
convertContract' :: forall (param :: T) (store :: T).
UntypingOptions -> Contract param store -> Contract
convertContract' UntypingOptions
opts Contract{EntriesOrder
Notes store
ViewsSet' Instr store
ParamNotes param
ContractCode' Instr param store
cCode :: ContractCode' Instr param store
cParamNotes :: ParamNotes param
cStoreNotes :: Notes store
cViews :: ViewsSet' Instr store
cEntriesOrder :: EntriesOrder
cCode :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
Contract' instr cp st -> ContractCode' instr cp st
cParamNotes :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
Contract' instr cp st -> ParamNotes cp
cStoreNotes :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
Contract' instr cp st -> Notes st
cViews :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
Contract' instr cp st -> ViewsSet' instr st
cEntriesOrder :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
Contract' instr cp st -> EntriesOrder
..} =
  let c :: Contract
c = UntypingOptions -> ContractCode' Instr param store -> Contract
forall (param :: T) (store :: T).
(SingI param, SingI store) =>
UntypingOptions -> ContractCode param store -> Contract
convertContractCode' UntypingOptions
opts ContractCode' Instr param store
cCode
  in Contract
c { contractParameter :: ParameterType
U.contractParameter = ParamNotes param -> ParameterType
forall (cp :: T). ParamNotes cp -> ParameterType
convertParamNotes ParamNotes param
cParamNotes
       , contractStorage :: Ty
U.contractStorage = Notes store -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes store
cStoreNotes
       , entriesOrder :: EntriesOrder
U.entriesOrder = EntriesOrder
cEntriesOrder
       , contractViews :: ViewsSet ExpandedOp
U.contractViews = Map ViewName View -> ViewsSet ExpandedOp
forall instr. Map ViewName (View' instr) -> ViewsSet instr
U.ViewsSet (Map ViewName View -> ViewsSet ExpandedOp)
-> Map ViewName View -> ViewsSet ExpandedOp
forall a b. (a -> b) -> a -> b
$ UntypingOptions -> SomeView store -> View
forall (st :: T). UntypingOptions -> SomeView st -> View
convertSomeView' UntypingOptions
opts (SomeView store -> View)
-> Map ViewName (SomeView store) -> Map ViewName View
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ViewsSet' Instr store -> Map ViewName (SomeView store)
forall (instr :: [T] -> [T] -> *) (st :: T).
ViewsSet' instr st -> Map ViewName (SomeView' instr st)
unViewsSet ViewsSet' Instr store
cViews
       }

-- Note: if you change this type, check 'untypeValueImpl' wildcard patterns.
data UntypingOptions
  = Readable
  -- ^ Convert value to human-readable representation
  | Optimized
  -- ^ Convert value to optimized representation
  | Hashable
  -- ^ Like 'Optimized', but without list notation for pairs.
  -- Created to match @octez-client hash data@ behavior for typed values.
  -- See https://gitlab.com/morley-framework/morley/-/issues/611
  deriving stock (UntypingOptions -> UntypingOptions -> Bool
(UntypingOptions -> UntypingOptions -> Bool)
-> (UntypingOptions -> UntypingOptions -> Bool)
-> Eq UntypingOptions
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UntypingOptions -> UntypingOptions -> Bool
== :: UntypingOptions -> UntypingOptions -> Bool
$c/= :: UntypingOptions -> UntypingOptions -> Bool
/= :: UntypingOptions -> UntypingOptions -> Bool
Eq, Int -> UntypingOptions -> ShowS
[UntypingOptions] -> ShowS
UntypingOptions -> String
(Int -> UntypingOptions -> ShowS)
-> (UntypingOptions -> String)
-> ([UntypingOptions] -> ShowS)
-> Show UntypingOptions
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UntypingOptions -> ShowS
showsPrec :: Int -> UntypingOptions -> ShowS
$cshow :: UntypingOptions -> String
show :: UntypingOptions -> String
$cshowList :: [UntypingOptions] -> ShowS
showList :: [UntypingOptions] -> ShowS
Show)

-- | Convert a typed value to an untyped human-readable representation
untypeValue :: ForbidOp t => Value' Instr t -> U.Value
untypeValue :: forall (t :: T). ForbidOp t => Value' Instr t -> Value
untypeValue = UntypingOptions -> Value' Instr t -> Value
forall (t :: T).
ForbidOp t =>
UntypingOptions -> Value' Instr t -> Value
untypeValueImpl' UntypingOptions
Readable

-- | Like 'untypeValueOptimized', but without list notation for pairs.
--
-- Created to match @octez-client hash data@ behaviour for typed values.
untypeValueHashable :: ForbidOp t => Value' Instr t -> U.Value
untypeValueHashable :: forall (t :: T). ForbidOp t => Value' Instr t -> Value
untypeValueHashable = UntypingOptions -> Value' Instr t -> Value
forall (t :: T).
ForbidOp t =>
UntypingOptions -> Value' Instr t -> Value
untypeValueImpl' UntypingOptions
Hashable

-- | Convert a typed value to an untyped optimized representation
untypeValueOptimized :: ForbidOp t => Value' Instr t -> U.Value
untypeValueOptimized :: forall (t :: T). ForbidOp t => Value' Instr t -> Value
untypeValueOptimized = UntypingOptions -> Value' Instr t -> Value
forall (t :: T).
ForbidOp t =>
UntypingOptions -> Value' Instr t -> Value
untypeValueImpl' UntypingOptions
Optimized

untypeValueImpl'
  :: ForbidOp t
  => UntypingOptions
  -> Value' Instr t
  -> U.Value
untypeValueImpl' :: forall (t :: T).
ForbidOp t =>
UntypingOptions -> Value' Instr t -> Value
untypeValueImpl' UntypingOptions
opts Value' Instr t
val = UntypingOptions -> Sing t -> Value' Instr t -> Value
forall (t :: T).
ForbidOp t =>
UntypingOptions -> Sing t -> Value' Instr t -> Value
untypeValueImpl UntypingOptions
opts (Sing t
SingT t
SingI t => SingT t
forall {k} (a :: k). SingI a => Sing a
sing (SingI t => SingT t) -> Dict (SingI t) -> SingT t
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Value' Instr t -> Dict (SingI t)
forall (instr :: [T] -> [T] -> *) (t :: T).
Value' instr t -> Dict (SingI t)
valueTypeSanity Value' Instr t
val) Value' Instr t
val

-- | Convert a typed t'Morley.Michelson.Typed.Aliases.Value' to an untyped 'Value'.
--
-- For full isomorphism type of the given t'Morley.Michelson.Typed.Aliases.Value' should not contain
-- 'TOperation' - a compile error will be raised otherwise.
-- You can analyse its presence with 'checkTPresence' function.
untypeValueImpl
  :: ForbidOp t
  => UntypingOptions
  -> Sing t
  -> Value' Instr t
  -> U.Value
untypeValueImpl :: forall (t :: T).
ForbidOp t =>
UntypingOptions -> Sing t -> Value' Instr t -> Value
untypeValueImpl UntypingOptions
opts Sing t
sng Value' Instr t
val = case Value' Instr t
val of
  VInt Integer
i -> Integer -> Value
forall {k} (f :: k -> *) (op :: k). Integer -> Value' f op
U.ValueInt Integer
i
  VNat Natural
i -> Integer -> Value
forall {k} (f :: k -> *) (op :: k). Integer -> Value' f op
U.ValueInt (Integer -> Value) -> Integer -> Value
forall a b. (a -> b) -> a -> b
$ Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
i
  VString MText
s -> MText -> Value
forall {k} (f :: k -> *) (op :: k). MText -> Value' f op
U.ValueString MText
s
  VBytes ByteString
b -> InternalByteString -> Value
forall {k} (f :: k -> *) (op :: k).
InternalByteString -> Value' f op
U.ValueBytes (InternalByteString -> Value) -> InternalByteString -> Value
forall a b. (a -> b) -> a -> b
$ ByteString -> InternalByteString
U.InternalByteString ByteString
b
  VMutez Mutez
m -> Integer -> Value
forall {k} (f :: k -> *) (op :: k). Integer -> Value' f op
U.ValueInt (Integer -> Value) -> Integer -> Value
forall a b. (a -> b) -> a -> b
$ Word63 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word63 -> Integer) -> Word63 -> Integer
forall a b. (a -> b) -> a -> b
$ Mutez -> Word63
unMutez Mutez
m
  VBool Bool
True -> Value
forall {k} (f :: k -> *) (op :: k). Value' f op
U.ValueTrue
  VBool Bool
False -> Value
forall {k} (f :: k -> *) (op :: k). Value' f op
U.ValueFalse
  VKeyHash KeyHash
h ->
    case UntypingOptions
opts of
      UntypingOptions
Readable  -> MText -> Value
forall {k} (f :: k -> *) (op :: k). MText -> Value' f op
U.ValueString (MText -> Value) -> MText -> Value
forall a b. (a -> b) -> a -> b
$ KeyHash -> MText
forall (kind :: HashKind). Hash kind -> MText
mformatHash KeyHash
h
      UntypingOptions
_         -> InternalByteString -> Value
forall {k} (f :: k -> *) (op :: k).
InternalByteString -> Value' f op
U.ValueBytes (InternalByteString -> Value) -> InternalByteString -> Value
forall a b. (a -> b) -> a -> b
$ ByteString -> InternalByteString
U.InternalByteString (ByteString -> InternalByteString)
-> ByteString -> InternalByteString
forall a b. (a -> b) -> a -> b
$ KeyHash -> ByteString
forall (kind :: HashKind). Hash kind -> ByteString
hashToBytes KeyHash
h
  VBls12381Fr Bls12381Fr
v ->
    case UntypingOptions
opts of
      UntypingOptions
Readable  -> Integer -> Value
forall {k} (f :: k -> *) (op :: k). Integer -> Value' f op
U.ValueInt (Integer -> Value) -> Integer -> Value
forall a b. (a -> b) -> a -> b
$ Bls12381Fr -> Integer
forall a. Integral a => a -> Integer
toInteger Bls12381Fr
v
      UntypingOptions
_         -> InternalByteString -> Value
forall {k} (f :: k -> *) (op :: k).
InternalByteString -> Value' f op
U.ValueBytes (InternalByteString -> Value)
-> (ByteString -> InternalByteString) -> ByteString -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> InternalByteString
U.InternalByteString (ByteString -> Value) -> ByteString -> Value
forall a b. (a -> b) -> a -> b
$ Bls12381Fr -> ByteString
forall a. CurveObject a => a -> ByteString
BLS.toMichelsonBytes Bls12381Fr
v
  VBls12381G1 Bls12381G1
v ->
    InternalByteString -> Value
forall {k} (f :: k -> *) (op :: k).
InternalByteString -> Value' f op
U.ValueBytes (InternalByteString -> Value)
-> (ByteString -> InternalByteString) -> ByteString -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> InternalByteString
U.InternalByteString (ByteString -> Value) -> ByteString -> Value
forall a b. (a -> b) -> a -> b
$ Bls12381G1 -> ByteString
forall a. CurveObject a => a -> ByteString
BLS.toMichelsonBytes Bls12381G1
v
  VBls12381G2 Bls12381G2
v ->
    InternalByteString -> Value
forall {k} (f :: k -> *) (op :: k).
InternalByteString -> Value' f op
U.ValueBytes (InternalByteString -> Value)
-> (ByteString -> InternalByteString) -> ByteString -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> InternalByteString
U.InternalByteString (ByteString -> Value) -> ByteString -> Value
forall a b. (a -> b) -> a -> b
$ Bls12381G2 -> ByteString
forall a. CurveObject a => a -> ByteString
BLS.toMichelsonBytes Bls12381G2
v
  VTimestamp Timestamp
t ->
    case UntypingOptions
opts of
      UntypingOptions
Readable   -> MText -> Value
forall {k} (f :: k -> *) (op :: k). MText -> Value' f op
U.ValueString (MText -> Value) -> (Text -> MText) -> Text -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either Text MText -> MText
forall a b. (HasCallStack, Buildable a) => Either a b -> b
unsafe (Either Text MText -> MText)
-> (Text -> Either Text MText) -> Text -> MText
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Either Text MText
mkMText (Text -> Value) -> Text -> Value
forall a b. (a -> b) -> a -> b
$ Timestamp -> Text
forall a b. (Buildable a, FromDoc b) => a -> b
pretty Timestamp
t
      UntypingOptions
_          -> Integer -> Value
forall {k} (f :: k -> *) (op :: k). Integer -> Value' f op
U.ValueInt (Integer -> Value) -> Integer -> Value
forall a b. (a -> b) -> a -> b
$ Timestamp -> Integer
forall a. Integral a => Timestamp -> a
timestampToSeconds Timestamp
t
  VAddress EpAddress
a ->
    case UntypingOptions
opts of
      UntypingOptions
Readable  -> MText -> Value
forall {k} (f :: k -> *) (op :: k). MText -> Value' f op
U.ValueString (MText -> Value) -> MText -> Value
forall a b. (a -> b) -> a -> b
$ EpAddress -> MText
mformatEpAddress EpAddress
a
      UntypingOptions
_         -> InternalByteString -> Value
forall {k} (f :: k -> *) (op :: k).
InternalByteString -> Value' f op
U.ValueBytes (InternalByteString -> Value)
-> (ByteString -> InternalByteString) -> ByteString -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> InternalByteString
U.InternalByteString  (ByteString -> Value) -> ByteString -> Value
forall a b. (a -> b) -> a -> b
$ EpAddress -> ByteString
encodeEpAddress EpAddress
a
  VKey PublicKey
b ->
    case UntypingOptions
opts of
      UntypingOptions
Readable  -> MText -> Value
forall {k} (f :: k -> *) (op :: k). MText -> Value' f op
U.ValueString (MText -> Value) -> MText -> Value
forall a b. (a -> b) -> a -> b
$ PublicKey -> MText
mformatPublicKey PublicKey
b
      UntypingOptions
_         -> InternalByteString -> Value
forall {k} (f :: k -> *) (op :: k).
InternalByteString -> Value' f op
U.ValueBytes (InternalByteString -> Value)
-> (ByteString -> InternalByteString) -> ByteString -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> InternalByteString
U.InternalByteString (ByteString -> Value) -> ByteString -> Value
forall a b. (a -> b) -> a -> b
$ PublicKey -> ByteString
keyToBytes PublicKey
b
  Value' Instr t
VUnit ->
    Value
forall {k} (f :: k -> *) (op :: k). Value' f op
U.ValueUnit
  VSignature Signature
b ->
    case UntypingOptions
opts of
      UntypingOptions
Readable  -> MText -> Value
forall {k} (f :: k -> *) (op :: k). MText -> Value' f op
U.ValueString (MText -> Value) -> MText -> Value
forall a b. (a -> b) -> a -> b
$ Signature -> MText
mformatSignature Signature
b
      UntypingOptions
_         -> InternalByteString -> Value
forall {k} (f :: k -> *) (op :: k).
InternalByteString -> Value' f op
U.ValueBytes (InternalByteString -> Value)
-> (ByteString -> InternalByteString) -> ByteString -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> InternalByteString
U.InternalByteString (ByteString -> Value) -> ByteString -> Value
forall a b. (a -> b) -> a -> b
$ Signature -> ByteString
forall ba. ByteArray ba => Signature -> ba
signatureToBytes Signature
b
  VChainId ChainId
b ->
    case UntypingOptions
opts of
      UntypingOptions
Readable  -> MText -> Value
forall {k} (f :: k -> *) (op :: k). MText -> Value' f op
U.ValueString (MText -> Value) -> MText -> Value
forall a b. (a -> b) -> a -> b
$ ChainId -> MText
mformatChainId ChainId
b
      UntypingOptions
_         ->
        InternalByteString -> Value
forall {k} (f :: k -> *) (op :: k).
InternalByteString -> Value' f op
U.ValueBytes (InternalByteString -> Value)
-> (ByteString -> InternalByteString) -> ByteString -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> InternalByteString
U.InternalByteString (ByteString -> Value) -> ByteString -> Value
forall a b. (a -> b) -> a -> b
$ ByteString -> ByteString
forall bin bout.
(ByteArrayAccess bin, ByteArray bout) =>
bin -> bout
ByteArray.convert (ChainId -> ByteString
unChainId ChainId
b)
  VOption (Just Value' Instr t1
x) | STOption Sing n
op <- Sing t
sng ->
    Value -> Value
forall {k} (f :: k -> *) (op :: k). Value' f op -> Value' f op
U.ValueSome (UntypingOptions -> Sing t1 -> Value' Instr t1 -> Value
forall (t :: T).
ForbidOp t =>
UntypingOptions -> Sing t -> Value' Instr t -> Value
untypeValueImpl UntypingOptions
opts Sing t1
Sing n
op Value' Instr t1
x)
  VOption Maybe (Value' Instr t1)
Nothing -> Value
forall {k} (f :: k -> *) (op :: k). Value' f op
U.ValueNone
  VList [Value' Instr t1]
l | STList Sing n
lt <- Sing t
sng ->
    (NonEmpty Value -> Value) -> [Value] -> Value
forall {k} {a} {f :: k -> *} {op :: k}.
(NonEmpty a -> Value' f op) -> [a] -> Value' f op
vList NonEmpty Value -> Value
forall {k} (f :: k -> *) (op :: k).
(NonEmpty $ Value' f op) -> Value' f op
U.ValueSeq ([Value] -> Value) -> [Value] -> Value
forall a b. (a -> b) -> a -> b
$ (Value' Instr t1 -> Value) -> [Value' Instr t1] -> [Value]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map (UntypingOptions -> Sing t1 -> Value' Instr t1 -> Value
forall (t :: T).
ForbidOp t =>
UntypingOptions -> Sing t -> Value' Instr t -> Value
untypeValueImpl UntypingOptions
opts Sing t1
Sing n
lt) [Value' Instr t1]
l
  VSet Set (Value' Instr t1)
s | STSet Sing n
st <- Sing t
sng ->
    (NonEmpty Value -> Value) -> [Value] -> Value
forall {k} {a} {f :: k -> *} {op :: k}.
(NonEmpty a -> Value' f op) -> [a] -> Value' f op
vList NonEmpty Value -> Value
forall {k} (f :: k -> *) (op :: k).
(NonEmpty $ Value' f op) -> Value' f op
U.ValueSeq ([Value] -> Value) -> [Value] -> Value
forall a b. (a -> b) -> a -> b
$ (Value' Instr t1 -> Value) -> [Value' Instr t1] -> [Value]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map (UntypingOptions -> Sing t1 -> Value' Instr t1 -> Value
forall (t :: T).
ForbidOp t =>
UntypingOptions -> Sing t -> Value' Instr t -> Value
untypeValueImpl UntypingOptions
opts Sing t1
Sing n
st) ([Value' Instr t1] -> [Value]) -> [Value' Instr t1] -> [Value]
forall a b. (a -> b) -> a -> b
$ Set (Value' Instr t1) -> [Element (Set (Value' Instr t1))]
forall t. Container t => t -> [Element t]
toList Set (Value' Instr t1)
s
  VContract Address
addr SomeEntrypointCallT arg
sepc ->
    case UntypingOptions
opts of
      UntypingOptions
Readable  ->
        MText -> Value
forall {k} (f :: k -> *) (op :: k). MText -> Value' f op
U.ValueString (MText -> Value) -> (EpAddress -> MText) -> EpAddress -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpAddress -> MText
mformatEpAddress (EpAddress -> Value) -> EpAddress -> Value
forall a b. (a -> b) -> a -> b
$ Address -> EpName -> EpAddress
EpAddress' Address
addr (SomeEntrypointCallT arg -> EpName
forall (arg :: T). SomeEntrypointCallT arg -> EpName
sepcName SomeEntrypointCallT arg
sepc)
      UntypingOptions
_         -> InternalByteString -> Value
forall {k} (f :: k -> *) (op :: k).
InternalByteString -> Value' f op
U.ValueBytes (InternalByteString -> Value)
-> (EpAddress -> InternalByteString) -> EpAddress -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> InternalByteString
U.InternalByteString (ByteString -> InternalByteString)
-> (EpAddress -> ByteString) -> EpAddress -> InternalByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpAddress -> ByteString
encodeEpAddress (EpAddress -> Value) -> EpAddress -> Value
forall a b. (a -> b) -> a -> b
$
        Address -> EpName -> EpAddress
EpAddress' Address
addr (SomeEntrypointCallT arg -> EpName
forall (arg :: T). SomeEntrypointCallT arg -> EpName
sepcName SomeEntrypointCallT arg
sepc)
  VChest Chest
c -> InternalByteString -> Value
forall {k} (f :: k -> *) (op :: k).
InternalByteString -> Value' f op
U.ValueBytes (InternalByteString -> Value)
-> (ByteString -> InternalByteString) -> ByteString -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> InternalByteString
U.InternalByteString (ByteString -> Value) -> ByteString -> Value
forall a b. (a -> b) -> a -> b
$ Chest -> ByteString
chestBytes Chest
c
  VChestKey ChestKey
c -> InternalByteString -> Value
forall {k} (f :: k -> *) (op :: k).
InternalByteString -> Value' f op
U.ValueBytes (InternalByteString -> Value)
-> (ByteString -> InternalByteString) -> ByteString -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> InternalByteString
U.InternalByteString (ByteString -> Value) -> ByteString -> Value
forall a b. (a -> b) -> a -> b
$ ChestKey -> ByteString
chestKeyBytes ChestKey
c
  VTicket Address
s Value' Instr arg
v Natural
a | STTicket Sing n
vt <- Sing t
sng ->
    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 ->
        let us :: Value
us = UntypingOptions
-> Sing 'TAddress -> Value' Instr 'TAddress -> Value
forall (t :: T).
ForbidOp t =>
UntypingOptions -> Sing t -> Value' Instr t -> Value
untypeValueImpl UntypingOptions
opts Sing 'TAddress
SingT 'TAddress
STAddress (Value' Instr 'TAddress -> Value)
-> Value' Instr 'TAddress -> Value
forall a b. (a -> b) -> a -> b
$ EpAddress -> Value' Instr 'TAddress
forall (instr :: [T] -> [T] -> *).
EpAddress -> Value' instr 'TAddress
VAddress (Address -> EpName -> EpAddress
EpAddress' Address
s EpName
DefEpName)
            uv :: Value
uv = UntypingOptions -> Sing arg -> Value' Instr arg -> Value
forall (t :: T).
ForbidOp t =>
UntypingOptions -> Sing t -> Value' Instr t -> Value
untypeValueImpl UntypingOptions
opts Sing arg
Sing n
vt Value' Instr arg
v
            ua :: Value
ua = UntypingOptions -> Sing 'TNat -> Value' Instr 'TNat -> Value
forall (t :: T).
ForbidOp t =>
UntypingOptions -> Sing t -> Value' Instr t -> Value
untypeValueImpl UntypingOptions
opts Sing 'TNat
SingT 'TNat
STNat (Value' Instr 'TNat -> Value) -> Value' Instr 'TNat -> Value
forall a b. (a -> b) -> a -> b
$ Natural -> Value' Instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat Natural
a
        in case UntypingOptions
opts of
          UntypingOptions
Optimized -> NonEmpty Value -> Value
forall {k} (f :: k -> *) (op :: k).
(NonEmpty $ Value' f op) -> Value' f op
U.ValueSeq (NonEmpty Value -> Value) -> NonEmpty Value -> Value
forall a b. (a -> b) -> a -> b
$ Value
us Value -> [Value] -> NonEmpty Value
forall a. a -> [a] -> NonEmpty a
:| [Value
uv, Value
ua]
          UntypingOptions
_         -> Value -> Value -> Value
forall {k} (f :: k -> *) (op :: k).
Value' f op -> Value' f op -> Value' f op
U.ValuePair Value
us (Value -> Value -> Value
forall {k} (f :: k -> *) (op :: k).
Value' f op -> Value' f op -> Value' f op
U.ValuePair Value
uv Value
ua)
  VPair (Value' Instr l
l, Value' Instr r
r) -> case UntypingOptions
opts of
      UntypingOptions
Optimized -> NonEmpty Value -> Value
forall {k} (f :: k -> *) (op :: k).
(NonEmpty $ Value' f op) -> Value' f op
U.ValueSeq (NonEmpty Value -> Value) -> NonEmpty Value -> Value
forall a b. (a -> b) -> a -> b
$ (Value' Instr t, Sing t) -> NonEmpty Value
forall (ty :: T).
ForbidOp ty =>
(Value ty, Sing ty) -> NonEmpty Value
pairToSeq (Value' Instr t
val, Sing t
sng)
      UntypingOptions
_ | STPair Sing n1
lt Sing n2
rt <- Sing t
sng -> Sing 'PSOp
-> Sing l
-> Sing r
-> ((ForbidT 'PSOp l, ForbidT 'PSOp r) => Value)
-> Value
forall (a :: T) (b :: T) r (p :: TPredicateSym).
((ContainsT p a || ContainsT p b) ~ 'False) =>
Sing p
-> Sing a -> Sing b -> ((ForbidT p a, ForbidT p b) => r) -> r
deMorganForbidT Sing 'PSOp
SingTPredicateSym 'PSOp
SPSOp Sing l
Sing n1
lt Sing r
Sing n2
rt (((ForbidT 'PSOp l, ForbidT 'PSOp r) => Value) -> Value)
-> ((ForbidT 'PSOp l, ForbidT 'PSOp r) => Value) -> Value
forall a b. (a -> b) -> a -> b
$
        Value -> Value -> Value
forall {k} (f :: k -> *) (op :: k).
Value' f op -> Value' f op -> Value' f op
U.ValuePair (UntypingOptions -> Sing l -> Value' Instr l -> Value
forall (t :: T).
ForbidOp t =>
UntypingOptions -> Sing t -> Value' Instr t -> Value
untypeValueImpl UntypingOptions
opts Sing l
Sing n1
lt Value' Instr l
l) (UntypingOptions -> Sing r -> Value' Instr r -> Value
forall (t :: T).
ForbidOp t =>
UntypingOptions -> Sing t -> Value' Instr t -> Value
untypeValueImpl UntypingOptions
opts Sing r
Sing n2
rt Value' Instr r
r)

  VOr (Left Value' Instr l
x) | STOr Sing n1
lt Sing n2
rt <- Sing t
sng -> Sing 'PSOp
-> Sing l
-> Sing r
-> ((ForbidT 'PSOp l, ForbidT 'PSOp r) => Value)
-> Value
forall (a :: T) (b :: T) r (p :: TPredicateSym).
((ContainsT p a || ContainsT p b) ~ 'False) =>
Sing p
-> Sing a -> Sing b -> ((ForbidT p a, ForbidT p b) => r) -> r
deMorganForbidT Sing 'PSOp
SingTPredicateSym 'PSOp
SPSOp Sing l
Sing n1
lt Sing r
Sing n2
rt (((ForbidT 'PSOp l, ForbidT 'PSOp r) => Value) -> Value)
-> ((ForbidT 'PSOp l, ForbidT 'PSOp r) => Value) -> Value
forall a b. (a -> b) -> a -> b
$
    Value -> Value
forall {k} (f :: k -> *) (op :: k). Value' f op -> Value' f op
U.ValueLeft (UntypingOptions -> Sing l -> Value' Instr l -> Value
forall (t :: T).
ForbidOp t =>
UntypingOptions -> Sing t -> Value' Instr t -> Value
untypeValueImpl UntypingOptions
opts Sing l
Sing n1
lt Value' Instr l
x)

  VOr (Right Value' Instr r
x) | STOr Sing n1
lt Sing n2
rt <- Sing t
sng -> Sing 'PSOp
-> Sing l
-> Sing r
-> ((ForbidT 'PSOp l, ForbidT 'PSOp r) => Value)
-> Value
forall (a :: T) (b :: T) r (p :: TPredicateSym).
((ContainsT p a || ContainsT p b) ~ 'False) =>
Sing p
-> Sing a -> Sing b -> ((ForbidT p a, ForbidT p b) => r) -> r
deMorganForbidT Sing 'PSOp
SingTPredicateSym 'PSOp
SPSOp Sing l
Sing n1
lt Sing r
Sing n2
rt (((ForbidT 'PSOp l, ForbidT 'PSOp r) => Value) -> Value)
-> ((ForbidT 'PSOp l, ForbidT 'PSOp r) => Value) -> Value
forall a b. (a -> b) -> a -> b
$
    Value -> Value
forall {k} (f :: k -> *) (op :: k). Value' f op -> Value' f op
U.ValueRight (UntypingOptions -> Sing r -> Value' Instr r -> Value
forall (t :: T).
ForbidOp t =>
UntypingOptions -> Sing t -> Value' Instr t -> Value
untypeValueImpl UntypingOptions
opts Sing r
Sing n2
rt Value' Instr r
x)

  VLam (LambdaCode (RemFail Instr '[inp] '[out] -> Instr '[inp] '[out]
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
RemFail instr i o -> instr i o
rfAnyInstr -> Instr '[inp] '[out]
ops)) ->
    (NonEmpty ExpandedOp -> Value) -> [ExpandedOp] -> Value
forall {k} {a} {f :: k -> *} {op :: k}.
(NonEmpty a -> Value' f op) -> [a] -> Value' f op
vList ([ExpandedOp] -> Value
forall {k} (f :: k -> *) (op :: k). f op -> Value' f op
U.ValueLambda ([ExpandedOp] -> Value)
-> (NonEmpty ExpandedOp -> [ExpandedOp])
-> NonEmpty ExpandedOp
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty ExpandedOp -> [Element (NonEmpty ExpandedOp)]
NonEmpty ExpandedOp -> [ExpandedOp]
forall t. Container t => t -> [Element t]
toList) ([ExpandedOp] -> Value) -> [ExpandedOp] -> Value
forall a b. (a -> b) -> a -> b
$ UntypingOptions -> Instr '[inp] '[out] -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts Instr '[inp] '[out]
ops

  VLam (LambdaCodeRec (RemFail Instr '[inp, 'TLambda inp out] '[out]
-> Instr '[inp, 'TLambda inp out] '[out]
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
RemFail instr i o -> instr i o
rfAnyInstr -> Instr '[inp, 'TLambda inp out] '[out]
ops)) ->
    (NonEmpty ExpandedOp -> Value) -> [ExpandedOp] -> Value
forall {k} {a} {f :: k -> *} {op :: k}.
(NonEmpty a -> Value' f op) -> [a] -> Value' f op
vList ([ExpandedOp] -> Value
forall {k} (f :: k -> *) (op :: k). f op -> Value' f op
U.ValueLamRec ([ExpandedOp] -> Value)
-> (NonEmpty ExpandedOp -> [ExpandedOp])
-> NonEmpty ExpandedOp
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty ExpandedOp -> [Element (NonEmpty ExpandedOp)]
NonEmpty ExpandedOp -> [ExpandedOp]
forall t. Container t => t -> [Element t]
toList) ([ExpandedOp] -> Value) -> [ExpandedOp] -> Value
forall a b. (a -> b) -> a -> b
$ UntypingOptions
-> Instr '[inp, 'TLambda inp out] '[out] -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts Instr '[inp, 'TLambda inp out] '[out]
ops

  VMap Map (Value' Instr k) (Value' Instr v)
m | STMap Sing n1
kt Sing n2
vt <- Sing t
sng -> Sing 'PSOp
-> Sing k
-> Sing v
-> ((ForbidT 'PSOp k, ForbidT 'PSOp v) => Value)
-> Value
forall (a :: T) (b :: T) r (p :: TPredicateSym).
((ContainsT p a || ContainsT p b) ~ 'False) =>
Sing p
-> Sing a -> Sing b -> ((ForbidT p a, ForbidT p b) => r) -> r
deMorganForbidT Sing 'PSOp
SingTPredicateSym 'PSOp
SPSOp Sing k
Sing n1
kt Sing v
Sing n2
vt (((ForbidT 'PSOp k, ForbidT 'PSOp v) => Value) -> Value)
-> ((ForbidT 'PSOp k, ForbidT 'PSOp v) => Value) -> Value
forall a b. (a -> b) -> a -> b
$
    (NonEmpty (Elt [] ExpandedOp) -> Value)
-> [Elt [] ExpandedOp] -> Value
forall {k} {a} {f :: k -> *} {op :: k}.
(NonEmpty a -> Value' f op) -> [a] -> Value' f op
vList NonEmpty (Elt [] ExpandedOp) -> Value
forall {k} (f :: k -> *) (op :: k).
(NonEmpty $ Elt f op) -> Value' f op
U.ValueMap ([Elt [] ExpandedOp] -> Value) -> [Elt [] ExpandedOp] -> Value
forall a b. (a -> b) -> a -> b
$ Map (Value' Instr k) (Value' Instr v)
-> [(Value' Instr k, Value' Instr v)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Value' Instr k) (Value' Instr v)
m [(Value' Instr k, Value' Instr v)]
-> ((Value' Instr k, Value' Instr v) -> Elt [] ExpandedOp)
-> [Elt [] ExpandedOp]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(Value' Instr k
k, Value' Instr v
v) ->
      Value -> Value -> Elt [] ExpandedOp
forall {k} (f :: k -> *) (op :: k).
Value' f op -> Value' f op -> Elt f op
U.Elt (UntypingOptions -> Sing k -> Value' Instr k -> Value
forall (t :: T).
ForbidOp t =>
UntypingOptions -> Sing t -> Value' Instr t -> Value
untypeValueImpl UntypingOptions
opts Sing k
Sing n1
kt Value' Instr k
k) (UntypingOptions -> Sing v -> Value' Instr v -> Value
forall (t :: T).
ForbidOp t =>
UntypingOptions -> Sing t -> Value' Instr t -> Value
untypeValueImpl UntypingOptions
opts Sing v
Sing n2
vt Value' Instr v
v)

  VBigMap Maybe Natural
_ Map (Value' Instr k) (Value' Instr v)
m | STBigMap Sing n1
kt Sing n2
vt <- Sing t
sng -> Sing 'PSOp
-> Sing k
-> Sing v
-> ((ForbidT 'PSOp k, ForbidT 'PSOp v) => Value)
-> Value
forall (a :: T) (b :: T) r (p :: TPredicateSym).
((ContainsT p a || ContainsT p b) ~ 'False) =>
Sing p
-> Sing a -> Sing b -> ((ForbidT p a, ForbidT p b) => r) -> r
deMorganForbidT Sing 'PSOp
SingTPredicateSym 'PSOp
SPSOp Sing k
Sing n1
kt Sing v
Sing n2
vt (((ForbidT 'PSOp k, ForbidT 'PSOp v) => Value) -> Value)
-> ((ForbidT 'PSOp k, ForbidT 'PSOp v) => Value) -> Value
forall a b. (a -> b) -> a -> b
$
    (NonEmpty (Elt [] ExpandedOp) -> Value)
-> [Elt [] ExpandedOp] -> Value
forall {k} {a} {f :: k -> *} {op :: k}.
(NonEmpty a -> Value' f op) -> [a] -> Value' f op
vList NonEmpty (Elt [] ExpandedOp) -> Value
forall {k} (f :: k -> *) (op :: k).
(NonEmpty $ Elt f op) -> Value' f op
U.ValueMap ([Elt [] ExpandedOp] -> Value) -> [Elt [] ExpandedOp] -> Value
forall a b. (a -> b) -> a -> b
$ Map (Value' Instr k) (Value' Instr v)
-> [(Value' Instr k, Value' Instr v)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Value' Instr k) (Value' Instr v)
m [(Value' Instr k, Value' Instr v)]
-> ((Value' Instr k, Value' Instr v) -> Elt [] ExpandedOp)
-> [Elt [] ExpandedOp]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(Value' Instr k
k, Value' Instr v
v) ->
      Value -> Value -> Elt [] ExpandedOp
forall {k} (f :: k -> *) (op :: k).
Value' f op -> Value' f op -> Elt f op
U.Elt (UntypingOptions -> Sing k -> Value' Instr k -> Value
forall (t :: T).
ForbidOp t =>
UntypingOptions -> Sing t -> Value' Instr t -> Value
untypeValueImpl UntypingOptions
opts Sing k
Sing n1
kt Value' Instr k
k) (UntypingOptions -> Sing v -> Value' Instr v -> Value
forall (t :: T).
ForbidOp t =>
UntypingOptions -> Sing t -> Value' Instr t -> Value
untypeValueImpl UntypingOptions
opts Sing v
Sing n2
vt Value' Instr v
v)
  where
    vList :: (NonEmpty a -> Value' f op) -> [a] -> Value' f op
vList NonEmpty a -> Value' f op
ctor = Value' f op
-> (NonEmpty a -> Value' f op) -> Maybe (NonEmpty a) -> Value' f op
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Value' f op
forall {k} (f :: k -> *) (op :: k). Value' f op
U.ValueNil NonEmpty a -> Value' f op
ctor (Maybe (NonEmpty a) -> Value' f op)
-> ([a] -> Maybe (NonEmpty a)) -> [a] -> Value' f op
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Maybe (NonEmpty a)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty

    pairToSeq :: ForbidOp ty
              => (Value ty, Sing ty)
              -> NonEmpty U.Value
    pairToSeq :: forall (ty :: T).
ForbidOp ty =>
(Value ty, Sing ty) -> NonEmpty Value
pairToSeq = \case
      (VPair (Value' Instr l
a, Value' Instr r
b), STPair Sing n1
l Sing n2
r) -> Sing 'PSOp
-> Sing l
-> Sing r
-> ((ForbidT 'PSOp l, ForbidT 'PSOp r) => NonEmpty Value)
-> NonEmpty Value
forall (a :: T) (b :: T) r (p :: TPredicateSym).
((ContainsT p a || ContainsT p b) ~ 'False) =>
Sing p
-> Sing a -> Sing b -> ((ForbidT p a, ForbidT p b) => r) -> r
deMorganForbidT Sing 'PSOp
SingTPredicateSym 'PSOp
SPSOp Sing l
Sing n1
l Sing r
Sing n2
r (((ForbidT 'PSOp l, ForbidT 'PSOp r) => NonEmpty Value)
 -> NonEmpty Value)
-> ((ForbidT 'PSOp l, ForbidT 'PSOp r) => NonEmpty Value)
-> NonEmpty Value
forall a b. (a -> b) -> a -> b
$
        UntypingOptions -> Sing l -> Value' Instr l -> Value
forall (t :: T).
ForbidOp t =>
UntypingOptions -> Sing t -> Value' Instr t -> Value
untypeValueImpl UntypingOptions
opts Sing l
Sing n1
l Value' Instr l
a Value -> NonEmpty Value -> NonEmpty Value
forall a. a -> NonEmpty a -> NonEmpty a
<| (Value' Instr r, Sing r) -> NonEmpty Value
forall (ty :: T).
ForbidOp ty =>
(Value ty, Sing ty) -> NonEmpty Value
pairToSeq (Value' Instr r
b, Sing r
Sing n2
r)
      (Value ty
v, Sing ty
vt) -> UntypingOptions -> Sing ty -> Value ty -> Value
forall (t :: T).
ForbidOp t =>
UntypingOptions -> Sing t -> Value' Instr t -> Value
untypeValueImpl UntypingOptions
opts Sing ty
vt Value ty
v Value -> [Value] -> NonEmpty Value
forall a. a -> [a] -> NonEmpty a
:| []

    hashToBytes :: Hash kind -> ByteString
    hashToBytes :: forall (kind :: HashKind). Hash kind -> ByteString
hashToBytes Hash{ByteString
HashTag kind
hTag :: HashTag kind
hBytes :: ByteString
hTag :: forall (kind :: HashKind). Hash kind -> HashTag kind
hBytes :: forall (kind :: HashKind). Hash kind -> ByteString
..} = (ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
hBytes) (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$
      case HashTag kind
hTag of
        HashKey KeyType
kt -> OneItem ByteString -> ByteString
forall x. One x => OneItem x -> x
one (OneItem ByteString -> ByteString)
-> OneItem ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ KeyType -> Word8
keyTypeTag KeyType
kt
        HashTag kind
HashContract -> ByteString
""
        HashTag kind
HashSR  -> ByteString
""

    keyToBytes :: PublicKey -> ByteString
    keyToBytes :: PublicKey -> ByteString
keyToBytes PublicKey
x = OneItem ByteString -> ByteString
forall x. One x => OneItem x -> x
one (KeyType -> Word8
keyTypeTag (KeyType -> Word8) -> KeyType -> Word8
forall a b. (a -> b) -> a -> b
$ PublicKey -> KeyType
publicKeyType PublicKey
x) ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> PublicKey -> ByteString
publicKeyToBytes PublicKey
x

    encodeEpAddress :: EpAddress -> ByteString
    encodeEpAddress :: EpAddress -> ByteString
encodeEpAddress (EpAddress KindedAddress kind
addr EpName
epName) =
      KindedAddress kind -> ByteString
forall (kind :: AddressKind). KindedAddress kind -> ByteString
encodeAddress KindedAddress kind
addr ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> EpName -> ByteString
encodeEpName EpName
epName

    encodeAddress :: forall kind. KindedAddress kind -> ByteString
    encodeAddress :: forall (kind :: AddressKind). KindedAddress kind -> ByteString
encodeAddress KindedAddress kind
addr = OneItem ByteString -> ByteString
forall x. One x => OneItem x -> x
one (AddressKind -> Word8
addressKindTag AddressKind
ak) ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> case KindedAddress kind
addr of
      ImplicitAddress KeyHash
keyHash -> KeyHash -> ByteString
forall (kind :: HashKind). Hash kind -> ByteString
hashToBytes KeyHash
keyHash
      ContractAddress ContractHash
hash -> ContractHash -> ByteString
forall (kind :: HashKind). Hash kind -> ByteString
hashToBytes ContractHash
hash ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
"\x00"
      SmartRollupAddress SmartRollupHash
hash -> SmartRollupHash -> ByteString
forall (kind :: HashKind). Hash kind -> ByteString
hashToBytes SmartRollupHash
hash ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
"\x00"
      where ak :: AddressKind
ak = forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: AddressKind).
(SingKind AddressKind, SingI a) =>
Demote AddressKind
demote @kind (SingI kind => AddressKind) -> Dict (SingI kind) -> AddressKind
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ KindedAddress kind -> Dict (SingI kind)
forall (kind :: AddressKind).
KindedAddress kind -> Dict (SingI kind)
addressKindSanity KindedAddress kind
addr

    encodeEpName :: EpName -> ByteString
    encodeEpName :: EpName -> ByteString
encodeEpName = Text -> ByteString
forall a b. ConvertUtf8 a b => a -> b
encodeUtf8 (Text -> ByteString) -> (EpName -> Text) -> EpName -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RootAnn -> Text
forall {k} (tag :: k). Annotation tag -> Text
unAnnotation (RootAnn -> Text) -> (EpName -> RootAnn) -> EpName -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpName -> RootAnn
epNameToRefAnn (EpName -> RootAnn) -> (EpName -> EpName) -> EpName -> RootAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpName -> EpName
canonicalize
      where
        canonicalize :: EpName -> EpName
        canonicalize :: EpName -> EpName
canonicalize (UnsafeEpName Text
"default") = EpName
DefEpName
        canonicalize EpName
epName                   = EpName
epName

-- | Convert a Haskell type-level type tag into an
-- untyped value representation.
--
-- This function is intended to be used with @TypeApplications@.
untypeDemoteT :: forall (t :: T). SingI t => U.Ty
untypeDemoteT :: forall (t :: T). SingI t => Ty
untypeDemoteT = T -> Ty
toUType (T -> Ty) -> T -> Ty
forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @t

-- | Convert Haskell-typed 'Instr' to a list of optimized untyped operations
instrToOpsOptimized :: HasCallStack => Instr inp out -> [U.ExpandedOp]
instrToOpsOptimized :: forall (inp :: [T]) (out :: [T]).
HasCallStack =>
Instr inp out -> [ExpandedOp]
instrToOpsOptimized = UntypingOptions -> Instr inp out -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
Optimized

-- | Convert Haskell-typed 'Instr' to a list of human-readable untyped operations
instrToOps :: HasCallStack => Instr inp out -> [U.ExpandedOp]
instrToOps :: forall (inp :: [T]) (out :: [T]).
HasCallStack =>
Instr inp out -> [ExpandedOp]
instrToOps = UntypingOptions -> Instr inp out -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
Readable

instrToOpsImpl :: HasCallStack
               => UntypingOptions
               -> Instr inp out
               -> [U.ExpandedOp]
instrToOpsImpl :: forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts = \case
  Instr inp out
Nop -> []
  Seq Instr inp b
i1 Instr b out
i2 -> UntypingOptions -> Instr inp b -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts Instr inp b
i1 [ExpandedOp] -> [ExpandedOp] -> [ExpandedOp]
forall a. Semigroup a => a -> a -> a
<> UntypingOptions -> Instr b out -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts Instr b out
i2
  Nested Instr inp out
sq -> OneItem [ExpandedOp] -> [ExpandedOp]
forall x. One x => OneItem x -> x
one (OneItem [ExpandedOp] -> [ExpandedOp])
-> OneItem [ExpandedOp] -> [ExpandedOp]
forall a b. (a -> b) -> a -> b
$ [ExpandedOp] -> ExpandedOp
U.SeqEx ([ExpandedOp] -> ExpandedOp) -> [ExpandedOp] -> ExpandedOp
forall a b. (a -> b) -> a -> b
$ UntypingOptions -> Instr inp out -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts Instr inp out
sq
  DocGroup DocGrouping
_ Instr inp out
sq -> UntypingOptions -> Instr inp out -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts Instr inp out
sq
  Ext (ExtInstr inp
ext :: ExtInstr inp) -> (ExpandedInstr -> ExpandedOp
U.PrimEx (ExpandedInstr -> ExpandedOp)
-> (ExtInstrAbstract [] ExpandedOp -> ExpandedInstr)
-> ExtInstrAbstract [] ExpandedOp
-> ExpandedOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtInstrAbstract [] ExpandedOp -> ExpandedInstr
forall (f :: * -> *) op.
ExtInstrAbstract f op -> InstrAbstract f op
U.EXT) (ExtInstrAbstract [] ExpandedOp -> ExpandedOp)
-> [ExtInstrAbstract [] ExpandedOp] -> [ExpandedOp]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExtInstr inp -> [ExtInstrAbstract [] ExpandedOp]
forall (s :: [T]). ExtInstr s -> [ExtInstrAbstract [] ExpandedOp]
extInstrToOps ExtInstr inp
ext
  -- TODO [#283]: After representation of locations is polished,
  -- this place should be updated to pass it from typed to untyped ASTs.
  WithLoc ErrorSrcPos
_ Instr inp out
i -> UntypingOptions -> Instr inp out -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts Instr inp out
i
  Meta SomeMeta
_ Instr inp out
i -> UntypingOptions -> Instr inp out -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts Instr inp out
i
  Instr inp out
i -> ExpandedOp -> [ExpandedOp]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExpandedOp -> [ExpandedOp]) -> ExpandedOp -> [ExpandedOp]
forall a b. (a -> b) -> a -> b
$ ExpandedInstr -> ExpandedOp
U.PrimEx (ExpandedInstr -> ExpandedOp) -> ExpandedInstr -> ExpandedOp
forall a b. (a -> b) -> a -> b
$ case Instr inp out
i of
    Instr inp out
DROP -> ExpandedInstr
forall (f :: * -> *) op. InstrAbstract f op
U.DROP
    DROPN PeanoNatural n
s -> Word -> ExpandedInstr
forall (f :: * -> *) op. Word -> InstrAbstract f op
U.DROPN (forall a b. (HasCallStack, Integral a, Integral b) => a -> b
Unsafe.fromIntegral @Natural @Word (Natural -> Word) -> Natural -> Word
forall a b. (a -> b) -> a -> b
$ PeanoNatural n -> Natural
forall (n :: Peano). PeanoNatural n -> Natural
fromPeanoNatural PeanoNatural n
s)
    AnnDUP AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.DUP
    AnnDUPN AnnVar
ann PeanoNatural n
s -> AnnVar
-> AnnotateInstrArg '[VarAnn] (Word -> ExpandedInstr)
-> Word
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] (Word -> ExpandedInstr)
VarAnn -> Word -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> Word -> InstrAbstract f op
U.DUPN (forall a b. (HasCallStack, Integral a, Integral b) => a -> b
Unsafe.fromIntegral @Natural @Word (Natural -> Word) -> Natural -> Word
forall a b. (a -> b) -> a -> b
$ PeanoNatural n -> Natural
forall (n :: Peano). PeanoNatural n -> Natural
fromPeanoNatural PeanoNatural n
s)
    Instr inp out
SWAP -> ExpandedInstr
forall (f :: * -> *) op. InstrAbstract f op
U.SWAP
    DIG PeanoNatural n
s -> Word -> ExpandedInstr
forall (f :: * -> *) op. Word -> InstrAbstract f op
U.DIG (forall a b. (HasCallStack, Integral a, Integral b) => a -> b
Unsafe.fromIntegral @Natural @Word (Natural -> Word) -> Natural -> Word
forall a b. (a -> b) -> a -> b
$ PeanoNatural n -> Natural
forall (n :: Peano). PeanoNatural n -> Natural
fromPeanoNatural PeanoNatural n
s)
    DUG PeanoNatural n
s -> Word -> ExpandedInstr
forall (f :: * -> *) op. Word -> InstrAbstract f op
U.DUG (forall a b. (HasCallStack, Integral a, Integral b) => a -> b
Unsafe.fromIntegral @Natural @Word (Natural -> Word) -> Natural -> Word
forall a b. (a -> b) -> a -> b
$ PeanoNatural n -> Natural
forall (n :: Peano). PeanoNatural n -> Natural
fromPeanoNatural PeanoNatural n
s)
    AnnPUSH Anns '[VarAnn, Notes t]
ann Value' Instr t
val | Instr inp (t : inp)
_ :: Instr inp1 (t ': s) <- Instr inp out
i ->
      let value :: Value
value = UntypingOptions -> Sing t -> Value' Instr t -> Value
forall (t :: T).
ForbidOp t =>
UntypingOptions -> Sing t -> Value' Instr t -> Value
untypeValueImpl UntypingOptions
opts (forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @t) Value' Instr t
val
      in Anns '[VarAnn, Notes t]
-> AnnotateInstrArg '[VarAnn, Notes t] (Value -> ExpandedInstr)
-> Value
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr Anns '[VarAnn, Notes t]
ann AnnotateInstrArg '[VarAnn, Notes t] (Value -> ExpandedInstr)
VarAnn -> Ty -> Value -> ExpandedInstr
forall (f :: * -> *) op.
VarAnn -> Ty -> Value' f op -> InstrAbstract f op
U.PUSH Value
value
    AnnNONE Anns '[TypeAnn, VarAnn, Notes a]
ann | Instr inp ('TOption a : inp)
_ :: Instr inp1 ('TOption a ': inp1) <- Instr inp out
i ->
      Anns '[TypeAnn, VarAnn, Notes a]
-> AnnotateInstrArg '[TypeAnn, VarAnn, Notes a] ExpandedInstr
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr Anns '[TypeAnn, VarAnn, Notes a]
ann AnnotateInstrArg '[TypeAnn, VarAnn, Notes a] ExpandedInstr
TypeAnn -> VarAnn -> Ty -> ExpandedInstr
forall (f :: * -> *) op.
TypeAnn -> VarAnn -> Ty -> InstrAbstract f op
U.NONE
    AnnSOME Anns '[TypeAnn, VarAnn]
ann -> Anns '[TypeAnn, VarAnn]
-> AnnotateInstrArg '[TypeAnn, VarAnn] ExpandedInstr
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr Anns '[TypeAnn, VarAnn]
ann AnnotateInstrArg '[TypeAnn, VarAnn] ExpandedInstr
TypeAnn -> VarAnn -> ExpandedInstr
forall (f :: * -> *) op. TypeAnn -> VarAnn -> InstrAbstract f op
U.SOME
    AnnUNIT Anns '[TypeAnn, VarAnn]
ann -> Anns '[TypeAnn, VarAnn]
-> AnnotateInstrArg '[TypeAnn, VarAnn] ExpandedInstr
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr Anns '[TypeAnn, VarAnn]
ann AnnotateInstrArg '[TypeAnn, VarAnn] ExpandedInstr
TypeAnn -> VarAnn -> ExpandedInstr
forall (f :: * -> *) op. TypeAnn -> VarAnn -> InstrAbstract f op
U.UNIT
    IF_NONE Instr s out
i1 Instr (a : s) out
i2 -> [ExpandedOp] -> [ExpandedOp] -> ExpandedInstr
forall (f :: * -> *) op. f op -> f op -> InstrAbstract f op
U.IF_NONE (UntypingOptions -> Instr s out -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts Instr s out
i1) (UntypingOptions -> Instr (a : s) out -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts Instr (a : s) out
i2)
    AnnPAIR Anns '[TypeAnn, VarAnn, RootAnn, RootAnn]
ann -> Anns '[TypeAnn, VarAnn, RootAnn, RootAnn]
-> AnnotateInstrArg
     '[TypeAnn, VarAnn, RootAnn, RootAnn] ExpandedInstr
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr Anns '[TypeAnn, VarAnn, RootAnn, RootAnn]
ann AnnotateInstrArg '[TypeAnn, VarAnn, RootAnn, RootAnn] ExpandedInstr
TypeAnn -> VarAnn -> RootAnn -> RootAnn -> ExpandedInstr
forall (f :: * -> *) op.
TypeAnn -> VarAnn -> RootAnn -> RootAnn -> InstrAbstract f op
U.PAIR
    AnnUNPAIR Anns '[VarAnn, VarAnn, RootAnn, RootAnn]
ann -> Anns '[VarAnn, VarAnn, RootAnn, RootAnn]
-> AnnotateInstrArg
     '[VarAnn, VarAnn, RootAnn, RootAnn] ExpandedInstr
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr Anns '[VarAnn, VarAnn, RootAnn, RootAnn]
ann AnnotateInstrArg '[VarAnn, VarAnn, RootAnn, RootAnn] ExpandedInstr
VarAnn -> VarAnn -> RootAnn -> RootAnn -> ExpandedInstr
forall (f :: * -> *) op.
VarAnn -> VarAnn -> RootAnn -> RootAnn -> InstrAbstract f op
U.UNPAIR
    AnnPAIRN AnnVar
ann PeanoNatural n
n -> AnnVar
-> AnnotateInstrArg '[VarAnn] (Word -> ExpandedInstr)
-> Word
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] (Word -> ExpandedInstr)
VarAnn -> Word -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> Word -> InstrAbstract f op
U.PAIRN (forall a b. (HasCallStack, Integral a, Integral b) => a -> b
Unsafe.fromIntegral @Natural @Word (Natural -> Word) -> Natural -> Word
forall a b. (a -> b) -> a -> b
$ PeanoNatural n -> Natural
forall (n :: Peano). PeanoNatural n -> Natural
fromPeanoNatural PeanoNatural n
n)
    UNPAIRN PeanoNatural n
n -> Word -> ExpandedInstr
forall (f :: * -> *) op. Word -> InstrAbstract f op
U.UNPAIRN (forall a b. (HasCallStack, Integral a, Integral b) => a -> b
Unsafe.fromIntegral @Natural @Word (Natural -> Word) -> Natural -> Word
forall a b. (a -> b) -> a -> b
$ PeanoNatural n -> Natural
forall (n :: Peano). PeanoNatural n -> Natural
fromPeanoNatural PeanoNatural n
n)
    AnnCAR Anns '[VarAnn, RootAnn]
ann -> Anns '[VarAnn, RootAnn]
-> AnnotateInstrArg '[VarAnn, RootAnn] ExpandedInstr
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr Anns '[VarAnn, RootAnn]
ann AnnotateInstrArg '[VarAnn, RootAnn] ExpandedInstr
VarAnn -> RootAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> RootAnn -> InstrAbstract f op
U.CAR
    AnnCDR Anns '[VarAnn, RootAnn]
ann -> Anns '[VarAnn, RootAnn]
-> AnnotateInstrArg '[VarAnn, RootAnn] ExpandedInstr
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr Anns '[VarAnn, RootAnn]
ann AnnotateInstrArg '[VarAnn, RootAnn] ExpandedInstr
VarAnn -> RootAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> RootAnn -> InstrAbstract f op
U.CDR
    AnnLEFT Anns '[TypeAnn, VarAnn, RootAnn, RootAnn, Notes b]
ann | Instr (a : s) ('TOr a b : s)
_ :: Instr (a ': s) ('TOr a b ': s) <- Instr inp out
i ->
      Anns '[TypeAnn, VarAnn, RootAnn, RootAnn, Notes b]
-> AnnotateInstrArg
     '[TypeAnn, VarAnn, RootAnn, RootAnn, Notes b] ExpandedInstr
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr Anns '[TypeAnn, VarAnn, RootAnn, RootAnn, Notes b]
ann AnnotateInstrArg
  '[TypeAnn, VarAnn, RootAnn, RootAnn, Notes b] ExpandedInstr
TypeAnn -> VarAnn -> RootAnn -> RootAnn -> Ty -> ExpandedInstr
forall (f :: * -> *) op.
TypeAnn -> VarAnn -> RootAnn -> RootAnn -> Ty -> InstrAbstract f op
U.LEFT
    AnnRIGHT Anns '[TypeAnn, VarAnn, RootAnn, RootAnn, Notes a]
ann | Instr (b : s) ('TOr a b : s)
_ :: Instr (b ': s) ('TOr a b ': s) <- Instr inp out
i ->
      Anns '[TypeAnn, VarAnn, RootAnn, RootAnn, Notes a]
-> AnnotateInstrArg
     '[TypeAnn, VarAnn, RootAnn, RootAnn, Notes a] ExpandedInstr
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr Anns '[TypeAnn, VarAnn, RootAnn, RootAnn, Notes a]
ann AnnotateInstrArg
  '[TypeAnn, VarAnn, RootAnn, RootAnn, Notes a] ExpandedInstr
TypeAnn -> VarAnn -> RootAnn -> RootAnn -> Ty -> ExpandedInstr
forall (f :: * -> *) op.
TypeAnn -> VarAnn -> RootAnn -> RootAnn -> Ty -> InstrAbstract f op
U.RIGHT
    IF_LEFT Instr (a : s) out
i1 Instr (b : s) out
i2 -> [ExpandedOp] -> [ExpandedOp] -> ExpandedInstr
forall (f :: * -> *) op. f op -> f op -> InstrAbstract f op
U.IF_LEFT (UntypingOptions -> Instr (a : s) out -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts Instr (a : s) out
i1) (UntypingOptions -> Instr (b : s) out -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts Instr (b : s) out
i2)
    AnnNIL Anns '[TypeAnn, VarAnn, Notes p]
ann | Instr inp ('TList p : inp)
_ :: Instr s ('TList p ': s) <- Instr inp out
i ->
      Anns '[TypeAnn, VarAnn, Notes p]
-> AnnotateInstrArg '[TypeAnn, VarAnn, Notes p] ExpandedInstr
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr Anns '[TypeAnn, VarAnn, Notes p]
ann AnnotateInstrArg '[TypeAnn, VarAnn, Notes p] ExpandedInstr
TypeAnn -> VarAnn -> Ty -> ExpandedInstr
forall (f :: * -> *) op.
TypeAnn -> VarAnn -> Ty -> InstrAbstract f op
U.NIL
    AnnCONS AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.CONS
    IF_CONS Instr (a : 'TList a : s) out
i1 Instr s out
i2 -> [ExpandedOp] -> [ExpandedOp] -> ExpandedInstr
forall (f :: * -> *) op. f op -> f op -> InstrAbstract f op
U.IF_CONS (UntypingOptions -> Instr (a : 'TList a : s) out -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts Instr (a : 'TList a : s) out
i1) (UntypingOptions -> Instr s out -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts Instr s out
i2)
    AnnSIZE AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.SIZE
    AnnEMPTY_SET Anns '[TypeAnn, VarAnn, Notes e]
ann | Instr inp ('TSet e : inp)
_ :: Instr s ('TSet e ': s) <- Instr inp out
i ->
      Anns '[TypeAnn, VarAnn, Notes e]
-> AnnotateInstrArg '[TypeAnn, VarAnn, Notes e] ExpandedInstr
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr Anns '[TypeAnn, VarAnn, Notes e]
ann AnnotateInstrArg '[TypeAnn, VarAnn, Notes e] ExpandedInstr
TypeAnn -> VarAnn -> Ty -> ExpandedInstr
forall (f :: * -> *) op.
TypeAnn -> VarAnn -> Ty -> InstrAbstract f op
U.EMPTY_SET
    AnnEMPTY_MAP Anns '[TypeAnn, VarAnn, Notes a, Notes b]
ann | Instr inp ('TMap a b : inp)
_ :: Instr s ('TMap a b ': s) <- Instr inp out
i ->
      Anns '[TypeAnn, VarAnn, Notes a, Notes b]
-> AnnotateInstrArg
     '[TypeAnn, VarAnn, Notes a, Notes b] ExpandedInstr
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr Anns '[TypeAnn, VarAnn, Notes a, Notes b]
ann AnnotateInstrArg '[TypeAnn, VarAnn, Notes a, Notes b] ExpandedInstr
TypeAnn -> VarAnn -> Ty -> Ty -> ExpandedInstr
forall (f :: * -> *) op.
TypeAnn -> VarAnn -> Ty -> Ty -> InstrAbstract f op
U.EMPTY_MAP
    AnnEMPTY_BIG_MAP Anns '[TypeAnn, VarAnn, Notes a, Notes b]
ann | Instr inp ('TBigMap a b : inp)
_ :: Instr s ('TBigMap a b ': s) <- Instr inp out
i ->
      Anns '[TypeAnn, VarAnn, Notes a, Notes b]
-> AnnotateInstrArg
     '[TypeAnn, VarAnn, Notes a, Notes b] ExpandedInstr
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr Anns '[TypeAnn, VarAnn, Notes a, Notes b]
ann AnnotateInstrArg '[TypeAnn, VarAnn, Notes a, Notes b] ExpandedInstr
TypeAnn -> VarAnn -> Ty -> Ty -> ExpandedInstr
forall (f :: * -> *) op.
TypeAnn -> VarAnn -> Ty -> Ty -> InstrAbstract f op
U.EMPTY_BIG_MAP
    AnnMAP AnnVar
ann Instr (MapOpInp c : s) (b : s)
op -> AnnVar
-> AnnotateInstrArg '[VarAnn] ([ExpandedOp] -> ExpandedInstr)
-> [ExpandedOp]
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ([ExpandedOp] -> ExpandedInstr)
VarAnn -> [ExpandedOp] -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> f op -> InstrAbstract f op
U.MAP ([ExpandedOp] -> ExpandedInstr) -> [ExpandedOp] -> ExpandedInstr
forall a b. (a -> b) -> a -> b
$ UntypingOptions -> Instr (MapOpInp c : s) (b : s) -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts Instr (MapOpInp c : s) (b : s)
op
    ITER Instr (IterOpEl c : out) out
op -> [ExpandedOp] -> ExpandedInstr
forall (f :: * -> *) op. f op -> InstrAbstract f op
U.ITER ([ExpandedOp] -> ExpandedInstr) -> [ExpandedOp] -> ExpandedInstr
forall a b. (a -> b) -> a -> b
$ UntypingOptions -> Instr (IterOpEl c : out) out -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts Instr (IterOpEl c : out) out
op
    AnnMEM AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.MEM
    AnnGET AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.GET
    AnnGETN AnnVar
ann PeanoNatural ix
n -> AnnVar
-> AnnotateInstrArg '[VarAnn] (Word -> ExpandedInstr)
-> Word
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] (Word -> ExpandedInstr)
VarAnn -> Word -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> Word -> InstrAbstract f op
U.GETN (forall a b. (HasCallStack, Integral a, Integral b) => a -> b
Unsafe.fromIntegral @Natural @Word (Natural -> Word) -> Natural -> Word
forall a b. (a -> b) -> a -> b
$ PeanoNatural ix -> Natural
forall (n :: Peano). PeanoNatural n -> Natural
fromPeanoNatural PeanoNatural ix
n)
    AnnUPDATE AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.UPDATE
    AnnUPDATEN AnnVar
ann PeanoNatural ix
n -> AnnVar
-> AnnotateInstrArg '[VarAnn] (Word -> ExpandedInstr)
-> Word
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] (Word -> ExpandedInstr)
VarAnn -> Word -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> Word -> InstrAbstract f op
U.UPDATEN (forall a b. (HasCallStack, Integral a, Integral b) => a -> b
Unsafe.fromIntegral @Natural @Word (Natural -> Word) -> Natural -> Word
forall a b. (a -> b) -> a -> b
$ PeanoNatural ix -> Natural
forall (n :: Peano). PeanoNatural n -> Natural
fromPeanoNatural PeanoNatural ix
n)
    AnnGET_AND_UPDATE AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.GET_AND_UPDATE
    IF Instr s out
op1 Instr s out
op2 -> [ExpandedOp] -> [ExpandedOp] -> ExpandedInstr
forall (f :: * -> *) op. f op -> f op -> InstrAbstract f op
U.IF (UntypingOptions -> Instr s out -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts Instr s out
op1) (UntypingOptions -> Instr s out -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts Instr s out
op2)
    LOOP Instr out ('TBool : out)
op -> [ExpandedOp] -> ExpandedInstr
forall (f :: * -> *) op. f op -> InstrAbstract f op
U.LOOP (UntypingOptions -> Instr out ('TBool : out) -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts Instr out ('TBool : out)
op)
    LOOP_LEFT Instr (a : s) ('TOr a b : s)
op -> [ExpandedOp] -> ExpandedInstr
forall (f :: * -> *) op. f op -> InstrAbstract f op
U.LOOP_LEFT (UntypingOptions -> Instr (a : s) ('TOr a b : s) -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts Instr (a : s) ('TOr a b : s)
op)
    AnnLAMBDA Anns '[VarAnn, Notes i, Notes o]
ann RemFail Instr '[i] '[o]
l -> Anns '[VarAnn, Notes i, Notes o]
-> AnnotateInstrArg
     '[VarAnn, Notes i, Notes o] ([ExpandedOp] -> ExpandedInstr)
-> [ExpandedOp]
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr Anns '[VarAnn, Notes i, Notes o]
ann AnnotateInstrArg
  '[VarAnn, Notes i, Notes o] ([ExpandedOp] -> ExpandedInstr)
VarAnn -> Ty -> Ty -> [ExpandedOp] -> ExpandedInstr
forall (f :: * -> *) op.
VarAnn -> Ty -> Ty -> f op -> InstrAbstract f op
U.LAMBDA (UntypingOptions -> Instr '[i] '[o] -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts (Instr '[i] '[o] -> [ExpandedOp])
-> Instr '[i] '[o] -> [ExpandedOp]
forall a b. (a -> b) -> a -> b
$ RemFail Instr '[i] '[o] -> Instr '[i] '[o]
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
RemFail instr i o -> instr i o
rfAnyInstr RemFail Instr '[i] '[o]
l)
    AnnLAMBDA_REC Anns '[VarAnn, Notes i, Notes o]
ann RemFail Instr '[i, 'TLambda i o] '[o]
l -> Anns '[VarAnn, Notes i, Notes o]
-> AnnotateInstrArg
     '[VarAnn, Notes i, Notes o] ([ExpandedOp] -> ExpandedInstr)
-> [ExpandedOp]
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr Anns '[VarAnn, Notes i, Notes o]
ann AnnotateInstrArg
  '[VarAnn, Notes i, Notes o] ([ExpandedOp] -> ExpandedInstr)
VarAnn -> Ty -> Ty -> [ExpandedOp] -> ExpandedInstr
forall (f :: * -> *) op.
VarAnn -> Ty -> Ty -> f op -> InstrAbstract f op
U.LAMBDA_REC (UntypingOptions -> Instr '[i, 'TLambda i o] '[o] -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts (Instr '[i, 'TLambda i o] '[o] -> [ExpandedOp])
-> Instr '[i, 'TLambda i o] '[o] -> [ExpandedOp]
forall a b. (a -> b) -> a -> b
$ RemFail Instr '[i, 'TLambda i o] '[o]
-> Instr '[i, 'TLambda i o] '[o]
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
RemFail instr i o -> instr i o
rfAnyInstr RemFail Instr '[i, 'TLambda i o] '[o]
l)
    AnnEXEC AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.EXEC
    AnnAPPLY AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.APPLY
    DIP Instr a c
op -> [ExpandedOp] -> ExpandedInstr
forall (f :: * -> *) op. f op -> InstrAbstract f op
U.DIP (UntypingOptions -> Instr a c -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts Instr a c
op)
    DIPN PeanoNatural n
s Instr s s'
op ->
      Word -> [ExpandedOp] -> ExpandedInstr
forall (f :: * -> *) op. Word -> f op -> InstrAbstract f op
U.DIPN (forall a b. (HasCallStack, Integral a, Integral b) => a -> b
Unsafe.fromIntegral @Natural @Word (Natural -> Word) -> Natural -> Word
forall a b. (a -> b) -> a -> b
$ PeanoNatural n -> Natural
forall (n :: Peano). PeanoNatural n -> Natural
fromPeanoNatural PeanoNatural n
s) (UntypingOptions -> Instr s s' -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
opts Instr s s'
op)
    Instr inp out
FAILWITH -> ExpandedInstr
forall (f :: * -> *) op. InstrAbstract f op
U.FAILWITH
    AnnCAST Anns '[VarAnn, Notes a]
ann | Instr (a : s) (a : s)
_ :: Instr (a ': s) (a ': s) <- Instr inp out
i ->
      Anns '[VarAnn, Notes a]
-> AnnotateInstrArg '[VarAnn, Notes a] ExpandedInstr
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr Anns '[VarAnn, Notes a]
ann AnnotateInstrArg '[VarAnn, Notes a] ExpandedInstr
VarAnn -> Ty -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> Ty -> InstrAbstract f op
U.CAST
    AnnRENAME AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.RENAME
    AnnPACK AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.PACK
    AnnUNPACK Anns '[TypeAnn, VarAnn, Notes a]
ann
      | Instr ('TBytes : s) ('TOption a : s)
_ :: Instr ('TBytes ': s) ('TOption a ': s) <- Instr inp out
i ->
          Anns '[TypeAnn, VarAnn, Notes a]
-> AnnotateInstrArg '[TypeAnn, VarAnn, Notes a] ExpandedInstr
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr Anns '[TypeAnn, VarAnn, Notes a]
ann AnnotateInstrArg '[TypeAnn, VarAnn, Notes a] ExpandedInstr
TypeAnn -> VarAnn -> Ty -> ExpandedInstr
forall (f :: * -> *) op.
TypeAnn -> VarAnn -> Ty -> InstrAbstract f op
U.UNPACK
    AnnCONCAT AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.CONCAT
    AnnCONCAT' AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.CONCAT
    AnnSLICE AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.SLICE
    AnnISNAT AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.ISNAT
    AnnADD AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.ADD
    AnnSUB AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.SUB
    AnnSUB_MUTEZ AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.SUB_MUTEZ
    AnnMUL AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.MUL
    AnnEDIV AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.EDIV
    AnnABS AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.ABS
    AnnNEG AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.NEG
    AnnLSL AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.LSL
    AnnLSR AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.LSR
    AnnOR AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.OR
    AnnAND AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.AND
    AnnXOR AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.XOR
    AnnNOT AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.NOT
    AnnCOMPARE AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.COMPARE
    AnnEQ AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.EQ
    AnnNEQ AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.NEQ
    AnnLT AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.LT
    AnnGT AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.GT
    AnnLE AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.LE
    AnnGE AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.GE
    AnnINT AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.INT
    AnnNAT AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.NAT
    AnnBYTES AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.BYTES
    AnnVIEW Anns '[VarAnn, Notes ret]
ann ViewName
viewName -> Anns '[VarAnn, Notes ret]
-> AnnotateInstrArg '[VarAnn, Notes ret] ExpandedInstr
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr Anns '[VarAnn, Notes ret]
ann ((VarAnn -> ViewName -> Ty -> ExpandedInstr)
-> ViewName -> VarAnn -> Ty -> ExpandedInstr
forall a b c. (a -> b -> c) -> b -> a -> c
flip VarAnn -> ViewName -> Ty -> ExpandedInstr
forall (f :: * -> *) op.
VarAnn -> ViewName -> Ty -> InstrAbstract f op
U.VIEW ViewName
viewName)
    AnnSELF AnnVar
ann SomeEntrypointCallT arg
sepc ->
      AnnVar
-> AnnotateInstrArg '[VarAnn] (RootAnn -> ExpandedInstr)
-> RootAnn
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] (RootAnn -> ExpandedInstr)
VarAnn -> RootAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> RootAnn -> InstrAbstract f op
U.SELF (EpName -> RootAnn
epNameToRefAnn (EpName -> RootAnn) -> EpName -> RootAnn
forall a b. (a -> b) -> a -> b
$ SomeEntrypointCallT arg -> EpName
forall (arg :: T). SomeEntrypointCallT arg -> EpName
sepcName SomeEntrypointCallT arg
sepc)
    AnnCONTRACT Anns '[VarAnn, Notes p]
ann EpName
epName
      | Instr ('TAddress : s) ('TOption ('TContract p) : s)
_ :: Instr ('TAddress ': s) ('TOption ('TContract p) ': s) <- Instr inp out
i ->
          let fa :: RootAnn
fa = EpName -> RootAnn
epNameToRefAnn EpName
epName
          in Anns '[VarAnn, Notes p]
-> AnnotateInstrArg '[VarAnn, Notes p] ExpandedInstr
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr Anns '[VarAnn, Notes p]
ann ((VarAnn -> RootAnn -> Ty -> ExpandedInstr)
-> RootAnn -> VarAnn -> Ty -> ExpandedInstr
forall a b c. (a -> b -> c) -> b -> a -> c
flip VarAnn -> RootAnn -> Ty -> ExpandedInstr
forall (f :: * -> *) op.
VarAnn -> RootAnn -> Ty -> InstrAbstract f op
U.CONTRACT RootAnn
fa)
    AnnTRANSFER_TOKENS AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.TRANSFER_TOKENS
    AnnSET_DELEGATE AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.SET_DELEGATE
    AnnCREATE_CONTRACT Anns '[VarAnn, VarAnn]
ann Contract' Instr p g
contract
      | Instr
  ('TOption 'TKeyHash : 'TMutez : g : s)
  ('TOperation : 'TAddress : s)
_ :: Instr
          (  'TOption ('TKeyHash)
          ': 'TMutez
          ': g
          ': s)
          ('TOperation ': 'TAddress ': s) <- Instr inp out
i ->
        Anns '[VarAnn, VarAnn]
-> AnnotateInstrArg '[VarAnn, VarAnn] (Contract -> ExpandedInstr)
-> Contract
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr Anns '[VarAnn, VarAnn]
ann AnnotateInstrArg '[VarAnn, VarAnn] (Contract -> ExpandedInstr)
VarAnn -> VarAnn -> Contract -> ExpandedInstr
forall (f :: * -> *) op.
VarAnn -> VarAnn -> Contract' op -> InstrAbstract f op
U.CREATE_CONTRACT (UntypingOptions -> Contract' Instr p g -> Contract
forall (param :: T) (store :: T).
UntypingOptions -> Contract param store -> Contract
convertContract' UntypingOptions
opts Contract' Instr p g
contract)
    AnnIMPLICIT_ACCOUNT AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.IMPLICIT_ACCOUNT
    AnnNOW AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.NOW
    AnnAMOUNT AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.AMOUNT
    AnnBALANCE AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.BALANCE
    AnnVOTING_POWER AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.VOTING_POWER
    AnnTOTAL_VOTING_POWER AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.TOTAL_VOTING_POWER
    AnnCHECK_SIGNATURE AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.CHECK_SIGNATURE
    AnnSHA256 AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.SHA256
    AnnSHA512 AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.SHA512
    AnnBLAKE2B AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.BLAKE2B
    AnnSHA3 AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.SHA3
    AnnKECCAK AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.KECCAK
    AnnHASH_KEY AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.HASH_KEY
    AnnPAIRING_CHECK AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.PAIRING_CHECK
    AnnSOURCE AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.SOURCE
    AnnSENDER AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.SENDER
    AnnADDRESS AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.ADDRESS
    AnnCHAIN_ID AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.CHAIN_ID
    AnnLEVEL AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.LEVEL
    AnnSELF_ADDRESS AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.SELF_ADDRESS
    Instr inp out
NEVER -> ExpandedInstr
forall (f :: * -> *) op. InstrAbstract f op
U.NEVER
    AnnTICKET AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.TICKET
    AnnTICKET_DEPRECATED AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.TICKET_DEPRECATED
    AnnREAD_TICKET AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.READ_TICKET
    AnnSPLIT_TICKET AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.SPLIT_TICKET
    AnnJOIN_TICKETS AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.JOIN_TICKETS
    AnnOPEN_CHEST AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.OPEN_CHEST
    AnnSAPLING_EMPTY_STATE AnnVar
ann Sing n
s ->
      AnnVar
-> AnnotateInstrArg '[VarAnn] (Natural -> ExpandedInstr)
-> Natural
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] (Natural -> ExpandedInstr)
VarAnn -> Natural -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> Natural -> InstrAbstract f op
U.SAPLING_EMPTY_STATE (SingNat n -> Natural
forall (n :: Peano). SingNat n -> Natural
singPeanoVal Sing n
SingNat n
s)
    AnnSAPLING_VERIFY_UPDATE AnnVar
ann -> AnnVar -> AnnotateInstrArg '[VarAnn] ExpandedInstr -> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
ann AnnotateInstrArg '[VarAnn] ExpandedInstr
VarAnn -> ExpandedInstr
forall (f :: * -> *) op. VarAnn -> InstrAbstract f op
U.SAPLING_VERIFY_UPDATE
    AnnMIN_BLOCK_TIME [AnyAnn]
ann -> [AnyAnn] -> ExpandedInstr
forall (f :: * -> *) op. [AnyAnn] -> InstrAbstract f op
U.MIN_BLOCK_TIME [AnyAnn]
ann
    AnnEMIT AnnVar
va RootAnn
tag Maybe (Notes t)
ty -> AnnVar
-> AnnotateInstrArg
     '[VarAnn] (RootAnn -> Maybe Ty -> ExpandedInstr)
-> RootAnn
-> Maybe Ty
-> ExpandedInstr
forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr AnnVar
va AnnotateInstrArg '[VarAnn] (RootAnn -> Maybe Ty -> ExpandedInstr)
VarAnn -> RootAnn -> Maybe Ty -> ExpandedInstr
forall (f :: * -> *) op.
VarAnn -> RootAnn -> Maybe Ty -> InstrAbstract f op
U.EMIT RootAnn
tag (Maybe Ty -> ExpandedInstr) -> Maybe Ty -> ExpandedInstr
forall a b. (a -> b) -> a -> b
$ Notes t -> Ty
forall (x :: T). Notes x -> Ty
mkUType (Notes t -> Ty) -> Maybe (Notes t) -> Maybe Ty
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Notes t)
ty

untypeStackRef :: StackRef s -> U.StackRef
untypeStackRef :: forall (s :: [T]). StackRef s -> StackRef
untypeStackRef (StackRef PeanoNatural idx
n) = Natural -> StackRef
U.StackRef (PeanoNatural idx -> Natural
forall (n :: Peano). PeanoNatural n -> Natural
fromPeanoNatural PeanoNatural idx
n)

untypePrintComment :: PrintComment s -> U.PrintComment
untypePrintComment :: forall (s :: [T]). PrintComment s -> PrintComment
untypePrintComment (PrintComment [Either Text (StackRef s)]
pc) = [Either Text StackRef] -> PrintComment
U.PrintComment ([Either Text StackRef] -> PrintComment)
-> [Either Text StackRef] -> PrintComment
forall a b. (a -> b) -> a -> b
$ (Either Text (StackRef s) -> Either Text StackRef)
-> [Either Text (StackRef s)] -> [Either Text StackRef]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map ((StackRef s -> StackRef)
-> Either Text (StackRef s) -> Either Text StackRef
forall b c a. (b -> c) -> Either a b -> Either a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second StackRef s -> StackRef
forall (s :: [T]). StackRef s -> StackRef
untypeStackRef) [Either Text (StackRef s)]
pc

extInstrToOps :: ExtInstr s -> [U.ExpandedExtInstr]
extInstrToOps :: forall (s :: [T]). ExtInstr s -> [ExtInstrAbstract [] ExpandedOp]
extInstrToOps = \case
  PRINT PrintComment s
pc -> OneItem [ExtInstrAbstract [] ExpandedOp]
-> [ExtInstrAbstract [] ExpandedOp]
forall x. One x => OneItem x -> x
one (OneItem [ExtInstrAbstract [] ExpandedOp]
 -> [ExtInstrAbstract [] ExpandedOp])
-> OneItem [ExtInstrAbstract [] ExpandedOp]
-> [ExtInstrAbstract [] ExpandedOp]
forall a b. (a -> b) -> a -> b
$ PrintComment -> ExtInstrAbstract [] ExpandedOp
forall (f :: * -> *) op. PrintComment -> ExtInstrAbstract f op
U.UPRINT (PrintComment s -> PrintComment
forall (s :: [T]). PrintComment s -> PrintComment
untypePrintComment PrintComment s
pc)
  TEST_ASSERT (TestAssert Text
nm PrintComment s
pc Instr s ('TBool : out)
i) ->
    OneItem [ExtInstrAbstract [] ExpandedOp]
-> [ExtInstrAbstract [] ExpandedOp]
forall x. One x => OneItem x -> x
one (OneItem [ExtInstrAbstract [] ExpandedOp]
 -> [ExtInstrAbstract [] ExpandedOp])
-> OneItem [ExtInstrAbstract [] ExpandedOp]
-> [ExtInstrAbstract [] ExpandedOp]
forall a b. (a -> b) -> a -> b
$ TestAssert [] ExpandedOp -> ExtInstrAbstract [] ExpandedOp
forall (f :: * -> *) op. TestAssert f op -> ExtInstrAbstract f op
U.UTEST_ASSERT (TestAssert [] ExpandedOp -> ExtInstrAbstract [] ExpandedOp)
-> TestAssert [] ExpandedOp -> ExtInstrAbstract [] ExpandedOp
forall a b. (a -> b) -> a -> b
$
    Text -> PrintComment -> [ExpandedOp] -> TestAssert [] ExpandedOp
forall (f :: * -> *) op.
Text -> PrintComment -> f op -> TestAssert f op
U.TestAssert Text
nm (PrintComment s -> PrintComment
forall (s :: [T]). PrintComment s -> PrintComment
untypePrintComment PrintComment s
pc) (UntypingOptions -> Instr s ('TBool : out) -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
UntypingOptions -> Instr inp out -> [ExpandedOp]
instrToOpsImpl UntypingOptions
Readable Instr s ('TBool : out)
i)
  DOC_ITEM{} -> []
  COMMENT_ITEM CommentType
tp ->
    case CommentType
tp of
      FunctionStarts Text
name -> OneItem [ExtInstrAbstract [] ExpandedOp]
-> [ExtInstrAbstract [] ExpandedOp]
forall x. One x => OneItem x -> x
one (OneItem [ExtInstrAbstract [] ExpandedOp]
 -> [ExtInstrAbstract [] ExpandedOp])
-> OneItem [ExtInstrAbstract [] ExpandedOp]
-> [ExtInstrAbstract [] ExpandedOp]
forall a b. (a -> b) -> a -> b
$ Text -> ExtInstrAbstract [] ExpandedOp
forall (f :: * -> *) op. Text -> ExtInstrAbstract f op
U.UCOMMENT (Text -> ExtInstrAbstract [] ExpandedOp)
-> Text -> ExtInstrAbstract [] ExpandedOp
forall a b. (a -> b) -> a -> b
$ Text
name Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" [user func starts]"
      FunctionEnds Text
name -> OneItem [ExtInstrAbstract [] ExpandedOp]
-> [ExtInstrAbstract [] ExpandedOp]
forall x. One x => OneItem x -> x
one (OneItem [ExtInstrAbstract [] ExpandedOp]
 -> [ExtInstrAbstract [] ExpandedOp])
-> OneItem [ExtInstrAbstract [] ExpandedOp]
-> [ExtInstrAbstract [] ExpandedOp]
forall a b. (a -> b) -> a -> b
$ Text -> ExtInstrAbstract [] ExpandedOp
forall (f :: * -> *) op. Text -> ExtInstrAbstract f op
U.UCOMMENT (Text -> ExtInstrAbstract [] ExpandedOp)
-> Text -> ExtInstrAbstract [] ExpandedOp
forall a b. (a -> b) -> a -> b
$ Text
name Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" [user func ends]"
      StatementStarts Text
name -> OneItem [ExtInstrAbstract [] ExpandedOp]
-> [ExtInstrAbstract [] ExpandedOp]
forall x. One x => OneItem x -> x
one (OneItem [ExtInstrAbstract [] ExpandedOp]
 -> [ExtInstrAbstract [] ExpandedOp])
-> OneItem [ExtInstrAbstract [] ExpandedOp]
-> [ExtInstrAbstract [] ExpandedOp]
forall a b. (a -> b) -> a -> b
$ Text -> ExtInstrAbstract [] ExpandedOp
forall (f :: * -> *) op. Text -> ExtInstrAbstract f op
U.UCOMMENT (Text -> ExtInstrAbstract [] ExpandedOp)
-> Text -> ExtInstrAbstract [] ExpandedOp
forall a b. (a -> b) -> a -> b
$ Text
name Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" [user stmt starts]"
      StatementEnds Text
name -> OneItem [ExtInstrAbstract [] ExpandedOp]
-> [ExtInstrAbstract [] ExpandedOp]
forall x. One x => OneItem x -> x
one (OneItem [ExtInstrAbstract [] ExpandedOp]
 -> [ExtInstrAbstract [] ExpandedOp])
-> OneItem [ExtInstrAbstract [] ExpandedOp]
-> [ExtInstrAbstract [] ExpandedOp]
forall a b. (a -> b) -> a -> b
$ Text -> ExtInstrAbstract [] ExpandedOp
forall (f :: * -> *) op. Text -> ExtInstrAbstract f op
U.UCOMMENT (Text -> ExtInstrAbstract [] ExpandedOp)
-> Text -> ExtInstrAbstract [] ExpandedOp
forall a b. (a -> b) -> a -> b
$ Text
name Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" [user stmt ends]"
      JustComment Text
com -> OneItem [ExtInstrAbstract [] ExpandedOp]
-> [ExtInstrAbstract [] ExpandedOp]
forall x. One x => OneItem x -> x
one (OneItem [ExtInstrAbstract [] ExpandedOp]
 -> [ExtInstrAbstract [] ExpandedOp])
-> OneItem [ExtInstrAbstract [] ExpandedOp]
-> [ExtInstrAbstract [] ExpandedOp]
forall a b. (a -> b) -> a -> b
$ Text -> ExtInstrAbstract [] ExpandedOp
forall (f :: * -> *) op. Text -> ExtInstrAbstract f op
U.UCOMMENT Text
com
      StackTypeComment (Just [T]
stack) -> OneItem [ExtInstrAbstract [] ExpandedOp]
-> [ExtInstrAbstract [] ExpandedOp]
forall x. One x => OneItem x -> x
one (OneItem [ExtInstrAbstract [] ExpandedOp]
 -> [ExtInstrAbstract [] ExpandedOp])
-> OneItem [ExtInstrAbstract [] ExpandedOp]
-> [ExtInstrAbstract [] ExpandedOp]
forall a b. (a -> b) -> a -> b
$ Text -> ExtInstrAbstract [] ExpandedOp
forall (f :: * -> *) op. Text -> ExtInstrAbstract f op
U.UCOMMENT (Text -> ExtInstrAbstract [] ExpandedOp)
-> Text -> ExtInstrAbstract [] ExpandedOp
forall a b. (a -> b) -> a -> b
$ Doc -> Text
forall a b. (Buildable a, FromDoc b) => a -> b
pretty ([T] -> Doc
forall a (f :: * -> *). (Buildable a, Foldable f) => f a -> Doc
listF [T]
stack)
      StackTypeComment Maybe [T]
Nothing -> OneItem [ExtInstrAbstract [] ExpandedOp]
-> [ExtInstrAbstract [] ExpandedOp]
forall x. One x => OneItem x -> x
one (OneItem [ExtInstrAbstract [] ExpandedOp]
 -> [ExtInstrAbstract [] ExpandedOp])
-> OneItem [ExtInstrAbstract [] ExpandedOp]
-> [ExtInstrAbstract [] ExpandedOp]
forall a b. (a -> b) -> a -> b
$ Text -> ExtInstrAbstract [] ExpandedOp
forall (f :: * -> *) op. Text -> ExtInstrAbstract f op
U.UCOMMENT (Text -> ExtInstrAbstract [] ExpandedOp)
-> Text -> ExtInstrAbstract [] ExpandedOp
forall a b. (a -> b) -> a -> b
$ Doc -> Text
forall a. FromDoc a => Doc -> a
fmt Doc
"any stack type"
  STACKTYPE StackTypePattern
s -> OneItem [ExtInstrAbstract [] ExpandedOp]
-> [ExtInstrAbstract [] ExpandedOp]
forall x. One x => OneItem x -> x
one (OneItem [ExtInstrAbstract [] ExpandedOp]
 -> [ExtInstrAbstract [] ExpandedOp])
-> OneItem [ExtInstrAbstract [] ExpandedOp]
-> [ExtInstrAbstract [] ExpandedOp]
forall a b. (a -> b) -> a -> b
$ StackTypePattern -> ExtInstrAbstract [] ExpandedOp
forall (f :: * -> *) op. StackTypePattern -> ExtInstrAbstract f op
U.STACKTYPE StackTypePattern
s

-- | Extended equality of 'Instr' - this behaves like '(==)'
-- but does not require the compared instructions to be of strictly
-- the same type.
eqInstrExt :: Instr i1 o1 -> Instr i2 o2 -> Bool
eqInstrExt :: forall (i1 :: [T]) (o1 :: [T]) (i2 :: [T]) (o2 :: [T]).
Instr i1 o1 -> Instr i2 o2 -> Bool
eqInstrExt Instr i1 o1
i1 Instr i2 o2
i2 = Instr i1 o1 -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
Instr inp out -> [ExpandedOp]
instrToOps Instr i1 o1
i1 [ExpandedOp] -> [ExpandedOp] -> Bool
forall a. Eq a => a -> a -> Bool
== Instr i2 o2 -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
Instr inp out -> [ExpandedOp]
instrToOps Instr i2 o2
i2

-- It's an orphan instance, but it's better than checking all cases manually.
-- We can also move this convertion to the place where `Instr` is defined,
-- but then there will be a very large module (as we'll have to move a lot of
-- stuff as well).
instance Eq (Instr inp out) where
  == :: Instr inp out -> Instr inp out -> Bool
(==) = Instr inp out -> Instr inp out -> Bool
forall (i1 :: [T]) (o1 :: [T]) (i2 :: [T]) (o2 :: [T]).
Instr i1 o1 -> Instr i2 o2 -> Bool
eqInstrExt

instance SingI s => Eq (TestAssert s) where
  TestAssert   Text
name1 PrintComment s
pattern1 Instr s ('TBool : out)
instr1
    == :: TestAssert s -> TestAssert s -> Bool
==
    TestAssert Text
name2 PrintComment s
pattern2 Instr s ('TBool : out)
instr2
    = [Bool] -> Element [Bool]
forall c.
(Container c, BooleanMonoid (Element c)) =>
c -> Element c
and
    [ Text
name1 Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
name2
    , PrintComment s
pattern1 PrintComment s -> PrintComment s -> Bool
forall {k} (a1 :: k) (a2 :: k) (t :: k -> *).
(SingI a1, SingI a2, SDecide k, Eq (t a1)) =>
t a1 -> t a2 -> Bool
`eqParamSing` PrintComment s
pattern2
    , Instr s ('TBool : out)
instr1 Instr s ('TBool : out) -> Instr s ('TBool : out) -> Bool
forall (i1 :: [T]) (o1 :: [T]) (i2 :: [T]) (o2 :: [T]).
Instr i1 o1 -> Instr i2 o2 -> Bool
`eqInstrExt` Instr s ('TBool : out)
instr2
    ]

instance ForbidOp t => RenderDoc (Value' Instr t) where
  renderDoc :: RenderContext -> Value' Instr t -> Doc
renderDoc RenderContext
pn = RenderContext -> Value -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
pn (Value -> Doc)
-> (Value' Instr t -> Value) -> Value' Instr t -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value' Instr t -> Value
forall (t :: T). ForbidOp t => Value' Instr t -> Value
untypeValue

instance Buildable (Value' Instr t) where
  build :: Value' Instr t -> Doc
build Value' Instr t
val = let tv :: SingT t
tv = Value' Instr t -> (SingI t => SingT t) -> SingT t
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (SingI t => a) -> a
withValueTypeSanity Value' Instr t
val Sing t
SingT t
SingI t => SingT t
forall {k} (a :: k). SingI a => Sing a
sing
    in RenderContext
-> TPresence 'PSOp t -> (Value' Instr t, Sing t) -> Doc
forall (t :: T).
RenderContext
-> TPresence 'PSOp t -> (Value' Instr t, Sing t) -> Doc
renderDocSing RenderContext
doesntNeedParens (Sing 'PSOp -> Sing t -> TPresence 'PSOp t
forall (p :: TPredicateSym) (ty :: T).
Sing p -> Sing ty -> TPresence p ty
checkTPresence Sing 'PSOp
SingTPredicateSym 'PSOp
SPSOp Sing t
SingT t
tv) (Value' Instr t
val, Sing t
SingT t
tv)

instance RenderDoc (Instr inp out) where
  renderDoc :: RenderContext -> Instr inp out -> Doc
renderDoc RenderContext
context = RenderContext -> [ExpandedOp] -> Doc
forall a. RenderDoc a => RenderContext -> [a] -> Doc
renderDocList RenderContext
context ([ExpandedOp] -> Doc)
-> (Instr inp out -> [ExpandedOp]) -> Instr inp out -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr inp out -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
Instr inp out -> [ExpandedOp]
instrToOps

-- | Generate a value used for generating examples in documentation.
--
-- Since not for all types it is possible to produce a sensible example,
-- the result is optional. E.g. for operations, @never@, not proper
-- types like @contract operation@ we return 'Nothing'.
sampleTypedValue :: forall t. WellTyped t => Sing t -> Maybe (Value t)
sampleTypedValue :: forall (t :: T). WellTyped t => Sing t -> Maybe (Value t)
sampleTypedValue = \case
    Sing t
SingT t
STInt              -> Value t -> Maybe (Value t)
forall a. a -> Maybe a
Just (Value t -> Maybe (Value t)) -> Value t -> Maybe (Value t)
forall a b. (a -> b) -> a -> b
$ Integer -> Value' Instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt Integer
-1
    Sing t
SingT t
STNat              -> Value t -> Maybe (Value t)
forall a. a -> Maybe a
Just (Value t -> Maybe (Value t)) -> Value t -> Maybe (Value t)
forall a b. (a -> b) -> a -> b
$ Natural -> Value' Instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat Natural
0
    Sing t
SingT t
STString           -> Value t -> Maybe (Value t)
forall a. a -> Maybe a
Just (Value t -> Maybe (Value t)) -> Value t -> Maybe (Value t)
forall a b. (a -> b) -> a -> b
$ MText -> Value' Instr 'TString
forall (instr :: [T] -> [T] -> *). MText -> Value' instr 'TString
VString [mt|hello|]
    Sing t
SingT t
STMutez            -> Value t -> Maybe (Value t)
forall a. a -> Maybe a
Just (Value t -> Maybe (Value t)) -> Value t -> Maybe (Value t)
forall a b. (a -> b) -> a -> b
$ Mutez -> Value' Instr 'TMutez
forall (instr :: [T] -> [T] -> *). Mutez -> Value' instr 'TMutez
VMutez [tz|100u|]
    Sing t
SingT t
STBool             -> Value t -> Maybe (Value t)
forall a. a -> Maybe a
Just (Value t -> Maybe (Value t)) -> Value t -> Maybe (Value t)
forall a b. (a -> b) -> a -> b
$ Bool -> Value' Instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool Bool
True
    Sing t
SingT t
STKey              -> Value t -> Maybe (Value t)
forall a. a -> Maybe a
Just (Value t -> Maybe (Value t)) -> Value t -> Maybe (Value t)
forall a b. (a -> b) -> a -> b
$ PublicKey -> Value' Instr 'TKey
forall (instr :: [T] -> [T] -> *). PublicKey -> Value' instr 'TKey
VKey PublicKey
samplePublicKey
    Sing t
SingT t
STKeyHash          -> Value t -> Maybe (Value t)
forall a. a -> Maybe a
Just (Value t -> Maybe (Value t)) -> Value t -> Maybe (Value t)
forall a b. (a -> b) -> a -> b
$ KeyHash -> Value' Instr 'TKeyHash
forall (instr :: [T] -> [T] -> *).
KeyHash -> Value' instr 'TKeyHash
VKeyHash (KeyHash -> Value' Instr 'TKeyHash)
-> KeyHash -> Value' Instr 'TKeyHash
forall a b. (a -> b) -> a -> b
$ PublicKey -> KeyHash
hashKey PublicKey
samplePublicKey
    Sing t
SingT t
STBls12381Fr       -> Value t -> Maybe (Value t)
forall a. a -> Maybe a
Just (Value t -> Maybe (Value t)) -> Value t -> Maybe (Value t)
forall a b. (a -> b) -> a -> b
$ Bls12381Fr -> Value' Instr 'TBls12381Fr
forall (instr :: [T] -> [T] -> *).
Bls12381Fr -> Value' instr 'TBls12381Fr
VBls12381Fr Bls12381Fr
1
    Sing t
SingT t
STBls12381G1       -> Value t -> Maybe (Value t)
forall a. a -> Maybe a
Just (Value t -> Maybe (Value t)) -> Value t -> Maybe (Value t)
forall a b. (a -> b) -> a -> b
$ Bls12381G1 -> Value' Instr 'TBls12381G1
forall (instr :: [T] -> [T] -> *).
Bls12381G1 -> Value' instr 'TBls12381G1
VBls12381G1 Bls12381G1
BLS.g1One
    Sing t
SingT t
STBls12381G2       -> Value t -> Maybe (Value t)
forall a. a -> Maybe a
Just (Value t -> Maybe (Value t)) -> Value t -> Maybe (Value t)
forall a b. (a -> b) -> a -> b
$ Bls12381G2 -> Value' Instr 'TBls12381G2
forall (instr :: [T] -> [T] -> *).
Bls12381G2 -> Value' instr 'TBls12381G2
VBls12381G2 Bls12381G2
BLS.g2One
    Sing t
SingT t
STTimestamp        -> Value t -> Maybe (Value t)
forall a. a -> Maybe a
Just (Value t -> Maybe (Value t)) -> Value t -> Maybe (Value t)
forall a b. (a -> b) -> a -> b
$ Timestamp -> Value' Instr 'TTimestamp
forall (instr :: [T] -> [T] -> *).
Timestamp -> Value' instr 'TTimestamp
VTimestamp (Timestamp -> Value' Instr 'TTimestamp)
-> Timestamp -> Value' Instr 'TTimestamp
forall a b. (a -> b) -> a -> b
$ Integer -> Timestamp
timestampFromSeconds Integer
1564142952
    Sing t
SingT t
STBytes            -> Value t -> Maybe (Value t)
forall a. a -> Maybe a
Just (Value t -> Maybe (Value t)) -> Value t -> Maybe (Value t)
forall a b. (a -> b) -> a -> b
$ ByteString -> Value' Instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes ByteString
"\10"
    Sing t
SingT t
STAddress          -> Value t -> Maybe (Value t)
forall a. a -> Maybe a
Just (Value t -> Maybe (Value t)) -> Value t -> Maybe (Value t)
forall a b. (a -> b) -> a -> b
$ EpAddress -> Value' Instr 'TAddress
forall (instr :: [T] -> [T] -> *).
EpAddress -> Value' instr 'TAddress
VAddress (EpAddress -> Value' Instr 'TAddress)
-> EpAddress -> Value' Instr 'TAddress
forall a b. (a -> b) -> a -> b
$ EpAddress
sampleAddress
    Sing t
SingT t
STUnit             -> Value t -> Maybe (Value t)
forall a. a -> Maybe a
Just (Value t -> Maybe (Value t)) -> Value t -> Maybe (Value t)
forall a b. (a -> b) -> a -> b
$ Value t
Value' Instr 'TUnit
forall (instr :: [T] -> [T] -> *). Value' instr 'TUnit
VUnit
    Sing t
SingT t
STSignature        -> Value t -> Maybe (Value t)
forall a. a -> Maybe a
Just (Value t -> Maybe (Value t)) -> Value t -> Maybe (Value t)
forall a b. (a -> b) -> a -> b
$ Signature -> Value' Instr 'TSignature
forall (instr :: [T] -> [T] -> *).
Signature -> Value' instr 'TSignature
VSignature (Signature -> Value' Instr 'TSignature)
-> Signature -> Value' Instr 'TSignature
forall a b. (a -> b) -> a -> b
$ Signature
sampleSignature
    Sing t
SingT t
STChainId          -> Value t -> Maybe (Value t)
forall a. a -> Maybe a
Just (Value t -> Maybe (Value t)) -> Value t -> Maybe (Value t)
forall a b. (a -> b) -> a -> b
$ ChainId -> Value' Instr 'TChainId
forall (instr :: [T] -> [T] -> *).
ChainId -> Value' instr 'TChainId
VChainId ChainId
sampleChainId
    Sing t
SingT t
STOperation        -> Maybe (Value t)
forall a. Maybe a
Nothing
    -- It's not hard to generate a chest with a matching key, but
    -- representing those in source is extremely unwieldy due to large
    -- primes involved.
    Sing t
SingT t
STChest            -> Maybe (Value t)
forall a. Maybe a
Nothing
    Sing t
SingT t
STChestKey         -> Maybe (Value t)
forall a. Maybe a
Nothing
    Sing t
SingT t
STNever            -> Maybe (Value t)
forall a. Maybe a
Nothing
    STSaplingState Sing n
_   -> Maybe (Value t)
forall a. Maybe a
Nothing
    STSaplingTransaction Sing n
_ -> Maybe (Value t)
forall a. Maybe a
Nothing
    STOption Sing n
t -> Maybe (Value' Instr n) -> Value t
Maybe (Value' Instr n) -> Value' Instr ('TOption n)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
VOption (Maybe (Value' Instr n) -> Value t)
-> (Value' Instr n -> Maybe (Value' Instr n))
-> Value' Instr n
-> Value t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value' Instr n -> Maybe (Value' Instr n)
forall a. a -> Maybe a
Just (Value' Instr n -> Value t)
-> Maybe (Value' Instr n) -> Maybe (Value t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing n -> Maybe (Value' Instr n)
forall (t :: T). WellTyped t => Sing t -> Maybe (Value t)
sampleTypedValue Sing n
t
    STList Sing n
t -> [Value' Instr n] -> Value t
[Value' Instr n] -> Value' Instr ('TList n)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
[Value' instr t1] -> Value' instr ('TList t1)
VList ([Value' Instr n] -> Value t)
-> (Value' Instr n -> [Value' Instr n])
-> Value' Instr n
-> Value t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OneItem [Value' Instr n] -> [Value' Instr n]
Value' Instr n -> [Value' Instr n]
forall x. One x => OneItem x -> x
one (Value' Instr n -> Value t)
-> Maybe (Value' Instr n) -> Maybe (Value t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing n -> Maybe (Value' Instr n)
forall (t :: T). WellTyped t => Sing t -> Maybe (Value t)
sampleTypedValue Sing n
t
    STSet Sing n
t -> Set (Value' Instr n) -> Value t
Set (Value' Instr n) -> Value' Instr ('TSet n)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
Comparable t1 =>
Set (Value' instr t1) -> Value' instr ('TSet t1)
VSet (Set (Value' Instr n) -> Value t)
-> (Value' Instr n -> Set (Value' Instr n))
-> Value' Instr n
-> Value t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OneItem (Set (Value' Instr n)) -> Set (Value' Instr n)
Value' Instr n -> Set (Value' Instr n)
forall x. One x => OneItem x -> x
one (Value' Instr n -> Value t)
-> Maybe (Value' Instr n) -> Maybe (Value t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing n -> Maybe (Value' Instr n)
forall (t :: T). WellTyped t => Sing t -> Maybe (Value t)
sampleTypedValue Sing n
t
    STContract Sing n
_ -> Value t -> Maybe (Value t)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value t -> Maybe (Value t))
-> (SomeEntrypointCallT n -> Value t)
-> SomeEntrypointCallT n
-> Maybe (Value t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Address -> SomeEntrypointCallT n -> Value' Instr ('TContract n)
forall (arg :: T) (instr :: [T] -> [T] -> *).
(SingI arg, ForbidOp arg) =>
Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg)
VContract (EpAddress -> Address
eaAddress EpAddress
sampleAddress) (SomeEntrypointCallT n -> Maybe (Value t))
-> SomeEntrypointCallT n -> Maybe (Value t)
forall a b. (a -> b) -> a -> b
$ EntrypointCallT n n -> SomeEntrypointCallT n
forall (arg :: T) (param :: T).
ParameterScope param =>
EntrypointCallT param arg -> SomeEntrypointCallT arg
SomeEpc EntrypointCallT n n
forall (param :: T).
ParameterScope param =>
EntrypointCallT param param
unsafeEpcCallRoot
    STTicket Sing n
t -> do
      Value n
dat <- Sing n -> Maybe (Value n)
forall (t :: T). WellTyped t => Sing t -> Maybe (Value t)
sampleTypedValue Sing n
t
      VNat Natural
amount <- Sing 'TNat -> Maybe (Value' Instr 'TNat)
forall (t :: T). WellTyped t => Sing t -> Maybe (Value t)
sampleTypedValue Sing 'TNat
SingT 'TNat
STNat
      Value t -> Maybe (Value t)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value t -> Maybe (Value t)) -> Value t -> Maybe (Value t)
forall a b. (a -> b) -> a -> b
$ Address -> Value n -> Natural -> Value' Instr ('TTicket n)
forall (arg :: T) (instr :: [T] -> [T] -> *).
Comparable arg =>
Address
-> Value' instr arg -> Natural -> Value' instr ('TTicket arg)
VTicket (KindedAddress 'AddressKindContract -> Address
forall (kind :: AddressKind). KindedAddress kind -> Address
MkAddress KindedAddress 'AddressKindContract
sampleCTAddress) Value n
dat Natural
amount
    STPair Sing n1
t1 Sing n2
t2 -> (Value' Instr n1, Value' Instr n2) -> Value' Instr ('TPair n1 n2)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair ((Value' Instr n1, Value' Instr n2) -> Value' Instr ('TPair n1 n2))
-> (Value' Instr n1
    -> Value' Instr n2 -> (Value' Instr n1, Value' Instr n2))
-> Value' Instr n1
-> Value' Instr n2
-> Value t
forall a b c. SuperComposition a b c => a -> b -> c
... (,) (Value' Instr n1 -> Value' Instr n2 -> Value t)
-> Maybe (Value' Instr n1) -> Maybe (Value' Instr n2 -> Value t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing n1 -> Maybe (Value' Instr n1)
forall (t :: T). WellTyped t => Sing t -> Maybe (Value t)
sampleTypedValue Sing n1
t1 Maybe (Value' Instr n2 -> Value t)
-> Maybe (Value' Instr n2) -> Maybe (Value t)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sing n2 -> Maybe (Value' Instr n2)
forall (t :: T). WellTyped t => Sing t -> Maybe (Value t)
sampleTypedValue Sing n2
t2
    STOr Sing n1
tl Sing n2
tr ->
          Either (Value' Instr n1) (Value' Instr n2) -> Value t
Either (Value' Instr n1) (Value' Instr n2)
-> Value' Instr ('TOr n1 n2)
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 n1) (Value' Instr n2) -> Value t)
-> (Value' Instr n1 -> Either (Value' Instr n1) (Value' Instr n2))
-> Value' Instr n1
-> Value t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value' Instr n1 -> Either (Value' Instr n1) (Value' Instr n2)
forall a b. a -> Either a b
Left (Value' Instr n1 -> Value t)
-> Maybe (Value' Instr n1) -> Maybe (Value t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing n1 -> Maybe (Value' Instr n1)
forall (t :: T). WellTyped t => Sing t -> Maybe (Value t)
sampleTypedValue Sing n1
tl
      Maybe (Value t) -> Maybe (Value t) -> Maybe (Value t)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Either (Value' Instr n1) (Value' Instr n2) -> Value t
Either (Value' Instr n1) (Value' Instr n2)
-> Value' Instr ('TOr n1 n2)
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 n1) (Value' Instr n2) -> Value t)
-> (Value' Instr n2 -> Either (Value' Instr n1) (Value' Instr n2))
-> Value' Instr n2
-> Value t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value' Instr n2 -> Either (Value' Instr n1) (Value' Instr n2)
forall a b. b -> Either a b
Right (Value' Instr n2 -> Value t)
-> Maybe (Value' Instr n2) -> Maybe (Value t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing n2 -> Maybe (Value' Instr n2)
forall (t :: T). WellTyped t => Sing t -> Maybe (Value t)
sampleTypedValue Sing n2
tr
    STMap Sing n1
t1 Sing n2
t2 ->
      (\Value' Instr n1
k Value' Instr n2
v -> Map (Value' Instr n1) (Value' Instr n2)
-> Value' Instr ('TMap n1 n2)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(SingI v, Comparable k) =>
Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
VMap (Map (Value' Instr n1) (Value' Instr n2)
 -> Value' Instr ('TMap n1 n2))
-> Map (Value' Instr n1) (Value' Instr n2)
-> Value' Instr ('TMap n1 n2)
forall a b. (a -> b) -> a -> b
$ [(Value' Instr n1, Value' Instr n2)]
-> Map (Value' Instr n1) (Value' Instr n2)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Value' Instr n1
k, Value' Instr n2
v)]) (Value' Instr n1 -> Value' Instr n2 -> Value t)
-> Maybe (Value' Instr n1) -> Maybe (Value' Instr n2 -> Value t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing n1 -> Maybe (Value' Instr n1)
forall (t :: T). WellTyped t => Sing t -> Maybe (Value t)
sampleTypedValue Sing n1
t1 Maybe (Value' Instr n2 -> Value t)
-> Maybe (Value' Instr n2) -> Maybe (Value t)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sing n2 -> Maybe (Value' Instr n2)
forall (t :: T). WellTyped t => Sing t -> Maybe (Value t)
sampleTypedValue Sing n2
t2
    STBigMap Sing n1
t1 Sing n2
t2 -> (\Value' Instr n1
k Value' Instr n2
v -> Maybe Natural
-> Map (Value' Instr n1) (Value' Instr n2)
-> Value' Instr ('TBigMap n1 n2)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(SingI v, Comparable k, ForbidBigMap v) =>
Maybe Natural
-> Map (Value' instr k) (Value' instr v)
-> Value' instr ('TBigMap k v)
VBigMap Maybe Natural
forall a. Maybe a
Nothing (Map (Value' Instr n1) (Value' Instr n2)
 -> Value' Instr ('TBigMap n1 n2))
-> Map (Value' Instr n1) (Value' Instr n2)
-> Value' Instr ('TBigMap n1 n2)
forall a b. (a -> b) -> a -> b
$ [(Value' Instr n1, Value' Instr n2)]
-> Map (Value' Instr n1) (Value' Instr n2)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Value' Instr n1
k, Value' Instr n2
v)]) (Value' Instr n1 -> Value' Instr n2 -> Value t)
-> Maybe (Value' Instr n1) -> Maybe (Value' Instr n2 -> Value t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      Sing n1 -> Maybe (Value' Instr n1)
forall (t :: T). WellTyped t => Sing t -> Maybe (Value t)
sampleTypedValue Sing n1
t1 Maybe (Value' Instr n2 -> Value t)
-> Maybe (Value' Instr n2) -> Maybe (Value t)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sing n2 -> Maybe (Value' Instr n2)
forall (t :: T). WellTyped t => Sing t -> Maybe (Value t)
sampleTypedValue Sing n2
t2
    STLambda Sing n1
_ (Sing n2
t2 :: Sing t2) -> case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope t2) of
      Right Dict (ConstantScope n2)
Dict -> do
        Value n2
val <- Sing n2 -> Maybe (Value n2)
forall (t :: T). WellTyped t => Sing t -> Maybe (Value t)
sampleTypedValue Sing n2
t2
        pure $ (IsNotInView => RemFail Instr '[n1] '[n2])
-> Value' Instr ('TLambda n1 n2)
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 '[n1] '[n2])
 -> Value' Instr ('TLambda n1 n2))
-> (IsNotInView => RemFail Instr '[n1] '[n2])
-> Value' Instr ('TLambda n1 n2)
forall a b. (a -> b) -> a -> b
$ Instr '[n1] '[n2] -> RemFail Instr '[n1] '[n2]
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal (Instr '[n1] '[]
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr '[n1] '[] -> Instr '[] '[n2] -> Instr '[n1] '[n2]
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Value n2 -> Instr '[] '[n2]
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value n2
val)
      Either BadTypeForScope (Dict (ConstantScope n2))
_ -> Value t -> Maybe (Value t)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value t -> Maybe (Value t)) -> Value t -> Maybe (Value t)
forall a b. (a -> b) -> a -> b
$ (IsNotInView => RemFail Instr '[n1] '[n2])
-> Value' Instr ('TLambda n1 n2)
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 '[n1] '[n2])
 -> Value' Instr ('TLambda n1 n2))
-> (IsNotInView => RemFail Instr '[n1] '[n2])
-> Value' Instr ('TLambda n1 n2)
forall a b. (a -> b) -> a -> b
$ (forall (o' :: [T]). Instr '[n1] o') -> RemFail Instr '[n1] '[n2]
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
(forall (o' :: k). instr i o') -> RemFail instr i o
RfAlwaysFails (Value' Instr 'TString -> Instr '[n1] '[ 'TString, n1]
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH (MText -> Value' Instr 'TString
forall (instr :: [T] -> [T] -> *). MText -> Value' instr 'TString
VString [mt|lambda sample|]) Instr '[n1] '[ 'TString, n1]
-> Instr '[ 'TString, n1] o' -> Instr '[n1] o'
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr '[ 'TString, n1] o'
forall (a :: T) (s :: [T]) (out :: [T]).
(SingI a, ConstantScope a) =>
Instr (a : s) out
FAILWITH)
    where
      sampleCTAddress :: KindedAddress 'AddressKindContract
sampleCTAddress = [ta|KT1AEseqMV6fk2vtvQCVyA7ZCaxv7cpxtXdB|]
      sampleAddress :: EpAddress
sampleAddress = Either ParseEpAddressError EpAddress -> EpAddress
forall a b. (HasCallStack, Buildable a) => Either a b -> b
unsafe (Either ParseEpAddressError EpAddress -> EpAddress)
-> (Text -> Either ParseEpAddressError EpAddress)
-> Text
-> EpAddress
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Either ParseEpAddressError EpAddress
parseEpAddress (Text -> EpAddress) -> Text -> EpAddress
forall a b. (a -> b) -> a -> b
$ KindedAddress 'AddressKindContract -> Text
forall (kind :: AddressKind). KindedAddress kind -> Text
formatAddress KindedAddress 'AddressKindContract
sampleCTAddress
      samplePublicKey :: PublicKey
samplePublicKey = PublicKey -> Either CryptoParseError PublicKey -> PublicKey
forall b a. b -> Either a b -> b
fromRight (Text -> PublicKey
forall a. HasCallStack => Text -> a
error Text
"impossible") (Either CryptoParseError PublicKey -> PublicKey)
-> Either CryptoParseError PublicKey -> PublicKey
forall a b. (a -> b) -> a -> b
$ Text -> Either CryptoParseError PublicKey
parsePublicKey
        Text
"edpkuwTWKgQNnhR5v17H2DYHbfcxYepARyrPGbf1tbMoGQAj8Ljr3V"
      sampleSignature :: Signature
sampleSignature = Signature -> Either CryptoParseError Signature -> Signature
forall b a. b -> Either a b -> b
fromRight (Text -> Signature
forall a. HasCallStack => Text -> a
error Text
"impossible") (Either CryptoParseError Signature -> Signature)
-> Either CryptoParseError Signature -> Signature
forall a b. (a -> b) -> a -> b
$ Text -> Either CryptoParseError Signature
parseSignature
        Text
"edsigtrs8bK7vNfiR4Kd9dWasVa1bAWaQSu2ipnmLGZuwQa8ktCEMYVKqbWsbJ7zTS8dgYT9tiSUKorWCPFHosL5zPsiDwBQ6vb"
      sampleChainId :: ChainId
sampleChainId = ChainId -> Either ParseChainIdError ChainId -> ChainId
forall b a. b -> Either a b -> b
fromRight (Text -> ChainId
forall a. HasCallStack => Text -> a
error Text
"impossible") (Either ParseChainIdError ChainId -> ChainId)
-> Either ParseChainIdError ChainId -> ChainId
forall a b. (a -> b) -> a -> b
$ Text -> Either ParseChainIdError ChainId
parseChainId Text
"NetXUdfLh6Gm88t"

-- Misc
----------------------------------------------------------------------------

-- | Flatten a provided list of notes to a map of its entrypoints and its
-- corresponding utype. Please refer to 'U.mkEntrypointsMap' in regards to how
-- duplicate entrypoints are handled.
flattenEntrypoints :: U.HandleImplicitDefaultEp ->  ParamNotes t -> Map EpName U.Ty
flattenEntrypoints :: forall (t :: T).
HandleImplicitDefaultEp -> ParamNotes t -> Map EpName Ty
flattenEntrypoints HandleImplicitDefaultEp
hide = HandleImplicitDefaultEp -> ParameterType -> Map EpName Ty
U.mkEntrypointsMap HandleImplicitDefaultEp
hide (ParameterType -> Map EpName Ty)
-> (ParamNotes t -> ParameterType) -> ParamNotes t -> Map EpName Ty
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParamNotes t -> ParameterType
forall (cp :: T). ParamNotes cp -> ParameterType
convertParamNotes

-------------------------------------------------------------------------------
-- Rendering helpers
-------------------------------------------------------------------------------

-- | An extended version of renderDoc for typed values that handles VOp
-- accepts explicit singleton
renderDocSing :: RenderContext -> TPresence 'PSOp t -> (Value' Instr t, Sing t) -> Doc
renderDocSing :: forall (t :: T).
RenderContext
-> TPresence 'PSOp t -> (Value' Instr t, Sing t) -> Doc
renderDocSing RenderContext
pn = \case
  TPresence 'PSOp t
TAbsent -> RenderContext -> Value -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
pn (Value -> Doc)
-> ((Value' Instr t, SingT t) -> Value)
-> (Value' Instr t, SingT t)
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value' Instr t -> Value
forall (t :: T). ForbidOp t => Value' Instr t -> Value
untypeValue (Value' Instr t -> Value)
-> ((Value' Instr t, SingT t) -> Value' Instr t)
-> (Value' Instr t, SingT t)
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value' Instr t, SingT t) -> Value' Instr t
forall a b. (a, b) -> a
fst
  TPresence 'PSOp t
TPresent -> \case
    (VOp Operation' Instr
op, Sing t
_) -> Operation' Instr -> Doc
forall a. Buildable a => a -> Doc
build Operation' Instr
op
    -- other cases try to mimic instance RenderDoc U.Value, see "Michelson.Untyped.Value"
    (VOption Maybe (Value' Instr t1)
Nothing, Sing t
_) -> Doc
U.renderNone
    (VOption (Just Value' Instr t1
x), STOption Sing n
tx) -> RenderContext -> (RenderContext -> Doc) -> Doc
U.renderSome RenderContext
pn ((RenderContext -> Doc) -> Doc) -> (RenderContext -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ \RenderContext
ctx -> RenderContext
-> TPresence 'PSOp t1 -> (Value' Instr t1, Sing t1) -> Doc
forall (t :: T).
RenderContext
-> TPresence 'PSOp t -> (Value' Instr t, Sing t) -> Doc
renderDocSing RenderContext
ctx TPresence 'PSOp t1
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'True) =>
TPresence p t
TPresent (Value' Instr t1
x, Sing t1
Sing n
tx)
    (VList [Value' Instr t1]
xs, STList Sing n
txs) -> TPresence 'PSOp t1 -> Sing t1 -> [Value' Instr t1] -> Doc
forall (t :: T).
TPresence 'PSOp t -> Sing t -> [Value' Instr t] -> Doc
renderList TPresence 'PSOp t1
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'True) =>
TPresence p t
TPresent Sing t1
Sing n
txs [Value' Instr t1]
xs
    val :: (Value' Instr t, Sing t)
val@(VPair (Value' Instr l
_, (VPair (Value' Instr l
_, Value' Instr r
_))), Sing t
_) ->
      (Doc -> Doc) -> NonEmpty Doc -> Doc
forall e. (e -> Doc) -> NonEmpty e -> Doc
U.renderValuesList Doc -> Doc
forall a. a -> a
id (NonEmpty Doc -> Doc) -> NonEmpty Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (Value' Instr t, Sing t) -> NonEmpty Doc
forall (t :: T). (Value' Instr t, Sing t) -> NonEmpty Doc
renderLinearizedRightCombValuePair (Value' Instr t, Sing t)
val
    (VPair (Value' Instr l
l, Value' Instr r
r), STPair Sing n1
tl Sing n2
tr) -> RenderContext
-> (RenderContext -> Doc) -> (RenderContext -> Doc) -> Doc
U.renderPair RenderContext
pn (SingT l -> Value' Instr l -> RenderContext -> Doc
forall {t :: T}. SingT t -> Value' Instr t -> RenderContext -> Doc
render Sing n1
SingT l
tl Value' Instr l
l) (SingT r -> Value' Instr r -> RenderContext -> Doc
forall {t :: T}. SingT t -> Value' Instr t -> RenderContext -> Doc
render Sing n2
SingT r
tr Value' Instr r
r)
    (VOr (Left Value' Instr l
l), STOr Sing n1
tl Sing n2
_) -> RenderContext -> (RenderContext -> Doc) -> Doc
U.renderLeft RenderContext
pn ((RenderContext -> Doc) -> Doc) -> (RenderContext -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ SingT l -> Value' Instr l -> RenderContext -> Doc
forall {t :: T}. SingT t -> Value' Instr t -> RenderContext -> Doc
render Sing n1
SingT l
tl Value' Instr l
l
    (VOr (Right Value' Instr r
r), STOr Sing n1
_ Sing n2
tr) -> RenderContext -> (RenderContext -> Doc) -> Doc
U.renderRight RenderContext
pn ((RenderContext -> Doc) -> Doc) -> (RenderContext -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ SingT r -> Value' Instr r -> RenderContext -> Doc
forall {t :: T}. SingT t -> Value' Instr t -> RenderContext -> Doc
render Sing n2
SingT r
tr Value' Instr r
r
    (VMap Map (Value' Instr k) (Value' Instr v)
m, STMap Sing n1
tk Sing n2
tv) -> (Sing k, Sing v, TPresence 'PSOp v)
-> Map (Value' Instr k) (Value' Instr v) -> Doc
forall (tk :: T) (tv :: T).
ForbidOp tk =>
(Sing tk, Sing tv, TPresence 'PSOp tv)
-> Map (Value' Instr tk) (Value' Instr tv) -> Doc
renderMap (Sing k
Sing n1
tk, Sing v
Sing n2
tv, TPresence 'PSOp v
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'True) =>
TPresence p t
TPresent) Map (Value' Instr k) (Value' Instr v)
m ((ForbidOp k, ForbidNestedBigMaps k, ForbidTicket k,
  ForbidSaplingState k, ForbidBigMap k, ForbidContract k,
  ForbidNonComparable k) =>
 Doc)
-> Dict
     (ForbidOp k, ForbidNestedBigMaps k, ForbidTicket k,
      ForbidSaplingState k, ForbidBigMap k, ForbidContract k,
      ForbidNonComparable k)
-> Doc
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingT k
-> Dict
     (ForbidOp k, ForbidNestedBigMaps k, ForbidTicket k,
      ForbidSaplingState k, ForbidBigMap k, ForbidContract k,
      ForbidNonComparable k)
forall (t :: T) (proxy :: T -> *).
ForbidNonComparable t =>
proxy t -> Dict (ComparabilityImplies t)
comparableImplies Sing n1
SingT k
tk
    (VBigMap Maybe Natural
_ Map (Value' Instr k) (Value' Instr v)
m, STBigMap Sing n1
tk Sing n2
tv) -> (Sing k, Sing v, TPresence 'PSOp v)
-> Map (Value' Instr k) (Value' Instr v) -> Doc
forall (tk :: T) (tv :: T).
ForbidOp tk =>
(Sing tk, Sing tv, TPresence 'PSOp tv)
-> Map (Value' Instr tk) (Value' Instr tv) -> Doc
renderMap (Sing k
Sing n1
tk, Sing v
Sing n2
tv, TPresence 'PSOp v
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'True) =>
TPresence p t
TPresent) Map (Value' Instr k) (Value' Instr v)
m ((ForbidOp k, ForbidNestedBigMaps k, ForbidTicket k,
  ForbidSaplingState k, ForbidBigMap k, ForbidContract k,
  ForbidNonComparable k) =>
 Doc)
-> Dict
     (ForbidOp k, ForbidNestedBigMaps k, ForbidTicket k,
      ForbidSaplingState k, ForbidBigMap k, ForbidContract k,
      ForbidNonComparable k)
-> Doc
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingT k
-> Dict
     (ForbidOp k, ForbidNestedBigMaps k, ForbidTicket k,
      ForbidSaplingState k, ForbidBigMap k, ForbidContract k,
      ForbidNonComparable k)
forall (t :: T) (proxy :: T -> *).
ForbidNonComparable t =>
proxy t -> Dict (ComparabilityImplies t)
comparableImplies Sing n1
SingT k
tk
    (VSet{}, STSet Sing n
tv) -> case Sing t1 -> Comparability t1
forall (t :: T). Sing t -> Comparability t
checkComparability Sing t1
Sing n
tv of
    (VTicket{}, STTicket Sing n
tv) -> case Sing arg -> Comparability arg
forall (t :: T). Sing t -> Comparability t
checkComparability Sing arg
Sing n
tv of
  where render :: SingT t -> Value' Instr t -> RenderContext -> Doc
render SingT t
sg Value' Instr t
v RenderContext
ctx = RenderContext
-> TPresence 'PSOp t -> (Value' Instr t, Sing t) -> Doc
forall (t :: T).
RenderContext
-> TPresence 'PSOp t -> (Value' Instr t, Sing t) -> Doc
renderDocSing RenderContext
ctx (Sing 'PSOp -> Sing t -> TPresence 'PSOp t
forall (p :: TPredicateSym) (ty :: T).
Sing p -> Sing ty -> TPresence p ty
checkTPresence Sing 'PSOp
SingTPredicateSym 'PSOp
SPSOp Sing t
SingT t
sg) (Value' Instr t
v, Sing t
SingT t
sg)

renderList :: TPresence 'PSOp t -> Sing t -> [Value' Instr t] -> Doc
renderList :: forall (t :: T).
TPresence 'PSOp t -> Sing t -> [Value' Instr t] -> Doc
renderList TPresence 'PSOp t
osg Sing t
sg = (Value' Instr t -> Doc) -> [Value' Instr t] -> Doc
forall a. (a -> Doc) -> [a] -> Doc
renderList' ((Value' Instr t -> Doc) -> [Value' Instr t] -> Doc)
-> (Value' Instr t -> Doc) -> [Value' Instr t] -> Doc
forall a b. (a -> b) -> a -> b
$ RenderContext
-> TPresence 'PSOp t -> (Value' Instr t, Sing t) -> Doc
forall (t :: T).
RenderContext
-> TPresence 'PSOp t -> (Value' Instr t, Sing t) -> Doc
renderDocSing RenderContext
doesntNeedParens TPresence 'PSOp t
osg ((Value' Instr t, SingT t) -> Doc)
-> (Value' Instr t -> (Value' Instr t, SingT t))
-> Value' Instr t
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (, Sing t
SingT t
sg)

renderMap
  :: ForbidOp tk
  => (Sing tk, Sing tv, TPresence 'PSOp tv)
  -> Map (Value' Instr tk) (Value' Instr tv) -> Doc
renderMap :: forall (tk :: T) (tv :: T).
ForbidOp tk =>
(Sing tk, Sing tv, TPresence 'PSOp tv)
-> Map (Value' Instr tk) (Value' Instr tv) -> Doc
renderMap (Sing tk, Sing tv, TPresence 'PSOp tv)
ctx = ((Value' Instr tk, Value' Instr tv) -> Doc)
-> [(Value' Instr tk, Value' Instr tv)] -> Doc
forall a. (a -> Doc) -> [a] -> Doc
renderList' ((Sing tk, Sing tv, TPresence 'PSOp tv)
-> (Value' Instr tk, Value' Instr tv) -> Doc
forall (tk :: T) (tv :: T).
ForbidOp tk =>
(Sing tk, Sing tv, TPresence 'PSOp tv)
-> (Value' Instr tk, Value' Instr tv) -> Doc
renderElt (Sing tk, Sing tv, TPresence 'PSOp tv)
ctx) ([(Value' Instr tk, Value' Instr tv)] -> Doc)
-> (Map (Value' Instr tk) (Value' Instr tv)
    -> [(Value' Instr tk, Value' Instr tv)])
-> Map (Value' Instr tk) (Value' Instr tv)
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Value' Instr tk) (Value' Instr tv)
-> [(Value' Instr tk, Value' Instr tv)]
forall k a. Map k a -> [(k, a)]
Map.toList

renderList' :: (a -> Doc) -> [a] -> Doc
renderList' :: forall a. (a -> Doc) -> [a] -> Doc
renderList' a -> Doc
f = Doc -> (NonEmpty a -> Doc) -> Maybe (NonEmpty a) -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
"{ }" ((a -> Doc) -> NonEmpty a -> Doc
forall e. (e -> Doc) -> NonEmpty e -> Doc
U.renderValuesList a -> Doc
f) (Maybe (NonEmpty a) -> Doc)
-> ([a] -> Maybe (NonEmpty a)) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Maybe (NonEmpty a)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty

renderElt
  :: ForbidOp tk
  => (Sing tk, Sing tv, TPresence 'PSOp tv)
  -> (Value' Instr tk, Value' Instr tv) -> Doc
renderElt :: forall (tk :: T) (tv :: T).
ForbidOp tk =>
(Sing tk, Sing tv, TPresence 'PSOp tv)
-> (Value' Instr tk, Value' Instr tv) -> Doc
renderElt (Sing tk
tk, Sing tv
tv, TPresence 'PSOp tv
otv) (Value' Instr tk
k, Value' Instr tv
v) =
  (RenderContext -> Doc) -> (RenderContext -> Doc) -> Doc
U.renderElt' (TPresence 'PSOp tk
-> Value' Instr tk -> SingT tk -> RenderContext -> Doc
forall {t :: T}.
TPresence 'PSOp t
-> Value' Instr t -> SingT t -> RenderContext -> Doc
render TPresence 'PSOp tk
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'False) =>
TPresence p t
TAbsent Value' Instr tk
k Sing tk
SingT tk
tk) (TPresence 'PSOp tv
-> Value' Instr tv -> SingT tv -> RenderContext -> Doc
forall {t :: T}.
TPresence 'PSOp t
-> Value' Instr t -> SingT t -> RenderContext -> Doc
render TPresence 'PSOp tv
otv Value' Instr tv
v Sing tv
SingT tv
tv)
  where render :: TPresence 'PSOp t
-> Value' Instr t -> SingT t -> RenderContext -> Doc
render TPresence 'PSOp t
o Value' Instr t
x SingT t
tx RenderContext
ctx = RenderContext
-> TPresence 'PSOp t -> (Value' Instr t, Sing t) -> Doc
forall (t :: T).
RenderContext
-> TPresence 'PSOp t -> (Value' Instr t, Sing t) -> Doc
renderDocSing RenderContext
ctx TPresence 'PSOp t
o (Value' Instr t
x, Sing t
SingT t
tx)

-- | Mimics U.linearizeRightCombValuePair, but for typed values;
-- however, unlike U.linearizeRightCombValuePair renders values on-the-fly.
renderLinearizedRightCombValuePair :: (Value' Instr t, Sing t) -> NonEmpty Doc
renderLinearizedRightCombValuePair :: forall (t :: T). (Value' Instr t, Sing t) -> NonEmpty Doc
renderLinearizedRightCombValuePair = \case
  (VPair (Value' Instr l
l, Value' Instr r
r), STPair Sing n1
tl Sing n2
tr) -> RenderContext
-> TPresence 'PSOp l -> (Value' Instr l, Sing l) -> Doc
forall (t :: T).
RenderContext
-> TPresence 'PSOp t -> (Value' Instr t, Sing t) -> Doc
renderDocSing RenderContext
doesntNeedParens (Sing 'PSOp -> Sing l -> TPresence 'PSOp l
forall (p :: TPredicateSym) (ty :: T).
Sing p -> Sing ty -> TPresence p ty
checkTPresence Sing 'PSOp
SingTPredicateSym 'PSOp
SPSOp Sing l
Sing n1
tl) (Value' Instr l
l, Sing l
Sing n1
tl)
                               Doc -> NonEmpty Doc -> NonEmpty Doc
forall a. a -> NonEmpty a -> NonEmpty a
<| (Value' Instr r, Sing r) -> NonEmpty Doc
forall (t :: T). (Value' Instr t, Sing t) -> NonEmpty Doc
renderLinearizedRightCombValuePair (Value' Instr r
r, Sing r
Sing n2
tr)
  val :: (Value' Instr t, Sing t)
val@(Value' Instr t
_, Sing t
tv)                  -> RenderContext
-> TPresence 'PSOp t -> (Value' Instr t, Sing t) -> Doc
forall (t :: T).
RenderContext
-> TPresence 'PSOp t -> (Value' Instr t, Sing t) -> Doc
renderDocSing RenderContext
doesntNeedParens (Sing 'PSOp -> Sing t -> TPresence 'PSOp t
forall (p :: TPredicateSym) (ty :: T).
Sing p -> Sing ty -> TPresence p ty
checkTPresence Sing 'PSOp
SingTPredicateSym 'PSOp
SPSOp Sing t
tv) (Value' Instr t, Sing t)
val Doc -> [Doc] -> NonEmpty Doc
forall a. a -> [a] -> NonEmpty a
:| []