{-# LANGUAGE CPP
           , GADTs
           , KindSignatures
           , DataKinds
           , TypeOperators
           , Rank2Types
           , BangPatterns
           , FlexibleContexts
           , MultiParamTypeClasses
           , FunctionalDependencies
           , FlexibleInstances
           , UndecidableInstances
           , EmptyCase
           , ScopedTypeVariables
           #-}

{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
--                                                    2016.05.24
-- |
-- Module      :  Language.Hakaru.Evaluation.PEvalMonad
-- Copyright   :  Copyright (c) 2016 the Hakaru team
-- License     :  BSD3
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  experimental
-- Portability :  GHC-only
--
-- A unified 'EvaluationMonad' for pure evaluation, expect, and
-- disintegrate.
----------------------------------------------------------------
module Language.Hakaru.Evaluation.PEvalMonad
    (
    -- * The unified 'PEval' monad
    -- ** List-based version
      ListContext(..), PAns, PEval(..)
    , runPureEval, runImpureEval, runExpectEval
    -- ** TODO: IntMap-based version
    
    -- * Operators on the disintegration monad
    -- ** The \"zero\" and \"one\"
    , bot
    --, reject
    -- ** Emitting code
    , emit
    , emitMBind
    , emitLet
    , emitLet'
    , emitUnpair
    -- TODO: emitUneither
    -- emitCaseWith
    , emit_
    , emitMBind_
    , emitGuard
    , emitWeight
    , emitFork_
    , emitSuperpose
    , choose
    ) where

import           Prelude              hiding (id, (.))
import           Control.Category     (Category(..))
#if __GLASGOW_HASKELL__ < 710
import           Data.Monoid          (Monoid(..))
import           Data.Functor         ((<$>))
import           Control.Applicative  (Applicative(..))
#endif
import qualified Data.Foldable        as F
import qualified Data.Traversable     as T
import qualified Data.List.NonEmpty   as NE
import           Control.Applicative  (Alternative(..))
import           Control.Monad        (MonadPlus(..))
import           Data.Text            (Text)
import qualified Data.Text            as Text

import Language.Hakaru.Syntax.IClasses
import Data.Number.Nat
import Language.Hakaru.Types.DataKind
import Language.Hakaru.Types.Sing    (Sing, sUnMeasure, sUnPair)
import Language.Hakaru.Syntax.AST
import Language.Hakaru.Syntax.TypeOf
import Language.Hakaru.Syntax.ABT
import Language.Hakaru.Syntax.Datum
import Language.Hakaru.Syntax.DatumABT
import qualified Language.Hakaru.Syntax.Prelude as P
import Language.Hakaru.Evaluation.Types
import Language.Hakaru.Evaluation.Lazy (reifyPair)

#ifdef __TRACE_DISINTEGRATE__
import Debug.Trace (trace)
#endif

----------------------------------------------------------------
----------------------------------------------------------------
-- | An ordered collection of statements representing the context
-- surrounding the current focus of our program transformation.
-- That is, since some transformations work from the bottom up, we
-- need to keep track of the statements we passed along the way
-- when reaching for the bottom.
--
-- The tail of the list takes scope over the head of the list. Thus,
-- the back\/end of the list is towards the top of the program,
-- whereas the front of the list is towards the bottom.
--
-- This type was formerly called @Heap@ (presumably due to the
-- 'Statement' type being called @Binding@) but that seems like a
-- misnomer to me since this really has nothing to do with allocation.
-- However, it is still like a heap inasmuch as it's a dependency
-- graph and we may wish to change the topological sorting or remove
-- \"garbage\" (subject to correctness criteria).
--
-- TODO: Figure out what to do with 'SWeight', 'SGuard', 'SStuff',
-- etc, so that we can use an @IntMap (Statement abt)@ in order to
-- speed up the lookup times in 'select'. (Assuming callers don't
-- use 'unsafePush' unsafely: we can recover the order things were
-- inserted from their 'varID' since we've freshened them all and
-- therefore their IDs are monotonic in the insertion order.)
data ListContext (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) =
    ListContext
    { ListContext abt p -> Nat
nextFreshNat :: {-# UNPACK #-} !Nat
    , ListContext abt p -> [Statement abt Location p]
statements   :: [Statement abt Location p]
    }


-- HACK: we can't use a type family and do @abt xs (P p a)@ because
-- of non-injectivity. So we make this a GADT instead. Because it's
-- a GADT, there's a bunch of ugly rewrapping required; but everything
-- seems to work out just fine...
data P :: Purity -> ([Hakaru] -> Hakaru -> *) -> [Hakaru] -> Hakaru -> *
    where
    PPure   :: !(abt xs a)             -> P 'Pure    abt xs a
    PImpure :: !(abt xs ('HMeasure a)) -> P 'Impure  abt xs a
    PExpect :: !(abt xs 'HProb)        -> P 'ExpectP abt xs a

unPPure :: P 'Pure abt xs a -> abt xs a
unPPure :: P 'Pure abt xs a -> abt xs a
unPPure (PPure abt xs a
e) = abt xs a
e

unPImpure :: P 'Impure abt xs a -> abt xs ('HMeasure a)
unPImpure :: P 'Impure abt xs a -> abt xs ('HMeasure a)
unPImpure (PImpure abt xs ('HMeasure a)
e) = abt xs ('HMeasure a)
e

unPExpect :: P 'ExpectP abt xs a -> abt xs 'HProb
unPExpect :: P 'ExpectP abt xs a -> abt xs 'HProb
unPExpect (PExpect abt xs 'HProb
e) = abt xs 'HProb
e

mapPPure :: (abt xs a -> abt ys b) -> P 'Pure abt xs a -> P 'Pure abt ys b
mapPPure :: (abt xs a -> abt ys b) -> P 'Pure abt xs a -> P 'Pure abt ys b
mapPPure abt xs a -> abt ys b
f (PPure abt xs a
e) = abt ys b -> P 'Pure abt ys b
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
abt xs a -> P 'Pure abt xs a
PPure (abt xs a -> abt ys b
f abt xs a
e)

mapPImpure
    :: (abt xs ('HMeasure a) -> abt ys ('HMeasure b))
    -> P 'Impure abt xs a
    -> P 'Impure abt ys b
mapPImpure :: (abt xs ('HMeasure a) -> abt ys ('HMeasure b))
-> P 'Impure abt xs a -> P 'Impure abt ys b
mapPImpure abt xs ('HMeasure a) -> abt ys ('HMeasure b)
f (PImpure abt xs ('HMeasure a)
e) = abt ys ('HMeasure b) -> P 'Impure abt ys b
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
abt xs ('HMeasure a) -> P 'Impure abt xs a
PImpure (abt xs ('HMeasure a) -> abt ys ('HMeasure b)
f abt xs ('HMeasure a)
e)

mapPExpect
    :: (abt xs 'HProb -> abt ys 'HProb)
    -> P 'ExpectP abt xs a
    -> P 'ExpectP abt ys b
mapPExpect :: (abt xs 'HProb -> abt ys 'HProb)
-> P 'ExpectP abt xs a -> P 'ExpectP abt ys b
mapPExpect abt xs 'HProb -> abt ys 'HProb
f (PExpect abt xs 'HProb
e) = abt ys 'HProb -> P 'ExpectP abt ys b
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
abt xs 'HProb -> P 'ExpectP abt xs a
PExpect (abt xs 'HProb -> abt ys 'HProb
f abt xs 'HProb
e)

mapP
    :: (forall a. abt xs a -> abt ys a)
    -> P p abt xs b
    -> P p abt ys b
mapP :: (forall (a :: Hakaru). abt xs a -> abt ys a)
-> P p abt xs b -> P p abt ys b
mapP forall (a :: Hakaru). abt xs a -> abt ys a
f (PPure   abt xs b
e) = abt ys b -> P 'Pure abt ys b
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
abt xs a -> P 'Pure abt xs a
PPure   (abt ys b -> P 'Pure abt ys b) -> abt ys b -> P 'Pure abt ys b
forall a b. (a -> b) -> a -> b
$ abt xs b -> abt ys b
forall (a :: Hakaru). abt xs a -> abt ys a
f abt xs b
e
mapP forall (a :: Hakaru). abt xs a -> abt ys a
f (PImpure abt xs ('HMeasure b)
e) = abt ys ('HMeasure b) -> P 'Impure abt ys b
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
abt xs ('HMeasure a) -> P 'Impure abt xs a
PImpure (abt ys ('HMeasure b) -> P 'Impure abt ys b)
-> abt ys ('HMeasure b) -> P 'Impure abt ys b
forall a b. (a -> b) -> a -> b
$ abt xs ('HMeasure b) -> abt ys ('HMeasure b)
forall (a :: Hakaru). abt xs a -> abt ys a
f abt xs ('HMeasure b)
e
mapP forall (a :: Hakaru). abt xs a -> abt ys a
f (PExpect abt xs 'HProb
e) = abt ys 'HProb -> P 'ExpectP abt ys b
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
abt xs 'HProb -> P 'ExpectP abt xs a
PExpect (abt ys 'HProb -> P 'ExpectP abt ys b)
-> abt ys 'HProb -> P 'ExpectP abt ys b
forall a b. (a -> b) -> a -> b
$ abt xs 'HProb -> abt ys 'HProb
forall (a :: Hakaru). abt xs a -> abt ys a
f abt xs 'HProb
e

-- | Plug a term into a context. That is, the 'statements' of the
-- context specifies a program with a hole in it; so we plug the
-- given term into that hole, returning the complete program.
residualizeListContext
    :: forall abt p a
    .  (ABT Term abt)
    => ListContext abt p
    -> P p abt '[] a
    -> P p abt '[] a
residualizeListContext :: ListContext abt p -> P p abt '[] a -> P p abt '[] a
residualizeListContext =
    -- N.B., we use a left fold because the head of the list of
    -- statements is the one closest to the hole.
    \ListContext abt p
ss P p abt '[] a
e0 -> (P p abt '[] a -> Statement abt Location p -> P p abt '[] a)
-> P p abt '[] a -> [Statement abt Location p] -> P p abt '[] a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Statement abt Location p -> P p abt '[] a -> P p abt '[] a)
-> P p abt '[] a -> Statement abt Location p -> P p abt '[] a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Statement abt Location p -> P p abt '[] a -> P p abt '[] a
step) P p abt '[] a
e0 (ListContext abt p -> [Statement abt Location p]
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity).
ListContext abt p -> [Statement abt Location p]
statements ListContext abt p
ss)
    where
    step
        :: Statement abt Location p
        -> P p abt '[] a
        -> P p abt '[] a
    step :: Statement abt Location p -> P p abt '[] a -> P p abt '[] a
step (SLet  (Location Variable a
x) Lazy abt a
body [Index (abt '[])]
_)  = (forall (a :: Hakaru). abt '[] a -> abt '[] a)
-> P p abt '[] a -> P p abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (ys :: [Hakaru]) (p :: Purity) (b :: Hakaru).
(forall (a :: Hakaru). abt xs a -> abt ys a)
-> P p abt xs b -> P p abt ys b
mapP ((forall (a :: Hakaru). abt '[] a -> abt '[] a)
 -> P p abt '[] a -> P p abt '[] a)
-> (forall (a :: Hakaru). abt '[] a -> abt '[] a)
-> P p abt '[] a
-> P p abt '[] a
forall a b. (a -> b) -> a -> b
$ Variable a -> Lazy abt a -> abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Variable a -> Lazy abt a -> abt '[] b -> abt '[] b
residualizeLet Variable a
x Lazy abt a
body
    step (SBind (Location Variable a
x) Lazy abt ('HMeasure a)
body [Index (abt '[])]
_) = (abt '[] ('HMeasure a) -> abt '[] ('HMeasure a))
-> P 'Impure abt '[] a -> P 'Impure abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru) (ys :: [Hakaru]) (b :: Hakaru).
(abt xs ('HMeasure a) -> abt ys ('HMeasure b))
-> P 'Impure abt xs a -> P 'Impure abt ys b
mapPImpure ((abt '[] ('HMeasure a) -> abt '[] ('HMeasure a))
 -> P 'Impure abt '[] a -> P 'Impure abt '[] a)
-> (abt '[] ('HMeasure a) -> abt '[] ('HMeasure a))
-> P 'Impure abt '[] a
-> P 'Impure abt '[] a
forall a b. (a -> b) -> a -> b
$ \abt '[] ('HMeasure a)
e ->
        -- TODO: if @body@ is dirac, then treat as 'SLet'
        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) (b :: Hakaru).
SCon '[LC ('HMeasure a), '( '[a], 'HMeasure b)] ('HMeasure b)
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
:$ Lazy abt ('HMeasure a) -> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Lazy abt a -> abt '[] a
fromLazy Lazy abt ('HMeasure a)
body abt '[] ('HMeasure a)
-> SArgs abt '[ '( '[a], 'HMeasure a)]
-> SArgs abt '[LC ('HMeasure 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)
e 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)
    step (SGuard List1 Location xs
xs Pattern xs a
pat Lazy abt a
scrutinee [Index (abt '[])]
_) = (abt '[] ('HMeasure a) -> abt '[] ('HMeasure a))
-> P 'Impure abt '[] a -> P 'Impure abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru) (ys :: [Hakaru]) (b :: Hakaru).
(abt xs ('HMeasure a) -> abt ys ('HMeasure b))
-> P 'Impure abt xs a -> P 'Impure abt ys b
mapPImpure ((abt '[] ('HMeasure a) -> abt '[] ('HMeasure a))
 -> P 'Impure abt '[] a -> P 'Impure abt '[] a)
-> (abt '[] ('HMeasure a) -> abt '[] ('HMeasure a))
-> P 'Impure abt '[] a
-> P 'Impure abt '[] a
forall a b. (a -> b) -> a -> b
$ \abt '[] ('HMeasure a)
e ->
        -- TODO: avoid adding the 'PWild' branch if we know @pat@ covers the type
        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 (Term abt ('HMeasure a) -> abt '[] ('HMeasure a))
-> Term abt ('HMeasure a) -> abt '[] ('HMeasure a)
forall a b. (a -> b) -> a -> b
$ abt '[] a -> [Branch a abt ('HMeasure a)] -> Term abt ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
abt '[] a -> [Branch a abt b] -> Term abt b
Case_ (Lazy abt a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Lazy abt a -> abt '[] a
fromLazy Lazy abt a
scrutinee)
            [ Pattern xs a -> abt xs ('HMeasure a) -> Branch a abt ('HMeasure a)
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *) (b :: Hakaru)
       (xs :: [Hakaru]).
Pattern xs a -> abt xs b -> Branch a abt b
Branch Pattern xs a
pat   (abt xs ('HMeasure a) -> Branch a abt ('HMeasure a))
-> abt xs ('HMeasure a) -> Branch a abt ('HMeasure a)
forall a b. (a -> b) -> a -> b
$ List1 Variable xs -> abt '[] ('HMeasure a) -> abt xs ('HMeasure a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (b :: k).
ABT syn abt =>
List1 Variable xs -> abt '[] b -> abt xs b
binds_ (List1 Location xs -> List1 Variable xs
forall k (a :: [k]). List1 Location a -> List1 Variable a
fromLocations1 List1 Location xs
xs) abt '[] ('HMeasure a)
e
            , Pattern '[] a
-> abt '[] ('HMeasure a) -> Branch a abt ('HMeasure a)
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *) (b :: Hakaru)
       (xs :: [Hakaru]).
Pattern xs a -> abt xs b -> Branch a abt b
Branch Pattern '[] a
forall (a :: Hakaru). Pattern '[] a
PWild (abt '[] ('HMeasure a) -> Branch a abt ('HMeasure a))
-> abt '[] ('HMeasure a) -> Branch a abt ('HMeasure a)
forall a b. (a -> b) -> a -> b
$ Sing ('HMeasure a) -> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Sing ('HMeasure a) -> abt '[] ('HMeasure a)
P.reject (abt '[] ('HMeasure a) -> Sing ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] ('HMeasure a)
e)
            ]
    step (SWeight Lazy abt 'HProb
body [Index (abt '[])]
_) = (abt '[] ('HMeasure a) -> abt '[] ('HMeasure a))
-> P 'Impure abt '[] a -> P 'Impure abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru) (ys :: [Hakaru]) (b :: Hakaru).
(abt xs ('HMeasure a) -> abt ys ('HMeasure b))
-> P 'Impure abt xs a -> P 'Impure abt ys b
mapPImpure ((abt '[] ('HMeasure a) -> abt '[] ('HMeasure a))
 -> P 'Impure abt '[] a -> P 'Impure abt '[] a)
