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

{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
--                                                    2016.04.28
-- |
-- Module      :  Language.Hakaru.Evaluation.Types
-- Copyright   :  Copyright (c) 2016 the Hakaru team
-- License     :  BSD3
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  experimental
-- Portability :  GHC-only
--
-- The data types for "Language.Hakaru.Evaluation.Lazy"
--
-- BUG: completely gave up on structure sharing. Need to add that back in.
--
-- TODO: once we figure out the exact API\/type of 'evaluate' and
-- can separate it from Disintegrate.hs vs its other clients (i.e.,
-- Sample.hs and Expect.hs), this file will prolly be broken up
-- into Lazy.hs itself vs Disintegrate.hs
----------------------------------------------------------------
module Language.Hakaru.Evaluation.Types
    (
    -- * Terms in particular known forms\/formats
      Head(..), fromHead, toHead, viewHeadDatum
    , Whnf(..), fromWhnf, toWhnf, caseWhnf, viewWhnfDatum
    , Lazy(..), fromLazy, caseLazy
    , getLazyVariable, isLazyVariable
    , getLazyLiteral,  isLazyLiteral

    -- * Lazy partial evaluation
    , TermEvaluator
    , MeasureEvaluator
    , CaseEvaluator
    , VariableEvaluator
    
    -- * The monad for partial evaluation
    , Purity(..), Statement(..), statementVars, isBoundBy
    , Index, indVar, indSize, fromIndex
    , Location(..), locEq, locHint, locType, locations1
    , fromLocation, fromLocations1, freshenLoc, freshenLocs
    , LAssoc, LAssocs , emptyLAssocs, singletonLAssocs
    , toLAssocs1, insertLAssocs, lookupLAssoc
#ifdef __TRACE_DISINTEGRATE__
    , ppList
    , ppInds
    , ppStatement
    , pretty_Statements
    , pretty_Statements_withTerm
    , prettyAssocs
#endif
    , EvaluationMonad(..)
    , defaultCaseEvaluator
    , toVarStatements
    , extSubst
    , extSubsts
    , freshVar
    , freshenVar
    , Hint(..), freshVars
    , freshenVars
    , freshInd
    {- TODO: should we expose these?
    , freshLocStatement
    , push_
    -}
    , push
    , pushes
    ) where

import           Prelude              hiding (id, (.))
import           Control.Category     (Category(..))
#if __GLASGOW_HASKELL__ < 710
import           Data.Monoid          (Monoid(..))
import           Data.Functor         ((<$>))
import           Control.Applicative  (Applicative(..))
import           Data.Traversable
#endif
import           Control.Arrow        ((***))
import qualified Data.Foldable        as F
import           Data.List.NonEmpty   (NonEmpty(..))
import qualified Data.Text            as T
import           Data.Text            (Text)
import           Data.Proxy           (KProxy(..))

import Language.Hakaru.Syntax.IClasses
import Data.Number.Nat
import Language.Hakaru.Types.DataKind
import Language.Hakaru.Types.Sing    (Sing(..))
import Language.Hakaru.Types.Coercion
import Language.Hakaru.Syntax.AST
import Language.Hakaru.Syntax.Datum
import Language.Hakaru.Syntax.DatumCase (DatumEvaluator,
                                         MatchResult(..),
                                         matchBranches)
import Language.Hakaru.Syntax.AST.Eq (alphaEq)
-- import Language.Hakaru.Syntax.TypeOf
import Language.Hakaru.Syntax.ABT
import qualified Language.Hakaru.Syntax.Prelude as P

#ifdef __TRACE_DISINTEGRATE__
import qualified Text.PrettyPrint     as PP
import Language.Hakaru.Pretty.Haskell
import           Debug.Trace          (trace)
#endif

----------------------------------------------------------------
----------------------------------------------------------------
-- N.B., when putting things into the context, be sure to freshen
-- the variables as if we were allocating a new location on the
-- heap.
--
-- For simplicity we don't actually distinguish between "variables"
-- and "locations". In the old finally-tagless code we had an @s@
-- parameter like the 'ST' monad does in order to keep track of
-- which heap things belong to. But since we might have nested
-- disintegration, and thus nested heaps, doing that means we'd
-- have to do some sort of De Bruijn numbering in the @s@ parameter
-- in order to keep track of the nested regions; and that's just
-- too much work to bother with.


-- TODO: for forward disintegration (which is not just partial evaluation) we really do mean proper HNFs not just WHNFs. This falls out from our needing to guarantee that heap-bound variables can't possibly escape; whence the assumption that the result of forward disintegration contains no heap-bound variables.
--
-- TODO: is there a way to integrate this into the actual 'Term'
-- definition in order to reduce repetition?
--
-- HACK: can't use \"H\" as the prefix because that clashes with
-- the Hakaru datakind
--
-- | A \"weak-head\" for the sake of 'Whnf'. N.B., this doesn't
-- exactly correlate with the usual notion of \"weak-head\"; in
-- particular we keep track of type annotations and coercions, and
-- don't reduce integration\/summation. So really we should use
-- some other name for 'Whnf'...
data Head :: ([Hakaru] -> Hakaru -> *) -> Hakaru -> * where
    -- Simple heads (aka, the usual stuff)
    WLiteral :: !(Literal a) -> Head abt a
    -- BUG: even though the 'Datum' type has a single constructor, we get a warning about not being able to UNPACK it in 'WDatum'... wtf?
    WDatum :: !(Datum (abt '[]) (HData' t)) -> Head abt (HData' t)
    WEmpty :: !(Sing ('HArray a)) -> Head abt ('HArray a)
    WArray :: !(abt '[] 'HNat) -> !(abt '[ 'HNat] a) -> Head abt ('HArray a)
    WArrayLiteral
           :: [abt '[] a] -> Head abt ('HArray a)
    WLam   :: !(abt '[ a ] b) -> Head abt (a ':-> b)

    -- Measure heads (N.B., not simply @abt '[] ('HMeasure _)@)
    WMeasureOp
        :: (typs ~ UnLCs args, args ~ LCs typs)
        => !(MeasureOp typs a)
        -> !(SArgs abt args)
        -> Head abt ('HMeasure a)
    WDirac :: !(abt '[] a) -> Head abt ('HMeasure a)
    WMBind
        :: !(abt '[] ('HMeasure a))
        -> !(abt '[ a ] ('HMeasure b))
        -> Head abt ('HMeasure b)
    WPlate
        :: !(abt '[] 'HNat)
        -> !(abt '[ 'HNat ] ('HMeasure a))
        -> Head abt ('HMeasure ('HArray a))
    WChain
        :: !(abt '[] 'HNat)
        -> !(abt '[] s)
        -> !(abt '[ s ] ('HMeasure (HPair a s)))
        -> Head abt ('HMeasure (HPair ('HArray a) s))
    WSuperpose
        :: !(NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a)))
        -> Head abt ('HMeasure a)
    WReject
        :: !(Sing ('HMeasure a)) -> Head abt ('HMeasure a)

    -- Type coercion stuff. These are transparent re head-ness; that is, they behave more like HNF than WHNF.
    -- TODO: we prolly don't actually want\/need the coercion variants... we'd lose some proven-guarantees about cancellation, but everything should work just fine. The one issue that remains is if we have coercion of 'WIntegrate' or 'WSummate', since without the 'WCoerceTo'\/'WUnsafeFrom' constructors we'd be forced to call the coercion of an integration \"neutral\"--- even though it's not actually a neutral term!
    WCoerceTo   :: !(Coercion a b) -> !(Head abt a) -> Head abt b
    WUnsafeFrom :: !(Coercion a b) -> !(Head abt b) -> Head abt a

    -- Other funky stuff
    WIntegrate
        :: !(abt '[] 'HReal)
        -> !(abt '[] 'HReal)
        -> !(abt '[ 'HReal ] 'HProb)
        -> Head abt 'HProb
    -- WSummate
    --     :: !(abt '[] 'HReal)
    --     -> !(abt '[] 'HReal)
    --     -> !(abt '[ 'HInt ] 'HProb)
    --     -> Head abt 'HProb

    -- Quasi-/semi-/demi-/pseudo- normal form stuff
    {-
    NaryOp_ :: !(NaryOp a) -> !(Seq (abt '[] a)) -> Term abt a
    PrimOp_
        :: (typs ~ UnLCs args, args ~ LCs typs)
        => !(PrimOp typs a) -> SCon args a
    -- N.B., not 'ArrayOp_'
    -}


-- | Forget that something is a head.
fromHead :: (ABT Term abt) => Head abt a -> abt '[] a
fromHead :: Head abt a -> abt '[] a
fromHead (WLiteral    Literal a
v)        = 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 (Literal a -> Term abt a
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Term abt a
Literal_ Literal a
v)
fromHead (WDatum      Datum (abt '[]) (HData' t)
d)        = 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 (Datum (abt '[]) (HData' t) -> Term abt (HData' t)
forall (abt :: [Hakaru] -> Hakaru -> *) (t :: HakaruCon).
Datum (abt '[]) (HData' t) -> Term abt (HData' t)
Datum_ Datum (abt '[]) (HData' t)
d)
fromHead (WEmpty      Sing ('HArray a)
typ)      = Term abt ('HArray a) -> abt '[] ('HArray a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Sing ('HArray a) -> Term abt ('HArray a)
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Sing ('HArray a) -> Term abt ('HArray a)
Empty_ Sing ('HArray a)
typ)
fromHead (WArray      abt '[] 'HNat
e1 abt '[ 'HNat] a
e2)    = Term abt ('HArray a) -> abt '[] ('HArray a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (abt '[] 'HNat -> abt '[ 'HNat] a -> Term abt ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] 'HNat -> abt '[ 'HNat] a -> Term abt ('HArray a)
Array_ abt '[] 'HNat
e1 abt '[ 'HNat] a
e2)
fromHead (WArrayLiteral  [abt '[] a]
es)    = Term abt ('HArray a) -> abt '[] ('HArray a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn ([abt '[] a] -> Term abt ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
[abt '[] a] -> Term abt ('HArray a)
ArrayLiteral_ [abt '[] a]
es)
fromHead (WLam        abt '[a] b
e1)       = Term abt (a ':-> b) -> abt '[] (a ':-> b)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (SCon '[ '( '[a], b)] (a ':-> b)
forall (a :: Hakaru) (b :: Hakaru). SCon '[ '( '[a], b)] (a ':-> b)
Lam_ SCon '[ '( '[a], b)] (a ':-> b)
-> SArgs abt '[ '( '[a], b)] -> Term abt (a ':-> b)
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt '[a] b
e1 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)
fromHead (WMeasureOp  MeasureOp typs a
o  SArgs abt args
es)    = 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 (MeasureOp typs a -> SCon args ('HMeasure a)
forall (typs :: [Hakaru]) (args :: [([Hakaru], Hakaru)])
       (a :: Hakaru).
(typs ~ UnLCs args, args ~ LCs typs) =>
MeasureOp typs a -> SCon args ('HMeasure a)
MeasureOp_ MeasureOp typs a
o SCon args ('HMeasure a) -> SArgs abt args -> Term abt ('HMeasure a)
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ SArgs abt args
es)
fromHead (WDirac      abt '[] a
e1)       = 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
e1 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)
fromHead (WMBind      abt '[] ('HMeasure a)
e1 abt '[a] ('HMeasure b)
e2)    = Term abt ('HMeasure b) -> abt '[] ('HMeasure b)
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 b)] ('HMeasure b)
forall (a :: Hakaru) (a :: Hakaru).
SCon '[LC ('HMeasure a), '( '[a], 'HMeasure a)] ('HMeasure a)
MBind SCon '[LC ('HMeasure a), '( '[a], 'HMeasure b)] ('HMeasure b)
-> SArgs abt '[LC ('HMeasure a), '( '[a], 'HMeasure b)]
-> Term abt ('HMeasure b)
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt '[] ('HMeasure a)
e1 abt '[] ('HMeasure a)
-> SArgs abt '[ '( '[a], 'HMeasure b)]
-> SArgs abt '[LC ('HMeasure a), '( '[a], 'HMeasure b)]
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 b)
e2 abt '[a] ('HMeasure b)
-> SArgs abt '[] -> SArgs abt '[ '( '[a], 'HMeasure 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)
fromHead (WPlate      abt '[] 'HNat
e1 abt '[ 'HNat] ('HMeasure a)
e2)    = Term abt ('HMeasure ('HArray a)) -> abt '[] ('HMeasure ('HArray a))
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (SCon
  '[LC 'HNat, '( '[ 'HNat], 'HMeasure a)] ('HMeasure ('HArray a))
forall (a :: Hakaru).
SCon
  '[LC 'HNat, '( '[ 'HNat], 'HMeasure a)] ('HMeasure ('HArray a))
Plate SCon
  '[LC 'HNat, '( '[ 'HNat], 'HMeasure a)] ('HMeasure ('HArray a))
-> SArgs abt '[LC 'HNat, '( '[ 'HNat], 'HMeasure a)]
-> Term abt ('HMeasure ('HArray a))
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt '[] 'HNat
e1 abt '[] 'HNat
-> SArgs abt '[ '( '[ 'HNat], 'HMeasure a)]
-> SArgs abt '[LC 'HNat, '( '[ 'HNat], 'HMeasure a)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* abt '[ 'HNat] ('HMeasure a)
e2 abt '[ 'HNat] ('HMeasure a)
-> SArgs abt '[] -> SArgs abt '[ '( '[ 'HNat], 'HMeasure a)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs abt '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End)
fromHead (WChain      abt '[] 'HNat
e1 abt '[] s
e2 abt '[s] ('HMeasure (HPair a s))
e3) = Term abt ('HMeasure (HPair ('HArray a) s))
-> abt '[] ('HMeasure (HPair ('HArray a) s))
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (SCon
  '[LC 'HNat, LC s, '( '[s], 'HMeasure (HPair a s))]
  ('HMeasure (HPair ('HArray a) s))
forall (s :: Hakaru) (a :: Hakaru).
SCon
  '[LC 'HNat, LC s, '( '[s], 'HMeasure (HPair a s))]
  ('HMeasure (HPair ('HArray a) s))
Chain SCon
  '[LC 'HNat, LC s, '( '[s], 'HMeasure (HPair a s))]
  ('HMeasure (HPair ('HArray a) s))
