-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
--
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# OPTIONS_GHC -Wno-orphans #-}

module Lorentz.CustomArith.FixedArith
  ( -- * Lorentz instructions
    castNFixedToFixed
  , castFixedToNFixed
  , unsafeCastFixedToNFixed
    -- * Typeclasses
  , Fixed (..)
  , NFixed (..)

  -- * Support types and functions
  , LorentzFixedBaseKind
  , DecBase
  , BinBase
  , resolution_
  , toFixed
  , fromFixed
  , LorentzFixedBase

  -- * Internals
  , 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

-- | Open kind for fixed value bases.
type LorentzFixedBaseKind = LorentzFixedBaseKindTag -> Type

-- | Represents binary base of the Lorentz fixed-point values
data BinBase :: Lit.Nat -> LorentzFixedBaseKind

-- | Represents decimal base of the Lorentz fixed-point values
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))

-- | Special function to get resolution without argument
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

-- | Like @Fixed@ but with a @Natural@ value inside constructor
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

-- Note: This instances are copies of those in Data.Fixed for Fixed datatype
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

-- Helpers copied from Data.Fixed, because they are not exported from there
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

------------------------------------------------------------------------------
-- Arithmetic operations' Instances
------------------------------------------------------------------------------

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)

-- | Round is implemented using "banker's rounding" strategy, rounding half-way values
-- towards nearest even value
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

-- | Convert to the corresponding integral type by banker's rounding.
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_

-- | Convert from the corresponding integral type.
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

-- NFixed

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
  )

-- NB: Instances are parametrized by the result type by design since we also
-- have rational arithmetic.

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

----------------------------------------------------------------------------
-- Helpers
----------------------------------------------------------------------------

data RoundingPattern = Round | Ceil | Floor

-- Note: Round is implemented using "banker's rounding" strategy, rounding half-way values
-- towards the nearest even value.
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 (
                    -- rem >= halfNewPow
                    ((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
#
                    -- if rem == halfNewPow, check if quot is odd
                    ((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
#
                    -- if quot is odd or rem > halfNewPow, add 1 to quot.
                    (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)
    -- see Note [fixedDivHelper] below for an explanation.
    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

{-
Note [fixedDivHelper]
~~~~~~~~~~~~~~~~~~~~~

This code may look a little bit mysterious without an explanation, so here goes:

We want to compute r = x / y, where x = a β⁻ⁿ¹, y = b β⁻ⁿ², and r has to be
represented as some r = c β⁻ⁿ³. Ultimately we need to compute c. Thus:

c β⁻ⁿ³ = (a β⁻ⁿ¹) / (b β⁻ⁿ²)
c β⁻ⁿ³ = (a / b) β⁻ⁿ¹⁺ⁿ²
c = (a / b) β⁻ⁿ¹⁺ⁿ²⁺ⁿ³

Let ε = | -n₁ + n₂ + n₃ |
Let μ = βᵋ

(-n₁ + n₂ + n₃) can be either positive, negative, or zero. If it's zero, μ = 1,
and no futher action is necessary.
If it's positive, we need to multiply a by μ before division.
If it's negative, technically we could divide a by μ, but division is more
costly than multiplication, so instead we can multiply b by μ to obtain the same
result.

In the code above, β = getBase @base, μ = multiplier, and
(-n₁ + n₂ + n₃) = powDifference.

-- @lierdakil
-}

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