-> (abt '[] ('HMeasure a) -> abt '[] ('HMeasure a))
-> P 'Impure abt '[] a
-> P 'Impure abt '[] a
forall a b. (a -> b) -> a -> b
$ 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 (Lazy abt 'HProb -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Lazy abt a -> abt '[] a
fromLazy Lazy abt 'HProb
body)
    step (SStuff0    abt '[] 'HProb -> abt '[] 'HProb
f [Index (abt '[])]
_) = (abt '[] 'HProb -> abt '[] 'HProb)
-> P 'ExpectP abt '[] a -> P 'ExpectP abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (ys :: [Hakaru]) (a :: Hakaru) (b :: Hakaru).
(abt xs 'HProb -> abt ys 'HProb)
-> P 'ExpectP abt xs a -> P 'ExpectP abt ys b
mapPExpect abt '[] 'HProb -> abt '[] 'HProb
f
    step (SStuff1 Location a
_x abt '[] 'HProb -> abt '[] 'HProb
f [Index (abt '[])]
_) = (abt '[] 'HProb -> abt '[] 'HProb)
-> P 'ExpectP abt '[] a -> P 'ExpectP abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (ys :: [Hakaru]) (a :: Hakaru) (b :: Hakaru).
(abt xs 'HProb -> abt ys 'HProb)
-> P 'ExpectP abt xs a -> P 'ExpectP abt ys b
mapPExpect abt '[] 'HProb -> abt '[] 'HProb
f


-- TODO: move this to Prelude? Is there anyone else that actually needs these smarts?
residualizeLet
    :: (ABT Term abt) => Variable a -> Lazy abt a -> abt '[] b -> abt '[] b
residualizeLet :: Variable a -> Lazy abt a -> abt '[] b -> abt '[] b
residualizeLet Variable a
x Lazy abt a
body abt '[] b
scope
    -- Drop unused bindings
    | Bool -> Bool
not (Variable a
x Variable a -> VarSet (KindOf b) -> Bool
forall k (a :: k) (kproxy :: KProxy k).
(Show1 Sing, JmEq1 Sing) =>
Variable a -> VarSet kproxy -> Bool
`memberVarSet` abt '[] b -> VarSet (KindOf b)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> VarSet (KindOf a)
freeVars abt '[] b
scope) = abt '[] b
scope
    -- TODO: if used exactly once in @e@, then inline.
    | Bool
otherwise =
        case Lazy abt a -> Maybe (Variable a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Lazy abt a -> Maybe (Variable a)
getLazyVariable Lazy abt a
body of
        Just Variable a
y  -> Variable a -> abt '[] a -> abt '[] b -> abt '[] b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
(JmEq1 Sing, Show1 Sing, Traversable21 syn, ABT syn abt) =>
Variable a -> abt '[] a -> abt xs b -> abt xs b
subst Variable a
x (Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable a
y) abt '[] b
scope
        Maybe (Variable a)
Nothing ->
            case Lazy abt a -> Maybe (Literal a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Lazy abt a -> Maybe (Literal a)
getLazyLiteral Lazy abt a
body of
            Just Literal a
v  -> Variable a -> abt '[] a -> abt '[] b -> abt '[] b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
(JmEq1 Sing, Show1 Sing, Traversable21 syn, ABT syn abt) =>
Variable a -> abt '[] a -> abt xs b -> abt xs b
subst Variable a
x (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 -> abt '[] a) -> Term abt a -> abt '[] a
forall a b. (a -> b) -> a -> b
$ Literal a -> Term abt a
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Term abt a
Literal_ Literal a
v) abt '[] b
scope
            Maybe (Literal a)
Nothing ->
                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 (SCon '[LC a, '( '[a], b)] b
forall (a :: Hakaru) (b :: Hakaru). SCon '[LC a, '( '[a], b)] b
Let_ SCon '[LC a, '( '[a], b)] b
-> SArgs abt '[LC a, '( '[a], b)] -> Term abt b
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ Lazy abt a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Lazy abt a -> abt '[] a
fromLazy Lazy abt a
body abt '[] a
-> SArgs abt '[ '( '[a], b)] -> SArgs abt '[LC a, '( '[a], b)]
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 '[] b -> abt '[a] b
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 '[] b
scope abt '[a] b -> SArgs abt '[] -> SArgs abt '[ '( '[a], 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)

----------------------------------------------------------------
type PAns p abt m a = ListContext abt p -> m (P p abt '[] a)


----------------------------------------------------------------
-- TODO: defunctionalize the continuation. In particular, the only
-- heap modifications we need are 'push' and a variant of 'update'
-- for finding\/replacing a binding once we have the value in hand;
-- and the only 'freshNat' modifications are to allocate new 'Nat'.
-- We could defunctionalize the second arrow too by relying on the
-- @Codensity (ReaderT e m) ~= StateT e (Codensity m)@ isomorphism,
-- which makes explicit that the only thing other than 'ListContext'
-- updates is emitting something like @[Statement]@ to serve as the
-- beginning of the final result.
--
-- | TODO: give this a better, more informative name!
newtype PEval abt p m x =
    PEval { PEval abt p m x
-> forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a
unPEval :: forall a. (x -> PAns p abt m a) -> PAns p abt m a }
    -- == Codensity (PAns p abt m)


-- | Run an 'Impure' computation in the 'PEval' monad, residualizing
-- out all the statements in the final evaluation context. The
-- second argument should include all the terms altered by the
-- 'PEval' expression; this is necessary to ensure proper hygiene;
-- for example(s):
--
-- > runPEval (perform e) [Some2 e]
-- > runPEval (constrainOutcome e v) [Some2 e, Some2 v]
--
-- We use 'Some2' on the inputs because it doesn't matter what their
-- type or locally-bound variables are, so we want to allow @f@ to
-- contain terms with different indices.
runImpureEval
    :: (ABT Term abt, Applicative m, F.Foldable f)
    => PEval abt 'Impure m (abt '[] a)
    -> f (Some2 abt)
    -> m (abt '[] ('HMeasure a))
runImpureEval :: PEval abt 'Impure m (abt '[] a)
-> f (Some2 abt) -> m (abt '[] ('HMeasure a))
runImpureEval PEval abt 'Impure m (abt '[] a)
m f (Some2 abt)
es =
    P 'Impure abt '[] a -> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
P 'Impure abt xs a -> abt xs ('HMeasure a)
unPImpure (P 'Impure abt '[] a -> abt '[] ('HMeasure a))
-> m (P 'Impure abt '[] a) -> m (abt '[] ('HMeasure a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PEval abt 'Impure m (abt '[] a)
-> (abt '[] a -> PAns 'Impure abt m a) -> PAns 'Impure abt m a
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
PEval abt p m x
-> forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a
unPEval PEval abt 'Impure m (abt '[] a)
m abt '[] a -> PAns 'Impure abt m a
forall (f :: * -> *) (abt :: [Hakaru] -> Hakaru -> *)
       (a :: Hakaru).
(Applicative f, ABT Term abt) =>
abt '[] a -> ListContext abt 'Impure -> f (P 'Impure abt '[] a)
c0 ListContext abt 'Impure
h0
    where
    i0 :: Nat
i0      = f (Some2 abt) -> Nat
forall k2 (syn :: ([k2] -> k2 -> *) -> k2 -> *)
       (abt :: [k2] -> k2 -> *) (f :: * -> *).
(ABT syn abt, Foldable f) =>
f (Some2 abt) -> Nat
maxNextFree f (Some2 abt)
es -- TODO: is maxNextFreeOrBind better here?
    h0 :: ListContext abt 'Impure
h0      = Nat -> [Statement abt Location 'Impure] -> ListContext abt 'Impure
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity).
Nat -> [Statement abt Location p] -> ListContext abt p
ListContext Nat
i0 []
    -- TODO: we only use dirac because 'residualizeListContext'
    -- requires it to already be a measure; unfortunately this can
    -- result in an extraneous @(>>= \x -> dirac x)@ redex at the
    -- end of the program. In principle, we should be able to
    -- eliminate that redex by changing the type of
    -- 'residualizeListContext'...
    c0 :: abt '[] a -> ListContext abt 'Impure -> f (P 'Impure abt '[] a)
c0 abt '[] a
e ListContext abt 'Impure
ss =
        P 'Impure abt '[] a -> f (P 'Impure abt '[] a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        (P 'Impure abt '[] a -> f (P 'Impure abt '[] a))
-> (abt '[] ('HMeasure a) -> P 'Impure abt '[] a)
-> abt '[] ('HMeasure a)
-> f (P 'Impure abt '[] a)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ListContext abt 'Impure
-> P 'Impure abt '[] a -> P 'Impure abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity)
       (a :: Hakaru).
ABT Term abt =>
ListContext abt p -> P p abt '[] a -> P p abt '[] a
residualizeListContext ListContext abt 'Impure
ss
        (P 'Impure abt '[] a -> P 'Impure abt '[] a)
-> (abt '[] ('HMeasure a) -> P 'Impure abt '[] a)
-> abt '[] ('HMeasure a)
-> P 'Impure abt '[] a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. abt '[] ('HMeasure a) -> P 'Impure abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
abt xs ('HMeasure a) -> P 'Impure abt xs a
PImpure
        (abt '[] ('HMeasure a) -> f (P 'Impure abt '[] a))
-> abt '[] ('HMeasure a) -> f (P 'Impure abt '[] a)
forall a b. (a -> b) -> a -> b
$ 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] ('HMeasure a)
forall (a :: Hakaru). SCon '[LC a] ('HMeasure a)
Dirac SCon '[LC a] ('HMeasure a)
-> SArgs abt '[LC a] -> Term abt ('HMeasure a)
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)

