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

{-# 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
  , 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
  , 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
  , LorentzFunctor (..)
  ) where

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

import Data.Constraint ((\\))
import GHC.TypeNats (Nat)

import Lorentz.Address
import Lorentz.Arith
import Lorentz.Base
import Lorentz.Bytes
import Lorentz.Constraints
import Lorentz.Entrypoints
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(..), RemFail(..), SingI, SomeEntrypointCallT(..), UpdateN, Value'(..), pattern CAR,
  pattern CDR, pattern LEFT, pattern PAIR, pattern RIGHT, pattern UNPAIR, sepcName, starNotes)
import Morley.Michelson.Typed.Arith
import Morley.Michelson.Typed.Haskell.Value
import Morley.Util.Named
import Morley.Util.Peano
import Morley.Util.PeanoNatural
import Morley.Util.Type
import Morley.Util.TypeLits

nop :: s :-> s
nop :: 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 :: (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 :: 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
$ SingIPeano n => PeanoNatural (ToPeano n)
forall (n :: Nat). SingIPeano n => PeanoNatural (ToPeano n)
toPeanoNatural' @n
  where
    _example :: '[ Integer, Integer, Integer ] :-> '[]
    _example :: '[Integer, Integer, Integer] :-> '[]
_example = forall (s :: [*]).
(SingIPeano 3, RequireLongerOrSameLength (ToTs s) (ToPeano 3),
 Drop (ToPeano 3) (ToTs s) ~ ToTs (Drop (ToPeano 3) s)) =>
s :-> Drop (ToPeano 3) s
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 :: (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 (a :: T) (s :: [T]).
DupableScope a =>
Instr (a : s) (a : a : s)
DUP (DupableScope (ToT a) => (a : s) :-> (a : a : s))
-> (((SingI (ToT a), FailOnTicketFound (ContainsTicket (ToT a))),
     KnownValue a)
    :- DupableScope (ToT a))
-> (a : s) :-> (a : a : s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((SingI (ToT a), FailOnTicketFound (ContainsTicket (ToT a))),
 KnownValue a)
:- DupableScope (ToT a)
forall a. Dupable a :- DupableScope (ToT a)
dupableEvi @a

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 :: inp :-> out
dupNPeano = (Instr (ToTs inp) (ToTs (a : inp)) -> inp :-> (a : inp)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs inp) (ToTs (a : inp)) -> inp :-> (a : inp))
-> Instr (ToTs inp) (ToTs (a : inp)) -> inp :-> (a : inp)
forall a b. (a -> b) -> a -> b
$ PeanoNatural n
-> Instr
     (Take (Decrement n) (ToTs inp) ++ (ToT a : Drop n (ToTs inp)))
     (ToT a
        : (Take (Decrement n) (ToTs inp) ++ (ToT a : Drop n (ToTs inp))))
forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T).
(ConstraintDUPN n inp out a, DupableScope a) =>
PeanoNatural n -> Instr inp out
DUPN (PeanoNatural n
 -> Instr
      (Take (Decrement n) (ToTs inp) ++ (ToT a : Drop n (ToTs inp)))
      (ToT a
         : (Take (Decrement n) (ToTs inp) ++ (ToT a : Drop n (ToTs inp)))))
-> PeanoNatural n
-> Instr
     (Take (Decrement n) (ToTs inp) ++ (ToT a : Drop n (ToTs inp)))
     (ToT a
        : (Take (Decrement n) (ToTs inp) ++ (ToT a : Drop n (ToTs inp))))
forall a b. (a -> b) -> a -> b
$ SingI n => PeanoNatural n
forall (n :: Peano). SingI n => PeanoNatural n
toPeanoNatural @n) (DupableScope (ToT a) => inp :-> out)
-> (((SingI (ToT a), FailOnTicketFound (ContainsTicket (ToT a))),
     KnownValue a)
    :- DupableScope (ToT a))
-> inp :-> out
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((SingI (ToT a), FailOnTicketFound (ContainsTicket (ToT a))),
 KnownValue a)
:- DupableScope (ToT a)
forall a. Dupable a :- DupableScope (ToT a)
dupableEvi @a

dupN ::
  forall (n :: Nat) a inp out.
  ( ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a ) => inp :-> out
