{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Data.Comp.AG
( runAG
, runRewrite
, module I
) where
import Data.Comp.AG.Internal
import qualified Data.Comp.AG.Internal as I hiding (explicit)
import Data.Comp.Algebra
import Data.Comp.Mapping as I
import Data.Comp.Term
import Data.Comp.Projection as I
runAG :: forall f u d . Traversable f
=> Syn' f (u,d) u
-> Inh' f (u,d) d
-> (u -> d)
-> Term f
-> u
runAG up down dinit t = uFin where
uFin = run dFin t
dFin = dinit uFin
run :: d -> Term f -> u
run d (Term t) = u where
t' = fmap bel $ number t
bel (Numbered i s) =
let d' = lookupNumMap d i m
in Numbered i (run d' s, d')
m = explicit down (u,d) unNumbered t'
u = explicit up (u,d) unNumbered t'
runRewrite :: forall f g u d . (Traversable f, Functor g)
=> Syn' f (u,d) u -> Inh' f (u,d) d
-> Rewrite f (u,d) g
-> (u -> d)
-> Term f
-> (u, Term g)
runRewrite up down trans dinit t = res where
res@(uFin,_) = run dFin t
dFin = dinit uFin
run :: d -> Term f -> (u, Term g)
run d (Term t) = (u,t'') where
t' = fmap bel $ number t
bel (Numbered i s) =
let d' = lookupNumMap d i m
(u', s') = run d' s
in Numbered i ((u', d'),s')
m = explicit down (u,d) (fst . unNumbered) t'
u = explicit up (u,d) (fst . unNumbered) t'
t'' = appCxt $ fmap (snd . unNumbered) $ explicit trans (u,d) (fst . unNumbered) t'