runPureEval
    :: (ABT Term abt, Applicative m, F.Foldable f)
    => PEval abt 'Pure m (abt '[] a)
    -> f (Some2 abt)
    -> m (abt '[] a)
runPureEval :: PEval abt 'Pure m (abt '[] a) -> f (Some2 abt) -> m (abt '[] a)
runPureEval PEval abt 'Pure m (abt '[] a)
m f (Some2 abt)
es =
    P 'Pure abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
P 'Pure abt xs a -> abt xs a
unPPure (P 'Pure abt '[] a -> abt '[] a)
-> m (P 'Pure abt '[] a) -> m (abt '[] a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PEval abt 'Pure m (abt '[] a)
-> (abt '[] a -> PAns 'Pure abt m a) -> PAns 'Pure abt m a
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
PEval abt p m x
-> forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a
unPEval PEval abt 'Pure m (abt '[] a)
m abt '[] a -> PAns 'Pure abt m a
forall (f :: * -> *) (abt :: [Hakaru] -> Hakaru -> *)
       (a :: Hakaru).
(Applicative f, ABT Term abt) =>
abt '[] a -> ListContext abt 'Pure -> f (P 'Pure abt '[] a)
c0 ListContext abt 'Pure
h0
    where
    i0 :: Nat
i0      = f (Some2 abt) -> Nat
forall k2 (syn :: ([k2] -> k2 -> *) -> k2 -> *)
       (abt :: [k2] -> k2 -> *) (f :: * -> *).
(ABT syn abt, Foldable f) =>
f (Some2 abt) -> Nat
maxNextFree f (Some2 abt)
es -- TODO: is maxNextFreeOrBind better here?
    h0 :: ListContext abt 'Pure
h0      = Nat -> [Statement abt Location 'Pure] -> ListContext abt 'Pure
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity).
Nat -> [Statement abt Location p] -> ListContext abt p
ListContext Nat
i0 []
    c0 :: abt '[] a -> ListContext abt 'Pure -> f (P 'Pure abt '[] a)
c0 abt '[] a
e ListContext abt 'Pure
ss = P 'Pure abt '[] a -> f (P 'Pure abt '[] a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (P 'Pure abt '[] a -> f (P 'Pure abt '[] a))
-> (P 'Pure abt '[] a -> P 'Pure abt '[] a)
-> P 'Pure abt '[] a
-> f (P 'Pure abt '[] a)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ListContext abt 'Pure -> P 'Pure abt '[] a -> P 'Pure abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity)
       (a :: Hakaru).
ABT Term abt =>
ListContext abt p -> P p abt '[] a -> P p abt '[] a
residualizeListContext ListContext abt 'Pure
ss (P 'Pure abt '[] a -> f (P 'Pure abt '[] a))
-> P 'Pure abt '[] a -> f (P 'Pure abt '[] a)
forall a b. (a -> b) -> a -> b
$ abt '[] a -> P 'Pure abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
abt xs a -> P 'Pure abt xs a
PPure abt '[] a
e

runExpectEval
    :: (ABT Term abt, Applicative m, F.Foldable f)
    => PEval abt 'ExpectP m (abt '[] a)
    -> abt '[a] 'HProb
    -> f (Some2 abt)
    -> m (abt '[] 'HProb)
runExpectEval :: PEval abt 'ExpectP m (abt '[] a)
-> abt '[a] 'HProb -> f (Some2 abt) -> m (abt '[] 'HProb)
runExpectEval PEval abt 'ExpectP m (abt '[] a)
m abt '[a] 'HProb
f f (Some2 abt)
es =
    P 'ExpectP abt '[] Any -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
P 'ExpectP abt xs a -> abt xs 'HProb
unPExpect (P 'ExpectP abt '[] Any -> abt '[] 'HProb)
-> m (P 'ExpectP abt '[] Any) -> m (abt '[] 'HProb)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PEval abt 'ExpectP m (abt '[] a)
-> (abt '[] a -> PAns 'ExpectP abt m Any)
-> PAns 'ExpectP abt m Any
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
PEval abt p m x
-> forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a
unPEval PEval abt 'ExpectP m (abt '[] a)
m abt '[] a -> PAns 'ExpectP abt m Any
c0 ListContext abt 'ExpectP
h0
    where
    i0 :: Nat
i0      = abt '[a] 'HProb -> Nat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> Nat
nextFreeOrBind abt '[a] 'HProb
f Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
`max` f (Some2 abt) -> Nat
forall k2 (syn :: ([k2] -> k2 -> *) -> k2 -> *)
       (abt :: [k2] -> k2 -> *) (f :: * -> *).
(ABT syn abt, Foldable f) =>
f (Some2 abt) -> Nat
maxNextFreeOrBind f (Some2 abt)
es
    h0 :: ListContext abt 'ExpectP
h0      = Nat
-> [Statement abt Location 'ExpectP] -> ListContext abt 'ExpectP
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity).
Nat -> [Statement abt Location p] -> ListContext abt p
ListContext Nat
i0 []
    c0 :: abt '[] a -> PAns 'ExpectP abt m Any
c0 abt '[] a
e ListContext abt 'ExpectP
ss =
        P 'ExpectP abt '[] Any -> m (P 'ExpectP abt '[] Any)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        (P 'ExpectP abt '[] Any -> m (P 'ExpectP abt '[] Any))
-> (abt '[] 'HProb -> P 'ExpectP abt '[] Any)
-> abt '[] 'HProb
-> m (P 'ExpectP abt '[] Any)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ListContext abt 'ExpectP
-> P 'ExpectP abt '[] Any -> P 'ExpectP abt '[] Any
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity)
       (a :: Hakaru).
ABT Term abt =>
ListContext abt p -> P p abt '[] a -> P p abt '[] a
residualizeListContext ListContext abt 'ExpectP
ss
        (P 'ExpectP abt '[] Any -> P 'ExpectP abt '[] Any)
-> (abt '[] 'HProb -> P 'ExpectP abt '[] Any)
-> abt '[] 'HProb
-> P 'ExpectP abt '[] Any
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. abt '[] 'HProb -> P 'ExpectP abt '[] Any
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
abt xs 'HProb -> P 'ExpectP abt xs a
PExpect
        (abt '[] 'HProb -> m (P 'ExpectP abt '[] Any))
-> abt '[] 'HProb -> m (P 'ExpectP abt '[] Any)
forall a b. (a -> b) -> a -> b
$ abt '[] a
-> (Variable a -> abt '[] 'HProb)
-> (Term abt a -> abt '[] 'HProb)
-> abt '[] 'HProb
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 '[] a
e
            (\Variable a
x -> abt '[a] 'HProb
-> (Variable a -> abt '[] 'HProb -> abt '[] 'HProb)
-> abt '[] 'HProb
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 '[a] 'HProb
f ((Variable a -> abt '[] 'HProb -> abt '[] 'HProb)
 -> abt '[] 'HProb)
-> (Variable a -> abt '[] 'HProb -> abt '[] 'HProb)
-> abt '[] 'HProb
forall a b. (a -> b) -> a -> b
$ \Variable a
y abt '[] 'HProb
f' -> Variable a -> abt '[] a -> abt '[] 'HProb -> abt '[] 'HProb
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
(JmEq1 Sing, Show1 Sing, Traversable21 syn, ABT syn abt) =>
Variable a -> abt '[] a -> abt xs b -> abt xs b
subst Variable a
y (Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable a
x) abt '[] 'HProb
f')
            (\Term abt a
_ -> Term abt 'HProb -> abt '[] 'HProb
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (SCon '[LC a, '( '[a], 'HProb)] 'HProb
forall (a :: Hakaru) (b :: Hakaru). SCon '[LC a, '( '[a], b)] b
Let_ SCon '[LC a, '( '[a], 'HProb)] 'HProb
-> SArgs abt '[LC a, '( '[a], 'HProb)] -> Term abt 'HProb
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 '[ '( '[a], 'HProb)]
-> SArgs abt '[LC a, '( '[a], 'HProb)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* abt '[a] 'HProb
f abt '[a] 'HProb -> SArgs abt '[] -> SArgs abt '[ '( '[a], 'HProb)]
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))
        -- TODO: make this smarter still, to drop the let-binding entirely if it's not used in @f@.


instance Functor (PEval abt p m) where
    fmap :: (a -> b) -> PEval abt p m a -> PEval abt p m b