dupN :: inp :-> out
dupN = forall a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
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 a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano 3) inp out a, Dupable a) =>
inp :-> out
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 :: (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 :: 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
     (Take n (ToTs inp) ++ (ToT a : Drop ('S n) (ToTs inp)))
     (ToT a : (Take 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
      (Take n (ToTs inp) ++ (ToT a : Drop ('S n) (ToTs inp)))
      (ToT a : (Take n (ToTs inp) ++ Drop ('S n) (ToTs inp))))
-> PeanoNatural n
-> Instr
     (Take n (ToTs inp) ++ (ToT a : Drop ('S n) (ToTs inp)))
     (ToT a : (Take n (ToTs inp) ++ Drop ('S n) (ToTs inp)))
forall a b. (a -> b) -> a -> b
$ SingI n => PeanoNatural n
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 :: inp :-> out
dig = forall (inp :: [*]) (out :: [*]) a.
ConstraintDIGLorentz (ToPeano n) inp out a =>
inp :-> out
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 (inp :: [*]) (out :: [*]) a.
ConstraintDIGLorentz (ToPeano 3) inp out a =>
inp :-> out
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 :: 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 : ToTs (Drop ('S 'Z) inp))
     (Take 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 : ToTs (Drop ('S 'Z) inp))
      (Take n (Drop ('S 'Z) (ToTs inp))
       ++ (ToT a : Drop ('S n) (ToTs inp))))
-> PeanoNatural n
-> Instr
     (ToT a : ToTs (Drop ('S 'Z) inp))
     (Take n (Drop ('S 'Z) (ToTs inp))
      ++ (ToT a : Drop ('S n) (ToTs inp)))
forall a b. (a -> b) -> a -> b
$ SingI n => PeanoNatural n
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 :: inp :-> out
dug = forall (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz (ToPeano n) inp out a =>
inp :-> out
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 (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz (ToPeano 3) inp out a =>
inp :-> out
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 :: 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 (t :: T) (inp :: [T]).
ConstantScope t =>
Value' Instr t -> Instr inp (t : inp)
PUSH (t -> Value' Instr (ToT t)
forall a. IsoValue a => a -> Value (ToT a)
toVal t
a) (ConstantScope (ToT t) => Instr (ToTs s) (ToT t : ToTs s))
-> (((SingI (ToT t), WellTyped (ToT t),
      FailOnOperationFound (ContainsOp (ToT t)),
      FailOnBigMapFound (ContainsBigMap (ToT t)),
      FailOnContractFound (ContainsContract (ToT t)),
      FailOnTicketFound (ContainsTicket (ToT t)),
      FailOnSaplingStateFound (ContainsSaplingState (ToT t))),
     KnownValue t)
    :- ConstantScope (ToT t))
-> Instr (ToTs s) (ToT t : ToTs s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((SingI (ToT t), WellTyped (ToT t),
  FailOnOperationFound (ContainsOp (ToT t)),
  FailOnBigMapFound (ContainsBigMap (ToT t)),
  FailOnContractFound (ContainsContract (ToT t)),
  FailOnTicketFound (ContainsTicket (ToT t)),
  FailOnSaplingStateFound (ContainsSaplingState (ToT t))),
 KnownValue t)
:- ConstantScope (ToT t)
forall a. NiceConstant a :- ConstantScope (ToT a)
niceConstantEvi @t

some :: a : s :-> Maybe a : s
some :: (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 (a :: T) (s :: [T]). Instr (a : s) ('TOption a : s)
SOME

none :: forall a s . KnownValue a => s :-> (Maybe a : s)
none :: 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 (a :: T) (inp :: [T]).
SingI a =>
Instr inp ('TOption a : inp)
NONE

unit :: s :-> () : s
unit :: 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]). Instr inp ('TUnit : inp)
UNIT

ifNone
  :: (s :-> s') -> (a : s :-> s') -> (Maybe a : s :-> s')
ifNone :: (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 :: (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 (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ (a : b : s), o ~ ('TPair a b : s)) =>
Instr i o
PAIR

car :: (a, b) : s :-> a : s
car :: ((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 (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (a : s)) =>
Instr i o
CAR

cdr :: (a, b) : s :-> b : s
cdr :: ((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 (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (b : s)) =>
Instr i o
CDR

unpair :: (a, b) : s :-> a : b : s
unpair :: ((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 (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (a : b : s)) =>
Instr i o
UNPAIR

left :: forall a b s. KnownValue b => a : s :-> Either a b : s
left :: (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 (i :: [T]) (o :: [T]) (b :: T) (a :: T) (s :: [T]).
(SingI b, i ~ (a : s), o ~ ('TOr a b : s)) =>
Instr i o
LEFT

right :: forall a b s. KnownValue a => b : s :-> Either a b : s
right :: (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 (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(SingI a, i ~ (b : s), o ~ ('TOr a b : s)) =>
Instr i o
RIGHT

ifLeft
  :: (a : s :-> s') -> (b : s :-> s') -> (Either a b : s :-> s')
ifLeft :: ((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 :: 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 (p :: T) (inp :: [T]). SingI p => Instr inp ('TList p : inp)
NIL

cons :: a : List a : s :-> List a : s
cons :: (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 (a :: T) (s :: [T]). Instr (a : 'TList a : s) ('TList a : s)
CONS

ifCons
  :: (a : List a : s :-> s') -> (s :-> s') -> (List a : s :-> s')
ifCons :: ((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 :: (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 (c :: T) (s :: [T]). SizeOp c => Instr (c : s) ('TNat : s)
SIZE

emptySet :: (NiceComparable e) => s :-> Set e : s
emptySet :: 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 (e :: T) (inp :: [T]).
(SingI e, Comparable e) =>
Instr inp ('TSet e : inp)
EMPTY_SET

emptyMap :: (NiceComparable k, KnownValue v)
         => s :-> Map k v : s
emptyMap :: 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 (a :: T) (b :: T) (inp :: [T]).
(SingI a, SingI b, Comparable a) =>
Instr inp ('TMap a b : inp)
EMPTY_MAP

emptyBigMap :: (NiceComparable k, KnownValue v, NiceNoBigMap v)
            => s :-> BigMap k v : s
emptyBigMap :: 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 (a :: T) (b :: T) (inp :: [T]).
(SingI a, SingI b, Comparable a, HasNoBigMap b) =>
Instr inp ('TBigMap a b : inp)
EMPTY_BIG_MAP

map
  :: (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))
-> (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 (c :: T) (b :: T) (s :: [T]).
(MapOp c, SingI b) =>
Instr (MapOpInp c : s) (b : s) -> Instr (c : s) (MapOpRes c b : s)
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 :: ((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 :: (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 (c :: T) (s :: [T]).
MemOp c =>
Instr (MemOpKey c : c : s) ('TBool : s)
MEM

get
  :: (GetOpHs c, KnownValue (GetOpValHs c))
  => GetOpKeyHs c : c : s :-> Maybe (GetOpValHs c) : s
get :: (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 (c :: T) (s :: [T]).
(GetOp c, SingI (GetOpVal c)) =>
Instr (GetOpKey c : c : s) ('TOption (GetOpVal c) : s)
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 :: (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 (ix :: Peano) (pair :: T) (s :: [T]).
ConstraintGetN ix pair =>
PeanoNatural ix -> Instr (pair : s) (GetN ix pair : s)
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
$ SingIPeano n => PeanoNatural (ToPeano n)
forall (n :: Nat). SingIPeano n => PeanoNatural (ToPeano n)
toPeanoNatural' @n
  where
    _example :: '[ (Integer, Natural), () ] :-> '[ Integer, () ]
    _example :: '[(Integer, Natural), ()] :-> '[Integer, ()]
_example = forall pair (s :: [*]).
ConstraintPairGetLorentz 1 pair =>
(pair : s) :-> (PairGetHs (ToPeano 1) pair : s)
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 :: (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 (c :: T) (s :: [T]).
UpdOp c =>
Instr (UpdOpKey c : UpdOpParams c : c : s) (c : s)
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 :: (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 (c :: T) (s :: [T]).
(GetOp c, UpdOp c, SingI (GetOpVal c), UpdOpKey c ~ GetOpKey c) =>
Instr
  (UpdOpKey c : UpdOpParams c : c : s)
  ('TOption (GetOpVal c) : c : s)
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 :: (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 (ix :: Peano) (val :: T) (pair :: T) (s :: [T]).
ConstraintUpdateN ix pair =>
PeanoNatural ix -> Instr (val : pair : s) (UpdateN ix val pair : s)
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
$ SingIPeano n => PeanoNatural (ToPeano n)
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 val pair (s :: [*]).
ConstraintPairUpdateLorentz 1 val pair =>
(val : pair : s) :-> (PairUpdateHs (ToPeano 1) val pair : s)
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_ :: (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 :: (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 :: ((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]
  => (i :-> o) -> (s :-> (i :-> o) : s)
lambda :: (i :-> o) -> s :-> ((i :-> o) : s)
lambda i :-> o
instr = case (i :-> o) -> Lambda (ZippedStack i) (ZippedStack o)
forall (inp :: [*]) (out :: [*]).
ZipInstrs '[inp, out] =>
(inp :-> out) -> Lambda (ZippedStack inp) (ZippedStack out)
zippingStack i :-> o
instr of
  I l -> Instr (ToTs s) (ToTs ((i :-> o) : s)) -> s :-> ((i :-> o) : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Value' Instr ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)))
-> Instr
     (ToTs s)
     ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)) : ToTs s)
forall (i :: T) (o :: T) (inp :: [T]).
(SingI i, SingI o) =>
Value' Instr ('TLambda i o) -> Instr inp ('TLambda i o : inp)
LAMBDA (Value'
   Instr ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)))
 -> Instr
      (ToTs s)
      ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)) : ToTs s))
-> (RemFail Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)]
    -> Value'
         Instr ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o))))
-> RemFail Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)]
-> Instr
     (ToTs s)
     ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)) : ToTs s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RemFail Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)]
-> Value'
     Instr ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)))
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(SingI inp, SingI out,
 forall (i :: [T]) (o :: [T]). Show (instr i o),
 forall (i :: [T]) (o :: [T]). Eq (instr i o),
 forall (i :: [T]) (o :: [T]). NFData (instr i o)) =>
RemFail instr '[inp] '[out] -> Value' instr ('TLambda inp out)
VLam (RemFail Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)]
 -> Instr
      (ToTs s)
      ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)) : ToTs s))
-> 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 l -> Instr (ToTs s) (ToTs ((i :-> o) : s)) -> s :-> ((i :-> o) : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Value' Instr ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)))
-> Instr
     (ToTs s)
     ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)) : ToTs s)
forall (i :: T) (o :: T) (inp :: [T]).
(SingI i, SingI o) =>
Value' Instr ('TLambda i o) -> Instr inp ('TLambda i o : inp)
LAMBDA (Value'
   Instr ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)))
 -> Instr
      (ToTs s)
      ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)) : ToTs s))
-> (RemFail Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)]
    -> Value'
         Instr ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o))))
-> RemFail Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)]
-> Instr
     (ToTs s)
     ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)) : ToTs s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RemFail Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)]
-> Value'
     Instr ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)))
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(SingI inp, SingI out,
 forall (i :: [T]) (o :: [T]). Show (instr i o),
 forall (i :: [T]) (o :: [T]). Eq (instr i o),
 forall (i :: [T]) (o :: [T]). NFData (instr i o)) =>
RemFail instr '[inp] '[out] -> Value' instr ('TLambda inp out)
VLam (RemFail Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)]
 -> Instr
      (ToTs s)
      ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)) : ToTs s))
-> 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)

exec :: a : Lambda a b : s :-> b : s
exec :: (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 (t1 :: T) (t2 :: T) (s :: [T]).
Instr (t1 : 'TLambda t1 t2 : s) (t2 : s)
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])
  => ((i :-> o) : (i ++ s)) :-> (o ++ s)
execute :: ((i :-> o) : (i ++ s)) :-> (o ++ s)
execute = forall (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
framed @s ((((i :-> o) : i) :-> o) -> (((i :-> o) : i) ++ s) :-> (o ++ s))
-> (((i :-> o) : i) :-> o) -> (((i :-> o) : i) ++ s) :-> (o ++ s)
forall a b. (a -> b) -> a -> b
$
  (i :-> '[ZippedStack i])
-> ((i :-> o) : i) :-> '[i :-> o, ZippedStack i]
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (ZipInstr i => i :-> '[ZippedStack i]
forall (s :: [*]). ZipInstr s => s :-> '[ZippedStack s]
zipInstr @i) (((i :-> o) : i) :-> '[i :-> o, ZippedStack i])
-> ('[i :-> o, ZippedStack i] :-> '[ZippedStack i, i :-> o])
-> ((i :-> o) : i) :-> '[ZippedStack i, i :-> o]
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# '[i :-> o, ZippedStack i] :-> '[ZippedStack i, i :-> o]
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap (((i :-> o) : i) :-> '[ZippedStack i, i :-> o])
-> ('[ZippedStack i, i :-> o] :-> '[ZippedStack o])
-> ((i :-> o) : i) :-> '[ZippedStack o]
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Instr (ToTs '[ZippedStack i, i :-> o]) (ToTs '[ZippedStack o])
-> '[ZippedStack i, i :-> o] :-> '[ZippedStack o]
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs '[ZippedStack i, i :-> o]) (ToTs '[ZippedStack o])
forall (t1 :: T) (t2 :: T) (s :: [T]).
Instr (t1 : 'TLambda t1 t2 : s) (t2 : s)
EXEC (((i :-> o) : i) :-> '[ZippedStack o])
-> ('[ZippedStack o] :-> o) -> ((i :-> o) : i) :-> o
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ZipInstr o => '[ZippedStack o] :-> o
forall (s :: [*]). ZipInstr s => '[ZippedStack s] :-> s
unzipInstr @o
  where
    _example
      :: ([Integer, Natural] :-> [(), ()]) : Integer : Natural : s
      :-> () : () : s
    _example :: (('[Integer, Natural] :-> '[(), ()]) : Integer : Natural : s)
:-> (() : () : s)
_example = (('[Integer, Natural] :-> '[(), ()]) : Integer : Natural : s)
:-> (() : () : s)
forall (i :: [*]) (o :: [*]) (s :: [*]).
Each '[KnownList, ZipInstr] '[i, o] =>
((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 :: (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
$ ConstantScope (ToT a) =>
Instr
  (ToT a : 'TLambda ('TPair (ToT a) (ToT b)) (ToT c) : ToTs s)
  ('TLambda (ToT b) (ToT c) : ToTs s)
forall (a :: T) (b :: T) (c :: T) (s :: [T]).
(ConstantScope a, SingI b) =>
Instr (a : 'TLambda ('TPair a b) c : s) ('TLambda b c : s)
APPLY (ConstantScope (ToT a) =>
 Instr
   (ToT a : 'TLambda ('TPair (ToT a) (ToT b)) (ToT c) : ToTs s)
   ('TLambda (ToT b) (ToT c) : ToTs s))
-> (((SingI (ToT a), WellTyped (ToT a),
      FailOnOperationFound (ContainsOp (ToT a)),
      FailOnBigMapFound (ContainsBigMap (ToT a)),
      FailOnContractFound (ContainsContract (ToT a)),
      FailOnTicketFound (ContainsTicket (ToT a)),
      FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
     KnownValue a)
    :- ConstantScope (ToT a))
-> Instr
     (ToT a : 'TLambda ('TPair (ToT a) (ToT b)) (ToT c) : ToTs s)
     ('TLambda (ToT b) (ToT c) : ToTs s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((SingI (ToT a), WellTyped (ToT a),
  FailOnOperationFound (ContainsOp (ToT a)),
  FailOnBigMapFound (ContainsBigMap (ToT a)),
  FailOnContractFound (ContainsContract (ToT a)),
  FailOnTicketFound (ContainsTicket (ToT a)),
  FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
 KnownValue a)
:- ConstantScope (ToT a)
forall a. NiceConstant a :- ConstantScope (ToT a)
niceConstantEvi @a

-- | 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 : (a : b :-> c) : s :-> (b :-> c) : s
applicate :: (a : ((a : b) :-> c) : s) :-> ((b :-> c) : s)
applicate = Instr
  (ToTs (a : ((a : inp2nd : inpTail) :-> c) : s))
  (ToTs (((inp2nd : inpTail) :-> c) : s))
-> (a : ((a : inp2nd : inpTail) :-> c) : s)
   :-> (((inp2nd : inpTail) :-> c) : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr
  (ToTs (a : ((a : inp2nd : inpTail) :-> c) : s))
  (ToTs (((inp2nd : inpTail) :-> c) : s))
forall (a :: T) (b :: T) (c :: T) (s :: [T]).
(ConstantScope a, SingI b) =>
Instr (a : 'TLambda ('TPair a b) c : s) ('TLambda b c : s)
APPLY (ConstantScope (ToT a) =>
 (a : ((a : b) :-> c) : s) :-> ((b :-> c) : s))
-> (((SingI (ToT a), WellTyped (ToT a),
      FailOnOperationFound (ContainsOp (ToT a)),
      FailOnBigMapFound (ContainsBigMap (ToT a)),
      FailOnContractFound (ContainsContract (ToT a)),
      FailOnTicketFound (ContainsTicket (ToT a)),
      FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
     KnownValue a)
    :- ConstantScope (ToT a))
-> (a : ((a : b) :-> c) : s) :-> ((b :-> c) : s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((SingI (ToT a), WellTyped (ToT a),
  FailOnOperationFound (ContainsOp (ToT a)),
  FailOnBigMapFound (ContainsBigMap (ToT a)),
  FailOnContractFound (ContainsContract (ToT a)),
  FailOnTicketFound (ContainsTicket (ToT a)),
  FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
 KnownValue a)
:- ConstantScope (ToT a)
forall a. NiceConstant a :- ConstantScope (ToT a)
niceConstantEvi @a

dip :: forall a s s'. HasCallStack => (s :-> s') -> (a : s :-> a : s')
dip :: (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 :: (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 (ToTs s) (ToTs s') -> 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 (SingI n => PeanoNatural n
forall (n :: Peano). SingI n => PeanoNatural n
toPeanoNatural @n) Instr (ToTs s) (ToTs s')
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 :: (s :-> s') -> inp :-> out
dipN = forall (inp :: [*]) (out :: [*]) (s :: [*]) (s' :: [*]).
ConstraintDIPNLorentz (ToPeano n) inp out s s' =>
(s :-> s') -> inp :-> out
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 = ('[] :-> '[()])
-> '[Integer, Integer, Integer]
   :-> '[Integer, Integer, Integer, ()]
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 :: (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 (ConstantScope (ToT a) => (a : s) :-> t)
-> (((SingI (ToT a), WellTyped (ToT a),
      FailOnOperationFound (ContainsOp (ToT a)),
      FailOnBigMapFound (ContainsBigMap (ToT a)),
      FailOnContractFound (ContainsContract (ToT a)),
      FailOnTicketFound (ContainsTicket (ToT a)),
      FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
     KnownValue a)
    :- ConstantScope (ToT a))
-> (a : s) :-> t
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((SingI (ToT a), WellTyped (ToT a),
  FailOnOperationFound (ContainsOp (ToT a)),
  FailOnBigMapFound (ContainsBigMap (ToT a)),
  FailOnContractFound (ContainsContract (ToT a)),
  FailOnTicketFound (ContainsTicket (ToT a)),
  FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
 KnownValue a)
:- ConstantScope (ToT a)
forall a. NiceConstant a :- ConstantScope (ToT a)
niceConstantEvi @a

cast :: KnownValue a => (a : s :-> a : s)
cast :: (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 (a :: T) (s :: [T]). SingI a => Instr (a : s) (a : s)
CAST

pack
  :: forall a s. (NicePackedValue a)
  => a : s :-> Packed a : s
pack :: (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
$ PackedValScope (ToT a) => Instr (ToT a : ToTs s) ('TBytes : ToTs s)
forall (a :: T) (s :: [T]).
PackedValScope a =>
Instr (a : s) ('TBytes : s)
PACK (PackedValScope (ToT a) =>
 Instr (ToT a : ToTs s) ('TBytes : ToTs s))
-> (((SingI (ToT a), WellTyped (ToT a),
      FailOnOperationFound (ContainsOp (ToT a)),
      FailOnBigMapFound (ContainsBigMap (ToT a)),
      FailOnTicketFound (ContainsTicket (ToT a)),
      FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
     KnownValue a)
    :- PackedValScope (ToT a))
-> Instr (ToT a : ToTs s) ('TBytes : ToTs s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((SingI (ToT a), WellTyped (ToT a),
  FailOnOperationFound (ContainsOp (ToT a)),
  FailOnBigMapFound (ContainsBigMap (ToT a)),
  FailOnTicketFound (ContainsTicket (ToT a)),
  FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
 KnownValue a)
:- PackedValScope (ToT a)
forall a. NicePackedValue a :- PackedValScope (ToT a)
nicePackedValueEvi @a

unpack
  :: forall a s. (NiceUnpackedValue a)
  => Packed a : s :-> Maybe a : s
unpack :: (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
$ UnpackedValScope (ToT a) =>
Instr ('TBytes : ToTs s) ('TOption (ToT a) : ToTs s)
forall (a :: T) (s :: [T]).
(UnpackedValScope a, SingI a) =>
Instr ('TBytes : s) ('TOption a : s)
UNPACK (UnpackedValScope (ToT a) =>
 Instr ('TBytes : ToTs s) ('TOption (ToT a) : ToTs s))
-> ((((SingI (ToT a), WellTyped (ToT a),
       FailOnOperationFound (ContainsOp (ToT a)),
       FailOnBigMapFound (ContainsBigMap (ToT a)),
       FailOnTicketFound (ContainsTicket (ToT a)),
       FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
      (SingI (ToT a), WellTyped (ToT a),
       FailOnOperationFound (ContainsOp (ToT a)),
       FailOnBigMapFound (ContainsBigMap (ToT a)),
       FailOnContractFound (ContainsContract (ToT a)),
       FailOnTicketFound (ContainsTicket (ToT a)),
       FailOnSaplingStateFound (ContainsSaplingState (ToT a)))),
     KnownValue a)
    :- UnpackedValScope (ToT a))
-> Instr ('TBytes : ToTs s) ('TOption (ToT a) : ToTs s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (((SingI (ToT a), WellTyped (ToT a),
   FailOnOperationFound (ContainsOp (ToT a)),
   FailOnBigMapFound (ContainsBigMap (ToT a)),
   FailOnTicketFound (ContainsTicket (ToT a)),
   FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
  (SingI (ToT a), WellTyped (ToT a),
   FailOnOperationFound (ContainsOp (ToT a)),
   FailOnBigMapFound (ContainsBigMap (ToT a)),
   FailOnContractFound (ContainsContract (ToT a)),
   FailOnTicketFound (ContainsTicket (ToT a)),
   FailOnSaplingStateFound (ContainsSaplingState (ToT a)))),
 KnownValue a)
:- UnpackedValScope (ToT a)
forall a. NiceUnpackedValue a :- UnpackedValScope (ToT a)
niceUnpackedValueEvi @a

packRaw
  :: forall a s. (NicePackedValue a)
  => a : s :-> ByteString : s
packRaw :: (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
$ PackedValScope (ToT a) => Instr (ToT a : ToTs s) ('TBytes : ToTs s)
forall (a :: T) (s :: [T]).
PackedValScope a =>
Instr (a : s) ('TBytes : s)
PACK (PackedValScope (ToT a) =>
 Instr (ToT a : ToTs s) ('TBytes : ToTs s))
-> (((SingI (ToT a), WellTyped (ToT a),
      FailOnOperationFound (ContainsOp (ToT a)),
      FailOnBigMapFound (ContainsBigMap (ToT a)),
      FailOnTicketFound (ContainsTicket (ToT a)),
      FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
     KnownValue a)
    :- PackedValScope (ToT a))
-> Instr (ToT a : ToTs s) ('TBytes : ToTs s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((SingI (ToT a), WellTyped (ToT a),
  FailOnOperationFound (ContainsOp (ToT a)),
  FailOnBigMapFound (ContainsBigMap (ToT a)),
  FailOnTicketFound (ContainsTicket (ToT a)),
  FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
 KnownValue a)
:- PackedValScope (ToT a)
forall a. NicePackedValue a :- PackedValScope (ToT a)
nicePackedValueEvi @a

unpackRaw
  :: forall a s. (NiceUnpackedValue a)
  => ByteString : s :-> Maybe a : s
unpackRaw :: (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
$ UnpackedValScope (ToT a) =>
Instr ('TBytes : ToTs s) ('TOption (ToT a) : ToTs s)
forall (a :: T) (s :: [T]).
(UnpackedValScope a, SingI a) =>
Instr ('TBytes : s) ('TOption a : s)
UNPACK (UnpackedValScope (ToT a) =>
 Instr ('TBytes : ToTs s) ('TOption (ToT a) : ToTs s))
-> ((((SingI (ToT a), WellTyped (ToT a),
       FailOnOperationFound (ContainsOp (ToT a)),
       FailOnBigMapFound (ContainsBigMap (ToT a)),
       FailOnTicketFound (ContainsTicket (ToT a)),
       FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
      (SingI (ToT a), WellTyped (ToT a),
       FailOnOperationFound (ContainsOp (ToT a)),
       FailOnBigMapFound (ContainsBigMap (ToT a)),
       FailOnContractFound (ContainsContract (ToT a)),
       FailOnTicketFound (ContainsTicket (ToT a)),
       FailOnSaplingStateFound (ContainsSaplingState (ToT a)))),
     KnownValue a)
    :- UnpackedValScope (ToT a))
-> Instr ('TBytes : ToTs s) ('TOption (ToT a) : ToTs s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (((SingI (ToT a), WellTyped (ToT a),
   FailOnOperationFound (ContainsOp (ToT a)),
   FailOnBigMapFound (ContainsBigMap (ToT a)),
   FailOnTicketFound (ContainsTicket (ToT a)),
   FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
  (SingI (ToT a), WellTyped (ToT a),
   FailOnOperationFound (ContainsOp (ToT a)),
   FailOnBigMapFound (ContainsBigMap (ToT a)),
   FailOnContractFound (ContainsContract (ToT a)),
   FailOnTicketFound (ContainsTicket (ToT a)),
   FailOnSaplingStateFound (ContainsSaplingState (ToT a)))),
 KnownValue a)
:- UnpackedValScope (ToT a)
forall a. NiceUnpackedValue a :- UnpackedValScope (ToT a)
niceUnpackedValueEvi @a

concat :: ConcatOpHs c => c : c : s :-> c : s
concat :: (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 (c :: T) (s :: [T]). ConcatOp c => Instr (c : c : s) (c : s)
CONCAT

concat' :: ConcatOpHs c => List c : s :-> c : s
concat' :: (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 (c :: T) (s :: [T]).
ConcatOp c =>
Instr ('TList c : s) (c : s)
CONCAT'

slice
  :: (SliceOpHs c, KnownValue c)
  => Natural : Natural : c : s :-> Maybe c : s
slice :: (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 (c :: T) (s :: [T]).
(SliceOp c, SingI c) =>
Instr ('TNat : 'TNat : c : s) ('TOption c : s)
SLICE

isNat :: Integer : s :-> Maybe Natural : s
isNat :: (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 (s :: [T]). Instr ('TInt : s) ('TOption 'TNat : s)
ISNAT

add
  :: ArithOpHs Add n m r
  => n : m : s :-> r : s
add :: (n : m : s) :-> (r : s)
add = forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
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 :: (n : m : s) :-> (r : s)
sub = forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
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 :: (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 :: (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 (s :: [T]).
Instr ('TMutez : 'TMutez : s) ('TOption 'TMutez : s)
SUB_MUTEZ

rsubMutez :: Mutez : Mutez : s :-> Maybe Mutez : s
rsubMutez :: (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 :: (n : m : s) :-> (r : s)
mul = forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
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 :: (n : m : s) :-> (r : s)
ediv = forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
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 :: (n : s) :-> (UnaryArithResHs Abs n : s)
abs = forall n (s :: [*]).
UnaryArithOpHs Abs n =>
(n : s) :-> (UnaryArithResHs Abs n : s)
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 :: (n : s) :-> (UnaryArithResHs Neg n : s)
neg = forall n (s :: [*]).
UnaryArithOpHs Neg n =>
(n : s) :-> (UnaryArithResHs Neg n : s)
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 :: (n : m : s) :-> (r : s)
lsl = forall n m r (s :: [*]).
ArithOpHs Lsl n m r =>
(n : m : s) :-> (r : s)
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 :: (n : m : s) :-> (r : s)
lsr = forall n m r (s :: [*]).
ArithOpHs Lsr n m r =>
(n : m : s) :-> (r : s)
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 :: (n : m : s) :-> (r : s)
or = forall n m r (s :: [*]).
ArithOpHs Or n m r =>
(n : m : s) :-> (r : s)
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 :: (n : m : s) :-> (r : s)
and = forall n m r (s :: [*]).
ArithOpHs And n m r =>
(n : m : s) :-> (r : s)
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 :: (n : m : s) :-> (r : s)
xor = forall n m r (s :: [*]).
ArithOpHs Xor n m r =>
(n : m : s) :-> (r : s)
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 :: (n : s) :-> (UnaryArithResHs Not n : s)
not = forall n (s :: [*]).
UnaryArithOpHs Not n =>
(n : s) :-> (UnaryArithResHs Not n : s)
forall aop n (s :: [*]).
UnaryArithOpHs aop n =>
(n : s) :-> (UnaryArithResHs aop n : s)
evalUnaryArithOpHs @Not

compare :: NiceComparable n => n : n : s :-> Integer : s
compare :: (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 (n :: T) (s :: [T]).
(Comparable n, SingI n) =>
Instr (n : n : s) ('TInt : s)
COMPARE

eq0 :: UnaryArithOpHs Eq' n => n : s :-> UnaryArithResHs Eq' n : s
eq0 :: (n : s) :-> (UnaryArithResHs Eq' n : s)
eq0 = forall n (s :: [*]).
UnaryArithOpHs Eq' n =>
(n : s) :-> (UnaryArithResHs Eq' n : s)
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 :: (n : s) :-> (UnaryArithResHs Neq n : s)
neq0 = forall n (s :: [*]).
UnaryArithOpHs Neq n =>
(n : s) :-> (UnaryArithResHs Neq n : s)
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 :: (n : s) :-> (UnaryArithResHs Lt n : s)
lt0 = forall n (s :: [*]).
UnaryArithOpHs Lt n =>
(n : s) :-> (UnaryArithResHs Lt n : s)
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 :: (n : s) :-> (UnaryArithResHs Gt n : s)
gt0 = forall n (s :: [*]).
UnaryArithOpHs Gt n =>
(n : s) :-> (UnaryArithResHs Gt n : s)
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 :: (n : s) :-> (UnaryArithResHs Le n : s)
le0 = forall n (s :: [*]).
UnaryArithOpHs Le n =>
(n : s) :-> (UnaryArithResHs Le n : s)
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 :: (n : s) :-> (UnaryArithResHs Ge n : s)
ge0 = forall n (s :: [*]).
UnaryArithOpHs Ge n =>
(n : s) :-> (UnaryArithResHs Ge n : s)
forall aop n (s :: [*]).
UnaryArithOpHs aop n =>
(n : s) :-> (UnaryArithResHs aop n : s)
evalUnaryArithOpHs @Ge

int :: (ToIntegerArithOpHs i) => i : s :-> Integer : s
int :: (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' :: (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
-> Notes (ToT ret)
-> Instr
     (ToT arg : 'TAddress : ToTs s) ('TOption (ToT ret) : ToTs s)
forall (arg :: T) (ret :: T) (s :: [T]).
(SingI arg, ViewableScope ret) =>
ViewName
-> Notes ret -> Instr (arg : 'TAddress : s) ('TOption ret : s)
VIEW ((KnownSymbol name, HasCallStack) => ViewName
forall (name :: Symbol).
(KnownSymbol name, HasCallStack) =>
ViewName
demoteViewName @name) Notes (ToT ret)
forall (t :: T). SingI t => Notes t
starNotes
  (ViewableScope (ToT ret) =>
 Instr (ToT arg : 'TAddress : ToTs s) ('TOption (ToT ret) : ToTs s))
-> (((SingI (ToT ret), FailOnOperationFound (ContainsOp (ToT ret)),
      FailOnBigMapFound (ContainsBigMap (ToT ret)),
      FailOnTicketFound (ContainsTicket (ToT ret))),
     KnownValue ret)
    :- ViewableScope (ToT ret))
-> Instr
     (ToT arg : 'TAddress : ToTs s) ('TOption (ToT ret) : ToTs s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((SingI (ToT ret), FailOnOperationFound (ContainsOp (ToT ret)),
  FailOnBigMapFound (ContainsBigMap (ToT ret)),
  FailOnTicketFound (ContainsTicket (ToT ret))),
 KnownValue ret)
:- ViewableScope (ToT ret)
forall a. NiceViewable a :- ViewableScope (ToT a)
niceViewableEvi @ret

-- | 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)
  => s :-> ContractRef p : s
self :: 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 (arg :: T) (inp :: [T]).
ParameterScope arg =>
SomeEntrypointCallT arg -> Instr inp ('TContract arg : inp)
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
$ (NiceParameter p, ForbidExplicitDefaultEntrypoint p) =>
SomeEntrypointCallT (ToT p)
forall cp.
(NiceParameter cp, ForbidExplicitDefaultEntrypoint cp) =>
SomeEntrypointCall cp
sepcCallRootChecked @p) (ParameterScope (ToT p) => s :-> (ContractRef p : s))
-> (NiceParameter p :- ParameterScope (ToT p))
-> s :-> (ContractRef p : s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ NiceParameter p :- ParameterScope (ToT p)
forall a. NiceParameter a :- ParameterScope (ToT a)
niceParameterEvi @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)
  => EntrypointRef mname
  -> s :-> ContractRef (GetEntrypointArgCustom p mname) : s
selfCalling :: 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
$
  (((SingI (ToT p), WellTyped (ToT p),
   FailOnOperationFound (ContainsOp (ToT p)),
   FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT p))),
  KnownValue p)
 :- ParameterScope (ToT p))
-> (ParameterScope (ToT p) =>
    Instr
      (ToTs s)
      ('TContract (ToT (GetEntrypointArgCustom p mname)) : ToTs s))
-> Instr
     (ToTs s)
     ('TContract (ToT (GetEntrypointArgCustom p mname)) : ToTs s)
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (((SingI (ToT p), WellTyped (ToT p),
  FailOnOperationFound (ContainsOp (ToT p)),
  FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT p))),
 KnownValue p)
:- ParameterScope (ToT p)
forall a. NiceParameter a :- ParameterScope (ToT a)
niceParameterEvi @p) ((ParameterScope (ToT p) =>
  Instr
    (ToTs s)
    ('TContract (ToT (GetEntrypointArgCustom p mname)) : ToTs s))
 -> Instr
      (ToTs s)
      ('TContract (ToT (GetEntrypointArgCustom p mname)) : ToTs s))
-> (ParameterScope (ToT p) =>
    Instr
      (ToTs s)
      ('TContract (ToT (GetEntrypointArgCustom p mname)) : ToTs s))
-> Instr
     (ToTs s)
     ('TContract (ToT (GetEntrypointArgCustom p mname)) : ToTs s)
forall a b. (a -> b) -> a -> b
$
  case EntrypointRef mname
-> EntrypointCall p (GetEntrypointArgCustom p mname)
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 (arg :: T) (inp :: [T]).
ParameterScope arg =>
SomeEntrypointCallT arg -> Instr inp ('TContract arg : inp)
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 :: (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 (Notes (ToT p)
-> EpName
-> Instr
     ('TAddress : ToTs s) ('TOption ('TContract (ToT p)) : ToTs s)
forall (p :: T) (s :: [T]).
ParameterScope p =>
Notes p
-> EpName -> Instr ('TAddress : s) ('TOption ('TContract p) : s)
CONTRACT Notes (ToT p)
forall (t :: T). SingI t => Notes t
starNotes EpName
epName) (ParameterScope (ToT p) =>
 (addr : s) :-> (Maybe (ContractRef p) : s))
-> (((SingI (ToT p), WellTyped (ToT p),
      FailOnOperationFound (ContainsOp (ToT p)),
      FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT p))),
     KnownValue p)
    :- ParameterScope (ToT p))
-> (addr : s) :-> (Maybe (ContractRef p) : s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((SingI (ToT p), WellTyped (ToT p),
  FailOnOperationFound (ContainsOp (ToT p)),
  FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT p))),
 KnownValue p)
:- ParameterScope (ToT p)
forall a. NiceParameter a :- ParameterScope (ToT a)
niceParameterEvi @p
  where
    epName :: EpName
epName = SomeEntrypointCallT (ToT p) -> EpName
forall (arg :: T). SomeEntrypointCallT arg -> EpName
sepcName ((((SingI (ToT p), WellTyped (ToT p),
   FailOnOperationFound (ContainsOp (ToT p)),
   FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT p))),
  KnownValue p),
 ForbidExplicitDefaultEntrypoint p) =>
SomeEntrypointCallT (ToT p)
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 :: 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 epRef -> (Dict (ParameterScope (ToT epArg)), EpName)
forall k (cp :: k) 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) -> Notes (ToT epArg)
-> EpName
-> Instr
     ('TAddress : ToTs s) ('TOption ('TContract (ToT epArg)) : ToTs s)
forall (p :: T) (s :: [T]).
ParameterScope p =>
Notes p
-> EpName -> Instr ('TAddress : s) ('TOption ('TContract p) : s)
CONTRACT Notes (ToT epArg)
forall (t :: T). SingI t => Notes t
starNotes 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 :: 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 :: (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 :: (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 (Notes (ToT p)
-> EpName
-> Instr
     ('TAddress : ToTs s) ('TOption ('TContract (ToT p)) : ToTs s)
forall (p :: T) (s :: [T]).
ParameterScope p =>
Notes p
-> EpName -> Instr ('TAddress : s) ('TOption ('TContract p) : s)
CONTRACT Notes (ToT p)
forall (t :: T). SingI t => Notes t
starNotes EpName
DefEpName) (ParameterScope (ToT p) =>
 (EpAddress : s) :-> (Maybe (ContractRef p) : s))
-> (((SingI (ToT p), WellTyped (ToT p),
      FailOnOperationFound (ContainsOp (ToT p)),
      FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT p))),
     KnownValue p)
    :- ParameterScope (ToT p))
-> (EpAddress : s) :-> (Maybe (ContractRef p) : s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((SingI (ToT p), WellTyped (ToT p),
  FailOnOperationFound (ContainsOp (ToT p)),
  FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT p))),
 KnownValue p)
:- ParameterScope (ToT p)
forall a. NiceParameter a :- ParameterScope (ToT a)
niceParameterEvi @p

transferTokens
  :: forall p s. (NiceParameter p)
  => p : Mutez : ContractRef p : s :-> Operation : s
transferTokens :: (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))
 -> (p : Mutez : ContractRef p : s) :-> (Operation : s))
-> Instr
     (ToTs (p : Mutez : ContractRef p : s)) (ToTs (Operation : s))
-> (p : Mutez : ContractRef p : s) :-> (Operation : s)
forall a b. (a -> b) -> a -> b
$ ParameterScope (ToT p) =>
Instr
  (ToT p : 'TMutez : 'TContract (ToT p) : ToTs s)
  ('TOperation : ToTs s)
forall (p :: T) (s :: [T]).
ParameterScope p =>
Instr (p : 'TMutez : 'TContract p : s) ('TOperation : s)
TRANSFER_TOKENS (ParameterScope (ToT p) =>
 Instr
   (ToT p : 'TMutez : 'TContract (ToT p) : ToTs s)
   ('TOperation : ToTs s))
-> (((SingI (ToT p), WellTyped (ToT p),
      FailOnOperationFound (ContainsOp (ToT p)),
      FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT p))),
     KnownValue p)
    :- ParameterScope (ToT p))
-> Instr
     (ToT p : 'TMutez : 'TContract (ToT p) : ToTs s)
     ('TOperation : ToTs s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((SingI (ToT p), WellTyped (ToT p),
  FailOnOperationFound (ContainsOp (ToT p)),
  FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT p))),
 KnownValue p)
:- ParameterScope (ToT p)
forall a. NiceParameter a :- ParameterScope (ToT a)
niceParameterEvi @p

setDelegate :: Maybe KeyHash : s :-> Operation : s
setDelegate :: (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 (s :: [T]). Instr ('TOption 'TKeyHash : s) ('TOperation : s)
SET_DELEGATE

createContract
  :: forall p g vd s. Contract p g vd
  -> Maybe KeyHash : Mutez : g : s
  :-> Operation : TAddress p vd : s
createContract :: 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 (Instr
   (ToTs (Maybe KeyHash : Mutez : g : s))
   (ToTs (Operation : TAddress p vd : s))
 -> (Maybe KeyHash : Mutez : g : s)
    :-> (Operation : TAddress p vd : s))
-> Instr
     (ToTs (Maybe KeyHash : Mutez : g : s))
     (ToTs (Operation : TAddress p vd : s))
-> (Maybe KeyHash : Mutez : g : s)
   :-> (Operation : TAddress p vd : s)
forall a b. (a -> b) -> a -> b
$ Contract' Instr (ToT p) (ToT g)
-> Instr
     ('TOption 'TKeyHash : 'TMutez : ToT g : ToTs s)
     ('TOperation : 'TAddress : ToTs s)
forall (p :: T) (g :: T) (s :: [T]).
(ParameterScope p, StorageScope g) =>
Contract' Instr p g
-> Instr
     ('TOption 'TKeyHash : 'TMutez : g : s)
     ('TOperation : 'TAddress : s)
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)
    (ParameterScope (ToT p) =>
 Instr
   ('TOption 'TKeyHash : 'TMutez : ToT g : ToTs s)
   ('TOperation : 'TAddress : ToTs s))
-> (((SingI (ToT p), WellTyped (ToT p),
      FailOnOperationFound (ContainsOp (ToT p)),
      FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT p))),
     KnownValue p)
    :- ParameterScope (ToT p))
-> Instr
     ('TOption 'TKeyHash : 'TMutez : ToT g : ToTs s)
     ('TOperation : 'TAddress : ToTs s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((SingI (ToT p), WellTyped (ToT p),
  FailOnOperationFound (ContainsOp (ToT p)),
  FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT p))),
 KnownValue p)
:- ParameterScope (ToT p)
forall a. NiceParameter a :- ParameterScope (ToT a)
niceParameterEvi @p
    (StorageScope (ToT g) =>
 Instr
   ('TOption 'TKeyHash : 'TMutez : ToT g : ToTs s)
   ('TOperation : 'TAddress : ToTs s))
-> (((SingI (ToT g), WellTyped (ToT g),
      FailOnOperationFound (ContainsOp (ToT g)),
      FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT g)),
      FailOnContractFound (ContainsContract (ToT g))),
     KnownValue g)
    :- StorageScope (ToT g))
-> Instr
     ('TOption 'TKeyHash : 'TMutez : ToT g : ToTs s)
     ('TOperation : 'TAddress : ToTs s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((SingI (ToT g), WellTyped (ToT g),
  FailOnOperationFound (ContainsOp (ToT g)),
  FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT g)),
  FailOnContractFound (ContainsContract (ToT g))),
 KnownValue g)
:- StorageScope (ToT g)
forall a. NiceStorage a :- StorageScope (ToT a)
niceStorageEvi @g

implicitAccount :: KeyHash : s :-> ContractRef () : s
implicitAccount :: (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 (s :: [T]). Instr ('TKeyHash : s) ('TContract 'TUnit : s)
IMPLICIT_ACCOUNT

now :: s :-> Timestamp : s
now :: 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]). Instr inp ('TTimestamp : inp)
NOW

amount :: s :-> Mutez : s
amount :: 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]). Instr inp ('TMutez : inp)
AMOUNT

balance :: s :-> Mutez : s
balance :: 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]). Instr inp ('TMutez : inp)
BALANCE

votingPower :: KeyHash : s :-> Natural : s
votingPower :: (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 (s :: [T]). Instr ('TKeyHash : s) ('TNat : s)
VOTING_POWER

totalVotingPower :: s :-> Natural : s
totalVotingPower :: 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]). Instr inp ('TNat : inp)
TOTAL_VOTING_POWER

checkSignature :: BytesLike bs => PublicKey : TSignature bs : bs : s :-> Bool : s
checkSignature :: (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 (s :: [T]).
Instr ('TKey : 'TSignature : 'TBytes : s) ('TBool : s)
CHECK_SIGNATURE

sha256 :: BytesLike bs => bs : s :-> Hash Sha256 bs : s
sha256 :: (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 (s :: [T]). Instr ('TBytes : s) ('TBytes : s)
SHA256

sha512 :: BytesLike bs => bs : s :-> Hash Sha512 bs : s
sha512 :: (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 (s :: [T]). Instr ('TBytes : s) ('TBytes : s)
SHA512

blake2B :: BytesLike bs => bs : s :-> Hash Blake2b bs : s
blake2B :: (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 (s :: [T]). Instr ('TBytes : s) ('TBytes : s)
BLAKE2B

sha3 :: BytesLike bs => bs : s :-> Hash Sha3 bs : s
sha3 :: (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 (s :: [T]). Instr ('TBytes : s) ('TBytes : s)
SHA3

keccak :: BytesLike bs => bs : s :-> Hash Keccak bs : s
keccak :: (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 (s :: [T]). Instr ('TBytes : s) ('TBytes : s)
KECCAK

hashKey :: PublicKey : s :-> KeyHash : s
hashKey :: (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 (s :: [T]). Instr ('TKey : s) ('TKeyHash : s)
HASH_KEY

pairingCheck :: [(Bls12381G1, Bls12381G2)] : s :-> Bool : s
pairingCheck :: ([(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 (s :: [T]).
Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : s) ('TBool : s)
PAIRING_CHECK

{-# WARNING source
    "Using `source` is considered a bad practice.\n\
\    Consider using `sender` instead until further investigation" #-}
source :: s :-> Address : s
source :: 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]). Instr inp ('TAddress : inp)
SOURCE

sender :: s :-> Address : s
sender :: 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]). Instr inp ('TAddress : inp)
SENDER

address :: ContractRef a : s :-> Address : s
address :: (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 (a :: T) (s :: [T]).
Instr ('TContract a : s) ('TAddress : s)
ADDRESS

chainId :: s :-> ChainId : s
chainId :: 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]). Instr inp ('TChainId : inp)
CHAIN_ID

level :: s :-> Natural : s
level :: 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]). Instr inp ('TNat : inp)
LEVEL

selfAddress :: s :-> Address : s
selfAddress :: 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]). Instr inp ('TAddress : inp)
SELF_ADDRESS

never :: Never : s :-> s'
never :: (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 :-> Ticket a : s
ticket :: (a : Natural : s) :-> (Ticket a : s)
ticket = Instr (ToTs (a : Natural : s)) (ToTs (Ticket a : s))
-> (a : Natural : s) :-> (Ticket a : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (a : Natural : s)) (ToTs (Ticket a : s))
forall (a :: T) (s :: [T]).
Comparable a =>
Instr (a : 'TNat : s) ('TTicket a : s)
TICKET

-- | Note: for more advanced helpers for tickets see "Lorentz.Tickets" module.
readTicket :: Ticket a : s :-> ReadTicket a : Ticket a : s
readTicket :: (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 (a :: T) (s :: [T]).
Instr
  ('TTicket a : s)
  (RightComb '[ 'TAddress, a, 'TNat] : 'TTicket a : s)
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 :: (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 (a :: T) (s :: [T]).
Instr
  ('TTicket a : 'TPair 'TNat 'TNat : s)
  ('TOption ('TPair ('TTicket a) ('TTicket a)) : s)
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 :: (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 (a :: T) (s :: [T]).
Instr
  ('TTicket a : 'TPair 'TNat 'TNat : s)
  ('TOption ('TPair ('TTicket a) ('TTicket a)) : s)
SPLIT_TICKET

-- | Note: for more advanced helpers for tickets see "Lorentz.Tickets" module.
joinTickets :: (Ticket a, Ticket a) : s :-> Maybe (Ticket a) : s
joinTickets :: ((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 (a :: T) (s :: [T]).
Instr
  ('TPair ('TTicket a) ('TTicket a) : s) ('TOption ('TTicket a) : s)
JOIN_TICKETS

openChest :: ChestKey : Chest : Natural : s :-> OpenChest : s
openChest :: (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 (s :: [T]).
Instr ('TChestKey : 'TChest : 'TNat : s) ('TOr 'TBytes 'TBool : s)
OPEN_CHEST

-- | Execute given instruction on truncated stack.
--
-- This instruction requires you to specify the piece of stack to truncate
-- as type argument.
framed
  :: forall s i o.
      (KnownList i, KnownList o)
  => (i :-> o) -> ((i ++ s) :-> (o ++ s))
framed :: (i :-> o) -> (i ++ s) :-> (o ++ s)
framed ((i :-> o) -> Instr (ToTs i) (ToTs o)
forall (inp :: [*]) (out :: [*]).
HasCallStack =>
(inp :-> out) -> Instr (ToTs inp) (ToTs out)
iNonFailingCode -> Instr (ToTs i) (ToTs o)
i) =
  Instr (ToTs (i ++ s)) (ToTs (o ++ s)) -> (i ++ s) :-> (o ++ s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs (i ++ s)) (ToTs (o ++ s)) -> (i ++ s) :-> (o ++ s))
-> Instr (ToTs (i ++ s)) (ToTs (o ++ s)) -> (i ++ s) :-> (o ++ s)
forall a b. (a -> b) -> a -> b
$ Proxy (ToTs s)
-> Instr (ToTs i) (ToTs o)
-> Instr (ToTs i ++ ToTs s) (ToTs o ++ ToTs s)
forall (a :: [T]) (b :: [T]) (s :: [T]).
(KnownList a, KnownList b) =>
Proxy s -> Instr a b -> Instr (a ++ s) (b ++ s)
FrameInstr (Proxy (ToTs s)
forall k (t :: k). Proxy t
Proxy @(ToTs s)) Instr (ToTs i) (ToTs o)
i
    (KnownList (ToTs i) => Instr (ToTs (i ++ s)) (ToTs (o ++ s)))
-> (KnownList i :- KnownList (ToTs i))
-> Instr (ToTs (i ++ s)) (ToTs (o ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ KnownList i :- KnownList (ToTs i)
forall (s :: [*]). KnownList s :- KnownList (ToTs s)
totsKnownLemma @i
    (KnownList (ToTs o) => Instr (ToTs (i ++ s)) (ToTs (o ++ s)))
-> (KnownList o :- KnownList (ToTs o))
-> Instr (ToTs (i ++ s)) (ToTs (o ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ KnownList o :- KnownList (ToTs o)
forall (s :: [*]). KnownList s :- KnownList (ToTs s)
totsKnownLemma @o
    ((ToTs (i ++ s) ~ (ToTs i ++ ToTs s)) =>
 Instr (ToTs (i ++ s)) (ToTs (o ++ s)))
-> Dict (ToTs (i ++ s) ~ (ToTs i ++ ToTs s))
-> Instr (ToTs (i ++ s)) (ToTs (o ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ KnownList i => Dict (ToTs (i ++ s) ~ (ToTs i ++ ToTs s))
forall (a :: [*]) (b :: [*]).
KnownList a =>
Dict (ToTs (a ++ b) ~ (ToTs a ++ ToTs b))
totsAppendLemma @i @s
    ((ToTs (o ++ s) ~ (ToTs o ++ ToTs s)) =>
 Instr (ToTs (i ++ s)) (ToTs (o ++ s)))
-> Dict (ToTs (o ++ s) ~ (ToTs o ++ ToTs s))
-> Instr (ToTs (i ++ s)) (ToTs (o ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ KnownList o => Dict (ToTs (o ++ s) ~ (ToTs o ++ ToTs s))
forall (a :: [*]) (b :: [*]).
KnownList a =>
Dict (ToTs (a ++ b) ~ (ToTs a ++ ToTs b))
totsAppendLemma @o @s

----------------------------------------------------------------------------
-- 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 (s0 :: [*]). (k : s0) :-> (e : s0)) -> st :-> st
failingWhenPresent forall (s0 :: [*]). (k : s0) :-> (e : s0)
mkErr =
  forall a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano 3) inp out a, Dupable a) =>
inp :-> out
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 a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano 2) inp out a, Dupable a) =>
inp :-> out
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 (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) where
  lmap :: KnownValue b => (a : s :-> b : s) -> (c a : s :-> c b : s)

instance LorentzFunctor Maybe where
  lmap :: ((a : s) :-> (b : s)) -> (Maybe a : s) :-> (Maybe b : s)
lmap (a : s) :-> (b : s)
f = (s :-> (Maybe b : s))
-> ((a : s) :-> (Maybe b : s)) -> (Maybe a : s) :-> (Maybe b : s)
forall (s :: [*]) (s' :: [*]) a.
(s :-> s') -> ((a : s) :-> s') -> (Maybe a : s) :-> s'
ifNone s :-> (Maybe b : s)
forall a (s :: [*]). KnownValue a => s :-> (Maybe a : s)
none ((a : s) :-> (b : s)
f ((a : s) :-> (b : s))
-> ((b : s) :-> (Maybe b : s)) -> (a : s) :-> (Maybe b : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (b : s) :-> (Maybe b : s)
forall a (s :: [*]). (a : s) :-> (Maybe a : s)
some)