module Lorentz.Rebinded
( (>>)
, pure
, return
, ifThenElse
, Condition (..)
, (<.)
, (>.)
, (<=.)
, (>=.)
, (==.)
, (/=.)
, keepIfArgs
, fromInteger
, fromString
, fromLabel
) where
import Prelude hiding (drop, swap, (>>), (>>=))
import Data.Vinyl.Derived (Label)
import Named ((:!))
import Lorentz.Arith
import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Instr
import Lorentz.Macro
import Michelson.Typed.Arith
(>>) :: (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 = \case
Holds -> if_
IsSome -> flip ifNone
IsNone -> ifNone
IsLeft -> ifLeft
IsRight -> flip ifLeft
IsCons -> ifCons
IsNil -> flip ifCons
IsZero -> \l r -> eq0 # if_ l r
IsNotZero -> \l r -> eq0 # if_ r l
IsEq -> ifEq
IsNeq -> ifNeq
IsLt -> ifLt
IsGt -> ifGt
IsLe -> ifLe
IsGe -> ifGe
NamedBinCondition condition l1 l2 -> \l r ->
fromNamed l1 # dip (fromNamed l2) # ifThenElse condition l r
PreserveArgsBinCondition condition -> \l r ->
dip dup # swap # dip dup # swap #
ifThenElse condition
(l # drop # drop)
(r # drop # drop)
infix 4 <.
(<.)
:: NiceComparable a
=> Label n1 -> Label n2
-> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
(<.) = NamedBinCondition IsLt
infix 4 >.
(>.)
:: NiceComparable a
=> Label n1 -> Label n2
-> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
(>.) = NamedBinCondition IsGt
infix 4 <=.
(<=.)
:: NiceComparable a
=> Label n1 -> Label n2
-> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
(<=.) = NamedBinCondition IsLe
infix 4 >=.
(>=.)
:: NiceComparable a
=> Label n1 -> Label n2
-> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
(>=.) = NamedBinCondition IsGe
infix 4 ==.
(==.)
:: NiceComparable a
=> Label n1 -> Label n2
-> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
(==.) = NamedBinCondition IsEq
infix 4 /=.
(/=.)
:: NiceComparable a
=> Label n1 -> Label n2
-> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
(/=.) = NamedBinCondition 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 = PreserveArgsBinCondition