{-# LANGUAGE CPP
, DataKinds
, GADTs
, TypeOperators
, PolyKinds
, FlexibleContexts
, ScopedTypeVariables
, UndecidableInstances
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs -fno-warn-orphans -fno-warn-name-shadowing #-}
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 Unsafe.Coerce
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
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
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)
_))
| 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'')
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
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
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
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)
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
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
(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