{-# LANGUAGE CPP, GADTs #-}

{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
--                                                    2015.12.19
-- |
-- Module      :  Language.Hakaru.Syntax.AST.Sing
-- Copyright   :  Copyright (c) 2016 the Hakaru team
-- License     :  BSD3
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  experimental
-- Portability :  GHC-only
--
-- Factored out from "Language.Hakaru.Syntax.AST".
--
-- TODO: if we're not going to have this in "Language.Hakaru.Syntax.AST", then we should rename it to @Language.Hakaru.Syntax.AST.Sing@ or the like.
----------------------------------------------------------------
module Language.Hakaru.Syntax.AST.Sing
    ( sing_NaryOp
    , sing_PrimOp
    , sing_ArrayOp
    , sing_MeasureOp
    , sing_Literal
    ) where

import Language.Hakaru.Syntax.IClasses
import Language.Hakaru.Types.HClasses
import Language.Hakaru.Types.Sing
import Language.Hakaru.Syntax.AST

----------------------------------------------------------------
----------------------------------------------------------------

-- N.B., we do case analysis so that we don't need the class constraint!
sing_Literal :: Literal a -> Sing a
sing_Literal :: Literal a -> Sing a
sing_Literal (LNat  Natural
_) = Sing a
forall k (a :: k). SingI a => Sing a
sing
sing_Literal (LInt  Integer
_) = Sing a
forall k (a :: k). SingI a => Sing a
sing
sing_Literal (LProb NonNegativeRational
_) = Sing a
forall k (a :: k). SingI a => Sing a
sing
sing_Literal (LReal Rational
_) = Sing a
forall k (a :: k). SingI a => Sing a
sing

-- TODO: we don't need to store the HOrd\/HSemiring values here,
-- we can recover them by typeclass, just like we use 'sing' to get
-- 'sBool' for the other ones...
sing_NaryOp :: NaryOp a -> Sing a
sing_NaryOp :: NaryOp a -> Sing a
sing_NaryOp NaryOp a
And            = Sing a
forall k (a :: k). SingI a => Sing a
sing
sing_NaryOp NaryOp a
Or             = Sing a
forall k (a :: k). SingI a => Sing a
sing
sing_NaryOp NaryOp a
Xor            = Sing a
forall k (a :: k). SingI a => Sing a
sing
sing_NaryOp NaryOp a
Iff            = Sing a
forall k (a :: k). SingI a => Sing a
sing
sing_NaryOp (Min  HOrd a
theOrd)  = HOrd a -> Sing a
forall (a :: Hakaru). HOrd a -> Sing a
sing_HOrd      HOrd a
theOrd
sing_NaryOp (Max  HOrd a
theOrd)  = HOrd a -> Sing a
forall (a :: Hakaru). HOrd a -> Sing a
sing_HOrd      HOrd a
theOrd
sing_NaryOp (Sum  HSemiring a
theSemi) = HSemiring a -> Sing a
forall (a :: Hakaru). HSemiring a -> Sing a
sing_HSemiring HSemiring a
theSemi
sing_NaryOp (Prod HSemiring a
theSemi) = HSemiring a -> Sing a
forall (a :: Hakaru). HSemiring a -> Sing a
sing_HSemiring HSemiring a
theSemi

-- TODO: is there any way to define a @sing_List1@ like @sing@ for automating all these monomorphic cases?
sing_PrimOp :: PrimOp typs a -> (List1 Sing typs, Sing a)
sing_PrimOp :: PrimOp typs a -> (List1 Sing typs, Sing a)
sing_PrimOp PrimOp typs a
Not          = (Sing HBool
forall k (a :: k). SingI a => Sing a
sing Sing HBool -> List1 Sing '[] -> List1 Sing '[HBool]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
Impl         = (Sing HBool
forall k (a :: k). SingI a => Sing a
sing Sing HBool -> List1 Sing '[HBool] -> List1 Sing '[HBool, HBool]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` Sing HBool
forall k (a :: k). SingI a => Sing a
sing Sing HBool -> List1 Sing '[] -> List1 Sing '[HBool]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
Diff         = (Sing HBool
forall k (a :: k). SingI a => Sing a
sing Sing HBool -> List1 Sing '[HBool] -> List1 Sing '[HBool, HBool]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` Sing HBool
forall k (a :: k). SingI a => Sing a
sing Sing HBool -> List1 Sing '[] -> List1 Sing '[HBool]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
Nand         = (Sing HBool
forall k (a :: k). SingI a => Sing a
sing Sing HBool -> List1 Sing '[HBool] -> List1 Sing '[HBool, HBool]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` Sing HBool
forall k (a :: k). SingI a => Sing a
sing Sing HBool -> List1 Sing '[] -> List1 Sing '[HBool]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
Nor          = (Sing HBool
forall k (a :: k). SingI a => Sing a
sing Sing HBool -> List1 Sing '[HBool] -> List1 Sing '[HBool, HBool]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` Sing HBool
forall k (a :: k). SingI a => Sing a
sing Sing HBool -> List1 Sing '[] -> List1 Sing '[HBool]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
Pi           = (List1 Sing typs
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
Sin          = (Sing 'HReal
forall k (a :: k). SingI a => Sing a
sing Sing 'HReal -> List1 Sing '[] -> List1 Sing '[ 'HReal]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
Cos          = (Sing 'HReal
forall k (a :: k). SingI a => Sing a
sing Sing 'HReal -> List1 Sing '[] -> List1 Sing '[ 'HReal]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
Tan          = (Sing 'HReal
forall k (a :: k). SingI a => Sing a
sing Sing 'HReal -> List1 Sing '[] -> List1 Sing '[ 'HReal]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
Asin         = (Sing 'HReal
forall k (a :: k). SingI a => Sing a
sing Sing 'HReal -> List1 Sing '[] -> List1 Sing '[ 'HReal]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
Acos         = (Sing 'HReal
forall k (a :: k). SingI a => Sing a
sing Sing 'HReal -> List1 Sing '[] -> List1 Sing '[ 'HReal]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
Atan         = (Sing 'HReal
forall k (a :: k). SingI a => Sing a
sing Sing 'HReal -> List1 Sing '[] -> List1 Sing '[ 'HReal]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
Sinh         = (Sing 'HReal
forall k (a :: k). SingI a => Sing a
sing Sing 'HReal -> List1 Sing '[] -> List1 Sing '[ 'HReal]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
Cosh         = (Sing 'HReal
forall k (a :: k). SingI a => Sing a
sing Sing 'HReal -> List1 Sing '[] -> List1 Sing '[ 'HReal]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
Tanh         = (Sing 'HReal
forall k (a :: k). SingI a => Sing a
sing Sing 'HReal -> List1 Sing '[] -> List1 Sing '[ 'HReal]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
Asinh        = (Sing 'HReal
forall k (a :: k). SingI a => Sing a
sing Sing 'HReal -> List1 Sing '[] -> List1 Sing '[ 'HReal]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
Acosh        = (Sing 'HReal
forall k (a :: k). SingI a => Sing a
sing Sing 'HReal -> List1 Sing '[] -> List1 Sing '[ 'HReal]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
Atanh        = (Sing 'HReal
forall k (a :: k). SingI a => Sing a
sing Sing 'HReal -> List1 Sing '[] -> List1 Sing '[ 'HReal]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
RealPow      = (Sing 'HProb
forall k (a :: k). SingI a => Sing a
sing Sing 'HProb
-> List1 Sing '[ 'HReal] -> List1 Sing '[ 'HProb, 'HReal]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` Sing 'HReal
forall k (a :: k). SingI a => Sing a
sing Sing 'HReal -> List1 Sing '[] -> List1 Sing '[ 'HReal]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
Choose       = (Sing 'HNat
forall k (a :: k). SingI a => Sing a
sing Sing 'HNat -> List1 Sing '[ 'HNat] -> List1 Sing '[ 'HNat, 'HNat]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` Sing 'HNat
forall k (a :: k). SingI a => Sing a
sing Sing 'HNat -> List1 Sing '[] -> List1 Sing '[ 'HNat]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
Exp          = (Sing 'HReal
forall k (a :: k). SingI a => Sing a
sing Sing 'HReal -> List1 Sing '[] -> List1 Sing '[ 'HReal]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
Log          = (Sing 'HProb
forall k (a :: k). SingI a => Sing a
sing Sing 'HProb -> List1 Sing '[] -> List1 Sing '[ 'HProb]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
Floor        = (Sing 'HProb
forall k (a :: k). SingI a => Sing a
sing Sing 'HProb -> List1 Sing '[] -> List1 Sing '[ 'HProb]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp (Infinity HIntegrable a
h) = (List1 Sing typs
forall k (a :: k -> *). List1 a '[]
Nil1, HIntegrable a -> Sing a
forall (a :: Hakaru). HIntegrable a -> Sing a
sing_HIntegrable HIntegrable a
h)
sing_PrimOp PrimOp typs a
GammaFunc    = (Sing 'HReal
forall k (a :: k). SingI a => Sing a
sing Sing 'HReal -> List1 Sing '[] -> List1 Sing '[ 'HReal]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_PrimOp PrimOp typs a
BetaFunc     = (Sing 'HProb
forall k (a :: k). SingI a => Sing a
sing Sing 'HProb
-> List1 Sing '[ 'HProb] -> List1 Sing '[ 'HProb, 'HProb]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` Sing 'HProb
forall k (a :: k). SingI a => Sing a
sing Sing 'HProb -> List1 Sing '[] -> List1 Sing '[ 'HProb]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
-- Mere case analysis isn't enough for the rest of these, because
-- of the class constraints. We fix that by various helper functions
-- on explicit dictionary passing.
--
-- TODO: is there any way to automate building these from their
-- respective @a@ proofs?
sing_PrimOp (Equal HEq a
theEq) =
    let a :: Sing a
a = HEq a -> Sing a
forall (a :: Hakaru). HEq a -> Sing a
sing_HEq HEq a
theEq
    in  (Sing a
a Sing a -> List1 Sing '[a] -> List1 Sing '[a, a]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` Sing a
a Sing a -> List1 Sing '[] -> List1 Sing '[a]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
Sing HBool
sBool)
sing_PrimOp (Less HOrd a
theOrd) =
    let a :: Sing a
a = HOrd a -> Sing a
forall (a :: Hakaru). HOrd a -> Sing a
sing_HOrd HOrd a
theOrd
    in  (Sing a
a Sing a -> List1 Sing '[a] -> List1 Sing '[a, a]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` Sing a
a Sing a -> List1 Sing '[] -> List1 Sing '[a]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
Sing HBool
sBool)
sing_PrimOp (NatPow HSemiring a
theSemi) =
    let a :: Sing a
a = HSemiring a -> Sing a
forall (a :: Hakaru). HSemiring a -> Sing a
sing_HSemiring HSemiring a
theSemi
    in  (Sing a
a Sing a -> List1 Sing '[ 'HNat] -> List1 Sing '[a, 'HNat]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` Sing 'HNat
SNat Sing 'HNat -> List1 Sing '[] -> List1 Sing '[ 'HNat]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
a)
sing_PrimOp (Negate HRing a
theRing) =
    let a :: Sing a
a = HRing a -> Sing a
forall (a :: Hakaru). HRing a -> Sing a
sing_HRing HRing a
theRing
    in  (Sing a
a Sing a -> List1 Sing '[] -> List1 Sing '[a]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
a)
sing_PrimOp (Abs HRing a
theRing) =
    let a :: Sing a
a = HRing a -> Sing a
forall (a :: Hakaru). HRing a -> Sing a
sing_HRing HRing a
theRing
        b :: Sing (NonNegative a)
b = HRing a -> Sing (NonNegative a)
forall (a :: Hakaru). HRing a -> Sing (NonNegative a)
sing_NonNegative HRing a
theRing
    in  (Sing a
a Sing a -> List1 Sing '[] -> List1 Sing '[a]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
Sing (NonNegative a)
b)
sing_PrimOp (Signum HRing a
theRing) =
    let a :: Sing a
a = HRing a -> Sing a
forall (a :: Hakaru). HRing a -> Sing a
sing_HRing HRing a
theRing
    in  (Sing a
a Sing a -> List1 Sing '[] -> List1 Sing '[a]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
a)
sing_PrimOp (Recip HFractional a
theFrac) =
    let a :: Sing a
a = HFractional a -> Sing a
forall (a :: Hakaru). HFractional a -> Sing a
sing_HFractional HFractional a
theFrac
    in  (Sing a
a Sing a -> List1 Sing '[] -> List1 Sing '[a]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
a)
sing_PrimOp (NatRoot HRadical a
theRad) =
    let a :: Sing a
a = HRadical a -> Sing a
forall (a :: Hakaru). HRadical a -> Sing a
sing_HRadical HRadical a
theRad
    in  (Sing a
a Sing a -> List1 Sing '[ 'HNat] -> List1 Sing '[a, 'HNat]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` Sing 'HNat
SNat Sing 'HNat -> List1 Sing '[] -> List1 Sing '[ 'HNat]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
a)
sing_PrimOp (Erf HContinuous a
theCont) =
    let a :: Sing a
a = HContinuous a -> Sing a
forall (a :: Hakaru). HContinuous a -> Sing a
sing_HContinuous HContinuous a
theCont
    in  (Sing a
a Sing a -> List1 Sing '[] -> List1 Sing '[a]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
a)


sing_ArrayOp :: ArrayOp typs a -> (List1 Sing typs, Sing a)
sing_ArrayOp :: ArrayOp typs a -> (List1 Sing typs, Sing a)
sing_ArrayOp (Index  Sing a
a) = (Sing a -> Sing ('HArray a)
forall (a :: Hakaru). Sing a -> Sing ('HArray a)
SArray Sing a
a Sing ('HArray a)
-> List1 Sing '[ 'HNat] -> List1 Sing '[ 'HArray a, 'HNat]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` Sing 'HNat
SNat Sing 'HNat -> List1 Sing '[] -> List1 Sing '[ 'HNat]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
a)
sing_ArrayOp (Size   Sing a
a) = (Sing a -> Sing ('HArray a)
forall (a :: Hakaru). Sing a -> Sing ('HArray a)
SArray Sing a
a Sing ('HArray a) -> List1 Sing '[] -> List1 Sing '[ 'HArray a]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
Sing 'HNat
SNat)
sing_ArrayOp (Reduce Sing a
a) =
    ((Sing a
a Sing a -> Sing (a ':-> a) -> Sing (a ':-> (a ':-> a))
forall (a :: Hakaru) (b :: Hakaru).
Sing a -> Sing b -> Sing (a ':-> b)
`SFun` Sing a
a Sing a -> Sing a -> Sing (a ':-> a)
forall (a :: Hakaru) (b :: Hakaru).
Sing a -> Sing b -> Sing (a ':-> b)
`SFun` Sing a
a) Sing (a ':-> (a ':-> a))
-> List1 Sing '[a, 'HArray a]
-> List1 Sing '[ a ':-> (a ':-> a), a, 'HArray a]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` Sing a
a Sing a -> List1 Sing '[ 'HArray a] -> List1 Sing '[a, 'HArray a]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` Sing a -> Sing ('HArray a)
forall (a :: Hakaru). Sing a -> Sing ('HArray a)
SArray Sing a
a Sing ('HArray a) -> List1 Sing '[] -> List1 Sing '[ 'HArray a]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
a)


sing_MeasureOp :: MeasureOp typs a -> (List1 Sing typs, Sing a)
sing_MeasureOp :: MeasureOp typs a -> (List1 Sing typs, Sing a)
sing_MeasureOp MeasureOp typs a
Lebesgue    = (Sing 'HReal
forall k (a :: k). SingI a => Sing a
sing Sing 'HReal
-> List1 Sing '[ 'HReal] -> List1 Sing '[ 'HReal, 'HReal]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` Sing 'HReal
forall k (a :: k). SingI a => Sing a
sing Sing 'HReal -> List1 Sing '[] -> List1 Sing '[ 'HReal]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_MeasureOp MeasureOp typs a
Counting    = (List1 Sing typs
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_MeasureOp MeasureOp typs a
Categorical = (Sing ('HArray 'HProb)
forall k (a :: k). SingI a => Sing a
sing Sing ('HArray 'HProb)
-> List1 Sing '[] -> List1 Sing '[ 'HArray 'HProb]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_MeasureOp MeasureOp typs a
Uniform     = (Sing 'HReal
forall k (a :: k). SingI a => Sing a
sing Sing 'HReal
-> List1 Sing '[ 'HReal] -> List1 Sing '[ 'HReal, 'HReal]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` Sing 'HReal
forall k (a :: k). SingI a => Sing a
sing Sing 'HReal -> List1 Sing '[] -> List1 Sing '[ 'HReal]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_MeasureOp MeasureOp typs a
Normal      = (Sing 'HReal
forall k (a :: k). SingI a => Sing a
sing Sing 'HReal
-> List1 Sing '[ 'HProb] -> List1 Sing '[ 'HReal, 'HProb]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` Sing 'HProb
forall k (a :: k). SingI a => Sing a
sing Sing 'HProb -> List1 Sing '[] -> List1 Sing '[ 'HProb]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_MeasureOp MeasureOp typs a
Poisson     = (Sing 'HProb
forall k (a :: k). SingI a => Sing a
sing Sing 'HProb -> List1 Sing '[] -> List1 Sing '[ 'HProb]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_MeasureOp MeasureOp typs a
Gamma       = (Sing 'HProb
forall k (a :: k). SingI a => Sing a
sing Sing 'HProb
-> List1 Sing '[ 'HProb] -> List1 Sing '[ 'HProb, 'HProb]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` Sing 'HProb
forall k (a :: k). SingI a => Sing a
sing Sing 'HProb -> List1 Sing '[] -> List1 Sing '[ 'HProb]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)
sing_MeasureOp MeasureOp typs a
Beta        = (Sing 'HProb
forall k (a :: k). SingI a => Sing a
sing Sing 'HProb
-> List1 Sing '[ 'HProb] -> List1 Sing '[ 'HProb, 'HProb]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` Sing 'HProb
forall k (a :: k). SingI a => Sing a
sing Sing 'HProb -> List1 Sing '[] -> List1 Sing '[ 'HProb]
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
`Cons1` List1 Sing '[]
forall k (a :: k -> *). List1 a '[]
Nil1, Sing a
forall k (a :: k). SingI a => Sing a
sing)

----------------------------------------------------------------
----------------------------------------------------------- fin.