{-# LANGUAGE CPP
           , DataKinds
           , GADTs
           , TypeOperators
           , PolyKinds
           , FlexibleContexts
           , ScopedTypeVariables
           , UndecidableInstances
           #-}

-- TODO: all the instances here are orphans. To ensure that we don't
-- have issues about orphan instances, we should give them all
-- newtypes and only provide the instance for those newtypes!
-- (and\/or: for the various op types, it's okay to move them to
-- AST.hs to avoid orphanage. It's just the instances for 'Term'
-- itself which are morally suspect outside of testing.)
{-# OPTIONS_GHC -Wall -fwarn-tabs -fno-warn-orphans -fno-warn-name-shadowing #-}
----------------------------------------------------------------
--                                                    2016.05.24
-- |
-- Module      :  Language.Hakaru.Syntax.ABT.Eq
-- Copyright   :  Copyright (c) 2016 the Hakaru team
-- License     :  BSD3
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  experimental
-- Portability :  GHC-only
--
-- Warning: The following module is for testing purposes only. Using
-- the 'JmEq1' instance for 'Term' is inefficient and should not
-- be done accidentally. To implement that (orphan) instance we
-- also provide the following (orphan) instances:
--
-- > SArgs      : JmEq1
-- > Term       : JmEq1, Eq1, Eq
-- > TrivialABT : JmEq2, JmEq1, Eq2, Eq1, Eq
--
-- TODO: because this is only for testing, everything else should
-- move to the @Tests@ directory.
----------------------------------------------------------------
module Language.Hakaru.Syntax.AST.Eq where

import Language.Hakaru.Types.DataKind
import Language.Hakaru.Types.Sing
import Language.Hakaru.Types.Coercion
import Language.Hakaru.Types.HClasses
import Language.Hakaru.Syntax.IClasses
import Language.Hakaru.Syntax.ABT
import Language.Hakaru.Syntax.AST
import Language.Hakaru.Syntax.Datum
import Language.Hakaru.Syntax.TypeOf
import Language.Hakaru.Syntax.Reducer

import Control.Monad.Reader

import qualified Data.Foldable      as F
import qualified Data.List.NonEmpty as L
import qualified Data.Sequence      as S
import qualified Data.Traversable   as T

#if __GLASGOW_HASKELL__ < 710
import           Data.Functor ((<$>))
import           Data.Traversable
#endif


import Data.Maybe
import Data.List (inits,tails)
-- import Data.Number.Nat

import Unsafe.Coerce

---------------------------------------------------------------------
-- | This function performs 'jmEq' on a @(:$)@ node of the AST.
-- It's necessary to break it out like this since we can't just
-- give a 'JmEq1' instance for 'SCon' due to polymorphism issues
-- (e.g., we can't just say that 'Lam_' is John Major equal to
-- 'Lam_', since they may be at different types). However, once the
-- 'SArgs' associated with the 'SCon' is given, that resolves the
-- polymorphism.
jmEq_S
    :: (ABT Term abt, JmEq2 abt)
    => SCon args  a  -> SArgs abt args
    -> SCon args' a' -> SArgs abt args'
    -> Maybe (TypeEq a a', TypeEq args args')
jmEq_S :: SCon args a
-> SArgs abt args
-> SCon args' a'
-> SArgs abt args'
-> Maybe (TypeEq a a', TypeEq args args')
jmEq_S SCon args a
Lam_      SArgs abt args
es SCon args' a'
Lam_       SArgs abt args'
es' =
    SArgs abt args -> SArgs abt args' -> Maybe (TypeEq args args')
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 SArgs abt args
es SArgs abt args'
es' Maybe (TypeEq args args')
-> (TypeEq args args' -> Maybe (TypeEq a a', TypeEq args args'))
-> Maybe (TypeEq a a', TypeEq args args')
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq args args'
Refl -> (TypeEq (a ':-> b) (a ':-> b),
 TypeEq '[ '( '[a], b)] '[ '( '[a], b)])
-> Maybe
     (TypeEq (a ':-> b) (a ':-> b),
      TypeEq '[ '( '[a], b)] '[ '( '[a], b)])
forall a. a -> Maybe a
Just (TypeEq (a ':-> b) (a ':-> b)
forall k (a :: k). TypeEq a a
Refl, TypeEq '[ '( '[a], b)] '[ '( '[a], b)]
forall k (a :: k). TypeEq a a
Refl)
jmEq_S SCon args a
App_      SArgs abt args
es SCon args' a'
App_       SArgs abt args'
es' =
    SArgs abt args -> SArgs abt args' -> Maybe (TypeEq args args')
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 SArgs abt args
es SArgs abt args'
es' Maybe (TypeEq args args')
-> (TypeEq args args' -> Maybe (TypeEq a a', TypeEq args args'))
-> Maybe (TypeEq a a', TypeEq args args')
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq args args'
Refl -> (TypeEq a a, TypeEq '[LC (a ':-> a), LC a] '[LC (a ':-> a), LC a])
-> Maybe
     (TypeEq a a, TypeEq '[LC (a ':-> a), LC a] '[LC (a ':-> a), LC a])
forall a. a -> Maybe a
Just (TypeEq a a
forall k (a :: k). TypeEq a a
Refl, TypeEq '[LC (a ':-> a), LC a] '[LC (a ':-> a), LC a]
forall k (a :: k). TypeEq a a
Refl)
jmEq_S SCon args a
Let_      SArgs abt args
es SCon args' a'
Let_       SArgs abt args'
es' =
    SArgs abt args -> SArgs abt args' -> Maybe (TypeEq args args')
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 SArgs abt args
es SArgs abt args'
es' Maybe (TypeEq args args')
-> (TypeEq args args' -> Maybe (TypeEq a a', TypeEq args args'))
-> Maybe (TypeEq a a', TypeEq args args')
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq args args'
Refl -> (TypeEq a a, TypeEq '[LC a, '( '[a], a)] '[LC a, '( '[a], a)])
-> Maybe
     (TypeEq a a, TypeEq '[LC a, '( '[a], a)] '[LC a, '( '[a], a)])
forall a. a -> Maybe a
Just (TypeEq a a
forall k (a :: k). TypeEq a a
Refl, TypeEq '[LC a, '( '[a], a)] '[LC a, '( '[a], a)]
forall k (a :: k). TypeEq a a
Refl)
jmEq_S (CoerceTo_ Coercion a a
c) (abt vars a
es :* SArgs abt args
End) (CoerceTo_ Coercion a a'
c') (abt vars a
es' :* SArgs abt args
End) = do
    (TypeEq vars vars
Refl, TypeEq a a
Refl) <- abt vars a -> abt vars a -> Maybe (TypeEq vars vars, TypeEq a a)
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 vars a
es abt vars a
es'
    let t1 :: Sing a
t1 = Coercion a a -> Sing a -> Sing a
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f a -> f b
coerceTo Coercion a a
c  (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt vars a
abt '[] a
es)
    let t2 :: Sing a'
t2 = Coercion a a' -> Sing a -> Sing a'
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f a -> f b
coerceTo Coercion a a'
c' (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt vars a
abt '[] a
es')
    TypeEq a a'
Refl <- 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
t1 Sing a'
t2
    (TypeEq a a, TypeEq args args)
-> Maybe (TypeEq a a, TypeEq args args)
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeEq a a
forall k (a :: k). TypeEq a a
Refl, TypeEq args args
forall k (a :: k). TypeEq a a
Refl)
jmEq_S (UnsafeFrom_ Coercion a b
c) (abt vars a
es :* SArgs abt args
End) (UnsafeFrom_ Coercion a' b
c') (abt vars a
es' :* SArgs abt args
End) = do
    (TypeEq vars vars
Refl, TypeEq a a
Refl) <- abt vars a -> abt vars a -> Maybe (TypeEq vars vars, TypeEq a a)
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 vars a
es abt vars a
es'
    let t1 :: Sing a
t1 = Coercion a b -> Sing b -> Sing a
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f b -> f a
coerceFrom Coercion a b
c  (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt vars a
abt '[] a
es)
    let t2 :: Sing a'
t2 = Coercion a' b -> Sing b -> Sing a'
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f b -> f a
coerceFrom Coercion a' b
c' (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt vars a
abt '[] a
es')
    TypeEq a a'
Refl <- 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
t1 Sing a'
t2
    (TypeEq a a, TypeEq args args)
-> Maybe (TypeEq a a, TypeEq args args)
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeEq a a
forall k (a :: k). TypeEq a a
Refl, TypeEq args args
forall k (a :: k). TypeEq a a
Refl)
jmEq_S (PrimOp_ PrimOp typs a
op) SArgs abt args
es (PrimOp_ PrimOp typs a'
op') SArgs abt args'
es' = do
    TypeEq args args'
Refl <- SArgs abt args -> SArgs abt args' -> Maybe (TypeEq args args')
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 SArgs abt args
es SArgs abt args'
es'
    (TypeEq typs typs
Refl, TypeEq a a'
Refl) <- PrimOp typs a
-> PrimOp typs a' -> Maybe (TypeEq typs typs, TypeEq a a')
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 PrimOp typs a
op PrimOp typs a'
op'
    (TypeEq a a, TypeEq args args)
-> Maybe (TypeEq a a, TypeEq args args)
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeEq a a
forall k (a :: k). TypeEq a a
Refl, TypeEq args args
forall k (a :: k). TypeEq a a
Refl)
jmEq_S (ArrayOp_ ArrayOp typs a
op) SArgs abt args
es (ArrayOp_ ArrayOp typs a'
op') SArgs abt args'
es' = do
    TypeEq args args'
Refl <- SArgs abt args -> SArgs abt args' -> Maybe (TypeEq args args')
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 SArgs abt args
es SArgs abt args'
es'
    (TypeEq typs typs
Refl, TypeEq a a'
Refl) <- ArrayOp typs a
-> ArrayOp typs a' -> Maybe (TypeEq typs typs, TypeEq a a')
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 ArrayOp typs a
op ArrayOp typs a'
op'
    (TypeEq a a, TypeEq args args)
-> Maybe (TypeEq a a, TypeEq args args)
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeEq a a
forall k (a :: k). TypeEq a a
Refl, TypeEq args args
forall k (a :: k). TypeEq a a
Refl)
jmEq_S (MeasureOp_ MeasureOp typs a
op) SArgs abt args
es (MeasureOp_ MeasureOp typs a
op') SArgs abt args'
es' = do
    TypeEq args args'
Refl <- SArgs abt args -> SArgs abt args' -> Maybe (TypeEq args args')
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 SArgs abt args
es SArgs abt args'
es'
    (TypeEq typs typs
Refl, TypeEq a a
Refl) <- MeasureOp typs a
-> MeasureOp typs a -> Maybe (TypeEq typs typs, TypeEq a a)
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 MeasureOp typs a
op MeasureOp typs a
op'
    (TypeEq a a, TypeEq args args)
-> Maybe (TypeEq a a, TypeEq args args)
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeEq a a
forall k (a :: k). TypeEq a a
Refl, TypeEq args args
forall k (a :: k). TypeEq a a
Refl)
jmEq_S SCon args a
Dirac     SArgs abt args
es SCon args' a'
Dirac      SArgs abt args'
es' =
    SArgs abt args -> SArgs abt args' -> Maybe (TypeEq args args')
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 SArgs abt args
es SArgs abt args'
es' Maybe (TypeEq args args')
-> (TypeEq args args' -> Maybe (TypeEq a a', TypeEq args args'))
-> Maybe (TypeEq a a', TypeEq args args')
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq args args'
Refl -> (TypeEq ('HMeasure a) ('HMeasure a), TypeEq '[LC a] '[LC a])
-> Maybe
     (TypeEq ('HMeasure a) ('HMeasure a), TypeEq '[LC a] '[LC a])
forall a. a -> Maybe a
Just (TypeEq ('HMeasure a) ('HMeasure a)
forall k (a :: k). TypeEq a a
Refl, TypeEq '[LC a] '[LC a]
forall k (a :: k). TypeEq a a
Refl)
jmEq_S SCon args a
MBind     SArgs abt args
es SCon args' a'
MBind      SArgs abt args'
es' =
    SArgs abt args -> SArgs abt args' -> Maybe (TypeEq args args')
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 SArgs abt args
es SArgs abt args'
es' Maybe (TypeEq args args')
-> (TypeEq args args' -> Maybe (TypeEq a a', TypeEq args args'))
-> Maybe (TypeEq a a', TypeEq args args')
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq args args'
Refl -> (TypeEq ('HMeasure b) ('HMeasure b),
 TypeEq
   '[LC ('HMeasure a), '( '[a], 'HMeasure b)]
   '[LC ('HMeasure a), '( '[a], 'HMeasure b)])
-> Maybe
     (TypeEq ('HMeasure b) ('HMeasure b),
      TypeEq
        '[LC ('HMeasure a), '( '[a], 'HMeasure b)]
        '[LC ('HMeasure a), '( '[a], 'HMeasure b)])
