-- 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, ($), (++), (==), type (~))
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

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
$c== :: Rational -> Rational -> Bool
== :: Rational -> Rational -> Bool
$c/= :: Rational -> Rational -> Bool
/= :: 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)
Notes ('TPair 'TInt 'TNat)
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
$c== :: NRational -> NRational -> Bool
== :: NRational -> NRational -> Bool
$c/= :: NRational -> NRational -> Bool
/= :: 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)
Notes ('TPair 'TNat 'TNat)
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)
(r : s) :-> (Unwrappabled r : 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)
(r : s) :-> (Unwrappabled r : 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)
(r : s) :-> (Unwrappabled r : 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)
forall a (s :: [*]).
(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)
(Unwrappabled r : 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)
(Unwrappabled r : 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 :: Natural) (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)
(Unwrappabled r : 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 :: 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)
forall a (s :: [*]).
(Unwrappabled Rational ~ (a, Natural)) =>
(Rational : 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)
(Natural : s) :-> (UnaryArithResHs Neg Natural : 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)
(Integer : Integer : s)
:-> (UnaryArithResHs Abs Integer : 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)
forall a (s :: [*]).
(Unwrappabled Rational ~ (a, Natural)) =>
(a : Natural : s) :-> (Rational : s)
constructRational
  reduce :: forall (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)
forall a (s :: [*]).
(Unwrappabled NRational ~ (a, Natural)) =>
(NRational : 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)
forall a (s :: [*]).
(Unwrappabled NRational ~ (a, Natural)) =>
(a : Natural : s) :-> (NRational : s)
constructRational
  reduce :: forall (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) :-> (r : s))
