-- 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
  , LorentzFixedCast (..)
  , Fixed (..)
  , NFixed (..)

  -- * Support types and functions
  , DecBase (..)
  , BinBase (..)
  , resolution_

  ) where

import Data.Fixed (Fixed(..), HasResolution(..))
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) #-}

-- | Datatypes, representing base of the fixed-point values
data DecBase p where
  DecBase :: KnownNat p => DecBase p
data BinBase p where
  BinBase :: KnownNat p => BinBase p

instance KnownNat p => HasResolution (DecBase p) where
  resolution :: forall (p :: * -> *). p (DecBase p) -> Integer
resolution p (DecBase p)
_ = Integer
10 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 {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @p))

instance KnownNat p => HasResolution (BinBase p) where
  resolution :: forall (p :: * -> *). p (BinBase p) -> Integer
resolution p (BinBase p)
_ = Integer
2 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 {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @p))

-- | Special function to get resolution without argument
resolution_ :: forall a. HasResolution a => Natural
resolution_ :: forall {k} (a :: k). HasResolution a => Natural
resolution_ =
  let r :: Integer
r = Proxy a -> Integer
forall k (a :: k) (p :: k -> *). HasResolution a => 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 -> Natural
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
/= :: 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
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
min :: NFixed p -> NFixed p -> NFixed p
$cmin :: forall k (p :: k). NFixed p -> NFixed p -> NFixed p
max :: NFixed p -> NFixed p -> NFixed p
$cmax :: forall k (p :: k). NFixed p -> NFixed p -> NFixed p
>= :: 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
$c< :: forall k (p :: k). NFixed p -> NFixed p -> Bool
compare :: NFixed p -> NFixed p -> Ordering
$ccompare :: forall k (p :: k). NFixed p -> NFixed p -> Ordering
Ord)

convertNFixedToFixed :: NFixed a -> Fixed a
convertNFixedToFixed :: forall {k} (a :: k). NFixed a -> Fixed a
convertNFixedToFixed (MkNFixed Natural
a) = Integer -> Fixed a
forall k (a :: k). Integer -> Fixed a
MkFixed (forall a b. (HasCallStack, Integral a, Integral b) => a -> b
Unsafe.fromIntegral @Natural @Integer Natural
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 Natural
a) + :: NFixed a -> NFixed a -> NFixed a
+ (MkNFixed Natural
b) = Natural -> NFixed a
forall {k} (p :: k). Natural -> NFixed p
MkNFixed (Natural
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
b)
  (MkNFixed Natural
a) - :: NFixed a -> NFixed a -> NFixed a
- (MkNFixed Natural
b) = Natural -> NFixed a
forall {k} (p :: k). Natural -> NFixed p
MkNFixed (Natural
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
b)
  fa :: NFixed a
fa@(MkNFixed Natural
a) * :: NFixed a -> NFixed a -> NFixed a
* (MkNFixed Natural
b) = Natural -> NFixed a
forall {k} (p :: k). Natural -> NFixed p
MkNFixed (Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
P.div (Natural
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
b) (Integer -> Natural
forall a. (HasCallStack, Integral a) => Integer -> a
fromInteger (NFixed a -> Integer
forall k (a :: k) (p :: k -> *). HasResolution a => p a -> Integer
resolution NFixed a
fa)))
  negate :: NFixed a -> NFixed a
negate (MkNFixed Natural
a) = Natural -> NFixed a
forall {k} (p :: k). Natural -> NFixed p
MkNFixed (Natural -> Natural
forall a. Num a => a -> a
negate Natural
a)
  abs :: NFixed a -> NFixed a
abs = NFixed a -> NFixed a
forall a. a -> a
id
  signum :: NFixed a -> NFixed a
signum (MkNFixed Natural
a) = Natural -> NFixed a
forall {k} (p :: k). Natural -> NFixed p
MkNFixed (Natural -> Natural
forall a. Num a => a -> a
signum Natural
a)
  fromInteger :: Integer -> NFixed a
fromInteger Integer
i = (Natural -> NFixed a) -> NFixed a
forall {k} (a :: k) (f :: k -> *).
HasResolution a =>
(Natural -> f a) -> f a
withResolution (\Natural
res -> Natural -> NFixed a
forall {k} (p :: k). Natural -> NFixed p
MkNFixed ((Integer -> Natural
forall a. (HasCallStack, Integral a) => Integer -> a
fromInteger Integer
i) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
res))

instance (HasResolution a) => Fractional (NFixed a) where
  fa :: NFixed a
fa@(MkNFixed Natural
a) / :: NFixed a -> NFixed a -> NFixed a
/ (MkNFixed Natural
b) = Natural -> NFixed a
forall {k} (p :: k). Natural -> NFixed p
MkNFixed (Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
P.div (Natural
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* (Integer -> Natural
forall a. (HasCallStack, Integral a) => Integer -> a
fromInteger (NFixed a -> Integer
forall k (a :: k) (p :: k -> *). HasResolution a => p a -> Integer
resolution NFixed a
fa))) Natural
b)
  recip :: NFixed a -> NFixed a
recip fa :: NFixed a
fa@(MkNFixed Natural
a) = Natural -> NFixed a
forall {k} (p :: k). Natural -> NFixed p
MkNFixed (Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
P.div (Natural
res Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
res) Natural
a) where
      res :: Natural
res = Integer -> Natural
forall a. (HasCallStack, Integral a) => Integer -> a
fromInteger (Integer -> Natural) -> Integer -> Natural
forall a b. (a -> b) -> a -> b
$ NFixed a -> Integer
forall k (a :: k) (p :: k -> *). HasResolution a => p a -> Integer
resolution NFixed a
fa
  fromRational :: Rational -> NFixed a
fromRational Rational
r = (Natural -> NFixed a) -> NFixed a
forall {k} (a :: k) (f :: k -> *).
HasResolution a =>
(Natural -> f a) -> f a
withResolution (\Natural
res -> Natural -> NFixed a
forall {k} (p :: k). Natural -> NFixed p
MkNFixed (Rational -> Natural
forall a b. (RealFrac a, Integral b) => a -> b
floor (Rational
r Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* (Natural -> Rational
forall a. Real a => a -> Rational
toRational Natural
res))))

instance IsoValue (NFixed p) where
  type ToT (NFixed p) = 'TNat
  toVal :: NFixed p -> Value (ToT (NFixed p))
toVal (MkNFixed Natural
x) = Natural -> Value' Instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat Natural
x
  fromVal :: Value (ToT (NFixed p)) -> NFixed p
