{-# LANGUAGE CPP
           , GADTs
           , KindSignatures
           , DataKinds
           , Rank2Types
           , ScopedTypeVariables
           , MultiParamTypeClasses
           , FlexibleContexts
           , FlexibleInstances
           #-}

{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
--                                                    2016.05.24
-- |
-- Module      :  Language.Hakaru.Evaluation.EvalMonad
-- Copyright   :  Copyright (c) 2016 the Hakaru team
-- License     :  BSD3
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  experimental
-- Portability :  GHC-only
--
--
----------------------------------------------------------------
module Language.Hakaru.Evaluation.EvalMonad
    ( runPureEvaluate
    , pureEvaluate

    -- * The pure-evaluation monad
    -- ** List-based version
    , ListContext(..), PureAns, Eval(..), runEval
    , residualizePureListContext
    -- ** TODO: IntMap-based version
    ) 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(..))


-- The rest of these are just for the emit code, which isn't currently exported.
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

----------------------------------------------------------------
----------------------------------------------------------------
-- | Call 'evaluate' on a term. This variant returns an @abt@ expression itself so you needn't worry about the 'Eval' monad. For the monadic-version, see 'pureEvaluate'.
--
-- BUG: now that we've indexed 'ListContext' by a 'Purity', does exposing the implementation details still enable clients to break our invariants?
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]


-- 'evaluate' itself can never @lub@ or @bot@, as captured by the
-- fact that it's type doesn't include 'Alternative' nor 'MonadPlus'
-- constraints. So non-singularity of results could only come from
-- calling @perform@. However, we will never call perform because: (a) the initial heap must be 'Pure' so we will never call @perform@ for a statement on the initial heap, and (b) 'evaluate' itself will never push impure statements so we will never call @perform@ for the statements we push either.
--
-- | Call 'evaluate' on a term. This variant returns something in the 'Eval' monad so you can string multiple evaluation calls together. For the non-monadic version, see 'runPureEvaluate'.
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")


-- | Run a computation in the 'Eval' monad, residualizing out all the
-- statements in the final evaluation context. The second argument
-- should include all the terms altered by the 'Eval' expression; this
-- is necessary to ensure proper hygiene; for example(s):
--
-- > runEval (pureEvaluate e) [Some2 e]
--
-- We use 'Some2' on the inputs because it doesn't matter what their
-- type or locally-bound variables are, so we want to allow @f@ to
-- contain terms with different indices.
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
    -- TODO: make paremetric in the purity, so we can combine 'residualizeListContext' with this function.
    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
            -- TODO: if used exactly once in @e@, then inline.
            | Bool
otherwise ->
                case Lazy abt a -> Maybe (Variable a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Lazy abt a -> Maybe (Variable a)
getLazyVariable Lazy abt a
body of
                Just Variable a
y  -> Variable a -> abt '[] a -> abt '[] 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))

    -- N.B., the use of 'reverse' is necessary so that the order
    -- of pushing matches that of 'pushes'
    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
        -- TODO: use a DList to avoid reversing inside 'unsafePushes'
        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  ->
                    -- Alas, @p@ will have to recheck 'isBoundBy'
                    -- in order to grab the 'Refl' proof we erased;
                    -- but there's nothing to be done for it.
                    case Location a
x Location a -> Statement abt Location '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)

-- TODO: make parametric in the purity
-- | Not exported because we only need it for defining 'select' on 'Eval'.
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 some code that binds a variable, and return the variable
-- thus bound. The function says what to wrap the result of the
-- continuation with; i.e., what we're actually emitting.
emit
    :: (ABT Term abt)
    => 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


-- | A smart constructor for emitting let-bindings. If the input
-- is already a variable then we just return it; otherwise we emit
-- the let-binding. N.B., this function provides the invariant that
-- the result is in fact a variable; whereas 'emitLet'' does not.
emitLet :: (ABT Term abt) => 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)

-- | A smart constructor for emitting let-bindings. If the input
-- is already a variable or a literal constant, then we just return
-- it; otherwise we emit the let-binding. N.B., this function
-- provides weaker guarantees on the type of the result; if you
-- require the result to always be a variable, then see 'emitLet'
-- instead.
emitLet' :: (ABT Term abt) => 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)

-- | A smart constructor for emitting \"unpair\". If the input
-- argument is actually a constructor then we project out the two
-- components; otherwise we emit the case-binding and return the
-- two variables.
emitUnpair
    :: (ABT Term abt)
    => 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
                -- TODO: we want this to duplicate the current
                -- continuation for (the evaluation of @loop@ in)
                -- all branches. So far our traces all end up
                -- returning @bot@ on the first branch, and hence
                -- @bot@ for the whole case-expression, so we can't
                -- quite tell whether it does what is intended.
                --
                -- N.B., the only 'Eval'-effects in 'applyBranch'
                -- are to freshen variables; thus this use of
                -- 'traverse' is perfectly sound.
                (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

-- TODO: emitUneither

-- | Run each of the elements of the traversable using the same
-- heap and continuation for each one, then pass the results to a
-- function for emitting code.
emitFork_
    :: (ABT Term abt, 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 #-}

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