-> SArgs abt '[LC 'HNat, LC s, '( '[s], 'HMeasure (HPair a s))]
-> Term abt ('HMeasure (HPair ('HArray a) s))
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt '[] 'HNat
e1 abt '[] 'HNat
-> SArgs abt '[LC s, '( '[s], 'HMeasure (HPair a s))]
-> SArgs abt '[LC 'HNat, LC s, '( '[s], 'HMeasure (HPair a s))]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* abt '[] s
e2 abt '[] s
-> SArgs abt '[ '( '[s], 'HMeasure (HPair a s))]
-> SArgs abt '[LC s, '( '[s], 'HMeasure (HPair a s))]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* abt '[s] ('HMeasure (HPair a s))
e3 abt '[s] ('HMeasure (HPair a s))
-> SArgs abt '[] -> SArgs abt '[ '( '[s], 'HMeasure (HPair a s))]
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)
fromHead (WSuperpose  NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
pes)      = 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 (NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> Term abt ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> Term abt ('HMeasure a)
Superpose_ NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
pes)
fromHead (WReject     Sing ('HMeasure a)
typ)      = 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 (Sing ('HMeasure a) -> Term abt ('HMeasure a)
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Sing ('HMeasure a) -> Term abt ('HMeasure a)
Reject_ Sing ('HMeasure a)
typ)
fromHead (WCoerceTo   Coercion a a
c Head abt a
e1)     = Term abt a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Coercion a a -> SCon '[LC a] a
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> SCon '[LC a] b
CoerceTo_   Coercion a a
c SCon '[LC a] a -> SArgs abt '[LC a] -> Term abt a
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ Head abt a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Head abt a -> abt '[] a
fromHead Head abt a
e1 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)
fromHead (WUnsafeFrom Coercion a b
c Head abt b
e1)     = Term abt a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Coercion a b -> SCon '[LC b] a
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> SCon '[LC b] a
UnsafeFrom_ Coercion a b
c SCon '[LC b] a -> SArgs abt '[LC b] -> Term abt a
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ Head abt b -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Head abt a -> abt '[] a
fromHead Head abt b
e1 abt '[] b -> SArgs abt '[] -> SArgs abt '[LC b]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs abt '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End)
fromHead (WIntegrate  abt '[] 'HReal
e1 abt '[] 'HReal
e2 abt '[ 'HReal] 'HProb
e3) = 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 'HReal, LC 'HReal, '( '[ 'HReal], 'HProb)] 'HProb
Integrate SCon '[LC 'HReal, LC 'HReal, '( '[ 'HReal], 'HProb)] 'HProb
-> SArgs abt '[LC 'HReal, LC 'HReal, '( '[ 'HReal], 'HProb)]
-> Term abt 'HProb
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt '[] 'HReal
e1 abt '[] 'HReal
-> SArgs abt '[LC 'HReal, '( '[ 'HReal], 'HProb)]
-> SArgs abt '[LC 'HReal, LC 'HReal, '( '[ 'HReal], 'HProb)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* abt '[] 'HReal
e2 abt '[] 'HReal
-> SArgs abt '[ '( '[ 'HReal], 'HProb)]
-> SArgs abt '[LC 'HReal, '( '[ 'HReal], 'HProb)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* abt '[ 'HReal] 'HProb
e3 abt '[ 'HReal] 'HProb
-> SArgs abt '[] -> SArgs abt '[ '( '[ 'HReal], '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)
--fromHead (WSummate    e1 e2 e3) = syn (Summate   :$ e1 :* e2 :* e3 :* End)


-- | Identify terms which are already heads.
toHead :: (ABT Term abt) => abt '[] a -> Maybe (Head abt a)
toHead :: abt '[] a -> Maybe (Head abt a)
toHead abt '[] a
e =
    abt '[] a
-> (Variable a -> Maybe (Head abt a))
-> (Term abt a -> Maybe (Head abt a))
-> Maybe (Head 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 (Maybe (Head abt a) -> Variable a -> Maybe (Head abt a)
forall a b. a -> b -> a
const Maybe (Head abt a)
forall a. Maybe a
Nothing) ((Term abt a -> Maybe (Head abt a)) -> Maybe (Head abt a))
-> (Term abt a -> Maybe (Head abt a)) -> Maybe (Head abt a)
forall a b. (a -> b) -> a -> b
$ \Term abt a
t ->
        case Term abt a
t of
        Literal_     Literal a
v                      -> Head abt a -> Maybe (Head abt a)
forall a. a -> Maybe a
Just (Head abt a -> Maybe (Head abt a))
-> Head abt a -> Maybe (Head abt a)
forall a b. (a -> b) -> a -> b
$ Literal a -> Head abt a
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Head abt a
WLiteral   Literal a
v
        Datum_       Datum (abt '[]) (HData' t)
d                      -> Head abt a -> Maybe (Head abt a)
forall a. a -> Maybe a
Just (Head abt a -> Maybe (Head abt a))
-> Head abt a -> Maybe (Head abt a)
forall a b. (a -> b) -> a -> b
$ 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
        Empty_       Sing ('HArray a)
typ                    -> Head abt ('HArray a) -> Maybe (Head abt ('HArray a))
forall a. a -> Maybe a
Just (Head abt ('HArray a) -> Maybe (Head abt ('HArray a)))
-> Head abt ('HArray a) -> Maybe (Head abt ('HArray a))
forall a b. (a -> b) -> a -> b
$ Sing ('HArray a) -> Head abt ('HArray a)
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Sing ('HArray a) -> Head abt ('HArray a)
WEmpty     Sing ('HArray a)
typ
        Array_       abt '[] 'HNat
e1     abt '[ 'HNat] a
e2              -> Head abt ('HArray a) -> Maybe (Head abt ('HArray a))
forall a. a -> Maybe a
Just (Head abt ('HArray a) -> Maybe (Head abt ('HArray a)))
-> Head abt ('HArray a) -> Maybe (Head abt ('HArray a))
forall a b. (a -> b) -> a -> b
$ abt '[] 'HNat -> abt '[ 'HNat] a -> Head abt ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] 'HNat -> abt '[ 'HNat] a -> Head abt ('HArray a)
WArray     abt '[] 'HNat
e1 abt '[ 'HNat] a
e2
        ArrayLiteral_       [abt '[] a]
es              -> Head abt ('HArray a) -> Maybe (Head abt ('HArray a))
forall a. a -> Maybe a
Just (Head abt ('HArray a) -> Maybe (Head abt ('HArray a)))
-> Head abt ('HArray a) -> Maybe (Head abt ('HArray a))
forall a b. (a -> b) -> a -> b
$ [abt '[] a] -> Head abt ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
[abt '[] a] -> Head abt ('HArray a)
WArrayLiteral [abt '[] a]
es
        SCon args a
Lam_      :$ abt vars a
e1  :* SArgs abt args
End             -> Head abt (a ':-> a) -> Maybe (Head abt (a ':-> a))
forall a. a -> Maybe a
Just (Head abt (a ':-> a) -> Maybe (Head abt (a ':-> a)))
-> Head abt (a ':-> a) -> Maybe (Head abt (a ':-> a))
forall a b. (a -> b) -> a -> b
$ abt '[a] a -> Head abt (a ':-> a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (typs :: Hakaru).
abt '[a] typs -> Head abt (a ':-> typs)
WLam       abt vars a
abt '[a] a
e1
        MeasureOp_   MeasureOp typs a
o   :$ SArgs abt args
es              -> Head abt ('HMeasure a) -> Maybe (Head abt ('HMeasure a))
forall a. a -> Maybe a
Just (Head abt ('HMeasure a) -> Maybe (Head abt ('HMeasure a)))
-> Head abt ('HMeasure a) -> Maybe (Head abt ('HMeasure a))
forall a b. (a -> b) -> a -> b
$ MeasureOp typs a -> SArgs abt args -> Head abt ('HMeasure a)
forall (typs :: [Hakaru]) (args :: [([Hakaru], Hakaru)])
       (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
(typs ~ UnLCs args, args ~ LCs typs) =>
MeasureOp typs a -> SArgs abt args -> Head abt ('HMeasure a)
WMeasureOp MeasureOp typs a
o  SArgs abt args
es
        SCon args a
Dirac     :$ abt vars a
e1  :* SArgs abt args
End             -> Head abt ('HMeasure a) -> Maybe (Head abt ('HMeasure a))
forall a. a -> Maybe a
Just (Head abt ('HMeasure a) -> Maybe (Head abt ('HMeasure a)))
-> Head abt ('HMeasure a) -> Maybe (Head abt ('HMeasure a))
forall a b. (a -> b) -> a -> b
$ abt '[] a -> Head abt ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Head abt ('HMeasure a)
WDirac     abt vars a
abt '[] a
e1
        SCon args a
MBind     :$ abt vars a
e1  :* abt vars a
e2 :* SArgs abt args
End       -> Head abt ('HMeasure b) -> Maybe (Head abt ('HMeasure b))
forall a. a -> Maybe a
Just (Head abt ('HMeasure b) -> Maybe (Head abt ('HMeasure b)))
-> Head abt ('HMeasure b) -> Maybe (Head abt ('HMeasure b))
forall a b. (a -> b) -> a -> b
$ abt '[] ('HMeasure a)
-> abt '[a] ('HMeasure b) -> Head abt ('HMeasure b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
abt '[] ('HMeasure a)
-> abt '[a] ('HMeasure b) -> Head abt ('HMeasure b)
WMBind     abt vars a
abt '[] ('HMeasure a)
e1 abt vars a
abt '[a] ('HMeasure b)
e2
        SCon args a
Plate     :$ abt vars a
e1  :* abt vars a
e2 :* SArgs abt args
End       -> Head abt ('HMeasure ('HArray a))
-> Maybe (Head abt ('HMeasure ('HArray a)))
forall a. a -> Maybe a
Just (Head abt ('HMeasure ('HArray a))
 -> Maybe (Head abt ('HMeasure ('HArray a))))
-> Head abt ('HMeasure ('HArray a))
-> Maybe (Head abt ('HMeasure ('HArray a)))
forall a b. (a -> b) -> a -> b
$ abt '[] 'HNat
-> abt '[ 'HNat] ('HMeasure a) -> Head abt ('HMeasure ('HArray a))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] 'HNat
-> abt '[ 'HNat] ('HMeasure a) -> Head abt ('HMeasure ('HArray a))
WPlate     abt vars a
abt '[] 'HNat
e1 abt vars a
abt '[ 'HNat] ('HMeasure a)
e2
        SCon args a
Chain     :$ abt vars a
e1  :* abt vars a
e2 :* abt vars a
e3 :* SArgs abt args
End -> Head abt ('HMeasure (HPair ('HArray a) a))
-> Maybe (Head abt ('HMeasure (HPair ('HArray a) a)))
forall a. a -> Maybe a
Just (Head abt ('HMeasure (HPair ('HArray a) a))
 -> Maybe (Head abt ('HMeasure (HPair ('HArray a) a))))
-> Head abt ('HMeasure (HPair ('HArray a) a))
-> Maybe (Head abt ('HMeasure (HPair ('HArray a) a)))
forall a b. (a -> b) -> a -> b
$ abt '[] 'HNat
-> abt '[] a
-> abt '[a] ('HMeasure (HPair a a))
-> Head abt ('HMeasure (HPair ('HArray a) a))
forall (abt :: [Hakaru] -> Hakaru -> *) (s :: Hakaru)
       (a :: Hakaru).
abt '[] 'HNat
-> abt '[] s
-> abt '[s] ('HMeasure (HPair a s))
-> Head abt ('HMeasure (HPair ('HArray a) s))
WChain     abt vars a
abt '[] 'HNat
e1 abt vars a
abt '[] a
e2 abt vars a
abt '[a] ('HMeasure (HPair a a))
e3 
        Superpose_   NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
pes                    -> Head abt ('HMeasure a) -> Maybe (Head abt ('HMeasure a))
forall a. a -> Maybe a
Just (Head abt ('HMeasure a) -> Maybe (Head abt ('HMeasure a)))
-> Head abt ('HMeasure a) -> Maybe (Head abt ('HMeasure a))
forall a b. (a -> b) -> a -> b
$ NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> Head abt ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> Head abt ('HMeasure a)
WSuperpose NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
pes
        CoerceTo_    Coercion a a
c   :$ abt vars a
e1 :* SArgs abt args
End       -> Coercion a a -> Head abt a -> Head abt a
forall (a :: Hakaru) (b :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
Coercion a b -> Head abt a -> Head abt b
WCoerceTo   Coercion a a
c (Head abt a -> Head abt a)
-> Maybe (Head abt a) -> Maybe (Head abt a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> abt '[] a -> Maybe (Head abt a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Maybe (Head abt a)
toHead abt vars a
abt '[] a
e1
        UnsafeFrom_  Coercion a b
c   :$ abt vars a
e1 :* SArgs abt args
End       -> Coercion a b -> Head abt b -> Head abt a
forall (a :: Hakaru) (b :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
Coercion a b -> Head abt b -> Head abt a
WUnsafeFrom Coercion a b
c (Head abt b -> Head abt a)
-> Maybe (Head abt b) -> Maybe (Head abt a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> abt '[] a -> Maybe (Head abt a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Maybe (Head abt a)
toHead abt vars a
abt '[] a
e1
        SCon args a
Integrate :$ abt vars a
e1  :* abt vars a
e2 :* abt vars a
e3 :* SArgs abt args
End -> Head abt 'HProb -> Maybe (Head abt 'HProb)
forall a. a -> Maybe a
Just (Head abt 'HProb -> Maybe (Head abt 'HProb))
-> Head abt 'HProb -> Maybe (Head abt 'HProb)
forall a b. (a -> b) -> a -> b
$ abt '[] 'HReal
-> abt '[] 'HReal -> abt '[ 'HReal] 'HProb -> Head abt 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
abt '[] 'HReal
-> abt '[] 'HReal -> abt '[ 'HReal] 'HProb -> Head abt 'HProb
WIntegrate abt vars a
abt '[] 'HReal
e1 abt vars a
abt '[] 'HReal
e2 abt vars a
abt '[ 'HReal] 'HProb
e3
        --Summate   :$ e1  :* e2 :* e3 :* End -> Just $ WSummate   e1 e2 e3
        Term abt a
_ -> Maybe (Head abt a)
forall a. Maybe a
Nothing

instance Functor21 Head where
    fmap21 :: (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i)
-> Head a j -> Head b j
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
_ (WLiteral    Literal j
v)        = Literal j -> Head b j
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Head abt a
WLiteral Literal j
v
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (WDatum      Datum (a '[]) (HData' t)
d)        = Datum (b '[]) (HData' t) -> Head b (HData' t)
forall (abt :: [Hakaru] -> Hakaru -> *) (t :: HakaruCon).
Datum (abt '[]) (HData' t) -> Head abt (HData' t)
WDatum ((forall (i :: Hakaru). a '[] i -> b '[] i)
-> Datum (a '[]) (HData' t) -> Datum (b '[]) (HData' t)
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *)
       (b :: k1 -> *) (j :: k2).
Functor11 f =>
(forall (i :: k1). a i -> b i) -> f a j -> f b j
fmap11 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
forall (i :: Hakaru). a '[] i -> b '[] i
f Datum (a '[]) (HData' t)
d)
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
_ (WEmpty      Sing ('HArray a)
typ)      = Sing ('HArray a) -> Head b ('HArray a)
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Sing ('HArray a) -> Head abt ('HArray a)
WEmpty Sing ('HArray a)
typ
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (WArray      a '[] 'HNat
e1 a '[ 'HNat] a
e2)    = b '[] 'HNat -> b '[ 'HNat] a -> Head b ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] 'HNat -> abt '[ 'HNat] a -> Head abt ('HArray a)
WArray (a '[] 'HNat -> b '[] 'HNat
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[] 'HNat
e1) (a '[ 'HNat] a -> b '[ 'HNat] a
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[ 'HNat] a
e2)
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (WArrayLiteral  [a '[] a]
es)    = [b '[] a] -> Head b ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
[abt '[] a] -> Head abt ('HArray a)
WArrayLiteral ((a '[] a -> b '[] a) -> [a '[] a] -> [b '[] a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a '[] a -> b '[] a
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f [a '[] a]
es)
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (WLam        a '[a] b
e1)       = b '[a] b -> Head b (a ':-> b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (typs :: Hakaru).
abt '[a] typs -> Head abt (a ':-> typs)
WLam (a '[a] b -> b '[a] b
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[a] b
e1)
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (WMeasureOp  MeasureOp typs a
o  SArgs a args
es)    = MeasureOp typs a -> SArgs b args -> Head b ('HMeasure a)
forall (typs :: [Hakaru]) (args :: [([Hakaru], Hakaru)])
       (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
(typs ~ UnLCs args, args ~ LCs typs) =>
MeasureOp typs a -> SArgs abt args -> Head abt ('HMeasure a)
WMeasureOp MeasureOp typs a
o ((forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i)
-> SArgs a args -> SArgs b args
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *)
       (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
Functor21 f =>
(forall (h :: k1) (i :: k2). a h i -> b h i) -> f a j -> f b j
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f SArgs a args
es)
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (WDirac      a '[] a
e1)       = b '[] a -> Head b ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Head abt ('HMeasure a)
WDirac (a '[] a -> b '[] a
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[] a
e1)
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (WMBind      a '[] ('HMeasure a)
e1 a '[a] ('HMeasure b)
e2)    = b '[] ('HMeasure a) -> b '[a] ('HMeasure b) -> Head b ('HMeasure b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
abt '[] ('HMeasure a)
-> abt '[a] ('HMeasure b) -> Head abt ('HMeasure b)
WMBind (a '[] ('HMeasure a) -> b '[] ('HMeasure a)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[] ('HMeasure a)
e1) (a '[a] ('HMeasure b) -> b '[a] ('HMeasure b)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[a] ('HMeasure b)
e2)
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (WPlate      a '[] 'HNat
e1 a '[ 'HNat] ('HMeasure a)
e2)    = b '[] 'HNat
-> b '[ 'HNat] ('HMeasure a) -> Head b ('HMeasure ('HArray a))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] 'HNat
-> abt '[ 'HNat] ('HMeasure a) -> Head abt ('HMeasure ('HArray a))
WPlate (a '[] 'HNat -> b '[] 'HNat
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[] 'HNat
e1) (a '[ 'HNat] ('HMeasure a) -> b '[ 'HNat] ('HMeasure a)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[ 'HNat] ('HMeasure a)
e2)
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (WChain      a '[] 'HNat
e1 a '[] s
e2 a '[s] ('HMeasure (HPair a s))
e3) = b '[] 'HNat
-> b '[] s
-> b '[s] ('HMeasure (HPair a s))
-> Head b ('HMeasure (HPair ('HArray a) s))
forall (abt :: [Hakaru] -> Hakaru -> *) (s :: Hakaru)
       (a :: Hakaru).
abt '[] 'HNat
-> abt '[] s
-> abt '[s] ('HMeasure (HPair a s))
-> Head abt ('HMeasure (HPair ('HArray a) s))
WChain (a '[] 'HNat -> b '[] 'HNat
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[] 'HNat
e1) (a '[] s -> b '[] s
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[] s
e2) (a '[s] ('HMeasure (HPair a s)) -> b '[s] ('HMeasure (HPair a s))
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[s] ('HMeasure (HPair a s))
e3)
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (WSuperpose  NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
pes)      = NonEmpty (b '[] 'HProb, b '[] ('HMeasure a))
-> Head b ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> Head abt ('HMeasure a)
WSuperpose (((a '[] 'HProb, a '[] ('HMeasure a))
 -> (b '[] 'HProb, b '[] ('HMeasure a)))
-> NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
-> NonEmpty (b '[] 'HProb, b '[] ('HMeasure a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a '[] 'HProb -> b '[] 'HProb
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (a '[] 'HProb -> b '[] 'HProb)
-> (a '[] ('HMeasure a) -> b '[] ('HMeasure a))
-> (a '[] 'HProb, a '[] ('HMeasure a))
-> (b '[] 'HProb, b '[] ('HMeasure a))
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** a '[] ('HMeasure a) -> b '[] ('HMeasure a)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f) NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
pes)
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
_ (WReject     Sing ('HMeasure a)
typ)      = Sing ('HMeasure a) -> Head b ('HMeasure a)
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Sing ('HMeasure a) -> Head abt ('HMeasure a)
WReject Sing ('HMeasure a)
typ
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (WCoerceTo   Coercion a j
c Head a a
e1)     = Coercion a j -> Head b a -> Head b j
forall (a :: Hakaru) (b :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
Coercion a b -> Head abt a -> Head abt b
WCoerceTo   Coercion a j
c ((forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i)
-> Head a a -> Head b a
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *)
       (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
Functor21 f =>
(forall (h :: k1) (i :: k2). a h i -> b h i) -> f a j -> f b j
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f Head a a
e1)
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (WUnsafeFrom Coercion j b
c Head a b
e1)     = Coercion j b -> Head b b -> Head b j
forall (a :: Hakaru) (b :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
Coercion a b -> Head abt b -> Head abt a
WUnsafeFrom Coercion j b
c ((forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i)
-> Head a b -> Head b b
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *)
       (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
Functor21 f =>
(forall (h :: k1) (i :: k2). a h i -> b h i) -> f a j -> f b j
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f Head a b
e1)
    fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (WIntegrate  a '[] 'HReal
e1 a '[] 'HReal
e2 a '[ 'HReal] 'HProb
e3) = b '[] 'HReal
-> b '[] 'HReal -> b '[ 'HReal] 'HProb -> Head b 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
abt '[] 'HReal
-> abt '[] 'HReal -> abt '[ 'HReal] 'HProb -> Head abt 'HProb
WIntegrate (a '[] 'HReal -> b '[] 'HReal
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[] 'HReal
e1) (a '[] 'HReal -> b '[] 'HReal
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[] 'HReal
e2) (a '[ 'HReal] 'HProb -> b '[ 'HReal] 'HProb
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a '[ 'HReal] 'HProb
e3)
    --fmap21 f (WSummate    e1 e2 e3) = WSummate   (f e1) (f e2) (f e3)

instance Foldable21 Head where
    foldMap21 :: (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m) -> Head a j -> m
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
_ (WLiteral    Literal j
_)        = m
forall a. Monoid a => a
mempty
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (WDatum      Datum (a '[]) (HData' t)
d)        = (forall (i :: Hakaru). a '[] i -> m)
-> Datum (a '[]) (HData' t) -> m
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) m (a :: k1 -> *)
       (j :: k2).
