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

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

module Lorentz.Instr
  ( nop
  , justComment
  , comment
  , commentAroundFun
  , commentAroundStmt
  , 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
  , neg
  , lsl
  , lsr
  , or
  , and
  , xor
  , not
  , compare
  , eq0
  , neq0
  , lt0
  , gt0
  , le0
  , ge0
  , int
  , toTAddress_
  , 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
  , joinTickets
  , chainId
  , level
  , never
  , framed
  , LorentzFunctor (..)
  , NonZero (..)
  ) where

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

import Data.Constraint ((\\))
import qualified GHC.TypeNats as GHC (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.Zip
import Michelson.Typed
  (CommentType(..), ConstraintDIG, ConstraintDIG', ConstraintDIPN, ConstraintDIPN', ConstraintDUG,
  ConstraintDUG', ConstraintDUPN, ConstraintDUPN', ConstraintGetN, ConstraintUpdateN,
  EntrypointCallT(..), ExtInstr(..), GetN, Instr(..), SingI, RemFail(..), SomeEntrypointCallT(..), UpdateN,
  Value'(..), pattern CAR, pattern CDR, pattern LEFT, pattern PAIR, pattern RIGHT, pattern UNPAIR,
  sepcName, starNotes)
import Michelson.Typed.Arith
import Michelson.Typed.Haskell.Value
import Util.Peano
import Util.PeanoNatural
import Util.Type

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

justComment :: Text -> s :-> s
justComment :: Text -> s :-> s
justComment = CommentType -> s :-> s
forall (s :: [*]). CommentType -> s :-> s
comment (CommentType -> s :-> s)
-> (Text -> CommentType) -> Text -> s :-> s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> CommentType
JustComment

comment :: CommentType -> s :-> s
comment :: CommentType -> s :-> s
comment = Instr (ToTs s) (ToTs s) -> s :-> s
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs s) (ToTs s) -> s :-> s)
-> (CommentType -> Instr (ToTs s) (ToTs s))
-> CommentType
-> s :-> s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtInstr (ToTs s) -> Instr (ToTs s) (ToTs s)
forall (inp :: [T]). ExtInstr inp -> Instr inp inp
Ext (ExtInstr (ToTs s) -> Instr (ToTs s) (ToTs s))
-> (CommentType -> ExtInstr (ToTs s))
-> CommentType
-> Instr (ToTs s) (ToTs s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommentType -> ExtInstr (ToTs s)
forall (s :: [T]). CommentType -> ExtInstr s
COMMENT_ITEM

commentAroundFun :: Text -> (i :-> o) -> (i :-> o)
commentAroundFun :: Text -> (i :-> o) -> i :-> o
commentAroundFun Text
funName i :-> o
funBody =
  CommentType -> i :-> i
forall (s :: [*]). CommentType -> s :-> s
comment (Text -> CommentType
FunctionStarts Text
funName) (i :-> i) -> (i :-> o) -> i :-> o
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  i :-> o
funBody (i :-> o) -> (o :-> o) -> i :-> o
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  CommentType -> o :-> o
forall (s :: [*]). CommentType -> s :-> s
comment (Text -> CommentType
FunctionEnds Text
funName)

commentAroundStmt :: Text -> (i :-> o) -> (i :-> o)
commentAroundStmt :: Text -> (i :-> o) -> i :-> o
commentAroundStmt Text
stmtName i :-> o
stmtBody =
  CommentType -> i :-> i
forall (s :: [*]). CommentType -> s :-> s
comment (Text -> CommentType
StatementStarts Text
stmtName) (i :-> i) -> (i :-> o) -> i :-> o
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  i :-> o
stmtBody (i :-> o) -> (o :-> o) -> i :-> o
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  CommentType -> o :-> o
forall (s :: [*]). CommentType -> s :-> s
comment (Text -> CommentType
StatementEnds Text
stmtName)


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 :: GHC.Nat) (s :: [Type]).
  -- Note: if we introduce `nPeano ~ ToPeano n` variable,
  -- GHC will complain that this constraint is redundant.
  ( SingI (ToPeano 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, NFData (Sing 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
$ SingI (ToPeano n) => PeanoNatural (ToPeano n)
forall (n :: Nat). SingI (ToPeano n) => PeanoNatural (ToPeano n)
toPeanoNatural' @n
  where
    _example :: '[ Integer, Integer, Integer ] :-> '[]
    _example :: '[Integer, Integer, Integer] :-> '[]
_example = forall (s :: [*]).
(SingI (ToPeano 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 :: [*]).
(SingI (ToPeano 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, NFData (Sing n)) =>
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 :: GHC.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, NFData (Sing n)) =>
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 :: GHC.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, NFData (Sing n)) =>
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 :: GHC.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), FailOnOperationFound (ContainsOp (ToT t)),
      FailOnBigMapFound (ContainsBigMap (ToT t)),
      FailOnContractFound (ContainsContract (ToT t)),
      FailOnTicketFound (ContainsTicket (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), FailOnOperationFound (ContainsOp (ToT t)),
  FailOnBigMapFound (ContainsBigMap (ToT t)),
  FailOnContractFound (ContainsContract (ToT t)),
  FailOnTicketFound (ContainsTicket (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 :: GHC.Nat) (pair :: Type) =
  ( ConstraintGetN (ToPeano n) (ToT pair)
  , ToT (PairGetHs (ToPeano n) pair) ~ GetN (ToPeano n) (ToT pair)
  , SingI (ToPeano 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 :: GHC.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
$ SingI (ToPeano n) => PeanoNatural (ToPeano n)
forall (n :: Nat). SingI (ToPeano 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 :: GHC.Nat) (val :: Type) (pair :: Type) =
  ( ConstraintUpdateN (ToPeano n) (ToT pair)
  , ToT (PairUpdateHs (ToPeano n) val pair) ~ UpdateN (ToPeano n) (ToT val) (ToT pair)
  , SingI (ToPeano 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 :: GHC.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
$ SingI (ToPeano n) => PeanoNatural (ToPeano n)
forall (n :: Nat). SingI (ToPeano 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), FailOnOperationFound (ContainsOp (ToT a)),
      FailOnBigMapFound (ContainsBigMap (ToT a)),
      FailOnContractFound (ContainsContract (ToT a)),
      FailOnTicketFound (ContainsTicket (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), FailOnOperationFound (ContainsOp (ToT a)),
  FailOnBigMapFound (ContainsBigMap (ToT a)),
  FailOnContractFound (ContainsContract (ToT a)),
  FailOnTicketFound (ContainsTicket (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), FailOnOperationFound (ContainsOp (ToT a)),
      FailOnBigMapFound (ContainsBigMap (ToT a)),
      FailOnContractFound (ContainsContract (ToT a)),
      FailOnTicketFound (ContainsTicket (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), FailOnOperationFound (ContainsOp (ToT a)),
  FailOnBigMapFound (ContainsBigMap (ToT a)),
  FailOnContractFound (ContainsContract (ToT a)),
  FailOnTicketFound (ContainsTicket (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', NFData (Sing n)) =>
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 :: GHC.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), FailOnOperationFound (ContainsOp (ToT a)),
      FailOnBigMapFound (ContainsBigMap (ToT a)),
      FailOnContractFound (ContainsContract (ToT a)),
      FailOnTicketFound (ContainsTicket (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), FailOnOperationFound (ContainsOp (ToT a)),
  FailOnBigMapFound (ContainsBigMap (ToT a)),
  FailOnContractFound (ContainsContract (ToT a)),
  FailOnTicketFound (ContainsTicket (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), FailOnOperationFound (ContainsOp (ToT a)),
      FailOnBigMapFound (ContainsBigMap (ToT a)),
      FailOnTicketFound (ContainsTicket (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), FailOnOperationFound (ContainsOp (ToT a)),
  FailOnBigMapFound (ContainsBigMap (ToT a)),
  FailOnTicketFound (ContainsTicket (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), FailOnOperationFound (ContainsOp (ToT a)),
       FailOnBigMapFound (ContainsBigMap (ToT a)),
       FailOnTicketFound (ContainsTicket (ToT a))),
      (SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)),
       FailOnBigMapFound (ContainsBigMap (ToT a)),
       FailOnContractFound (ContainsContract (ToT a)),
       FailOnTicketFound (ContainsTicket (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), FailOnOperationFound (ContainsOp (ToT a)),
   FailOnBigMapFound (ContainsBigMap (ToT a)),
   FailOnTicketFound (ContainsTicket (ToT a))),
  (SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)),
   FailOnBigMapFound (ContainsBigMap (ToT a)),
   FailOnContractFound (ContainsContract (ToT a)),
   FailOnTicketFound (ContainsTicket (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), FailOnOperationFound (ContainsOp (ToT a)),
      FailOnBigMapFound (ContainsBigMap (ToT a)),
      FailOnTicketFound (ContainsTicket (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), FailOnOperationFound (ContainsOp (ToT a)),
  FailOnBigMapFound (ContainsBigMap (ToT a)),
  FailOnTicketFound (ContainsTicket (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), FailOnOperationFound (ContainsOp (ToT a)),
       FailOnBigMapFound (ContainsBigMap (ToT a)),
       FailOnTicketFound (ContainsTicket (ToT a))),
      (SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)),
       FailOnBigMapFound (ContainsBigMap (ToT a)),
       FailOnContractFound (ContainsContract (ToT a)),
       FailOnTicketFound (ContainsTicket (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), FailOnOperationFound (ContainsOp (ToT a)),
   FailOnBigMapFound (ContainsBigMap (ToT a)),
   FailOnTicketFound (ContainsTicket (ToT a))),
  (SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)),
   FailOnBigMapFound (ContainsBigMap (ToT a)),
   FailOnContractFound (ContainsContract (ToT a)),
   FailOnTicketFound (ContainsTicket (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
  => n : m : s :-> ArithResHs Add n m : s
add :: (n : m : s) :-> (ArithResHs Add n m : s)
add = Instr (ToTs (n : m : s)) (ToTs (ArithResHs Add n m : s))
-> (n : m : s) :-> (ArithResHs Add n m : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (n : m : s)) (ToTs (ArithResHs Add n m : s))
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
Instr (n : m : s) (ArithRes Add n m : s)
ADD

sub
  :: ArithOpHs Sub n m
  => n : m : s :-> ArithResHs Sub n m : s
sub :: (n : m : s) :-> (ArithResHs Sub n m : s)
sub = Instr (ToTs (n : m : s)) (ToTs (ArithResHs Sub n m : s))
-> (n : m : s) :-> (ArithResHs Sub n m : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (n : m : s)) (ToTs (ArithResHs Sub n m : s))
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Sub n m =>
Instr (n : m : s) (ArithRes Sub n m : s)
SUB

rsub
  :: ArithOpHs Sub n m
  => m : n : s :-> ArithResHs Sub n m : s
rsub :: (m : n : s) :-> (ArithResHs Sub n m : 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) :-> (ArithResHs Sub n m : s))
-> (m : n : s) :-> (ArithResHs Sub n m : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (n : m : s) :-> (ArithResHs Sub n m : s)
forall n m (s :: [*]).
ArithOpHs Sub n m =>
(n : m : s) :-> (ArithResHs Sub n m : s)
sub

mul
  :: ArithOpHs Mul n m
  => n : m : s :-> ArithResHs Mul n m : s
mul :: (n : m : s) :-> (ArithResHs Mul n m : s)
mul = Instr (ToTs (n : m : s)) (ToTs (ArithResHs Mul n m : s))
-> (n : m : s) :-> (ArithResHs Mul n m : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (n : m : s)) (ToTs (ArithResHs Mul n m : s))
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
Instr (n : m : s) (ArithRes Mul n m : s)
MUL

ediv :: EDivOpHs n m
     => n : m : s
     :-> Maybe ((EDivOpResHs n m, EModOpResHs n m)) : s
ediv :: (n : m : s) :-> (Maybe (EDivOpResHs n m, EModOpResHs n m) : s)
ediv = Instr
  (ToTs (n : m : s))
  (ToTs (Maybe (EDivOpResHs n m, EModOpResHs n m) : s))
-> (n : m : s) :-> (Maybe (EDivOpResHs n m, EModOpResHs n m) : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr
  (ToTs (n : m : s))
  (ToTs (Maybe (EDivOpResHs n m, EModOpResHs n m) : s))
forall (n :: T) (m :: T) (s :: [T]).
EDivOp n m =>
Instr
  (n : m : s) ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : s)
EDIV

abs :: UnaryArithOpHs Abs n => n : s :-> UnaryArithResHs Abs n : s
abs :: (n : s) :-> (UnaryArithResHs Abs n : s)
abs = Instr (ToTs (n : s)) (ToTs (UnaryArithResHs Abs n : s))
-> (n : s) :-> (UnaryArithResHs Abs n : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (n : s)) (ToTs (UnaryArithResHs Abs n : s))
forall (n :: T) (s :: [T]).
UnaryArithOp Abs n =>
Instr (n : s) (UnaryArithRes Abs n : s)
ABS

neg :: UnaryArithOpHs Neg n => n : s :-> UnaryArithResHs Neg n : s
neg :: (n : s) :-> (UnaryArithResHs Neg n : s)
neg = Instr (ToTs (n : s)) (ToTs (UnaryArithResHs Neg n : s))
-> (n : s) :-> (UnaryArithResHs Neg n : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (n : s)) (ToTs (UnaryArithResHs Neg n : s))
forall (n :: T) (s :: [T]).
UnaryArithOp Neg n =>
Instr (n : s) (UnaryArithRes Neg n : s)
NEG


lsl
  :: ArithOpHs Lsl n m
  => n : m : s :-> ArithResHs Lsl n m : s
lsl :: (n : m : s) :-> (ArithResHs Lsl n m : s)
lsl = Instr (ToTs (n : m : s)) (ToTs (ArithResHs Lsl n m : s))
-> (n : m : s) :-> (ArithResHs Lsl n m : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (n : m : s)) (ToTs (ArithResHs Lsl n m : s))
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Lsl n m =>
Instr (n : m : s) (ArithRes Lsl n m : s)
LSL

lsr
  :: ArithOpHs Lsr n m
  => n : m : s :-> ArithResHs Lsr n m : s
lsr :: (n : m : s) :-> (ArithResHs Lsr n m : s)
lsr = Instr (ToTs (n : m : s)) (ToTs (ArithResHs Lsr n m : s))
-> (n : m : s) :-> (ArithResHs Lsr n m : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (n : m : s)) (ToTs (ArithResHs Lsr n m : s))
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Lsr n m =>
Instr (n : m : s) (ArithRes Lsr n m : s)
LSR

or
  :: ArithOpHs Or n m
  => n : m : s :-> ArithResHs Or n m : s
or :: (n : m : s) :-> (ArithResHs Or n m : s)
or = Instr (ToTs (n : m : s)) (ToTs (ArithResHs Or n m : s))
-> (n : m : s) :-> (ArithResHs Or n m : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (n : m : s)) (ToTs (ArithResHs Or n m : s))
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Or n m =>
Instr (n : m : s) (ArithRes Or n m : s)
OR

and
  :: ArithOpHs And n m
  => n : m : s :-> ArithResHs And n m : s
and :: (n : m : s) :-> (ArithResHs And n m : s)
and = Instr (ToTs (n : m : s)) (ToTs (ArithResHs And n m : s))
-> (n : m : s) :-> (ArithResHs And n m : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (n : m : s)) (ToTs (ArithResHs And n m : s))
forall (n :: T) (m :: T) (s :: [T]).
ArithOp And n m =>
Instr (n : m : s) (ArithRes And n m : s)
AND

xor
  :: (ArithOpHs Xor n m)
  => n : m : s :-> ArithResHs Xor n m : s
xor :: (n : m : s) :-> (ArithResHs Xor n m : s)
xor = Instr (ToTs (n : m : s)) (ToTs (ArithResHs Xor n m : s))
-> (n : m : s) :-> (ArithResHs Xor n m : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (n : m : s)) (ToTs (ArithResHs Xor n m : s))
forall (n :: T) (m :: T) (s :: [T]).
ArithOp Xor n m =>
Instr (n : m : s) (ArithRes Xor n m : s)
XOR

not :: UnaryArithOpHs Not n => n : s :-> UnaryArithResHs Not n : s
not :: (n : s) :-> (UnaryArithResHs Not n : s)
not = Instr (ToTs (n : s)) (ToTs (UnaryArithResHs Not n : s))
-> (n : s) :-> (UnaryArithResHs Not n : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (n : s)) (ToTs (UnaryArithResHs Not n : s))
forall (n :: T) (s :: [T]).
UnaryArithOp Not n =>
Instr (n : s) (UnaryArithRes Not n : s)
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 = Instr (ToTs (n : s)) (ToTs (UnaryArithResHs Eq' n : s))
-> (n : s) :-> (UnaryArithResHs Eq' n : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (n : s)) (ToTs (UnaryArithResHs Eq' n : s))
forall (n :: T) (s :: [T]).
UnaryArithOp Eq' n =>
Instr (n : s) (UnaryArithRes Eq' n : s)
EQ

neq0 :: UnaryArithOpHs Neq n => n : s :-> UnaryArithResHs Neq n : s
neq0 :: (n : s) :-> (UnaryArithResHs Neq n : s)
neq0 = Instr (ToTs (n : s)) (ToTs (UnaryArithResHs Neq n : s))
-> (n : s) :-> (UnaryArithResHs Neq n : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (n : s)) (ToTs (UnaryArithResHs Neq n : s))
forall (n :: T) (s :: [T]).
UnaryArithOp Neq n =>
Instr (n : s) (UnaryArithRes Neq n : s)
NEQ

lt0 :: UnaryArithOpHs Lt n => n : s :-> UnaryArithResHs Lt n : s
lt0 :: (n : s) :-> (UnaryArithResHs Lt n : s)
lt0 = Instr (ToTs (n : s)) (ToTs (UnaryArithResHs Lt n : s))
-> (n : s) :-> (UnaryArithResHs Lt n : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (n : s)) (ToTs (UnaryArithResHs Lt n : s))
forall (n :: T) (s :: [T]).
UnaryArithOp Lt n =>
Instr (n : s) (UnaryArithRes Lt n : s)
LT

gt0 :: UnaryArithOpHs Gt n => n : s :-> UnaryArithResHs Gt n : s
gt0 :: (n : s) :-> (UnaryArithResHs Gt n : s)
gt0 = Instr (ToTs (n : s)) (ToTs (UnaryArithResHs Gt n : s))
-> (n : s) :-> (UnaryArithResHs Gt n : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (n : s)) (ToTs (UnaryArithResHs Gt n : s))
forall (n :: T) (s :: [T]).
UnaryArithOp Gt n =>
Instr (n : s) (UnaryArithRes Gt n : s)
GT

le0 :: UnaryArithOpHs Le n => n : s :-> UnaryArithResHs Le n : s
le0 :: (n : s) :-> (UnaryArithResHs Le n : s)
le0 = Instr (ToTs (n : s)) (ToTs (UnaryArithResHs Le n : s))
-> (n : s) :-> (UnaryArithResHs Le n : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (n : s)) (ToTs (UnaryArithResHs Le n : s))
forall (n :: T) (s :: [T]).
UnaryArithOp Le n =>
Instr (n : s) (UnaryArithRes Le n : s)
LE

ge0 :: UnaryArithOpHs Ge n => n : s :-> UnaryArithResHs Ge n : s
ge0 :: (n : s) :-> (UnaryArithResHs Ge n : s)
ge0 = Instr (ToTs (n : s)) (ToTs (UnaryArithResHs Ge n : s))
-> (n : s) :-> (UnaryArithResHs Ge n : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (n : s)) (ToTs (UnaryArithResHs Ge n : s))
forall (n :: T) (s :: [T]).
UnaryArithOp Ge n =>
Instr (n : s) (UnaryArithRes Ge n : s)
GE

int :: (ToIntegerArithOpHs i) => i : s :-> Integer : s
int :: (i : s) :-> (Integer : s)
int = Instr (ToTs (i : s)) (ToTs (Integer : s))
-> (i : s) :-> (Integer : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (i : s)) (ToTs (Integer : s))
forall (n :: T) (s :: [T]).
ToIntArithOp n =>
Instr (n : s) ('TInt : s)
INT

-- | 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), 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), 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 addr s.
      ( NiceParameterFull p, ForbidExplicitDefaultEntrypoint p
      , ToTAddress_ p 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), 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), 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), 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 s.
     (HasEntrypointArg cp epRef epArg, ToTAddress_ cp 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 (s :: [*]).
(HasEntrypointArg cp epRef epArg, ToTAddress_ cp 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), 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), 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), 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), 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 s. Contract p g
  -> Maybe KeyHash : Mutez : g : s
  :-> Operation : Address : s
createContract :: Contract p g
-> (Maybe KeyHash : Mutez : g : s) :-> (Operation : Address : s)
createContract cntrc :: Contract p g
cntrc@Contract{} =
  Instr
  (ToTs (Maybe KeyHash : Mutez : g : s))
  (ToTs (Operation : Address : s))
-> (Maybe KeyHash : Mutez : g : s) :-> (Operation : Address : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
   (ToTs (Maybe KeyHash : Mutez : g : s))
   (ToTs (Operation : Address : s))
 -> (Maybe KeyHash : Mutez : g : s) :-> (Operation : Address : s))
-> Instr
     (ToTs (Maybe KeyHash : Mutez : g : s))
     (ToTs (Operation : Address : s))
-> (Maybe KeyHash : Mutez : g : s) :-> (Operation : Address : s)
forall a b. (a -> b) -> a -> b
$ Contract (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 p g
-> Instr
     ('TOption 'TKeyHash : 'TMutez : g : s)
     ('TOperation : 'TAddress : s)
CREATE_CONTRACT (Contract p g -> Contract (ToT p) (ToT g)
forall cp st. Contract cp st -> Contract (ToT cp) (ToT st)
toMichelsonContract Contract p g
cntrc)
    (ParameterScope (ToT p) =>
 Instr
   ('TOption 'TKeyHash : 'TMutez : ToT g : ToTs s)
   ('TOperation : 'TAddress : ToTs s))
-> (((SingI (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), 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), FailOnOperationFound (ContainsOp (ToT g)),
      FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT g)),
      FailOnContractFound (ContainsContract (ToT g))),
     HasAnnotation 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), FailOnOperationFound (ContainsOp (ToT g)),
  FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT g)),
  FailOnContractFound (ContainsContract (ToT g))),
 HasAnnotation 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

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

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

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

-- | 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)

class NonZero t where
  -- | Retain the value only if it is not zero.
  nonZero :: t : s :-> Maybe t : s

instance NonZero Integer where
  nonZero :: (Integer : s) :-> (Maybe Integer : s)
nonZero = (Integer : s) :-> (Integer : Integer : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup ((Integer : s) :-> (Integer : Integer : s))
-> ((Integer : Integer : s) :-> (Bool : Integer : s))
-> (Integer : s) :-> (Bool : Integer : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Integer : s) :-> (Bool : Integer : s)
forall n (s :: [*]).
UnaryArithOpHs Eq' n =>
(n : s) :-> (UnaryArithResHs Eq' n : s)
eq0 ((Integer : s) :-> (Bool : Integer : s))
-> ((Bool : Integer : s) :-> (Maybe Integer : s))
-> (Integer : s) :-> (Maybe Integer : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((Integer : s) :-> (Maybe Integer : s))
-> ((Integer : s) :-> (Maybe Integer : s))
-> (Bool : Integer : s) :-> (Maybe Integer : s)
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
if_ ((Integer : s) :-> s
forall a (s :: [*]). (a : s) :-> s
drop ((Integer : s) :-> s)
-> (s :-> (Maybe Integer : s))
-> (Integer : s) :-> (Maybe Integer : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# s :-> (Maybe Integer : s)
forall a (s :: [*]). KnownValue a => s :-> (Maybe a : s)
none) (Integer : s) :-> (Maybe Integer : s)
forall a (s :: [*]). (a : s) :-> (Maybe a : s)
some

instance NonZero Natural where
  nonZero :: (Natural : s) :-> (Maybe Natural : s)
nonZero = (Natural : s) :-> (Natural : Natural : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup ((Natural : s) :-> (Natural : Natural : s))
-> ((Natural : Natural : s) :-> (Integer : Natural : s))
-> (Natural : s) :-> (Integer : Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : Natural : s) :-> (Integer : Natural : s)
forall i (s :: [*]).
ToIntegerArithOpHs i =>
(i : s) :-> (Integer : s)
int ((Natural : s) :-> (Integer : Natural : s))
-> ((Integer : Natural : s) :-> (Bool : Natural : s))
-> (Natural : s) :-> (Bool : Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Natural : s) :-> (Bool : Natural : s)
forall n (s :: [*]).
UnaryArithOpHs Eq' n =>
(n : s) :-> (UnaryArithResHs Eq' n : s)
eq0 ((Natural : s) :-> (Bool : Natural : s))
-> ((Bool : Natural : s) :-> (Maybe Natural : s))
-> (Natural : s) :-> (Maybe Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((Natural : s) :-> (Maybe Natural : s))
-> ((Natural : s) :-> (Maybe Natural : s))
-> (Bool : Natural : s) :-> (Maybe Natural : s)
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
if_ ((Natural : s) :-> s
forall a (s :: [*]). (a : s) :-> s
drop ((Natural : s) :-> s)
-> (s :-> (Maybe Natural : s))
-> (Natural : s) :-> (Maybe Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# s :-> (Maybe Natural : s)
forall a (s :: [*]). KnownValue a => s :-> (Maybe a : s)
none) (Natural : s) :-> (Maybe Natural : s)
forall a (s :: [*]). (a : s) :-> (Maybe a : s)
some