{-# LANGUAGE CPP
, DataKinds
, InstanceSigs
, GADTs
, KindSignatures
, Rank2Types
, TypeOperators
#-}
module Language.Hakaru.Syntax.Reducer where
import Language.Hakaru.Types.DataKind
import Language.Hakaru.Types.HClasses
import Language.Hakaru.Syntax.IClasses
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative
import Data.Monoid (Monoid(..))
#endif
data Reducer (abt :: [Hakaru] -> Hakaru -> *)
(xs :: [Hakaru])
(a :: Hakaru) where
Red_Fanout
:: Reducer abt xs a
-> Reducer abt xs b
-> Reducer abt xs (HPair a b)
Red_Index
:: abt xs 'HNat
-> abt ( 'HNat ': xs) 'HNat
-> Reducer abt ( 'HNat ': xs) a
-> Reducer abt xs ('HArray a)
Red_Split
:: abt ( 'HNat ': xs) HBool
-> Reducer abt xs a
-> Reducer abt xs b
-> Reducer abt xs (HPair a b)
Red_Nop
:: Reducer abt xs HUnit
Red_Add
:: HSemiring a
-> abt ( 'HNat ': xs) a
-> Reducer abt xs a
instance Functor22 Reducer where
fmap22 :: (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i)
-> Reducer a j l -> Reducer b j l
fmap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (Red_Fanout Reducer a j a
r1 Reducer a j b
r2) = Reducer b j a -> Reducer b j b -> Reducer b j (HPair a b)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru) (b :: Hakaru).
Reducer abt xs a -> Reducer abt xs b -> Reducer abt xs (HPair a b)
Red_Fanout ((forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i)
-> Reducer a j a -> Reducer b j a
forall k1 k2 k3 k4 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *)
(a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3) (l :: k4).
Functor22 f =>
(forall (h :: k1) (i :: k2). a h i -> b h i) -> f a j l -> f b j l
fmap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f Reducer a j a
r1) ((forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i)
-> Reducer a j b -> Reducer b j b
forall k1 k2 k3 k4 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *)
(a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3) (l :: k4).
Functor22 f =>
(forall (h :: k1) (i :: k2). a h i -> b h i) -> f a j l -> f b j l
fmap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f Reducer a j b
r2)
fmap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (Red_Index a j 'HNat
n a ('HNat : j) 'HNat
ix Reducer a ('HNat : j) a
r) = b j 'HNat
-> b ('HNat : j) 'HNat
-> Reducer b ('HNat : j) a
-> Reducer b j ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru).
abt xs 'HNat
-> abt ('HNat : xs) 'HNat
-> Reducer abt ('HNat : xs) a
-> Reducer abt xs ('HArray a)
Red_Index (a j 'HNat -> b j 'HNat
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a j 'HNat
n) (a ('HNat : j) 'HNat -> b ('HNat : j) 'HNat
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a ('HNat : j) 'HNat
ix) ((forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i)
-> Reducer a ('HNat : j) a -> Reducer b ('HNat : j) a
forall k1 k2 k3 k4 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *)
(a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3) (l :: k4).
Functor22 f =>
(forall (h :: k1) (i :: k2). a h i -> b h i) -> f a j l -> f b j l
fmap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f Reducer a ('HNat : j) a
r)
fmap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (Red_Split a ('HNat : j) HBool
b Reducer a j a
r1 Reducer a j b
r2) = b ('HNat : j) HBool
-> Reducer b j a -> Reducer b j b -> Reducer b j (HPair a b)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru) (b :: Hakaru).
abt ('HNat : xs) HBool
-> Reducer abt xs a
-> Reducer abt xs b
-> Reducer abt xs (HPair a b)
Red_Split (a ('HNat : j) HBool -> b ('HNat : j) HBool
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a ('HNat : j) HBool
b) ((forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i)
-> Reducer a j a -> Reducer b j a
forall k1 k2 k3 k4 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *)
(a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3) (l :: k4).
Functor22 f =>
(forall (h :: k1) (i :: k2). a h i -> b h i) -> f a j l -> f b j l
fmap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f Reducer a j a
r1) ((forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i)
-> Reducer a j b -> Reducer b j b
forall k1 k2 k3 k4 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *)
(a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3) (l :: k4).
Functor22 f =>
(forall (h :: k1) (i :: k2). a h i -> b h i) -> f a j l -> f b j l
fmap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f Reducer a j b
r2)
fmap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
_ Reducer a j l
Red_Nop = Reducer b j l
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru]).
Reducer abt xs HUnit
Red_Nop
fmap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (Red_Add HSemiring l
h a ('HNat : j) l
e) = HSemiring l -> b ('HNat : j) l -> Reducer b j l
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *)
(xs :: [Hakaru]).
HSemiring a -> abt ('HNat : xs) a -> Reducer abt xs a
Red_Add HSemiring l
h (a ('HNat : j) l -> b ('HNat : j) l
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a ('HNat : j) l
e)
instance Foldable22 Reducer where
foldMap22 :: (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m)
-> Reducer a j l -> m
foldMap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (Red_Fanout Reducer a j a
r1 Reducer a j b
r2) = (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m)
-> Reducer a j a -> m
forall k1 k2 k3 k4 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *) m
(a :: k1 -> k2 -> *) (j :: k3) (l :: k4).
(Foldable22 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j l -> m
foldMap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f Reducer a j a
r1 m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m)
-> Reducer a j b -> m
forall k1 k2 k3 k4 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *) m
(a :: k1 -> k2 -> *) (j :: k3) (l :: k4).
(Foldable22 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j l -> m
foldMap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f Reducer a j b
r2
foldMap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (Red_Index a j 'HNat
n a ('HNat : j) 'HNat
ix Reducer a ('HNat : j) a
r) = a j 'HNat -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a j 'HNat
n m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` a ('HNat : j) 'HNat -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a ('HNat : j) 'HNat
ix m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m)
-> Reducer a ('HNat : j) a -> m
forall k1 k2 k3 k4 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *) m
(a :: k1 -> k2 -> *) (j :: k3) (l :: k4).
(Foldable22 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j l -> m
foldMap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f Reducer a ('HNat : j) a
r
foldMap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (Red_Split a ('HNat : j) HBool
b Reducer a j a
r1 Reducer a j b
r2) = a ('HNat : j) HBool -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a ('HNat : j) HBool
b m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m)
-> Reducer a j a -> m
forall k1 k2 k3 k4 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *) m
(a :: k1 -> k2 -> *) (j :: k3) (l :: k4).
(Foldable22 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j l -> m
foldMap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f Reducer a j a
r1 m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m)
-> Reducer a j b -> m
forall k1 k2 k3 k4 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *) m
(a :: k1 -> k2 -> *) (j :: k3) (l :: k4).
(Foldable22 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j l -> m
foldMap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f Reducer a j b
r2
foldMap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
_ Reducer a j l
Red_Nop = m
forall a. Monoid a => a
mempty
foldMap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (Red_Add HSemiring l
_ a ('HNat : j) l
e) = a ('HNat : j) l -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a ('HNat : j) l
e
instance Traversable22 Reducer where
traverse22 :: (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> Reducer a j l -> f (Reducer b j l)
traverse22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (Red_Fanout Reducer a j a
r1 Reducer a j b
r2) = Reducer b j a -> Reducer b j b -> Reducer b j (HPair a b)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru) (b :: Hakaru).
Reducer abt xs a -> Reducer abt xs b -> Reducer abt xs (HPair a b)
Red_Fanout (Reducer b j a -> Reducer b j b -> Reducer b j (HPair a b))
-> f (Reducer b j a)
-> f (Reducer b j b -> Reducer b j (HPair a b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> Reducer a j a -> f (Reducer b j a)
forall k1 k2 k3 k4 (t :: (k1 -> k2 -> *) -> k3 -> k4 -> *)
(f :: * -> *) (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3)
(l :: k4).
(Traversable22 t, Applicative f) =>
(forall (h :: k1) (i :: k2). a h i -> f (b h i))
-> t a j l -> f (t b j l)
traverse22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f Reducer a j a
r1 f (Reducer b j b -> Reducer b j (HPair a b))
-> f (Reducer b j b) -> f (Reducer b j (HPair a b))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> Reducer a j b -> f (Reducer b j b)
forall k1 k2 k3 k4 (t :: (k1 -> k2 -> *) -> k3 -> k4 -> *)
(f :: * -> *) (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3)
(l :: k4).
(Traversable22 t, Applicative f) =>
(forall (h :: k1) (i :: k2). a h i -> f (b h i))
-> t a j l -> f (t b j l)
traverse22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f Reducer a j b
r2
traverse22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (Red_Index a j 'HNat
n a ('HNat : j) 'HNat
ix Reducer a ('HNat : j) a
r) = b j 'HNat
-> b ('HNat : j) 'HNat
-> Reducer b ('HNat : j) a
-> Reducer b j ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru).
abt xs 'HNat
-> abt ('HNat : xs) 'HNat
-> Reducer abt ('HNat : xs) a
-> Reducer abt xs ('HArray a)
Red_Index (b j 'HNat
-> b ('HNat : j) 'HNat
-> Reducer b ('HNat : j) a
-> Reducer b j ('HArray a))
-> f (b j 'HNat)
-> f (b ('HNat : j) 'HNat
-> Reducer b ('HNat : j) a -> Reducer b j ('HArray a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a j 'HNat -> f (b j 'HNat)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a j 'HNat
n f (b ('HNat : j) 'HNat
-> Reducer b ('HNat : j) a -> Reducer b j ('HArray a))
-> f (b ('HNat : j) 'HNat)
-> f (Reducer b ('HNat : j) a -> Reducer b j ('HArray a))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a ('HNat : j) 'HNat -> f (b ('HNat : j) 'HNat)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a ('HNat : j) 'HNat
ix f (Reducer b ('HNat : j) a -> Reducer b j ('HArray a))
-> f (Reducer b ('HNat : j) a) -> f (Reducer b j ('HArray a))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> Reducer a ('HNat : j) a -> f (Reducer b ('HNat : j) a)
forall k1 k2 k3 k4 (t :: (k1 -> k2 -> *) -> k3 -> k4 -> *)
(f :: * -> *) (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3)
(l :: k4).
(Traversable22 t, Applicative f) =>
(forall (h :: k1) (i :: k2). a h i -> f (b h i))
-> t a j l -> f (t b j l)
traverse22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f Reducer a ('HNat : j) a
r
traverse22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (Red_Split a ('HNat : j) HBool
b Reducer a j a
r1 Reducer a j b
r2) = b ('HNat : j) HBool
-> Reducer b j a -> Reducer b j b -> Reducer b j (HPair a b)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru) (b :: Hakaru).
abt ('HNat : xs) HBool
-> Reducer abt xs a
-> Reducer abt xs b
-> Reducer abt xs (HPair a b)
Red_Split (b ('HNat : j) HBool
-> Reducer b j a -> Reducer b j b -> Reducer b j (HPair a b))
-> f (b ('HNat : j) HBool)
-> f (Reducer b j a -> Reducer b j b -> Reducer b j (HPair a b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a ('HNat : j) HBool -> f (b ('HNat : j) HBool)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a ('HNat : j) HBool
b f (Reducer b j a -> Reducer b j b -> Reducer b j (HPair a b))
-> f (Reducer b j a)
-> f (Reducer b j b -> Reducer b j (HPair a b))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> Reducer a j a -> f (Reducer b j a)
forall k1 k2 k3 k4 (t :: (k1 -> k2 -> *) -> k3 -> k4 -> *)
(f :: * -> *) (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3)
(l :: k4).
(Traversable22 t, Applicative f) =>
(forall (h :: k1) (i :: k2). a h i -> f (b h i))
-> t a j l -> f (t b j l)
traverse22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f Reducer a j a
r1 f (Reducer b j b -> Reducer b j (HPair a b))
-> f (Reducer b j b) -> f (Reducer b j (HPair a b))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> Reducer a j b -> f (Reducer b j b)
forall k1 k2 k3 k4 (t :: (k1 -> k2 -> *) -> k3 -> k4 -> *)
(f :: * -> *) (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3)
(l :: k4).
(Traversable22 t, Applicative f) =>
(forall (h :: k1) (i :: k2). a h i -> f (b h i))
-> t a j l -> f (t b j l)
traverse22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f Reducer a j b
r2
traverse22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
_ Reducer a j l
Red_Nop = Reducer b j HUnit -> f (Reducer b j HUnit)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Reducer b j HUnit
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru]).
Reducer abt xs HUnit
Red_Nop
traverse22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (Red_Add HSemiring l
h a ('HNat : j) l
e) = HSemiring l -> b ('HNat : j) l -> Reducer b j l
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *)
(xs :: [Hakaru]).
HSemiring a -> abt ('HNat : xs) a -> Reducer abt xs a
Red_Add HSemiring l
h (b ('HNat : j) l -> Reducer b j l)
-> f (b ('HNat : j) l) -> f (Reducer b j l)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a ('HNat : j) l -> f (b ('HNat : j) l)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a ('HNat : j) l
e
instance Eq2 abt => Eq1 (Reducer abt xs) where
eq1 :: Reducer abt xs i -> Reducer abt xs i -> Bool
eq1 (Red_Fanout Reducer abt xs a
r1 Reducer abt xs b
r2) (Red_Fanout Reducer abt xs a
r1' Reducer abt xs b
r2') = Reducer abt xs a -> Reducer abt xs a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1 Reducer abt xs a
r1 Reducer abt xs a
Reducer abt xs a
r1' Bool -> Bool -> Bool
&& Reducer abt xs b -> Reducer abt xs b -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1 Reducer abt xs b
r2 Reducer abt xs b
Reducer abt xs b
r2'
eq1 (Red_Index abt xs 'HNat
n abt ('HNat : xs) 'HNat
ix Reducer abt ('HNat : xs) a
r) (Red_Index abt xs 'HNat
n' abt ('HNat : xs) 'HNat
ix' Reducer abt ('HNat : xs) a
r') = abt xs 'HNat -> abt xs 'HNat -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2 abt xs 'HNat
n abt xs 'HNat
n' Bool -> Bool -> Bool
&& abt ('HNat : xs) 'HNat -> abt ('HNat : xs) 'HNat -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2 abt ('HNat : xs) 'HNat
ix abt ('HNat : xs) 'HNat
ix' Bool -> Bool -> Bool
&& Reducer abt ('HNat : xs) a -> Reducer abt ('HNat : xs) a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1 Reducer abt ('HNat : xs) a
r Reducer abt ('HNat : xs) a
Reducer abt ('HNat : xs) a
r'
eq1 (Red_Split abt ('HNat : xs) HBool
b Reducer abt xs a
r1 Reducer abt xs b
r2) (Red_Split abt ('HNat : xs) HBool
b' Reducer abt xs a
r1' Reducer abt xs b
r2') = abt ('HNat : xs) HBool -> abt ('HNat : xs) HBool -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2 abt ('HNat : xs) HBool
b abt ('HNat : xs) HBool
b' Bool -> Bool -> Bool
&& Reducer abt xs a -> Reducer abt xs a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1 Reducer abt xs a
r1 Reducer abt xs a
Reducer abt xs a
r1' Bool -> Bool -> Bool
&& Reducer abt xs b -> Reducer abt xs b -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1 Reducer abt xs b
r2 Reducer abt xs b
Reducer abt xs b
r2'
eq1 Reducer abt xs i
Red_Nop Reducer abt xs i
Red_Nop = Bool
True
eq1 (Red_Add HSemiring i
_ abt ('HNat : xs) i
e) (Red_Add HSemiring i
_ abt ('HNat : xs) i
e') = abt ('HNat : xs) i -> abt ('HNat : xs) i -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2 abt ('HNat : xs) i
e abt ('HNat : xs) i
e'
eq1 Reducer abt xs i
_ Reducer abt xs i
_ = Bool
False
instance JmEq2 abt => JmEq1 (Reducer abt xs) where
jmEq1 :: Reducer abt xs i -> Reducer abt xs j -> Maybe (TypeEq i j)
jmEq1 = Reducer abt xs i -> Reducer abt xs j -> Maybe (TypeEq i j)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru) (b :: Hakaru).
JmEq2 abt =>
Reducer abt xs a -> Reducer abt xs b -> Maybe (TypeEq a b)
jmEqReducer
jmEqReducer
:: (JmEq2 abt)
=> Reducer abt xs a
-> Reducer abt xs b
-> Maybe (TypeEq a b)
jmEqReducer :: Reducer abt xs a -> Reducer abt xs b -> Maybe (TypeEq a b)
jmEqReducer (Red_Fanout Reducer abt xs a
a Reducer abt xs b
b) (Red_Fanout Reducer abt xs a
a' Reducer abt xs b
b') = do
TypeEq a a
Refl <- Reducer abt xs a -> Reducer abt xs a -> Maybe (TypeEq a a)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru) (b :: Hakaru).
JmEq2 abt =>
Reducer abt xs a -> Reducer abt xs b -> Maybe (TypeEq a b)
jmEqReducer Reducer abt xs a
a Reducer abt xs a
a'
TypeEq b b
Refl <- Reducer abt xs b -> Reducer abt xs b -> Maybe (TypeEq b b)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru) (b :: Hakaru).
JmEq2 abt =>
Reducer abt xs a -> Reducer abt xs b -> Maybe (TypeEq a b)
jmEqReducer Reducer abt xs b
b Reducer abt xs b
b'
TypeEq a a -> Maybe (TypeEq a a)
forall (m :: * -> *) a. Monad m => a -> m a
return TypeEq a a
forall k (a :: k). TypeEq a a
Refl
jmEqReducer (Red_Index abt xs 'HNat
s abt ('HNat : xs) 'HNat
i Reducer abt ('HNat : xs) a
r) (Red_Index abt xs 'HNat
s' abt ('HNat : xs) 'HNat
i' Reducer abt ('HNat : xs) a
r') = do
(TypeEq xs xs
Refl, TypeEq 'HNat 'HNat
Refl) <- abt xs 'HNat
-> abt xs 'HNat -> Maybe (TypeEq xs xs, TypeEq 'HNat 'HNat)
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 abt xs 'HNat
s abt xs 'HNat
s'
(TypeEq ('HNat : xs) ('HNat : xs)
Refl, TypeEq 'HNat 'HNat
Refl) <- abt ('HNat : xs) 'HNat
-> abt ('HNat : xs) 'HNat
-> Maybe (TypeEq ('HNat : xs) ('HNat : xs), TypeEq 'HNat 'HNat)
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 abt ('HNat : xs) 'HNat
i abt ('HNat : xs) 'HNat
i'
TypeEq a a
Refl <- Reducer abt ('HNat : xs) a
-> Reducer abt ('HNat : xs) a -> Maybe (TypeEq a a)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru) (b :: Hakaru).
JmEq2 abt =>
Reducer abt xs a -> Reducer abt xs b -> Maybe (TypeEq a b)
jmEqReducer Reducer abt ('HNat : xs) a
r Reducer abt ('HNat : xs) a
r'
TypeEq a a -> Maybe (TypeEq a a)
forall (m :: * -> *) a. Monad m => a -> m a
return TypeEq a a
forall k (a :: k). TypeEq a a
Refl
jmEqReducer (Red_Split abt ('HNat : xs) HBool
b Reducer abt xs a
r Reducer abt xs b
s) (Red_Split abt ('HNat : xs) HBool
b' Reducer abt xs a
r' Reducer abt xs b
s') = do
(TypeEq ('HNat : xs) ('HNat : xs)
Refl, TypeEq HBool HBool
Refl) <- abt ('HNat : xs) HBool
-> abt ('HNat : xs) HBool
-> Maybe (TypeEq ('HNat : xs) ('HNat : xs), TypeEq HBool HBool)
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 abt ('HNat : xs) HBool
b abt ('HNat : xs) HBool
b'
TypeEq a a
Refl <- Reducer abt xs a -> Reducer abt xs a -> Maybe (TypeEq a a)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru) (b :: Hakaru).
JmEq2 abt =>
Reducer abt xs a -> Reducer abt xs b -> Maybe (TypeEq a b)
jmEqReducer Reducer abt xs a
r Reducer abt xs a
r'
TypeEq b b
Refl <- Reducer abt xs b -> Reducer abt xs b -> Maybe (TypeEq b b)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru) (b :: Hakaru).
JmEq2 abt =>
Reducer abt xs a -> Reducer abt xs b -> Maybe (TypeEq a b)
jmEqReducer Reducer abt xs b
s Reducer abt xs b
s'
TypeEq a a -> Maybe (TypeEq a a)
forall (m :: * -> *) a. Monad m => a -> m a
return TypeEq a a
forall k (a :: k). TypeEq a a
Refl
jmEqReducer Reducer abt xs a
Red_Nop Reducer abt xs b
Red_Nop = TypeEq a a -> Maybe (TypeEq a a)
forall (m :: * -> *) a. Monad m => a -> m a
return TypeEq a a
forall k (a :: k). TypeEq a a
Refl
jmEqReducer (Red_Add HSemiring a
_ abt ('HNat : xs) a
x) (Red_Add HSemiring b
_ abt ('HNat : xs) b
x') = do
(TypeEq ('HNat : xs) ('HNat : xs)
Refl, TypeEq a b
Refl) <- abt ('HNat : xs) a
-> abt ('HNat : xs) b
-> Maybe (TypeEq ('HNat : xs) ('HNat : xs), TypeEq a 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 abt ('HNat : xs) a
x abt ('HNat : xs) b
x'
TypeEq a a -> Maybe (TypeEq a a)
forall (m :: * -> *) a. Monad m => a -> m a
return TypeEq a a
forall k (a :: k). TypeEq a a
Refl
jmEqReducer Reducer abt xs a
_ Reducer abt xs b
_ = Maybe (TypeEq a b)
forall a. Maybe a
Nothing