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

module Lorentz.Instr
  ( nop
  , justComment
  , comment
  , commentAroundFun
  , commentAroundStmt
  , drop
  , dropN
  , dup
  , swap
  , ConstraintDIGLorentz
  , digPeano
  , dig
  , ConstraintDUGLorentz
  , dugPeano
  , dug
  , push
  , some
  , none
  , unit
  , ifNone
  , pair
  , car
  , cdr
  , left
  , right
  , ifLeft
  , nil
  , cons
  , size
  , emptySet
  , emptyMap
  , emptyBigMap
  , map
  , iter
  , mem
  , get
  , update
  , failingWhenPresent
  , updateNew
  , if_
  , ifCons
  , loop
  , loopLeft
  , lambda
  , exec
  , execute
  , apply
  , dip
  , ConstraintDIPNLorentz
  , dipNPeano
  , dipN
  , failWith
  , cast
  , pack
  , unpack
  , 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
  , contractCallingUnsafe
  , runFutureContract
  , epAddressToContract
  , transferTokens
  , setDelegate
  , createContract
  , implicitAccount
  , now
  , amount
  , balance
  , checkSignature
  , sha256
  , sha512
  , blake2B
  , hashKey
  , source
  , sender
  , address
  , chainId
  , 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 Data.Kind as Kind
import Data.Singletons (SingI, sing)
import qualified GHC.TypeNats as GHC (Nat)

import Lorentz.Address
import Lorentz.Arith
import Lorentz.Base
import Lorentz.Constraints
import Lorentz.Entrypoints
import Lorentz.Polymorphic
import Lorentz.Run (Contract, compileLorentzContract)
import Lorentz.Value
import Lorentz.Zip
import Michelson.Typed
  (pattern CAR, pattern CDR, CommentType(..), ConstraintDIG, ConstraintDIG', ConstraintDIPN,
  ConstraintDIPN', ConstraintDUG, ConstraintDUG', EntrypointCallT(..), ExtInstr(..), Instr(..),
  RemFail(..), pattern PAIR, SomeEntrypointCallT(..), Value'(..), sepcName, starNotes)
import Michelson.Typed.Arith
import Michelson.Typed.Haskell.Value
import Util.Peano
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 funName :: Text
funName funBody :: 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 stmtName :: Text
stmtName stmtBody :: 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 :: [Kind.Type]).
  -- Note: if we introduce `nPeano ~ ToPeano n` variable,
  -- GHC will complain that this constraint is redundant.
  ( SingI (ToPeano n), KnownPeano (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 (Sing (ToPeano n) -> Instr (ToTs s) (ToTs (Drop (ToPeano n) s))
forall (n :: Peano) (inp :: [T]).
(SingI n, KnownPeano n, RequireLongerOrSameLength inp n,
 NFData (Sing n)) =>
Sing n -> Instr inp (Drop n inp)
DROPN (Sing (ToPeano n) -> Instr (ToTs s) (ToTs (Drop (ToPeano n) s)))
-> Sing (ToPeano n) -> Instr (ToTs s) (ToTs (Drop (ToPeano n) s))
forall a b. (a -> b) -> a -> b
$ SingI (ToPeano n) => Sing (ToPeano n)
forall k (a :: k). SingI a => Sing a
sing @(ToPeano n))
  where
    _example :: '[ Integer, Integer, Integer ] :-> '[]
    _example :: '[Integer, Integer, Integer] :-> '[]
_example = forall (s :: [*]).
(SingI (ToPeano 3), KnownPeano (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), KnownPeano (ToPeano n),
 RequireLongerOrSameLength (ToTs s) (ToPeano n),
 Drop (ToPeano n) (ToTs s) ~ ToTs (Drop (ToPeano n) s)) =>
s :-> Drop (ToPeano n) s
dropN @3

dup  :: 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]). Instr (a : s) (a : a : s)
DUP

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 :: [Kind.Type]) (out :: [Kind.Type])
  (a :: Kind.Type) =
  ( ConstraintDIG n (ToTs inp) (ToTs out) (ToT a)
  , ConstraintDIG' Kind.Type n inp out a
  )

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

