{-# LANGUAGE CPP
, GADTs
, KindSignatures
, DataKinds
, Rank2Types
, ScopedTypeVariables
, MultiParamTypeClasses
, FlexibleContexts
, FlexibleInstances
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Evaluation.EvalMonad
( runPureEvaluate
, pureEvaluate
, ListContext(..), PureAns, Eval(..), runEval
, residualizePureListContext
) where
import Prelude hiding (id, (.))
import Control.Category (Category(..))
#if __GLASGOW_HASKELL__ < 710
import Data.Functor ((<$>))
import Control.Applicative (Applicative(..))
#endif
import qualified Data.Foldable as F
import Language.Hakaru.Syntax.IClasses (Some2(..))
import Language.Hakaru.Syntax.Variable (memberVarSet)
import Language.Hakaru.Syntax.ABT (ABT(..), subst, maxNextFree)
import Language.Hakaru.Syntax.DatumABT
import Language.Hakaru.Syntax.AST
import Language.Hakaru.Evaluation.Types
import Language.Hakaru.Evaluation.Lazy (evaluate)
import Language.Hakaru.Evaluation.PEvalMonad (ListContext(..))
import Data.Text (Text)
import qualified Data.Text as Text
import qualified Data.Traversable as T
import Language.Hakaru.Syntax.IClasses (Functor11(..))
import Language.Hakaru.Syntax.Variable (Variable(), toAssocs1)
import Language.Hakaru.Syntax.ABT (caseVarSyn, caseBinds, substs)
import Language.Hakaru.Types.DataKind
import Language.Hakaru.Types.Sing (Sing, sUnPair)
import Language.Hakaru.Syntax.TypeOf (typeOf)
import Language.Hakaru.Syntax.Datum
import Language.Hakaru.Evaluation.Lazy (reifyPair)
#ifdef __TRACE_DISINTEGRATE__
import Debug.Trace (trace)
#endif
runPureEvaluate :: (ABT Term abt) => abt '[] a -> abt '[] a
runPureEvaluate :: abt '[] a -> abt '[] a
runPureEvaluate abt '[] a
e = Eval abt (abt '[] a) -> [Some2 abt] -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (f :: * -> *)
(a :: Hakaru).
(ABT Term abt, Foldable f) =>
Eval abt (abt '[] a) -> f (Some2 abt) -> abt '[] a
runEval (Whnf abt a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Whnf abt a -> abt '[] a
fromWhnf (Whnf abt a -> abt '[] a)
-> Eval abt (Whnf abt a) -> Eval abt (abt '[] a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> abt '[] a -> Eval abt (Whnf abt a)
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
TermEvaluator abt (Eval abt)
pureEvaluate abt '[] a
e) [abt '[] a -> Some2 abt
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
a i j -> Some2 a
Some2 abt '[] a
e]
pureEvaluate :: (ABT Term abt) => TermEvaluator abt (Eval abt)
pureEvaluate :: TermEvaluator abt (Eval abt)
pureEvaluate = MeasureEvaluator abt (Eval abt) -> TermEvaluator abt (Eval abt)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
(p :: Purity).
(ABT Term abt, EvaluationMonad abt m p) =>
MeasureEvaluator abt m -> TermEvaluator abt m
evaluate (String -> abt '[] ('HMeasure a) -> Eval abt (Whnf abt a)
forall a. String -> a
brokenInvariant String
"perform")
type PureAns abt a = ListContext abt 'Pure -> abt '[] a
newtype Eval abt x =
Eval { Eval abt x
-> forall (a :: Hakaru). (x -> PureAns abt a) -> PureAns abt a
unEval :: forall a. (x -> PureAns abt a) -> PureAns abt a }
brokenInvariant :: String -> a
brokenInvariant :: String -> a
brokenInvariant String
loc = String -> a
forall a. HasCallStack => String -> a
error (String
loc String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": Eval's invariant broken")
runEval :: (ABT Term abt, F.Foldable f)
=> Eval abt (abt '[] a)
-> f (Some2 abt)
-> abt '[] a
runEval :: Eval abt (abt '[] a) -> f (Some2 abt) -> abt '[] a
runEval (Eval forall (a :: Hakaru). (abt '[] a -> PureAns abt a) -> PureAns abt a
m) f (Some2 abt)
es =
(abt '[] a -> PureAns abt a) -> PureAns abt a
forall (a :: Hakaru). (abt '[] a -> PureAns abt a) -> PureAns abt a
m abt '[] a -> PureAns abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> ListContext abt 'Pure -> abt '[] a
residualizePureListContext (Nat -> [Statement abt Location 'Pure] -> ListContext abt 'Pure
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity).
Nat -> [Statement abt Location p] -> ListContext abt p
ListContext (f (Some2 abt) -> Nat
forall k2 (syn :: ([k2] -> k2 -> *) -> k2 -> *)
(abt :: [k2] -> k2 -> *) (f :: * -> *).
(ABT syn abt, Foldable f) =>
f (Some2 abt) -> Nat
maxNextFree f (Some2 abt)
es) [])
residualizePureListContext
:: forall abt a
. (ABT Term abt)
=> abt '[] a
-> ListContext abt 'Pure
-> abt '[] a
residualizePureListContext :: abt '[] a -> ListContext abt 'Pure -> abt '[] a
residualizePureListContext abt '[] a
e0 =
(abt '[] a -> Statement abt Location 'Pure -> abt '[] a)
-> abt '[] a -> [Statement abt Location 'Pure] -> abt '[] a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl abt '[] a -> Statement abt Location 'Pure -> abt '[] a
step abt '[] a
e0 ([Statement abt Location 'Pure] -> abt '[] a)
-> (ListContext abt 'Pure -> [Statement abt Location 'Pure])
-> ListContext abt 'Pure
-> abt '[] a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ListContext abt 'Pure -> [Statement abt Location 'Pure]
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity).
ListContext abt p -> [Statement abt Location p]
statements
where
step :: abt '[] a -> Statement abt Location 'Pure -> abt '[] a
step :: abt '[] a -> Statement abt Location 'Pure -> abt '[] a
step abt '[] a
e Statement abt Location 'Pure
s =
case Statement abt Location 'Pure
s of
SLet (Location Variable a
x) Lazy abt a
body [Index (abt '[])]
_
| Bool -> Bool
not (Variable a
x Variable a -> VarSet (KindOf a) -> Bool
forall k (a :: k) (kproxy :: KProxy k).
(Show1 Sing, JmEq1 Sing) =>
Variable a -> VarSet kproxy -> Bool
`memberVarSet` abt '[] a -> VarSet (KindOf a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> VarSet (KindOf a)
freeVars abt '[] a
e) -> abt '[] a
e
| Bool
otherwise ->
case Lazy abt a -> Maybe (Variable a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Lazy abt a -> Maybe (Variable a)
getLazyVariable Lazy abt a
body of
Just Variable a
y -> Variable a -> abt '[] a -> abt '[] a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
(JmEq1 Sing, Show1 Sing, Traversable21 syn, ABT syn abt) =>
Variable a -> abt '[] a -> abt xs b -> abt xs b
subst Variable a
x (Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable a
y) abt '[] a
e
Maybe (Variable a)
Nothing ->
case Lazy abt a -> Maybe (Literal a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Lazy abt a -> Maybe (Literal a)
getLazyLiteral Lazy abt a
body of
Just Literal a
v -> Variable a -> abt '[] a -> abt '[] a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
(JmEq1 Sing, Show1 Sing, Traversable21 syn, ABT syn abt) =>
Variable a -> abt '[] a -> abt xs b -> abt xs b
subst Variable a
x (Term abt a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term abt a -> abt '[] a) -> Term abt a -> abt '[] a
forall a b. (a -> b) -> a -> b
$ Literal a -> Term abt a
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
Literal a -> Term abt a
Literal_ Literal a
v) abt '[] a
e
Maybe (Literal a)
Nothing ->
Term abt a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (SCon '[LC a, '( '[a], a)] a
forall (a :: Hakaru) (b :: Hakaru). SCon '[LC a, '( '[a], b)] b
Let_ SCon '[LC a, '( '[a], a)] a
-> SArgs abt '[LC a, '( '[a], a)] -> Term abt a
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
(abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ Lazy abt a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Lazy abt a -> abt '[] a
fromLazy Lazy abt a
body abt '[] a
-> SArgs abt '[ '( '[a], a)] -> SArgs abt '[LC a, '( '[a], a)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* Variable a -> abt '[] a -> abt '[a] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable a
x abt '[] a
e abt '[a] a -> SArgs abt '[] -> SArgs abt '[ '( '[a], a)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs abt '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End)
instance Functor (Eval abt) where
fmap :: (a -> b) -> Eval abt a -> Eval abt b
fmap a -> b
f (Eval forall (a :: Hakaru). (a -> PureAns abt a) -> PureAns abt a
m) = (forall (a :: Hakaru). (b -> PureAns abt a) -> PureAns abt a)
-> Eval abt b
forall (abt :: [Hakaru] -> Hakaru -> *) x.
(forall (a :: Hakaru). (x -> PureAns abt a) -> PureAns abt a)
-> Eval abt x
Eval ((forall (a :: Hakaru). (b -> PureAns abt a) -> PureAns abt a)
-> Eval abt b)
-> (forall (a :: Hakaru). (b -> PureAns abt a) -> PureAns abt a)
-> Eval abt b
forall a b. (a -> b) -> a -> b
$ \b -> PureAns abt a
c -> (a -> PureAns abt a) -> PureAns abt a
forall (a :: Hakaru). (a -> PureAns abt a) -> PureAns abt a
m (b -> PureAns abt a
c (b -> PureAns abt a) -> (a -> b) -> a -> PureAns abt a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> b
f)
instance Applicative (Eval abt) where
pure :: a -> Eval abt a
pure a
x = (forall (a :: Hakaru). (a -> PureAns abt a) -> PureAns abt a)
-> Eval abt a
forall (abt :: [Hakaru] -> Hakaru -> *) x.
(forall (a :: Hakaru). (x -> PureAns abt a) -> PureAns abt a)
-> Eval abt x
Eval ((forall (a :: Hakaru). (a -> PureAns abt a) -> PureAns abt a)
-> Eval abt a)
-> (forall (a :: Hakaru). (a -> PureAns abt a) -> PureAns abt a)
-> Eval abt a
forall a b. (a -> b) -> a -> b
$ \a -> PureAns abt a
c -> a -> PureAns abt a
c a
x
Eval forall (a :: Hakaru). ((a -> b) -> PureAns abt a) -> PureAns abt a
mf <*> :: Eval abt (a -> b) -> Eval abt a -> Eval abt b
<*> Eval forall (a :: Hakaru). (a -> PureAns abt a) -> PureAns abt a
mx = (forall (a :: Hakaru). (b -> PureAns abt a) -> PureAns abt a)
-> Eval abt b
forall (abt :: [Hakaru] -> Hakaru -> *) x.
(forall (a :: Hakaru). (x -> PureAns abt a) -> PureAns abt a)
-> Eval abt x
Eval ((forall (a :: Hakaru). (b -> PureAns abt a) -> PureAns abt a)
-> Eval abt b)
-> (forall (a :: Hakaru). (b -> PureAns abt a) -> PureAns abt a)
-> Eval abt b
forall a b. (a -> b) -> a -> b
$ \b -> PureAns abt a
c -> ((a -> b) -> PureAns abt a) -> PureAns abt a
forall (a :: Hakaru). ((a -> b) -> PureAns abt a) -> PureAns abt a
mf (((a -> b) -> PureAns abt a) -> PureAns abt a)
-> ((a -> b) -> PureAns abt a) -> PureAns abt a
forall a b. (a -> b) -> a -> b
$ \a -> b
f -> (a -> PureAns abt a) -> PureAns abt a
forall (a :: Hakaru). (a -> PureAns abt a) -> PureAns abt a
mx ((a -> PureAns abt a) -> PureAns abt a)
-> (a -> PureAns abt a) -> PureAns abt a
forall a b. (a -> b) -> a -> b
$ \a
x -> b -> PureAns abt a
c (a -> b
f a
x)
instance Monad (Eval abt) where
return :: a -> Eval abt a
return = a -> Eval abt a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
Eval forall (a :: Hakaru). (a -> PureAns abt a) -> PureAns abt a
m >>= :: Eval abt a -> (a -> Eval abt b) -> Eval abt b
>>= a -> Eval abt b
k = (forall (a :: Hakaru). (b -> PureAns abt a) -> PureAns abt a)
-> Eval abt b
forall (abt :: [Hakaru] -> Hakaru -> *) x.
(forall (a :: Hakaru). (x -> PureAns abt a) -> PureAns abt a)
-> Eval abt x
Eval ((forall (a :: Hakaru). (b -> PureAns abt a) -> PureAns abt a)
-> Eval abt b)
-> (forall (a :: Hakaru). (b -> PureAns abt a) -> PureAns abt a)
-> Eval abt b
forall a b. (a -> b) -> a -> b
$ \b -> PureAns abt a
c -> (a -> PureAns abt a) -> PureAns abt a
forall (a :: Hakaru). (a -> PureAns abt a) -> PureAns abt a
m ((a -> PureAns abt a) -> PureAns abt a)
-> (a -> PureAns abt a) -> PureAns abt a
forall a b. (a -> b) -> a -> b
$ \a
x -> Eval abt b -> (b -> PureAns abt a) -> PureAns abt a
forall (abt :: [Hakaru] -> Hakaru -> *) x.
Eval abt x
-> forall (a :: Hakaru). (x -> PureAns abt a) -> PureAns abt a
unEval (a -> Eval abt b
k a
x) b -> PureAns abt a
c
instance (ABT Term abt) => EvaluationMonad abt (Eval abt) 'Pure where
freshNat :: Eval abt Nat
freshNat =
(forall (a :: Hakaru). (Nat -> PureAns abt a) -> PureAns abt a)
-> Eval abt Nat
forall (abt :: [Hakaru] -> Hakaru -> *) x.
(forall (a :: Hakaru). (x -> PureAns abt a) -> PureAns abt a)
-> Eval abt x
Eval ((forall (a :: Hakaru). (Nat -> PureAns abt a) -> PureAns abt a)
-> Eval abt Nat)
-> (forall (a :: Hakaru). (Nat -> PureAns abt a) -> PureAns abt a)
-> Eval abt Nat
forall a b. (a -> b) -> a -> b
$ \Nat -> PureAns abt a
c (ListContext Nat
i [Statement abt Location 'Pure]
ss) ->
Nat -> PureAns abt a
c Nat
i (Nat -> [Statement abt Location 'Pure] -> ListContext abt 'Pure
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity).
Nat -> [Statement abt Location p] -> ListContext abt p
ListContext (Nat
iNat -> Nat -> Nat
forall a. Num a => a -> a -> a
+Nat
1) [Statement abt Location 'Pure]
ss)
unsafePush :: Statement abt Location 'Pure -> Eval abt ()
unsafePush Statement abt Location 'Pure
s =
(forall (a :: Hakaru). (() -> PureAns abt a) -> PureAns abt a)
-> Eval abt ()
forall (abt :: [Hakaru] -> Hakaru -> *) x.
(forall (a :: Hakaru). (x -> PureAns abt a) -> PureAns abt a)
-> Eval abt x
Eval ((forall (a :: Hakaru). (() -> PureAns abt a) -> PureAns abt a)
-> Eval abt ())
-> (forall (a :: Hakaru). (() -> PureAns abt a) -> PureAns abt a)
-> Eval abt ()
forall a b. (a -> b) -> a -> b
$ \() -> PureAns abt a
c (ListContext Nat
i [Statement abt Location 'Pure]
ss) ->
() -> PureAns abt a
c () (Nat -> [Statement abt Location 'Pure] -> ListContext abt 'Pure
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity).
Nat -> [Statement abt Location p] -> ListContext abt p
ListContext Nat
i (Statement abt Location 'Pure
sStatement abt Location 'Pure
-> [Statement abt Location 'Pure] -> [Statement abt Location 'Pure]
forall a. a -> [a] -> [a]
:[Statement abt Location 'Pure]
ss))
unsafePushes :: [Statement abt Location 'Pure] -> Eval abt ()
unsafePushes [Statement abt Location 'Pure]
ss =
(forall (a :: Hakaru). (() -> PureAns abt a) -> PureAns abt a)
-> Eval abt ()
forall (abt :: [Hakaru] -> Hakaru -> *) x.
(forall (a :: Hakaru). (x -> PureAns abt a) -> PureAns abt a)
-> Eval abt x
Eval ((forall (a :: Hakaru). (() -> PureAns abt a) -> PureAns abt a)
-> Eval abt ())
-> (forall (a :: Hakaru). (() -> PureAns abt a) -> PureAns abt a)
-> Eval abt ()
forall a b. (a -> b) -> a -> b
$ \() -> PureAns abt a
c (ListContext Nat
i [Statement abt Location 'Pure]
ss') ->
() -> PureAns abt a
c () (Nat -> [Statement abt Location 'Pure] -> ListContext abt 'Pure
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity).
Nat -> [Statement abt Location p] -> ListContext abt p
ListContext Nat
i ([Statement abt Location 'Pure] -> [Statement abt Location 'Pure]
forall a. [a] -> [a]
reverse [Statement abt Location 'Pure]
ss [Statement abt Location 'Pure]
-> [Statement abt Location 'Pure] -> [Statement abt Location 'Pure]
forall a. [a] -> [a] -> [a]
++ [Statement abt Location 'Pure]
ss'))
select :: Location a
-> (Statement abt Location 'Pure -> Maybe (Eval abt r))
-> Eval abt (Maybe r)
select Location a
x Statement abt Location 'Pure -> Maybe (Eval abt r)
p = [Statement abt Location 'Pure] -> Eval abt (Maybe r)
loop []
where
loop :: [Statement abt Location 'Pure] -> Eval abt (Maybe r)
loop [Statement abt Location 'Pure]
ss = do
Maybe (Statement abt Location 'Pure)
ms <- Eval abt (Maybe (Statement abt Location 'Pure))
forall (abt :: [Hakaru] -> Hakaru -> *).
Eval abt (Maybe (Statement abt Location 'Pure))
unsafePop
case Maybe (Statement abt Location 'Pure)
ms of
Maybe (Statement abt Location 'Pure)
Nothing -> do
[Statement abt Location 'Pure] -> Eval abt ()
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
(p :: Purity).
EvaluationMonad abt m p =>
[Statement abt Location p] -> m ()
unsafePushes [Statement abt Location 'Pure]
ss
Maybe r -> Eval abt (Maybe r)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe r
forall a. Maybe a
Nothing
Just Statement abt Location 'Pure
s ->
case Location a
x Location a -> Statement abt Location 'Pure -> Maybe ()
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *)
(p :: Purity).
Location a -> Statement abt Location p -> Maybe ()
`isBoundBy` Statement abt Location 'Pure
s Maybe () -> Maybe (Eval abt r) -> Maybe (Eval abt r)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Statement abt Location 'Pure -> Maybe (Eval abt r)
p Statement abt Location 'Pure
s of
Maybe (Eval abt r)
Nothing -> [Statement abt Location 'Pure] -> Eval abt (Maybe r)
loop (Statement abt Location 'Pure
sStatement abt Location 'Pure
-> [Statement abt Location 'Pure] -> [Statement abt Location 'Pure]
forall a. a -> [a] -> [a]
:[Statement abt Location 'Pure]
ss)
Just Eval abt r
mr -> do
r
r <- Eval abt r
mr
[Statement abt Location 'Pure] -> Eval abt ()
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
(p :: Purity).
EvaluationMonad abt m p =>
[Statement abt Location p] -> m ()
unsafePushes [Statement abt Location 'Pure]
ss
Maybe r -> Eval abt (Maybe r)
forall (m :: * -> *) a. Monad m => a -> m a
return (r -> Maybe r
forall a. a -> Maybe a
Just r
r)
unsafePop :: Eval abt (Maybe (Statement abt Location 'Pure))
unsafePop :: Eval abt (Maybe (Statement abt Location 'Pure))
unsafePop =
(forall (a :: Hakaru).
(Maybe (Statement abt Location 'Pure) -> PureAns abt a)
-> PureAns abt a)
-> Eval abt (Maybe (Statement abt Location 'Pure))
forall (abt :: [Hakaru] -> Hakaru -> *) x.
(forall (a :: Hakaru). (x -> PureAns abt a) -> PureAns abt a)
-> Eval abt x
Eval ((forall (a :: Hakaru).
(Maybe (Statement abt Location 'Pure) -> PureAns abt a)
-> PureAns abt a)
-> Eval abt (Maybe (Statement abt Location 'Pure)))
-> (forall (a :: Hakaru).
(Maybe (Statement abt Location 'Pure) -> PureAns abt a)
-> PureAns abt a)
-> Eval abt (Maybe (Statement abt Location 'Pure))
forall a b. (a -> b) -> a -> b
$ \Maybe (Statement abt Location 'Pure) -> PureAns abt a
c h :: ListContext abt 'Pure
h@(ListContext Nat
i [Statement abt Location 'Pure]
ss) ->
case [Statement abt Location 'Pure]
ss of
[] -> Maybe (Statement abt Location 'Pure) -> PureAns abt a
c Maybe (Statement abt Location 'Pure)
forall a. Maybe a
Nothing ListContext abt 'Pure
h
Statement abt Location 'Pure
s:[Statement abt Location 'Pure]
ss' -> Maybe (Statement abt Location 'Pure) -> PureAns abt a
c (Statement abt Location 'Pure
-> Maybe (Statement abt Location 'Pure)
forall a. a -> Maybe a
Just Statement abt Location 'Pure
s) (Nat -> [Statement abt Location 'Pure] -> ListContext abt 'Pure
forall (abt :: [Hakaru] -> Hakaru -> *) (p :: Purity).
Nat -> [Statement abt Location p] -> ListContext abt p
ListContext Nat
i [Statement abt Location 'Pure]
ss')
emit
:: (ABT Term abt)
=> Text
-> Sing a
-> (forall r. abt '[a] r -> abt '[] r)
-> Eval abt (Variable a)
emit :: Text
-> Sing a
-> (forall (r :: Hakaru). abt '[a] r -> abt '[] r)
-> Eval abt (Variable a)
emit Text
hint Sing a
typ forall (r :: Hakaru). abt '[a] r -> abt '[] r
f = do
Variable a
x <- Text -> Sing a -> Eval abt (Variable a)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
(a :: Hakaru).
EvaluationMonad abt m p =>
Text -> Sing a -> m (Variable a)
freshVar Text
hint Sing a
typ
(forall (a :: Hakaru).
(Variable a -> PureAns abt a) -> PureAns abt a)
-> Eval abt (Variable a)
forall (abt :: [Hakaru] -> Hakaru -> *) x.
(forall (a :: Hakaru). (x -> PureAns abt a) -> PureAns abt a)
-> Eval abt x
Eval ((forall (a :: Hakaru).
(Variable a -> PureAns abt a) -> PureAns abt a)
-> Eval abt (Variable a))
-> (forall (a :: Hakaru).
(Variable a -> PureAns abt a) -> PureAns abt a)
-> Eval abt (Variable a)
forall a b. (a -> b) -> a -> b
$ \Variable a -> PureAns abt a
c ListContext abt 'Pure
h -> (abt '[a] a -> abt '[] a
forall (r :: Hakaru). abt '[a] r -> abt '[] r
f (abt '[a] a -> abt '[] a)
-> (abt '[] a -> abt '[a] a) -> abt '[] a -> abt '[] a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Variable a -> abt '[] a -> abt '[a] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable a
x) (abt '[] a -> abt '[] a) -> abt '[] a -> abt '[] a
forall a b. (a -> b) -> a -> b
$ Variable a -> PureAns abt a
c Variable a
x ListContext abt 'Pure
h
emitLet :: (ABT Term abt) => abt '[] a -> Eval abt (Variable a)
emitLet :: abt '[] a -> Eval abt (Variable a)
emitLet abt '[] a
e =
abt '[] a
-> (Variable a -> Eval abt (Variable a))
-> (Term abt a -> Eval abt (Variable a))
-> Eval abt (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 -> Eval abt (Variable a)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Term abt a -> Eval abt (Variable a)) -> Eval abt (Variable a))
-> (Term abt a -> Eval abt (Variable a)) -> Eval abt (Variable a)
forall a b. (a -> b) -> a -> b
$ \Term abt a
_ ->
Text
-> Sing a
-> (forall (r :: Hakaru). abt '[a] r -> abt '[] r)
-> Eval abt (Variable a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Text
-> Sing a
-> (forall (r :: Hakaru). abt '[a] r -> abt '[] r)
-> Eval abt (Variable a)
emit Text
Text.empty (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] a
e) ((forall (r :: Hakaru). abt '[a] r -> abt '[] r)
-> Eval abt (Variable a))
-> (forall (r :: Hakaru). abt '[a] r -> abt '[] r)
-> Eval abt (Variable a)
forall a b. (a -> b) -> a -> b
$ \abt '[a] r
f ->
Term abt r -> abt '[] r
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (SCon '[LC a, '( '[a], r)] r
forall (a :: Hakaru) (b :: Hakaru). SCon '[LC a, '( '[a], b)] b
Let_ SCon '[LC a, '( '[a], r)] r
-> SArgs abt '[LC a, '( '[a], r)] -> Term abt r
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
(abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt '[] a
e abt '[] a
-> SArgs abt '[ '( '[a], r)] -> SArgs abt '[LC a, '( '[a], r)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* abt '[a] r
f abt '[a] r -> SArgs abt '[] -> SArgs abt '[ '( '[a], r)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs abt '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End)
emitLet' :: (ABT Term abt) => abt '[] a -> Eval abt (abt '[] a)
emitLet' :: abt '[] a -> Eval abt (abt '[] a)
emitLet' abt '[] a
e =
abt '[] a
-> (Variable a -> Eval abt (abt '[] a))
-> (Term abt a -> Eval abt (abt '[] a))
-> Eval abt (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 (Eval abt (abt '[] a) -> Variable a -> Eval abt (abt '[] a)
forall a b. a -> b -> a
const (Eval abt (abt '[] a) -> Variable a -> Eval abt (abt '[] a))
-> Eval abt (abt '[] a) -> Variable a -> Eval abt (abt '[] a)
forall a b. (a -> b) -> a -> b
$ abt '[] a -> Eval abt (abt '[] a)
forall (m :: * -> *) a. Monad m => a -> m a
return abt '[] a
e) ((Term abt a -> Eval abt (abt '[] a)) -> Eval abt (abt '[] a))
-> (Term abt a -> Eval abt (abt '[] a)) -> Eval abt (abt '[] a)
forall a b. (a -> b) -> a -> b
$ \Term abt a
t ->
case Term abt a
t of
Literal_ Literal a
_ -> abt '[] a -> Eval abt (abt '[] a)
forall (m :: * -> *) a. Monad m => a -> m a
return abt '[] a
e
Term abt a
_ -> do
Variable a
x <- Text
-> Sing a
-> (forall (r :: Hakaru). abt '[a] r -> abt '[] r)
-> Eval abt (Variable a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Text
-> Sing a
-> (forall (r :: Hakaru). abt '[a] r -> abt '[] r)
-> Eval abt (Variable a)
emit Text
Text.empty (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] a
e) ((forall (r :: Hakaru). abt '[a] r -> abt '[] r)
-> Eval abt (Variable a))
-> (forall (r :: Hakaru). abt '[a] r -> abt '[] r)
-> Eval abt (Variable a)
forall a b. (a -> b) -> a -> b
$ \abt '[a] r
f ->
Term abt r -> abt '[] r
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (SCon '[LC a, '( '[a], r)] r
forall (a :: Hakaru) (b :: Hakaru). SCon '[LC a, '( '[a], b)] b
Let_ SCon '[LC a, '( '[a], r)] r
-> SArgs abt '[LC a, '( '[a], r)] -> Term abt r
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
(abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt '[] a
e abt '[] a
-> SArgs abt '[ '( '[a], r)] -> SArgs abt '[LC a, '( '[a], r)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* abt '[a] r
f abt '[a] r -> SArgs abt '[] -> SArgs abt '[ '( '[a], r)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs abt '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End)
abt '[] a -> Eval abt (abt '[] a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable a
x)
emitUnpair
:: (ABT Term abt)
=> Whnf abt (HPair a b)
-> Eval abt (abt '[] a, abt '[] b)
emitUnpair :: Whnf abt (HPair a b) -> Eval abt (abt '[] a, abt '[] b)
emitUnpair (Head_ Head abt (HPair a b)
w) = (abt '[] a, abt '[] b) -> Eval abt (abt '[] a, abt '[] b)
forall (m :: * -> *) a. Monad m => a -> m a
return ((abt '[] a, abt '[] b) -> Eval abt (abt '[] a, abt '[] b))
-> (abt '[] a, abt '[] b) -> Eval abt (abt '[] a, abt '[] b)
forall a b. (a -> b) -> a -> b
$ Head abt (HPair a b) -> (abt '[] a, abt '[] b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
Head abt (HPair a b) -> (abt '[] a, abt '[] b)
reifyPair Head abt (HPair a b)
w
emitUnpair (Neutral abt '[] (HPair a b)
e) = do
let (Sing a
a,Sing b
b) = Sing (HPair a b) -> (Sing a, Sing b)
forall (a :: Hakaru) (b :: Hakaru).
Sing (HPair a b) -> (Sing a, Sing b)
sUnPair (abt '[] (HPair a b) -> Sing (HPair a b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] (HPair a b)
e)
Variable a
x <- Text -> Sing a -> Eval abt (Variable a)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
(a :: Hakaru).
EvaluationMonad abt m p =>
Text -> Sing a -> m (Variable a)
freshVar Text
Text.empty Sing a
a
Variable b
y <- Text -> Sing b -> Eval abt (Variable b)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
(a :: Hakaru).
EvaluationMonad abt m p =>
Text -> Sing a -> m (Variable a)
freshVar Text
Text.empty Sing b
b
Variable a
-> Variable b
-> abt '[] (HPair a b)
-> Eval abt (abt '[] a, abt '[] b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
Variable a
-> Variable b
-> abt '[] (HPair a b)
-> Eval abt (abt '[] a, abt '[] b)
emitUnpair_ Variable a
x Variable b
y abt '[] (HPair a b)
e
emitUnpair_
:: forall abt a b
. (ABT Term abt)
=> Variable a
-> Variable b
-> abt '[] (HPair a b)
-> Eval abt (abt '[] a, abt '[] b)
emitUnpair_ :: Variable a
-> Variable b
-> abt '[] (HPair a b)
-> Eval abt (abt '[] a, abt '[] b)
emitUnpair_ Variable a
x Variable b
y = abt '[] (HPair a b) -> Eval abt (abt '[] a, abt '[] b)
loop
where
done :: abt '[] (HPair a b) -> Eval abt (abt '[] a, abt '[] b)
done :: abt '[] (HPair a b) -> Eval abt (abt '[] a, abt '[] b)
done abt '[] (HPair a b)
e =
#ifdef __TRACE_DISINTEGRATE__
trace "-- emitUnpair: done (term is not Datum_ nor Case_)" $
#endif
(forall (a :: Hakaru).
((abt '[] a, abt '[] b) -> PureAns abt a) -> PureAns abt a)
-> Eval abt (abt '[] a, abt '[] b)
forall (abt :: [Hakaru] -> Hakaru -> *) x.
(forall (a :: Hakaru). (x -> PureAns abt a) -> PureAns abt a)
-> Eval abt x
Eval ((forall (a :: Hakaru).
((abt '[] a, abt '[] b) -> PureAns abt a) -> PureAns abt a)
-> Eval abt (abt '[] a, abt '[] b))
-> (forall (a :: Hakaru).
((abt '[] a, abt '[] b) -> PureAns abt a) -> PureAns abt a)
-> Eval abt (abt '[] a, abt '[] b)
forall a b. (a -> b) -> a -> b
$ \(abt '[] a, abt '[] b) -> PureAns abt a
c ListContext abt 'Pure
h ->
( Term abt a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn
(Term abt a -> abt '[] a)
-> (abt '[] a -> Term abt a) -> abt '[] a -> abt '[] a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. abt '[] (HPair a b) -> [Branch (HPair a b) abt a] -> Term abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
abt '[] a -> [Branch a abt b] -> Term abt b
Case_ abt '[] (HPair a b)
e
([Branch (HPair a b) abt a] -> Term abt a)
-> (abt '[] a -> [Branch (HPair a b) abt a])
-> abt '[] a
-> Term abt a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Branch (HPair a b) abt a
-> [Branch (HPair a b) abt a] -> [Branch (HPair a b) abt a]
forall a. a -> [a] -> [a]
:[])
(Branch (HPair a b) abt a -> [Branch (HPair a b) abt a])
-> (abt '[] a -> Branch (HPair a b) abt a)
-> abt '[] a
-> [Branch (HPair a b) abt a]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Pattern '[a, b] (HPair a b)
-> abt '[a, b] a -> Branch (HPair a b) abt a
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *) (b :: Hakaru)
(xs :: [Hakaru]).
Pattern xs a -> abt xs b -> Branch a abt b
Branch (Pattern '[a] a
-> Pattern '[b] b -> Pattern ('[a] ++ '[b]) (HPair a b)
forall (vars1 :: [Hakaru]) (a :: Hakaru) (vars2 :: [Hakaru])
(b :: Hakaru).
Pattern vars1 a
-> Pattern vars2 b -> Pattern (vars1 ++ vars2) (HPair a b)
pPair Pattern '[a] a
forall (a :: Hakaru). Pattern '[a] a
PVar Pattern '[b] b
forall (a :: Hakaru). Pattern '[a] a
PVar)
(abt '[a, b] a -> Branch (HPair a b) abt a)
-> (abt '[] a -> abt '[a, b] a)
-> abt '[] a
-> Branch (HPair a b) abt a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Variable a -> abt '[b] a -> abt '[a, b] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable a
x
(abt '[b] a -> abt '[a, b] a)
-> (abt '[] a -> abt '[b] a) -> abt '[] a -> abt '[a, b] a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Variable b -> abt '[] a -> abt '[b] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable b
y
) (abt '[] a -> abt '[] a) -> abt '[] a -> abt '[] a
forall a b. (a -> b) -> a -> b
$ (abt '[] a, abt '[] b) -> PureAns abt a
c (Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable a
x, Variable b -> abt '[] b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable b
y) ListContext abt 'Pure
h
loop :: abt '[] (HPair a b) -> Eval abt (abt '[] a, abt '[] b)
loop :: abt '[] (HPair a b) -> Eval abt (abt '[] a, abt '[] b)
loop abt '[] (HPair a b)
e0 =
abt '[] (HPair a b)
-> (Variable (HPair a b) -> Eval abt (abt '[] a, abt '[] b))
-> (Term abt (HPair a b) -> Eval abt (abt '[] a, abt '[] b))
-> Eval abt (abt '[] a, abt '[] b)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) r.
ABT syn abt =>
abt '[] a -> (Variable a -> r) -> (syn abt a -> r) -> r
caseVarSyn abt '[] (HPair a b)
e0 (abt '[] (HPair a b) -> Eval abt (abt '[] a, abt '[] b)
done (abt '[] (HPair a b) -> Eval abt (abt '[] a, abt '[] b))
-> (Variable (HPair a b) -> abt '[] (HPair a b))
-> Variable (HPair a b)
-> Eval abt (abt '[] a, abt '[] b)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Variable (HPair a b) -> abt '[] (HPair a b)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var) ((Term abt (HPair a b) -> Eval abt (abt '[] a, abt '[] b))
-> Eval abt (abt '[] a, abt '[] b))
-> (Term abt (HPair a b) -> Eval abt (abt '[] a, abt '[] b))
-> Eval abt (abt '[] a, abt '[] b)
forall a b. (a -> b) -> a -> b
$ \Term abt (HPair a b)
t ->
case Term abt (HPair a b)
t of
Datum_ Datum (abt '[]) (HData' t)
d -> do
#ifdef __TRACE_DISINTEGRATE__
trace "-- emitUnpair: found Datum_" $ return ()
#endif
(abt '[] a, abt '[] b) -> Eval abt (abt '[] a, abt '[] b)
forall (m :: * -> *) a. Monad m => a -> m a
return ((abt '[] a, abt '[] b) -> Eval abt (abt '[] a, abt '[] b))
-> (abt '[] a, abt '[] b) -> Eval abt (abt '[] a, abt '[] b)
forall a b. (a -> b) -> a -> b
$ Head abt (HPair a b) -> (abt '[] a, abt '[] b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
Head abt (HPair a b) -> (abt '[] a, abt '[] b)
reifyPair (Datum (abt '[]) (HData' t) -> Head abt (HData' t)
forall (abt :: [Hakaru] -> Hakaru -> *) (t :: HakaruCon).
Datum (abt '[]) (HData' t) -> Head abt (HData' t)
WDatum Datum (abt '[]) (HData' t)
d)
Case_ abt '[] a
e [Branch a abt (HPair a b)]
bs -> do
#ifdef __TRACE_DISINTEGRATE__
trace "-- emitUnpair: going under Case_" $ return ()
#endif
(abt '[] (HPair a b) -> Eval abt (abt '[] a, abt '[] b))
-> abt '[] a
-> [Branch a abt (HPair a b)]
-> Eval abt (abt '[] a, abt '[] b)
forall (abt :: [Hakaru] -> Hakaru -> *) (b :: Hakaru) r
(a :: Hakaru).
ABT Term abt =>
(abt '[] b -> Eval abt r)
-> abt '[] a -> [Branch a abt b] -> Eval abt r
emitCaseWith abt '[] (HPair a b) -> Eval abt (abt '[] a, abt '[] b)
loop abt '[] a
e [Branch a abt (HPair a b)]
bs
Term abt (HPair a b)
_ -> abt '[] (HPair a b) -> Eval abt (abt '[] a, abt '[] b)
done abt '[] (HPair a b)
e0
emitFork_
:: (ABT Term abt, T.Traversable t)
=> (forall r. t (abt '[] r) -> abt '[] r)
-> t (Eval abt a)
-> Eval abt a
emitFork_ :: (forall (r :: Hakaru). t (abt '[] r) -> abt '[] r)
-> t (Eval abt a) -> Eval abt a
emitFork_ forall (r :: Hakaru). t (abt '[] r) -> abt '[] r
f t (Eval abt a)
ms =
(forall (a :: Hakaru). (a -> PureAns abt a) -> PureAns abt a)
-> Eval abt a
forall (abt :: [Hakaru] -> Hakaru -> *) x.
(forall (a :: Hakaru). (x -> PureAns abt a) -> PureAns abt a)
-> Eval abt x
Eval ((forall (a :: Hakaru). (a -> PureAns abt a) -> PureAns abt a)
-> Eval abt a)
-> (forall (a :: Hakaru). (a -> PureAns abt a) -> PureAns abt a)
-> Eval abt a
forall a b. (a -> b) -> a -> b
$ \a -> PureAns abt a
c ListContext abt 'Pure
h -> t (abt '[] a) -> abt '[] a
forall (r :: Hakaru). t (abt '[] r) -> abt '[] r
f (t (abt '[] a) -> abt '[] a) -> t (abt '[] a) -> abt '[] a
forall a b. (a -> b) -> a -> b
$ (Eval abt a -> abt '[] a) -> t (Eval abt a) -> t (abt '[] a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Eval abt a
m -> Eval abt a -> (a -> PureAns abt a) -> PureAns abt a
forall (abt :: [Hakaru] -> Hakaru -> *) x.
Eval abt x
-> forall (a :: Hakaru). (x -> PureAns abt a) -> PureAns abt a
unEval Eval abt a
m a -> PureAns abt a
c ListContext abt 'Pure
h) t (Eval abt a)
ms
emitCaseWith
:: (ABT Term abt)
=> (abt '[] b -> Eval abt r)
-> abt '[] a
-> [Branch a abt b]
-> Eval abt r
emitCaseWith :: (abt '[] b -> Eval abt r)
-> abt '[] a -> [Branch a abt b] -> Eval abt r
emitCaseWith abt '[] b -> Eval abt r
f abt '[] a
e [Branch a abt b]
bs = do
[GBranch a (Eval abt r)]
gms <- [Branch a abt b]
-> (Branch a abt b -> Eval abt (GBranch a (Eval abt r)))
-> Eval abt [GBranch a (Eval abt r)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
T.for [Branch a abt b]
bs ((Branch a abt b -> Eval abt (GBranch a (Eval abt r)))
-> Eval abt [GBranch a (Eval abt r)])
-> (Branch a abt b -> Eval abt (GBranch a (Eval abt r)))
-> Eval abt [GBranch a (Eval abt r)]
forall a b. (a -> b) -> a -> b
$ \(Branch Pattern xs a
pat abt xs b
body) ->
let (List1 Variable xs
vars, abt '[] b
body') = abt xs b -> (List1 Variable xs, abt '[] b)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> (List1 Variable xs, abt '[] a)
caseBinds abt xs b
body
in (\List1 Variable xs
vars' ->
let rho :: Assocs (abt '[])
rho = List1 Variable xs -> List1 (abt '[]) xs -> Assocs (abt '[])
forall k (xs :: [k]) (ast :: k -> *).
List1 Variable xs -> List1 ast xs -> Assocs ast
toAssocs1 List1 Variable xs
vars ((forall (i :: Hakaru). Variable i -> abt '[] i)
-> List1 Variable xs -> List1 (abt '[]) xs
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *)
(b :: k1 -> *) (j :: k2).
Functor11 f =>
(forall (i :: k1). a i -> b i) -> f a j -> f b j
fmap11 forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
forall (i :: Hakaru). Variable i -> abt '[] i
var List1 Variable xs
vars')
in Pattern xs a
-> List1 Variable xs -> Eval abt r -> GBranch a (Eval abt r)
forall (a :: Hakaru) r (xs :: [Hakaru]).
Pattern xs a -> List1 Variable xs -> r -> GBranch a r
GBranch Pattern xs a
pat List1 Variable xs
vars' (abt '[] b -> Eval abt r
f (abt '[] b -> Eval abt r) -> abt '[] b -> Eval abt r
forall a b. (a -> b) -> a -> b
$ Assocs (abt '[]) -> abt '[] b -> abt '[] b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
(ABT syn abt, JmEq1 Sing, Show1 Sing, Traversable21 syn) =>
Assocs (abt '[]) -> abt xs a -> abt xs a
substs Assocs (abt '[])
rho abt '[] b
body')
) (List1 Variable xs -> GBranch a (Eval abt r))
-> Eval abt (List1 Variable xs)
-> Eval abt (GBranch a (Eval abt r))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 Variable xs -> Eval abt (List1 Variable xs)
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *) (p :: Purity)
(xs :: [Hakaru]).
EvaluationMonad abt m p =>
List1 Variable xs -> m (List1 Variable xs)
freshenVars List1 Variable xs
vars
(forall (a :: Hakaru). (r -> PureAns abt a) -> PureAns abt a)
-> Eval abt r
forall (abt :: [Hakaru] -> Hakaru -> *) x.
(forall (a :: Hakaru). (x -> PureAns abt a) -> PureAns abt a)
-> Eval abt x
Eval ((forall (a :: Hakaru). (r -> PureAns abt a) -> PureAns abt a)
-> Eval abt r)
-> (forall (a :: Hakaru). (r -> PureAns abt a) -> PureAns abt a)
-> Eval abt r
forall a b. (a -> b) -> a -> b
$ \r -> PureAns abt a
c ListContext abt 'Pure
h ->
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 (abt '[] a -> [Branch a abt a] -> Term abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
abt '[] a -> [Branch a abt b] -> Term abt b
Case_ abt '[] a
e
((GBranch a (Eval abt r) -> Branch a abt a)
-> [GBranch a (Eval abt r)] -> [Branch a abt a]
forall a b. (a -> b) -> [a] -> [b]
map (GBranch a (abt '[] a) -> Branch a abt a
forall (syn :: ([Hakaru] -> Hakaru -> *) -> Hakaru -> *)
(abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
ABT syn abt =>
GBranch a (abt '[] b) -> Branch a abt b
fromGBranch (GBranch a (abt '[] a) -> Branch a abt a)
-> (GBranch a (Eval abt r) -> GBranch a (abt '[] a))
-> GBranch a (Eval abt r)
-> Branch a abt a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Eval abt r -> abt '[] a)
-> GBranch a (Eval abt r) -> GBranch a (abt '[] a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Eval abt r
m -> Eval abt r -> (r -> PureAns abt a) -> PureAns abt a
forall (abt :: [Hakaru] -> Hakaru -> *) x.
Eval abt x
-> forall (a :: Hakaru). (x -> PureAns abt a) -> PureAns abt a
unEval Eval abt r
m r -> PureAns abt a
c ListContext abt 'Pure
h)) [GBranch a (Eval abt r)]
gms))
{-# INLINE emitCaseWith #-}