{-# OPTIONS_GHC -Wno-orphans #-}
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
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
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
take :: Expr (a : s) s a
take :: Expr (a : s) s a
take = Expr (a : s) s a
forall (s :: [*]). s :-> s
nop
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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)
(|@|)
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
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