-- | Version of `dig` which uses Peano number.
-- It is inteded 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 (Sing n -> Instr (ToTs inp) (ToTs out)
forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T).
(ConstraintDIG n inp out a, NFData (Sing n)) =>
Sing n -> Instr inp out
DIG (Sing n -> Instr (ToTs inp) (ToTs out))
-> Sing n -> Instr (ToTs inp) (ToTs out)
forall a b. (a -> b) -> a -> b
$ SingI n => Sing n
forall k (a :: k). SingI a => Sing a
sing @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 inteded 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 (Sing n -> Instr (ToTs inp) (ToTs out)
forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T).
(ConstraintDUG n inp out a, NFData (Sing n)) =>
Sing n -> Instr inp out
DUG (Sing n -> Instr (ToTs inp) (ToTs out))
-> Sing n -> Instr (ToTs inp) (ToTs out)
forall a b. (a -> b) -> a -> b
$ SingI n => Sing n
forall k (a :: k). SingI a => Sing a
sing @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 a :: 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) ((SingI (ToT t), HasNoOp (ToT t), HasNoBigMap (ToT t),
  HasNoContract (ToT t)) =>
 Instr (ToTs s) (ToT t : ToTs s))
-> ((KnownValue t,
     (SingI (ToT t), FailOnOperationFound (ContainsOp (ToT t)),
      FailOnBigMapFound (ContainsBigMap (ToT t)),
      FailOnContractFound (ContainsContract (ToT t))))
    :- (SingI (ToT t), HasNoOp (ToT t), HasNoBigMap (ToT t),
        HasNoContract (ToT t)))
-> Instr (ToTs s) (ToT t : ToTs s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (KnownValue t,
 (SingI (ToT t), FailOnOperationFound (ContainsOp (ToT t)),
  FailOnBigMapFound (ContainsBigMap (ToT t)),
  FailOnContractFound (ContainsContract (ToT t))))
:- (SingI (ToT t), HasNoOp (ToT t), HasNoBigMap (ToT t),
    HasNoContract (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]).
KnownT 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

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 (b :: T) (a :: T) (s :: [T]).
KnownT b =>
Instr (a : s) ('TOr a b : s)
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 (a :: T) (b :: T) (s :: [T]).
KnownT a =>
Instr (b : s) ('TOr a b : s)
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]).
KnownT 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]).
(KnownT 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]).
(KnownT a, KnownT b, Comparable a) =>
Instr inp ('TMap a b : inp)
EMPTY_MAP

emptyBigMap :: (NiceComparable k, KnownValue 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]).
(KnownT a, KnownT b, Comparable a) =>
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, KnownT 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, KnownT (GetOpVal c)) =>
Instr (GetOpKey c : c : s) ('TOption (GetOpVal c) : s)
GET

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

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 instr :: 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]).
(KnownT i, KnownT 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] -> *).
(KnownT inp, KnownT 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) (ToTs ((i :-> o) & s)))
-> RemFail Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)]
-> Instr (ToTs s) (ToTs ((i :-> o) & 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]).
(KnownT i, KnownT 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] -> *).
(KnownT inp, KnownT 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) (ToTs ((i :-> o) & s)))
-> RemFail Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)]
-> Instr (ToTs s) (ToTs ((i :-> o) & 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
$ (SingI (ToT a), HasNoOp (ToT a), HasNoBigMap (ToT a),
 HasNoContract (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, KnownT b) =>
Instr (a : 'TLambda ('TPair a b) c : s) ('TLambda b c : s)
APPLY ((SingI (ToT a), HasNoOp (ToT a), HasNoBigMap (ToT a),
  HasNoContract (ToT a)) =>
 Instr
   (ToT a : 'TLambda ('TPair (ToT a) (ToT b)) (ToT c) : ToTs s)
   ('TLambda (ToT b) (ToT c) : ToTs s))
-> ((KnownValue a,
     (SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)),
      FailOnBigMapFound (ContainsBigMap (ToT a)),
      FailOnContractFound (ContainsContract (ToT a))))
    :- (SingI (ToT a), HasNoOp (ToT a), HasNoBigMap (ToT a),
        HasNoContract (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
\\ (KnownValue a,
 (SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)),
  FailOnBigMapFound (ContainsBigMap (ToT a)),
  FailOnContractFound (ContainsContract (ToT a))))
:- (SingI (ToT a), HasNoOp (ToT a), HasNoBigMap (ToT a),
    HasNoContract (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 :: [Kind.Type]) (out :: [Kind.Type])
  (s :: [Kind.Type]) (s' :: [Kind.Type]) =
  ( ConstraintDIPN n (ToTs inp) (ToTs out) (ToTs s) (ToTs s')
  , ConstraintDIPN' Kind.Type n inp out s s'
  )

-- | Version of `dipN` which uses Peano number.
-- It is inteded for internal usage in Lorentz.
dipNPeano ::
  forall (n :: Peano) (inp :: [Kind.Type]) (out :: [Kind.Type]) (s :: [Kind.Type]) (s' :: [Kind.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 (Sing 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)) =>
Sing n -> Instr s s' -> Instr inp out
DIPN (SingI n => Sing n
forall k (a :: k). SingI a => Sing a
sing @n) Instr (ToTs s) (ToTs s')
a)

dipN ::
  forall (n :: GHC.Nat) (inp :: [Kind.Type]) (out :: [Kind.Type]) (s :: [Kind.Type]) (s' :: [Kind.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

failWith :: KnownValue 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]).
KnownT a =>
Instr (a : s) out
FAILWITH

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

unpack
  :: forall a s. (NiceUnpackedValue a)
  => ByteString & s :-> Maybe a & s
unpack :: (ByteString & s) :-> (Maybe a & s)
unpack = 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
$ (PackedValScope (ToT a), ConstantScope (ToT a)) =>
Instr ('TBytes : ToTs s) ('TOption (ToT a) : ToTs s)
forall (a :: T) (s :: [T]).
(UnpackedValScope a, KnownT a) =>
Instr ('TBytes : s) ('TOption a : s)
UNPACK ((PackedValScope (ToT a), ConstantScope (ToT a)) =>
 Instr ('TBytes : ToTs s) ('TOption (ToT a) : ToTs s))
-> ((KnownValue a,
     ((SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)),
       FailOnBigMapFound (ContainsBigMap (ToT a))),
      (SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)),
       FailOnBigMapFound (ContainsBigMap (ToT a)),
       FailOnContractFound (ContainsContract (ToT a)))))
    :- (PackedValScope (ToT a), ConstantScope (ToT a)))
-> Instr ('TBytes : ToTs s) ('TOption (ToT a) : ToTs s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (KnownValue a,
 ((SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)),
   FailOnBigMapFound (ContainsBigMap (ToT a))),
  (SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)),
   FailOnBigMapFound (ContainsBigMap (ToT a)),
   FailOnContractFound (ContainsContract (ToT a)))))