forall a. a -> Maybe a
Just (TypeEq ('HMeasure b) ('HMeasure b)
forall k (a :: k). TypeEq a a
Refl, TypeEq
  '[LC ('HMeasure a), '( '[a], 'HMeasure b)]
  '[LC ('HMeasure a), '( '[a], 'HMeasure b)]
forall k (a :: k). TypeEq a a
Refl)
jmEq_S SCon args a
Integrate SArgs abt args
es SCon args' a'
Integrate  SArgs abt args'
es' =
    SArgs abt args -> SArgs abt args' -> Maybe (TypeEq args args')
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 SArgs abt args
es SArgs abt args'
es' Maybe (TypeEq args args')
-> (TypeEq args args' -> Maybe (TypeEq a a', TypeEq args args'))
-> Maybe (TypeEq a a', TypeEq args args')
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq args args'
Refl -> (TypeEq 'HProb 'HProb,
 TypeEq
   '[LC 'HReal, LC 'HReal, '( '[ 'HReal], 'HProb)]
   '[LC 'HReal, LC 'HReal, '( '[ 'HReal], 'HProb)])
-> Maybe
     (TypeEq 'HProb 'HProb,
      TypeEq
        '[LC 'HReal, LC 'HReal, '( '[ 'HReal], 'HProb)]
        '[LC 'HReal, LC 'HReal, '( '[ 'HReal], 'HProb)])
forall a. a -> Maybe a
Just (TypeEq 'HProb 'HProb
forall k (a :: k). TypeEq a a
Refl, TypeEq
  '[LC 'HReal, LC 'HReal, '( '[ 'HReal], 'HProb)]
  '[LC 'HReal, LC 'HReal, '( '[ 'HReal], 'HProb)]
forall k (a :: k). TypeEq a a
Refl)
jmEq_S (Summate HDiscrete a
h1 HSemiring a
h2) SArgs abt args
es (Summate HDiscrete a
h1' HSemiring a'
h2') SArgs abt args'
es' = do
    TypeEq a a
Refl <- 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 (HDiscrete a -> Sing a
forall (a :: Hakaru). HDiscrete a -> Sing a
sing_HDiscrete HDiscrete a
h1) (HDiscrete a -> Sing a
forall (a :: Hakaru). HDiscrete a -> Sing a
sing_HDiscrete HDiscrete a
h1')
    TypeEq a a'
Refl <- 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 (HSemiring a -> Sing a
forall (a :: Hakaru). HSemiring a -> Sing a
sing_HSemiring HSemiring a
h2) (HSemiring a' -> Sing a'
forall (a :: Hakaru). HSemiring a -> Sing a
sing_HSemiring HSemiring a'
h2')
    TypeEq args args'
Refl <- SArgs abt args -> SArgs abt args' -> Maybe (TypeEq args args')
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 SArgs abt args
es SArgs abt args'
es'
    (TypeEq a a, TypeEq args args)
-> Maybe (TypeEq a a, TypeEq args args)
forall a. a -> Maybe a
Just (TypeEq a a
forall k (a :: k). TypeEq a a
Refl, TypeEq args args
forall k (a :: k). TypeEq a a
Refl)
jmEq_S (Product HDiscrete a
h1 HSemiring a
h2) SArgs abt args
es (Product HDiscrete a
h1' HSemiring a'
h2') SArgs abt args'
es' = do
    TypeEq a a
Refl <- 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 (HDiscrete a -> Sing a
forall (a :: Hakaru). HDiscrete a -> Sing a
sing_HDiscrete HDiscrete a
h1) (HDiscrete a -> Sing a
forall (a :: Hakaru). HDiscrete a -> Sing a
sing_HDiscrete HDiscrete a
h1')
    TypeEq a a'
Refl <- 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 (HSemiring a -> Sing a
forall (a :: Hakaru). HSemiring a -> Sing a
sing_HSemiring HSemiring a
h2) (HSemiring a' -> Sing a'
forall (a :: Hakaru). HSemiring a -> Sing a
sing_HSemiring HSemiring a'
h2')
    TypeEq args args'
Refl <- SArgs abt args -> SArgs abt args' -> Maybe (TypeEq args args')
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 SArgs abt args
es SArgs abt args'
es'
    (TypeEq a a, TypeEq args args)
-> Maybe (TypeEq a a, TypeEq args args)
forall a. a -> Maybe a
Just (TypeEq a a
forall k (a :: k). TypeEq a a
Refl, TypeEq args args
forall k (a :: k). TypeEq a a
Refl)
jmEq_S (Transform_ Transform args a
t0) SArgs abt args
es (Transform_ Transform args' a'
t1)   SArgs abt args'
es' = do
    TypeEq args args'
Refl <- SArgs abt args -> SArgs abt args' -> Maybe (TypeEq args args')
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 SArgs abt args
es SArgs abt args'
es'
    TypeEq a a'
Refl <- Transform args a -> Transform args a' -> Maybe (TypeEq a a')
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru) (a' :: Hakaru).
Transform args a -> Transform args a' -> Maybe (TypeEq a a')
jmEq_Transform Transform args a
t0 Transform args a'
Transform args' a'
t1
    (TypeEq a a, TypeEq args args)
-> Maybe (TypeEq a a, TypeEq args args)
forall a. a -> Maybe a
Just (TypeEq a a
forall k (a :: k). TypeEq a a
Refl, TypeEq args args
forall k (a :: k). TypeEq a a
Refl)
jmEq_S SCon args a
_         SArgs abt args
_  SCon args' a'
_          SArgs abt args'
_   = Maybe (TypeEq a a', TypeEq args args')
forall a. Maybe a
Nothing

jmEq_Transform
    :: Transform args a
    -> Transform args a'
    -> Maybe (TypeEq a a')
jmEq_Transform :: Transform args a -> Transform args a' -> Maybe (TypeEq a a')
jmEq_Transform Transform args a
t0 Transform args a'
t1 =
  case (Transform args a
t0, Transform args a'
t1) of
    (Transform args a
Expect   , Transform args a'
Expect   ) -> TypeEq a a -> Maybe (TypeEq a a)
forall a. a -> Maybe a
Just TypeEq a a
forall k (a :: k). TypeEq a a
Refl
    (Transform args a
Observe  , Transform args a'
Observe  ) -> TypeEq a a -> Maybe (TypeEq a a)
forall a. a -> Maybe a
Just TypeEq a a
forall k (a :: k). TypeEq a a
Refl
    (Transform args a
MH       , Transform args a'
MH       ) -> TypeEq a a -> Maybe (TypeEq a a)
forall a. a -> Maybe a
Just TypeEq a a
forall k (a :: k). TypeEq a a
Refl
    (Transform args a
MCMC     , Transform args a'
MCMC     ) -> TypeEq a a -> Maybe (TypeEq a a)
forall a. a -> Maybe a
Just TypeEq a a
forall k (a :: k). TypeEq a a
Refl
    (Disint TransformImpl
k0, Disint TransformImpl
k1) ->
      if TransformImpl
k0TransformImpl -> TransformImpl -> Bool
forall a. Eq a => a -> a -> Bool
==TransformImpl
k1 then TypeEq a a -> Maybe (TypeEq a a)
forall a. a -> Maybe a
Just TypeEq a a
forall k (a :: k). TypeEq a a
Refl else Maybe (TypeEq a a')
forall a. Maybe a
Nothing
    (Transform args a
Summarize, Transform args a'
Summarize) -> TypeEq a a -> Maybe (TypeEq a a)
forall a. a -> Maybe a
Just TypeEq a a
forall k (a :: k). TypeEq a a
Refl
    (Transform args a
Simplify , Transform args a'
Simplify ) -> TypeEq a a -> Maybe (TypeEq a a)
forall a. a -> Maybe a
Just TypeEq a a
forall k (a :: k). TypeEq a a
Refl
    (Transform args a
Reparam  , Transform args a'
Reparam  ) -> TypeEq a a -> Maybe (TypeEq a a)
forall a. a -> Maybe a
Just TypeEq a a
forall k (a :: k). TypeEq a a
Refl
    (Transform args a, Transform args a')
_                      -> Maybe (TypeEq a a')
forall a. Maybe a
Nothing

-- TODO: Handle jmEq2 of pat and pat'
jmEq_Branch
    :: (ABT Term abt, JmEq2 abt)
    => [(Branch a abt b, Branch a abt b')]
    -> Maybe (TypeEq b b')
jmEq_Branch :: [(Branch a abt b, Branch a abt b')] -> Maybe (TypeEq b b')
jmEq_Branch []                                  = Maybe (TypeEq b b')
forall a. Maybe a
Nothing
jmEq_Branch [(Branch Pattern xs a
_ abt xs b
e, Branch Pattern xs a
_ abt xs b'
e')]    = do
    (TypeEq xs xs
Refl, TypeEq b b'
Refl) <- abt xs b -> abt xs b' -> Maybe (TypeEq xs xs, 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 abt xs b
e abt xs b'
e'
    TypeEq b b -> Maybe (TypeEq b b)
forall (m :: * -> *) a. Monad m => a -> m a
return TypeEq b b
forall k (a :: k). TypeEq a a
Refl
jmEq_Branch ((Branch Pattern xs a
_ abt xs b
e, Branch Pattern xs a
_ abt xs b'
e'):[(Branch a abt b, Branch a abt b')]
es) = do
    (TypeEq xs xs
Refl, TypeEq b b'
Refl) <- abt xs b -> abt xs b' -> Maybe (TypeEq xs xs, 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 abt xs b
e abt xs b'
e'
    [(Branch a abt b, Branch a abt b')] -> Maybe (TypeEq b b')
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru) (b :: Hakaru)
       (b' :: Hakaru).
(ABT Term abt, JmEq2 abt) =>
[(Branch a abt b, Branch a abt b')] -> Maybe (TypeEq b b')
jmEq_Branch [(Branch a abt b, Branch a abt b')]
es

instance JmEq2 abt => JmEq1 (SArgs abt) where
    jmEq1 :: SArgs abt i -> SArgs abt j -> Maybe (TypeEq i j)
jmEq1 SArgs abt i
End       SArgs abt j
End       = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
    jmEq1 (abt vars a
x :* SArgs abt args
xs) (abt vars a
y :* SArgs abt args
ys) =
        abt vars a -> abt vars a -> Maybe (TypeEq vars vars, TypeEq a a)
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 vars a
x  abt vars a
y  Maybe (TypeEq vars vars, TypeEq a a)
-> ((TypeEq vars vars, TypeEq a a) -> Maybe (TypeEq i j))
-> Maybe (TypeEq i j)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(TypeEq vars vars
Refl, TypeEq a a
Refl) ->
        SArgs abt args -> SArgs abt args -> Maybe (TypeEq args args)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 SArgs abt args
xs SArgs abt args
ys Maybe (TypeEq args args)
-> (TypeEq args args -> Maybe (TypeEq i j)) -> Maybe (TypeEq i j)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq args args
Refl ->
        TypeEq ('(vars, a) : args) ('(vars, a) : args)
-> Maybe (TypeEq ('(vars, a) : args) ('(vars, a) : args))
forall a. a -> Maybe a
Just TypeEq ('(vars, a) : args) ('(vars, a) : args)
forall k (a :: k). TypeEq a a
Refl
    jmEq1 SArgs abt i
_         SArgs abt j
_         = Maybe (TypeEq i j)
forall a. Maybe a
Nothing


instance (ABT Term abt, JmEq2 abt) => JmEq1 (Term abt) where
    jmEq1 :: Term abt i -> Term abt j -> Maybe (TypeEq i j)
jmEq1 (SCon args i
o :$ SArgs abt args
es) (SCon args j
o' :$ SArgs abt args
es') = do
        (TypeEq i j
Refl, TypeEq args args
Refl) <- SCon args i
-> SArgs abt args
-> SCon args j
-> SArgs abt args
-> Maybe (TypeEq i j, TypeEq args args)
forall (abt :: [Hakaru] -> Hakaru -> *)
       (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (args' :: [([Hakaru], Hakaru)]) (a' :: Hakaru).
(ABT Term abt, JmEq2 abt) =>
SCon args a
-> SArgs abt args
-> SCon args' a'
-> SArgs abt args'
-> Maybe (TypeEq a a', TypeEq args args')
jmEq_S SCon args i
o SArgs abt args
es SCon args j
o' SArgs abt args
es'
        TypeEq i i -> Maybe (TypeEq i i)
forall (m :: * -> *) a. Monad m => a -> m a
return TypeEq i i
forall k (a :: k). TypeEq a a
Refl
    jmEq1 (NaryOp_ NaryOp i
o Seq (abt '[] i)
es) (NaryOp_ NaryOp j
o' Seq (abt '[] j)
es') = do
        TypeEq i j
Refl <- NaryOp i -> NaryOp j -> Maybe (TypeEq i j)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 NaryOp i
o NaryOp j
o'
        () <- Seq (abt '[] i) -> Seq (abt '[] i) -> Maybe ()
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, JmEq2 abt) =>
Seq (abt '[] a) -> Seq (abt '[] a) -> Maybe ()
all_jmEq2 Seq (abt '[] i)
es Seq (abt '[] i)
Seq (abt '[] j)
es'
        TypeEq i i -> Maybe (TypeEq i i)
forall (m :: * -> *) a. Monad m => a -> m a
return TypeEq i i
forall k (a :: k). TypeEq a a
Refl
    jmEq1 (Literal_ Literal i
v)  (Literal_ Literal j
w)   = Literal i -> Literal j -> Maybe (TypeEq i j)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Literal i
v Literal j
w
    jmEq1 (Empty_ Sing ('HArray a)
a)    (Empty_ Sing ('HArray a)
b)     = Sing ('HArray a)
-> Sing ('HArray a) -> Maybe (TypeEq ('HArray a) ('HArray a))
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing ('HArray a)
a Sing ('HArray a)
b
    jmEq1 (Array_ abt '[] 'HNat
i abt '[ 'HNat] a
f)  (Array_ abt '[] 'HNat
j abt '[ 'HNat] a
g)   = do
        (TypeEq '[] '[]
Refl, TypeEq 'HNat 'HNat
Refl) <- abt '[] 'HNat
-> abt '[] 'HNat -> Maybe (TypeEq '[] '[], 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
i abt '[] 'HNat
j
        (TypeEq '[ 'HNat] '[ 'HNat]
Refl, TypeEq a a
Refl) <- abt '[ 'HNat] a
-> abt '[ 'HNat] a
-> Maybe (TypeEq '[ 'HNat] '[ 'HNat], TypeEq a a)
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] a
f abt '[ 'HNat] a
g
        TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
    -- Assumes nonempty literal arrays. The hope is that Empty_ covers that case.
    -- TODO handle empty literal arrays.
    jmEq1 (ArrayLiteral_ (abt '[] a
e:[abt '[] a]
es)) (ArrayLiteral_ (abt '[] a
e':[abt '[] a]
es')) = do
        (TypeEq '[] '[]
Refl, TypeEq a a
Refl) <- abt '[] a -> abt '[] a -> Maybe (TypeEq '[] '[], TypeEq a a)
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 '[] a
e abt '[] a
e'
        () <- Seq (abt '[] a) -> Seq (abt '[] a) -> Maybe ()
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, JmEq2 abt) =>
Seq (abt '[] a) -> Seq (abt '[] a) -> Maybe ()
all_jmEq2 ([abt '[] a] -> Seq (abt '[] a)
forall a. [a] -> Seq a
S.fromList [abt '[] a]
es) ([abt '[] a] -> Seq (abt '[] a)
forall a. [a] -> Seq a
S.fromList [abt '[] a]
es')
        TypeEq i i -> Maybe (TypeEq i i)
forall (m :: * -> *) a. Monad m => a -> m a
return TypeEq i i
forall k (a :: k). TypeEq a a
Refl
    jmEq1 (Bucket abt '[] 'HNat
a abt '[] 'HNat
b Reducer abt '[] i
r) (Bucket abt '[] 'HNat
a' abt '[] 'HNat
b' Reducer abt '[] j
r') = do
        (TypeEq '[] '[]
Refl, TypeEq 'HNat 'HNat
Refl) <- abt '[] 'HNat
-> abt '[] 'HNat -> Maybe (TypeEq '[] '[], 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
a abt '[] 'HNat
a'
        (TypeEq '[] '[]
Refl, TypeEq 'HNat 'HNat
Refl) <- abt '[] 'HNat
-> abt '[] 'HNat -> Maybe (TypeEq '[] '[], 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
b abt '[] 'HNat
b'
        TypeEq i j
Refl         <- Reducer abt '[] i -> Reducer abt '[] j -> Maybe (TypeEq i j)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Reducer abt '[] i
r Reducer abt '[] j
r'
        TypeEq i i -> Maybe (TypeEq i i)
forall (m :: * -> *) a. Monad m => a -> m a
return TypeEq i i
forall k (a :: k). TypeEq a a
Refl
    jmEq1 (Datum_ (Datum Text
hint Sing (HData' t)
_ DatumCode (Code t) (abt '[]) (HData' t)
_)) (Datum_ (Datum Text
hint' Sing (HData' t)
_ DatumCode (Code t) (abt '[]) (HData' t)
_))
        -- BUG: We need to compare structurally rather than using the hint
        | Text
hint Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
hint' = Maybe (TypeEq Any Any) -> Maybe (TypeEq i j)
forall a b. a -> b
unsafeCoerce (TypeEq Any Any -> Maybe (TypeEq Any Any)
forall a. a -> Maybe a
Just TypeEq Any Any
forall k (a :: k). TypeEq a a
Refl)
        | Bool
otherwise     = Maybe (TypeEq i j)
forall a. Maybe a
Nothing
    jmEq1 (Case_  abt '[] a
a [Branch a abt i]
bs) (Case_  abt '[] a
a' [Branch a abt j]
bs')      = do
        (TypeEq '[] '[]
Refl, TypeEq a a
Refl) <- abt '[] a -> abt '[] a -> Maybe (TypeEq '[] '[], TypeEq a a)
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 '[] a
a abt '[] a
a'
        [(Branch a abt i, Branch a abt j)] -> Maybe (TypeEq i j)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru) (b :: Hakaru)
       (b' :: Hakaru).
(ABT Term abt, JmEq2 abt) =>
[(Branch a abt b, Branch a abt b')] -> Maybe (TypeEq b b')
jmEq_Branch ([Branch a abt i]
-> [Branch a abt j] -> [(Branch a abt i, Branch a abt j)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Branch a abt i]
bs [Branch a abt j]
bs')
    jmEq1 (Superpose_ NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
pms) (Superpose_ NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
pms') = do
      (TypeEq 'HProb 'HProb
Refl,TypeEq ('HMeasure a) ('HMeasure a)
Refl) L.:| [(TypeEq 'HProb 'HProb, TypeEq ('HMeasure a) ('HMeasure a))]
_ <- NonEmpty
  (Maybe (TypeEq 'HProb 'HProb, TypeEq ('HMeasure a) ('HMeasure a)))
-> Maybe
     (NonEmpty
        (TypeEq 'HProb 'HProb, TypeEq ('HMeasure a) ('HMeasure a)))
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
T.sequence (NonEmpty
   (Maybe (TypeEq 'HProb 'HProb, TypeEq ('HMeasure a) ('HMeasure a)))
 -> Maybe
      (NonEmpty
         (TypeEq 'HProb 'HProb, TypeEq ('HMeasure a) ('HMeasure a))))
-> NonEmpty
     (Maybe (TypeEq 'HProb 'HProb, TypeEq ('HMeasure a) ('HMeasure a)))
-> Maybe
     (NonEmpty
        (TypeEq 'HProb 'HProb, TypeEq ('HMeasure a) ('HMeasure a)))
forall a b. (a -> b) -> a -> b
$ (((abt '[] 'HProb, abt '[] ('HMeasure a)),
  (abt '[] 'HProb, abt '[] ('HMeasure a)))
 -> Maybe
      (TypeEq 'HProb 'HProb, TypeEq ('HMeasure a) ('HMeasure a)))
-> NonEmpty
     ((abt '[] 'HProb, abt '[] ('HMeasure a)),
      (abt '[] 'HProb, abt '[] ('HMeasure a)))
-> NonEmpty
     (Maybe (TypeEq 'HProb 'HProb, TypeEq ('HMeasure a) ('HMeasure a)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((abt '[] 'HProb, abt '[] ('HMeasure a)),
 (abt '[] 'HProb, abt '[] ('HMeasure a)))
-> Maybe (TypeEq 'HProb 'HProb, TypeEq ('HMeasure a) ('HMeasure a))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru) (b :: Hakaru)
       (a' :: Hakaru) (b' :: Hakaru).
(ABT Term abt, JmEq2 abt) =>
((abt '[] a, abt '[] b), (abt '[] a', abt '[] b'))
-> Maybe (TypeEq a a', TypeEq b b')
jmEq_Tuple (NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> NonEmpty
     ((abt '[] 'HProb, abt '[] ('HMeasure a)),
      (abt '[] 'HProb, abt '[] ('HMeasure a)))
forall a b. NonEmpty a -> NonEmpty b -> NonEmpty (a, b)
L.zip NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
pms NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
pms')
      TypeEq i i -> Maybe (TypeEq i i)
forall (m :: * -> *) a. Monad m => a -> m a
return TypeEq i i
forall k (a :: k). TypeEq a a
Refl
    jmEq1 Term abt i
_              Term abt j
_              = Maybe (TypeEq i j)
forall a. Maybe a
Nothing


all_jmEq2
    :: (ABT Term abt, JmEq2 abt)
    => S.Seq (abt '[] a)
    -> S.Seq (abt '[] a)
    -> Maybe ()
all_jmEq2 :: Seq (abt '[] a) -> Seq (abt '[] a) -> Maybe ()
all_jmEq2 Seq (abt '[] a)
xs Seq (abt '[] a)
ys =
    let eq :: a i1 j1 -> a i2 j2 -> Bool
eq a i1 j1
x a i2 j2
y = Maybe (TypeEq i1 i2, TypeEq j1 j2) -> Bool
forall a. Maybe a -> Bool
isJust (a i1 j1 -> a i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
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 a i1 j1
x a i2 j2
y)
    in if Seq Bool -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
F.and ((abt '[] a -> abt '[] a -> Bool)
-> Seq (abt '[] a) -> Seq (abt '[] a) -> Seq Bool
forall a b c. (a -> b -> c) -> Seq a -> Seq b -> Seq c
S.zipWith abt '[] a -> abt '[] a -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i1 :: k1) (j1 :: k2) (i2 :: k1)
       (j2 :: k2).
JmEq2 a =>
a i1 j1 -> a i2 j2 -> Bool
eq Seq (abt '[] a)
xs Seq (abt '[] a)
ys) then () -> Maybe ()
forall a. a -> Maybe a
Just () else Maybe ()
forall a. Maybe a
Nothing


jmEq_Tuple :: (ABT Term abt, JmEq2 abt)
           => ((abt '[] a , abt '[] b), 
               (abt '[] a', abt '[] b'))
           -> Maybe (TypeEq a a', TypeEq b b')
jmEq_Tuple :: ((abt '[] a, abt '[] b), (abt '[] a', abt '[] b'))
-> Maybe (TypeEq a a', TypeEq b b')
jmEq_Tuple ((abt '[] a
a,abt '[] b
b), (abt '[] a'
a',abt '[] b'
b')) = do
  TypeEq a a'
a'' <- abt '[] a -> abt '[] a' -> Maybe (TypeEq '[] '[], TypeEq a a')
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 '[] a
a abt '[] a'
a' Maybe (TypeEq '[] '[], TypeEq a a')
-> ((TypeEq '[] '[], TypeEq a a') -> Maybe (TypeEq a a'))
-> Maybe (TypeEq a a')
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\(TypeEq '[] '[]
Refl, TypeEq a a'
Refl) -> TypeEq a a -> Maybe (TypeEq a a)
forall a. a -> Maybe a
Just TypeEq a a
forall k (a :: k). TypeEq a a
Refl)
  TypeEq b b'
b'' <- abt '[] b -> abt '[] b' -> Maybe (TypeEq '[] '[], 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 abt '[] b
b abt '[] b'
b' Maybe (TypeEq '[] '[], TypeEq b b')
-> ((TypeEq '[] '[], TypeEq b b') -> Maybe (TypeEq b b'))
-> Maybe (TypeEq b b')
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\(TypeEq '[] '[]
Refl, TypeEq b b'
Refl) -> TypeEq b b -> Maybe (TypeEq b b)
forall a. a -> Maybe a
Just TypeEq b b
forall k (a :: k). TypeEq a a
Refl)
  (TypeEq a a', TypeEq b b') -> Maybe (TypeEq a a', TypeEq b b')
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeEq a a'
a'', TypeEq b b'
b'')


-- TODO: a more general function of type:
--   (JmEq2 abt) => Term abt a -> Term abt b -> Maybe (Sing a, TypeEq a b)
-- This can then be used to define typeOf and instance JmEq2 Term

instance (ABT Term abt, JmEq2 abt) => Eq1 (Term abt) where
    eq1 :: Term abt i -> Term abt i -> Bool
eq1 Term abt i
x Term abt i
y = Maybe (TypeEq i i) -> Bool
forall a. Maybe a -> Bool
isJust (Term abt i -> Term abt i -> Maybe (TypeEq i i)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Term abt i
x Term abt i
y)

instance (ABT Term abt, JmEq2 abt) => Eq (Term abt a) where
    == :: Term abt a -> Term abt a -> Bool
(==) = Term abt a -> Term abt a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1

instance ( Show1 (Sing :: k -> *)
         , JmEq1 (Sing :: k -> *)
         , JmEq1 (syn (TrivialABT syn))
         , Foldable21 syn
         ) => JmEq2 (TrivialABT (syn :: ([k] -> k -> *) -> k -> *))
    where
    jmEq2 :: TrivialABT syn i1 j1
-> TrivialABT syn i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 TrivialABT syn i1 j1
x TrivialABT syn i2 j2
y =
        case (TrivialABT syn i1 j1 -> View (syn (TrivialABT syn)) i1 j1
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT TrivialABT syn i1 j1
x, TrivialABT syn i2 j2 -> View (syn (TrivialABT syn)) i2 j2
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT TrivialABT syn i2 j2
y) of
        (Syn syn (TrivialABT syn) j1
t1, Syn syn (TrivialABT syn) j2
t2) ->
            syn (TrivialABT syn) j1
-> syn (TrivialABT syn) j2 -> Maybe (TypeEq j1 j2)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 syn (TrivialABT syn) j1
t1 syn (TrivialABT syn) j2
t2 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 '[] '[], TypeEq j1 j1)
-> Maybe (TypeEq '[] '[], TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq '[] '[]
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl) 
        (Var (Variable Text
_ Nat
_ Sing j1
t1), Var (Variable Text
_ Nat
_ Sing j2
t2)) ->
            Sing j1 -> Sing j2 -> Maybe (TypeEq j1 j2)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing j1
t1 Sing j2
t2 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 '[] '[], TypeEq j1 j1)
-> Maybe (TypeEq '[] '[], TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq '[] '[]
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
        (Bind (Variable Text
_ Nat
_ Sing a
x1) View (syn (TrivialABT syn)) xs j1
v1, Bind (Variable Text
_ Nat
_ Sing a
x2) View (syn (TrivialABT syn)) xs j2
v2) -> do
            TypeEq a a
Refl <- 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
x1 Sing a
x2
            (TypeEq xs xs
Refl,TypeEq j1 j2
Refl) <- TrivialABT syn xs j1
-> TrivialABT syn xs j2 -> Maybe (TypeEq xs xs, TypeEq j1 j2)
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 (View (syn (TrivialABT syn)) xs j1 -> TrivialABT syn xs j1
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
View (syn abt) xs a -> abt xs a
unviewABT View (syn (TrivialABT syn)) xs j1
v1) (View (syn (TrivialABT syn)) xs j2 -> TrivialABT syn xs j2
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
View (syn abt) xs a -> abt xs a
unviewABT View (syn (TrivialABT syn)) xs j2
v2)
            (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
        (View (syn (TrivialABT syn)) i1 j1,
 View (syn (TrivialABT syn)) i2 j2)
_ -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall a. Maybe a
Nothing

instance ( Show1 (Sing :: k -> *)
         , JmEq1 (Sing :: k -> *)
         , JmEq1 (syn (TrivialABT syn))
         , Foldable21 syn
         ) => JmEq1 (TrivialABT (syn :: ([k] -> k -> *) -> k -> *) xs)
    where
    jmEq1 :: TrivialABT syn xs i -> TrivialABT syn xs j -> Maybe (TypeEq i j)
jmEq1 TrivialABT syn xs i
x TrivialABT syn xs j
y = TrivialABT syn xs i
-> TrivialABT syn xs j -> Maybe (TypeEq xs xs, 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 TrivialABT syn xs i
x TrivialABT syn xs j
y Maybe (TypeEq xs xs, TypeEq i j)
-> ((TypeEq xs xs, TypeEq i j) -> Maybe (TypeEq i j))
-> Maybe (TypeEq i j)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(TypeEq xs xs
Refl, TypeEq i j
Refl) -> TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl

instance ( Show1 (Sing :: k ->  *)
         , JmEq1 (Sing :: k -> *)
         , Foldable21 syn
         , JmEq1 (syn (TrivialABT syn))
         ) => Eq2 (TrivialABT (syn :: ([k] -> k -> *) -> k -> *))
    where
    eq2 :: TrivialABT syn i j -> TrivialABT syn i j -> Bool
eq2 TrivialABT syn i j
x TrivialABT syn i j
y = Maybe (TypeEq i i, TypeEq j j) -> Bool
forall a. Maybe a -> Bool
isJust (TrivialABT syn i j
-> TrivialABT syn 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 TrivialABT syn i j
x TrivialABT syn i j
y)

instance ( Show1 (Sing :: k ->  *)
         , JmEq1 (Sing :: k -> *)
         , Foldable21 syn
         , JmEq1 (syn (TrivialABT syn))
         ) => Eq1 (TrivialABT (syn :: ([k] -> k -> *) -> k -> *) xs)
    where
    eq1 :: TrivialABT syn xs i -> TrivialABT syn xs i -> Bool
eq1 = TrivialABT syn xs i -> TrivialABT syn xs i -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2

instance ( Show1 (Sing :: k ->  *)
         , JmEq1 (Sing :: k -> *)
         , Foldable21 syn
         , JmEq1 (syn (TrivialABT syn))
         ) => Eq (TrivialABT (syn :: ([k] -> k -> *) -> k -> *) xs a)
    where
    == :: TrivialABT syn xs a -> TrivialABT syn xs a -> Bool
(==) = TrivialABT syn xs a -> TrivialABT syn xs a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1


type Varmap = Assocs (Variable :: Hakaru -> *)

void_jmEq1
    :: Sing (a :: Hakaru)
    -> Sing (b :: Hakaru)
    -> ReaderT Varmap Maybe ()
void_jmEq1 :: Sing a -> Sing b -> ReaderT Varmap Maybe ()
void_jmEq1 Sing a
x Sing b
y = Maybe (TypeEq a b) -> ReaderT Varmap Maybe (TypeEq a b)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (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
x Sing b
y) ReaderT Varmap Maybe (TypeEq a b)
-> ReaderT Varmap Maybe () -> ReaderT Varmap Maybe ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> ReaderT Varmap Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

void_varEq
    :: Variable (a :: Hakaru)
    -> Variable (b :: Hakaru)
    -> ReaderT Varmap Maybe ()   
void_varEq :: Variable a -> Variable b -> ReaderT Varmap Maybe ()
void_varEq Variable a
x Variable b
y = Maybe (TypeEq a b) -> ReaderT Varmap Maybe (TypeEq a b)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Variable a -> Variable b -> Maybe (TypeEq a b)
forall k (a :: k) (b :: k).
(Show1 Sing, JmEq1 Sing) =>
Variable a -> Variable b -> Maybe (TypeEq a b)
varEq Variable a
x Variable b
y) ReaderT Varmap Maybe (TypeEq a b)
-> ReaderT Varmap Maybe () -> ReaderT Varmap Maybe ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> ReaderT Varmap Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

try_bool :: Bool -> ReaderT Varmap Maybe ()
try_bool :: Bool -> ReaderT Varmap Maybe ()
try_bool Bool
b = Maybe () -> ReaderT Varmap Maybe ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Maybe () -> ReaderT Varmap Maybe ())
-> Maybe () -> ReaderT Varmap Maybe ()
forall a b. (a -> b) -> a -> b
$ if Bool
b then () -> Maybe ()
forall a. a -> Maybe a
Just () else Maybe ()
forall a. Maybe a
Nothing

split :: [a] -> [(a,[a])]
split :: [a] -> [(a, [a])]
split [a]
xs = ([a] -> [a] -> (a, [a])) -> [[a]] -> [[a]] -> [(a, [a])]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\[a]
as (a
b:[a]
bs)->(a
b,[a]
as[a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++[a]
bs)) ([a] -> [[a]]
forall a. [a] -> [[a]]
inits [a]
xs) ([[a]] -> [[a]]
forall a. [a] -> [a]
init ([[a]] -> [[a]]) -> [[a]] -> [[a]]
forall a b. (a -> b) -> a -> b
$ [a] -> [[a]]
forall a. [a] -> [[a]]
tails [a]
xs)

zipWithSetM :: MonadPlus m => (a -> a -> m ()) -> [a] -> [a] -> m ()
zipWithSetM :: (a -> a -> m ()) -> [a] -> [a] -> m ()
zipWithSetM a -> a -> m ()
_ [] [a]
ys = Bool -> m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard ([a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
ys)
zipWithSetM a -> a -> m ()
q (a
x:[a]
xs) [a]
ys = [m ()] -> m ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ a -> a -> m ()
q a
x a
y m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (a -> a -> m ()) -> [a] -> [a] -> m ()
forall (m :: * -> *) a.
MonadPlus m =>
(a -> a -> m ()) -> [a] -> [a] -> m ()
zipWithSetM a -> a -> m ()
q [a]
xs [a]
ys' | (a
y,[a]
ys') <- [a] -> [(a, [a])]
forall a. [a] -> [(a, [a])]
split [a]
ys ]

zipWithSetMF :: (MonadPlus m, F.Foldable f) => (a -> a -> m ()) -> f a -> f a -> m ()
zipWithSetMF :: (a -> a -> m ()) -> f a -> f a -> m ()
zipWithSetMF a -> a -> m ()
q f a
a f a
b = (a -> a -> m ()) -> [a] -> [a] -> m ()
forall (m :: * -> *) a.
MonadPlus m =>
(a -> a -> m ()) -> [a] -> [a] -> m ()
zipWithSetM a -> a -> m ()
q (f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList f a
a) (f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList f a
b)


alphaEq
    :: forall abt d
    .  (ABT Term abt)
    => abt '[] d
    -> abt '[] d
    -> Bool
alphaEq :: abt '[] d -> abt '[] d -> Bool
alphaEq abt '[] d
e1 abt '[] d
e2 =
    Bool -> (() -> Bool) -> Maybe () -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> () -> Bool
forall a b. a -> b -> a
const Bool
True)
        (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ ReaderT Varmap Maybe () -> Varmap -> Maybe ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (View (Term abt) '[] d
-> View (Term abt) '[] d -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt '[] d -> View (Term abt) '[] d
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] d
e1) (abt '[] d -> View (Term abt) '[] d
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] d
e2)) Varmap
forall k (abt :: k -> *). Assocs abt
emptyAssocs
    where
    -- Don't compare @x@ to @y@ directly; instead,
    -- look up whatever @x@ renames to (i.e., @y'@)
    -- and then see whether that is equal to @y@.
    go  :: forall xs1 xs2 a
        .  View (Term abt) xs1 a
        -> View (Term abt) xs2 a
        -> ReaderT Varmap Maybe ()
    go :: View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (Var Variable a
x) (Var Variable a
y) = do
        Varmap
s <- ReaderT Varmap Maybe Varmap
forall r (m :: * -> *). MonadReader r m => m r
ask
        case Variable a -> Varmap -> Maybe (Variable a)
forall k (a :: k) (ast :: k -> *).
(Show1 Sing, JmEq1 Sing) =>
Variable a -> Assocs ast -> Maybe (ast a)
lookupAssoc Variable a
x Varmap
s of
            Maybe (Variable a)
Nothing -> Variable a -> Variable a -> ReaderT Varmap Maybe ()
forall (a :: Hakaru) (b :: Hakaru).
Variable a -> Variable b -> ReaderT Varmap Maybe ()
void_varEq Variable a
x  Variable a
y -- free variables
            Just Variable a
y' -> Variable a -> Variable a -> ReaderT Varmap Maybe ()
forall (a :: Hakaru) (b :: Hakaru).
Variable a -> Variable b -> ReaderT Varmap Maybe ()
void_varEq Variable a
y' Variable a
y

    -- remember that @x@ renames to @y@ and recurse
    go (Bind Variable a
x View (Term abt) xs a
e1) (Bind Variable a
y View (Term abt) xs a
e2) = do
        TypeEq a a
Refl <- Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a))
-> Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall a b. (a -> b) -> a -> b
$ 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 (Variable a -> Sing a
forall k (a :: k). Variable a -> Sing a
varType Variable a
x) (Variable a -> Sing a
forall k (a :: k). Variable a -> Sing a
varType Variable a
y)
        (Varmap -> Varmap)
-> ReaderT Varmap Maybe () -> ReaderT Varmap Maybe ()
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (Assoc Variable -> Varmap -> Varmap
forall k (ast :: k -> *). Assoc ast -> Assocs ast -> Assocs ast
insertAssoc (Variable a -> Variable a -> Assoc Variable
forall k (ast :: k -> *) (a :: k). Variable a -> ast a -> Assoc ast
Assoc Variable a
x Variable a
Variable a
y)) (View (Term abt) xs a
-> View (Term abt) xs a -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go View (Term abt) xs a
e1 View (Term abt) xs a
e2)

    -- perform the core comparison for syntactic equality
    go (Syn Term abt a
t1) (Syn Term abt a
t2) = Term abt a -> Term abt a -> ReaderT Varmap Maybe ()
forall (a :: Hakaru).
Term abt a -> Term abt a -> ReaderT Varmap Maybe ()
termEq Term abt a
t1 Term abt a
t2

    -- if the views don't match, then clearly they are not equal.
    go View (Term abt) xs1 a
_ View (Term abt) xs2 a
_ = Maybe () -> ReaderT Varmap Maybe ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Maybe ()
forall a. Maybe a
Nothing

    termEq :: forall a
        .  Term abt a
        -> Term abt a
        -> ReaderT Varmap Maybe ()
    termEq :: Term abt a -> Term abt a -> ReaderT Varmap Maybe ()
termEq Term abt a
e1 Term abt a
e2 =
        case (Term abt a
e1, Term abt a
e2) of
        (SCon args a
o1 :$ SArgs abt args
es1, SCon args a
o2 :$ SArgs abt args
es2)             -> SCon args a
-> SArgs abt args
-> SCon args a
-> SArgs abt args
-> ReaderT Varmap Maybe ()
forall (a :: Hakaru) (args1 :: [([Hakaru], Hakaru)])
       (args2 :: [([Hakaru], Hakaru)]).
SCon args1 a
-> SArgs abt args1
-> SCon args2 a
-> SArgs abt args2
-> ReaderT Varmap Maybe ()
sConEq SCon args a
o1 SArgs abt args
es1 SCon args a
o2 SArgs abt args
es2
        (NaryOp_ NaryOp a
op1 Seq (abt '[] a)
es1, NaryOp_ NaryOp a
op2 Seq (abt '[] a)
es2) -> do
            Bool -> ReaderT Varmap Maybe ()
try_bool (NaryOp a
op1 NaryOp a -> NaryOp a -> Bool
forall a. Eq a => a -> a -> Bool
== NaryOp a
op2)
            (View (Term abt) '[] a
 -> View (Term abt) '[] a -> ReaderT Varmap Maybe ())
-> Seq (View (Term abt) '[] a)
-> Seq (View (Term abt) '[] a)
-> ReaderT Varmap Maybe ()
forall (m :: * -> *) (f :: * -> *) a.
(MonadPlus m, Foldable f) =>
(a -> a -> m ()) -> f a -> f a -> m ()
zipWithSetMF View (Term abt) '[] a
-> View (Term abt) '[] a -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt '[] a -> View (Term abt) '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT (abt '[] a -> View (Term abt) '[] a)
-> Seq (abt '[] a) -> Seq (View (Term abt) '[] a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Seq (abt '[] a)
es1) (abt '[] a -> View (Term abt) '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT (abt '[] a -> View (Term abt) '[] a)
-> Seq (abt '[] a) -> Seq (View (Term abt) '[] a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Seq (abt '[] a)
es2)
        (Literal_ Literal a
x, Literal_ Literal a
y)           -> Bool -> ReaderT Varmap Maybe ()
try_bool (Literal a
x Literal a -> Literal a -> Bool
forall a. Eq a => a -> a -> Bool
== Literal a
y)
        (Empty_ Sing ('HArray a)
x, Empty_ Sing ('HArray a)
y)               -> Sing ('HArray a) -> Sing ('HArray a) -> ReaderT Varmap Maybe ()
forall (a :: Hakaru) (b :: Hakaru).
Sing a -> Sing b -> ReaderT Varmap Maybe ()
void_jmEq1 Sing ('HArray a)
x Sing ('HArray a)
y
        (Datum_ Datum (abt '[]) (HData' t)
d1, Datum_ Datum (abt '[]) (HData' t)
d2)             -> Datum (abt '[]) (HData' t)
-> Datum (abt '[]) (HData' t) -> ReaderT Varmap Maybe ()
forall (a :: Hakaru).
Datum (abt '[]) a -> Datum (abt '[]) a -> ReaderT Varmap Maybe ()
datumEq Datum (abt '[]) (HData' t)
d1 Datum (abt '[]) (HData' t)
Datum (abt '[]) (HData' t)
d2
        (Array_ abt '[] 'HNat
n1 abt '[ 'HNat] a
e1, Array_ abt '[] 'HNat
n2 abt '[ 'HNat] a
e2)       -> do
            View (Term abt) '[] 'HNat
-> View (Term abt) '[] 'HNat -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt '[] 'HNat -> View (Term abt) '[] 'HNat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] 'HNat
n1) (abt '[] 'HNat -> View (Term abt) '[] 'HNat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] 'HNat
n2)
            View (Term abt) '[ 'HNat] a
-> View (Term abt) '[ 'HNat] a -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt '[ 'HNat] a -> View (Term abt) '[ 'HNat] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[ 'HNat] a
e1) (abt '[ 'HNat] a -> View (Term abt) '[ 'HNat] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[ 'HNat] a
e2)
        (ArrayLiteral_ [abt '[] a]
es, ArrayLiteral_ [abt '[] a]
es') ->
            [ReaderT Varmap Maybe ()] -> ReaderT Varmap Maybe ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
F.sequence_ ([ReaderT Varmap Maybe ()] -> ReaderT Varmap Maybe ())
-> [ReaderT Varmap Maybe ()] -> ReaderT Varmap Maybe ()
forall a b. (a -> b) -> a -> b
$ (View (Term abt) '[] a
 -> View (Term abt) '[] a -> ReaderT Varmap Maybe ())
-> [View (Term abt) '[] a]
-> [View (Term abt) '[] a]
-> [ReaderT Varmap Maybe ()]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith View (Term abt) '[] a
-> View (Term abt) '[] a -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt '[] a -> View (Term abt) '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT (abt '[] a -> View (Term abt) '[] a)
-> [abt '[] a] -> [View (Term abt) '[] a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [abt '[] a]
es) (abt '[] a -> View (Term abt) '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT (abt '[] a -> View (Term abt) '[] a)
-> [abt '[] a] -> [View (Term abt) '[] a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [abt '[] a]
es')
        (Bucket abt '[] 'HNat
a abt '[] 'HNat
b Reducer abt '[] a
r, Bucket abt '[] 'HNat
a' abt '[] 'HNat
b' Reducer abt '[] a
r')    -> do
            View (Term abt) '[] 'HNat
-> View (Term abt) '[] 'HNat -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt '[] 'HNat -> View (Term abt) '[] 'HNat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] 'HNat
a) (abt '[] 'HNat -> View (Term abt) '[] 'HNat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] 'HNat
a')
            View (Term abt) '[] 'HNat
-> View (Term abt) '[] 'HNat -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt '[] 'HNat -> View (Term abt) '[] 'HNat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] 'HNat
b) (abt '[] 'HNat -> View (Term abt) '[] 'HNat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] 'HNat
b')
            Reducer abt '[] a -> Reducer abt '[] a -> ReaderT Varmap Maybe ()
forall (xs :: [Hakaru]) (b :: Hakaru).
Reducer abt xs b -> Reducer abt xs b -> ReaderT Varmap Maybe ()
reducerEq Reducer abt '[] a
r Reducer abt '[] a
r'
        (Case_ abt '[] a
e1 [Branch a abt a]
bs1, Case_ abt '[] a
e2 [Branch a abt a]
bs2)       -> do
            TypeEq a a
Refl <- Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a))
-> Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall a b. (a -> b) -> a -> b
$ 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 (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] a
e1) (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] a
e2)
            View (Term abt) '[] a
-> View (Term abt) '[] a -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt '[] a -> View (Term abt) '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] a
e1) (abt '[] a -> View (Term abt) '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] a
e2)
            (Branch a abt a -> Branch a abt a -> ReaderT Varmap Maybe ())
-> [Branch a abt a] -> [Branch a abt a] -> ReaderT Varmap Maybe ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ Branch a abt a -> Branch a abt a -> ReaderT Varmap Maybe ()
forall (c :: Hakaru) (b :: Hakaru).
Branch c abt b -> Branch c abt b -> ReaderT Varmap Maybe ()
sBranch [Branch a abt a]
bs1 [Branch a abt a]
[Branch a abt a]
bs2
        (Superpose_ NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
pms1, Superpose_ NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
pms2) ->
            ((abt '[] 'HProb, abt '[] ('HMeasure a))
 -> (abt '[] 'HProb, abt '[] ('HMeasure a))
 -> ReaderT Varmap Maybe ())
-> NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> ReaderT Varmap Maybe ()
forall (m :: * -> *) (f :: * -> *) a.
(MonadPlus m, Foldable f) =>
(a -> a -> m ()) -> f a -> f a -> m ()
zipWithSetMF (abt '[] 'HProb, abt '[] ('HMeasure a))
-> (abt '[] 'HProb, abt '[] ('HMeasure a))
-> ReaderT Varmap Maybe ()
forall (c :: Hakaru) (b :: Hakaru).
(abt '[] c, abt '[] b)
-> (abt '[] c, abt '[] b) -> ReaderT Varmap Maybe ()
pairEq NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
pms1 NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
pms2
        (Reject_ Sing ('HMeasure a)
x, Reject_ Sing ('HMeasure a)
y)             -> Sing ('HMeasure a) -> Sing ('HMeasure a) -> ReaderT Varmap Maybe ()
forall (a :: Hakaru) (b :: Hakaru).
Sing a -> Sing b -> ReaderT Varmap Maybe ()
void_jmEq1 Sing ('HMeasure a)
x Sing ('HMeasure a)
y
        (Term abt a
_, Term abt a
_)                             -> Maybe () -> ReaderT Varmap Maybe ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Maybe ()
forall a. Maybe a
Nothing

    sArgsEq
        :: forall args
        .  SArgs abt args
        -> SArgs abt args
        -> ReaderT Varmap Maybe ()
    sArgsEq :: SArgs abt args -> SArgs abt args -> ReaderT Varmap Maybe ()
sArgsEq SArgs abt args
End         SArgs abt args
End         = () -> ReaderT Varmap Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    sArgsEq (abt vars a
e1 :* SArgs abt args
es1) (abt vars a
e2 :* SArgs abt args
es2) = do
        View (Term abt) vars a
-> View (Term abt) vars a -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e1) (abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e2)
        SArgs abt args -> SArgs abt args -> ReaderT Varmap Maybe ()
forall (args :: [([Hakaru], Hakaru)]).
SArgs abt args -> SArgs abt args -> ReaderT Varmap Maybe ()
sArgsEq SArgs abt args
es1 SArgs abt args
SArgs abt args
es2

    sConEq
        :: forall a args1 args2
        .  SCon  args1 a
        -> SArgs abt args1
        -> SCon args2 a
        -> SArgs abt args2
        -> ReaderT Varmap Maybe ()
    sConEq :: SCon args1 a
-> SArgs abt args1
-> SCon args2 a
-> SArgs abt args2
-> ReaderT Varmap Maybe ()
sConEq SCon args1 a
Lam_   SArgs abt args1
e1
           SCon args2 a
Lam_   SArgs abt args2
e2 = SArgs abt args1 -> SArgs abt args1 -> ReaderT Varmap Maybe ()
forall (args :: [([Hakaru], Hakaru)]).
SArgs abt args -> SArgs abt args -> ReaderT Varmap Maybe ()
sArgsEq SArgs abt args1
e1 SArgs abt args1
SArgs abt args2
e2

    sConEq SCon args1 a
App_   (abt vars a
e1  :* abt vars a
e2  :* SArgs abt args
End)
           SCon args2 a
App_   (abt vars a
e1' :* abt vars a
e2' :* SArgs abt args
End) = do
        TypeEq a a
Refl <- Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a))
-> Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall a b. (a -> b) -> a -> b
$ 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 (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt vars a
abt '[] a
e2) (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt vars a
abt '[] a
e2')
        View (Term abt) vars a
-> View (Term abt) vars a -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e1) (abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e1')
        View (Term abt) vars a
-> View (Term abt) vars a -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e2) (abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e2')

    sConEq SCon args1 a
Let_   (abt vars a
e1  :* abt vars a
e2  :* SArgs abt args
End)
           SCon args2 a
Let_   (abt vars a
e1' :* abt vars a
e2' :* SArgs abt args
End) = do
        TypeEq a a
Refl <- Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a))
-> Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall a b. (a -> b) -> a -> b
$ 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 (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt vars a
abt '[] a
e1) (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt vars a
abt '[] a
e1')
        View (Term abt) vars a
-> View (Term abt) vars a -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e1) (abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e1')
        View (Term abt) vars a
-> View (Term abt) vars a -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e2) (abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e2')

    sConEq (CoerceTo_ Coercion a a
_) (abt vars a
e1 :* SArgs abt args
End)
           (CoerceTo_ Coercion a a
_) (abt vars a
e2 :* SArgs abt args
End) = do
        TypeEq a a
Refl <- Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a))
-> Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall a b. (a -> b) -> a -> b
$ 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 (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt vars a
abt '[] a
e1) (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt vars a
abt '[] a
e2)
        View (Term abt) vars a
-> View (Term abt) vars a -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e1) (abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e2)

    sConEq (UnsafeFrom_ Coercion a b
_) (abt vars a
e1 :* SArgs abt args
End)
           (UnsafeFrom_ Coercion a b
_) (abt vars a
e2 :* SArgs abt args
End) = do
        TypeEq a a
Refl <- Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a))
-> Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall a b. (a -> b) -> a -> b
$ 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 (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt vars a
abt '[] a
e1) (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt vars a
abt '[] a
e2)
        View (Term abt) vars a
-> View (Term abt) vars a -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e1) (abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e2)

    sConEq (PrimOp_ PrimOp typs a
o1) SArgs abt args1
es1
           (PrimOp_ PrimOp typs a
o2) SArgs abt args2
es2    = PrimOp typs a
-> SArgs abt args1
-> PrimOp typs a
-> SArgs abt args2
-> ReaderT Varmap Maybe ()
forall (a :: Hakaru) (typs1 :: [Hakaru]) (typs2 :: [Hakaru])
       (args1 :: [([Hakaru], Hakaru)]) (args2 :: [([Hakaru], Hakaru)]).
(typs1 ~ UnLCs args1, args1 ~ LCs typs1, typs2 ~ UnLCs args2,
 args2 ~ LCs typs2) =>
PrimOp typs1 a
-> SArgs abt args1
-> PrimOp typs2 a
-> SArgs abt args2
-> ReaderT Varmap Maybe ()
primOpEq PrimOp typs a
o1 SArgs abt args1
es1 PrimOp typs a
o2 SArgs abt args2
es2

    sConEq (ArrayOp_ ArrayOp typs a
o1) SArgs abt args1
es1
           (ArrayOp_ ArrayOp typs a
o2) SArgs abt args2
es2   = ArrayOp typs a
-> SArgs abt args1
-> ArrayOp typs a
-> SArgs abt args2
-> ReaderT Varmap Maybe ()
forall (a :: Hakaru) (typs1 :: [Hakaru]) (typs2 :: [Hakaru])
       (args1 :: [([Hakaru], Hakaru)]) (args2 :: [([Hakaru], Hakaru)]).
(typs1 ~ UnLCs args1, args1 ~ LCs typs1, typs2 ~ UnLCs args2,
 args2 ~ LCs typs2) =>
ArrayOp typs1 a
-> SArgs abt args1
-> ArrayOp typs2 a
-> SArgs abt args2
-> ReaderT Varmap Maybe ()
arrayOpEq ArrayOp typs a
o1 SArgs abt args1
es1 ArrayOp typs a
o2 SArgs abt args2
es2

    sConEq (MeasureOp_ MeasureOp typs a
o1) SArgs abt args1
es1
           (MeasureOp_ MeasureOp typs a
o2) SArgs abt args2
es2 = MeasureOp typs a
-> SArgs abt args1
-> MeasureOp typs a
-> SArgs abt args2
-> ReaderT Varmap Maybe ()
forall (a :: Hakaru) (typs1 :: [Hakaru]) (typs2 :: [Hakaru])
       (args1 :: [([Hakaru], Hakaru)]) (args2 :: [([Hakaru], Hakaru)]).
(typs1 ~ UnLCs args1, args1 ~ LCs typs1, typs2 ~ UnLCs args2,
 args2 ~ LCs typs2) =>
MeasureOp typs1 a
-> SArgs abt args1
-> MeasureOp typs2 a
-> SArgs abt args2
-> ReaderT Varmap Maybe ()
measureOpEq MeasureOp typs a
o1 SArgs abt args1
es1 MeasureOp typs a
MeasureOp typs a
o2 SArgs abt args2
es2

    sConEq SCon args1 a
Dirac SArgs abt args1
e1
           SCon args2 a
Dirac SArgs abt args2
e2            = SArgs abt args1 -> SArgs abt args1 -> ReaderT Varmap Maybe ()
forall (args :: [([Hakaru], Hakaru)]).
SArgs abt args -> SArgs abt args -> ReaderT Varmap Maybe ()
sArgsEq SArgs abt args1
e1 SArgs abt args1
SArgs abt args2
e2

    sConEq SCon args1 a
MBind (abt vars a
e1  :* abt vars a
e2  :* SArgs abt args
End)
           SCon args2 a
MBind (abt vars a
e1' :* abt vars a
e2' :* SArgs abt args
End) = do
        TypeEq a a
Refl <- Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a))
-> Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall a b. (a -> b) -> a -> b
$ 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 (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt vars a
abt '[] a
e1) (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt vars a
abt '[] a
e1')
        View (Term abt) vars a
-> View (Term abt) vars a -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e1) (abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e1')
        View (Term abt) vars a
-> View (Term abt) vars a -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e2) (abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e2')

    sConEq SCon args1 a
Plate     SArgs abt args1
e1 SCon args2 a
Plate     SArgs abt args2
e2    = SArgs abt args1 -> SArgs abt args1 -> ReaderT Varmap Maybe ()
forall (args :: [([Hakaru], Hakaru)]).
SArgs abt args -> SArgs abt args -> ReaderT Varmap Maybe ()
sArgsEq SArgs abt args1
e1 SArgs abt args1
SArgs abt args2
e2
    sConEq SCon args1 a
Chain     SArgs abt args1
e1 SCon args2 a
Chain     SArgs abt args2
e2    = SArgs abt args1 -> SArgs abt args1 -> ReaderT Varmap Maybe ()
forall (args :: [([Hakaru], Hakaru)]).
SArgs abt args -> SArgs abt args -> ReaderT Varmap Maybe ()
sArgsEq SArgs abt args1
e1 SArgs abt args1
SArgs abt args2
e2
    sConEq SCon args1 a
Integrate SArgs abt args1
e1 SCon args2 a
Integrate SArgs abt args2
e2    = SArgs abt args1 -> SArgs abt args1 -> ReaderT Varmap Maybe ()
forall (args :: [([Hakaru], Hakaru)]).
SArgs abt args -> SArgs abt args -> ReaderT Varmap Maybe ()
sArgsEq SArgs abt args1
e1 SArgs abt args1
SArgs abt args2
e2

    sConEq (Summate HDiscrete a
h1 HSemiring a
h2) SArgs abt args1
e1 (Summate HDiscrete a
h1' HSemiring a
h2') SArgs abt args2
e2 = do
        TypeEq a a
Refl <- Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a))
-> Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall a b. (a -> b) -> a -> b
$ 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 (HDiscrete a -> Sing a
forall (a :: Hakaru). HDiscrete a -> Sing a
sing_HDiscrete HDiscrete a
h1) (HDiscrete a -> Sing a
forall (a :: Hakaru). HDiscrete a -> Sing a
sing_HDiscrete HDiscrete a
h1')
        TypeEq a a
Refl <- Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a))
-> Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall a b. (a -> b) -> a -> b
$ 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 (HSemiring a -> Sing a
forall (a :: Hakaru). HSemiring a -> Sing a
sing_HSemiring HSemiring a
h2) (HSemiring a -> Sing a
forall (a :: Hakaru). HSemiring a -> Sing a
sing_HSemiring HSemiring a
h2')
        SArgs abt args1 -> SArgs abt args1 -> ReaderT Varmap Maybe ()
forall (args :: [([Hakaru], Hakaru)]).
SArgs abt args -> SArgs abt args -> ReaderT Varmap Maybe ()
sArgsEq SArgs abt args1
e1 SArgs abt args1
SArgs abt args2
e2

    sConEq (Product HDiscrete a
h1 HSemiring a
h2) SArgs abt args1
e1 (Product HDiscrete a
h1' HSemiring a
h2') SArgs abt args2
e2 = do
        TypeEq a a
Refl <- Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a))
-> Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall a b. (a -> b) -> a -> b
$ 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 (HDiscrete a -> Sing a
forall (a :: Hakaru). HDiscrete a -> Sing a
sing_HDiscrete HDiscrete a
h1) (HDiscrete a -> Sing a
forall (a :: Hakaru). HDiscrete a -> Sing a
sing_HDiscrete HDiscrete a
h1')
        TypeEq a a
Refl <- Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a))
-> Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall a b. (a -> b) -> a -> b
$ 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 (HSemiring a -> Sing a
forall (a :: Hakaru). HSemiring a -> Sing a
sing_HSemiring HSemiring a
h2) (HSemiring a -> Sing a
forall (a :: Hakaru). HSemiring a -> Sing a
sing_HSemiring HSemiring a
h2')
        SArgs abt args1 -> SArgs abt args1 -> ReaderT Varmap Maybe ()
forall (args :: [([Hakaru], Hakaru)]).
SArgs abt args -> SArgs abt args -> ReaderT Varmap Maybe ()
sArgsEq SArgs abt args1
e1 SArgs abt args1
SArgs abt args2
e2

    sConEq (Transform_ Transform args1 a
t1) SArgs abt args1
e1
           (Transform_ Transform args2 a
t2) SArgs abt args2
e2 = Transform args1 a
-> SArgs abt args1
-> Transform args2 a
-> SArgs abt args2
-> ReaderT Varmap Maybe ()
forall (args1 :: [([Hakaru], Hakaru)]) (a1 :: Hakaru)
       (args2 :: [([Hakaru], Hakaru)]).
Transform args1 a1
-> SArgs abt args1
-> Transform args2 a1
-> SArgs abt args2
-> ReaderT Varmap Maybe ()
transformEq Transform args1 a
t1 SArgs abt args1
e1 Transform args2 a
t2 SArgs abt args2
e2

    sConEq SCon args1 a
_ SArgs abt args1
_ SCon args2 a
_ SArgs abt args2
_ = Maybe () -> ReaderT Varmap Maybe ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Maybe ()
forall a. Maybe a
Nothing

    transformEq
        :: Transform args1 a1
        -> SArgs abt args1
        -> Transform args2 a1
        -> SArgs abt args2
        -> ReaderT Varmap Maybe ()
    transformEq :: Transform args1 a1
-> SArgs abt args1
-> Transform args2 a1
-> SArgs abt args2
-> ReaderT Varmap Maybe ()
transformEq Transform args1 a1
t0 SArgs abt args1
e0 Transform args2 a1
t1 SArgs abt args2
e1 =
      case (Transform args1 a1
t0, Transform args2 a1
t1) of
        -- Special case needed because some type variables in the input do not
        -- appear in the output
        (Transform args1 a1
Expect   , Transform args2 a1
Expect   ) ->
          case (SArgs abt args1
e0, SArgs abt args2
e1) of
           (abt vars a
e1  :* abt vars a
e2  :* SArgs abt args
End,
            abt vars a
e1' :* abt vars a
e2' :* SArgs abt args
End) -> do
             TypeEq a a
Refl <- Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a))
-> Maybe (TypeEq a a) -> ReaderT Varmap Maybe (TypeEq a a)
forall a b. (a -> b) -> a -> b
$ 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 (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt vars a
abt '[] a
e1) (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt vars a
abt '[] a
e1')
             View (Term abt) vars a
-> View (Term abt) vars a -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e1) (abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e1')
             View (Term abt) vars a
-> View (Term abt) vars a -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e2) (abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e2')
        (Transform args1 a1
Observe  , Transform args2 a1
Observe  ) -> SArgs abt args1 -> SArgs abt args1 -> ReaderT Varmap Maybe ()
forall (args :: [([Hakaru], Hakaru)]).
SArgs abt args -> SArgs abt args -> ReaderT Varmap Maybe ()
sArgsEq SArgs abt args1
e0 SArgs abt args1
SArgs abt args2
e1
        (Transform args1 a1
MH       , Transform args2 a1
MH       ) -> SArgs abt args1 -> SArgs abt args1 -> ReaderT Varmap Maybe ()
forall (args :: [([Hakaru], Hakaru)]).
SArgs abt args -> SArgs abt args -> ReaderT Varmap Maybe ()
sArgsEq SArgs abt args1
e0 SArgs abt args1
SArgs abt args2
e1
        (Transform args1 a1
MCMC     , Transform args2 a1
MCMC     ) -> SArgs abt args1 -> SArgs abt args1 -> ReaderT Varmap Maybe ()
forall (args :: [([Hakaru], Hakaru)]).
SArgs abt args -> SArgs abt args -> ReaderT Varmap Maybe ()
sArgsEq SArgs abt args1
e0 SArgs abt args1
SArgs abt args2
e1
        (Disint TransformImpl
k0, Disint TransformImpl
k1) ->
          if TransformImpl
k0TransformImpl -> TransformImpl -> Bool
forall a. Eq a => a -> a -> Bool
==TransformImpl
k1 then SArgs abt args1 -> SArgs abt args1 -> ReaderT Varmap Maybe ()
forall (args :: [([Hakaru], Hakaru)]).
SArgs abt args -> SArgs abt args -> ReaderT Varmap Maybe ()
sArgsEq SArgs abt args1
e0 SArgs abt args1
SArgs abt args2
e1 else Maybe () -> ReaderT Varmap Maybe ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Maybe ()
forall a. Maybe a
Nothing
        (Transform args1 a1
Summarize, Transform args2 a1
Summarize) -> SArgs abt args1 -> SArgs abt args1 -> ReaderT Varmap Maybe ()
forall (args :: [([Hakaru], Hakaru)]).
SArgs abt args -> SArgs abt args -> ReaderT Varmap Maybe ()
sArgsEq SArgs abt args1
e0 SArgs abt args1
SArgs abt args2
e1
        (Transform args1 a1
Simplify , Transform args2 a1
Simplify ) -> SArgs abt args1 -> SArgs abt args1 -> ReaderT Varmap Maybe ()
forall (args :: [([Hakaru], Hakaru)]).
SArgs abt args -> SArgs abt args -> ReaderT Varmap Maybe ()
sArgsEq SArgs abt args1
e0 SArgs abt args1
SArgs abt args2
e1
        (Transform args1 a1
Reparam  , Transform args2 a1
Reparam  ) -> SArgs abt args1 -> SArgs abt args1 -> ReaderT Varmap Maybe ()
forall (args :: [([Hakaru], Hakaru)]).
SArgs abt args -> SArgs abt args -> ReaderT Varmap Maybe ()
sArgsEq SArgs abt args1
e0 SArgs abt args1
SArgs abt args2
e1
        (Transform args1 a1, Transform args2 a1)
_                      -> Maybe () -> ReaderT Varmap Maybe ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Maybe ()
forall a. Maybe a
Nothing

    primOpEq
        :: forall a typs1 typs2 args1 args2
        .  (typs1 ~ UnLCs args1, args1 ~ LCs typs1,
            typs2 ~ UnLCs args2, args2 ~ LCs typs2)
        => PrimOp typs1 a -> SArgs abt args1
        -> PrimOp typs2 a -> SArgs abt args2
        -> ReaderT Varmap Maybe ()
    primOpEq :: PrimOp typs1 a
-> SArgs abt args1
-> PrimOp typs2 a
-> SArgs abt args2
-> ReaderT Varmap Maybe ()
primOpEq PrimOp typs1 a
p1 SArgs abt args1
e1' PrimOp typs2 a
p2 SArgs abt args2
e2' = do
        (TypeEq typs1 typs2
Refl, TypeEq a a
Refl) <- Maybe (TypeEq typs1 typs2, TypeEq a a)
-> ReaderT Varmap Maybe (TypeEq typs1 typs2, TypeEq a a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Maybe (TypeEq typs1 typs2, TypeEq a a)
 -> ReaderT Varmap Maybe (TypeEq typs1 typs2, TypeEq a a))
-> Maybe (TypeEq typs1 typs2, TypeEq a a)
-> ReaderT Varmap Maybe (TypeEq typs1 typs2, TypeEq a a)
forall a b. (a -> b) -> a -> b
$ PrimOp typs1 a
-> PrimOp typs2 a -> Maybe (TypeEq typs1 typs2, TypeEq a a)
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 PrimOp typs1 a
p1 PrimOp typs2 a
p2
        SArgs abt args1 -> SArgs abt args1 -> ReaderT Varmap Maybe ()
forall (args :: [([Hakaru], Hakaru)]).
SArgs abt args -> SArgs abt args -> ReaderT Varmap Maybe ()
sArgsEq SArgs abt args1
e1' SArgs abt args1
SArgs abt args2
e2'

    arrayOpEq
        :: forall a typs1 typs2 args1 args2
        .  (typs1 ~ UnLCs args1, args1 ~ LCs typs1,
            typs2 ~ UnLCs args2, args2 ~ LCs typs2)
        => ArrayOp typs1 a -> SArgs abt args1
        -> ArrayOp typs2 a -> SArgs abt args2
        -> ReaderT Varmap Maybe ()
    arrayOpEq :: ArrayOp typs1 a
-> SArgs abt args1
-> ArrayOp typs2 a
-> SArgs abt args2
-> ReaderT Varmap Maybe ()
arrayOpEq ArrayOp typs1 a
p1 SArgs abt args1
e1 ArrayOp typs2 a
p2 SArgs abt args2
e2 = do
        (TypeEq typs1 typs2
Refl, TypeEq a a
Refl) <- Maybe (TypeEq typs1 typs2, TypeEq a a)
-> ReaderT Varmap Maybe (TypeEq typs1 typs2, TypeEq a a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Maybe (TypeEq typs1 typs2, TypeEq a a)
 -> ReaderT Varmap Maybe (TypeEq typs1 typs2, TypeEq a a))
-> Maybe (TypeEq typs1 typs2, TypeEq a a)
-> ReaderT Varmap Maybe (TypeEq typs1 typs2, TypeEq a a)
forall a b. (a -> b) -> a -> b
$ ArrayOp typs1 a
-> ArrayOp typs2 a -> Maybe (TypeEq typs1 typs2, TypeEq a a)
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 ArrayOp typs1 a
p1 ArrayOp typs2 a
p2
        SArgs abt args1 -> SArgs abt args1 -> ReaderT Varmap Maybe ()
forall (args :: [([Hakaru], Hakaru)]).
SArgs abt args -> SArgs abt args -> ReaderT Varmap Maybe ()
sArgsEq SArgs abt args1
e1 SArgs abt args1
SArgs abt args2
e2

    measureOpEq
        :: forall a typs1 typs2 args1 args2
        . (typs1 ~ UnLCs args1, args1 ~ LCs typs1,
            typs2 ~ UnLCs args2, args2 ~ LCs typs2)
        => MeasureOp typs1 a -> SArgs abt args1
        -> MeasureOp typs2 a -> SArgs abt args2
        -> ReaderT Varmap Maybe ()
    measureOpEq :: MeasureOp typs1 a
-> SArgs abt args1
-> MeasureOp typs2 a
-> SArgs abt args2
-> ReaderT Varmap Maybe ()
measureOpEq MeasureOp typs1 a
m1 SArgs abt args1
e1' MeasureOp typs2 a
m2 SArgs abt args2
e2' = do
        (TypeEq typs1 typs2
Refl,TypeEq a a
Refl) <- Maybe (TypeEq typs1 typs2, TypeEq a a)
-> ReaderT Varmap Maybe (TypeEq typs1 typs2, TypeEq a a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Maybe (TypeEq typs1 typs2, TypeEq a a)
 -> ReaderT Varmap Maybe (TypeEq typs1 typs2, TypeEq a a))
-> Maybe (TypeEq typs1 typs2, TypeEq a a)
-> ReaderT Varmap Maybe (TypeEq typs1 typs2, TypeEq a a)
forall a b. (a -> b) -> a -> b
$ MeasureOp typs1 a
-> MeasureOp typs2 a -> Maybe (TypeEq typs1 typs2, TypeEq a a)
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 MeasureOp typs1 a
m1 MeasureOp typs2 a
m2
        SArgs abt args1 -> SArgs abt args1 -> ReaderT Varmap Maybe ()
forall (args :: [([Hakaru], Hakaru)]).
SArgs abt args -> SArgs abt args -> ReaderT Varmap Maybe ()
sArgsEq SArgs abt args1
e1' SArgs abt args1
SArgs abt args2
e2'

    datumEq :: forall a
        .  Datum (abt '[]) a
        -> Datum (abt '[]) a
        -> ReaderT Varmap Maybe ()
    datumEq :: Datum (abt '[]) a -> Datum (abt '[]) a -> ReaderT Varmap Maybe ()
datumEq (Datum Text
_ Sing (HData' t)
_ DatumCode (Code t) (abt '[]) (HData' t)
d1) (Datum Text
_ Sing (HData' t)
_ DatumCode (Code t) (abt '[]) (HData' t)
d2) = DatumCode (Code t) (abt '[]) (HData' t)
-> DatumCode (Code t) (abt '[]) (HData' t)
-> ReaderT Varmap Maybe ()
forall (xss :: [[HakaruFun]]) (a :: Hakaru).
DatumCode xss (abt '[]) a
-> DatumCode xss (abt '[]) a -> ReaderT Varmap Maybe ()
datumCodeEq DatumCode (Code t) (abt '[]) (HData' t)
d1 DatumCode (Code t) (abt '[]) (HData' t)
DatumCode (Code t) (abt '[]) (HData' t)
d2

    datumCodeEq
        :: forall xss a
        .  DatumCode xss (abt '[]) a
        -> DatumCode xss (abt '[]) a
        -> ReaderT Varmap Maybe ()
    datumCodeEq :: DatumCode xss (abt '[]) a
-> DatumCode xss (abt '[]) a -> ReaderT Varmap Maybe ()
datumCodeEq (Inr DatumCode xss (abt '[]) a
c) (Inr DatumCode xss (abt '[]) a
d) = DatumCode xss (abt '[]) a
-> DatumCode xss (abt '[]) a -> ReaderT Varmap Maybe ()
forall (xss :: [[HakaruFun]]) (a :: Hakaru).
DatumCode xss (abt '[]) a
-> DatumCode xss (abt '[]) a -> ReaderT Varmap Maybe ()
datumCodeEq DatumCode xss (abt '[]) a
c DatumCode xss (abt '[]) a
DatumCode xss (abt '[]) a
d
    datumCodeEq (Inl DatumStruct xs (abt '[]) a
c) (Inl DatumStruct xs (abt '[]) a
d) = DatumStruct xs (abt '[]) a
-> DatumStruct xs (abt '[]) a -> ReaderT Varmap Maybe ()
forall (xs :: [HakaruFun]) (a :: Hakaru).
DatumStruct xs (abt '[]) a
-> DatumStruct xs (abt '[]) a -> ReaderT Varmap Maybe ()
datumStructEq DatumStruct xs (abt '[]) a
c DatumStruct xs (abt '[]) a
DatumStruct xs (abt '[]) a
d
    datumCodeEq DatumCode xss (abt '[]) a
_       DatumCode xss (abt '[]) a
_       = Maybe () -> ReaderT Varmap Maybe ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Maybe ()
forall a. Maybe a
Nothing

    datumStructEq
        :: forall xs a
        .  DatumStruct xs (abt '[]) a
        -> DatumStruct xs (abt '[]) a
        -> ReaderT Varmap Maybe ()
    datumStructEq :: DatumStruct xs (abt '[]) a
-> DatumStruct xs (abt '[]) a -> ReaderT Varmap Maybe ()
datumStructEq (Et DatumFun x (abt '[]) a
c1 DatumStruct xs (abt '[]) a
c2) (Et DatumFun x (abt '[]) a
d1 DatumStruct xs (abt '[]) a
d2) = do
        DatumFun x (abt '[]) a
-> DatumFun x (abt '[]) a -> ReaderT Varmap Maybe ()
forall (x :: HakaruFun) (a :: Hakaru).
DatumFun x (abt '[]) a
-> DatumFun x (abt '[]) a -> ReaderT Varmap Maybe ()
datumFunEq DatumFun x (abt '[]) a
c1 DatumFun x (abt '[]) a
DatumFun x (abt '[]) a
d1
        DatumStruct xs (abt '[]) a
-> DatumStruct xs (abt '[]) a -> ReaderT Varmap Maybe ()
forall (xs :: [HakaruFun]) (a :: Hakaru).
DatumStruct xs (abt '[]) a
-> DatumStruct xs (abt '[]) a -> ReaderT Varmap Maybe ()
datumStructEq DatumStruct xs (abt '[]) a
c2 DatumStruct xs (abt '[]) a
DatumStruct xs (abt '[]) a
d2
    datumStructEq DatumStruct xs (abt '[]) a
Done       DatumStruct xs (abt '[]) a
Done       = () -> ReaderT Varmap Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    
    datumFunEq
        :: forall x a
        .  DatumFun x (abt '[]) a
        -> DatumFun x (abt '[]) a
        -> ReaderT Varmap Maybe ()
    datumFunEq :: DatumFun x (abt '[]) a
-> DatumFun x (abt '[]) a -> ReaderT Varmap Maybe ()
datumFunEq (Konst abt '[] b
e) (Konst abt '[] b
f) = View (Term abt) '[] b
-> View (Term abt) '[] b -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt '[] b -> View (Term abt) '[] b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] b
e) (abt '[] b -> View (Term abt) '[] b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] b
f) 
    datumFunEq (Ident abt '[] a
e) (Ident abt '[] a
f) = View (Term abt) '[] a
-> View (Term abt) '[] a -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt '[] a -> View (Term abt) '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] a
e) (abt '[] a -> View (Term abt) '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] a
f) 
    
    pairEq
        :: forall c b
        .  (abt '[] c, abt '[] b)
        -> (abt '[] c, abt '[] b)
        -> ReaderT Varmap Maybe ()
    pairEq :: (abt '[] c, abt '[] b)
-> (abt '[] c, abt '[] b) -> ReaderT Varmap Maybe ()
pairEq (abt '[] c
x1, abt '[] b
y1) (abt '[] c
x2, abt '[] b
y2) = do
        View (Term abt) '[] c
-> View (Term abt) '[] c -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt '[] c -> View (Term abt) '[] c
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] c
x1) (abt '[] c -> View (Term abt) '[] c
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] c
x2)
        View (Term abt) '[] b
-> View (Term abt) '[] b -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt '[] b -> View (Term abt) '[] b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] b
y1) (abt '[] b -> View (Term abt) '[] b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] b
y2)

    sBranch
        :: forall c b
        .  Branch c abt b
        -> Branch c abt b
        -> ReaderT Varmap Maybe ()
    sBranch :: Branch c abt b -> Branch c abt b -> ReaderT Varmap Maybe ()
sBranch (Branch Pattern xs c
p3 abt xs b
e3) (Branch Pattern xs c
p4 abt xs b
e4) = Pattern xs c -> Pattern xs c -> ReaderT Varmap Maybe ()
forall (a0 :: [Hakaru]) (b0 :: Hakaru) (a1 :: [Hakaru])
       (b1 :: Hakaru).
Pattern a0 b0 -> Pattern a1 b1 -> ReaderT Varmap Maybe ()
patternEq Pattern xs c
p3 Pattern xs c
p4 ReaderT Varmap Maybe ()
-> ReaderT Varmap Maybe () -> ReaderT Varmap Maybe ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> View (Term abt) xs b
-> View (Term abt) xs b -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt xs b -> View (Term abt) xs b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt xs b
e3) (abt xs b -> View (Term abt) xs b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt xs b
e4)

    patternEq 
        :: Pattern a0 b0
        -> Pattern a1 b1
        -> ReaderT Varmap Maybe ()
    patternEq :: Pattern a0 b0 -> Pattern a1 b1 -> ReaderT Varmap Maybe ()
patternEq Pattern a0 b0
PWild         Pattern a1 b1
PWild       = () -> ReaderT Varmap Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return () 
    patternEq Pattern a0 b0
PVar          Pattern a1 b1
PVar        = () -> ReaderT Varmap Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return () 
    patternEq (PDatum Text
_ PDatumCode (Code t) a0 (HData' t)
a) (PDatum Text
_ PDatumCode (Code t) a1 (HData' t)
b) = PDatumCode (Code t) a0 (HData' t)
-> PDatumCode (Code t) a1 (HData' t) -> ReaderT Varmap Maybe ()
forall (xss0 :: [[HakaruFun]]) (vs0 :: [Hakaru]) (a0 :: Hakaru)
       (xss1 :: [[HakaruFun]]) (vs1 :: [Hakaru]) (a1 :: Hakaru).
PDatumCode xss0 vs0 a0
-> PDatumCode xss1 vs1 a1 -> ReaderT Varmap Maybe ()
pdatumCodeEq PDatumCode (Code t) a0 (HData' t)
a PDatumCode (Code t) a1 (HData' t)
b 
    patternEq Pattern a0 b0
_             Pattern a1 b1
_           = ReaderT Varmap Maybe ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero 
      
    pdatumCodeEq
        :: PDatumCode xss0 vs0 a0
        -> PDatumCode xss1 vs1 a1
        -> ReaderT Varmap Maybe ()
    pdatumCodeEq :: PDatumCode xss0 vs0 a0
-> PDatumCode xss1 vs1 a1 -> ReaderT Varmap Maybe ()
pdatumCodeEq (PInr PDatumCode xss vs0 a0
c) (PInr PDatumCode xss vs1 a1
d) = PDatumCode xss vs0 a0
-> PDatumCode xss vs1 a1 -> ReaderT Varmap Maybe ()
forall (xss0 :: [[HakaruFun]]) (vs0 :: [Hakaru]) (a0 :: Hakaru)
       (xss1 :: [[HakaruFun]]) (vs1 :: [Hakaru]) (a1 :: Hakaru).
PDatumCode xss0 vs0 a0
-> PDatumCode xss1 vs1 a1 -> ReaderT Varmap Maybe ()
pdatumCodeEq PDatumCode xss vs0 a0
c PDatumCode xss vs1 a1
d
    pdatumCodeEq (PInl PDatumStruct xs vs0 a0
c) (PInl PDatumStruct xs vs1 a1
d) = PDatumStruct xs vs0 a0
-> PDatumStruct xs vs1 a1 -> ReaderT Varmap Maybe ()
forall (xs0 :: [HakaruFun]) (vs0 :: [Hakaru]) (a0 :: Hakaru)
       (xs1 :: [HakaruFun]) (vs1 :: [Hakaru]) (a1 :: Hakaru).
PDatumStruct xs0 vs0 a0
-> PDatumStruct xs1 vs1 a1 -> ReaderT Varmap Maybe ()
pdatumStructEq PDatumStruct xs vs0 a0
c PDatumStruct xs vs1 a1
d
    pdatumCodeEq PDatumCode xss0 vs0 a0
_         PDatumCode xss1 vs1 a1
_       = ReaderT Varmap Maybe ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero

    pdatumStructEq
        :: PDatumStruct xs0 vs0 a0
        -> PDatumStruct xs1 vs1 a1
        -> ReaderT Varmap Maybe ()
    pdatumStructEq :: PDatumStruct xs0 vs0 a0
-> PDatumStruct xs1 vs1 a1 -> ReaderT Varmap Maybe ()
pdatumStructEq (PEt PDatumFun x vars1 a0
c1 PDatumStruct xs vars2 a0
c2) (PEt PDatumFun x vars1 a1
d1 PDatumStruct xs vars2 a1
d2) = do
        PDatumFun x vars1 a0
-> PDatumFun x vars1 a1 -> ReaderT Varmap Maybe ()
forall (x0 :: HakaruFun) (vs0 :: [Hakaru]) (a0 :: Hakaru)
       (x1 :: HakaruFun) (vs1 :: [Hakaru]) (a1 :: Hakaru).
PDatumFun x0 vs0 a0
-> PDatumFun x1 vs1 a1 -> ReaderT Varmap Maybe ()
pdatumFunEq PDatumFun x vars1 a0
c1 PDatumFun x vars1 a1
d1
        PDatumStruct xs vars2 a0
-> PDatumStruct xs vars2 a1 -> ReaderT Varmap Maybe ()
forall (xs0 :: [HakaruFun]) (vs0 :: [Hakaru]) (a0 :: Hakaru)
       (xs1 :: [HakaruFun]) (vs1 :: [Hakaru]) (a1 :: Hakaru).
PDatumStruct xs0 vs0 a0
-> PDatumStruct xs1 vs1 a1 -> ReaderT Varmap Maybe ()
pdatumStructEq PDatumStruct xs vars2 a0
c2 PDatumStruct xs vars2 a1
d2
    pdatumStructEq PDatumStruct xs0 vs0 a0
PDone        PDatumStruct xs1 vs1 a1
PDone      = () -> ReaderT Varmap Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    pdatumStructEq PDatumStruct xs0 vs0 a0
_            PDatumStruct xs1 vs1 a1
_          = Maybe () -> ReaderT Varmap Maybe ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Maybe ()
forall a. Maybe a
Nothing

    pdatumFunEq
        :: PDatumFun x0 vs0 a0
        -> PDatumFun x1 vs1 a1
        -> ReaderT Varmap Maybe ()
    pdatumFunEq :: PDatumFun x0 vs0 a0
-> PDatumFun x1 vs1 a1 -> ReaderT Varmap Maybe ()
pdatumFunEq (PKonst Pattern vs0 b
e) (PKonst Pattern vs1 b
f) = Pattern vs0 b -> Pattern vs1 b -> ReaderT Varmap Maybe ()
forall (a0 :: [Hakaru]) (b0 :: Hakaru) (a1 :: [Hakaru])
       (b1 :: Hakaru).
Pattern a0 b0 -> Pattern a1 b1 -> ReaderT Varmap Maybe ()
patternEq Pattern vs0 b
e Pattern vs1 b
f
    pdatumFunEq (PIdent Pattern vs0 a0
e) (PIdent Pattern vs1 a1
f) = Pattern vs0 a0 -> Pattern vs1 a1 -> ReaderT Varmap Maybe ()
forall (a0 :: [Hakaru]) (b0 :: Hakaru) (a1 :: [Hakaru])
       (b1 :: Hakaru).
Pattern a0 b0 -> Pattern a1 b1 -> ReaderT Varmap Maybe ()
patternEq Pattern vs0 a0
e Pattern vs1 a1
f
    pdatumFunEq PDatumFun x0 vs0 a0
_          PDatumFun x1 vs1 a1
_          = Maybe () -> ReaderT Varmap Maybe ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Maybe ()
forall a. Maybe a
Nothing

    reducerEq
        :: forall xs b
        .  Reducer abt xs b
        -> Reducer abt xs b
        -> ReaderT Varmap Maybe ()
    reducerEq :: Reducer abt xs b -> Reducer abt xs b -> ReaderT Varmap Maybe ()
reducerEq (Red_Fanout Reducer abt xs a
r Reducer abt xs b
s) (Red_Fanout Reducer abt xs a
r' Reducer abt xs b
s')    = do
        Reducer abt xs a -> Reducer abt xs a -> ReaderT Varmap Maybe ()
forall (xs :: [Hakaru]) (b :: Hakaru).
Reducer abt xs b -> Reducer abt xs b -> ReaderT Varmap Maybe ()
reducerEq Reducer abt xs a
r Reducer abt xs a
Reducer abt xs a
r'
        Reducer abt xs b -> Reducer abt xs b -> ReaderT Varmap Maybe ()
forall (xs :: [Hakaru]) (b :: Hakaru).
Reducer abt xs b -> Reducer abt xs b -> ReaderT Varmap Maybe ()
reducerEq Reducer abt xs b
s Reducer abt xs b
Reducer abt xs b
s'
    reducerEq (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
        View (Term abt) xs 'HNat
-> View (Term abt) xs 'HNat -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt xs 'HNat -> View (Term abt) xs 'HNat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt xs 'HNat
s) (abt xs 'HNat -> View (Term abt) xs 'HNat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt xs 'HNat
s')
        View (Term abt) ('HNat : xs) 'HNat
-> View (Term abt) ('HNat : xs) 'HNat -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt ('HNat : xs) 'HNat -> View (Term abt) ('HNat : xs) 'HNat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt ('HNat : xs) 'HNat
i) (abt ('HNat : xs) 'HNat -> View (Term abt) ('HNat : xs) 'HNat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt ('HNat : xs) 'HNat
i')
        Reducer abt ('HNat : xs) a
-> Reducer abt ('HNat : xs) a -> ReaderT Varmap Maybe ()
forall (xs :: [Hakaru]) (b :: Hakaru).
Reducer abt xs b -> Reducer abt xs b -> ReaderT Varmap Maybe ()
reducerEq Reducer abt ('HNat : xs) a
r Reducer abt ('HNat : xs) a
Reducer abt ('HNat : xs) a
r'
    reducerEq (Red_Split abt ('HNat : xs) HBool
i Reducer abt xs a
r Reducer abt xs b
s) (Red_Split abt ('HNat : xs) HBool
i' Reducer abt xs a
r' Reducer abt xs b
s') = do
        View (Term abt) ('HNat : xs) HBool
-> View (Term abt) ('HNat : xs) HBool -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt ('HNat : xs) HBool -> View (Term abt) ('HNat : xs) HBool
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt ('HNat : xs) HBool
i) (abt ('HNat : xs) HBool -> View (Term abt) ('HNat : xs) HBool
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt ('HNat : xs) HBool
i')
        Reducer abt xs a -> Reducer abt xs a -> ReaderT Varmap Maybe ()
forall (xs :: [Hakaru]) (b :: Hakaru).
Reducer abt xs b -> Reducer abt xs b -> ReaderT Varmap Maybe ()
reducerEq Reducer abt xs a
r Reducer abt xs a
Reducer abt xs a
r'
        Reducer abt xs b -> Reducer abt xs b -> ReaderT Varmap Maybe ()
forall (xs :: [Hakaru]) (b :: Hakaru).
Reducer abt xs b -> Reducer abt xs b -> ReaderT Varmap Maybe ()
reducerEq Reducer abt xs b
s Reducer abt xs b
Reducer abt xs b
s'
    reducerEq Reducer abt xs b
Red_Nop Reducer abt xs b
Red_Nop                        = () -> ReaderT Varmap Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    reducerEq (Red_Add HSemiring b
_ abt ('HNat : xs) b
x) (Red_Add HSemiring b
_ abt ('HNat : xs) b
x')           = View (Term abt) ('HNat : xs) b
-> View (Term abt) ('HNat : xs) b -> ReaderT Varmap Maybe ()
forall (xs1 :: [Hakaru]) (xs2 :: [Hakaru]) (a :: Hakaru).
View (Term abt) xs1 a
-> View (Term abt) xs2 a -> ReaderT Varmap Maybe ()
go (abt ('HNat : xs) b -> View (Term abt) ('HNat : xs) b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt ('HNat : xs) b
x) (abt ('HNat : xs) b -> View (Term abt) ('HNat : xs) b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt ('HNat : xs) b
x')
    reducerEq Reducer abt xs b
_ Reducer abt xs b
_                                    = Maybe () -> ReaderT Varmap Maybe ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Maybe ()
forall a. Maybe a
Nothing