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

{-# 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
  , createContractE
  , viewE
  ) where

import Prelude (HasCallStack, foldr, uncurry, ($))

import Lorentz.Arith
import Lorentz.Base
import Lorentz.Constraints
import Lorentz.CustomArith
import Lorentz.Errors
import Lorentz.Instr
import Lorentz.Macro
import Lorentz.Rebinded
import Lorentz.Value
import Lorentz.ViewBase
import Morley.Michelson.Typed.Arith
import Morley.Util.Named
import Morley.Util.TypeLits

-- | 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 :: forall a (s :: [*]). Expr (a : s) s a
take = (a : s) :-> (a : s)
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 a r (s0 :: [*]) (s1 :: [*]).
(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)) -> s0 :-> (r : s1)
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 a r (s0 :: [*]) (s1 :: [*]).
(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 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)
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)) -> s0 :-> (r : s2)
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
|+| :: forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
ArithOpHs Add a b 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
|-| :: forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
ArithOpHs Sub a b 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
|*| :: forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
ArithOpHs Mul a b 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
|==| :: forall a (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
NiceComparable a =>
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
|/=| :: forall a (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
NiceComparable a =>
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
|<| :: forall a (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
NiceComparable a =>
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
|>| :: forall a (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
NiceComparable a =>
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
|<=| :: forall a (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
NiceComparable a =>
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
|>=| :: forall a (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
NiceComparable a =>
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
|&| :: forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
ArithOpHs And a b 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
||| :: forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
ArithOpHs Or a b 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
|.|.| :: forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
ArithOpHs Or a b 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
|^| :: forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
ArithOpHs Xor a b 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
|<<| :: forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
ArithOpHs Lsl a b 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
|>>| :: forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
ArithOpHs Lsr a b 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
-- @
infixr 1 |:|
(|:|) :: Expr s0 s1 a -> Expr s1 s2 [a] -> Expr s0 s2 [a]
|:| :: forall (s0 :: [*]) (s1 :: [*]) a (s2 :: [*]).
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'.
infixr 0 |@|
(|@|) :: 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)
(|@|) = (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

-- | Construct a 'Rational' value from a given nominator and denominator.
-- In case denominator is 0, fails with custom exception.
infixl 7 |%!|
(|%!|) :: Expr s0 s1 Integer -> Expr s1 s2 Natural -> Expr s0 s2 Rational
|%!| :: forall (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
Expr s0 s1 Integer -> Expr s1 s2 Natural -> Expr s0 s2 Rational
(|%!|) = (forall (s :: [*]). (Integer : Natural : s) :-> (Rational : s))
-> Expr s0 s1 Integer -> Expr s1 s2 Natural -> Expr s0 s2 Rational
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 :: [*]). (Integer : Natural : s) :-> (Rational : s))
 -> Expr s0 s1 Integer -> Expr s1 s2 Natural -> Expr s0 s2 Rational)
-> (forall (s :: [*]). (Integer : Natural : s) :-> (Rational : s))
-> Expr s0 s1 Integer
-> Expr s1 s2 Natural
-> Expr s0 s2 Rational
forall a b. (a -> b) -> a -> b
$ (forall (s0 :: [*]).
 ErrInstr (("numerator" :! Integer, "denominator" :! Natural) : s0))
-> (Integer : Natural : s) :-> (Rational : s)
forall (s :: [*]).
(forall (s0 :: [*]).
 ErrInstr (("numerator" :! Integer, "denominator" :! Natural) : s0))
-> (Integer : Natural : s) :-> (Rational : s)
mkRational_ (Label "zero_denominator"
-> (("numerator" :! Integer, "denominator" :! Natural) : s0)
   :-> serr
forall (tag :: Symbol) err (s :: [*]) (any :: [*]).
(MustHaveErrorArg tag (MText, err), CustomErrorHasDoc tag,
 KnownError err) =>
Label tag -> (err : s) :-> any
failCustom IsLabel "zero_denominator" (Label "zero_denominator")
Label "zero_denominator"
#zero_denominator)

-- | 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 :: forall (s0 :: [*]) (s1 :: [*]) a (s2 :: [*]) b.
(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 :: forall a (s :: [*]). KnownValue a => [Expr s s a] -> Expr s s [a]
listE = (Element [Expr s s a]
 -> (s :-> (List a : s)) -> s :-> (List a : s))
-> (s :-> (List a : s)) -> [Expr s s a] -> s :-> (List a : s)
forall t b. Container t => (Element t -> b -> b) -> b -> t -> b
foldr (\Element [Expr s s a]
pushElem s :-> (List a : s)
pushRec -> Element [Expr s s a]
Expr s s a
pushElem Expr s s a
-> ((a : s) :-> (a : List a : s)) -> s :-> (a : List a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> (List a : s)) -> (a : s) :-> (a : List a : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip s :-> (List a : s)
pushRec (s :-> (a : List a : s))
-> ((a : List a : s) :-> (List a : s)) -> s :-> (List a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : List a : s) :-> (List a : s)
forall a (s :: [*]). (a : List a : s) :-> (List a : s)
cons) s :-> (List a : s)
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, IsNotInView)
  => ("arg" :! Expr s0 s1 p)
  -> ("amount" :! Expr s1 s2 Mutez)
  -> ("contract" :! Expr s2 s3 (ContractRef p))
  -> Expr s0 s3 Operation
transferTokensE :: forall p (s0 :: [*]) (s1 :: [*]) (s2 :: [*]) (s3 :: [*]).
(NiceParameter p, IsNotInView) =>
("arg" :! Expr s0 s1 p)
-> ("amount" :! Expr s1 s2 Mutez)
-> ("contract" :! Expr s2 s3 (ContractRef p))
-> Expr s0 s3 Operation
transferTokensE (Name "arg" -> ("arg" :! Expr s0 s1 p) -> Expr s0 s1 p
forall (name :: Symbol) a. Name name -> (name :! a) -> a
arg IsLabel "arg" (Name "arg")
Name "arg"
#arg -> Expr s0 s1 p
paramE)
                (Name "amount" -> ("amount" :! Expr s1 s2 Mutez) -> Expr s1 s2 Mutez
forall (name :: Symbol) a. Name name -> (name :! a) -> a
arg IsLabel "amount" (Name "amount")
Name "amount"
#amount -> Expr s1 s2 Mutez
amountE)
                (Name "contract"
-> ("contract" :! Expr s2 s3 (ContractRef p))
-> Expr s2 s3 (ContractRef p)
forall (name :: Symbol) a. Name name -> (name :! a) -> a
arg IsLabel "contract" (Name "contract")
Name "contract"
#contract -> 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))
-> s0 :-> (Operation : s3)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (p : Mutez : ContractRef p : s3) :-> (Operation : s3)
forall p (s :: [*]).
(NiceParameter p, IsNotInView) =>
(p : Mutez : ContractRef p : s) :-> (Operation : s)
transferTokens

-- | Version of 'createContract' instruction that accepts
-- all the arguments as expressions.
--
-- @
-- createContractE
--   ! #delegate none
--   ! #balance (push zeroMutez)
--   ! #storage unit
--   ! #contract myContract
-- @
--
-- Note that this returns an operation, and pushes the address of the newly
-- created contract as a side-effect.
createContractE
  :: IsNotInView
  => ("delegate" :! Expr s0 s1 (Maybe KeyHash))
  -> ("balance" :! Expr s1 s2 Mutez)
  -> ("storage" :! Expr s2 s3 st)
  -> ("contract" :! Contract p st vd)
  -> Expr s0 (TAddress p vd : s3) Operation
createContractE :: forall (s0 :: [*]) (s1 :: [*]) (s2 :: [*]) (s3 :: [*]) st p vd.
IsNotInView =>
("delegate" :! Expr s0 s1 (Maybe KeyHash))
-> ("balance" :! Expr s1 s2 Mutez)
-> ("storage" :! Expr s2 s3 st)
-> ("contract" :! Contract p st vd)
-> Expr s0 (TAddress p vd : s3) Operation
createContractE (Name "delegate"
-> ("delegate" :! Expr s0 s1 (Maybe KeyHash))
-> Expr s0 s1 (Maybe KeyHash)
forall (name :: Symbol) a. Name name -> (name :! a) -> a
arg IsLabel "delegate" (Name "delegate")
Name "delegate"
#delegate -> Expr s0 s1 (Maybe KeyHash)
delegatorE)
                (Name "balance"
-> ("balance" :! Expr s1 s2 Mutez) -> Expr s1 s2 Mutez
forall (name :: Symbol) a. Name name -> (name :! a) -> a
arg IsLabel "balance" (Name "balance")
Name "balance"
#balance -> Expr s1 s2 Mutez
balanceE)
                (Name "storage" -> ("storage" :! Expr s2 s3 st) -> Expr s2 s3 st
forall (name :: Symbol) a. Name name -> (name :! a) -> a
arg IsLabel "storage" (Name "storage")
Name "storage"
#storage -> Expr s2 s3 st
storageE)
                (Name "contract"
-> ("contract" :! Contract p st vd) -> Contract p st vd
forall (name :: Symbol) a. Name name -> (name :! a) -> a
arg IsLabel "contract" (Name "contract")
Name "contract"
#contract -> Contract p st vd
contract') =
  Expr s0 s1 (Maybe KeyHash)
delegatorE Expr s0 s1 (Maybe KeyHash)
-> ((Maybe KeyHash : s1) :-> (Maybe KeyHash : Mutez : st : s3))
-> s0 :-> (Maybe KeyHash : Mutez : st : s3)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s1 :-> (Mutez : st : s3))
-> (Maybe KeyHash : s1) :-> (Maybe KeyHash : Mutez : st : s3)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Expr s1 s2 Mutez
balanceE Expr s1 s2 Mutez
-> ((Mutez : s2) :-> (Mutez : st : s3)) -> s1 :-> (Mutez : st : s3)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Expr s2 s3 st -> (Mutez : s2) :-> (Mutez : st : s3)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip Expr s2 s3 st
storageE) (s0 :-> (Maybe KeyHash : Mutez : st : s3))
-> ((Maybe KeyHash : Mutez : st : s3)
    :-> (Operation : TAddress p vd : s3))
-> s0 :-> (Operation : TAddress p vd : s3)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Contract p st vd
-> (Maybe KeyHash : Mutez : st : s3)
   :-> (Operation : TAddress p vd : s3)
forall p g vd (s :: [*]).
IsNotInView =>
Contract p g vd
-> (Maybe KeyHash : Mutez : g : s)
   :-> (Operation : TAddress p vd : s)
createContract Contract p st vd
contract'

-- | Version of 'view' instruction that accepts all the arguments as expressions.
--
-- @
-- viewE @"myview"
--   ! #arg (push zeroMutez)
--   ! #address (push addr)
-- @
viewE
  :: forall name arg ret p vd s0 s1 s2.
    ( HasCallStack, KnownSymbol name, KnownValue arg
    , NiceViewable ret, HasView vd name arg ret
    )
  => ("arg" :! Expr s0 s1 arg)
  -> ("address" :! Expr s1 s2 (TAddress p vd))
  -> Expr s0 s2 ret
viewE :: forall (name :: Symbol) arg ret p vd (s0 :: [*]) (s1 :: [*])
       (s2 :: [*]).
(HasCallStack, KnownSymbol name, KnownValue arg, NiceViewable ret,
 HasView vd name arg ret) =>
("arg" :! Expr s0 s1 arg)
-> ("address" :! Expr s1 s2 (TAddress p vd)) -> Expr s0 s2 ret
viewE (Name "arg" -> ("arg" :! Expr s0 s1 arg) -> Expr s0 s1 arg
forall (name :: Symbol) a. Name name -> (name :! a) -> a
arg IsLabel "arg" (Name "arg")
Name "arg"
#arg -> Expr s0 s1 arg
argE) (Name "address"
-> ("address" :! Expr s1 s2 (TAddress p vd))
-> Expr s1 s2 (TAddress p vd)
forall (name :: Symbol) a. Name name -> (name :! a) -> a
arg IsLabel "address" (Name "address")
Name "address"
#address -> Expr s1 s2 (TAddress p vd)
addrE) =
  Expr s0 s1 arg
argE Expr s0 s1 arg
-> ((arg : s1) :-> (arg : TAddress p vd : s2))
-> s0 :-> (arg : TAddress p vd : s2)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Expr s1 s2 (TAddress p vd)
-> (arg : s1) :-> (arg : TAddress p vd : s2)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip Expr s1 s2 (TAddress p vd)
addrE (s0 :-> (arg : TAddress p vd : s2))
-> ((arg : TAddress p vd : s2) :-> (ret : s2)) -> s0 :-> (ret : s2)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall (name :: Symbol) arg ret p vd (s :: [*]).
(HasCallStack, KnownSymbol name, KnownValue arg, NiceViewable ret,
 HasView vd name arg ret) =>
(arg : TAddress p vd : s) :-> (ret : s)
view @name