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

{-# OPTIONS_GHC -Wno-deprecations #-} -- due to temporary OPEN_CHEST deprecation

{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}

module Lorentz.Instr
  ( nop
  , drop
  , dropN
  , ConstraintDUPNLorentz
  , dup
  , dupNPeano
  , dupN
  , swap
  , ConstraintDIGLorentz
  , digPeano
  , dig
  , ConstraintDUGLorentz
  , dugPeano
  , dug
  , push
  , some
  , none
  , unit
  , ifNone
  , pair
  , car
  , cdr
  , unpair
  , left
  , right
  , ifLeft
  , nil
  , cons
  , size
  , emptySet
  , emptyMap
  , emptyBigMap
  , map
  , iter
  , mem
  , get
  , ConstraintPairGetLorentz
  , PairGetHs
  , pairGet
  , update
  , getAndUpdate
  , ConstraintPairUpdateLorentz
  , PairUpdateHs
  , pairUpdate
  , failingWhenPresent
  , updateNew
  , if_
  , ifCons
  , loop
  , loopLeft
  , lambda
  , lambdaRec
  , exec
  , execute
  , apply
  , applicate
  , dip
  , ConstraintDIPNLorentz
  , dipNPeano
  , dipN
  , failWith
  , cast
  , pack
  , unpack
  , packRaw
  , unpackRaw
  , concat
  , concat'
  , slice, isNat, add, sub, rsub, mul, ediv, abs
  , subMutez, rsubMutez
  , neg
  , lsl
  , lsr
  , or
  , and
  , xor
  , not
  , compare
  , eq0
  , neq0
  , lt0
  , gt0
  , le0
  , ge0
  , int
  , toTAddress_
  , view'
  , self
  , selfCalling
  , contract
  , contractCalling
  , unsafeContractCalling
  , runFutureContract
  , epAddressToContract
  , transferTokens
  , setDelegate
  , createContract
  , implicitAccount
  , now
  , minBlockTime
  , amount
  , balance
  , votingPower
  , totalVotingPower
  , checkSignature
  , sha256
  , sha512
  , blake2B
  , sha3
  , keccak
  , hashKey
  , pairingCheck
  , source
  , sender
  , address
  , selfAddress
  , ticket
  , ReadTicket
  , readTicket
  , splitTicket
  , splitTicketNamed
  , joinTickets
  , openChest
  , chainId
  , level
  , never
  , framed
  , emit
  , emit'
  , emitAuto
  , LorentzFunctor (..)
  ) where

import Prelude hiding
  (EQ, GT, LT, abs, and, compare, concat, drop, get, map, not, or, some, swap, xor)

import GHC.TypeNats (Nat)

import Lorentz.Address
import Lorentz.Annotation
import Lorentz.Arith
import Lorentz.Base
import Lorentz.Bytes
import Lorentz.Constraints
import Lorentz.Entrypoints
import Lorentz.Instr.Framed
import Lorentz.Lambda
import Lorentz.Polymorphic
import Lorentz.Value
import Lorentz.ViewBase
import Lorentz.Zip
import Morley.Michelson.Typed
  (ConstraintDIG, ConstraintDIG', ConstraintDIPN, ConstraintDIPN', ConstraintDUG, ConstraintDUG',
  ConstraintDUPN, ConstraintDUPN', ConstraintGetN, ConstraintUpdateN, EntrypointCallT(..), GetN,
  Instr(..), Notes, RemFail(..), SingI, SomeEntrypointCallT(..), UpdateN, pattern CAR, pattern CDR,
  pattern LEFT, pattern PAIR, pattern RIGHT, pattern UNPAIR, sepcName, starNotes)
import Morley.Michelson.Typed.Arith
import Morley.Michelson.Typed.Contract (giveNotInView)
import Morley.Michelson.Typed.Haskell.Value
import Morley.Michelson.Untyped (FieldAnn)
import Morley.Util.Named
import Morley.Util.Peano
import Morley.Util.PeanoNatural
import Morley.Util.Type
import Morley.Util.TypeLits

nop :: s :-> s
nop :: forall (s :: [*]). s :-> s
nop = Instr (ToTs s) (ToTs s) -> s :-> s
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs s) (ToTs s)
forall (inp :: [T]). Instr inp inp
Nop

drop :: a : s :-> s
drop :: forall a (s :: [*]). (a : s) :-> s
drop = Instr (ToTs (a : s)) (ToTs s) -> (a : s) :-> s
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (a : s)) (ToTs s)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP

-- | Drop top @n@ elements from the stack.
dropN ::
  forall (n :: Nat) (s :: [Type]).
  -- Note: if we introduce `nPeano ~ ToPeano n` variable,
  -- GHC will complain that this constraint is redundant.
  ( SingIPeano n
  , RequireLongerOrSameLength (ToTs s) (ToPeano n)
  -- ↓ Kinda obvious, but not to GHC.
  , Drop (ToPeano n) (ToTs s) ~ ToTs (Drop (ToPeano n) s)
  ) => s :-> Drop (ToPeano n) s
dropN :: forall (n :: Nat) (s :: [*]).
(SingIPeano n, RequireLongerOrSameLength (ToTs s) (ToPeano n),
 Drop (ToPeano n) (ToTs s) ~ ToTs (Drop (ToPeano n) s)) =>
s :-> Drop (ToPeano n) s
dropN = Instr (ToTs s) (ToTs (Drop (ToPeano n) s))
-> s :-> Drop (ToPeano n) s
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs s) (ToTs (Drop (ToPeano n) s))
 -> s :-> Drop (ToPeano n) s)
-> Instr (ToTs s) (ToTs (Drop (ToPeano n) s))
-> s :-> Drop (ToPeano n) s
forall a b. (a -> b) -> a -> b
$ PeanoNatural (ToPeano n)
-> Instr (ToTs s) (Drop (ToPeano n) (ToTs s))
forall (n :: Peano) (inp :: [T]).
RequireLongerOrSameLength inp n =>
PeanoNatural n -> Instr inp (Drop n inp)
DROPN (PeanoNatural (ToPeano n)
 -> Instr (ToTs s) (Drop (ToPeano n) (ToTs s)))
-> PeanoNatural (ToPeano n)
-> Instr (ToTs s) (Drop (ToPeano n) (ToTs s))
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SingIPeano n => PeanoNatural (ToPeano n)
toPeanoNatural' @n
  where
    _example :: '[ Integer, Integer, Integer ] :-> '[]
    _example :: '[Integer, Integer, Integer] :-> '[]
_example = forall (n :: Nat) (s :: [*]).
(SingIPeano n, RequireLongerOrSameLength (ToTs s) (ToPeano n),
 Drop (ToPeano n) (ToTs s) ~ ToTs (Drop (ToPeano n) s)) =>
s :-> Drop (ToPeano n) s
dropN @3

-- | Copies a stack argument.
--
-- Hit the 'Dupable' constraint?
-- Polymorphism and abstractions do not play very well with this constraint,
-- you can enjoy suffering from the linear types feature under various sauces:
--
-- 1. The most trivial option is to just propagate 'Dupable' constraint when you
--    want to use 'dup', this suits for case when you are not planning to work
--    with non-dupable types like tickets.
-- 2. Sometimes it is possible to avoid 'dup' and use other instructions instead
--    (e.g. 'unpair' allows splitting a pair without using 'dup's,
--     'getAndUpdate' allows accessing a map value without implicit duplication).
--    But you may have to learn to write code in a completely different way,
--    and the result may be less efficient comparing to the option with using
--    @dup@.
-- 3. Use 'decideOnDupable' to provide two code paths - when type is dupable
--    and when it is not.
dup :: forall a s. Dupable a => a : s :-> a : a : s
dup :: forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup = Instr (ToTs (a : s)) (ToTs (a : a : s)) -> (a : s) :-> (a : a : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (a : s)) (ToTs (a : a : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ (a : a : s), DupableScope a) =>
Instr inp out
DUP

type ConstraintDUPNLorentz (n :: Peano) (inp :: [Type]) (out :: [Type])
  (a :: Type) =
  ( ConstraintDUPN n (ToTs inp) (ToTs out) (ToT a)
  , ConstraintDUPN' Type n inp out a
  , SingI n
  )

dupNPeano ::
  forall (n :: Peano) a inp out.
  ( ConstraintDUPNLorentz n inp out a, Dupable a ) => inp :-> out
dupNPeano :: forall (n :: Peano) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz n inp out a, Dupable a) =>
inp :-> out
dupNPeano = Instr (ToTs inp) (ToTs out) -> inp :-> out
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs inp) (ToTs out) -> inp :-> out)
-> Instr (ToTs inp) (ToTs out) -> inp :-> out
forall a b. (a -> b) -> a -> b
$ PeanoNatural n
-> Instr
     (LazyTake (Decrement n) (ToTs inp) ++ (ToT a : Drop n (ToTs inp)))
     (ToT a
        : (LazyTake (Decrement n) (ToTs inp)
           ++ (ToT a : Drop n (ToTs inp))))
forall {inp :: [T]} {out :: [T]} (n :: Peano) (inp1 :: [T])
       (out1 :: [T]) (a :: T).
(inp ~ inp1, out ~ out1, ConstraintDUPN n inp1 out1 a,
 DupableScope a) =>
PeanoNatural n -> Instr inp out
DUPN (PeanoNatural n
 -> Instr
      (LazyTake (Decrement n) (ToTs inp) ++ (ToT a : Drop n (ToTs inp)))
      (ToT a
         : (LazyTake (Decrement n) (ToTs inp)
            ++ (ToT a : Drop n (ToTs inp)))))
-> PeanoNatural n
-> Instr
     (LazyTake (Decrement n) (ToTs inp) ++ (ToT a : Drop n (ToTs inp)))
     (ToT a
        : (LazyTake (Decrement n) (ToTs inp)
           ++ (ToT a : Drop n (ToTs inp))))
forall a b. (a -> b) -> a -> b
$ forall (n :: Peano). SingI n => PeanoNatural n
toPeanoNatural @n

dupN ::
  forall (n :: Nat) a inp out.
  ( ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a ) => inp :-> out
dupN :: forall (n :: Nat) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN = forall (n :: Peano) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz n inp out a, Dupable a) =>
inp :-> out
dupNPeano @(ToPeano n)
  where
    _example :: '[ Integer, (), Bool ] :-> '[ Bool, Integer, (), Bool ]
    _example :: '[Integer, (), Bool] :-> '[Bool, Integer, (), Bool]
_example = forall (n :: Nat) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @3

swap :: a : b : s :-> b : a : s
swap :: forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap = Instr (ToTs (a : b : s)) (ToTs (b : a : s))
-> (a : b : s) :-> (b : a : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (a : b : s)) (ToTs (b : a : s))
forall (a :: T) (b :: T) (s :: [T]). Instr (a : b : s) (b : a : s)
SWAP

