module Indigo.Rebound
(
ifThenElse
, fromInteger
, nat
, int
, mutez
, IsLabel (..)
) where
import Data.Kind qualified as Kind
import Prelude qualified as P
import Indigo.Backend.Conditional (IfConstraint)
import Indigo.Common.Expr (IsExpr, toExpr)
import Indigo.Frontend (IndigoM, RetVars, if_)
import Indigo.Lorentz
import Morley.Tezos.Core (mkMutez)
import Morley.Util.Label (IsLabel(..))
ifThenElse
:: (IfConstraint a b, IsExpr exa Bool)
=> exa
-> IndigoM a
-> IndigoM b
-> IndigoM (RetVars a)
ifThenElse :: forall a b exa.
(IfConstraint a b, IsExpr exa Bool) =>
exa -> IndigoM a -> IndigoM b -> IndigoM (RetVars a)
ifThenElse exa
cond = Expr Bool -> IndigoM a -> IndigoM b -> IndigoM (RetVars a)
forall a b ex.
(IfConstraint a b, ex :~> Bool, HasCallStack) =>
ex -> IndigoM a -> IndigoM b -> IndigoM (RetVars a)
if_ (exa -> Expr (ExprType exa)
forall a. ToExpr a => a -> Expr (ExprType a)
toExpr exa
cond)
data NumKind = Nat | Int | Mtz
data NumType (n :: NumKind) (t :: Kind.Type) where
NNat :: NumType 'Nat Natural
NInt :: NumType 'Int Integer
NMtz :: NumType 'Mtz Mutez
nat :: NumType 'Nat Natural
nat :: NumType 'Nat Natural
nat = NumType 'Nat Natural
NNat
int :: NumType 'Int Integer
int :: NumType 'Int Integer
int = NumType 'Int Integer
NInt
mutez :: NumType 'Mtz Mutez
mutez :: NumType 'Mtz Mutez
mutez = NumType 'Mtz Mutez
NMtz
fromInteger :: Integer -> NumType n t -> t
fromInteger :: forall (n :: NumKind) t. Integer -> NumType n t -> t
fromInteger Integer
val = \case
NumType n t
NNat -> Integer -> t
forall a. (HasCallStack, Integral a) => Integer -> a
P.fromInteger Integer
val
NumType n t
NInt -> t
Integer
val
NumType n t
NMtz -> Either Text Mutez -> Mutez
forall a b. (HasCallStack, Buildable a) => Either a b -> b
P.unsafe (Integer -> Either Text Mutez
forall i. Integral i => i -> Either Text Mutez
mkMutez Integer
val)