{-# 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, ($), (++), (==))
import Text.Show qualified
import Lorentz.Annotation
import Lorentz.Arith
import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Constraints.Scopes
import Lorentz.CustomArith.Common
import Lorentz.Errors
import Lorentz.Instr
import Lorentz.Macro
import Lorentz.Rebound
import Morley.Michelson.Text
import Morley.Michelson.Typed
import Morley.Util.Named
import Morley.Util.Type
newtype Rational =
UnsafeRational (Integer, Natural)
deriving newtype (Rational -> Rational -> Bool
(Rational -> Rational -> Bool)
-> (Rational -> Rational -> Bool) -> Eq Rational
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Rational -> Rational -> Bool
$c/= :: Rational -> Rational -> Bool
== :: Rational -> Rational -> Bool
$c== :: Rational -> Rational -> Bool
Eq)
infixl 7 %!
(%!) :: Integer -> Natural -> Rational
%! :: Integer -> Natural -> Rational
(%!) Integer
x Natural
y = Either Text Rational -> Rational
forall a b. (HasCallStack, Buildable a) => Either a b -> b
unsafe (Either Text Rational -> Rational)
-> Either Text Rational -> Rational
forall a b. (a -> b) -> a -> b
$ (Integer, Natural) -> Either Text Rational
mkRational (Integer
x, Natural
y)
mkRational :: (Integer, Natural) -> Either Text Rational
mkRational :: (Integer, Natural) -> Either Text Rational
mkRational (Integer
x, Natural
y) = case Natural
y of
Natural
0 -> Text -> Either Text Rational
forall a b. a -> Either a b
Left (Text -> Either Text Rational) -> Text -> Either Text Rational
forall a b. (a -> b) -> a -> b
$ Text
"Attempt to construct Rational with zero denominator."
Natural
_ -> Rational -> Either Text Rational
forall a b. b -> Either a b
Right (Rational -> Either Text Rational)
-> Rational -> Either Text Rational
forall a b. (a -> b) -> a -> b
$ (Integer, Natural) -> Rational
UnsafeRational (Integer
x, Natural
y)
instance Show Rational where
show :: Rational -> String
show (UnsafeRational (Integer
a, Natural
b)) = Integer -> String
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show Integer
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" / " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show Natural
b
instance HasAnnotation Rational where
getAnnotation :: FollowEntrypointFlag -> Notes (ToT Rational)
getAnnotation FollowEntrypointFlag
_ = Notes (ToT Rational)
forall (t :: T). SingI t => Notes t
starNotes
instance IsoValue Rational where
type ToT Rational = 'TPair 'TInt 'TNat
toVal :: Rational -> Value (ToT Rational)
toVal (UnsafeRational (Integer
a, Natural
b)) = (Value' Instr 'TInt, Value' Instr 'TNat)
-> Value' Instr ('TPair 'TInt 'TNat)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Integer -> Value' Instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt Integer
a, Natural -> Value' Instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat Natural
b)
fromVal :: Value (ToT Rational) -> Rational
fromVal (VPair (VInt Integer
a, VNat Natural
b)) = (Integer, Natural) -> Rational
UnsafeRational (Integer
a, Natural
b)
instance Unwrappable Rational where
type Unwrappabled Rational = (Integer, Natural)
newtype NRational =
UnsafeNRational (Natural, Natural)
deriving newtype (NRational -> NRational -> Bool
(NRational -> NRational -> Bool)
-> (NRational -> NRational -> Bool) -> Eq NRational
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NRational -> NRational -> Bool
$c/= :: NRational -> NRational -> Bool
== :: NRational -> NRational -> Bool
$c== :: NRational -> NRational -> Bool
Eq)
mkNRational :: (Natural, Natural) -> Either Text NRational
mkNRational :: (Natural, Natural) -> Either Text NRational
mkNRational (Natural
x, Natural
y) = case Natural
y of
Natural
0 -> Text -> Either Text NRational
forall a b. a -> Either a b
Left Text
"Attempt to construct NRational with zero denominator."
Natural
_ -> NRational -> Either Text NRational
forall a b. b -> Either a b
Right (NRational -> Either Text NRational)
-> NRational -> Either Text NRational
forall a b. (a -> b) -> a -> b
$ (Natural, Natural) -> NRational
UnsafeNRational (Natural
x, Natural
y)
infixl 7 %%!
(%%!) :: Natural -> Natural -> NRational
%%! :: Natural -> Natural -> NRational
(%%!) Natural
x Natural
y = Either Text NRational -> NRational
forall a b. (HasCallStack, Buildable a) => Either a b -> b
unsafe (Either Text NRational -> NRational)
-> Either Text NRational -> NRational
forall a b. (a -> b) -> a -> b
$ (Natural, Natural) -> Either Text NRational
mkNRational (Natural
x, Natural
y)
instance Show NRational where
show :: NRational -> String
show (UnsafeNRational (Natural
a, Natural
b)) = Natural -> String
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show Natural
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" / " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show Natural
b
instance HasAnnotation NRational where
getAnnotation :: FollowEntrypointFlag -> Notes (ToT NRational)
getAnnotation FollowEntrypointFlag
_ = Notes (ToT NRational)
forall (t :: T). SingI t => Notes t
starNotes
instance IsoValue NRational where
type ToT NRational = 'TPair 'TNat 'TNat
toVal :: NRational -> Value (ToT NRational)
toVal (UnsafeNRational (Natural
a, Natural
b)) = (Value' Instr 'TNat, Value' Instr 'TNat)
-> Value' Instr ('TPair 'TNat 'TNat)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Natural -> Value' Instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat Natural
a, Natural -> Value' Instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat Natural
b)
fromVal :: Value (ToT NRational) -> NRational
fromVal (VPair (VNat Natural
a, VNat Natural
b)) = (Natural, Natural) -> NRational
UnsafeNRational (Natural
a, Natural
b)
instance Unwrappable NRational where
type Unwrappabled NRational = (Natural, Natural)
class Unwrappable r => LorentzRational r where
numerator :: Unwrappabled r ~ (a, Natural) => r : s :-> a : s
numerator = (r : s) :-> ((a, Natural) : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((r : s) :-> ((a, Natural) : s))
-> (((a, Natural) : s) :-> (a : s)) -> (r : s) :-> (a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, Natural) : s) :-> (a : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : s)
car
denominator :: Unwrappabled r ~ (a, Natural) => r : s :-> Natural : s
denominator = (r : s) :-> ((a, Natural) : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((r : s) :-> ((a, Natural) : s))
-> (((a, Natural) : s) :-> (Natural : s))
-> (r : s) :-> (Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, Natural) : s) :-> (Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (b : s)
cdr
deconstructRational :: Unwrappabled r ~ (a, Natural) => r : s :-> a : Natural : s
deconstructRational = (r : s) :-> ((a, Natural) : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((r : s) :-> ((a, Natural) : s))
-> (((a, Natural) : s) :-> (a : Natural : s))
-> (r : s) :-> (a : Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, Natural) : s) :-> (a : Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair
constructRational :: Unwrappabled r ~ (a, Natural) => a : Natural : s :-> r : s
constructRational = (a : Natural : s) :-> ((a, Natural) : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair ((a : Natural : s) :-> ((a, Natural) : s))
-> (((a, Natural) : s) :-> (r : s))
-> (a : Natural : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, Natural) : s) :-> (r : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
((a, Natural) : s) :-> (r : s)
uncheckedPairToRational
unsafePairToRational :: Unwrappabled r ~ (a, Natural) => (a, Natural) : s :-> r : s
unsafePairToRational = ((a, Natural) : s) :-> (a : Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair (((a, Natural) : s) :-> (a : Natural : s))
-> ((a : Natural : s) :-> (a : Natural : s))
-> ((a, Natural) : s) :-> (a : Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((Natural : s) :-> (Natural : s))
-> (a : Natural : s) :-> (a : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip ((Natural : s) :-> (Natural : Natural : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup ((Natural : s) :-> (Natural : Natural : s))
-> ((Natural : Natural : s) :-> (Natural : s))
-> (Natural : s) :-> (Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# MText -> (Natural : Natural : s) :-> (Natural : s)
forall a err (s :: [*]).
(IfCmp0Constraints a Neq, IsError err) =>
err -> (a : s) :-> s
assertNeq0 [mt|Attempt to construct rational with zero denominator|]) (((a, Natural) : s) :-> (a : Natural : s))
-> ((a : Natural : s) :-> ((a, Natural) : s))
-> ((a, Natural) : s) :-> ((a, Natural) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : Natural : s) :-> ((a, Natural) : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair (((a, Natural) : s) :-> ((a, Natural) : s))
-> (((a, Natural) : s) :-> (r : s))
-> ((a, Natural) : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, Natural) : s) :-> (r : s)
forall a (s :: [*]).
Unwrappable a =>
(Unwrappabled a : s) :-> (a : s)
unsafeCoerceWrap
uncheckedPairToRational :: Unwrappabled r ~ (a, Natural) => (a, Natural) : s :-> r : s
uncheckedPairToRational = ((a, Natural) : s) :-> (r : s)
forall a (s :: [*]).
Unwrappable a =>
(Unwrappabled a : s) :-> (a : s)
unsafeCoerceWrap
pairToRational :: (Unwrappabled r ~ (a, Natural), KnownValue r) => (a, Natural) : s :-> Maybe r : s
pairToRational = do
((a, Natural) : s) :-> (a : Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair; (a : Natural : s) :-> (Natural : a : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
(Natural : a : s) :-> (Natural : Natural : a : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup
((Natural : a : s) :-> (Maybe r : s))
-> ((Natural : a : s) :-> (Maybe r : s))
-> (Natural : Natural : a : s) :-> (Maybe r : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Eq' =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifEq0
do
forall (n :: Nat) (s :: [*]).
(SingIPeano n, RequireLongerOrSameLength (ToTs s) (ToPeano n),
Drop (ToPeano n) (ToTs s) ~ ToTs (Drop (ToPeano n) s)) =>
s :-> Drop (ToPeano n) s
dropN @2
s :-> (Maybe r : s)
forall a (s :: [*]). KnownValue a => s :-> (Maybe a : s)
none
do
(Natural : a : s) :-> (a : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
(a : Natural : s) :-> ((a, Natural) : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair
((a, Natural) : s) :-> (r : s)
forall a (s :: [*]).
Unwrappable a =>
(Unwrappabled a : s) :-> (a : s)
unsafeCoerceWrap
(r : s) :-> (Maybe r : s)
forall a (s :: [*]). (a : s) :-> (Maybe a : s)
some
oppositeRational :: r : s :-> r : s
reduce :: (KnownList s, KnownList (ToTs s)) => r : s :-> r : s
instance LorentzRational Rational where
oppositeRational :: forall (s :: [*]). (Rational : s) :-> (Rational : s)
oppositeRational = do
(Rational : s) :-> (Integer : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
(Integer : Natural : s) :-> (Integer : Integer : Natural : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup
((Integer : Natural : s) :-> (Integer : Integer : s))
-> ((Integer : Natural : s) :-> (Integer : Integer : s))
-> (Integer : Integer : Natural : s) :-> (Integer : Integer : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Lt =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifLt0 (((Natural : s) :-> (Integer : s))
-> (Integer : Natural : s) :-> (Integer : Integer : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Natural : s) :-> (Integer : s)
forall n (s :: [*]).
UnaryArithOpHs Neg n =>
(n : s) :-> (UnaryArithResHs Neg n : s)
neg) (((Natural : s) :-> (Integer : s))
-> (Integer : Natural : s) :-> (Integer : Integer : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Natural : s) :-> (Integer : s)
forall i (s :: [*]).
ToIntegerArithOpHs i =>
(i : s) :-> (Integer : s)
int)
(Integer : Integer : s) :-> (Natural : Integer : s)
forall n (s :: [*]).
UnaryArithOpHs Abs n =>
(n : s) :-> (UnaryArithResHs Abs n : s)
abs
(Natural : Integer : s) :-> (Integer : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
(Integer : Natural : s) :-> (Rational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational
reduce :: forall (s :: [*]).
(KnownList s, KnownList (ToTs s)) =>
(Rational : s) :-> (Rational : s)
reduce = (Rational : s) :-> (Rational : s)
forall (s :: [*]). (Rational : s) :-> (Rational : s)
reduceRationalHelper
instance LorentzRational NRational where
oppositeRational :: forall (s :: [*]). (NRational : s) :-> (NRational : s)
oppositeRational = do
(NRational : s) :-> (Natural : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
(Natural : Natural : s) :-> (Natural : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
(Natural : Natural : s) :-> (NRational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational
reduce :: forall (s :: [*]).
(KnownList s, KnownList (ToTs s)) =>
(NRational : s) :-> (NRational : s)
reduce = (NRational : s) :-> (NRational : s)
forall (s :: [*]). (NRational : s) :-> (NRational : s)
reduceNRationalHelper
instance (r ~ Rational) => ArithOpHs Add Rational Integer r where
evalArithOpHs :: forall (s :: [*]). (Rational : Integer : s) :-> (r : s)
evalArithOpHs = (Rational : Integer : s) :-> (Integer : Rational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((Rational : Integer : s) :-> (Integer : Rational : s))
-> ((Integer : Rational : s) :-> (r : s))
-> (Rational : Integer : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Rational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
instance (r ~ Rational) => ArithOpHs Add Integer Rational r where
evalArithOpHs :: forall (s :: [*]). (Integer : Rational : s) :-> (r : s)
evalArithOpHs = ((Integer : Integer : Natural : s) :-> (Integer : Natural : s))
-> (Integer : Rational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 b r (s1 :: [*]) (s2 :: [*]).
(b ~ Natural, NiceConstant a1, ArithOpHs Mul a2 a1 r,
Unwrappable a3, Unwrappabled a3 ~ (a5, a1),
Unwrappabled a4 ~ (a6, Natural), LorentzRational a4) =>
((r : a5 : a1 : s1) :-> (a6 : b : s2))
-> (a2 : a3 : s1) :-> (a4 : s2)
addSubHelper (Integer : Integer : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
instance (r ~ Rational) => ArithOpHs Add Rational Natural r where
evalArithOpHs :: forall (s :: [*]). (Rational : Natural : s) :-> (r : s)
evalArithOpHs = (Rational : Natural : s) :-> (Natural : Rational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((Rational : Natural : s) :-> (Natural : Rational : s))
-> ((Natural : Rational : s) :-> (r : s))
-> (Rational : Natural : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : Rational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
instance (r ~ Rational) => ArithOpHs Add Natural Rational r where
evalArithOpHs :: forall (s :: [*]). (Natural : Rational : s) :-> (r : s)
evalArithOpHs = ((Natural : Integer : Natural : s) :-> (Integer : Natural : s))
-> (Natural : Rational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 b r (s1 :: [*]) (s2 :: [*]).
(b ~ Natural, NiceConstant a1, ArithOpHs Mul a2 a1 r,
Unwrappable a3, Unwrappabled a3 ~ (a5, a1),
Unwrappabled a4 ~ (a6, Natural), LorentzRational a4) =>
((r : a5 : a1 : s1) :-> (a6 : b : s2))
-> (a2 : a3 : s1) :-> (a4 : s2)
addSubHelper (Natural : Integer : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
instance (r ~ Rational) => ArithOpHs Add Rational Rational r where
evalArithOpHs :: forall (s :: [*]). (Rational : Rational : s) :-> (r : s)
evalArithOpHs = ((Integer : Integer : Natural : Natural : s)
:-> (Integer : Natural : Natural : s))
-> (Rational : Rational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 a7 a8 r1 r2 r3 n m (s1 :: [*])
(s2 :: [*]).
(NiceConstant a1, NiceConstant a2, LorentzRational a7,
r3 ~ Natural, ArithOpHs Mul a1 a3 r1, ArithOpHs Mul a2 a4 r2,
ArithOpHs Mul n m r3, Unwrappable a5, Unwrappable a6,
Unwrappabled a7 ~ (a8, r3), Unwrappabled a5 ~ (a3, a2),
Unwrappabled a6 ~ (a4, a1)) =>
((r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2))
-> (a6 : a5 : s1) :-> (a7 : s2)
addSubRationalHelper (Integer : Integer : Natural : Natural : s)
:-> (Integer : Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
instance (r ~ Rational) => ArithOpHs Sub Rational Integer r where
evalArithOpHs :: forall (s :: [*]). (Rational : Integer : s) :-> (r : s)
evalArithOpHs = (Rational : Integer : s) :-> (Integer : Rational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((Rational : Integer : s) :-> (Integer : Rational : s))
-> ((Integer : Rational : s) :-> (Rational : s))
-> (Rational : Integer : s) :-> (Rational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Rational : s) :-> (Rational : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub ((Rational : Integer : s) :-> (Rational : s))
-> ((Rational : s) :-> (Rational : s))
-> (Rational : Integer : s) :-> (Rational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : s) :-> (Rational : s)
forall (s :: [*]). (Rational : s) :-> (Rational : s)
negRational
instance (r ~ Rational) => ArithOpHs Sub Integer Rational r where
evalArithOpHs :: forall (s :: [*]). (Integer : Rational : s) :-> (r : s)
evalArithOpHs = ((Integer : Integer : Natural : s) :-> (Integer : Natural : s))
-> (Integer : Rational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 b r (s1 :: [*]) (s2 :: [*]).
(b ~ Natural, NiceConstant a1, ArithOpHs Mul a2 a1 r,
Unwrappable a3, Unwrappabled a3 ~ (a5, a1),
Unwrappabled a4 ~ (a6, Natural), LorentzRational a4) =>
((r : a5 : a1 : s1) :-> (a6 : b : s2))
-> (a2 : a3 : s1) :-> (a4 : s2)
addSubHelper (Integer : Integer : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub
instance (r ~ Rational) => ArithOpHs Sub Rational Natural r where
evalArithOpHs :: forall (s :: [*]). (Rational : Natural : s) :-> (r : s)
evalArithOpHs = (Rational : Natural : s) :-> (Natural : Rational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((Rational : Natural : s) :-> (Natural : Rational : s))
-> ((Natural : Rational : s) :-> (Rational : s))
-> (Rational : Natural : s) :-> (Rational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : Rational : s) :-> (Rational : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub ((Rational : Natural : s) :-> (Rational : s))
-> ((Rational : s) :-> (Rational : s))
-> (Rational : Natural : s) :-> (Rational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : s) :-> (Rational : s)
forall (s :: [*]). (Rational : s) :-> (Rational : s)
negRational
instance (r ~ Rational) => ArithOpHs Sub Natural Rational r where
evalArithOpHs :: forall (s :: [*]). (Natural : Rational : s) :-> (r : s)
evalArithOpHs = ((Natural : Integer : Natural : s) :-> (Integer : Natural : s))
-> (Natural : Rational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 b r (s1 :: [*]) (s2 :: [*]).
(b ~ Natural, NiceConstant a1, ArithOpHs Mul a2 a1 r,
Unwrappable a3, Unwrappabled a3 ~ (a5, a1),
Unwrappabled a4 ~ (a6, Natural), LorentzRational a4) =>
((r : a5 : a1 : s1) :-> (a6 : b : s2))
-> (a2 : a3 : s1) :-> (a4 : s2)
addSubHelper (Natural : Integer : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub
instance (r ~ Rational) => ArithOpHs Sub Rational Rational r where
evalArithOpHs :: forall (s :: [*]). (Rational : Rational : s) :-> (r : s)
evalArithOpHs = ((Integer : Integer : Natural : Natural : s)
:-> (Integer : Natural : Natural : s))
-> (Rational : Rational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 a7 a8 r1 r2 r3 n m (s1 :: [*])
(s2 :: [*]).
(NiceConstant a1, NiceConstant a2, LorentzRational a7,
r3 ~ Natural, ArithOpHs Mul a1 a3 r1, ArithOpHs Mul a2 a4 r2,
ArithOpHs Mul n m r3, Unwrappable a5, Unwrappable a6,
Unwrappabled a7 ~ (a8, r3), Unwrappabled a5 ~ (a3, a2),
Unwrappabled a6 ~ (a4, a1)) =>
((r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2))
-> (a6 : a5 : s1) :-> (a7 : s2)
addSubRationalHelper (Integer : Integer : Natural : Natural : s)
:-> (Integer : Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub
instance (r ~ Rational) => ArithOpHs Mul Rational Integer r where
evalArithOpHs :: forall (s :: [*]). (Rational : Integer : s) :-> (r : s)
evalArithOpHs = (Rational : Integer : s) :-> (Integer : Rational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((Rational : Integer : s) :-> (Integer : Rational : s))
-> ((Integer : Rational : s) :-> (r : s))
-> (Rational : Integer : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Rational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ Rational) => ArithOpHs Mul Integer Rational r where
evalArithOpHs :: forall (s :: [*]). (Integer : Rational : s) :-> (r : s)
evalArithOpHs = ((Rational : s) :-> (Integer : Natural : s))
-> (Integer : Rational : s) :-> (Integer : Integer : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Rational : s) :-> (Integer : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational ((Integer : Rational : s) :-> (Integer : Integer : Natural : s))
-> ((Integer : Integer : Natural : s) :-> (Integer : Natural : s))
-> (Integer : Rational : s) :-> (Integer : Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Integer : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul ((Integer : Rational : s) :-> (Integer : Natural : s))
-> ((Integer : Natural : s) :-> (r : s))
-> (Integer : Rational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Natural : s) :-> (r : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational
instance (r ~ Rational) => ArithOpHs Mul Rational Natural r where
evalArithOpHs :: forall (s :: [*]). (Rational : Natural : s) :-> (r : s)
evalArithOpHs = (Rational : Natural : s) :-> (Natural : Rational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((Rational : Natural : s) :-> (Natural : Rational : s))
-> ((Natural : Rational : s) :-> (r : s))
-> (Rational : Natural : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : Rational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ Rational) => ArithOpHs Mul Natural Rational r where
evalArithOpHs :: forall (s :: [*]). (Natural : Rational : s) :-> (r : s)
evalArithOpHs = ((Rational : s) :-> (Integer : Natural : s))
-> (Natural : Rational : s) :-> (Natural : Integer : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Rational : s) :-> (Integer : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational ((Natural : Rational : s) :-> (Natural : Integer : Natural : s))
-> ((Natural : Integer : Natural : s) :-> (Integer : Natural : s))
-> (Natural : Rational : s) :-> (Integer : Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : Integer : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul ((Natural : Rational : s) :-> (Integer : Natural : s))
-> ((Integer : Natural : s) :-> (r : s))
-> (Natural : Rational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Natural : s) :-> (r : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational
instance (r ~ Rational) => ArithOpHs Mul Rational Rational r where
evalArithOpHs :: forall (s :: [*]). (Rational : Rational : s) :-> (r : s)
evalArithOpHs = forall r1 r2 r3 a b c (s :: [*]).
(LorentzRational r1, LorentzRational r2, LorentzRational r3,
Unwrappabled r1 ~ (a, Natural), Unwrappabled r2 ~ (b, Natural),
Unwrappabled r3 ~ (c, Natural), ArithOpHs Mul a b c) =>
(r1 : r2 : s) :-> (r3 : s)
mulRationalHelper @Rational @Rational @Rational
instance (r ~ Rational) => ArithOpHs Div Integer Rational r where
evalArithOpHs :: forall (s :: [*]). (Integer : Rational : s) :-> (r : s)
evalArithOpHs = ((Rational : s) :-> (Rational : s))
-> (Integer : Rational : s) :-> (Integer : Rational : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Rational : s) :-> (Rational : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((Integer : Rational : s) :-> (Integer : Rational : s))
-> ((Integer : Rational : s) :-> (r : s))
-> (Integer : Rational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Rational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ Rational) => ArithOpHs Div Natural Rational r where
evalArithOpHs :: forall (s :: [*]). (Natural : Rational : s) :-> (r : s)
evalArithOpHs = ((Rational : s) :-> (Rational : s))
-> (Natural : Rational : s) :-> (Natural : Rational : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Rational : s) :-> (Rational : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((Natural : Rational : s) :-> (Natural : Rational : s))
-> ((Natural : Rational : s) :-> (r : s))
-> (Natural : Rational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : Rational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ Rational) => ArithOpHs Div Rational Integer r where
evalArithOpHs :: forall (s :: [*]). (Rational : Integer : s) :-> (r : s)
evalArithOpHs = (Rational : Integer : s) :-> (Rational : Integer : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((Rational : Integer : s) :-> (Rational : Integer : s))
-> ((Rational : Integer : s) :-> (r : s))
-> (Rational : Integer : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : Integer : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul ((Rational : Integer : s) :-> (r : s))
-> ((r : s) :-> (r : s)) -> (Rational : Integer : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (r : s) :-> (r : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational
instance (r ~ Rational) => ArithOpHs Div Rational Natural r where
evalArithOpHs :: forall (s :: [*]). (Rational : Natural : s) :-> (r : s)
evalArithOpHs = (Rational : Natural : s) :-> (Rational : Natural : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((Rational : Natural : s) :-> (Rational : Natural : s))
-> ((Rational : Natural : s) :-> (r : s))
-> (Rational : Natural : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : Natural : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ Rational) => ArithOpHs Div Rational Rational r where
evalArithOpHs :: forall (s :: [*]). (Rational : Rational : s) :-> (r : s)
evalArithOpHs = ((Rational : s) :-> (Rational : s))
-> (Rational : Rational : s) :-> (Rational : Rational : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Rational : s) :-> (Rational : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((Rational : Rational : s) :-> (Rational : Rational : s))
-> ((Rational : Rational : s) :-> (r : s))
-> (Rational : Rational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : Rational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ Rational) => ArithOpHs Add NRational Integer r where
evalArithOpHs :: forall (s :: [*]). (NRational : Integer : s) :-> (r : s)
evalArithOpHs = (NRational : Integer : s) :-> (Integer : NRational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((NRational : Integer : s) :-> (Integer : NRational : s))
-> ((Integer : NRational : s) :-> (r : s))
-> (NRational : Integer : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : NRational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
instance (r ~ Rational) => ArithOpHs Add Integer NRational r where
evalArithOpHs :: forall (s :: [*]). (Integer : NRational : s) :-> (r : s)
evalArithOpHs = ((Integer : Natural : Natural : s) :-> (Integer : Natural : s))
-> (Integer : NRational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 b r (s1 :: [*]) (s2 :: [*]).
(b ~ Natural, NiceConstant a1, ArithOpHs Mul a2 a1 r,
Unwrappable a3, Unwrappabled a3 ~ (a5, a1),
Unwrappabled a4 ~ (a6, Natural), LorentzRational a4) =>
((r : a5 : a1 : s1) :-> (a6 : b : s2))
-> (a2 : a3 : s1) :-> (a4 : s2)
addSubHelper (Integer : Natural : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
instance (r ~ NRational) => ArithOpHs Add NRational Natural r where
evalArithOpHs :: forall (s :: [*]). (NRational : Natural : s) :-> (r : s)
evalArithOpHs = (NRational : Natural : s) :-> (Natural : NRational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((NRational : Natural : s) :-> (Natural : NRational : s))
-> ((Natural : NRational : s) :-> (r : s))
-> (NRational : Natural : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : NRational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
instance (r ~ NRational) => ArithOpHs Add Natural NRational r where
evalArithOpHs :: forall (s :: [*]). (Natural : NRational : s) :-> (r : s)
evalArithOpHs = ((Natural : Natural : Natural : s) :-> (Natural : Natural : s))
-> (Natural : NRational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 b r (s1 :: [*]) (s2 :: [*]).
(b ~ Natural, NiceConstant a1, ArithOpHs Mul a2 a1 r,
Unwrappable a3, Unwrappabled a3 ~ (a5, a1),
Unwrappabled a4 ~ (a6, Natural), LorentzRational a4) =>
((r : a5 : a1 : s1) :-> (a6 : b : s2))
-> (a2 : a3 : s1) :-> (a4 : s2)
addSubHelper (Natural : Natural : Natural : s) :-> (Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
instance (r ~ NRational) => ArithOpHs Add NRational NRational r where
evalArithOpHs :: forall (s :: [*]). (NRational : NRational : s) :-> (r : s)
evalArithOpHs = ((Natural : Natural : Natural : Natural : s)
:-> (Natural : Natural : Natural : s))
-> (NRational : NRational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 a7 a8 r1 r2 r3 n m (s1 :: [*])
(s2 :: [*]).
(NiceConstant a1, NiceConstant a2, LorentzRational a7,
r3 ~ Natural, ArithOpHs Mul a1 a3 r1, ArithOpHs Mul a2 a4 r2,
ArithOpHs Mul n m r3, Unwrappable a5, Unwrappable a6,
Unwrappabled a7 ~ (a8, r3), Unwrappabled a5 ~ (a3, a2),
Unwrappabled a6 ~ (a4, a1)) =>
((r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2))
-> (a6 : a5 : s1) :-> (a7 : s2)
addSubRationalHelper (Natural : Natural : Natural : Natural : s)
:-> (Natural : Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
instance (r ~ Rational) => ArithOpHs Sub NRational Integer r where
evalArithOpHs :: forall (s :: [*]). (NRational : Integer : s) :-> (r : s)
evalArithOpHs = (NRational : Integer : s) :-> (Integer : NRational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((NRational : Integer : s) :-> (Integer : NRational : s))
-> ((Integer : NRational : s) :-> (Rational : s))
-> (NRational : Integer : s) :-> (Rational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : NRational : s) :-> (Rational : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub ((NRational : Integer : s) :-> (Rational : s))
-> ((Rational : s) :-> (Rational : s))
-> (NRational : Integer : s) :-> (Rational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : s) :-> (Rational : s)
forall (s :: [*]). (Rational : s) :-> (Rational : s)
negRational
instance (r ~ Rational) => ArithOpHs Sub Integer NRational r where
evalArithOpHs :: forall (s :: [*]). (Integer : NRational : s) :-> (r : s)
evalArithOpHs = ((Integer : Natural : Natural : s) :-> (Integer : Natural : s))
-> (Integer : NRational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 b r (s1 :: [*]) (s2 :: [*]).
(b ~ Natural, NiceConstant a1, ArithOpHs Mul a2 a1 r,
Unwrappable a3, Unwrappabled a3 ~ (a5, a1),
Unwrappabled a4 ~ (a6, Natural), LorentzRational a4) =>
((r : a5 : a1 : s1) :-> (a6 : b : s2))
-> (a2 : a3 : s1) :-> (a4 : s2)
addSubHelper (Integer : Natural : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub
instance (r ~ Rational) => ArithOpHs Sub NRational Natural r where
evalArithOpHs :: forall (s :: [*]). (NRational : Natural : s) :-> (r : s)
evalArithOpHs = (NRational : Natural : s) :-> (Natural : NRational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((NRational : Natural : s) :-> (Natural : NRational : s))
-> ((Natural : NRational : s) :-> (Rational : s))
-> (NRational : Natural : s) :-> (Rational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : NRational : s) :-> (Rational : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub ((NRational : Natural : s) :-> (Rational : s))
-> ((Rational : s) :-> (Rational : s))
-> (NRational : Natural : s) :-> (Rational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : s) :-> (Rational : s)
forall (s :: [*]). (Rational : s) :-> (Rational : s)
negRational
instance (r ~ Rational) => ArithOpHs Sub Natural NRational r where
evalArithOpHs :: forall (s :: [*]). (Natural : NRational : s) :-> (r : s)
evalArithOpHs = ((Natural : Natural : Natural : s) :-> (Integer : Natural : s))
-> (Natural : NRational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 b r (s1 :: [*]) (s2 :: [*]).
(b ~ Natural, NiceConstant a1, ArithOpHs Mul a2 a1 r,
Unwrappable a3, Unwrappabled a3 ~ (a5, a1),
Unwrappabled a4 ~ (a6, Natural), LorentzRational a4) =>
((r : a5 : a1 : s1) :-> (a6 : b : s2))
-> (a2 : a3 : s1) :-> (a4 : s2)
addSubHelper (Natural : Natural : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub
instance (r ~ Rational) => ArithOpHs Sub NRational NRational r where
evalArithOpHs :: forall (s :: [*]). (NRational : NRational : s) :-> (r : s)
evalArithOpHs = ((Natural : Natural : Natural : Natural : s)
:-> (Integer : Natural : Natural : s))
-> (NRational : NRational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 a7 a8 r1 r2 r3 n m (s1 :: [*])
(s2 :: [*]).
(NiceConstant a1, NiceConstant a2, LorentzRational a7,
r3 ~ Natural, ArithOpHs Mul a1 a3 r1, ArithOpHs Mul a2 a4 r2,
ArithOpHs Mul n m r3, Unwrappable a5, Unwrappable a6,
Unwrappabled a7 ~ (a8, r3), Unwrappabled a5 ~ (a3, a2),
Unwrappabled a6 ~ (a4, a1)) =>
((r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2))
-> (a6 : a5 : s1) :-> (a7 : s2)
addSubRationalHelper (Natural : Natural : Natural : Natural : s)
:-> (Integer : Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub
instance (r ~ Rational) => ArithOpHs Mul NRational Integer r where
evalArithOpHs :: forall (s :: [*]). (NRational : Integer : s) :-> (r : s)
evalArithOpHs = (NRational : Integer : s) :-> (Integer : NRational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((NRational : Integer : s) :-> (Integer : NRational : s))
-> ((Integer : NRational : s) :-> (r : s))
-> (NRational : Integer : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : NRational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ Rational) => ArithOpHs Mul Integer NRational r where
evalArithOpHs :: forall (s :: [*]). (Integer : NRational : s) :-> (r : s)
evalArithOpHs = ((NRational : s) :-> (Natural : Natural : s))
-> (Integer : NRational : s) :-> (Integer : Natural : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (NRational : s) :-> (Natural : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational ((Integer : NRational : s) :-> (Integer : Natural : Natural : s))
-> ((Integer : Natural : Natural : s) :-> (Integer : Natural : s))
-> (Integer : NRational : s) :-> (Integer : Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Natural : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul ((Integer : NRational : s) :-> (Integer : Natural : s))
-> ((Integer : Natural : s) :-> (r : s))
-> (Integer : NRational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Natural : s) :-> (r : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational
instance (r ~ NRational) => ArithOpHs Mul NRational Natural r where
evalArithOpHs :: forall (s :: [*]). (NRational : Natural : s) :-> (r : s)
evalArithOpHs = (NRational : Natural : s) :-> (Natural : NRational : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((NRational : Natural : s) :-> (Natural : NRational : s))
-> ((Natural : NRational : s) :-> (r : s))
-> (NRational : Natural : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : NRational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ NRational) => ArithOpHs Mul Natural NRational r where
evalArithOpHs :: forall (s :: [*]). (Natural : NRational : s) :-> (r : s)
evalArithOpHs = ((NRational : s) :-> (Natural : Natural : s))
-> (Natural : NRational : s) :-> (Natural : Natural : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (NRational : s) :-> (Natural : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational ((Natural : NRational : s) :-> (Natural : Natural : Natural : s))
-> ((Natural : Natural : Natural : s) :-> (Natural : Natural : s))
-> (Natural : NRational : s) :-> (Natural : Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : Natural : Natural : s) :-> (Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul ((Natural : NRational : s) :-> (Natural : Natural : s))
-> ((Natural : Natural : s) :-> (r : s))
-> (Natural : NRational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : Natural : s) :-> (r : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational
instance (r ~ NRational) => ArithOpHs Mul NRational NRational r where
evalArithOpHs :: forall (s :: [*]). (NRational : NRational : s) :-> (r : s)
evalArithOpHs = forall r1 r2 r3 a b c (s :: [*]).
(LorentzRational r1, LorentzRational r2, LorentzRational r3,
Unwrappabled r1 ~ (a, Natural), Unwrappabled r2 ~ (b, Natural),
Unwrappabled r3 ~ (c, Natural), ArithOpHs Mul a b c) =>
(r1 : r2 : s) :-> (r3 : s)
mulRationalHelper @NRational @NRational @NRational
instance (r ~ Rational) => ArithOpHs Div Integer NRational r where
evalArithOpHs :: forall (s :: [*]). (Integer : NRational : s) :-> (r : s)
evalArithOpHs = ((NRational : s) :-> (NRational : s))
-> (Integer : NRational : s) :-> (Integer : NRational : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (NRational : s) :-> (NRational : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((Integer : NRational : s) :-> (Integer : NRational : s))
-> ((Integer : NRational : s) :-> (r : s))
-> (Integer : NRational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : NRational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ NRational) => ArithOpHs Div Natural NRational r where
evalArithOpHs :: forall (s :: [*]). (Natural : NRational : s) :-> (r : s)
evalArithOpHs = ((NRational : s) :-> (NRational : s))
-> (Natural : NRational : s) :-> (Natural : NRational : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (NRational : s) :-> (NRational : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((Natural : NRational : s) :-> (Natural : NRational : s))
-> ((Natural : NRational : s) :-> (r : s))
-> (Natural : NRational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : NRational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ Rational) => ArithOpHs Div NRational Integer r where
evalArithOpHs :: forall (s :: [*]). (NRational : Integer : s) :-> (r : s)
evalArithOpHs = (NRational : Integer : s) :-> (NRational : Integer : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((NRational : Integer : s) :-> (NRational : Integer : s))
-> ((NRational : Integer : s) :-> (r : s))
-> (NRational : Integer : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (NRational : Integer : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul ((NRational : Integer : s) :-> (r : s))
-> ((r : s) :-> (r : s)) -> (NRational : Integer : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (r : s) :-> (r : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational
instance (r ~ NRational) => ArithOpHs Div NRational Natural r where
evalArithOpHs :: forall (s :: [*]). (NRational : Natural : s) :-> (r : s)
evalArithOpHs = (NRational : Natural : s) :-> (NRational : Natural : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((NRational : Natural : s) :-> (NRational : Natural : s))
-> ((NRational : Natural : s) :-> (r : s))
-> (NRational : Natural : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (NRational : Natural : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ NRational) => ArithOpHs Div NRational NRational r where
evalArithOpHs :: forall (s :: [*]). (NRational : NRational : s) :-> (r : s)
evalArithOpHs = ((NRational : s) :-> (NRational : s))
-> (NRational : NRational : s) :-> (NRational : NRational : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (NRational : s) :-> (NRational : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((NRational : NRational : s) :-> (NRational : NRational : s))
-> ((NRational : NRational : s) :-> (r : s))
-> (NRational : NRational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (NRational : NRational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ Rational) => ArithOpHs Add Rational NRational r where
evalArithOpHs :: forall (s :: [*]). (Rational : NRational : s) :-> (r : s)
evalArithOpHs = ((Integer : Natural : Natural : Natural : s)
:-> (Integer : Natural : Natural : s))
-> (Rational : NRational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 a7 a8 r1 r2 r3 n m (s1 :: [*])
(s2 :: [*]).
(NiceConstant a1, NiceConstant a2, LorentzRational a7,
r3 ~ Natural, ArithOpHs Mul a1 a3 r1, ArithOpHs Mul a2 a4 r2,
ArithOpHs Mul n m r3, Unwrappable a5, Unwrappable a6,
Unwrappabled a7 ~ (a8, r3), Unwrappabled a5 ~ (a3, a2),
Unwrappabled a6 ~ (a4, a1)) =>
((r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2))
-> (a6 : a5 : s1) :-> (a7 : s2)
addSubRationalHelper (Integer : Natural : Natural : Natural : s)
:-> (Integer : Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
instance (r ~ Rational) => ArithOpHs Add NRational Rational r where
evalArithOpHs :: forall (s :: [*]). (NRational : Rational : s) :-> (r : s)
evalArithOpHs = ((Natural : Integer : Natural : Natural : s)
:-> (Integer : Natural : Natural : s))
-> (NRational : Rational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 a7 a8 r1 r2 r3 n m (s1 :: [*])
(s2 :: [*]).
(NiceConstant a1, NiceConstant a2, LorentzRational a7,
r3 ~ Natural, ArithOpHs Mul a1 a3 r1, ArithOpHs Mul a2 a4 r2,
ArithOpHs Mul n m r3, Unwrappable a5, Unwrappable a6,
Unwrappabled a7 ~ (a8, r3), Unwrappabled a5 ~ (a3, a2),
Unwrappabled a6 ~ (a4, a1)) =>
((r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2))
-> (a6 : a5 : s1) :-> (a7 : s2)
addSubRationalHelper (Natural : Integer : Natural : Natural : s)
:-> (Integer : Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
instance (r ~ Rational) => ArithOpHs Sub Rational NRational r where
evalArithOpHs :: forall (s :: [*]). (Rational : NRational : s) :-> (r : s)
evalArithOpHs = ((Integer : Natural : Natural : Natural : s)
:-> (Integer : Natural : Natural : s))
-> (Rational : NRational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 a7 a8 r1 r2 r3 n m (s1 :: [*])
(s2 :: [*]).
(NiceConstant a1, NiceConstant a2, LorentzRational a7,
r3 ~ Natural, ArithOpHs Mul a1 a3 r1, ArithOpHs Mul a2 a4 r2,
ArithOpHs Mul n m r3, Unwrappable a5, Unwrappable a6,
Unwrappabled a7 ~ (a8, r3), Unwrappabled a5 ~ (a3, a2),
Unwrappabled a6 ~ (a4, a1)) =>
((r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2))
-> (a6 : a5 : s1) :-> (a7 : s2)
addSubRationalHelper (Integer : Natural : Natural : Natural : s)
:-> (Integer : Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub
instance (r ~ Rational) => ArithOpHs Sub NRational Rational r where
evalArithOpHs :: forall (s :: [*]). (NRational : Rational : s) :-> (r : s)
evalArithOpHs = ((Natural : Integer : Natural : Natural : s)
:-> (Integer : Natural : Natural : s))
-> (NRational : Rational : s) :-> (r : s)
forall a1 a2 a3 a4 a5 a6 a7 a8 r1 r2 r3 n m (s1 :: [*])
(s2 :: [*]).
(NiceConstant a1, NiceConstant a2, LorentzRational a7,
r3 ~ Natural, ArithOpHs Mul a1 a3 r1, ArithOpHs Mul a2 a4 r2,
ArithOpHs Mul n m r3, Unwrappable a5, Unwrappable a6,
Unwrappabled a7 ~ (a8, r3), Unwrappabled a5 ~ (a3, a2),
Unwrappabled a6 ~ (a4, a1)) =>
((r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2))
-> (a6 : a5 : s1) :-> (a7 : s2)
addSubRationalHelper (Natural : Integer : Natural : Natural : s)
:-> (Integer : Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub
instance (r ~ Rational) => ArithOpHs Mul Rational NRational r where
evalArithOpHs :: forall (s :: [*]). (Rational : NRational : s) :-> (r : s)
evalArithOpHs = forall r1 r2 r3 a b c (s :: [*]).
(LorentzRational r1, LorentzRational r2, LorentzRational r3,
Unwrappabled r1 ~ (a, Natural), Unwrappabled r2 ~ (b, Natural),
Unwrappabled r3 ~ (c, Natural), ArithOpHs Mul a b c) =>
(r1 : r2 : s) :-> (r3 : s)
mulRationalHelper @Rational @NRational @Rational
instance (r ~ Rational) => ArithOpHs Mul NRational Rational r where
evalArithOpHs :: forall (s :: [*]). (NRational : Rational : s) :-> (r : s)
evalArithOpHs = forall r1 r2 r3 a b c (s :: [*]).
(LorentzRational r1, LorentzRational r2, LorentzRational r3,
Unwrappabled r1 ~ (a, Natural), Unwrappabled r2 ~ (b, Natural),
Unwrappabled r3 ~ (c, Natural), ArithOpHs Mul a b c) =>
(r1 : r2 : s) :-> (r3 : s)
mulRationalHelper @NRational @Rational @Rational
instance (r ~ Rational) => ArithOpHs Div Rational NRational r where
evalArithOpHs :: forall (s :: [*]). (Rational : NRational : s) :-> (r : s)
evalArithOpHs = ((NRational : s) :-> (NRational : s))
-> (Rational : NRational : s) :-> (Rational : NRational : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (NRational : s) :-> (NRational : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((Rational : NRational : s) :-> (Rational : NRational : s))
-> ((Rational : NRational : s) :-> (r : s))
-> (Rational : NRational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : NRational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance (r ~ Rational) => ArithOpHs Div NRational Rational r where
evalArithOpHs :: forall (s :: [*]). (NRational : Rational : s) :-> (r : s)
evalArithOpHs = ((Rational : s) :-> (Rational : s))
-> (NRational : Rational : s) :-> (NRational : Rational : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Rational : s) :-> (Rational : s)
forall r (s :: [*]). LorentzRational r => (r : s) :-> (r : s)
oppositeRational ((NRational : Rational : s) :-> (NRational : Rational : s))
-> ((NRational : Rational : s) :-> (r : s))
-> (NRational : Rational : s) :-> (r : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (NRational : Rational : s) :-> (r : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
instance {-# OVERLAPPABLE #-} ( LorentzRational r
, Unwrappabled r ~ (a, Natural)
, ArithOpHs EDiv a Natural (Maybe (a, Natural))
, ArithOpHs Add a Natural a
, ArithOpHs Add Natural a a
) => LorentzRounding r a where
round_ :: forall (s :: [*]). (r : s) :-> (a : s)
round_ = do
(r : s) :-> (a : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational; ((Natural : s) :-> (Natural : Natural : s))
-> (a : Natural : s) :-> (a : Natural : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Natural : s) :-> (Natural : Natural : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup
forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv @a @Natural @(Maybe (a, Natural)); Impossible "Division by zero impossible here"
-> (Maybe (a, Natural) : Natural : s)
:-> ((a, Natural) : Natural : s)
forall err a (s :: [*]).
IsError err =>
err -> (Maybe a : s) :-> (a : s)
assertSome (forall (reason :: Symbol). HasCallStack => Impossible reason
Impossible @"Division by zero impossible here")
((a, Natural) : Natural : s) :-> (a : Natural : Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair
((Natural : Natural : s) :-> (Natural : s))
-> (a : Natural : Natural : s) :-> (a : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip do
Natural
-> (Natural : Natural : s) :-> (Natural : Natural : Natural : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Natural
2 :: Natural)
(Natural : Natural : Natural : s) :-> (Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
(s :-> (Natural : s))
-> (s :-> (Natural : s))
-> (Natural : Natural : s) :-> (Natural : s)
forall a (s :: [*]) (s' :: [*]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a : a : s) :-> s'
ifGt (Natural -> s :-> (Natural : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Natural
1 :: Natural)) (Natural -> s :-> (Natural : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Natural
0 :: Natural))
(a : Natural : s) :-> (a : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
ceil_ :: forall (s :: [*]). (r : s) :-> (a : s)
ceil_ = do
(r : s) :-> (a : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv @a @Natural @(Maybe (a, Natural)); Impossible "Division by zero impossible here"
-> (Maybe (a, Natural) : s) :-> ((a, Natural) : s)
forall err a (s :: [*]).
IsError err =>
err -> (Maybe a : s) :-> (a : s)
assertSome (forall (reason :: Symbol). HasCallStack => Impossible reason
Impossible @"Division by zero impossible here")
((a, Natural) : s) :-> (a : Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair
(a : Natural : s) :-> (Natural : a : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
((a : s) :-> (a : s))
-> ((a : s) :-> (a : s)) -> (Natural : a : s) :-> (a : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Eq' =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifEq0 (a : s) :-> (a : s)
forall (s :: [*]). s :-> s
nop (((a : s) :-> (a : s)) -> (Natural : a : s) :-> (a : s))
-> ((a : s) :-> (a : s)) -> (Natural : a : s) :-> (a : s)
forall a b. (a -> b) -> a -> b
$ do
Natural -> (a : s) :-> (Natural : a : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Natural
1 :: Natural)
(Natural : a : s) :-> (a : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
floor_ :: forall (s :: [*]). (r : s) :-> (a : s)
floor_ = do
(r : s) :-> (a : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv @a @Natural @(Maybe (a, Natural)); Impossible "Division by zero impossible here"
-> (Maybe (a, Natural) : s) :-> ((a, Natural) : s)
forall err a (s :: [*]).
IsError err =>
err -> (Maybe a : s) :-> (a : s)
assertSome (forall (reason :: Symbol). HasCallStack => Impossible reason
Impossible @"Division by zero impossible here")
((a, Natural) : s) :-> (a : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : s)
car
tripleMul :: forall r a s. (ArithOpHs Mul a a a, Unwrappabled r ~ (a, Natural), LorentzRational r) => r : r : r : s :-> r : s
tripleMul :: forall r a (s :: [*]).
(ArithOpHs Mul a a a, Unwrappabled r ~ (a, Natural),
LorentzRational r) =>
(r : r : r : s) :-> (r : s)
tripleMul = do
((r : r : s) :-> (a : Natural : a : Natural : s))
-> (r : r : r : s) :-> (r : a : Natural : a : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip do
((r : s) :-> (a : Natural : s))
-> (r : r : s) :-> (r : a : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (r : s) :-> (a : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
(r : a : Natural : s) :-> (a : Natural : a : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
(r : a : Natural : a : Natural : s)
:-> (a : Natural : a : Natural : a : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
((Natural : a : Natural : a : Natural : s)
:-> (a : Natural : Natural : a : Natural : s))
-> (a : Natural : a : Natural : a : Natural : s)
:-> (a : a : Natural : Natural : a : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip ((Natural : a : Natural : a : Natural : s)
:-> (a : Natural : Natural : a : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap)
forall (n :: Nat) (inp :: [*]) (out :: [*]) (s :: [*]) (s' :: [*]).
ConstraintDIPNLorentz (ToPeano n) inp out s s' =>
(s :-> s') -> inp :-> out
dipN @3 ((Natural : a : Natural : s) :-> (a : Natural : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap)
forall (n :: Nat) (inp :: [*]) (out :: [*]) (s :: [*]) (s' :: [*]).
ConstraintDIPNLorentz (ToPeano n) inp out s s' =>
(s :-> s') -> inp :-> out
dipN @2 ((Natural : a : Natural : Natural : s)
:-> (a : Natural : Natural : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul @a @a @a; forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul @a @a @a
((Natural : Natural : Natural : s) :-> (Natural : s))
-> (a : Natural : Natural : Natural : s) :-> (a : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (do (Natural : Natural : Natural : s) :-> (Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul; (Natural : Natural : s) :-> (Natural : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul)
(a : Natural : s) :-> (r : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational
gcdEuclid :: Natural : Natural : s :-> Natural : s
gcdEuclid :: forall (s :: [*]). (Natural : Natural : s) :-> (Natural : s)
gcdEuclid = do
(Natural : Natural : s)
:-> (Natural : Natural : Natural : Natural : s)
forall a b (s :: [*]).
(Dupable a, Dupable b) =>
(a : b : s) :-> (a : b : a : b : s)
dupTop2
((Natural : Natural : s) :-> (Natural : Natural : s))
-> ((Natural : Natural : s) :-> (Natural : Natural : s))
-> (Natural : Natural : Natural : Natural : s)
:-> (Natural : Natural : s)
forall a (s :: [*]) (s' :: [*]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a : a : s) :-> s'
ifLt (Natural : Natural : s) :-> (Natural : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap (Natural : Natural : s) :-> (Natural : Natural : s)
forall (s :: [*]). s :-> s
nop
forall (n :: Nat) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @2
(Natural : Natural : Natural : s)
:-> (Bool : Natural : Natural : s)
forall n (s :: [*]).
UnaryArithOpHs Neq n =>
(n : s) :-> (UnaryArithResHs Neq n : s)
neq0
((Natural : Natural : s) :-> (Bool : Natural : Natural : s))
-> (Bool : Natural : Natural : s) :-> (Natural : Natural : s)
forall (s :: [*]). (s :-> (Bool : s)) -> (Bool : s) :-> s
loop do
((Natural : s) :-> (Natural : Natural : s))
-> (Natural : Natural : s) :-> (Natural : Natural : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Natural : s) :-> (Natural : Natural : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup
(Natural : Natural : Natural : s)
:-> (Maybe (Natural, Natural) : Natural : s)
forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv
Impossible "Division by zero impossible here"
-> (Maybe (Natural, Natural) : Natural : s)
:-> ((Natural, Natural) : Natural : s)
forall err a (s :: [*]).
IsError err =>
err -> (Maybe a : s) :-> (a : s)
assertSome (forall (reason :: Symbol). HasCallStack => Impossible reason
Impossible @"Division by zero impossible here")
((Natural, Natural) : Natural : s) :-> (Natural : Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (b : s)
cdr
(Natural : Natural : s) :-> (Natural : Natural : Natural : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup
(Natural : Natural : Natural : s)
:-> (Bool : Natural : Natural : s)
forall n (s :: [*]).
UnaryArithOpHs Neq n =>
(n : s) :-> (UnaryArithResHs Neq n : s)
neq0
((Natural : Natural : s) :-> (Natural : Natural : s))
-> (Bool : Natural : Natural : s)
:-> (Bool : Natural : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Natural : Natural : s) :-> (Natural : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
((Natural : s) :-> s) -> (Natural : Natural : s) :-> (Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Natural : s) :-> s
forall a (s :: [*]). (a : s) :-> s
drop
reduceRationalHelper :: Rational : s :-> Rational : s
reduceRationalHelper :: forall (s :: [*]). (Rational : s) :-> (Rational : s)
reduceRationalHelper = do
(Rational : s) :-> (Integer : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
(Integer : Natural : s) :-> (Integer : Integer : Natural : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup; ((Integer : Natural : s) :-> (Integer : Integer : Natural : s))
-> ((Integer : Natural : s) :-> (Integer : Integer : Natural : s))
-> (Integer : Integer : Natural : s)
:-> (Integer : Integer : Natural : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Lt =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifLt0 (Integer
-> (Integer : Natural : s) :-> (Integer : Integer : Natural : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Integer
-1 :: Integer)) (Integer
-> (Integer : Natural : s) :-> (Integer : Integer : Natural : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Integer
1 :: Integer)); forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz (ToPeano n) inp out a =>
inp :-> out
dug @2; (Integer : Natural : Integer : s)
:-> (Natural : Natural : Integer : s)
forall n (s :: [*]).
UnaryArithOpHs Abs n =>
(n : s) :-> (UnaryArithResHs Abs n : s)
abs;
(Natural : Natural : Integer : s)
:-> (Natural : Natural : Integer : s)
forall (s :: [*]).
(Natural : Natural : s) :-> (Natural : Natural : s)
reduceHelper; forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDIGLorentz (ToPeano n) inp out a =>
inp :-> out
dig @2; (Integer : Natural : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul; (Integer : Natural : s) :-> ((Integer, Natural) : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair; ((Integer, Natural) : s) :-> (Rational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
((a, Natural) : s) :-> (r : s)
uncheckedPairToRational
reduceNRationalHelper :: NRational : s :-> NRational : s
reduceNRationalHelper :: forall (s :: [*]). (NRational : s) :-> (NRational : s)
reduceNRationalHelper = do
(NRational : s) :-> (Natural : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
(Natural : Natural : s) :-> (Natural : Natural : s)
forall (s :: [*]).
(Natural : Natural : s) :-> (Natural : Natural : s)
reduceHelper;
(Natural : Natural : s) :-> (NRational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational
reduceHelper :: Natural : Natural : s :-> Natural : Natural : s
reduceHelper :: forall (s :: [*]).
(Natural : Natural : s) :-> (Natural : Natural : s)
reduceHelper = do
(Natural : Natural : s)
:-> (Natural : Natural : Natural : Natural : s)
forall a b (s :: [*]).
(Dupable a, Dupable b) =>
(a : b : s) :-> (a : b : a : b : s)
dupTop2; (Natural : Natural : Natural : Natural : s)
:-> (Natural : Natural : Natural : s)
forall (s :: [*]). (Natural : Natural : s) :-> (Natural : s)
gcdEuclid; (Natural : Natural : Natural : s)
:-> (Natural : Natural : Natural : Natural : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup; Natural
-> (Natural : Natural : Natural : Natural : s)
:-> (Natural : Natural : Natural : Natural : Natural : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Natural
1 :: Natural)
((Natural : Natural : Natural : s) :-> (Natural : Natural : s))
-> ((Natural : Natural : Natural : s) :-> (Natural : Natural : s))
-> (Natural : Natural : Natural : Natural : Natural : s)
:-> (Natural : Natural : s)
forall a (s :: [*]) (s' :: [*]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a : a : s) :-> s'
ifEq (Natural : Natural : Natural : s) :-> (Natural : Natural : s)
forall a (s :: [*]). (a : s) :-> s
drop (((Natural : Natural : Natural : s) :-> (Natural : Natural : s))
-> (Natural : Natural : Natural : Natural : Natural : s)
:-> (Natural : Natural : s))
-> ((Natural : Natural : Natural : s) :-> (Natural : Natural : s))
-> (Natural : Natural : Natural : Natural : Natural : s)
:-> (Natural : Natural : s)
forall a b. (a -> b) -> a -> b
$ do
(Natural : Natural : Natural : s)
:-> (Natural : Natural : Natural : Natural : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup; forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz (ToPeano n) inp out a =>
inp :-> out
dug @3; (Natural : Natural : Natural : Natural : s)
:-> (Natural : Natural : Natural : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap;
(Natural : Natural : Natural : Natural : s)
:-> (Maybe (Natural, Natural) : Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv; Impossible "Division by zero impossible here"
-> (Maybe (Natural, Natural) : Natural : Natural : s)
:-> ((Natural, Natural) : Natural : Natural : s)
forall err a (s :: [*]).
IsError err =>
err -> (Maybe a : s) :-> (a : s)
assertSome (forall (reason :: Symbol). HasCallStack => Impossible reason
Impossible @"Division by zero impossible here"); ((Natural, Natural) : Natural : Natural : s)
:-> (Natural : Natural : Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : s)
car; forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz (ToPeano n) inp out a =>
inp :-> out
dug @2
(Natural : Natural : Natural : s)
:-> (Maybe (Natural, Natural) : Natural : s)
forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv; Impossible "Division by zero impossible here"
-> (Maybe (Natural, Natural) : Natural : s)
:-> ((Natural, Natural) : Natural : s)
forall err a (s :: [*]).
IsError err =>
err -> (Maybe a : s) :-> (a : s)
assertSome (forall (reason :: Symbol). HasCallStack => Impossible reason
Impossible @"Division by zero impossible here"); ((Natural, Natural) : Natural : s) :-> (Natural : Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : s)
car
(Natural : Natural : s) :-> (Natural : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
euclidExtendedNormalization :: forall s. Rational : s :-> Rational : s
euclidExtendedNormalization :: forall (s :: [*]). (Rational : s) :-> (Rational : s)
euclidExtendedNormalization = do
(Rational : s) :-> (Integer : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational; ((Natural : s) :-> (Integer : s))
-> (Integer : Natural : s) :-> (Integer : Integer : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Natural : s) :-> (Integer : s)
forall i (s :: [*]).
ToIntegerArithOpHs i =>
(i : s) :-> (Integer : s)
int
forall (n :: Nat) (inp :: [*]) (out :: [*]) (s :: [*]) (s' :: [*]).
ConstraintDIPNLorentz (ToPeano n) inp out s s' =>
(s :-> s') -> inp :-> out
dipN @2 do
Integer -> s :-> (Integer : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Integer
1 :: Integer)
Integer -> (Integer : s) :-> (Integer : Integer : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Integer
0 :: Integer)
Integer
-> (Integer : Integer : s) :-> (Integer : Integer : Integer : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Integer
0 :: Integer)
Integer
-> (Integer : Integer : Integer : s)
:-> (Integer : Integer : Integer : Integer : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Integer
1 :: Integer)
(Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer : Integer : Integer : Integer : Integer : Integer : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap; (Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer
: Integer : Integer : Integer : Integer : Integer : Integer : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup; (Integer
: Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Bool
: Integer : Integer : Integer : Integer : Integer : Integer : s)
forall n (s :: [*]).
UnaryArithOpHs Neq n =>
(n : s) :-> (UnaryArithResHs Neq n : s)
neq0; ((Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer
: Integer : Integer : Integer : Integer : Integer : s))
-> (Bool
: Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Bool
: Integer : Integer : Integer : Integer : Integer : Integer : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer : Integer : Integer : Integer : Integer : Integer : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap;
((Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Bool
: Integer : Integer : Integer : Integer : Integer : Integer : s))
-> (Bool
: Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer : Integer : Integer : Integer : Integer : Integer : s)
forall (s :: [*]). (s :-> (Bool : s)) -> (Bool : s) :-> s
loop do
(Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer
: Integer : Integer : Integer : Integer : Integer : Integer
: Integer : s)
forall a b (s :: [*]).
(Dupable a, Dupable b) =>
(a : b : s) :-> (a : b : a : b : s)
dupTop2
(Integer
: Integer : Integer : Integer : Integer : Integer : Integer
: Integer : s)
:-> (Maybe (Integer, Natural)
: Integer : Integer : Integer : Integer : Integer : Integer : s)
forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv
Impossible "Division by zero impossible here"
-> (Maybe (Integer, Natural)
: Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> ((Integer, Natural)
: Integer : Integer : Integer : Integer : Integer : Integer : s)
forall err a (s :: [*]).
IsError err =>
err -> (Maybe a : s) :-> (a : s)
assertSome (forall (reason :: Symbol). HasCallStack => Impossible reason
Impossible @"Division by zero impossible here")
((Integer, Natural)
: Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer
: Integer : Integer : Integer : Integer : Integer : Integer : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : s)
car
(Integer
: Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer
: Integer : Integer : Integer : Integer : Integer : Integer
: Integer : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup
(Integer
: Integer : Integer : Integer : Integer : Integer : Integer
: Integer : s)
:-> (Integer
: Integer : Integer : Integer : Integer : Integer : Integer
: Integer : Integer : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup
forall (n :: Nat) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @9; (Integer
: Integer : Integer : Integer : Integer : Integer : Integer
: Integer : Integer : Integer : s)
:-> (Integer
: Integer : Integer : Integer : Integer : Integer : Integer
: Integer : Integer : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul; forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDIGLorentz (ToPeano n) inp out a =>
inp :-> out
dig @7; (Integer
: Integer : Integer : Integer : Integer : Integer : Integer
: Integer : Integer : s)
:-> (Integer
: Integer : Integer : Integer : Integer : Integer : Integer
: Integer : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub; forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz (ToPeano n) inp out a =>
inp :-> out
dug @2
forall (n :: Nat) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @7; (Integer
: Integer : Integer : Integer : Integer : Integer : Integer
: Integer : Integer : s)
:-> (Integer
: Integer : Integer : Integer : Integer : Integer : Integer
: Integer : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul; forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDIGLorentz (ToPeano n) inp out a =>
inp :-> out
dig @5; (Integer
: Integer : Integer : Integer : Integer : Integer : Integer
: Integer : s)
:-> (Integer
: Integer : Integer : Integer : Integer : Integer : Integer : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub; (Integer
: Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer
: Integer : Integer : Integer : Integer : Integer : Integer : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
forall (n :: Nat) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @5; (Integer
: Integer : Integer : Integer : Integer : Integer : Integer
: Integer : s)
:-> (Integer
: Integer : Integer : Integer : Integer : Integer : Integer : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul; forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDIGLorentz (ToPeano n) inp out a =>
inp :-> out
dig @3; (Integer
: Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer : Integer : Integer : Integer : Integer : Integer : s)
forall n m r (s :: [*]).
ArithOpHs Sub n m r =>
(n : m : s) :-> (r : s)
sub
forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDIGLorentz (ToPeano n) inp out a =>
inp :-> out
dig @3; forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDIGLorentz (ToPeano n) inp out a =>
inp :-> out
dig @4; forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz (ToPeano n) inp out a =>
inp :-> out
dug @2; forall (n :: Nat) (inp :: [*]) (out :: [*]) (s :: [*]) (s' :: [*]).
ConstraintDIPNLorentz (ToPeano n) inp out s s' =>
(s :-> s') -> inp :-> out
dipN @4 ((Integer : Integer : s) :-> (Integer : Integer : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap)
(Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer : Integer : Integer : Integer : Integer : Integer : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap; (Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer
: Integer : Integer : Integer : Integer : Integer : Integer : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup; (Integer
: Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Bool
: Integer : Integer : Integer : Integer : Integer : Integer : s)
forall n (s :: [*]).
UnaryArithOpHs Neq n =>
(n : s) :-> (UnaryArithResHs Neq n : s)
neq0; ((Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer
: Integer : Integer : Integer : Integer : Integer : s))
-> (Bool
: Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Bool
: Integer : Integer : Integer : Integer : Integer : Integer : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Integer : Integer : Integer : Integer : Integer : Integer : s)
:-> (Integer : Integer : Integer : Integer : Integer : Integer : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
forall (n :: Nat) (s :: [*]).
(SingIPeano n, RequireLongerOrSameLength (ToTs s) (ToPeano n),
Drop (ToPeano n) (ToTs s) ~ ToTs (Drop (ToPeano n) s)) =>
s :-> Drop (ToPeano n) s
dropN @3; ((Integer : Integer : s) :-> (Integer : s))
-> (Integer : Integer : Integer : s) :-> (Integer : Integer : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Integer : Integer : s) :-> (Integer : s)
forall a (s :: [*]). (a : s) :-> s
drop
(Integer : Integer : s) :-> (Integer : Integer : Integer : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup; ((Integer : Integer : s) :-> (Integer : Integer : s))
-> ((Integer : Integer : s) :-> (Integer : Integer : s))
-> (Integer : Integer : Integer : s) :-> (Integer : Integer : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Lt =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifLt0 (((Integer : s) :-> (Integer : s))
-> (Integer : Integer : s) :-> (Integer : Integer : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Integer : s) :-> (Integer : s)
forall n (s :: [*]).
UnaryArithOpHs Neg n =>
(n : s) :-> (UnaryArithResHs Neg n : s)
neg) ((Integer : Integer : s) :-> (Integer : Integer : s)
forall (s :: [*]). s :-> s
nop); (Integer : Integer : s) :-> (Natural : Integer : s)
forall n (s :: [*]).
UnaryArithOpHs Abs n =>
(n : s) :-> (UnaryArithResHs Abs n : s)
abs; (Natural : Integer : s) :-> (Integer : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
(Integer : Natural : s) :-> (Integer : Natural : s)
forall n (s :: [*]).
UnaryArithOpHs Neg n =>
(n : s) :-> (UnaryArithResHs Neg n : s)
neg; (Integer : Natural : s) :-> ((Integer, Natural) : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair; ((Integer, Natural) : s) :-> (Rational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
((a, Natural) : s) :-> (r : s)
uncheckedPairToRational
addSubHelper
:: forall a1 a2 a3 a4 a5 a6 b r s1 s2.
( b ~ Natural
, NiceConstant a1
, ArithOpHs Mul a2 a1 r
, Unwrappable a3
, Unwrappabled a3 ~ (a5, a1)
, Unwrappabled a4 ~ (a6, Natural)
, LorentzRational a4
)
=> ((r : a5 : a1 : s1) :-> (a6 : b : s2))
-> (a2 : a3 : s1) :-> (a4 : s2)
addSubHelper :: forall a1 a2 a3 a4 a5 a6 b r (s1 :: [*]) (s2 :: [*]).
(b ~ Natural, NiceConstant a1, ArithOpHs Mul a2 a1 r,
Unwrappable a3, Unwrappabled a3 ~ (a5, a1),
Unwrappabled a4 ~ (a6, Natural), LorentzRational a4) =>
((r : a5 : a1 : s1) :-> (a6 : b : s2))
-> (a2 : a3 : s1) :-> (a4 : s2)
addSubHelper (r : a5 : a1 : s1) :-> (a6 : b : s2)
oper = do
((a3 : s1) :-> (a1 : a5 : a1 : s1))
-> (a2 : a3 : s1) :-> (a2 : a1 : a5 : a1 : s1)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip do
(a3 : s1) :-> ((a5, a1) : s1)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap
((a5, a1) : s1) :-> (a5 : a1 : s1)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair
forall (n :: Nat) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @2
(a2 : a1 : a5 : a1 : s1) :-> (r : a5 : a1 : s1)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
(r : a5 : a1 : s1) :-> (a6 : b : s2)
oper
(a6 : b : s2) :-> ((a6, b) : s2)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair
((a6, b) : s2) :-> (a4 : s2)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
((a, Natural) : s) :-> (r : s)
uncheckedPairToRational
addSubRationalHelper
:: forall a1 a2 a3 a4 a5 a6 a7 a8 r1 r2 r3 n m s1 s2.
( NiceConstant a1
, NiceConstant a2
, LorentzRational a7
, r3 ~ Natural
, ArithOpHs Mul a1 a3 r1, ArithOpHs Mul a2 a4 r2
, ArithOpHs Mul n m r3, Unwrappable a5, Unwrappable a6
, Unwrappabled a7 ~ (a8, r3)
, Unwrappabled a5 ~ (a3, a2), Unwrappabled a6 ~ (a4, a1)
)
=> ((r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2))
-> (a6 : a5 : s1) :-> (a7 : s2)
addSubRationalHelper :: forall a1 a2 a3 a4 a5 a6 a7 a8 r1 r2 r3 n m (s1 :: [*])
(s2 :: [*]).
(NiceConstant a1, NiceConstant a2, LorentzRational a7,
r3 ~ Natural, ArithOpHs Mul a1 a3 r1, ArithOpHs Mul a2 a4 r2,
ArithOpHs Mul n m r3, Unwrappable a5, Unwrappable a6,
Unwrappabled a7 ~ (a8, r3), Unwrappabled a5 ~ (a3, a2),
Unwrappabled a6 ~ (a4, a1)) =>
((r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2))
-> (a6 : a5 : s1) :-> (a7 : s2)
addSubRationalHelper (r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2)
oper = do
((a5 : s1) :-> (a3 : a2 : s1))
-> (a6 : a5 : s1) :-> (a6 : a3 : a2 : s1)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip do
(a5 : s1) :-> ((a3, a2) : s1)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap
((a3, a2) : s1) :-> (a3 : a2 : s1)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair
(a6 : a3 : a2 : s1) :-> ((a4, a1) : a3 : a2 : s1)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap; ((a4, a1) : a3 : a2 : s1) :-> (a4 : a1 : a3 : a2 : s1)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair
((a1 : a3 : a2 : s1) :-> (r1 : a1 : a2 : s1))
-> (a4 : a1 : a3 : a2 : s1) :-> (a4 : r1 : a1 : a2 : s1)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip do
(a1 : a3 : a2 : s1) :-> (a1 : a1 : a3 : a2 : s1)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup
forall (n :: Nat) (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz (ToPeano n) inp out a =>
inp :-> out
dug @2
(a1 : a3 : a1 : a2 : s1) :-> (r1 : a1 : a2 : s1)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
forall (n :: Nat) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @4
(a2 : a4 : r1 : a1 : a2 : s1) :-> (r2 : r1 : a1 : a2 : s1)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
(r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2)
oper
((n : m : s2) :-> (Natural : s2))
-> (a8 : n : m : s2) :-> (a8 : Natural : s2)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (n : m : s2) :-> (Natural : s2)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
(a8 : Natural : s2) :-> ((a8, Natural) : s2)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair
((a8, Natural) : s2) :-> (a7 : s2)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
((a, Natural) : s) :-> (r : s)
uncheckedPairToRational
mulRationalHelper
:: forall r1 r2 r3 a b c s.
( LorentzRational r1
, LorentzRational r2
, LorentzRational r3
, Unwrappabled r1 ~ (a, Natural)
, Unwrappabled r2 ~ (b, Natural)
, Unwrappabled r3 ~ (c, Natural)
, ArithOpHs Mul a b c
)
=> r1 : r2 : s :-> r3 : s
mulRationalHelper :: forall r1 r2 r3 a b c (s :: [*]).
(LorentzRational r1, LorentzRational r2, LorentzRational r3,
Unwrappabled r1 ~ (a, Natural), Unwrappabled r2 ~ (b, Natural),
Unwrappabled r3 ~ (c, Natural), ArithOpHs Mul a b c) =>
(r1 : r2 : s) :-> (r3 : s)
mulRationalHelper = do
((r2 : s) :-> (b : Natural : s))
-> (r1 : r2 : s) :-> (r1 : b : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (r2 : s) :-> (b : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
(r1 : b : Natural : s) :-> (a : Natural : b : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
((Natural : b : Natural : s) :-> (b : Natural : Natural : s))
-> (a : Natural : b : Natural : s)
:-> (a : b : Natural : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Natural : b : Natural : s) :-> (b : Natural : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
(a : b : Natural : Natural : s) :-> (c : Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
((Natural : Natural : s) :-> (Natural : s))
-> (c : Natural : Natural : s) :-> (c : Natural : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Natural : Natural : s) :-> (Natural : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
(c : Natural : s) :-> (r3 : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational
negRational :: Rational : s :-> Rational : s
negRational :: forall (s :: [*]). (Rational : s) :-> (Rational : s)
negRational = (Rational : s) :-> (Integer : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational ((Rational : s) :-> (Integer : Natural : s))
-> ((Integer : Natural : s) :-> (Integer : Natural : s))
-> (Rational : s) :-> (Integer : Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Natural : s) :-> (Integer : Natural : s)
forall n (s :: [*]).
UnaryArithOpHs Neg n =>
(n : s) :-> (UnaryArithResHs Neg n : s)
neg ((Rational : s) :-> (Integer : Natural : s))
-> ((Integer : Natural : s) :-> (Rational : s))
-> (Rational : s) :-> (Rational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Natural : s) :-> (Rational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational
mkRational_
:: (forall s0. ErrInstr (("numerator" :! Integer, "denominator" :! Natural) : s0))
-> Integer : Natural : s :-> Rational : s
mkRational_ :: forall (s :: [*]).
(forall (s0 :: [*]).
ErrInstr (("numerator" :! Integer, "denominator" :! Natural) : s0))
-> (Integer : Natural : s) :-> (Rational : s)
mkRational_ forall (s0 :: [*]).
ErrInstr (("numerator" :! Integer, "denominator" :! Natural) : s0)
onZeroDenominator = do
(Integer : Natural : s) :-> (Natural : Integer : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
(Natural : Integer : s) :-> (Natural : Natural : Integer : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup
((Natural : Integer : s) :-> (Rational : s))
-> ((Natural : Integer : s) :-> (Rational : s))
-> (Natural : Natural : Integer : s) :-> (Rational : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Eq' =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifEq0
do
Label "denominator"
-> (Natural : Integer : s)
:-> (("denominator" :! Natural) : Integer : s)
forall (name :: Symbol) a (s :: [*]).
Label name -> (a : s) :-> ((name :! a) : s)
toNamed Label "denominator"
forall (x :: Symbol) a. IsLabel x a => a
#denominator
(("denominator" :! Natural) : Integer : s)
:-> (Integer : ("denominator" :! Natural) : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
Label "numerator"
-> (Integer : ("denominator" :! Natural) : s)
:-> (("numerator" :! Integer) : ("denominator" :! Natural) : s)
forall (name :: Symbol) a (s :: [*]).
Label name -> (a : s) :-> ((name :! a) : s)
toNamed Label "numerator"
forall (x :: Symbol) a. IsLabel x a => a
#numerator
(("numerator" :! Integer) : ("denominator" :! Natural) : s)
:-> (("numerator" :! Integer, "denominator" :! Natural) : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair
(("numerator" :! Integer, "denominator" :! Natural) : s)
:-> (Rational : s)
forall (s0 :: [*]).
ErrInstr (("numerator" :! Integer, "denominator" :! Natural) : s0)
onZeroDenominator
do
(Natural : Integer : s) :-> (Integer : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
(Integer : Natural : s) :-> (Rational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational
type instance ErrorArg "zero_denominator" =
("numerator" :! Integer, "denominator" :! Natural)
instance CustomErrorHasDoc "zero_denominator" where
customErrClass :: ErrorClass
customErrClass = ErrorClass
ErrClassActionException
customErrDocMdCause :: Markdown
customErrDocMdCause =
Markdown
"Attempt to construct rational with zero denominator."