-- | 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, RankNTypes, MultiParamTypeClasses, FlexibleInstances, BangPatterns #-} module Data.BreadthFirstCata.Cata (Child(Child),Inh,Syn,Comp ,invoke,final,info,resume ,inject,sem_Inject,Inject,lazyEval,oneStep,Outcome(Step,Fin)) where -- | Semantics of a child of type @n@ as a function from inherited -- attributes (@Inh n@) to a computation @Comp i n@ of synthesized attributes (@Syn n@). newtype Child i n = Child (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 n' n) -> Comp i n' -> 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 n' n where Cont :: !(Node i n' k) -> !(Parents i k n) -> Parents i n' 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 n' n = Node (Syn n' -> 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 n -> Syn n lazyEval (Pending stack r) = evalParents stack (lazyEval r) lazyEval (Final v) = v lazyEval (Info _ r) = lazyEval r evalParents :: Parents i n' n -> Syn n' -> 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 n = Fin !(Syn n) | Step !i (Comp i n) -- | One step strict evaluation. Reduction proceeds until -- the computation is either finished or yields an @Info@-effect. oneStep :: Comp i n -> Outcome i n 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 n' n -> Syn n' -> Comp i n reduceParent Root v = Final v reduceParent (Cont (Node f) c) v = Pending c (f v) -- | Unwraps a @Child@ invoke :: Child i n -> Inh n -> Comp i n invoke (Child f) inh = f inh -- | 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 n' -> (Syn n' -> 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 :: Child i Inject sem_Inject = Child (const \$ final \$ Syn_Inject {}) inject :: i -> Comp i Inject inject i = info i \$ final \$ Syn_Inject {}