{-# LANGUAGE CPP
, DataKinds
, PolyKinds
, GADTs
, StandaloneDeriving
, TypeOperators
, TypeFamilies
, FlexibleContexts
, UndecidableInstances
, Rank2Types
, DeriveDataTypeable
, LambdaCase
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Syntax.AST
(
SCon(..)
, SArgs(..)
, Term(..)
, Transform(..), TransformImpl(..)
, LCs, UnLCs
, LC_(..)
, NaryOp(..)
, PrimOp(..)
, ArrayOp(..)
, MeasureOp(..)
, Literal(..)
, foldMapPairs
, traversePairs
, module Language.Hakaru.Syntax.SArgs
, module Language.Hakaru.Syntax.Transform
) where
import Data.Sequence (Seq)
import qualified Data.Foldable as F
import qualified Data.List.NonEmpty as L
#if __GLASGOW_HASKELL__ < 710
import Data.Monoid (Monoid(..))
import Control.Applicative
import Data.Traversable
#endif
import Control.Arrow ((***))
import Data.Ratio (numerator, denominator)
import Data.Data ()
import Data.Number.Natural
import Language.Hakaru.Syntax.IClasses
import Language.Hakaru.Types.DataKind
import Language.Hakaru.Types.Sing
import Language.Hakaru.Types.HClasses
import Language.Hakaru.Types.Coercion
import Language.Hakaru.Syntax.Datum
import Language.Hakaru.Syntax.Reducer
import Language.Hakaru.Syntax.ABT (ABT(syn))
import Language.Hakaru.Syntax.SArgs
import Language.Hakaru.Syntax.Transform
data Literal :: Hakaru -> * where
LNat :: !Natural -> Literal 'HNat
LInt :: !Integer -> Literal 'HInt
LProb :: {-# UNPACK #-} !NonNegativeRational -> Literal 'HProb
LReal :: {-# UNPACK #-} !Rational -> Literal 'HReal
instance JmEq1 Literal where
jmEq1 :: Literal i -> Literal j -> Maybe (TypeEq i j)
jmEq1 (LNat Natural
x) (LNat Natural
y) = if Natural
x Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
y then TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl else Maybe (TypeEq i j)
forall a. Maybe a
Nothing
jmEq1 (LInt Integer
x) (LInt Integer
y) = if Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
y then TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl else Maybe (TypeEq i j)
forall a. Maybe a
Nothing
jmEq1 (LProb NonNegativeRational
x) (LProb NonNegativeRational
y) = if NonNegativeRational
x NonNegativeRational -> NonNegativeRational -> Bool
forall a. Eq a => a -> a -> Bool
== NonNegativeRational
y then TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl else Maybe (TypeEq i j)
forall a. Maybe a
Nothing
jmEq1 (LReal Rational
x) (LReal Rational
y) = if Rational
x Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
y then TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl else Maybe (TypeEq i j)
forall a. Maybe a
Nothing
jmEq1 Literal i
_ Literal j
_ = Maybe (TypeEq i j)
forall a. Maybe a
Nothing
instance Eq1 Literal where
eq1 :: Literal i -> Literal i -> Bool
eq1 (LNat Natural
x) (LNat Natural
y) = Natural
x Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
y
eq1 (LInt Integer
x) (LInt Integer
y) = Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
y
eq1 (LProb NonNegativeRational
x) (LProb NonNegativeRational
y) = NonNegativeRational
x NonNegativeRational -> NonNegativeRational -> Bool
forall a. Eq a => a -> a -> Bool
== NonNegativeRational
y
eq1 (LReal Rational
x) (LReal Rational
y) = Rational
x Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
y
instance Eq (Literal a) where
== :: Literal a -> Literal a -> Bool
(==) = Literal a -> Literal a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Show1 Literal where
showsPrec1 :: Int -> Literal i -> ShowS
showsPrec1 Int
p Literal i
t =
case Literal i
t of
LNat Natural
v -> Int -> String -> Natural -> ShowS
forall a. Show a => Int -> String -> a -> ShowS
showParen_0 Int
p String
"LNat" Natural
v
LInt Integer
v -> Int -> String -> Integer -> ShowS
forall a. Show a => Int -> String -> a -> ShowS
showParen_0 Int
p String
"LInt" Integer
v
LProb NonNegativeRational
v -> Int -> String -> NonNegativeRational -> ShowS
forall a. Show a => Int -> String -> a -> ShowS
showParen_0 Int
p String
"LProb" NonNegativeRational
v
LReal Rational
v -> Int -> String -> Rational -> ShowS
forall a. Show a => Int -> String -> a -> ShowS
showParen_0 Int
p String
"LReal" Rational
v
instance Show (Literal a) where
showsPrec :: Int -> Literal a -> ShowS
showsPrec = Int -> Literal a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: Literal a -> String
show = Literal a -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
instance Coerce Literal where
coerceTo :: Coercion a b -> Literal a -> Literal b
coerceTo Coercion a b
CNil Literal a
v = Literal a
Literal b
v
coerceTo (CCons PrimCoercion a b
c Coercion b b
cs) Literal a
v = Coercion b b -> Literal b -> Literal b
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f a -> f b
coerceTo Coercion b b
cs (PrimCoercion a b -> Literal a -> Literal b
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
PrimCoerce f =>
PrimCoercion a b -> f a -> f b
primCoerceTo PrimCoercion a b
c Literal a
v)
coerceFrom :: Coercion a b -> Literal b -> Literal a
coerceFrom Coercion a b
CNil Literal b
v = Literal a
Literal b
v
coerceFrom (CCons PrimCoercion a b
c Coercion b b
cs) Literal b
v = PrimCoercion a b -> Literal b -> Literal a
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
PrimCoerce f =>
PrimCoercion a b -> f b -> f a
primCoerceFrom PrimCoercion a b
c (Coercion b b -> Literal b -> Literal b
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f b -> f a
coerceFrom Coercion b b
cs Literal b
v)
instance PrimCoerce Literal where
primCoerceTo :: PrimCoercion a b -> Literal a -> Literal b
primCoerceTo PrimCoercion a b
c =
case PrimCoercion a b
c of
Signed HRing b
HRing_Int -> \(LNat Natural
n) -> Integer -> Literal 'HInt
LInt (Natural -> Integer
nat2int Natural
n)
Signed HRing b
HRing_Real -> \(LProb NonNegativeRational
p) -> Rational -> Literal 'HReal
LReal (NonNegativeRational -> Rational
prob2real NonNegativeRational
p)
Continuous HContinuous b
HContinuous_Prob -> \(LNat Natural
n) -> NonNegativeRational -> Literal 'HProb
LProb (Natural -> NonNegativeRational
nat2prob Natural
n)
Continuous HContinuous b
HContinuous_Real -> \(LInt Integer
i) -> Rational -> Literal 'HReal
LReal (Integer -> Rational
int2real Integer
i)
where
nat2int :: Natural -> Integer
nat2int :: Natural -> Integer
nat2int = Natural -> Integer
fromNatural
nat2prob :: Natural -> NonNegativeRational
nat2prob :: Natural -> NonNegativeRational
nat2prob = Rational -> NonNegativeRational
unsafeNonNegativeRational (Rational -> NonNegativeRational)
-> (Natural -> Rational) -> Natural -> NonNegativeRational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Rational
forall a. Real a => a -> Rational
toRational
prob2real :: NonNegativeRational -> Rational
prob2real :: NonNegativeRational -> Rational
prob2real = NonNegativeRational -> Rational
fromNonNegativeRational
int2real :: Integer -> Rational
int2real :: Integer -> Rational
int2real = Integer -> Rational
forall a b. (Integral a, Num b) => a -> b
fromIntegral
primCoerceFrom :: PrimCoercion a b -> Literal b -> Literal a
primCoerceFrom PrimCoercion a b
c =
case PrimCoercion a b
c of
Signed HRing b
HRing_Int -> \(LInt Integer
i) -> Natural -> Literal 'HNat
LNat (Integer -> Natural
int2nat Integer
i)
Signed HRing b
HRing_Real -> \(LReal Rational
r) -> NonNegativeRational -> Literal 'HProb
LProb (Rational -> NonNegativeRational
real2prob Rational
r)
Continuous HContinuous b
HContinuous_Prob -> \(LProb NonNegativeRational
p) -> Natural -> Literal 'HNat
LNat (NonNegativeRational -> Natural
prob2nat NonNegativeRational
p)
Continuous HContinuous b
HContinuous_Real -> \(LReal Rational
r) -> Integer -> Literal 'HInt
LInt (Rational -> Integer
real2int Rational
r)
where
int2nat :: Integer -> Natural
int2nat :: Integer -> Natural
int2nat Integer
x =
case Integer -> Maybe Natural
toNatural Integer
x of
Just Natural
y -> Natural
y
Maybe Natural
Nothing -> String -> Natural
forall a. HasCallStack => String -> a
error (String -> Natural) -> String -> Natural
forall a b. (a -> b) -> a -> b
$ String
"primCoerceFrom@Literal: negative HInt " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
x
prob2nat :: NonNegativeRational -> Natural
prob2nat :: NonNegativeRational -> Natural
prob2nat NonNegativeRational
x =
if NonNegativeRational -> Natural
forall a. Ratio a -> a
denominator NonNegativeRational
x Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
1
then NonNegativeRational -> Natural
forall a. Ratio a -> a
numerator NonNegativeRational
x
else String -> Natural
forall a. HasCallStack => String -> a
error (String -> Natural) -> String -> Natural
forall a b. (a -> b) -> a -> b
$ String
"primCoerceFrom@Literal: non-integral HProb " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NonNegativeRational -> String
forall a. Show a => a -> String
show NonNegativeRational
x
real2prob :: Rational -> NonNegativeRational
real2prob :: Rational -> NonNegativeRational
real2prob Rational
x =
case Rational -> Maybe NonNegativeRational
toNonNegativeRational Rational
x of
Just NonNegativeRational
y -> NonNegativeRational
y
Maybe NonNegativeRational
Nothing -> String -> NonNegativeRational
forall a. HasCallStack => String -> a
error (String -> NonNegativeRational) -> String -> NonNegativeRational
forall a b. (a -> b) -> a -> b
$ String
"primCoerceFrom@Literal: negative HReal " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rational -> String
forall a. Show a => a -> String
show Rational
x
real2int :: Rational -> Integer
real2int :: Rational -> Integer
real2int Rational
x =
if Rational -> Integer
forall a. Ratio a -> a
denominator Rational
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1
then Rational -> Integer
forall a. Ratio a -> a
numerator Rational
x
else String -> Integer
forall a. HasCallStack => String -> a
error (String -> Integer) -> String -> Integer
forall a b. (a -> b) -> a -> b
$ String
"primCoerceFrom@Literal: non-integral HReal " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rational -> String
forall a. Show a => a -> String
show Rational
x
data NaryOp :: Hakaru -> * where
And :: NaryOp HBool
Or :: NaryOp HBool
Xor :: NaryOp HBool
Iff :: NaryOp HBool
Min :: !(HOrd a) -> NaryOp a
Max :: !(HOrd a) -> NaryOp a
Sum :: !(HSemiring a) -> NaryOp a
Prod :: !(HSemiring a) -> NaryOp a
deriving instance Show (NaryOp a)
instance JmEq1 NaryOp where
jmEq1 :: NaryOp i -> NaryOp j -> Maybe (TypeEq i j)
jmEq1 NaryOp i
And NaryOp j
And = 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 NaryOp i
Or NaryOp j
Or = 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 NaryOp i
Xor NaryOp j
Xor = 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 NaryOp i
Iff NaryOp j
Iff = 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 (Min HOrd i
a) (Min HOrd j
b) = Sing i -> Sing j -> Maybe (TypeEq i j)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 (HOrd i -> Sing i
forall (a :: Hakaru). HOrd a -> Sing a
sing_HOrd HOrd i
a) (HOrd j -> Sing j
forall (a :: Hakaru). HOrd a -> Sing a
sing_HOrd HOrd j
b)
jmEq1 (Max HOrd i
a) (Max HOrd j
b) = Sing i -> Sing j -> Maybe (TypeEq i j)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 (HOrd i -> Sing i
forall (a :: Hakaru). HOrd a -> Sing a
sing_HOrd HOrd i
a) (HOrd j -> Sing j
forall (a :: Hakaru). HOrd a -> Sing a
sing_HOrd HOrd j
b)
jmEq1 (Sum HSemiring i
a) (Sum HSemiring j
b) = HSemiring i -> HSemiring j -> Maybe (TypeEq i j)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HSemiring i
a HSemiring j
b
jmEq1 (Prod HSemiring i
a) (Prod HSemiring j
b) = HSemiring i -> HSemiring j -> Maybe (TypeEq i j)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HSemiring i
a HSemiring j
b
jmEq1 NaryOp i
_ NaryOp j
_ = Maybe (TypeEq i j)
forall a. Maybe a
Nothing
instance Eq1 NaryOp where
eq1 :: NaryOp i -> NaryOp i -> Bool
eq1 NaryOp i
x NaryOp i
y = Bool -> (TypeEq i i -> Bool) -> Maybe (TypeEq i i) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> TypeEq i i -> Bool
forall a b. a -> b -> a
const Bool
True) (NaryOp i -> NaryOp i -> Maybe (TypeEq i i)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 NaryOp i
x NaryOp i
y)
instance Eq (NaryOp a) where
== :: NaryOp a -> NaryOp a -> Bool
(==) = NaryOp a -> NaryOp a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
type family LCs (xs :: [Hakaru]) :: [([Hakaru], Hakaru)] where
LCs '[] = '[]
LCs (x ': xs) = LC x ': LCs xs
type family UnLCs (xs :: [([Hakaru], Hakaru)]) :: [Hakaru] where
UnLCs '[] = '[]
UnLCs ( '( '[], x ) ': xs) = x ': UnLCs xs
data PrimOp :: [Hakaru] -> Hakaru -> * where
Not :: PrimOp '[ HBool ] HBool
Impl :: PrimOp '[ HBool, HBool ] HBool
Diff :: PrimOp '[ HBool, HBool ] HBool
Nand :: PrimOp '[ HBool, HBool ] HBool
Nor :: PrimOp '[ HBool, HBool ] HBool
Pi :: PrimOp '[] 'HProb
Sin :: PrimOp '[ 'HReal ] 'HReal
Cos :: PrimOp '[ 'HReal ] 'HReal
Tan :: PrimOp '[ 'HReal ] 'HReal
Asin :: PrimOp '[ 'HReal ] 'HReal
Acos :: PrimOp '[ 'HReal ] 'HReal
Atan :: PrimOp '[ 'HReal ] 'HReal
Sinh :: PrimOp '[ 'HReal ] 'HReal
Cosh :: PrimOp '[ 'HReal ] 'HReal
Tanh :: PrimOp '[ 'HReal ] 'HReal
Asinh :: PrimOp '[ 'HReal ] 'HReal
Acosh :: PrimOp '[ 'HReal ] 'HReal
Atanh :: PrimOp '[ 'HReal ] 'HReal
RealPow :: PrimOp '[ 'HProb, 'HReal ] 'HProb
Choose :: PrimOp '[ 'HNat, 'HNat ] 'HNat
Exp :: PrimOp '[ 'HReal ] 'HProb
Log :: PrimOp '[ 'HProb ] 'HReal
Infinity :: HIntegrable a -> PrimOp '[] a
GammaFunc :: PrimOp '[ 'HReal ] 'HProb
BetaFunc :: PrimOp '[ 'HProb, 'HProb ] 'HProb
Equal :: !(HEq a) -> PrimOp '[ a, a ] HBool
Less :: !(HOrd a) -> PrimOp '[ a, a ] HBool
NatPow :: !(HSemiring a) -> PrimOp '[ a, 'HNat ] a
Negate :: !(HRing a) -> PrimOp '[ a ] a
Abs :: !(HRing a) -> PrimOp '[ a ] (NonNegative a)
Signum :: !(HRing a) -> PrimOp '[ a ] a
Floor :: PrimOp '[ 'HProb ] 'HNat
Recip :: !(HFractional a) -> PrimOp '[ a ] a
NatRoot :: !(HRadical a) -> PrimOp '[ a, 'HNat ] a
Erf :: !(HContinuous a) -> PrimOp '[ a ] a
deriving instance Show (PrimOp args a)
instance JmEq2 PrimOp where
jmEq2 :: PrimOp i1 j1 -> PrimOp i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 PrimOp i1 j1
Not PrimOp i2 j2
Not = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
Impl PrimOp i2 j2
Impl = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
Diff PrimOp i2 j2
Diff = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
Nand PrimOp i2 j2
Nand = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
Nor PrimOp i2 j2
Nor = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
Pi PrimOp i2 j2
Pi = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
Sin PrimOp i2 j2
Sin = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
Cos PrimOp i2 j2
Cos = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
Tan PrimOp i2 j2
Tan = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
Asin PrimOp i2 j2
Asin = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
Acos PrimOp i2 j2
Acos = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
Atan PrimOp i2 j2
Atan = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
Sinh PrimOp i2 j2
Sinh = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
Cosh PrimOp i2 j2
Cosh = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
Tanh PrimOp i2 j2
Tanh = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
Asinh PrimOp i2 j2
Asinh = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
Acosh PrimOp i2 j2
Acosh = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
Atanh PrimOp i2 j2
Atanh = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
RealPow PrimOp i2 j2
RealPow = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
Exp PrimOp i2 j2
Exp = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
Log PrimOp i2 j2
Log = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
GammaFunc PrimOp i2 j2
GammaFunc = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
BetaFunc PrimOp i2 j2
BetaFunc = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 (Equal HEq a
a) (Equal HEq 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 (HEq a -> Sing a
forall (a :: Hakaru). HEq a -> Sing a
sing_HEq HEq a
a) (HEq a -> Sing a
forall (a :: Hakaru). HEq a -> Sing a
sing_HEq HEq a
b) Maybe (TypeEq a a)
-> (TypeEq a a -> 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 a a
Refl ->
(TypeEq '[a, a] '[a, a],
TypeEq
('HData ('TyCon "Bool") '[ '[], '[]])
('HData ('TyCon "Bool") '[ '[], '[]]))
-> Maybe
(TypeEq '[a, a] '[a, a],
TypeEq
('HData ('TyCon "Bool") '[ '[], '[]])
('HData ('TyCon "Bool") '[ '[], '[]]))
forall a. a -> Maybe a
Just (TypeEq '[a, a] '[a, a]
forall k (a :: k). TypeEq a a
Refl, TypeEq
('HData ('TyCon "Bool") '[ '[], '[]])
('HData ('TyCon "Bool") '[ '[], '[]])
forall k (a :: k). TypeEq a a
Refl)
jmEq2 (Less HOrd a
a) (Less HOrd 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 (HOrd a -> Sing a
forall (a :: Hakaru). HOrd a -> Sing a
sing_HOrd HOrd a
a) (HOrd a -> Sing a
forall (a :: Hakaru). HOrd a -> Sing a
sing_HOrd HOrd a
b) Maybe (TypeEq a a)
-> (TypeEq a a -> 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 a a
Refl ->
(TypeEq '[a, a] '[a, a],
TypeEq
('HData ('TyCon "Bool") '[ '[], '[]])
('HData ('TyCon "Bool") '[ '[], '[]]))
-> Maybe
(TypeEq '[a, a] '[a, a],
TypeEq
('HData ('TyCon "Bool") '[ '[], '[]])
('HData ('TyCon "Bool") '[ '[], '[]]))
forall a. a -> Maybe a
Just (TypeEq '[a, a] '[a, a]
forall k (a :: k). TypeEq a a
Refl, TypeEq
('HData ('TyCon "Bool") '[ '[], '[]])
('HData ('TyCon "Bool") '[ '[], '[]])
forall k (a :: k). TypeEq a a
Refl)
jmEq2 (Infinity HIntegrable j1
a) (Infinity HIntegrable j2
b) =
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 (HIntegrable j1 -> Sing j1
forall (a :: Hakaru). HIntegrable a -> Sing a
sing_HIntegrable HIntegrable j1
a) (HIntegrable j2 -> Sing j2
forall (a :: Hakaru). HIntegrable a -> Sing a
sing_HIntegrable HIntegrable j2
b) 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)
jmEq2 (NatPow HSemiring j1
a) (NatPow HSemiring j2
b) = HSemiring j1 -> HSemiring j2 -> Maybe (TypeEq j1 j2)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HSemiring j1
a HSemiring j2
b 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 '[j1, 'HNat] '[j1, 'HNat], TypeEq j1 j1)
-> Maybe (TypeEq '[j1, 'HNat] '[j1, 'HNat], TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq '[j1, 'HNat] '[j1, 'HNat]
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 (Negate HRing j1
a) (Negate HRing j2
b) = HRing j1 -> HRing j2 -> Maybe (TypeEq j1 j2)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HRing j1
a HRing j2
b 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 '[j1] '[j1], TypeEq j1 j1)
-> Maybe (TypeEq '[j1] '[j1], TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq '[j1] '[j1]
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 (Abs HRing a
a) (Abs HRing a
b) = HRing a -> HRing a -> Maybe (TypeEq a a)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HRing a
a HRing a
b Maybe (TypeEq a a)
-> (TypeEq a a -> 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 a a
Refl -> (TypeEq '[a] '[a], TypeEq j1 j1)
-> Maybe (TypeEq '[a] '[a], TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq '[a] '[a]
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 (Signum HRing j1
a) (Signum HRing j2
b) = HRing j1 -> HRing j2 -> Maybe (TypeEq j1 j2)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HRing j1
a HRing j2
b 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 '[j1] '[j1], TypeEq j1 j1)
-> Maybe (TypeEq '[j1] '[j1], TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq '[j1] '[j1]
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 (Recip HFractional j1
a) (Recip HFractional j2
b) = HFractional j1 -> HFractional j2 -> Maybe (TypeEq j1 j2)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HFractional j1
a HFractional j2
b 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 '[j1] '[j1], TypeEq j1 j1)
-> Maybe (TypeEq '[j1] '[j1], TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq '[j1] '[j1]
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 (NatRoot HRadical j1
a) (NatRoot HRadical j2
b) = HRadical j1 -> HRadical j2 -> Maybe (TypeEq j1 j2)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HRadical j1
a HRadical j2
b 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 '[j1, 'HNat] '[j1, 'HNat], TypeEq j1 j1)
-> Maybe (TypeEq '[j1, 'HNat] '[j1, 'HNat], TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq '[j1, 'HNat] '[j1, 'HNat]
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 (Erf HContinuous j1
a) (Erf HContinuous j2
b) = HContinuous j1 -> HContinuous j2 -> Maybe (TypeEq j1 j2)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HContinuous j1
a HContinuous j2
b 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 '[j1] '[j1], TypeEq j1 j1)
-> Maybe (TypeEq '[j1] '[j1], TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq '[j1] '[j1]
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 PrimOp i1 j1
_ PrimOp i2 j2
_ = Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall a. Maybe a
Nothing
instance Eq2 PrimOp where
eq2 :: PrimOp i j -> PrimOp i j -> Bool
eq2 PrimOp i j
x PrimOp i j
y = Bool
-> ((TypeEq i i, TypeEq j j) -> Bool)
-> Maybe (TypeEq i i, TypeEq j j)
-> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> (TypeEq i i, TypeEq j j) -> Bool
forall a b. a -> b -> a
const Bool
True) (PrimOp i j -> PrimOp 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 PrimOp i j
x PrimOp i j
y)
instance Eq1 (PrimOp args) where
eq1 :: PrimOp args i -> PrimOp args i -> Bool
eq1 = PrimOp args i -> PrimOp args i -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2
instance Eq (PrimOp args a) where
== :: PrimOp args a -> PrimOp args a -> Bool
(==) = PrimOp args a -> PrimOp args a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
data ArrayOp :: [Hakaru] -> Hakaru -> * where
Index :: !(Sing a) -> ArrayOp '[ 'HArray a, 'HNat ] a
Size :: !(Sing a) -> ArrayOp '[ 'HArray a ] 'HNat
Reduce :: !(Sing a) -> ArrayOp '[ a ':-> a ':-> a, a, 'HArray a ] a
deriving instance Show (ArrayOp args a)
instance JmEq2 ArrayOp where
jmEq2 :: ArrayOp i1 j1
-> ArrayOp i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 (Index Sing j1
a) (Index Sing j2
b) = 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
a Sing j2
b 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 '[ 'HArray j1, 'HNat] '[ 'HArray j1, 'HNat], TypeEq j1 j1)
-> Maybe
(TypeEq '[ 'HArray j1, 'HNat] '[ 'HArray j1, 'HNat], TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq '[ 'HArray j1, 'HNat] '[ 'HArray j1, 'HNat]
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 (Size Sing a
a) (Size Sing 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 Sing a
a Sing a
b Maybe (TypeEq a a)
-> (TypeEq a a -> 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 a a
Refl -> (TypeEq '[ 'HArray a] '[ 'HArray a], TypeEq 'HNat 'HNat)
-> Maybe (TypeEq '[ 'HArray a] '[ 'HArray a], TypeEq 'HNat 'HNat)
forall a. a -> Maybe a
Just (TypeEq '[ 'HArray a] '[ 'HArray a]
forall k (a :: k). TypeEq a a
Refl, TypeEq 'HNat 'HNat
forall k (a :: k). TypeEq a a
Refl)
jmEq2 (Reduce Sing j1
a) (Reduce Sing j2
b) = 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
a Sing j2
b 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
'[ j1 ':-> (j1 ':-> j1), j1, 'HArray j1]
'[ j1 ':-> (j1 ':-> j1), j1, 'HArray j1],
TypeEq j1 j1)
-> Maybe
(TypeEq
'[ j1 ':-> (j1 ':-> j1), j1, 'HArray j1]
'[ j1 ':-> (j1 ':-> j1), j1, 'HArray j1],
TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq
'[ j1 ':-> (j1 ':-> j1), j1, 'HArray j1]
'[ j1 ':-> (j1 ':-> j1), j1, 'HArray j1]
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 ArrayOp i1 j1
_ ArrayOp i2 j2
_ = Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall a. Maybe a
Nothing
instance Eq2 ArrayOp where
eq2 :: ArrayOp i j -> ArrayOp i j -> Bool
eq2 ArrayOp i j
x ArrayOp i j
y = Bool
-> ((TypeEq i i, TypeEq j j) -> Bool)
-> Maybe (TypeEq i i, TypeEq j j)
-> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> (TypeEq i i, TypeEq j j) -> Bool
forall a b. a -> b -> a
const Bool
True) (ArrayOp i j -> ArrayOp 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 ArrayOp i j
x ArrayOp i j
y)
instance Eq1 (ArrayOp args) where
eq1 :: ArrayOp args i -> ArrayOp args i -> Bool
eq1 = ArrayOp args i -> ArrayOp args i -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2
instance Eq (ArrayOp args a) where
== :: ArrayOp args a -> ArrayOp args a -> Bool
(==) = ArrayOp args a -> ArrayOp args a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
data MeasureOp :: [Hakaru] -> Hakaru -> * where
Lebesgue :: MeasureOp '[ 'HReal, 'HReal ] 'HReal
Counting :: MeasureOp '[] 'HInt
Categorical :: MeasureOp '[ 'HArray 'HProb ] 'HNat
Uniform :: MeasureOp '[ 'HReal, 'HReal ] 'HReal
Normal :: MeasureOp '[ 'HReal, 'HProb ] 'HReal
Poisson :: MeasureOp '[ 'HProb ] 'HNat
Gamma :: MeasureOp '[ 'HProb, 'HProb ] 'HProb
Beta :: MeasureOp '[ 'HProb, 'HProb ] 'HProb
deriving instance Show (MeasureOp typs a)
instance JmEq2 MeasureOp where
jmEq2 :: MeasureOp i1 j1
-> MeasureOp i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 MeasureOp i1 j1
Lebesgue MeasureOp i2 j2
Lebesgue = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 MeasureOp i1 j1
Counting MeasureOp i2 j2
Counting = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 MeasureOp i1 j1
Categorical MeasureOp i2 j2
Categorical = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 MeasureOp i1 j1
Uniform MeasureOp i2 j2
Uniform = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 MeasureOp i1 j1
Normal MeasureOp i2 j2
Normal = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 MeasureOp i1 j1
Poisson MeasureOp i2 j2
Poisson = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 MeasureOp i1 j1
Gamma MeasureOp i2 j2
Gamma = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 MeasureOp i1 j1
Beta MeasureOp i2 j2
Beta = (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
jmEq2 MeasureOp i1 j1
_ MeasureOp i2 j2
_ = Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall a. Maybe a
Nothing
instance Eq2 MeasureOp where
eq2 :: MeasureOp i j -> MeasureOp i j -> Bool
eq2 MeasureOp i j
x MeasureOp i j
y = Bool
-> ((TypeEq i i, TypeEq j j) -> Bool)
-> Maybe (TypeEq i i, TypeEq j j)
-> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> (TypeEq i i, TypeEq j j) -> Bool
forall a b. a -> b -> a
const Bool
True) (MeasureOp i j -> MeasureOp 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 MeasureOp i j
x MeasureOp i j
y)
instance Eq1 (MeasureOp typs) where
eq1 :: MeasureOp typs i -> MeasureOp typs i -> Bool
eq1 = MeasureOp typs i -> MeasureOp typs i -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2
instance Eq (MeasureOp typs a) where
== :: MeasureOp typs a -> MeasureOp typs a -> Bool
(==) = MeasureOp typs a -> MeasureOp typs a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
infix 4 :$
data SCon :: [([Hakaru], Hakaru)] -> Hakaru -> * where
Lam_ :: SCon '[ '( '[ a ], b ) ] (a ':-> b)
App_ :: SCon '[ LC (a ':-> b ), LC a ] b
Let_ :: SCon '[ LC a, '( '[ a ], b ) ] b
CoerceTo_ :: !(Coercion a b) -> SCon '[ LC a ] b
UnsafeFrom_ :: !(Coercion a b) -> SCon '[ LC b ] a
PrimOp_
:: (typs ~ UnLCs args, args ~ LCs typs)
=> !(PrimOp typs a) -> SCon args a
ArrayOp_
:: (typs ~ UnLCs args, args ~ LCs typs)
=> !(ArrayOp typs a) -> SCon args a
MeasureOp_
:: (typs ~ UnLCs args, args ~ LCs typs)
=> !(MeasureOp typs a) -> SCon args ('HMeasure a)
Dirac :: SCon '[ LC a ] ('HMeasure a)
MBind :: SCon
'[ LC ('HMeasure a)
, '( '[ a ], 'HMeasure b)
] ('HMeasure b)
Plate :: SCon
'[ LC 'HNat
, '( '[ 'HNat ], 'HMeasure a)
] ('HMeasure ('HArray a))
Chain :: SCon
'[ LC 'HNat, LC s
, '( '[ s ], 'HMeasure (HPair a s))
] ('HMeasure (HPair ('HArray a) s))
Integrate
:: SCon '[ LC 'HReal, LC 'HReal, '( '[ 'HReal ], 'HProb) ] 'HProb
Summate
:: HDiscrete a
-> HSemiring b
-> SCon '[ LC a, LC a, '( '[ a ], b) ] b
Product
:: HDiscrete a
-> HSemiring b
-> SCon '[ LC a, LC a, '( '[ a ], b) ] b
Transform_ :: !(Transform as x)
-> SCon as x
deriving instance Eq (SCon args a)
deriving instance Show (SCon args a)
data Term :: ([Hakaru] -> Hakaru -> *) -> Hakaru -> * where
(:$) :: !(SCon args a) -> !(SArgs abt args) -> Term abt a
NaryOp_ :: !(NaryOp a) -> !(Seq (abt '[] a)) -> Term abt a
Literal_ :: !(Literal a) -> Term abt a
Empty_ :: !(Sing ('HArray a)) -> Term abt ('HArray a)
Array_
:: !(abt '[] 'HNat)
-> !(abt '[ 'HNat ] a)
-> Term abt ('HArray a)
ArrayLiteral_
:: [abt '[] a]
-> Term abt ('HArray a)
Bucket
:: !(abt '[] 'HNat)
-> !(abt '[] 'HNat)
-> Reducer abt '[] a
-> Term abt a
Datum_ :: !(Datum (abt '[]) (HData' t)) -> Term abt (HData' t)
Case_ :: !(abt '[] a) -> [Branch a abt b] -> Term abt b
Superpose_
:: L.NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> Term abt ('HMeasure a)
Reject_ :: !(Sing ('HMeasure a)) -> Term abt ('HMeasure a)
newtype LC_ (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru) =
LC_ { LC_ abt a -> abt '[] a
unLC_ :: abt '[] a }
instance Show2 abt => Show1 (LC_ abt) where
showsPrec1 :: Int -> LC_ abt i -> ShowS
showsPrec1 Int
p = Int -> abt '[] i -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> a i j -> ShowS
showsPrec2 Int
p (abt '[] i -> ShowS)
-> (LC_ abt i -> abt '[] i) -> LC_ abt i -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LC_ abt i -> abt '[] i
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
LC_ abt a -> abt '[] a
unLC_
show1 :: LC_ abt i -> String
show1 = abt '[] i -> String
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
a i j -> String
show2 (abt '[] i -> String)
-> (LC_ abt i -> abt '[] i) -> LC_ abt i -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LC_ abt i -> abt '[] i
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
LC_ abt a -> abt '[] a
unLC_
instance ABT Term abt => Coerce (LC_ abt) where
coerceTo :: Coercion a b -> LC_ abt a -> LC_ abt b
coerceTo Coercion a b
CNil LC_ abt a
e = LC_ abt a
LC_ abt b
e
coerceTo Coercion a b
c (LC_ abt '[] a
e) = abt '[] b -> LC_ abt b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> LC_ abt a
LC_ (Term abt b -> abt '[] b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Coercion a b -> SCon '[LC a] b
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> SCon '[LC a] b
CoerceTo_ Coercion a b
c SCon '[LC a] b -> SArgs abt '[LC a] -> Term abt b
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
(abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt '[] a
e abt '[] a -> SArgs abt '[] -> SArgs abt '[LC a]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs abt '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End))
coerceFrom :: Coercion a b -> LC_ abt b -> LC_ abt a
coerceFrom Coercion a b
CNil LC_ abt b
e = LC_ abt a
LC_ abt b
e
coerceFrom Coercion a b
c (LC_ abt '[] b
e) = abt '[] a -> LC_ abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> LC_ abt a
LC_ (Term abt a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Coercion a b -> SCon '[LC b] a
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> SCon '[LC b] a
UnsafeFrom_ Coercion a b
c SCon '[LC b] a -> SArgs abt '[LC b] -> Term abt a
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
(abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt '[] b
e abt '[] b -> SArgs abt '[] -> SArgs abt '[LC b]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs abt '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End))
instance ABT Term abt => Coerce (Term abt) where
coerceTo :: Coercion a b -> Term abt a -> Term abt b
coerceTo Coercion a b
CNil Term abt a
e = Term abt a
Term abt b
e
coerceTo Coercion a b
c Term abt a
e = Coercion a b -> SCon '[LC a] b
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> SCon '[LC a] b
CoerceTo_ Coercion a b
c SCon '[LC a] b -> SArgs abt '[LC a] -> Term abt b
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
(abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ Term abt a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn Term abt a
e abt '[] a -> SArgs abt '[] -> SArgs abt '[LC a]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs abt '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End
coerceFrom :: Coercion a b -> Term abt b -> Term abt a
coerceFrom Coercion a b
CNil Term abt b
e = Term abt a
Term abt b
e
coerceFrom Coercion a b
c Term abt b
e = Coercion a b -> SCon '[LC b] a
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> SCon '[LC b] a
UnsafeFrom_ Coercion a b
c SCon '[LC b] a -> SArgs abt '[LC b] -> Term abt a
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
(abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ Term abt b -> abt '[] b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn Term abt b
e abt '[] b -> SArgs abt '[] -> SArgs abt '[LC b]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs abt '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End
instance Show2 abt => Show1 (Term abt) where
showsPrec1 :: Int -> Term abt i -> ShowS
showsPrec1 Int
p Term abt i
t =
case Term abt i
t of
SCon args i
o :$ SArgs abt args
es ->
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
4)
( Int -> SCon args i -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) SCon args i
o
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" :$ "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SArgs abt args -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1 (Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) SArgs abt args
es
)
NaryOp_ NaryOp i
o Seq (abt '[] i)
es ->
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
( String -> ShowS
showString String
"NaryOp_ "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> NaryOp i -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 NaryOp i
o
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> ShowS -> ShowS
showParen Bool
True
( String -> ShowS
showString String
"Seq.fromList "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [abt '[] i] -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
[a i j] -> ShowS
showList2 (Seq (abt '[] i) -> [abt '[] i]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (abt '[] i)
es)
)
)
Literal_ Literal i
v -> Int -> String -> Literal i -> ShowS
forall a. Show a => Int -> String -> a -> ShowS
showParen_0 Int
p String
"Literal_" Literal i
v
Empty_ Sing ('HArray a)
_ -> String -> ShowS
showString String
"Empty_"
Array_ abt '[] 'HNat
e1 abt '[ 'HNat] a
e2 -> Int -> String -> abt '[] 'HNat -> abt '[ 'HNat] a -> ShowS
forall k4 k5 k6 k7 (a :: k4 -> k5 -> *) (b :: k6 -> k7 -> *)
(i1 :: k4) (j1 :: k5) (i2 :: k6) (j2 :: k7).
(Show2 a, Show2 b) =>
Int -> String -> a i1 j1 -> b i2 j2 -> ShowS
showParen_22 Int
p String
"Array_" abt '[] 'HNat
e1 abt '[ 'HNat] a
e2
ArrayLiteral_ [abt '[] a]
es -> Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (String -> ShowS
showString String
"ArrayLiteral_" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [abt '[] a] -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
[a i j] -> ShowS
showList2 [abt '[] a]
es)
Datum_ Datum (abt '[]) (HData' t)
d -> Int -> String -> Datum (LC_ abt) (HData' t) -> ShowS
forall k (a :: k -> *) (i :: k).
Show1 a =>
Int -> String -> a i -> ShowS
showParen_1 Int
p String
"Datum_" ((forall (i :: Hakaru). abt '[] i -> LC_ abt i)
-> Datum (abt '[]) (HData' t) -> Datum (LC_ abt) (HData' t)
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *)
(b :: k1 -> *) (j :: k2).
Functor11 f =>
(forall (i :: k1). a i -> b i) -> f a j -> f b j
fmap11 forall (i :: Hakaru). abt '[] i -> LC_ abt i
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> LC_ abt a
LC_ Datum (abt '[]) (HData' t)
d)
Case_ abt '[] a
e [Branch a abt i]
bs ->
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
( String -> ShowS
showString String
"Case_ "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> abt '[] a -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> a i j -> ShowS
showsPrec2 Int
11 abt '[] a
e
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Branch a abt i] -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => [a i] -> ShowS
showList1 [Branch a abt i]
bs
)
Bucket abt '[] 'HNat
_ abt '[] 'HNat
_ Reducer abt '[] i
_ -> String -> ShowS
showString String
"Bucket ..."
Superpose_ NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
pes ->
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
( String -> ShowS
showString String
"Superpose_ "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((abt '[] 'HProb, abt '[] ('HMeasure a)) -> ShowS)
-> [(abt '[] 'HProb, abt '[] ('HMeasure a))] -> ShowS
forall a. (a -> ShowS) -> [a] -> ShowS
showListWith
(\(abt '[] 'HProb
e1,abt '[] ('HMeasure a)
e2) -> [ShowS] -> ShowS
showTuple [abt '[] 'HProb -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
a i j -> ShowS
shows2 abt '[] 'HProb
e1, abt '[] ('HMeasure a) -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
a i j -> ShowS
shows2 abt '[] ('HMeasure a)
e2])
(NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> [(abt '[] 'HProb, abt '[] ('HMeasure a))]
forall a. NonEmpty a -> [a]
L.toList NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
pes)
)
Reject_ Sing ('HMeasure a)
_ -> String -> ShowS
showString String
"Reject_"
instance Show2 abt => Show (Term abt a) where
showsPrec :: Int -> Term abt a -> ShowS
showsPrec = Int -> Term abt a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: Term abt a -> String
show = Term abt a -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
instance Functor21 Term where
fmap21 :: (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i)
-> Term a j -> Term b j
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (SCon args j
o :$ SArgs a args
es) = SCon args j
o SCon args j -> SArgs b args -> Term b j
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
(abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i)
-> SArgs a args -> SArgs b args
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *)
(a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
Functor21 f =>
(forall (h :: k1) (i :: k2). a h i -> b h i) -> f a j -> f b j
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f SArgs a args
es
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (NaryOp_ NaryOp j
o Seq (a '[] j)
es) = NaryOp j -> Seq (b '[] j) -> Term b j
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
NaryOp a -> Seq (abt '[] a) -> Term abt a
NaryOp_ NaryOp j
o ((a '[] j -> b '[] j) -> Seq (a '[] j) -> Seq (b '[] j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a '[] j -> b '[] j
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f Seq (a '[] j)
es)
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
_ (Literal_ Literal j
v) = Literal j -> Term b j
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Term abt a
Literal_ Literal j
v
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
_ (Empty_ Sing ('HArray a)
t) = Sing ('HArray a) -> Term b ('HArray a)
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Sing ('HArray a) -> Term abt ('HArray a)
Empty_ Sing ('HArray a)
t
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (Array_ a '[] 'HNat
e1 a '[ 'HNat] a
e2) = b '[] 'HNat -> b '[ 'HNat] a -> Term b ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] 'HNat -> abt '[ 'HNat] a -> Term abt ('HArray a)
Array_ (a '[] 'HNat -> b '[] 'HNat
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[] 'HNat
e1) (a '[ 'HNat] a -> b '[ 'HNat] a
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[ 'HNat] a
e2)
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (ArrayLiteral_ [a '[] a]
es) = [b '[] a] -> Term b ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
[abt '[] a] -> Term abt ('HArray a)
ArrayLiteral_ ((a '[] a -> b '[] a) -> [a '[] a] -> [b '[] a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a '[] a -> b '[] a
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f [a '[] a]
es)
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (Datum_ Datum (a '[]) (HData' t)
d) = Datum (b '[]) (HData' t) -> Term b (HData' t)
forall (abt :: [Hakaru] -> Hakaru -> *) (t :: HakaruCon).
Datum (abt '[]) (HData' t) -> Term abt (HData' t)
Datum_ ((forall (i :: Hakaru). a '[] i -> b '[] i)
-> Datum (a '[]) (HData' t) -> Datum (b '[]) (HData' t)
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *)
(b :: k1 -> *) (j :: k2).
Functor11 f =>
(forall (i :: k1). a i -> b i) -> f a j -> f b j
fmap11 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
forall (i :: Hakaru). a '[] i -> b '[] i
f Datum (a '[]) (HData' t)
d)
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (Case_ a '[] a
e [Branch a a j]
bs) = b '[] a -> [Branch a b j] -> Term b j
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
abt '[] a -> [Branch a abt b] -> Term abt b
Case_ (a '[] a -> b '[] a
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[] a
e) ((Branch a a j -> Branch a b j) -> [Branch a a j] -> [Branch a b j]
forall a b. (a -> b) -> [a] -> [b]
map ((forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i)
-> Branch a a j -> Branch a b j
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *)
(a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
Functor21 f =>
(forall (h :: k1) (i :: k2). a h i -> b h i) -> f a j -> f b j
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f) [Branch a a j]
bs)
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (Bucket a '[] 'HNat
b a '[] 'HNat
e Reducer a '[] j
r) = b '[] 'HNat -> b '[] 'HNat -> Reducer b '[] j -> Term b j
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] 'HNat -> abt '[] 'HNat -> Reducer abt '[] a -> Term abt a
Bucket (a '[] 'HNat -> b '[] 'HNat
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[] 'HNat
b) (a '[] 'HNat -> b '[] 'HNat
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[] 'HNat
e) ((forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i)
-> Reducer a '[] j -> Reducer b '[] j
forall k1 k2 k3 k4 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *)
(a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3) (l :: k4).
Functor22 f =>
(forall (h :: k1) (i :: k2). a h i -> b h i) -> f a j l -> f b j l
fmap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f Reducer a '[] j
r)
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (Superpose_ NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
pes) = NonEmpty (b '[] 'HProb, b '[] ('HMeasure a))
-> Term b ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> Term abt ('HMeasure a)
Superpose_ (((a '[] 'HProb, a '[] ('HMeasure a))
-> (b '[] 'HProb, b '[] ('HMeasure a)))
-> NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
-> NonEmpty (b '[] 'HProb, b '[] ('HMeasure a))
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
L.map (a '[] 'HProb -> b '[] 'HProb
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (a '[] 'HProb -> b '[] 'HProb)
-> (a '[] ('HMeasure a) -> b '[] ('HMeasure a))
-> (a '[] 'HProb, a '[] ('HMeasure a))
-> (b '[] 'HProb, b '[] ('HMeasure a))
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** a '[] ('HMeasure a) -> b '[] ('HMeasure a)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f) NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
pes)
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
_ (Reject_ Sing ('HMeasure a)
t) = Sing ('HMeasure a) -> Term b ('HMeasure a)
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Sing ('HMeasure a) -> Term abt ('HMeasure a)
Reject_ Sing ('HMeasure a)
t
instance Foldable21 Term where
foldMap21 :: (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m) -> Term a j -> m
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (SCon args j
_ :$ SArgs a args
es) = (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m)
-> SArgs a args -> m
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *) m
(a :: k1 -> k2 -> *) (j :: k3).
(Foldable21 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j -> m
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f SArgs a args
es
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (NaryOp_ NaryOp j
_ Seq (a '[] j)
es) = (a '[] j -> m) -> Seq (a '[] j) -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
F.foldMap a '[] j -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f Seq (a '[] j)
es
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
_ (Literal_ Literal j
_) = m
forall a. Monoid a => a
mempty
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
_ (Empty_ Sing ('HArray a)
_) = m
forall a. Monoid a => a
mempty
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (Array_ a '[] 'HNat
e1 a '[ 'HNat] a
e2) = a '[] 'HNat -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[] 'HNat
e1 m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` a '[ 'HNat] a -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[ 'HNat] a
e2
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (ArrayLiteral_ [a '[] a]
es) = (a '[] a -> m) -> [a '[] a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
F.foldMap a '[] a -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f [a '[] a]
es
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (Datum_ Datum (a '[]) (HData' t)
d) = (forall (i :: Hakaru). a '[] i -> m)
-> Datum (a '[]) (HData' t) -> m
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) m (a :: k1 -> *)
(j :: k2).
(Foldable11 f, Monoid m) =>
(forall (i :: k1). a i -> m) -> f a j -> m
foldMap11 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
forall (i :: Hakaru). a '[] i -> m
f Datum (a '[]) (HData' t)
d
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (Case_ a '[] a
e [Branch a a j]
bs) = a '[] a -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[] a
e m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` (Branch a a j -> m) -> [Branch a a j] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
F.foldMap ((forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m)
-> Branch a a j -> m
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *) m
(a :: k1 -> k2 -> *) (j :: k3).
(Foldable21 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j -> m
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f) [Branch a a j]
bs
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (Bucket a '[] 'HNat
b a '[] 'HNat
e Reducer a '[] j
r) = a '[] 'HNat -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[] 'HNat
b m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` a '[] 'HNat -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[] 'HNat
e m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m)
-> Reducer a '[] j -> m
forall k1 k2 k3 k4 (f :: (k1 -> k2 -> *) -> k3 -> k4 -> *) m
(a :: k1 -> k2 -> *) (j :: k3) (l :: k4).
(Foldable22 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j l -> m
foldMap22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f Reducer a '[] j
r
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (Superpose_ NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
pes) = (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m)
-> NonEmpty (a '[] 'HProb, a '[] ('HMeasure a)) -> m
forall k k m (f :: * -> *) (abt :: k -> k -> *) (xs :: k) (a :: k)
(ys :: k) (b :: k).
(Monoid m, Foldable f) =>
(forall (h :: k) (i :: k). abt h i -> m)
-> f (abt xs a, abt ys b) -> m
foldMapPairs forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
pes
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
_ (Reject_ Sing ('HMeasure a)
_) = m
forall a. Monoid a => a
mempty
foldMapPairs
:: (Monoid m, F.Foldable f)
=> (forall h i. abt h i -> m)
-> f (abt xs a, abt ys b)
-> m
foldMapPairs :: (forall (h :: k) (i :: k). abt h i -> m)
-> f (abt xs a, abt ys b) -> m
foldMapPairs forall (h :: k) (i :: k). abt h i -> m
f = ((abt xs a, abt ys b) -> m) -> f (abt xs a, abt ys b) -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
F.foldMap (((abt xs a, abt ys b) -> m) -> f (abt xs a, abt ys b) -> m)
-> ((abt xs a, abt ys b) -> m) -> f (abt xs a, abt ys b) -> m
forall a b. (a -> b) -> a -> b
$ \(abt xs a
e1,abt ys b
e2) -> abt xs a -> m
forall (h :: k) (i :: k). abt h i -> m
f abt xs a
e1 m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` abt ys b -> m
forall (h :: k) (i :: k). abt h i -> m
f abt ys b
e2
instance Traversable21 Term where
traverse21 :: (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> Term a j -> f (Term b j)
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (SCon args j
o :$ SArgs a args
es) = (SCon args j
o SCon args j -> SArgs b args -> Term b j
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
(abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$) (SArgs b args -> Term b j) -> f (SArgs b args) -> f (Term b j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> SArgs a args -> f (SArgs b args)
forall k1 k2 k3 (t :: (k1 -> k2 -> *) -> k3 -> *) (f :: * -> *)
(a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
(Traversable21 t, Applicative f) =>
(forall (h :: k1) (i :: k2). a h i -> f (b h i))
-> t a j -> f (t b j)
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f SArgs a args
es
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (NaryOp_ NaryOp j
o Seq (a '[] j)
es) = NaryOp j -> Seq (b '[] j) -> Term b j
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
NaryOp a -> Seq (abt '[] a) -> Term abt a
NaryOp_ NaryOp j
o (Seq (b '[] j) -> Term b j) -> f (Seq (b '[] j)) -> f (Term b j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a '[] j -> f (b '[] j)) -> Seq (a '[] j) -> f (Seq (b '[] j))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a '[] j -> f (b '[] j)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f Seq (a '[] j)
es
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
_ (Literal_ Literal j
v) = Term b j -> f (Term b j)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term b j -> f (Term b j)) -> Term b j -> f (Term b j)
forall a b. (a -> b) -> a -> b
$ Literal j -> Term b j
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Term abt a
Literal_ Literal j
v
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
_ (Empty_ Sing ('HArray a)
typ) = Term b ('HArray a) -> f (Term b ('HArray a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term b ('HArray a) -> f (Term b ('HArray a)))
-> Term b ('HArray a) -> f (Term b ('HArray a))
forall a b. (a -> b) -> a -> b
$ Sing ('HArray a) -> Term b ('HArray a)
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Sing ('HArray a) -> Term abt ('HArray a)
Empty_ Sing ('HArray a)
typ
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (Array_ a '[] 'HNat
e1 a '[ 'HNat] a
e2) = b '[] 'HNat -> b '[ 'HNat] a -> Term b ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] 'HNat -> abt '[ 'HNat] a -> Term abt ('HArray a)
Array_ (b '[] 'HNat -> b '[ 'HNat] a -> Term b ('HArray a))
-> f (b '[] 'HNat) -> f (b '[ 'HNat] a -> Term b ('HArray a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a '[] 'HNat -> f (b '[] 'HNat)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[] 'HNat
e1 f (b '[ 'HNat] a -> Term b ('HArray a))
-> f (b '[ 'HNat] a) -> f (Term b ('HArray a))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a '[ 'HNat] a -> f (b '[ 'HNat] a)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[ 'HNat] a
e2
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (ArrayLiteral_ [a '[] a]
es) = [b '[] a] -> Term b ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
[abt '[] a] -> Term abt ('HArray a)
ArrayLiteral_ ([b '[] a] -> Term b ('HArray a))
-> f [b '[] a] -> f (Term b ('HArray a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a '[] a -> f (b '[] a)) -> [a '[] a] -> f [b '[] a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a '[] a -> f (b '[] a)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f [a '[] a]
es
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (Bucket a '[] 'HNat
b a '[] 'HNat
e Reducer a '[] j
r) = b '[] 'HNat -> b '[] 'HNat -> Reducer b '[] j -> Term b j
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] 'HNat -> abt '[] 'HNat -> Reducer abt '[] a -> Term abt a
Bucket (b '[] 'HNat -> b '[] 'HNat -> Reducer b '[] j -> Term b j)
-> f (b '[] 'HNat)
-> f (b '[] 'HNat -> Reducer b '[] j -> Term b j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a '[] 'HNat -> f (b '[] 'HNat)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[] 'HNat
b f (b '[] 'HNat -> Reducer b '[] j -> Term b j)
-> f (b '[] 'HNat) -> f (Reducer b '[] j -> Term b j)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a '[] 'HNat -> f (b '[] 'HNat)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[] 'HNat
e f (Reducer b '[] j -> Term b j)
-> f (Reducer b '[] j) -> f (Term b j)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> Reducer a '[] j -> f (Reducer b '[] j)
forall k1 k2 k3 k4 (t :: (k1 -> k2 -> *) -> k3 -> k4 -> *)
(f :: * -> *) (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3)
(l :: k4).
(Traversable22 t, Applicative f) =>
(forall (h :: k1) (i :: k2). a h i -> f (b h i))
-> t a j l -> f (t b j l)
traverse22 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f Reducer a '[] j
r
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (Datum_ Datum (a '[]) (HData' t)
d) = Datum (b '[]) (HData' t) -> Term b j
forall (abt :: [Hakaru] -> Hakaru -> *) (t :: HakaruCon).
Datum (abt '[]) (HData' t) -> Term abt (HData' t)
Datum_ (Datum (b '[]) (HData' t) -> Term b j)
-> f (Datum (b '[]) (HData' t)) -> f (Term b j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (i :: Hakaru). a '[] i -> f (b '[] i))
-> Datum (a '[]) (HData' t) -> f (Datum (b '[]) (HData' t))
forall k1 k2 (t :: (k1 -> *) -> k2 -> *) (f :: * -> *)
(a :: k1 -> *) (b :: k1 -> *) (j :: k2).
(Traversable11 t, Applicative f) =>
(forall (i :: k1). a i -> f (b i)) -> t a j -> f (t b j)
traverse11 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
forall (i :: Hakaru). a '[] i -> f (b '[] i)
f Datum (a '[]) (HData' t)
d
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (Case_ a '[] a
e [Branch a a j]
bs) = b '[] a -> [Branch a b j] -> Term b j
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
abt '[] a -> [Branch a abt b] -> Term abt b
Case_ (b '[] a -> [Branch a b j] -> Term b j)
-> f (b '[] a) -> f ([Branch a b j] -> Term b j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a '[] a -> f (b '[] a)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[] a
e f ([Branch a b j] -> Term b j) -> f [Branch a b j] -> f (Term b j)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Branch a a j -> f (Branch a b j))
-> [Branch a a j] -> f [Branch a b j]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> Branch a a j -> f (Branch a b j)
forall k1 k2 k3 (t :: (k1 -> k2 -> *) -> k3 -> *) (f :: * -> *)
(a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
(Traversable21 t, Applicative f) =>
(forall (h :: k1) (i :: k2). a h i -> f (b h i))
-> t a j -> f (t b j)
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f) [Branch a a j]
bs
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (Superpose_ NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
pes) = NonEmpty (b '[] 'HProb, b '[] ('HMeasure a))
-> Term b ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> Term abt ('HMeasure a)
Superpose_ (NonEmpty (b '[] 'HProb, b '[] ('HMeasure a))
-> Term b ('HMeasure a))
-> f (NonEmpty (b '[] 'HProb, b '[] ('HMeasure a)))
-> f (Term b ('HMeasure a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
-> f (NonEmpty (b '[] 'HProb, b '[] ('HMeasure a)))
forall k k (f :: * -> *) (t :: * -> *) (abt1 :: k -> k -> *)
(abt2 :: k -> k -> *) (xs :: k) (a :: k) (ys :: k) (b :: k).
(Applicative f, Traversable t) =>
(forall (h :: k) (i :: k). abt1 h i -> f (abt2 h i))
-> t (abt1 xs a, abt1 ys b) -> f (t (abt2 xs a, abt2 ys b))
traversePairs forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
pes
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
_ (Reject_ Sing ('HMeasure a)
typ) = Term b ('HMeasure a) -> f (Term b ('HMeasure a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term b ('HMeasure a) -> f (Term b ('HMeasure a)))
-> Term b ('HMeasure a) -> f (Term b ('HMeasure a))
forall a b. (a -> b) -> a -> b
$ Sing ('HMeasure a) -> Term b ('HMeasure a)
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Sing ('HMeasure a) -> Term abt ('HMeasure a)
Reject_ Sing ('HMeasure a)
typ
traversePairs
:: (Applicative f, Traversable t)
=> (forall h i. abt1 h i -> f (abt2 h i))
-> t (abt1 xs a, abt1 ys b)
-> f (t (abt2 xs a, abt2 ys b))
traversePairs :: (forall (h :: k) (i :: k). abt1 h i -> f (abt2 h i))
-> t (abt1 xs a, abt1 ys b) -> f (t (abt2 xs a, abt2 ys b))
traversePairs forall (h :: k) (i :: k). abt1 h i -> f (abt2 h i)
f = ((abt1 xs a, abt1 ys b) -> f (abt2 xs a, abt2 ys b))
-> t (abt1 xs a, abt1 ys b) -> f (t (abt2 xs a, abt2 ys b))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (((abt1 xs a, abt1 ys b) -> f (abt2 xs a, abt2 ys b))
-> t (abt1 xs a, abt1 ys b) -> f (t (abt2 xs a, abt2 ys b)))
-> ((abt1 xs a, abt1 ys b) -> f (abt2 xs a, abt2 ys b))
-> t (abt1 xs a, abt1 ys b)
-> f (t (abt2 xs a, abt2 ys b))
forall a b. (a -> b) -> a -> b
$ \(abt1 xs a
x,abt1 ys b
y) -> (,) (abt2 xs a -> abt2 ys b -> (abt2 xs a, abt2 ys b))
-> f (abt2 xs a) -> f (abt2 ys b -> (abt2 xs a, abt2 ys b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> abt1 xs a -> f (abt2 xs a)
forall (h :: k) (i :: k). abt1 h i -> f (abt2 h i)
f abt1 xs a
x f (abt2 ys b -> (abt2 xs a, abt2 ys b))
-> f (abt2 ys b) -> f (abt2 xs a, abt2 ys b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> abt1 ys b -> f (abt2 ys b)
forall (h :: k) (i :: k). abt1 h i -> f (abt2 h i)
f abt1 ys b
y