module Lorentz.Rebinded
( (>>)
, pure
, return
, ifThenElse
, Condition (..)
, fromInteger
, fromString
, fromLabel
) where
import Prelude hiding ((>>), (>>=))
import Lorentz.Arith
import Lorentz.Base
import Lorentz.Instr
import Lorentz.Macro
import Michelson.Typed.Arith
(>>) :: (a :-> b) -> (b :-> c) -> (a :-> c)
(>>) = (#)
data Condition arg argl argr where
Holds :: Condition (Bool ': s) s s
IsSome :: Condition (Maybe a ': s) (a ': s) s
IsNone :: Condition (Maybe a ': s) s (a ': s)
IsLeft :: Condition (Either l r ': s) (l ': s) (r ': s)
IsRight :: Condition (Either l r ': s) (r ': s) (l ': s)
IsCons :: Condition ([a] ': s) (a ': [a] ': s) s
IsNil :: Condition ([a] ': s) s (a ': [a] ': s)
IsZero :: (UnaryArithOpHs Eq' a, UnaryArithResHs Eq' a ~ Bool)
=> Condition (a ': s) s s
IsNotZero :: (UnaryArithOpHs Eq' a, UnaryArithResHs Eq' a ~ Bool)
=> Condition (a ': s) s s
IsEq :: NiceComparable a => Condition (a ': a ': s) s s
IsNeq :: NiceComparable a => Condition (a ': a ': s) s s
IsLt :: NiceComparable a => Condition (a ': a ': s) s s
IsGt :: NiceComparable a => Condition (a ': a ': s) s s
IsLe :: NiceComparable a => Condition (a ': a ': s) s s
IsGe :: NiceComparable a => Condition (a ': a ': s) s s
ifThenElse
:: Condition arg argl argr
-> (argl :-> o) -> (argr :-> o) -> (arg :-> o)
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