fmap a -> b
f PEval abt p m a
m = (forall (a :: Hakaru). (b -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m b
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
(forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m x
PEval ((forall (a :: Hakaru). (b -> PAns p abt m a) -> PAns p abt m a)
 -> PEval abt p m b)
-> (forall (a :: Hakaru). (b -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m b
forall a b. (a -> b) -> a -> b
$ \b -> PAns p abt m a
c -> PEval abt p m a -> (a -> PAns p abt m a) -> PAns p abt m a
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
PEval abt p m x
-> forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a
unPEval PEval abt p m a
m (b -> PAns p abt m a
c (b -> PAns p abt m a) -> (a -> b) -> a -> PAns p abt m a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> b
f)

instance Applicative (PEval abt p m) where
    pure :: a -> PEval abt p m a
pure a
x    = (forall (a :: Hakaru). (a -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m a
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
(forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m x
PEval ((forall (a :: Hakaru). (a -> PAns p abt m a) -> PAns p abt m a)
 -> PEval abt p m a)
-> (forall (a :: Hakaru). (a -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m a
forall a b. (a -> b) -> a -> b
$ \a -> PAns p abt m a
c -> a -> PAns p abt m a
c a
x
    PEval abt p m (a -> b)
mf <*> :: PEval abt p m (a -> b) -> PEval abt p m a -> PEval abt p m b
<*> PEval abt p m a
mx = (forall (a :: Hakaru). (b -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m b
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
(forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m x
PEval ((forall (a :: Hakaru). (b -> PAns p abt m a) -> PAns p abt m a)
 -> PEval abt p m b)
-> (forall (a :: Hakaru). (b -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m b
forall a b. (a -> b) -> a -> b
$ \b -> PAns p abt m a
c -> PEval abt p m (a -> b)
-> forall (a :: Hakaru).
   ((a -> b) -> PAns p abt m a) -> PAns p abt m a
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
PEval abt p m x
-> forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a
unPEval PEval abt p m (a -> b)
mf (((a -> b) -> PAns p abt m a) -> PAns p abt m a)
-> ((a -> b) -> PAns p abt m a) -> PAns p abt m a
forall a b. (a -> b) -> a -> b
$ \a -> b
f -> PEval abt p m a
-> forall (a :: Hakaru). (a -> PAns p abt m a) -> PAns p abt m a
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
PEval abt p m x
-> forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a
unPEval PEval abt p m a
mx ((a -> PAns p abt m a) -> PAns p abt m a)
-> (a -> PAns p abt m a) -> PAns p abt m a
forall a b. (a -> b) -> a -> b
$ \a
x -> b -> PAns p abt m a
c (a -> b
f a
x)

instance Monad (PEval abt p m) where
    return :: a -> PEval abt p m a
return   = a -> PEval abt p m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    PEval abt p m a
mx >>= :: PEval abt p m a -> (a -> PEval abt p m b) -> PEval abt p m b
>>= a -> PEval abt p m b
k = (forall (a :: Hakaru). (b -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m b
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
(forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m x
PEval ((forall (a :: Hakaru). (b -> PAns p abt m a) -> PAns p abt m a)
 -> PEval abt p m b)
-> (forall (a :: Hakaru). (b -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m b
forall a b. (a -> b) -> a -> b
$ \b -> PAns p abt m a
c -> PEval abt p m a
-> forall (a :: Hakaru). (a -> PAns p abt m a) -> PAns p abt m a
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
PEval abt p m x
-> forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a
unPEval PEval abt p m a
mx ((a -> PAns p abt m a) -> PAns p abt m a)
-> (a -> PAns p abt m a) -> PAns p abt m a
forall a b. (a -> b) -> a -> b
$ \a
x -> PEval abt p m b -> (b -> PAns p abt m a) -> PAns p abt m a
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
PEval abt p m x
-> forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a
unPEval (a -> PEval abt p m b
k a
x) b -> PAns p abt m a
c

instance Alternative m => Alternative (PEval abt p m) where
    empty :: PEval abt p m a
empty   = (forall (a :: Hakaru). (a -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m a
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
(forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m x
PEval ((forall (a :: Hakaru). (a -> PAns p abt m a) -> PAns p abt m a)
 -> PEval abt p m a)
-> (forall (a :: Hakaru). (a -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m a
forall a b. (a -> b) -> a -> b
$ \a -> PAns p abt m a
_ ListContext abt p
_ -> m (P p abt '[] a)
forall (f :: * -> *) a. Alternative f => f a
empty
    PEval abt p m a
m <|> :: PEval abt p m a -> PEval abt p m a -> PEval abt p m a
<|> PEval abt p m a
n = (forall (a :: Hakaru). (a -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m a
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
(forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m x
PEval ((forall (a :: Hakaru). (a -> PAns p abt m a) -> PAns p abt m a)
 -> PEval abt p m a)
-> (forall (a :: Hakaru). (a -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m a
forall a b. (a -> b) -> a -> b
$ \a -> PAns p abt m a
c ListContext abt p
h -> PEval abt p m a -> (a -> PAns p abt m a) -> PAns p abt m a
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
PEval abt p m x
-> forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a
unPEval PEval abt p m a
m a -> PAns p abt m a
c ListContext abt p
h m (P p abt '[] a) -> m (P p abt '[] a) -> m (P p abt '[] a)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> PEval abt p m a -> (a -> PAns p abt m a) -> PAns p abt m a
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
PEval abt p m x
-> forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a
unPEval PEval abt p m a
n a -> PAns p abt m a
c ListContext abt p
h

instance Alternative m => MonadPlus (PEval abt p m) where
    mzero :: PEval abt p m a
mzero = PEval abt p m a
forall (f :: * -> *) a. Alternative f => f a
empty -- aka "bot"
    mplus :: PEval abt p m a -> PEval abt p m a -> PEval abt p m a
mplus = PEval abt p m a -> PEval abt p m a -> PEval abt p m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) -- aka "lub"

instance (ABT Term abt) => EvaluationMonad abt (PEval abt p m) p where
    freshNat :: PEval abt p m Nat
freshNat =
        (forall (a :: Hakaru). (Nat -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m Nat
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
(forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m x
PEval ((forall (a :: Hakaru). (Nat -> PAns p abt m a) -> PAns p abt m a)
 -> PEval abt p m Nat)
-> (forall (a :: Hakaru).
    (Nat -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m Nat
forall a b. (a -> b) -> a -> b
$ \Nat -> PAns p abt m a
c (ListContext Nat
i [Statement abt Location p]
ss) ->
            Nat -> PAns p abt m a
c Nat
i (Nat -> [Statement abt Location p] -> ListContext abt p
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity).
Nat -> [Statement abt Location p] -> ListContext abt p
ListContext (Nat
iNat -> Nat -> Nat
forall a. Num a => a -> a -> a
+Nat
1) [Statement abt Location p]
ss)

    unsafePush :: Statement abt Location p -> PEval abt p m ()
unsafePush Statement abt Location p
s =
        (forall (a :: Hakaru). (() -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m ()
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
(forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m x
PEval ((forall (a :: Hakaru). (() -> PAns p abt m a) -> PAns p abt m a)
 -> PEval abt p m ())
-> (forall (a :: Hakaru). (() -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m ()
forall a b. (a -> b) -> a -> b
$ \() -> PAns p abt m a
c (ListContext Nat
i [Statement abt Location p]
ss) ->
            () -> PAns p abt m a
c () (Nat -> [Statement abt Location p] -> ListContext abt p
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity).
Nat -> [Statement abt Location p] -> ListContext abt p
ListContext Nat
i (Statement abt Location p
sStatement abt Location p
-> [Statement abt Location p] -> [Statement abt Location p]
forall a. a -> [a] -> [a]
:[Statement abt Location p]
ss))

    -- N.B., the use of 'reverse' is necessary so that the order
    -- of pushing matches that of 'pushes'
    unsafePushes :: [Statement abt Location p] -> PEval abt p m ()
unsafePushes [Statement abt Location p]
ss =
        (forall (a :: Hakaru). (() -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m ()
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
(forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m x
PEval ((forall (a :: Hakaru). (() -> PAns p abt m a) -> PAns p abt m a)
 -> PEval abt p m ())
-> (forall (a :: Hakaru). (() -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m ()
forall a b. (a -> b) -> a -> b
$ \() -> PAns p abt m a
c (ListContext Nat
i [Statement abt Location p]
ss') ->
            () -> PAns p abt m a
c () (Nat -> [Statement abt Location p] -> ListContext abt p
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity).
Nat -> [Statement abt Location p] -> ListContext abt p
ListContext Nat
i ([Statement abt Location p] -> [Statement abt Location p]
forall a. [a] -> [a]
reverse [Statement abt Location p]
ss [Statement abt Location p]
-> [Statement abt Location p] -> [Statement abt Location p]
forall a. [a] -> [a] -> [a]
++ [Statement abt Location p]
ss'))

    select :: Location a
-> (Statement abt Location p -> Maybe (PEval abt p m r))
-> PEval abt p m (Maybe r)
select Location a
x Statement abt Location p -> Maybe (PEval abt p m r)
p = [Statement abt Location p] -> PEval abt p m (Maybe r)
loop []
        where
        -- TODO: use a DList to avoid reversing inside 'unsafePushes'
        loop :: [Statement abt Location p] -> PEval abt p m (Maybe r)
loop [Statement abt Location p]
ss = do
            Maybe (Statement abt Location p)
ms <- PEval abt p m (Maybe (Statement abt Location p))
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity)
       (m :: * -> *).
PEval abt p m (Maybe (Statement abt Location p))
unsafePop
            case Maybe (Statement abt Location p)
ms of
                Maybe (Statement abt Location p)
Nothing -> do
                    [Statement abt Location p] -> PEval abt p m ()
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
       (p :: Purity).
EvaluationMonad abt m p =>
[Statement abt Location p] -> m ()
unsafePushes [Statement abt Location p]
ss
                    Maybe r -> PEval abt p m (Maybe r)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe r
forall a. Maybe a
Nothing
                Just Statement abt Location p
s  ->
                    -- Alas, @p@ will have to recheck 'isBoundBy'
                    -- in order to grab the 'Refl' proof we erased;
                    -- but there's nothing to be done for it.
                    case Location a
x Location a -> Statement abt Location p -> Maybe ()
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *)
       (p :: Purity).
Location a -> Statement abt Location p -> Maybe ()
`isBoundBy` Statement abt Location p
s Maybe () -> Maybe (PEval abt p m r) -> Maybe (PEval abt p m r)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Statement abt Location p -> Maybe (PEval abt p m r)
p Statement abt Location p
s of
                    Maybe (PEval abt p m r)
Nothing -> [Statement abt Location p] -> PEval abt p m (Maybe r)
loop (Statement abt Location p
sStatement abt Location p
-> [Statement abt Location p] -> [Statement abt Location p]
forall a. a -> [a] -> [a]
:[Statement abt Location p]
ss) -- BUG: we only want to loop if @x@ isn't bound by @s@; if it is bound but @p@ fails (e.g., because @s@ is 'Stuff1'), then we should fail/stop (thus the return type should be @2+r@ to distinguish no-match = free vs failed-match = bound-but-inalterable)
                    Just PEval abt p m r
mr -> do
                        r
r <- PEval abt p m r
mr
                        [Statement abt Location p] -> PEval abt p m ()
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
       (p :: Purity).
EvaluationMonad abt m p =>
[Statement abt Location p] -> m ()
unsafePushes [Statement abt Location p]
ss
                        Maybe r -> PEval abt p m (Maybe r)
forall (m :: * -> *) a. Monad m => a -> m a
return (r -> Maybe r
forall a. a -> Maybe a
Just r
r)

-- | Not exported because we only need it for defining 'select' on 'PEval'.
unsafePop :: PEval abt p m (Maybe (Statement abt Location p))
unsafePop :: PEval abt p m (Maybe (Statement abt Location p))
unsafePop =
    (forall (a :: Hakaru).
 (Maybe (Statement abt Location p) -> PAns p abt m a)
 -> PAns p abt m a)
-> PEval abt p m (Maybe (Statement abt Location p))
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
(forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m x
PEval ((forall (a :: Hakaru).
  (Maybe (Statement abt Location p) -> PAns p abt m a)
  -> PAns p abt m a)
 -> PEval abt p m (Maybe (Statement abt Location p)))
-> (forall (a :: Hakaru).
    (Maybe (Statement abt Location p) -> PAns p abt m a)
    -> PAns p abt m a)
-> PEval abt p m (Maybe (Statement abt Location p))
forall a b. (a -> b) -> a -> b
$ \Maybe (Statement abt Location p) -> PAns p abt m a
c h :: ListContext abt p
h@(ListContext Nat
i [Statement abt Location p]
ss) ->
        case [Statement abt Location p]
ss of
        []    -> Maybe (Statement abt Location p) -> PAns p abt m a
c Maybe (Statement abt Location p)
forall a. Maybe a
Nothing  ListContext abt p
h
        Statement abt Location p
s:[Statement abt Location p]
ss' -> Maybe (Statement abt Location p) -> PAns p abt m a
c (Statement abt Location p -> Maybe (Statement abt Location p)
forall a. a -> Maybe a
Just Statement abt Location p
s) (Nat -> [Statement abt Location p] -> ListContext abt p
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity).
Nat -> [Statement abt Location p] -> ListContext abt p
ListContext Nat
i [Statement abt Location p]
ss')

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

-- | It is impossible to satisfy the constraints, or at least we
-- give up on trying to do so. This function is identical to 'empty'
-- and 'mzero' for 'PEval'; we just give it its own name since this is
-- the name used in our papers.
--
-- TODO: add some sort of trace information so we can get a better
-- idea what caused a disintegration to fail.
bot :: (ABT Term abt, Alternative m) => PEval abt p m a
bot :: PEval abt p m a
bot = PEval abt p m a
forall (f :: * -> *) a. Alternative f => f a
empty


{-
-- BUG: no longer typechecks after splitting 'Reject_' out from 'Superpose_'
-- | The empty measure is a solution to the constraints.
reject :: (ABT Term abt) => PEval abt p m a
reject = PEval $ \_ _ -> return . P.reject $ SMeasure sing
-}


-- Something essentially like this function was called @insert_@
-- in the finally-tagless code.
--
-- | Emit some code that binds a variable, and return the variable
-- thus bound. The function says what to wrap the result of the
-- continuation with; i.e., what we're actually emitting.
emit
    :: (ABT Term abt, Functor m)
    => Text
    -> Sing a
    -> (forall r. P p abt '[a] r -> P p abt '[] r)
    -> PEval abt p m (Variable a)
emit :: Text
-> Sing a
-> (forall (r :: Hakaru). P p abt '[a] r -> P p abt '[] r)
-> PEval abt p m (Variable a)
emit Text
hint Sing a
typ forall (r :: Hakaru). P p abt '[a] r -> P p abt '[] r
f = do
    Variable a
x <- Text -> Sing a -> PEval abt p m (Variable a)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
       (a :: Hakaru).
EvaluationMonad abt m p =>
Text -> Sing a -> m (Variable a)
freshVar Text
hint Sing a
typ
    (forall (a :: Hakaru).
 (Variable a -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m (Variable a)
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
(forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m x
PEval ((forall (a :: Hakaru).
  (Variable a -> PAns p abt m a) -> PAns p abt m a)
 -> PEval abt p m (Variable a))
-> (forall (a :: Hakaru).
    (Variable a -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m (Variable a)
forall a b. (a -> b) -> a -> b
$ \Variable a -> PAns p abt m a
c ListContext abt p
h -> (P p abt '[a] a -> P p abt '[] a
forall (r :: Hakaru). P p abt '[a] r -> P p abt '[] r
f (P p abt '[a] a -> P p abt '[] a)
-> (P p abt '[] a -> P p abt '[a] a)
-> P p abt '[] a
-> P p abt '[] a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (forall (a :: Hakaru). abt '[] a -> abt '[a] a)
-> P p abt '[] a -> P p abt '[a] a
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (ys :: [Hakaru]) (p :: Purity) (b :: Hakaru).
(forall (a :: Hakaru). abt xs a -> abt ys a)
-> P p abt xs b -> P p abt ys b
mapP (Variable a -> abt '[] a -> abt '[a] 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)) (P p abt '[] a -> P p abt '[] a)
-> m (P p abt '[] a) -> m (P p abt '[] a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Variable a -> PAns p abt m a
c Variable a
x ListContext abt p
h


-- This function was called @lift@ in the finally-tagless code.
-- | Emit an 'MBind' (i.e., \"@m >>= \x ->@\") and return the
-- variable thus bound (i.e., @x@).
emitMBind
    :: (ABT Term abt, Functor m)
    => abt '[] ('HMeasure a)
    -> PEval abt 'Impure m (Variable a)
emitMBind :: abt '[] ('HMeasure a) -> PEval abt 'Impure m (Variable a)
emitMBind abt '[] ('HMeasure a)
m =
    Text
-> Sing a
-> (forall (r :: Hakaru).
    P 'Impure abt '[a] r -> P 'Impure abt '[] r)
-> PEval abt 'Impure m (Variable a)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (a :: Hakaru)
       (p :: Purity).
(ABT Term abt, Functor m) =>
Text
-> Sing a
-> (forall (r :: Hakaru). P p abt '[a] r -> P p abt '[] r)
-> PEval abt p m (Variable a)
emit Text
Text.empty (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 '[] ('HMeasure a) -> Sing ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] ('HMeasure a)
m) ((forall (r :: Hakaru).
  P 'Impure abt '[a] r -> P 'Impure abt '[] r)
 -> PEval abt 'Impure m (Variable a))
-> (forall (r :: Hakaru).
    P 'Impure abt '[a] r -> P 'Impure abt '[] r)
-> PEval abt 'Impure m (Variable a)
forall a b. (a -> b) -> a -> b
$ \(PImpure abt '[a] ('HMeasure r)
e) ->
        abt '[] ('HMeasure r) -> P 'Impure abt '[] r
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
abt xs ('HMeasure a) -> P 'Impure abt xs a
PImpure (abt '[] ('HMeasure r) -> P 'Impure abt '[] r)
-> abt '[] ('HMeasure r) -> P 'Impure abt '[] r
forall a b. (a -> b) -> a -> b
$ Term abt ('HMeasure r) -> abt '[] ('HMeasure r)
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 r)] ('HMeasure r)
forall (a :: Hakaru) (b :: Hakaru).
SCon '[LC ('HMeasure a), '( '[a], 'HMeasure b)] ('HMeasure b)
MBind SCon '[LC ('HMeasure a), '( '[a], 'HMeasure r)] ('HMeasure r)
-> SArgs abt '[LC ('HMeasure a), '( '[a], 'HMeasure r)]
-> Term abt ('HMeasure r)
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt '[] ('HMeasure a)
m abt '[] ('HMeasure a)
-> SArgs abt '[ '( '[a], 'HMeasure r)]
-> SArgs abt '[LC ('HMeasure a), '( '[a], 'HMeasure r)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* abt '[a] ('HMeasure r)
e abt '[a] ('HMeasure r)
-> SArgs abt '[] -> SArgs abt '[ '( '[a], 'HMeasure r)]
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)


-- | A smart constructor for emitting let-bindings. If the input
-- is already a variable then we just return it; otherwise we emit
-- the let-binding. N.B., this function provides the invariant that
-- the result is in fact a variable; whereas 'emitLet'' does not.
emitLet
    :: (ABT Term abt, Functor m) => abt '[] a -> PEval abt p m (Variable a)
emitLet :: abt '[] a -> PEval abt p m (Variable a)
emitLet abt '[] a
e =
    abt '[] a
-> (Variable a -> PEval abt p m (Variable a))
-> (Term abt a -> PEval abt p m (Variable a))
-> PEval abt p m (Variable 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 '[] a
e Variable a -> PEval abt p m (Variable a)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Term abt a -> PEval abt p m (Variable a))
 -> PEval abt p m (Variable a))
-> (Term abt a -> PEval abt p m (Variable a))
-> PEval abt p m (Variable a)
forall a b. (a -> b) -> a -> b
$ \Term abt a
_ ->
        -- N.B., must use the second @($)@ here because rank-2 polymorphism
        Text
-> Sing a
-> (forall (r :: Hakaru). P p abt '[a] r -> P p abt '[] r)
-> PEval abt p m (Variable a)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (a :: Hakaru)
       (p :: Purity).
(ABT Term abt, Functor m) =>
Text
-> Sing a
-> (forall (r :: Hakaru). P p abt '[a] r -> P p abt '[] r)
-> PEval abt p m (Variable a)
emit Text
Text.empty (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] a
e) ((forall (r :: Hakaru). P p abt '[a] r -> P p abt '[] r)
 -> PEval abt p m (Variable a))
-> (forall (r :: Hakaru). P p abt '[a] r -> P p abt '[] r)
-> PEval abt p m (Variable a)
forall a b. (a -> b) -> a -> b
$ (forall (a :: Hakaru). abt '[a] a -> abt '[] a)
-> P p abt '[a] r -> P p abt '[] r
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (ys :: [Hakaru]) (p :: Purity) (b :: Hakaru).
(forall (a :: Hakaru). abt xs a -> abt ys a)
-> P p abt xs b -> P p abt ys b
mapP ((forall (a :: Hakaru). abt '[a] a -> abt '[] a)
 -> P p abt '[a] r -> P p abt '[] r)
-> (forall (a :: Hakaru). abt '[a] a -> abt '[] a)
-> P p abt '[a] r
-> P p abt '[] r
forall a b. (a -> b) -> a -> b
$ \abt '[a] a
m ->
            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 (SCon '[LC a, '( '[a], a)] a
forall (a :: Hakaru) (b :: Hakaru). SCon '[LC a, '( '[a], b)] b
Let_ SCon '[LC a, '( '[a], a)] a
-> SArgs abt '[LC a, '( '[a], a)] -> Term abt a
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 '[ '( '[a], a)] -> SArgs abt '[LC a, '( '[a], a)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* abt '[a] a
m abt '[a] a -> SArgs abt '[] -> SArgs abt '[ '( '[a], 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)

-- | A smart constructor for emitting let-bindings. If the input
-- is already a variable or a literal constant, then we just return
-- it; otherwise we emit the let-binding. N.B., this function
-- provides weaker guarantees on the type of the result; if you
-- require the result to always be a variable, then see 'emitLet'
-- instead.
emitLet'
    :: (ABT Term abt, Functor m) => abt '[] a -> PEval abt p m (abt '[] a)
emitLet' :: abt '[] a -> PEval abt p m (abt '[] a)
emitLet' abt '[] a
e =
    abt '[] a
-> (Variable a -> PEval abt p m (abt '[] a))
-> (Term abt a -> PEval abt p m (abt '[] a))
-> PEval abt p m (abt '[] 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 '[] a
e (PEval abt p m (abt '[] a)
-> Variable a -> PEval abt p m (abt '[] a)
forall a b. a -> b -> a
const (PEval abt p m (abt '[] a)
 -> Variable a -> PEval abt p m (abt '[] a))
-> PEval abt p m (abt '[] a)
-> Variable a
-> PEval abt p m (abt '[] a)
forall a b. (a -> b) -> a -> b
$ abt '[] a -> PEval abt p m (abt '[] a)
forall (m :: * -> *) a. Monad m => a -> m a
return abt '[] a
e) ((Term abt a -> PEval abt p m (abt '[] a))
 -> PEval abt p m (abt '[] a))
-> (Term abt a -> PEval abt p m (abt '[] a))
-> PEval abt p m (abt '[] a)
forall a b. (a -> b) -> a -> b
$ \Term abt a
t ->
        case Term abt a
t of
        Literal_ Literal a
_ -> abt '[] a -> PEval abt p m (abt '[] a)
forall (m :: * -> *) a. Monad m => a -> m a
return abt '[] a
e
        Term abt a
_ -> do
            -- N.B., must use the second @($)@ here because rank-2 polymorphism
            Variable a
x <- Text
-> Sing a
-> (forall (r :: Hakaru). P p abt '[a] r -> P p abt '[] r)
-> PEval abt p m (Variable a)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (a :: Hakaru)
       (p :: Purity).
(ABT Term abt, Functor m) =>
Text
-> Sing a
-> (forall (r :: Hakaru). P p abt '[a] r -> P p abt '[] r)
-> PEval abt p m (Variable a)
emit Text
Text.empty (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] a
e) ((forall (r :: Hakaru). P p abt '[a] r -> P p abt '[] r)
 -> PEval abt p m (Variable a))
-> (forall (r :: Hakaru). P p abt '[a] r -> P p abt '[] r)
-> PEval abt p m (Variable a)
forall a b. (a -> b) -> a -> b
$ (forall (a :: Hakaru). abt '[a] a -> abt '[] a)
-> P p abt '[a] r -> P p abt '[] r
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (ys :: [Hakaru]) (p :: Purity) (b :: Hakaru).
(forall (a :: Hakaru). abt xs a -> abt ys a)
-> P p abt xs b -> P p abt ys b
mapP ((forall (a :: Hakaru). abt '[a] a -> abt '[] a)
 -> P p abt '[a] r -> P p abt '[] r)
-> (forall (a :: Hakaru). abt '[a] a -> abt '[] a)
-> P p abt '[a] r
-> P p abt '[] r
forall a b. (a -> b) -> a -> b
$ \abt '[a] a
m ->
                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 (SCon '[LC a, '( '[a], a)] a
forall (a :: Hakaru) (b :: Hakaru). SCon '[LC a, '( '[a], b)] b
Let_ SCon '[LC a, '( '[a], a)] a
-> SArgs abt '[LC a, '( '[a], a)] -> Term abt a
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 '[ '( '[a], a)] -> SArgs abt '[LC a, '( '[a], a)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* abt '[a] a
m abt '[a] a -> SArgs abt '[] -> SArgs abt '[ '( '[a], 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)
            abt '[] a -> PEval abt p m (abt '[] a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable a
x)

-- | A smart constructor for emitting \"unpair\". If the input
-- argument is actually a constructor then we project out the two
-- components; otherwise we emit the case-binding and return the
-- two variables.
emitUnpair
    :: (ABT Term abt, Applicative m)
    => Whnf abt (HPair a b)
    -> PEval abt p m (abt '[] a, abt '[] b)
emitUnpair :: Whnf abt (HPair a b) -> PEval abt p m (abt '[] a, abt '[] b)
emitUnpair (Head_   Head abt (HPair a b)
w) = (abt '[] a, abt '[] b) -> PEval abt p m (abt '[] a, abt '[] b)
forall (m :: * -> *) a. Monad m => a -> m a
return ((abt '[] a, abt '[] b) -> PEval abt p m (abt '[] a, abt '[] b))
-> (abt '[] a, abt '[] b) -> PEval abt p m (abt '[] a, abt '[] b)
forall a b. (a -> b) -> a -> b
$ Head abt (HPair a b) -> (abt '[] a, abt '[] b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Head abt (HPair a b) -> (abt '[] a, abt '[] b)
reifyPair Head abt (HPair a b)
w
emitUnpair (Neutral abt '[] (HPair a b)
e) = do
    let (Sing a
a,Sing b
b) = Sing (HPair a b) -> (Sing a, Sing b)
forall (a :: Hakaru) (b :: Hakaru).
Sing (HPair a b) -> (Sing a, Sing b)
sUnPair (abt '[] (HPair a b) -> Sing (HPair a b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] (HPair a b)
e)
    Variable a
x <- Text -> Sing a -> PEval abt p m (Variable a)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
       (a :: Hakaru).
EvaluationMonad abt m p =>
Text -> Sing a -> m (Variable a)
freshVar Text
Text.empty Sing a
a
    Variable b
y <- Text -> Sing b -> PEval abt p m (Variable b)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
       (a :: Hakaru).
EvaluationMonad abt m p =>
Text -> Sing a -> m (Variable a)
freshVar Text
Text.empty Sing b
b
    Variable a
-> Variable b
-> abt '[] (HPair a b)
-> PEval abt p m (abt '[] a, abt '[] b)
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       (a :: Hakaru) (b :: Hakaru).
(ABT Term abt, Applicative m) =>
Variable a
-> Variable b
-> abt '[] (HPair a b)
-> PEval abt p m (abt '[] a, abt '[] b)
emitUnpair_ Variable a
x Variable b
y abt '[] (HPair a b)
e

emitUnpair_
    :: forall abt p m a b
    .  (ABT Term abt, Applicative m)
    => Variable a
    -> Variable b
    -> abt '[] (HPair a b)
    -> PEval abt p m (abt '[] a, abt '[] b)
emitUnpair_ :: Variable a
-> Variable b
-> abt '[] (HPair a b)
-> PEval abt p m (abt '[] a, abt '[] b)
emitUnpair_ Variable a
x Variable b
y = abt '[] (HPair a b) -> PEval abt p m (abt '[] a, abt '[] b)
loop
    where
    done :: abt '[] (HPair a b) -> PEval abt p m (abt '[] a, abt '[] b)
    done :: abt '[] (HPair a b) -> PEval abt p m (abt '[] a, abt '[] b)
done abt '[] (HPair a b)
e =
#ifdef __TRACE_DISINTEGRATE__
        trace "-- emitUnpair: done (term is not Datum_ nor Case_)" $
#endif
        (forall (a :: Hakaru).
 ((abt '[] a, abt '[] b) -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m (abt '[] a, abt '[] b)
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
(forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m x
PEval ((forall (a :: Hakaru).
  ((abt '[] a, abt '[] b) -> PAns p abt m a) -> PAns p abt m a)
 -> PEval abt p m (abt '[] a, abt '[] b))
-> (forall (a :: Hakaru).
    ((abt '[] a, abt '[] b) -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m (abt '[] a, abt '[] b)
forall a b. (a -> b) -> a -> b
$ \(abt '[] a, abt '[] b) -> PAns p abt m a
c ListContext abt p
h ->
            (forall (a :: Hakaru). abt '[] a -> abt '[] a)
-> P p abt '[] a -> P p abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (ys :: [Hakaru]) (p :: Purity) (b :: Hakaru).
(forall (a :: Hakaru). abt xs a -> abt ys a)
-> P p abt xs b -> P p abt ys b
mapP ( 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 -> abt '[] a)
-> (abt '[] a -> Term abt a) -> abt '[] a -> abt '[] a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. abt '[] (HPair a b) -> [Branch (HPair a b) abt a] -> Term abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
abt '[] a -> [Branch a abt b] -> Term abt b
Case_ abt '[] (HPair a b)
e
            ([Branch (HPair a b) abt a] -> Term abt a)
-> (abt '[] a -> [Branch (HPair a b) abt a])
-> abt '[] a
-> Term abt a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Branch (HPair a b) abt a
-> [Branch (HPair a b) abt a] -> [Branch (HPair a b) abt a]
forall a. a -> [a] -> [a]
:[])
            (Branch (HPair a b) abt a -> [Branch (HPair a b) abt a])
-> (abt '[] a -> Branch (HPair a b) abt a)
-> abt '[] a
-> [Branch (HPair a b) abt a]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Pattern '[a, b] (HPair a b)
-> abt '[a, b] a -> Branch (HPair a b) abt a
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *) (b :: Hakaru)
       (xs :: [Hakaru]).
Pattern xs a -> abt xs b -> Branch a abt b
Branch (Pattern '[a] a
-> Pattern '[b] b -> Pattern ('[a] ++ '[b]) (HPair a b)
forall (vars1 :: [Hakaru]) (a :: Hakaru) (vars2 :: [Hakaru])
       (b :: Hakaru).
Pattern vars1 a
-> Pattern vars2 b -> Pattern (vars1 ++ vars2) (HPair a b)
pPair Pattern '[a] a
forall (a :: Hakaru). Pattern '[a] a
PVar Pattern '[b] b
forall (a :: Hakaru). Pattern '[a] a
PVar)
            (abt '[a, b] a -> Branch (HPair a b) abt a)
-> (abt '[] a -> abt '[a, b] a)
-> abt '[] a
-> Branch (HPair a b) abt a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Variable a -> abt '[b] a -> abt '[a, b] 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 '[b] a -> abt '[a, b] a)
-> (abt '[] a -> abt '[b] a) -> abt '[] a -> abt '[a, b] a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Variable b -> abt '[] a -> abt '[b] 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 b
y
            ) (P p abt '[] a -> P p abt '[] a)
-> m (P p abt '[] a) -> m (P p abt '[] a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (abt '[] a, abt '[] b) -> PAns p abt m a
c (Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable a
x, Variable b -> abt '[] b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable b
y) ListContext abt p
h

    loop :: abt '[] (HPair a b) -> PEval abt p m (abt '[] a, abt '[] b)
    loop :: abt '[] (HPair a b) -> PEval abt p m (abt '[] a, abt '[] b)
loop abt '[] (HPair a b)
e0 =
        abt '[] (HPair a b)
-> (Variable (HPair a b) -> PEval abt p m (abt '[] a, abt '[] b))
-> (Term abt (HPair a b) -> PEval abt p m (abt '[] a, abt '[] b))
-> PEval abt p m (abt '[] a, abt '[] b)
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 '[] (HPair a b)
e0 (abt '[] (HPair a b) -> PEval abt p m (abt '[] a, abt '[] b)
done (abt '[] (HPair a b) -> PEval abt p m (abt '[] a, abt '[] b))
-> (Variable (HPair a b) -> abt '[] (HPair a b))
-> Variable (HPair a b)
-> PEval abt p m (abt '[] a, abt '[] b)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Variable (HPair a b) -> abt '[] (HPair a b)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var) ((Term abt (HPair a b) -> PEval abt p m (abt '[] a, abt '[] b))
 -> PEval abt p m (abt '[] a, abt '[] b))
-> (Term abt (HPair a b) -> PEval abt p m (abt '[] a, abt '[] b))
-> PEval abt p m (abt '[] a, abt '[] b)
forall a b. (a -> b) -> a -> b
$ \Term abt (HPair a b)
t ->
            case Term abt (HPair a b)
t of
            Datum_ Datum (abt '[]) (HData' t)
d   -> do
#ifdef __TRACE_DISINTEGRATE__
                trace "-- emitUnpair: found Datum_" $ return ()
#endif
                (abt '[] a, abt '[] b) -> PEval abt p m (abt '[] a, abt '[] b)
forall (m :: * -> *) a. Monad m => a -> m a
return ((abt '[] a, abt '[] b) -> PEval abt p m (abt '[] a, abt '[] b))
-> (abt '[] a, abt '[] b) -> PEval abt p m (abt '[] a, abt '[] b)
forall a b. (a -> b) -> a -> b
$ Head abt (HPair a b) -> (abt '[] a, abt '[] b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Head abt (HPair a b) -> (abt '[] a, abt '[] b)
reifyPair (Datum (abt '[]) (HData' t) -> Head abt (HData' t)
forall (abt :: [Hakaru] -> Hakaru -> *) (t :: HakaruCon).
Datum (abt '[]) (HData' t) -> Head abt (HData' t)
WDatum Datum (abt '[]) (HData' t)
d)
            Case_ abt '[] a
e [Branch a abt (HPair a b)]
bs -> do
#ifdef __TRACE_DISINTEGRATE__
                trace "-- emitUnpair: going under Case_" $ return ()
#endif
                -- TODO: we want this to duplicate the current
                -- continuation for (the evaluation of @loop@ in)
                -- all branches. So far our traces all end up
                -- returning @bot@ on the first branch, and hence
                -- @bot@ for the whole case-expression, so we can't
                -- quite tell whether it does what is intended.
                --
                -- N.B., the only 'PEval'-effects in 'applyBranch'
                -- are to freshen variables; thus this use of
                -- 'traverse' is perfectly sound.
                (abt '[] (HPair a b) -> PEval abt p m (abt '[] a, abt '[] b))
-> abt '[] a
-> [Branch a abt (HPair a b)]
-> PEval abt p m (abt '[] a, abt '[] b)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (b :: Hakaru)
       (p :: Purity) r (a :: Hakaru).
(ABT Term abt, Applicative m) =>
(abt '[] b -> PEval abt p m r)
-> abt '[] a -> [Branch a abt b] -> PEval abt p m r
emitCaseWith abt '[] (HPair a b) -> PEval abt p m (abt '[] a, abt '[] b)
loop abt '[] a
e [Branch a abt (HPair a b)]
bs
            Term abt (HPair a b)
_ -> abt '[] (HPair a b) -> PEval abt p m (abt '[] a, abt '[] b)
done abt '[] (HPair a b)
e0


-- TODO: emitUneither


-- This function was called @insert_@ in the old finally-tagless code.
-- | Emit some code that doesn't bind any variables. This function
-- provides an optimisation over using 'emit' and then discarding
-- the generated variable.
emit_
    :: (ABT Term abt, Functor m)
    => (forall r. P p abt '[] r -> P p abt '[] r)
    -> PEval abt p m ()
emit_ :: (forall (r :: Hakaru). P p abt '[] r -> P p abt '[] r)
-> PEval abt p m ()
emit_ forall (r :: Hakaru). P p abt '[] r -> P p abt '[] r
f = (forall (a :: Hakaru). (() -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m ()
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
(forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m x
PEval ((forall (a :: Hakaru). (() -> PAns p abt m a) -> PAns p abt m a)
 -> PEval abt p m ())
-> (forall (a :: Hakaru). (() -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m ()
forall a b. (a -> b) -> a -> b
$ \() -> PAns p abt m a
c ListContext abt p
h -> P p abt '[] a -> P p abt '[] a
forall (r :: Hakaru). P p abt '[] r -> P p abt '[] r
f (P p abt '[] a -> P p abt '[] a)
-> m (P p abt '[] a) -> m (P p abt '[] a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> () -> PAns p abt m a
c () ListContext abt p
h


-- | Emit an 'MBind' that discards its result (i.e., \"@m >>@\").
-- We restrict the type of the argument to be 'HUnit' so as to avoid
-- accidentally dropping things.
emitMBind_
    :: (ABT Term abt, Functor m)
    => abt '[] ('HMeasure HUnit)
    -> PEval abt 'Impure m ()
emitMBind_ :: abt '[] ('HMeasure HUnit) -> PEval abt 'Impure m ()
emitMBind_ abt '[] ('HMeasure HUnit)
m = (forall (r :: Hakaru). P 'Impure abt '[] r -> P 'Impure abt '[] r)
-> PEval abt 'Impure m ()
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
       (p :: Purity).
(ABT Term abt, Functor m) =>
(forall (r :: Hakaru). P p abt '[] r -> P p abt '[] r)
-> PEval abt p m ()
emit_ ((forall (r :: Hakaru). P 'Impure abt '[] r -> P 'Impure abt '[] r)
 -> PEval abt 'Impure m ())
-> (forall (r :: Hakaru).
    P 'Impure abt '[] r -> P 'Impure abt '[] r)
-> PEval abt 'Impure m ()
forall a b. (a -> b) -> a -> b
$ (abt '[] ('HMeasure r) -> abt '[] ('HMeasure r))
-> P 'Impure abt '[] r -> P 'Impure abt '[] r
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru) (ys :: [Hakaru]) (b :: Hakaru).
(abt xs ('HMeasure a) -> abt ys ('HMeasure b))
-> P 'Impure abt xs a -> P 'Impure abt ys b
mapPImpure (abt '[] ('HMeasure HUnit)
m abt '[] ('HMeasure HUnit)
-> abt '[] ('HMeasure r) -> abt '[] ('HMeasure r)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
(ABT Term abt, SingI a) =>
abt '[] ('HMeasure a)
-> abt '[] ('HMeasure b) -> abt '[] ('HMeasure b)
P.>>)


-- TODO: if the argument is a value, then we can evaluate the 'P.if_' immediately rather than emitting it.
-- | Emit an assertion that the condition is true.
emitGuard
    :: (ABT Term abt, Functor m)
    => abt '[] HBool
    -> PEval abt 'Impure m ()
emitGuard :: abt '[] HBool -> PEval abt 'Impure m ()
emitGuard abt '[] HBool
b = (forall (r :: Hakaru). P 'Impure abt '[] r -> P 'Impure abt '[] r)
-> PEval abt 'Impure m ()
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
       (p :: Purity).
(ABT Term abt, Functor m) =>
(forall (r :: Hakaru). P p abt '[] r -> P p abt '[] r)
-> PEval abt p m ()
emit_ ((forall (r :: Hakaru). P 'Impure abt '[] r -> P 'Impure abt '[] r)
 -> PEval abt 'Impure m ())
-> (forall (r :: Hakaru).
    P 'Impure abt '[] r -> P 'Impure abt '[] r)
-> PEval abt 'Impure m ()
forall a b. (a -> b) -> a -> b
$ (abt '[] ('HMeasure r) -> abt '[] ('HMeasure r))
-> P 'Impure abt '[] r -> P 'Impure abt '[] r
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru) (ys :: [Hakaru]) (b :: Hakaru).
(abt xs ('HMeasure a) -> abt ys ('HMeasure b))
-> P 'Impure abt xs a -> P 'Impure abt ys b
mapPImpure (abt '[] HBool -> abt '[] ('HMeasure r) -> abt '[] ('HMeasure r)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] HBool -> abt '[] ('HMeasure a) -> abt '[] ('HMeasure a)
P.withGuard abt '[] HBool
b)
    -- == emit_ $ \m -> P.if_ b m P.reject

-- TODO: if the argument is the literal 1, then we can avoid emitting anything.
emitWeight
    :: (ABT Term abt, Functor m)
    => abt '[] 'HProb
    -> PEval abt 'Impure m ()
emitWeight :: abt '[] 'HProb -> PEval abt 'Impure m ()
emitWeight abt '[] 'HProb
w = (forall (r :: Hakaru). P 'Impure abt '[] r -> P 'Impure abt '[] r)
-> PEval abt 'Impure m ()
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
       (p :: Purity).
(ABT Term abt, Functor m) =>
(forall (r :: Hakaru). P p abt '[] r -> P p abt '[] r)
-> PEval abt p m ()
emit_ ((forall (r :: Hakaru). P 'Impure abt '[] r -> P 'Impure abt '[] r)
 -> PEval abt 'Impure m ())
-> (forall (r :: Hakaru).
    P 'Impure abt '[] r -> P 'Impure abt '[] r)
-> PEval abt 'Impure m ()
forall a b. (a -> b) -> a -> b
$ (abt '[] ('HMeasure r) -> abt '[] ('HMeasure r))
-> P 'Impure abt '[] r -> P 'Impure abt '[] r
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru) (ys :: [Hakaru]) (b :: Hakaru).
(abt xs ('HMeasure a) -> abt ys ('HMeasure b))
-> P 'Impure abt xs a -> P 'Impure abt ys b
mapPImpure (abt '[] 'HProb -> abt '[] ('HMeasure r) -> abt '[] ('HMeasure r)
forall (abt :: [Hakaru] -> Hakaru -> *) (w :: Hakaru).
ABT Term abt =>
abt '[] 'HProb -> abt '[] ('HMeasure w) -> abt '[] ('HMeasure w)
P.withWeight abt '[] 'HProb
w)


-- N.B., this use of 'T.traverse' is definitely correct. It's
-- sequentializing @t [abt '[] ('HMeasure a)]@ into @[t (abt '[]
-- ('HMeasure a))]@ by chosing one of the possibilities at each
-- position in @t@. No heap\/context effects can escape to mess
-- things up. In contrast, using 'T.traverse' to sequentialize @t
-- (PEval abt a)@ as @PEval abt (t a)@ is /wrong/! Doing that would give
-- the conjunctive semantics where we have effects from one position
-- in @t@ escape to affect the other positions. This has to do with
-- the general issue in partial evaluation where we need to duplicate
-- downstream work (as we do by passing the same heap to everyone)
-- because there's no general way to combing the resulting heaps
-- for each branch.
--
-- | Run each of the elements of the traversable using the same
-- heap and continuation for each one, then pass the results to a
-- function for emitting code.
emitFork_
    :: (ABT Term abt, Applicative m, T.Traversable t)
    => (forall r. t (P p abt '[] r) -> P p abt '[] r)
    -> t (PEval abt p m a)
    -> PEval abt p m a
emitFork_ :: (forall (r :: Hakaru). t (P p abt '[] r) -> P p abt '[] r)
-> t (PEval abt p m a) -> PEval abt p m a
emitFork_ forall (r :: Hakaru). t (P p abt '[] r) -> P p abt '[] r
f t (PEval abt p m a)
ms =
    (forall (a :: Hakaru). (a -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m a
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
(forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m x
PEval ((forall (a :: Hakaru). (a -> PAns p abt m a) -> PAns p abt m a)
 -> PEval abt p m a)
-> (forall (a :: Hakaru). (a -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m a
forall a b. (a -> b) -> a -> b
$ \a -> PAns p abt m a
c ListContext abt p
h -> t (P p abt '[] a) -> P p abt '[] a
forall (r :: Hakaru). t (P p abt '[] r) -> P p abt '[] r
f (t (P p abt '[] a) -> P p abt '[] a)
-> m (t (P p abt '[] a)) -> m (P p abt '[] a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PEval abt p m a -> m (P p abt '[] a))
-> t (PEval abt p m a) -> m (t (P p abt '[] a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
T.traverse (\PEval abt p m a
m -> PEval abt p m a -> (a -> PAns p abt m a) -> PAns p abt m a
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
PEval abt p m x
-> forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a
unPEval PEval abt p m a
m a -> PAns p abt m a
c ListContext abt p
h) t (PEval abt p m a)
ms


-- | Emit a 'Superpose_' of the alternatives, each with unit weight.
emitSuperpose
    :: (ABT Term abt, Functor m)
    => [abt '[] ('HMeasure a)]
    -> PEval abt 'Impure m (Variable a)
emitSuperpose :: [abt '[] ('HMeasure a)] -> PEval abt 'Impure m (Variable a)
emitSuperpose []  = [Char] -> PEval abt 'Impure m (Variable a)
forall a. HasCallStack => [Char] -> a
error [Char]
"BUG: emitSuperpose: can't use Prelude.superpose because it'll throw an error"
emitSuperpose [abt '[] ('HMeasure a)
e] = abt '[] ('HMeasure a) -> PEval abt 'Impure m (Variable a)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
       (a :: Hakaru).
(ABT Term abt, Functor m) =>
abt '[] ('HMeasure a) -> PEval abt 'Impure m (Variable a)
emitMBind abt '[] ('HMeasure a)
e
emitSuperpose [abt '[] ('HMeasure a)]
es  =
    abt '[] ('HMeasure a) -> PEval abt 'Impure m (Variable a)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
       (a :: Hakaru).
(ABT Term abt, Functor m) =>
abt '[] ('HMeasure a) -> PEval abt 'Impure m (Variable a)
emitMBind (abt '[] ('HMeasure a) -> PEval abt 'Impure m (Variable a))
-> (NonEmpty (abt '[] ('HMeasure a)) -> abt '[] ('HMeasure a))
-> NonEmpty (abt '[] ('HMeasure a))
-> PEval abt 'Impure m (Variable a)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
P.superpose (NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
 -> abt '[] ('HMeasure a))
-> (NonEmpty (abt '[] ('HMeasure a))
    -> NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a)))
-> NonEmpty (abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (abt '[] ('HMeasure a) -> (abt '[] 'HProb, abt '[] ('HMeasure a)))
-> NonEmpty (abt '[] ('HMeasure a))
-> NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((,) abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HSemiring_ a) =>
abt '[] a
P.one) (NonEmpty (abt '[] ('HMeasure a))
 -> PEval abt 'Impure m (Variable a))
-> NonEmpty (abt '[] ('HMeasure a))
-> PEval abt 'Impure m (Variable a)
forall a b. (a -> b) -> a -> b
$ [abt '[] ('HMeasure a)] -> NonEmpty (abt '[] ('HMeasure a))
forall a. [a] -> NonEmpty a
NE.fromList [abt '[] ('HMeasure a)]
es


-- | Emit a 'Superpose_' of the alternatives, each with unit weight.
choose
    :: (ABT Term abt, Applicative m)
    => [PEval abt 'Impure m a]
    -> PEval abt 'Impure m a
choose :: [PEval abt 'Impure m a] -> PEval abt 'Impure m a
choose []  = [Char] -> PEval abt 'Impure m a
forall a. HasCallStack => [Char] -> a
error [Char]
"BUG: choose: can't use Prelude.superpose because it'll throw an error"
choose [PEval abt 'Impure m a
m] = PEval abt 'Impure m a
m
choose [PEval abt 'Impure m a]
ms  =
    (forall (r :: Hakaru).
 [P 'Impure abt '[] r] -> P 'Impure abt '[] r)
-> [PEval abt 'Impure m a] -> PEval abt 'Impure m a
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (t :: * -> *)
       (p :: Purity) a.
(ABT Term abt, Applicative m, Traversable t) =>
(forall (r :: Hakaru). t (P p abt '[] r) -> P p abt '[] r)
-> t (PEval abt p m a) -> PEval abt p m a
emitFork_
        (abt '[] ('HMeasure r) -> P 'Impure abt '[] r
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
abt xs ('HMeasure a) -> P 'Impure abt xs a
PImpure (abt '[] ('HMeasure r) -> P 'Impure abt '[] r)
-> ([P 'Impure abt '[] r] -> abt '[] ('HMeasure r))
-> [P 'Impure abt '[] r]
-> P 'Impure abt '[] r
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure r))
-> abt '[] ('HMeasure r)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
P.superpose (NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure r))
 -> abt '[] ('HMeasure r))
-> ([P 'Impure abt '[] r]
    -> NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure r)))
-> [P 'Impure abt '[] r]
-> abt '[] ('HMeasure r)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (P 'Impure abt '[] r -> (abt '[] 'HProb, abt '[] ('HMeasure r)))
-> NonEmpty (P 'Impure abt '[] r)
-> NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure r))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((,) abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HSemiring_ a) =>
abt '[] a
P.one (abt '[] ('HMeasure r) -> (abt '[] 'HProb, abt '[] ('HMeasure r)))
-> (P 'Impure abt '[] r -> abt '[] ('HMeasure r))
-> P 'Impure abt '[] r
-> (abt '[] 'HProb, abt '[] ('HMeasure r))
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. P 'Impure abt '[] r -> abt '[] ('HMeasure r)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
P 'Impure abt xs a -> abt xs ('HMeasure a)
unPImpure) (NonEmpty (P 'Impure abt '[] r)
 -> NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure r)))
-> ([P 'Impure abt '[] r] -> NonEmpty (P 'Impure abt '[] r))
-> [P 'Impure abt '[] r]
-> NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure r))
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [P 'Impure abt '[] r] -> NonEmpty (P 'Impure abt '[] r)
forall a. [a] -> NonEmpty a
NE.fromList)
        [PEval abt 'Impure m a]
ms


-- | Given some function we can call on the bodies of the branches,
-- freshen all the pattern-bound variables and then run the function
-- on all the branches in parallel (i.e., with the same continuation
-- and heap) and then emit a case-analysis expression with the
-- results of the continuations as the bodies of the branches. This
-- function is useful for when we really do want to emit a 'Case_'
-- expression, rather than doing the superpose of guard patterns
-- thing that 'constrainValue' does.
--
-- N.B., this function assumes (and does not verify) that the second
-- argument is emissible. So callers must guarantee this invariant,
-- by calling 'atomize' as necessary.
--
-- TODO: capture the emissibility requirement on the second argument
-- in the types.
emitCaseWith
    :: (ABT Term abt, Applicative m)
    => (abt '[] b -> PEval abt p m r)
    -> abt '[] a
    -> [Branch a abt b]
    -> PEval abt p m r
emitCaseWith :: (abt '[] b -> PEval abt p m r)
-> abt '[] a -> [Branch a abt b] -> PEval abt p m r
emitCaseWith abt '[] b -> PEval abt p m r
f abt '[] a
e [Branch a abt b]
bs = do
    [Char] -> PEval abt p m r
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: emitCaseWith"
{-
-- BUG: this doesn't typecheck with keeping @p@ polymorphic...
    gms <- T.for bs $ \(Branch pat body) ->
        let (vars, body') = caseBinds body
        in  (\vars' ->
                let rho = toAssocs vars (fmap11 var vars')
                in  GBranch pat vars' (f $ substs rho body')
            ) <$> freshenVars vars
    PEval $ \c h ->
        (syn . Case_ e) <$> T.for gms (\gm ->
            fromGBranch <$> T.for gm (\m ->
                unPEval m c h))
{-# INLINE emitCaseWith #-}
-}


-- HACK: to get the one case we really need to work at least.
emitCaseWith_Impure
    :: (ABT Term abt, Applicative m)
    => (abt '[] b -> PEval abt 'Impure m r)
    -> abt '[] a
    -> [Branch a abt b]
    -> PEval abt 'Impure m r
emitCaseWith_Impure :: (abt '[] b -> PEval abt 'Impure m r)
-> abt '[] a -> [Branch a abt b] -> PEval abt 'Impure m r
emitCaseWith_Impure abt '[] b -> PEval abt 'Impure m r
f abt '[] a
e [Branch a abt b]
bs = do
    [GBranch a (PEval abt 'Impure m r)]
gms <- [Branch a abt b]
-> (Branch a abt b
    -> PEval abt 'Impure m (GBranch a (PEval abt 'Impure m r)))
-> PEval abt 'Impure m [GBranch a (PEval abt 'Impure m r)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
T.for [Branch a abt b]
bs ((Branch a abt b
  -> PEval abt 'Impure m (GBranch a (PEval abt 'Impure m r)))
 -> PEval abt 'Impure m [GBranch a (PEval abt 'Impure m r)])
-> (Branch a abt b
    -> PEval abt 'Impure m (GBranch a (PEval abt 'Impure m r)))
-> PEval abt 'Impure m [GBranch a (PEval abt 'Impure m r)]
forall a b. (a -> b) -> a -> b
$ \(Branch Pattern xs a
pat abt xs b
body) ->
        let (List1 Variable xs
vars, abt '[] b
body') = abt xs b -> (List1 Variable xs, abt '[] b)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> (List1 Variable xs, abt '[] a)
caseBinds abt xs b
body
        in  (\List1 Variable xs
vars' ->
                let rho :: Assocs (abt '[])
rho = List1 Variable xs -> List1 (abt '[]) xs -> Assocs (abt '[])
forall k (xs :: [k]) (ast :: k -> *).
List1 Variable xs -> List1 ast xs -> Assocs ast
toAssocs1 List1 Variable xs
vars ((forall (i :: Hakaru). Variable i -> abt '[] i)
-> List1 Variable xs -> List1 (abt '[]) xs
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 k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
Variable a -> abt '[] a
forall (i :: Hakaru). Variable i -> abt '[] i
var List1 Variable xs
vars')
                in  Pattern xs a
-> List1 Variable xs
-> PEval abt 'Impure m r
-> GBranch a (PEval abt 'Impure m r)
forall (a :: Hakaru) r (xs :: [Hakaru]).
Pattern xs a -> List1 Variable xs -> r -> GBranch a r
GBranch Pattern xs a
pat List1 Variable xs
vars' (abt '[] b -> PEval abt 'Impure m r
f (abt '[] b -> PEval abt 'Impure m r)
-> abt '[] b -> PEval abt 'Impure m r
forall a b. (a -> b) -> a -> b
$ Assocs (abt '[]) -> abt '[] b -> abt '[] b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
(ABT syn abt, JmEq1 Sing, Show1 Sing, Traversable21 syn) =>
Assocs (abt '[]) -> abt xs a -> abt xs a
substs Assocs (abt '[])
rho abt '[] b
body')
            ) (List1 Variable xs -> GBranch a (PEval abt 'Impure m r))
-> PEval abt 'Impure m (List1 Variable xs)
-> PEval abt 'Impure m (GBranch a (PEval abt 'Impure m r))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 Variable xs -> PEval abt 'Impure m (List1 Variable xs)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
       (xs :: [Hakaru]).
EvaluationMonad abt m p =>
List1 Variable xs -> m (List1 Variable xs)
freshenVars List1 Variable xs
vars
    (forall (a :: Hakaru).
 (r -> PAns 'Impure abt m a) -> PAns 'Impure abt m a)
-> PEval abt 'Impure m r
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
(forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a)
-> PEval abt p m x
PEval ((forall (a :: Hakaru).
  (r -> PAns 'Impure abt m a) -> PAns 'Impure abt m a)
 -> PEval abt 'Impure m r)
-> (forall (a :: Hakaru).
    (r -> PAns 'Impure abt m a) -> PAns 'Impure abt m a)
-> PEval abt 'Impure m r
forall a b. (a -> b) -> a -> b
$ \r -> PAns 'Impure abt m a
c ListContext abt 'Impure
h ->
        (abt '[] ('HMeasure a) -> P 'Impure abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
abt xs ('HMeasure a) -> P 'Impure abt xs a
PImpure (abt '[] ('HMeasure a) -> P 'Impure abt '[] a)
-> ([Branch a abt ('HMeasure a)] -> abt '[] ('HMeasure a))
-> [Branch a abt ('HMeasure a)]
-> P 'Impure abt '[] a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. 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 (Term abt ('HMeasure a) -> abt '[] ('HMeasure a))
-> ([Branch a abt ('HMeasure a)] -> Term abt ('HMeasure a))
-> [Branch a abt ('HMeasure a)]
-> abt '[] ('HMeasure a)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. abt '[] a -> [Branch a abt ('HMeasure a)] -> Term abt ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
abt '[] a -> [Branch a abt b] -> Term abt b
Case_ abt '[] a
e) ([Branch a abt ('HMeasure a)] -> P 'Impure abt '[] a)
-> m [Branch a abt ('HMeasure a)] -> m (P 'Impure abt '[] a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GBranch a (PEval abt 'Impure m r)]
-> (GBranch a (PEval abt 'Impure m r)
    -> m (Branch a abt ('HMeasure a)))
-> m [Branch a abt ('HMeasure a)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
T.for [GBranch a (PEval abt 'Impure m r)]
gms (\GBranch a (PEval abt 'Impure m r)
gm ->
            GBranch a (abt '[] ('HMeasure a)) -> Branch a abt ('HMeasure a)
forall (syn :: ([Hakaru] -> Hakaru -> *) -> Hakaru -> *)
       (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
ABT syn abt =>
GBranch a (abt '[] b) -> Branch a abt b
fromGBranch (GBranch a (abt '[] ('HMeasure a)) -> Branch a abt ('HMeasure a))
-> m (GBranch a (abt '[] ('HMeasure a)))
-> m (Branch a abt ('HMeasure a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GBranch a (PEval abt 'Impure m r)
-> (PEval abt 'Impure m r -> m (abt '[] ('HMeasure a)))
-> m (GBranch a (abt '[] ('HMeasure a)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
T.for GBranch a (PEval abt 'Impure m r)
gm (\PEval abt 'Impure m r
m ->
                P 'Impure abt '[] a -> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
P 'Impure abt xs a -> abt xs ('HMeasure a)
unPImpure (P 'Impure abt '[] a -> abt '[] ('HMeasure a))
-> m (P 'Impure abt '[] a) -> m (abt '[] ('HMeasure a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PEval abt 'Impure m r
-> (r -> PAns 'Impure abt m a) -> PAns 'Impure abt m a
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity) (m :: * -> *)
       x.
PEval abt p m x
-> forall (a :: Hakaru). (x -> PAns p abt m a) -> PAns p abt m a
unPEval PEval abt 'Impure m r
m r -> PAns 'Impure abt m a
c ListContext abt 'Impure
h))
{-# INLINE emitCaseWith_Impure #-}


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