{-# OPTIONS_GHC -Wno-orphans #-}
module Lorentz.Expr
( Expr
, take
, unaryExpr
, ($:)
, binaryExpr
, (|+|)
, (|-|)
, (|*|)
, (|==|)
, (|/=|)
, (|<|)
, (|>|)
, (|<=|)
, (|>=|)
, (|&|)
, (|||)
, (|.|.|)
, (|^|)
, (|<<|)
, (|>>|)
, (|:|)
, (|@|)
, listE
) where
import Prelude (foldr)
import Lorentz.Arith
import Lorentz.Base
import Lorentz.Constraints
import Lorentz.Instr
import Lorentz.Macro
import Lorentz.Rebinded
import Lorentz.Value
import Michelson.Typed.Arith
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)
=> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Add a b)
|+| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Add a b)
(|+|) = (forall (s :: [*]). (a : b : s) :-> (ArithResHs Add a b : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Add 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) :-> (ArithResHs Add a b : s)
forall n m (s :: [*]).
ArithOpHs Add n m =>
(n : m : s) :-> (ArithResHs Add n m : s)
add
infixl 6 |-|
(|-|)
:: (ArithOpHs Sub a b)
=> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Sub a b)
|-| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Sub a b)
(|-|) = (forall (s :: [*]). (a : b : s) :-> (ArithResHs Sub a b : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Sub 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) :-> (ArithResHs Sub a b : s)
forall n m (s :: [*]).
ArithOpHs Sub n m =>
(n : m : s) :-> (ArithResHs Sub n m : s)
sub
infixl 7 |*|
(|*|)
:: (ArithOpHs Mul a b)
=> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Mul a b)
|*| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Mul a b)
(|*|) = (forall (s :: [*]). (a : b : s) :-> (ArithResHs Mul a b : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Mul 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) :-> (ArithResHs Mul a b : s)
forall n m (s :: [*]).
ArithOpHs Mul n m =>
(n : m : s) :-> (ArithResHs Mul n m : 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)
=> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs And a b)
|&| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs And a b)
(|&|) = (forall (s :: [*]). (a : b : s) :-> (ArithResHs And a b : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs And 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) :-> (ArithResHs And a b : s)
forall n m (s :: [*]).
ArithOpHs And n m =>
(n : m : s) :-> (ArithResHs And n m : s)
and
infixl 1 |||
(|||)
:: (ArithOpHs Or a b)
=> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Or a b)
||| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Or a b)
(|||) = (forall (s :: [*]). (a : b : s) :-> (ArithResHs Or a b : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Or 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) :-> (ArithResHs Or a b : s)
forall n m (s :: [*]).
ArithOpHs Or n m =>
(n : m : s) :-> (ArithResHs Or n m : s)
or
infixl 1 |.|.|
(|.|.|)
:: (ArithOpHs Or a b)
=> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Or a b)
|.|.| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Or a b)
(|.|.|) = (forall (s :: [*]). (a : b : s) :-> (ArithResHs Or a b : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Or 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) :-> (ArithResHs Or a b : s)
forall n m (s :: [*]).
ArithOpHs Or n m =>
(n : m : s) :-> (ArithResHs Or n m : s)
or
infixl 3 |^|
(|^|)
:: (ArithOpHs Xor a b)
=> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Xor a b)
|^| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Xor a b)
(|^|) = (forall (s :: [*]). (a : b : s) :-> (ArithResHs Xor a b : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Xor 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) :-> (ArithResHs Xor a b : s)
forall n m (s :: [*]).
ArithOpHs Xor n m =>
(n : m : s) :-> (ArithResHs Xor n m : s)
xor
infix 8 |<<|
(|<<|)
:: (ArithOpHs Lsl a b)
=> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Lsl a b)
|<<| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Lsl a b)
(|<<|) = (forall (s :: [*]). (a : b : s) :-> (ArithResHs Lsl a b : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Lsl 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) :-> (ArithResHs Lsl a b : s)
forall n m (s :: [*]).
ArithOpHs Lsl n m =>
(n : m : s) :-> (ArithResHs Lsl n m : s)
lsl
infix 8 |>>|
(|>>|)
:: (ArithOpHs Lsr a b)
=> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Lsr a b)
|>>| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Lsr a b)
(|>>|) = (forall (s :: [*]). (a : b : s) :-> (ArithResHs Lsr a b : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Lsr 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) :-> (ArithResHs Lsr a b : s)
forall n m (s :: [*]).
ArithOpHs Lsr n m =>
(n : m : s) :-> (ArithResHs Lsr n m : 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
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