{-# OPTIONS_GHC -Wno-orphans #-}
module Lorentz.Expr
( Expr
, take
, unaryExpr
, ($:)
, binaryExpr
, (|+|)
, (|-|)
, (|*|)
, (|==|)
, (|/=|)
, (|<|)
, (|>|)
, (|<=|)
, (|>=|)
, (|&|)
, (|||)
, (|.|.|)
, (|^|)
, (|<<|)
, (|>>|)
, (|:|)
, pairE
, (|@|)
, (|%!|)
, listE
, transferTokensE
, createContractE
, viewE
) where
import Prelude (HasCallStack, foldr, uncurry, ($), type (~))
import Lorentz.Arith
import Lorentz.Base
import Lorentz.Constraints
import Lorentz.CustomArith
import Lorentz.Errors
import Lorentz.Instr
import Lorentz.Macro
import Lorentz.Rebound
import Lorentz.Value
import Lorentz.ViewBase
import Morley.Michelson.Typed.Arith
import Morley.Util.Named
import Morley.Util.TypeLits
type Expr inp out res = inp :-> res : out
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
arg :-> (r : o)
e (arg :-> (r : o)) -> ((r : o) :-> out) -> arg :-> out
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (o :-> out) -> (o :-> out) -> (Bool : o) :-> out
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
if_ o :-> out
argl :-> outb
l o :-> out
argr :-> outb
r
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
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
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
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
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 (a : b : s) :-> (r : s)
forall (s :: [*]). (a : b : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
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 (a : b : s) :-> (r : s)
forall (s :: [*]). (a : b : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub
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 (a : b : s) :-> (r : s)
forall (s :: [*]). (a : b : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
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 (a : a : s) :-> (Bool : s)
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 (a : a : s) :-> (Bool : s)
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 (a : a : s) :-> (Bool : s)
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 (a : a : s) :-> (Bool : s)
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 (a : a : s) :-> (Bool : s)
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 (a : a : s) :-> (Bool : s)
forall (s :: [*]). (a : a : s) :-> (Bool : s)
forall n (s :: [*]). NiceComparable n => (n : n : s) :-> (Bool : s)
ge
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 (a : b : s) :-> (r : s)
forall (s :: [*]). (a : b : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs And n m r =>
(n : m : s) :-> (r : s)
and
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 (a : b : s) :-> (r : s)
forall (s :: [*]). (a : b : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Or n m r =>
(n : m : s) :-> (r : s)
or
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 (a : b : s) :-> (r : s)
forall (s :: [*]). (a : b : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Or n m r =>
(n : m : s) :-> (r : s)
or
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 (a : b : s) :-> (r : s)
forall (s :: [*]). (a : b : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Xor n m r =>
(n : m : s) :-> (r : s)
xor
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 (a : b : s) :-> (r : s)
forall (s :: [*]). (a : b : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Lsl n m r =>
(n : m : s) :-> (r : s)
lsl
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 (a : b : s) :-> (r : s)
forall (s :: [*]). (a : b : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Lsr n m r =>
(n : m : s) :-> (r : s)
lsr
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 (a : [a] : s) :-> ([a] : s)
forall (s :: [*]). (a : [a] : s) :-> ([a] : s)
forall a (s :: [*]). (a : List a : s) :-> (List a : s)
cons
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 (a : b : s) :-> ((a, b) : s)
forall (s :: [*]). (a : b : s) :-> ((a, b) : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair
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 :: [*]) (serr :: [*]).
(("numerator" :! Integer, "denominator" :! Natural) : s0) :-> serr)
-> (Integer : Natural : s) :-> (Rational : s)
forall (s :: [*]).
(forall (s0 :: [*]) (serr :: [*]).
(("numerator" :! Integer, "denominator" :! Natural) : s0) :-> serr)
-> (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 Label "zero_denominator"
#zero_denominator)
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)
(|@|)
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] -> 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
forall b.
(Element [Expr s s a] -> b -> b) -> b -> [Expr s s a] -> 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
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 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 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 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
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 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 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 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 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'
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 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 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