Lorentz.CustomArith.Common

Arithmetic operations

div :: forall r n m s. ArithOpHs Div n m r => (n : (m : s)) :-> (r : s)

Operation that represents division of two values with a given result

Lorentz casts

class LorentzRounding a b where

Class that enables support of rounding operations for Lorentz non-integer values

Methods

round_ :: (a : s) :-> (b : s)

ceil_ :: (a : s) :-> (b : s)

floor_ :: (a : s) :-> (b : s)

Instances

(LorentzRational r, Unwrappabled r ~ (a, Natural), ArithOpHs EDiv a Natural (Maybe (a, Natural)), ArithOpHs Add a Natural a, ArithOpHs Add Natural a a) => LorentzRounding r a

Defined in Lorentz.CustomArith.RationalArith

Methods

round_ :: forall (s :: [Type]). (r ': s) :-> (a ': s)

ceil_ :: forall (s :: [Type]). (r ': s) :-> (a ': s)

floor_ :: forall (s :: [Type]). (r ': s) :-> (a ': s)

(KnownNat a, KnownNat b, b1 ~ b2, LorentzFixedBase b1) => LorentzRounding (Fixed (b1 a)) (Fixed (b2 b))

Round is implemented using "banker's rounding" strategy, rounding half-way values towards nearest even value

Defined in Lorentz.CustomArith.FixedArith

Methods

round_ :: forall (s :: [Type]). (Fixed (b1 a) ': s) :-> (Fixed (b2 b) ': s)

ceil_ :: forall (s :: [Type]). (Fixed (b1 a) ': s) :-> (Fixed (b2 b) ': s)

floor_ :: forall (s :: [Type]). (Fixed (b1 a) ': s) :-> (Fixed (b2 b) ': s)

(KnownNat a, KnownNat b, b1 ~ b2, LorentzFixedBase b1) => LorentzRounding (NFixed (b1 a)) (NFixed (b2 b))

Defined in Lorentz.CustomArith.FixedArith

Methods

round_ :: forall (s :: [Type]). (NFixed (b1 a) ': s) :-> (NFixed (b2 b) ': s)

ceil_ :: forall (s :: [Type]). (NFixed (b1 a) ': s) :-> (NFixed (b2 b) ': s)

floor_ :: forall (s :: [Type]). (NFixed (b1 a) ': s) :-> (NFixed (b2 b) ': s)

Additional Arithmetic operations

data Div

Since Michelson doesn't support divide operation, we will use our own to represent divison of Fixed and Rational values

Instances

r ~ NRational => ArithOpHs Div NRational NRational r

Defined in Lorentz.CustomArith.RationalArith

Methods

evalArithOpHs :: forall (s :: [Type]). (NRational ': (NRational ': s)) :-> (r ': s)

r ~ Rational => ArithOpHs Div NRational Rational r

Defined in Lorentz.CustomArith.RationalArith

Methods

evalArithOpHs :: forall (s :: [Type]). (NRational ': (Rational ': s)) :-> (r ': s)

r ~ Rational => ArithOpHs Div NRational Integer r

Defined in Lorentz.CustomArith.RationalArith

Methods

evalArithOpHs :: forall (s :: [Type]). (NRational ': (Integer ': s)) :-> (r ': s)

r ~ NRational => ArithOpHs Div NRational Natural r

Defined in Lorentz.CustomArith.RationalArith

Methods

evalArithOpHs :: forall (s :: [Type]). (NRational ': (Natural ': s)) :-> (r ': s)

r ~ Rational => ArithOpHs Div Rational NRational r

Defined in Lorentz.CustomArith.RationalArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Rational ': (NRational ': s)) :-> (r ': s)

r ~ Rational => ArithOpHs Div Rational Rational r

Defined in Lorentz.CustomArith.RationalArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Rational ': (Rational ': s)) :-> (r ': s)

r ~ Rational => ArithOpHs Div Rational Integer r

Defined in Lorentz.CustomArith.RationalArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Rational ': (Integer ': s)) :-> (r ': s)

r ~ Rational => ArithOpHs Div Rational Natural r

Defined in Lorentz.CustomArith.RationalArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Rational ': (Natural ': s)) :-> (r ': s)

r ~ Rational => ArithOpHs Div Integer NRational r

Defined in Lorentz.CustomArith.RationalArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (NRational ': s)) :-> (r ': s)

r ~ Rational => ArithOpHs Div Integer Rational r

Defined in Lorentz.CustomArith.RationalArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (Rational ': s)) :-> (r ': s)

r ~ NRational => ArithOpHs Div Natural NRational r

Defined in Lorentz.CustomArith.RationalArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (NRational ': s)) :-> (r ': s)

r ~ Rational => ArithOpHs Div Natural Rational r

Defined in Lorentz.CustomArith.RationalArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Rational ': s)) :-> (r ': s)

