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

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

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

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

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

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

nop :: s :-> s
nop = I Nop

drop :: a : s :-> s
drop = I DROP

-- | Drop top @n@ elements from the stack.
dropN ::
  forall (n :: Nat) (s :: [Type]).
  -- Note: if we introduce `nPeano ~ ToPeano n` variable,
  -- GHC will complain that this constraint is redundant.
  ( SingIPeano n
  , RequireLongerOrSameLength (ToTs s) (ToPeano n)
  -- ↓ Kinda obvious, but not to GHC.
  , Drop (ToPeano n) (ToTs s) ~ ToTs (Drop (ToPeano n) s)
  ) => s :-> Drop (ToPeano n) s
dropN = I $ DROPN $ toPeanoNatural' @n
  where
    _example :: '[ Integer, Integer, Integer ] :-> '[]
    _example = 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 = I DUP \\ 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 = (I $ DUPN $ toPeanoNatural @n) \\ dupableEvi @a

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

swap :: a : b : s :-> b : a : s
swap = I 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 = I $ DIG $ toPeanoNatural @n

dig ::
  forall (n :: Nat) inp out a.
  ( ConstraintDIGLorentz (ToPeano n) inp out a
  ) => inp :-> out
dig = digPeano @(ToPeano n)
  where
    _example ::
      '[ Integer, Integer, Integer, Bool ] :->
      '[ Bool, Integer, Integer, Integer ]
    _example = 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 = I $ DUG $ toPeanoNatural @n

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

push :: forall t s . NiceConstant t => t -> (s :-> t : s)
push a = I $ PUSH (toVal a) \\ niceConstantEvi @t

some :: a : s :-> Maybe a : s
some = I SOME

none :: forall a s . KnownValue a => s :-> (Maybe a : s)
none = I NONE

unit :: s :-> () : s
unit = I UNIT