-- See a comment about `ConstraintDIPNLorentz'.
type ConstraintDIGLorentz (n :: Peano) (inp :: [Type]) (out :: [Type])
  (a :: Type) =
  ( ConstraintDIG n (ToTs inp) (ToTs out) (ToT a)
  , ConstraintDIG' Type n inp out a
  , SingI n
  )

type ConstraintDUGLorentz (n :: Peano) (inp :: [Type]) (out :: [Type])
  (a :: Type) =
  ( ConstraintDUG n (ToTs inp) (ToTs out) (ToT a)
  , ConstraintDUG' Type n inp out a
  , SingI n
  )

-- | Version of `dig` which uses Peano number.
-- It is intended for internal usage in Lorentz.
digPeano ::
  forall (n :: Peano) inp out a.
  ( ConstraintDIGLorentz n inp out a
  ) => inp :-> out
digPeano :: forall (n :: Peano) (inp :: [*]) (out :: [*]) a.
ConstraintDIGLorentz n inp out a =>
inp :-> out
digPeano = Instr (ToTs inp) (ToTs out) -> inp :-> out
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs inp) (ToTs out) -> inp :-> out)
-> Instr (ToTs inp) (ToTs out) -> inp :-> out
forall a b. (a -> b) -> a -> b
$ PeanoNatural n
-> Instr
     (LazyTake n (Drop ('S 'Z) (ToTs out))
      ++ (ToT a : Drop ('S n) (ToTs out)))
     (ToT a : (LazyTake n (ToTs inp) ++ Drop ('S n) (ToTs inp)))
forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T).
ConstraintDIG n inp out a =>
PeanoNatural n -> Instr inp out
DIG (PeanoNatural n
 -> Instr
      (LazyTake n (Drop ('S 'Z) (ToTs out))
       ++ (ToT a : Drop ('S n) (ToTs out)))
      (ToT a : (LazyTake n (ToTs inp) ++ Drop ('S n) (ToTs inp))))
-> PeanoNatural n
-> Instr
     (LazyTake n (Drop ('S 'Z) (ToTs out))
      ++ (ToT a : Drop ('S n) (ToTs out)))
     (ToT a : (LazyTake n (ToTs inp) ++ Drop ('S n) (ToTs inp)))
forall a b. (a -> b) -> a -> b
$ forall (n :: Peano). SingI n => PeanoNatural n
toPeanoNatural @n

dig ::
  forall (n :: Nat) inp out a.
  ( ConstraintDIGLorentz (ToPeano n) inp out a
  ) => inp :-> out
dig :: forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDIGLorentz (ToPeano n) inp out a =>
inp :-> out
dig = forall (n :: Peano) (inp :: [*]) (out :: [*]) a.
ConstraintDIGLorentz n inp out a =>
inp :-> out
digPeano @(ToPeano n)
  where
    _example ::
      '[ Integer, Integer, Integer, Bool ] :->
      '[ Bool, Integer, Integer, Integer ]
    _example :: '[Integer, Integer, Integer, Bool]
:-> '[Bool, Integer, Integer, Integer]
_example = forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDIGLorentz (ToPeano n) inp out a =>
inp :-> out
dig @3

-- | Version of `dug` which uses Peano number.
-- It is intended for internal usage in Lorentz.
dugPeano ::
  forall (n :: Peano) inp out a.
  ( ConstraintDUGLorentz n inp out a
  ) => inp :-> out
dugPeano :: forall (n :: Peano) (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz n inp out a =>
inp :-> out
dugPeano = Instr (ToTs inp) (ToTs out) -> inp :-> out
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs inp) (ToTs out) -> inp :-> out)
-> Instr (ToTs inp) (ToTs out) -> inp :-> out
forall a b. (a -> b) -> a -> b
$ PeanoNatural n
-> Instr
     (ToT a : (LazyTake n (ToTs out) ++ Drop ('S n) (ToTs out)))
     (LazyTake n (Drop ('S 'Z) (ToTs inp))
      ++ (ToT a : Drop ('S n) (ToTs inp)))
forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T).
ConstraintDUG n inp out a =>
PeanoNatural n -> Instr inp out
DUG (PeanoNatural n
 -> Instr
      (ToT a : (LazyTake n (ToTs out) ++ Drop ('S n) (ToTs out)))
      (LazyTake n (Drop ('S 'Z) (ToTs inp))
       ++ (ToT a : Drop ('S n) (ToTs inp))))
-> PeanoNatural n
-> Instr
     (ToT a : (LazyTake n (ToTs out) ++ Drop ('S n) (ToTs out)))
     (LazyTake n (Drop ('S 'Z) (ToTs inp))
      ++ (ToT a : Drop ('S n) (ToTs inp)))
forall a b. (a -> b) -> a -> b
$ forall (n :: Peano). SingI n => PeanoNatural n
toPeanoNatural @n

dug ::
  forall (n :: Nat) inp out a.
  ( ConstraintDUGLorentz (ToPeano n) inp out a
  ) => inp :-> out
dug :: forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz (ToPeano n) inp out a =>
inp :-> out
dug = forall (n :: Peano) (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz n inp out a =>
inp :-> out
dugPeano @(ToPeano n)
  where
    _example ::
      '[ Bool, Integer, Integer, Integer ] :->
      '[ Integer, Integer, Integer, Bool ]
    _example :: '[Bool, Integer, Integer, Integer]
:-> '[Integer, Integer, Integer, Bool]
_example = forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz (ToPeano n) inp out a =>
inp :-> out
dug @3

push :: forall t s . NiceConstant t => t -> (s :-> t : s)
push :: forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push t
a = Instr (ToTs s) (ToTs (t : s)) -> s :-> (t : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs s) (ToTs (t : s)) -> s :-> (t : s))
-> Instr (ToTs s) (ToTs (t : s)) -> s :-> (t : s)
forall a b. (a -> b) -> a -> b
$ Value' Instr (ToT t) -> Instr (ToTs s) (ToT t : ToTs s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH (t -> Value' Instr (ToT t)
forall a. IsoValue a => a -> Value (ToT a)
toVal t
a)

some :: a : s :-> Maybe a : s
some :: forall a (s :: [*]). (a : s) :-> (Maybe a : s)
some = Instr (ToTs (a : s)) (ToTs (Maybe a : s))
-> (a : s) :-> (Maybe a : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (a : s)) (ToTs (Maybe a : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ ('TOption a : s)) =>
Instr inp out
SOME

none :: forall a s . KnownValue a => s :-> (Maybe a : s)
none :: forall a (s :: [*]). KnownValue a => s :-> (Maybe a : s)
none = Instr (ToTs s) (ToTs (Maybe a : s)) -> s :-> (Maybe a : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs s) (ToTs (Maybe a : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ s, out ~ ('TOption a : s), SingI a) =>
Instr inp out
NONE

unit :: s :-> () : s
unit :: forall (s :: [*]). s :-> (() : s)
unit = Instr (ToTs s) (ToTs (() : s)) -> s :-> (() : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs s) (ToTs (() : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TUnit : s)) =>
Instr inp out
UNIT

ifNone
  :: (s :-> s') -> (a : s :-> s') -> (Maybe a : s :-> s')
ifNone :: forall (s :: [*]) (s' :: [*]) a.
(s :-> s') -> ((a : s) :-> s') -> (Maybe a : s) :-> s'
ifNone = (forall (s' :: [T]).
 Instr (ToTs s) s'
 -> Instr (ToTs (a : s)) s' -> Instr (ToTs (Maybe a : s)) s')
-> (s :-> s') -> ((a : s) :-> s') -> (Maybe a : s) :-> s'
forall (a :: [*]) (b :: [*]) (c :: [*]) (s :: [*]).
(forall (s' :: [T]).
 Instr (ToTs a) s' -> Instr (ToTs b) s' -> Instr (ToTs c) s')
-> (a :-> s) -> (b :-> s) -> c :-> s
iGenericIf forall (s' :: [T]).
Instr (ToTs s) s'
-> Instr (ToTs (a : s)) s' -> Instr (ToTs (Maybe a : s)) s'
forall (s :: [T]) (out :: [T]) (a :: T).
Instr s out -> Instr (a : s) out -> Instr ('TOption a : s) out
IF_NONE

pair :: a : b : s :-> (a, b) : s
pair :: forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair = Instr (ToTs (a : b : s)) (ToTs ((a, b) : s))
-> (a : b : s) :-> ((a, b) : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (a : b : s)) (ToTs ((a, b) : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (a : b : s), out ~ ('TPair a b : s)) =>
Instr inp out
PAIR

car :: (a, b) : s :-> a : s
car :: forall a b (s :: [*]). ((a, b) : s) :-> (a : s)
car = Instr (ToTs ((a, b) : s)) (ToTs (a : s))
-> ((a, b) : s) :-> (a : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs ((a, b) : s)) (ToTs (a : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (a : s)) =>
Instr inp out
CAR

cdr :: (a, b) : s :-> b : s
cdr :: forall a b (s :: [*]). ((a, b) : s) :-> (b : s)
cdr = Instr (ToTs ((a, b) : s)) (ToTs (b : s))
-> ((a, b) : s) :-> (b : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs ((a, b) : s)) (ToTs (b : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (b : s)) =>
Instr inp out
CDR

unpair :: (a, b) : s :-> a : b : s
unpair :: forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair = Instr (ToTs ((a, b) : s)) (ToTs (a : b : s))
-> ((a, b) : s) :-> (a : b : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs ((a, b) : s)) (ToTs (a : b : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (a : b : s)) =>
Instr inp out
UNPAIR

left :: forall a b s. KnownValue b => a : s :-> Either a b : s
left :: forall a b (s :: [*]). KnownValue b => (a : s) :-> (Either a b : s)
left = Instr (ToTs (a : s)) (ToTs (Either a b : s))
-> (a : s) :-> (Either a b : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (a : s)) (ToTs (Either a b : s))
forall {inp :: [T]} {out :: [T]} (b :: T) (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ ('TOr a b : s), SingI b) =>
Instr inp out
LEFT

right :: forall a b s. KnownValue a => b : s :-> Either a b : s
right :: forall a b (s :: [*]). KnownValue a => (b : s) :-> (Either a b : s)
right = Instr (ToTs (b : s)) (ToTs (Either a b : s))
-> (b : s) :-> (Either a b : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (b : s)) (ToTs (Either a b : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (b : s), out ~ ('TOr a b : s), SingI a) =>
Instr inp out
RIGHT

ifLeft
  :: (a : s :-> s') -> (b : s :-> s') -> (Either a b : s :-> s')
ifLeft :: forall a (s :: [*]) (s' :: [*]) b.
((a : s) :-> s') -> ((b : s) :-> s') -> (Either a b : s) :-> s'
ifLeft = (forall (s' :: [T]).
 Instr (ToTs (a : s)) s'
 -> Instr (ToTs (b : s)) s' -> Instr (ToTs (Either a b : s)) s')
-> ((a : s) :-> s') -> ((b : s) :-> s') -> (Either a b : s) :-> s'
forall (a :: [*]) (b :: [*]) (c :: [*]) (s :: [*]).
(forall (s' :: [T]).
 Instr (ToTs a) s' -> Instr (ToTs b) s' -> Instr (ToTs c) s')
-> (a :-> s) -> (b :-> s) -> c :-> s
iGenericIf forall (s' :: [T]).
Instr (ToTs (a : s)) s'
-> Instr (ToTs (b : s)) s' -> Instr (ToTs (Either a b : s)) s'
forall (a :: T) (s :: [T]) (out :: [T]) (b :: T).
Instr (a : s) out -> Instr (b : s) out -> Instr ('TOr a b : s) out
IF_LEFT

nil :: KnownValue p => s :-> List p : s
nil :: forall p (s :: [*]). KnownValue p => s :-> (List p : s)
nil = Instr (ToTs s) (ToTs (List p : s)) -> s :-> (List p : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs s) (ToTs (List p : s))
forall {inp :: [T]} {out :: [T]} (p :: T) (s :: [T]).
(inp ~ s, out ~ ('TList p : s), SingI p) =>
Instr inp out
NIL

cons :: a : List a : s :-> List a : s
cons :: forall a (s :: [*]). (a : List a : s) :-> (List a : s)
cons = Instr (ToTs (a : List a : s)) (ToTs (List a : s))
-> (a : List a : s) :-> (List a : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (a : List a : s)) (ToTs (List a : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : 'TList a : s), out ~ ('TList a : s)) =>
Instr inp out
CONS

ifCons
  :: (a : List a : s :-> s') -> (s :-> s') -> (List a : s :-> s')
ifCons :: forall a (s :: [*]) (s' :: [*]).
((a : List a : s) :-> s') -> (s :-> s') -> (List a : s) :-> s'
ifCons = (forall (s' :: [T]).
 Instr (ToTs (a : List a : s)) s'
 -> Instr (ToTs s) s' -> Instr (ToTs (List a : s)) s')
-> ((a : List a : s) :-> s') -> (s :-> s') -> (List a : s) :-> s'
forall (a :: [*]) (b :: [*]) (c :: [*]) (s :: [*]).
(forall (s' :: [T]).
 Instr (ToTs a) s' -> Instr (ToTs b) s' -> Instr (ToTs c) s')
-> (a :-> s) -> (b :-> s) -> c :-> s
iGenericIf forall (s' :: [T]).
Instr (ToTs (a : List a : s)) s'
-> Instr (ToTs s) s' -> Instr (ToTs (List a : s)) s'
forall (a :: T) (s :: [T]) (out :: [T]).
Instr (a : 'TList a : s) out
-> Instr s out -> Instr ('TList a : s) out
IF_CONS

size :: SizeOpHs c => c : s :-> Natural : s
size :: forall c (s :: [*]). SizeOpHs c => (c : s) :-> (Natural : s)
size = Instr (ToTs (c : s)) (ToTs (Natural : s))
-> (c : s) :-> (Natural : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (c : s)) (ToTs (Natural : s))
forall {inp :: [T]} {out :: [T]} (c :: T) (s :: [T]).
(inp ~ (c : s), out ~ ('TNat : s), SizeOp c) =>
Instr inp out
SIZE

emptySet :: (NiceComparable e) => s :-> Set e : s
emptySet :: forall e (s :: [*]). NiceComparable e => s :-> (Set e : s)
emptySet = Instr (ToTs s) (ToTs (Set e : s)) -> s :-> (Set e : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs s) (ToTs (Set e : s))
forall {inp :: [T]} {out :: [T]} (e :: T) (s :: [T]).
(inp ~ s, out ~ ('TSet e : s), SingI e, Comparable e) =>
Instr inp out
EMPTY_SET

emptyMap :: (NiceComparable k, KnownValue v)
         => s :-> Map k v : s
emptyMap :: forall k v (s :: [*]).
(NiceComparable k, KnownValue v) =>
s :-> (Map k v : s)
emptyMap = Instr (ToTs s) (ToTs (Map k v : s)) -> s :-> (Map k v : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs s) (ToTs (Map k v : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ s, out ~ ('TMap a b : s), SingI a, SingI b, Comparable a) =>
Instr inp out
EMPTY_MAP

emptyBigMap :: (NiceComparable k, KnownValue v, NiceNoBigMap v)
            => s :-> BigMap k v : s
emptyBigMap :: forall k v (s :: [*]).
(NiceComparable k, KnownValue v, NiceNoBigMap v) =>
s :-> (BigMap k v : s)
emptyBigMap = Instr (ToTs s) (ToTs (BigMap k v : s)) -> s :-> (BigMap k v : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs s) (ToTs (BigMap k v : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ s, out ~ ('TBigMap a b : s), SingI a, SingI b, Comparable a,
 HasNoBigMap b) =>
Instr inp out
EMPTY_BIG_MAP

map
  :: (MapOpHs c, IsoMapOpRes c b, KnownValue b, HasCallStack)
  => (MapOpInpHs c : s :-> b : s) -> (c : s :-> MapOpResHs c b : s)
map :: forall c b (s :: [*]).
(MapOpHs c, IsoMapOpRes c b, KnownValue b, HasCallStack) =>
((MapOpInpHs c : s) :-> (b : s))
-> (c : s) :-> (MapOpResHs c b : s)
map (((MapOpInpHs c : s) :-> (b : s))
-> Instr (ToTs (MapOpInpHs c : s)) (ToTs (b : s))
forall (inp :: [*]) (out :: [*]).
HasCallStack =>
(inp :-> out) -> Instr (ToTs inp) (ToTs out)
iNonFailingCode -> Instr (ToTs (MapOpInpHs c : s)) (ToTs (b : s))
action) = Instr (ToTs (c : s)) (ToTs (MapOpResHs c b : s))
-> (c : s) :-> (MapOpResHs c b : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (MapOpInp (ToT c) : ToTs s) (ToT b : ToTs s)
-> Instr (ToT c : ToTs s) (MapOpRes (ToT c) (ToT b) : ToTs s)
forall {inp :: [T]} {out :: [T]} (c :: T) (b :: T) (s :: [T]).
(inp ~ (c : s), out ~ (MapOpRes c b : s), MapOp c, SingI b) =>
Instr (MapOpInp c : s) (b : s) -> Instr inp out
MAP Instr (MapOpInp (ToT c) : ToTs s) (ToT b : ToTs s)
Instr (ToTs (MapOpInpHs c : s)) (ToTs (b : s))
action)

iter
  :: (IterOpHs c, HasCallStack)
  => (IterOpElHs c : s :-> s) -> (c : s :-> s)
iter :: forall c (s :: [*]).
(IterOpHs c, HasCallStack) =>
((IterOpElHs c : s) :-> s) -> (c : s) :-> s
iter (((IterOpElHs c : s) :-> s)
-> Instr (ToTs (IterOpElHs c : s)) (ToTs s)
forall (inp :: [*]) (out :: [*]).
HasCallStack =>
(inp :-> out) -> Instr (ToTs inp) (ToTs out)
iNonFailingCode -> Instr (ToTs (IterOpElHs c : s)) (ToTs s)
action) = Instr (ToTs (c : s)) (ToTs s) -> (c : s) :-> s
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (IterOpEl (ToT c) : ToTs s) (ToTs s)
-> Instr (ToT c : ToTs s) (ToTs s)
forall (c :: T) (out :: [T]).
IterOp c =>
Instr (IterOpEl c : out) out -> Instr (c : out) out
ITER Instr (IterOpEl (ToT c) : ToTs s) (ToTs s)
Instr (ToTs (IterOpElHs c : s)) (ToTs s)
action)

mem :: MemOpHs c => MemOpKeyHs c : c : s :-> Bool : s
mem :: forall c (s :: [*]).
MemOpHs c =>
(MemOpKeyHs c : c : s) :-> (Bool : s)
mem = Instr (ToTs (MemOpKeyHs c : c : s)) (ToTs (Bool : s))
-> (MemOpKeyHs c : c : s) :-> (Bool : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (MemOpKeyHs c : c : s)) (ToTs (Bool : s))
forall {inp :: [T]} {out :: [T]} (c :: T) (s :: [T]).
(inp ~ (MemOpKey c : c : s), out ~ ('TBool : s), MemOp c) =>
Instr inp out
MEM

get
  :: (GetOpHs c, KnownValue (GetOpValHs c))
  => GetOpKeyHs c : c : s :-> Maybe (GetOpValHs c) : s
get :: forall c (s :: [*]).
(GetOpHs c, KnownValue (GetOpValHs c)) =>
(GetOpKeyHs c : c : s) :-> (Maybe (GetOpValHs c) : s)
get = Instr
  (ToTs (GetOpKeyHs c : c : s)) (ToTs (Maybe (GetOpValHs c) : s))
-> (GetOpKeyHs c : c : s) :-> (Maybe (GetOpValHs c) : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr
  (ToTs (GetOpKeyHs c : c : s)) (ToTs (Maybe (GetOpValHs c) : s))
forall {inp :: [T]} {out :: [T]} (c :: T) (s :: [T]).
(inp ~ (GetOpKey c : c : s), out ~ ('TOption (GetOpVal c) : s),
 GetOp c, SingI (GetOpVal c)) =>
Instr inp out
GET

type ConstraintPairGetLorentz (n :: Nat) (pair :: Type) =
  ( ConstraintGetN (ToPeano n) (ToT pair)
  , ToT (PairGetHs (ToPeano n) pair) ~ GetN (ToPeano n) (ToT pair)
  , SingIPeano n
  )

type family PairGetHs (ix :: Peano) (pair :: Type) :: Type where
  PairGetHs 'Z val                 = val
  PairGetHs ('S 'Z) (left, _)      = left
  PairGetHs ('S ('S n)) (_, right) = PairGetHs n right

pairGet
  :: forall (n :: Nat) (pair :: Type) (s :: [Type]).
     ConstraintPairGetLorentz n pair
  => pair : s :-> PairGetHs (ToPeano n) pair : s
pairGet :: forall (n :: Nat) pair (s :: [*]).
ConstraintPairGetLorentz n pair =>
(pair : s) :-> (PairGetHs (ToPeano n) pair : s)
pairGet = Instr (ToTs (pair : s)) (ToTs (PairGetHs (ToPeano n) pair : s))
-> (pair : s) :-> (PairGetHs (ToPeano n) pair : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs (pair : s)) (ToTs (PairGetHs (ToPeano n) pair : s))
 -> (pair : s) :-> (PairGetHs (ToPeano n) pair : s))
-> Instr (ToTs (pair : s)) (ToTs (PairGetHs (ToPeano n) pair : s))
-> (pair : s) :-> (PairGetHs (ToPeano n) pair : s)
forall a b. (a -> b) -> a -> b
$ PeanoNatural (ToPeano n)
-> Instr (ToT pair : ToTs s) (GetN (ToPeano n) (ToT pair) : ToTs s)
forall {inp :: [T]} {out :: [T]} (ix :: Peano) (pair :: T)
       (s :: [T]).
(inp ~ (pair : s), out ~ (GetN ix pair : s),
 ConstraintGetN ix pair) =>
PeanoNatural ix -> Instr inp out
GETN (PeanoNatural (ToPeano n)
 -> Instr
      (ToT pair : ToTs s) (GetN (ToPeano n) (ToT pair) : ToTs s))
-> PeanoNatural (ToPeano n)
-> Instr (ToT pair : ToTs s) (GetN (ToPeano n) (ToT pair) : ToTs s)
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SingIPeano n => PeanoNatural (ToPeano n)
toPeanoNatural' @n
  where
    _example :: '[ (Integer, Natural), () ] :-> '[ Integer, () ]
    _example :: '[(Integer, Natural), ()] :-> '[Integer, ()]
_example = forall (n :: Nat) pair (s :: [*]).
ConstraintPairGetLorentz n pair =>
(pair : s) :-> (PairGetHs (ToPeano n) pair : s)
pairGet @1

update :: UpdOpHs c => UpdOpKeyHs c : UpdOpParamsHs c : c : s :-> c : s
update :: forall c (s :: [*]).
UpdOpHs c =>
(UpdOpKeyHs c : UpdOpParamsHs c : c : s) :-> (c : s)
update = Instr
  (ToTs (UpdOpKeyHs c : UpdOpParamsHs c : c : s)) (ToTs (c : s))
-> (UpdOpKeyHs c : UpdOpParamsHs c : c : s) :-> (c : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr
  (ToTs (UpdOpKeyHs c : UpdOpParamsHs c : c : s)) (ToTs (c : s))
forall {inp :: [T]} {out :: [T]} (c :: T) (s :: [T]).
(inp ~ (UpdOpKey c : UpdOpParams c : c : s), out ~ (c : s),
 UpdOp c) =>
Instr inp out
UPDATE

getAndUpdate
  :: (GetOpHs c, UpdOpHs c, KnownValue (GetOpValHs c), UpdOpKeyHs c ~ GetOpKeyHs c)
  => UpdOpKeyHs c : UpdOpParamsHs c : c : s :-> Maybe (GetOpValHs c) : c : s
getAndUpdate :: forall c (s :: [*]).
(GetOpHs c, UpdOpHs c, KnownValue (GetOpValHs c),
 UpdOpKeyHs c ~ GetOpKeyHs c) =>
(UpdOpKeyHs c : UpdOpParamsHs c : c : s)
:-> (Maybe (GetOpValHs c) : c : s)
getAndUpdate = Instr
  (ToTs (GetOpKeyHs c : UpdOpParamsHs c : c : s))
  (ToTs (Maybe (GetOpValHs c) : c : s))
-> (GetOpKeyHs c : UpdOpParamsHs c : c : s)
   :-> (Maybe (GetOpValHs c) : c : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr
  (ToTs (GetOpKeyHs c : UpdOpParamsHs c : c : s))
  (ToTs (Maybe (GetOpValHs c) : c : s))
forall {inp :: [T]} {out :: [T]} (c :: T) (s :: [T]).
(inp ~ (UpdOpKey c : UpdOpParams c : c : s),
 out ~ ('TOption (GetOpVal c) : c : s), GetOp c, UpdOp c,
 SingI (GetOpVal c), UpdOpKey c ~ GetOpKey c) =>
Instr inp out
GET_AND_UPDATE

type ConstraintPairUpdateLorentz (n :: Nat) (val :: Type) (pair :: Type) =
  ( ConstraintUpdateN (ToPeano n) (ToT pair)
  , ToT (PairUpdateHs (ToPeano n) val pair) ~ UpdateN (ToPeano n) (ToT val) (ToT pair)
  , SingIPeano n
  )

type family PairUpdateHs (ix :: Peano) (val :: Type) (pair :: Type) :: Type where
  PairUpdateHs 'Z          val _             = val
  PairUpdateHs ('S 'Z)     val (_, right)    = (val, right)
  PairUpdateHs ('S ('S n)) val (left, right) = (left, PairUpdateHs n val right)

pairUpdate
  :: forall (n :: Nat) (val :: Type) (pair :: Type) (s :: [Type]).
     (ConstraintPairUpdateLorentz n val pair)
  => val : pair : s :-> PairUpdateHs (ToPeano n) val pair : s
pairUpdate :: forall (n :: Nat) val pair (s :: [*]).
ConstraintPairUpdateLorentz n val pair =>
(val : pair : s) :-> (PairUpdateHs (ToPeano n) val pair : s)
pairUpdate = Instr
  (ToTs (val : pair : s))
  (ToTs (PairUpdateHs (ToPeano n) val pair : s))
-> (val : pair : s) :-> (PairUpdateHs (ToPeano n) val pair : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
   (ToTs (val : pair : s))
   (ToTs (PairUpdateHs (ToPeano n) val pair : s))
 -> (val : pair : s) :-> (PairUpdateHs (ToPeano n) val pair : s))
-> Instr
     (ToTs (val : pair : s))
     (ToTs (PairUpdateHs (ToPeano n) val pair : s))
-> (val : pair : s) :-> (PairUpdateHs (ToPeano n) val pair : s)
forall a b. (a -> b) -> a -> b
$ PeanoNatural (ToPeano n)
-> Instr
     (ToT val : ToT pair : ToTs s)
     (UpdateN (ToPeano n) (ToT val) (ToT pair) : ToTs s)
forall {inp :: [T]} {out :: [T]} (ix :: Peano) (val :: T)
       (pair :: T) (s :: [T]).
(inp ~ (val : pair : s), out ~ (UpdateN ix val pair : s),
 ConstraintUpdateN ix pair) =>
PeanoNatural ix -> Instr inp out
UPDATEN (PeanoNatural (ToPeano n)
 -> Instr
      (ToT val : ToT pair : ToTs s)
      (UpdateN (ToPeano n) (ToT val) (ToT pair) : ToTs s))
-> PeanoNatural (ToPeano n)
-> Instr
     (ToT val : ToT pair : ToTs s)
     (UpdateN (ToPeano n) (ToT val) (ToT pair) : ToTs s)
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SingIPeano n => PeanoNatural (ToPeano n)
toPeanoNatural' @n
  where
    _example :: '[ MText, (Integer, Natural) ] :-> '[ (MText, Natural) ]
    _example :: '[MText, (Integer, Natural)] :-> '[(MText, Natural)]
_example = forall (n :: Nat) val pair (s :: [*]).
ConstraintPairUpdateLorentz n val pair =>
(val : pair : s) :-> (PairUpdateHs (ToPeano n) val pair : s)
pairUpdate @1

if_ :: (s :-> s') -> (s :-> s') -> (Bool : s :-> s')
if_ :: forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
if_ = (forall (s' :: [T]).
 Instr (ToTs s) s'
 -> Instr (ToTs s) s' -> Instr (ToTs (Bool : s)) s')
-> (s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
forall (a :: [*]) (b :: [*]) (c :: [*]) (s :: [*]).
(forall (s' :: [T]).
 Instr (ToTs a) s' -> Instr (ToTs b) s' -> Instr (ToTs c) s')
-> (a :-> s) -> (b :-> s) -> c :-> s
iGenericIf forall (s' :: [T]).
Instr (ToTs s) s'
-> Instr (ToTs s) s' -> Instr (ToTs (Bool : s)) s'
forall (s :: [T]) (out :: [T]).
Instr s out -> Instr s out -> Instr ('TBool : s) out
IF

loop :: (s :-> Bool : s) -> (Bool : s :-> s)
loop :: forall (s :: [*]). (s :-> (Bool : s)) -> (Bool : s) :-> s
loop ((s :-> (Bool : s)) -> Instr (ToTs s) (ToTs (Bool : s))
forall (inp :: [*]) (out :: [*]).
(inp :-> out) -> Instr (ToTs inp) (ToTs out)
iAnyCode -> Instr (ToTs s) (ToTs (Bool : s))
b) = Instr (ToTs (Bool : s)) (ToTs s) -> (Bool : s) :-> s
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs s) ('TBool : ToTs s)
-> Instr ('TBool : ToTs s) (ToTs s)
forall (out :: [T]).
Instr out ('TBool : out) -> Instr ('TBool : out) out
LOOP Instr (ToTs s) ('TBool : ToTs s)
Instr (ToTs s) (ToTs (Bool : s))
b)

loopLeft
  :: (a : s :-> Either a b : s) -> (Either a b : s :-> b : s)
loopLeft :: forall a (s :: [*]) b.
((a : s) :-> (Either a b : s)) -> (Either a b : s) :-> (b : s)
loopLeft (((a : s) :-> (Either a b : s))
-> Instr (ToTs (a : s)) (ToTs (Either a b : s))
forall (inp :: [*]) (out :: [*]).
(inp :-> out) -> Instr (ToTs inp) (ToTs out)
iAnyCode -> Instr (ToTs (a : s)) (ToTs (Either a b : s))
b) = Instr (ToTs (Either a b : s)) (ToTs (b : s))
-> (Either a b : s) :-> (b : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToT a : ToTs s) ('TOr (ToT a) (ToT b) : ToTs s)
-> Instr ('TOr (ToT a) (ToT b) : ToTs s) (ToT b : ToTs s)
forall (a :: T) (s :: [T]) (b :: T).
Instr (a : s) ('TOr a b : s) -> Instr ('TOr a b : s) (b : s)
LOOP_LEFT Instr (ToT a : ToTs s) ('TOr (ToT a) (ToT b) : ToTs s)
Instr (ToTs (a : s)) (ToTs (Either a b : s))
b)

lambda
  :: ZipInstrs [i, o]
  => (IsNotInView => i :-> o) -> (s :-> WrappedLambda i o : s)
lambda :: forall (i :: [*]) (o :: [*]) (s :: [*]).
ZipInstrs '[i, o] =>
(IsNotInView => i :-> o) -> s :-> (WrappedLambda i o : s)
lambda IsNotInView => i :-> o
instr = case (i :-> o) -> Fn (ZippedStack i) (ZippedStack o)
forall (inp :: [*]) (out :: [*]).
ZipInstrs '[inp, out] =>
(inp :-> out) -> Fn (ZippedStack inp) (ZippedStack out)
zippingStack ((i :-> o) -> Fn (ZippedStack i) (ZippedStack o))
-> (i :-> o) -> Fn (ZippedStack i) (ZippedStack o)
forall a b. (a -> b) -> a -> b
$ (IsNotInView => i :-> o) -> i :-> o
forall r. (IsNotInView => r) -> r
giveNotInView IsNotInView => i :-> o
instr of
  I Instr (ToTs '[ZippedStack i]) (ToTs '[ZippedStack o])
l -> Instr (ToTs s) (ToTs (WrappedLambda i o : s))
-> s :-> (WrappedLambda i o : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I ((IsNotInView =>
 RemFail Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)])
-> Instr
     (ToTs s)
     ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)) : ToTs s)
forall (s :: [T]) (r :: [T]) (i :: T) (o :: T).
(SingI i, SingI o, r ~ ('TLambda i o : s)) =>
(IsNotInView => RemFail Instr '[i] '[o]) -> Instr s r
LAMBDA ((IsNotInView =>
  RemFail Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)])
 -> Instr
      (ToTs s)
      ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)) : ToTs s))
-> (IsNotInView =>
    RemFail Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)])
-> Instr
     (ToTs s)
     ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)) : ToTs s)
forall a b. (a -> b) -> a -> b
$ Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)]
-> RemFail Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)]
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)]
Instr (ToTs '[ZippedStack i]) (ToTs '[ZippedStack o])
l)
  FI forall (out' :: [T]). Instr (ToTs '[ZippedStack i]) out'
l -> Instr (ToTs s) (ToTs (WrappedLambda i o : s))
-> s :-> (WrappedLambda i o : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I ((IsNotInView =>
 RemFail Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)])
-> Instr
     (ToTs s)
     ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)) : ToTs s)
forall (s :: [T]) (r :: [T]) (i :: T) (o :: T).
(SingI i, SingI o, r ~ ('TLambda i o : s)) =>
(IsNotInView => RemFail Instr '[i] '[o]) -> Instr s r
LAMBDA ((IsNotInView =>
  RemFail Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)])
 -> Instr
      (ToTs s)
      ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)) : ToTs s))
-> (IsNotInView =>
    RemFail Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)])
-> Instr
     (ToTs s)
     ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)) : ToTs s)
forall a b. (a -> b) -> a -> b
$ (forall (o' :: [T]). Instr '[ToT (ZippedStack i)] o')
-> RemFail Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)]
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
(forall (o' :: k). instr i o') -> RemFail instr i o
RfAlwaysFails forall (o' :: [T]). Instr '[ToT (ZippedStack i)] o'
forall (out' :: [T]). Instr (ToTs '[ZippedStack i]) out'
l)

lambdaRec
  :: forall i o s. (ZipInstrs [i, o], KnownList i)
  => (IsNotInView => (i ++ '[WrappedLambda i o]) :-> o) -> (s :-> WrappedLambda i o : s)
lambdaRec :: forall (i :: [*]) (o :: [*]) (s :: [*]).
(ZipInstrs '[i, o], KnownList i) =>
(IsNotInView => (i ++ '[WrappedLambda i o]) :-> o)
-> s :-> (WrappedLambda i o : s)
lambdaRec IsNotInView => (i ++ '[WrappedLambda i o]) :-> o
instr = case '[ZippedStack i, WrappedLambda i o] :-> '[ZippedStack o]
code of
  I Instr
  (ToTs '[ZippedStack i, WrappedLambda i o]) (ToTs '[ZippedStack o])
l -> Instr (ToTs s) (ToTs (WrappedLambda i o : s))
-> s :-> (WrappedLambda i o : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs s) (ToTs (WrappedLambda i o : s))
 -> s :-> (WrappedLambda i o : s))
-> Instr (ToTs s) (ToTs (WrappedLambda i o : s))
-> s :-> (WrappedLambda i o : s)
forall a b. (a -> b) -> a -> b
$ (IsNotInView =>
 RemFail
   Instr
   '[ToT (ZippedStack i),
     'TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o))]
   '[ToT (ZippedStack o)])
-> Instr
     (ToTs s)
     ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)) : ToTs s)
forall (s :: [T]) (r :: [T]) (i :: T) (o :: T).
(SingI i, SingI o, r ~ ('TLambda i o : s)) =>
(IsNotInView => RemFail Instr '[i, 'TLambda i o] '[o]) -> Instr s r
LAMBDA_REC ((IsNotInView =>
  RemFail
    Instr
    '[ToT (ZippedStack i),
      'TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o))]
    '[ToT (ZippedStack o)])
 -> Instr
      (ToTs s)
      ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)) : ToTs s))
-> (IsNotInView =>
    RemFail
      Instr
      '[ToT (ZippedStack i),
        'TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o))]
      '[ToT (ZippedStack o)])
-> Instr
     (ToTs s)
     ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)) : ToTs s)
forall a b. (a -> b) -> a -> b
$ Instr
  '[ToT (ZippedStack i),
    'TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o))]
  '[ToT (ZippedStack o)]
-> RemFail
     Instr
     '[ToT (ZippedStack i),
       'TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o))]
     '[ToT (ZippedStack o)]
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal Instr
  '[ToT (ZippedStack i),
    'TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o))]
  '[ToT (ZippedStack o)]
Instr
  (ToTs '[ZippedStack i, WrappedLambda i o]) (ToTs '[ZippedStack o])
l
  FI forall (out' :: [T]).
Instr (ToTs '[ZippedStack i, WrappedLambda i o]) out'
l -> Instr (ToTs s) (ToTs (WrappedLambda i o : s))
-> s :-> (WrappedLambda i o : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs s) (ToTs (WrappedLambda i o : s))
 -> s :-> (WrappedLambda i o : s))
-> Instr (ToTs s) (ToTs (WrappedLambda i o : s))
-> s :-> (WrappedLambda i o : s)
forall a b. (a -> b) -> a -> b
$ (IsNotInView =>
 RemFail
   Instr
   '[ToT (ZippedStack i),
     'TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o))]
   '[ToT (ZippedStack o)])
-> Instr
     (ToTs s)
     ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)) : ToTs s)
forall (s :: [T]) (r :: [T]) (i :: T) (o :: T).
(SingI i, SingI o, r ~ ('TLambda i o : s)) =>
(IsNotInView => RemFail Instr '[i, 'TLambda i o] '[o]) -> Instr s r
LAMBDA_REC ((IsNotInView =>
  RemFail
    Instr
    '[ToT (ZippedStack i),
      'TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o))]
    '[ToT (ZippedStack o)])
 -> Instr
      (ToTs s)
      ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)) : ToTs s))
-> (IsNotInView =>
    RemFail
      Instr
      '[ToT (ZippedStack i),
        'TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o))]
      '[ToT (ZippedStack o)])
-> Instr
     (ToTs s)
     ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)) : ToTs s)
forall a b. (a -> b) -> a -> b
$ (forall (o' :: [T]).
 Instr
   '[ToT (ZippedStack i),
     'TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o))]
   o')
-> RemFail
     Instr
     '[ToT (ZippedStack i),
       'TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o))]
     '[ToT (ZippedStack o)]
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
(forall (o' :: k). instr i o') -> RemFail instr i o
RfAlwaysFails forall (o' :: [T]).
Instr
  '[ToT (ZippedStack i),
    'TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o))]
  o'
forall (out' :: [T]).
Instr (ToTs '[ZippedStack i, WrappedLambda i o]) out'
l
  where
    code :: '[ZippedStack i, WrappedLambda i o] :-> '[ZippedStack o]
code =
      forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
framed @'[WrappedLambda i o] (forall (s :: [*]). ZipInstr s => '[ZippedStack s] :-> s
unzipInstr @i)
      ## giveNotInView instr
      ## zipInstr

exec :: a : Lambda a b : s :-> b : s
exec :: forall a b (s :: [*]). (a : Lambda a b : s) :-> (b : s)
exec = Instr (ToTs (a : Lambda a b : s)) (ToTs (b : s))
-> (a : Lambda a b : s) :-> (b : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (a : Lambda a b : s)) (ToTs (b : s))
forall {inp :: [T]} {out :: [T]} (t1 :: T) (t2 :: T) (s :: [T]).
(inp ~ (t1 : 'TLambda t1 t2 : s), out ~ (t2 : s)) =>
Instr inp out
EXEC

-- | Similar to 'exec' but works for lambdas with arbitrary size of input
-- and output.
--
-- Note that this instruction has its arguments flipped, lambda goes first.
-- This seems to be the only reasonable way to achieve good inference.
execute
  :: forall i o s.
      (Each [KnownList, ZipInstr] [i, o])
  => (WrappedLambda i o : (i ++ s)) :-> (o ++ s)
execute :: forall (i :: [*]) (o :: [*]) (s :: [*]).
Each '[KnownList, ZipInstr] '[i, o] =>
(WrappedLambda i o : (i ++ s)) :-> (o ++ s)
execute = forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
framed @s (((WrappedLambda i o : i) :-> o)
 -> ((WrappedLambda i o : i) ++ s) :-> (o ++ s))
-> ((WrappedLambda i o : i) :-> o)
-> ((WrappedLambda i o : i) ++ s) :-> (o ++ s)
forall a b. (a -> b) -> a -> b
$
  (i :-> '[ZippedStack i])
-> (WrappedLambda i o : i) :-> '[WrappedLambda i o, ZippedStack i]
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (forall (s :: [*]). ZipInstr s => s :-> '[ZippedStack s]
zipInstr @i) ((WrappedLambda i o : i) :-> '[WrappedLambda i o, ZippedStack i])
-> ('[WrappedLambda i o, ZippedStack i]
    :-> '[ZippedStack i, WrappedLambda i o])
-> (WrappedLambda i o : i) :-> '[ZippedStack i, WrappedLambda i o]
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# '[WrappedLambda i o, ZippedStack i]
:-> '[ZippedStack i, WrappedLambda i o]
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((WrappedLambda i o : i) :-> '[ZippedStack i, WrappedLambda i o])
-> ('[ZippedStack i, WrappedLambda i o] :-> '[ZippedStack o])
-> (WrappedLambda i o : i) :-> '[ZippedStack o]
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Instr
  (ToTs '[ZippedStack i, WrappedLambda i o]) (ToTs '[ZippedStack o])
-> '[ZippedStack i, WrappedLambda i o] :-> '[ZippedStack o]
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr
  (ToTs '[ZippedStack i, WrappedLambda i o]) (ToTs '[ZippedStack o])
forall {inp :: [T]} {out :: [T]} (t1 :: T) (t2 :: T) (s :: [T]).
(inp ~ (t1 : 'TLambda t1 t2 : s), out ~ (t2 : s)) =>
Instr inp out
EXEC ((WrappedLambda i o : i) :-> '[ZippedStack o])
-> ('[ZippedStack o] :-> o) -> (WrappedLambda i o : i) :-> o
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall (s :: [*]). ZipInstr s => '[ZippedStack s] :-> s
unzipInstr @o
  where
    _example :: (WrappedLambda [Integer, Natural] [(), ()]) : Integer : Natural : s :-> () : () : s
    _example :: (WrappedLambda '[Integer, Natural] '[(), ()]
   : Integer : Natural : s)
:-> (() : () : s)
_example = (WrappedLambda '[Integer, Natural] '[(), ()]
   : Integer : Natural : s)
:-> (() : () : s)
forall (i :: [*]) (o :: [*]) (s :: [*]).
Each '[KnownList, ZipInstr] '[i, o] =>
(WrappedLambda i o : (i ++ s)) :-> (o ++ s)
execute

apply
  :: forall a b c s. (NiceConstant a, KnownValue b)
  => a : Lambda (a, b) c : s :-> Lambda b c : s
apply :: forall a b c (s :: [*]).
(NiceConstant a, KnownValue b) =>
(a : Lambda (a, b) c : s) :-> (Lambda b c : s)
apply = Instr (ToTs (a : Lambda (a, b) c : s)) (ToTs (Lambda b c : s))
-> (a : Lambda (a, b) c : s) :-> (Lambda b c : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs (a : Lambda (a, b) c : s)) (ToTs (Lambda b c : s))
 -> (a : Lambda (a, b) c : s) :-> (Lambda b c : s))
-> Instr (ToTs (a : Lambda (a, b) c : s)) (ToTs (Lambda b c : s))
-> (a : Lambda (a, b) c : s) :-> (Lambda b c : s)
forall a b. (a -> b) -> a -> b
$ Instr (ToTs (a : Lambda (a, b) c : s)) (ToTs (Lambda b c : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (c :: T)
       (s :: [T]).
(inp ~ (a : 'TLambda ('TPair a b) c : s), out ~ ('TLambda b c : s),
 ConstantScope a, SingI b) =>
Instr inp out
APPLY

-- | Version of 'apply' that works for lambdas with arbitrary length
-- input and output.
applicate
  :: forall a b c inp2nd inpTail s.
     (NiceConstant a, ZipInstr b, b ~ (inp2nd : inpTail))
  => a : WrappedLambda (a : b) c : s :-> WrappedLambda b c : s
applicate :: forall a (b :: [*]) (c :: [*]) inp2nd (inpTail :: [*]) (s :: [*]).
(NiceConstant a, ZipInstr b, b ~ (inp2nd : inpTail)) =>
(a : WrappedLambda (a : b) c : s) :-> (WrappedLambda b c : s)
applicate = Instr
  (ToTs (a : WrappedLambda (a : b) c : s))
  (ToTs (WrappedLambda b c : s))
-> (a : WrappedLambda (a : b) c : s) :-> (WrappedLambda b c : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr
  (ToTs (a : WrappedLambda (a : b) c : s))
  (ToTs (WrappedLambda b c : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (c :: T)
       (s :: [T]).
(inp ~ (a : 'TLambda ('TPair a b) c : s), out ~ ('TLambda b c : s),
 ConstantScope a, SingI b) =>
Instr inp out
APPLY

dip :: forall a s s'. HasCallStack => (s :-> s') -> (a : s :-> a : s')
dip :: forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip ((s :-> s') -> Instr (ToTs s) (ToTs s')
forall (inp :: [*]) (out :: [*]).
HasCallStack =>
(inp :-> out) -> Instr (ToTs inp) (ToTs out)
iNonFailingCode -> Instr (ToTs s) (ToTs s')
a) = Instr (ToTs (a : s)) (ToTs (a : s')) -> (a : s) :-> (a : s')
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs s) (ToTs s')
-> Instr (ToT a : ToTs s) (ToT a : ToTs s')
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr (ToTs s) (ToTs s')
a)

-- Helper constraint we need for 'dipN'.
-- The first constraint here is sufficient to make 'dipN' compile.
-- However, it is not enough for good type inference. If we use only the first
-- constraint, '_example' below will not compile because GHC will not be able
-- to deduce type of the input stack for 'unit'.
-- It can only deduce that 'ToTs s0' is empty (where 's0' is input stack), but
-- 'ToTs' is not injective, hence 's0' is ambiguous.
-- So we need both and we merge them into one to avoid a warning about
-- a redundant constraint.
type ConstraintDIPNLorentz (n :: Peano) (inp :: [Type]) (out :: [Type])
  (s :: [Type]) (s' :: [Type]) =
  ( ConstraintDIPN n (ToTs inp) (ToTs out) (ToTs s) (ToTs s')
  , ConstraintDIPN' Type n inp out s s'
  , SingI n
  )

-- | Version of `dipN` which uses Peano number.
-- It is intended for internal usage in Lorentz.
dipNPeano ::
  forall (n :: Peano) (inp :: [Type]) (out :: [Type]) (s :: [Type]) (s' :: [Type]).
  ( ConstraintDIPNLorentz n inp out s s'
  ) => s :-> s' -> inp :-> out
dipNPeano :: forall (n :: Peano) (inp :: [*]) (out :: [*]) (s :: [*])
       (s' :: [*]).
ConstraintDIPNLorentz n inp out s s' =>
(s :-> s') -> inp :-> out
dipNPeano ((s :-> s') -> Instr (ToTs s) (ToTs s')
forall (inp :: [*]) (out :: [*]).
HasCallStack =>
(inp :-> out) -> Instr (ToTs inp) (ToTs out)
iNonFailingCode -> Instr (ToTs s) (ToTs s')
a) = Instr (ToTs inp) (ToTs out) -> inp :-> out
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (PeanoNatural n
-> Instr (Drop n (ToTs inp)) (Drop n (ToTs out))
-> Instr (ToTs inp) (ToTs out)
forall (n :: Peano) (inp :: [T]) (out :: [T]) (s :: [T])
       (s' :: [T]).
ConstraintDIPN n inp out s s' =>
PeanoNatural n -> Instr s s' -> Instr inp out
DIPN (forall (n :: Peano). SingI n => PeanoNatural n
toPeanoNatural @n) Instr (ToTs s) (ToTs s')
Instr (Drop n (ToTs inp)) (Drop n (ToTs out))
a)

dipN ::
  forall (n :: Nat) (inp :: [Type]) (out :: [Type]) (s :: [Type]) (s' :: [Type]).
  ( ConstraintDIPNLorentz (ToPeano n) inp out s s'
  ) => s :-> s' -> inp :-> out
dipN :: forall (n :: Nat) (inp :: [*]) (out :: [*]) (s :: [*]) (s' :: [*]).
ConstraintDIPNLorentz (ToPeano n) inp out s s' =>
(s :-> s') -> inp :-> out
dipN = forall (n :: Peano) (inp :: [*]) (out :: [*]) (s :: [*])
       (s' :: [*]).
ConstraintDIPNLorentz n inp out s s' =>
(s :-> s') -> inp :-> out
dipNPeano @(ToPeano n)
  where
    _example :: '[ Integer, Integer, Integer ] :-> '[ Integer, Integer, Integer, () ]
    _example :: '[Integer, Integer, Integer] :-> '[Integer, Integer, Integer, ()]
_example = forall (n :: Nat) (inp :: [*]) (out :: [*]) (s :: [*]) (s' :: [*]).
ConstraintDIPNLorentz (ToPeano n) inp out s s' =>
(s :-> s') -> inp :-> out
dipN @3 '[] :-> '[()]
forall (s :: [*]). s :-> (() : s)
unit

-- Since 008 it's prohibited to fail with non-packable values and with the
-- 'Contract t' type values, which is equivalent to our @NiceConstant@ constraint.
-- See https://gitlab.com/tezos/tezos/-/issues/1093#note_496066354 for more information.
failWith :: forall a s t. NiceConstant a => a : s :-> t
failWith :: forall a (s :: [*]) (t :: [*]). NiceConstant a => (a : s) :-> t
failWith = (forall (out' :: [T]). Instr (ToTs (a : s)) out') -> (a : s) :-> t
forall (inp :: [*]) (out :: [*]).
(forall (out' :: [T]). Instr (ToTs inp) out') -> inp :-> out
FI forall (out' :: [T]). Instr (ToTs (a : s)) out'
forall (a :: T) (s :: [T]) (out :: [T]).
(SingI a, ConstantScope a) =>
Instr (a : s) out
FAILWITH

cast :: KnownValue a => (a : s :-> a : s)
cast :: forall a (s :: [*]). KnownValue a => (a : s) :-> (a : s)
cast = Instr (ToTs (a : s)) (ToTs (a : s)) -> (a : s) :-> (a : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (a : s)) (ToTs (a : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ (a : s), SingI a) =>
Instr inp out
CAST

pack
  :: forall a s. (NicePackedValue a)
  => a : s :-> Packed a : s
pack :: forall a (s :: [*]).
NicePackedValue a =>
(a : s) :-> (Packed a : s)
pack = Instr (ToTs (a : s)) (ToTs (Packed a : s))
-> (a : s) :-> (Packed a : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs (a : s)) (ToTs (Packed a : s))
 -> (a : s) :-> (Packed a : s))
-> Instr (ToTs (a : s)) (ToTs (Packed a : s))
-> (a : s) :-> (Packed a : s)
forall a b. (a -> b) -> a -> b
$ Instr (ToTs (a : s)) (ToTs (Packed a : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ ('TBytes : s), PackedValScope a) =>
Instr inp out
PACK

unpack
  :: forall a s. (NiceUnpackedValue a)
  => Packed a : s :-> Maybe a : s
unpack :: forall a (s :: [*]).
NiceUnpackedValue a =>
(Packed a : s) :-> (Maybe a : s)
unpack = Instr (ToTs (Packed a : s)) (ToTs (Maybe a : s))
-> (Packed a : s) :-> (Maybe a : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs (Packed a : s)) (ToTs (Maybe a : s))
 -> (Packed a : s) :-> (Maybe a : s))
-> Instr (ToTs (Packed a : s)) (ToTs (Maybe a : s))
-> (Packed a : s) :-> (Maybe a : s)
forall a b. (a -> b) -> a -> b
$ Instr (ToTs (Packed a : s)) (ToTs (Maybe a : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ ('TBytes : s), out ~ ('TOption a : s), UnpackedValScope a,
 SingI a) =>
Instr inp out
UNPACK

packRaw
  :: forall a s. (NicePackedValue a)
  => a : s :-> ByteString : s
packRaw :: forall a (s :: [*]).
NicePackedValue a =>
(a : s) :-> (ByteString : s)
packRaw = Instr (ToTs (a : s)) (ToTs (ByteString : s))
-> (a : s) :-> (ByteString : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs (a : s)) (ToTs (ByteString : s))
 -> (a : s) :-> (ByteString : s))
-> Instr (ToTs (a : s)) (ToTs (ByteString : s))
-> (a : s) :-> (ByteString : s)
forall a b. (a -> b) -> a -> b
$ Instr (ToTs (a : s)) (ToTs (ByteString : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ ('TBytes : s), PackedValScope a) =>
Instr inp out
PACK

unpackRaw
  :: forall a s. (NiceUnpackedValue a)
  => ByteString : s :-> Maybe a : s
unpackRaw :: forall a (s :: [*]).
NiceUnpackedValue a =>
(ByteString : s) :-> (Maybe a : s)
unpackRaw = Instr (ToTs (ByteString : s)) (ToTs (Maybe a : s))
-> (ByteString : s) :-> (Maybe a : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs (ByteString : s)) (ToTs (Maybe a : s))
 -> (ByteString : s) :-> (Maybe a : s))
-> Instr (ToTs (ByteString : s)) (ToTs (Maybe a : s))
-> (ByteString : s) :-> (Maybe a : s)
forall a b. (a -> b) -> a -> b
$ Instr (ToTs (ByteString : s)) (ToTs (Maybe a : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ ('TBytes : s), out ~ ('TOption a : s), UnpackedValScope a,
 SingI a) =>
Instr inp out
UNPACK

concat :: ConcatOpHs c => c : c : s :-> c : s
concat :: forall c (s :: [*]). ConcatOpHs c => (c : c : s) :-> (c : s)
concat = Instr (ToTs (c : c : s)) (ToTs (c : s)) -> (c : c : s) :-> (c : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (c : c : s)) (ToTs (c : s))
forall {inp :: [T]} {out :: [T]} (c :: T) (s :: [T]).
(inp ~ (c : c : s), out ~ (c : s), ConcatOp c) =>
Instr inp out
CONCAT

concat' :: ConcatOpHs c => List c : s :-> c : s
concat' :: forall c (s :: [*]). ConcatOpHs c => (List c : s) :-> (c : s)
concat' = Instr (ToTs (List c : s)) (ToTs (c : s))
-> (List c : s) :-> (c : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (List c : s)) (ToTs (c : s))
forall {inp :: [T]} {out :: [T]} (c :: T) (s :: [T]).
(inp ~ ('TList c : s), out ~ (c : s), ConcatOp c) =>
Instr inp out
CONCAT'

slice
  :: (SliceOpHs c, KnownValue c)
  => Natural : Natural : c : s :-> Maybe c : s
slice :: forall c (s :: [*]).
(SliceOpHs c, KnownValue c) =>
(Natural : Natural : c : s) :-> (Maybe c : s)
slice = Instr (ToTs (Natural : Natural : c : s)) (ToTs (Maybe c : s))
-> (Natural : Natural : c : s) :-> (Maybe c : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (Natural : Natural : c : s)) (ToTs (Maybe c : s))
forall {inp :: [T]} {out :: [T]} (c :: T) (s :: [T]).
(inp ~ ('TNat : 'TNat : c : s), out ~ ('TOption c : s), SliceOp c,
 SingI c) =>
Instr inp out
SLICE

isNat :: Integer : s :-> Maybe Natural : s
isNat :: forall (s :: [*]). (Integer : s) :-> (Maybe Natural : s)
isNat = Instr (ToTs (Integer : s)) (ToTs (Maybe Natural : s))
-> (Integer : s) :-> (Maybe Natural : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (Integer : s)) (ToTs (Maybe Natural : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ ('TInt : s), out ~ ('TOption 'TNat : s)) =>
Instr inp out
ISNAT

add
  :: ArithOpHs Add n m r
  => n : m : s :-> r : s
add :: forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add = forall aop n m r (s :: [*]).
ArithOpHs aop n m r =>
(n : m : s) :-> (r : s)
evalArithOpHs @Add

sub
  :: ArithOpHs Sub n m r
  => n : m : s :-> r : s
sub :: forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub = forall aop n m r (s :: [*]).
ArithOpHs aop n m r =>
(n : m : s) :-> (r : s)
evalArithOpHs @Sub

rsub
  :: ArithOpHs Sub n m r
  => m : n : s :-> r : s
rsub :: forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(m : n : s) :-> (r : s)
rsub = (m : n : s) :-> (n : m : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((m : n : s) :-> (n : m : s))
-> ((n : m : s) :-> (r : s)) -> (m : n : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (n : m : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub

subMutez :: Mutez : Mutez : s :-> Maybe Mutez : s
subMutez :: forall (s :: [*]). (Mutez : Mutez : s) :-> (Maybe Mutez : s)
subMutez = Instr (ToTs (Mutez : Mutez : s)) (ToTs (Maybe Mutez : s))
-> (Mutez : Mutez : s) :-> (Maybe Mutez : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (Mutez : Mutez : s)) (ToTs (Maybe Mutez : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ ('TMutez : 'TMutez : s), out ~ ('TOption 'TMutez : s)) =>
Instr inp out
SUB_MUTEZ

rsubMutez :: Mutez : Mutez : s :-> Maybe Mutez : s
rsubMutez :: forall (s :: [*]). (Mutez : Mutez : s) :-> (Maybe Mutez : s)
rsubMutez = (Mutez : Mutez : s) :-> (Mutez : Mutez : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((Mutez : Mutez : s) :-> (Mutez : Mutez : s))
-> ((Mutez : Mutez : s) :-> (Maybe Mutez : s))
-> (Mutez : Mutez : s) :-> (Maybe Mutez : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Mutez : Mutez : s) :-> (Maybe Mutez : s)
forall (s :: [*]). (Mutez : Mutez : s) :-> (Maybe Mutez : s)
subMutez

mul
  :: ArithOpHs Mul n m r
  => n : m : s :-> r : s
mul :: forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul = forall aop n m r (s :: [*]).
ArithOpHs aop n m r =>
(n : m : s) :-> (r : s)
evalArithOpHs @Mul

ediv :: ArithOpHs EDiv n m r
     => n : m : s
     :-> r : s
ediv :: forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv = forall aop n m r (s :: [*]).
ArithOpHs aop n m r =>
(n : m : s) :-> (r : s)
evalArithOpHs @EDiv

abs :: UnaryArithOpHs Abs n => n : s :-> UnaryArithResHs Abs n : s
abs :: forall n (s :: [*]).
UnaryArithOpHs Abs n =>
(n : s) :-> (UnaryArithResHs Abs n : s)
abs = forall aop n (s :: [*]).
UnaryArithOpHs aop n =>
(n : s) :-> (UnaryArithResHs aop n : s)
evalUnaryArithOpHs @Abs

neg :: UnaryArithOpHs Neg n => n : s :-> UnaryArithResHs Neg n : s
neg :: forall n (s :: [*]).
UnaryArithOpHs Neg n =>
(n : s) :-> (UnaryArithResHs Neg n : s)
neg = forall aop n (s :: [*]).
UnaryArithOpHs aop n =>
(n : s) :-> (UnaryArithResHs aop n : s)
evalUnaryArithOpHs @Neg

lsl
  :: ArithOpHs Lsl n m r
  => n : m : s :-> r : s
lsl :: forall n m r (s :: [*]).
ArithOpHs Lsl n m r =>
(n : m : s) :-> (r : s)
lsl = forall aop n m r (s :: [*]).
ArithOpHs aop n m r =>
(n : m : s) :-> (r : s)
evalArithOpHs @Lsl

lsr
  :: ArithOpHs Lsr n m r
  => n : m : s :-> r : s
lsr :: forall n m r (s :: [*]).
ArithOpHs Lsr n m r =>
(n : m : s) :-> (r : s)
lsr = forall aop n m r (s :: [*]).
ArithOpHs aop n m r =>
(n : m : s) :-> (r : s)
evalArithOpHs @Lsr

or
  :: ArithOpHs Or n m r
  => n : m : s :-> r : s
or :: forall n m r (s :: [*]).
ArithOpHs Or n m r =>
(n : m : s) :-> (r : s)
or = forall aop n m r (s :: [*]).
ArithOpHs aop n m r =>
(n : m : s) :-> (r : s)
evalArithOpHs @Or

and
  :: ArithOpHs And n m r
  => n : m : s :-> r : s
and :: forall n m r (s :: [*]).
ArithOpHs And n m r =>
(n : m : s) :-> (r : s)
and = forall aop n m r (s :: [*]).
ArithOpHs aop n m r =>
(n : m : s) :-> (r : s)
evalArithOpHs @And

xor
  :: (ArithOpHs Xor n m r)
  => n : m : s :-> r : s
xor :: forall n m r (s :: [*]).
ArithOpHs Xor n m r =>
(n : m : s) :-> (r : s)
xor = forall aop n m r (s :: [*]).
ArithOpHs aop n m r =>
(n : m : s) :-> (r : s)
evalArithOpHs @Xor

not :: UnaryArithOpHs Not n => n : s :-> UnaryArithResHs Not n : s
not :: forall n (s :: [*]).
UnaryArithOpHs Not n =>
(n : s) :-> (UnaryArithResHs Not n : s)
not = forall aop n (s :: [*]).
UnaryArithOpHs aop n =>
(n : s) :-> (UnaryArithResHs aop n : s)
evalUnaryArithOpHs @Not

compare :: NiceComparable n => n : n : s :-> Integer : s
compare :: forall n (s :: [*]).
NiceComparable n =>
(n : n : s) :-> (Integer : s)
compare = Instr (ToTs (n : n : s)) (ToTs (Integer : s))
-> (n : n : s) :-> (Integer : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (n : n : s)) (ToTs (Integer : s))
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : n : s), out ~ ('TInt : s), Comparable n, SingI n) =>
Instr inp out
COMPARE

eq0 :: UnaryArithOpHs Eq' n => n : s :-> UnaryArithResHs Eq' n : s
eq0 :: forall n (s :: [*]).
UnaryArithOpHs Eq' n =>
(n : s) :-> (UnaryArithResHs Eq' n : s)
eq0 = forall aop n (s :: [*]).
UnaryArithOpHs aop n =>
(n : s) :-> (UnaryArithResHs aop n : s)
evalUnaryArithOpHs @Eq'

neq0 :: UnaryArithOpHs Neq n => n : s :-> UnaryArithResHs Neq n : s
neq0 :: forall n (s :: [*]).
UnaryArithOpHs Neq n =>
(n : s) :-> (UnaryArithResHs Neq n : s)
neq0 = forall aop n (s :: [*]).
UnaryArithOpHs aop n =>
(n : s) :-> (UnaryArithResHs aop n : s)
evalUnaryArithOpHs @Neq

lt0 :: UnaryArithOpHs Lt n => n : s :-> UnaryArithResHs Lt n : s
lt0 :: forall n (s :: [*]).
UnaryArithOpHs Lt n =>
(n : s) :-> (UnaryArithResHs Lt n : s)
lt0 = forall aop n (s :: [*]).
UnaryArithOpHs aop n =>
(n : s) :-> (UnaryArithResHs aop n : s)
evalUnaryArithOpHs @Lt

gt0 :: UnaryArithOpHs Gt n => n : s :-> UnaryArithResHs Gt n : s
gt0 :: forall n (s :: [*]).
UnaryArithOpHs Gt n =>
(n : s) :-> (UnaryArithResHs Gt n : s)
gt0 = forall aop n (s :: [*]).
UnaryArithOpHs aop n =>
(n : s) :-> (UnaryArithResHs aop n : s)
evalUnaryArithOpHs @Gt

le0 :: UnaryArithOpHs Le n => n : s :-> UnaryArithResHs Le n : s
le0 :: forall n (s :: [*]).
UnaryArithOpHs Le n =>
(n : s) :-> (UnaryArithResHs Le n : s)
le0 = forall aop n (s :: [*]).
UnaryArithOpHs aop n =>
(n : s) :-> (UnaryArithResHs aop n : s)
evalUnaryArithOpHs @Le

ge0 :: UnaryArithOpHs Ge n => n : s :-> UnaryArithResHs Ge n : s
ge0 :: forall n (s :: [*]).
UnaryArithOpHs Ge n =>
(n : s) :-> (UnaryArithResHs Ge n : s)
ge0 = forall aop n (s :: [*]).
UnaryArithOpHs aop n =>
(n : s) :-> (UnaryArithResHs aop n : s)
evalUnaryArithOpHs @Ge

int :: (ToIntegerArithOpHs i) => i : s :-> Integer : s
int :: forall i (s :: [*]).
ToIntegerArithOpHs i =>
(i : s) :-> (Integer : s)
int = (i : s) :-> (Integer : s)
forall n (s :: [*]).
ToIntegerArithOpHs n =>
(n : s) :-> (Integer : s)
evalToIntOpHs

-- | Manual variation of @VIEW@ instruction.
-- It is pretty much like Michelson's @VIEW@, you must make sure that the compiler can
-- infer the argument and return types of the view.
--
-- In most cases prefer 'Lorentz.Macro.view' instead.
view'
  :: forall name ret arg s.
    (HasCallStack, KnownSymbol name, KnownValue arg, NiceViewable ret)
  => arg : Address : s :-> Maybe ret : s
view' :: forall (name :: Symbol) ret arg (s :: [*]).
(HasCallStack, KnownSymbol name, KnownValue arg,
 NiceViewable ret) =>
(arg : Address : s) :-> (Maybe ret : s)
view' = Instr (ToTs (arg : Address : s)) (ToTs (Maybe ret : s))
-> (arg : Address : s) :-> (Maybe ret : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs (arg : Address : s)) (ToTs (Maybe ret : s))
 -> (arg : Address : s) :-> (Maybe ret : s))
-> Instr (ToTs (arg : Address : s)) (ToTs (Maybe ret : s))
-> (arg : Address : s) :-> (Maybe ret : s)
forall a b. (a -> b) -> a -> b
$ ViewName
-> Instr
     (ToT arg : 'TAddress : ToTs s) ('TOption (ToT ret) : ToTs s)
forall {inp :: [T]} {out :: [T]} (arg :: T) (ret :: T) (s :: [T]).
(inp ~ (arg : 'TAddress : s), out ~ ('TOption ret : s), SingI arg,
 ViewableScope ret) =>
ViewName -> Instr inp out
VIEW (forall (name :: Symbol).
(KnownSymbol name, HasCallStack) =>
ViewName
demoteViewName @name)

-- | Get a reference to the current contract.
--
-- Note that, similar to 'CONTRACT' instruction, in Michelson 'SELF' instruction
-- can accept an entrypoint as field annotation, and without annotation specified
-- it creates a @contract@ value which calls the default entrypoint.
--
-- This particular function carries the behaviour of @SELF@ before introduction
-- of lightweight entrypoints feature.
-- Thus the contract must __not__ have explicit "default" entrypoint for this to
-- work.
--
-- If you are going to call a specific entrypoint of the contract, see 'selfCalling'.
self
  :: forall p s.
      (NiceParameterFull p, ForbidExplicitDefaultEntrypoint p, IsNotInView)
  => s :-> ContractRef p : s
self :: forall p (s :: [*]).
(NiceParameterFull p, ForbidExplicitDefaultEntrypoint p,
 IsNotInView) =>
s :-> (ContractRef p : s)
self = Instr (ToTs s) (ToTs (ContractRef p : s))
-> s :-> (ContractRef p : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (SomeEntrypointCallT (ToT p)
-> Instr (ToTs s) ('TContract (ToT p) : ToTs s)
forall {inp :: [T]} {out :: [T]} (arg :: T) (s :: [T]).
(inp ~ s, out ~ ('TContract arg : s), ParameterScope arg,
 IsNotInView) =>
SomeEntrypointCallT arg -> Instr inp out
SELF (SomeEntrypointCallT (ToT p)
 -> Instr (ToTs s) ('TContract (ToT p) : ToTs s))
-> SomeEntrypointCallT (ToT p)
-> Instr (ToTs s) ('TContract (ToT p) : ToTs s)
forall a b. (a -> b) -> a -> b
$ forall cp.
(NiceParameter cp, ForbidExplicitDefaultEntrypoint cp) =>
SomeEntrypointCall cp
sepcCallRootChecked @p)

-- | Make a reference to the current contract, maybe a specific entrypoint.
--
-- Note that, since information about parameter of the current contract is not
-- carried around, in this function you need to specify parameter type @p@
-- explicitly.
selfCalling
  :: forall p mname s.
     (NiceParameterFull p, IsNotInView)
  => EntrypointRef mname
  -> s :-> ContractRef (GetEntrypointArgCustom p mname) : s
selfCalling :: forall p (mname :: Maybe Symbol) (s :: [*]).
(NiceParameterFull p, IsNotInView) =>
EntrypointRef mname
-> s :-> (ContractRef (GetEntrypointArgCustom p mname) : s)
selfCalling EntrypointRef mname
epRef = Instr
  (ToTs s) (ToTs (ContractRef (GetEntrypointArgCustom p mname) : s))
-> s :-> (ContractRef (GetEntrypointArgCustom p mname) : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
   (ToTs s) (ToTs (ContractRef (GetEntrypointArgCustom p mname) : s))
 -> s :-> (ContractRef (GetEntrypointArgCustom p mname) : s))
-> Instr
     (ToTs s) (ToTs (ContractRef (GetEntrypointArgCustom p mname) : s))
-> s :-> (ContractRef (GetEntrypointArgCustom p mname) : s)
forall a b. (a -> b) -> a -> b
$
  case forall cp (mname :: Maybe Symbol).
ParameterDeclaresEntrypoints cp =>
EntrypointRef mname
-> EntrypointCall cp (GetEntrypointArgCustom cp mname)
parameterEntrypointCallCustom @p EntrypointRef mname
epRef of
    epc :: EntrypointCall p (GetEntrypointArgCustom p mname)
epc@EntrypointCall{} -> SomeEntrypointCallT (ToT (GetEntrypointArgCustom p mname))
-> Instr
     (ToTs s)
     ('TContract (ToT (GetEntrypointArgCustom p mname)) : ToTs s)
forall {inp :: [T]} {out :: [T]} (arg :: T) (s :: [T]).
(inp ~ s, out ~ ('TContract arg : s), ParameterScope arg,
 IsNotInView) =>
SomeEntrypointCallT arg -> Instr inp out
SELF (EntrypointCall p (GetEntrypointArgCustom p mname)
-> SomeEntrypointCallT (ToT (GetEntrypointArgCustom p mname))
forall (arg :: T) (param :: T).
ParameterScope param =>
EntrypointCallT param arg -> SomeEntrypointCallT arg
SomeEpc EntrypointCall p (GetEntrypointArgCustom p mname)
epc)

-- | Get a reference to a contract by its address.
--
-- This instruction carries the behaviour of @CONTRACT@ before introduction
-- of lightweight entrypoints feature.
-- The contract must __not__ have explicit "default" entrypoint for this to work.
--
-- If you are going to call a specific entrypoint of the contract, see 'contractCalling'.
contract
  :: forall p vd addr s.
      ( NiceParameterFull p, ForbidExplicitDefaultEntrypoint p
      , ToTAddress_ p vd addr
      )
  => addr : s :-> Maybe (ContractRef p) : s
contract :: forall p vd addr (s :: [*]).
(NiceParameterFull p, ForbidExplicitDefaultEntrypoint p,
 ToTAddress_ p vd addr) =>
(addr : s) :-> (Maybe (ContractRef p) : s)
contract = Instr (ToTs (addr : s)) (ToTs (Maybe (ContractRef p) : s))
-> (addr : s) :-> (Maybe (ContractRef p) : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (EpName
-> Instr
     ('TAddress : ToTs s) ('TOption ('TContract (ToT p)) : ToTs s)
forall {inp :: [T]} {out :: [T]} (p :: T) (s :: [T]).
(inp ~ ('TAddress : s), out ~ ('TOption ('TContract p) : s),
 ParameterScope p) =>
EpName -> Instr inp out
CONTRACT EpName
epName)
  where
    epName :: EpName
epName = SomeEntrypointCallT (ToT p) -> EpName
forall (arg :: T). SomeEntrypointCallT arg -> EpName
sepcName (forall cp.
(NiceParameter cp, ForbidExplicitDefaultEntrypoint cp) =>
SomeEntrypointCall cp
sepcCallRootChecked @p)

-- | Make a reference to a contract, maybe a specific entrypoint.
--
-- When calling this function, make sure that parameter type is known.
-- It's recommended that you supply 'TAddress' with a concrete parameter as the
-- stack argument.
contractCalling
  :: forall cp epRef epArg addr vd s.
     (HasEntrypointArg cp epRef epArg, ToTAddress_ cp vd addr)
  => epRef
  -> addr : s :-> Maybe (ContractRef epArg) : s
contractCalling :: forall cp epRef epArg addr vd (s :: [*]).
(HasEntrypointArg cp epRef epArg, ToTAddress_ cp vd addr) =>
epRef -> (addr : s) :-> (Maybe (ContractRef epArg) : s)
contractCalling epRef
epRef = Instr (ToTs (addr : s)) (ToTs (Maybe (ContractRef epArg) : s))
-> (addr : s) :-> (Maybe (ContractRef epArg) : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs (addr : s)) (ToTs (Maybe (ContractRef epArg) : s))
 -> (addr : s) :-> (Maybe (ContractRef epArg) : s))
-> Instr (ToTs (addr : s)) (ToTs (Maybe (ContractRef epArg) : s))
-> (addr : s) :-> (Maybe (ContractRef epArg) : s)
forall a b. (a -> b) -> a -> b
$
  case forall {k} (cp :: k) name arg.
HasEntrypointArg cp name arg =>
name -> (Dict (ParameterScope (ToT arg)), EpName)
forall cp name arg.
HasEntrypointArg cp name arg =>
name -> (Dict (ParameterScope (ToT arg)), EpName)
useHasEntrypointArg @cp @epRef @epArg epRef
epRef of
    (Dict (ParameterScope (ToT epArg))
Dict, EpName
epName) -> EpName
-> Instr
     ('TAddress : ToTs s) ('TOption ('TContract (ToT epArg)) : ToTs s)
forall {inp :: [T]} {out :: [T]} (p :: T) (s :: [T]).
(inp ~ ('TAddress : s), out ~ ('TOption ('TContract p) : s),
 ParameterScope p) =>
EpName -> Instr inp out
CONTRACT EpName
epName

-- | Specialized version of 'contractCalling' for the case when you do
-- not have compile-time evidence of appropriate 'HasEntrypointArg'.
-- For instance, if you have untyped 'EpName' you can not have this
-- evidence (the value is only available in runtime).
-- If you have typed 'EntrypointRef', use 'eprName' to construct 'EpName'.
unsafeContractCalling
  :: forall arg s.
     (NiceParameter arg)
  => EpName
  -> Address : s :-> Maybe (ContractRef arg) : s
unsafeContractCalling :: forall arg (s :: [*]).
NiceParameter arg =>
EpName -> (Address : s) :-> (Maybe (ContractRef arg) : s)
unsafeContractCalling EpName
epName = TrustEpName -> (Address : s) :-> (Maybe (ContractRef arg) : s)
forall cp epRef epArg addr vd (s :: [*]).
(HasEntrypointArg cp epRef epArg, ToTAddress_ cp vd addr) =>
epRef -> (addr : s) :-> (Maybe (ContractRef epArg) : s)
contractCalling (EpName -> TrustEpName
TrustEpName EpName
epName)

-- | Version of 'contract' instruction which may accept address with already
-- specified entrypoint name.
--
-- Also you cannot specify entrypoint name here because this could result in
-- conflict.
runFutureContract
  :: forall p s. (NiceParameter p)
  => FutureContract p : s :-> Maybe (ContractRef p) : s
runFutureContract :: forall p (s :: [*]).
NiceParameter p =>
(FutureContract p : s) :-> (Maybe (ContractRef p) : s)
runFutureContract =
  Instr (ToTs (FutureContract p : s)) (ToTs (EpAddress : s))
-> (FutureContract p : s) :-> (EpAddress : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (FutureContract p : s)) (ToTs (EpAddress : s))
forall (inp :: [T]). Instr inp inp
Nop ((FutureContract p : s) :-> (EpAddress : s))
-> ((EpAddress : s) :-> (Maybe (ContractRef p) : s))
-> (FutureContract p : s) :-> (Maybe (ContractRef p) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (EpAddress : s) :-> (Maybe (ContractRef p) : s)
forall p (s :: [*]).
NiceParameter p =>
(EpAddress : s) :-> (Maybe (ContractRef p) : s)
epAddressToContract

-- | Similar to 'runFutureContract', works with 'EpAddress'.
--
-- Validity of such operation cannot be ensured at compile time.
epAddressToContract
  :: forall p s. (NiceParameter p)
  => EpAddress : s :-> Maybe (ContractRef p) : s
epAddressToContract :: forall p (s :: [*]).
NiceParameter p =>
(EpAddress : s) :-> (Maybe (ContractRef p) : s)
epAddressToContract = Instr (ToTs (EpAddress : s)) (ToTs (Maybe (ContractRef p) : s))
-> (EpAddress : s) :-> (Maybe (ContractRef p) : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (EpName
-> Instr
     ('TAddress : ToTs s) ('TOption ('TContract (ToT p)) : ToTs s)
forall {inp :: [T]} {out :: [T]} (p :: T) (s :: [T]).
(inp ~ ('TAddress : s), out ~ ('TOption ('TContract p) : s),
 ParameterScope p) =>
EpName -> Instr inp out
CONTRACT EpName
DefEpName)

transferTokens
  :: forall p s. (NiceParameter p, IsNotInView)
  => p : Mutez : ContractRef p : s :-> Operation : s
transferTokens :: forall p (s :: [*]).
(NiceParameter p, IsNotInView) =>
(p : Mutez : ContractRef p : s) :-> (Operation : s)
transferTokens = Instr (ToTs (p : Mutez : ContractRef p : s)) (ToTs (Operation : s))
-> (p : Mutez : ContractRef p : s) :-> (Operation : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (p : Mutez : ContractRef p : s)) (ToTs (Operation : s))
forall {inp :: [T]} {out :: [T]} (p :: T) (s :: [T]).
(inp ~ (p : 'TMutez : 'TContract p : s), out ~ ('TOperation : s),
 ParameterScope p, IsNotInView) =>
Instr inp out
TRANSFER_TOKENS

setDelegate :: IsNotInView => Maybe KeyHash : s :-> Operation : s
setDelegate :: forall (s :: [*]).
IsNotInView =>
(Maybe KeyHash : s) :-> (Operation : s)
setDelegate = Instr (ToTs (Maybe KeyHash : s)) (ToTs (Operation : s))
-> (Maybe KeyHash : s) :-> (Operation : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (Maybe KeyHash : s)) (ToTs (Operation : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ ('TOption 'TKeyHash : s), out ~ ('TOperation : s),
 IsNotInView) =>
Instr inp out
SET_DELEGATE

createContract
  :: forall p g vd s. IsNotInView
  => Contract p g vd
  -> Maybe KeyHash : Mutez : g : s
  :-> Operation : TAddress p vd : s
createContract :: forall p g vd (s :: [*]).
IsNotInView =>
Contract p g vd
-> (Maybe KeyHash : Mutez : g : s)
   :-> (Operation : TAddress p vd : s)
createContract cntrc :: Contract p g vd
cntrc@Contract{} =
  Instr
  (ToTs (Maybe KeyHash : Mutez : g : s))
  (ToTs (Operation : TAddress p vd : s))
-> (Maybe KeyHash : Mutez : g : s)
   :-> (Operation : TAddress p vd : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Contract' Instr (ToT p) (ToT g)
-> Instr
     ('TOption 'TKeyHash : 'TMutez : ToT g : ToTs s)
     ('TOperation : 'TAddress : ToTs s)
forall {inp :: [T]} {out :: [T]} (p :: T) (g :: T) (s :: [T]).
(inp ~ ('TOption 'TKeyHash : 'TMutez : g : s),
 out ~ ('TOperation : 'TAddress : s), ParameterScope p,
 StorageScope g, IsNotInView) =>
Contract' Instr p g -> Instr inp out
CREATE_CONTRACT (Contract p g vd -> Contract' Instr (ToT p) (ToT g)
forall cp st vd. Contract cp st vd -> Contract (ToT cp) (ToT st)
toMichelsonContract Contract p g vd
cntrc))

implicitAccount :: KeyHash : s :-> ContractRef () : s
implicitAccount :: forall (s :: [*]). (KeyHash : s) :-> (ContractRef () : s)
implicitAccount = Instr (ToTs (KeyHash : s)) (ToTs (ContractRef () : s))
-> (KeyHash : s) :-> (ContractRef () : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (KeyHash : s)) (ToTs (ContractRef () : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ ('TKeyHash : s), out ~ ('TContract 'TUnit : s)) =>
Instr inp out
IMPLICIT_ACCOUNT

now :: s :-> Timestamp : s
now :: forall (s :: [*]). s :-> (Timestamp : s)
now = Instr (ToTs s) (ToTs (Timestamp : s)) -> s :-> (Timestamp : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs s) (ToTs (Timestamp : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TTimestamp : s)) =>
Instr inp out
NOW

minBlockTime :: s :-> Natural : s
minBlockTime :: forall (s :: [*]). s :-> (Natural : s)
minBlockTime = Instr (ToTs s) (ToTs (Natural : s)) -> s :-> (Natural : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs s) (ToTs (Natural : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TNat : s)) =>
Instr inp out
MIN_BLOCK_TIME

amount :: s :-> Mutez : s
amount :: forall (s :: [*]). s :-> (Mutez : s)
amount = Instr (ToTs s) (ToTs (Mutez : s)) -> s :-> (Mutez : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs s) (ToTs (Mutez : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TMutez : s)) =>
Instr inp out
AMOUNT

balance :: s :-> Mutez : s
balance :: forall (s :: [*]). s :-> (Mutez : s)
balance = Instr (ToTs s) (ToTs (Mutez : s)) -> s :-> (Mutez : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs s) (ToTs (Mutez : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TMutez : s)) =>
Instr inp out
BALANCE

votingPower :: KeyHash : s :-> Natural : s
votingPower :: forall (s :: [*]). (KeyHash : s) :-> (Natural : s)
votingPower = Instr (ToTs (KeyHash : s)) (ToTs (Natural : s))
-> (KeyHash : s) :-> (Natural : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (KeyHash : s)) (ToTs (Natural : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ ('TKeyHash : s), out ~ ('TNat : s)) =>
Instr inp out
VOTING_POWER

totalVotingPower :: s :-> Natural : s
totalVotingPower :: forall (s :: [*]). s :-> (Natural : s)
totalVotingPower = Instr (ToTs s) (ToTs (Natural : s)) -> s :-> (Natural : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs s) (ToTs (Natural : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TNat : s)) =>
Instr inp out
TOTAL_VOTING_POWER

checkSignature :: BytesLike bs => PublicKey : TSignature bs : bs : s :-> Bool : s
checkSignature :: forall bs (s :: [*]).
BytesLike bs =>
(PublicKey : TSignature bs : bs : s) :-> (Bool : s)
checkSignature = Instr (ToTs (PublicKey : TSignature bs : bs : s)) (ToTs (Bool : s))
-> (PublicKey : TSignature bs : bs : s) :-> (Bool : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (PublicKey : TSignature bs : bs : s)) (ToTs (Bool : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ ('TKey : 'TSignature : 'TBytes : s), out ~ ('TBool : s)) =>
Instr inp out
CHECK_SIGNATURE

sha256 :: BytesLike bs => bs : s :-> Hash Sha256 bs : s
sha256 :: forall bs (s :: [*]).
BytesLike bs =>
(bs : s) :-> (Hash Sha256 bs : s)
sha256 = Instr (ToTs (bs : s)) (ToTs (Hash Sha256 bs : s))
-> (bs : s) :-> (Hash Sha256 bs : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (bs : s)) (ToTs (Hash Sha256 bs : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ ('TBytes : s), out ~ ('TBytes : s)) =>
Instr inp out
SHA256

sha512 :: BytesLike bs => bs : s :-> Hash Sha512 bs : s
sha512 :: forall bs (s :: [*]).
BytesLike bs =>
(bs : s) :-> (Hash Sha512 bs : s)
sha512 = Instr (ToTs (bs : s)) (ToTs (Hash Sha512 bs : s))
-> (bs : s) :-> (Hash Sha512 bs : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (bs : s)) (ToTs (Hash Sha512 bs : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ ('TBytes : s), out ~ ('TBytes : s)) =>
Instr inp out
SHA512

blake2B :: BytesLike bs => bs : s :-> Hash Blake2b bs : s
blake2B :: forall bs (s :: [*]).
BytesLike bs =>
(bs : s) :-> (Hash Blake2b bs : s)
blake2B = Instr (ToTs (bs : s)) (ToTs (Hash Blake2b bs : s))
-> (bs : s) :-> (Hash Blake2b bs : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (bs : s)) (ToTs (Hash Blake2b bs : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ ('TBytes : s), out ~ ('TBytes : s)) =>
Instr inp out
BLAKE2B

sha3 :: BytesLike bs => bs : s :-> Hash Sha3 bs : s
sha3 :: forall bs (s :: [*]).
BytesLike bs =>
(bs : s) :-> (Hash Sha3 bs : s)
sha3 = Instr (ToTs (bs : s)) (ToTs (Hash Sha3 bs : s))
-> (bs : s) :-> (Hash Sha3 bs : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (bs : s)) (ToTs (Hash Sha3 bs : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ ('TBytes : s), out ~ ('TBytes : s)) =>
Instr inp out
SHA3

keccak :: BytesLike bs => bs : s :-> Hash Keccak bs : s
keccak :: forall bs (s :: [*]).
BytesLike bs =>
(bs : s) :-> (Hash Keccak bs : s)
keccak = Instr (ToTs (bs : s)) (ToTs (Hash Keccak bs : s))
-> (bs : s) :-> (Hash Keccak bs : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (bs : s)) (ToTs (Hash Keccak bs : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ ('TBytes : s), out ~ ('TBytes : s)) =>
Instr inp out
KECCAK

hashKey :: PublicKey : s :-> KeyHash : s
hashKey :: forall (s :: [*]). (PublicKey : s) :-> (KeyHash : s)
hashKey = Instr (ToTs (PublicKey : s)) (ToTs (KeyHash : s))
-> (PublicKey : s) :-> (KeyHash : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (PublicKey : s)) (ToTs (KeyHash : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ ('TKey : s), out ~ ('TKeyHash : s)) =>
Instr inp out
HASH_KEY

pairingCheck :: [(Bls12381G1, Bls12381G2)] : s :-> Bool : s
pairingCheck :: forall (s :: [*]). ([(Bls12381G1, Bls12381G2)] : s) :-> (Bool : s)
pairingCheck = Instr (ToTs ([(Bls12381G1, Bls12381G2)] : s)) (ToTs (Bool : s))
-> ([(Bls12381G1, Bls12381G2)] : s) :-> (Bool : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs ([(Bls12381G1, Bls12381G2)] : s)) (ToTs (Bool : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ ('TList ('TPair 'TBls12381G1 'TBls12381G2) : s),
 out ~ ('TBool : s)) =>
Instr inp out
PAIRING_CHECK

{-# WARNING source
    "Using `source` is considered a bad practice.\n\
\    Consider using `sender` instead until further investigation" #-}
source :: s :-> Address : s
source :: forall (s :: [*]). s :-> (Address : s)
source = Instr (ToTs s) (ToTs (Address : s)) -> s :-> (Address : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs s) (ToTs (Address : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TAddress : s)) =>
Instr inp out
SOURCE

sender :: s :-> Address : s
sender :: forall (s :: [*]). s :-> (Address : s)
sender = Instr (ToTs s) (ToTs (Address : s)) -> s :-> (Address : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs s) (ToTs (Address : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TAddress : s)) =>
Instr inp out
SENDER

address :: ContractRef a : s :-> Address : s
address :: forall a (s :: [*]). (ContractRef a : s) :-> (Address : s)
address = Instr (ToTs (ContractRef a : s)) (ToTs (Address : s))
-> (ContractRef a : s) :-> (Address : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (ContractRef a : s)) (ToTs (Address : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ ('TContract a : s), out ~ ('TAddress : s)) =>
Instr inp out
ADDRESS

chainId :: s :-> ChainId : s
chainId :: forall (s :: [*]). s :-> (ChainId : s)
chainId = Instr (ToTs s) (ToTs (ChainId : s)) -> s :-> (ChainId : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs s) (ToTs (ChainId : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TChainId : s)) =>
Instr inp out
CHAIN_ID

level :: s :-> Natural : s
level :: forall (s :: [*]). s :-> (Natural : s)
level = Instr (ToTs s) (ToTs (Natural : s)) -> s :-> (Natural : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs s) (ToTs (Natural : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TNat : s)) =>
Instr inp out
LEVEL

selfAddress :: s :-> Address : s
selfAddress :: forall (s :: [*]). s :-> (Address : s)
selfAddress = Instr (ToTs s) (ToTs (Address : s)) -> s :-> (Address : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs s) (ToTs (Address : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TAddress : s)) =>
Instr inp out
SELF_ADDRESS

never :: Never : s :-> s'
never :: forall (s :: [*]) (s' :: [*]). (Never : s) :-> s'
never = (forall (out' :: [T]). Instr (ToTs (Never : s)) out')
-> (Never : s) :-> s'
forall (inp :: [*]) (out :: [*]).
(forall (out' :: [T]). Instr (ToTs inp) out') -> inp :-> out
FI forall (out' :: [T]). Instr (ToTs (Never : s)) out'
forall (s :: [T]) (out :: [T]). Instr ('TNever : s) out
NEVER

ticket :: (NiceComparable a) => a : Natural : s :-> Maybe (Ticket a) : s
ticket :: forall a (s :: [*]).
NiceComparable a =>
(a : Natural : s) :-> (Maybe (Ticket a) : s)
ticket = Instr (ToTs (a : Natural : s)) (ToTs (Maybe (Ticket a) : s))
-> (a : Natural : s) :-> (Maybe (Ticket a) : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (a : Natural : s)) (ToTs (Maybe (Ticket a) : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : 'TNat : s), out ~ ('TOption ('TTicket a) : s),
 Comparable a) =>
Instr inp out
TICKET

-- | Note: for more advanced helpers for tickets see "Lorentz.Tickets" module.
readTicket :: Ticket a : s :-> ReadTicket a : Ticket a : s
readTicket :: forall a (s :: [*]).
(Ticket a : s) :-> (ReadTicket a : Ticket a : s)
readTicket = Instr (ToTs (Ticket a : s)) (ToTs (ReadTicket a : Ticket a : s))
-> (Ticket a : s) :-> (ReadTicket a : Ticket a : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (Ticket a : s)) (ToTs (ReadTicket a : Ticket a : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ ('TTicket a : s),
 out ~ (RightComb '[ 'TAddress, a, 'TNat] : 'TTicket a : s)) =>
Instr inp out
READ_TICKET

-- | Note: for more advanced helpers for tickets see "Lorentz.Tickets" module.
splitTicket :: Ticket a : (Natural, Natural) : s :-> Maybe (Ticket a, Ticket a) : s
splitTicket :: forall a (s :: [*]).
(Ticket a : (Natural, Natural) : s)
:-> (Maybe (Ticket a, Ticket a) : s)
splitTicket = Instr
  (ToTs (Ticket a : (Natural, Natural) : s))
  (ToTs (Maybe (Ticket a, Ticket a) : s))
-> (Ticket a : (Natural, Natural) : s)
   :-> (Maybe (Ticket a, Ticket a) : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr
  (ToTs (Ticket a : (Natural, Natural) : s))
  (ToTs (Maybe (Ticket a, Ticket a) : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ ('TTicket a : 'TPair 'TNat 'TNat : s),
 out ~ ('TOption ('TPair ('TTicket a) ('TTicket a)) : s)) =>
Instr inp out
SPLIT_TICKET

-- | Version of 'splitTicket' with entries named.
splitTicketNamed
  :: forall n1 n2 a s.
     Ticket a : (n1 :! Natural, n2 :! Natural) : s
  :-> Maybe (n1 :! Ticket a, n2 :! Ticket a) : s
splitTicketNamed :: forall (n1 :: Symbol) (n2 :: Symbol) a (s :: [*]).
(Ticket a : (n1 :! Natural, n2 :! Natural) : s)
:-> (Maybe (n1 :! Ticket a, n2 :! Ticket a) : s)
splitTicketNamed = Instr
  (ToTs (Ticket a : (n1 :! Natural, n2 :! Natural) : s))
  (ToTs (Maybe (n1 :! Ticket a, n2 :! Ticket a) : s))
-> (Ticket a : (n1 :! Natural, n2 :! Natural) : s)
   :-> (Maybe (n1 :! Ticket a, n2 :! Ticket a) : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr
  (ToTs (Ticket a : (n1 :! Natural, n2 :! Natural) : s))
  (ToTs (Maybe (n1 :! Ticket a, n2 :! Ticket a) : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ ('TTicket a : 'TPair 'TNat 'TNat : s),
 out ~ ('TOption ('TPair ('TTicket a) ('TTicket a)) : s)) =>
Instr inp out
SPLIT_TICKET

-- | Note: for more advanced helpers for tickets see "Lorentz.Tickets" module.
joinTickets :: (Ticket a, Ticket a) : s :-> Maybe (Ticket a) : s
joinTickets :: forall a (s :: [*]).
((Ticket a, Ticket a) : s) :-> (Maybe (Ticket a) : s)
joinTickets = Instr
  (ToTs ((Ticket a, Ticket a) : s)) (ToTs (Maybe (Ticket a) : s))
-> ((Ticket a, Ticket a) : s) :-> (Maybe (Ticket a) : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr
  (ToTs ((Ticket a, Ticket a) : s)) (ToTs (Maybe (Ticket a) : s))
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ ('TPair ('TTicket a) ('TTicket a) : s),
 out ~ ('TOption ('TTicket a) : s)) =>
Instr inp out
JOIN_TICKETS

openChest :: ChestKey : Chest : Natural : s :-> OpenChest : s
openChest :: forall (s :: [*]).
(ChestKey : Chest : Natural : s) :-> (OpenChest : s)
openChest = Instr
  (ToTs (ChestKey : Chest : Natural : s)) (ToTs (OpenChest : s))
-> (ChestKey : Chest : Natural : s) :-> (OpenChest : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr
  (ToTs (ChestKey : Chest : Natural : s)) (ToTs (OpenChest : s))
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ ('TChestKey : 'TChest : 'TNat : s),
 out ~ ('TOr 'TBytes 'TBool : s)) =>
Instr inp out
OPEN_CHEST

{-# DEPRECATED openChest
  "Due to a vulnerability discovered in time-lock protocol, \
  \OPEN_CHEST is temporarily deprecated since Lima" #-}

-- | Version of 'emit' that adds the type annotation, only when @t@ has annotations.
emit :: forall t s. (NicePackedValue t, HasAnnotation t) => FieldAnn -> t : s :-> Operation : s
emit :: forall t (s :: [*]).
(NicePackedValue t, HasAnnotation t) =>
FieldAnn -> (t : s) :-> (Operation : s)
emit FieldAnn
tag = FieldAnn -> Maybe (Notes (ToT t)) -> (t : s) :-> (Operation : s)
forall t (s :: [*]).
NicePackedValue t =>
FieldAnn -> Maybe (Notes (ToT t)) -> (t : s) :-> (Operation : s)
emit' FieldAnn
tag Maybe (Notes (ToT t))
ann'
  where
    ann :: Notes (ToT t)
ann = forall a. HasAnnotation a => FollowEntrypointFlag -> Notes (ToT a)
getAnnotation @t FollowEntrypointFlag
NotFollowEntrypoint
    -- type without annotations can be inferred by the runtime, so
    -- here we omit the annotation for efficiency if it's unnecessary.
    ann' :: Maybe (Notes (ToT t))
ann' | Notes (ToT t)
ann Notes (ToT t) -> Notes (ToT t) -> Bool
forall a. Eq a => a -> a -> Bool
== Notes (ToT t)
forall (t :: T). SingI t => Notes t
starNotes = Maybe (Notes (ToT t))
forall a. Maybe a
Nothing
         | Bool
otherwise = Notes (ToT t) -> Maybe (Notes (ToT t))
forall a. a -> Maybe a
Just Notes (ToT t)
ann

-- | Version of 'emit' that omits the type annotation, letting the runtime infer
-- it instead.
emitAuto :: forall t s. NicePackedValue t => FieldAnn -> t : s :-> Operation : s
emitAuto :: forall t (s :: [*]).
NicePackedValue t =>
FieldAnn -> (t : s) :-> (Operation : s)
emitAuto FieldAnn
tag = FieldAnn -> Maybe (Notes (ToT t)) -> (t : s) :-> (Operation : s)
forall t (s :: [*]).
NicePackedValue t =>
FieldAnn -> Maybe (Notes (ToT t)) -> (t : s) :-> (Operation : s)
emit' FieldAnn
tag Maybe (Notes (ToT t))
forall a. Maybe a
Nothing

emit'
  :: forall t s. NicePackedValue t
  => FieldAnn
  -> Maybe (Notes (ToT t))
  -> t : s :-> Operation : s
emit' :: forall t (s :: [*]).
NicePackedValue t =>
FieldAnn -> Maybe (Notes (ToT t)) -> (t : s) :-> (Operation : s)
emit' FieldAnn
tag Maybe (Notes (ToT t))
mNotes = Instr (ToTs (t : s)) (ToTs (Operation : s))
-> (t : s) :-> (Operation : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs (t : s)) (ToTs (Operation : s))
 -> (t : s) :-> (Operation : s))
-> Instr (ToTs (t : s)) (ToTs (Operation : s))
-> (t : s) :-> (Operation : s)
forall a b. (a -> b) -> a -> b
$ FieldAnn
-> Maybe (Notes (ToT t))
-> Instr (ToT t : ToTs s) ('TOperation : ToTs s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ (t : s), out ~ ('TOperation : s), PackedValScope t) =>
FieldAnn -> Maybe (Notes t) -> Instr inp out
EMIT FieldAnn
tag Maybe (Notes (ToT t))
mNotes

----------------------------------------------------------------------------
-- Non-canonical instructions
----------------------------------------------------------------------------

-- | Helper instruction.
--
-- Checks whether given key present in the storage and fails if it is.
-- This instruction leaves stack intact.
failingWhenPresent
  :: forall c k s v st e.
     ( MemOpHs c, k ~ MemOpKeyHs c
     , NiceConstant e
     , Dupable c, Dupable (MemOpKeyHs c)
     , st ~ (k : v : c : s)
     )
  => (forall s0. k : s0 :-> e : s0)
  -> st :-> st
failingWhenPresent :: forall c k (s :: [*]) v (st :: [*]) e.
(MemOpHs c, k ~ MemOpKeyHs c, NiceConstant e, Dupable c,
 Dupable (MemOpKeyHs c), st ~ (k : v : c : s)) =>
(forall (s0 :: [*]). (k : s0) :-> (e : s0)) -> st :-> st
failingWhenPresent forall (s0 :: [*]). (k : s0) :-> (e : s0)
mkErr =
  forall (n :: Nat) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @3 (st :-> (c : k : v : c : s))
-> ((c : k : v : c : s) :-> (MemOpKeyHs c : c : k : v : c : s))
-> st :-> (MemOpKeyHs c : c : k : v : c : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall (n :: Nat) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @2 (st :-> (MemOpKeyHs c : c : k : v : c : s))
-> ((MemOpKeyHs c : c : k : v : c : s) :-> (Bool : k : v : c : s))
-> st :-> (Bool : k : v : c : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (MemOpKeyHs c : c : k : v : c : s) :-> (Bool : k : v : c : s)
forall c (s :: [*]).
MemOpHs c =>
(MemOpKeyHs c : c : s) :-> (Bool : s)
mem (st :-> (Bool : k : v : c : s))
-> ((Bool : k : v : c : s) :-> (k : v : c : s))
-> st :-> (k : v : c : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  ((k : v : c : s) :-> (k : v : c : s))
-> ((k : v : c : s) :-> (k : v : c : s))
-> (Bool : k : v : c : s) :-> (k : v : c : s)
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
if_ ((k : v : c : s) :-> (e : v : c : s)
forall (s0 :: [*]). (k : s0) :-> (e : s0)
mkErr ((k : v : c : s) :-> (e : v : c : s))
-> ((e : v : c : s) :-> (k : v : c : s))
-> (k : v : c : s) :-> (k : v : c : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (e : v : c : s) :-> (k : v : c : s)
forall a (s :: [*]) (t :: [*]). NiceConstant a => (a : s) :-> t
failWith) (k : v : c : s) :-> (k : v : c : s)
forall (s :: [*]). s :-> s
nop

-- | Like 'update', but throw an error on attempt to overwrite existing entry.
updateNew
  :: forall c k s e.
     ( UpdOpHs c, MemOpHs c, GetOpHs c
     , k ~ UpdOpKeyHs c, k ~ MemOpKeyHs c, k ~ GetOpKeyHs c
     , KnownValue (GetOpValHs c), NiceConstant e, Dupable k
     )
  => (forall s0. k : s0 :-> e : s0)
  -> k : UpdOpParamsHs c : c : s :-> c : s
updateNew :: forall c k (s :: [*]) e.
(UpdOpHs c, MemOpHs c, GetOpHs c, k ~ UpdOpKeyHs c,
 k ~ MemOpKeyHs c, k ~ GetOpKeyHs c, KnownValue (GetOpValHs c),
 NiceConstant e, Dupable k) =>
(forall (s0 :: [*]). (k : s0) :-> (e : s0))
-> (k : UpdOpParamsHs c : c : s) :-> (c : s)
updateNew forall (s0 :: [*]). (k : s0) :-> (e : s0)
mkErr = (k : UpdOpParamsHs c : c : s) :-> (k : k : UpdOpParamsHs c : c : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup ((k : UpdOpParamsHs c : c : s)
 :-> (k : k : UpdOpParamsHs c : c : s))
-> ((k : k : UpdOpParamsHs c : c : s)
    :-> (k : Maybe (GetOpValHs c) : c : s))
-> (k : UpdOpParamsHs c : c : s)
   :-> (k : Maybe (GetOpValHs c) : c : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((k : UpdOpParamsHs c : c : s) :-> (Maybe (GetOpValHs c) : c : s))
-> (k : k : UpdOpParamsHs c : c : s)
   :-> (k : Maybe (GetOpValHs c) : c : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (k : UpdOpParamsHs c : c : s) :-> (Maybe (GetOpValHs c) : c : s)
forall c (s :: [*]).
(GetOpHs c, UpdOpHs c, KnownValue (GetOpValHs c),
 UpdOpKeyHs c ~ GetOpKeyHs c) =>
(UpdOpKeyHs c : UpdOpParamsHs c : c : s)
:-> (Maybe (GetOpValHs c) : c : s)
getAndUpdate ((k : UpdOpParamsHs c : c : s)
 :-> (k : Maybe (GetOpValHs c) : c : s))
-> ((k : Maybe (GetOpValHs c) : c : s)
    :-> (Maybe (GetOpValHs c) : k : c : s))
-> (k : UpdOpParamsHs c : c : s)
   :-> (Maybe (GetOpValHs c) : k : c : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (k : Maybe (GetOpValHs c) : c : s)
:-> (Maybe (GetOpValHs c) : k : c : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((k : UpdOpParamsHs c : c : s)
 :-> (Maybe (GetOpValHs c) : k : c : s))
-> ((Maybe (GetOpValHs c) : k : c : s) :-> (c : s))
-> (k : UpdOpParamsHs c : c : s) :-> (c : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((k : c : s) :-> (c : s))
-> ((GetOpValHs c : k : c : s) :-> (c : s))
-> (Maybe (GetOpValHs c) : k : c : s) :-> (c : s)
forall (s :: [*]) (s' :: [*]) a.
(s :-> s') -> ((a : s) :-> s') -> (Maybe a : s) :-> s'
ifNone (k : c : s) :-> (c : s)
forall a (s :: [*]). (a : s) :-> s
drop ((GetOpValHs c : k : c : s) :-> (k : c : s)
forall a (s :: [*]). (a : s) :-> s
drop ((GetOpValHs c : k : c : s) :-> (k : c : s))
-> ((k : c : s) :-> (e : c : s))
-> (GetOpValHs c : k : c : s) :-> (e : c : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (k : c : s) :-> (e : c : s)
forall (s0 :: [*]). (k : s0) :-> (e : s0)
mkErr ((GetOpValHs c : k : c : s) :-> (e : c : s))
-> ((e : c : s) :-> (c : s))
-> (GetOpValHs c : k : c : s) :-> (c : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (e : c : s) :-> (c : s)
forall a (s :: [*]) (t :: [*]). NiceConstant a => (a : s) :-> t
failWith)

class LorentzFunctor (c :: Type -> Type) a b where
  lmap :: KnownValue b => ('[a] :-> '[b]) -> (c a : s :-> c b : s)

instance LorentzFunctor Maybe a b where
  lmap :: forall (s :: [*]).
KnownValue b =>
('[a] :-> '[b]) -> (Maybe a : s) :-> (Maybe b : s)
lmap = ('[Maybe a] :-> '[Maybe b]) -> (Maybe a : s) :-> (Maybe b : s)
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
framed (('[Maybe a] :-> '[Maybe b]) -> (Maybe a : s) :-> (Maybe b : s))
-> (('[a] :-> '[b]) -> '[Maybe a] :-> '[Maybe b])
-> ('[a] :-> '[b])
-> (Maybe a : s) :-> (Maybe b : s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ('[a] :-> '[b]) -> '[Maybe a] :-> '[Maybe b]
forall c b (s :: [*]).
(MapOpHs c, IsoMapOpRes c b, KnownValue b, HasCallStack) =>
((MapOpInpHs c : s) :-> (b : s))
-> (c : s) :-> (MapOpResHs c b : s)
map

instance KnownValue a => LorentzFunctor (Either a) a b where
  lmap :: forall (s :: [*]).
KnownValue b =>
('[a] :-> '[b]) -> (Either a a : s) :-> (Either a b : s)
lmap '[a] :-> '[b]
f = (((a : s) :-> (Either a b : s))
-> ((a : s) :-> (Either a b : s))
-> (Either a a : s) :-> (Either a b : s)
forall a (s :: [*]) (s' :: [*]) b.
((a : s) :-> s') -> ((b : s) :-> s') -> (Either a b : s) :-> s'
ifLeft (a : s) :-> (Either a b : s)
forall a b (s :: [*]). KnownValue b => (a : s) :-> (Either a b : s)
left (('[a] :-> '[b]) -> ('[a] ++ s) :-> ('[b] ++ s)
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
framed '[a] :-> '[b]
f ((a : s) :-> (b : s))
-> ((b : s) :-> (Either a b : s)) -> (a : s) :-> (Either a b : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (b : s) :-> (Either a b : s)
forall a b (s :: [*]). KnownValue a => (b : s) :-> (Either a b : s)
right))

instance LorentzFunctor [] a b where
  lmap :: forall (s :: [*]).
KnownValue b =>
('[a] :-> '[b]) -> ([a] : s) :-> ([b] : s)
lmap = ('[[a]] :-> '[[b]]) -> ([a] : s) :-> ([b] : s)
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
framed (('[[a]] :-> '[[b]]) -> ([a] : s) :-> ([b] : s))
-> (('[a] :-> '[b]) -> '[[a]] :-> '[[b]])
-> ('[a] :-> '[b])
-> ([a] : s) :-> ([b] : s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ('[a] :-> '[b]) -> '[[a]] :-> '[[b]]
forall c b (s :: [*]).
(MapOpHs c, IsoMapOpRes c b, KnownValue b, HasCallStack) =>
((MapOpInpHs c : s) :-> (b : s))
-> (c : s) :-> (MapOpResHs c b : s)
map

instance NiceComparable k => LorentzFunctor (Map k) a b where
  lmap :: forall (s :: [*]).
KnownValue b =>
('[a] :-> '[b]) -> (Map k a : s) :-> (Map k b : s)
lmap '[a] :-> '[b]
f = (((MapOpInpHs (Map k a) : s) :-> (b : s))
-> (Map k a : s) :-> (MapOpResHs (Map k a) b : s)
forall c b (s :: [*]).
(MapOpHs c, IsoMapOpRes c b, KnownValue b, HasCallStack) =>
((MapOpInpHs c : s) :-> (b : s))
-> (c : s) :-> (MapOpResHs c b : s)
map (((k, a) : s) :-> (a : s)
forall a b (s :: [*]). ((a, b) : s) :-> (b : s)
cdr (((k, a) : s) :-> (a : s))
-> ((a : s) :-> (b : s)) -> ((k, a) : s) :-> (b : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ('[a] :-> '[b]) -> ('[a] ++ s) :-> ('[b] ++ s)
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
framed '[a] :-> '[b]
f))

instance (NiceComparable a, NiceComparable b) => LorentzFunctor Set a b where
  lmap :: forall (s :: [*]).
KnownValue b =>
('[a] :-> '[b]) -> (Set a : s) :-> (Set b : s)
lmap '[a] :-> '[b]
f = (s :-> (Set b : s)) -> (Set a : s) :-> (Set a : Set b : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip s :-> (Set b : s)
forall e (s :: [*]). NiceComparable e => s :-> (Set e : s)
emptySet ((Set a : s) :-> (Set a : Set b : s))
-> ((Set a : Set b : s) :-> (Set b : s))
-> (Set a : s) :-> (Set b : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((IterOpElHs (Set a) : Set b : s) :-> (Set b : s))
-> (Set a : Set b : s) :-> (Set b : s)
forall c (s :: [*]).
(IterOpHs c, HasCallStack) =>
((IterOpElHs c : s) :-> s) -> (c : s) :-> s
iter (IterOpElHs (Set a) : Set b : s) :-> (Set b : s)
forall (s :: [*]). (a : Set b : s) :-> (Set b : s)
body
    where
      body :: a : Set b : s :-> Set b : s
      body :: forall (s :: [*]). (a : Set b : s) :-> (Set b : s)
body =
        ('[a] :-> '[b]) -> ('[a] ++ (Set b : s)) :-> ('[b] ++ (Set b : s))
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
framed '[a] :-> '[b]
f ((a : Set b : s) :-> (b : Set b : s))
-> ((b : Set b : s) :-> (b : Bool : Set b : s))
-> (a : Set b : s) :-> (b : Bool : Set b : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
        ((Set b : s) :-> (Bool : Set b : s))
-> (b : Set b : s) :-> (b : Bool : Set b : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Bool -> (Set b : s) :-> (Bool : Set b : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Bool
True) ((a : Set b : s) :-> (b : Bool : Set b : s))
-> ((b : Bool : Set b : s) :-> (Set b : s))
-> (a : Set b : s) :-> (Set b : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
        (b : Bool : Set b : s) :-> (Set b : s)
forall c (s :: [*]).
UpdOpHs c =>
(UpdOpKeyHs c : UpdOpParamsHs c : c : s) :-> (c : s)
update