{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE NoApplicativeDo #-}
{-# OPTIONS_GHC -Wno-unused-do-bind #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Lorentz.CustomArith.RationalArith
( Rational
, NRational
, oppositeRational
, gcdEuclid
, euclidExtendedNormalization
, reduce
, tripleMul
, mkRational
, (%!)
, mkNRational
, (%%!)
, LorentzRational
, 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
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
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
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
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
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."