ifNone
  :: (s :-> s') -> (a : s :-> s') -> (Maybe a : s :-> s')
ifNone = iGenericIf IF_NONE

pair :: a : b : s :-> (a, b) : s
pair = I PAIR

car :: (a, b) : s :-> a : s
car = I CAR

cdr :: (a, b) : s :-> b : s
cdr = I CDR

unpair :: (a, b) : s :-> a : b : s
unpair = I UNPAIR

left :: forall a b s. KnownValue b => a : s :-> Either a b : s
left = I LEFT

right :: forall a b s. KnownValue a => b : s :-> Either a b : s
right = I RIGHT

ifLeft
  :: (a : s :-> s') -> (b : s :-> s') -> (Either a b : s :-> s')
ifLeft = iGenericIf IF_LEFT

nil :: KnownValue p => s :-> List p : s
nil = I NIL

cons :: a : List a : s :-> List a : s
cons = I CONS

ifCons
  :: (a : List a : s :-> s') -> (s :-> s') -> (List a : s :-> s')
ifCons = iGenericIf IF_CONS

size :: SizeOpHs c => c : s :-> Natural : s
size = I SIZE

emptySet :: (NiceComparable e) => s :-> Set e : s
emptySet = I EMPTY_SET

emptyMap :: (NiceComparable k, KnownValue v)
         => s :-> Map k v : s
emptyMap = I EMPTY_MAP

emptyBigMap :: (NiceComparable k, KnownValue v, NiceNoBigMap v)
            => s :-> BigMap k v : s
emptyBigMap = I EMPTY_BIG_MAP

map
  :: (MapOpHs c, IsoMapOpRes c b, KnownValue b, HasCallStack)
  => (MapOpInpHs c : s :-> b : s) -> (c : s :-> MapOpResHs c b : s)
map (iNonFailingCode -> action) = I (MAP action)

iter
  :: (IterOpHs c, HasCallStack)
  => (IterOpElHs c : s :-> s) -> (c : s :-> s)
iter (iNonFailingCode -> action) = I (ITER action)

mem :: MemOpHs c => MemOpKeyHs c : c : s :-> Bool : s
mem = I MEM

get
  :: (GetOpHs c, KnownValue (GetOpValHs c))
  => GetOpKeyHs c : c : s :-> Maybe (GetOpValHs c) : s
get = I GET

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

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

pairGet
  :: forall (n :: Nat) (pair :: Type) (s :: [Type]).
     ConstraintPairGetLorentz n pair
  => pair : s :-> PairGetHs (ToPeano n) pair : s
pairGet = I $ GETN $ toPeanoNatural' @n
  where
    _example :: '[ (Integer, Natural), () ] :-> '[ Integer, () ]
    _example = pairGet @1

update :: UpdOpHs c => UpdOpKeyHs c : UpdOpParamsHs c : c : s :-> c : s
update = I 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 = I GET_AND_UPDATE

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

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

pairUpdate
  :: forall (n :: Nat) (val :: Type) (pair :: Type) (s :: [Type]).
     (ConstraintPairUpdateLorentz n val pair)
  => val : pair : s :-> PairUpdateHs (ToPeano n) val pair : s
pairUpdate = I $ UPDATEN $ toPeanoNatural' @n
  where
    _example :: '[ MText, (Integer, Natural) ] :-> '[ (MText, Natural) ]
    _example = pairUpdate @1

if_ :: (s :-> s') -> (s :-> s') -> (Bool : s :-> s')
if_ = iGenericIf IF

loop :: (s :-> Bool : s) -> (Bool : s :-> s)
loop (iAnyCode -> b) = I (LOOP b)

loopLeft
  :: (a : s :-> Either a b : s) -> (Either a b : s :-> b : s)
loopLeft (iAnyCode -> b) = I (LOOP_LEFT b)

lambda
  :: ZipInstrs [i, o]
  => (IsNotInView => i :-> o) -> (s :-> WrappedLambda i o : s)
lambda instr = case zippingStack $ giveNotInView instr of
  I l -> I (LAMBDA $ VLam $ RfNormal l)
  FI l -> I (LAMBDA $ VLam $ RfAlwaysFails l)

exec :: a : Lambda a b : s :-> b : s
exec = I EXEC

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

apply
  :: forall a b c s. (NiceConstant a, KnownValue b)
  => a : Lambda (a, b) c : s :-> Lambda b c : s
apply = I $ APPLY \\ 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 : WrappedLambda (a : b) c : s :-> WrappedLambda b c : s
applicate = I APPLY \\ niceConstantEvi @a

dip :: forall a s s'. HasCallStack => (s :-> s') -> (a : s :-> a : s')
dip (iNonFailingCode -> a) = I (DIP 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 (iNonFailingCode -> a) = I (DIPN (toPeanoNatural @n) a)

dipN ::
  forall (n :: Nat) (inp :: [Type]) (out :: [Type]) (s :: [Type]) (s' :: [Type]).
  ( ConstraintDIPNLorentz (ToPeano n) inp out s s'
  ) => s :-> s' -> inp :-> out
dipN = dipNPeano @(ToPeano n)
  where
    _example :: '[ Integer, Integer, Integer ] :-> '[ Integer, Integer, Integer, () ]
    _example = dipN @3 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 = FI FAILWITH \\ niceConstantEvi @a

cast :: KnownValue a => (a : s :-> a : s)
cast = I CAST

pack
  :: forall a s. (NicePackedValue a)
  => a : s :-> Packed a : s
pack = I $ PACK \\ nicePackedValueEvi @a

unpack
  :: forall a s. (NiceUnpackedValue a)
  => Packed a : s :-> Maybe a : s
unpack = I $ UNPACK \\ niceUnpackedValueEvi @a

packRaw
  :: forall a s. (NicePackedValue a)
  => a : s :-> ByteString : s
packRaw = I $ PACK \\ nicePackedValueEvi @a

unpackRaw
  :: forall a s. (NiceUnpackedValue a)
  => ByteString : s :-> Maybe a : s
unpackRaw = I $ UNPACK \\ niceUnpackedValueEvi @a

concat :: ConcatOpHs c => c : c : s :-> c : s
concat = I CONCAT

concat' :: ConcatOpHs c => List c : s :-> c : s
concat' = I CONCAT'

slice
  :: (SliceOpHs c, KnownValue c)
  => Natural : Natural : c : s :-> Maybe c : s
slice = I SLICE

isNat :: Integer : s :-> Maybe Natural : s
isNat = I ISNAT

add
  :: ArithOpHs Add n m r
  => n : m : s :-> r : s
add = evalArithOpHs @Add

sub
  :: ArithOpHs Sub n m r
  => n : m : s :-> r : s
sub = evalArithOpHs @Sub

rsub
  :: ArithOpHs Sub n m r
  => m : n : s :-> r : s
rsub = swap # sub

subMutez :: Mutez : Mutez : s :-> Maybe Mutez : s
subMutez = I SUB_MUTEZ

rsubMutez :: Mutez : Mutez : s :-> Maybe Mutez : s
rsubMutez = swap # subMutez

mul
  :: ArithOpHs Mul n m r
  => n : m : s :-> r : s
mul = evalArithOpHs @Mul

ediv :: ArithOpHs EDiv n m r
     => n : m : s
     :-> r : s
ediv = evalArithOpHs @EDiv

abs :: UnaryArithOpHs Abs n => n : s :-> UnaryArithResHs Abs n : s
abs = evalUnaryArithOpHs @Abs

neg :: UnaryArithOpHs Neg n => n : s :-> UnaryArithResHs Neg n : s
neg = evalUnaryArithOpHs @Neg

lsl
  :: ArithOpHs Lsl n m r
  => n : m : s :-> r : s
lsl = evalArithOpHs @Lsl

lsr
  :: ArithOpHs Lsr n m r
  => n : m : s :-> r : s
lsr = evalArithOpHs @Lsr

or
  :: ArithOpHs Or n m r
  => n : m : s :-> r : s
or = evalArithOpHs @Or

and
  :: ArithOpHs And n m r
  => n : m : s :-> r : s
and = evalArithOpHs @And

xor
  :: (ArithOpHs Xor n m r)
  => n : m : s :-> r : s
xor = evalArithOpHs @Xor

not :: UnaryArithOpHs Not n => n : s :-> UnaryArithResHs Not n : s
not = evalUnaryArithOpHs @Not

compare :: NiceComparable n => n : n : s :-> Integer : s
compare = I COMPARE

eq0 :: UnaryArithOpHs Eq' n => n : s :-> UnaryArithResHs Eq' n : s
eq0 = evalUnaryArithOpHs @Eq'

neq0 :: UnaryArithOpHs Neq n => n : s :-> UnaryArithResHs Neq n : s
neq0 = evalUnaryArithOpHs @Neq

lt0 :: UnaryArithOpHs Lt n => n : s :-> UnaryArithResHs Lt n : s
lt0 = evalUnaryArithOpHs @Lt

gt0 :: UnaryArithOpHs Gt n => n : s :-> UnaryArithResHs Gt n : s
gt0 = evalUnaryArithOpHs @Gt

le0 :: UnaryArithOpHs Le n => n : s :-> UnaryArithResHs Le n : s
le0 = evalUnaryArithOpHs @Le

ge0 :: UnaryArithOpHs Ge n => n : s :-> UnaryArithResHs Ge n : s
ge0 = evalUnaryArithOpHs @Ge

int :: (ToIntegerArithOpHs i) => i : s :-> Integer : s
int = evalToIntOpHs

-- | Manual variation of @VIEW@ instruction.
-- It is pretty much like Michelson's @VIEW@, you must make sure that the compiler can
-- infer the argument and return types of the view.
--
-- In most cases prefer 'Lorentz.Macro.view' instead.
view'
  :: forall name ret arg s.
    (HasCallStack, KnownSymbol name, KnownValue arg, NiceViewable ret)
  => arg : Address : s :-> Maybe ret : s
view' = I $ VIEW (demoteViewName @name)
  \\ niceViewableEvi @ret

-- | Get a reference to the current contract.
--
-- Note that, similar to 'CONTRACT' instruction, in Michelson 'SELF' instruction
-- can accept an entrypoint as field annotation, and without annotation specified
-- it creates a @contract@ value which calls the default entrypoint.
--
-- This particular function carries the behaviour of @SELF@ before introduction
-- of lightweight entrypoints feature.
-- Thus the contract must __not__ have explicit "default" entrypoint for this to
-- work.
--
-- If you are going to call a specific entrypoint of the contract, see 'selfCalling'.
self
  :: forall p s.
      (NiceParameterFull p, ForbidExplicitDefaultEntrypoint p, IsNotInView)
  => s :-> ContractRef p : s
self = I (SELF $ sepcCallRootChecked @p) \\ 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, IsNotInView)
  => EntrypointRef mname
  -> s :-> ContractRef (GetEntrypointArgCustom p mname) : s
selfCalling epRef = I $
  withDict (niceParameterEvi @p) $
  case parameterEntrypointCallCustom @p epRef of
    epc@EntrypointCall{} -> SELF (SomeEpc epc)

-- | Get a reference to a contract by its address.
--
-- This instruction carries the behaviour of @CONTRACT@ before introduction
-- of lightweight entrypoints feature.
-- The contract must __not__ have explicit "default" entrypoint for this to work.
--
-- If you are going to call a specific entrypoint of the contract, see 'contractCalling'.
contract
  :: forall p vd addr s.
      ( NiceParameterFull p, ForbidExplicitDefaultEntrypoint p
      , ToTAddress_ p vd addr
      )
  => addr : s :-> Maybe (ContractRef p) : s
contract = I (CONTRACT epName) \\ niceParameterEvi @p
  where
    epName = sepcName (sepcCallRootChecked @p)

-- | Make a reference to a contract, maybe a specific entrypoint.
--
-- When calling this function, make sure that parameter type is known.
-- It's recommended that you supply 'TAddress' with a concrete parameter as the
-- stack argument.
contractCalling
  :: forall cp epRef epArg addr vd s.
     (HasEntrypointArg cp epRef epArg, ToTAddress_ cp vd addr)
  => epRef
  -> addr : s :-> Maybe (ContractRef epArg) : s
contractCalling epRef = I $
  case useHasEntrypointArg @cp @epRef @epArg epRef of
    (Dict, epName) -> CONTRACT 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 = contractCalling (TrustEpName 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 =
  I Nop # 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 =
  I (CONTRACT DefEpName) \\ niceParameterEvi @p

transferTokens
  :: forall p s. (NiceParameter p, IsNotInView)
  => p : Mutez : ContractRef p : s :-> Operation : s
transferTokens = I $ TRANSFER_TOKENS \\ niceParameterEvi @p

setDelegate :: IsNotInView => Maybe KeyHash : s :-> Operation : s
setDelegate = I SET_DELEGATE

createContract
  :: forall p g vd s. IsNotInView
  => Contract p g vd
  -> Maybe KeyHash : Mutez : g : s
  :-> Operation : TAddress p vd : s
createContract cntrc@Contract{} =
  I $ CREATE_CONTRACT (toMichelsonContract cntrc)
    \\ niceParameterEvi @p
    \\ niceStorageEvi @g

implicitAccount :: KeyHash : s :-> ContractRef () : s
implicitAccount = I IMPLICIT_ACCOUNT

now :: s :-> Timestamp : s
now = I NOW

minBlockTime :: s :-> Natural : s
minBlockTime = I MIN_BLOCK_TIME

amount :: s :-> Mutez : s
amount = I AMOUNT

balance :: s :-> Mutez : s
balance = I BALANCE

votingPower :: KeyHash : s :-> Natural : s
votingPower = I VOTING_POWER

totalVotingPower :: s :-> Natural : s
totalVotingPower = I TOTAL_VOTING_POWER

checkSignature :: BytesLike bs => PublicKey : TSignature bs : bs : s :-> Bool : s
checkSignature = I CHECK_SIGNATURE

sha256 :: BytesLike bs => bs : s :-> Hash Sha256 bs : s
sha256 = I SHA256

sha512 :: BytesLike bs => bs : s :-> Hash Sha512 bs : s
sha512 = I SHA512

blake2B :: BytesLike bs => bs : s :-> Hash Blake2b bs : s
blake2B = I BLAKE2B

sha3 :: BytesLike bs => bs : s :-> Hash Sha3 bs : s
sha3 = I SHA3

keccak :: BytesLike bs => bs : s :-> Hash Keccak bs : s
keccak = I KECCAK

hashKey :: PublicKey : s :-> KeyHash : s
hashKey = I HASH_KEY

pairingCheck :: [(Bls12381G1, Bls12381G2)] : s :-> Bool : s
pairingCheck = I PAIRING_CHECK

{-# WARNING source
    "Using `source` is considered a bad practice.\n\
\    Consider using `sender` instead until further investigation" #-}
source :: s :-> Address : s
source = I SOURCE

sender :: s :-> Address : s
sender = I SENDER

address :: ContractRef a : s :-> Address : s
address = I ADDRESS

chainId :: s :-> ChainId : s
chainId = I CHAIN_ID

level :: s :-> Natural : s
level = I LEVEL

selfAddress :: s :-> Address : s
selfAddress = I SELF_ADDRESS

never :: Never : s :-> s'
never = FI NEVER

ticket :: (NiceComparable a) => a : Natural : s :-> Ticket a : s
ticket = I TICKET

-- | Note: for more advanced helpers for tickets see "Lorentz.Tickets" module.
readTicket :: Ticket a : s :-> ReadTicket a : Ticket a : s
readTicket = I READ_TICKET

-- | Note: for more advanced helpers for tickets see "Lorentz.Tickets" module.
splitTicket :: Ticket a : (Natural, Natural) : s :-> Maybe (Ticket a, Ticket a) : s
splitTicket = I SPLIT_TICKET

-- | Version of 'splitTicket' with entries named.
splitTicketNamed
  :: forall n1 n2 a s.
     Ticket a : (n1 :! Natural, n2 :! Natural) : s
  :-> Maybe (n1 :! Ticket a, n2 :! Ticket a) : s
splitTicketNamed = I SPLIT_TICKET

-- | Note: for more advanced helpers for tickets see "Lorentz.Tickets" module.
joinTickets :: (Ticket a, Ticket a) : s :-> Maybe (Ticket a) : s
joinTickets = I JOIN_TICKETS

openChest :: ChestKey : Chest : Natural : s :-> OpenChest : s
openChest = I OPEN_CHEST

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

-- | Version of 'emit' that omits the type annotation, letting the runtime infer
-- it instead.
emitAuto :: forall t s. NicePackedValue t => FieldAnn -> t : s :-> Operation : s
emitAuto tag = emit' tag Nothing

emit'
  :: forall t s. NicePackedValue t
  => FieldAnn
  -> Maybe (Notes (ToT t))
  -> t : s :-> Operation : s
emit' tag mNotes = I $ EMIT tag mNotes \\ nicePackedValueEvi @t

-- | 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 (iNonFailingCode -> i) =
  I $ FrameInstr (Proxy @(ToTs s)) i
    \\ totsKnownLemma @i
    \\ totsKnownLemma @o
    \\ totsAppendLemma @i @s
    \\ 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 mkErr =
  dupN @3 # dupN @2 # mem #
  if_ (mkErr # failWith) 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 mkErr = dup # dip getAndUpdate # swap # ifNone drop (drop # mkErr # 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 = map