{-# LANGUAGE DataKinds
           , GADTs
           , FlexibleContexts
           , KindSignatures
           , PolyKinds
           #-}

{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
--                                                    2016.04.21
-- |
-- Module      :  Language.Hakaru.Observe
-- Copyright   :  Copyright (c) 2016 the Hakaru team
-- License     :  BSD3
-- Maintainer  :  ppaml@indiana.edu
-- Stability   :  experimental
-- Portability :  GHC-only
--
-- A simpler version of the work done in 'Language.Hakaru.Disintegrate'
--
-- In principle, this module's functionality is entirely subsumed
-- by the work done in Language.Hakaru.Disintegrate, so we can hope
-- to define observe in terms of disintegrate. This is still useful
-- as a guide to those that want something more in line with what other
-- probabilisitc programming systems support.
----------------------------------------------------------------
module Language.Hakaru.Observe where

import           Language.Hakaru.Syntax.AST
import           Language.Hakaru.Syntax.ABT
import           Language.Hakaru.Types.DataKind
import           Language.Hakaru.Types.Sing
import qualified Language.Hakaru.Syntax.Prelude as P
import           Language.Hakaru.Syntax.TypeOf

observe
    :: (ABT Term abt)
    => abt '[] ('HMeasure a)
    -> abt '[] a 
    -> abt '[] ('HMeasure a)
