{-# LANGUAGE CPP
, KindSignatures
, DataKinds
, GADTs
, StandaloneDeriving
, ExistentialQuantification
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Types.Coercion
(
PrimCoercion(..)
, PrimCoerce(..)
, Coercion(..)
, singletonCoercion
, signed
, continuous
, Coerce(..)
, singCoerceDom
, singCoerceCod
, singCoerceDomCod
, CoercionMode(..)
, findCoercion
, findEitherCoercion
, Lub(..)
, findLub
, SomeRing(..)
, findRing
, SomeFractional(..)
, findFractional
, ZigZag(..)
, simplifyZZ
) where
import Prelude hiding (id, (.))
import Control.Category (Category(..))
#if __GLASGOW_HASKELL__ < 710
import Data.Functor ((<$>))
#endif
import Control.Applicative ((<|>))
import Language.Hakaru.Types.DataKind
import Language.Hakaru.Types.Sing
import Language.Hakaru.Types.HClasses
import Language.Hakaru.Syntax.IClasses
(TypeEq(..), Eq1(..), Eq2(..), JmEq1(..), JmEq2(..))
data PrimCoercion :: Hakaru -> Hakaru -> * where
Signed :: !(HRing a) -> PrimCoercion (NonNegative a) a
Continuous :: !(HContinuous a) -> PrimCoercion (HIntegral a) a
deriving instance Show (PrimCoercion a b)
instance Eq (PrimCoercion a b) where
== :: PrimCoercion a b -> PrimCoercion a b -> Bool
(==) = PrimCoercion a b -> PrimCoercion a b -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Eq1 (PrimCoercion a) where
eq1 :: PrimCoercion a i -> PrimCoercion a i -> Bool
eq1 = PrimCoercion a i -> PrimCoercion a i -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2
instance Eq2 PrimCoercion where
eq2 :: PrimCoercion i j -> PrimCoercion i j -> Bool
eq2 PrimCoercion i j
x PrimCoercion i j
y = Bool
-> ((TypeEq i i, TypeEq j j) -> Bool)
-> Maybe (TypeEq i i, TypeEq j j)
-> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> (TypeEq i i, TypeEq j j) -> Bool
forall a b. a -> b -> a
const Bool
True) (PrimCoercion i j
-> PrimCoercion i j -> Maybe (TypeEq i i, TypeEq j j)
forall k1 k2 (a :: k1 -> k2 -> *) (i1 :: k1) (j1 :: k2) (i2 :: k1)
(j2 :: k2).
JmEq2 a =>
a i1 j1 -> a i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 PrimCoercion i j
x PrimCoercion i j
y)
instance JmEq1 (PrimCoercion a) where
jmEq1 :: PrimCoercion a i -> PrimCoercion a j -> Maybe (TypeEq i j)
jmEq1 PrimCoercion a i
x PrimCoercion a j
y = (TypeEq a a, TypeEq i j) -> TypeEq i j
forall a b. (a, b) -> b
snd ((TypeEq a a, TypeEq i j) -> TypeEq i j)
-> Maybe (TypeEq a a, TypeEq i j) -> Maybe (TypeEq i j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PrimCoercion a i
-> PrimCoercion a j -> Maybe (TypeEq a a, TypeEq i j)
forall k1 k2 (a :: k1 -> k2 -> *) (i1 :: k1) (j1 :: k2) (i2 :: k1)
(j2 :: k2).
JmEq2 a =>
a i1 j1 -> a i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 PrimCoercion a i
x PrimCoercion a j
y
instance JmEq2 PrimCoercion where
jmEq2 :: PrimCoercion i1 j1
-> PrimCoercion i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 (Signed HRing j1
r1) (Signed HRing j2
r2) =
HRing j1 -> HRing j2 -> Maybe (TypeEq j1 j2)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HRing j1
r1 HRing j2
r2 Maybe (TypeEq j1 j2)
-> (TypeEq j1 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2))
-> Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq j1 j2
Refl -> (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 (Continuous HContinuous j1
c1) (Continuous HContinuous j2
c2) =
HContinuous j1 -> HContinuous j2 -> Maybe (TypeEq j1 j2)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HContinuous j1
c1 HContinuous j2
c2 Maybe (TypeEq j1 j2)
-> (TypeEq j1 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2))
-> Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq j1 j2
Refl -> (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimCoercion i1 j1
_ PrimCoercion i2 j2
_ = Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall a. Maybe a
Nothing
data Coercion :: Hakaru -> Hakaru -> * where
CNil :: Coercion a a
CCons :: !(PrimCoercion a b) -> !(Coercion b c) -> Coercion a c
infixr 5 `CCons`
deriving instance Show (Coercion a b)
instance Eq (Coercion a b) where
== :: Coercion a b -> Coercion a b -> Bool
(==) = Coercion a b -> Coercion a b -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Eq1 (Coercion a) where
eq1 :: Coercion a i -> Coercion a i -> Bool
eq1 = Coercion a i -> Coercion a i -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2
instance Eq2 Coercion where
eq2 :: Coercion i j -> Coercion i j -> Bool
eq2 Coercion i j
CNil Coercion i j
CNil = Bool
True
eq2 (CCons PrimCoercion i b
x Coercion b j
xs) (CCons PrimCoercion i b
y Coercion b j
ys) =
case PrimCoercion i b
-> PrimCoercion i b -> Maybe (TypeEq i i, TypeEq b b)
forall k1 k2 (a :: k1 -> k2 -> *) (i1 :: k1) (j1 :: k2) (i2 :: k1)
(j2 :: k2).
JmEq2 a =>
a i1 j1 -> a i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 PrimCoercion i b
x PrimCoercion i b
y of
Just (TypeEq i i
Refl, TypeEq b b
Refl) -> Coercion b j -> Coercion b j -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2 Coercion b j
xs Coercion b j
Coercion b j
ys
Maybe (TypeEq i i, TypeEq b b)
Nothing -> Bool
False
eq2 Coercion i j
_ Coercion i j
_ = Bool
False
instance Category Coercion where
id :: Coercion a a
id = Coercion a a
forall (a :: Hakaru). Coercion a a
CNil
Coercion b c
xs . :: Coercion b c -> Coercion a b -> Coercion a c
. Coercion a b
CNil = Coercion b c
Coercion a c
xs
Coercion b c
xs . CCons PrimCoercion a b
y Coercion b b
ys = PrimCoercion a b -> Coercion b c -> Coercion a c
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
PrimCoercion a b -> Coercion b c -> Coercion a c
CCons PrimCoercion a b
y (Coercion b c
xs Coercion b c -> Coercion b b -> Coercion b c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Coercion b b
ys)
singletonCoercion :: PrimCoercion a b -> Coercion a b
singletonCoercion :: PrimCoercion a b -> Coercion a b
singletonCoercion PrimCoercion a b
c = PrimCoercion a b -> Coercion b b -> Coercion a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
PrimCoercion a b -> Coercion b c -> Coercion a c
CCons PrimCoercion a b
c Coercion b b
forall (a :: Hakaru). Coercion a a
CNil
signed :: (HRing_ a) => Coercion (NonNegative a) a
signed :: Coercion (NonNegative a) a
signed = PrimCoercion (NonNegative a) a -> Coercion (NonNegative a) a
forall (a :: Hakaru) (b :: Hakaru).
PrimCoercion a b -> Coercion a b
singletonCoercion (PrimCoercion (NonNegative a) a -> Coercion (NonNegative a) a)
-> PrimCoercion (NonNegative a) a -> Coercion (NonNegative a) a
forall a b. (a -> b) -> a -> b
$ HRing a -> PrimCoercion (NonNegative a) a
forall (a :: Hakaru). HRing a -> PrimCoercion (NonNegative a) a
Signed HRing a
forall (a :: Hakaru). HRing_ a => HRing a
hRing
continuous :: (HContinuous_ a) => Coercion (HIntegral a) a
continuous :: Coercion (HIntegral a) a
continuous = PrimCoercion (HIntegral a) a -> Coercion (HIntegral a) a
forall (a :: Hakaru) (b :: Hakaru).
PrimCoercion a b -> Coercion a b
singletonCoercion (PrimCoercion (HIntegral a) a -> Coercion (HIntegral a) a)
-> PrimCoercion (HIntegral a) a -> Coercion (HIntegral a) a
forall a b. (a -> b) -> a -> b
$ HContinuous a -> PrimCoercion (HIntegral a) a
forall (a :: Hakaru). HContinuous a -> PrimCoercion (HIntegral a) a
Continuous HContinuous a
forall (a :: Hakaru). HContinuous_ a => HContinuous a
hContinuous
class PrimCoerce (f :: Hakaru -> *) where
primCoerceTo :: PrimCoercion a b -> f a -> f b
primCoerceFrom :: PrimCoercion a b -> f b -> f a
instance PrimCoerce (Sing :: Hakaru -> *) where
primCoerceTo :: PrimCoercion a b -> Sing a -> Sing b
primCoerceTo (Signed HRing b
theRing) Sing a
s =
case Sing a -> Sing a -> Maybe (TypeEq a a)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing a
s (HRing b -> Sing (NonNegative b)
forall (a :: Hakaru). HRing a -> Sing (NonNegative a)
sing_NonNegative HRing b
theRing) of
Just TypeEq a a
Refl -> HRing b -> Sing b
forall (a :: Hakaru). HRing a -> Sing a
sing_HRing HRing b
theRing
Maybe (TypeEq a a)
Nothing -> String -> Sing b
forall a. HasCallStack => String -> a
error String
"primCoerceTo@Sing: the impossible happened"
primCoerceTo (Continuous HContinuous b
theCont) Sing a
s =
case Sing a -> Sing a -> Maybe (TypeEq a a)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing a
s (HContinuous b -> Sing (HIntegral b)
forall (a :: Hakaru). HContinuous a -> Sing (HIntegral a)
sing_HIntegral HContinuous b
theCont) of
Just TypeEq a a
Refl -> HContinuous b -> Sing b
forall (a :: Hakaru). HContinuous a -> Sing a
sing_HContinuous HContinuous b
theCont
Maybe (TypeEq a a)
Nothing -> String -> Sing b
forall a. HasCallStack => String -> a
error String
"primCoerceTo@Sing: the impossible happened"
primCoerceFrom :: PrimCoercion a b -> Sing b -> Sing a
primCoerceFrom (Signed HRing b
theRing) Sing b
s =
case Sing b -> Sing b -> Maybe (TypeEq b b)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing b
s (HRing b -> Sing b
forall (a :: Hakaru). HRing a -> Sing a
sing_HRing HRing b
theRing) of
Just TypeEq b b
Refl -> HRing b -> Sing (NonNegative b)
forall (a :: Hakaru). HRing a -> Sing (NonNegative a)
sing_NonNegative HRing b
theRing
Maybe (TypeEq b b)
Nothing -> String -> Sing a
forall a. HasCallStack => String -> a
error String
"primCoerceFrom@Sing: the impossible happened"
primCoerceFrom (Continuous HContinuous b
theCont) Sing b
s =
case Sing b -> Sing b -> Maybe (TypeEq b b)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing b
s (HContinuous b -> Sing b
forall (a :: Hakaru). HContinuous a -> Sing a
sing_HContinuous HContinuous b
theCont) of
Just TypeEq b b
Refl -> HContinuous b -> Sing (HIntegral b)
forall (a :: Hakaru). HContinuous a -> Sing (HIntegral a)
sing_HIntegral HContinuous b
theCont
Maybe (TypeEq b b)
Nothing -> String -> Sing a
forall a. HasCallStack => String -> a
error String
"primCoerceFrom@Sing: the impossible happened"
class Coerce (f :: Hakaru -> *) where
coerceTo :: Coercion a b -> f a -> f b
coerceFrom :: Coercion a b -> f b -> f a
instance Coerce (Sing :: Hakaru -> *) where
coerceTo :: Coercion a b -> Sing a -> Sing b
coerceTo Coercion a b
CNil Sing a
s = Sing a
Sing b
s
coerceTo (CCons PrimCoercion a b
c Coercion b b
cs) Sing a
s = Coercion b b -> Sing b -> Sing b
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f a -> f b
coerceTo Coercion b b
cs (PrimCoercion a b -> Sing a -> Sing b
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
PrimCoerce f =>
PrimCoercion a b -> f a -> f b
primCoerceTo PrimCoercion a b
c Sing a
s)
coerceFrom :: Coercion a b -> Sing b -> Sing a
coerceFrom Coercion a b
CNil Sing b
s = Sing a
Sing b
s
coerceFrom (CCons PrimCoercion a b
c Coercion b b
cs) Sing b
s = PrimCoercion a b -> Sing b -> Sing a
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
PrimCoerce f =>
PrimCoercion a b -> f b -> f a
primCoerceFrom PrimCoercion a b
c (Coercion b b -> Sing b -> Sing b
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f b -> f a
coerceFrom Coercion b b
cs Sing b
s)
singPrimCoerceDom :: PrimCoercion a b -> Sing a
singPrimCoerceDom :: PrimCoercion a b -> Sing a
singPrimCoerceDom (Signed HRing b
theRing) = HRing b -> Sing (NonNegative b)
forall (a :: Hakaru). HRing a -> Sing (NonNegative a)
sing_NonNegative HRing b
theRing
singPrimCoerceDom (Continuous HContinuous b
theCont) = HContinuous b -> Sing (HIntegral b)
forall (a :: Hakaru). HContinuous a -> Sing (HIntegral a)
sing_HIntegral HContinuous b
theCont
singPrimCoerceCod :: PrimCoercion a b -> Sing b
singPrimCoerceCod :: PrimCoercion a b -> Sing b
singPrimCoerceCod (Signed HRing b
theRing) = HRing b -> Sing b
forall (a :: Hakaru). HRing a -> Sing a
sing_HRing HRing b
theRing
singPrimCoerceCod (Continuous HContinuous b
theCont) = HContinuous b -> Sing b
forall (a :: Hakaru). HContinuous a -> Sing a
sing_HContinuous HContinuous b
theCont
singCoerceDom :: Coercion a b -> Maybe (Sing a)
singCoerceDom :: Coercion a b -> Maybe (Sing a)
singCoerceDom Coercion a b
CNil = Maybe (Sing a)
forall a. Maybe a
Nothing
singCoerceDom (CCons PrimCoercion a b
c Coercion b b
CNil) = Sing a -> Maybe (Sing a)
forall a. a -> Maybe a
Just (Sing a -> Maybe (Sing a)) -> Sing a -> Maybe (Sing a)
forall a b. (a -> b) -> a -> b
$ PrimCoercion a b -> Sing a
forall (a :: Hakaru) (b :: Hakaru). PrimCoercion a b -> Sing a
singPrimCoerceDom PrimCoercion a b
c
singCoerceDom (CCons PrimCoercion a b
c Coercion b b
cs) = PrimCoercion a b -> Sing b -> Sing a
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
PrimCoerce f =>
PrimCoercion a b -> f b -> f a
primCoerceFrom PrimCoercion a b
c (Sing b -> Sing a) -> Maybe (Sing b) -> Maybe (Sing a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion b b -> Maybe (Sing b)
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> Maybe (Sing a)
singCoerceDom Coercion b b
cs
singCoerceCod :: Coercion a b -> Maybe (Sing b)
singCoerceCod :: Coercion a b -> Maybe (Sing b)
singCoerceCod Coercion a b
CNil = Maybe (Sing b)
forall a. Maybe a
Nothing
singCoerceCod (CCons PrimCoercion a b
c Coercion b b
CNil) = Sing b -> Maybe (Sing b)
forall a. a -> Maybe a
Just (Sing b -> Maybe (Sing b)) -> Sing b -> Maybe (Sing b)
forall a b. (a -> b) -> a -> b
$ PrimCoercion a b -> Sing b
forall (a :: Hakaru) (b :: Hakaru). PrimCoercion a b -> Sing b
singPrimCoerceCod PrimCoercion a b
c
singCoerceCod (CCons PrimCoercion a b
c Coercion b b
cs) = Sing b -> Maybe (Sing b)
forall a. a -> Maybe a
Just (Sing b -> Maybe (Sing b))
-> (Sing b -> Sing b) -> Sing b -> Maybe (Sing b)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Coercion b b -> Sing b -> Sing b
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f a -> f b
coerceTo Coercion b b
cs (Sing b -> Maybe (Sing b)) -> Sing b -> Maybe (Sing b)
forall a b. (a -> b) -> a -> b
$ PrimCoercion a b -> Sing b
forall (a :: Hakaru) (b :: Hakaru). PrimCoercion a b -> Sing b
singPrimCoerceCod PrimCoercion a b
c
singCoerceDomCod :: Coercion a b -> Maybe (Sing a, Sing b)
singCoerceDomCod :: Coercion a b -> Maybe (Sing a, Sing b)
singCoerceDomCod Coercion a b
CNil = Maybe (Sing a, Sing b)
forall a. Maybe a
Nothing
singCoerceDomCod (CCons PrimCoercion a b
c Coercion b b
CNil) =
(Sing a, Sing b) -> Maybe (Sing a, Sing b)
forall a. a -> Maybe a
Just (PrimCoercion a b -> Sing a
forall (a :: Hakaru) (b :: Hakaru). PrimCoercion a b -> Sing a
singPrimCoerceDom PrimCoercion a b
c, PrimCoercion a b -> Sing b
forall (a :: Hakaru) (b :: Hakaru). PrimCoercion a b -> Sing b
singPrimCoerceCod PrimCoercion a b
c)
singCoerceDomCod (CCons PrimCoercion a b
c Coercion b b
cs) = do
Sing b
dom <- Coercion b b -> Maybe (Sing b)
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> Maybe (Sing a)
singCoerceDom Coercion b b
cs
(Sing a, Sing b) -> Maybe (Sing a, Sing b)
forall a. a -> Maybe a
Just (PrimCoercion a b -> Sing b -> Sing a
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
PrimCoerce f =>
PrimCoercion a b -> f b -> f a
primCoerceFrom PrimCoercion a b
c Sing b
dom
, Coercion b b -> Sing b -> Sing b
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f a -> f b
coerceTo Coercion b b
cs (Sing b -> Sing b) -> Sing b -> Sing b
forall a b. (a -> b) -> a -> b
$ PrimCoercion a b -> Sing b
forall (a :: Hakaru) (b :: Hakaru). PrimCoercion a b -> Sing b
singPrimCoerceCod PrimCoercion a b
c
)
findCoercion :: Sing a -> Sing b -> Maybe (Coercion a b)
findCoercion :: Sing a -> Sing b -> Maybe (Coercion a b)
findCoercion Sing a
SNat Sing b
SInt = Coercion a b -> Maybe (Coercion a b)
forall a. a -> Maybe a
Just Coercion a b
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed
findCoercion Sing a
SProb Sing b
SReal = Coercion a b -> Maybe (Coercion a b)
forall a. a -> Maybe a
Just Coercion a b
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed
findCoercion Sing a
SNat Sing b
SProb = Coercion a b -> Maybe (Coercion a b)
forall a. a -> Maybe a
Just Coercion a b
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous
findCoercion Sing a
SInt Sing b
SReal = Coercion a b -> Maybe (Coercion a b)
forall a. a -> Maybe a
Just Coercion a b
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous
findCoercion Sing a
SNat Sing b
SReal = Coercion a b -> Maybe (Coercion a b)
forall a. a -> Maybe a
Just (Coercion 'HInt b
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous Coercion 'HInt b -> Coercion a 'HInt -> Coercion a b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Coercion a 'HInt
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed)
findCoercion Sing a
a Sing b
b = Sing a -> Sing b -> Maybe (TypeEq a b)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing a
a Sing b
b Maybe (TypeEq a b)
-> (TypeEq a b -> Maybe (Coercion a b)) -> Maybe (Coercion a b)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq a b
Refl -> Coercion a a -> Maybe (Coercion a a)
forall a. a -> Maybe a
Just Coercion a a
forall (a :: Hakaru). Coercion a a
CNil
findMixedCoercion
:: Sing a
-> Sing b
-> Maybe (Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
findMixedCoercion :: Sing a
-> Sing b -> Maybe (Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
findMixedCoercion Sing a
SProb Sing b
SInt = (Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
-> Maybe (Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
forall a. a -> Maybe a
Just (Sing 'HNat
SNat, Coercion 'HNat a
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous, Coercion 'HNat b
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed)
findMixedCoercion Sing a
SInt Sing b
SProb = (Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
-> Maybe (Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
forall a. a -> Maybe a
Just (Sing 'HNat
SNat, Coercion 'HNat a
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed, Coercion 'HNat b
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous)
findMixedCoercion Sing a
_ Sing b
_ = Maybe (Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
forall a. Maybe a
Nothing
data CoercionMode a b =
Safe (Coercion a b)
| Unsafe (Coercion b a)
| forall c. Mixed (Sing c, Coercion c a, Coercion c b)
findEitherCoercion
:: Sing a
-> Sing b
-> Maybe (CoercionMode a b)
findEitherCoercion :: Sing a -> Sing b -> Maybe (CoercionMode a b)
findEitherCoercion Sing a
a Sing b
b =
(Coercion a b -> CoercionMode a b
forall (a :: Hakaru) (b :: Hakaru).
Coercion a b -> CoercionMode a b
Safe (Coercion a b -> CoercionMode a b)
-> Maybe (Coercion a b) -> Maybe (CoercionMode a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing a -> Sing b -> Maybe (Coercion a b)
forall (a :: Hakaru) (b :: Hakaru).
Sing a -> Sing b -> Maybe (Coercion a b)
findCoercion Sing a
a Sing b
b) Maybe (CoercionMode a b)
-> Maybe (CoercionMode a b) -> Maybe (CoercionMode a b)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
(Coercion b a -> CoercionMode a b
forall (a :: Hakaru) (b :: Hakaru).
Coercion b a -> CoercionMode a b
Unsafe (Coercion b a -> CoercionMode a b)
-> Maybe (Coercion b a) -> Maybe (CoercionMode a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing b -> Sing a -> Maybe (Coercion b a)
forall (a :: Hakaru) (b :: Hakaru).
Sing a -> Sing b -> Maybe (Coercion a b)
findCoercion Sing b
b Sing a
a) Maybe (CoercionMode a b)
-> Maybe (CoercionMode a b) -> Maybe (CoercionMode a b)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
((Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
-> CoercionMode a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
(Sing c, Coercion c a, Coercion c b) -> CoercionMode a b
Mixed ((Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
-> CoercionMode a b)
-> Maybe (Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
-> Maybe (CoercionMode a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing a
-> Sing b -> Maybe (Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
forall (a :: Hakaru) (b :: Hakaru).
Sing a
-> Sing b -> Maybe (Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
findMixedCoercion Sing a
a Sing b
b)
data Lub (a :: Hakaru) (b :: Hakaru)
= forall c. Lub !(Sing c) !(Coercion a c) !(Coercion b c)
findLub :: Sing a -> Sing b -> Maybe (Lub a b)
findLub :: Sing a -> Sing b -> Maybe (Lub a b)
findLub Sing a
SNat Sing b
SInt = Lub a 'HInt -> Maybe (Lub a 'HInt)
forall a. a -> Maybe a
Just (Lub a 'HInt -> Maybe (Lub a 'HInt))
-> Lub a 'HInt -> Maybe (Lub a 'HInt)
forall a b. (a -> b) -> a -> b
$ Sing 'HInt
-> Coercion a 'HInt -> Coercion 'HInt 'HInt -> Lub a 'HInt
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HInt
SInt Coercion a 'HInt
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed Coercion 'HInt 'HInt
forall (a :: Hakaru). Coercion a a
CNil
findLub Sing a
SProb Sing b
SReal = Lub a 'HReal -> Maybe (Lub a 'HReal)
forall a. a -> Maybe a
Just (Lub a 'HReal -> Maybe (Lub a 'HReal))
-> Lub a 'HReal -> Maybe (Lub a 'HReal)
forall a b. (a -> b) -> a -> b
$ Sing 'HReal
-> Coercion a 'HReal -> Coercion 'HReal 'HReal -> Lub a 'HReal
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HReal
SReal Coercion a 'HReal
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed Coercion 'HReal 'HReal
forall (a :: Hakaru). Coercion a a
CNil
findLub Sing a
SNat Sing b
SProb = Lub a 'HProb -> Maybe (Lub a 'HProb)
forall a. a -> Maybe a
Just (Lub a 'HProb -> Maybe (Lub a 'HProb))
-> Lub a 'HProb -> Maybe (Lub a 'HProb)
forall a b. (a -> b) -> a -> b
$ Sing 'HProb
-> Coercion a 'HProb -> Coercion 'HProb 'HProb -> Lub a 'HProb
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HProb
SProb Coercion a 'HProb
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous Coercion 'HProb 'HProb
forall (a :: Hakaru). Coercion a a
CNil
findLub Sing a
SInt Sing b
SReal = Lub a 'HReal -> Maybe (Lub a 'HReal)
forall a. a -> Maybe a
Just (Lub a 'HReal -> Maybe (Lub a 'HReal))
-> Lub a 'HReal -> Maybe (Lub a 'HReal)
forall a b. (a -> b) -> a -> b
$ Sing 'HReal
-> Coercion a 'HReal -> Coercion 'HReal 'HReal -> Lub a 'HReal
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HReal
SReal Coercion a 'HReal
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous Coercion 'HReal 'HReal
forall (a :: Hakaru). Coercion a a
CNil
findLub Sing a
SNat Sing b
SReal = Lub a 'HReal -> Maybe (Lub a 'HReal)
forall a. a -> Maybe a
Just (Lub a 'HReal -> Maybe (Lub a 'HReal))
-> Lub a 'HReal -> Maybe (Lub a 'HReal)
forall a b. (a -> b) -> a -> b
$ Sing 'HReal
-> Coercion a 'HReal -> Coercion 'HReal 'HReal -> Lub a 'HReal
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HReal
SReal (Coercion 'HInt 'HReal
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous Coercion 'HInt 'HReal -> Coercion a 'HInt -> Coercion a 'HReal
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Coercion a 'HInt
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed) Coercion 'HReal 'HReal
forall (a :: Hakaru). Coercion a a
CNil
findLub Sing a
SInt Sing b
SNat = Lub 'HInt b -> Maybe (Lub 'HInt b)
forall a. a -> Maybe a
Just (Lub 'HInt b -> Maybe (Lub 'HInt b))
-> Lub 'HInt b -> Maybe (Lub 'HInt b)
forall a b. (a -> b) -> a -> b
$ Sing 'HInt
-> Coercion 'HInt 'HInt -> Coercion b 'HInt -> Lub 'HInt b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HInt
SInt Coercion 'HInt 'HInt
forall (a :: Hakaru). Coercion a a
CNil Coercion b 'HInt
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed
findLub Sing a
SReal Sing b
SProb = Lub 'HReal b -> Maybe (Lub 'HReal b)
forall a. a -> Maybe a
Just (Lub 'HReal b -> Maybe (Lub 'HReal b))
-> Lub 'HReal b -> Maybe (Lub 'HReal b)
forall a b. (a -> b) -> a -> b
$ Sing 'HReal
-> Coercion 'HReal 'HReal -> Coercion b 'HReal -> Lub 'HReal b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HReal
SReal Coercion 'HReal 'HReal
forall (a :: Hakaru). Coercion a a
CNil Coercion b 'HReal
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed
findLub Sing a
SProb Sing b
SNat = Lub 'HProb b -> Maybe (Lub 'HProb b)
forall a. a -> Maybe a
Just (Lub 'HProb b -> Maybe (Lub 'HProb b))
-> Lub 'HProb b -> Maybe (Lub 'HProb b)
forall a b. (a -> b) -> a -> b
$ Sing 'HProb
-> Coercion 'HProb 'HProb -> Coercion b 'HProb -> Lub 'HProb b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HProb
SProb Coercion 'HProb 'HProb
forall (a :: Hakaru). Coercion a a
CNil Coercion b 'HProb
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous
findLub Sing a
SReal Sing b
SInt = Lub 'HReal b -> Maybe (Lub 'HReal b)
forall a. a -> Maybe a
Just (Lub 'HReal b -> Maybe (Lub 'HReal b))
-> Lub 'HReal b -> Maybe (Lub 'HReal b)
forall a b. (a -> b) -> a -> b
$ Sing 'HReal
-> Coercion 'HReal 'HReal -> Coercion b 'HReal -> Lub 'HReal b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HReal
SReal Coercion 'HReal 'HReal
forall (a :: Hakaru). Coercion a a
CNil Coercion b 'HReal
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous
findLub Sing a
SReal Sing b
SNat = Lub 'HReal b -> Maybe (Lub 'HReal b)
forall a. a -> Maybe a
Just (Lub 'HReal b -> Maybe (Lub 'HReal b))
-> Lub 'HReal b -> Maybe (Lub 'HReal b)
forall a b. (a -> b) -> a -> b
$ Sing 'HReal
-> Coercion 'HReal 'HReal -> Coercion b 'HReal -> Lub 'HReal b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HReal
SReal Coercion 'HReal 'HReal
forall (a :: Hakaru). Coercion a a
CNil (Coercion 'HInt 'HReal
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous Coercion 'HInt 'HReal -> Coercion b 'HInt -> Coercion b 'HReal
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Coercion b 'HInt
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed)
findLub Sing a
SInt Sing b
SProb = Lub a b -> Maybe (Lub a b)
forall a. a -> Maybe a
Just (Lub a b -> Maybe (Lub a b)) -> Lub a b -> Maybe (Lub a b)
forall a b. (a -> b) -> a -> b
$ Sing 'HReal -> Coercion a 'HReal -> Coercion b 'HReal -> Lub a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HReal
SReal Coercion a 'HReal
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous Coercion b 'HReal
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed
findLub Sing a
SProb Sing b
SInt = Lub a b -> Maybe (Lub a b)
forall a. a -> Maybe a
Just (Lub a b -> Maybe (Lub a b)) -> Lub a b -> Maybe (Lub a b)
forall a b. (a -> b) -> a -> b
$ Sing 'HReal -> Coercion a 'HReal -> Coercion b 'HReal -> Lub a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HReal
SReal Coercion a 'HReal
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed Coercion b 'HReal
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous
findLub Sing a
a Sing b
b = Sing a -> Sing b -> Maybe (TypeEq a b)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing a
a Sing b
b Maybe (TypeEq a b)
-> (TypeEq a b -> Maybe (Lub a b)) -> Maybe (Lub a b)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq a b
Refl -> Lub a a -> Maybe (Lub a a)
forall a. a -> Maybe a
Just (Lub a a -> Maybe (Lub a a)) -> Lub a a -> Maybe (Lub a a)
forall a b. (a -> b) -> a -> b
$ Sing a -> Coercion a a -> Coercion a a -> Lub a a
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing a
a Coercion a a
forall (a :: Hakaru). Coercion a a
CNil Coercion a a
forall (a :: Hakaru). Coercion a a
CNil
data SomeRing (a :: Hakaru)
= forall b. SomeRing !(HRing b) !(Coercion a b)
findRing :: Sing a -> Maybe (SomeRing a)
findRing :: Sing a -> Maybe (SomeRing a)
findRing Sing a
SNat = SomeRing a -> Maybe (SomeRing a)
forall a. a -> Maybe a
Just (HRing 'HInt -> Coercion a 'HInt -> SomeRing a
forall (a :: Hakaru) (b :: Hakaru).
HRing b -> Coercion a b -> SomeRing a
SomeRing HRing 'HInt
HRing_Int Coercion a 'HInt
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed)
findRing Sing a
SInt = SomeRing 'HInt -> Maybe (SomeRing 'HInt)
forall a. a -> Maybe a
Just (HRing 'HInt -> Coercion 'HInt 'HInt -> SomeRing 'HInt
forall (a :: Hakaru) (b :: Hakaru).
HRing b -> Coercion a b -> SomeRing a
SomeRing HRing 'HInt
HRing_Int Coercion 'HInt 'HInt
forall (a :: Hakaru). Coercion a a
CNil)
findRing Sing a
SProb = SomeRing a -> Maybe (SomeRing a)
forall a. a -> Maybe a
Just (HRing 'HReal -> Coercion a 'HReal -> SomeRing a
forall (a :: Hakaru) (b :: Hakaru).
HRing b -> Coercion a b -> SomeRing a
SomeRing HRing 'HReal
HRing_Real Coercion a 'HReal
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed)
findRing Sing a
SReal = SomeRing 'HReal -> Maybe (SomeRing 'HReal)
forall a. a -> Maybe a
Just (HRing 'HReal -> Coercion 'HReal 'HReal -> SomeRing 'HReal
forall (a :: Hakaru) (b :: Hakaru).
HRing b -> Coercion a b -> SomeRing a
SomeRing HRing 'HReal
HRing_Real Coercion 'HReal 'HReal
forall (a :: Hakaru). Coercion a a
CNil)
findRing Sing a
_ = Maybe (SomeRing a)
forall a. Maybe a
Nothing
data SomeFractional (a :: Hakaru)
= forall b. SomeFractional !(HFractional b) !(Coercion a b)
findFractional :: Sing a -> Maybe (SomeFractional a)
findFractional :: Sing a -> Maybe (SomeFractional a)
findFractional Sing a
SNat = SomeFractional a -> Maybe (SomeFractional a)
forall a. a -> Maybe a
Just (HFractional 'HProb -> Coercion a 'HProb -> SomeFractional a
forall (a :: Hakaru) (b :: Hakaru).
HFractional b -> Coercion a b -> SomeFractional a
SomeFractional HFractional 'HProb
HFractional_Prob Coercion a 'HProb
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous)
findFractional Sing a
SInt = SomeFractional a -> Maybe (SomeFractional a)
forall a. a -> Maybe a
Just (HFractional 'HReal -> Coercion a 'HReal -> SomeFractional a
forall (a :: Hakaru) (b :: Hakaru).
HFractional b -> Coercion a b -> SomeFractional a
SomeFractional HFractional 'HReal
HFractional_Real Coercion a 'HReal
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous)
findFractional Sing a
SProb = SomeFractional 'HProb -> Maybe (SomeFractional 'HProb)
forall a. a -> Maybe a
Just (HFractional 'HProb
-> Coercion 'HProb 'HProb -> SomeFractional 'HProb
forall (a :: Hakaru) (b :: Hakaru).
HFractional b -> Coercion a b -> SomeFractional a
SomeFractional HFractional 'HProb
HFractional_Prob Coercion 'HProb 'HProb
forall (a :: Hakaru). Coercion a a
CNil)
findFractional Sing a
SReal = SomeFractional 'HReal -> Maybe (SomeFractional 'HReal)
forall a. a -> Maybe a
Just (HFractional 'HReal
-> Coercion 'HReal 'HReal -> SomeFractional 'HReal
forall (a :: Hakaru) (b :: Hakaru).
HFractional b -> Coercion a b -> SomeFractional a
SomeFractional HFractional 'HReal
HFractional_Real Coercion 'HReal 'HReal
forall (a :: Hakaru). Coercion a a
CNil)
findFractional Sing a
_ = Maybe (SomeFractional a)
forall a. Maybe a
Nothing
data CoerceTo_UnsafeFrom :: Hakaru -> Hakaru -> * where
CTUF :: !(Coercion b c) -> !(Coercion b a) -> CoerceTo_UnsafeFrom a c
deriving instance Show (CoerceTo_UnsafeFrom a b)
simplifyCTUF :: CoerceTo_UnsafeFrom a c -> CoerceTo_UnsafeFrom a c
simplifyCTUF :: CoerceTo_UnsafeFrom a c -> CoerceTo_UnsafeFrom a c
simplifyCTUF (CTUF Coercion b c
xs Coercion b a
ys) =
case Coercion b c
xs of
Coercion b c
CNil -> Coercion b b -> Coercion b a -> CoerceTo_UnsafeFrom a b
forall (b :: Hakaru) (c :: Hakaru) (a :: Hakaru).
Coercion b c -> Coercion b a -> CoerceTo_UnsafeFrom a c
CTUF Coercion b b
forall (a :: Hakaru). Coercion a a
CNil Coercion b a
ys
CCons PrimCoercion b b
x Coercion b c
xs' ->
case Coercion b a
ys of
Coercion b a
CNil -> Coercion b c -> Coercion b b -> CoerceTo_UnsafeFrom b c
forall (b :: Hakaru) (c :: Hakaru) (a :: Hakaru).
Coercion b c -> Coercion b a -> CoerceTo_UnsafeFrom a c
CTUF Coercion b c
xs Coercion b b
forall (a :: Hakaru). Coercion a a
CNil
CCons PrimCoercion b b
y Coercion b a
ys' ->
case PrimCoercion b b
-> PrimCoercion b b -> Maybe (TypeEq b b, TypeEq b b)
forall k1 k2 (a :: k1 -> k2 -> *) (i1 :: k1) (j1 :: k2) (i2 :: k1)
(j2 :: k2).
JmEq2 a =>
a i1 j1 -> a i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 PrimCoercion b b
x PrimCoercion b b
y of
Just (TypeEq b b
Refl, TypeEq b b
Refl) -> CoerceTo_UnsafeFrom a c -> CoerceTo_UnsafeFrom a c
forall (a :: Hakaru) (c :: Hakaru).
CoerceTo_UnsafeFrom a c -> CoerceTo_UnsafeFrom a c
simplifyCTUF (Coercion b c -> Coercion b a -> CoerceTo_UnsafeFrom a c
forall (b :: Hakaru) (c :: Hakaru) (a :: Hakaru).
Coercion b c -> Coercion b a -> CoerceTo_UnsafeFrom a c
CTUF Coercion b c
xs' Coercion b a
Coercion b a
ys')
Maybe (TypeEq b b, TypeEq b b)
Nothing -> Coercion b c -> Coercion b a -> CoerceTo_UnsafeFrom a c
forall (b :: Hakaru) (c :: Hakaru) (a :: Hakaru).
Coercion b c -> Coercion b a -> CoerceTo_UnsafeFrom a c
CTUF Coercion b c
xs Coercion b a
ys
data RevCoercion :: Hakaru -> Hakaru -> * where
CLin :: RevCoercion a a
CSnoc :: !(RevCoercion a b) -> !(PrimCoercion b c) -> RevCoercion a c
deriving instance Show (RevCoercion a b)
instance Category RevCoercion where
id :: RevCoercion a a
id = RevCoercion a a
forall (a :: Hakaru). RevCoercion a a
CLin
RevCoercion b c
CLin . :: RevCoercion b c -> RevCoercion a b -> RevCoercion a c
. RevCoercion a b
xs = RevCoercion a b
RevCoercion a c
xs
CSnoc RevCoercion b b
ys PrimCoercion b c
y . RevCoercion a b
xs = RevCoercion a b -> PrimCoercion b c -> RevCoercion a c
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
RevCoercion a b -> PrimCoercion b c -> RevCoercion a c
CSnoc (RevCoercion b b
ys RevCoercion b b -> RevCoercion a b -> RevCoercion a b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. RevCoercion a b
xs) PrimCoercion b c
y
revCons :: PrimCoercion a b -> RevCoercion b c -> RevCoercion a c
revCons :: PrimCoercion a b -> RevCoercion b c -> RevCoercion a c
revCons PrimCoercion a b
x RevCoercion b c
CLin = RevCoercion a a -> PrimCoercion a b -> RevCoercion a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
RevCoercion a b -> PrimCoercion b c -> RevCoercion a c
CSnoc RevCoercion a a
forall (a :: Hakaru). RevCoercion a a
CLin PrimCoercion a b
x
revCons PrimCoercion a b
x (CSnoc RevCoercion b b
ys PrimCoercion b c
y) = RevCoercion a b -> PrimCoercion b c -> RevCoercion a c
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
RevCoercion a b -> PrimCoercion b c -> RevCoercion a c
CSnoc (PrimCoercion a b -> RevCoercion b b -> RevCoercion a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
PrimCoercion a b -> RevCoercion b c -> RevCoercion a c
revCons PrimCoercion a b
x RevCoercion b b
ys) PrimCoercion b c
y
toRev :: Coercion a b -> RevCoercion a b
toRev :: Coercion a b -> RevCoercion a b
toRev Coercion a b
CNil = RevCoercion a b
forall (a :: Hakaru). RevCoercion a a
CLin
toRev (CCons PrimCoercion a b
x Coercion b b
xs) = PrimCoercion a b -> RevCoercion b b -> RevCoercion a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
PrimCoercion a b -> RevCoercion b c -> RevCoercion a c
revCons PrimCoercion a b
x (Coercion b b -> RevCoercion b b
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> RevCoercion a b
toRev Coercion b b
xs)
obvSnoc :: Coercion a b -> PrimCoercion b c -> Coercion a c
obvSnoc :: Coercion a b -> PrimCoercion b c -> Coercion a c
obvSnoc Coercion a b
CNil PrimCoercion b c
y = PrimCoercion b c -> Coercion c c -> Coercion b c
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
PrimCoercion a b -> Coercion b c -> Coercion a c
CCons PrimCoercion b c
y Coercion c c
forall (a :: Hakaru). Coercion a a
CNil
obvSnoc (CCons PrimCoercion a b
x Coercion b b
xs) PrimCoercion b c
y = PrimCoercion a b -> Coercion b c -> Coercion a c
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
PrimCoercion a b -> Coercion b c -> Coercion a c
CCons PrimCoercion a b
x (Coercion b b -> PrimCoercion b c -> Coercion b c
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Coercion a b -> PrimCoercion b c -> Coercion a c
obvSnoc Coercion b b
xs PrimCoercion b c
y)
fromRev :: RevCoercion a b -> Coercion a b
fromRev :: RevCoercion a b -> Coercion a b
fromRev RevCoercion a b
CLin = Coercion a b
forall (a :: Hakaru). Coercion a a
CNil
fromRev (CSnoc RevCoercion a b
xs PrimCoercion b b
x) = Coercion a b -> PrimCoercion b b -> Coercion a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Coercion a b -> PrimCoercion b c -> Coercion a c
obvSnoc (RevCoercion a b -> Coercion a b
forall (a :: Hakaru) (b :: Hakaru). RevCoercion a b -> Coercion a b
fromRev RevCoercion a b
xs) PrimCoercion b b
x
data UnsafeFrom_CoerceTo :: Hakaru -> Hakaru -> * where
UFCT
:: !(Coercion c b)
-> !(Coercion a b)
-> UnsafeFrom_CoerceTo a c
deriving instance Show (UnsafeFrom_CoerceTo a b)
data RevUFCT :: Hakaru -> Hakaru -> * where
RevUFCT :: !(RevCoercion c b) -> !(RevCoercion a b) -> RevUFCT a c
simplifyUFCT :: UnsafeFrom_CoerceTo a c -> UnsafeFrom_CoerceTo a c
simplifyUFCT :: UnsafeFrom_CoerceTo a c -> UnsafeFrom_CoerceTo a c
simplifyUFCT (UFCT Coercion c b
xs Coercion a b
ys) =
case RevUFCT a c -> RevUFCT a c
forall (a :: Hakaru) (c :: Hakaru). RevUFCT a c -> RevUFCT a c
simplifyRevUFCT (RevUFCT a c -> RevUFCT a c) -> RevUFCT a c -> RevUFCT a c
forall a b. (a -> b) -> a -> b
$ RevCoercion c b -> RevCoercion a b -> RevUFCT a c
forall (c :: Hakaru) (b :: Hakaru) (a :: Hakaru).
RevCoercion c b -> RevCoercion a b -> RevUFCT a c
RevUFCT (Coercion c b -> RevCoercion c b
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> RevCoercion a b
toRev Coercion c b
xs) (Coercion a b -> RevCoercion a b
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> RevCoercion a b
toRev Coercion a b
ys) of
RevUFCT RevCoercion c b
xs' RevCoercion a b
ys' -> Coercion c b -> Coercion a b -> UnsafeFrom_CoerceTo a c
forall (c :: Hakaru) (b :: Hakaru) (a :: Hakaru).
Coercion c b -> Coercion a b -> UnsafeFrom_CoerceTo a c
UFCT (RevCoercion c b -> Coercion c b
forall (a :: Hakaru) (b :: Hakaru). RevCoercion a b -> Coercion a b
fromRev RevCoercion c b
xs') (RevCoercion a b -> Coercion a b
forall (a :: Hakaru) (b :: Hakaru). RevCoercion a b -> Coercion a b
fromRev RevCoercion a b
ys')
simplifyRevUFCT :: RevUFCT a c -> RevUFCT a c
simplifyRevUFCT :: RevUFCT a c -> RevUFCT a c
simplifyRevUFCT (RevUFCT RevCoercion c b
xs RevCoercion a b
ys) =
case RevCoercion c b
xs of
RevCoercion c b
CLin -> RevCoercion b b -> RevCoercion a b -> RevUFCT a b
forall (c :: Hakaru) (b :: Hakaru) (a :: Hakaru).
RevCoercion c b -> RevCoercion a b -> RevUFCT a c
RevUFCT RevCoercion b b
forall (a :: Hakaru). RevCoercion a a
CLin RevCoercion a b
ys
CSnoc RevCoercion c b
xs' PrimCoercion b b
x ->
case RevCoercion a b
ys of
RevCoercion a b
CLin -> RevCoercion c b -> RevCoercion b b -> RevUFCT b c
forall (c :: Hakaru) (b :: Hakaru) (a :: Hakaru).
RevCoercion c b -> RevCoercion a b -> RevUFCT a c
RevUFCT RevCoercion c b
xs RevCoercion b b
forall (a :: Hakaru). RevCoercion a a
CLin
CSnoc RevCoercion a b
ys' PrimCoercion b b
y ->
case PrimCoercion b b
-> PrimCoercion b b -> Maybe (TypeEq b b, TypeEq b b)
forall k1 k2 (a :: k1 -> k2 -> *) (i1 :: k1) (j1 :: k2) (i2 :: k1)
(j2 :: k2).
JmEq2 a =>
a i1 j1 -> a i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 PrimCoercion b b
x PrimCoercion b b
y of
Just (TypeEq b b
Refl, TypeEq b b
Refl) -> RevUFCT a c -> RevUFCT a c
forall (a :: Hakaru) (c :: Hakaru). RevUFCT a c -> RevUFCT a c
simplifyRevUFCT (RevCoercion c b -> RevCoercion a b -> RevUFCT a c
forall (c :: Hakaru) (b :: Hakaru) (a :: Hakaru).
RevCoercion c b -> RevCoercion a b -> RevUFCT a c
RevUFCT RevCoercion c b
xs' RevCoercion a b
RevCoercion a b
ys')
Maybe (TypeEq b b, TypeEq b b)
Nothing -> RevCoercion c b -> RevCoercion a b -> RevUFCT a c
forall (c :: Hakaru) (b :: Hakaru) (a :: Hakaru).
RevCoercion c b -> RevCoercion a b -> RevUFCT a c
RevUFCT RevCoercion c b
xs RevCoercion a b
ys
data ZigZag :: Hakaru -> Hakaru -> * where
ZRefl :: ZigZag a a
Zig :: !(Coercion a b) -> !(ZigZag b c) -> ZigZag a c
Zag :: !(Coercion b a) -> !(ZigZag b c) -> ZigZag a c
deriving instance Show (ZigZag a b)
simplifyZZ :: ZigZag a b -> ZigZag a b
simplifyZZ :: ZigZag a b -> ZigZag a b
simplifyZZ ZigZag a b
ZRefl = ZigZag a b
forall (a :: Hakaru). ZigZag a a
ZRefl
simplifyZZ (Zig Coercion a b
x ZigZag b b
xs) =
case ZigZag b b -> ZigZag b b
forall (a :: Hakaru) (b :: Hakaru). ZigZag a b -> ZigZag a b
simplifyZZ ZigZag b b
xs of
ZigZag b b
ZRefl -> Coercion a b -> ZigZag b b -> ZigZag a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Coercion a b -> ZigZag b c -> ZigZag a c
Zig Coercion a b
x ZigZag b b
forall (a :: Hakaru). ZigZag a a
ZRefl
Zig Coercion b b
y ZigZag b b
z -> Coercion a b -> ZigZag b b -> ZigZag a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Coercion a b -> ZigZag b c -> ZigZag a c
Zig (Coercion b b
y Coercion b b -> Coercion a b -> Coercion a b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Coercion a b
x) ZigZag b b
z
Zag Coercion b b
y ZigZag b b
z ->
case UnsafeFrom_CoerceTo b a -> UnsafeFrom_CoerceTo b a
forall (a :: Hakaru) (c :: Hakaru).
UnsafeFrom_CoerceTo a c -> UnsafeFrom_CoerceTo a c
simplifyUFCT (Coercion a b -> Coercion b b -> UnsafeFrom_CoerceTo b a
forall (c :: Hakaru) (b :: Hakaru) (a :: Hakaru).
Coercion c b -> Coercion a b -> UnsafeFrom_CoerceTo a c
UFCT Coercion a b
x Coercion b b
y) of
UFCT Coercion a b
CNil Coercion b b
CNil -> ZigZag a b
ZigZag b b
z
UFCT Coercion a b
CNil Coercion b b
y' -> Coercion b b -> ZigZag b b -> ZigZag b b
forall (b :: Hakaru) (a :: Hakaru) (c :: Hakaru).
Coercion b a -> ZigZag b c -> ZigZag a c
Zag Coercion b b
y' ZigZag b b
z
UFCT Coercion a b
x' Coercion b b
CNil -> Coercion a b -> ZigZag b b -> ZigZag a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Coercion a b -> ZigZag b c -> ZigZag a c
Zig Coercion a b
x' ZigZag b b
ZigZag b b
z
UFCT Coercion a b
x' Coercion b b
y' -> Coercion a b -> ZigZag b b -> ZigZag a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Coercion a b -> ZigZag b c -> ZigZag a c
Zig Coercion a b
x' (Coercion b b -> ZigZag b b -> ZigZag b b
forall (b :: Hakaru) (a :: Hakaru) (c :: Hakaru).
Coercion b a -> ZigZag b c -> ZigZag a c
Zag Coercion b b
y' ZigZag b b
z)
simplifyZZ (Zag Coercion b a
x ZigZag b b
xs) =
case ZigZag b b -> ZigZag b b
forall (a :: Hakaru) (b :: Hakaru). ZigZag a b -> ZigZag a b
simplifyZZ ZigZag b b
xs of
ZigZag b b
ZRefl -> Coercion b a -> ZigZag b b -> ZigZag a b
forall (b :: Hakaru) (a :: Hakaru) (c :: Hakaru).
Coercion b a -> ZigZag b c -> ZigZag a c
Zag Coercion b a
x ZigZag b b
forall (a :: Hakaru). ZigZag a a
ZRefl
Zag Coercion b b
y ZigZag b b
z -> Coercion b a -> ZigZag b b -> ZigZag a b
forall (b :: Hakaru) (a :: Hakaru) (c :: Hakaru).
Coercion b a -> ZigZag b c -> ZigZag a c
Zag (Coercion b a
x Coercion b a -> Coercion b b -> Coercion b a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Coercion b b
y) ZigZag b b
z
Zig Coercion b b
y ZigZag b b
z ->
case CoerceTo_UnsafeFrom b a -> CoerceTo_UnsafeFrom b a
forall (a :: Hakaru) (c :: Hakaru).
CoerceTo_UnsafeFrom a c -> CoerceTo_UnsafeFrom a c
simplifyCTUF (Coercion b a -> Coercion b b -> CoerceTo_UnsafeFrom b a
forall (b :: Hakaru) (c :: Hakaru) (a :: Hakaru).
Coercion b c -> Coercion b a -> CoerceTo_UnsafeFrom a c
CTUF Coercion b a
x Coercion b b
y) of
CTUF Coercion b a
CNil Coercion b b
CNil -> ZigZag a b
ZigZag b b
z
CTUF Coercion b a
CNil Coercion b b
y' -> Coercion b b -> ZigZag b b -> ZigZag b b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Coercion a b -> ZigZag b c -> ZigZag a c
Zig Coercion b b
y' ZigZag b b
z
CTUF Coercion b a
x' Coercion b b
CNil -> Coercion b a -> ZigZag b b -> ZigZag a b
forall (b :: Hakaru) (a :: Hakaru) (c :: Hakaru).
Coercion b a -> ZigZag b c -> ZigZag a c
Zag Coercion b a
x' ZigZag b b
ZigZag b b
z
CTUF Coercion b a
x' Coercion b b
y' -> Coercion b a -> ZigZag b b -> ZigZag a b
forall (b :: Hakaru) (a :: Hakaru) (c :: Hakaru).
Coercion b a -> ZigZag b c -> ZigZag a c
Zag Coercion b a
x' (Coercion b b -> ZigZag b b -> ZigZag b b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Coercion a b -> ZigZag b c -> ZigZag a c
Zig Coercion b b
y' ZigZag b b
z)