(Foldable11 f, Monoid m) =>
(forall (i :: k1). a i -> m) -> f a j -> m
foldMap11 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
forall (i :: Hakaru). a '[] i -> m
f Datum (a '[]) (HData' t)
d
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
_ (WEmpty      Sing ('HArray a)
_)        = m
forall a. Monoid a => a
mempty
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (WArray      a '[] 'HNat
e1 a '[ 'HNat] a
e2)    = a '[] 'HNat -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[] 'HNat
e1 m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` a '[ 'HNat] a -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[ 'HNat] a
e2
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (WArrayLiteral  [a '[] a]
es)    = (a '[] a -> m) -> [a '[] a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
F.foldMap a '[] a -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f [a '[] a]
es
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (WLam        a '[a] b
e1)       = a '[a] b -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[a] b
e1
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (WMeasureOp  MeasureOp typs a
_  SArgs a args
es)    = (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m)
-> SArgs a args -> m
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *) m
       (a :: k1 -> k2 -> *) (j :: k3).
(Foldable21 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j -> m
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f SArgs a args
es
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (WDirac      a '[] a
e1)       = a '[] a -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[] a
e1
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (WMBind      a '[] ('HMeasure a)
e1 a '[a] ('HMeasure b)
e2)    = a '[] ('HMeasure a) -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[] ('HMeasure a)
e1 m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` a '[a] ('HMeasure b) -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[a] ('HMeasure b)
e2
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (WPlate      a '[] 'HNat
e1 a '[ 'HNat] ('HMeasure a)
e2)    = a '[] 'HNat -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[] 'HNat
e1 m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` a '[ 'HNat] ('HMeasure a) -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[ 'HNat] ('HMeasure a)
e2
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (WChain      a '[] 'HNat
e1 a '[] s
e2 a '[s] ('HMeasure (HPair a s))
e3) = a '[] 'HNat -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[] 'HNat
e1 m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` a '[] s -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[] s
e2 m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` a '[s] ('HMeasure (HPair a s)) -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[s] ('HMeasure (HPair a s))
e3
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (WSuperpose  NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
pes)      = (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m)
-> NonEmpty (a '[] 'HProb, a '[] ('HMeasure a)) -> m
forall k1 k2 m (f :: * -> *) (abt :: k1 -> k2 -> *) (xs :: k1)
       (a :: k2) (ys :: k1) (b :: k2).
(Monoid m, Foldable f) =>
(forall (h :: k1) (i :: k2). abt h i -> m)
-> f (abt xs a, abt ys b) -> m
foldMapPairs forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
pes
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
_ (WReject     Sing ('HMeasure a)
_)        = m
forall a. Monoid a => a
mempty
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (WCoerceTo   Coercion a j
_ Head a a
e1)     = (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m) -> Head a a -> m
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *) m
       (a :: k1 -> k2 -> *) (j :: k3).
(Foldable21 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j -> m
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f Head a a
e1
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (WUnsafeFrom Coercion j b
_ Head a b
e1)     = (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m) -> Head a b -> m
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *) m
       (a :: k1 -> k2 -> *) (j :: k3).
(Foldable21 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j -> m
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f Head a b
e1
    foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (WIntegrate  a '[] 'HReal
e1 a '[] 'HReal
e2 a '[ 'HReal] 'HProb
e3) = a '[] 'HReal -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[] 'HReal
e1 m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` a '[] 'HReal -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[] 'HReal
e2 m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` a '[ 'HReal] 'HProb -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a '[ 'HReal] 'HProb
e3
    --foldMap21 f (WSummate    e1 e2 e3) = f e1 `mappend` f e2 `mappend` f e3

instance Traversable21 Head where
    traverse21 :: (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> Head a j -> f (Head b j)
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
_ (WLiteral    Literal j
v)        = Head b j -> f (Head b j)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Head b j -> f (Head b j)) -> Head b j -> f (Head b j)
forall a b. (a -> b) -> a -> b
$ Literal j -> Head b j
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Head abt a
WLiteral Literal j
v
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (WDatum      Datum (a '[]) (HData' t)
d)        = Datum (b '[]) (HData' t) -> Head b j
forall (abt :: [Hakaru] -> Hakaru -> *) (t :: HakaruCon).
Datum (abt '[]) (HData' t) -> Head abt (HData' t)
WDatum (Datum (b '[]) (HData' t) -> Head b j)
-> f (Datum (b '[]) (HData' t)) -> f (Head b j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (i :: Hakaru). a '[] i -> f (b '[] i))
-> Datum (a '[]) (HData' t) -> f (Datum (b '[]) (HData' t))
forall k1 k2 (t :: (k1 -> *) -> k2 -> *) (f :: * -> *)
       (a :: k1 -> *) (b :: k1 -> *) (j :: k2).
(Traversable11 t, Applicative f) =>
(forall (i :: k1). a i -> f (b i)) -> t a j -> f (t b j)
traverse11 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
forall (i :: Hakaru). a '[] i -> f (b '[] i)
f Datum (a '[]) (HData' t)
d
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
_ (WEmpty      Sing ('HArray a)
typ)      = Head b ('HArray a) -> f (Head b ('HArray a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Head b ('HArray a) -> f (Head b ('HArray a)))
-> Head b ('HArray a) -> f (Head b ('HArray a))
forall a b. (a -> b) -> a -> b
$ Sing ('HArray a) -> Head b ('HArray a)
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Sing ('HArray a) -> Head abt ('HArray a)
WEmpty Sing ('HArray a)
typ
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (WArray      a '[] 'HNat
e1 a '[ 'HNat] a
e2)    = b '[] 'HNat -> b '[ 'HNat] a -> Head b ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] 'HNat -> abt '[ 'HNat] a -> Head abt ('HArray a)
WArray (b '[] 'HNat -> b '[ 'HNat] a -> Head b ('HArray a))
-> f (b '[] 'HNat) -> f (b '[ 'HNat] a -> Head b ('HArray a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a '[] 'HNat -> f (b '[] 'HNat)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[] 'HNat
e1 f (b '[ 'HNat] a -> Head b ('HArray a))
-> f (b '[ 'HNat] a) -> f (Head b ('HArray a))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a '[ 'HNat] a -> f (b '[ 'HNat] a)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[ 'HNat] a
e2
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (WArrayLiteral  [a '[] a]
es)    = [b '[] a] -> Head b ('HArray a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
[abt '[] a] -> Head abt ('HArray a)
WArrayLiteral ([b '[] a] -> Head b ('HArray a))
-> f [b '[] a] -> f (Head b ('HArray a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a '[] a -> f (b '[] a)) -> [a '[] a] -> f [b '[] a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a '[] a -> f (b '[] a)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f [a '[] a]
es
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (WLam        a '[a] b
e1)       = b '[a] b -> Head b (a ':-> b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (typs :: Hakaru).
abt '[a] typs -> Head abt (a ':-> typs)
WLam (b '[a] b -> Head b (a ':-> b))
-> f (b '[a] b) -> f (Head b (a ':-> b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a '[a] b -> f (b '[a] b)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[a] b
e1
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (WMeasureOp  MeasureOp typs a
o  SArgs a args
es)    = MeasureOp typs a -> SArgs b args -> Head b ('HMeasure a)
forall (typs :: [Hakaru]) (args :: [([Hakaru], Hakaru)])
       (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
(typs ~ UnLCs args, args ~ LCs typs) =>
MeasureOp typs a -> SArgs abt args -> Head abt ('HMeasure a)
WMeasureOp MeasureOp typs a
o (SArgs b args -> Head b ('HMeasure a))
-> f (SArgs b args) -> f (Head b ('HMeasure a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> SArgs a args -> f (SArgs b args)
forall k1 k2 k3 (t :: (k1 -> k2 -> *) -> k3 -> *) (f :: * -> *)
       (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
(Traversable21 t, Applicative f) =>
(forall (h :: k1) (i :: k2). a h i -> f (b h i))
-> t a j -> f (t b j)
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f SArgs a args
es
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (WDirac      a '[] a
e1)       = b '[] a -> Head b ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Head abt ('HMeasure a)
WDirac (b '[] a -> Head b ('HMeasure a))
-> f (b '[] a) -> f (Head b ('HMeasure a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a '[] a -> f (b '[] a)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[] a
e1
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (WMBind      a '[] ('HMeasure a)
e1 a '[a] ('HMeasure b)
e2)    = b '[] ('HMeasure a) -> b '[a] ('HMeasure b) -> Head b ('HMeasure b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
abt '[] ('HMeasure a)
-> abt '[a] ('HMeasure b) -> Head abt ('HMeasure b)
WMBind (b '[] ('HMeasure a)
 -> b '[a] ('HMeasure b) -> Head b ('HMeasure b))
-> f (b '[] ('HMeasure a))
-> f (b '[a] ('HMeasure b) -> Head b ('HMeasure b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a '[] ('HMeasure a) -> f (b '[] ('HMeasure a))
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[] ('HMeasure a)
e1 f (b '[a] ('HMeasure b) -> Head b ('HMeasure b))
-> f (b '[a] ('HMeasure b)) -> f (Head b ('HMeasure b))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a '[a] ('HMeasure b) -> f (b '[a] ('HMeasure b))
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[a] ('HMeasure b)
e2
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (WPlate      a '[] 'HNat
e1 a '[ 'HNat] ('HMeasure a)
e2)    = b '[] 'HNat
-> b '[ 'HNat] ('HMeasure a) -> Head b ('HMeasure ('HArray a))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] 'HNat
-> abt '[ 'HNat] ('HMeasure a) -> Head abt ('HMeasure ('HArray a))
WPlate (b '[] 'HNat
 -> b '[ 'HNat] ('HMeasure a) -> Head b ('HMeasure ('HArray a)))
-> f (b '[] 'HNat)
-> f (b '[ 'HNat] ('HMeasure a) -> Head b ('HMeasure ('HArray a)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a '[] 'HNat -> f (b '[] 'HNat)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[] 'HNat
e1 f (b '[ 'HNat] ('HMeasure a) -> Head b ('HMeasure ('HArray a)))
-> f (b '[ 'HNat] ('HMeasure a))
-> f (Head b ('HMeasure ('HArray a)))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a '[ 'HNat] ('HMeasure a) -> f (b '[ 'HNat] ('HMeasure a))
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[ 'HNat] ('HMeasure a)
e2
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (WChain      a '[] 'HNat
e1 a '[] s
e2 a '[s] ('HMeasure (HPair a s))
e3) = b '[] 'HNat
-> b '[] s
-> b '[s] ('HMeasure (HPair a s))
-> Head b ('HMeasure (HPair ('HArray a) s))
forall (abt :: [Hakaru] -> Hakaru -> *) (s :: Hakaru)
       (a :: Hakaru).
abt '[] 'HNat
-> abt '[] s
-> abt '[s] ('HMeasure (HPair a s))
-> Head abt ('HMeasure (HPair ('HArray a) s))
WChain (b '[] 'HNat
 -> b '[] s
 -> b '[s] ('HMeasure (HPair a s))
 -> Head b ('HMeasure (HPair ('HArray a) s)))
-> f (b '[] 'HNat)
-> f (b '[] s
      -> b '[s] ('HMeasure (HPair a s))
      -> Head b ('HMeasure (HPair ('HArray a) s)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a '[] 'HNat -> f (b '[] 'HNat)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[] 'HNat
e1 f (b '[] s
   -> b '[s] ('HMeasure (HPair a s))
   -> Head b ('HMeasure (HPair ('HArray a) s)))
-> f (b '[] s)
-> f (b '[s] ('HMeasure (HPair a s))
      -> Head b ('HMeasure (HPair ('HArray a) s)))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a '[] s -> f (b '[] s)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[] s
e2 f (b '[s] ('HMeasure (HPair a s))
   -> Head b ('HMeasure (HPair ('HArray a) s)))
-> f (b '[s] ('HMeasure (HPair a s)))
-> f (Head b ('HMeasure (HPair ('HArray a) s)))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a '[s] ('HMeasure (HPair a s))
-> f (b '[s] ('HMeasure (HPair a s)))
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[s] ('HMeasure (HPair a s))
e3
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (WSuperpose  NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
pes)      = NonEmpty (b '[] 'HProb, b '[] ('HMeasure a))
-> Head b ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> Head abt ('HMeasure a)
WSuperpose (NonEmpty (b '[] 'HProb, b '[] ('HMeasure a))
 -> Head b ('HMeasure a))
-> f (NonEmpty (b '[] 'HProb, b '[] ('HMeasure a)))
-> f (Head b ('HMeasure a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
-> f (NonEmpty (b '[] 'HProb, b '[] ('HMeasure a)))
forall k1 k2 (f :: * -> *) (t :: * -> *) (abt1 :: k1 -> k2 -> *)
       (abt2 :: k1 -> k2 -> *) (xs :: k1) (a :: k2) (ys :: k1) (b :: k2).
(Applicative f, Traversable t) =>
(forall (h :: k1) (i :: k2). abt1 h i -> f (abt2 h i))
-> t (abt1 xs a, abt1 ys b) -> f (t (abt2 xs a, abt2 ys b))
traversePairs forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f NonEmpty (a '[] 'HProb, a '[] ('HMeasure a))
pes
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
_ (WReject     Sing ('HMeasure a)
typ)      = Head b ('HMeasure a) -> f (Head b ('HMeasure a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Head b ('HMeasure a) -> f (Head b ('HMeasure a)))
-> Head b ('HMeasure a) -> f (Head b ('HMeasure a))
forall a b. (a -> b) -> a -> b
$ Sing ('HMeasure a) -> Head b ('HMeasure a)
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Sing ('HMeasure a) -> Head abt ('HMeasure a)
WReject Sing ('HMeasure a)
typ
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (WCoerceTo   Coercion a j
c Head a a
e1)     = Coercion a j -> Head b a -> Head b j
forall (a :: Hakaru) (b :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
Coercion a b -> Head abt a -> Head abt b
WCoerceTo   Coercion a j
c (Head b a -> Head b j) -> f (Head b a) -> f (Head b j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> Head a a -> f (Head b a)
forall k1 k2 k3 (t :: (k1 -> k2 -> *) -> k3 -> *) (f :: * -> *)
       (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
(Traversable21 t, Applicative f) =>
(forall (h :: k1) (i :: k2). a h i -> f (b h i))
-> t a j -> f (t b j)
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f Head a a
e1
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (WUnsafeFrom Coercion j b
c Head a b
e1)     = Coercion j b -> Head b b -> Head b j
forall (a :: Hakaru) (b :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
Coercion a b -> Head abt b -> Head abt a
WUnsafeFrom Coercion j b
c (Head b b -> Head b j) -> f (Head b b) -> f (Head b j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> Head a b -> f (Head b b)
forall k1 k2 k3 (t :: (k1 -> k2 -> *) -> k3 -> *) (f :: * -> *)
       (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
(Traversable21 t, Applicative f) =>
(forall (h :: k1) (i :: k2). a h i -> f (b h i))
-> t a j -> f (t b j)
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f Head a b
e1
    traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (WIntegrate  a '[] 'HReal
e1 a '[] 'HReal
e2 a '[ 'HReal] 'HProb
e3) = b '[] 'HReal
-> b '[] 'HReal -> b '[ 'HReal] 'HProb -> Head b 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
abt '[] 'HReal
-> abt '[] 'HReal -> abt '[ 'HReal] 'HProb -> Head abt 'HProb
WIntegrate (b '[] 'HReal
 -> b '[] 'HReal -> b '[ 'HReal] 'HProb -> Head b 'HProb)
-> f (b '[] 'HReal)
-> f (b '[] 'HReal -> b '[ 'HReal] 'HProb -> Head b 'HProb)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a '[] 'HReal -> f (b '[] 'HReal)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[] 'HReal
e1 f (b '[] 'HReal -> b '[ 'HReal] 'HProb -> Head b 'HProb)
-> f (b '[] 'HReal) -> f (b '[ 'HReal] 'HProb -> Head b 'HProb)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a '[] 'HReal -> f (b '[] 'HReal)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[] 'HReal
e2 f (b '[ 'HReal] 'HProb -> Head b 'HProb)
-> f (b '[ 'HReal] 'HProb) -> f (Head b 'HProb)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a '[ 'HReal] 'HProb -> f (b '[ 'HReal] 'HProb)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a '[ 'HReal] 'HProb
e3
    --traverse21 f (WSummate    e1 e2 e3) = WSummate   <$> f e1 <*> f e2 <*> f e3


----------------------------------------------------------------
-- BUG: haddock doesn't like annotations on GADT constructors. So
-- here we'll avoid using the GADT syntax, even though it'd make
-- the data type declaration prettier\/cleaner.
-- <https://github.com/hakaru-dev/hakaru/issues/6>

-- | Weak head-normal forms are either heads or neutral terms (i.e.,
-- a term whose reduction is blocked on some free variable).
data Whnf (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
    = Head_   !(Head abt a)
    | Neutral !(abt '[] a)
    -- TODO: would it be helpful to track which variable it's blocked
    -- on? To do so we'd need 'GotStuck' to return that info...
    --
    -- TODO: is there some /clean/ way to ensure that the neutral term
    -- is exactly a chain of blocked redexes? That is, we want to be
    -- able to pull out neutral 'Case_' terms; so we want to make sure
    -- they're not wrapped in let-bindings, coercions, etc.

-- | Forget that something is a WHNF.
fromWhnf :: (ABT Term abt) => Whnf abt a -> abt '[] a
fromWhnf :: Whnf abt a -> abt '[] a
fromWhnf (Head_   Head abt a
e) = Head abt a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Head abt a -> abt '[] a
fromHead Head abt a
e
fromWhnf (Neutral abt '[] a
e) = abt '[] a
e


-- | Identify terms which are already heads. N.B., we make no attempt
-- to identify neutral terms, we just massage the type of 'toHead'.
toWhnf :: (ABT Term abt) => abt '[] a -> Maybe (Whnf abt a)
toWhnf :: abt '[] a -> Maybe (Whnf abt a)
toWhnf abt '[] a
e = Head abt a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt a -> Whnf abt a)
-> Maybe (Head abt a) -> Maybe (Whnf abt a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> abt '[] a -> Maybe (Head abt a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Maybe (Head abt a)
toHead abt '[] a
e

-- | Case analysis on 'Whnf' as a combinator.
caseWhnf :: Whnf abt a -> (Head abt a -> r) -> (abt '[] a -> r) -> r
caseWhnf :: Whnf abt a -> (Head abt a -> r) -> (abt '[] a -> r) -> r
caseWhnf (Head_   Head abt a
e) Head abt a -> r
k abt '[] a -> r
_ = Head abt a -> r
k Head abt a
e
caseWhnf (Neutral abt '[] a
e) Head abt a -> r
_ abt '[] a -> r
k = abt '[] a -> r
k abt '[] a
e


-- | Given some WHNF, try to extract a 'Datum' from it.
viewWhnfDatum
    :: (ABT Term abt)
    => Whnf abt (HData' t)
    -> Maybe (Datum (abt '[]) (HData' t))
viewWhnfDatum :: Whnf abt (HData' t) -> Maybe (Datum (abt '[]) (HData' t))
viewWhnfDatum (Head_   Head abt (HData' t)
v) = Datum (abt '[]) (HData' t) -> Maybe (Datum (abt '[]) (HData' t))
forall a. a -> Maybe a
Just (Datum (abt '[]) (HData' t) -> Maybe (Datum (abt '[]) (HData' t)))
-> Datum (abt '[]) (HData' t) -> Maybe (Datum (abt '[]) (HData' t))
forall a b. (a -> b) -> a -> b
$ Head abt (HData' t) -> Datum (abt '[]) (HData' t)
forall (abt :: [Hakaru] -> Hakaru -> *) (t :: HakaruCon).
ABT Term abt =>
Head abt (HData' t) -> Datum (abt '[]) (HData' t)
viewHeadDatum Head abt (HData' t)
v
viewWhnfDatum (Neutral abt '[] (HData' t)
_) = Maybe (Datum (abt '[]) (HData' t))
forall a. Maybe a
Nothing
    -- N.B., we always return Nothing for 'Neutral' terms because of
    -- what 'Neutral' is supposed to mean. If we wanted to be paranoid
    -- then we could use the following code to throw an error if
    -- we're given a \"neutral\" term which is in fact a head
    -- (because that indicates an error in our logic of constructing
    -- 'Neutral' values):
    {-
    caseVarSyn e (const Nothing) $ \t ->
        case t of
        Datum_ d -> error "bad \"neutral\" value!"
        _        -> Nothing
    -}

viewHeadDatum
    :: (ABT Term abt)
    => Head abt (HData' t)
    -> Datum (abt '[]) (HData' t)
viewHeadDatum :: Head abt (HData' t) -> Datum (abt '[]) (HData' t)
viewHeadDatum (WDatum Datum (abt '[]) (HData' t)
d) = Datum (abt '[]) (HData' t)
Datum (abt '[]) (HData' t)
d
viewHeadDatum Head abt (HData' t)
_          = [Char] -> Datum (abt '[]) (HData' t)
forall a. HasCallStack => [Char] -> a
error [Char]
"viewHeadDatum: the impossible happened"


-- Alas, to avoid the orphanage, this instance must live here rather than in Lazy.hs where it more conceptually belongs.
-- TODO: better unify the two cases of Whnf
-- HACK: this instance requires -XUndecidableInstances
instance (ABT Term abt) => Coerce (Whnf abt) where
    coerceTo :: Coercion a b -> Whnf abt a -> Whnf abt b
coerceTo Coercion a b
c Whnf abt a
w =
        case Whnf abt a
w of
        Neutral abt '[] a
e ->
            abt '[] b -> Whnf abt b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral (abt '[] b -> Whnf abt b)
-> (Maybe (abt '[] b) -> abt '[] b)
-> Maybe (abt '[] b)
-> Whnf abt b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. abt '[] b
-> (abt '[] b -> abt '[] b) -> Maybe (abt '[] b) -> abt '[] b
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Coercion a b -> abt '[] a -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Coercion a b -> abt '[] a -> abt '[] b
P.coerceTo_ Coercion a b
c abt '[] a
e) abt '[] b -> abt '[] b
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
                (Maybe (abt '[] b) -> Whnf abt b)
-> Maybe (abt '[] b) -> Whnf abt b
forall a b. (a -> b) -> a -> b
$ abt '[] a
-> (Variable a -> Maybe (abt '[] b))
-> (Term abt a -> Maybe (abt '[] b))
-> Maybe (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 '[] a
e (Maybe (abt '[] b) -> Variable a -> Maybe (abt '[] b)
forall a b. a -> b -> a
const Maybe (abt '[] b)
forall a. Maybe a
Nothing) ((Term abt a -> Maybe (abt '[] b)) -> Maybe (abt '[] b))
-> (Term abt a -> Maybe (abt '[] b)) -> Maybe (abt '[] b)
forall a b. (a -> b) -> a -> b
$ \Term abt a
t ->
                    case Term abt a
t of
                    -- BUG: literals should never be neutral in the first place; but even if we got one, we shouldn't call it neutral after coercing it.
                    Literal_ Literal a
x          -> abt '[] b -> Maybe (abt '[] b)
forall a. a -> Maybe a
Just (abt '[] b -> Maybe (abt '[] b)) -> abt '[] b -> Maybe (abt '[] b)
forall a b. (a -> b) -> a -> b
$ Literal b -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Literal a -> abt '[] a
P.literal_ (Coercion a b -> Literal a -> Literal b
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f a -> f b
coerceTo Coercion a b
c Literal a
x)
                    -- UnsafeFrom_ c' :$ es' -> TODO: cancellation
                    CoerceTo_ Coercion a a
c' :$ SArgs abt args
es' ->
                        case SArgs abt args
es' of
                        abt vars a
e' :* SArgs abt args
End -> abt '[] b -> Maybe (abt '[] b)
forall a. a -> Maybe a
Just (abt '[] b -> Maybe (abt '[] b)) -> abt '[] b -> Maybe (abt '[] b)
forall a b. (a -> b) -> a -> b
$ Coercion a b -> abt '[] a -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Coercion a b -> abt '[] a -> abt '[] b
P.coerceTo_ (Coercion a b
c Coercion a b -> Coercion a a -> Coercion a b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Coercion a a
c') abt vars a
abt '[] a
e'
                    Term abt a
_ -> Maybe (abt '[] b)
forall a. Maybe a
Nothing
        Head_ Head abt a
v ->
            case Head abt a
v of
            WLiteral Literal a
x      -> Head abt b -> Whnf abt b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt b -> Whnf abt b) -> Head abt b -> Whnf abt b
forall a b. (a -> b) -> a -> b
$ Literal b -> Head abt b
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Head abt a
WLiteral (Coercion a b -> Literal a -> Literal b
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f a -> f b
coerceTo Coercion a b
c Literal a
x)
            -- WUnsafeFrom c' v' -> TODO: cancellation
            WCoerceTo Coercion a a
c' Head abt a
v' -> Head abt b -> Whnf abt b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt b -> Whnf abt b) -> Head abt b -> Whnf abt b
forall a b. (a -> b) -> a -> b
$ Coercion a b -> Head abt a -> Head abt b
forall (a :: Hakaru) (b :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
Coercion a b -> Head abt a -> Head abt b
WCoerceTo (Coercion a b
c Coercion a b -> Coercion a a -> Coercion a b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Coercion a a
c') Head abt a
v'
            Head abt a
_               -> Head abt b -> Whnf abt b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt b -> Whnf abt b) -> Head abt b -> Whnf abt b
forall a b. (a -> b) -> a -> b
$ Coercion a b -> Head abt a -> Head abt b
forall (a :: Hakaru) (b :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
Coercion a b -> Head abt a -> Head abt b
WCoerceTo Coercion a b
c Head abt a
v
    
    coerceFrom :: Coercion a b -> Whnf abt b -> Whnf abt a
coerceFrom Coercion a b
c Whnf abt b
w =
        case Whnf abt b
w of
        Neutral abt '[] b
e ->
            abt '[] a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral (abt '[] a -> Whnf abt a)
-> (Maybe (abt '[] a) -> abt '[] a)
-> Maybe (abt '[] a)
-> Whnf 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 '[] a
-> (abt '[] a -> abt '[] a) -> Maybe (abt '[] a) -> abt '[] a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Coercion a b -> abt '[] b -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Coercion a b -> abt '[] b -> abt '[] a
P.unsafeFrom_ Coercion a b
c abt '[] b
e) abt '[] a -> abt '[] a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
                (Maybe (abt '[] a) -> Whnf abt a)
-> Maybe (abt '[] a) -> Whnf abt a
forall a b. (a -> b) -> a -> b
$ abt '[] b
-> (Variable b -> Maybe (abt '[] a))
-> (Term abt b -> Maybe (abt '[] a))
-> Maybe (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 '[] b
e (Maybe (abt '[] a) -> Variable b -> Maybe (abt '[] a)
forall a b. a -> b -> a
const Maybe (abt '[] a)
forall a. Maybe a
Nothing) ((Term abt b -> Maybe (abt '[] a)) -> Maybe (abt '[] a))
-> (Term abt b -> Maybe (abt '[] a)) -> Maybe (abt '[] a)
forall a b. (a -> b) -> a -> b
$ \Term abt b
t ->
                    case Term abt b
t of
                    -- BUG: literals should never be neutral in the first place; but even if we got one, we shouldn't call it neutral after coercing it.
                    Literal_ Literal b
x -> abt '[] a -> Maybe (abt '[] a)
forall a. a -> Maybe a
Just (abt '[] a -> Maybe (abt '[] a)) -> abt '[] a -> Maybe (abt '[] a)
forall a b. (a -> b) -> a -> b
$ Literal a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Literal a -> abt '[] a
P.literal_ (Coercion a b -> Literal b -> Literal a
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f b -> f a
coerceFrom Coercion a b
c Literal b
x)
                    -- CoerceTo_ c' :$ es' -> TODO: cancellation
                    UnsafeFrom_ Coercion b b
c' :$ SArgs abt args
es' ->
                        case SArgs abt args
es' of
                        abt vars a
e' :* SArgs abt args
End -> abt '[] a -> Maybe (abt '[] a)
forall a. a -> Maybe a
Just (abt '[] a -> Maybe (abt '[] a)) -> abt '[] a -> Maybe (abt '[] a)
forall a b. (a -> b) -> a -> b
$ Coercion a b -> abt '[] b -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Coercion a b -> abt '[] b -> abt '[] a
P.unsafeFrom_ (Coercion b b
c' Coercion b b -> Coercion a b -> Coercion a b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Coercion a b
c) abt vars a
abt '[] b
e'
                    Term abt b
_ -> Maybe (abt '[] a)
forall a. Maybe a
Nothing
        Head_ Head abt b
v ->
            case Head abt b
v of
            WLiteral Literal b
x        -> Head abt a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt a -> Whnf abt a) -> Head abt a -> Whnf abt a
forall a b. (a -> b) -> a -> b
$ Literal a -> Head abt a
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Head abt a
WLiteral (Coercion a b -> Literal b -> Literal a
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f b -> f a
coerceFrom Coercion a b
c Literal b
x)
            -- WCoerceTo c' v' -> TODO: cancellation
            WUnsafeFrom Coercion b b
c' Head abt b
v' -> Head abt a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt a -> Whnf abt a) -> Head abt a -> Whnf abt a
forall a b. (a -> b) -> a -> b
$ Coercion a b -> Head abt b -> Head abt a
forall (a :: Hakaru) (b :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
Coercion a b -> Head abt b -> Head abt a
WUnsafeFrom (Coercion b b
c' Coercion b b -> Coercion a b -> Coercion a b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Coercion a b
c) Head abt b
v'
            Head abt b
_                 -> Head abt a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Head abt a -> Whnf abt a
Head_ (Head abt a -> Whnf abt a) -> Head abt a -> Whnf abt a
forall a b. (a -> b) -> a -> b
$ Coercion a b -> Head abt b -> Head abt a
forall (a :: Hakaru) (b :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
Coercion a b -> Head abt b -> Head abt a
WUnsafeFrom Coercion a b
c Head abt b
v


----------------------------------------------------------------
-- BUG: haddock doesn't like annotations on GADT constructors. So
-- here we'll avoid using the GADT syntax, even though it'd make
-- the data type declaration prettier\/cleaner.
-- <https://github.com/hakaru-dev/hakaru/issues/6>

-- | Lazy terms are either thunks (i.e., any term, which we may
-- decide to evaluate later) or are already evaluated to WHNF.
data Lazy (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
    = Whnf_ !(Whnf abt a)
    | Thunk !(abt '[] a)

-- | Forget whether a term has been evaluated to WHNF or not.
fromLazy :: (ABT Term abt) => Lazy abt a -> abt '[] a
fromLazy :: Lazy abt a -> abt '[] a
fromLazy (Whnf_ Whnf abt a
e) = Whnf abt a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Whnf abt a -> abt '[] a
fromWhnf Whnf abt a
e
fromLazy (Thunk abt '[] a
e) = abt '[] a
e

-- | Case analysis on 'Lazy' as a combinator.
caseLazy :: Lazy abt a -> (Whnf abt a -> r) -> (abt '[] a -> r) -> r
caseLazy :: Lazy abt a -> (Whnf abt a -> r) -> (abt '[] a -> r) -> r
caseLazy (Whnf_ Whnf abt a
e) Whnf abt a -> r
k abt '[] a -> r
_ = Whnf abt a -> r
k Whnf abt a
e
caseLazy (Thunk abt '[] a
e) Whnf abt a -> r
_ abt '[] a -> r
k = abt '[] a -> r
k abt '[] a
e

-- | Is the lazy value a variable?
getLazyVariable :: (ABT Term abt) => Lazy abt a -> Maybe (Variable a)
getLazyVariable :: Lazy abt a -> Maybe (Variable a)
getLazyVariable Lazy abt a
e =
    case Lazy abt a
e of
    Whnf_ (Head_   Head abt a
_)  -> Maybe (Variable a)
forall a. Maybe a
Nothing
    Whnf_ (Neutral abt '[] a
e') -> abt '[] a
-> (Variable a -> Maybe (Variable a))
-> (Term abt a -> Maybe (Variable a))
-> Maybe (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 -> Maybe (Variable a)
forall a. a -> Maybe a
Just (Maybe (Variable a) -> Term abt a -> Maybe (Variable a)
forall a b. a -> b -> a
const Maybe (Variable a)
forall a. Maybe a
Nothing)
    Thunk abt '[] a
e'           -> abt '[] a
-> (Variable a -> Maybe (Variable a))
-> (Term abt a -> Maybe (Variable a))
-> Maybe (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 -> Maybe (Variable a)
forall a. a -> Maybe a
Just (Maybe (Variable a) -> Term abt a -> Maybe (Variable a)
forall a b. a -> b -> a
const Maybe (Variable a)
forall a. Maybe a
Nothing)

-- | Boolean-blind variant of 'getLazyVariable'
isLazyVariable :: (ABT Term abt) => Lazy abt a -> Bool
isLazyVariable :: Lazy abt a -> Bool
isLazyVariable = Bool -> (Variable a -> Bool) -> Maybe (Variable a) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> Variable a -> Bool
forall a b. a -> b -> a
const Bool
True) (Maybe (Variable a) -> Bool)
-> (Lazy abt a -> Maybe (Variable a)) -> Lazy abt a -> Bool
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Lazy abt a -> Maybe (Variable a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Lazy abt a -> Maybe (Variable a)
getLazyVariable


-- | Is the lazy value a literal?
getLazyLiteral :: (ABT Term abt) => Lazy abt a -> Maybe (Literal a)
getLazyLiteral :: Lazy abt a -> Maybe (Literal a)
getLazyLiteral Lazy abt a
e =
    case Lazy abt a
e of
    Whnf_ (Head_ (WLiteral Literal a
v)) -> Literal a -> Maybe (Literal a)
forall a. a -> Maybe a
Just Literal a
v
    Whnf_ Whnf abt a
_                    -> Maybe (Literal a)
forall a. Maybe a
Nothing -- by construction
    Thunk abt '[] a
e' ->
        abt '[] a
-> (Variable a -> Maybe (Literal a))
-> (Term abt a -> Maybe (Literal a))
-> Maybe (Literal 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' (Maybe (Literal a) -> Variable a -> Maybe (Literal a)
forall a b. a -> b -> a
const Maybe (Literal a)
forall a. Maybe a
Nothing) ((Term abt a -> Maybe (Literal a)) -> Maybe (Literal a))
-> (Term abt a -> Maybe (Literal a)) -> Maybe (Literal a)
forall a b. (a -> b) -> a -> b
$ \Term abt a
t ->
            case Term abt a
t of
            Literal_ Literal a
v -> Literal a -> Maybe (Literal a)
forall a. a -> Maybe a
Just Literal a
v
            Term abt a
_          -> Maybe (Literal a)
forall a. Maybe a
Nothing

-- | Boolean-blind variant of 'getLazyLiteral'
isLazyLiteral :: (ABT Term abt) => Lazy abt a -> Bool
isLazyLiteral :: Lazy abt a -> Bool
isLazyLiteral = Bool -> (Literal a -> Bool) -> Maybe (Literal a) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> Literal a -> Bool
forall a b. a -> b -> a
const Bool
True) (Maybe (Literal a) -> Bool)
-> (Lazy abt a -> Maybe (Literal a)) -> Lazy abt a -> Bool
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Lazy abt a -> Maybe (Literal a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Lazy abt a -> Maybe (Literal a)
getLazyLiteral

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

-- | A kind for indexing 'Statement' to know whether the statement
-- is pure (and thus can be evaluated in any ambient monad) vs
-- impure (i.e., must be evaluated in the 'HMeasure' monad).
--
-- TODO: better names!
data Purity = Pure | Impure | ExpectP
    deriving (Purity -> Purity -> Bool
(Purity -> Purity -> Bool)
-> (Purity -> Purity -> Bool) -> Eq Purity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Purity -> Purity -> Bool
$c/= :: Purity -> Purity -> Bool
== :: Purity -> Purity -> Bool
$c== :: Purity -> Purity -> Bool
Eq, ReadPrec [Purity]
ReadPrec Purity
Int -> ReadS Purity
ReadS [Purity]
(Int -> ReadS Purity)
-> ReadS [Purity]
-> ReadPrec Purity
-> ReadPrec [Purity]
-> Read Purity
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Purity]
$creadListPrec :: ReadPrec [Purity]
readPrec :: ReadPrec Purity
$creadPrec :: ReadPrec Purity
readList :: ReadS [Purity]
$creadList :: ReadS [Purity]
readsPrec :: Int -> ReadS Purity
$creadsPrec :: Int -> ReadS Purity
Read, Int -> Purity -> ShowS
[Purity] -> ShowS
Purity -> [Char]
(Int -> Purity -> ShowS)
-> (Purity -> [Char]) -> ([Purity] -> ShowS) -> Show Purity
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Purity] -> ShowS
$cshowList :: [Purity] -> ShowS
show :: Purity -> [Char]
$cshow :: Purity -> [Char]
showsPrec :: Int -> Purity -> ShowS
$cshowsPrec :: Int -> Purity -> ShowS
Show)

-- | A type for tracking the arrays under which the term resides
-- This is used as a binding form when we "lift" transformations
-- (currently only Disintegrate) to work on arrays
data Index ast = Ind (Variable 'HNat) (ast 'HNat)

instance (ABT Term abt) => Eq (Index (abt '[])) where
    Ind Variable 'HNat
i1 abt '[] 'HNat
s1 == :: Index (abt '[]) -> Index (abt '[]) -> Bool
== Ind Variable 'HNat
i2 abt '[] 'HNat
s2 = Variable 'HNat
i1 Variable 'HNat -> Variable 'HNat -> Bool
forall a. Eq a => a -> a -> Bool
== Variable 'HNat
i2 Bool -> Bool -> Bool
&& (abt '[] 'HNat -> abt '[] 'HNat -> Bool
forall (abt :: [Hakaru] -> Hakaru -> *) (d :: Hakaru).
ABT Term abt =>
abt '[] d -> abt '[] d -> Bool
alphaEq abt '[] 'HNat
s1 abt '[] 'HNat
s2)

instance (ABT Term abt) => Ord (Index (abt '[])) where
    compare :: Index (abt '[]) -> Index (abt '[]) -> Ordering
compare (Ind Variable 'HNat
i abt '[] 'HNat
_) (Ind Variable 'HNat
j abt '[] 'HNat
_) = Variable 'HNat -> Variable 'HNat -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Variable 'HNat
i Variable 'HNat
j -- TODO check this

indVar :: Index ast -> Variable 'HNat                                 
indVar :: Index ast -> Variable 'HNat
indVar (Ind Variable 'HNat
v ast 'HNat
_ ) = Variable 'HNat
v
          
indSize :: Index ast -> ast 'HNat
indSize :: Index ast -> ast 'HNat
indSize (Ind Variable 'HNat
_ ast 'HNat
a) = ast 'HNat
a

fromIndex :: (ABT Term abt) => Index (abt '[]) -> abt '[] 'HNat
fromIndex :: Index (abt '[]) -> abt '[] 'HNat
fromIndex (Ind Variable 'HNat
v abt '[] 'HNat
_) = Variable 'HNat -> abt '[] 'HNat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable 'HNat
v

-- | Distinguish between variables and heap locations
newtype Location (a :: k) = Location (Variable a)

instance Show (Sing a) => Show (Location a) where
    show :: Location a -> [Char]
show (Location Variable a
v) = Variable a -> [Char]
forall a. Show a => a -> [Char]
show Variable a
v

locHint :: Location a -> Text
locHint :: Location a -> Text
locHint (Location Variable a
x) = Variable a -> Text
forall k (a :: k). Variable a -> Text
varHint Variable a
x

locType :: Location a -> Sing a
locType :: Location a -> Sing a
locType (Location Variable a
x) = Variable a -> Sing a
forall k (a :: k). Variable a -> Sing a
varType Variable a
x

locEq :: (Show1 (Sing :: k -> *), JmEq1 (Sing :: k -> *))
      => Location (a :: k)
      -> Location (b :: k)
      -> Maybe (TypeEq a b)
locEq :: Location a -> Location b -> Maybe (TypeEq a b)
locEq (Location Variable a
a) (Location Variable b
b) = Variable a -> Variable b -> Maybe (TypeEq a b)
forall k (a :: k) (b :: k).
(Show1 Sing, JmEq1 Sing) =>
Variable a -> Variable b -> Maybe (TypeEq a b)
varEq Variable a
a Variable b
b

fromLocation :: Location a -> Variable a
fromLocation :: Location a -> Variable a
fromLocation (Location Variable a
v) = Variable a
v

fromLocations1 :: List1 Location a -> List1 Variable a
fromLocations1 :: List1 Location a -> List1 Variable a
fromLocations1 = (forall (i :: k). Location i -> Variable i)
-> List1 Location a -> List1 Variable a
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *)
       (b :: k1 -> *) (j :: k2).
Functor11 f =>
(forall (i :: k1). a i -> b i) -> f a j -> f b j
fmap11 forall (i :: k). Location i -> Variable i
forall k (a :: k). Location a -> Variable a
fromLocation

locations1 :: List1 Variable a -> List1 Location a
locations1 :: List1 Variable a -> List1 Location a
locations1 = (forall (i :: k). Variable i -> Location i)
-> List1 Variable a -> List1 Location a
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *)
       (b :: k1 -> *) (j :: k2).
Functor11 f =>
(forall (i :: k1). a i -> b i) -> f a j -> f b j
fmap11 forall (i :: k). Variable i -> Location i
forall k (a :: k). Variable a -> Location a
Location

newtype LAssoc ast = LAssoc (Assoc ast)
newtype LAssocs ast = LAssocs (Assocs ast)

emptyLAssocs :: LAssocs abt
emptyLAssocs :: LAssocs abt
emptyLAssocs = Assocs abt -> LAssocs abt
forall k (ast :: k -> *). Assocs ast -> LAssocs ast
LAssocs (Assocs abt
forall k (abt :: k -> *). Assocs abt
emptyAssocs)
    
singletonLAssocs :: Location a -> f a -> LAssocs f
singletonLAssocs :: Location a -> f a -> LAssocs f
singletonLAssocs (Location Variable a
v) f a
e = Assocs f -> LAssocs f
forall k (ast :: k -> *). Assocs ast -> LAssocs ast
LAssocs (Variable a -> f a -> Assocs f
forall k (a :: k) (f :: k -> *). Variable a -> f a -> Assocs f
singletonAssocs Variable a
v f a
e)

toLAssocs1 :: List1 Location xs -> List1 ast xs -> LAssocs ast
toLAssocs1 :: List1 Location xs -> List1 ast xs -> LAssocs ast
toLAssocs1 List1 Location xs
ls List1 ast xs
es = Assocs ast -> LAssocs ast
forall k (ast :: k -> *). Assocs ast -> LAssocs ast
LAssocs (List1 Variable xs -> List1 ast xs -> Assocs ast
forall k (xs :: [k]) (ast :: k -> *).
List1 Variable xs -> List1 ast xs -> Assocs ast
toAssocs1 (List1 Location xs -> List1 Variable xs
forall k (a :: [k]). List1 Location a -> List1 Variable a
fromLocations1 List1 Location xs
ls) List1 ast xs
es)

insertLAssocs :: LAssocs ast -> LAssocs ast -> LAssocs ast
insertLAssocs :: LAssocs ast -> LAssocs ast -> LAssocs ast
insertLAssocs (LAssocs Assocs ast
a) (LAssocs Assocs ast
b) = Assocs ast -> LAssocs ast
forall k (ast :: k -> *). Assocs ast -> LAssocs ast
LAssocs (Assocs ast -> Assocs ast -> Assocs ast
forall k (ast :: k -> *). Assocs ast -> Assocs ast -> Assocs ast
insertAssocs Assocs ast
a Assocs ast
b)

lookupLAssoc :: (Show1 (Sing :: k -> *), JmEq1 (Sing :: k -> *))
             => Location (a :: k)
             -> LAssocs ast
             -> Maybe (ast a)
lookupLAssoc :: Location a -> LAssocs ast -> Maybe (ast a)
lookupLAssoc (Location Variable a
v) (LAssocs Assocs ast
a) = Variable a -> Assocs ast -> Maybe (ast a)
forall k (a :: k) (ast :: k -> *).
(Show1 Sing, JmEq1 Sing) =>
Variable a -> Assocs ast -> Maybe (ast a)
lookupAssoc Variable a
v Assocs ast
a
                                  
-- | A single statement in some ambient monad (specified by the @p@
-- type index). In particular, note that the the first argument to
-- 'MBind' (or 'Let_') together with the variable bound in the
-- second argument forms the \"statement\" (leaving out the body
-- of the second argument, which may be part of a following statement).
-- In addition to these binding constructs, we also include a few
-- non-binding statements like 'SWeight'.
--
-- Statements are parameterized by the type of the bound element,
-- which (if present) is either a Variable or a Location.
-- 
-- The semantics of this type are as follows. Let @ss :: [Statement
-- abt v p]@ be a sequence of statements. We have @Γ@: the collection
-- of all free variables that occur in the term expressions in @ss@,
-- viewed as a measureable space (namely the product of the measureable
-- spaces for each variable). And we have @Δ@: the collection of
-- all variables bound by the statements in @ss@, also viewed as a
-- measurable space. The semantic interpretation of @ss@ is a
-- measurable function of type @Γ ':-> M Δ@ where @M@ is either
-- @HMeasure@ (if @p ~ 'Impure@) or @Identity@ (if @p ~ 'Pure@).
data Statement :: ([Hakaru] -> Hakaru -> *) -> (Hakaru -> *) -> Purity -> * where
    -- BUG: haddock doesn't like annotations on GADT constructors. So we can't make the constructor descriptions below available to Haddock.
    -- <https://github.com/hakaru-dev/hakaru/issues/6>
    
    -- A variable bound by 'MBind' to a measure expression.
    SBind
        :: forall abt (v :: Hakaru -> *) (a :: Hakaru)
        .  {-# UNPACK #-} !(v a)
        -> !(Lazy abt ('HMeasure a))
        -> [Index (abt '[])]
        -> Statement abt v 'Impure

    -- A variable bound by 'Let_' to an expression.
    SLet
        :: forall abt p (v :: Hakaru -> *) (a :: Hakaru)
        .  {-# UNPACK #-} !(v a)
        -> !(Lazy abt a)
        -> [Index (abt '[])]
        -> Statement abt v p


    -- A weight; i.e., the first component of each argument to
    -- 'Superpose_'. This is a statement just so that we can avoid
    -- needing to atomize the weight itself.
    SWeight
        :: forall abt (v :: Hakaru -> *)
        .  !(Lazy abt 'HProb)
        -> [Index (abt '[])]
        -> Statement abt v 'Impure

    -- A monadic guard statement. If the scrutinee matches the
    -- pattern, then we bind the variables as usual; otherwise, we
    -- return the empty measure. N.B., this statement type is only
    -- for capturing constraints that some pattern matches /in a/
    -- /monadic context/. In pure contexts we should be able to
    -- handle case analysis without putting anything onto the heap.
    SGuard
        :: forall abt (v :: Hakaru -> *) (xs :: [Hakaru]) (a :: Hakaru)
        .  !(List1 v xs)
        -> !(Pattern xs a)
        -> !(Lazy abt a)
        -> [Index (abt '[])]
        -> Statement abt v 'Impure

    -- Some arbitrary pure code. This is a statement just so that we can avoid needing to atomize the stuff in the pure code.
    --
    -- TODO: real names for these.
    -- TODO: generalize to use a 'VarSet' so we can collapse these
    -- TODO: defunctionalize? These break pretty printing...
    SStuff0
        :: forall abt (v :: Hakaru -> *)
        .  (abt '[] 'HProb -> abt '[] 'HProb)
        -> [Index (abt '[])]
        -> Statement abt v 'ExpectP
    SStuff1
        :: forall abt (v :: Hakaru -> *) (a :: Hakaru)
        . {-# UNPACK #-} !(v a)
        -> (abt '[] 'HProb -> abt '[] 'HProb)
        -> [Index (abt '[])]
        -> Statement abt v 'ExpectP

statementVars :: Statement abt Location p -> VarSet ('KProxy :: KProxy Hakaru)
statementVars :: Statement abt Location p -> VarSet 'KProxy
statementVars (SBind Location a
x Lazy abt ('HMeasure a)
_ [Index (abt '[])]
_)     = Variable a -> VarSet 'KProxy
forall k (a :: k). Variable a -> VarSet (KindOf a)
singletonVarSet (Location a -> Variable a
forall k (a :: k). Location a -> Variable a
fromLocation Location a
x)
statementVars (SLet  Location a
x Lazy abt a
_ [Index (abt '[])]
_)     = Variable a -> VarSet 'KProxy
forall k (a :: k). Variable a -> VarSet (KindOf a)
singletonVarSet (Location a -> Variable a
forall k (a :: k). Location a -> Variable a
fromLocation Location a
x)
statementVars (SWeight Lazy abt 'HProb
_ [Index (abt '[])]
_)     = VarSet 'KProxy
forall k (kproxy :: KProxy k). VarSet kproxy
emptyVarSet
statementVars (SGuard List1 Location xs
xs Pattern xs a
_ Lazy abt a
_ [Index (abt '[])]
_) = List1 Variable xs -> VarSet 'KProxy
forall k (xs :: [k]) (kproxy :: KProxy k).
List1 Variable xs -> VarSet kproxy
toVarSet1 (List1 Location xs -> List1 Variable xs
forall k (a :: [k]). List1 Location a -> List1 Variable a
fromLocations1 List1 Location xs
xs)
statementVars (SStuff0   abt '[] 'HProb -> abt '[] 'HProb
_ [Index (abt '[])]
_)   = VarSet 'KProxy
forall k (kproxy :: KProxy k). VarSet kproxy
emptyVarSet
statementVars (SStuff1 Location a
x abt '[] 'HProb -> abt '[] 'HProb
_ [Index (abt '[])]
_)   = Variable a -> VarSet 'KProxy
forall k (a :: k). Variable a -> VarSet (KindOf a)
singletonVarSet (Location a -> Variable a
forall k (a :: k). Location a -> Variable a
fromLocation Location a
x)

-- | Is the Location bound by the statement?
--
-- We return @Maybe ()@ rather than @Bool@ because in our primary
-- use case we're already in the @Maybe@ monad and so it's easier
-- to just stick with that. If we find other situations where we'd
-- really rather have the @Bool@, then we can easily change things
-- and use some @boolToMaybe@ function to do the coercion wherever
-- needed.
isBoundBy :: Location (a :: Hakaru) -> Statement abt Location p -> Maybe ()
Location a
x isBoundBy :: Location a -> Statement abt Location p -> Maybe ()
`isBoundBy` SBind  Location a
y  Lazy abt ('HMeasure a)
_ [Index (abt '[])]
_   = () -> TypeEq a a -> ()
forall a b. a -> b -> a
const () (TypeEq a a -> ()) -> Maybe (TypeEq a a) -> Maybe ()
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Location a -> Location a -> Maybe (TypeEq a a)
forall k (a :: k) (b :: k).
(Show1 Sing, JmEq1 Sing) =>
Location a -> Location b -> Maybe (TypeEq a b)
locEq Location a
x Location a
y
Location a
x `isBoundBy` SLet   Location a
y  Lazy abt a
_ [Index (abt '[])]
_   = () -> TypeEq a a -> ()
forall a b. a -> b -> a
const () (TypeEq a a -> ()) -> Maybe (TypeEq a a) -> Maybe ()
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Location a -> Location a -> Maybe (TypeEq a a)
forall k (a :: k) (b :: k).
(Show1 Sing, JmEq1 Sing) =>
Location a -> Location b -> Maybe (TypeEq a b)
locEq Location a
x Location a
y
Location a
_ `isBoundBy` SWeight   Lazy abt 'HProb
_ [Index (abt '[])]
_   = Maybe ()
forall a. Maybe a
Nothing
Location a
x `isBoundBy` SGuard List1 Location xs
ys Pattern xs a
_ Lazy abt a
_ [Index (abt '[])]
_ =
    -- TODO: just check membership directly, rather than going through VarSet
    if Variable a -> VarSet Any -> Bool
forall k (a :: k) (kproxy :: KProxy k).
(Show1 Sing, JmEq1 Sing) =>
Variable a -> VarSet kproxy -> Bool
memberVarSet (Location a -> Variable a
forall k (a :: k). Location a -> Variable a
fromLocation Location a
x) (List1 Variable xs -> VarSet Any
forall k (xs :: [k]) (kproxy :: KProxy k).
List1 Variable xs -> VarSet kproxy
toVarSet1 ((forall (i :: Hakaru). Location i -> Variable i)
-> List1 Location xs -> List1 Variable 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 (a :: k). Location a -> Variable a
forall (i :: Hakaru). Location i -> Variable i
fromLocation List1 Location xs
ys))
    then () -> Maybe ()
forall a. a -> Maybe a
Just ()
    else Maybe ()
forall a. Maybe a
Nothing
Location a
_ `isBoundBy` SStuff0   abt '[] 'HProb -> abt '[] 'HProb
_ [Index (abt '[])]
_   = Maybe ()
forall a. Maybe a
Nothing
Location a
x `isBoundBy` SStuff1 Location a
y abt '[] 'HProb -> abt '[] 'HProb
_ [Index (abt '[])]
_   = () -> TypeEq a a -> ()
forall a b. a -> b -> a
const () (TypeEq a a -> ()) -> Maybe (TypeEq a a) -> Maybe ()
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Location a -> Location a -> Maybe (TypeEq a a)
forall k (a :: k) (b :: k).
(Show1 Sing, JmEq1 Sing) =>
Location a -> Location b -> Maybe (TypeEq a b)
locEq Location a
x Location a
y


-- TODO: remove this CPP guard, provided we don't end up with a cyclic dependency...
#ifdef __TRACE_DISINTEGRATE__
instance (ABT Term abt) => Pretty (Whnf abt) where
    prettyPrec_ p (Head_   w) = ppApply1 p "Head_" (fromHead w) -- HACK
    prettyPrec_ p (Neutral e) = ppApply1 p "Neutral" e

instance (ABT Term abt) => Pretty (Lazy abt) where
    prettyPrec_ p (Whnf_ w) = ppFun p "Whnf_" [PP.sep (prettyPrec_ 11 w)]
    prettyPrec_ p (Thunk e) = ppApply1 p "Thunk" e

ppApply1 :: (ABT Term abt) => Int -> String -> abt '[] a -> [PP.Doc]
ppApply1 p f e1 =
    let d = PP.text f PP.<+> PP.nest (1 + length f) (prettyPrec 11 e1)
    in [if p > 9 then PP.parens (PP.nest 1 d) else d]

ppFun :: Int -> String -> [PP.Doc] -> [PP.Doc]
ppFun _ f [] = [PP.text f]
ppFun p f ds =
    parens (p > 9) [PP.text f PP.<+> PP.nest (1 + length f) (PP.sep ds)]

parens :: Bool -> [PP.Doc] -> [PP.Doc]
parens True  ds = [PP.parens (PP.nest 1 (PP.sep ds))]
parens False ds = ds

ppList :: [PP.Doc] -> PP.Doc
ppList = PP.sep . (:[]) . PP.brackets . PP.nest 1 . PP.fsep . PP.punctuate PP.comma

ppInds :: (ABT Term abt) => [Index (abt '[])] -> PP.Doc
ppInds = ppList . map (ppVariable . indVar)

ppStatement :: (ABT Term abt) => Int -> Statement abt Location p -> PP.Doc
ppStatement p s =
    case s of
    SBind (Location x) e inds ->
        PP.sep $ ppFun p "SBind"
            [ ppVariable x
            , PP.sep $ prettyPrec_ 11 e
            , ppInds inds
            ]
    SLet (Location x) e inds ->
        PP.sep $ ppFun p "SLet"
            [ ppVariable x
            , PP.sep $ prettyPrec_ 11 e
            , ppInds inds
            ]
    SWeight e inds ->
        PP.sep $ ppFun p "SWeight"
            [ PP.sep $ prettyPrec_ 11 e
            , ppInds inds
            ]
    SGuard xs pat e inds ->
        PP.sep $ ppFun p "SGuard"
            [ PP.sep $ ppVariables (fromLocations1 xs)
            , PP.sep $ prettyPrec_ 11 pat
            , PP.sep $ prettyPrec_ 11 e
            , ppInds inds
            ]
    SStuff0   _ _ ->
        PP.sep $ ppFun p "SStuff0"
            [ PP.text "TODO: ppStatement{SStuff0}"
            ]
    SStuff1 _ _ _ ->
        PP.sep $ ppFun p "SStuff1"
            [ PP.text "TODO: ppStatement{SStuff1}"
            ]

pretty_Statements :: (ABT Term abt) => [Statement abt Location p] -> PP.Doc
pretty_Statements []     = PP.text "[]"
pretty_Statements (s:ss) =
    foldl
        (\d s' -> d PP.$+$ PP.comma PP.<+> ppStatement 0 s')
        (PP.text "[" PP.<+> ppStatement 0 s)
        ss
    PP.$+$ PP.text "]"

pretty_Statements_withTerm
    :: (ABT Term abt) => [Statement abt Location p] -> abt '[] a -> PP.Doc
pretty_Statements_withTerm ss e =
    pretty_Statements ss PP.$+$ pretty e

prettyAssocs
    :: (ABT Term abt)
    => Assocs (abt '[])
    -> PP.Doc
prettyAssocs a = PP.vcat $ map go (fromAssocs a)
  where go (Assoc x e) = ppVariable x PP.<+>
                         PP.text "->" PP.<+>
                         pretty e
                                
#endif


-----------------------------------------------------------------
-- | A function for evaluating any term to weak-head normal form.
type TermEvaluator abt m =
    forall a. abt '[] a -> m (Whnf abt a)

-- | A function for \"performing\" an 'HMeasure' monadic action.
-- This could mean actual random sampling, or simulated sampling
-- by generating a new term and returning the newly bound variable,
-- or anything else.
type MeasureEvaluator abt m =
    forall a. abt '[] ('HMeasure a) -> m (Whnf abt a)

-- | A function for evaluating any case-expression to weak-head
-- normal form.
type CaseEvaluator abt m =
    forall a b. abt '[] a -> [Branch a abt b] -> m (Whnf abt b)

-- | A function for evaluating any variable to weak-head normal form.
type VariableEvaluator abt m =
    forall a. Variable a -> m (Whnf abt a)
                            

----------------------------------------------------------------
-- | This class captures the monadic operations needed by the
-- 'evaluate' function in "Language.Hakaru.Lazy".
class (Functor m, Applicative m, Monad m, ABT Term abt)
    => EvaluationMonad abt m p | m -> abt p
    where
    -- TODO: should we have a *method* for arbitrarily incrementing the stored 'nextFreshNat'; or should we only rely on it being initialized correctly? Beware correctness issues about updating the lower bound after having called 'freshNat'...

    -- | Return a fresh natural number. That is, a number which is
    -- not the 'varID' of any free variable in the expressions of
    -- interest, and isn't a number we've returned previously.
    freshNat :: m Nat


    -- | Internal function for renaming the variables bound by a
    -- statement. We return the renamed statement along with a substitution
    -- for mapping the old variable names to their new variable names.
    freshLocStatement
        :: Statement abt Variable p
        -> m (Statement abt Location p, Assocs (Variable :: Hakaru -> *))
    freshLocStatement Statement abt Variable p
s =
        case Statement abt Variable p
s of
          SWeight Lazy abt 'HProb
w [Index (abt '[])]
e    -> (Statement abt Location 'Impure, Assocs Variable)
-> m (Statement abt Location 'Impure, Assocs Variable)
forall (m :: * -> *) a. Monad m => a -> m a
return (Lazy abt 'HProb
-> [Index (abt '[])] -> Statement abt Location 'Impure
forall (abt :: [Hakaru] -> Hakaru -> *) (v :: Hakaru -> *).
Lazy abt 'HProb -> [Index (abt '[])] -> Statement abt v 'Impure
SWeight Lazy abt 'HProb
w [Index (abt '[])]
e, Assocs Variable
forall a. Monoid a => a
mempty)
          SBind Variable a
x Lazy abt ('HMeasure a)
body [Index (abt '[])]
i -> do
               Variable a
x' <- Variable a -> m (Variable a)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
       (a :: Hakaru).
EvaluationMonad abt m p =>
Variable a -> m (Variable a)
freshenVar Variable a
x
               (Statement abt Location 'Impure, Assocs Variable)
-> m (Statement abt Location 'Impure, Assocs Variable)
forall (m :: * -> *) a. Monad m => a -> m a
return (Location a
-> Lazy abt ('HMeasure a)
-> [Index (abt '[])]
-> Statement abt Location 'Impure
forall (abt :: [Hakaru] -> Hakaru -> *) (v :: Hakaru -> *)
       (a :: Hakaru).
v a
-> Lazy abt ('HMeasure a)
-> [Index (abt '[])]
-> Statement abt v 'Impure
SBind (Variable a -> Location a
forall k (a :: k). Variable a -> Location a
Location Variable a
x') Lazy abt ('HMeasure a)
body [Index (abt '[])]
i, Variable a -> Variable a -> Assocs Variable
forall k (a :: k) (f :: k -> *). Variable a -> f a -> Assocs f
singletonAssocs Variable a
x Variable a
x')
          SLet Variable a
x  Lazy abt a
body [Index (abt '[])]
i -> do
               Variable a
x' <- Variable a -> m (Variable a)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
       (a :: Hakaru).
EvaluationMonad abt m p =>
Variable a -> m (Variable a)
freshenVar Variable a
x
               (Statement abt Location p, Assocs Variable)
-> m (Statement abt Location p, Assocs Variable)
forall (m :: * -> *) a. Monad m => a -> m a
return (Location a
-> Lazy abt a -> [Index (abt '[])] -> Statement abt Location p
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity)
       (v :: Hakaru -> *) (a :: Hakaru).
v a -> Lazy abt a -> [Index (abt '[])] -> Statement abt v p
SLet (Variable a -> Location a
forall k (a :: k). Variable a -> Location a
Location Variable a
x') Lazy abt a
body [Index (abt '[])]
i, Variable a -> Variable a -> Assocs Variable
forall k (a :: k) (f :: k -> *). Variable a -> f a -> Assocs f
singletonAssocs Variable a
x Variable a
x')
          SGuard List1 Variable xs
xs Pattern xs a
pat Lazy abt a
scrutinee [Index (abt '[])]
i -> do
               List1 Variable xs
xs' <- List1 Variable xs -> 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
xs
               (Statement abt Location 'Impure, Assocs Variable)
-> m (Statement abt Location 'Impure, Assocs Variable)
forall (m :: * -> *) a. Monad m => a -> m a
return (List1 Location xs
-> Pattern xs a
-> Lazy abt a
-> [Index (abt '[])]
-> Statement abt Location 'Impure
forall (abt :: [Hakaru] -> Hakaru -> *) (v :: Hakaru -> *)
       (xs :: [Hakaru]) (a :: Hakaru).
List1 v xs
-> Pattern xs a
-> Lazy abt a
-> [Index (abt '[])]
-> Statement abt v 'Impure
SGuard (List1 Variable xs -> List1 Location xs
forall k (a :: [k]). List1 Variable a -> List1 Location a
locations1 List1 Variable xs
xs') Pattern xs a
pat Lazy abt a
scrutinee [Index (abt '[])]
i,
                       List1 Variable xs -> List1 Variable xs -> Assocs Variable
forall k (xs :: [k]) (ast :: k -> *).
List1 Variable xs -> List1 ast xs -> Assocs ast
toAssocs1 List1 Variable xs
xs List1 Variable xs
xs')
          SStuff0   abt '[] 'HProb -> abt '[] 'HProb
e [Index (abt '[])]
e' -> (Statement abt Location 'ExpectP, Assocs Variable)
-> m (Statement abt Location 'ExpectP, Assocs Variable)
forall (m :: * -> *) a. Monad m => a -> m a
return ((abt '[] 'HProb -> abt '[] 'HProb)
-> [Index (abt '[])] -> Statement abt Location 'ExpectP
forall (abt :: [Hakaru] -> Hakaru -> *) (v :: Hakaru -> *).
(abt '[] 'HProb -> abt '[] 'HProb)
-> [Index (abt '[])] -> Statement abt v 'ExpectP
SStuff0 abt '[] 'HProb -> abt '[] 'HProb
e [Index (abt '[])]
e', Assocs Variable
forall a. Monoid a => a
mempty)
          SStuff1 Variable a
x abt '[] 'HProb -> abt '[] 'HProb
f [Index (abt '[])]
i -> do
               Variable a
x' <- Variable a -> m (Variable a)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
       (a :: Hakaru).
EvaluationMonad abt m p =>
Variable a -> m (Variable a)
freshenVar Variable a
x
               (Statement abt Location 'ExpectP, Assocs Variable)
-> m (Statement abt Location 'ExpectP, Assocs Variable)
forall (m :: * -> *) a. Monad m => a -> m a
return (Location a
-> (abt '[] 'HProb -> abt '[] 'HProb)
-> [Index (abt '[])]
-> Statement abt Location 'ExpectP
forall (abt :: [Hakaru] -> Hakaru -> *) (v :: Hakaru -> *)
       (a :: Hakaru).
v a
-> (abt '[] 'HProb -> abt '[] 'HProb)
-> [Index (abt '[])]
-> Statement abt v 'ExpectP
SStuff1 (Variable a -> Location a
forall k (a :: k). Variable a -> Location a
Location Variable a
x') abt '[] 'HProb -> abt '[] 'HProb
f [Index (abt '[])]
i, Variable a -> Variable a -> Assocs Variable
forall k (a :: k) (f :: k -> *). Variable a -> f a -> Assocs f
singletonAssocs Variable a
x Variable a
x')


    -- | Returns the current Indices. Currently, this is only
    -- applicable to the Disintegration Monad, but could be
    -- relevant as other partial evaluators begin to handle
    -- Plate and Array
    getIndices :: m [Index (abt '[])]
    getIndices =  [Index (abt '[])] -> m [Index (abt '[])]
forall (m :: * -> *) a. Monad m => a -> m a
return []

    -- | Add a statement to the top of the context. This is unsafe
    -- because it may allow confusion between variables with the
    -- same name but different scopes (thus, may allow variable
    -- capture). Prefer using 'push_', 'push', or 'pushes'.
    unsafePush :: Statement abt Location p -> m ()

    -- | Call 'unsafePush' repeatedly. Is part of the class since
    -- we may be able to do this more efficiently than actually
    -- calling 'unsafePush' repeatedly.
    --
    -- N.B., this should push things in the same order as 'pushes'
    -- does.
    unsafePushes :: [Statement abt Location p] -> m ()
    unsafePushes = (Statement abt Location p -> m ())
-> [Statement abt Location p] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Statement abt Location p -> m ()
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
       (p :: Purity).
EvaluationMonad abt m p =>
Statement abt Location p -> m ()
unsafePush

    -- | Look for the statement @s@ binding the variable. If found,
    -- then call the continuation with @s@ in the context where @s@
    -- itself and everything @s@ (transitively)depends on is included
    -- but everything that (transitively)depends on @s@ is excluded;
    -- thus, the continuation may only alter the dependencies of
    -- @s@. After the continuation returns, restore all the bindings
    -- that were removed before calling the continuation. If no
    -- such @s@ can be found, then return 'Nothing' without altering
    -- the context at all.
    --
    -- N.B., the statement @s@ itself is popped! Thus, it is up to
    -- the continuation to make sure to push new statements that
    -- bind /all/ the variables bound by @s@!
    --
    -- TODO: pass the continuation more detail, so it can avoid
    -- needing to be in the 'Maybe' monad due to the redundant call
    -- to 'varEq' in the continuation. In particular, we want to
    -- do this so that we can avoid the return type @m (Maybe (Maybe r))@
    -- while still correctly handling statements like 'SStuff1'
    -- which (a) do bind variables and thus should shadow bindings
    -- further up the 'ListContext', but which (b) offer up no
    -- expression the variable is bound to, and thus cannot be
    -- altered by forcing etc. To do all this, we need to pass the
    -- 'TypeEq' proof from (the 'varEq' call in) the 'isBoundBy'
    -- call in the instance; but that means we also need some way
    -- of tying it together with the existential variable in the
    -- 'Statement'. Perhaps we should have an alternative statement
    -- type which exposes the existential?
    select
        :: Location (a :: Hakaru)
        -> (Statement abt Location p -> Maybe (m r))
        -> m (Maybe r)

    substVar :: Variable a -> abt '[] a
             -> (forall b'. Variable b' -> m (abt '[] b'))
    substVar Variable a
_ abt '[] a
_ = abt '[] b' -> m (abt '[] b')
forall (m :: * -> *) a. Monad m => a -> m a
return (abt '[] b' -> m (abt '[] b'))
-> (Variable b' -> abt '[] b') -> Variable b' -> m (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 b' -> abt '[] b'
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var


    extFreeVars :: abt xs a -> m (VarSet (KindOf a))
    extFreeVars abt xs a
e = VarSet 'KProxy -> m (VarSet 'KProxy)
forall (m :: * -> *) a. Monad m => a -> m a
return (abt xs a -> VarSet 'KProxy
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> VarSet (KindOf a)
freeVars abt xs a
e)


    -- The first argument to @evaluateCase@ will be the
    -- 'TermEvaluator' we're constructing (thus tying the knot).
    evaluateCase :: TermEvaluator abt m -> CaseEvaluator abt m
    {-# INLINE evaluateCase #-}
    evaluateCase = TermEvaluator abt m
-> abt '[] a -> [Branch a abt b] -> m (Whnf abt b)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
       (p :: Purity).
(ABT Term abt, EvaluationMonad abt m p) =>
TermEvaluator abt m -> CaseEvaluator abt m
defaultCaseEvaluator

               
    -- TODO: figure out how to abstract this so it can be reused by
    -- 'constrainValue'. Especially the 'SBranch case of 'step'
    -- TODO: we could speed up the case for free variables by having
    -- the 'Context' also keep track of the largest free var. That way,
    -- we can just check up front whether @varID x < nextFreeVarID@.
    -- Of course, we'd have to make sure we've sufficiently renamed all
    -- bound variables to be above @nextFreeVarID@; but then we have to
    -- do that anyways.
    evaluateVar :: MeasureEvaluator  abt m
                -> TermEvaluator     abt m
                -> VariableEvaluator abt m
    evaluateVar MeasureEvaluator abt m
perform TermEvaluator abt m
evaluate_ = \Variable a
x ->
    -- If we get 'Nothing', then it turns out @x@ is a free variable
      (Maybe (Whnf abt a) -> Whnf abt a)
-> m (Maybe (Whnf abt a)) -> m (Whnf abt a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Whnf abt a
-> (Whnf abt a -> Whnf abt a) -> Maybe (Whnf abt a) -> Whnf abt a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (abt '[] a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral (abt '[] a -> Whnf abt a) -> abt '[] a -> Whnf abt a
forall a b. (a -> b) -> a -> b
$ 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) Whnf abt a -> Whnf abt a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) (m (Maybe (Whnf abt a)) -> m (Whnf abt a))
-> ((Statement abt Location p -> Maybe (m (Whnf abt a)))
    -> m (Maybe (Whnf abt a)))
-> (Statement abt Location p -> Maybe (m (Whnf abt a)))
-> m (Whnf abt a)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Location a
-> (Statement abt Location p -> Maybe (m (Whnf abt a)))
-> m (Maybe (Whnf abt a))
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
       (a :: Hakaru) r.
EvaluationMonad abt m p =>
Location a
-> (Statement abt Location p -> Maybe (m r)) -> m (Maybe r)
select (Variable a -> Location a
forall k (a :: k). Variable a -> Location a
Location Variable a
x) ((Statement abt Location p -> Maybe (m (Whnf abt a)))
 -> m (Whnf abt a))
-> (Statement abt Location p -> Maybe (m (Whnf abt a)))
-> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ \Statement abt Location p
s ->
        case Statement abt Location p
s of
        SBind Location a
y Lazy abt ('HMeasure a)
e [Index (abt '[])]
i -> do
            TypeEq a a
Refl <- Location a -> Location a -> Maybe (TypeEq a a)
forall k (a :: k) (b :: k).
(Show1 Sing, JmEq1 Sing) =>
Location a -> Location b -> Maybe (TypeEq a b)
locEq (Variable a -> Location a
forall k (a :: k). Variable a -> Location a
Location Variable a
x) Location a
y
            m (Whnf abt a) -> Maybe (m (Whnf abt a))
forall a. a -> Maybe a
Just (m (Whnf abt a) -> Maybe (m (Whnf abt a)))
-> m (Whnf abt a) -> Maybe (m (Whnf abt a))
forall a b. (a -> b) -> a -> b
$ do
                Whnf abt a
w <- abt '[] ('HMeasure a) -> m (Whnf abt a)
MeasureEvaluator abt m
perform (abt '[] ('HMeasure a) -> m (Whnf abt a))
-> abt '[] ('HMeasure a) -> m (Whnf abt a)
forall a b. (a -> b) -> a -> b
$ Lazy abt ('HMeasure a)
-> (Whnf abt ('HMeasure a) -> abt '[] ('HMeasure a))
-> (abt '[] ('HMeasure a) -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru) r.
Lazy abt a -> (Whnf abt a -> r) -> (abt '[] a -> r) -> r
caseLazy Lazy abt ('HMeasure a)
e Whnf abt ('HMeasure a) -> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Whnf abt a -> abt '[] a
fromWhnf abt '[] ('HMeasure a) -> abt '[] ('HMeasure a)
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
                Statement abt Location 'Impure -> m ()
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
       (p :: Purity).
EvaluationMonad abt m p =>
Statement abt Location p -> m ()
unsafePush (Location a
-> Lazy abt a
-> [Index (abt '[])]
-> Statement abt Location 'Impure
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity)
       (v :: Hakaru -> *) (a :: Hakaru).
v a -> Lazy abt a -> [Index (abt '[])] -> Statement abt v p
SLet (Variable a -> Location a
forall k (a :: k). Variable a -> Location a
Location Variable a
x) (Whnf abt a -> Lazy abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Whnf abt a -> Lazy abt a
Whnf_ Whnf abt a
w) [Index (abt '[])]
i)
#ifdef __TRACE_DISINTEGRATE__
                trace ("-- updated "
                    ++ show (ppStatement 11 s)
                    ++ " to "
                    ++ show (ppStatement 11 (SLet (Location x) (Whnf_ w) i))
                    ) $ return ()
#endif
                Whnf abt a -> m (Whnf abt a)
forall (m :: * -> *) a. Monad m => a -> m a
return Whnf abt a
w
        SLet Location a
y Lazy abt a
e [Index (abt '[])]
i -> do
            TypeEq a a
Refl <- Location a -> Location a -> Maybe (TypeEq a a)
forall k (a :: k) (b :: k).
(Show1 Sing, JmEq1 Sing) =>
Location a -> Location b -> Maybe (TypeEq a b)
locEq (Variable a -> Location a
forall k (a :: k). Variable a -> Location a
Location Variable a
x) Location a
y
            m (Whnf abt a) -> Maybe (m (Whnf abt a))
forall a. a -> Maybe a
Just (m (Whnf abt a) -> Maybe (m (Whnf abt a)))
-> m (Whnf abt a) -> Maybe (m (Whnf abt a))
forall a b. (a -> b) -> a -> b
$ do
                Whnf abt a
w <- Lazy abt a
-> (Whnf abt a -> m (Whnf abt a))
-> (abt '[] a -> m (Whnf abt a))
-> m (Whnf abt a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru) r.
Lazy abt a -> (Whnf abt a -> r) -> (abt '[] a -> r) -> r
caseLazy Lazy abt a
e Whnf abt a -> m (Whnf abt a)
forall (m :: * -> *) a. Monad m => a -> m a
return abt '[] a -> m (Whnf abt a)
TermEvaluator abt m
evaluate_
                Statement abt Location p -> m ()
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
       (p :: Purity).
EvaluationMonad abt m p =>
Statement abt Location p -> m ()
unsafePush (Location a
-> Lazy abt a -> [Index (abt '[])] -> Statement abt Location p
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity)
       (v :: Hakaru -> *) (a :: Hakaru).
v a -> Lazy abt a -> [Index (abt '[])] -> Statement abt v p
SLet (Variable a -> Location a
forall k (a :: k). Variable a -> Location a
Location Variable a
x) (Whnf abt a -> Lazy abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
Whnf abt a -> Lazy abt a
Whnf_ Whnf abt a
w) [Index (abt '[])]
i)
                Whnf abt a -> m (Whnf abt a)
forall (m :: * -> *) a. Monad m => a -> m a
return Whnf abt a
w
        -- These two don't bind any variables, so they definitely
        -- can't match.
        SWeight   Lazy abt 'HProb
_ [Index (abt '[])]
_ -> Maybe (m (Whnf abt a))
forall a. Maybe a
Nothing
        SStuff0   abt '[] 'HProb -> abt '[] 'HProb
_ [Index (abt '[])]
_ -> Maybe (m (Whnf abt a))
forall a. Maybe a
Nothing
        -- These two do bind variables, but there's no expression we
        -- can return for them because the variables are
        -- untouchable\/abstract.
        SStuff1 Location a
_ abt '[] 'HProb -> abt '[] 'HProb
_ [Index (abt '[])]
_ -> m (Whnf abt a) -> Maybe (m (Whnf abt a))
forall a. a -> Maybe a
Just (m (Whnf abt a) -> Maybe (m (Whnf abt a)))
-> (abt '[] a -> m (Whnf abt a))
-> abt '[] a
-> Maybe (m (Whnf abt a))
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Whnf abt a -> m (Whnf abt a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt a -> m (Whnf abt a))
-> (abt '[] a -> Whnf abt a) -> abt '[] a -> m (Whnf 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 '[] a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral (abt '[] a -> Maybe (m (Whnf abt a)))
-> abt '[] a -> Maybe (m (Whnf abt a))
forall a b. (a -> b) -> a -> b
$ 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
        SGuard List1 Location xs
_ Pattern xs a
_ Lazy abt a
_ [Index (abt '[])]
_ -> m (Whnf abt a) -> Maybe (m (Whnf abt a))
forall a. a -> Maybe a
Just (m (Whnf abt a) -> Maybe (m (Whnf abt a)))
-> (abt '[] a -> m (Whnf abt a))
-> abt '[] a
-> Maybe (m (Whnf abt a))
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Whnf abt a -> m (Whnf abt a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt a -> m (Whnf abt a))
-> (abt '[] a -> Whnf abt a) -> abt '[] a -> m (Whnf 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 '[] a -> Whnf abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral (abt '[] a -> Maybe (m (Whnf abt a)))
-> abt '[] a -> Maybe (m (Whnf abt a))
forall a b. (a -> b) -> a -> b
$ 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 simple 'CaseEvaluator' which uses the 'DatumEvaluator' to
-- force the scrutinee, and if 'matchBranches' succeeds then we
-- call the 'TermEvaluator' to continue evaluating the body of the
-- matched branch. If we 'GotStuck' then we return a 'Neutral' term
-- of the case expression itself (n.b, any side effects from having
-- called the 'DatumEvaluator' will still persist when returning
-- this neutral term). If we didn't get stuck and yet none of the
-- branches matches, then we throw an exception.
defaultCaseEvaluator
    :: forall abt m p
    .  (ABT Term abt, EvaluationMonad abt m p)
    => TermEvaluator abt m
    -> CaseEvaluator abt m
{-# INLINE defaultCaseEvaluator #-}
defaultCaseEvaluator :: TermEvaluator abt m -> CaseEvaluator abt m
defaultCaseEvaluator TermEvaluator abt m
evaluate_ = abt '[] a -> [Branch a abt b] -> m (Whnf abt b)
CaseEvaluator abt m
evaluateCase_
    where
    -- TODO: At present, whenever we residualize a case expression we'll
    -- generate a 'Neutral' term which will, when run, repeat the work
    -- we're doing in the evaluation here. We could eliminate this
    -- redundancy by introducing a new variable for @e@ each time this
    -- function is called--- if only we had some way of getting those
    -- variables put into the right place for when we residualize the
    -- original scrutinee...
    --
    -- N.B., 'DatumEvaluator' is a rank-2 type so it requires a signature
    evaluateDatum :: DatumEvaluator (abt '[]) m
    evaluateDatum :: abt '[] (HData' t) -> m (Maybe (Datum (abt '[]) (HData' t)))
evaluateDatum abt '[] (HData' t)
e = Whnf abt (HData' t) -> Maybe (Datum (abt '[]) (HData' t))
forall (abt :: [Hakaru] -> Hakaru -> *) (t :: HakaruCon).
ABT Term abt =>
Whnf abt (HData' t) -> Maybe (Datum (abt '[]) (HData' t))
viewWhnfDatum (Whnf abt (HData' t) -> Maybe (Datum (abt '[]) (HData' t)))
-> m (Whnf abt (HData' t))
-> m (Maybe (Datum (abt '[]) (HData' t)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> abt '[] (HData' t) -> m (Whnf abt (HData' t))
TermEvaluator abt m
evaluate_ abt '[] (HData' t)
e

    evaluateCase_ :: CaseEvaluator abt m
    evaluateCase_ :: abt '[] a -> [Branch a abt b] -> m (Whnf abt b)
evaluateCase_ abt '[] a
e [Branch a abt b]
bs = do
        Maybe (MatchResult (abt '[]) abt b)
match <- DatumEvaluator (abt '[]) m
-> abt '[] a
-> [Branch a abt b]
-> m (Maybe (MatchResult (abt '[]) abt b))
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
       (ast :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
(ABT Term abt, Monad m) =>
DatumEvaluator ast m
-> ast a -> [Branch a abt b] -> m (Maybe (MatchResult ast abt b))
matchBranches DatumEvaluator (abt '[]) m
evaluateDatum abt '[] a
e [Branch a abt b]
bs
        case Maybe (MatchResult (abt '[]) abt b)
match of
            Maybe (MatchResult (abt '[]) abt b)
Nothing ->
                -- TODO: print more info about where this error
                -- happened
                --
                -- TODO: rather than throwing a Haskell error,
                -- instead capture the possibility of failure in
                -- the 'EvaluationMonad' monad.
                [Char] -> m (Whnf abt b)
forall a. HasCallStack => [Char] -> a
error [Char]
"defaultCaseEvaluator: non-exhaustive patterns in case!"
            Just MatchResult (abt '[]) abt b
GotStuck ->
                Whnf abt b -> m (Whnf abt b)
forall (m :: * -> *) a. Monad m => a -> m a
return (Whnf abt b -> m (Whnf abt b))
-> (Term abt b -> Whnf abt b) -> Term abt b -> m (Whnf abt b)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. abt '[] b -> Whnf abt b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Whnf abt a
Neutral (abt '[] b -> Whnf abt b)
-> (Term abt b -> abt '[] b) -> Term abt b -> Whnf abt b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Term abt b -> abt '[] b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term abt b -> m (Whnf abt b)) -> Term abt b -> m (Whnf abt b)
forall a b. (a -> b) -> a -> b
$ abt '[] a -> [Branch a abt b] -> Term abt b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
abt '[] a -> [Branch a abt b] -> Term abt b
Case_ abt '[] a
e [Branch a abt b]
bs
            Just (Matched Assocs (abt '[])
ss abt '[] b
body) ->
                [Statement abt Variable p] -> abt '[] b -> m (abt '[] b)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
       (xs :: [Hakaru]) (a :: Hakaru).
(ABT Term abt, EvaluationMonad abt m p) =>
[Statement abt Variable p] -> abt xs a -> m (abt xs a)
pushes (Assocs (abt '[]) -> [Statement abt Variable p]
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity).
Assocs (abt '[]) -> [Statement abt Variable p]
toVarStatements Assocs (abt '[])
ss) abt '[] b
body m (abt '[] b) -> (abt '[] b -> m (Whnf abt b)) -> m (Whnf abt b)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= abt '[] b -> m (Whnf abt b)
TermEvaluator abt m
evaluate_


toVarStatements :: Assocs (abt '[]) -> [Statement abt Variable p]
toVarStatements :: Assocs (abt '[]) -> [Statement abt Variable p]
toVarStatements = (Assoc (abt '[]) -> Statement abt Variable p)
-> [Assoc (abt '[])] -> [Statement abt Variable p]
forall a b. (a -> b) -> [a] -> [b]
map (\(Assoc Variable a
x abt '[] a
e) -> Variable a
-> Lazy abt a -> [Index (abt '[])] -> Statement abt Variable p
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity)
       (v :: Hakaru -> *) (a :: Hakaru).
v a -> Lazy abt a -> [Index (abt '[])] -> Statement abt v p
SLet Variable a
x (abt '[] a -> Lazy abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> Lazy abt a
Thunk abt '[] a
e) []) ([Assoc (abt '[])] -> [Statement abt Variable p])
-> (Assocs (abt '[]) -> [Assoc (abt '[])])
-> Assocs (abt '[])
-> [Statement abt Variable p]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.
                  Assocs (abt '[]) -> [Assoc (abt '[])]
forall k (ast :: k -> *). Assocs ast -> [Assoc ast]
fromAssocs
 
extSubst
    :: forall abt a xs b m p. (EvaluationMonad abt m p)
    => Variable a
    -> abt '[] a
    -> abt xs b
    -> m (abt xs b)
extSubst :: Variable a -> abt '[] a -> abt xs b -> m (abt xs b)
extSubst Variable a
x abt '[] a
e = Variable a
-> abt '[] a
-> (forall (b' :: Hakaru). Variable b' -> m (abt '[] b'))
-> abt xs b
-> m (abt xs b)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k) (m :: * -> *).
(JmEq1 Sing, Show1 Sing, Traversable21 syn, ABT syn abt,
 Applicative m, Functor m, Monad m) =>
Variable a
-> abt '[] a
-> (forall (b' :: k). Variable b' -> m (abt '[] b'))
-> abt xs b
-> m (abt xs b)
substM Variable a
x abt '[] a
e (Variable a
-> abt '[] a
-> forall (b' :: Hakaru). Variable b' -> m (abt '[] b')
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
       (a :: Hakaru).
EvaluationMonad abt m p =>
Variable a
-> abt '[] a
-> forall (b' :: Hakaru). Variable b' -> m (abt '[] b')
substVar Variable a
x abt '[] a
e)

extSubsts
    :: forall abt a xs m p. (EvaluationMonad abt m p)
    => Assocs (abt '[])
    -> abt xs a
    -> m (abt xs a)
extSubsts :: Assocs (abt '[]) -> abt xs a -> m (abt xs a)
extSubsts Assocs (abt '[])
rho0 abt xs a
e0 =
    (abt xs a -> Assoc (abt '[]) -> m (abt xs a))
-> abt xs a -> IntMap (Assoc (abt '[])) -> m (abt xs a)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
F.foldlM (\abt xs a
e (Assoc Variable a
x abt '[] a
v) -> Variable a -> abt '[] a -> abt xs a -> m (abt xs a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (xs :: [Hakaru]) (b :: Hakaru) (m :: * -> *) (p :: Purity).
EvaluationMonad abt m p =>
Variable a -> abt '[] a -> abt xs b -> m (abt xs b)
extSubst Variable a
x abt '[] a
v abt xs a
e) abt xs a
e0 (Assocs (abt '[]) -> IntMap (Assoc (abt '[]))
forall k (ast :: k -> *). Assocs ast -> IntMap (Assoc ast)
unAssocs Assocs (abt '[])
rho0)

           
-- TODO: define a new NameSupply monad in "Language.Hakaru.Syntax.Variable" for encapsulating these four fresh(en) functions?


-- | Given some hint and type, generate a variable with a fresh
-- 'varID'.
freshVar
    :: (EvaluationMonad abt m p)
    => Text
    -> Sing (a :: Hakaru)
    -> m (Variable a)
freshVar :: Text -> Sing a -> m (Variable a)
freshVar Text
hint Sing a
typ = (\Nat
i -> Text -> Nat -> Sing a -> Variable a
forall k (a :: k). Text -> Nat -> Sing a -> Variable a
Variable Text
hint Nat
i Sing a
typ) (Nat -> Variable a) -> m Nat -> m (Variable a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Nat
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
       (p :: Purity).
EvaluationMonad abt m p =>
m Nat
freshNat


-- TODO: move to "Language.Hakaru.Syntax.Variable" in case anyone else wants it too.
data Hint (a :: Hakaru) = Hint {-# UNPACK #-} !Text !(Sing a)

-- | Call 'freshVar' repeatedly.
-- TODO: make this more efficient than actually calling 'freshVar'
-- repeatedly.
freshVars
    :: (EvaluationMonad abt m p)
    => List1 Hint xs
    -> m (List1 Variable xs)
freshVars :: List1 Hint xs -> m (List1 Variable xs)
freshVars List1 Hint xs
Nil1         = List1 Variable '[] -> m (List1 Variable '[])
forall (m :: * -> *) a. Monad m => a -> m a
return List1 Variable '[]
forall k (a :: k -> *). List1 a '[]
Nil1
freshVars (Cons1 Hint x
x List1 Hint xs
xs) = Variable x -> List1 Variable xs -> List1 Variable (x : xs)
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 (Variable x -> List1 Variable xs -> List1 Variable (x : xs))
-> m (Variable x)
-> m (List1 Variable xs -> List1 Variable (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Hint x -> m (Variable x)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
       (a :: Hakaru).
EvaluationMonad abt m p =>
Hint a -> m (Variable a)
freshVar' Hint x
x m (List1 Variable xs -> List1 Variable (x : xs))
-> m (List1 Variable xs) -> m (List1 Variable (x : xs))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> List1 Hint xs -> m (List1 Variable xs)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
       (xs :: [Hakaru]).
EvaluationMonad abt m p =>
List1 Hint xs -> m (List1 Variable xs)
freshVars List1 Hint xs
xs
    where
    freshVar' :: Hint a -> m (Variable a)
freshVar' (Hint Text
hint Sing a
typ) = Text -> Sing a -> 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


-- | Given a variable, return a new variable with the same hint and
-- type but with a fresh 'varID'.
freshenVar
    :: (EvaluationMonad abt m p)
    => Variable (a :: Hakaru)
    -> m (Variable a)
freshenVar :: Variable a -> m (Variable a)
freshenVar Variable a
x = (\Nat
i -> Variable a
x{varID :: Nat
varID=Nat
i}) (Nat -> Variable a) -> m Nat -> m (Variable a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Nat
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
       (p :: Purity).
EvaluationMonad abt m p =>
m Nat
freshNat


-- | Call 'freshenVar' repeatedly.
-- TODO: make this more efficient than actually calling 'freshenVar'
-- repeatedly.
freshenVars
    :: (EvaluationMonad abt m p)
    => List1 Variable (xs :: [Hakaru])
    -> m (List1 Variable xs)
freshenVars :: List1 Variable xs -> m (List1 Variable xs)
freshenVars List1 Variable xs
Nil1         = List1 Variable '[] -> m (List1 Variable '[])
forall (m :: * -> *) a. Monad m => a -> m a
return List1 Variable '[]
forall k (a :: k -> *). List1 a '[]
Nil1
freshenVars (Cons1 Variable x
x List1 Variable xs
xs) = Variable x -> List1 Variable xs -> List1 Variable (x : xs)
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 (Variable x -> List1 Variable xs -> List1 Variable (x : xs))
-> m (Variable x)
-> m (List1 Variable xs -> List1 Variable (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Variable x -> m (Variable x)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
       (a :: Hakaru).
EvaluationMonad abt m p =>
Variable a -> m (Variable a)
freshenVar Variable x
x m (List1 Variable xs -> List1 Variable (x : xs))
-> m (List1 Variable xs) -> m (List1 Variable (x : xs))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> List1 Variable xs -> 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
xs
{-
-- TODO: get this faster version to typecheck! And once we do, move it to IClasses.hs or wherever 'List1'\/'DList1' end up
freshenVars = go dnil1
    where
    go  :: (EvaluationMonad abt m p)
        => DList1 Variable (ys :: [Hakaru])
        -> List1  Variable (zs :: [Hakaru])
        -> m (List1 Variable (ys ++ zs))
    go k Nil1         = return (unDList1 k Nil1) -- for typechecking, don't use 'toList1' here.
    go k (Cons1 x xs) = do
        x' <- freshenVar x
        go (k `dsnoc1` x') xs -- BUG: type error....
-}

-- | Given a size, generate a fresh Index
freshInd :: (EvaluationMonad abt m p)
         => abt '[] 'HNat
         -> m (Index (abt '[]))
freshInd :: abt '[] 'HNat -> m (Index (abt '[]))
freshInd abt '[] 'HNat
s = do
  Variable 'HNat
x <- Text -> Sing 'HNat -> m (Variable 'HNat)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
       (a :: Hakaru).
EvaluationMonad abt m p =>
Text -> Sing a -> m (Variable a)
freshVar Text
T.empty Sing 'HNat
SNat
  Index (abt '[]) -> m (Index (abt '[]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Index (abt '[]) -> m (Index (abt '[])))
-> Index (abt '[]) -> m (Index (abt '[]))
forall a b. (a -> b) -> a -> b
$ Variable 'HNat -> abt '[] 'HNat -> Index (abt '[])
forall (ast :: Hakaru -> *).
Variable 'HNat -> ast 'HNat -> Index ast
Ind Variable 'HNat
x abt '[] 'HNat
s


-- | Given a location, return a new Location with the same hint
-- and type but with a fresh ID
freshenLoc :: (EvaluationMonad abt m p)
           => Location (a :: Hakaru) -> m (Location a)
freshenLoc :: Location a -> m (Location a)
freshenLoc (Location Variable a
x) = Variable a -> Location a
forall k (a :: k). Variable a -> Location a
Location (Variable a -> Location a) -> m (Variable a) -> m (Location a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Variable a -> m (Variable a)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
       (a :: Hakaru).
EvaluationMonad abt m p =>
Variable a -> m (Variable a)
freshenVar Variable a
x

-- | Call `freshenLoc` repeatedly
freshenLocs :: (EvaluationMonad abt m p)
            => List1 Location (ls :: [Hakaru])
            -> m (List1 Location ls)
freshenLocs :: List1 Location ls -> m (List1 Location ls)
freshenLocs List1 Location ls
Nil1         = List1 Location '[] -> m (List1 Location '[])
forall (m :: * -> *) a. Monad m => a -> m a
return List1 Location '[]
forall k (a :: k -> *). List1 a '[]
Nil1
freshenLocs (Cons1 Location x
l List1 Location xs
ls) = Location x -> List1 Location xs -> List1 Location (x : xs)
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 (Location x -> List1 Location xs -> List1 Location (x : xs))
-> m (Location x)
-> m (List1 Location xs -> List1 Location (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Location x -> m (Location x)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
       (a :: Hakaru).
EvaluationMonad abt m p =>
Location a -> m (Location a)
freshenLoc Location x
l m (List1 Location xs -> List1 Location (x : xs))
-> m (List1 Location xs) -> m (List1 Location (x : xs))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> List1 Location xs -> m (List1 Location xs)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
       (ls :: [Hakaru]).
EvaluationMonad abt m p =>
List1 Location ls -> m (List1 Location ls)
freshenLocs List1 Location xs
ls

                           

-- | Add a statement to the top of the context, renaming any variables
-- the statement binds and returning the substitution mapping the
-- old variables to the new ones. This is safer than 'unsafePush'
-- because it avoids variable confusion; but it is still somewhat
-- unsafe since you may forget to apply the substitution to \"the
-- rest of the term\". You almost certainly should use 'push' or
-- 'pushes' instead.
push_
    :: (ABT Term abt, EvaluationMonad abt m p)
    => Statement abt Variable p
    -> m (Assocs (Variable :: Hakaru -> *))
push_ :: Statement abt Variable p -> m (Assocs Variable)
push_ Statement abt Variable p
s = do
    (Statement abt Location p
s',Assocs Variable
rho) <- Statement abt Variable p
-> m (Statement abt Location p, Assocs Variable)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
       (p :: Purity).
EvaluationMonad abt m p =>
Statement abt Variable p
-> m (Statement abt Location p, Assocs Variable)
freshLocStatement Statement abt Variable p
s
    Statement abt Location p -> m ()
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
       (p :: Purity).
EvaluationMonad abt m p =>
Statement abt Location p -> m ()
unsafePush Statement abt Location p
s'
    Assocs Variable -> m (Assocs Variable)
forall (m :: * -> *) a. Monad m => a -> m a
return Assocs Variable
rho


-- | Push a statement onto the context, renaming variables along
-- the way. The second argument represents \"the rest of the term\"
-- after we've peeled the statement off; it's passed so that we can
-- update the variable names there so that they match with the
-- (renamed)binding statement. The third argument is the continuation
-- for what to do with the renamed term. Rather than taking the
-- second and third arguments we could return an 'Assocs' giving
-- the renaming of variables; however, doing that would make it too
-- easy to accidentally drop the substitution on the floor rather
-- than applying it to the term before calling the continuation.
push
    :: (ABT Term abt, EvaluationMonad abt m p)
    => Statement abt Variable p   -- ^ the statement to push
    -> abt xs a          -- ^ the \"rest\" of the term
    -- -> (abt xs a -> m r) -- ^ what to do with the renamed \"rest\"
    -> m (abt xs a)               -- ^ the final result
push :: Statement abt Variable p -> abt xs a -> m (abt xs a)
push Statement abt Variable p
s abt xs a
e = do
    Assocs Variable
rho <- Statement abt Variable p -> m (Assocs Variable)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
       (p :: Purity).
(ABT Term abt, EvaluationMonad abt m p) =>
Statement abt Variable p -> m (Assocs Variable)
push_ Statement abt Variable p
s
    abt xs a -> m (abt xs a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Assocs Variable -> abt xs a -> abt xs a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
(ABT syn abt, JmEq1 Sing, Show1 Sing, Functor21 syn) =>
Assocs Variable -> abt xs a -> abt xs a
renames Assocs Variable
rho abt xs a
e)


-- | Call 'push' repeatedly. (N.B., is more efficient than actually
-- calling 'push' repeatedly.) The head is pushed first and thus
-- is the furthest away in the final context, whereas the tail is
-- pushed last and is the closest in the final context.
pushes
    :: (ABT Term abt, EvaluationMonad abt m p)
    => [Statement abt Variable p] -- ^ the statements to push
    -> abt xs a          -- ^ the \"rest\" of the term
    -- -> (abt xs a -> m r) -- ^ what to do with the renamed \"rest\"
    -> m (abt xs a)         -- ^ the final result
pushes :: [Statement abt Variable p] -> abt xs a -> m (abt xs a)
pushes [Statement abt Variable p]
ss abt xs a
e = do
    -- TODO: is 'foldlM' the right one? or do we want 'foldrM'?
    Assocs Variable
rho <- (Assocs Variable
 -> Statement abt Variable p -> m (Assocs Variable))
-> Assocs Variable
-> [Statement abt Variable p]
-> m (Assocs Variable)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
F.foldlM (\Assocs Variable
rho Statement abt Variable p
s -> Assocs Variable -> Assocs Variable -> Assocs Variable
forall a. Monoid a => a -> a -> a
mappend Assocs Variable
rho (Assocs Variable -> Assocs Variable)
-> m (Assocs Variable) -> m (Assocs Variable)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Statement abt Variable p -> m (Assocs Variable)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
       (p :: Purity).
(ABT Term abt, EvaluationMonad abt m p) =>
Statement abt Variable p -> m (Assocs Variable)
push_ Statement abt Variable p
s) Assocs Variable
forall a. Monoid a => a
mempty [Statement abt Variable p]
ss
    abt xs a -> m (abt xs a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Assocs Variable -> abt xs a -> abt xs a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
(ABT syn abt, JmEq1 Sing, Show1 Sing, Functor21 syn) =>
Assocs Variable -> abt xs a -> abt xs a
renames Assocs Variable
rho abt xs a
e)

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