{-# OPTIONS_GHC -Wno-orphans #-}
module Lorentz.CustomArith.FixedArith
(
castNFixedToFixed
, castFixedToNFixed
, unsafeCastFixedToNFixed
, Fixed (..)
, NFixed (..)
, LorentzFixedBaseKind
, DecBase
, BinBase
, resolution_
, toFixed
, fromFixed
, LorentzFixedBase
, getBase
) where
import Data.Fixed (Fixed(..), HasResolution(..))
import Data.Ratio ((%))
import GHC.Num qualified (fromInteger)
import GHC.TypeLits qualified as Lit
import Prelude hiding (and, compare, drop, natVal, some, swap)
import Prelude qualified as P
import Text.Show qualified
import Lorentz.Arith
import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Constraints.Scopes
import Lorentz.CustomArith.Common
import Lorentz.Errors
import Lorentz.Instr
import Lorentz.Macro
import Lorentz.Value
import Morley.Michelson.Typed
import Unsafe qualified
{-# ANN module ("HLint: ignore Use 'natVal' from Universum" :: Text) #-}
data LorentzFixedBaseKindTag
type LorentzFixedBaseKind = LorentzFixedBaseKindTag -> Type
data BinBase :: Lit.Nat -> LorentzFixedBaseKind
data DecBase :: Lit.Nat -> LorentzFixedBaseKind
type LorentzFixedBase :: (Lit.Nat -> LorentzFixedBaseKind) -> Constraint
class Typeable a => LorentzFixedBase a where
getBase :: Num b => b
instance LorentzFixedBase DecBase where
getBase :: forall b. Num b => b
getBase = b
10
instance LorentzFixedBase BinBase where
getBase :: forall b. Num b => b
getBase = b
2
instance KnownNat p => HasResolution (DecBase p) where
resolution :: forall (p :: LorentzFixedBaseKind -> *). p (DecBase p) -> Integer
resolution p (DecBase p)
_ = forall (a :: Nat -> LorentzFixedBaseKind) b.
(LorentzFixedBase a, Num b) =>
b
getBase @DecBase Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Proxy p -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @p))
instance KnownNat p => HasResolution (BinBase p) where
resolution :: forall (p :: LorentzFixedBaseKind -> *). p (BinBase p) -> Integer
resolution p (BinBase p)
_ = forall (a :: Nat -> LorentzFixedBaseKind) b.
(LorentzFixedBase a, Num b) =>
b
getBase @BinBase Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Proxy p -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @p))
resolution_ :: forall a. HasResolution a => Natural
resolution_ :: forall {k} (a :: k). HasResolution a => Nat
resolution_ =
let r :: Integer
r = Proxy a -> Integer
forall k (a :: k) (p :: k -> *). HasResolution a => p a -> Integer
forall (p :: k -> *). p a -> Integer
resolution (forall (t :: k). Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)
in if Integer
r Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0
then Text -> Nat
forall a. HasCallStack => Text -> a
error Text
"Lorentz Rationals support only positive resolutions"
else forall a b. (HasCallStack, Integral a, Integral b) => a -> b
Unsafe.fromIntegral @Integer @Natural Integer
r
newtype NFixed p = MkNFixed Natural deriving stock (NFixed p -> NFixed p -> Bool
(NFixed p -> NFixed p -> Bool)
-> (NFixed p -> NFixed p -> Bool) -> Eq (NFixed p)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (p :: k). NFixed p -> NFixed p -> Bool
$c== :: forall k (p :: k). NFixed p -> NFixed p -> Bool
== :: NFixed p -> NFixed p -> Bool
$c/= :: forall k (p :: k). NFixed p -> NFixed p -> Bool
/= :: NFixed p -> NFixed p -> Bool
Eq, Eq (NFixed p)
Eq (NFixed p)
-> (NFixed p -> NFixed p -> Ordering)
-> (NFixed p -> NFixed p -> Bool)
-> (NFixed p -> NFixed p -> Bool)
-> (NFixed p -> NFixed p -> Bool)
-> (NFixed p -> NFixed p -> Bool)
-> (NFixed p -> NFixed p -> NFixed p)
-> (NFixed p -> NFixed p -> NFixed p)
-> Ord (NFixed p)
NFixed p -> NFixed p -> Bool
NFixed p -> NFixed p -> Ordering
NFixed p -> NFixed p -> NFixed p
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (p :: k). Eq (NFixed p)
forall k (p :: k). NFixed p -> NFixed p -> Bool
forall k (p :: k). NFixed p -> NFixed p -> Ordering
forall k (p :: k). NFixed p -> NFixed p -> NFixed p
$ccompare :: forall k (p :: k). NFixed p -> NFixed p -> Ordering
compare :: NFixed p -> NFixed p -> Ordering
$c< :: forall k (p :: k). NFixed p -> NFixed p -> Bool
< :: NFixed p -> NFixed p -> Bool
$c<= :: forall k (p :: k). NFixed p -> NFixed p -> Bool
<= :: NFixed p -> NFixed p -> Bool
$c> :: forall k (p :: k). NFixed p -> NFixed p -> Bool
> :: NFixed p -> NFixed p -> Bool
$c>= :: forall k (p :: k). NFixed p -> NFixed p -> Bool
>= :: NFixed p -> NFixed p -> Bool
$cmax :: forall k (p :: k). NFixed p -> NFixed p -> NFixed p
max :: NFixed p -> NFixed p -> NFixed p
$cmin :: forall k (p :: k). NFixed p -> NFixed p -> NFixed p
min :: NFixed p -> NFixed p -> NFixed p
Ord)
convertNFixedToFixed :: NFixed a -> Fixed a
convertNFixedToFixed :: forall {k} (a :: k). NFixed a -> Fixed a
convertNFixedToFixed (MkNFixed Nat
a) = Integer -> Fixed a
forall k (a :: k). Integer -> Fixed a
MkFixed (forall a b. (Integral a, Integral b, CheckIntSubType a b) => a -> b
fromIntegral @Natural @Integer Nat
a)
instance (HasResolution a) => Show (NFixed a) where
show :: NFixed a -> String
show = Fixed a -> String
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show (Fixed a -> String) -> (NFixed a -> Fixed a) -> NFixed a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NFixed a -> Fixed a
forall {k} (a :: k). NFixed a -> Fixed a
convertNFixedToFixed
instance (HasResolution a) => Num (NFixed a) where
(MkNFixed Nat
a) + :: NFixed a -> NFixed a -> NFixed a
+ (MkNFixed Nat
b) = Nat -> NFixed a
forall {k} (p :: k). Nat -> NFixed p
MkNFixed (Nat
a Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
b)
(MkNFixed Nat
a) - :: NFixed a -> NFixed a -> NFixed a
- (MkNFixed Nat
b) = Nat -> NFixed a
forall {k} (p :: k). Nat -> NFixed p
MkNFixed (Nat
a Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
b)
fa :: NFixed a
fa@(MkNFixed Nat
a) * :: NFixed a -> NFixed a -> NFixed a
* (MkNFixed Nat
b) = Nat -> NFixed a
forall {k} (p :: k). Nat -> NFixed p
MkNFixed (Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
P.div (Nat
a Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
* Nat
b) (Integer -> Nat
forall a. (HasCallStack, Integral a) => Integer -> a
fromInteger (NFixed a -> Integer
forall k (a :: k) (p :: k -> *). HasResolution a => p a -> Integer
forall (p :: k -> *). p a -> Integer
resolution NFixed a
fa)))
negate :: NFixed a -> NFixed a
negate (MkNFixed Nat
a) = Nat -> NFixed a
forall {k} (p :: k). Nat -> NFixed p
MkNFixed (Nat -> Nat
forall a. Num a => a -> a
negate Nat
a)
abs :: NFixed a -> NFixed a
abs = NFixed a -> NFixed a
forall a. a -> a
id
signum :: NFixed a -> NFixed a
signum (MkNFixed Nat
a) = Nat -> NFixed a
forall {k} (p :: k). Nat -> NFixed p
MkNFixed (Nat -> Nat
forall a. Num a => a -> a
signum Nat
a)
fromInteger :: Integer -> NFixed a
fromInteger Integer
i = (Nat -> NFixed a) -> NFixed a
forall {k} (a :: k) (f :: k -> *).
HasResolution a =>
(Nat -> f a) -> f a
withResolution (\Nat
res -> Nat -> NFixed a
forall {k} (p :: k). Nat -> NFixed p
MkNFixed ((Integer -> Nat
forall a. (HasCallStack, Integral a) => Integer -> a
fromInteger Integer
i) Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
* Nat
res))
instance (HasResolution a) => Fractional (NFixed a) where
fa :: NFixed a
fa@(MkNFixed Nat
a) / :: NFixed a -> NFixed a -> NFixed a
/ (MkNFixed Nat
b) = Nat -> NFixed a
forall {k} (p :: k). Nat -> NFixed p
MkNFixed (Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
P.div (Nat
a Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
* (Integer -> Nat
forall a. (HasCallStack, Integral a) => Integer -> a
fromInteger (NFixed a -> Integer
forall k (a :: k) (p :: k -> *). HasResolution a => p a -> Integer
forall (p :: k -> *). p a -> Integer
resolution NFixed a
fa))) Nat
b)
recip :: NFixed a -> NFixed a
recip fa :: NFixed a
fa@(MkNFixed Nat
a) = Nat -> NFixed a
forall {k} (p :: k). Nat -> NFixed p
MkNFixed (Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
P.div (Nat
res Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
* Nat
res) Nat
a) where
res :: Nat
res = Integer -> Nat
forall a. (HasCallStack, Integral a) => Integer -> a
fromInteger (Integer -> Nat) -> Integer -> Nat
forall a b. (a -> b) -> a -> b
$ NFixed a -> Integer
forall k (a :: k) (p :: k -> *). HasResolution a => p a -> Integer
forall (p :: k -> *). p a -> Integer
resolution NFixed a
fa
fromRational :: Rational -> NFixed a
fromRational Rational
r = (Nat -> NFixed a) -> NFixed a
forall {k} (a :: k) (f :: k -> *).
HasResolution a =>
(Nat -> f a) -> f a
withResolution (\Nat
res -> Nat -> NFixed a
forall {k} (p :: k). Nat -> NFixed p
MkNFixed (Rational -> Nat
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor (Rational
r Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* (Nat -> Rational
forall a. Real a => a -> Rational
toRational Nat
res))))
instance (HasResolution a) => Real (NFixed a) where
toRational :: NFixed a -> Rational
toRational (MkNFixed Nat
x) = Nat -> Integer
forall a b. (Integral a, Integral b, CheckIntSubType a b) => a -> b
fromIntegral Nat
x Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Proxy a -> Integer
forall k (a :: k) (p :: k -> *). HasResolution a => p a -> Integer
forall (p :: k -> *). p a -> Integer
resolution (forall (t :: k). Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)
instance IsoValue (NFixed p) where
type ToT (NFixed p) = 'TNat
toVal :: NFixed p -> Value (ToT (NFixed p))
toVal (MkNFixed Nat
x) = Nat -> Value' Instr 'TNat
forall (instr :: [T] -> [T] -> *). Nat -> Value' instr 'TNat
VNat Nat
x
fromVal :: Value (ToT (NFixed p)) -> NFixed p
fromVal (VNat Nat
x) = Nat -> NFixed p
forall {k} (p :: k). Nat -> NFixed p
MkNFixed Nat
x
instance Unwrappable (NFixed a) where
type Unwrappabled (NFixed a) = Natural
withResolution :: forall a f. (HasResolution a) => (Natural -> f a) -> f a
withResolution :: forall {k} (a :: k) (f :: k -> *).
HasResolution a =>
(Nat -> f a) -> f a
withResolution Nat -> f a
foo = Nat -> f a
foo (Nat -> f a) -> (Proxy a -> Nat) -> Proxy a -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Nat
forall a. (HasCallStack, Integral a) => Integer -> a
fromInteger (Integer -> Nat) -> (Proxy a -> Integer) -> Proxy a -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy a -> Integer
forall k (a :: k) (p :: k -> *). HasResolution a => p a -> Integer
forall (p :: k -> *). p a -> Integer
resolution (Proxy a -> f a) -> Proxy a -> f a
forall a b. (a -> b) -> a -> b
$ forall (t :: k). Proxy t
forall {k} (t :: k). Proxy t
Proxy @a
instance (r ~ (Fixed p)) => ArithOpHs Add (Fixed p) (Fixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Add (Fixed p) Integer r
instance (r ~ (Fixed p)) => ArithOpHs Add (Fixed p) Natural r
instance (r ~ (Fixed p)) => ArithOpHs Add Integer (Fixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Add Natural (Fixed p) r
instance (r ~ (NFixed p)) => ArithOpHs Add (NFixed p) (NFixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Add (NFixed p) Integer r
instance (r ~ (NFixed p)) => ArithOpHs Add (NFixed p) Natural r
instance (r ~ (Fixed p)) => ArithOpHs Add Integer (NFixed p) r
instance (r ~ (NFixed p)) => ArithOpHs Add Natural (NFixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Add (Fixed p) (NFixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Add (NFixed p) (Fixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Sub (Fixed p) (Fixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Sub (Fixed p) Integer r
instance (r ~ (Fixed p)) => ArithOpHs Sub (Fixed p) Natural r
instance (r ~ (Fixed p)) => ArithOpHs Sub Integer (Fixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Sub Natural (Fixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Sub (NFixed p) (NFixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Sub (NFixed p) Integer r
instance (r ~ (Fixed p)) => ArithOpHs Sub (NFixed p) Natural r
instance (r ~ (Fixed p)) => ArithOpHs Sub Integer (NFixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Sub Natural (NFixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Sub (Fixed p) (NFixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Sub (NFixed p) (Fixed p) r
instance (r ~ Fixed (b1 (a Lit.+ b)), b1 ~ b2) => ArithOpHs Mul (Fixed (b1 a)) (Fixed (b2 b)) r
instance (r ~ (Fixed p)) => ArithOpHs Mul (Fixed p) Integer r
instance (r ~ (Fixed p)) => ArithOpHs Mul (Fixed p) Natural r
instance (r ~ (Fixed p)) => ArithOpHs Mul Integer (Fixed p) r
instance (r ~ (Fixed p)) => ArithOpHs Mul Natural (Fixed p) r
instance (r ~ NFixed (b1 (a Lit.+ b)), b1 ~ b2) => ArithOpHs Mul (NFixed (b1 a)) (NFixed (b2 b)) r
instance (r ~ (Fixed p)) => ArithOpHs Mul (NFixed p) Integer r
instance (r ~ (NFixed p)) => ArithOpHs Mul (NFixed p) Natural r
instance (r ~ (Fixed p)) => ArithOpHs Mul Integer (NFixed p) r
instance (r ~ (NFixed p)) => ArithOpHs Mul Natural (NFixed p) r
instance (r ~ Fixed (b1 (a Lit.+ b)), b1 ~ b2) => ArithOpHs Mul (Fixed (b1 a)) (NFixed (b2 b)) r
instance (r ~ Fixed (b1 (a Lit.+ b)), b1 ~ b2) => ArithOpHs Mul (NFixed (b1 a)) (Fixed (b2 b)) r
instance (r ~ (NFixed (BinBase a))) => ArithOpHs Lsl (NFixed (BinBase a)) Natural r
instance (r ~ (NFixed (BinBase a))) => ArithOpHs Lsr (NFixed (BinBase a)) Natural r
instance UnaryArithOpHs Neg (Fixed p) where
type UnaryArithResHs Neg (Fixed p) = (Fixed p)
instance UnaryArithOpHs Neg (NFixed p) where
type UnaryArithResHs Neg (NFixed p) = (Fixed p)
instance ToIntegerArithOpHs (NFixed a)
instance (KnownNat a, KnownNat b, b1 ~ b2, LorentzFixedBase b1)
=> LorentzRounding (Fixed (b1 a)) (Fixed (b2 b)) where
round_ :: forall (s :: [*]). (Fixed (b1 a) : s) :-> (Fixed (b2 b) : s)
round_ = RoundingPattern -> (Fixed (b1 a) : s) :-> (Fixed (b2 b) : s)
forall (a :: Nat) (b :: Nat) r1 r2 (s :: [*])
(base :: Nat -> LorentzFixedBaseKind)
(f :: LorentzFixedBaseKind -> *).
(KnownNat a, KnownNat b, ForbidTicket (ToT (Unwrappabled r1)),
MichelsonCoercible r1 r2, SingI (ToT (Unwrappabled r1)),
Unwrappable r2, Unwrappable r1,
ArithOpHs Add Nat (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs
Add (Unwrappabled r2) (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs And (Unwrappabled r2) Nat Nat,
ArithOpHs
EDiv (Unwrappabled r1) Nat (Maybe (Unwrappabled r2, Nat)),
ArithOpHs Mul Nat r1 r1, LorentzFixedBase base, r1 ~ f (base a),
r2 ~ f (base b), NiceConstant (Unwrappabled r2),
Num (Unwrappabled r2)) =>
RoundingPattern -> (r1 : s) :-> (r2 : s)
roundingHelper RoundingPattern
Round
ceil_ :: forall (s :: [*]). (Fixed (b1 a) : s) :-> (Fixed (b2 b) : s)
ceil_ = RoundingPattern -> (Fixed (b1 a) : s) :-> (Fixed (b2 b) : s)
forall (a :: Nat) (b :: Nat) r1 r2 (s :: [*])
(base :: Nat -> LorentzFixedBaseKind)
(f :: LorentzFixedBaseKind -> *).
(KnownNat a, KnownNat b, ForbidTicket (ToT (Unwrappabled r1)),
MichelsonCoercible r1 r2, SingI (ToT (Unwrappabled r1)),
Unwrappable r2, Unwrappable r1,
ArithOpHs Add Nat (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs
Add (Unwrappabled r2) (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs And (Unwrappabled r2) Nat Nat,
ArithOpHs
EDiv (Unwrappabled r1) Nat (Maybe (Unwrappabled r2, Nat)),
ArithOpHs Mul Nat r1 r1, LorentzFixedBase base, r1 ~ f (base a),
r2 ~ f (base b), NiceConstant (Unwrappabled r2),
Num (Unwrappabled r2)) =>
RoundingPattern -> (r1 : s) :-> (r2 : s)
roundingHelper RoundingPattern
Ceil
floor_ :: forall (s :: [*]). (Fixed (b1 a) : s) :-> (Fixed (b2 b) : s)
floor_ = RoundingPattern -> (Fixed (b1 a) : s) :-> (Fixed (b2 b) : s)
forall (a :: Nat) (b :: Nat) r1 r2 (s :: [*])
(base :: Nat -> LorentzFixedBaseKind)
(f :: LorentzFixedBaseKind -> *).
(KnownNat a, KnownNat b, ForbidTicket (ToT (Unwrappabled r1)),
MichelsonCoercible r1 r2, SingI (ToT (Unwrappabled r1)),
Unwrappable r2, Unwrappable r1,
ArithOpHs Add Nat (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs
Add (Unwrappabled r2) (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs And (Unwrappabled r2) Nat Nat,
ArithOpHs
EDiv (Unwrappabled r1) Nat (Maybe (Unwrappabled r2, Nat)),
ArithOpHs Mul Nat r1 r1, LorentzFixedBase base, r1 ~ f (base a),
r2 ~ f (base b), NiceConstant (Unwrappabled r2),
Num (Unwrappabled r2)) =>
RoundingPattern -> (r1 : s) :-> (r2 : s)
roundingHelper RoundingPattern
Floor
instance (KnownNat a, KnownNat b, b1 ~ b2, LorentzFixedBase b1)
=> LorentzRounding (NFixed (b1 a)) (NFixed (b2 b)) where
round_ :: forall (s :: [*]). (NFixed (b1 a) : s) :-> (NFixed (b2 b) : s)
round_ = RoundingPattern -> (NFixed (b1 a) : s) :-> (NFixed (b2 b) : s)
forall (a :: Nat) (b :: Nat) r1 r2 (s :: [*])
(base :: Nat -> LorentzFixedBaseKind)
(f :: LorentzFixedBaseKind -> *).
(KnownNat a, KnownNat b, ForbidTicket (ToT (Unwrappabled r1)),
MichelsonCoercible r1 r2, SingI (ToT (Unwrappabled r1)),
Unwrappable r2, Unwrappable r1,
ArithOpHs Add Nat (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs
Add (Unwrappabled r2) (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs And (Unwrappabled r2) Nat Nat,
ArithOpHs
EDiv (Unwrappabled r1) Nat (Maybe (Unwrappabled r2, Nat)),
ArithOpHs Mul Nat r1 r1, LorentzFixedBase base, r1 ~ f (base a),
r2 ~ f (base b), NiceConstant (Unwrappabled r2),
Num (Unwrappabled r2)) =>
RoundingPattern -> (r1 : s) :-> (r2 : s)
roundingHelper RoundingPattern
Round
ceil_ :: forall (s :: [*]). (NFixed (b1 a) : s) :-> (NFixed (b2 b) : s)
ceil_ = RoundingPattern -> (NFixed (b1 a) : s) :-> (NFixed (b2 b) : s)
forall (a :: Nat) (b :: Nat) r1 r2 (s :: [*])
(base :: Nat -> LorentzFixedBaseKind)
(f :: LorentzFixedBaseKind -> *).
(KnownNat a, KnownNat b, ForbidTicket (ToT (Unwrappabled r1)),
MichelsonCoercible r1 r2, SingI (ToT (Unwrappabled r1)),
Unwrappable r2, Unwrappable r1,
ArithOpHs Add Nat (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs
Add (Unwrappabled r2) (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs And (Unwrappabled r2) Nat Nat,
ArithOpHs
EDiv (Unwrappabled r1) Nat (Maybe (Unwrappabled r2, Nat)),
ArithOpHs Mul Nat r1 r1, LorentzFixedBase base, r1 ~ f (base a),
r2 ~ f (base b), NiceConstant (Unwrappabled r2),
Num (Unwrappabled r2)) =>
RoundingPattern -> (r1 : s) :-> (r2 : s)
roundingHelper RoundingPattern
Ceil
floor_ :: forall (s :: [*]). (NFixed (b1 a) : s) :-> (NFixed (b2 b) : s)
floor_ = RoundingPattern -> (NFixed (b1 a) : s) :-> (NFixed (b2 b) : s)
forall (a :: Nat) (b :: Nat) r1 r2 (s :: [*])
(base :: Nat -> LorentzFixedBaseKind)
(f :: LorentzFixedBaseKind -> *).
(KnownNat a, KnownNat b, ForbidTicket (ToT (Unwrappabled r1)),
MichelsonCoercible r1 r2, SingI (ToT (Unwrappabled r1)),
Unwrappable r2, Unwrappable r1,
ArithOpHs Add Nat (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs
Add (Unwrappabled r2) (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs And (Unwrappabled r2) Nat Nat,
ArithOpHs
EDiv (Unwrappabled r1) Nat (Maybe (Unwrappabled r2, Nat)),
ArithOpHs Mul Nat r1 r1, LorentzFixedBase base, r1 ~ f (base a),
r2 ~ f (base b), NiceConstant (Unwrappabled r2),
Num (Unwrappabled r2)) =>
RoundingPattern -> (r1 : s) :-> (r2 : s)
roundingHelper RoundingPattern
Floor
fromFixed
:: forall a f base t s.
( a ~ f (base t)
, ToT (f (base 0)) ~ ToT (Unwrappabled a)
, LorentzRounding a (f (base 0))
)
=> a : s :-> Unwrappabled a : s
fromFixed :: forall {k} a (f :: k -> *) (base :: Nat -> k) (t :: Nat)
(s :: [*]).
(a ~ f (base t), ToT (f (base 0)) ~ ToT (Unwrappabled a),
LorentzRounding a (f (base 0))) =>
(a : s) :-> (Unwrappabled a : s)
fromFixed = forall a b (s :: [*]). LorentzRounding a b => (a : s) :-> (b : s)
round_ @_ @(f (base 0)) ((a : s) :-> (f (base 0) : s))
-> ((f (base 0) : s) :-> (Unwrappabled (f (base t)) : s))
-> (a : s) :-> (Unwrappabled (f (base t)) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (f (base 0) : s) :-> (Unwrappabled (f (base t)) : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_
toFixed
:: forall a f base t s.
( a ~ f (base t), LorentzFixedBase base
, Unwrappable a
, KnownNat t
, ArithOpHs Mul Natural (Unwrappabled a) (Unwrappabled a)
)
=> Unwrappabled a : s :-> a : s
toFixed :: forall a (f :: LorentzFixedBaseKind -> *)
(base :: Nat -> LorentzFixedBaseKind) (t :: Nat) (s :: [*]).
(a ~ f (base t), LorentzFixedBase base, Unwrappable a, KnownNat t,
ArithOpHs Mul Nat (Unwrappabled a) (Unwrappabled a)) =>
(Unwrappabled a : s) :-> (a : s)
toFixed = forall (base :: Nat -> LorentzFixedBaseKind) (exp :: Nat) b
(s :: [*]).
(KnownNat exp, ArithOpHs Mul Nat b b, LorentzFixedBase base) =>
(b : s) :-> (b : s)
rebase @base @t ((Unwrappabled (f (base t)) : s)
:-> (Unwrappabled (f (base t)) : s))
-> ((Unwrappabled (f (base t)) : s) :-> (a : s))
-> (Unwrappabled (f (base t)) : s) :-> (a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_ @(Unwrappabled a) @(f (base t))
type DivConstraint a b t r f b1 b2 =
( KnownNat b
, b1 ~ b2
, DivConstraint1 a t r f b1
)
type DivConstraint1 a t r f base =
( KnownNat a
, KnownNat t
, LorentzFixedBase base
, r ~ Maybe (f (base t))
)
instance DivConstraint a b t r Fixed b1 b2 => ArithOpHs Div (Fixed (b1 a)) (Fixed (b2 b)) r where
evalArithOpHs :: forall (s :: [*]). (Fixed (b1 a) : Fixed (b2 b) : s) :-> (r : s)
evalArithOpHs = (Fixed (b1 a) : Fixed (b2 b) : s) :-> (r : s)
(Fixed (b1 a) : Fixed (b2 b) : s) :-> (Maybe (Fixed (b2 t)) : s)
forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat)
(base :: Nat -> LorentzFixedBaseKind) any (s :: [*])
(f :: LorentzFixedBaseKind -> *) x y r.
(x ~ f (base t1), y ~ f (base t2), r ~ f (base t3),
LorentzFixedBase base, Each '[Unwrappable] '[x, y, r],
Each '[KnownNat] '[t1, t2, t3],
ArithOpHs
EDiv
(Unwrappabled x)
(Unwrappabled y)
(Maybe (Unwrappabled r, any)),
IsoValue r, Typeable f, ArithOpHs Mul Nat x x,
ArithOpHs Mul Nat y y) =>
(x : y : s) :-> (Maybe r : s)
fixedDivHelper
instance DivConstraint1 a t r Fixed b1 => ArithOpHs Div Integer (Fixed (b1 a)) r where
evalArithOpHs :: forall (s :: [*]). (Integer : Fixed (b1 a) : s) :-> (r : s)
evalArithOpHs = forall a (f :: LorentzFixedBaseKind -> *)
(base :: Nat -> LorentzFixedBaseKind) (t :: Nat) (s :: [*]).
(a ~ f (base t), LorentzFixedBase base, Unwrappable a, KnownNat t,
ArithOpHs Mul Nat (Unwrappabled a) (Unwrappabled a)) =>
(Unwrappabled a : s) :-> (a : s)
toFixed @_ @_ @_ @0 ((Integer : Fixed (b1 a) : s)
:-> (Fixed (b1 0) : Fixed (b1 a) : s))
-> ((Fixed (b1 0) : Fixed (b1 a) : s) :-> (r : s))
-> (Integer : Fixed (b1 a) : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (b1 0) : Fixed (b1 a) : s) :-> (r : s)
(Fixed (b1 0) : Fixed (b1 a) : s) :-> (Maybe (Fixed (b1 t)) : s)
forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat)
(base :: Nat -> LorentzFixedBaseKind) any (s :: [*])
(f :: LorentzFixedBaseKind -> *) x y r.
(x ~ f (base t1), y ~ f (base t2), r ~ f (base t3),
LorentzFixedBase base, Each '[Unwrappable] '[x, y, r],
Each '[KnownNat] '[t1, t2, t3],
ArithOpHs
EDiv
(Unwrappabled x)
(Unwrappabled y)
(Maybe (Unwrappabled r, any)),
IsoValue r, Typeable f, ArithOpHs Mul Nat x x,
ArithOpHs Mul Nat y y) =>
(x : y : s) :-> (Maybe r : s)
fixedDivHelper
instance DivConstraint1 a t r Fixed b1 => ArithOpHs Div Natural (Fixed (b1 a)) r where
evalArithOpHs :: forall (s :: [*]). (Nat : Fixed (b1 a) : s) :-> (r : s)
evalArithOpHs = (Nat : Fixed (b1 a) : s) :-> (Integer : Fixed (b1 a) : s)
forall i (s :: [*]).
ToIntegerArithOpHs i =>
(i : s) :-> (Integer : s)
int ((Nat : Fixed (b1 a) : s) :-> (Integer : Fixed (b1 a) : s))
-> ((Integer : Fixed (b1 a) : s)
:-> (Fixed (b1 0) : Fixed (b1 a) : s))
-> (Nat : Fixed (b1 a) : s) :-> (Fixed (b1 0) : Fixed (b1 a) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall a (f :: LorentzFixedBaseKind -> *)
(base :: Nat -> LorentzFixedBaseKind) (t :: Nat) (s :: [*]).
(a ~ f (base t), LorentzFixedBase base, Unwrappable a, KnownNat t,
ArithOpHs Mul Nat (Unwrappabled a) (Unwrappabled a)) =>
(Unwrappabled a : s) :-> (a : s)
toFixed @_ @_ @_ @0 ((Nat : Fixed (b1 a) : s) :-> (Fixed (b1 0) : Fixed (b1 a) : s))
-> ((Fixed (b1 0) : Fixed (b1 a) : s) :-> (r : s))
-> (Nat : Fixed (b1 a) : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (b1 0) : Fixed (b1 a) : s) :-> (r : s)
(Fixed (b1 0) : Fixed (b1 a) : s) :-> (Maybe (Fixed (b1 t)) : s)
forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat)
(base :: Nat -> LorentzFixedBaseKind) any (s :: [*])
(f :: LorentzFixedBaseKind -> *) x y r.
(x ~ f (base t1), y ~ f (base t2), r ~ f (base t3),
LorentzFixedBase base, Each '[Unwrappable] '[x, y, r],
Each '[KnownNat] '[t1, t2, t3],
ArithOpHs
EDiv
(Unwrappabled x)
(Unwrappabled y)
(Maybe (Unwrappabled r, any)),
IsoValue r, Typeable f, ArithOpHs Mul Nat x x,
ArithOpHs Mul Nat y y) =>
(x : y : s) :-> (Maybe r : s)
fixedDivHelper
instance DivConstraint a b t r NFixed b1 b2 => ArithOpHs Div (NFixed (b1 a)) (NFixed (b2 b)) r where
evalArithOpHs :: forall (s :: [*]). (NFixed (b1 a) : NFixed (b2 b) : s) :-> (r : s)
evalArithOpHs = (NFixed (b1 a) : NFixed (b2 b) : s) :-> (r : s)
(NFixed (b1 a) : NFixed (b2 b) : s) :-> (Maybe (NFixed (b2 t)) : s)
forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat)
(base :: Nat -> LorentzFixedBaseKind) any (s :: [*])
(f :: LorentzFixedBaseKind -> *) x y r.
(x ~ f (base t1), y ~ f (base t2), r ~ f (base t3),
LorentzFixedBase base, Each '[Unwrappable] '[x, y, r],
Each '[KnownNat] '[t1, t2, t3],
ArithOpHs
EDiv
(Unwrappabled x)
(Unwrappabled y)
(Maybe (Unwrappabled r, any)),
IsoValue r, Typeable f, ArithOpHs Mul Nat x x,
ArithOpHs Mul Nat y y) =>
(x : y : s) :-> (Maybe r : s)
fixedDivHelper
instance DivConstraint1 a t r NFixed b1 => ArithOpHs Div Natural (NFixed (b1 a)) r where
evalArithOpHs :: forall (s :: [*]). (Nat : NFixed (b1 a) : s) :-> (r : s)
evalArithOpHs = forall a (f :: LorentzFixedBaseKind -> *)
(base :: Nat -> LorentzFixedBaseKind) (t :: Nat) (s :: [*]).
(a ~ f (base t), LorentzFixedBase base, Unwrappable a, KnownNat t,
ArithOpHs Mul Nat (Unwrappabled a) (Unwrappabled a)) =>
(Unwrappabled a : s) :-> (a : s)
toFixed @_ @_ @_ @0 ((Nat : NFixed (b1 a) : s) :-> (NFixed (b1 0) : NFixed (b1 a) : s))
-> ((NFixed (b1 0) : NFixed (b1 a) : s) :-> (r : s))
-> (Nat : NFixed (b1 a) : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (NFixed (b1 0) : NFixed (b1 a) : s) :-> (r : s)
(NFixed (b1 0) : NFixed (b1 a) : s) :-> (Maybe (NFixed (b1 t)) : s)
forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat)
(base :: Nat -> LorentzFixedBaseKind) any (s :: [*])
(f :: LorentzFixedBaseKind -> *) x y r.
(x ~ f (base t1), y ~ f (base t2), r ~ f (base t3),
LorentzFixedBase base, Each '[Unwrappable] '[x, y, r],
Each '[KnownNat] '[t1, t2, t3],
ArithOpHs
EDiv
(Unwrappabled x)
(Unwrappabled y)
(Maybe (Unwrappabled r, any)),
IsoValue r, Typeable f, ArithOpHs Mul Nat x x,
ArithOpHs Mul Nat y y) =>
(x : y : s) :-> (Maybe r : s)
fixedDivHelper
instance DivConstraint1 a t r Fixed b1 => ArithOpHs Div Integer (NFixed (b1 a)) r where
evalArithOpHs :: forall (s :: [*]). (Integer : NFixed (b1 a) : s) :-> (r : s)
evalArithOpHs = forall a (f :: LorentzFixedBaseKind -> *)
(base :: Nat -> LorentzFixedBaseKind) (t :: Nat) (s :: [*]).
(a ~ f (base t), LorentzFixedBase base, Unwrappable a, KnownNat t,
ArithOpHs Mul Nat (Unwrappabled a) (Unwrappabled a)) =>
(Unwrappabled a : s) :-> (a : s)
toFixed @_ @_ @_ @0 ((Integer : NFixed (b1 a) : s)
:-> (Fixed (b1 0) : NFixed (b1 a) : s))
-> ((Fixed (b1 0) : NFixed (b1 a) : s)
:-> (Fixed (b1 0) : Fixed (b1 a) : s))
-> (Integer : NFixed (b1 a) : s)
:-> (Fixed (b1 0) : Fixed (b1 a) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((NFixed (b1 a) : s) :-> (Fixed (b1 a) : s))
-> (Fixed (b1 0) : NFixed (b1 a) : s)
:-> (Fixed (b1 0) : Fixed (b1 a) : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (NFixed (b1 a) : s) :-> (Fixed (b1 a) : s)
forall {k} (p :: k) (s :: [*]). (NFixed p : s) :-> (Fixed p : s)
castNFixedToFixed ((Integer : NFixed (b1 a) : s)
:-> (Fixed (b1 0) : Fixed (b1 a) : s))
-> ((Fixed (b1 0) : Fixed (b1 a) : s) :-> (r : s))
-> (Integer : NFixed (b1 a) : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (b1 0) : Fixed (b1 a) : s) :-> (r : s)
(Fixed (b1 0) : Fixed (b1 a) : s) :-> (Maybe (Fixed (b1 t)) : s)
forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat)
(base :: Nat -> LorentzFixedBaseKind) any (s :: [*])
(f :: LorentzFixedBaseKind -> *) x y r.
(x ~ f (base t1), y ~ f (base t2), r ~ f (base t3),
LorentzFixedBase base, Each '[Unwrappable] '[x, y, r],
Each '[KnownNat] '[t1, t2, t3],
ArithOpHs
EDiv
(Unwrappabled x)
(Unwrappabled y)
(Maybe (Unwrappabled r, any)),
IsoValue r, Typeable f, ArithOpHs Mul Nat x x,
ArithOpHs Mul Nat y y) =>
(x : y : s) :-> (Maybe r : s)
fixedDivHelper
type DivIntegralConstraint r b =
( KnownNat r
, LorentzFixedBase b
)
instance DivIntegralConstraint r b => ArithOpHs Div Integer Integer (Maybe (Fixed (b r))) where
evalArithOpHs :: forall (s :: [*]).
(Integer : Integer : s) :-> (Maybe (Fixed (b r)) : s)
evalArithOpHs = forall a (f :: LorentzFixedBaseKind -> *)
(base :: Nat -> LorentzFixedBaseKind) (t :: Nat) (s :: [*]).
(a ~ f (base t), LorentzFixedBase base, Unwrappable a, KnownNat t,
ArithOpHs Mul Nat (Unwrappabled a) (Unwrappabled a)) =>
(Unwrappabled a : s) :-> (a : s)
toFixed @(Fixed (b r)) ((Integer : Integer : s) :-> (Fixed (b r) : Integer : s))
-> ((Fixed (b r) : Integer : s)
:-> (Fixed (b r) : Fixed (b 0) : s))
-> (Integer : Integer : s) :-> (Fixed (b r) : Fixed (b 0) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((Integer : s) :-> (Fixed (b 0) : s))
-> (Fixed (b r) : Integer : s) :-> (Fixed (b r) : Fixed (b 0) : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (forall a (f :: LorentzFixedBaseKind -> *)
(base :: Nat -> LorentzFixedBaseKind) (t :: Nat) (s :: [*]).
(a ~ f (base t), LorentzFixedBase base, Unwrappable a, KnownNat t,
ArithOpHs Mul Nat (Unwrappabled a) (Unwrappabled a)) =>
(Unwrappabled a : s) :-> (a : s)
toFixed @(Fixed (b 0))) ((Integer : Integer : s) :-> (Fixed (b r) : Fixed (b 0) : s))
-> ((Fixed (b r) : Fixed (b 0) : s) :-> (Maybe (Fixed (b r)) : s))
-> (Integer : Integer : s) :-> (Maybe (Fixed (b r)) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (b r) : Fixed (b 0) : s) :-> (Maybe (Fixed (b r)) : s)
forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat)
(base :: Nat -> LorentzFixedBaseKind) any (s :: [*])
(f :: LorentzFixedBaseKind -> *) x y r.
(x ~ f (base t1), y ~ f (base t2), r ~ f (base t3),
LorentzFixedBase base, Each '[Unwrappable] '[x, y, r],
Each '[KnownNat] '[t1, t2, t3],
ArithOpHs
EDiv
(Unwrappabled x)
(Unwrappabled y)
(Maybe (Unwrappabled r, any)),
IsoValue r, Typeable f, ArithOpHs Mul Nat x x,
ArithOpHs Mul Nat y y) =>
(x : y : s) :-> (Maybe r : s)
fixedDivHelper
instance DivIntegralConstraint r b => ArithOpHs Div Natural Natural (Maybe (Fixed (b r))) where
evalArithOpHs :: forall (s :: [*]). (Nat : Nat : s) :-> (Maybe (Fixed (b r)) : s)
evalArithOpHs = (Nat : Nat : s) :-> (Integer : Nat : s)
forall i (s :: [*]).
ToIntegerArithOpHs i =>
(i : s) :-> (Integer : s)
int ((Nat : Nat : s) :-> (Integer : Nat : s))
-> ((Integer : Nat : s) :-> (Fixed (b r) : Nat : s))
-> (Nat : Nat : s) :-> (Fixed (b r) : Nat : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall a (f :: LorentzFixedBaseKind -> *)
(base :: Nat -> LorentzFixedBaseKind) (t :: Nat) (s :: [*]).
(a ~ f (base t), LorentzFixedBase base, Unwrappable a, KnownNat t,
ArithOpHs Mul Nat (Unwrappabled a) (Unwrappabled a)) =>
(Unwrappabled a : s) :-> (a : s)
toFixed @(Fixed (b r)) ((Nat : Nat : s) :-> (Fixed (b r) : Nat : s))
-> ((Fixed (b r) : Nat : s) :-> (Fixed (b r) : Fixed (b 0) : s))
-> (Nat : Nat : s) :-> (Fixed (b r) : Fixed (b 0) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((Nat : s) :-> (Fixed (b 0) : s))
-> (Fixed (b r) : Nat : s) :-> (Fixed (b r) : Fixed (b 0) : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip ((Nat : s) :-> (Integer : s)
forall i (s :: [*]).
ToIntegerArithOpHs i =>
(i : s) :-> (Integer : s)
int ((Nat : s) :-> (Integer : s))
-> ((Integer : s) :-> (Fixed (b 0) : s))
-> (Nat : s) :-> (Fixed (b 0) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall a (f :: LorentzFixedBaseKind -> *)
(base :: Nat -> LorentzFixedBaseKind) (t :: Nat) (s :: [*]).
(a ~ f (base t), LorentzFixedBase base, Unwrappable a, KnownNat t,
ArithOpHs Mul Nat (Unwrappabled a) (Unwrappabled a)) =>
(Unwrappabled a : s) :-> (a : s)
toFixed @(Fixed (b 0))) ((Nat : Nat : s) :-> (Fixed (b r) : Fixed (b 0) : s))
-> ((Fixed (b r) : Fixed (b 0) : s) :-> (Maybe (Fixed (b r)) : s))
-> (Nat : Nat : s) :-> (Maybe (Fixed (b r)) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (b r) : Fixed (b 0) : s) :-> (Maybe (Fixed (b r)) : s)
forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat)
(base :: Nat -> LorentzFixedBaseKind) any (s :: [*])
(f :: LorentzFixedBaseKind -> *) x y r.
(x ~ f (base t1), y ~ f (base t2), r ~ f (base t3),
LorentzFixedBase base, Each '[Unwrappable] '[x, y, r],
Each '[KnownNat] '[t1, t2, t3],
ArithOpHs
EDiv
(Unwrappabled x)
(Unwrappabled y)
(Maybe (Unwrappabled r, any)),
IsoValue r, Typeable f, ArithOpHs Mul Nat x x,
ArithOpHs Mul Nat y y) =>
(x : y : s) :-> (Maybe r : s)
fixedDivHelper
instance DivIntegralConstraint r b => ArithOpHs Div Integer Natural (Maybe (Fixed (b r))) where
evalArithOpHs :: forall (s :: [*]).
(Integer : Nat : s) :-> (Maybe (Fixed (b r)) : s)
evalArithOpHs = forall a (f :: LorentzFixedBaseKind -> *)
(base :: Nat -> LorentzFixedBaseKind) (t :: Nat) (s :: [*]).
(a ~ f (base t), LorentzFixedBase base, Unwrappable a, KnownNat t,
ArithOpHs Mul Nat (Unwrappabled a) (Unwrappabled a)) =>
(Unwrappabled a : s) :-> (a : s)
toFixed @(Fixed (b r)) ((Integer : Nat : s) :-> (Fixed (b r) : Nat : s))
-> ((Fixed (b r) : Nat : s) :-> (Fixed (b r) : Fixed (b 0) : s))
-> (Integer : Nat : s) :-> (Fixed (b r) : Fixed (b 0) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((Nat : s) :-> (Fixed (b 0) : s))
-> (Fixed (b r) : Nat : s) :-> (Fixed (b r) : Fixed (b 0) : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip ((Nat : s) :-> (Integer : s)
forall i (s :: [*]).
ToIntegerArithOpHs i =>
(i : s) :-> (Integer : s)
int ((Nat : s) :-> (Integer : s))
-> ((Integer : s) :-> (Fixed (b 0) : s))
-> (Nat : s) :-> (Fixed (b 0) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall a (f :: LorentzFixedBaseKind -> *)
(base :: Nat -> LorentzFixedBaseKind) (t :: Nat) (s :: [*]).
(a ~ f (base t), LorentzFixedBase base, Unwrappable a, KnownNat t,
ArithOpHs Mul Nat (Unwrappabled a) (Unwrappabled a)) =>
(Unwrappabled a : s) :-> (a : s)
toFixed @(Fixed (b 0))) ((Integer : Nat : s) :-> (Fixed (b r) : Fixed (b 0) : s))
-> ((Fixed (b r) : Fixed (b 0) : s) :-> (Maybe (Fixed (b r)) : s))
-> (Integer : Nat : s) :-> (Maybe (Fixed (b r)) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (b r) : Fixed (b 0) : s) :-> (Maybe (Fixed (b r)) : s)
forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat)
(base :: Nat -> LorentzFixedBaseKind) any (s :: [*])
(f :: LorentzFixedBaseKind -> *) x y r.
(x ~ f (base t1), y ~ f (base t2), r ~ f (base t3),
LorentzFixedBase base, Each '[Unwrappable] '[x, y, r],
Each '[KnownNat] '[t1, t2, t3],
ArithOpHs
EDiv
(Unwrappabled x)
(Unwrappabled y)
(Maybe (Unwrappabled r, any)),
IsoValue r, Typeable f, ArithOpHs Mul Nat x x,
ArithOpHs Mul Nat y y) =>
(x : y : s) :-> (Maybe r : s)
fixedDivHelper
instance DivIntegralConstraint r b => ArithOpHs Div Natural Integer (Maybe (Fixed (b r))) where
evalArithOpHs :: forall (s :: [*]).
(Nat : Integer : s) :-> (Maybe (Fixed (b r)) : s)
evalArithOpHs = (Nat : Integer : s) :-> (Integer : Integer : s)
forall i (s :: [*]).
ToIntegerArithOpHs i =>
(i : s) :-> (Integer : s)
int ((Nat : Integer : s) :-> (Integer : Integer : s))
-> ((Integer : Integer : s) :-> (Fixed (b r) : Integer : s))
-> (Nat : Integer : s) :-> (Fixed (b r) : Integer : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall a (f :: LorentzFixedBaseKind -> *)
(base :: Nat -> LorentzFixedBaseKind) (t :: Nat) (s :: [*]).
(a ~ f (base t), LorentzFixedBase base, Unwrappable a, KnownNat t,
ArithOpHs Mul Nat (Unwrappabled a) (Unwrappabled a)) =>
(Unwrappabled a : s) :-> (a : s)
toFixed @(Fixed (b r)) ((Nat : Integer : s) :-> (Fixed (b r) : Integer : s))
-> ((Fixed (b r) : Integer : s)
:-> (Fixed (b r) : Fixed (b 0) : s))
-> (Nat : Integer : s) :-> (Fixed (b r) : Fixed (b 0) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((Integer : s) :-> (Fixed (b 0) : s))
-> (Fixed (b r) : Integer : s) :-> (Fixed (b r) : Fixed (b 0) : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (forall a (f :: LorentzFixedBaseKind -> *)
(base :: Nat -> LorentzFixedBaseKind) (t :: Nat) (s :: [*]).
(a ~ f (base t), LorentzFixedBase base, Unwrappable a, KnownNat t,
ArithOpHs Mul Nat (Unwrappabled a) (Unwrappabled a)) =>
(Unwrappabled a : s) :-> (a : s)
toFixed @(Fixed (b 0))) ((Nat : Integer : s) :-> (Fixed (b r) : Fixed (b 0) : s))
-> ((Fixed (b r) : Fixed (b 0) : s) :-> (Maybe (Fixed (b r)) : s))
-> (Nat : Integer : s) :-> (Maybe (Fixed (b r)) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (b r) : Fixed (b 0) : s) :-> (Maybe (Fixed (b r)) : s)
forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat)
(base :: Nat -> LorentzFixedBaseKind) any (s :: [*])
(f :: LorentzFixedBaseKind -> *) x y r.
(x ~ f (base t1), y ~ f (base t2), r ~ f (base t3),
LorentzFixedBase base, Each '[Unwrappable] '[x, y, r],
Each '[KnownNat] '[t1, t2, t3],
ArithOpHs
EDiv
(Unwrappabled x)
(Unwrappabled y)
(Maybe (Unwrappabled r, any)),
IsoValue r, Typeable f, ArithOpHs Mul Nat x x,
ArithOpHs Mul Nat y y) =>
(x : y : s) :-> (Maybe r : s)
fixedDivHelper
instance DivIntegralConstraint r b => ArithOpHs Div Natural Natural (Maybe (NFixed (b r))) where
evalArithOpHs :: forall (s :: [*]). (Nat : Nat : s) :-> (Maybe (NFixed (b r)) : s)
evalArithOpHs = forall a (f :: LorentzFixedBaseKind -> *)
(base :: Nat -> LorentzFixedBaseKind) (t :: Nat) (s :: [*]).
(a ~ f (base t), LorentzFixedBase base, Unwrappable a, KnownNat t,
ArithOpHs Mul Nat (Unwrappabled a) (Unwrappabled a)) =>
(Unwrappabled a : s) :-> (a : s)
toFixed @(NFixed (b r)) ((Nat : Nat : s) :-> (NFixed (b r) : Nat : s))
-> ((NFixed (b r) : Nat : s) :-> (NFixed (b r) : NFixed (b r) : s))
-> (Nat : Nat : s) :-> (NFixed (b r) : NFixed (b r) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((Nat : s) :-> (NFixed (b r) : s))
-> (NFixed (b r) : Nat : s) :-> (NFixed (b r) : NFixed (b r) : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (forall a (f :: LorentzFixedBaseKind -> *)
(base :: Nat -> LorentzFixedBaseKind) (t :: Nat) (s :: [*]).
(a ~ f (base t), LorentzFixedBase base, Unwrappable a, KnownNat t,
ArithOpHs Mul Nat (Unwrappabled a) (Unwrappabled a)) =>
(Unwrappabled a : s) :-> (a : s)
toFixed @(NFixed (b r))) ((Nat : Nat : s) :-> (NFixed (b r) : NFixed (b r) : s))
-> ((NFixed (b r) : NFixed (b r) : s)
:-> (Maybe (NFixed (b r)) : s))
-> (Nat : Nat : s) :-> (Maybe (NFixed (b r)) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (NFixed (b r) : NFixed (b r) : s) :-> (Maybe (NFixed (b r)) : s)
forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat)
(base :: Nat -> LorentzFixedBaseKind) any (s :: [*])
(f :: LorentzFixedBaseKind -> *) x y r.
(x ~ f (base t1), y ~ f (base t2), r ~ f (base t3),
LorentzFixedBase base, Each '[Unwrappable] '[x, y, r],
Each '[KnownNat] '[t1, t2, t3],
ArithOpHs
EDiv
(Unwrappabled x)
(Unwrappabled y)
(Maybe (Unwrappabled r, any)),
IsoValue r, Typeable f, ArithOpHs Mul Nat x x,
ArithOpHs Mul Nat y y) =>
(x : y : s) :-> (Maybe r : s)
fixedDivHelper
castNFixedToFixed :: NFixed p : s :-> Fixed p : s
castNFixedToFixed :: forall {k} (p :: k) (s :: [*]). (NFixed p : s) :-> (Fixed p : s)
castNFixedToFixed = (NFixed p : s) :-> (Integer : s)
forall i (s :: [*]).
ToIntegerArithOpHs i =>
(i : s) :-> (Integer : s)
int ((NFixed p : s) :-> (Integer : s))
-> ((Integer : s) :-> (Fixed p : s))
-> (NFixed p : s) :-> (Fixed p : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : s) :-> (Fixed p : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_
castFixedToNFixed :: Fixed p : s :-> Maybe (NFixed p) : s
castFixedToNFixed :: forall {k} (p :: k) (s :: [*]).
(Fixed p : s) :-> (Maybe (NFixed p) : s)
castFixedToNFixed = (Fixed p : s) :-> (Integer : s)
(Fixed p : s) :-> (Unwrappabled (Fixed p) : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((Fixed p : s) :-> (Integer : s))
-> ((Integer : s) :-> (Maybe Nat : s))
-> (Fixed p : s) :-> (Maybe Nat : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : s) :-> (Maybe Nat : s)
forall (s :: [*]). (Integer : s) :-> (Maybe Nat : s)
isNat ((Fixed p : s) :-> (Maybe Nat : s))
-> ((Maybe Nat : s) :-> (Maybe (NFixed p) : s))
-> (Fixed p : s) :-> (Maybe (NFixed p) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Maybe Nat : s) :-> (Maybe (NFixed p) : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_
unsafeCastFixedToNFixed :: Fixed p : s :-> NFixed p : s
unsafeCastFixedToNFixed :: forall {k} (p :: k) (s :: [*]). (Fixed p : s) :-> (NFixed p : s)
unsafeCastFixedToNFixed = (Fixed p : s) :-> (Integer : s)
(Fixed p : s) :-> (Unwrappabled (Fixed p) : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((Fixed p : s) :-> (Integer : s))
-> ((Integer : s) :-> (Nat : s)) -> (Fixed p : s) :-> (Nat : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : s) :-> (Nat : s)
(Integer : s) :-> (UnaryArithResHs Abs Integer : s)
forall n (s :: [*]).
UnaryArithOpHs Abs n =>
(n : s) :-> (UnaryArithResHs Abs n : s)
Lorentz.Instr.abs ((Fixed p : s) :-> (Nat : s))
-> ((Nat : s) :-> (NFixed p : s))
-> (Fixed p : s) :-> (NFixed p : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Nat : s) :-> (NFixed p : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_
instance (r ~ Maybe (Integer, NFixed (base a)), KnownNat a, LorentzFixedBase base)
=> ArithOpHs EDiv (Fixed (base a)) Integer r where
evalArithOpHs :: forall (s :: [*]). (Fixed (base a) : Integer : s) :-> (r : s)
evalArithOpHs = (Fixed (base a) : Integer : s) :-> (r : s)
(Fixed (base a) : Integer : s)
:-> (Maybe (Integer, NFixed (base a)) : s)
forall (a :: Nat) (base :: Nat -> LorentzFixedBaseKind) x y r1 r2
(s :: [*]) (f :: LorentzFixedBaseKind -> *).
(KnownNat a, ArithOpHs Mul Nat y y,
ArithOpHs EDiv (Unwrappabled x) y (Maybe (r1, Unwrappabled r2)),
Unwrappable x, Unwrappable r2, LorentzFixedBase base,
x ~ f (base a)) =>
(x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper
instance (r ~ Maybe (Integer, NFixed (base a)), KnownNat a, LorentzFixedBase base)
=> ArithOpHs EDiv (Fixed (base a)) Natural r where
evalArithOpHs :: forall (s :: [*]). (Fixed (base a) : Nat : s) :-> (r : s)
evalArithOpHs = (Fixed (base a) : Nat : s) :-> (r : s)
(Fixed (base a) : Nat : s)
:-> (Maybe (Integer, NFixed (base a)) : s)
forall (a :: Nat) (base :: Nat -> LorentzFixedBaseKind) x y r1 r2
(s :: [*]) (f :: LorentzFixedBaseKind -> *).
(KnownNat a, ArithOpHs Mul Nat y y,
ArithOpHs EDiv (Unwrappabled x) y (Maybe (r1, Unwrappabled r2)),
Unwrappable x, Unwrappable r2, LorentzFixedBase base,
x ~ f (base a)) =>
(x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper
instance (r ~ Maybe (Integer, NFixed (base a)), KnownNat a, LorentzFixedBase base)
=> ArithOpHs EDiv (NFixed (base a)) Integer r where
evalArithOpHs :: forall (s :: [*]). (NFixed (base a) : Integer : s) :-> (r : s)
evalArithOpHs = (NFixed (base a) : Integer : s) :-> (r : s)
(NFixed (base a) : Integer : s)
:-> (Maybe (Integer, NFixed (base a)) : s)
forall (a :: Nat) (base :: Nat -> LorentzFixedBaseKind) x y r1 r2
(s :: [*]) (f :: LorentzFixedBaseKind -> *).
(KnownNat a, ArithOpHs Mul Nat y y,
ArithOpHs EDiv (Unwrappabled x) y (Maybe (r1, Unwrappabled r2)),
Unwrappable x, Unwrappable r2, LorentzFixedBase base,
x ~ f (base a)) =>
(x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper
instance (r ~ Maybe (Natural, NFixed (base a)), KnownNat a, LorentzFixedBase base)
=> ArithOpHs EDiv (NFixed (base a)) Natural r where
evalArithOpHs :: forall (s :: [*]). (NFixed (base a) : Nat : s) :-> (r : s)
evalArithOpHs = (NFixed (base a) : Nat : s) :-> (r : s)
(NFixed (base a) : Nat : s) :-> (Maybe (Nat, NFixed (base a)) : s)
forall (a :: Nat) (base :: Nat -> LorentzFixedBaseKind) x y r1 r2
(s :: [*]) (f :: LorentzFixedBaseKind -> *).
(KnownNat a, ArithOpHs Mul Nat y y,
ArithOpHs EDiv (Unwrappabled x) y (Maybe (r1, Unwrappabled r2)),
Unwrappable x, Unwrappable r2, LorentzFixedBase base,
x ~ f (base a)) =>
(x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper
data RoundingPattern = Round | Ceil | Floor
roundingHelper
:: forall a b r1 r2 s base f.
( KnownNat a, KnownNat b
, ForbidTicket (ToT (Unwrappabled r1))
, MichelsonCoercible r1 r2
, SingI (ToT (Unwrappabled r1))
, Unwrappable r2
, Unwrappable r1
, ArithOpHs Add Natural (Unwrappabled r2) (Unwrappabled r2)
, ArithOpHs Add (Unwrappabled r2) (Unwrappabled r2) (Unwrappabled r2)
, ArithOpHs And (Unwrappabled r2) Natural Natural
, ArithOpHs EDiv (Unwrappabled r1) Natural (Maybe (Unwrappabled r2, Natural))
, ArithOpHs Mul Natural r1 r1
, LorentzFixedBase base
, r1 ~ f (base a)
, r2 ~ f (base b)
, NiceConstant (Unwrappabled r2)
, Num (Unwrappabled r2)
)
=> RoundingPattern -> (r1 : s :-> r2 : s)
roundingHelper :: forall (a :: Nat) (b :: Nat) r1 r2 (s :: [*])
(base :: Nat -> LorentzFixedBaseKind)
(f :: LorentzFixedBaseKind -> *).
(KnownNat a, KnownNat b, ForbidTicket (ToT (Unwrappabled r1)),
MichelsonCoercible r1 r2, SingI (ToT (Unwrappabled r1)),
Unwrappable r2, Unwrappable r1,
ArithOpHs Add Nat (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs
Add (Unwrappabled r2) (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs And (Unwrappabled r2) Nat Nat,
ArithOpHs
EDiv (Unwrappabled r1) Nat (Maybe (Unwrappabled r2, Nat)),
ArithOpHs Mul Nat r1 r1, LorentzFixedBase base, r1 ~ f (base a),
r2 ~ f (base b), NiceConstant (Unwrappabled r2),
Num (Unwrappabled r2)) =>
RoundingPattern -> (r1 : s) :-> (r2 : s)
roundingHelper RoundingPattern
rp =
let Nat
halfBase :: Natural = Nat
base Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
`P.div` Nat
2
Integer
powDifference :: Integer = Proxy b -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @b) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Proxy a -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)
newPow :: Nat
newPow = Nat
2 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
* Nat
halfNewPow
Nat
halfNewPow :: Natural = Nat
halfBase Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
* (Nat
base Nat -> Integer -> Nat
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer -> Integer
forall a. Num a => a -> a
Prelude.abs Integer
powDifference Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1))
base :: Nat
base = forall (a :: Nat -> LorentzFixedBaseKind) b.
(LorentzFixedBase a, Num b) =>
b
getBase @base
in case () of
()
_ | Integer
powDifference Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 -> ((r1 : s) :-> (r2 : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_ :: (r1 : s :-> r2 : s))
| Integer
powDifference Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 ->
Nat -> (r1 : s) :-> (Nat : r1 : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Nat
newPow ((r1 : s) :-> (Nat : r1 : s))
-> ((Nat : r1 : s) :-> (r1 : s)) -> (r1 : s) :-> (r1 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Nat : r1 : s) :-> (r1 : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul ((r1 : s) :-> (r1 : s))
-> ((r1 : s) :-> (r2 : s)) -> (r1 : s) :-> (r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((r1 : s) :-> (r2 : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_ :: (r1 : s :-> r2 : s))
| Bool
otherwise ->
Nat -> (r1 : s) :-> (Nat : r1 : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Nat
newPow ((r1 : s) :-> (Nat : r1 : s))
-> ((Nat : r1 : s) :-> (r1 : Nat : s))
-> (r1 : s) :-> (r1 : Nat : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(Nat : r1 : s) :-> (r1 : Nat : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((r1 : s) :-> (r1 : Nat : s))
-> ((r1 : Nat : s) :-> (Unwrappabled (f (base a)) : Nat : s))
-> (r1 : s) :-> (Unwrappabled (f (base a)) : Nat : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(r1 : Nat : s) :-> (Unwrappabled r1 : Nat : s)
(r1 : Nat : s) :-> (Unwrappabled (f (base a)) : Nat : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((r1 : s) :-> (Unwrappabled (f (base a)) : Nat : s))
-> ((Unwrappabled (f (base a)) : Nat : s)
:-> (Maybe (Unwrappabled (f (base b)), Nat) : s))
-> (r1 : s) :-> (Maybe (Unwrappabled (f (base b)), Nat) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Unwrappabled (f (base a)) : Nat : s)
:-> (Maybe (Unwrappabled (f (base b)), Nat) : s)
forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv ((r1 : s) :-> (Maybe (Unwrappabled (f (base b)), Nat) : s))
-> ((Maybe (Unwrappabled (f (base b)), Nat) : s)
:-> ((Unwrappabled (f (base b)), Nat) : s))
-> (r1 : s) :-> ((Unwrappabled (f (base b)), Nat) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
Impossible "Division by zero impossible here"
-> (Maybe (Unwrappabled (f (base b)), Nat) : s)
:-> ((Unwrappabled (f (base b)), Nat) : s)
forall err a (s :: [*]).
IsError err =>
err -> (Maybe a : s) :-> (a : s)
assertSome (forall (reason :: Symbol). HasCallStack => Impossible reason
Impossible @"Division by zero impossible here") ((r1 : s) :-> ((Unwrappabled (f (base b)), Nat) : s))
-> (((Unwrappabled (f (base b)), Nat) : s)
:-> (Unwrappabled (f (base b)) : s))
-> (r1 : s) :-> (Unwrappabled (f (base b)) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
case RoundingPattern
rp of
RoundingPattern
Round ->
((Unwrappabled (f (base b)), Nat) : s)
:-> (Unwrappabled (f (base b)) : Nat : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair (((Unwrappabled (f (base b)), Nat) : s)
:-> (Unwrappabled (f (base b)) : Nat : s))
-> ((Unwrappabled (f (base b)) : Nat : s)
:-> (Nat : Unwrappabled (f (base b)) : s))
-> ((Unwrappabled (f (base b)), Nat) : s)
:-> (Nat : Unwrappabled (f (base b)) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(Unwrappabled (f (base b)) : Nat : s)
:-> (Nat : Unwrappabled (f (base b)) : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap (((Unwrappabled (f (base b)), Nat) : s)
:-> (Nat : Unwrappabled (f (base b)) : s))
-> ((Nat : Unwrappabled (f (base b)) : s)
:-> (Nat : Nat : Unwrappabled (f (base b)) : s))
-> ((Unwrappabled (f (base b)), Nat) : s)
:-> (Nat : Nat : Unwrappabled (f (base b)) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
Nat
-> (Nat : Unwrappabled (f (base b)) : s)
:-> (Nat : Nat : Unwrappabled (f (base b)) : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Nat
halfNewPow (((Unwrappabled (f (base b)), Nat) : s)
:-> (Nat : Nat : Unwrappabled (f (base b)) : s))
-> ((Nat : Nat : Unwrappabled (f (base b)) : s)
:-> (Integer : Unwrappabled (f (base b)) : s))
-> ((Unwrappabled (f (base b)), Nat) : s)
:-> (Integer : Unwrappabled (f (base b)) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(Nat : Nat : Unwrappabled (f (base b)) : s)
:-> (Integer : Unwrappabled (f (base b)) : s)
forall n (s :: [*]).
NiceComparable n =>
(n : n : s) :-> (Integer : s)
compare (((Unwrappabled (f (base b)), Nat) : s)
:-> (Integer : Unwrappabled (f (base b)) : s))
-> ((Integer : Unwrappabled (f (base b)) : s)
:-> (Integer : Integer : Unwrappabled (f (base b)) : s))
-> ((Unwrappabled (f (base b)), Nat) : s)
:-> (Integer : Integer : Unwrappabled (f (base b)) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(Integer : Unwrappabled (f (base b)) : s)
:-> (Integer : Integer : Unwrappabled (f (base b)) : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup (((Unwrappabled (f (base b)), Nat) : s)
:-> (Integer : Integer : Unwrappabled (f (base b)) : s))
-> ((Integer : Integer : Unwrappabled (f (base b)) : s)
:-> (Unwrappabled (f (base b)) : s))
-> ((Unwrappabled (f (base b)), Nat) : s)
:-> (Unwrappabled (f (base b)) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((Integer : Unwrappabled (f (base b)) : s)
:-> (Unwrappabled (f (base b)) : s))
-> ((Integer : Unwrappabled (f (base b)) : s)
:-> (Unwrappabled (f (base b)) : s))
-> (Integer : Integer : Unwrappabled (f (base b)) : s)
:-> (Unwrappabled (f (base b)) : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Ge =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifGe0 (Integer : Unwrappabled (f (base b)) : s)
:-> (Unwrappabled (f (base b)) : s)
forall a (s :: [*]). (a : s) :-> s
drop (
((Unwrappabled (f (base b)) : s)
:-> (Nat : Unwrappabled (f (base b)) : s))
-> (Integer : Unwrappabled (f (base b)) : s)
:-> (Integer : Nat : Unwrappabled (f (base b)) : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Nat
-> (Unwrappabled (f (base b)) : s)
:-> (Nat : Unwrappabled (f (base b)) : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Nat
1 :: Natural)) ((Integer : Unwrappabled (f (base b)) : s)
:-> (Integer : Nat : Unwrappabled (f (base b)) : s))
-> ((Integer : Nat : Unwrappabled (f (base b)) : s)
:-> (Nat : Unwrappabled (f (base b)) : s))
-> (Integer : Unwrappabled (f (base b)) : s)
:-> (Nat : Unwrappabled (f (base b)) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((Nat : Unwrappabled (f (base b)) : s)
:-> (Nat : Unwrappabled (f (base b)) : s))
-> ((Nat : Unwrappabled (f (base b)) : s)
:-> (Nat : Unwrappabled (f (base b)) : s))
-> (Integer : Nat : Unwrappabled (f (base b)) : s)
:-> (Nat : Unwrappabled (f (base b)) : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Eq' =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifEq0 (forall (n :: Nat) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @2 ((Nat : Unwrappabled (f (base b)) : s)
:-> (Unwrappabled (f (base b))
: Nat : Unwrappabled (f (base b)) : s))
-> ((Unwrappabled (f (base b))
: Nat : Unwrappabled (f (base b)) : s)
:-> (Nat : Unwrappabled (f (base b)) : s))
-> (Nat : Unwrappabled (f (base b)) : s)
:-> (Nat : Unwrappabled (f (base b)) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Unwrappabled (f (base b)) : Nat : Unwrappabled (f (base b)) : s)
:-> (Nat : Unwrappabled (f (base b)) : s)
forall n m r (s :: [*]).
ArithOpHs And n m r =>
(n : m : s) :-> (r : s)
and) (Nat : Unwrappabled (f (base b)) : s)
:-> (Nat : Unwrappabled (f (base b)) : s)
forall (s :: [*]). s :-> s
nop ((Integer : Unwrappabled (f (base b)) : s)
:-> (Nat : Unwrappabled (f (base b)) : s))
-> ((Nat : Unwrappabled (f (base b)) : s)
:-> (Unwrappabled (f (base b)) : s))
-> (Integer : Unwrappabled (f (base b)) : s)
:-> (Unwrappabled (f (base b)) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(Nat : Unwrappabled (f (base b)) : s)
:-> (Unwrappabled (f (base b)) : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
)
RoundingPattern
Ceil ->
((Unwrappabled (f (base b)), Nat) : s)
:-> (Unwrappabled (f (base b)) : Nat : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair (((Unwrappabled (f (base b)), Nat) : s)
:-> (Unwrappabled (f (base b)) : Nat : s))
-> ((Unwrappabled (f (base b)) : Nat : s)
:-> (Nat : Unwrappabled (f (base b)) : s))
-> ((Unwrappabled (f (base b)), Nat) : s)
:-> (Nat : Unwrappabled (f (base b)) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(Unwrappabled (f (base b)) : Nat : s)
:-> (Nat : Unwrappabled (f (base b)) : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap (((Unwrappabled (f (base b)), Nat) : s)
:-> (Nat : Unwrappabled (f (base b)) : s))
-> ((Nat : Unwrappabled (f (base b)) : s)
:-> (Unwrappabled (f (base b)) : s))
-> ((Unwrappabled (f (base b)), Nat) : s)
:-> (Unwrappabled (f (base b)) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((Unwrappabled (f (base b)) : s)
:-> (Unwrappabled (f (base b)) : s))
-> ((Unwrappabled (f (base b)) : s)
:-> (Unwrappabled (f (base b)) : s))
-> (Nat : Unwrappabled (f (base b)) : s)
:-> (Unwrappabled (f (base b)) : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Neq =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifNeq0 (Unwrappabled (f (base b))
-> (Unwrappabled (f (base b)) : s)
:-> (Unwrappabled (f (base b)) : Unwrappabled (f (base b)) : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Unwrappabled r2
Unwrappabled (f (base b))
1 :: Unwrappabled r2) ((Unwrappabled (f (base b)) : s)
:-> (Unwrappabled (f (base b)) : Unwrappabled (f (base b)) : s))
-> ((Unwrappabled (f (base b)) : Unwrappabled (f (base b)) : s)
:-> (Unwrappabled (f (base b)) : s))
-> (Unwrappabled (f (base b)) : s)
:-> (Unwrappabled (f (base b)) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Unwrappabled (f (base b)) : Unwrappabled (f (base b)) : s)
:-> (Unwrappabled (f (base b)) : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add) (Unwrappabled (f (base b)) : s) :-> (Unwrappabled (f (base b)) : s)
forall (s :: [*]). s :-> s
nop
RoundingPattern
Floor -> ((Unwrappabled (f (base b)), Nat) : s)
:-> (Unwrappabled (f (base b)) : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : s)
car
# unsafeCoerceWrap
fixedDivHelper
:: forall t1 t2 t3 base any s f x y r.
( x ~ f (base t1), y ~ f (base t2), r ~ f (base t3)
, LorentzFixedBase base
, Each '[Unwrappable] '[x, y, r]
, Each '[KnownNat] '[t1, t2, t3]
, ArithOpHs
EDiv
(Unwrappabled x)
(Unwrappabled y)
(Maybe (Unwrappabled r, any))
, IsoValue r, Typeable f
, ArithOpHs Mul Natural x x
, ArithOpHs Mul Natural y y
)
=> x : y : s :-> Maybe r : s
fixedDivHelper :: forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat)
(base :: Nat -> LorentzFixedBaseKind) any (s :: [*])
(f :: LorentzFixedBaseKind -> *) x y r.
(x ~ f (base t1), y ~ f (base t2), r ~ f (base t3),
LorentzFixedBase base, Each '[Unwrappable] '[x, y, r],
Each '[KnownNat] '[t1, t2, t3],
ArithOpHs
EDiv
(Unwrappabled x)
(Unwrappabled y)
(Maybe (Unwrappabled r, any)),
IsoValue r, Typeable f, ArithOpHs Mul Nat x x,
ArithOpHs Mul Nat y y) =>
(x : y : s) :-> (Maybe r : s)
fixedDivHelper =
(x : y : s) :-> (x : y : s)
forall {s :: [*]}. (x : y : s) :-> (x : y : s)
adjust ((x : y : s) :-> (x : y : s))
-> ((x : y : s) :-> (x : Unwrappabled (f (base t2)) : s))
-> (x : y : s) :-> (x : Unwrappabled (f (base t2)) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((y : s) :-> (Unwrappabled (f (base t2)) : s))
-> (x : y : s) :-> (x : Unwrappabled (f (base t2)) : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (y : s) :-> (Unwrappabled y : s)
(y : s) :-> (Unwrappabled (f (base t2)) : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((x : y : s) :-> (x : Unwrappabled (f (base t2)) : s))
-> ((x : Unwrappabled (f (base t2)) : s)
:-> (Unwrappabled (f (base t1)) : Unwrappabled (f (base t2)) : s))
-> (x : y : s)
:-> (Unwrappabled (f (base t1)) : Unwrappabled (f (base t2)) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(x : Unwrappabled (f (base t2)) : s)
:-> (Unwrappabled x : Unwrappabled (f (base t2)) : s)
(x : Unwrappabled (f (base t2)) : s)
:-> (Unwrappabled (f (base t1)) : Unwrappabled (f (base t2)) : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((x : y : s)
:-> (Unwrappabled (f (base t1)) : Unwrappabled (f (base t2)) : s))
-> ((Unwrappabled (f (base t1)) : Unwrappabled (f (base t2)) : s)
:-> (Maybe (Unwrappabled (f (base t3)), any) : s))
-> (x : y : s) :-> (Maybe (Unwrappabled (f (base t3)), any) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(Unwrappabled (f (base t1)) : Unwrappabled (f (base t2)) : s)
:-> (Maybe (Unwrappabled (f (base t3)), any) : s)
forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv ((x : y : s) :-> (Maybe (Unwrappabled (f (base t3)), any) : s))
-> ((Maybe (Unwrappabled (f (base t3)), any) : s)
:-> (Maybe r : s))
-> (x : y : s) :-> (Maybe r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
forall c b (s :: [*]).
(MapOpHs c, IsoMapOpRes c b, KnownValue b, HasCallStack) =>
((MapOpInpHs c : s) :-> (b : s))
-> (c : s) :-> (MapOpResHs c b : s)
Lorentz.Instr.map @(Maybe (Unwrappabled r, any)) (((Unwrappabled (f (base t3)), any) : s)
:-> (Unwrappabled (f (base t3)) : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : s)
car (((Unwrappabled (f (base t3)), any) : s)
:-> (Unwrappabled (f (base t3)) : s))
-> ((Unwrappabled (f (base t3)) : s) :-> (f (base t3) : s))
-> ((Unwrappabled (f (base t3)), any) : s) :-> (f (base t3) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Unwrappabled (f (base t3)) : s) :-> (f (base t3) : s)
forall a (s :: [*]).
Unwrappable a =>
(Unwrappabled a : s) :-> (a : s)
unsafeCoerceWrap)
where
powDifference :: Integer
powDifference :: Integer
powDifference = Proxy t2 -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @t2) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Proxy t3 -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @t3) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Proxy t1 -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @t1)
multiplier :: Natural
multiplier :: Nat
multiplier = forall (a :: Nat -> LorentzFixedBaseKind) b.
(LorentzFixedBase a, Num b) =>
b
getBase @base Nat -> Integer -> Nat
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer -> Integer
forall a. Num a => a -> a
P.abs Integer
powDifference
adjust :: (x : y : s) :-> (x : y : s)
adjust = case Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
P.compare Integer
powDifference Integer
0 of
Ordering
P.EQ -> (x : y : s) :-> (x : y : s)
forall (s :: [*]). s :-> s
nop
Ordering
P.GT -> Nat -> (x : y : s) :-> (Nat : x : y : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Nat
multiplier ((x : y : s) :-> (Nat : x : y : s))
-> ((Nat : x : y : s) :-> (x : y : s))
-> (x : y : s) :-> (x : y : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Nat : x : y : s) :-> (x : y : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
Ordering
P.LT -> ((y : s) :-> (y : s)) -> (x : y : s) :-> (x : y : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (((y : s) :-> (y : s)) -> (x : y : s) :-> (x : y : s))
-> ((y : s) :-> (y : s)) -> (x : y : s) :-> (x : y : s)
forall a b. (a -> b) -> a -> b
$ Nat -> (y : s) :-> (Nat : y : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Nat
multiplier ((y : s) :-> (Nat : y : s))
-> ((Nat : y : s) :-> (y : s)) -> (y : s) :-> (y : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Nat : y : s) :-> (y : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
edivHelper
:: forall a base x y r1 r2 s f.
( KnownNat a
, ArithOpHs Mul Natural y y
, ArithOpHs EDiv (Unwrappabled x) y (Maybe (r1, Unwrappabled r2))
, Unwrappable x, Unwrappable r2
, LorentzFixedBase base
, x ~ f (base a)
)
=> (x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper :: forall (a :: Nat) (base :: Nat -> LorentzFixedBaseKind) x y r1 r2
(s :: [*]) (f :: LorentzFixedBaseKind -> *).
(KnownNat a, ArithOpHs Mul Nat y y,
ArithOpHs EDiv (Unwrappabled x) y (Maybe (r1, Unwrappabled r2)),
Unwrappable x, Unwrappable r2, LorentzFixedBase base,
x ~ f (base a)) =>
(x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper =
((y : s) :-> (y : s)) -> (x : y : s) :-> (x : y : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (forall (base :: Nat -> LorentzFixedBaseKind) (exp :: Nat) b
(s :: [*]).
(KnownNat exp, ArithOpHs Mul Nat b b, LorentzFixedBase base) =>
(b : s) :-> (b : s)
rebase @base @a) ((x : y : s) :-> (x : y : s))
-> ((x : y : s) :-> (Unwrappabled (f (base a)) : y : s))
-> (x : y : s) :-> (Unwrappabled (f (base a)) : y : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(x : y : s) :-> (Unwrappabled x : y : s)
(x : y : s) :-> (Unwrappabled (f (base a)) : y : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((x : y : s) :-> (Unwrappabled (f (base a)) : y : s))
-> ((Unwrappabled (f (base a)) : y : s)
:-> (Maybe (r1, Unwrappabled r2) : s))
-> (x : y : s) :-> (Maybe (r1, Unwrappabled r2) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(Unwrappabled (f (base a)) : y : s)
:-> (Maybe (r1, Unwrappabled r2) : s)
forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv ((x : y : s) :-> (Maybe (r1, Unwrappabled r2) : s))
-> ((Maybe (r1, Unwrappabled r2) : s) :-> (Maybe (r1, r2) : s))
-> (x : y : s) :-> (Maybe (r1, r2) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_ @(Maybe (r1, Unwrappabled r2)) @(Maybe (r1, r2))
rebase
:: forall base (exp :: Lit.Nat) b s.
(KnownNat exp, ArithOpHs Mul Natural b b, LorentzFixedBase base)
=> b : s :-> b : s
rebase :: forall (base :: Nat -> LorentzFixedBaseKind) (exp :: Nat) b
(s :: [*]).
(KnownNat exp, ArithOpHs Mul Nat b b, LorentzFixedBase base) =>
(b : s) :-> (b : s)
rebase = case forall (a :: Nat -> LorentzFixedBaseKind) b.
(LorentzFixedBase a, Num b) =>
b
getBase @base Nat -> Integer -> Nat
forall a b. (Num a, Integral b) => a -> b -> a
^ Proxy exp -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @exp) :: Natural of
Nat
1 -> (b : s) :-> (b : s)
forall (s :: [*]). s :-> s
nop
Nat
pow -> Nat -> (b : s) :-> (Nat : b : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Nat
pow ((b : s) :-> (Nat : b : s))
-> ((Nat : b : s) :-> (b : s)) -> (b : s) :-> (b : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Nat : b : s) :-> (b : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul