module Data.Comp.Automata
(
QHom
, below
, above
, pureHom
, upTrans
, runUpHom
, runUpHomSt
, downTrans
, runDownHom
, runQHom
, UpTrans
, UpTrans'
, mkUpTrans
, runUpTrans
, compUpTrans
, compUpTransHom
, compHomUpTrans
, compUpTransSig
, compSigUpTrans
, compAlgUpTrans
, UpState
, tagUpState
, runUpState
, prodUpState
, DUpState
, dUpState
, upState
, runDUpState
, prodDUpState
, (|*|)
, DownTrans
, DownTrans'
, mkDownTrans
, runDownTrans
, compDownTrans
, compDownTransSig
, compSigDownTrans
, compDownTransHom
, compHomDownTrans
, DownState
, tagDownState
, prodDownState
, DDownState
, dDownState
, downState
, prodDDownState
, (>*<)
, runDState
, (&)
, (|->)
, o
, module Data.Comp.Automata.Product
) where
import Data.Comp.Number
import Data.Comp.Automata.Product
import Data.Comp.Term
import Data.Comp.Algebra
import Data.Map (Map)
import qualified Data.Map as Map
infix 1 |->
infixr 0 &
(&) :: Ord k => Map k v -> Map k v -> Map k v
(&) = Map.union
(|->) :: k -> a -> Map k a
(|->) = Map.singleton
o :: Map k a
o = Map.empty
below :: (?below :: a -> q, p :< q) => a -> p
below = pr . ?below
above :: (?above :: q, p :< q) => p
above = pr ?above
explicit :: ((?above :: q, ?below :: a -> q) => b) -> q -> (a -> q) -> b
explicit x ab be = x where ?above = ab; ?below = be
type QHom f q g = forall a . (?below :: a -> q, ?above :: q) => f a -> Context g a
pureHom :: (forall q . QHom f q g) -> Hom f g
pureHom phom t = let ?above = undefined
?below = const undefined
in phom t
type UpTrans f q g = forall a. f (q,a) -> (q, Context g a)
type UpTrans' f q g = forall a. f (q,Context g a) -> (q, Context g a)
mkUpTrans :: Functor f => UpTrans' f q g -> UpTrans f q g
mkUpTrans tr t = tr $ fmap (\(q,a) -> (q, Hole a)) t
upAlg :: (Functor g) => UpTrans f q g -> Alg f (q, Term g)
upAlg trans = fmap appCxt . trans
runUpTrans :: (Functor f, Functor g) => UpTrans f q g -> Term f -> Term g
runUpTrans trans = snd . runUpTransSt trans
runUpTransSt :: (Functor f, Functor g) => UpTrans f q g -> Term f -> (q, Term g)
runUpTransSt = cata . upAlg
runUpTrans' :: (Functor f, Functor g) => UpTrans f q g -> Context f (q,a) -> (q, Context g a)
runUpTrans' trans = run where
run (Hole (q,a)) = (q, Hole a)
run (Term t) = fmap appCxt $ trans $ fmap run t
compUpTrans :: (Functor f, Functor g, Functor h)
=> UpTrans g p h -> UpTrans f q g -> UpTrans f (q,p) h
compUpTrans t2 t1 x = ((q1,q2), c2) where
(q1, c1) = t1 $ fmap (\((q1,q2),a) -> (q1,(q2,a))) x
(q2, c2) = runUpTrans' t2 c1
compAlgUpTrans :: (Functor g)
=> Alg g a -> UpTrans f q g -> Alg f (q,a)
compAlgUpTrans alg trans = fmap (cata' alg) . trans
compSigUpTrans :: (Functor g) => SigFun g h -> UpTrans f q g -> UpTrans f q h
compSigUpTrans sig trans x = (q, appSigFun sig x') where
(q, x') = trans x
compUpTransSig :: UpTrans g q h -> SigFun f g -> UpTrans f q h
compUpTransSig trans sig = trans . sig
compHomUpTrans :: (Functor g, Functor h) => Hom g h -> UpTrans f q g -> UpTrans f q h
compHomUpTrans hom trans x = (q, appHom hom x') where
(q, x') = trans x
compUpTransHom :: (Functor g, Functor h) => UpTrans g q h -> Hom f g -> UpTrans f q h
compUpTransHom trans hom x = runUpTrans' trans . hom $ x
type UpState f q = Alg f q
tagUpState :: (Functor f) => (q -> p) -> (p -> q) -> UpState f q -> UpState f p
tagUpState i o s = i . s . fmap o
runUpState :: (Functor f) => UpState f q -> Term f -> q
runUpState = cata
prodUpState :: Functor f => UpState f p -> UpState f q -> UpState f (p,q)
prodUpState sp sq t = (p,q) where
p = sp $ fmap fst t
q = sq $ fmap snd t
upTrans :: (Functor f, Functor g) => UpState f q -> QHom f q g -> UpTrans f q g
upTrans st f t = (q, c)
where q = st $ fmap fst t
c = fmap snd $ explicit f q fst t
runUpHom :: (Functor f, Functor g) => UpState f q -> QHom f q g -> Term f -> Term g
runUpHom st hom = snd . runUpHomSt st hom
runUpHomSt :: (Functor f, Functor g) => UpState f q -> QHom f q g -> Term f -> (q,Term g)
runUpHomSt alg h = runUpTransSt (upTrans alg h)
type DUpState f p q = (q :< p) => DUpState' f p q
type DUpState' f p q = forall a . (?below :: a -> p, ?above :: p) => f a -> q
dUpState :: Functor f => UpState f q -> DUpState f p q
dUpState f = f . fmap below
upState :: DUpState f q q -> UpState f q
upState f s = res where res = explicit f res id s
runDUpState :: Functor f => DUpState f q q -> Term f -> q
runDUpState = runUpState . upState
prodDUpState :: (p :< c, q :< c)
=> DUpState f c p -> DUpState f c q -> DUpState f c (p,q)
prodDUpState sp sq t = (sp t, sq t)
(|*|) :: (p :< c, q :< c)
=> DUpState f c p -> DUpState f c q -> DUpState f c (p,q)
(|*|) = prodDUpState
type DownTrans f q g = forall a. q -> f (q -> a) -> Context g a
type DownTrans' f q g = forall a. q -> f (q -> Context g a) -> Context g a
mkDownTrans :: Functor f => DownTrans' f q g -> DownTrans f q g
mkDownTrans tr q t = tr q (fmap (Hole .) t)
runDownTrans :: (Functor f, Functor g) => DownTrans f q g -> q -> Cxt h f a -> Cxt h g a
runDownTrans tr q t = run t q where
run (Term t) q = appCxt $ tr q $ fmap run t
run (Hole a) _ = Hole a
runDownTrans' :: (Functor f, Functor g) => DownTrans f q g -> q -> Cxt h f (q -> a) -> Cxt h g a
runDownTrans' tr q t = run t q where
run (Term t) q = appCxt $ tr q $ fmap run $ t
run (Hole a) q = Hole (a q)
compDownTrans :: (Functor f, Functor g, Functor h)
=> DownTrans g p h -> DownTrans f q g -> DownTrans f (q,p) h
compDownTrans t2 t1 (q,p) t = runDownTrans' t2 p $ t1 q (fmap curry t)
compSigDownTrans :: (Functor g) => SigFun g h -> DownTrans f q g -> DownTrans f q h
compSigDownTrans sig trans q = appSigFun sig . trans q
compDownTransSig :: DownTrans g q h -> SigFun f g -> DownTrans f q h
compDownTransSig trans hom q t = trans q (hom t)
compHomDownTrans :: (Functor g, Functor h)
=> Hom g h -> DownTrans f q g -> DownTrans f q h
compHomDownTrans hom trans q = appHom hom . trans q
compDownTransHom :: (Functor g, Functor h)
=> DownTrans g q h -> Hom f g -> DownTrans f q h
compDownTransHom trans hom q t = runDownTrans' trans q (hom t)
type DownState f q = forall a. Ord a => (q, f a) -> Map a q
tagDownState :: (q -> p) -> (p -> q) -> DownState f q -> DownState f p
tagDownState i o t (q,s) = fmap i $ t (o q,s)
prodDownState :: DownState f p -> DownState f q -> DownState f (p,q)
prodDownState sp sq ((p,q),t) = prodMap p q (sp (p, t)) (sq (q, t))
data ProdState p q = LState p
| RState q
| BState p q
prodMap :: (Ord i) => p -> q -> Map i p -> Map i q -> Map i (p,q)
prodMap p q mp mq = Map.map final $ Map.unionWith combine ps qs
where ps = Map.map LState mp
qs = Map.map RState mq
combine (LState p) (RState q) = BState p q
combine (RState q) (LState p) = BState p q
combine _ _ = error "unexpected merging"
final (LState p) = (p, q)
final (RState q) = (p, q)
final (BState p q) = (p,q)
appMap :: Traversable f => (forall i . Ord i => f i -> Map i q)
-> q -> f (q -> b) -> f (q,b)
appMap qmap q s = fmap qfun s'
where s' = number s
qfun k@(Numbered (_,a)) = let q' = Map.findWithDefault q k (qmap s')
in (q', a q')
downTrans :: (Traversable f, Functor g) => DownState f q -> QHom f q g -> DownTrans f q g
downTrans st f q s = fmap snd $ explicit f q fst (appMap (curry st q) q s)
runDownHom :: (Traversable f, Functor g)
=> DownState f q -> QHom f q g -> q -> Term f -> Term g
runDownHom st h = runDownTrans (downTrans st h)
type DDownState f p q = (q :< p) => DDownState' f p q
type DDownState' f p q = forall i . (Ord i, ?below :: i -> p, ?above :: p)
=> f i -> Map i q
dDownState :: DownState f q -> DDownState f p q
dDownState f t = f (above,t)
downState :: DDownState f q q -> DownState f q
downState f (q,s) = res
where res = explicit f q bel s
bel k = Map.findWithDefault q k res
prodDDownState :: (p :< c, q :< c)
=> DDownState f c p -> DDownState f c q -> DDownState f c (p,q)
prodDDownState sp sq t = prodMap above above (sp t) (sq t)
(>*<) :: (p :< c, q :< c, Functor f)
=> DDownState f c p -> DDownState f c q -> DDownState f c (p,q)
(>*<) = prodDDownState
runDState :: Traversable f => DUpState' f (u,d) u -> DDownState' f (u,d) d -> d -> Term f -> u
runDState up down d (Term t) = u where
t' = fmap bel $ number t
bel (Numbered (i,s)) =
let d' = Map.findWithDefault d (Numbered (i,undefined)) m
in Numbered (i, (runDState up down d' s, d'))
m = explicit down (u,d) unNumbered t'
u = explicit up (u,d) unNumbered t'
runQHom :: (Traversable f, Functor g) =>
DUpState' f (u,d) u -> DDownState' f (u,d) d ->
QHom f (u,d) g ->
d -> Term f -> (u, Term g)
runQHom up down trans d (Term t) = (u,t'') where
t' = fmap bel $ number t
bel (Numbered (i,s)) =
let d' = Map.findWithDefault d (Numbered (i,undefined)) m
(u', s') = runQHom up down trans 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'