{-# LANGUAGE InstanceSigs #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Lorentz.FixedArith
(
Lorentz.FixedArith.div
, castNFixedToFixed
, castFixedToNFixed
, LorentzRounding (..)
, LorentzFixedCast (..)
) where
import Data.Fixed
import qualified GHC.TypeLits as Lit
import Prelude hiding (and, compare, drop, natVal, some, swap)
import qualified Prelude as P
import Lorentz.Arith
import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Constraints.Scopes
import Lorentz.Errors
import Lorentz.Instr
import Lorentz.Macro
import Lorentz.Value
import Morley.Michelson.Typed.Arith
import Morley.Michelson.Typed.Scope
class LorentzRounding a b where
round_ :: a : s :-> b : s
ceil_ :: a : s :-> b : s
floor_ :: a : s :-> b : s
instance (KnownNat a, KnownNat b) => LorentzRounding (Fixed (DecBase a)) (Fixed (DecBase b)) where
round_ :: (Fixed (DecBase a) : s) :-> (Fixed (DecBase b) : s)
round_ = RoundingPattern
-> Natural -> (Fixed (DecBase a) : s) :-> (Fixed (DecBase b) : s)
forall (a :: Nat) (b :: Nat) r1 r2 (s :: [*]).
(KnownNat a, KnownNat b,
FailOnTicketFound (ContainsTicket (ToT (Unwrappabled r1))),
MichelsonCoercible r1 r2, Typeable (Unwrappabled r2),
IsoValue (Unwrappabled r2), SingI (ToT (Unwrappabled r1)),
Unwrappable r2, Unwrappable r1,
ArithOpHs Add Integer (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs Add Natural (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs And (Unwrappabled r2) Natural Natural,
ArithOpHs
EDiv (Unwrappabled r1) Integer (Maybe (Unwrappabled r2, Natural)),
ArithOpHs Mul Integer r1 r1) =>
RoundingPattern -> Natural -> (r1 : s) :-> (r2 : s)
roundingHelper @a @b RoundingPattern
Round Natural
10
ceil_ :: (Fixed (DecBase a) : s) :-> (Fixed (DecBase b) : s)
ceil_ = RoundingPattern
-> Natural -> (Fixed (DecBase a) : s) :-> (Fixed (DecBase b) : s)
forall (a :: Nat) (b :: Nat) r1 r2 (s :: [*]).
(KnownNat a, KnownNat b,
FailOnTicketFound (ContainsTicket (ToT (Unwrappabled r1))),
MichelsonCoercible r1 r2, Typeable (Unwrappabled r2),
IsoValue (Unwrappabled r2), SingI (ToT (Unwrappabled r1)),
Unwrappable r2, Unwrappable r1,
ArithOpHs Add Integer (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs Add Natural (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs And (Unwrappabled r2) Natural Natural,
ArithOpHs
EDiv (Unwrappabled r1) Integer (Maybe (Unwrappabled r2, Natural)),
ArithOpHs Mul Integer r1 r1) =>
RoundingPattern -> Natural -> (r1 : s) :-> (r2 : s)
roundingHelper @a @b RoundingPattern
Ceil Natural
10
floor_ :: (Fixed (DecBase a) : s) :-> (Fixed (DecBase b) : s)
floor_ = RoundingPattern
-> Natural -> (Fixed (DecBase a) : s) :-> (Fixed (DecBase b) : s)
forall (a :: Nat) (b :: Nat) r1 r2 (s :: [*]).
(KnownNat a, KnownNat b,
FailOnTicketFound (ContainsTicket (ToT (Unwrappabled r1))),
MichelsonCoercible r1 r2, Typeable (Unwrappabled r2),
IsoValue (Unwrappabled r2), SingI (ToT (Unwrappabled r1)),
Unwrappable r2, Unwrappable r1,
ArithOpHs Add Integer (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs Add Natural (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs And (Unwrappabled r2) Natural Natural,
ArithOpHs
EDiv (Unwrappabled r1) Integer (Maybe (Unwrappabled r2, Natural)),
ArithOpHs Mul Integer r1 r1) =>
RoundingPattern -> Natural -> (r1 : s) :-> (r2 : s)
roundingHelper @a @b RoundingPattern
Floor Natural
10
instance (KnownNat a, KnownNat b) => LorentzRounding (Fixed (BinBase a)) (Fixed (BinBase b)) where
round_ :: (Fixed (BinBase a) : s) :-> (Fixed (BinBase b) : s)
round_ = RoundingPattern
-> Natural -> (Fixed (BinBase a) : s) :-> (Fixed (BinBase b) : s)
forall (a :: Nat) (b :: Nat) r1 r2 (s :: [*]).
(KnownNat a, KnownNat b,
FailOnTicketFound (ContainsTicket (ToT (Unwrappabled r1))),
MichelsonCoercible r1 r2, Typeable (Unwrappabled r2),
IsoValue (Unwrappabled r2), SingI (ToT (Unwrappabled r1)),
Unwrappable r2, Unwrappable r1,
ArithOpHs Add Integer (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs Add Natural (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs And (Unwrappabled r2) Natural Natural,
ArithOpHs
EDiv (Unwrappabled r1) Integer (Maybe (Unwrappabled r2, Natural)),
ArithOpHs Mul Integer r1 r1) =>
RoundingPattern -> Natural -> (r1 : s) :-> (r2 : s)
roundingHelper @a @b RoundingPattern
Round Natural
2
ceil_ :: (Fixed (BinBase a) : s) :-> (Fixed (BinBase b) : s)
ceil_ = RoundingPattern
-> Natural -> (Fixed (BinBase a) : s) :-> (Fixed (BinBase b) : s)
forall (a :: Nat) (b :: Nat) r1 r2 (s :: [*]).
(KnownNat a, KnownNat b,
FailOnTicketFound (ContainsTicket (ToT (Unwrappabled r1))),
MichelsonCoercible r1 r2, Typeable (Unwrappabled r2),
IsoValue (Unwrappabled r2), SingI (ToT (Unwrappabled r1)),
Unwrappable r2, Unwrappable r1,
ArithOpHs Add Integer (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs Add Natural (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs And (Unwrappabled r2) Natural Natural,
ArithOpHs
EDiv (Unwrappabled r1) Integer (Maybe (Unwrappabled r2, Natural)),
ArithOpHs Mul Integer r1 r1) =>
RoundingPattern -> Natural -> (r1 : s) :-> (r2 : s)
roundingHelper @a @b RoundingPattern
Ceil Natural
2
floor_ :: (Fixed (BinBase a) : s) :-> (Fixed (BinBase b) : s)
floor_ = RoundingPattern
-> Natural -> (Fixed (BinBase a) : s) :-> (Fixed (BinBase b) : s)
forall (a :: Nat) (b :: Nat) r1 r2 (s :: [*]).
(KnownNat a, KnownNat b,
FailOnTicketFound (ContainsTicket (ToT (Unwrappabled r1))),
MichelsonCoercible r1 r2, Typeable (Unwrappabled r2),
IsoValue (Unwrappabled r2), SingI (ToT (Unwrappabled r1)),
Unwrappable r2, Unwrappable r1,
ArithOpHs Add Integer (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs Add Natural (Unwrappabled r2) (Unwrappabled r2),
ArithOpHs And (Unwrappabled r2) Natural Natural,
ArithOpHs
EDiv (Unwrappabled r1) Integer (Maybe (Unwrappabled r2, Natural)),
ArithOpHs Mul Integer r1 r1) =>
RoundingPattern -> Natural -> (r1 : s) :-> (r2 : s)
roundingHelper @a @b RoundingPattern
Floor Natural
2
instance (LorentzRounding (Fixed (DecBase a)) (Fixed (DecBase b)))
=> LorentzRounding (NFixed (DecBase a)) (NFixed (DecBase b)) where
round_ :: (NFixed (DecBase a) : s) :-> (NFixed (DecBase b) : s)
round_ = (NFixed (DecBase a) : s) :-> (Fixed (DecBase a) : s)
forall k (p :: k) (s :: [*]). (NFixed p : s) :-> (Fixed p : s)
castNFixedToFixed ((NFixed (DecBase a) : s) :-> (Fixed (DecBase a) : s))
-> ((Fixed (DecBase a) : s) :-> (Fixed (DecBase b) : s))
-> (NFixed (DecBase a) : s) :-> (Fixed (DecBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (DecBase a) : s) :-> (Fixed (DecBase b) : s)
forall a b (s :: [*]). LorentzRounding a b => (a : s) :-> (b : s)
round_ ((NFixed (DecBase a) : s) :-> (Fixed (DecBase b) : s))
-> ((Fixed (DecBase b) : s) :-> (NFixed (DecBase b) : s))
-> (NFixed (DecBase a) : s) :-> (NFixed (DecBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (DecBase b) : s) :-> (NFixed (DecBase b) : s)
forall k (p :: k) (s :: [*]). (Fixed p : s) :-> (NFixed p : s)
unsafeCastFixedToNFixed
ceil_ :: (NFixed (DecBase a) : s) :-> (NFixed (DecBase b) : s)
ceil_ = (NFixed (DecBase a) : s) :-> (Fixed (DecBase a) : s)
forall k (p :: k) (s :: [*]). (NFixed p : s) :-> (Fixed p : s)
castNFixedToFixed ((NFixed (DecBase a) : s) :-> (Fixed (DecBase a) : s))
-> ((Fixed (DecBase a) : s) :-> (Fixed (DecBase b) : s))
-> (NFixed (DecBase a) : s) :-> (Fixed (DecBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (DecBase a) : s) :-> (Fixed (DecBase b) : s)
forall a b (s :: [*]). LorentzRounding a b => (a : s) :-> (b : s)
ceil_ ((NFixed (DecBase a) : s) :-> (Fixed (DecBase b) : s))
-> ((Fixed (DecBase b) : s) :-> (NFixed (DecBase b) : s))
-> (NFixed (DecBase a) : s) :-> (NFixed (DecBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (DecBase b) : s) :-> (NFixed (DecBase b) : s)
forall k (p :: k) (s :: [*]). (Fixed p : s) :-> (NFixed p : s)
unsafeCastFixedToNFixed
floor_ :: (NFixed (DecBase a) : s) :-> (NFixed (DecBase b) : s)
floor_ = (NFixed (DecBase a) : s) :-> (Fixed (DecBase a) : s)
forall k (p :: k) (s :: [*]). (NFixed p : s) :-> (Fixed p : s)
castNFixedToFixed ((NFixed (DecBase a) : s) :-> (Fixed (DecBase a) : s))
-> ((Fixed (DecBase a) : s) :-> (Fixed (DecBase b) : s))
-> (NFixed (DecBase a) : s) :-> (Fixed (DecBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (DecBase a) : s) :-> (Fixed (DecBase b) : s)
forall a b (s :: [*]). LorentzRounding a b => (a : s) :-> (b : s)
floor_ ((NFixed (DecBase a) : s) :-> (Fixed (DecBase b) : s))
-> ((Fixed (DecBase b) : s) :-> (NFixed (DecBase b) : s))
-> (NFixed (DecBase a) : s) :-> (NFixed (DecBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (DecBase b) : s) :-> (NFixed (DecBase b) : s)
forall k (p :: k) (s :: [*]). (Fixed p : s) :-> (NFixed p : s)
unsafeCastFixedToNFixed
instance (KnownNat a, KnownNat b)
=> LorentzRounding (NFixed (BinBase a)) (NFixed (BinBase b)) where
round_ :: (NFixed (BinBase a) : s) :-> (NFixed (BinBase b) : s)
round_ = (NFixed (BinBase a) : s) :-> (Fixed (BinBase a) : s)
forall k (p :: k) (s :: [*]). (NFixed p : s) :-> (Fixed p : s)
castNFixedToFixed ((NFixed (BinBase a) : s) :-> (Fixed (BinBase a) : s))
-> ((Fixed (BinBase a) : s) :-> (Fixed (BinBase b) : s))
-> (NFixed (BinBase a) : s) :-> (Fixed (BinBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (BinBase a) : s) :-> (Fixed (BinBase b) : s)
forall a b (s :: [*]). LorentzRounding a b => (a : s) :-> (b : s)
round_ ((NFixed (BinBase a) : s) :-> (Fixed (BinBase b) : s))
-> ((Fixed (BinBase b) : s) :-> (NFixed (BinBase b) : s))
-> (NFixed (BinBase a) : s) :-> (NFixed (BinBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (BinBase b) : s) :-> (NFixed (BinBase b) : s)
forall k (p :: k) (s :: [*]). (Fixed p : s) :-> (NFixed p : s)
unsafeCastFixedToNFixed
ceil_ :: (NFixed (BinBase a) : s) :-> (NFixed (BinBase b) : s)
ceil_ = (NFixed (BinBase a) : s) :-> (Fixed (BinBase a) : s)
forall k (p :: k) (s :: [*]). (NFixed p : s) :-> (Fixed p : s)
castNFixedToFixed ((NFixed (BinBase a) : s) :-> (Fixed (BinBase a) : s))
-> ((Fixed (BinBase a) : s) :-> (Fixed (BinBase b) : s))
-> (NFixed (BinBase a) : s) :-> (Fixed (BinBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (BinBase a) : s) :-> (Fixed (BinBase b) : s)
forall a b (s :: [*]). LorentzRounding a b => (a : s) :-> (b : s)
ceil_ ((NFixed (BinBase a) : s) :-> (Fixed (BinBase b) : s))
-> ((Fixed (BinBase b) : s) :-> (NFixed (BinBase b) : s))
-> (NFixed (BinBase a) : s) :-> (NFixed (BinBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (BinBase b) : s) :-> (NFixed (BinBase b) : s)
forall k (p :: k) (s :: [*]). (Fixed p : s) :-> (NFixed p : s)
unsafeCastFixedToNFixed
floor_ :: (NFixed (BinBase a) : s) :-> (NFixed (BinBase b) : s)
floor_ = (NFixed (BinBase a) : s) :-> (Fixed (BinBase a) : s)
forall k (p :: k) (s :: [*]). (NFixed p : s) :-> (Fixed p : s)
castNFixedToFixed ((NFixed (BinBase a) : s) :-> (Fixed (BinBase a) : s))
-> ((Fixed (BinBase a) : s) :-> (Fixed (BinBase b) : s))
-> (NFixed (BinBase a) : s) :-> (Fixed (BinBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (BinBase a) : s) :-> (Fixed (BinBase b) : s)
forall a b (s :: [*]). LorentzRounding a b => (a : s) :-> (b : s)
floor_ ((NFixed (BinBase a) : s) :-> (Fixed (BinBase b) : s))
-> ((Fixed (BinBase b) : s) :-> (NFixed (BinBase b) : s))
-> (NFixed (BinBase a) : s) :-> (NFixed (BinBase b) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (BinBase b) : s) :-> (NFixed (BinBase b) : s)
forall k (p :: k) (s :: [*]). (Fixed p : s) :-> (NFixed p : s)
unsafeCastFixedToNFixed
class LorentzFixedCast a where
fromFixed :: a : s :-> Integer : s
toFixed :: Integer : s :-> a : s
instance (KnownNat a) => LorentzFixedCast (Fixed (DecBase a)) where
fromFixed :: (Fixed (DecBase a)) : s :-> Integer : s
fromFixed :: (Fixed (DecBase a) : s) :-> (Integer : s)
fromFixed = (forall (s :: [*]).
LorentzRounding (Fixed (DecBase a)) (Fixed (DecBase 0)) =>
(Fixed (DecBase a) : s) :-> (Fixed (DecBase 0) : s)
forall a b (s :: [*]). LorentzRounding a b => (a : s) :-> (b : s)
round_ @(Fixed (DecBase a)) @(Fixed (DecBase 0))) ((Fixed (DecBase a) : s) :-> (Fixed (DecBase 0) : s))
-> ((Fixed (DecBase 0) : s) :-> (Integer : s))
-> (Fixed (DecBase a) : s) :-> (Integer : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (DecBase 0) : s) :-> (Integer : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_
toFixed :: (Integer : s) :-> (Fixed (DecBase a) : s)
toFixed = let Integer
pow :: Integer = Integer
10 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Proxy a -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (Proxy a
forall k (t :: k). Proxy t
Proxy @a) in Integer -> (Integer : s) :-> (Integer : Integer : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Integer
pow ((Integer : s) :-> (Integer : Integer : s))
-> ((Integer : Integer : s) :-> (Integer : s))
-> (Integer : s) :-> (Integer : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Integer : s) :-> (Integer : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul ((Integer : s) :-> (Integer : s))
-> ((Integer : s) :-> (Fixed (DecBase a) : s))
-> (Integer : s) :-> (Fixed (DecBase a) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall (s :: [*]).
MichelsonCoercible Integer (Fixed (DecBase a)) =>
(Integer : s) :-> (Fixed (DecBase a) : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_ @Integer @(Fixed (DecBase a))
instance (KnownNat a) => LorentzFixedCast (Fixed (BinBase a)) where
fromFixed :: (Fixed (BinBase a)) : s :-> Integer : s
fromFixed :: (Fixed (BinBase a) : s) :-> (Integer : s)
fromFixed = (forall (s :: [*]).
LorentzRounding (Fixed (BinBase a)) (Fixed (BinBase 0)) =>
(Fixed (BinBase a) : s) :-> (Fixed (BinBase 0) : s)
forall a b (s :: [*]). LorentzRounding a b => (a : s) :-> (b : s)
round_ @(Fixed (BinBase a)) @(Fixed (BinBase 0))) ((Fixed (BinBase a) : s) :-> (Fixed (BinBase 0) : s))
-> ((Fixed (BinBase 0) : s) :-> (Integer : s))
-> (Fixed (BinBase a) : s) :-> (Integer : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed (BinBase 0) : s) :-> (Integer : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_
toFixed :: (Integer : s) :-> (Fixed (BinBase a) : s)
toFixed = let Integer
pow :: Integer = Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Proxy a -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (Proxy a
forall k (t :: k). Proxy t
Proxy @a) in Integer -> (Integer : s) :-> (Integer : Integer : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Integer
pow ((Integer : s) :-> (Integer : Integer : s))
-> ((Integer : Integer : s) :-> (Integer : s))
-> (Integer : s) :-> (Integer : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Integer : s) :-> (Integer : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul ((Integer : s) :-> (Integer : s))
-> ((Integer : s) :-> (Fixed (BinBase a) : s))
-> (Integer : s) :-> (Fixed (BinBase a) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall (s :: [*]).
MichelsonCoercible Integer (Fixed (BinBase a)) =>
(Integer : s) :-> (Fixed (BinBase a) : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_ @Integer @(Fixed (BinBase a))
instance (LorentzFixedCast (Fixed a)) => LorentzFixedCast (NFixed a) where
fromFixed :: (NFixed a : s) :-> (Integer : s)
fromFixed = (NFixed a : s) :-> (Fixed a : s)
forall k (p :: k) (s :: [*]). (NFixed p : s) :-> (Fixed p : s)
castNFixedToFixed ((NFixed a : s) :-> (Fixed a : s))
-> ((Fixed a : s) :-> (Integer : s))
-> (NFixed a : s) :-> (Integer : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed a : s) :-> (Integer : s)
forall a (s :: [*]).
LorentzFixedCast a =>
(a : s) :-> (Integer : s)
fromFixed
toFixed :: (Integer : s) :-> (NFixed a : s)
toFixed = (Integer : s) :-> (Fixed a : s)
forall a (s :: [*]).
LorentzFixedCast a =>
(Integer : s) :-> (a : s)
toFixed ((Integer : s) :-> (Fixed a : s))
-> ((Fixed a : s) :-> (Maybe (NFixed a) : s))
-> (Integer : s) :-> (Maybe (NFixed a) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed a : s) :-> (Maybe (NFixed a) : s)
forall k (p :: k) (s :: [*]).
(Fixed p : s) :-> (Maybe (NFixed p) : s)
castFixedToNFixed ((Integer : s) :-> (Maybe (NFixed a) : s))
-> ((Maybe (NFixed a) : s) :-> (NFixed a : s))
-> (Integer : s) :-> (NFixed a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# MText -> (Maybe (NFixed a) : s) :-> (NFixed a : s)
forall err a (s :: [*]).
IsError err =>
err -> (Maybe a : s) :-> (a : s)
assertSome [mt|casting negative value to NFixed|]
data Div
instance ( KnownNat a
, KnownNat b
, KnownNat r
) => ArithOpHs Div (Fixed (DecBase a)) (Fixed (DecBase b)) (Maybe (Fixed (DecBase r))) where
evalArithOpHs :: (Fixed (DecBase a) : Fixed (DecBase b) : s)
:-> (Maybe (Fixed (DecBase r)) : s)
evalArithOpHs = Integer
-> (Fixed (DecBase a) : Fixed (DecBase b) : s)
:-> (Maybe (Fixed (DecBase r)) : s)
forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat) base b1 b2 a r
(s :: [*]).
(KnownNat t1, KnownNat t2, KnownNat t3, Num base,
NiceConstant base, Unwrappable r, Unwrappable b1, Unwrappable a,
Unwrappabled a ~ base, ArithOpHs Mul base r r,
ArithOpHs
EDiv (Unwrappabled r) (Unwrappabled b1) (Maybe (base, b2)),
IsoValue a, Typeable a) =>
base -> (r : b1 : s) :-> (Maybe a : s)
fixedDivHelper @a @b @r Integer
10
instance ( KnownNat a
, KnownNat b
, KnownNat r
) => ArithOpHs Div (Fixed (BinBase a)) (Fixed (BinBase b)) (Maybe (Fixed (BinBase r))) where
evalArithOpHs :: (Fixed (BinBase a) : Fixed (BinBase b) : s)
:-> (Maybe (Fixed (BinBase r)) : s)
evalArithOpHs = Integer
-> (Fixed (BinBase a) : Fixed (BinBase b) : s)
:-> (Maybe (Fixed (BinBase r)) : s)
forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat) base b1 b2 a r
(s :: [*]).
(KnownNat t1, KnownNat t2, KnownNat t3, Num base,
NiceConstant base, Unwrappable r, Unwrappable b1, Unwrappable a,
Unwrappabled a ~ base, ArithOpHs Mul base r r,
ArithOpHs
EDiv (Unwrappabled r) (Unwrappabled b1) (Maybe (base, b2)),
IsoValue a, Typeable a) =>
base -> (r : b1 : s) :-> (Maybe a : s)
fixedDivHelper @a @b @r Integer
2
instance ( KnownNat a
, KnownNat b
, KnownNat r
) => ArithOpHs Div (NFixed (DecBase a)) (NFixed (DecBase b)) (Maybe (NFixed (DecBase r))) where
evalArithOpHs :: (NFixed (DecBase a) : NFixed (DecBase b) : s)
:-> (Maybe (NFixed (DecBase r)) : s)
evalArithOpHs = Natural
-> (NFixed (DecBase a) : NFixed (DecBase b) : s)
:-> (Maybe (NFixed (DecBase r)) : s)
forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat) base b1 b2 a r
(s :: [*]).
(KnownNat t1, KnownNat t2, KnownNat t3, Num base,
NiceConstant base, Unwrappable r, Unwrappable b1, Unwrappable a,
Unwrappabled a ~ base, ArithOpHs Mul base r r,
ArithOpHs
EDiv (Unwrappabled r) (Unwrappabled b1) (Maybe (base, b2)),
IsoValue a, Typeable a) =>
base -> (r : b1 : s) :-> (Maybe a : s)
fixedDivHelper @a @b @r Natural
10
instance ( KnownNat a
, KnownNat b
, KnownNat r
) => ArithOpHs Div (NFixed (BinBase a)) (NFixed (BinBase b)) (Maybe (NFixed (BinBase r))) where
evalArithOpHs :: (NFixed (BinBase a) : NFixed (BinBase b) : s)
:-> (Maybe (NFixed (BinBase r)) : s)
evalArithOpHs = Natural
-> (NFixed (BinBase a) : NFixed (BinBase b) : s)
:-> (Maybe (NFixed (BinBase r)) : s)
forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat) base b1 b2 a r
(s :: [*]).
(KnownNat t1, KnownNat t2, KnownNat t3, Num base,
NiceConstant base, Unwrappable r, Unwrappable b1, Unwrappable a,
Unwrappabled a ~ base, ArithOpHs Mul base r r,
ArithOpHs
EDiv (Unwrappabled r) (Unwrappabled b1) (Maybe (base, b2)),
IsoValue a, Typeable a) =>
base -> (r : b1 : s) :-> (Maybe a : s)
fixedDivHelper @a @b @r Natural
2
div
:: forall r n m s. ArithOpHs Div n m r
=> n : m : s :-> r : s
div :: (n : m : s) :-> (r : s)
div = forall n m r (s :: [*]).
ArithOpHs Div n m r =>
(n : m : s) :-> (r : s)
forall aop n m r (s :: [*]).
ArithOpHs aop n m r =>
(n : m : s) :-> (r : s)
evalArithOpHs @Div
castNFixedToFixed :: NFixed p : s :-> Fixed p : s
castNFixedToFixed :: (NFixed p : s) :-> (Fixed p : s)
castNFixedToFixed = (NFixed p : s) :-> (Integer : s)
forall i (s :: [*]).
ToIntegerArithOpHs i =>
(i : s) :-> (Integer : s)
int ((NFixed p : s) :-> (Integer : s))
-> ((Integer : s) :-> (Fixed p : s))
-> (NFixed p : s) :-> (Fixed p : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : s) :-> (Fixed p : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_
castFixedToNFixed :: Fixed p : s :-> Maybe (NFixed p) : s
castFixedToNFixed :: (Fixed p : s) :-> (Maybe (NFixed p) : s)
castFixedToNFixed = (Fixed p : s) :-> (Integer : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((Fixed p : s) :-> (Integer : s))
-> ((Integer : s) :-> (Maybe Natural : s))
-> (Fixed p : s) :-> (Maybe Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : s) :-> (Maybe Natural : s)
forall (s :: [*]). (Integer : s) :-> (Maybe Natural : s)
isNat ((Fixed p : s) :-> (Maybe Natural : s))
-> ((Maybe Natural : s) :-> (Maybe (NFixed p) : s))
-> (Fixed p : s) :-> (Maybe (NFixed p) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Maybe Natural : s) :-> (Maybe (NFixed p) : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_
unsafeCastFixedToNFixed :: Fixed p : s :-> NFixed p : s
unsafeCastFixedToNFixed :: (Fixed p : s) :-> (NFixed p : s)
unsafeCastFixedToNFixed = (Fixed p : s) :-> (Integer : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((Fixed p : s) :-> (Integer : s))
-> ((Integer : s) :-> (Natural : s))
-> (Fixed p : s) :-> (Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : s) :-> (Natural : s)
forall n (s :: [*]).
UnaryArithOpHs Abs n =>
(n : s) :-> (UnaryArithResHs Abs n : s)
Lorentz.Instr.abs ((Fixed p : s) :-> (Natural : s))
-> ((Natural : s) :-> (NFixed p : s))
-> (Fixed p : s) :-> (NFixed p : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : s) :-> (NFixed p : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_
instance (r ~ Maybe (Integer, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (DecBase a)) Integer r where
evalArithOpHs :: (Fixed (DecBase a) : Integer : s) :-> (r : s)
evalArithOpHs = Integer
-> (Fixed (DecBase a) : Integer : s)
:-> (Maybe (Integer, NFixed (DecBase a)) : s)
forall (a :: Nat) base x y r1 r2 m (s :: [*]).
(KnownNat a, Num base, NiceConstant base, KnownValue r1,
KnownValue r2, Dupable m, UnaryArithOpHs Eq' m,
ArithOpHs Mul base y m,
ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2)),
Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool) =>
base -> (x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper @a @Integer Integer
10
instance (r ~ Maybe (Integer, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (DecBase a)) Natural r where
evalArithOpHs :: (Fixed (DecBase a) : Natural : s) :-> (r : s)
evalArithOpHs = Integer
-> (Fixed (DecBase a) : Natural : s)
:-> (Maybe (Integer, NFixed (DecBase a)) : s)
forall (a :: Nat) base x y r1 r2 m (s :: [*]).
(KnownNat a, Num base, NiceConstant base, KnownValue r1,
KnownValue r2, Dupable m, UnaryArithOpHs Eq' m,
ArithOpHs Mul base y m,
ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2)),
Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool) =>
base -> (x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper @a @Integer Integer
10
instance (r ~ Maybe (Integer, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (BinBase a)) Integer r where
evalArithOpHs :: (Fixed (BinBase a) : Integer : s) :-> (r : s)
evalArithOpHs = Natural
-> (Fixed (BinBase a) : Integer : s)
:-> (Maybe (Integer, NFixed (BinBase a)) : s)
forall (a :: Nat) base x y r1 r2 m (s :: [*]).
(KnownNat a, Num base, NiceConstant base, KnownValue r1,
KnownValue r2, Dupable m, UnaryArithOpHs Eq' m,
ArithOpHs Mul base y m,
ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2)),
Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool) =>
base -> (x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper @a @Natural Natural
2
instance (r ~ Maybe (Integer, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (BinBase a)) Natural r where
evalArithOpHs :: (Fixed (BinBase a) : Natural : s) :-> (r : s)
evalArithOpHs = Natural
-> (Fixed (BinBase a) : Natural : s)
:-> (Maybe (Integer, NFixed (BinBase a)) : s)
forall (a :: Nat) base x y r1 r2 m (s :: [*]).
(KnownNat a, Num base, NiceConstant base, KnownValue r1,
KnownValue r2, Dupable m, UnaryArithOpHs Eq' m,
ArithOpHs Mul base y m,
ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2)),
Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool) =>
base -> (x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper @a @Natural Natural
2
instance (r ~ Maybe (Integer, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (DecBase a)) Integer r where
evalArithOpHs :: (NFixed (DecBase a) : Integer : s) :-> (r : s)
evalArithOpHs = Integer
-> (NFixed (DecBase a) : Integer : s)
:-> (Maybe (Integer, NFixed (DecBase a)) : s)
forall (a :: Nat) base x y r1 r2 m (s :: [*]).
(KnownNat a, Num base, NiceConstant base, KnownValue r1,
KnownValue r2, Dupable m, UnaryArithOpHs Eq' m,
ArithOpHs Mul base y m,
ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2)),
Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool) =>
base -> (x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper @a @Integer Integer
10
instance (r ~ Maybe (Natural, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (DecBase a)) Natural r where
evalArithOpHs :: (NFixed (DecBase a) : Natural : s) :-> (r : s)
evalArithOpHs = Natural
-> (NFixed (DecBase a) : Natural : s)
:-> (Maybe (Natural, NFixed (DecBase a)) : s)
forall (a :: Nat) base x y r1 r2 m (s :: [*]).
(KnownNat a, Num base, NiceConstant base, KnownValue r1,
KnownValue r2, Dupable m, UnaryArithOpHs Eq' m,
ArithOpHs Mul base y m,
ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2)),
Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool) =>
base -> (x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper @a @Natural Natural
10
instance (r ~ Maybe (Integer, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (BinBase a)) Integer r where
evalArithOpHs :: (NFixed (BinBase a) : Integer : s) :-> (r : s)
evalArithOpHs = Natural
-> (NFixed (BinBase a) : Integer : s)
:-> (Maybe (Integer, NFixed (BinBase a)) : s)
forall (a :: Nat) base x y r1 r2 m (s :: [*]).
(KnownNat a, Num base, NiceConstant base, KnownValue r1,
KnownValue r2, Dupable m, UnaryArithOpHs Eq' m,
ArithOpHs Mul base y m,
ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2)),
Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool) =>
base -> (x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper @a @Natural Natural
2
instance (r ~ Maybe (Natural, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (BinBase a)) Natural r where
evalArithOpHs :: (NFixed (BinBase a) : Natural : s) :-> (r : s)
evalArithOpHs = Natural
-> (NFixed (BinBase a) : Natural : s)
:-> (Maybe (Natural, NFixed (BinBase a)) : s)
forall (a :: Nat) base x y r1 r2 m (s :: [*]).
(KnownNat a, Num base, NiceConstant base, KnownValue r1,
KnownValue r2, Dupable m, UnaryArithOpHs Eq' m,
ArithOpHs Mul base y m,
ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2)),
Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool) =>
base -> (x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper @a @Natural Natural
2
data RoundingPattern = Round | Ceil | Floor
roundingHelper
:: forall a b r1 r2 s.
( KnownNat a, KnownNat b
, FailOnTicketFound (ContainsTicket (ToT (Unwrappabled r1)))
, MichelsonCoercible r1 r2
, Typeable (Unwrappabled r2)
, IsoValue (Unwrappabled r2)
, SingI (ToT (Unwrappabled r1))
, Unwrappable r2
, Unwrappable r1
, ArithOpHs Add Integer (Unwrappabled r2) (Unwrappabled r2)
, ArithOpHs Add Natural (Unwrappabled r2) (Unwrappabled r2)
, ArithOpHs And (Unwrappabled r2) Natural Natural
, ArithOpHs EDiv (Unwrappabled r1) Integer (Maybe (Unwrappabled r2, Natural))
, ArithOpHs Mul Integer r1 r1
)
=> RoundingPattern -> Natural -> (r1 : s :-> r2 : s)
roundingHelper :: RoundingPattern -> Natural -> (r1 : s) :-> (r2 : s)
roundingHelper RoundingPattern
rp Natural
base =
let Natural
halfBase :: Natural = Natural
base Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`P.div` Natural
2
Integer
powDifference :: Integer = (Proxy b -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (Proxy b
forall k (t :: k). Proxy t
Proxy @b)) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- (Proxy a -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (Proxy a
forall k (t :: k). Proxy t
Proxy @a))
Integer
newPow :: Integer = Natural -> Integer
forall a b.
(Integral a, Integral b, IsIntSubType a b ~ 'True) =>
a -> b
fromIntegral (Natural -> Integer) -> Natural -> Integer
forall a b. (a -> b) -> a -> b
$ Natural
2 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
halfNewPow
Natural
halfNewPow :: Natural = Natural
halfBase Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* (Natural
base Natural -> Integer -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer -> Integer
forall a. Num a => a -> a
Prelude.abs Integer
powDifference Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1))
in case () of
()
_ | Integer
powDifference Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 -> ((r1 : s) :-> (r2 : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_ :: (r1 : s :-> r2 : s))
| Integer
powDifference Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 ->
Integer -> (r1 : s) :-> (Integer : r1 : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Integer
newPow ((r1 : s) :-> (Integer : r1 : s))
-> ((Integer : r1 : s) :-> (r1 : s)) -> (r1 : s) :-> (r1 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : r1 : s) :-> (r1 : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul ((r1 : s) :-> (r1 : s))
-> ((r1 : s) :-> (r2 : s)) -> (r1 : s) :-> (r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((r1 : s) :-> (r2 : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_ :: (r1 : s :-> r2 : s))
| Bool
otherwise ->
Integer -> (r1 : s) :-> (Integer : r1 : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Integer
newPow ((r1 : s) :-> (Integer : r1 : s))
-> ((Integer : r1 : s) :-> (r1 : Integer : s))
-> (r1 : s) :-> (r1 : Integer : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(Integer : r1 : s) :-> (r1 : Integer : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((r1 : s) :-> (r1 : Integer : s))
-> ((r1 : Integer : s) :-> (Unwrappabled r1 : Integer : s))
-> (r1 : s) :-> (Unwrappabled r1 : Integer : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(r1 : Integer : s) :-> (Unwrappabled r1 : Integer : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((r1 : s) :-> (Unwrappabled r1 : Integer : s))
-> ((Unwrappabled r1 : Integer : s)
:-> (Maybe (Unwrappabled r2, Natural) : s))
-> (r1 : s) :-> (Maybe (Unwrappabled r2, Natural) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Unwrappabled r1 : Integer : s)
:-> (Maybe (Unwrappabled r2, Natural) : s)
forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv ((r1 : s) :-> (Maybe (Unwrappabled r2, Natural) : s))
-> ((Maybe (Unwrappabled r2, Natural) : s)
:-> ((Unwrappabled r2, Natural) : s))
-> (r1 : s) :-> ((Unwrappabled r2, Natural) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
Impossible "Division by zero impossible here"
-> (Maybe (Unwrappabled r2, Natural) : s)
:-> ((Unwrappabled r2, Natural) : s)
forall err a (s :: [*]).
IsError err =>
err -> (Maybe a : s) :-> (a : s)
assertSome (HasCallStack => Impossible "Division by zero impossible here"
forall (reason :: Symbol). HasCallStack => Impossible reason
Impossible @"Division by zero impossible here") ((r1 : s) :-> ((Unwrappabled r2, Natural) : s))
-> (((Unwrappabled r2, Natural) : s) :-> (Unwrappabled r2 : s))
-> (r1 : s) :-> (Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
case RoundingPattern
rp of
RoundingPattern
Round ->
((Unwrappabled r2, Natural) : s)
:-> (Unwrappabled r2 : Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair (((Unwrappabled r2, Natural) : s)
:-> (Unwrappabled r2 : Natural : s))
-> ((Unwrappabled r2 : Natural : s)
:-> (Natural : Unwrappabled r2 : s))
-> ((Unwrappabled r2, Natural) : s)
:-> (Natural : Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(Unwrappabled r2 : Natural : s) :-> (Natural : Unwrappabled r2 : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap (((Unwrappabled r2, Natural) : s)
:-> (Natural : Unwrappabled r2 : s))
-> ((Natural : Unwrappabled r2 : s)
:-> (Natural : Natural : Unwrappabled r2 : s))
-> ((Unwrappabled r2, Natural) : s)
:-> (Natural : Natural : Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
Natural
-> (Natural : Unwrappabled r2 : s)
:-> (Natural : Natural : Unwrappabled r2 : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Natural
halfNewPow (((Unwrappabled r2, Natural) : s)
:-> (Natural : Natural : Unwrappabled r2 : s))
-> ((Natural : Natural : Unwrappabled r2 : s)
:-> (Integer : Unwrappabled r2 : s))
-> ((Unwrappabled r2, Natural) : s)
:-> (Integer : Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(Natural : Natural : Unwrappabled r2 : s)
:-> (Integer : Unwrappabled r2 : s)
forall n (s :: [*]).
NiceComparable n =>
(n : n : s) :-> (Integer : s)
compare (((Unwrappabled r2, Natural) : s)
:-> (Integer : Unwrappabled r2 : s))
-> ((Integer : Unwrappabled r2 : s)
:-> (Integer : Integer : Unwrappabled r2 : s))
-> ((Unwrappabled r2, Natural) : s)
:-> (Integer : Integer : Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(Integer : Unwrappabled r2 : s)
:-> (Integer : Integer : Unwrappabled r2 : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup (((Unwrappabled r2, Natural) : s)
:-> (Integer : Integer : Unwrappabled r2 : s))
-> ((Integer : Integer : Unwrappabled r2 : s)
:-> (Unwrappabled r2 : s))
-> ((Unwrappabled r2, Natural) : s) :-> (Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((Integer : Unwrappabled r2 : s) :-> (Unwrappabled r2 : s))
-> ((Integer : Unwrappabled r2 : s) :-> (Unwrappabled r2 : s))
-> (Integer : Integer : Unwrappabled r2 : s)
:-> (Unwrappabled r2 : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Ge =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifGe0 (Integer : Unwrappabled r2 : s) :-> (Unwrappabled r2 : s)
forall a (s :: [*]). (a : s) :-> s
drop (
((Unwrappabled r2 : s) :-> (Natural : Unwrappabled r2 : s))
-> (Integer : Unwrappabled r2 : s)
:-> (Integer : Natural : Unwrappabled r2 : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Natural
-> (Unwrappabled r2 : s) :-> (Natural : Unwrappabled r2 : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Natural
1 :: Natural)) ((Integer : Unwrappabled r2 : s)
:-> (Integer : Natural : Unwrappabled r2 : s))
-> ((Integer : Natural : Unwrappabled r2 : s)
:-> (Natural : Unwrappabled r2 : s))
-> (Integer : Unwrappabled r2 : s)
:-> (Natural : Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((Natural : Unwrappabled r2 : s)
:-> (Natural : Unwrappabled r2 : s))
-> ((Natural : Unwrappabled r2 : s)
:-> (Natural : Unwrappabled r2 : s))
-> (Integer : Natural : Unwrappabled r2 : s)
:-> (Natural : Unwrappabled r2 : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Eq' =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifEq0 (forall a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano 2) inp out a, Dupable a) =>
inp :-> out
forall (n :: Nat) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @2 ((Natural : Unwrappabled r2 : s)
:-> (Unwrappabled r2 : Natural : Unwrappabled r2 : s))
-> ((Unwrappabled r2 : Natural : Unwrappabled r2 : s)
:-> (Natural : Unwrappabled r2 : s))
-> (Natural : Unwrappabled r2 : s)
:-> (Natural : Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Unwrappabled r2 : Natural : Unwrappabled r2 : s)
:-> (Natural : Unwrappabled r2 : s)
forall n m r (s :: [*]).
ArithOpHs And n m r =>
(n : m : s) :-> (r : s)
and) (Natural : Unwrappabled r2 : s) :-> (Natural : Unwrappabled r2 : s)
forall (s :: [*]). s :-> s
nop ((Integer : Unwrappabled r2 : s)
:-> (Natural : Unwrappabled r2 : s))
-> ((Natural : Unwrappabled r2 : s) :-> (Unwrappabled r2 : s))
-> (Integer : Unwrappabled r2 : s) :-> (Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(Natural : Unwrappabled r2 : s) :-> (Unwrappabled r2 : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
)
RoundingPattern
Ceil ->
((Unwrappabled r2, Natural) : s)
:-> (Unwrappabled r2 : Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair (((Unwrappabled r2, Natural) : s)
:-> (Unwrappabled r2 : Natural : s))
-> ((Unwrappabled r2 : Natural : s)
:-> (Natural : Unwrappabled r2 : s))
-> ((Unwrappabled r2, Natural) : s)
:-> (Natural : Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(Unwrappabled r2 : Natural : s) :-> (Natural : Unwrappabled r2 : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap (((Unwrappabled r2, Natural) : s)
:-> (Natural : Unwrappabled r2 : s))
-> ((Natural : Unwrappabled r2 : s) :-> (Unwrappabled r2 : s))
-> ((Unwrappabled r2, Natural) : s) :-> (Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((Unwrappabled r2 : s) :-> (Unwrappabled r2 : s))
-> ((Unwrappabled r2 : s) :-> (Unwrappabled r2 : s))
-> (Natural : Unwrappabled r2 : s) :-> (Unwrappabled r2 : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Neq =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifNeq0 (Integer
-> (Unwrappabled r2 : s) :-> (Integer : Unwrappabled r2 : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Integer
1 :: Integer) ((Unwrappabled r2 : s) :-> (Integer : Unwrappabled r2 : s))
-> ((Integer : Unwrappabled r2 : s) :-> (Unwrappabled r2 : s))
-> (Unwrappabled r2 : s) :-> (Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Unwrappabled r2 : s) :-> (Unwrappabled r2 : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add) (Unwrappabled r2 : s) :-> (Unwrappabled r2 : s)
forall (s :: [*]). s :-> s
nop
RoundingPattern
Floor -> ((Unwrappabled r2, Natural) : s) :-> (Unwrappabled r2 : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : s)
car
# unsafeCoerceWrap
fixedDivHelper
:: forall t1 t2 t3 base b1 b2 a r s.
( KnownNat t1, KnownNat t2, KnownNat t3
, Num base, NiceConstant base
, Unwrappable r, Unwrappable b1, Unwrappable a
, Unwrappabled a ~ base
, ArithOpHs Mul base r r
, ArithOpHs EDiv (Unwrappabled r) (Unwrappabled b1) (Maybe (base, b2))
, IsoValue a, Typeable a
)
=> base -> (r : b1 : s) :-> (Maybe a : s)
fixedDivHelper :: base -> (r : b1 : s) :-> (Maybe a : s)
fixedDivHelper base
base =
let powA :: Integer
powA = Proxy t1 -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (Proxy t1
forall k (t :: k). Proxy t
Proxy @t1)
powB :: Integer
powB = Proxy t2 -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (Proxy t2
forall k (t :: k). Proxy t
Proxy @t2)
powR :: base
powR = base
base base -> Integer -> base
forall a b. (Num a, Integral b) => a -> b -> a
^ (Proxy t3 -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (Proxy t3
forall k (t :: k). Proxy t
Proxy @t3) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
in
Integer -> (r : b1 : s) :-> (Integer : r : b1 : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Integer
powB ((r : b1 : s) :-> (Integer : r : b1 : s))
-> ((Integer : r : b1 : s) :-> (Integer : Integer : r : b1 : s))
-> (r : b1 : s) :-> (Integer : Integer : r : b1 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
Integer
-> (Integer : r : b1 : s) :-> (Integer : Integer : r : b1 : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Integer
powA ((r : b1 : s) :-> (Integer : Integer : r : b1 : s))
-> ((Integer : Integer : r : b1 : s) :-> (r : b1 : s))
-> (r : b1 : s) :-> (r : b1 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((r : b1 : s) :-> (r : b1 : s))
-> ((r : b1 : s) :-> (r : b1 : s))
-> (Integer : Integer : r : b1 : s) :-> (r : b1 : s)
forall a (s :: [*]) (s' :: [*]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a : a : s) :-> s'
ifGt (base -> (r : b1 : s) :-> (base : r : b1 : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push base
powR ((r : b1 : s) :-> (base : r : b1 : s))
-> ((base : r : b1 : s) :-> (r : b1 : s))
-> (r : b1 : s) :-> (r : b1 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (base : r : b1 : s) :-> (r : b1 : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul) (r : b1 : s) :-> (r : b1 : s)
forall (s :: [*]). s :-> s
nop ((r : b1 : s) :-> (r : b1 : s))
-> ((r : b1 : s) :-> (r : Unwrappabled b1 : s))
-> (r : b1 : s) :-> (r : Unwrappabled b1 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((b1 : s) :-> (Unwrappabled b1 : s))
-> (r : b1 : s) :-> (r : Unwrappabled b1 : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (b1 : s) :-> (Unwrappabled b1 : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((r : b1 : s) :-> (r : Unwrappabled b1 : s))
-> ((r : Unwrappabled b1 : s)
:-> (Unwrappabled r : Unwrappabled b1 : s))
-> (r : b1 : s) :-> (Unwrappabled r : Unwrappabled b1 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(r : Unwrappabled b1 : s)
:-> (Unwrappabled r : Unwrappabled b1 : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((r : b1 : s) :-> (Unwrappabled r : Unwrappabled b1 : s))
-> ((Unwrappabled r : Unwrappabled b1 : s)
:-> (Maybe (base, b2) : s))
-> (r : b1 : s) :-> (Maybe (base, b2) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
forall (s :: [*]).
ArithOpHs
EDiv (Unwrappabled r) (Unwrappabled b1) (Maybe (base, b2)) =>
(Unwrappabled r : Unwrappabled b1 : s) :-> (Maybe (base, b2) : s)
forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv @_ @_ @(Maybe (base, b2)) ((r : b1 : s) :-> (Maybe (base, b2) : s))
-> ((Maybe (base, b2) : s) :-> (Maybe a : s))
-> (r : b1 : s) :-> (Maybe a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(s :-> (Maybe a : s))
-> (((base, b2) : s) :-> (Maybe a : s))
-> (Maybe (base, b2) : s) :-> (Maybe a : s)
forall (s :: [*]) (s' :: [*]) a.
(s :-> s') -> ((a : s) :-> s') -> (Maybe a : s) :-> s'
ifNone (s :-> (Maybe a : s)
forall a (s :: [*]). KnownValue a => s :-> (Maybe a : s)
none) (((base, b2) : s) :-> (base : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : s)
car (((base, b2) : s) :-> (base : s))
-> ((base : s) :-> (a : s)) -> ((base, b2) : s) :-> (a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (base : s) :-> (a : s)
forall a (s :: [*]).
Unwrappable a =>
(Unwrappabled a : s) :-> (a : s)
unsafeCoerceWrap (((base, b2) : s) :-> (a : s))
-> ((a : s) :-> (Maybe a : s))
-> ((base, b2) : s) :-> (Maybe a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : s) :-> (Maybe a : s)
forall a (s :: [*]). (a : s) :-> (Maybe a : s)
some)
edivHelper
:: forall a base x y r1 r2 m s.
( KnownNat a, Num base, NiceConstant base, KnownValue r1, KnownValue r2, Dupable m
, UnaryArithOpHs Eq' m, ArithOpHs Mul base y m
, ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2))
, Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool
)
=> base -> (x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper :: base -> (x : y : s) :-> (Maybe (r1, r2) : s)
edivHelper base
base =
let powA :: base
powA = base
base base -> Integer -> base
forall a b. (Num a, Integral b) => a -> b -> a
^ (Proxy a -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
Lit.natVal (Proxy a
forall k (t :: k). Proxy t
Proxy @a))
in
(x : y : s) :-> (y : x : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((x : y : s) :-> (y : x : s))
-> ((y : x : s) :-> (base : y : x : s))
-> (x : y : s) :-> (base : y : x : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
base -> (y : x : s) :-> (base : y : x : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push base
powA ((x : y : s) :-> (base : y : x : s))
-> ((base : y : x : s) :-> (m : x : s))
-> (x : y : s) :-> (m : x : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(base : y : x : s) :-> (m : x : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul ((x : y : s) :-> (m : x : s))
-> ((m : x : s) :-> (m : m : x : s))
-> (x : y : s) :-> (m : m : x : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(m : x : s) :-> (m : m : x : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup ((x : y : s) :-> (m : m : x : s))
-> ((m : m : x : s) :-> (Maybe (r1, r2) : s))
-> (x : y : s) :-> (Maybe (r1, r2) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((m : x : s) :-> (Maybe (r1, r2) : s))
-> ((m : x : s) :-> (Maybe (r1, r2) : s))
-> (m : m : x : s) :-> (Maybe (r1, r2) : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Eq' =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifEq0 @m (forall (s :: [*]).
(SingI (ToPeano 2), RequireLongerOrSameLength (ToTs s) (ToPeano 2),
Drop (ToPeano 2) (ToTs s) ~ ToTs (Drop (ToPeano 2) s)) =>
s :-> Drop (ToPeano 2) s
forall (n :: Nat) (s :: [*]).
(SingI (ToPeano n), RequireLongerOrSameLength (ToTs s) (ToPeano n),
Drop (ToPeano n) (ToTs s) ~ ToTs (Drop (ToPeano n) s)) =>
s :-> Drop (ToPeano n) s
dropN @2 ((m : x : s) :-> s)
-> (s :-> (Maybe (r1, r2) : s))
-> (m : x : s) :-> (Maybe (r1, r2) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# s :-> (Maybe (r1, r2) : s)
forall a (s :: [*]). KnownValue a => s :-> (Maybe a : s)
none)
(
(m : x : s) :-> (x : m : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap ((m : x : s) :-> (x : m : s))
-> ((x : m : s) :-> (Unwrappabled x : m : s))
-> (m : x : s) :-> (Unwrappabled x : m : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(x : m : s) :-> (Unwrappabled x : m : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap ((m : x : s) :-> (Unwrappabled x : m : s))
-> ((Unwrappabled x : m : s) :-> (Maybe (r1, Unwrappabled r2) : s))
-> (m : x : s) :-> (Maybe (r1, Unwrappabled r2) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(Unwrappabled x : m : s) :-> (Maybe (r1, Unwrappabled r2) : s)
forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv ((m : x : s) :-> (Maybe (r1, Unwrappabled r2) : s))
-> ((Maybe (r1, Unwrappabled r2) : s)
:-> ((r1, Unwrappabled r2) : s))
-> (m : x : s) :-> ((r1, Unwrappabled r2) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
Impossible "Division by zero impossible here"
-> (Maybe (r1, Unwrappabled r2) : s)
:-> ((r1, Unwrappabled r2) : s)
forall err a (s :: [*]).
IsError err =>
err -> (Maybe a : s) :-> (a : s)
assertSome (HasCallStack => Impossible "Division by zero impossible here"
forall (reason :: Symbol). HasCallStack => Impossible reason
Impossible @"Division by zero impossible here") ((m : x : s) :-> ((r1, Unwrappabled r2) : s))
-> (((r1, Unwrappabled r2) : s) :-> (r1 : Unwrappabled r2 : s))
-> (m : x : s) :-> (r1 : Unwrappabled r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((r1, Unwrappabled r2) : s) :-> (r1 : Unwrappabled r2 : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair ((m : x : s) :-> (r1 : Unwrappabled r2 : s))
-> ((r1 : Unwrappabled r2 : s) :-> (r1 : r2 : s))
-> (m : x : s) :-> (r1 : r2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((Unwrappabled r2 : s) :-> (r2 : s))
-> (r1 : Unwrappabled r2 : s) :-> (r1 : r2 : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Unwrappabled r2 : s) :-> (r2 : s)
forall a (s :: [*]).
Unwrappable a =>
(Unwrappabled a : s) :-> (a : s)
unsafeCoerceWrap ((m : x : s) :-> (r1 : r2 : s))
-> ((r1 : r2 : s) :-> ((r1, r2) : s))
-> (m : x : s) :-> ((r1, r2) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(r1 : r2 : s) :-> ((r1, r2) : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair ((m : x : s) :-> ((r1, r2) : s))
-> (((r1, r2) : s) :-> (Maybe (r1, r2) : s))
-> (m : x : s) :-> (Maybe (r1, r2) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((r1, r2) : s) :-> (Maybe (r1, r2) : s)
forall a (s :: [*]). (a : s) :-> (Maybe a : s)
some
)