{-# 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                 -- size of resulting array
         -> abt ( 'HNat ': xs) 'HNat     -- index into array (bound i)
         -> Reducer abt ( 'HNat ': xs) a -- reduction body (bound b)
         -> Reducer abt xs ('HArray a)
     Red_Split
         :: abt ( 'HNat ': xs) HBool     -- (bound i)
         -> 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         -- (bound i)
         -> 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