DivIntegralConstraint r b => ArithOpHs Div Integer Integer (Maybe (Fixed (b r)))

Defined in Lorentz.CustomArith.FixedArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (Integer ': s)) :-> (Maybe (Fixed (b r)) ': s)

ArithOpHs Div Integer Integer (Maybe Rational)

Defined in Lorentz.CustomArith.RationalArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (Integer ': s)) :-> (Maybe Rational ': s)

DivIntegralConstraint r b => ArithOpHs Div Integer Natural (Maybe (Fixed (b r)))

Defined in Lorentz.CustomArith.FixedArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (Natural ': s)) :-> (Maybe (Fixed (b r)) ': s)

ArithOpHs Div Integer Natural (Maybe Rational)

Defined in Lorentz.CustomArith.RationalArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (Natural ': s)) :-> (Maybe Rational ': s)

DivIntegralConstraint r b => ArithOpHs Div Natural Integer (Maybe (Fixed (b r)))

Defined in Lorentz.CustomArith.FixedArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Integer ': s)) :-> (Maybe (Fixed (b r)) ': s)

ArithOpHs Div Natural Integer (Maybe Rational)

Defined in Lorentz.CustomArith.RationalArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Integer ': s)) :-> (Maybe Rational ': s)

DivIntegralConstraint r b => ArithOpHs Div Natural Natural (Maybe (Fixed (b r)))

Defined in Lorentz.CustomArith.FixedArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Natural ': s)) :-> (Maybe (Fixed (b r)) ': s)

DivIntegralConstraint r b => ArithOpHs Div Natural Natural (Maybe (NFixed (b r)))

Defined in Lorentz.CustomArith.FixedArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Natural ': s)) :-> (Maybe (NFixed (b r)) ': s)

ArithOpHs Div Natural Natural (Maybe NRational)

Defined in Lorentz.CustomArith.RationalArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Natural ': s)) :-> (Maybe NRational ': s)

DivConstraint1 a t r (Fixed :: LorentzFixedBaseKind -> Type) b1 => ArithOpHs Div Integer (Fixed (b1 a)) r

Defined in Lorentz.CustomArith.FixedArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (Fixed (b1 a) ': s)) :-> (r ': s)

DivConstraint1 a t r (Fixed :: LorentzFixedBaseKind -> Type) b1 => ArithOpHs Div Integer (NFixed (b1 a)) r

Defined in Lorentz.CustomArith.FixedArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Integer ': (NFixed (b1 a) ': s)) :-> (r ': s)

DivConstraint1 a t r (Fixed :: LorentzFixedBaseKind -> Type) b1 => ArithOpHs Div Natural (Fixed (b1 a)) r

Defined in Lorentz.CustomArith.FixedArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (Fixed (b1 a) ': s)) :-> (r ': s)

DivConstraint1 a t r (NFixed :: LorentzFixedBaseKind -> Type) b1 => ArithOpHs Div Natural (NFixed (b1 a)) r

Defined in Lorentz.CustomArith.FixedArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Natural ': (NFixed (b1 a) ': s)) :-> (r ': s)

DivConstraint a b t r (Fixed :: LorentzFixedBaseKind -> Type) b1 b2 => ArithOpHs Div (Fixed (b1 a)) (Fixed (b2 b)) r

Defined in Lorentz.CustomArith.FixedArith

Methods

evalArithOpHs :: forall (s :: [Type]). (Fixed (b1 a) ': (Fixed (b2 b) ': s)) :-> (r ': s)

DivConstraint a b t r (NFixed :: LorentzFixedBaseKind -> Type) b1 b2 => ArithOpHs Div (NFixed (b1 a)) (NFixed (b2 b)) r

Defined in Lorentz.CustomArith.FixedArith

Methods

evalArithOpHs :: forall (s :: [Type]). (NFixed (b1 a) ': (NFixed (b2 b) ': s)) :-> (r ': s)