-- SPDX-FileCopyrightText: 2021 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE NoApplicativeDo #-}
{-# OPTIONS_GHC -Wno-unused-do-bind #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Lorentz.CustomArith.RationalArith
  ( Rational
  , NRational

  -- * Common functions
  , oppositeRational
  , gcdEuclid
  , euclidExtendedNormalization
  , reduce
  , tripleMul

    -- * Constructor functions for Rational
  , mkRational
  , (%!)

   -- * Constructor functions for NRational
  , mkNRational
  , (%%!)

    -- * Rational specific typeclasses
  , LorentzRational

    -- * Constructors
  , mkRational_
  , numerator
  , denominator
  , constructRational
  , deconstructRational
  , uncheckedPairToRational
  , unsafePairToRational
  , pairToRational
  ) where

import Prelude (Either(..), Eq, Integer, Maybe, Natural, Show, Text, show, unsafe, ($), (++), (==))
import Text.Show qualified

import Lorentz.Annotation
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.Rebound
import Morley.Michelson.Text
import Morley.Michelson.Typed
import Morley.Util.Named
import Morley.Util.Type

newtype Rational =
  UnsafeRational (Integer, Natural)
  deriving newtype (Rational -> Rational -> Bool
(Rational -> Rational -> Bool)
-> (Rational -> Rational -> Bool) -> Eq Rational
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Rational -> Rational -> Bool
$c/= :: Rational -> Rational -> Bool
== :: Rational -> Rational -> Bool
$c== :: Rational -> Rational -> Bool
Eq)

infixl 7 %!
(%!) :: Integer -> Natural -> Rational
%! :: Integer -> Natural -> Rational
(%!) Integer
x Natural
y = Either Text Rational -> Rational
forall a b. (HasCallStack, Buildable a) => Either a b -> b
unsafe (Either Text Rational -> Rational)
-> Either Text Rational -> Rational
forall a b. (a -> b) -> a -> b
$ (Integer, Natural) -> Either Text Rational
mkRational (Integer
x, Natural
y)

mkRational :: (Integer, Natural) -> Either Text Rational
mkRational :: (Integer, Natural) -> Either Text Rational
mkRational (Integer
x, Natural
y) = case Natural
y of
  Natural
0 -> Text -> Either Text Rational
forall a b. a -> Either a b
Left (Text -> Either Text Rational) -> Text -> Either Text Rational
forall a b. (a -> b) -> a -> b
$ Text
"Attempt to construct Rational with zero denominator."
  Natural
_ -> Rational -> Either Text Rational
forall a b. b -> Either a b
Right (Rational -> Either Text Rational)
-> Rational -> Either Text Rational
forall a b. (a -> b) -> a -> b
$ (Integer, Natural) -> Rational
UnsafeRational (Integer
x, Natural
y)

instance Show Rational where
  show :: Rational -> String
show (UnsafeRational (Integer
a, Natural
b)) = Integer -> String
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show Integer
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" / " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show Natural
b

instance HasAnnotation Rational where
  getAnnotation :: FollowEntrypointFlag -> Notes (ToT Rational)
getAnnotation FollowEntrypointFlag
_ = Notes (ToT Rational)
forall (t :: T). SingI t => Notes t
starNotes

instance IsoValue Rational where
  type ToT Rational = 'TPair 'TInt 'TNat
  toVal :: Rational -> Value (ToT Rational)
toVal (UnsafeRational (Integer
a, Natural
b)) = (Value' Instr 'TInt, Value' Instr 'TNat)
-> Value' Instr ('TPair 'TInt 'TNat)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Integer -> Value' Instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt Integer
a, Natural -> Value' Instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat Natural
b)
  fromVal :: Value (ToT Rational) -> Rational
fromVal (VPair (VInt Integer
a, VNat Natural
b)) = (Integer, Natural) -> Rational
UnsafeRational (Integer
a, Natural
b)

instance Unwrappable Rational where
  type Unwrappabled Rational = (Integer, Natural)

newtype NRational =
  UnsafeNRational (Natural, Natural)
  deriving newtype (NRational -> NRational -> Bool
(NRational -> NRational -> Bool)
-> (NRational -> NRational -> Bool) -> Eq NRational
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NRational -> NRational -> Bool
$c/= :: NRational -> NRational -> Bool
== :: NRational -> NRational -> Bool
$c== :: NRational -> NRational -> Bool
Eq)

mkNRational :: (Natural, Natural) -> Either Text NRational
mkNRational :: (Natural, Natural) -> Either Text NRational
mkNRational (Natural
x, Natural
y) = case Natural
y of
  Natural
0 -> Text -> Either Text NRational
forall a b. a -> Either a b
Left Text
"Attempt to construct NRational with zero denominator."
  Natural
_ -> NRational -> Either Text NRational
forall a b. b -> Either a b
Right (NRational -> Either Text NRational)
-> NRational -> Either Text NRational
forall a b. (a -> b) -> a -> b
$ (Natural, Natural) -> NRational
UnsafeNRational (Natural
x, Natural
y)

infixl 7 %%!
(%%!) :: Natural -> Natural -> NRational
%%! :: Natural -> Natural -> NRational
(%%!) Natural
x Natural
y = Either Text NRational -> NRational
forall a b. (HasCallStack, Buildable a) => Either a b -> b
unsafe (Either Text NRational -> NRational)
-> Either Text NRational -> NRational
forall a b. (a -> b) -> a -> b
$ (Natural, Natural) -> Either Text NRational
mkNRational (Natural
x, Natural
y)

instance Show NRational where
  show :: NRational -> String
show (UnsafeNRational (Natural
a, Natural
b)) = Natural -> String
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show Natural
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" / " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show Natural
b

instance HasAnnotation NRational where
  getAnnotation :: FollowEntrypointFlag -> Notes (ToT NRational)
getAnnotation FollowEntrypointFlag
_ = Notes (ToT NRational)
forall (t :: T). SingI t => Notes t
starNotes

instance IsoValue NRational where
  type ToT NRational = 'TPair 'TNat 'TNat
  toVal :: NRational -> Value (ToT NRational)
toVal (UnsafeNRational (Natural
a, Natural
b)) = (Value' Instr 'TNat, Value' Instr 'TNat)
-> Value' Instr ('TPair 'TNat 'TNat)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Natural -> Value' Instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat Natural
a, Natural -> Value' Instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat Natural
b)
  fromVal :: Value (ToT NRational) -> NRational
fromVal (VPair (VNat Natural
a, VNat Natural
b)) = (Natural, Natural) -> NRational
UnsafeNRational (Natural
a, Natural
b)

instance Unwrappable NRational where
  type Unwrappabled NRational = (Natural, Natural)

