module Lorentz.Rebinded
( (>>)
, pure
, return
, ifThenElse
, Condition (..)
, (<.)
, (>.)
, (<=.)
, (>=.)
, (==.)
, (/=.)
, keepIfArgs
, fromInteger
, fromString
, fromLabel
, negate
) where
import Prelude hiding (drop, swap, (>>), (>>=))
import Named ((:!))
import Lorentz.Arith
import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Instr
import Lorentz.Macro
import Michelson.Typed.Arith
import Util.Label (Label)
(>>) :: (a :-> b) -> (b :-> c) -> (a :-> c)
>> :: (a :-> b) -> (b :-> c) -> a :-> c
(>>) = (a :-> b) -> (b :-> c) -> a :-> c
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
(#)
data Condition arg argl argr outb out where
Holds :: Condition (Bool ': s) s s o o
IsSome :: Condition (Maybe a ': s) (a ': s) s o o
IsNone :: Condition (Maybe a ': s) s (a ': s) o o
IsLeft :: Condition (Either l r ': s) (l ': s) (r ': s) o o
IsRight :: Condition (Either l r ': s) (r ': s) (l ': s) o o
IsCons :: Condition ([a] ': s) (a ': [a] ': s) s o o
IsNil :: Condition ([a] ': s) s (a ': [a] ': s) o o
IsZero :: (UnaryArithOpHs Eq' a, UnaryArithResHs Eq' a ~ Bool)
=> Condition (a ': s) s s o o
IsNotZero :: (UnaryArithOpHs Eq' a, UnaryArithResHs Eq' a ~ Bool)
=> Condition (a ': s) s s o o
IsEq :: NiceComparable a => Condition (a ': a ': s) s s o o
IsNeq :: NiceComparable a => Condition (a ': a ': s) s s o o
IsLt :: NiceComparable a => Condition (a ': a ': s) s s o o
IsGt :: NiceComparable a => Condition (a ': a ': s) s s o o
IsLe :: NiceComparable a => Condition (a ': a ': s) s s o o
IsGe :: NiceComparable a => Condition (a ': a ': s) s s o o
NamedBinCondition ::
Condition (a ': a ': s) s s o o ->
Label n1 -> Label n2 ->
Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
PreserveArgsBinCondition ::
(forall st o. Condition (a ': b ': st) st st o o) ->
Condition (a ': b ': s) (a ': b ': s) (a ': b ': s) (a ': b ': s) s
ifThenElse
:: Condition arg argl argr outb out
-> (argl :-> outb) -> (argr :-> outb) -> (arg :-> out)
ifThenElse :: Condition arg argl argr outb out
-> (argl :-> outb) -> (argr :-> outb) -> arg :-> out
ifThenElse = \case
Condition arg argl argr outb out
Holds -> (argl :-> outb) -> (argr :-> outb) -> arg :-> out
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
if_
Condition arg argl argr outb out
IsSome -> ((argr :-> out)
-> ((a : argr) :-> out) -> (Maybe a : argr) :-> out)
-> ((a : argr) :-> out)
-> (argr :-> out)
-> (Maybe a : argr) :-> out
forall a b c. (a -> b -> c) -> b -> a -> c
flip (argr :-> out) -> ((a : argr) :-> out) -> (Maybe a : argr) :-> out
forall (s :: [*]) (s' :: [*]) a.
(s :-> s') -> ((a : s) :-> s') -> (Maybe a : s) :-> s'
ifNone
Condition arg argl argr outb out
IsNone -> (argl :-> outb) -> (argr :-> outb) -> arg :-> out
forall (s :: [*]) (s' :: [*]) a.
(s :-> s') -> ((a : s) :-> s') -> (Maybe a : s) :-> s'
ifNone
Condition arg argl argr outb out
IsLeft -> (argl :-> outb) -> (argr :-> outb) -> arg :-> out
forall a (s :: [*]) (s' :: [*]) b.
((a : s) :-> s') -> ((b : s) :-> s') -> (Either a b : s) :-> s'
ifLeft
Condition arg argl argr outb out
IsRight -> (((l : s) :-> out)
-> ((r : s) :-> out) -> (Either l r : s) :-> out)
-> ((r : s) :-> out)
-> ((l : s) :-> out)
-> (Either l r : s) :-> out
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((l : s) :-> out) -> ((r : s) :-> out) -> (Either l r : s) :-> out
forall a (s :: [*]) (s' :: [*]) b.
((a : s) :-> s') -> ((b : s) :-> s') -> (Either a b : s) :-> s'
ifLeft
Condition arg argl argr outb out
IsCons -> (argl :-> outb) -> (argr :-> outb) -> arg :-> out
forall a (s :: [*]) (s' :: [*]).
((a : List a : s) :-> s') -> (s :-> s') -> (List a : s) :-> s'
ifCons
Condition arg argl argr outb out
IsNil -> (((a : List a : argl) :-> out)
-> (argl :-> out) -> (List a : argl) :-> out)
-> (argl :-> out)
-> ((a : List a : argl) :-> out)
-> (List a : argl) :-> out
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((a : List a : argl) :-> out)
-> (argl :-> out) -> (List a : argl) :-> out
forall a (s :: [*]) (s' :: [*]).
((a : List a : s) :-> s') -> (s :-> s') -> (List a : s) :-> s'
ifCons
Condition arg argl argr outb out
IsZero -> \argl :-> outb
l argr :-> outb
r -> (a : argl) :-> (Bool : argl)
forall n (s :: [*]).
UnaryArithOpHs Eq' n =>
(n : s) :-> (UnaryArithResHs Eq' n : s)
eq0 ((a : argl) :-> (Bool : argl))
-> ((Bool : argl) :-> outb) -> (a : argl) :-> 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
Condition arg argl argr outb out
IsNotZero -> \argl :-> outb
l argr :-> outb
r -> (a : argl) :-> (Bool : argr)
forall n (s :: [*]).
UnaryArithOpHs Eq' n =>
(n : s) :-> (UnaryArithResHs Eq' n : s)
eq0 ((a : argl) :-> (Bool : argr))
-> ((Bool : argr) :-> outb) -> (a : argl) :-> outb
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (argr :-> outb) -> (argr :-> outb) -> (Bool : argr) :-> outb
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
if_ argr :-> outb
r argl :-> outb
argr :-> outb
l
Condition arg argl argr outb out
IsEq -> (argl :-> outb) -> (argr :-> outb) -> arg :-> out
forall a (s :: [*]) (s' :: [*]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a : a : s) :-> s'
ifEq
Condition arg argl argr outb out
IsNeq -> (argl :-> outb) -> (argr :-> outb) -> arg :-> out
forall a (s :: [*]) (s' :: [*]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a : a : s) :-> s'
ifNeq
Condition arg argl argr outb out
IsLt -> (argl :-> outb) -> (argr :-> outb) -> arg :-> out
forall a (s :: [*]) (s' :: [*]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a : a : s) :-> s'
ifLt
Condition arg argl argr outb out
IsGt -> (argl :-> outb) -> (argr :-> outb) -> arg :-> out
forall a (s :: [*]) (s' :: [*]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a : a : s) :-> s'
ifGt
Condition arg argl argr outb out
IsLe -> (argl :-> outb) -> (argr :-> outb) -> arg :-> out
forall a (s :: [*]) (s' :: [*]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a : a : s) :-> s'
ifLe
Condition arg argl argr outb out
IsGe -> (argl :-> outb) -> (argr :-> outb) -> arg :-> out
forall a (s :: [*]) (s' :: [*]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a : a : s) :-> s'
ifGe
NamedBinCondition Condition (a : a : argl) argl argl outb outb
condition Label n1
l1 Label n2
l2 -> \argl :-> outb
l argr :-> outb
r ->
Label n1
-> (NamedF Identity a n1 : NamedF Identity a n2 : argl)
:-> (a : NamedF Identity a n2 : argl)
forall (name :: Symbol) a (s :: [*]).
Label name -> (NamedF Identity a name : s) :-> (a : s)
fromNamed Label n1
l1 ((NamedF Identity a n1 : NamedF Identity a n2 : argl)
:-> (a : NamedF Identity a n2 : argl))
-> ((a : NamedF Identity a n2 : argl) :-> (a : a : argl))
-> (NamedF Identity a n1 : NamedF Identity a n2 : argl)
:-> (a : a : argl)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((NamedF Identity a n2 : argl) :-> (a : argl))
-> (a : NamedF Identity a n2 : argl) :-> (a : a : argl)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Label n2 -> (NamedF Identity a n2 : argl) :-> (a : argl)
forall (name :: Symbol) a (s :: [*]).
Label name -> (NamedF Identity a name : s) :-> (a : s)
fromNamed Label n2
l2) ((NamedF Identity a n1 : NamedF Identity a n2 : argl)
:-> (a : a : argl))
-> ((a : a : argl) :-> outb)
-> (NamedF Identity a n1 : NamedF Identity a n2 : argl) :-> outb
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Condition (a : a : argl) argl argl outb outb
-> (argl :-> outb) -> (argl :-> outb) -> (a : a : argl) :-> outb
forall (arg :: [*]) (argl :: [*]) (argr :: [*]) (outb :: [*])
(out :: [*]).
Condition arg argl argr outb out
-> (argl :-> outb) -> (argr :-> outb) -> arg :-> out
ifThenElse Condition (a : a : argl) argl argl outb outb
condition argl :-> outb
l argl :-> outb
argr :-> outb
r
PreserveArgsBinCondition forall (st :: [*]) (o :: [*]). Condition (a : b : st) st st o o
condition -> \argl :-> outb
l argr :-> outb
r ->
forall (inp :: [*]) (out :: [*]) a.
ConstraintDUPNLorentz (ToPeano 2) inp out a =>
inp :-> out
forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDUPNLorentz (ToPeano n) inp out a =>
inp :-> out
dupN @2 (arg :-> (b : a : b : out))
-> ((b : a : b : out) :-> (a : b : argl)) -> arg :-> (a : b : argl)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall (inp :: [*]) (out :: [*]) a.
ConstraintDUPNLorentz (ToPeano 2) inp out a =>
inp :-> out
forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDUPNLorentz (ToPeano n) inp out a =>
inp :-> out
dupN @2 (arg :-> (a : b : argl)) -> ((a : b : argl) :-> out) -> arg :-> out
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
Condition (a : b : argl) argl argl out out
-> (argl :-> out) -> (argl :-> out) -> (a : b : argl) :-> out
forall (arg :: [*]) (argl :: [*]) (argr :: [*]) (outb :: [*])
(out :: [*]).
Condition arg argl argr outb out
-> (argl :-> outb) -> (argr :-> outb) -> arg :-> out
ifThenElse Condition (a : b : argl) argl argl out out
forall (st :: [*]) (o :: [*]). Condition (a : b : st) st st o o
condition
(argl :-> outb
l (argl :-> outb) -> (outb :-> (b : out)) -> argl :-> (b : out)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# outb :-> (b : out)
forall a (s :: [*]). (a : s) :-> s
drop (argl :-> (b : out)) -> ((b : out) :-> out) -> argl :-> out
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (b : out) :-> out
forall a (s :: [*]). (a : s) :-> s
drop)
(argr :-> outb
r (argr :-> outb) -> (outb :-> (b : out)) -> argr :-> (b : out)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# outb :-> (b : out)
forall a (s :: [*]). (a : s) :-> s
drop (argr :-> (b : out)) -> ((b : out) :-> out) -> argr :-> out
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (b : out) :-> out
forall a (s :: [*]). (a : s) :-> s
drop)
infix 4 <.
(<.)
:: NiceComparable a
=> Label n1 -> Label n2
-> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
<. :: Label n1
-> Label n2 -> Condition ((n1 :! a) : (n2 :! a) : s) s s o o
(<.) = Condition (a : a : s) s s o o
-> Label n1
-> Label n2
-> Condition ((n1 :! a) : (n2 :! a) : s) s s o o
forall a (s :: [*]) (o :: [*]) (n1 :: Symbol) (n2 :: Symbol).
Condition (a : a : s) s s o o
-> Label n1
-> Label n2
-> Condition ((n1 :! a) : (n2 :! a) : s) s s o o
NamedBinCondition Condition (a : a : s) s s o o
forall a (s :: [*]) (o :: [*]).
NiceComparable a =>
Condition (a : a : s) s s o o
IsLt
infix 4 >.
(>.)
:: NiceComparable a
=> Label n1 -> Label n2
-> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
>. :: Label n1
-> Label n2 -> Condition ((n1 :! a) : (n2 :! a) : s) s s o o
(>.) = Condition (a : a : s) s s o o
-> Label n1
-> Label n2
-> Condition ((n1 :! a) : (n2 :! a) : s) s s o o
forall a (s :: [*]) (o :: [*]) (n1 :: Symbol) (n2 :: Symbol).
Condition (a : a : s) s s o o
-> Label n1
-> Label n2
-> Condition ((n1 :! a) : (n2 :! a) : s) s s o o
NamedBinCondition Condition (a : a : s) s s o o
forall a (s :: [*]) (o :: [*]).
NiceComparable a =>
Condition (a : a : s) s s o o
IsGt
infix 4 <=.
(<=.)
:: NiceComparable a
=> Label n1 -> Label n2
-> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
<=. :: Label n1
-> Label n2 -> Condition ((n1 :! a) : (n2 :! a) : s) s s o o
(<=.) = Condition (a : a : s) s s o o
-> Label n1
-> Label n2
-> Condition ((n1 :! a) : (n2 :! a) : s) s s o o
forall a (s :: [*]) (o :: [*]) (n1 :: Symbol) (n2 :: Symbol).
Condition (a : a : s) s s o o
-> Label n1
-> Label n2
-> Condition ((n1 :! a) : (n2 :! a) : s) s s o o
NamedBinCondition Condition (a : a : s) s s o o
forall a (s :: [*]) (o :: [*]).
NiceComparable a =>
Condition (a : a : s) s s o o
IsLe
infix 4 >=.
(>=.)
:: NiceComparable a
=> Label n1 -> Label n2
-> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
>=. :: Label n1
-> Label n2 -> Condition ((n1 :! a) : (n2 :! a) : s) s s o o
(>=.) = Condition (a : a : s) s s o o
-> Label n1
-> Label n2
-> Condition ((n1 :! a) : (n2 :! a) : s) s s o o
forall a (s :: [*]) (o :: [*]) (n1 :: Symbol) (n2 :: Symbol).
Condition (a : a : s) s s o o
-> Label n1
-> Label n2
-> Condition ((n1 :! a) : (n2 :! a) : s) s s o o
NamedBinCondition Condition (a : a : s) s s o o
forall a (s :: [*]) (o :: [*]).
NiceComparable a =>
Condition (a : a : s) s s o o
IsGe
infix 4 ==.
(==.)
:: NiceComparable a
=> Label n1 -> Label n2
-> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
==. :: Label n1
-> Label n2 -> Condition ((n1 :! a) : (n2 :! a) : s) s s o o
(==.) = Condition (a : a : s) s s o o
-> Label n1
-> Label n2
-> Condition ((n1 :! a) : (n2 :! a) : s) s s o o
forall a (s :: [*]) (o :: [*]) (n1 :: Symbol) (n2 :: Symbol).
Condition (a : a : s) s s o o
-> Label n1
-> Label n2
-> Condition ((n1 :! a) : (n2 :! a) : s) s s o o
NamedBinCondition Condition (a : a : s) s s o o
forall a (s :: [*]) (o :: [*]).
NiceComparable a =>
Condition (a : a : s) s s o o
IsEq
infix 4 /=.
(/=.)
:: NiceComparable a
=> Label n1 -> Label n2
-> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
/=. :: Label n1
-> Label n2 -> Condition ((n1 :! a) : (n2 :! a) : s) s s o o
(/=.) = Condition (a : a : s) s s o o
-> Label n1
-> Label n2
-> Condition ((n1 :! a) : (n2 :! a) : s) s s o o
forall a (s :: [*]) (o :: [*]) (n1 :: Symbol) (n2 :: Symbol).
Condition (a : a : s) s s o o
-> Label n1
-> Label n2
-> Condition ((n1 :! a) : (n2 :! a) : s) s s o o
NamedBinCondition Condition (a : a : s) s s o o
forall a (s :: [*]) (o :: [*]).
NiceComparable a =>
Condition (a : a : s) s s o o
IsNeq
keepIfArgs
:: (forall st o. Condition (a ': b ': st) st st o o)
-> Condition (a ': b ': s) (a ': b ': s) (a ': b ': s) (a ': b ': s) s
keepIfArgs :: (forall (st :: [*]) (o :: [*]). Condition (a : b : st) st st o o)
-> Condition (a : b : s) (a : b : s) (a : b : s) (a : b : s) s
keepIfArgs = (forall (st :: [*]) (o :: [*]). Condition (a : b : st) st st o o)
-> Condition (a : b : s) (a : b : s) (a : b : s) (a : b : s) s
forall a b (s :: [*]).
(forall (st :: [*]) (o :: [*]). Condition (a : b : st) st st o o)
-> Condition (a : b : s) (a : b : s) (a : b : s) (a : b : s) s
PreserveArgsBinCondition