-- | Some combinators to express breadth-first evaluation of catamorphisms,
-- which allows you to stepwise evaluate the results of children. If,
-- during the evaluation of an alternative, a choice needs to be made between taking
-- the results of its children, with these combinators, you can stepwise
-- evaluate the children in parallel, until a choice can be made.
-- Until a choice is made, evaluation proceeds strictly; after a choice
-- is made, evaluation proceeds lazily.
-- What constitutes to be a step is determined by the callee.

{-# LANGUAGE GADTs, TypeFamilies, EmptyDataDecls #-}
module Data.BreadthFirstCata.Cata (Sem(Sem),Inh,Syn,Comp,invoke,final,info,resume,inject,sem_Inject,Inject,lazyEval,oneStep,Outcome(Step,Fin)) where


-- | Semantics of a nonterminal of type @n@ as a function from inherited
-- attributes (@Inh n@) to a computation @Comp i n@ of synthesized attributes (@Syn n@).

newtype Sem i n = Sem (Inh n -> Comp i n)
data family Inh n    -- index @n@ uniquely determines the type of the inherited and
data family Syn n    -- synthesized attributes.


-- | Computation of synthesized attributes of nonterminal of type @n@.
-- It is a trace of @Info@-effects, that keeps track of the intermediate
-- states of the tree (using @Pending@), ending ultimately in the
-- synthesized values (using @Final@).
-- Operationally, we lift @Info@-values over @Pending@-values, thereby
-- gradually rewriting the latter, until it results in a @Final@.

data Comp i n where
  Pending :: Parents i m n -> Comp i m -> Comp i n
  Final   :: Syn n -> Comp i n
  Info    :: i -> Comp i n -> Comp i n


-- | Given a node of type @m@ that is currently being evaluated for a
-- tree of type @n@, @Parents i m n@ is the stack of its parent nodes
-- (that wait for values of their children to continue evaluation).
-- The outermost @Cont@-value) is the top of the stack, i.e. the direct
-- parent of the formerly mentioned node.

data Parents i m n where
  Cont :: Node i m k -> Parents i k n -> Parents i m n
  Root :: Parents i n n


-- | Explicit closure for a node that expects results of a child of type @m@
-- in order to continue evaluation. The state of a node consists of the
-- (still needed) results of already constructed children and local
-- attributes.

newtype Node i m n = Node (Syn m -> Comp i n)


-- | Lazy evaluation of a computation.
-- Note: we cannot inspect the effect-trace, as it would sequentialize
-- the evaluation of children.

lazyEval :: Comp i a -> Syn a
lazyEval (Pending stack r) = evalParents stack (lazyEval r)
lazyEval (Final v)  = v
lazyEval (Info _ r) = lazyEval r

evalParents :: Parents i m n -> Syn m -> Syn n
evalParents Root v = v
evalParents (Cont (Node f) c) v = evalParents c (lazyEval (f v))


-- | Result of one step evaluation: either the final result
-- or an updated computation. What constitutes to a step
-- depends on the application: evaluation proceeds until
-- an outcome can be given.

data Outcome i a
  = Fin  (Syn a)
  | Step i (Comp i a)


-- | One step strict evaluation. Reduction proceeds until
-- the computation is either finished or yields an @Info@-effect.

oneStep :: Comp i a -> Outcome i a
oneStep (Pending stack r)
  = case oneStep r of
      Fin v     -> oneStep (reduceParent stack v)
      Step i r' -> Step i (Pending stack r')
oneStep (Final v)  = Fin v
oneStep (Info i r) = Step i r

reduceParent :: Parents i m n -> Syn m -> Comp i n
reduceParent Root v = Final v
reduceParent (Cont (Node f) c) v = Pending c (f v)


-- | Unwrapper for @Sem@.
invoke :: Sem i n -> Inh n -> Comp i n
invoke (Sem f) = f

-- | Wrapper for final result.
final :: Syn n -> Comp i n
final = Final

-- | Wrapper for an effect.
info :: i -> Comp i n -> Comp i n
info = Info

-- | Create a |Pending| computation that waits for the given computation.
resume :: Comp i m -> (Syn m -> Comp i n) -> Comp i n
resume c k = Pending (Cont (Node k) Root) c


-- | Injection of steps as conventional call

data Inject
data instance Inh Inject = Inh_Inject {}
data instance Syn Inject = Syn_Inject {}

sem_Inject :: Sem i Inject
sem_Inject = Sem (const $ final $ Syn_Inject {})

inject :: i -> Comp i Inject
inject i = info i $ final $ Syn_Inject {}