:- (PackedValScope (ToT a), ConstantScope (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, KnownT 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, Typeable n, Typeable 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, Typeable n, Typeable 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, Typeable n, Typeable 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, Typeable n, Typeable 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, Typeable n, Typeable 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, Typeable n, Typeable 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, Typeable n, Typeable 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, Typeable n, Typeable 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, KnownT 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 :: Natural & s :-> Integer & s
int :: (Natural & s) :-> (Integer & s)
int = Instr (ToTs (Natural & s)) (ToTs (Integer & s))
-> (Natural & s) :-> (Integer & s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (Natural & s)) (ToTs (Integer & s))
forall (s :: [T]). Instr ('TNat : 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) (ToTs (ContractRef p & s))
forall (arg :: T) (inp :: [T]).
ParameterScope arg =>
SomeEntrypointCallT arg -> Instr inp ('TContract arg : inp)
SELF (SomeEntrypointCallT (ToT p)
 -> Instr (ToTs s) (ToTs (ContractRef p & s)))
-> SomeEntrypointCallT (ToT p)
-> Instr (ToTs s) (ToTs (ContractRef p & 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) ((KnownT (ToT p), HasNoOp (ToT p), HasNoNestedBigMaps (ToT p)) =>
 s :-> (ContractRef p & s))
-> (NiceParameter p
    :- (KnownT (ToT p), HasNoOp (ToT p), HasNoNestedBigMaps (ToT p)))
-> s :-> (ContractRef p & s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ NiceParameter p
:- (KnownT (ToT p), HasNoOp (ToT p), HasNoNestedBigMaps (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 epRef :: 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
$
  ((KnownValue p,
  (KnownT (ToT p), FailOnOperationFound (ContainsOp (ToT p)),
   FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT p))))
 :- (KnownT (ToT p), HasNoOp (ToT p), HasNoNestedBigMaps (ToT p)))
-> ((KnownT (ToT p), HasNoOp (ToT p),
     HasNoNestedBigMaps (ToT p)) =>
    Instr
      (ToTs s)
      (ToT (ContractRef (GetEntrypointArgCustom p mname)) : ToTs s))
-> Instr
     (ToTs s)
     (ToT (ContractRef (GetEntrypointArgCustom p mname)) : ToTs s)
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict ((KnownValue p,
 (KnownT (ToT p), FailOnOperationFound (ContainsOp (ToT p)),
  FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT p))))
:- (KnownT (ToT p), HasNoOp (ToT p), HasNoNestedBigMaps (ToT p))
forall a. NiceParameter a :- ParameterScope (ToT a)
niceParameterEvi @p) (((KnownT (ToT p), HasNoOp (ToT p), HasNoNestedBigMaps (ToT p)) =>
  Instr
    (ToTs s)
    (ToT (ContractRef (GetEntrypointArgCustom p mname)) : ToTs s))
 -> Instr
      (ToTs s) (ToTs (ContractRef (GetEntrypointArgCustom p mname) & s)))
-> ((KnownT (ToT p), HasNoOp (ToT p),
     HasNoNestedBigMaps (ToT p)) =>
    Instr
      (ToTs s)
      (ToT (ContractRef (GetEntrypointArgCustom p mname)) : ToTs s))
-> Instr
     (ToTs s) (ToTs (ContractRef (GetEntrypointArgCustom p mname) & 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) ((KnownT (ToT p), HasNoOp (ToT p), HasNoNestedBigMaps (ToT p)) =>
 (addr & s) :-> (Maybe (ContractRef p) & s))
-> ((KnownValue p,
     (KnownT (ToT p), FailOnOperationFound (ContainsOp (ToT p)),
      FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT p))))
    :- (KnownT (ToT p), HasNoOp (ToT p), HasNoNestedBigMaps (ToT p)))
-> (addr & s) :-> (Maybe (ContractRef p) & s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (KnownValue p,
 (KnownT (ToT p), FailOnOperationFound (ContainsOp (ToT p)),
  FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT p))))
:- (KnownT (ToT p), HasNoOp (ToT p), HasNoNestedBigMaps (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 (((KnownValue p,
  (KnownT (ToT p), FailOnOperationFound (ContainsOp (ToT p)),
   FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT 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
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, epName :: 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'.
contractCallingUnsafe
  :: forall arg s.
     (NiceParameter arg)
  => EpName
  -> Address & s :-> Maybe (ContractRef arg) & s
contractCallingUnsafe :: EpName -> (Address & s) :-> (Maybe (ContractRef arg) & s)
contractCallingUnsafe epName :: 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) ((KnownT (ToT p), HasNoOp (ToT p), HasNoNestedBigMaps (ToT p)) =>
 (EpAddress & s) :-> (Maybe (ContractRef p) & s))
-> ((KnownValue p,
     (KnownT (ToT p), FailOnOperationFound (ContainsOp (ToT p)),
      FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT p))))
    :- (KnownT (ToT p), HasNoOp (ToT p), HasNoNestedBigMaps (ToT p)))
-> (EpAddress & s) :-> (Maybe (ContractRef p) & s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (KnownValue p,
 (KnownT (ToT p), FailOnOperationFound (ContainsOp (ToT p)),
  FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT p))))
:- (KnownT (ToT p), HasNoOp (ToT p), HasNoNestedBigMaps (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
$ (KnownT (ToT p), HasNoOp (ToT p), HasNoNestedBigMaps (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 ((KnownT (ToT p), HasNoOp (ToT p), HasNoNestedBigMaps (ToT p)) =>
 Instr
   (ToT p : 'TMutez : 'TContract (ToT p) : ToTs s)
   ('TOperation : ToTs s))
-> ((KnownValue p,
     (KnownT (ToT p), FailOnOperationFound (ContainsOp (ToT p)),
      FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT p))))
    :- (KnownT (ToT p), HasNoOp (ToT p), HasNoNestedBigMaps (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
\\ (KnownValue p,
 (KnownT (ToT p), FailOnOperationFound (ContainsOp (ToT p)),
  FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT p))))
:- (KnownT (ToT p), HasNoOp (ToT p), HasNoNestedBigMaps (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. (NiceStorage g, NiceParameterFull p)
  => 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 =
  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.
(NiceParameterFull cp, NiceStorage st) =>
Contract cp st -> Contract (ToT cp) (ToT st)
compileLorentzContract Contract p g
cntrc)
    ((KnownT (ToT p), HasNoOp (ToT p), HasNoNestedBigMaps (ToT p)) =>
 Instr
   ('TOption 'TKeyHash : 'TMutez : ToT g : ToTs s)
   ('TOperation : 'TAddress : ToTs s))
-> ((KnownValue p,
     (KnownT (ToT p), FailOnOperationFound (ContainsOp (ToT p)),
      FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT p))))
    :- (KnownT (ToT p), HasNoOp (ToT p), HasNoNestedBigMaps (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
\\ (KnownValue p,
 (KnownT (ToT p), FailOnOperationFound (ContainsOp (ToT p)),
  FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT p))))
:- (KnownT (ToT p), HasNoOp (ToT p), HasNoNestedBigMaps (ToT p))
forall a. NiceParameter a :- ParameterScope (ToT a)
niceParameterEvi @p
    ((KnownT (ToT g), HasNoOp (ToT g), HasNoNestedBigMaps (ToT g),
  HasNoContract (ToT g)) =>
 Instr
   ('TOption 'TKeyHash : 'TMutez : ToT g : ToTs s)
   ('TOperation : 'TAddress : ToTs s))
-> ((HasAnnotation g, KnownValue g,
     (KnownT (ToT g), FailOnOperationFound (ContainsOp (ToT g)),
      FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT g)),
      FailOnContractFound (ContainsContract (ToT g))))
    :- (KnownT (ToT g), HasNoOp (ToT g), HasNoNestedBigMaps (ToT g),
        HasNoContract (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
\\ (HasAnnotation g, KnownValue g,
 (KnownT (ToT g), FailOnOperationFound (ContainsOp (ToT g)),
  FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT g)),
  FailOnContractFound (ContainsContract (ToT g))))
:- (KnownT (ToT g), HasNoOp (ToT g), HasNoNestedBigMaps (ToT g),
    HasNoContract (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

checkSignature :: PublicKey & Signature & ByteString & s :-> Bool & s
checkSignature :: (PublicKey & (Signature & (ByteString & s))) :-> (Bool & s)
checkSignature = Instr
  (ToTs (PublicKey & (Signature & (ByteString & s))))
  (ToTs (Bool & s))
-> (PublicKey & (Signature & (ByteString & s))) :-> (Bool & s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr
  (ToTs (PublicKey & (Signature & (ByteString & s))))
  (ToTs (Bool & s))
forall (s :: [T]).
Instr ('TKey : 'TSignature : 'TBytes : s) ('TBool : s)
CHECK_SIGNATURE

sha256 :: ByteString & s :-> ByteString & s
sha256 :: (ByteString & s) :-> (ByteString & s)
sha256 = Instr (ToTs (ByteString & s)) (ToTs (ByteString & s))
-> (ByteString & s) :-> (ByteString & s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (ByteString & s)) (ToTs (ByteString & s))
forall (s :: [T]). Instr ('TBytes : s) ('TBytes : s)
SHA256

sha512 :: ByteString & s :-> ByteString & s
sha512 :: (ByteString & s) :-> (ByteString & s)
sha512 = Instr (ToTs (ByteString & s)) (ToTs (ByteString & s))
-> (ByteString & s) :-> (ByteString & s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (ByteString & s)) (ToTs (ByteString & s))
forall (s :: [T]). Instr ('TBytes : s) ('TBytes : s)
SHA512

blake2B :: ByteString & s :-> ByteString & s
blake2B :: (ByteString & s) :-> (ByteString & s)
blake2B = Instr (ToTs (ByteString & s)) (ToTs (ByteString & s))
-> (ByteString & s) :-> (ByteString & s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (ByteString & s)) (ToTs (ByteString & s))
forall (s :: [T]). Instr ('TBytes : s) ('TBytes : s)
BLAKE2B

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

{-# 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

-- | 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
     , KnownValue e
     , st ~ (k & v & c & s)
     )
  => (forall s0. k : s0 :-> e : s0)
  -> st :-> st
failingWhenPresent :: (forall (s0 :: [*]). (k : s0) :-> (e : s0)) -> st :-> st
failingWhenPresent mkErr :: forall (s0 :: [*]). (k : s0) :-> (e : s0)
mkErr =
  ((v & (c & s)) :-> (c & (v & (c & s))))
-> (k & (v & (c & s))) :-> (k & (c & (v & (c & s))))
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip (((c & s) :-> (c & (c & s)))
-> (v & (c & s)) :-> (v & (c & (c & s)))
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip (c & s) :-> (c & (c & s))
forall a (s :: [*]). (a & s) :-> (a & (a & s))
dup ((v & (c & s)) :-> (v & (c & (c & s))))
-> ((v & (c & (c & s))) :-> (c & (v & (c & s))))
-> (v & (c & s)) :-> (c & (v & (c & s)))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (v & (c & (c & s))) :-> (c & (v & (c & s)))
forall a b (s :: [*]). (a & (b & s)) :-> (b & (a & s))
swap) ((k & (v & (c & s))) :-> (k & (c & (v & (c & s)))))
-> ((k & (c & (v & (c & s)))) :-> (c & (k & (v & (c & s)))))
-> (k & (v & (c & s))) :-> (c & (k & (v & (c & s))))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (k & (c & (v & (c & s)))) :-> (c & (k & (v & (c & s))))
forall a b (s :: [*]). (a & (b & s)) :-> (b & (a & s))
swap ((k & (v & (c & s))) :-> (c & (k & (v & (c & s)))))
-> ((c & (k & (v & (c & s)))) :-> (c & (k & (k & (v & (c & s))))))
-> (k & (v & (c & s))) :-> (c & (k & (k & (v & (c & s)))))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((k & (v & (c & s))) :-> (k & (k & (v & (c & s)))))
-> (c & (k & (v & (c & s)))) :-> (c & (k & (k & (v & (c & s)))))
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip (k & (v & (c & s))) :-> (k & (k & (v & (c & s))))
forall a (s :: [*]). (a & s) :-> (a & (a & s))
dup ((k & (v & (c & s))) :-> (c & (k & (k & (v & (c & s))))))
-> ((c & (k & (k & (v & (c & s)))))
    :-> (k & (c & (k & (v & (c & s))))))
-> (k & (v & (c & s))) :-> (k & (c & (k & (v & (c & s)))))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (c & (k & (k & (v & (c & s))))) :-> (k & (c & (k & (v & (c & s)))))
forall a b (s :: [*]). (a & (b & s)) :-> (b & (a & s))
swap ((k & (v & (c & s))) :-> (k & (c & (k & (v & (c & s))))))
-> ((k & (c & (k & (v & (c & s)))))
    :-> (Bool & (k & (v & (c & s)))))
-> (k & (v & (c & s))) :-> (Bool & (k & (v & (c & s))))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (k & (c & (k & (v & (c & s))))) :-> (Bool & (k & (v & (c & s))))
forall c (s :: [*]).
MemOpHs c =>
(MemOpKeyHs c & (c & s)) :-> (Bool & s)
mem ((k & (v & (c & s))) :-> (Bool & (k & (v & (c & s)))))
-> ((Bool & (k & (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
#
  ((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 :: [*]). KnownValue 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, k ~ UpdOpKeyHs c, k ~ MemOpKeyHs c
     , KnownValue e
     )
  => (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 mkErr :: forall (s0 :: [*]). (k : s0) :-> (e : s0)
mkErr = (forall (s0 :: [*]). (k : s0) :-> (e : s0))
-> (k & (UpdOpParamsHs c & (c & s)))
   :-> (k & (UpdOpParamsHs c & (c & s)))
forall c k (s :: [*]) v (st :: [*]) e.
(MemOpHs c, k ~ MemOpKeyHs c, KnownValue e,
 st ~ (k & (v & (c & s)))) =>
(forall (s0 :: [*]). (k : s0) :-> (e : s0)) -> st :-> st
failingWhenPresent forall (s0 :: [*]). (k : s0) :-> (e : s0)
mkErr ((k & (UpdOpParamsHs c & (c & s)))
 :-> (k & (UpdOpParamsHs c & (c & s))))
-> ((k & (UpdOpParamsHs c & (c & s))) :-> (c & s))
-> (k & (UpdOpParamsHs c & (c & s))) :-> (c & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (k & (UpdOpParamsHs c & (c & s))) :-> (c & s)
forall c (s :: [*]).
UpdOpHs c =>
(UpdOpKeyHs c & (UpdOpParamsHs c & (c & s))) :-> (c & s)
update

class LorentzFunctor (c :: Kind.Type -> Kind.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 f :: (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 :: [*]). (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 :: [*]). (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 (s :: [*]). (Natural & 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