fromVal (VNat Natural
x) = Natural -> NFixed p
forall {k} (p :: k). Natural -> NFixed p
MkNFixed Natural
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 =>
(Natural -> f a) -> f a
withResolution Natural -> f a
foo = Natural -> f a
foo (Natural -> f a) -> (Proxy a -> Natural) -> Proxy a -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Natural
forall a. (HasCallStack, Integral a) => Integer -> a
fromInteger (Integer -> Natural) -> (Proxy a -> Integer) -> Proxy a -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy a -> Integer
forall k (a :: k) (p :: k -> *). HasResolution a => 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' Insances
------------------------------------------------------------------------------

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 ~ (a Lit.+ b)) => ArithOpHs Mul (Fixed (DecBase a)) (Fixed (DecBase b)) (Fixed (DecBase r))
instance (r ~ (a Lit.+ b)) => ArithOpHs Mul (Fixed (BinBase a)) (Fixed (BinBase b)) (Fixed (BinBase 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 ~ (a Lit.+ b)) => ArithOpHs Mul (NFixed (DecBase a)) (NFixed (DecBase b)) (NFixed (DecBase r))
instance (r ~ (a Lit.+ b)) => ArithOpHs Mul (NFixed (BinBase a)) (NFixed (BinBase b)) (NFixed (BinBase 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 ~ (a Lit.+ b)) => ArithOpHs Mul (NFixed (DecBase a)) (Fixed (DecBase b)) (Fixed (DecBase r))
instance (r ~ (a Lit.+ b)) => ArithOpHs Mul (Fixed (DecBase a)) (NFixed (DecBase b)) (Fixed (DecBase r))
instance (r ~ (a Lit.+ b)) => ArithOpHs Mul (NFixed (BinBase a)) (Fixed (BinBase b)) (Fixed (BinBase r))
instance (r ~ (a Lit.+ b)) => ArithOpHs Mul (Fixed (BinBase a)) (NFixed (BinBase b)) (Fixed (BinBase r))

instance (r ~ (NFixed (BinBase b))) => ArithOpHs Lsl (NFixed (BinBase a)) Natural r
instance (r ~ (NFixed (BinBase b))) => 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) => LorentzRounding (Fixed (DecBase a)) (Fixed (DecBase b)) where
  round_ :: forall (s :: [*]).
(Fixed (DecBase a) : s) :-> (Fixed (DecBase b) : s)
round_ = forall (a :: Nat) (b :: Nat) r1 r2 (s :: [*]).
(KnownNat a, KnownNat b, ForbidTicket (ToT (Unwrappabled r1)),
 MichelsonCoercible r1 r2, Typeable (Unwrappabled r2),
 IsoValue (Unwrappabled r2), SingI (ToT (Unwrappabled r1)),
 Unwrappable r2, Unwrappable r1,
 ArithOpHs Add Integer (Unwrappabled r2) (Unwrappabled r2),
 ArithOpHs Add Natural (Unwrappabled r2) (Unwrappabled r2),
 ArithOpHs And (Unwrappabled r2) Natural Natural,
 ArithOpHs
   EDiv (Unwrappabled r1) Integer (Maybe (Unwrappabled r2, Natural)),
 ArithOpHs Mul Integer r1 r1) =>
RoundingPattern -> Natural -> (r1 : s) :-> (r2 : s)
roundingHelper @a @b RoundingPattern
Round Natural
10
  ceil_ :: forall (s :: [*]).
(Fixed (DecBase a) : s) :-> (Fixed (DecBase b) : s)
ceil_ = forall (a :: Nat) (b :: Nat) r1 r2 (s :: [*]).
(KnownNat a, KnownNat b, ForbidTicket (ToT (Unwrappabled r1)),
 MichelsonCoercible r1 r2, Typeable (Unwrappabled r2),
 IsoValue (Unwrappabled r2), SingI (ToT (Unwrappabled r1)),
 Unwrappable r2, Unwrappable r1,
 ArithOpHs Add Integer (Unwrappabled r2) (Unwrappabled r2),
 ArithOpHs Add Natural (Unwrappabled r2) (Unwrappabled r2),
 ArithOpHs And (Unwrappabled r2) Natural Natural,
 ArithOpHs
   EDiv (Unwrappabled r1) Integer (Maybe (Unwrappabled r2, Natural)),
 ArithOpHs Mul Integer r1 r1) =>
RoundingPattern -> Natural -> (r1 : s) :-> (r2 : s)
roundingHelper @a @b RoundingPattern
Ceil Natural
10
  floor_ :: forall (s :: [*]).
(Fixed (DecBase a) : s) :-> (Fixed (DecBase b) : s)
floor_ = forall (a :: Nat) (b :: Nat) r1 r2 (s :: [*]).
(KnownNat a, KnownNat b, ForbidTicket (ToT (Unwrappabled r1)),
 MichelsonCoercible r1 r2, Typeable (Unwrappabled r2),
 IsoValue (Unwrappabled r2), SingI (ToT (Unwrappabled r1)),
 Unwrappable r2, Unwrappable r1,
 ArithOpHs Add Integer (Unwrappabled r2) (Unwrappabled r2),
 ArithOpHs Add Natural (Unwrappabled r2) (Unwrappabled r2),
 ArithOpHs And (Unwrappabled r2) Natural Natural,
 ArithOpHs
   EDiv (Unwrappabled r1) Integer (Maybe (Unwrappabled r2, Natural)),
 ArithOpHs Mul Integer r1 r1) =>
RoundingPattern -> Natural -> (r1 : s) :-> (r2 : s)
roundingHelper @a @b RoundingPattern
Floor Natural
10

instance (KnownNat a, KnownNat b) => LorentzRounding (Fixed (BinBase a)) (Fixed (BinBase b)) where
  round_ :: forall (s :: [*]).
(Fixed (BinBase a) : s) :-> (Fixed (BinBase b) : s)
round_ = forall (a :: Nat) (b :: Nat) r1 r2 (s :: [*]).
(KnownNat a, KnownNat b, ForbidTicket (ToT (Unwrappabled r1)),
 MichelsonCoercible r1 r2, Typeable (Unwrappabled r2),
 IsoValue (Unwrappabled r2), SingI (ToT (Unwrappabled r1)),
 Unwrappable r2, Unwrappable r1,
 ArithOpHs Add Integer (Unwrappabled r2) (Unwrappabled r2),
 ArithOpHs Add Natural (Unwrappabled r2) (Unwrappabled r2),
 ArithOpHs And (Unwrappabled r2) Natural Natural,
 ArithOpHs
   EDiv (Unwrappabled r1) Integer (Maybe (Unwrappabled r2, Natural)),
 ArithOpHs Mul Integer r1 r1) =>
RoundingPattern -> Natural -> (r1 : s) :-> (r2 : s)
roundingHelper @a @b RoundingPattern
Round Natural
2
  ceil_ :: forall (s :: [*]).
(Fixed (BinBase a) : s) :-> (Fixed (BinBase b) : s)
ceil_ = forall (a :: Nat) (b :: Nat) r1 r2 (s :: [*]).
(KnownNat a, KnownNat b, ForbidTicket (ToT (Unwrappabled r1)),
 MichelsonCoercible r1 r2, Typeable (Unwrappabled r2),
 IsoValue (Unwrappabled r2), SingI (ToT (Unwrappabled r1)),
 Unwrappable r2, Unwrappable r1,
 ArithOpHs Add Integer (Unwrappabled r2) (Unwrappabled r2),
 ArithOpHs Add Natural (Unwrappabled r2) (Unwrappabled r2),
 ArithOpHs And (Unwrappabled r2) Natural Natural,
 ArithOpHs
   EDiv (Unwrappabled r1) Integer (Maybe (Unwrappabled r2, Natural)),
 ArithOpHs Mul Integer r1 r1) =>
RoundingPattern -> Natural -> (r1 : s) :-> (r2 : s)
roundingHelper @a @b RoundingPattern
Ceil Natural
2
  floor_ :: forall (s :: [*]).
(Fixed (BinBase a) : s) :-> (Fixed (BinBase b) : s)
floor_ = forall (a :: Nat) (b :: Nat) r1 r2 (s :: [*]).
(KnownNat a, KnownNat b, ForbidTicket (ToT (Unwrappabled r1)),
 MichelsonCoercible r1 r2, Typeable (Unwrappabled r2),
 IsoValue (Unwrappabled r2), SingI (ToT (Unwrappabled r1)),
 Unwrappable r2, Unwrappable r1,
 ArithOpHs Add Integer (Unwrappabled r2) (Unwrappabled r2),
 ArithOpHs Add Natural (Unwrappabled r2) (Unwrappabled r2),
 ArithOpHs And (Unwrappabled r2) Natural Natural,
 ArithOpHs
   EDiv (Unwrappabled r1) Integer (Maybe (Unwrappabled r2, Natural)),
 ArithOpHs Mul Integer r1 r1) =>
RoundingPattern -> Natural -> (r1 : s) :-> (r2 : s)
roundingHelper @a @b RoundingPattern
Floor Natural
2

instance (LorentzRounding (Fixed (DecBase a)) (Fixed (DecBase b)))
  => LorentzRounding (NFixed (DecBase a)) (NFixed (DecBase b)) where
  round_ :: forall (s :: [*]).
(NFixed (DecBase a) : s) :-> (NFixed (DecBase b) : s)
round_ = (NFixed (DecBase a) : s) :-> (Fixed (DecBase a) : s)
forall {k} (p :: k) (s :: [*]). (NFixed p : s) :-> (Fixed p : s)
castNFixedToFixed ((NFixed (DecBase a) : s) :-> (Fixed (DecBase a) : s))
-> ((Fixed (DecBase a) : s) :-> (Fixed (DecBase b) : s))
-> (NFixed (DecBase a) : s) :-> (Fixed (DecBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (DecBase a) : s) :-> (Fixed (DecBase b) : s)
forall a b (s :: [*]). LorentzRounding a b => (a : s) :-> (b : s)
round_ ((NFixed (DecBase a) : s) :-> (Fixed (DecBase b) : s))
-> ((Fixed (DecBase b) : s) :-> (NFixed (DecBase b) : s))
-> (NFixed (DecBase a) : s) :-> (NFixed (DecBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (DecBase b) : s) :-> (NFixed (DecBase b) : s)
forall {k} (p :: k) (s :: [*]). (Fixed p : s) :-> (NFixed p : s)
unsafeCastFixedToNFixed
  ceil_ :: forall (s :: [*]).
(NFixed (DecBase a) : s) :-> (NFixed (DecBase b) : s)
ceil_ = (NFixed (DecBase a) : s) :-> (Fixed (DecBase a) : s)
forall {k} (p :: k) (s :: [*]). (NFixed p : s) :-> (Fixed p : s)
castNFixedToFixed ((NFixed (DecBase a) : s) :-> (Fixed (DecBase a) : s))
-> ((Fixed (DecBase a) : s) :-> (Fixed (DecBase b) : s))
-> (NFixed (DecBase a) : s) :-> (Fixed (DecBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (DecBase a) : s) :-> (Fixed (DecBase b) : s)
forall a b (s :: [*]). LorentzRounding a b => (a : s) :-> (b : s)
ceil_ ((NFixed (DecBase a) : s) :-> (Fixed (DecBase b) : s))
-> ((Fixed (DecBase b) : s) :-> (NFixed (DecBase b) : s))
-> (NFixed (DecBase a) : s) :-> (NFixed (DecBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (DecBase b) : s) :-> (NFixed (DecBase b) : s)
forall {k} (p :: k) (s :: [*]). (Fixed p : s) :-> (NFixed p : s)
unsafeCastFixedToNFixed
  floor_ :: forall (s :: [*]).
(NFixed (DecBase a) : s) :-> (NFixed (DecBase b) : s)
floor_ = (NFixed (DecBase a) : s) :-> (Fixed (DecBase a) : s)
forall {k} (p :: k) (s :: [*]). (NFixed p : s) :-> (Fixed p : s)
castNFixedToFixed ((NFixed (DecBase a) : s) :-> (Fixed (DecBase a) : s))
-> ((Fixed (DecBase a) : s) :-> (Fixed (DecBase b) : s))
-> (NFixed (DecBase a) : s) :-> (Fixed (DecBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (DecBase a) : s) :-> (Fixed (DecBase b) : s)
forall a b (s :: [*]). LorentzRounding a b => (a : s) :-> (b : s)
floor_ ((NFixed (DecBase a) : s) :-> (Fixed (DecBase b) : s))
-> ((Fixed (DecBase b) : s) :-> (NFixed (DecBase b) : s))
-> (NFixed (DecBase a) : s) :-> (NFixed (DecBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (DecBase b) : s) :-> (NFixed (DecBase b) : s)
forall {k} (p :: k) (s :: [*]). (Fixed p : s) :-> (NFixed p : s)
unsafeCastFixedToNFixed

instance (KnownNat a, KnownNat b)
  => LorentzRounding (NFixed (BinBase a)) (NFixed (BinBase b)) where
  round_ :: forall (s :: [*]).
(NFixed (BinBase a) : s) :-> (NFixed (BinBase b) : s)
round_ = (NFixed (BinBase a) : s) :-> (Fixed (BinBase a) : s)
forall {k} (p :: k) (s :: [*]). (NFixed p : s) :-> (Fixed p : s)
castNFixedToFixed ((NFixed (BinBase a) : s) :-> (Fixed (BinBase a) : s))
-> ((Fixed (BinBase a) : s) :-> (Fixed (BinBase b) : s))
-> (NFixed (BinBase a) : s) :-> (Fixed (BinBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (BinBase a) : s) :-> (Fixed (BinBase b) : s)
forall a b (s :: [*]). LorentzRounding a b => (a : s) :-> (b : s)
round_ ((NFixed (BinBase a) : s) :-> (Fixed (BinBase b) : s))
-> ((Fixed (BinBase b) : s) :-> (NFixed (BinBase b) : s))
-> (NFixed (BinBase a) : s) :-> (NFixed (BinBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (BinBase b) : s) :-> (NFixed (BinBase b) : s)
forall {k} (p :: k) (s :: [*]). (Fixed p : s) :-> (NFixed p : s)
unsafeCastFixedToNFixed
  ceil_ :: forall (s :: [*]).
(NFixed (BinBase a) : s) :-> (NFixed (BinBase b) : s)
ceil_ = (NFixed (BinBase a) : s) :-> (Fixed (BinBase a) : s)
forall {k} (p :: k) (s :: [*]). (NFixed p : s) :-> (Fixed p : s)
castNFixedToFixed ((NFixed (BinBase a) : s) :-> (Fixed (BinBase a) : s))
-> ((Fixed (BinBase a) : s) :-> (Fixed (BinBase b) : s))
-> (NFixed (BinBase a) : s) :-> (Fixed (BinBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (BinBase a) : s) :-> (Fixed (BinBase b) : s)
forall a b (s :: [*]). LorentzRounding a b => (a : s) :-> (b : s)
ceil_ ((NFixed (BinBase a) : s) :-> (Fixed (BinBase b) : s))
-> ((Fixed (BinBase b) : s) :-> (NFixed (BinBase b) : s))
-> (NFixed (BinBase a) : s) :-> (NFixed (BinBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (BinBase b) : s) :-> (NFixed (BinBase b) : s)
forall {k} (p :: k) (s :: [*]). (Fixed p : s) :-> (NFixed p : s)
unsafeCastFixedToNFixed
  floor_ :: forall (s :: [*]).
(NFixed (BinBase a) : s) :-> (NFixed (BinBase b) : s)
floor_ = (NFixed (BinBase a) : s) :-> (Fixed (BinBase a) : s)
forall {k} (p :: k) (s :: [*]). (NFixed p : s) :-> (Fixed p : s)
castNFixedToFixed ((NFixed (BinBase a) : s) :-> (Fixed (BinBase a) : s))
-> ((Fixed (BinBase a) : s) :-> (Fixed (BinBase b) : s))
-> (NFixed (BinBase a) : s) :-> (Fixed (BinBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (BinBase a) : s) :-> (Fixed (BinBase b) : s)
forall a b (s :: [*]). LorentzRounding a b => (a : s) :-> (b : s)
floor_ ((NFixed (BinBase a) : s) :-> (Fixed (BinBase b) : s))
-> ((Fixed (BinBase b) : s) :-> (NFixed (BinBase b) : s))
-> (NFixed (BinBase a) : s) :-> (NFixed (BinBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (BinBase b) : s) :-> (NFixed (BinBase b) : s)
forall {k} (p :: k) (s :: [*]). (Fixed p : s) :-> (NFixed p : s)
unsafeCastFixedToNFixed

-- | Class that allows casting @Fixed@ values to Integer in vice versa
class LorentzFixedCast a where
  fromFixed :: a : s :-> Integer : s
  toFixed :: Integer : s :-> a : s

instance (KnownNat a) => LorentzFixedCast (Fixed (DecBase a)) where
  fromFixed :: (Fixed (DecBase a)) : s :-> Integer : s
  fromFixed :: forall (s :: [*]). (Fixed (DecBase a) : s) :-> (Integer : s)
fromFixed = (forall a b (s :: [*]). LorentzRounding a b => (a : s) :-> (b : s)
round_ @(Fixed (DecBase a)) @(Fixed (DecBase 0))) ((Fixed (DecBase a) : s) :-> (Fixed (DecBase 0) : s))
-> ((Fixed (DecBase 0) : s) :-> (Integer : s))
-> (Fixed (DecBase a) : s) :-> (Integer : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (DecBase 0) : s) :-> (Integer : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_
  toFixed :: forall (s :: [*]). (Integer : s) :-> (Fixed (DecBase a) : s)
toFixed = let Integer
pow :: Integer = Integer
10 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Proxy a -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @a) in Integer -> (Integer : s) :-> (Integer : Integer : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Integer
pow ((Integer : s) :-> (Integer : Integer : s))
-> ((Integer : Integer : s) :-> (Integer : s))
-> (Integer : s) :-> (Integer : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Integer : s) :-> (Integer : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul ((Integer : s) :-> (Integer : s))
-> ((Integer : s) :-> (Fixed (DecBase a) : s))
-> (Integer : s) :-> (Fixed (DecBase a) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_ @Integer @(Fixed (DecBase a))

instance (KnownNat a) => LorentzFixedCast (Fixed (BinBase a)) where
  fromFixed :: (Fixed (BinBase a)) : s :-> Integer : s
  fromFixed :: forall (s :: [*]). (Fixed (BinBase a) : s) :-> (Integer : s)
fromFixed = (forall a b (s :: [*]). LorentzRounding a b => (a : s) :-> (b : s)
round_ @(Fixed (BinBase a)) @(Fixed (BinBase 0))) ((Fixed (BinBase a) : s) :-> (Fixed (BinBase 0) : s))
-> ((Fixed (BinBase 0) : s) :-> (Integer : s))
-> (Fixed (BinBase a) : s) :-> (Integer : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (BinBase 0) : s) :-> (Integer : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_
  toFixed :: forall (s :: [*]). (Integer : s) :-> (Fixed (BinBase a) : s)
toFixed = let Integer
pow :: Integer = Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Proxy a -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @a) in Integer -> (Integer : s) :-> (Integer : Integer : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Integer
pow ((Integer : s) :-> (Integer : Integer : s))
-> ((Integer : Integer : s) :-> (Integer : s))
-> (Integer : s) :-> (Integer : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Integer : s) :-> (Integer : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul ((Integer : s) :-> (Integer : s))
-> ((Integer : s) :-> (Fixed (BinBase a) : s))
-> (Integer : s) :-> (Fixed (BinBase a) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_ @Integer @(Fixed (BinBase a))

instance (LorentzFixedCast (Fixed a)) => LorentzFixedCast (NFixed a) where
  fromFixed :: forall (s :: [*]). (NFixed a : s) :-> (Integer : s)
fromFixed = (NFixed a : s) :-> (Fixed a : s)
forall {k} (p :: k) (s :: [*]). (NFixed p : s) :-> (Fixed p : s)
castNFixedToFixed ((NFixed a : s) :-> (Fixed a : s))
-> ((Fixed a : s) :-> (Integer : s))
-> (NFixed a : s) :-> (Integer : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed a : s) :-> (Integer : s)
forall a (s :: [*]).
LorentzFixedCast a =>
(a : s) :-> (Integer : s)
fromFixed
  toFixed :: forall (s :: [*]). (Integer : s) :-> (NFixed a : s)
toFixed = (Integer : s) :-> (Fixed a : s)
forall a (s :: [*]).
LorentzFixedCast a =>
(Integer : s) :-> (a : s)
toFixed ((Integer : s) :-> (Fixed a : s))
-> ((Fixed a : s) :-> (Maybe (NFixed a) : s))
-> (Integer : s) :-> (Maybe (NFixed a) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed a : s) :-> (Maybe (NFixed a) : s)
forall {k} (p :: k) (s :: [*]).
(Fixed p : s) :-> (Maybe (NFixed p) : s)
castFixedToNFixed ((Integer : s) :-> (Maybe (NFixed a) : s))
-> ((Maybe (NFixed a) : s) :-> (NFixed a : s))
-> (Integer : s) :-> (NFixed a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# MText -> (Maybe (NFixed a) : s) :-> (NFixed a : s)
forall err a (s :: [*]).
IsError err =>
err -> (Maybe a : s) :-> (a : s)
assertSome [mt|casting negative value to NFixed|]

instance ( KnownNat a
         , KnownNat b
         , KnownNat r
         ) => ArithOpHs Div (Fixed (DecBase a)) (Fixed (DecBase b)) (Maybe (Fixed (DecBase r))) where
  evalArithOpHs :: forall (s :: [*]).
(Fixed (DecBase a) : Fixed (DecBase b) : s)
:-> (Maybe (Fixed (DecBase r)) : s)
evalArithOpHs = forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat) base b1 b2 a r
       (s :: [*]).
(KnownNat t1, KnownNat t2, KnownNat t3, Num base,
 NiceConstant base, Unwrappable r, Unwrappable b1, Unwrappable a,
 Unwrappabled a ~ base, ArithOpHs Mul base r r,
 ArithOpHs
   EDiv (Unwrappabled r) (Unwrappabled b1) (Maybe (base, b2)),
 IsoValue a, Typeable a) =>
base -> (r : b1 : s) :-> (Maybe a : s)
fixedDivHelper @a @b @r Integer
10

instance ( KnownNat a
         , KnownNat b
         , KnownNat r
         ) => ArithOpHs Div (Fixed (BinBase a)) (Fixed (BinBase b)) (Maybe (Fixed (BinBase r))) where
  evalArithOpHs :: forall (s :: [*]).
(Fixed (BinBase a) : Fixed (BinBase b) : s)
:-> (Maybe (Fixed (BinBase r)) : s)
evalArithOpHs = forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat) base b1 b2 a r
       (s :: [*]).
(KnownNat t1, KnownNat t2, KnownNat t3, Num base,
 NiceConstant base, Unwrappable r, Unwrappable b1, Unwrappable a,
 Unwrappabled a ~ base, ArithOpHs Mul base r r,
 ArithOpHs
   EDiv (Unwrappabled r) (Unwrappabled b1) (Maybe (base, b2)),
 IsoValue a, Typeable a) =>
base -> (r : b1 : s) :-> (Maybe a : s)
fixedDivHelper @a @b @r Integer
2

instance ( KnownNat a
         , KnownNat b
         , KnownNat r
         ) => ArithOpHs Div (NFixed (DecBase a)) (NFixed (DecBase b)) (Maybe (NFixed (DecBase r))) where
  evalArithOpHs :: forall (s :: [*]).
(NFixed (DecBase a) : NFixed (DecBase b) : s)
:-> (Maybe (NFixed (DecBase r)) : s)
evalArithOpHs = forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat) base b1 b2 a r
       (s :: [*]).
(KnownNat t1, KnownNat t2, KnownNat t3, Num base,
 NiceConstant base, Unwrappable r, Unwrappable b1, Unwrappable a,
 Unwrappabled a ~ base, ArithOpHs Mul base r r,
 ArithOpHs
   EDiv (Unwrappabled r) (Unwrappabled b1) (Maybe (base, b2)),
 IsoValue a, Typeable a) =>
base -> (r : b1 : s) :-> (Maybe a : s)
fixedDivHelper @a @b @r Natural
10

instance ( KnownNat a
         , KnownNat b
         , KnownNat r
         ) => ArithOpHs Div (NFixed (BinBase a)) (NFixed (BinBase b)) (Maybe (NFixed (BinBase r))) where
  evalArithOpHs :: forall (s :: [*]).
(NFixed (BinBase a) : NFixed (BinBase b) : s)
:-> (Maybe (NFixed (BinBase r)) : s)
evalArithOpHs = forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat) base b1 b2 a r
       (s :: [*]).
(KnownNat t1, KnownNat t2, KnownNat t3, Num base,
 NiceConstant base, Unwrappable r, Unwrappable b1, Unwrappable a,
 Unwrappabled a ~ base, ArithOpHs Mul base r r,
 ArithOpHs
   EDiv (Unwrappabled r) (Unwrappabled b1) (Maybe (base, b2)),
 IsoValue a, Typeable a) =>
base -> (r : b1 : s) :-> (Maybe a : s)
fixedDivHelper @a @b @r Natural
2


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)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((Fixed p : s) :-> (Integer : s))
-> ((Integer : s) :-> (Maybe Natural : s))
-> (Fixed p : s) :-> (Maybe Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : s) :-> (Maybe Natural : s)
forall (s :: [*]). (Integer : s) :-> (Maybe Natural : s)
isNat ((Fixed p : s) :-> (Maybe Natural : s))
-> ((Maybe Natural : s) :-> (Maybe (NFixed p) : s))
-> (Fixed p : s) :-> (Maybe (NFixed p) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Maybe Natural : 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)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((Fixed p : s) :-> (Integer : s))
-> ((Integer : s) :-> (Natural : s))
-> (Fixed p : s) :-> (Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : s) :-> (Natural : s)
forall n (s :: [*]).
UnaryArithOpHs Abs n =>
(n : s) :-> (UnaryArithResHs Abs n : s)
Lorentz.Instr.abs ((Fixed p : s) :-> (Natural : s))
-> ((Natural : s) :-> (NFixed p : s))
-> (Fixed p : s) :-> (NFixed p : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : s) :-> (NFixed p : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_

instance (r ~ Maybe (Integer, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (DecBase a)) Integer r where
  evalArithOpHs :: forall (s :: [*]). (Fixed (DecBase a) : Integer : s) :-> (r : s)
evalArithOpHs = forall (a :: Nat) base x y r1 r2 m (s :: [*]).
(KnownNat a, Num base, NiceConstant base, KnownValue r1,
 KnownValue r2, Dupable m, UnaryArithOpHs Eq' m,
 ArithOpHs Mul base y m,
 ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2)),
 Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool) =>
base -> (x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper @a @Integer Integer
10

instance (r ~ Maybe (Integer, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (DecBase a)) Natural r where
  evalArithOpHs :: forall (s :: [*]). (Fixed (DecBase a) : Natural : s) :-> (r : s)
evalArithOpHs = forall (a :: Nat) base x y r1 r2 m (s :: [*]).
(KnownNat a, Num base, NiceConstant base, KnownValue r1,
 KnownValue r2, Dupable m, UnaryArithOpHs Eq' m,
 ArithOpHs Mul base y m,
 ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2)),
 Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool) =>
base -> (x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper @a @Integer Integer
10

instance (r ~ Maybe (Integer, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (BinBase a)) Integer r where
  evalArithOpHs :: forall (s :: [*]). (Fixed (BinBase a) : Integer : s) :-> (r : s)
evalArithOpHs = forall (a :: Nat) base x y r1 r2 m (s :: [*]).
(KnownNat a, Num base, NiceConstant base, KnownValue r1,
 KnownValue r2, Dupable m, UnaryArithOpHs Eq' m,
 ArithOpHs Mul base y m,
 ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2)),
 Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool) =>
base -> (x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper @a @Natural Natural
2

instance (r ~ Maybe (Integer, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (BinBase a)) Natural r where
  evalArithOpHs :: forall (s :: [*]). (Fixed (BinBase a) : Natural : s) :-> (r : s)
evalArithOpHs = forall (a :: Nat) base x y r1 r2 m (s :: [*]).
(KnownNat a, Num base, NiceConstant base, KnownValue r1,
 KnownValue r2, Dupable m, UnaryArithOpHs Eq' m,
 ArithOpHs Mul base y m,
 ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2)),
 Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool) =>
base -> (x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper @a @Natural Natural
2

instance (r ~ Maybe (Integer, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (DecBase a)) Integer r where
  evalArithOpHs :: forall (s :: [*]). (NFixed (DecBase a) : Integer : s) :-> (r : s)
evalArithOpHs = forall (a :: Nat) base x y r1 r2 m (s :: [*]).
(KnownNat a, Num base, NiceConstant base, KnownValue r1,
 KnownValue r2, Dupable m, UnaryArithOpHs Eq' m,
 ArithOpHs Mul base y m,
 ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2)),
 Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool) =>
base -> (x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper @a @Integer Integer
10

instance (r ~ Maybe (Natural, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (DecBase a)) Natural r where
  evalArithOpHs :: forall (s :: [*]). (NFixed (DecBase a) : Natural : s) :-> (r : s)
evalArithOpHs = forall (a :: Nat) base x y r1 r2 m (s :: [*]).
(KnownNat a, Num base, NiceConstant base, KnownValue r1,
 KnownValue r2, Dupable m, UnaryArithOpHs Eq' m,
 ArithOpHs Mul base y m,
 ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2)),
 Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool) =>
base -> (x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper @a @Natural Natural
10

instance (r ~ Maybe (Integer, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (BinBase a)) Integer r where
  evalArithOpHs :: forall (s :: [*]). (NFixed (BinBase a) : Integer : s) :-> (r : s)
evalArithOpHs = forall (a :: Nat) base x y r1 r2 m (s :: [*]).
(KnownNat a, Num base, NiceConstant base, KnownValue r1,
 KnownValue r2, Dupable m, UnaryArithOpHs Eq' m,
 ArithOpHs Mul base y m,
 ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2)),
 Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool) =>
base -> (x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper @a @Natural Natural
2

instance (r ~ Maybe (Natural, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (BinBase a)) Natural r where
  evalArithOpHs :: forall (s :: [*]). (NFixed (BinBase a) : Natural : s) :-> (r : s)
evalArithOpHs = forall (a :: Nat) base x y r1 r2 m (s :: [*]).
(KnownNat a, Num base, NiceConstant base, KnownValue r1,
 KnownValue r2, Dupable m, UnaryArithOpHs Eq' m,
 ArithOpHs Mul base y m,
 ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2)),
 Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool) =>
base -> (x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper @a @Natural Natural
2

----------------------------------------------------------------------------
-- 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.
    ( KnownNat a, KnownNat b
    , ForbidTicket (ToT (Unwrappabled r1))
    , MichelsonCoercible r1 r2
    , Typeable (Unwrappabled r2)
    , IsoValue (Unwrappabled r2)
    , SingI (ToT (Unwrappabled r1))
    , Unwrappable r2
    , Unwrappable r1
    , ArithOpHs Add Integer (Unwrappabled r2) (Unwrappabled r2)
    , ArithOpHs Add Natural (Unwrappabled r2) (Unwrappabled r2)
    , ArithOpHs And (Unwrappabled r2) Natural Natural
    , ArithOpHs EDiv (Unwrappabled r1) Integer (Maybe (Unwrappabled r2, Natural))
    , ArithOpHs Mul Integer r1 r1
    )
  => RoundingPattern -> Natural -> (r1 : s :-> r2 : s)
roundingHelper :: forall (a :: Nat) (b :: Nat) r1 r2 (s :: [*]).
(KnownNat a, KnownNat b, ForbidTicket (ToT (Unwrappabled r1)),
 MichelsonCoercible r1 r2, Typeable (Unwrappabled r2),
 IsoValue (Unwrappabled r2), SingI (ToT (Unwrappabled r1)),
 Unwrappable r2, Unwrappable r1,
 ArithOpHs Add Integer (Unwrappabled r2) (Unwrappabled r2),
 ArithOpHs Add Natural (Unwrappabled r2) (Unwrappabled r2),
 ArithOpHs And (Unwrappabled r2) Natural Natural,
 ArithOpHs
   EDiv (Unwrappabled r1) Integer (Maybe (Unwrappabled r2, Natural)),
 ArithOpHs Mul Integer r1 r1) =>
RoundingPattern -> Natural -> (r1 : s) :-> (r2 : s)
roundingHelper RoundingPattern
rp Natural
base =
  let Natural
halfBase :: Natural = Natural
base Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`P.div` Natural
2
      Integer
powDifference :: Integer = (Proxy b -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. 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 {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @a))
      Integer
newPow :: Integer = Natural -> Integer
forall a b. (Integral a, Integral b, CheckIntSubType a b) => a -> b
fromIntegral (Natural -> Integer) -> Natural -> Integer
forall a b. (a -> b) -> a -> b
$ Natural
2 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
halfNewPow
      Natural
halfNewPow :: Natural = Natural
halfBase Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* (Natural
base Natural -> Integer -> Natural
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))
   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 ->
              Integer -> (r1 : s) :-> (Integer : r1 : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Integer
newPow ((r1 : s) :-> (Integer : r1 : s))
-> ((Integer : r1 : s) :-> (r1 : s)) -> (r1 : s) :-> (r1 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : 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 ->
              Integer -> (r1 : s) :-> (Integer : r1 : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Integer
newPow ((r1 : s) :-> (Integer : r1 : s))
-> ((Integer : r1 : s) :-> (r1 : Integer : s))
-> (r1 : s) :-> (r1 : Integer : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
              (Integer : r1 : s) :-> (r1 : Integer : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((r1 : s) :-> (r1 : Integer : s))
-> ((r1 : Integer : s) :-> (Unwrappabled r1 : Integer : s))
-> (r1 : s) :-> (Unwrappabled r1 : Integer : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
              (r1 : Integer : s) :-> (Unwrappabled r1 : Integer : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((r1 : s) :-> (Unwrappabled r1 : Integer : s))
-> ((Unwrappabled r1 : Integer : s)
    :-> (Maybe (Unwrappabled r2, Natural) : s))
-> (r1 : s) :-> (Maybe (Unwrappabled r2, Natural) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Unwrappabled r1 : Integer : s)
:-> (Maybe (Unwrappabled r2, Natural) : s)
forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv ((r1 : s) :-> (Maybe (Unwrappabled r2, Natural) : s))
-> ((Maybe (Unwrappabled r2, Natural) : s)
    :-> ((Unwrappabled r2, Natural) : s))
-> (r1 : s) :-> ((Unwrappabled r2, Natural) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
              Impossible "Division by zero impossible here"
-> (Maybe (Unwrappabled r2, Natural) : s)
   :-> ((Unwrappabled r2, Natural) : 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 r2, Natural) : s))
-> (((Unwrappabled r2, Natural) : s) :-> (Unwrappabled r2 : s))
-> (r1 : s) :-> (Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
              case RoundingPattern
rp of
                RoundingPattern
Round ->
                  ((Unwrappabled r2, Natural) : s)
:-> (Unwrappabled r2 : Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair (((Unwrappabled r2, Natural) : s)
 :-> (Unwrappabled r2 : Natural : s))
-> ((Unwrappabled r2 : Natural : s)
    :-> (Natural : Unwrappabled r2 : s))
-> ((Unwrappabled r2, Natural) : s)
   :-> (Natural : Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
                  (Unwrappabled r2 : Natural : s) :-> (Natural : Unwrappabled r2 : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap (((Unwrappabled r2, Natural) : s)
 :-> (Natural : Unwrappabled r2 : s))
-> ((Natural : Unwrappabled r2 : s)
    :-> (Natural : Natural : Unwrappabled r2 : s))
-> ((Unwrappabled r2, Natural) : s)
   :-> (Natural : Natural : Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
                  Natural
-> (Natural : Unwrappabled r2 : s)
   :-> (Natural : Natural : Unwrappabled r2 : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Natural
halfNewPow (((Unwrappabled r2, Natural) : s)
 :-> (Natural : Natural : Unwrappabled r2 : s))
-> ((Natural : Natural : Unwrappabled r2 : s)
    :-> (Integer : Unwrappabled r2 : s))
-> ((Unwrappabled r2, Natural) : s)
   :-> (Integer : Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
                  (Natural : Natural : Unwrappabled r2 : s)
:-> (Integer : Unwrappabled r2 : s)
forall n (s :: [*]).
NiceComparable n =>
(n : n : s) :-> (Integer : s)
compare (((Unwrappabled r2, Natural) : s)
 :-> (Integer : Unwrappabled r2 : s))
-> ((Integer : Unwrappabled r2 : s)
    :-> (Integer : Integer : Unwrappabled r2 : s))
-> ((Unwrappabled r2, Natural) : s)
   :-> (Integer : Integer : Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
                  (Integer : Unwrappabled r2 : s)
:-> (Integer : Integer : Unwrappabled r2 : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup (((Unwrappabled r2, Natural) : s)
 :-> (Integer : Integer : Unwrappabled r2 : s))
-> ((Integer : Integer : Unwrappabled r2 : s)
    :-> (Unwrappabled r2 : s))
-> ((Unwrappabled r2, Natural) : s) :-> (Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
                  ((Integer : Unwrappabled r2 : s) :-> (Unwrappabled r2 : s))
-> ((Integer : Unwrappabled r2 : s) :-> (Unwrappabled r2 : s))
-> (Integer : Integer : Unwrappabled r2 : s)
   :-> (Unwrappabled r2 : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Ge =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifGe0 (Integer : Unwrappabled r2 : s) :-> (Unwrappabled r2 : s)
forall a (s :: [*]). (a : s) :-> s
drop (
                    -- rem >= halfNewPow
                    ((Unwrappabled r2 : s) :-> (Natural : Unwrappabled r2 : s))
-> (Integer : Unwrappabled r2 : s)
   :-> (Integer : Natural : Unwrappabled r2 : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Natural
-> (Unwrappabled r2 : s) :-> (Natural : Unwrappabled r2 : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Natural
1 :: Natural)) ((Integer : Unwrappabled r2 : s)
 :-> (Integer : Natural : Unwrappabled r2 : s))
-> ((Integer : Natural : Unwrappabled r2 : s)
    :-> (Natural : Unwrappabled r2 : s))
-> (Integer : Unwrappabled r2 : s)
   :-> (Natural : Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
                    -- if rem == halfNewPow, check if quot is odd
                    ((Natural : Unwrappabled r2 : s)
 :-> (Natural : Unwrappabled r2 : s))
-> ((Natural : Unwrappabled r2 : s)
    :-> (Natural : Unwrappabled r2 : s))
-> (Integer : Natural : Unwrappabled r2 : s)
   :-> (Natural : Unwrappabled r2 : 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 ((Natural : Unwrappabled r2 : s)
 :-> (Unwrappabled r2 : Natural : Unwrappabled r2 : s))
-> ((Unwrappabled r2 : Natural : Unwrappabled r2 : s)
    :-> (Natural : Unwrappabled r2 : s))
-> (Natural : Unwrappabled r2 : s)
   :-> (Natural : Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Unwrappabled r2 : Natural : Unwrappabled r2 : s)
:-> (Natural : Unwrappabled r2 : s)
forall n m r (s :: [*]).
ArithOpHs And n m r =>
(n : m : s) :-> (r : s)
and) (Natural : Unwrappabled r2 : s) :-> (Natural : Unwrappabled r2 : s)
forall (s :: [*]). s :-> s
nop ((Integer : Unwrappabled r2 : s)
 :-> (Natural : Unwrappabled r2 : s))
-> ((Natural : Unwrappabled r2 : s) :-> (Unwrappabled r2 : s))
-> (Integer : Unwrappabled r2 : s) :-> (Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
                    -- if quot is odd or rem > halfNewPow, add 1 to quot.
                    (Natural : Unwrappabled r2 : s) :-> (Unwrappabled r2 : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
                   )
                RoundingPattern
Ceil ->
                  ((Unwrappabled r2, Natural) : s)
:-> (Unwrappabled r2 : Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair (((Unwrappabled r2, Natural) : s)
 :-> (Unwrappabled r2 : Natural : s))
-> ((Unwrappabled r2 : Natural : s)
    :-> (Natural : Unwrappabled r2 : s))
-> ((Unwrappabled r2, Natural) : s)
   :-> (Natural : Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
                  (Unwrappabled r2 : Natural : s) :-> (Natural : Unwrappabled r2 : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap (((Unwrappabled r2, Natural) : s)
 :-> (Natural : Unwrappabled r2 : s))
-> ((Natural : Unwrappabled r2 : s) :-> (Unwrappabled r2 : s))
-> ((Unwrappabled r2, Natural) : s) :-> (Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
                  ((Unwrappabled r2 : s) :-> (Unwrappabled r2 : s))
-> ((Unwrappabled r2 : s) :-> (Unwrappabled r2 : s))
-> (Natural : Unwrappabled r2 : s) :-> (Unwrappabled r2 : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Neq =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifNeq0 (Integer
-> (Unwrappabled r2 : s) :-> (Integer : Unwrappabled r2 : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Integer
1 :: Integer) ((Unwrappabled r2 : s) :-> (Integer : Unwrappabled r2 : s))
-> ((Integer : Unwrappabled r2 : s) :-> (Unwrappabled r2 : s))
-> (Unwrappabled r2 : s) :-> (Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Unwrappabled r2 : s) :-> (Unwrappabled r2 : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add) (Unwrappabled r2 : s) :-> (Unwrappabled r2 : s)
forall (s :: [*]). s :-> s
nop
                RoundingPattern
Floor -> ((Unwrappabled r2, Natural) : s) :-> (Unwrappabled r2 : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : s)
car
              # unsafeCoerceWrap

fixedDivHelper
  :: forall t1 t2 t3 base b1 b2 a r s.
     ( KnownNat t1, KnownNat t2, KnownNat t3
     , Num base, NiceConstant base
     , Unwrappable r, Unwrappable b1, Unwrappable a
     , Unwrappabled a ~ base
     , ArithOpHs Mul base r r
     , ArithOpHs EDiv (Unwrappabled r) (Unwrappabled b1) (Maybe (base, b2))
     , IsoValue a, Typeable a
     )
  => base -> (r : b1 : s) :-> (Maybe a : s)
fixedDivHelper :: forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat) base b1 b2 a r
       (s :: [*]).
(KnownNat t1, KnownNat t2, KnownNat t3, Num base,
 NiceConstant base, Unwrappable r, Unwrappable b1, Unwrappable a,
 Unwrappabled a ~ base, ArithOpHs Mul base r r,
 ArithOpHs
   EDiv (Unwrappabled r) (Unwrappabled b1) (Maybe (base, b2)),
 IsoValue a, Typeable a) =>
base -> (r : b1 : s) :-> (Maybe a : s)
fixedDivHelper base
base =
  let powA :: Integer
powA = Proxy t1 -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @t1)
      powB :: Integer
powB = Proxy t2 -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @t2)
      powR :: base
powR = base
base base -> Integer -> base
forall a b. (Num a, Integral b) => a -> b -> a
^ (Proxy t3 -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @t3) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
   in
     Integer -> (r : b1 : s) :-> (Integer : r : b1 : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Integer
powB ((r : b1 : s) :-> (Integer : r : b1 : s))
-> ((Integer : r : b1 : s) :-> (Integer : Integer : r : b1 : s))
-> (r : b1 : s) :-> (Integer : Integer : r : b1 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
     Integer
-> (Integer : r : b1 : s) :-> (Integer : Integer : r : b1 : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Integer
powA ((r : b1 : s) :-> (Integer : Integer : r : b1 : s))
-> ((Integer : Integer : r : b1 : s) :-> (r : b1 : s))
-> (r : b1 : s) :-> (r : b1 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
     ((r : b1 : s) :-> (r : b1 : s))
-> ((r : b1 : s) :-> (r : b1 : s))
-> (Integer : Integer : r : b1 : s) :-> (r : b1 : s)
forall a (s :: [*]) (s' :: [*]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a : a : s) :-> s'
ifGt (base -> (r : b1 : s) :-> (base : r : b1 : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push base
powR ((r : b1 : s) :-> (base : r : b1 : s))
-> ((base : r : b1 : s) :-> (r : b1 : s))
-> (r : b1 : s) :-> (r : b1 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (base : r : b1 : s) :-> (r : b1 : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul) (r : b1 : s) :-> (r : b1 : s)
forall (s :: [*]). s :-> s
nop ((r : b1 : s) :-> (r : b1 : s))
-> ((r : b1 : s) :-> (r : Unwrappabled b1 : s))
-> (r : b1 : s) :-> (r : Unwrappabled b1 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
     ((b1 : s) :-> (Unwrappabled b1 : s))
-> (r : b1 : s) :-> (r : Unwrappabled b1 : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (b1 : s) :-> (Unwrappabled b1 : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((r : b1 : s) :-> (r : Unwrappabled b1 : s))
-> ((r : Unwrappabled b1 : s)
    :-> (Unwrappabled r : Unwrappabled b1 : s))
-> (r : b1 : s) :-> (Unwrappabled r : Unwrappabled b1 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
     (r : Unwrappabled b1 : s)
:-> (Unwrappabled r : Unwrappabled b1 : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((r : b1 : s) :-> (Unwrappabled r : Unwrappabled b1 : s))
-> ((Unwrappabled r : Unwrappabled b1 : s)
    :-> (Maybe (base, b2) : s))
-> (r : b1 : s) :-> (Maybe (base, b2) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
     forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv @_ @_ @(Maybe (base, b2)) ((r : b1 : s) :-> (Maybe (base, b2) : s))
-> ((Maybe (base, b2) : s) :-> (Maybe a : s))
-> (r : b1 : s) :-> (Maybe a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
     (s :-> (Maybe a : s))
-> (((base, b2) : s) :-> (Maybe a : s))
-> (Maybe (base, b2) : s) :-> (Maybe a : s)
forall (s :: [*]) (s' :: [*]) a.
(s :-> s') -> ((a : s) :-> s') -> (Maybe a : s) :-> s'
ifNone (s :-> (Maybe a : s)
forall a (s :: [*]). KnownValue a => s :-> (Maybe a : s)
none) (((base, b2) : s) :-> (base : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : s)
car (((base, b2) : s) :-> (base : s))
-> ((base : s) :-> (a : s)) -> ((base, b2) : s) :-> (a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (base : s) :-> (a : s)
forall a (s :: [*]).
Unwrappable a =>
(Unwrappabled a : s) :-> (a : s)
unsafeCoerceWrap (((base, b2) : s) :-> (a : s))
-> ((a : s) :-> (Maybe a : s))
-> ((base, b2) : s) :-> (Maybe a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : s) :-> (Maybe a : s)
forall a (s :: [*]). (a : s) :-> (Maybe a : s)
some)

edivHelper
  :: forall a base x y r1 r2 m s.
     ( KnownNat a, Num base, NiceConstant base, KnownValue r1, KnownValue r2, Dupable m
     , UnaryArithOpHs Eq' m, ArithOpHs Mul base y m
     , ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2))
     , Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool
     )
  => base -> (x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper :: forall (a :: Nat) base x y r1 r2 m (s :: [*]).
(KnownNat a, Num base, NiceConstant base, KnownValue r1,
 KnownValue r2, Dupable m, UnaryArithOpHs Eq' m,
 ArithOpHs Mul base y m,
 ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2)),
 Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool) =>
base -> (x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper base
base =
  let powA :: base
powA = base
base base -> Integer -> base
forall a b. (Num a, Integral b) => a -> b -> a
^ (Proxy a -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (forall {k} (t :: k). Proxy t
forall {t :: Nat}. Proxy t
Proxy @a))
   in
     (x : y : s) :-> (y : x : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap  ((x : y : s) :-> (y : x : s))
-> ((y : x : s) :-> (base : y : x : s))
-> (x : y : s) :-> (base : y : x : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
     base -> (y : x : s) :-> (base : y : x : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push base
powA ((x : y : s) :-> (base : y : x : s))
-> ((base : y : x : s) :-> (m : x : s))
-> (x : y : s) :-> (m : x : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
     (base : y : x : s) :-> (m : x : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul ((x : y : s) :-> (m : x : s))
-> ((m : x : s) :-> (m : m : x : s))
-> (x : y : s) :-> (m : m : x : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
     (m : x : s) :-> (m : m : x : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup ((x : y : s) :-> (m : m : x : s))
-> ((m : m : x : s) :-> (Maybe (r1, r2) : s))
-> (x : y : s) :-> (Maybe (r1, r2) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
     forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Eq' =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifEq0 @m (forall (n :: Nat) (s :: [*]).
(SingIPeano n, RequireLongerOrSameLength (ToTs s) (ToPeano n),
 Drop (ToPeano n) (ToTs s) ~ ToTs (Drop (ToPeano n) s)) =>
s :-> Drop (ToPeano n) s
dropN @2 ((m : x : s) :-> s)
-> (s :-> (Maybe (r1, r2) : s))
-> (m : x : s) :-> (Maybe (r1, r2) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# s :-> (Maybe (r1, r2) : s)
forall a (s :: [*]). KnownValue a => s :-> (Maybe a : s)
none)
     (
       (m : x : s) :-> (x : m : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((m : x : s) :-> (x : m : s))
-> ((x : m : s) :-> (Unwrappabled x : m : s))
-> (m : x : s) :-> (Unwrappabled x : m : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
       (x : m : s) :-> (Unwrappabled x : m : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((m : x : s) :-> (Unwrappabled x : m : s))
-> ((Unwrappabled x : m : s) :-> (Maybe (r1, Unwrappabled r2) : s))
-> (m : x : s) :-> (Maybe (r1, Unwrappabled r2) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
       (Unwrappabled x : m : s) :-> (Maybe (r1, Unwrappabled r2) : s)
forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv ((m : x : s) :-> (Maybe (r1, Unwrappabled r2) : s))
-> ((Maybe (r1, Unwrappabled r2) : s)
    :-> ((r1, Unwrappabled r2) : s))
-> (m : x : s) :-> ((r1, Unwrappabled r2) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
       Impossible "Division by zero impossible here"
-> (Maybe (r1, Unwrappabled r2) : s)
   :-> ((r1, Unwrappabled r2) : 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") ((m : x : s) :-> ((r1, Unwrappabled r2) : s))
-> (((r1, Unwrappabled r2) : s) :-> (r1 : Unwrappabled r2 : s))
-> (m : x : s) :-> (r1 : Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
       ((r1, Unwrappabled r2) : s) :-> (r1 : Unwrappabled r2 : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair ((m : x : s) :-> (r1 : Unwrappabled r2 : s))
-> ((r1 : Unwrappabled r2 : s) :-> (r1 : r2 : s))
-> (m : x : s) :-> (r1 : r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
       ((Unwrappabled r2 : s) :-> (r2 : s))
-> (r1 : Unwrappabled r2 : s) :-> (r1 : r2 : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Unwrappabled r2 : s) :-> (r2 : s)
forall a (s :: [*]).
Unwrappable a =>
(Unwrappabled a : s) :-> (a : s)
unsafeCoerceWrap ((m : x : s) :-> (r1 : r2 : s))
-> ((r1 : r2 : s) :-> ((r1, r2) : s))
-> (m : x : s) :-> ((r1, r2) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
       (r1 : r2 : s) :-> ((r1, r2) : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair ((m : x : s) :-> ((r1, r2) : s))
-> (((r1, r2) : s) :-> (Maybe (r1, r2) : s))
-> (m : x : s) :-> (Maybe (r1, r2) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
       ((r1, r2) : s) :-> (Maybe (r1, r2) : s)
forall a (s :: [*]). (a : s) :-> (Maybe a : s)
some
     )