diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2014 Patrick Bahr + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + +1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + +2. Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + +3. Neither the name of the author nor the names of his contributors + may be used to endorse or promote products derived from this software + without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR +IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED +WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR +ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS +OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) +HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, +STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN +ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE +POSSIBILITY OF SUCH DAMAGE. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/benchmark/Benchmark.hs b/benchmark/Benchmark.hs new file mode 100644 --- /dev/null +++ b/benchmark/Benchmark.hs @@ -0,0 +1,59 @@ +{-# LANGUAGE TypeOperators, DeriveFunctor, DeriveTraversable, DeriveFoldable, TemplateHaskell, GADTs #-} + +module Main where + +import Criterion.Main +import Data.Comp.Derive +import Data.Comp.DeepSeq () +import Data.Comp.Arbitrary () +import Data.Comp.Show () +import Data.Comp + +import qualified Functions.Mono as M +import qualified DataTypes.Mono as M + + + +benchmarks :: String -> Term M.ArithLet -> String -> Term M.ArithExc -> Benchmark +benchmarks n t n' t' = rnf t `seq` rnf t' `seq` getBench + where getBench = bgroup "" [letBench, excBench] + letBench = bgroup n + [ inlineAnnBench + , annInlineBench + ] + excBench = bgroup n' + [ compAnnBench + , annCompBench] + inlineAnnBench = bgroup "inlineAnn" + [ bench "fused" (nf M.inlineAnnFuse t) + , bench "seq" (nf M.inlineAnnSeq t) + , bench "implicit, fused" (nf M.inlineAnnImpFuse t) + , bench "implicit, seq" (nf M.inlineAnnImpSeq t) ] + annInlineBench = bgroup "annInline" + [ bench "fused" (nf M.annInlineFuse t) + , bench "seq" (nf M.annInlineSeq t) + , bench "implicit, fused)" (nf M.annInlineImpFuse t) + , bench "implicit, seq" (nf M.annInlineImpSeq t) ] + compAnnBench = bgroup "compAnn" + [ bench "fused" (nf M.compAnnFuse t') + , bench "seq" (nf M.compAnnSeq t')] + annCompBench = bgroup "annComp" + [ bench "fused" (nf M.annCompFuse t') + , bench "seq" (nf M.annCompSeq t')] + +genExpr :: Int -> IO Benchmark +genExpr s = do + let t = M.exprAL s + let t' = M.exprAE s + putStr "size of the term: " + let termsize = size t + let termsize' = size t' + print termsize + putStr "size of the other term: " + print termsize' + return $ benchmarks ("term size="++ show termsize) t ("term size="++ show termsize') t' + +main = do b0 <- genExpr 11 + b1 <- genExpr 8 + b2 <- genExpr 4 + defaultMain [b0, b1,b2] diff --git a/benchmark/DataTypes/Comp.hs b/benchmark/DataTypes/Comp.hs new file mode 100644 --- /dev/null +++ b/benchmark/DataTypes/Comp.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE DeriveFunctor, DeriveTraversable, DeriveFoldable, TemplateHaskell, FlexibleContexts #-} + +module DataTypes.Comp where + +import Data.Comp.Derive + +type Var = String + +data Arith a = Add a a | Val Int + deriving (Show, Functor, Foldable, Traversable) + +data Let a = Let Var a a | Var Var + deriving (Show, Functor, Foldable, Traversable) +data Exc a = Throw | Catch a a + deriving (Show, Functor, Foldable, Traversable) + +data Code a = PUSH Int a + | ADD a + | THROW + | MARK a a + | UNMARK a + | NIL + + + +$(derive + [makeEqF, makeNFDataF, makeArbitraryF, smartConstructors] + [''Arith, ''Let, ''Exc]) diff --git a/benchmark/DataTypes/Mono.hs b/benchmark/DataTypes/Mono.hs new file mode 100644 --- /dev/null +++ b/benchmark/DataTypes/Mono.hs @@ -0,0 +1,43 @@ +{-# LANGUAGE DeriveFunctor, DeriveTraversable, DeriveFoldable, TemplateHaskell, + FlexibleContexts, ConstraintKinds #-} + +module DataTypes.Mono where + +import Data.Comp.Derive +import Data.Comp + +type Var = String + +data ArithLet a = Add a a | Mult a a | Sub a a | Val Int | Let Var a a | Var Var + deriving (Show, Functor, Foldable, Traversable) + +data ArithExc a = Add' a a | Val' Int | Throw | Catch a a + deriving (Show, Functor, Foldable, Traversable) + +data Code a = PUSH Int a + | ADD a + | THROW + | MARK a a + | UNMARK a + | NIL + deriving (Show, Functor, Foldable, Traversable) + + +$(derive + [makeShowF, makeEqF, makeNFDataF, makeArbitraryF, smartConstructors] + [''ArithLet, ''ArithExc, ''Code]) + + +exprAL :: Int -> Term ArithLet +exprAL 0 = iVal 4 +exprAL n = iLet "x" e1 e2 + where e1 = (iVal 1 `iSub` iVal 2) `iAdd` iLet "y" e3 e4 + e2 = iVar "x" `iMult` iVal 4 `iAdd` iLet "z" e5 e6 `iSub` exprAL (n-1) + e3 = iVal 2 `iAdd` iVal 3 + e4 = iVar "y" `iAdd` iVar "y" + e5 = iVar "x" `iMult` iVar "x" + e6 = (iVar "x" `iSub` iVar "z") `iAdd` exprAL (n-1) + +exprAE :: Int -> Term ArithExc +exprAE 0 = iVal' 3 +exprAE n = iVal' 1 `iAdd'` iCatch (exprAE (n-1) `iAdd'` iThrow) (iVal' 2 `iAdd'` exprAE (n-1)) diff --git a/benchmark/Functions/Comp.hs b/benchmark/Functions/Comp.hs new file mode 100644 --- /dev/null +++ b/benchmark/Functions/Comp.hs @@ -0,0 +1,17 @@ +module Functions.Comp where + +import DataTypes.Comp + +import Data.Comp +import Data.Comp.MacroAutomata + +import Data.Map (Map) +import qualified Data.Map as Map + + +inlineTrans :: MacroTrans' Arith (Map Var) Arith +inlineTrans m (Var v) = case Map.lookup v m of + Nothing -> iVar v + Just e -> e +inlineTrans m (Let v x y) = y (Map.insert v (x m) m) +inlineTrans m f = Term $ fmap ($ m) f diff --git a/benchmark/Functions/Mono.hs b/benchmark/Functions/Mono.hs new file mode 100644 --- /dev/null +++ b/benchmark/Functions/Mono.hs @@ -0,0 +1,98 @@ +{-# LANGUAGE TypeOperators #-} + +module Functions.Mono where + +import DataTypes.Mono + +import Data.Comp +import Data.Comp.MacroAutomata +import Data.Comp.Automata +import Data.Comp.Mapping + +import Data.Map (Map) +import qualified Data.Map as Map + +pathAnnTrans :: (Functor g, Traversable g) => DownTrans g [Int] (g :&: [Int]) +pathAnnTrans q t = simpCxt (fmap (\ (Numbered n s) -> s (n:q)) (number t) :&: q) + + +-- Inlining + + +inlineTrans :: MacroTrans' ArithLet (Map Var) ArithLet +inlineTrans m (Var v) = case Map.lookup v m of + Nothing -> iVar v + Just e -> e +inlineTrans m (Let v x y) = y (Map.insert v (x m) m) +inlineTrans m f = Term $ fmap ($ m) f + + +inlineTransExplicit :: MacroTrans ArithLet (Map Var) ArithLet +inlineTransExplicit m (Var v) = case Map.lookup v m of + Nothing -> iVar v + Just e -> Hole e +inlineTransExplicit m (Let v x y) = Hole $ y (Map.insert v (Hole $ x m') m') + where m' = fmap Hole m +inlineTransExplicit m (Add x y) = iAdd (Hole $ x m') (Hole $ y m') + where m' = fmap Hole m +inlineTransExplicit m (Mult x y) = iMult (Hole $ x m') (Hole $ y m') + where m' = fmap Hole m +inlineTransExplicit m (Sub x y) = iSub (Hole $ x m') (Hole $ y m') + where m' = fmap Hole m +inlineTransExplicit _ (Val n) = iVal n + + +inlineAnnFuse :: Term ArithLet -> Term (ArithLet :&: [Int]) +inlineAnnFuse t = runMacroTrans (compMacroDown (propAnnMacro inlineTransExplicit) pathAnnTrans) + (Map.empty :&: []) t + +inlineAnnImpFuse :: Term ArithLet -> Term (ArithLet :&: [Int]) +inlineAnnImpFuse t = runMacroTrans (compMacroDown (propAnnMacro $ mkMacroTrans inlineTrans) + pathAnnTrans) (Map.empty :&: []) t + +inlineAnnSeq :: Term ArithLet -> Term (ArithLet :&: [Int]) +inlineAnnSeq t = runMacroTrans (propAnnMacro inlineTransExplicit) Map.empty + (runDownTrans pathAnnTrans [] t) + +inlineAnnImpSeq :: Term ArithLet -> Term (ArithLet :&: [Int]) +inlineAnnImpSeq t = runMacroTrans (propAnnMacro $ mkMacroTrans inlineTrans) Map.empty + (runDownTrans pathAnnTrans [] t) + +annInlineFuse :: Term ArithLet -> Term (ArithLet :&: [Int]) +annInlineFuse t = runMacroTrans (compDownMacro pathAnnTrans inlineTransExplicit) + (Map.empty :^: []) t + +annInlineImpFuse :: Term ArithLet -> Term (ArithLet :&: [Int]) +annInlineImpFuse t = runMacroTrans (compDownMacro pathAnnTrans (mkMacroTrans inlineTrans)) + (Map.empty :^: []) t + +annInlineSeq :: Term ArithLet -> Term (ArithLet :&: [Int]) +annInlineSeq t = runDownTrans pathAnnTrans [] (runMacroTrans inlineTransExplicit Map.empty t) + +annInlineImpSeq :: Term ArithLet -> Term (ArithLet :&: [Int]) +annInlineImpSeq t = runDownTrans pathAnnTrans [] (runMacroTrans (mkMacroTrans inlineTrans) Map.empty t) + + +-- Code generator + +compTrans :: MacroTransId' ArithExc Code +compTrans q (Val' n) = iPUSH n q +compTrans q (Add' x y) = x $ y $ iADD q +compTrans _ Throw = iTHROW +compTrans q (Catch x h) = iMARK (h q) (x $ iUNMARK q) + + +compAnnFuse :: Term ArithExc -> Term (Code :&: [Int]) +compAnnFuse t = runMacroTrans (compMacroDown (propAnnMacro $ fromMacroTransId' compTrans) pathAnnTrans ) (I (ann [] iNIL) :&: []) t + +compAnnSeq :: Term ArithExc -> Term (Code :&: [Int]) +compAnnSeq t = runMacroTrans (propAnnMacro $ fromMacroTransId' compTrans) (I (ann [] iNIL)) + (runDownTrans pathAnnTrans [] t) + +annCompFuse :: Term ArithExc -> Term (Code :&: [Int]) +annCompFuse t = runMacroTrans (compDownMacro pathAnnTrans (fromMacroTransId' compTrans)) + (I (`ann` iNIL) :^: []) t + +annCompSeq :: Term ArithExc -> Term (Code :&: [Int]) +annCompSeq t = runDownTrans pathAnnTrans [] (runMacroTrans (fromMacroTransId' compTrans) + (I iNIL) t) diff --git a/compdata-automata.cabal b/compdata-automata.cabal new file mode 100644 --- /dev/null +++ b/compdata-automata.cabal @@ -0,0 +1,52 @@ +Name: compdata-automata +Version: 0.9 +Synopsis: Tree automata on Compositional Data Types +Description: + This library extends the @compdata@ package with advanced recursion + schemes derived from tree automata. These recursion schemes allow + for a higher degree of modularity and make it possible to apply + fusion. See /Modular Tree Automata/ (Mathematics of Program + Construction, 263-299, 2012, + ) and /Programming + Macro Tree Transducers/ (Workshop on Generic Programming, 61-72, + 2013, ). + + +Category: Generics +License: BSD3 +License-file: LICENSE +Author: Patrick Bahr +Maintainer: paba@di.ku.dk +Build-Type: Simple +Cabal-Version: >=1.9.2 +bug-reports: https://github.com/pa-ba/compdata-automata/issues + +extra-source-files: + -- benchmark files + benchmark/*.hs + benchmark/DataTypes/*.hs + benchmark/Functions/*.hs + -- example files + examples/Examples/Automata/*.hs + +library + Exposed-Modules: Data.Comp.Automata + Data.Comp.MacroAutomata + Build-Depends: base >= 4.7, base < 5, containers, compdata == 0.9.*, projection + hs-source-dirs: src + ghc-options: -W + + +Benchmark macro + Type: exitcode-stdio-1.0 + Main-is: Benchmark.hs + hs-source-dirs: src benchmark + ghc-options: -W -O2 + -- Disable short-cut fusion rules in order to compare optimised and unoptimised code. + cpp-options: -DNO_RULES + Build-Depends: base >= 4.7, base < 5, containers, compdata == 0.9.*, projection, criterion + +source-repository head + type: git + location: https://github.com/pa-ba/compdata-automata + diff --git a/examples/Examples/Automata/Compiler.hs b/examples/Examples/Automata/Compiler.hs new file mode 100644 --- /dev/null +++ b/examples/Examples/Automata/Compiler.hs @@ -0,0 +1,192 @@ +{-# LANGUAGE TemplateHaskell, FlexibleContexts, MultiParamTypeClasses, +TypeOperators, FlexibleInstances, UndecidableInstances, +ScopedTypeVariables, TypeSynonymInstances, GeneralizedNewtypeDeriving, +OverlappingInstances, ConstraintKinds #-} + +module Examples.Automata.Compiler where + +import Data.Comp.Automata +import Data.Comp.Derive +import Data.Comp.Ops +import Data.Comp hiding (height) +import Data.Foldable +import Prelude hiding (foldl) + +import Data.Set (Set, union, singleton, delete, member) +import qualified Data.Set as Set + +import Data.Map (Map) +import qualified Data.Map as Map + +type Var = String + +data Val a = Const Int +data Op a = Plus a a + | Times a a +type Core = Op :+: Val +data Let a = Let Var a a + | Var Var + +type CoreLet = Let :+: Core + +data Sugar a = Neg a + | Minus a a + +$(derive [makeFunctor, makeFoldable, makeTraversable, smartConstructors, makeShowF] + [''Val, ''Op, ''Let, ''Sugar]) + + +class Eval f where + evalSt :: UpState f Int + +$(derive [liftSum] [''Eval]) + +instance Eval Val where + evalSt (Const i) = i + +instance Eval Op where + evalSt (Plus x y) = x + y + evalSt (Times x y) = x * y + +type Addr = Int + +data Instr = Acc Int + | Load Addr + | Store Addr + | Add Int + | Sub Int + | Mul Int + deriving (Show) + +type Code = [Instr] + +data MState = MState { + mRam :: Map Addr Int, + mAcc :: Int } + +runCode :: Code -> MState -> MState +runCode [] = id +runCode (ins:c) = runCode c . step ins + where step (Acc i) s = s{mAcc = i} + step (Load a) s = case Map.lookup a (mRam s) of + Nothing -> error $ "memory cell " ++ show a ++ " is not set" + Just n -> s {mAcc = n} + step (Store a) s = s {mRam = Map.insert a (mAcc s) (mRam s)} + step (Add a) s = exec (+) a s + step (Sub a) s = exec (-) a s + step (Mul a) s = exec (*) a s + exec op a s = case Map.lookup a (mRam s) of + Nothing -> error $ "memory cell " ++ show a ++ " is not set" + Just n -> s {mAcc = mAcc s `op` n} + + +runCode' :: Code -> Int +runCode' c = mAcc $ runCode c MState{mRam = Map.empty, mAcc = error "accumulator is not set"} + + +-- | Defines the height of an expression. +heightSt :: Foldable f => UpState f Int +heightSt t = foldl max 0 t + 1 + +tmpAddrSt :: Foldable f => UpState f Int +tmpAddrSt = (+1) . heightSt + + +newtype VarAddr = VarAddr {varAddr :: Int} deriving (Eq, Show, Num) + +class VarAddrSt f where + varAddrSt :: DownState f VarAddr + +instance (VarAddrSt f, VarAddrSt g) => VarAddrSt (f :+: g) where + varAddrSt (q,Inl x) = varAddrSt (q, x) + varAddrSt (q,Inr x) = varAddrSt (q, x) + +instance VarAddrSt Let where + varAddrSt (d, Let _ _ x) = x `Map.singleton` (d + 2) + varAddrSt _ = Map.empty + +instance VarAddrSt f where + varAddrSt _ = Map.empty + + +type Bind = Map Var Int + +bindSt :: (Let :<: f,VarAddr :< q) => DDownState f q Bind +bindSt t = case proj t of + Just (Let v _ e) -> Map.singleton e q' + where q' = Map.insert v (varAddr above) above + _ -> Map.empty + +-- | Defines the code that an expression is compiled to. It depends on +-- an integer state that denotes the height of the current node. +class CodeSt f q where + codeSt :: DUpState f q Code + +instance (CodeSt f q, CodeSt g q) => CodeSt (f :+: g) q where + codeSt (Inl x) = codeSt x + codeSt (Inr x) = codeSt x + + +instance CodeSt Val q where + codeSt (Const i) = [Acc i] + +instance (Int :< q) => CodeSt Op q where + codeSt (Plus x y) = below x ++ [Store i] ++ below y ++ [Add i] + where i = below y + codeSt (Times x y) = below x ++ [Store i] ++ below y ++ [Mul i] + where i = below y + +instance (VarAddr :< q, Bind :< q) => CodeSt Let q where + codeSt (Let _ b e) = below b ++ [Store i] ++ below e + where i = varAddr above + codeSt (Var v) = case Map.lookup v above of + Nothing -> error $ "unbound variable " ++ v + Just i -> [Load i] + +compile' :: (CodeSt f (Code,Int), Foldable f, Functor f) => Term f -> Code +compile' = fst . runDUpState (codeSt `prodDUpState` dUpState tmpAddrSt) + + +exComp' = compile' (iConst 2 `iPlus` iConst 3 :: Term Core) + + + +compile :: (CodeSt f ((Code,Int),(Bind,VarAddr)), Traversable f, Functor f, Let :<: f, VarAddrSt f) + => Term f -> Code +compile = fst . runDState + (codeSt `prodDUpState` dUpState tmpAddrSt) + (bindSt `prodDDownState` dDownState varAddrSt) + (Map.empty, VarAddr 1) + + +exComp = compile (iLet "x" (iLet "x" (iConst 5) (iConst 10 `iPlus` iVar "x")) (iConst 2 `iPlus` iVar "x") :: Term CoreLet) + +-- | Defines the set of free variables +class VarsSt f where + varsSt :: UpState f (Set Var) + +$(derive [liftSum] [''VarsSt]) + +instance VarsSt Val where + varsSt _ = Set.empty + +instance VarsSt Op where + varsSt (Plus x y) = x `union` y + varsSt (Times x y) = x `union` y + +instance VarsSt Let where + varsSt (Var v) = singleton v + varsSt (Let v x y) = (if v `member` y then x else Set.empty) `union` delete v y + +-- | Stateful homomorphism that removes unnecessary let bindings. +remLetHom :: (Set Var :< q, Let :<: f, Functor f) => QHom f q f +remLetHom t = case proj t of + Just (Let v _ y) + | not (v `member` below y) -> Hole y + _ -> simpCxt t + +-- | Removes unnecessary let bindings. +remLet :: (Let :<: f, Functor f, VarsSt f) => Term f -> Term f +remLet = runUpHom varsSt remLetHom + +exLet = remLet (iLet "x" (iConst 3) (iConst 2 `iPlus` iVar "y") :: Term CoreLet) diff --git a/src/Data/Comp/Automata.hs b/src/Data/Comp/Automata.hs new file mode 100644 --- /dev/null +++ b/src/Data/Comp/Automata.hs @@ -0,0 +1,524 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ScopedTypeVariables #-} + +-------------------------------------------------------------------------------- +-- | +-- Module : Data.Comp.Automata +-- Copyright : (c) 2010-2012 Patrick Bahr +-- License : BSD3 +-- Maintainer : Patrick Bahr +-- Stability : experimental +-- Portability : non-portable (GHC Extensions) +-- +-- This module defines stateful term homomorphisms. This (slightly +-- oxymoronic) notion extends per se stateless term homomorphisms with +-- a state that is maintained separately by a bottom-up or top-down +-- state transformation. Additionally, this module also provides +-- combinators to run state transformations themselves. +-- +-- Like regular term homomorphisms also stateful homomorphisms (as +-- well as transducers) can be lifted to annotated signatures +-- (cf. "Data.Comp.Annotation"). +-- +-- The recursion schemes provided in this module are derived from tree +-- automata. They allow for a higher degree of modularity and make it +-- possible to apply fusion. The implementation is based on the paper +-- /Modular Tree Automata/ (Mathematics of Program Construction, +-- 263-299, 2012, ). +-- +-------------------------------------------------------------------------------- + +module Data.Comp.Automata + ( + -- * Stateful Term Homomorphisms + QHom + , below + , above + , pureHom + -- ** Bottom-Up State Propagation + , upTrans + , runUpHom + , runUpHomSt + -- ** Top-Down State Propagation + , downTrans + , runDownHom + -- ** Bidirectional State Propagation + , runQHom + -- * Deterministic Bottom-Up Tree Transducers + , UpTrans + , UpTrans' + , mkUpTrans + , runUpTrans + , compUpTrans + , compUpTransHom + , compHomUpTrans + , compUpTransSig + , compSigUpTrans + , compAlgUpTrans + -- * Deterministic Bottom-Up Tree State Transformations + -- ** Monolithic State + , UpState + , tagUpState + , runUpState + , prodUpState + -- ** Modular State + , DUpState + , dUpState + , upState + , runDUpState + , prodDUpState + , (|*|) + -- * Deterministic Top-Down Tree Transducers + , DownTrans + , DownTrans' + , mkDownTrans + , runDownTrans + , compDownTrans + , compDownTransSig + , compSigDownTrans + , compDownTransHom + , compHomDownTrans + -- * Deterministic Top-Down Tree State Transformations + -- ** Monolithic State + , DownState + , tagDownState + , prodDownState + -- ** Modular State + , DDownState + , dDownState + , downState + , prodDDownState + , (>*<) + -- * Bidirectional Tree State Transformations + , runDState + -- * Operators for Finite Mappings + , (&) + , (|->) + , empty + -- * Product State Spaces + , module Data.Projection + -- * Annotations + , propAnnQ + , propAnnUp + , propAnnDown + , pathAnn + ) where + +import Data.Comp.Algebra +import Data.Comp.Annotation +import Data.Projection +import Data.Comp.Mapping +import Data.Comp.Term + + + + + + +-- | This function provides access to components of the states from +-- "below". + +below :: (?below :: a -> q, p :< q) => a -> p +below = pr . ?below + +-- | This function provides access to components of the state from +-- "above" + +above :: (?above :: q, p :< q) => p +above = pr ?above + +-- | Turns the explicit parameters @?above@ and @?below@ into explicit +-- ones. + +explicit :: ((?above :: q, ?below :: a -> q) => b) -> q -> (a -> q) -> b +explicit x ab be = x where ?above = ab; ?below = be + + +-- | This type represents stateful term homomorphisms. Stateful term +-- homomorphisms have access to a state that is provided (separately) +-- by a bottom-up or top-down state transformation function (or both). + +type QHom f q g = forall a . (?below :: a -> q, ?above :: q) => f a -> Context g a + + +-- | This function turns a stateful homomorphism with a fully +-- polymorphic state type into a (stateless) homomorphism. +pureHom :: (forall q . QHom f q g) -> Hom f g +pureHom phom t = let ?above = undefined + ?below = const undefined + in phom t + +-- | This type represents transition functions of total, deterministic +-- bottom-up tree transducers (UTTs). + +type UpTrans f q g = forall a. f (q,a) -> (q, Context g a) + + +-- | This is a variant of the 'UpTrans' type that makes it easier to +-- define UTTs as it avoids the explicit use of 'Hole' to inject +-- placeholders into the result. + +type UpTrans' f q g = forall a. f (q,Context g a) -> (q, Context g a) + +-- | This function turns a UTT defined using the type 'UpTrans'' in +-- to the canonical form of type 'UpTrans'. + +mkUpTrans :: Functor f => UpTrans' f q g -> UpTrans f q g +mkUpTrans tr t = tr $ fmap (\(q,a) -> (q, Hole a)) t + +-- | This function transforms a UTT transition function into an +-- algebra. + +upAlg :: (Functor g) => UpTrans f q g -> Alg f (q, Term g) +upAlg trans = fmap appCxt . trans + +-- | This function runs the given UTT on the given term. + +runUpTrans :: (Functor f, Functor g) => UpTrans f q g -> Term f -> Term g +runUpTrans trans = snd . runUpTransSt trans + +-- | This function is a variant of 'runUpTrans' that additionally +-- returns the final state of the run. + +runUpTransSt :: (Functor f, Functor g) => UpTrans f q g -> Term f -> (q, Term g) +runUpTransSt = cata . upAlg + +-- | This function generalises 'runUpTrans' to contexts. Therefore, +-- additionally, a transition function for the holes is needed. + +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 + +-- | This function composes two UTTs. (see TATA, Theorem 6.4.5) + +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 + + +-- | This function composes a UTT with an algebra. + +compAlgUpTrans :: (Functor g) + => Alg g a -> UpTrans f q g -> Alg f (q,a) +compAlgUpTrans alg trans = fmap (cata' alg) . trans + + +-- | This combinator composes a UTT followed by a signature function. + +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 + +-- | This combinator composes a signature function followed by a UTT. + +compUpTransSig :: UpTrans g q h -> SigFun f g -> UpTrans f q h +compUpTransSig trans sig = trans . sig + +-- | This combinator composes a UTT followed by a homomorphism. + +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 + +-- | This combinator composes a homomorphism followed by a UTT. + +compUpTransHom :: (Functor g, Functor h) => UpTrans g q h -> Hom f g -> UpTrans f q h +compUpTransHom trans hom x = runUpTrans' trans . hom $ x + +-- | This type represents transition functions of total, deterministic +-- bottom-up tree acceptors (UTAs). + +type UpState f q = Alg f q + +-- | Changes the state space of the UTA using the given isomorphism. + +tagUpState :: (Functor f) => (q -> p) -> (p -> q) -> UpState f q -> UpState f p +tagUpState i o s = i . s . fmap o + +-- | This combinator runs the given UTA on a term returning the final +-- state of the run. + +runUpState :: (Functor f) => UpState f q -> Term f -> q +runUpState = cata + +-- | This function combines the product UTA of the two given UTAs. + +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 + + +-- | This function constructs a UTT from a given stateful term +-- homomorphism with the state propagated by the given UTA. + +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 + +-- | This function applies a given stateful term homomorphism with +-- a state space propagated by the given UTA to a term. + +runUpHom :: (Functor f, Functor g) => UpState f q -> QHom f q g -> Term f -> Term g +runUpHom st hom = snd . runUpHomSt st hom + +-- | This is a variant of 'runUpHom' that also returns the final state +-- of the run. + +runUpHomSt :: (Functor f, Functor g) => UpState f q -> QHom f q g -> Term f -> (q,Term g) +runUpHomSt alg h = runUpTransSt (upTrans alg h) + + +-- | This type represents transition functions of generalised +-- deterministic bottom-up tree acceptors (GUTAs) which have access +-- to an extended state space. + +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 + +-- | This combinator turns an arbitrary UTA into a GUTA. + +dUpState :: Functor f => UpState f q -> DUpState f p q +dUpState f = f . fmap below + +-- | This combinator turns a GUTA with the smallest possible state +-- space into a UTA. + +upState :: DUpState f q q -> UpState f q +upState f s = res where res = explicit f res id s + +-- | This combinator runs a GUTA on a term. + +runDUpState :: Functor f => DUpState f q q -> Term f -> q +runDUpState = runUpState . upState + +-- | This combinator constructs the product of two GUTA. + +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 + + + +-- | This type represents transition functions of total deterministic +-- top-down tree transducers (DTTs). + +type DownTrans f q g = forall a. q -> f (q -> a) -> Context g a + + +-- | This is a variant of the 'DownTrans' type that makes it easier to +-- define DTTs as it avoids the explicit use of 'Hole' to inject +-- placeholders into the result. + +type DownTrans' f q g = forall a. q -> f (q -> Context g a) -> Context g a + +-- | This function turns a DTT defined using the type 'DownTrans'' in +-- to the canonical form of type 'DownTrans'. +mkDownTrans :: Functor f => DownTrans' f q g -> DownTrans f q g +mkDownTrans tr q t = tr q (fmap (Hole .) t) + +-- | Thsis function runs the given DTT on the given tree. + +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 + +-- | This function runs the given DTT on the given tree. + +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) + +-- | This function composes two DTTs. (see W.C. Rounds /Mappings and +-- grammars on trees/, Theorem 2.) + +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) + + + +-- | This function composes a signature function after a DTT. + +compSigDownTrans :: (Functor g) => SigFun g h -> DownTrans f q g -> DownTrans f q h +compSigDownTrans sig trans q = appSigFun sig . trans q + +-- | This function composes a DTT after a function. + +compDownTransSig :: DownTrans g q h -> SigFun f g -> DownTrans f q h +compDownTransSig trans hom q t = trans q (hom t) + + +-- | This function composes a homomorphism after a DTT. + +compHomDownTrans :: (Functor g, Functor h) + => Hom g h -> DownTrans f q g -> DownTrans f q h +compHomDownTrans hom trans q = appHom hom . trans q + +-- | This function composes a DTT after a homomorphism. + +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) + + +-- | This type represents transition functions of total, deterministic +-- top-down tree acceptors (DTAs). + +type DownState f q = forall m a. Mapping m a => (q, f a) -> m q + + +-- | Changes the state space of the DTA using the given isomorphism. + +tagDownState :: (q -> p) -> (p -> q) -> DownState f q -> DownState f p +tagDownState i o t (q,s) = fmap i $ t (o q,s) + +-- | This function constructs the product DTA of the given two DTAs. + +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)) + + +-- | Apply the given state mapping to the given functorial value by +-- adding the state to the corresponding index if it is in the map and +-- otherwise adding the provided default state. + +appMap :: Traversable f => (forall m i . Mapping m i => f i -> m q) + -> q -> f (q -> b) -> f (q,b) +appMap qmap q s = fmap qfun s' + where s' = number s + qfun (Numbered i a) = let q' = lookupNumMap q i (qmap s') + in (q', a q') + +-- | This function constructs a DTT from a given stateful term-- +-- homomorphism with the state propagated by the given DTA. + +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) + + +-- | This function applies a given stateful term homomorphism with a +-- state space propagated by the given DTA to a term. + +runDownHom :: (Traversable f, Functor g) + => DownState f q -> QHom f q g -> q -> Term f -> Term g +runDownHom st h = runDownTrans (downTrans st h) + +-- | This type represents transition functions of generalised +-- deterministic top-down tree acceptors (GDTAs) which have access + +-- to an extended state space. +type DDownState f p q = (q :< p) => DDownState' f p q + +type DDownState' f p q = forall m i . (Mapping m i, ?below :: i -> p, ?above :: p) + => f i -> m q + +-- | This combinator turns an arbitrary DTA into a GDTA. + +dDownState :: DownState f q -> DDownState f p q +dDownState f t = f (above,t) + +-- | This combinator turns a GDTA with the smallest possible state +-- space into a DTA. + +downState :: DDownState f q q -> DownState f q +downState f (q,s) = res + where res = explicit f q bel s + bel k = findWithDefault q k res + + +-- | This combinator constructs the product of two dependant top-down +-- state transformations. + +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) + +-- | This is a synonym for 'prodDDownState'. + +(>*<) :: (p :< c, q :< c, Functor f) + => DDownState f c p -> DDownState f c q -> DDownState f c (p,q) +(>*<) = prodDDownState + + +-- | This combinator combines a bottom-up and a top-down state +-- transformations. Both state transformations can depend mutually +-- recursive on each other. + +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' = lookupNumMap d i m + in Numbered i (runDState up down d' s, d') + m = explicit down (u,d) unNumbered t' + u = explicit up (u,d) unNumbered t' + +-- | This combinator runs a stateful term homomorphisms with a state +-- space produced both on a bottom-up and a top-down state +-- transformation. + +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' = lookupNumMap d i 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' + + +-- | Lift a stateful term homomorphism over signatures @f@ and @g@ to +-- a stateful term homomorphism over the same signatures, but extended with +-- annotations. +propAnnQ :: (DistAnn f p f', DistAnn g p g', Functor g) + => QHom f q g -> QHom f' q g' +propAnnQ hom f' = ann p (hom f) + where (f,p) = projectA f' + +-- | Lift a bottom-up tree transducer over signatures @f@ and @g@ to a +-- bottom-up tree transducer over the same signatures, but extended +-- with annotations. +propAnnUp :: (DistAnn f p f', DistAnn g p g', Functor g) + => UpTrans f q g -> UpTrans f' q g' +propAnnUp trans f' = (q, ann p t) + where (f,p) = projectA f' + (q,t) = trans f + +-- | Lift a top-down tree transducer over signatures @f@ and @g@ to a +-- top-down tree transducer over the same signatures, but extended +-- with annotations. +propAnnDown :: (DistAnn f p f', DistAnn g p g', Functor g) + => DownTrans f q g -> DownTrans f' q g' +propAnnDown trans q f' = ann p (trans q f) + where (f,p) = projectA f' + + +-- | This function adds unique annotations to a term/context. Each +-- node in the term/context is annotated with its path from the root, +-- which is represented as an integer list. It is implemented as a +-- DTT. +pathAnn :: forall g. (Traversable g) => CxtFun g (g :&: [Int]) +pathAnn = runDownTrans trans [] where + trans :: DownTrans g [Int] (g :&: [Int]) + trans q t = simpCxt (fmap (\ (Numbered n s) -> s (n:q)) (number t) :&: q) diff --git a/src/Data/Comp/MacroAutomata.hs b/src/Data/Comp/MacroAutomata.hs new file mode 100644 --- /dev/null +++ b/src/Data/Comp/MacroAutomata.hs @@ -0,0 +1,221 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} +-------------------------------------------------------------------------------- +-- | +-- Module : Data.Comp.MacroAutomata +-- Copyright : (c) 2013 Patrick Bahr +-- License : BSD3 +-- Maintainer : Patrick Bahr +-- Stability : experimental +-- Portability : non-portable (GHC Extensions) +-- +-- This module defines macro tree transducers (MTTs). It provides +-- functions to run MTTs and to compose them with top down tree +-- transducers. It also defines MTTs with regular look-ahead which +-- combines MTTs with bottom-up tree acceptors. +-- +-------------------------------------------------------------------------------- + +module Data.Comp.MacroAutomata + ( + -- * Macro Tree Transducers + MacroTrans + , MacroTrans' + , mkMacroTrans + , runMacroTrans + , compMacroDown + , compDownMacro + -- * Macro Tree Transducers with Singleton State Space + , MacroTransId + , MacroTransId' + , fromMacroTransId + , fromMacroTransId' + -- * Macro Tree Transducers with Regular Look-Ahead + , MacroTransLA + , MacroTransLA' + , mkMacroTransLA + , runMacroTransLA + , compDownMacroLA + -- * Macro Tree Transducers with Regular Look-Ahead + , (:^:) (..) + , I (..) + -- * Annotations + , propAnnMacro + , propAnnMacroLA + ) + where + +import Data.Comp.Algebra +import Data.Comp.Annotation +import Data.Comp.Automata +import Data.Comp.Multi.HFunctor (I (..)) +import Data.Comp.Term + +-- | This type represents total deterministic macro tree transducers +-- (MTTs). + +type MacroTrans f q g = forall a. q a -> f (q (Context g a) -> a) -> Context g a + +-- | This is a variant of the type 'MacroTrans' that makes it easier +-- to define MTTs as it avoids the explicit use of 'Hole' when using +-- placeholders in the result. + +type MacroTrans' f q g = forall a . q (Context g a) -> f (q (Context g a) -> Context g a) + -> Context g a + +-- | This function turns an MTT defined using the more convenient type +-- 'MacroTrans'' into its canonical form of type 'MacroTrans'. + +mkMacroTrans :: (Functor f, Functor q) => MacroTrans' f q g -> MacroTrans f q g +mkMacroTrans tr q t = tr (fmap Hole q) (fmap (Hole .) t) + +-- | This function defines the semantics of MTTs. It applies a given +-- MTT to an input with and an initial state. + +runMacroTrans :: (Functor g, Functor f, Functor q) => + MacroTrans f q g -> q (Cxt h g a) -> Cxt h f a -> Cxt h g a +runMacroTrans tr q t = run t q where + run (Term t) q = appCxt (tr q (fmap run' t)) + run (Hole a) _ = Hole a + run' t q = run t (fmap appCxt q) + + +-- This function is a variant of 'runMacroTrans' that is used to +-- define composition. Restricted to 'Term's, both functions coincide. + +runMacroTrans' :: forall g f q h a. + (Functor g, Functor f, Functor q) => MacroTrans f q g -> q (Cxt h g a) + -> Cxt h f (q (Cxt h g a) -> a) -> Cxt h g a +runMacroTrans' tr q t = run t q where + run :: Cxt h f (q (Cxt h g a) -> a) -> q (Cxt h g a) -> Cxt h g a + run (Term t) q = appCxt (tr q (fmap run' t)) + run (Hole a) q = Hole (a q) + + run' :: Cxt h f (q (Cxt h g a) -> a) -> q (Context g (Cxt h g a)) -> Cxt h g a + run' t q = run t (fmap appCxt q) + + +-- | This function composes a DTT followed by an MTT. The resulting +-- MTT's semantics is equivalent to the function composition of the +-- semantics of the original MTT and DTT. + +compMacroDown :: (Functor f, Functor g, Functor h, Functor p) + => MacroTrans g p h -> DownTrans f q g -> MacroTrans f (p :&: q) h +compMacroDown t2 t1 (p :&: q) t = runMacroTrans' t2 (fmap Hole p) (t1 q (fmap curryF t)) + where curryF :: ((p :&: q) a -> b) -> q -> p a -> b + curryF f q p = f (p :&: q) + +-- | This function is a variant of 'runDownTrans' that is used to +-- define composition, similarly to the function 'runMacroTrans''. + +runDownTrans' :: (Functor f, Functor g) => DownTrans f q g -> q -> Cxt h f (q -> a) -> Cxt h g a +runDownTrans' tr q (Term t) = appCxt $ tr q $ fmap (\s q -> runDownTrans' tr q s) t +runDownTrans' _ q (Hole a) = Hole (a q) + +-- | This type constructor is used to define the state space of an MTT +-- that is obtained by composing an MTT followed by a DTT. + +data (q :^: p) a = q (p -> a) :^: p + +instance Functor q => Functor (q :^: p) where + fmap f (q :^: p) = fmap (f .) q :^: p + +-- | This function composes an MTT followed by a DTT. The resulting +-- MTT's semantics is equivalent to first running the original MTT and +-- then the DTT. + +compDownMacro :: forall f g h q p . (Functor f, Functor g, Functor h, Functor q) + => DownTrans g p h -> MacroTrans f q g -> MacroTrans f (q :^: p) h +compDownMacro t2 t1 (q :^: p) t = runDownTrans' t2 p (t1 (fmap (\a p' -> a p') q) (fmap reshape t)) + where reshape :: ((q :^: p) (Context h a) -> a) -> (q (Context g (p -> a)) -> p -> a) + reshape f q' p' = f (fmap (\s p'' -> runDownTrans' t2 p'' s) q' :^: p') + + +-- | This type is an instantiation of the 'MacroTrans' type to a state +-- space with only a single state with a single accumulation parameter +-- (i.e. the state space is the identity functor). + +type MacroTransId f g = forall a. a -> f (Context g a -> a) -> Context g a + +-- | This type is a variant of the 'MacroTransId' which is more +-- convenient to work with as it avoids the explicit use of 'Hole' to +-- embed placeholders into the result. +type MacroTransId' f g = forall a. Context g a -> f (Context g a -> Context g a) -> Context g a + + +-- | This function transforms an MTT of type |MacroTransId| into the +-- canonical type such that it can be run. + +fromMacroTransId :: Functor f => MacroTransId f g -> MacroTrans f I g +fromMacroTransId tr (I a) t = tr a (fmap (. I) t) + + +-- | This function transforms an MTT of type |MacroTransId'| into the +-- canonical type such that it can be run. + +fromMacroTransId' :: Functor f => MacroTransId' f g -> MacroTrans f I g +fromMacroTransId' tr (I a) t = tr (Hole a) (fmap (\f -> Hole . f . I) t) + +-- | This type represents MTTs with regular look-ahead, i.e. MTTs that +-- have access to information that is generated by a separate UTA. + +type MacroTransLA f q p g = forall a. q a -> p -> f (q (Context g a) -> a, p) -> Context g a + +-- | This type is a more convenient variant of 'MacroTransLA' with +-- which one can avoid using 'Hole' explicitly when injecting +-- placeholders in the result. +type MacroTransLA' f q p g = forall a. q (Context g a) -> p -> + f (q (Context g a) -> Context g a, p) -> Context g a + + +-- | This function turns an MTT with regular look-ahead defined using +-- the more convenient type |MacroTransLA'| into its canonical form of +-- type |MacroTransLA|. +mkMacroTransLA :: (Functor q, Functor f) => MacroTransLA' f q p g -> MacroTransLA f q p g +mkMacroTransLA tr q p t = tr (fmap Hole q) p (fmap (\ (f, p) -> (Hole . f,p)) t) + + +-- | This function defines the semantics of MTTs with regular +-- look-ahead. It applies a given MTT with regular look-ahead +-- (including an accompanying bottom-up state transition function) to +-- an input with and an initial state. +runMacroTransLA :: forall g f q p. (Functor g, Functor f, Functor q) => + UpState f p -> MacroTransLA f q p g -> q (Term g) -> Term f -> Term g +runMacroTransLA st tr q t = fst (run t) q where + run :: Term f -> (q (Term g) -> Term g, p) + run (Term t) = let p = st $ fmap snd t' + t' = fmap run' t + in (\ q -> appCxt (tr q p t'), p) + run' :: Term f -> (q (Context g (Term g)) -> (Term g), p) + run' t = let (res, p) = run t + in (res . fmap appCxt, p) + +-- | This function composes an MTT with regular look-ahead followed by +-- a DTT. + +compDownMacroLA :: forall f g h q1 q2 p . (Functor f, Functor g, Functor h, Functor q1) => + DownTrans g q2 h -> MacroTransLA f q1 p g -> MacroTransLA f (q1 :^: q2) p h +compDownMacroLA t2 t1 (q1 :^: q2) p t = runDownTrans' t2 q2 (t1 (fmap (\a q2' -> a q2') q1) p (fmap reshape t)) + where reshape :: ((q1 :^: q2) (Context h a) -> a,p) -> (q1 (Context g (q2 -> a)) -> q2 -> a,p) + reshape (f,p) = (\q1' q2' -> f (fmap (\s q2'' -> runDownTrans' t2 q2'' s) q1' :^: q2'),p) + + +-- | Lift a macro tree transducer over signatures @f@ and @g@ to a +-- macro tree transducer over the same signatures, but extended +-- with annotations. +propAnnMacro :: (Functor f, Functor q, DistAnn f p f', DistAnn g p g', Functor g) + => MacroTrans f q g -> MacroTrans f' q g' +propAnnMacro trans q f' = ann p (trans q (fmap ann' f)) + where (f,p) = projectA f' + ann' s q' = s (fmap (ann p) q') + +-- | Lift a macro tree transducer with regular look-ahead over +-- signatures @f@ and @g@ to a macro tree transducer with regular +-- look-ahead over the same signatures, but extended with annotations. +propAnnMacroLA :: (Functor f, Functor q, DistAnn f p f', DistAnn g p g', Functor g) + => MacroTransLA f q p g -> MacroTransLA f' q p g' +propAnnMacroLA trans q p f' = ann an (trans q p (fmap ann' f)) + where (f,an) = projectA f' + ann' (s,p) = (s . fmap (ann an), p)