observe :: abt '[] ('HMeasure a) -> abt '[] a -> abt '[] ('HMeasure a)
observe abt '[] ('HMeasure a)
m abt '[] a
a = LC_ abt ('HMeasure a) -> LC_ abt a -> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
LC_ abt ('HMeasure a) -> LC_ abt a -> abt '[] ('HMeasure a)
observeAST (abt '[] ('HMeasure a) -> LC_ abt ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> LC_ abt a
LC_ abt '[] ('HMeasure a)
m) (abt '[] a -> LC_ abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> LC_ abt a
LC_ abt '[] a
a)


-- TODO: move this to ABT.hs
freshenVarRe
    :: ABT syn abt => Variable (a :: k) -> abt '[] (b :: k) -> Variable a
freshenVarRe :: Variable a -> abt '[] b -> Variable a
freshenVarRe Variable a
x abt '[] b
m = Variable a
x {varID :: Nat
varID = abt '[] b -> Nat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> Nat
nextFree abt '[] b
m Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
`max` abt '[] b -> Nat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> Nat
nextBind abt '[] b
m}


observeAST
    :: (ABT Term abt)
    => LC_ abt ('HMeasure a)
    -> LC_ abt a
    -> abt '[] ('HMeasure a)
observeAST :: LC_ abt ('HMeasure a) -> LC_ abt a -> abt '[] ('HMeasure a)
observeAST (LC_ abt '[] ('HMeasure a)
m) (LC_ abt '[] a
a) =
    abt '[] ('HMeasure a)
-> (Variable ('HMeasure a) -> abt '[] ('HMeasure a))
-> (Term abt ('HMeasure a) -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) r.
ABT syn abt =>
abt '[] a -> (Variable a -> r) -> (syn abt a -> r) -> r
caseVarSyn abt '[] ('HMeasure a)
m Variable ('HMeasure a) -> abt '[] ('HMeasure a)
forall k (a :: k) r. Variable a -> r
observeVar ((Term abt ('HMeasure a) -> abt '[] ('HMeasure a))
 -> abt '[] ('HMeasure a))
-> (Term abt ('HMeasure a) -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
forall a b. (a -> b) -> a -> b
$ \Term abt ('HMeasure a)
ast ->
        case Term abt ('HMeasure a)
ast of
        -- TODO: Add a name supply
        SCon args ('HMeasure a)
Let_ :$ abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End ->
            abt '[a] a
-> (Variable a -> abt '[] a -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (x :: k) (xs :: [k]) (a :: k) r.
ABT syn abt =>
abt (x : xs) a -> (Variable x -> abt xs a -> r) -> r
caseBind abt vars a
abt '[a] a
e2 ((Variable a -> abt '[] a -> abt '[] ('HMeasure a))
 -> abt '[] ('HMeasure a))
-> (Variable a -> abt '[] a -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
forall a b. (a -> b) -> a -> b
$ \Variable a
x abt '[] a
e2' ->
            let x' :: Variable a
x'   = Variable a -> abt '[] ('HMeasure a) -> Variable a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (b :: k).
ABT syn abt =>
Variable a -> abt '[] b -> Variable a
freshenVarRe Variable a
x abt '[] ('HMeasure a)
m
                e2'' :: abt '[] a
e2'' = Variable a -> Variable a -> abt '[] a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
(JmEq1 Sing, Show1 Sing, Functor21 syn, ABT syn abt) =>
Variable a -> Variable a -> abt xs b -> abt xs b
rename Variable a
x Variable a
x' abt '[] a
e2'
            in Term abt ('HMeasure a) -> abt '[] ('HMeasure a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (SCon '[LC a, '( '[a], 'HMeasure a)] ('HMeasure a)
forall (a :: Hakaru) (b :: Hakaru). SCon '[LC a, '( '[a], b)] b
Let_ SCon '[LC a, '( '[a], 'HMeasure a)] ('HMeasure a)
-> SArgs abt '[LC a, '( '[a], 'HMeasure a)]
-> Term abt ('HMeasure a)
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt vars a
e1 abt vars a
-> SArgs abt '[ '( '[a], 'HMeasure a)]
-> SArgs abt '[ '(vars, a), '( '[a], 'HMeasure a)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* Variable a -> abt '[] ('HMeasure a) -> abt '[a] ('HMeasure a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable a
x' (abt '[] ('HMeasure a) -> abt '[] a -> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] ('HMeasure a) -> abt '[] a -> abt '[] ('HMeasure a)
observe abt '[] a
abt '[] ('HMeasure a)
e2'' abt '[] a
a) abt '[a] ('HMeasure a)
-> SArgs abt '[] -> SArgs abt '[ '( '[a], 'HMeasure 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)
        --Dirac :$ e :* End -> P.if_ (e P.== a) (P.dirac a) P.reject
        -- TODO: Add a name supply
        SCon args ('HMeasure a)
MBind :$ abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End ->
            abt '[a] a
-> (Variable a -> abt '[] a -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (x :: k) (xs :: [k]) (a :: k) r.
ABT syn abt =>
abt (x : xs) a -> (Variable x -> abt xs a -> r) -> r
caseBind abt vars a
abt '[a] a
e2 ((Variable a -> abt '[] a -> abt '[] ('HMeasure a))
 -> abt '[] ('HMeasure a))
-> (Variable a -> abt '[] a -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
forall a b. (a -> b) -> a -> b
$ \Variable a
x abt '[] a
e2' ->
            let x' :: Variable a
x'   = Variable a -> abt '[] ('HMeasure a) -> Variable a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (b :: k).
ABT syn abt =>
Variable a -> abt '[] b -> Variable a
freshenVarRe Variable a
x abt '[] ('HMeasure a)
m
                e2'' :: abt '[] a
e2'' = Variable a -> Variable a -> abt '[] a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
(JmEq1 Sing, Show1 Sing, Functor21 syn, ABT syn abt) =>
Variable a -> Variable a -> abt xs b -> abt xs b
rename Variable a
x Variable a
x' abt '[] a
e2'
            in Term abt ('HMeasure a) -> abt '[] ('HMeasure a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (SCon '[LC ('HMeasure a), '( '[a], 'HMeasure a)] ('HMeasure a)
forall (a :: Hakaru) (a :: Hakaru).
SCon '[LC ('HMeasure a), '( '[a], 'HMeasure a)] ('HMeasure a)
MBind SCon '[LC ('HMeasure a), '( '[a], 'HMeasure a)] ('HMeasure a)
-> SArgs abt '[LC ('HMeasure a), '( '[a], 'HMeasure a)]
-> Term abt ('HMeasure a)
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt vars a
e1 abt vars a
-> SArgs abt '[ '( '[a], 'HMeasure a)]
-> SArgs abt '[ '(vars, a), '( '[a], 'HMeasure a)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* Variable a -> abt '[] ('HMeasure a) -> abt '[a] ('HMeasure a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable a
x' (abt '[] ('HMeasure a) -> abt '[] a -> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] ('HMeasure a) -> abt '[] a -> abt '[] ('HMeasure a)
observe abt '[] a
abt '[] ('HMeasure a)
e2'' abt '[] a
a) abt '[a] ('HMeasure a)
-> SArgs abt '[] -> SArgs abt '[ '( '[a], 'HMeasure 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)
        SCon args ('HMeasure a)
Plate :$ abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End ->
            abt '[ 'HNat] a
-> (Variable 'HNat -> abt '[] a -> abt '[] ('HMeasure ('HArray a)))
-> abt '[] ('HMeasure ('HArray a))
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (x :: k) (xs :: [k]) (a :: k) r.
ABT syn abt =>
abt (x : xs) a -> (Variable x -> abt xs a -> r) -> r
caseBind abt vars a
abt '[ 'HNat] a
e2 ((Variable 'HNat -> abt '[] a -> abt '[] ('HMeasure ('HArray a)))
 -> abt '[] ('HMeasure ('HArray a)))
-> (Variable 'HNat -> abt '[] a -> abt '[] ('HMeasure ('HArray a)))
-> abt '[] ('HMeasure ('HArray a))
forall a b. (a -> b) -> a -> b
$ \Variable 'HNat
x abt '[] a
e2' ->
            let a' :: abt '[] a
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 (ArrayOp '[ 'HArray a, 'HNat] a
-> SCon '[ '( '[], a), '( '[], 'HNat)] a
forall (typs :: [Hakaru]) (args :: [([Hakaru], Hakaru)])
       (a :: Hakaru).
(typs ~ UnLCs args, args ~ LCs typs) =>
ArrayOp typs a -> SCon args a
ArrayOp_ (Sing a -> ArrayOp '[ 'HArray a, 'HNat] a
forall (a :: Hakaru). Sing a -> ArrayOp '[ 'HArray a, 'HNat] a
Index (Sing ('HMeasure a) -> Sing a
forall (a :: Hakaru). Sing ('HMeasure a) -> Sing a
sUnMeasure (Sing ('HMeasure a) -> Sing a) -> Sing ('HMeasure a) -> Sing a
forall a b. (a -> b) -> a -> b
$ abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] a
e2'))
                        SCon '[ '( '[], a), '( '[], 'HNat)] a
-> SArgs abt '[ '( '[], a), '( '[], 'HNat)] -> Term abt a
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt '[] a
a
                        abt '[] a
-> SArgs abt '[ '( '[], 'HNat)]
-> SArgs abt '[ '( '[], a), '( '[], 'HNat)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* Variable 'HNat -> abt '[] 'HNat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable 'HNat
x abt '[] 'HNat -> SArgs abt '[] -> SArgs abt '[ '( '[], 'HNat)]
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)
            in Term abt ('HMeasure ('HArray a)) -> abt '[] ('HMeasure ('HArray a))
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (SCon
  '[ '( '[], 'HNat), '( '[ 'HNat], 'HMeasure a)]
  ('HMeasure ('HArray a))
forall (a :: Hakaru).
SCon
  '[ '( '[], 'HNat), '( '[ 'HNat], 'HMeasure a)]
  ('HMeasure ('HArray a))
Plate SCon
  '[ '( '[], 'HNat), '( '[ 'HNat], 'HMeasure a)]
  ('HMeasure ('HArray a))
-> SArgs abt '[ '( '[], 'HNat), '( '[ 'HNat], 'HMeasure a)]
-> Term abt ('HMeasure ('HArray a))
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt vars a
e1 abt vars a
-> SArgs abt '[ '( '[ 'HNat], 'HMeasure a)]
-> SArgs abt '[ '(vars, a), '( '[ 'HNat], 'HMeasure a)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* Variable 'HNat
-> abt '[] ('HMeasure a) -> abt '[ 'HNat] ('HMeasure a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable 'HNat
x (abt '[] ('HMeasure a) -> abt '[] a -> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] ('HMeasure a) -> abt '[] a -> abt '[] ('HMeasure a)
observe abt '[] a
abt '[] ('HMeasure a)
e2' abt '[] a
a') abt '[ 'HNat] ('HMeasure a)
-> SArgs abt '[] -> SArgs abt '[ '( '[ 'HNat], 'HMeasure 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)
        MeasureOp_ MeasureOp typs a
op :$ SArgs abt args
es -> MeasureOp typs a
-> SArgs abt args -> abt '[] a -> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (typs :: [Hakaru])
       (args :: [([Hakaru], Hakaru)]) (a :: Hakaru).
(ABT Term abt, typs ~ UnLCs args, args ~ LCs typs) =>
MeasureOp typs a
-> SArgs abt args -> abt '[] a -> abt '[] ('HMeasure a)
observeMeasureOp MeasureOp typs a
op SArgs abt args
es abt '[] a
abt '[] a
a
        Term abt ('HMeasure a)
_ -> [Char] -> abt '[] ('HMeasure a)
forall a. HasCallStack => [Char] -> a
error [Char]
"observe can only be applied to measure primitives"

-- This function can't inspect a variable due to
-- calls to subst that happens in Let_ and Bind_
observeVar :: Variable a -> r
observeVar :: Variable a -> r
observeVar = [Char] -> Variable a -> r
forall a. HasCallStack => [Char] -> a
error [Char]
"observe can only be applied measure primitives"

observeMeasureOp
    :: (ABT Term abt, typs ~ UnLCs args, args ~ LCs typs)
    => MeasureOp typs a
    -> SArgs abt args
    -> abt '[] a
    -> abt '[] ('HMeasure a)
observeMeasureOp :: MeasureOp typs a
-> SArgs abt args -> abt '[] a -> abt '[] ('HMeasure a)
observeMeasureOp MeasureOp typs a
Normal = \(abt vars a
mu :* abt vars a
sd :* SArgs abt args
End) abt '[] a
a ->
    abt '[] 'HProb -> abt '[] ('HMeasure a) -> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (w :: Hakaru).
ABT Term abt =>
abt '[] 'HProb -> abt '[] ('HMeasure w) -> abt '[] ('HMeasure w)
P.withWeight (abt '[] 'HReal
-> abt '[] 'HProb -> abt '[] 'HReal -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal
-> abt '[] 'HProb -> abt '[] 'HReal -> abt '[] 'HProb
P.densityNormal abt vars a
abt '[] 'HReal
mu abt vars a
abt '[] 'HProb
sd abt '[] a
abt '[] 'HReal
a) (abt '[] a -> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> abt '[] ('HMeasure a)
P.dirac abt '[] a
a)
observeMeasureOp MeasureOp typs a
Uniform = \(abt vars a
lo :* abt vars a
hi :* SArgs abt args
End) abt '[] a
a ->
    abt '[] HBool
-> abt '[] ('HMeasure a)
-> abt '[] ('HMeasure a)
-> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] HBool -> abt '[] a -> abt '[] a -> abt '[] a
P.if_ (abt vars a
abt '[] a
lo abt '[] a -> abt '[] a -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HOrd_ a) =>
abt '[] a -> abt '[] a -> abt '[] HBool
P.<= abt '[] a
abt '[] a
a abt '[] HBool -> abt '[] HBool -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] HBool -> abt '[] HBool -> abt '[] HBool
P.&& abt '[] a
a abt '[] a -> abt '[] a -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HOrd_ a) =>
abt '[] a -> abt '[] a -> abt '[] HBool
P.<= abt vars a
abt '[] a
hi)
        (abt '[] 'HProb -> abt '[] ('HMeasure a) -> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (w :: Hakaru).
ABT Term abt =>
abt '[] 'HProb -> abt '[] ('HMeasure w) -> abt '[] ('HMeasure w)
P.withWeight (abt '[] 'HReal -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HProb
P.unsafeProb (abt '[] 'HReal -> abt '[] 'HProb)
-> abt '[] 'HReal -> abt '[] 'HProb
forall a b. (a -> b) -> a -> b
$ abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HFractional_ a) =>
abt '[] a -> abt '[] a
P.recip (abt '[] a -> abt '[] a) -> abt '[] a -> abt '[] a
forall a b. (a -> b) -> a -> b
$ abt vars a
abt '[] a
hi abt '[] a -> abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HRing_ a) =>
abt '[] a -> abt '[] a -> abt '[] a
P.- abt vars a
abt '[] a
lo) (abt '[] a -> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> abt '[] ('HMeasure a)
P.dirac abt '[] a
a))
        (Sing ('HMeasure 'HReal) -> abt '[] ('HMeasure 'HReal)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Sing ('HMeasure a) -> abt '[] ('HMeasure a)
P.reject (Sing 'HReal -> Sing ('HMeasure 'HReal)
forall (a :: Hakaru). Sing a -> Sing ('HMeasure a)
SMeasure Sing 'HReal
SReal))
observeMeasureOp MeasureOp typs a
_ = [Char] -> SArgs abt args -> abt '[] a -> abt '[] ('HMeasure a)
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO{Observe:observeMeasureOp}"