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

{-# OPTIONS_GHC -Wno-orphans #-}

{- | Evaluation of expressions.

Stack-based languages allow convenient expressions evaluation, for that
we just need binary instructions in infix notation, not in Polish postfix
notation that 'add' and other primitives provide. Compare:

> push 1; push 2; push 3; push 4; mul; rsub; add

vs

> push 1 |+| push 2 |-| push 3 |*| push 4

In these expressions each atom is some instruction providing a single value
on top of the stack, for example:

@
nthOdd :: Lambda Natural Natural
nthOdd = take |*| push @Natural 2 |+| push @Natural 1
@

For binary operations we provide the respective operators. Unary operations can
be lifted with 'unaryExpr':

@
implication :: [Bool, Bool] :-> '[Bool]
implication = unaryExpr not take |.|.| take
@

or with its alias in form of an operator:

@
implication :: [Bool, Bool] :-> '[Bool]
implication = not $: take |.|.| take
@

Stack changes are propagated from left to right. If an atom consumes an element
at the top of the stack, the next atom will accept only the remainder of the
stack.

In most cases you should prefer providing named variables to the formulas in
order to avoid messing up with the arguments:

@
f :: ("a" :! Natural) : ("b" :! Natural) : ("c" :! Natural) : s :-> Integer : s
f = fromNamed #a |+| fromNamed #b |-| fromNamed #c
@

Instead of putting all the elements on the stack upon applying the formula,
you may find it more convenient to evaluate most of the arguments right within
the formula:

@
withinRange
  :: Natural : a : b : c : ("config" :! Config) : s
  :-> Bool : a : b : c : ("config" :! Config) : s
withinRange =
  dup  |>=| do{ dupL #config; toField #minBound } |&|
  take |<=| do{ dupL #config; toField #maxBound }
@

-}
module Lorentz.Expr
  ( Expr
  , take
  , unaryExpr
  , ($:)
  , binaryExpr
  , (|+|)
  , (|-|)
  , (|*|)
  , (|==|)
  , (|/=|)
  , (|<|)
  , (|>|)
  , (|<=|)
  , (|>=|)
  , (|&|)
  , (|||)
  , (|.|.|)
  , (|^|)
  , (|<<|)
  , (|>>|)
  , (|:|)
  , pairE
  , (|@|)
  , listE
  , transferTokensE
  ) where

import Prelude (foldr, uncurry)

import Lorentz.Arith
import Lorentz.Base
import Lorentz.Constraints
import Lorentz.Instr
import Lorentz.Macro
import Lorentz.Rebinded
import Lorentz.Value
import Morley.Michelson.Typed.Arith
import Morley.Util.Named

-- | Expression is just an instruction accepting stack @inp@ and producing
-- stack @out@ with evaluation result @res@ at the top.

-- Stack flows from left to right, so e.g. @ fromNamed #a |<| fromNamed #b @
-- consumes first the value with label @a@ from the stack's top, then the value
-- with label @b@.
type Expr inp out res = inp :-> res : out

{- Note on the type alias ↑

It was pretty difficult to decide whether 'Expr' should be a newtype or type
alias.

Pros of newtype:
* It is safer and clearer.
* It allows defining such 'IsLabel name (Expr ...)' instance that would allow
  writing @ #a |<| #b @ (which should consume values asserting their labels).

It would /not/ allow writing @5 :: Expr ... Natural@, because this way we lose
GHC checks on passing out-of-bounds numbers like @(-1) :: Natural@.

Cons:
* Any non-trivial operation like @push@, @dupL@ and others will require a
  wrapper.

To make all this as simple to use and understand as possible, we used a
type alias.
-}

-- | An expression producing 'Bool' can be placed as condition to 'if'.
instance (i ~ arg, o ~ argl, o ~ argr, r ~ Bool, outb ~ out) =>
         IsCondition (Expr i o r) arg argl argr outb out where
  ifThenElse :: Expr i o r -> (argl :-> outb) -> (argr :-> outb) -> arg :-> out
ifThenElse Expr i o r
e argl :-> outb
l argr :-> outb
r = Expr i o r
e Expr i o r -> ((r : o) :-> outb) -> i :-> outb
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (argl :-> outb) -> (argl :-> outb) -> (Bool : argl) :-> outb
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
if_ argl :-> outb
l argl :-> outb
argr :-> outb
r

-- | Consume an element at the top of stack. This is just an alias for @nop@.
take :: Expr (a : s) s a
take :: Expr (a : s) s a
take = Expr (a : s) s a
forall (s :: [*]). s :-> s
nop

-- | Lift an instruction to an unary operation on expressions.
unaryExpr
  :: (forall s. a : s :-> r : s)
  -> Expr s0 s1 a -> Expr s0 s1 r
unaryExpr :: (forall (s :: [*]). (a : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s0 s1 r
unaryExpr forall (s :: [*]). (a : s) :-> (r : s)
op Expr s0 s1 a
a = Expr s0 s1 a
a Expr s0 s1 a -> ((a : s1) :-> (r : s1)) -> Expr s0 s1 r
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : s1) :-> (r : s1)
forall (s :: [*]). (a : s) :-> (r : s)
op

-- | An alias for 'unaryExpr'.
infixr 9 $:
($:)
  :: (forall s. a : s :-> r : s)
  -> Expr s0 s1 a -> Expr s0 s1 r
$: :: (forall (s :: [*]). (a : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s0 s1 r
($:) = (forall (s :: [*]). (a : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s0 s1 r
forall a r (s0 :: [*]) (s1 :: [*]).
(forall (s :: [*]). (a : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s0 s1 r
unaryExpr

-- | Lift an instruction to a binary operation on expressions.
binaryExpr
  :: (forall s. a : b : s :-> r : s)
  -> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr :: (forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : b : s) :-> (r : s)
op Expr s0 s1 a
l Expr s1 s2 b
r = Expr s0 s1 a
l Expr s0 s1 a -> ((a : s1) :-> (a : b : s2)) -> s0 :-> (a : b : s2)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Expr s1 s2 b -> (a : s1) :-> (a : b : s2)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip Expr s1 s2 b
r (s0 :-> (a : b : s2))
-> ((a : b : s2) :-> (r : s2)) -> Expr s0 s2 r
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : b : s2) :-> (r : s2)
forall (s :: [*]). (a : b : s) :-> (r : s)
op

-- | Expressions addition.
infixl 6 |+|
(|+|)
  :: (ArithOpHs Add a b r)
  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
|+| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
(|+|) = (forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : b : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add

-- | Expressions subtraction.
infixl 6 |-|
(|-|)
  :: (ArithOpHs Sub a b r)
  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
|-| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
(|-|) = (forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : b : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub

-- | Expressions multiplication.
infixl 7 |*|
(|*|)
  :: (ArithOpHs Mul a b r)
  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
|*| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
(|*|) = (forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : b : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul

-- | Expressions comparison.
infix 4 |==|
infix 4 |/=|
infix 4 |<|
infix 4 |>|
infix 4 |<=|
infix 4 |>=|
(|==|), (|/=|), (|<|), (|>|), (|>=|), (|<=|)
  :: (NiceComparable a)
  => Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
|==| :: Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
(|==|) = (forall (s :: [*]). (a : a : s) :-> (Bool : s))
-> Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : a : s) :-> (Bool : s)
forall n (s :: [*]). NiceComparable n => (n : n : s) :-> (Bool : s)
eq
|/=| :: Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
(|/=|) = (forall (s :: [*]). (a : a : s) :-> (Bool : s))
-> Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : a : s) :-> (Bool : s)
forall n (s :: [*]). NiceComparable n => (n : n : s) :-> (Bool : s)
neq
|<| :: Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
(|<|) = (forall (s :: [*]). (a : a : s) :-> (Bool : s))
-> Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : a : s) :-> (Bool : s)
forall n (s :: [*]). NiceComparable n => (n : n : s) :-> (Bool : s)
lt
|>| :: Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
(|>|) = (forall (s :: [*]). (a : a : s) :-> (Bool : s))
-> Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : a : s) :-> (Bool : s)
forall n (s :: [*]). NiceComparable n => (n : n : s) :-> (Bool : s)
gt
|<=| :: Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
(|<=|) = (forall (s :: [*]). (a : a : s) :-> (Bool : s))
-> Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : a : s) :-> (Bool : s)
forall n (s :: [*]). NiceComparable n => (n : n : s) :-> (Bool : s)
le
|>=| :: Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
(|>=|) = (forall (s :: [*]). (a : a : s) :-> (Bool : s))
-> Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : a : s) :-> (Bool : s)
forall n (s :: [*]). NiceComparable n => (n : n : s) :-> (Bool : s)
ge

-- | Bitwise/logical @AND@ on expressions.
infixl 2 |&|
(|&|)
  :: (ArithOpHs And a b r)
  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
|&| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
(|&|) = (forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : b : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs And n m r =>
(n : m : s) :-> (r : s)
and

-- | Bitwise/logical @OR@ on expressions.
--
-- In case you find this operator looking weird, see '|.|.|'
infixl 1 |||
(|||)
  :: (ArithOpHs Or a b r)
  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
||| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
(|||) = (forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : b : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Or n m r =>
(n : m : s) :-> (r : s)
or

-- | An alias for '|||'.
infixl 1 |.|.|
(|.|.|)
  :: (ArithOpHs Or a b r)
  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
|.|.| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
(|.|.|) = (forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : b : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Or n m r =>
(n : m : s) :-> (r : s)
or

-- | Bitwise/logical @XOR@ on expressions.
infixl 3 |^|
(|^|)
  :: (ArithOpHs Xor a b r)
  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
|^| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
(|^|) = (forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : b : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Xor n m r =>
(n : m : s) :-> (r : s)
xor

-- | Left shift on expressions.
infix 8 |<<|
(|<<|)
  :: (ArithOpHs Lsl a b r)
  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
|<<| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
(|<<|) = (forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : b : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Lsl n m r =>
(n : m : s) :-> (r : s)
lsl

-- | Right shift on expressions.
infix 8 |>>|
(|>>|)
  :: (ArithOpHs Lsr a b r)
  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
|>>| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
(|>>|) = (forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : b : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Lsr n m r =>
(n : m : s) :-> (r : s)
lsr

-- | 'cons' on expressions.
--
-- @
-- one :: a : s :-> [a] : s
-- one = take |:| nil
-- @
infix 1 |:|
(|:|) :: Expr s0 s1 a -> Expr s1 s2 [a] -> Expr s0 s2 [a]
|:| :: Expr s0 s1 a -> Expr s1 s2 [a] -> Expr s0 s2 [a]
(|:|) = (forall (s :: [*]). (a : [a] : s) :-> ([a] : s))
-> Expr s0 s1 a -> Expr s1 s2 [a] -> Expr s0 s2 [a]
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : [a] : s) :-> ([a] : s)
forall a (s :: [*]). (a : List a : s) :-> (List a : s)
cons

-- | Construct a simple pair.
--
-- @
-- trivialContract :: ((), storage) :-> ([Operation], Storage)
-- trivialContract = nil |@| cdr
-- @
--
-- This is useful as pair appears even in simple contracts.
-- For more advanced types, use 'Lorentz.ADT.constructT'.
infix 0 |@|
(|@|) :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (a, b)
|@| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (a, b)
(|@|) = (forall (s :: [*]). (a : b : s) :-> ((a, b) : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (a, b)
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : b : s) :-> ((a, b) : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair

-- | An alias for '|@|'.
--
-- @
-- trivialContract :: ((), storage) :-> ([Operation], Storage)
-- trivialContract =
--   pairE
--     ( nil
--     , cdr
--     )
-- @
pairE :: (Expr s0 s1 a, Expr s1 s2 b) -> Expr s0 s2 (a, b)
pairE :: (Expr s0 s1 a, Expr s1 s2 b) -> Expr s0 s2 (a, b)
pairE = (Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (a, b))
-> (Expr s0 s1 a, Expr s1 s2 b) -> Expr s0 s2 (a, b)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (a, b)
forall (s0 :: [*]) (s1 :: [*]) a (s2 :: [*]) b.
Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (a, b)
(|@|)

-- | Construct a list given the constructor for each element.
listE :: KnownValue a => [Expr s s a] -> Expr s s [a]
listE :: [Expr s s a] -> Expr s s [a]
listE = (Element [Expr s s a] -> Expr s s [a] -> Expr s s [a])
-> Expr s s [a] -> [Expr s s a] -> Expr s s [a]
forall t b. Container t => (Element t -> b -> b) -> b -> t -> b
foldr (\Element [Expr s s a]
pushElem Expr s s [a]
pushRec -> Element [Expr s s a]
Expr s s a
pushElem Expr s s a -> ((a : s) :-> (a : [a] : s)) -> s :-> (a : [a] : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Expr s s [a] -> (a : s) :-> (a : [a] : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip Expr s s [a]
pushRec (s :-> (a : [a] : s))
-> ((a : [a] : s) :-> ([a] : s)) -> Expr s s [a]
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : [a] : s) :-> ([a] : s)
forall a (s :: [*]). (a : List a : s) :-> (List a : s)
cons) Expr s s [a]
forall p (s :: [*]). KnownValue p => s :-> (List p : s)
nil

-- | Version of 'transferTokens' instruction that accepts
-- all the arguments as expressions.
--
-- @
-- transferTokensE
--   ! #arg L.unit
--   ! #amount (push zeroMutez)
--   ! #contract take
--   |:| nil
-- @
--
-- You can provide arguments in arbitrary order, but direction of stack changes
-- flow is fixed: stack change in @arg@ expression affects stack available in
-- @amount@ expression, and stack changes in @amount@ expression affect
-- stack changes in @contract@ expression.
transferTokensE
  :: (NiceParameter p)
  => ("arg" :! Expr s0 s1 p)
  -> ("amount" :! Expr s1 s2 Mutez)
  -> ("contract" :! Expr s2 s3 (ContractRef p))
  -> Expr s0 s3 Operation
transferTokensE :: ("arg" :! Expr s0 s1 p)
-> ("amount" :! Expr s1 s2 Mutez)
-> ("contract" :! Expr s2 s3 (ContractRef p))
-> Expr s0 s3 Operation
transferTokensE (N Expr s0 s1 p
paramE)
                (N Expr s1 s2 Mutez
amountE)
                (N Expr s2 s3 (ContractRef p)
contractE) =
  Expr s0 s1 p
paramE Expr s0 s1 p
-> ((p : s1) :-> (p : Mutez : ContractRef p : s3))
-> s0 :-> (p : Mutez : ContractRef p : s3)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s1 :-> (Mutez : ContractRef p : s3))
-> (p : s1) :-> (p : Mutez : ContractRef p : s3)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Expr s1 s2 Mutez
amountE Expr s1 s2 Mutez
-> ((Mutez : s2) :-> (Mutez : ContractRef p : s3))
-> s1 :-> (Mutez : ContractRef p : s3)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Expr s2 s3 (ContractRef p)
-> (Mutez : s2) :-> (Mutez : ContractRef p : s3)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip Expr s2 s3 (ContractRef p)
contractE) (s0 :-> (p : Mutez : ContractRef p : s3))
-> ((p : Mutez : ContractRef p : s3) :-> (Operation : s3))
-> Expr s0 s3 Operation
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (p : Mutez : ContractRef p : s3) :-> (Operation : s3)
forall p (s :: [*]).
NiceParameter p =>
(p : Mutez : ContractRef p : s) :-> (Operation : s)
transferTokens