-> (Rational : Integer : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : s) :-> (r : s)
(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) :-> (r : s))
-> (Rational : Natural : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : s) :-> (r : s)
(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)
forall a (s :: [*]).
(Unwrappabled Rational ~ (a, Natural)) =>
(Rational : 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)
forall a (s :: [*]).
(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)
forall a (s :: [*]).
(Unwrappabled Rational ~ (a, Natural)) =>
(Rational : 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)
forall a (s :: [*]).
(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 = (Rational : Rational : s) :-> (r : s)
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

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 (s :: [*]). (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 (s :: [*]). (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 (s :: [*]). (Rational : s) :-> (Rational : 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 (s :: [*]). (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 (s :: [*]). (Rational : s) :-> (Rational : 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 ((Rational : Natural : s) :-> (r : s))
-> ((r : s) :-> (r : s)) -> (Rational : Natural : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (r : s) :-> (r : s)
forall (s :: [*]). (r : s) :-> (r : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational
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 (s :: [*]). (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) :-> (r : s))
-> (NRational : Integer : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : s) :-> (r : s)
(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) :-> (r : s))
-> (NRational : Natural : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : s) :-> (r : s)
(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)
forall a (s :: [*]).
(Unwrappabled NRational ~ (a, Natural)) =>
(NRational : 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)
forall a (s :: [*]).
(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)
forall a (s :: [*]).
(Unwrappabled NRational ~ (a, Natural)) =>
(NRational : 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)
forall a (s :: [*]).
(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 = (NRational : NRational : s) :-> (r : s)
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

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 (s :: [*]). (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 (s :: [*]). (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 (s :: [*]). (NRational : s) :-> (NRational : 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 (s :: [*]). (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 (s :: [*]). (NRational : s) :-> (NRational : 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 ((NRational : Natural : s) :-> (r : s))
-> ((r : s) :-> (r : s)) -> (NRational : Natural : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (r : s) :-> (r : s)
forall (s :: [*]). (r : s) :-> (r : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational
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 (s :: [*]). (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 = (Rational : NRational : s) :-> (r : s)
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
instance (r ~ Rational) => ArithOpHs Mul NRational Rational r where
  evalArithOpHs :: forall (s :: [*]). (NRational : Rational : s) :-> (r : s)
evalArithOpHs = (NRational : Rational : s) :-> (r : s)
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
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 (s :: [*]). (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 (s :: [*]). (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

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

instance ArithOpHs Div Integer Integer (Maybe Rational) where
  evalArithOpHs :: forall (s :: [*]). (Integer : Integer : s) :-> (Maybe Rational : s)
evalArithOpHs = do
    forall (n :: Natural) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @2; ((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 : Integer : s) :-> (Integer : Integer : s)
(Integer : Integer : s)
:-> (UnaryArithResHs Neg Integer : 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 : s) :-> (Natural : s))
-> (Integer : Integer : s) :-> (Integer : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Integer : s) :-> (Natural : s)
(Integer : s) :-> (UnaryArithResHs Abs Integer : s)
forall n (s :: [*]).
UnaryArithOpHs Abs n =>
(n : s) :-> (UnaryArithResHs Abs n : s)
abs
    (Integer : Natural : s) :-> (Maybe Rational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural), KnownValue r) =>
(a : Natural : s) :-> (Maybe r : s)
mkRatReduce
instance ArithOpHs Div Natural Natural (Maybe NRational) where
  evalArithOpHs :: forall (s :: [*]).
(Natural : Natural : s) :-> (Maybe NRational : s)
evalArithOpHs = (Natural : Natural : s) :-> (Maybe NRational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural), KnownValue r) =>
(a : Natural : s) :-> (Maybe r : s)
mkRatReduce
instance ArithOpHs Div Integer Natural (Maybe Rational) where
  evalArithOpHs :: forall (s :: [*]). (Integer : Natural : s) :-> (Maybe Rational : s)
evalArithOpHs = (Integer : Natural : s) :-> (Maybe Rational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural), KnownValue r) =>
(a : Natural : s) :-> (Maybe r : s)
mkRatReduce
instance ArithOpHs Div Natural Integer (Maybe Rational) where
  evalArithOpHs :: forall (s :: [*]). (Natural : Integer : s) :-> (Maybe Rational : s)
evalArithOpHs = do
    forall (n :: Natural) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @2; ((Natural : Integer : s) :-> (Integer : Integer : s))
-> ((Natural : Integer : s) :-> (Integer : Integer : s))
-> (Integer : Natural : Integer : s) :-> (Integer : Integer : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Lt =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifLt0 (Natural : Integer : s) :-> (Integer : Integer : s)
(Natural : Integer : s)
:-> (UnaryArithResHs Neg Natural : Integer : s)
forall n (s :: [*]).
UnaryArithOpHs Neg n =>
(n : s) :-> (UnaryArithResHs Neg n : s)
neg (Natural : Integer : s) :-> (Integer : Integer : s)
forall i (s :: [*]).
ToIntegerArithOpHs i =>
(i : s) :-> (Integer : s)
int; ((Integer : s) :-> (Natural : s))
-> (Integer : Integer : s) :-> (Integer : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Integer : s) :-> (Natural : s)
(Integer : s) :-> (UnaryArithResHs Abs Integer : s)
forall n (s :: [*]).
UnaryArithOpHs Abs n =>
(n : s) :-> (UnaryArithResHs Abs n : s)
abs
    (Integer : Natural : s) :-> (Maybe Rational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural), KnownValue r) =>
(a : Natural : s) :-> (Maybe r : s)
mkRatReduce

mkRatReduce
  :: (LorentzRational r, Unwrappabled r ~ (a, Natural), KnownValue r)
  => a : Natural : s :-> Maybe r : s
mkRatReduce :: forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural), KnownValue r) =>
(a : Natural : s) :-> (Maybe r : s)
mkRatReduce = do (a : Natural : s) :-> ((a, Natural) : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair; ((a, Natural) : s) :-> (Maybe r : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural), KnownValue r) =>
((a, Natural) : s) :-> (Maybe r : s)
forall a (s :: [*]).
(Unwrappabled r ~ (a, Natural), KnownValue r) =>
((a, Natural) : s) :-> (Maybe r : s)
pairToRational; ((MapOpInpHs (Maybe r) : s) :-> (r : s))
-> (Maybe r : s) :-> (MapOpResHs (Maybe r) r : s)
forall c b (s :: [*]).
(MapOpHs c, IsoMapOpRes c b, KnownValue b, HasCallStack) =>
((MapOpInpHs c : s) :-> (b : s))
-> (c : s) :-> (MapOpResHs c b : s)
map (r : s) :-> (r : s)
(MapOpInpHs (Maybe r) : s) :-> (r : s)
forall (s :: [*]). (r : s) :-> (r : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
reduce

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)
forall a (s :: [*]).
(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)
forall a (s :: [*]).
(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)
forall a (s :: [*]).
(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)
forall a (s :: [*]).
(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)
forall a (s :: [*]).
(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)
forall a (s :: [*]).
(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 :: Natural) (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 :: Natural) (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)
forall a (s :: [*]).
(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 :: Natural) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @2
  (Natural : Natural : Natural : s)
:-> (Bool : Natural : Natural : s)
(Natural : Natural : Natural : s)
:-> (UnaryArithResHs Neq Natural : 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)
(Natural : Natural : Natural : s)
:-> (UnaryArithResHs Neq Natural : 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)
forall a (s :: [*]).
(Unwrappabled Rational ~ (a, Natural)) =>
(Rational : 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 :: Natural) (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz (ToPeano n) inp out a =>
inp :-> out
dug @2; (Integer : Natural : Integer : s)
:-> (Natural : Natural : Integer : s)
(Integer : Natural : Integer : s)
:-> (UnaryArithResHs Abs Integer : 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 :: Natural) (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)
forall a (s :: [*]).
(Unwrappabled Rational ~ (a, Natural)) =>
((a, Natural) : s) :-> (Rational : 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)
forall a (s :: [*]).
(Unwrappabled NRational ~ (a, Natural)) =>
(NRational : 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)
forall a (s :: [*]).
(Unwrappabled NRational ~ (a, Natural)) =>
(a : Natural : s) :-> (NRational : 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 :: Natural) (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 :: Natural) (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)
forall a (s :: [*]).
(Unwrappabled Rational ~ (a, Natural)) =>
(Rational : 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 :: Natural) (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)
(Integer
   : Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (UnaryArithResHs Neq Integer
       : 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 :: Natural) 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 :: Natural) (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 :: Natural) (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz (ToPeano n) inp out a =>
inp :-> out
dug @2
    forall (n :: Natural) 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 :: Natural) (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 :: Natural) 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 :: Natural) (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 :: Natural) (inp :: [*]) (out :: [*]) a.
ConstraintDIGLorentz (ToPeano n) inp out a =>
inp :-> out
dig @3; forall (n :: Natural) (inp :: [*]) (out :: [*]) a.
ConstraintDIGLorentz (ToPeano n) inp out a =>
inp :-> out
dig @4; forall (n :: Natural) (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz (ToPeano n) inp out a =>
inp :-> out
dug @2; forall (n :: Natural) (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)
(Integer
   : Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (UnaryArithResHs Neq Integer
       : 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 :: Natural) (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)
(Integer : s) :-> (UnaryArithResHs Neg 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)
:-> (UnaryArithResHs Abs Integer : Integer : s)
forall n (s :: [*]).
UnaryArithOpHs Abs n =>
(n : s) :-> (UnaryArithResHs Abs n : s)
abs; (UnaryArithResHs Abs Integer : Integer : s)
:-> (Integer : UnaryArithResHs Abs Integer : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
  (Integer : UnaryArithResHs Abs Integer : s)
:-> (Integer : Natural : s)
(Integer : UnaryArithResHs Abs Integer : s)
:-> (UnaryArithResHs Neg Integer : UnaryArithResHs Abs Integer : 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)
forall a (s :: [*]).
(Unwrappabled Rational ~ (a, Natural)) =>
((a, Natural) : s) :-> (Rational : 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)
(a3 : s1) :-> (Unwrappabled a3 : 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 :: Natural) 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)
((a6, Natural) : s2) :-> (a4 : s2)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
((a, Natural) : s) :-> (r : s)
forall a (s :: [*]).
(Unwrappabled a4 ~ (a, Natural)) =>
((a, Natural) : s) :-> (a4 : 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)
(a5 : s1) :-> (Unwrappabled a5 : 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)
(a6 : a3 : a2 : s1) :-> (Unwrappabled a6 : 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 :: Natural) (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 :: Natural) 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)
forall a (s :: [*]).
(Unwrappabled a7 ~ (a, Natural)) =>
((a, Natural) : s) :-> (a7 : 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)
forall a (s :: [*]).
(Unwrappabled r2 ~ (a, Natural)) =>
(r2 : 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)
forall a (s :: [*]).
(Unwrappabled r1 ~ (a, Natural)) =>
(r1 : 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)
forall a (s :: [*]).
(Unwrappabled r3 ~ (a, Natural)) =>
(a : Natural : s) :-> (r3 : 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)
forall a (s :: [*]).
(Unwrappabled Rational ~ (a, Natural)) =>
(Rational : 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)
(Integer : Natural : s)
:-> (UnaryArithResHs Neg 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)
forall a (s :: [*]).
(Unwrappabled Rational ~ (a, Natural)) =>
(a : Natural : s) :-> (Rational : s)
constructRational

mkRational_
  :: (forall s0. ErrInstr (("numerator" :! Integer, "denominator" :! Natural) : s0))
  -> Integer : Natural : s :-> Rational : s
mkRational_ :: forall (s :: [*]).
(forall (s0 :: [*]) (serr :: [*]).
 (("numerator" :! Integer, "denominator" :! Natural) : s0) :-> serr)
-> (Integer : Natural : s) :-> (Rational : s)
mkRational_ forall (s0 :: [*]) (serr :: [*]).
(("numerator" :! Integer, "denominator" :! Natural) : s0) :-> serr
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"
#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"
#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 :: [*]) (serr :: [*]).
(("numerator" :! Integer, "denominator" :! Natural) : s0) :-> serr
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)
forall a (s :: [*]).
(Unwrappabled Rational ~ (a, Natural)) =>
(a : Natural : s) :-> (Rational : 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."