class Unwrappable r => LorentzRational r where
  numerator :: Unwrappabled r ~ (a, Natural) => r : s :-> a : s
  numerator = (r : s) :-> ((a, Natural) : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((r : s) :-> ((a, Natural) : s))
-> (((a, Natural) : s) :-> (a : s)) -> (r : s) :-> (a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, Natural) : s) :-> (a : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : s)
car

  denominator :: Unwrappabled r ~ (a, Natural) => r : s :-> Natural : s
  denominator = (r : s) :-> ((a, Natural) : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((r : s) :-> ((a, Natural) : s))
-> (((a, Natural) : s) :-> (Natural : s))
-> (r : s) :-> (Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, Natural) : s) :-> (Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (b : s)
cdr

  deconstructRational :: Unwrappabled r ~ (a, Natural) => r : s :-> a : Natural : s
  deconstructRational = (r : s) :-> ((a, Natural) : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((r : s) :-> ((a, Natural) : s))
-> (((a, Natural) : s) :-> (a : Natural : s))
-> (r : s) :-> (a : Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, Natural) : s) :-> (a : Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair

  constructRational :: Unwrappabled r ~ (a, Natural) => a : Natural : s :-> r : s
  constructRational = (a : Natural : s) :-> ((a, Natural) : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair ((a : Natural : s) :-> ((a, Natural) : s))
-> (((a, Natural) : s) :-> (r : s))
-> (a : Natural : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, Natural) : s) :-> (r : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
((a, Natural) : s) :-> (r : s)
uncheckedPairToRational

  unsafePairToRational :: Unwrappabled r ~ (a, Natural) => (a, Natural) : s :-> r : s
  unsafePairToRational = ((a, Natural) : s) :-> (a : Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair (((a, Natural) : s) :-> (a : Natural : s))
-> ((a : Natural : s) :-> (a : Natural : s))
-> ((a, Natural) : s) :-> (a : Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((Natural : s) :-> (Natural : s))
-> (a : Natural : s) :-> (a : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip ((Natural : s) :-> (Natural : Natural : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup ((Natural : s) :-> (Natural : Natural : s))
-> ((Natural : Natural : s) :-> (Natural : s))
-> (Natural : s) :-> (Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# MText -> (Natural : Natural : s) :-> (Natural : s)
forall a err (s :: [*]).
(IfCmp0Constraints a Neq, IsError err) =>
err -> (a : s) :-> s
assertNeq0 [mt|Attempt to construct rational with zero denominator|]) (((a, Natural) : s) :-> (a : Natural : s))
-> ((a : Natural : s) :-> ((a, Natural) : s))
-> ((a, Natural) : s) :-> ((a, Natural) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : Natural : s) :-> ((a, Natural) : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair (((a, Natural) : s) :-> ((a, Natural) : s))
-> (((a, Natural) : s) :-> (r : s))
-> ((a, Natural) : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, Natural) : s) :-> (r : s)
forall a (s :: [*]).
Unwrappable a =>
(Unwrappabled a : s) :-> (a : s)
unsafeCoerceWrap

  uncheckedPairToRational :: Unwrappabled r ~ (a, Natural) => (a, Natural) : s :-> r : s
  uncheckedPairToRational = ((a, Natural) : s) :-> (r : s)
forall a (s :: [*]).
Unwrappable a =>
(Unwrappabled a : s) :-> (a : s)
unsafeCoerceWrap

  pairToRational :: (Unwrappabled r ~ (a, Natural), KnownValue r) => (a, Natural) : s :-> Maybe r : s
  pairToRational = do
    ((a, Natural) : s) :-> (a : Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair; (a : Natural : s) :-> (Natural : a : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
    (Natural : a : s) :-> (Natural : Natural : a : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup
    ((Natural : a : s) :-> (Maybe r : s))
-> ((Natural : a : s) :-> (Maybe r : s))
-> (Natural : Natural : a : s) :-> (Maybe r : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Eq' =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifEq0
      do
        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
        s :-> (Maybe r : s)
forall a (s :: [*]). KnownValue a => s :-> (Maybe a : s)
none
      do
        (Natural : a : s) :-> (a : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
        (a : Natural : s) :-> ((a, Natural) : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair
        ((a, Natural) : s) :-> (r : s)
forall a (s :: [*]).
Unwrappable a =>
(Unwrappabled a : s) :-> (a : s)
unsafeCoerceWrap
        (r : s) :-> (Maybe r : s)
forall a (s :: [*]). (a : s) :-> (Maybe a : s)
some

  oppositeRational :: r : s :-> r : s

  reduce :: (KnownList s, KnownList (ToTs s)) => r : s :-> r : s

instance LorentzRational Rational where
  oppositeRational :: forall (s :: [*]). (Rational : s) :-> (Rational : s)
oppositeRational = do
    (Rational : s) :-> (Integer : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
    (Integer : Natural : s) :-> (Integer : Integer : Natural : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup
    ((Integer : Natural : s) :-> (Integer : Integer : s))
-> ((Integer : Natural : s) :-> (Integer : Integer : s))
-> (Integer : Integer : Natural : s) :-> (Integer : Integer : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Lt =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifLt0 (((Natural : s) :-> (Integer : s))
-> (Integer : Natural : s) :-> (Integer : Integer : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Natural : s) :-> (Integer : s)
forall n (s :: [*]).
UnaryArithOpHs Neg n =>
(n : s) :-> (UnaryArithResHs Neg n : s)
neg) (((Natural : s) :-> (Integer : s))
-> (Integer : Natural : s) :-> (Integer : Integer : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Natural : s) :-> (Integer : s)
forall i (s :: [*]).
ToIntegerArithOpHs i =>
(i : s) :-> (Integer : s)
int)
    (Integer : Integer : s) :-> (Natural : Integer : s)
forall n (s :: [*]).
UnaryArithOpHs Abs n =>
(n : s) :-> (UnaryArithResHs Abs n : s)
abs
    (Natural : Integer : s) :-> (Integer : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
    (Integer : Natural : s) :-> (Rational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational
  reduce :: forall (s :: [*]).
(KnownList s, KnownList (ToTs s)) =>
(Rational : s) :-> (Rational : s)
reduce = (Rational : s) :-> (Rational : s)
forall (s :: [*]). (Rational : s) :-> (Rational : s)
reduceRationalHelper

instance LorentzRational NRational where
  oppositeRational :: forall (s :: [*]). (NRational : s) :-> (NRational : s)
oppositeRational = do
    (NRational : s) :-> (Natural : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
    (Natural : Natural : s) :-> (Natural : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
    (Natural : Natural : s) :-> (NRational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational
  reduce :: forall (s :: [*]).
(KnownList s, KnownList (ToTs s)) =>
(NRational : s) :-> (NRational : s)
reduce = (NRational : s) :-> (NRational : s)
forall (s :: [*]). (NRational : s) :-> (NRational : s)
reduceNRationalHelper

instance (r ~ Rational) => ArithOpHs Add Rational Integer r where
  evalArithOpHs :: forall (s :: [*]). (Rational : Integer : s) :-> (r : s)
evalArithOpHs = (Rational : Integer : s) :-> (Integer : Rational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((Rational : Integer : s) :-> (Integer : Rational : s))
-> ((Integer : Rational : s) :-> (r : s))
-> (Rational : Integer : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Rational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
instance (r ~ Rational) => ArithOpHs Add Integer Rational r where
  evalArithOpHs :: forall (s :: [*]). (Integer : Rational : s) :-> (r : s)
evalArithOpHs = ((Integer : Integer : Natural : s) :-> (Integer : Natural : s))
-> (Integer : Rational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 b r (s1 :: [*]) (s2 :: [*]).
(b ~ Natural, NiceConstant a1, ArithOpHs Mul a2 a1 r,
 Unwrappable a3, Unwrappabled a3 ~ (a5, a1),
 Unwrappabled a4 ~ (a6, Natural), LorentzRational a4) =>
((r : a5 : a1 : s1) :-> (a6 : b : s2))
-> (a2 : a3 : s1) :-> (a4 : s2)
addSubHelper (Integer : Integer : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
instance (r ~ Rational) => ArithOpHs Add Rational Natural r where
  evalArithOpHs :: forall (s :: [*]). (Rational : Natural : s) :-> (r : s)
evalArithOpHs = (Rational : Natural : s) :-> (Natural : Rational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((Rational : Natural : s) :-> (Natural : Rational : s))
-> ((Natural : Rational : s) :-> (r : s))
-> (Rational : Natural : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : Rational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
instance (r ~ Rational) => ArithOpHs Add Natural Rational r where
  evalArithOpHs :: forall (s :: [*]). (Natural : Rational : s) :-> (r : s)
evalArithOpHs = ((Natural : Integer : Natural : s) :-> (Integer : Natural : s))
-> (Natural : Rational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 b r (s1 :: [*]) (s2 :: [*]).
(b ~ Natural, NiceConstant a1, ArithOpHs Mul a2 a1 r,
 Unwrappable a3, Unwrappabled a3 ~ (a5, a1),
 Unwrappabled a4 ~ (a6, Natural), LorentzRational a4) =>
((r : a5 : a1 : s1) :-> (a6 : b : s2))
-> (a2 : a3 : s1) :-> (a4 : s2)
addSubHelper (Natural : Integer : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
instance (r ~ Rational) => ArithOpHs Add Rational Rational r where
  evalArithOpHs :: forall (s :: [*]). (Rational : Rational : s) :-> (r : s)
evalArithOpHs = ((Integer : Integer : Natural : Natural : s)
 :-> (Integer : Natural : Natural : s))
-> (Rational : Rational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 a7 a8 r1 r2 r3 n m (s1 :: [*])
       (s2 :: [*]).
(NiceConstant a1, NiceConstant a2, LorentzRational a7,
 r3 ~ Natural, ArithOpHs Mul a1 a3 r1, ArithOpHs Mul a2 a4 r2,
 ArithOpHs Mul n m r3, Unwrappable a5, Unwrappable a6,
 Unwrappabled a7 ~ (a8, r3), Unwrappabled a5 ~ (a3, a2),
 Unwrappabled a6 ~ (a4, a1)) =>
((r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2))
-> (a6 : a5 : s1) :-> (a7 : s2)
addSubRationalHelper (Integer : Integer : Natural : Natural : s)
:-> (Integer : Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add

instance (r ~ Rational) => ArithOpHs Sub Rational Integer r where
  evalArithOpHs :: forall (s :: [*]). (Rational : Integer : s) :-> (r : s)
evalArithOpHs = (Rational : Integer : s) :-> (Integer : Rational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((Rational : Integer : s) :-> (Integer : Rational : s))
-> ((Integer : Rational : s) :-> (Rational : s))
-> (Rational : Integer : s) :-> (Rational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Rational : s) :-> (Rational : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub ((Rational : Integer : s) :-> (Rational : s))
-> ((Rational : s) :-> (Rational : s))
-> (Rational : Integer : s) :-> (Rational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : s) :-> (Rational : s)
forall (s :: [*]). (Rational : s) :-> (Rational : s)
negRational
instance (r ~ Rational) => ArithOpHs Sub Integer Rational r where
  evalArithOpHs :: forall (s :: [*]). (Integer : Rational : s) :-> (r : s)
evalArithOpHs = ((Integer : Integer : Natural : s) :-> (Integer : Natural : s))
-> (Integer : Rational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 b r (s1 :: [*]) (s2 :: [*]).
(b ~ Natural, NiceConstant a1, ArithOpHs Mul a2 a1 r,
 Unwrappable a3, Unwrappabled a3 ~ (a5, a1),
 Unwrappabled a4 ~ (a6, Natural), LorentzRational a4) =>
((r : a5 : a1 : s1) :-> (a6 : b : s2))
-> (a2 : a3 : s1) :-> (a4 : s2)
addSubHelper (Integer : Integer : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub
instance (r ~ Rational) => ArithOpHs Sub Rational Natural r where
  evalArithOpHs :: forall (s :: [*]). (Rational : Natural : s) :-> (r : s)
evalArithOpHs = (Rational : Natural : s) :-> (Natural : Rational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((Rational : Natural : s) :-> (Natural : Rational : s))
-> ((Natural : Rational : s) :-> (Rational : s))
-> (Rational : Natural : s) :-> (Rational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : Rational : s) :-> (Rational : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub ((Rational : Natural : s) :-> (Rational : s))
-> ((Rational : s) :-> (Rational : s))
-> (Rational : Natural : s) :-> (Rational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : s) :-> (Rational : s)
forall (s :: [*]). (Rational : s) :-> (Rational : s)
negRational
instance (r ~ Rational) => ArithOpHs Sub Natural Rational r where
  evalArithOpHs :: forall (s :: [*]). (Natural : Rational : s) :-> (r : s)
evalArithOpHs = ((Natural : Integer : Natural : s) :-> (Integer : Natural : s))
-> (Natural : Rational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 b r (s1 :: [*]) (s2 :: [*]).
(b ~ Natural, NiceConstant a1, ArithOpHs Mul a2 a1 r,
 Unwrappable a3, Unwrappabled a3 ~ (a5, a1),
 Unwrappabled a4 ~ (a6, Natural), LorentzRational a4) =>
((r : a5 : a1 : s1) :-> (a6 : b : s2))
-> (a2 : a3 : s1) :-> (a4 : s2)
addSubHelper (Natural : Integer : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub
instance (r ~ Rational) => ArithOpHs Sub Rational Rational r where
  evalArithOpHs :: forall (s :: [*]). (Rational : Rational : s) :-> (r : s)
evalArithOpHs = ((Integer : Integer : Natural : Natural : s)
 :-> (Integer : Natural : Natural : s))
-> (Rational : Rational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 a7 a8 r1 r2 r3 n m (s1 :: [*])
       (s2 :: [*]).
(NiceConstant a1, NiceConstant a2, LorentzRational a7,
 r3 ~ Natural, ArithOpHs Mul a1 a3 r1, ArithOpHs Mul a2 a4 r2,
 ArithOpHs Mul n m r3, Unwrappable a5, Unwrappable a6,
 Unwrappabled a7 ~ (a8, r3), Unwrappabled a5 ~ (a3, a2),
 Unwrappabled a6 ~ (a4, a1)) =>
((r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2))
-> (a6 : a5 : s1) :-> (a7 : s2)
addSubRationalHelper (Integer : Integer : Natural : Natural : s)
:-> (Integer : Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub

instance (r ~ Rational) => ArithOpHs Mul Rational Integer r where
  evalArithOpHs :: forall (s :: [*]). (Rational : Integer : s) :-> (r : s)
evalArithOpHs = (Rational : Integer : s) :-> (Integer : Rational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((Rational : Integer : s) :-> (Integer : Rational : s))
-> ((Integer : Rational : s) :-> (r : s))
-> (Rational : Integer : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Rational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ Rational) => ArithOpHs Mul Integer Rational r where
  evalArithOpHs :: forall (s :: [*]). (Integer : Rational : s) :-> (r : s)
evalArithOpHs = ((Rational : s) :-> (Integer : Natural : s))
-> (Integer : Rational : s) :-> (Integer : Integer : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Rational : s) :-> (Integer : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational ((Integer : Rational : s) :-> (Integer : Integer : Natural : s))
-> ((Integer : Integer : Natural : s) :-> (Integer : Natural : s))
-> (Integer : Rational : s) :-> (Integer : Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Integer : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul ((Integer : Rational : s) :-> (Integer : Natural : s))
-> ((Integer : Natural : s) :-> (r : s))
-> (Integer : Rational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Natural : s) :-> (r : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational
instance (r ~ Rational) => ArithOpHs Mul Rational Natural r where
  evalArithOpHs :: forall (s :: [*]). (Rational : Natural : s) :-> (r : s)
evalArithOpHs = (Rational : Natural : s) :-> (Natural : Rational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((Rational : Natural : s) :-> (Natural : Rational : s))
-> ((Natural : Rational : s) :-> (r : s))
-> (Rational : Natural : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : Rational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ Rational) => ArithOpHs Mul Natural Rational r where
  evalArithOpHs :: forall (s :: [*]). (Natural : Rational : s) :-> (r : s)
evalArithOpHs = ((Rational : s) :-> (Integer : Natural : s))
-> (Natural : Rational : s) :-> (Natural : Integer : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Rational : s) :-> (Integer : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational ((Natural : Rational : s) :-> (Natural : Integer : Natural : s))
-> ((Natural : Integer : Natural : s) :-> (Integer : Natural : s))
-> (Natural : Rational : s) :-> (Integer : Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : Integer : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul ((Natural : Rational : s) :-> (Integer : Natural : s))
-> ((Integer : Natural : s) :-> (r : s))
-> (Natural : Rational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Natural : s) :-> (r : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational

instance (r ~ Rational) => ArithOpHs Mul Rational Rational r where
  evalArithOpHs :: forall (s :: [*]). (Rational : Rational : s) :-> (r : s)
evalArithOpHs = forall r1 r2 r3 a b c (s :: [*]).
(LorentzRational r1, LorentzRational r2, LorentzRational r3,
 Unwrappabled r1 ~ (a, Natural), Unwrappabled r2 ~ (b, Natural),
 Unwrappabled r3 ~ (c, Natural), ArithOpHs Mul a b c) =>
(r1 : r2 : s) :-> (r3 : s)
mulRationalHelper @Rational @Rational @Rational

instance (r ~ Rational) => ArithOpHs Div Integer Rational r where
  evalArithOpHs :: forall (s :: [*]). (Integer : Rational : s) :-> (r : s)
evalArithOpHs = ((Rational : s) :-> (Rational : s))
-> (Integer : Rational : s) :-> (Integer : Rational : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Rational : s) :-> (Rational : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((Integer : Rational : s) :-> (Integer : Rational : s))
-> ((Integer : Rational : s) :-> (r : s))
-> (Integer : Rational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Rational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ Rational) => ArithOpHs Div Natural Rational r where
  evalArithOpHs :: forall (s :: [*]). (Natural : Rational : s) :-> (r : s)
evalArithOpHs = ((Rational : s) :-> (Rational : s))
-> (Natural : Rational : s) :-> (Natural : Rational : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Rational : s) :-> (Rational : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((Natural : Rational : s) :-> (Natural : Rational : s))
-> ((Natural : Rational : s) :-> (r : s))
-> (Natural : Rational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : Rational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ Rational) => ArithOpHs Div Rational Integer r where
  evalArithOpHs :: forall (s :: [*]). (Rational : Integer : s) :-> (r : s)
evalArithOpHs = (Rational : Integer : s) :-> (Rational : Integer : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((Rational : Integer : s) :-> (Rational : Integer : s))
-> ((Rational : Integer : s) :-> (r : s))
-> (Rational : Integer : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : Integer : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul ((Rational : Integer : s) :-> (r : s))
-> ((r : s) :-> (r : s)) -> (Rational : Integer : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (r : s) :-> (r : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational
instance (r ~ Rational) => ArithOpHs Div Rational Natural r where
  evalArithOpHs :: forall (s :: [*]). (Rational : Natural : s) :-> (r : s)
evalArithOpHs = (Rational : Natural : s) :-> (Rational : Natural : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((Rational : Natural : s) :-> (Rational : Natural : s))
-> ((Rational : Natural : s) :-> (r : s))
-> (Rational : Natural : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : Natural : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ Rational) => ArithOpHs Div Rational Rational r where
  evalArithOpHs :: forall (s :: [*]). (Rational : Rational : s) :-> (r : s)
evalArithOpHs = ((Rational : s) :-> (Rational : s))
-> (Rational : Rational : s) :-> (Rational : Rational : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Rational : s) :-> (Rational : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((Rational : Rational : s) :-> (Rational : Rational : s))
-> ((Rational : Rational : s) :-> (r : s))
-> (Rational : Rational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : Rational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul

instance (r ~ Rational) => ArithOpHs Add NRational Integer r where
  evalArithOpHs :: forall (s :: [*]). (NRational : Integer : s) :-> (r : s)
evalArithOpHs = (NRational : Integer : s) :-> (Integer : NRational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((NRational : Integer : s) :-> (Integer : NRational : s))
-> ((Integer : NRational : s) :-> (r : s))
-> (NRational : Integer : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : NRational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
instance (r ~ Rational) => ArithOpHs Add Integer NRational r where
  evalArithOpHs :: forall (s :: [*]). (Integer : NRational : s) :-> (r : s)
evalArithOpHs = ((Integer : Natural : Natural : s) :-> (Integer : Natural : s))
-> (Integer : NRational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 b r (s1 :: [*]) (s2 :: [*]).
(b ~ Natural, NiceConstant a1, ArithOpHs Mul a2 a1 r,
 Unwrappable a3, Unwrappabled a3 ~ (a5, a1),
 Unwrappabled a4 ~ (a6, Natural), LorentzRational a4) =>
((r : a5 : a1 : s1) :-> (a6 : b : s2))
-> (a2 : a3 : s1) :-> (a4 : s2)
addSubHelper (Integer : Natural : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
instance (r ~ NRational) => ArithOpHs Add NRational Natural r where
  evalArithOpHs :: forall (s :: [*]). (NRational : Natural : s) :-> (r : s)
evalArithOpHs = (NRational : Natural : s) :-> (Natural : NRational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((NRational : Natural : s) :-> (Natural : NRational : s))
-> ((Natural : NRational : s) :-> (r : s))
-> (NRational : Natural : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : NRational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
instance (r ~ NRational) => ArithOpHs Add Natural NRational r where
  evalArithOpHs :: forall (s :: [*]). (Natural : NRational : s) :-> (r : s)
evalArithOpHs = ((Natural : Natural : Natural : s) :-> (Natural : Natural : s))
-> (Natural : NRational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 b r (s1 :: [*]) (s2 :: [*]).
(b ~ Natural, NiceConstant a1, ArithOpHs Mul a2 a1 r,
 Unwrappable a3, Unwrappabled a3 ~ (a5, a1),
 Unwrappabled a4 ~ (a6, Natural), LorentzRational a4) =>
((r : a5 : a1 : s1) :-> (a6 : b : s2))
-> (a2 : a3 : s1) :-> (a4 : s2)
addSubHelper (Natural : Natural : Natural : s) :-> (Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
instance (r ~ NRational) => ArithOpHs Add NRational NRational r where
  evalArithOpHs :: forall (s :: [*]). (NRational : NRational : s) :-> (r : s)
evalArithOpHs = ((Natural : Natural : Natural : Natural : s)
 :-> (Natural : Natural : Natural : s))
-> (NRational : NRational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 a7 a8 r1 r2 r3 n m (s1 :: [*])
       (s2 :: [*]).
(NiceConstant a1, NiceConstant a2, LorentzRational a7,
 r3 ~ Natural, ArithOpHs Mul a1 a3 r1, ArithOpHs Mul a2 a4 r2,
 ArithOpHs Mul n m r3, Unwrappable a5, Unwrappable a6,
 Unwrappabled a7 ~ (a8, r3), Unwrappabled a5 ~ (a3, a2),
 Unwrappabled a6 ~ (a4, a1)) =>
((r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2))
-> (a6 : a5 : s1) :-> (a7 : s2)
addSubRationalHelper (Natural : Natural : Natural : Natural : s)
:-> (Natural : Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add

instance (r ~ Rational) => ArithOpHs Sub NRational Integer r where
  evalArithOpHs :: forall (s :: [*]). (NRational : Integer : s) :-> (r : s)
evalArithOpHs = (NRational : Integer : s) :-> (Integer : NRational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((NRational : Integer : s) :-> (Integer : NRational : s))
-> ((Integer : NRational : s) :-> (Rational : s))
-> (NRational : Integer : s) :-> (Rational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : NRational : s) :-> (Rational : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub ((NRational : Integer : s) :-> (Rational : s))
-> ((Rational : s) :-> (Rational : s))
-> (NRational : Integer : s) :-> (Rational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : s) :-> (Rational : s)
forall (s :: [*]). (Rational : s) :-> (Rational : s)
negRational
instance (r ~ Rational) => ArithOpHs Sub Integer NRational r where
  evalArithOpHs :: forall (s :: [*]). (Integer : NRational : s) :-> (r : s)
evalArithOpHs = ((Integer : Natural : Natural : s) :-> (Integer : Natural : s))
-> (Integer : NRational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 b r (s1 :: [*]) (s2 :: [*]).
(b ~ Natural, NiceConstant a1, ArithOpHs Mul a2 a1 r,
 Unwrappable a3, Unwrappabled a3 ~ (a5, a1),
 Unwrappabled a4 ~ (a6, Natural), LorentzRational a4) =>
((r : a5 : a1 : s1) :-> (a6 : b : s2))
-> (a2 : a3 : s1) :-> (a4 : s2)
addSubHelper (Integer : Natural : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub
instance (r ~ Rational) => ArithOpHs Sub NRational Natural r where
  evalArithOpHs :: forall (s :: [*]). (NRational : Natural : s) :-> (r : s)
evalArithOpHs = (NRational : Natural : s) :-> (Natural : NRational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((NRational : Natural : s) :-> (Natural : NRational : s))
-> ((Natural : NRational : s) :-> (Rational : s))
-> (NRational : Natural : s) :-> (Rational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : NRational : s) :-> (Rational : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub ((NRational : Natural : s) :-> (Rational : s))
-> ((Rational : s) :-> (Rational : s))
-> (NRational : Natural : s) :-> (Rational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : s) :-> (Rational : s)
forall (s :: [*]). (Rational : s) :-> (Rational : s)
negRational
instance (r ~ Rational) => ArithOpHs Sub Natural NRational r where
  evalArithOpHs :: forall (s :: [*]). (Natural : NRational : s) :-> (r : s)
evalArithOpHs = ((Natural : Natural : Natural : s) :-> (Integer : Natural : s))
-> (Natural : NRational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 b r (s1 :: [*]) (s2 :: [*]).
(b ~ Natural, NiceConstant a1, ArithOpHs Mul a2 a1 r,
 Unwrappable a3, Unwrappabled a3 ~ (a5, a1),
 Unwrappabled a4 ~ (a6, Natural), LorentzRational a4) =>
((r : a5 : a1 : s1) :-> (a6 : b : s2))
-> (a2 : a3 : s1) :-> (a4 : s2)
addSubHelper (Natural : Natural : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub
instance (r ~ Rational) => ArithOpHs Sub NRational NRational r where
  evalArithOpHs :: forall (s :: [*]). (NRational : NRational : s) :-> (r : s)
evalArithOpHs = ((Natural : Natural : Natural : Natural : s)
 :-> (Integer : Natural : Natural : s))
-> (NRational : NRational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 a7 a8 r1 r2 r3 n m (s1 :: [*])
       (s2 :: [*]).
(NiceConstant a1, NiceConstant a2, LorentzRational a7,
 r3 ~ Natural, ArithOpHs Mul a1 a3 r1, ArithOpHs Mul a2 a4 r2,
 ArithOpHs Mul n m r3, Unwrappable a5, Unwrappable a6,
 Unwrappabled a7 ~ (a8, r3), Unwrappabled a5 ~ (a3, a2),
 Unwrappabled a6 ~ (a4, a1)) =>
((r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2))
-> (a6 : a5 : s1) :-> (a7 : s2)
addSubRationalHelper (Natural : Natural : Natural : Natural : s)
:-> (Integer : Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub

instance (r ~ Rational) => ArithOpHs Mul NRational Integer r where
  evalArithOpHs :: forall (s :: [*]). (NRational : Integer : s) :-> (r : s)
evalArithOpHs = (NRational : Integer : s) :-> (Integer : NRational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((NRational : Integer : s) :-> (Integer : NRational : s))
-> ((Integer : NRational : s) :-> (r : s))
-> (NRational : Integer : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : NRational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ Rational) => ArithOpHs Mul Integer NRational r where
  evalArithOpHs :: forall (s :: [*]). (Integer : NRational : s) :-> (r : s)
evalArithOpHs = ((NRational : s) :-> (Natural : Natural : s))
-> (Integer : NRational : s) :-> (Integer : Natural : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (NRational : s) :-> (Natural : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational ((Integer : NRational : s) :-> (Integer : Natural : Natural : s))
-> ((Integer : Natural : Natural : s) :-> (Integer : Natural : s))
-> (Integer : NRational : s) :-> (Integer : Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Natural : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul ((Integer : NRational : s) :-> (Integer : Natural : s))
-> ((Integer : Natural : s) :-> (r : s))
-> (Integer : NRational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Natural : s) :-> (r : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational
instance (r ~ NRational) => ArithOpHs Mul NRational Natural r where
  evalArithOpHs :: forall (s :: [*]). (NRational : Natural : s) :-> (r : s)
evalArithOpHs = (NRational : Natural : s) :-> (Natural : NRational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((NRational : Natural : s) :-> (Natural : NRational : s))
-> ((Natural : NRational : s) :-> (r : s))
-> (NRational : Natural : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : NRational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ NRational) => ArithOpHs Mul Natural NRational r where
  evalArithOpHs :: forall (s :: [*]). (Natural : NRational : s) :-> (r : s)
evalArithOpHs = ((NRational : s) :-> (Natural : Natural : s))
-> (Natural : NRational : s) :-> (Natural : Natural : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (NRational : s) :-> (Natural : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational ((Natural : NRational : s) :-> (Natural : Natural : Natural : s))
-> ((Natural : Natural : Natural : s) :-> (Natural : Natural : s))
-> (Natural : NRational : s) :-> (Natural : Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : Natural : Natural : s) :-> (Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul ((Natural : NRational : s) :-> (Natural : Natural : s))
-> ((Natural : Natural : s) :-> (r : s))
-> (Natural : NRational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : Natural : s) :-> (r : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational

instance (r ~ NRational) => ArithOpHs Mul NRational NRational r where
  evalArithOpHs :: forall (s :: [*]). (NRational : NRational : s) :-> (r : s)
evalArithOpHs = forall r1 r2 r3 a b c (s :: [*]).
(LorentzRational r1, LorentzRational r2, LorentzRational r3,
 Unwrappabled r1 ~ (a, Natural), Unwrappabled r2 ~ (b, Natural),
 Unwrappabled r3 ~ (c, Natural), ArithOpHs Mul a b c) =>
(r1 : r2 : s) :-> (r3 : s)
mulRationalHelper @NRational @NRational @NRational

instance (r ~ Rational) => ArithOpHs Div Integer NRational r where
  evalArithOpHs :: forall (s :: [*]). (Integer : NRational : s) :-> (r : s)
evalArithOpHs = ((NRational : s) :-> (NRational : s))
-> (Integer : NRational : s) :-> (Integer : NRational : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (NRational : s) :-> (NRational : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((Integer : NRational : s) :-> (Integer : NRational : s))
-> ((Integer : NRational : s) :-> (r : s))
-> (Integer : NRational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : NRational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ NRational) => ArithOpHs Div Natural NRational r where
  evalArithOpHs :: forall (s :: [*]). (Natural : NRational : s) :-> (r : s)
evalArithOpHs = ((NRational : s) :-> (NRational : s))
-> (Natural : NRational : s) :-> (Natural : NRational : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (NRational : s) :-> (NRational : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((Natural : NRational : s) :-> (Natural : NRational : s))
-> ((Natural : NRational : s) :-> (r : s))
-> (Natural : NRational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : NRational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ Rational) => ArithOpHs Div NRational Integer r where
  evalArithOpHs :: forall (s :: [*]). (NRational : Integer : s) :-> (r : s)
evalArithOpHs = (NRational : Integer : s) :-> (NRational : Integer : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((NRational : Integer : s) :-> (NRational : Integer : s))
-> ((NRational : Integer : s) :-> (r : s))
-> (NRational : Integer : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (NRational : Integer : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul ((NRational : Integer : s) :-> (r : s))
-> ((r : s) :-> (r : s)) -> (NRational : Integer : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (r : s) :-> (r : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational
instance (r ~ NRational) => ArithOpHs Div NRational Natural r where
  evalArithOpHs :: forall (s :: [*]). (NRational : Natural : s) :-> (r : s)
evalArithOpHs = (NRational : Natural : s) :-> (NRational : Natural : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((NRational : Natural : s) :-> (NRational : Natural : s))
-> ((NRational : Natural : s) :-> (r : s))
-> (NRational : Natural : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (NRational : Natural : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ NRational) => ArithOpHs Div NRational NRational r where
  evalArithOpHs :: forall (s :: [*]). (NRational : NRational : s) :-> (r : s)
evalArithOpHs = ((NRational : s) :-> (NRational : s))
-> (NRational : NRational : s) :-> (NRational : NRational : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (NRational : s) :-> (NRational : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((NRational : NRational : s) :-> (NRational : NRational : s))
-> ((NRational : NRational : s) :-> (r : s))
-> (NRational : NRational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (NRational : NRational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul

instance (r ~ Rational) => ArithOpHs Add Rational NRational r where
  evalArithOpHs :: forall (s :: [*]). (Rational : NRational : s) :-> (r : s)
evalArithOpHs = ((Integer : Natural : Natural : Natural : s)
 :-> (Integer : Natural : Natural : s))
-> (Rational : NRational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 a7 a8 r1 r2 r3 n m (s1 :: [*])
       (s2 :: [*]).
(NiceConstant a1, NiceConstant a2, LorentzRational a7,
 r3 ~ Natural, ArithOpHs Mul a1 a3 r1, ArithOpHs Mul a2 a4 r2,
 ArithOpHs Mul n m r3, Unwrappable a5, Unwrappable a6,
 Unwrappabled a7 ~ (a8, r3), Unwrappabled a5 ~ (a3, a2),
 Unwrappabled a6 ~ (a4, a1)) =>
((r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2))
-> (a6 : a5 : s1) :-> (a7 : s2)
addSubRationalHelper (Integer : Natural : Natural : Natural : s)
:-> (Integer : Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
instance (r ~ Rational) => ArithOpHs Add NRational Rational r where
  evalArithOpHs :: forall (s :: [*]). (NRational : Rational : s) :-> (r : s)
evalArithOpHs = ((Natural : Integer : Natural : Natural : s)
 :-> (Integer : Natural : Natural : s))
-> (NRational : Rational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 a7 a8 r1 r2 r3 n m (s1 :: [*])
       (s2 :: [*]).
(NiceConstant a1, NiceConstant a2, LorentzRational a7,
 r3 ~ Natural, ArithOpHs Mul a1 a3 r1, ArithOpHs Mul a2 a4 r2,
 ArithOpHs Mul n m r3, Unwrappable a5, Unwrappable a6,
 Unwrappabled a7 ~ (a8, r3), Unwrappabled a5 ~ (a3, a2),
 Unwrappabled a6 ~ (a4, a1)) =>
((r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2))
-> (a6 : a5 : s1) :-> (a7 : s2)
addSubRationalHelper (Natural : Integer : Natural : Natural : s)
:-> (Integer : Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
instance (r ~ Rational) => ArithOpHs Sub Rational NRational r where
  evalArithOpHs :: forall (s :: [*]). (Rational : NRational : s) :-> (r : s)
evalArithOpHs = ((Integer : Natural : Natural : Natural : s)
 :-> (Integer : Natural : Natural : s))
-> (Rational : NRational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 a7 a8 r1 r2 r3 n m (s1 :: [*])
       (s2 :: [*]).
(NiceConstant a1, NiceConstant a2, LorentzRational a7,
 r3 ~ Natural, ArithOpHs Mul a1 a3 r1, ArithOpHs Mul a2 a4 r2,
 ArithOpHs Mul n m r3, Unwrappable a5, Unwrappable a6,
 Unwrappabled a7 ~ (a8, r3), Unwrappabled a5 ~ (a3, a2),
 Unwrappabled a6 ~ (a4, a1)) =>
((r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2))
-> (a6 : a5 : s1) :-> (a7 : s2)
addSubRationalHelper (Integer : Natural : Natural : Natural : s)
:-> (Integer : Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub
instance (r ~ Rational) => ArithOpHs Sub NRational Rational r where
  evalArithOpHs :: forall (s :: [*]). (NRational : Rational : s) :-> (r : s)
evalArithOpHs = ((Natural : Integer : Natural : Natural : s)
 :-> (Integer : Natural : Natural : s))
-> (NRational : Rational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 a7 a8 r1 r2 r3 n m (s1 :: [*])
       (s2 :: [*]).
(NiceConstant a1, NiceConstant a2, LorentzRational a7,
 r3 ~ Natural, ArithOpHs Mul a1 a3 r1, ArithOpHs Mul a2 a4 r2,
 ArithOpHs Mul n m r3, Unwrappable a5, Unwrappable a6,
 Unwrappabled a7 ~ (a8, r3), Unwrappabled a5 ~ (a3, a2),
 Unwrappabled a6 ~ (a4, a1)) =>
((r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2))
-> (a6 : a5 : s1) :-> (a7 : s2)
addSubRationalHelper (Natural : Integer : Natural : Natural : s)
:-> (Integer : Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub
instance (r ~ Rational) => ArithOpHs Mul Rational NRational r where
  evalArithOpHs :: forall (s :: [*]). (Rational : NRational : s) :-> (r : s)
evalArithOpHs = forall r1 r2 r3 a b c (s :: [*]).
(LorentzRational r1, LorentzRational r2, LorentzRational r3,
 Unwrappabled r1 ~ (a, Natural), Unwrappabled r2 ~ (b, Natural),
 Unwrappabled r3 ~ (c, Natural), ArithOpHs Mul a b c) =>
(r1 : r2 : s) :-> (r3 : s)
mulRationalHelper @Rational @NRational @Rational
instance (r ~ Rational) => ArithOpHs Mul NRational Rational r where
  evalArithOpHs :: forall (s :: [*]). (NRational : Rational : s) :-> (r : s)
evalArithOpHs = forall r1 r2 r3 a b c (s :: [*]).
(LorentzRational r1, LorentzRational r2, LorentzRational r3,
 Unwrappabled r1 ~ (a, Natural), Unwrappabled r2 ~ (b, Natural),
 Unwrappabled r3 ~ (c, Natural), ArithOpHs Mul a b c) =>
(r1 : r2 : s) :-> (r3 : s)
mulRationalHelper @NRational @Rational @Rational
instance (r ~ Rational) => ArithOpHs Div Rational NRational r where
  evalArithOpHs :: forall (s :: [*]). (Rational : NRational : s) :-> (r : s)
evalArithOpHs = ((NRational : s) :-> (NRational : s))
-> (Rational : NRational : s) :-> (Rational : NRational : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (NRational : s) :-> (NRational : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((Rational : NRational : s) :-> (Rational : NRational : s))
-> ((Rational : NRational : s) :-> (r : s))
-> (Rational : NRational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : NRational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ Rational) => ArithOpHs Div NRational Rational r where
  evalArithOpHs :: forall (s :: [*]). (NRational : Rational : s) :-> (r : s)
evalArithOpHs = ((Rational : s) :-> (Rational : s))
-> (NRational : Rational : s) :-> (NRational : Rational : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Rational : s) :-> (Rational : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((NRational : Rational : s) :-> (NRational : Rational : s))
-> ((NRational : Rational : s) :-> (r : s))
-> (NRational : Rational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (NRational : Rational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul


instance {-# OVERLAPPABLE #-} ( LorentzRational r
         , Unwrappabled r ~ (a, Natural)
         , ArithOpHs EDiv a Natural (Maybe (a, Natural))
         , ArithOpHs Add a Natural a
         , ArithOpHs Add Natural a a
         ) => LorentzRounding r a where
  round_ :: forall (s :: [*]). (r : s) :-> (a : s)
round_ = do
    (r : s) :-> (a : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational; ((Natural : s) :-> (Natural : Natural : s))
-> (a : Natural : s) :-> (a : Natural : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Natural : s) :-> (Natural : Natural : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup
    forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv @a @Natural @(Maybe (a, Natural)); Impossible "Division by zero impossible here"
-> (Maybe (a, Natural) : Natural : s)
   :-> ((a, Natural) : 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")
    ((a, Natural) : Natural : s) :-> (a : Natural : Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair
    ((Natural : Natural : s) :-> (Natural : s))
-> (a : Natural : Natural : s) :-> (a : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip do
      Natural
-> (Natural : Natural : s) :-> (Natural : Natural : Natural : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Natural
2 :: Natural)
      (Natural : Natural : Natural : s) :-> (Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
      (s :-> (Natural : s))
-> (s :-> (Natural : s))
-> (Natural : Natural : s) :-> (Natural : s)
forall a (s :: [*]) (s' :: [*]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a : a : s) :-> s'
ifGt (Natural -> s :-> (Natural : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Natural
1 :: Natural)) (Natural -> s :-> (Natural : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Natural
0 :: Natural))
    (a : Natural : s) :-> (a : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
  ceil_ :: forall (s :: [*]). (r : s) :-> (a : s)
ceil_ = do
    (r : s) :-> (a : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
    forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv @a @Natural @(Maybe (a, Natural)); Impossible "Division by zero impossible here"
-> (Maybe (a, Natural) : s) :-> ((a, 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")
    ((a, Natural) : s) :-> (a : Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair
    (a : Natural : s) :-> (Natural : a : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
    ((a : s) :-> (a : s))
-> ((a : s) :-> (a : s)) -> (Natural : a : s) :-> (a : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Eq' =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifEq0 (a : s) :-> (a : s)
forall (s :: [*]). s :-> s
nop (((a : s) :-> (a : s)) -> (Natural : a : s) :-> (a : s))
-> ((a : s) :-> (a : s)) -> (Natural : a : s) :-> (a : s)
forall a b. (a -> b) -> a -> b
$ do
      Natural -> (a : s) :-> (Natural : a : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Natural
1 :: Natural)
      (Natural : a : s) :-> (a : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
  floor_ :: forall (s :: [*]). (r : s) :-> (a : s)
floor_ = do
    (r : s) :-> (a : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
    forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv @a @Natural @(Maybe (a, Natural)); Impossible "Division by zero impossible here"
-> (Maybe (a, Natural) : s) :-> ((a, 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")
    ((a, Natural) : s) :-> (a : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : s)
car

-- | Special multiplication helper, in case you want to multiply three 'Rational values'
-- given values @(a / b) * (c / d) * (e / f)@ performs @(a * c * e) / (b * d * f)@.
tripleMul :: forall r a s. (ArithOpHs Mul a a a, Unwrappabled r ~ (a, Natural), LorentzRational r) => r : r : r : s :-> r : s
tripleMul :: forall r a (s :: [*]).
(ArithOpHs Mul a a a, Unwrappabled r ~ (a, Natural),
 LorentzRational r) =>
(r : r : r : s) :-> (r : s)
tripleMul = do
  ((r : r : s) :-> (a : Natural : a : Natural : s))
-> (r : r : r : s) :-> (r : a : Natural : a : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip do
    ((r : s) :-> (a : Natural : s))
-> (r : r : s) :-> (r : a : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (r : s) :-> (a : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
    (r : a : Natural : s) :-> (a : Natural : a : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
  (r : a : Natural : a : Natural : s)
:-> (a : Natural : a : Natural : a : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
  ((Natural : a : Natural : a : Natural : s)
 :-> (a : Natural : Natural : a : Natural : s))
-> (a : Natural : a : Natural : a : Natural : s)
   :-> (a : a : Natural : Natural : a : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip ((Natural : a : Natural : a : Natural : s)
:-> (a : Natural : Natural : a : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap)
  forall (n :: Nat) (inp :: [*]) (out :: [*]) (s :: [*]) (s' :: [*]).
ConstraintDIPNLorentz (ToPeano n) inp out s s' =>
(s :-> s') -> inp :-> out
dipN @3 ((Natural : a : Natural : s) :-> (a : Natural : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap)
  forall (n :: Nat) (inp :: [*]) (out :: [*]) (s :: [*]) (s' :: [*]).
ConstraintDIPNLorentz (ToPeano n) inp out s s' =>
(s :-> s') -> inp :-> out
dipN @2 ((Natural : a : Natural : Natural : s)
:-> (a : Natural : Natural : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap)
  forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul @a @a @a; forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul @a @a @a
  ((Natural : Natural : Natural : s) :-> (Natural : s))
-> (a : Natural : Natural : Natural : s) :-> (a : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (do (Natural : Natural : Natural : s) :-> (Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul; (Natural : Natural : s) :-> (Natural : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul)
  (a : Natural : s) :-> (r : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational

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

-- | For a given 'Natural' values, calculates their gcd, using Euclid algorithm.
gcdEuclid :: Natural : Natural : s :-> Natural : s
gcdEuclid :: forall (s :: [*]). (Natural : Natural : s) :-> (Natural : s)
gcdEuclid = do
  (Natural : Natural : s)
:-> (Natural : Natural : Natural : Natural : s)
forall a b (s :: [*]).
(Dupable a, Dupable b) =>
(a : b : s) :-> (a : b : a : b : s)
dupTop2
  ((Natural : Natural : s) :-> (Natural : Natural : s))
-> ((Natural : Natural : s) :-> (Natural : Natural : s))
-> (Natural : Natural : Natural : Natural : s)
   :-> (Natural : Natural : s)
forall a (s :: [*]) (s' :: [*]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a : a : s) :-> s'
ifLt (Natural : Natural : s) :-> (Natural : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap (Natural : Natural : s) :-> (Natural : Natural : s)
forall (s :: [*]). s :-> s
nop
  forall (n :: Nat) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @2
  (Natural : Natural : Natural : s)
:-> (Bool : Natural : Natural : s)
forall n (s :: [*]).
UnaryArithOpHs Neq n =>
(n : s) :-> (UnaryArithResHs Neq n : s)
neq0
  ((Natural : Natural : s) :-> (Bool : Natural : Natural : s))
-> (Bool : Natural : Natural : s) :-> (Natural : Natural : s)
forall (s :: [*]). (s :-> (Bool : s)) -> (Bool : s) :-> s
loop do
    ((Natural : s) :-> (Natural : Natural : s))
-> (Natural : Natural : s) :-> (Natural : Natural : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Natural : s) :-> (Natural : Natural : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup
    (Natural : Natural : Natural : s)
:-> (Maybe (Natural, Natural) : Natural : s)
forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv
    Impossible "Division by zero impossible here"
-> (Maybe (Natural, Natural) : Natural : s)
   :-> ((Natural, Natural) : 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")
    ((Natural, Natural) : Natural : s) :-> (Natural : Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (b : s)
cdr
    (Natural : Natural : s) :-> (Natural : Natural : Natural : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup
    (Natural : Natural : Natural : s)
:-> (Bool : Natural : Natural : s)
forall n (s :: [*]).
UnaryArithOpHs Neq n =>
(n : s) :-> (UnaryArithResHs Neq n : s)
neq0
    ((Natural : Natural : s) :-> (Natural : Natural : s))
-> (Bool : Natural : Natural : s)
   :-> (Bool : Natural : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Natural : Natural : s) :-> (Natural : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
  ((Natural : s) :-> s) -> (Natural : Natural : s) :-> (Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Natural : s) :-> s
forall a (s :: [*]). (a : s) :-> s
drop

-- | Reduce 'Rational' value to the point, when numerator's and denominator's gcd is 1.
-- This operation should be commonly used after several arithmetic operations, because
-- numerator and denominator can become quite big. That in order, can lead to serious
-- gas consumption.
reduceRationalHelper :: Rational : s :-> Rational : s
reduceRationalHelper :: forall (s :: [*]). (Rational : s) :-> (Rational : s)
reduceRationalHelper = do
  (Rational : s) :-> (Integer : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
  (Integer : Natural : s) :-> (Integer : Integer : Natural : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup; ((Integer : Natural : s) :-> (Integer : Integer : Natural : s))
-> ((Integer : Natural : s) :-> (Integer : Integer : Natural : s))
-> (Integer : Integer : Natural : s)
   :-> (Integer : Integer : Natural : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Lt =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifLt0 (Integer
-> (Integer : Natural : s) :-> (Integer : Integer : Natural : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Integer
-1 :: Integer)) (Integer
-> (Integer : Natural : s) :-> (Integer : Integer : Natural : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Integer
1 :: Integer)); forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz (ToPeano n) inp out a =>
inp :-> out
dug @2; (Integer : Natural : Integer : s)
:-> (Natural : Natural : Integer : s)
forall n (s :: [*]).
UnaryArithOpHs Abs n =>
(n : s) :-> (UnaryArithResHs Abs n : s)
abs;
  (Natural : Natural : Integer : s)
:-> (Natural : Natural : Integer : s)
forall (s :: [*]).
(Natural : Natural : s) :-> (Natural : Natural : s)
reduceHelper; forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDIGLorentz (ToPeano n) inp out a =>
inp :-> out
dig @2; (Integer : Natural : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul; (Integer : Natural : s) :-> ((Integer, Natural) : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair; ((Integer, Natural) : s) :-> (Rational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
((a, Natural) : s) :-> (r : s)
uncheckedPairToRational

reduceNRationalHelper :: NRational : s :-> NRational : s
reduceNRationalHelper :: forall (s :: [*]). (NRational : s) :-> (NRational : s)
reduceNRationalHelper = do
  (NRational : s) :-> (Natural : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
  (Natural : Natural : s) :-> (Natural : Natural : s)
forall (s :: [*]).
(Natural : Natural : s) :-> (Natural : Natural : s)
reduceHelper;
  (Natural : Natural : s) :-> (NRational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational

reduceHelper :: Natural : Natural : s :-> Natural : Natural : s
reduceHelper :: forall (s :: [*]).
(Natural : Natural : s) :-> (Natural : Natural : s)
reduceHelper = do
  (Natural : Natural : s)
:-> (Natural : Natural : Natural : Natural : s)
forall a b (s :: [*]).
(Dupable a, Dupable b) =>
(a : b : s) :-> (a : b : a : b : s)
dupTop2; (Natural : Natural : Natural : Natural : s)
:-> (Natural : Natural : Natural : s)
forall (s :: [*]). (Natural : Natural : s) :-> (Natural : s)
gcdEuclid; (Natural : Natural : Natural : s)
:-> (Natural : Natural : Natural : Natural : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup; Natural
-> (Natural : Natural : Natural : Natural : s)
   :-> (Natural : Natural : Natural : Natural : Natural : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Natural
1 :: Natural)
  ((Natural : Natural : Natural : s) :-> (Natural : Natural : s))
-> ((Natural : Natural : Natural : s) :-> (Natural : Natural : s))
-> (Natural : Natural : Natural : Natural : Natural : s)
   :-> (Natural : Natural : s)
forall a (s :: [*]) (s' :: [*]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a : a : s) :-> s'
ifEq (Natural : Natural : Natural : s) :-> (Natural : Natural : s)
forall a (s :: [*]). (a : s) :-> s
drop (((Natural : Natural : Natural : s) :-> (Natural : Natural : s))
 -> (Natural : Natural : Natural : Natural : Natural : s)
    :-> (Natural : Natural : s))
-> ((Natural : Natural : Natural : s) :-> (Natural : Natural : s))
-> (Natural : Natural : Natural : Natural : Natural : s)
   :-> (Natural : Natural : s)
forall a b. (a -> b) -> a -> b
$ do
    (Natural : Natural : Natural : s)
:-> (Natural : Natural : Natural : Natural : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup; forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz (ToPeano n) inp out a =>
inp :-> out
dug @3; (Natural : Natural : Natural : Natural : s)
:-> (Natural : Natural : Natural : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap;
    (Natural : Natural : Natural : Natural : s)
:-> (Maybe (Natural, Natural) : Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv; Impossible "Division by zero impossible here"
-> (Maybe (Natural, Natural) : Natural : Natural : s)
   :-> ((Natural, Natural) : Natural : 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"); ((Natural, Natural) : Natural : Natural : s)
:-> (Natural : Natural : Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : s)
car; forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz (ToPeano n) inp out a =>
inp :-> out
dug @2
    (Natural : Natural : Natural : s)
:-> (Maybe (Natural, Natural) : Natural : s)
forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv; Impossible "Division by zero impossible here"
-> (Maybe (Natural, Natural) : Natural : s)
   :-> ((Natural, Natural) : 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"); ((Natural, Natural) : Natural : s) :-> (Natural : Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : s)
car
    (Natural : Natural : s) :-> (Natural : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap

-- | Reduce 'Rational' value, using extended Euclid algorithm.
-- Consumes slightly more gas, than @reduce@, but contract with it is cheaper in terms of origination.
euclidExtendedNormalization :: forall s. Rational : s :-> Rational : s
euclidExtendedNormalization :: forall (s :: [*]). (Rational : s) :-> (Rational : s)
euclidExtendedNormalization = do
  (Rational : s) :-> (Integer : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational; ((Natural : s) :-> (Integer : s))
-> (Integer : Natural : s) :-> (Integer : Integer : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Natural : s) :-> (Integer : s)
forall i (s :: [*]).
ToIntegerArithOpHs i =>
(i : s) :-> (Integer : s)
int
  forall (n :: Nat) (inp :: [*]) (out :: [*]) (s :: [*]) (s' :: [*]).
ConstraintDIPNLorentz (ToPeano n) inp out s s' =>
(s :-> s') -> inp :-> out
dipN @2 do
    Integer -> s :-> (Integer : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Integer
1 :: Integer)
    Integer -> (Integer : s) :-> (Integer : Integer : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Integer
0 :: Integer)
    Integer
-> (Integer : Integer : s) :-> (Integer : Integer : Integer : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Integer
0 :: Integer)
    Integer
-> (Integer : Integer : Integer : s)
   :-> (Integer : Integer : Integer : Integer : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Integer
1 :: Integer)
  (Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer : Integer : Integer : Integer : Integer : Integer : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap; (Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer
       : Integer : Integer : Integer : Integer : Integer : Integer : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup; (Integer
   : Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Bool
       : Integer : Integer : Integer : Integer : Integer : Integer : s)
forall n (s :: [*]).
UnaryArithOpHs Neq n =>
(n : s) :-> (UnaryArithResHs Neq n : s)
neq0; ((Integer : Integer : Integer : Integer : Integer : Integer : s)
 :-> (Integer
        : Integer : Integer : Integer : Integer : Integer : s))
-> (Bool
      : Integer : Integer : Integer : Integer : Integer : Integer : s)
   :-> (Bool
          : Integer : Integer : Integer : Integer : Integer : Integer : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer : Integer : Integer : Integer : Integer : Integer : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap;
  ((Integer : Integer : Integer : Integer : Integer : Integer : s)
 :-> (Bool
        : Integer : Integer : Integer : Integer : Integer : Integer : s))
-> (Bool
      : Integer : Integer : Integer : Integer : Integer : Integer : s)
   :-> (Integer : Integer : Integer : Integer : Integer : Integer : s)
forall (s :: [*]). (s :-> (Bool : s)) -> (Bool : s) :-> s
loop do
    (Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer
       : Integer : Integer : Integer : Integer : Integer : Integer
       : Integer : s)
forall a b (s :: [*]).
(Dupable a, Dupable b) =>
(a : b : s) :-> (a : b : a : b : s)
dupTop2
    (Integer
   : Integer : Integer : Integer : Integer : Integer : Integer
   : Integer : s)
:-> (Maybe (Integer, Natural)
       : Integer : Integer : Integer : Integer : Integer : Integer : s)
forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv
    Impossible "Division by zero impossible here"
-> (Maybe (Integer, Natural)
      : Integer : Integer : Integer : Integer : Integer : Integer : s)
   :-> ((Integer, Natural)
          : Integer : Integer : Integer : Integer : Integer : Integer : 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")
    ((Integer, Natural)
   : Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer
       : Integer : Integer : Integer : Integer : Integer : Integer : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : s)
car
    (Integer
   : Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer
       : Integer : Integer : Integer : Integer : Integer : Integer
       : Integer : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup
    (Integer
   : Integer : Integer : Integer : Integer : Integer : Integer
   : Integer : s)
:-> (Integer
       : Integer : Integer : Integer : Integer : Integer : Integer
       : Integer : Integer : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup
    forall (n :: Nat) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @9; (Integer
   : Integer : Integer : Integer : Integer : Integer : Integer
   : Integer : Integer : Integer : s)
:-> (Integer
       : Integer : Integer : Integer : Integer : Integer : Integer
       : Integer : Integer : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul; forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDIGLorentz (ToPeano n) inp out a =>
inp :-> out
dig @7; (Integer
   : Integer : Integer : Integer : Integer : Integer : Integer
   : Integer : Integer : s)
:-> (Integer
       : Integer : Integer : Integer : Integer : Integer : Integer
       : Integer : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub; forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz (ToPeano n) inp out a =>
inp :-> out
dug @2
    forall (n :: Nat) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @7; (Integer
   : Integer : Integer : Integer : Integer : Integer : Integer
   : Integer : Integer : s)
:-> (Integer
       : Integer : Integer : Integer : Integer : Integer : Integer
       : Integer : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul; forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDIGLorentz (ToPeano n) inp out a =>
inp :-> out
dig @5; (Integer
   : Integer : Integer : Integer : Integer : Integer : Integer
   : Integer : s)
:-> (Integer
       : Integer : Integer : Integer : Integer : Integer : Integer : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub; (Integer
   : Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer
       : Integer : Integer : Integer : Integer : Integer : Integer : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
    forall (n :: Nat) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @5; (Integer
   : Integer : Integer : Integer : Integer : Integer : Integer
   : Integer : s)
:-> (Integer
       : Integer : Integer : Integer : Integer : Integer : Integer : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul; forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDIGLorentz (ToPeano n) inp out a =>
inp :-> out
dig @3; (Integer
   : Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer : Integer : Integer : Integer : Integer : Integer : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub
    forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDIGLorentz (ToPeano n) inp out a =>
inp :-> out
dig @3; forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDIGLorentz (ToPeano n) inp out a =>
inp :-> out
dig @4; forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz (ToPeano n) inp out a =>
inp :-> out
dug @2; forall (n :: Nat) (inp :: [*]) (out :: [*]) (s :: [*]) (s' :: [*]).
ConstraintDIPNLorentz (ToPeano n) inp out s s' =>
(s :-> s') -> inp :-> out
dipN @4 ((Integer : Integer : s) :-> (Integer : Integer : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap)
    (Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer : Integer : Integer : Integer : Integer : Integer : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap; (Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer
       : Integer : Integer : Integer : Integer : Integer : Integer : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup; (Integer
   : Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Bool
       : Integer : Integer : Integer : Integer : Integer : Integer : s)
forall n (s :: [*]).
UnaryArithOpHs Neq n =>
(n : s) :-> (UnaryArithResHs Neq n : s)
neq0; ((Integer : Integer : Integer : Integer : Integer : Integer : s)
 :-> (Integer
        : Integer : Integer : Integer : Integer : Integer : s))
-> (Bool
      : Integer : Integer : Integer : Integer : Integer : Integer : s)
   :-> (Bool
          : Integer : Integer : Integer : Integer : Integer : Integer : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer : Integer : Integer : Integer : Integer : Integer : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
  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 @3; ((Integer : Integer : s) :-> (Integer : s))
-> (Integer : Integer : Integer : s) :-> (Integer : Integer : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Integer : Integer : s) :-> (Integer : s)
forall a (s :: [*]). (a : s) :-> s
drop
  (Integer : Integer : s) :-> (Integer : Integer : Integer : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup; ((Integer : Integer : s) :-> (Integer : Integer : s))
-> ((Integer : Integer : s) :-> (Integer : Integer : s))
-> (Integer : Integer : Integer : s) :-> (Integer : Integer : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Lt =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifLt0 (((Integer : s) :-> (Integer : s))
-> (Integer : Integer : s) :-> (Integer : Integer : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Integer : s) :-> (Integer : s)
forall n (s :: [*]).
UnaryArithOpHs Neg n =>
(n : s) :-> (UnaryArithResHs Neg n : s)
neg) ((Integer : Integer : s) :-> (Integer : Integer : s)
forall (s :: [*]). s :-> s
nop); (Integer : Integer : s) :-> (Natural : Integer : s)
forall n (s :: [*]).
UnaryArithOpHs Abs n =>
(n : s) :-> (UnaryArithResHs Abs n : s)
abs; (Natural : Integer : s) :-> (Integer : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
  (Integer : Natural : s) :-> (Integer : Natural : s)
forall n (s :: [*]).
UnaryArithOpHs Neg n =>
(n : s) :-> (UnaryArithResHs Neg n : s)
neg; (Integer : Natural : s) :-> ((Integer, Natural) : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair; ((Integer, Natural) : s) :-> (Rational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
((a, Natural) : s) :-> (r : s)
uncheckedPairToRational

addSubHelper
  :: forall a1 a2 a3 a4 a5 a6 b r s1 s2.
     (  b ~ Natural
     , NiceConstant a1
     , ArithOpHs Mul a2 a1 r
     , Unwrappable a3
     , Unwrappabled a3 ~ (a5, a1)
     , Unwrappabled a4 ~ (a6, Natural)
     , LorentzRational a4
     )
  => ((r : a5 : a1 : s1) :-> (a6 : b : s2))
  -> (a2 : a3 : s1) :-> (a4 : s2)
addSubHelper :: forall a1 a2 a3 a4 a5 a6 b r (s1 :: [*]) (s2 :: [*]).
(b ~ Natural, NiceConstant a1, ArithOpHs Mul a2 a1 r,
 Unwrappable a3, Unwrappabled a3 ~ (a5, a1),
 Unwrappabled a4 ~ (a6, Natural), LorentzRational a4) =>
((r : a5 : a1 : s1) :-> (a6 : b : s2))
-> (a2 : a3 : s1) :-> (a4 : s2)
addSubHelper (r : a5 : a1 : s1) :-> (a6 : b : s2)
oper = do
  ((a3 : s1) :-> (a1 : a5 : a1 : s1))
-> (a2 : a3 : s1) :-> (a2 : a1 : a5 : a1 : s1)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip do
    (a3 : s1) :-> ((a5, a1) : s1)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap
    ((a5, a1) : s1) :-> (a5 : a1 : s1)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair
    forall (n :: Nat) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @2
  (a2 : a1 : a5 : a1 : s1) :-> (r : a5 : a1 : s1)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
  (r : a5 : a1 : s1) :-> (a6 : b : s2)
oper
  (a6 : b : s2) :-> ((a6, b) : s2)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair
  ((a6, b) : s2) :-> (a4 : s2)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
((a, Natural) : s) :-> (r : s)
uncheckedPairToRational

addSubRationalHelper
  :: forall a1 a2 a3 a4 a5 a6 a7 a8 r1 r2 r3 n m s1 s2.
    ( NiceConstant a1
    , NiceConstant a2
    , LorentzRational a7
    , r3 ~ Natural
    , ArithOpHs Mul a1 a3 r1, ArithOpHs Mul a2 a4 r2
    , ArithOpHs Mul n m r3, Unwrappable a5, Unwrappable a6
    , Unwrappabled a7 ~ (a8, r3)
    , Unwrappabled a5 ~ (a3, a2), Unwrappabled a6 ~ (a4, a1)
    )
  => ((r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2))
  -> (a6 : a5 : s1) :-> (a7 : s2)
addSubRationalHelper :: forall a1 a2 a3 a4 a5 a6 a7 a8 r1 r2 r3 n m (s1 :: [*])
       (s2 :: [*]).
(NiceConstant a1, NiceConstant a2, LorentzRational a7,
 r3 ~ Natural, ArithOpHs Mul a1 a3 r1, ArithOpHs Mul a2 a4 r2,
 ArithOpHs Mul n m r3, Unwrappable a5, Unwrappable a6,
 Unwrappabled a7 ~ (a8, r3), Unwrappabled a5 ~ (a3, a2),
 Unwrappabled a6 ~ (a4, a1)) =>
((r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2))
-> (a6 : a5 : s1) :-> (a7 : s2)
addSubRationalHelper (r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2)
oper = do
  ((a5 : s1) :-> (a3 : a2 : s1))
-> (a6 : a5 : s1) :-> (a6 : a3 : a2 : s1)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip do
    (a5 : s1) :-> ((a3, a2) : s1)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap
    ((a3, a2) : s1) :-> (a3 : a2 : s1)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair
  (a6 : a3 : a2 : s1) :-> ((a4, a1) : a3 : a2 : s1)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap; ((a4, a1) : a3 : a2 : s1) :-> (a4 : a1 : a3 : a2 : s1)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair
  ((a1 : a3 : a2 : s1) :-> (r1 : a1 : a2 : s1))
-> (a4 : a1 : a3 : a2 : s1) :-> (a4 : r1 : a1 : a2 : s1)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip do
    (a1 : a3 : a2 : s1) :-> (a1 : a1 : a3 : a2 : s1)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup
    forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz (ToPeano n) inp out a =>
inp :-> out
dug @2
    (a1 : a3 : a1 : a2 : s1) :-> (r1 : a1 : a2 : s1)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
  forall (n :: Nat) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @4
  (a2 : a4 : r1 : a1 : a2 : s1) :-> (r2 : r1 : a1 : a2 : s1)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
  (r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2)
oper
  ((n : m : s2) :-> (Natural : s2))
-> (a8 : n : m : s2) :-> (a8 : Natural : s2)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (n : m : s2) :-> (Natural : s2)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
  (a8 : Natural : s2) :-> ((a8, Natural) : s2)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair
  ((a8, Natural) : s2) :-> (a7 : s2)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
((a, Natural) : s) :-> (r : s)
uncheckedPairToRational

mulRationalHelper
  :: forall r1 r2 r3 a b c s.
     ( LorentzRational r1
     , LorentzRational r2
     , LorentzRational r3
     , Unwrappabled r1 ~ (a, Natural)
     , Unwrappabled r2 ~ (b, Natural)
     , Unwrappabled r3 ~ (c, Natural)
     , ArithOpHs Mul a b c
     )
  => r1 : r2 : s :-> r3 : s
mulRationalHelper :: forall r1 r2 r3 a b c (s :: [*]).
(LorentzRational r1, LorentzRational r2, LorentzRational r3,
 Unwrappabled r1 ~ (a, Natural), Unwrappabled r2 ~ (b, Natural),
 Unwrappabled r3 ~ (c, Natural), ArithOpHs Mul a b c) =>
(r1 : r2 : s) :-> (r3 : s)
mulRationalHelper = do
  ((r2 : s) :-> (b : Natural : s))
-> (r1 : r2 : s) :-> (r1 : b : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (r2 : s) :-> (b : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
  (r1 : b : Natural : s) :-> (a : Natural : b : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
  ((Natural : b : Natural : s) :-> (b : Natural : Natural : s))
-> (a : Natural : b : Natural : s)
   :-> (a : b : Natural : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Natural : b : Natural : s) :-> (b : Natural : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
  (a : b : Natural : Natural : s) :-> (c : Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
  ((Natural : Natural : s) :-> (Natural : s))
-> (c : Natural : Natural : s) :-> (c : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Natural : Natural : s) :-> (Natural : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
  (c : Natural : s) :-> (r3 : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational

negRational :: Rational : s :-> Rational : s
negRational :: forall (s :: [*]). (Rational : s) :-> (Rational : s)
negRational = (Rational : s) :-> (Integer : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational ((Rational : s) :-> (Integer : Natural : s))
-> ((Integer : Natural : s) :-> (Integer : Natural : s))
-> (Rational : s) :-> (Integer : Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Natural : s) :-> (Integer : Natural : s)
forall n (s :: [*]).
UnaryArithOpHs Neg n =>
(n : s) :-> (UnaryArithResHs Neg n : s)
neg ((Rational : s) :-> (Integer : Natural : s))
-> ((Integer : Natural : s) :-> (Rational : s))
-> (Rational : s) :-> (Rational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Natural : s) :-> (Rational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational

mkRational_
  :: (forall s0. ErrInstr (("numerator" :! Integer, "denominator" :! Natural) : s0))
  -> Integer : Natural : s :-> Rational : s
mkRational_ :: forall (s :: [*]).
(forall (s0 :: [*]).
 ErrInstr (("numerator" :! Integer, "denominator" :! Natural) : s0))
-> (Integer : Natural : s) :-> (Rational : s)
mkRational_ forall (s0 :: [*]).
ErrInstr (("numerator" :! Integer, "denominator" :! Natural) : s0)
onZeroDenominator = do
  (Integer : Natural : s) :-> (Natural : Integer : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
  (Natural : Integer : s) :-> (Natural : Natural : Integer : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup
  ((Natural : Integer : s) :-> (Rational : s))
-> ((Natural : Integer : s) :-> (Rational : s))
-> (Natural : Natural : Integer : s) :-> (Rational : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Eq' =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifEq0
    do
      Label "denominator"
-> (Natural : Integer : s)
   :-> (("denominator" :! Natural) : Integer : s)
forall (name :: Symbol) a (s :: [*]).
Label name -> (a : s) :-> ((name :! a) : s)
toNamed Label "denominator"
forall (x :: Symbol) a. IsLabel x a => a
#denominator
      (("denominator" :! Natural) : Integer : s)
:-> (Integer : ("denominator" :! Natural) : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
      Label "numerator"
-> (Integer : ("denominator" :! Natural) : s)
   :-> (("numerator" :! Integer) : ("denominator" :! Natural) : s)
forall (name :: Symbol) a (s :: [*]).
Label name -> (a : s) :-> ((name :! a) : s)
toNamed Label "numerator"
forall (x :: Symbol) a. IsLabel x a => a
#numerator
      (("numerator" :! Integer) : ("denominator" :! Natural) : s)
:-> (("numerator" :! Integer, "denominator" :! Natural) : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair
      (("numerator" :! Integer, "denominator" :! Natural) : s)
:-> (Rational : s)
forall (s0 :: [*]).
ErrInstr (("numerator" :! Integer, "denominator" :! Natural) : s0)
onZeroDenominator
    do
      (Natural : Integer : s) :-> (Integer : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
      (Integer : Natural : s) :-> (Rational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational

type instance ErrorArg "zero_denominator" =
  ("numerator" :! Integer, "denominator" :! Natural)

instance CustomErrorHasDoc "zero_denominator" where
  customErrClass :: ErrorClass
customErrClass = ErrorClass
ErrClassActionException
  customErrDocMdCause :: Markdown
customErrDocMdCause =
    Markdown
"Attempt to construct rational with zero denominator."