{-# LANGUAGE CPP
, GADTs
, KindSignatures
, DataKinds
, PolyKinds
, TypeOperators
, Rank2Types
, BangPatterns
, FlexibleContexts
, MultiParamTypeClasses
, FunctionalDependencies
, FlexibleInstances
, UndecidableInstances
, EmptyCase
, ScopedTypeVariables
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Evaluation.Types
(
Head(..), fromHead, toHead, viewHeadDatum
, Whnf(..), fromWhnf, toWhnf, caseWhnf, viewWhnfDatum
, Lazy(..), fromLazy, caseLazy
, getLazyVariable, isLazyVariable
, getLazyLiteral, isLazyLiteral
, TermEvaluator
, MeasureEvaluator
, CaseEvaluator
, VariableEvaluator
, 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
, 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.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
data Head :: ([Hakaru] -> Hakaru -> *) -> Hakaru -> * where
WLiteral :: !(Literal a) -> Head abt a
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)
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)
WCoerceTo :: !(Coercion a b) -> !(Head abt a) -> Head abt b
WUnsafeFrom :: !(Coercion a b) -> !(Head abt b) -> Head abt a
WIntegrate
:: !(abt '[] 'HReal)
-> !(abt '[] 'HReal)
-> !(abt '[ 'HReal ] 'HProb)
-> Head abt 'HProb
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)
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
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)
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
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
data Whnf (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
= Head_ !(Head abt a)
| Neutral !(abt '[] a)
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
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
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
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
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"
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
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)
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)
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
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)
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)
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
data Lazy (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
= Whnf_ !(Whnf abt a)
| Thunk !(abt '[] a)
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
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
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)
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
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
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
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
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)
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
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
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
data Statement :: ([Hakaru] -> Hakaru -> *) -> (Hakaru -> *) -> Purity -> * where
SBind
:: forall abt (v :: Hakaru -> *) (a :: Hakaru)
. {-# UNPACK #-} !(v a)
-> !(Lazy abt ('HMeasure a))
-> [Index (abt '[])]
-> Statement abt v 'Impure
SLet
:: forall abt p (v :: Hakaru -> *) (a :: Hakaru)
. {-# UNPACK #-} !(v a)
-> !(Lazy abt a)
-> [Index (abt '[])]
-> Statement abt v p
SWeight
:: forall abt (v :: Hakaru -> *)
. !(Lazy abt 'HProb)
-> [Index (abt '[])]
-> Statement abt v 'Impure
SGuard
:: forall abt (v :: Hakaru -> *) (xs :: [Hakaru]) (a :: Hakaru)
. !(List1 v xs)
-> !(Pattern xs a)
-> !(Lazy abt a)
-> [Index (abt '[])]
-> Statement abt v 'Impure
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)
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 '[])]
_ =
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
#ifdef __TRACE_DISINTEGRATE__
instance (ABT Term abt) => Pretty (Whnf abt) where
prettyPrec_ p (Head_ w) = ppApply1 p "Head_" (fromHead w)
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
type TermEvaluator abt m =
forall a. abt '[] a -> m (Whnf abt a)
type MeasureEvaluator abt m =
forall a. abt '[] ('HMeasure a) -> m (Whnf abt a)
type CaseEvaluator abt m =
forall a b. abt '[] a -> [Branch a abt b] -> m (Whnf abt b)
type VariableEvaluator abt m =
forall a. Variable a -> m (Whnf abt a)
class (Functor m, Applicative m, Monad m, ABT Term abt)
=> EvaluationMonad abt m p | m -> abt p
where
freshNat :: m Nat
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')
getIndices :: m [Index (abt '[])]
getIndices = [Index (abt '[])] -> m [Index (abt '[])]
forall (m :: * -> *) a. Monad m => a -> m a
return []
unsafePush :: Statement abt Location p -> m ()
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
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)
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
evaluateVar :: MeasureEvaluator abt m
-> TermEvaluator abt m
-> VariableEvaluator abt m
evaluateVar MeasureEvaluator abt m
perform TermEvaluator abt m
evaluate_ = \Variable a
x ->
(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
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
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
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
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 ->
[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)
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
data Hint (a :: Hakaru) = Hint {-# UNPACK #-} !Text !(Sing a)
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
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
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
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
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
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
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
:: (ABT Term abt, EvaluationMonad abt m p)
=> Statement abt Variable p
-> abt xs a
-> m (abt xs a)
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)
pushes
:: (ABT Term abt, EvaluationMonad abt m p)
=> [Statement abt Variable p]
-> abt xs a
-> m (abt xs a)
pushes :: [Statement abt Variable p] -> abt xs a -> m (abt xs a)
pushes [Statement abt Variable p]
ss abt xs a
e = do
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)