pointless-rewrite 0.0.2 → 0.0.3
raw patch · 36 files changed
+2083/−986 lines, 36 filesdep +containersdep −haskell98dep ~pointless-haskelldep ~pointless-lenses
Dependencies added: containers
Dependencies removed: haskell98
Dependency ranges changed: pointless-haskell, pointless-lenses
Files
- README +14/−2
- pointless-rewrite.cabal +9/−4
- src/Data/Default.hs +68/−0
- src/Data/Equal.hs +332/−51
- src/Data/Equal.hs-boot +11/−0
- src/Data/Eval.hs +148/−61
- src/Data/Lens.hs +102/−63
- src/Data/Pf.hs +252/−0
- src/Data/Pf.hs-boot +3/−0
- src/Data/Spine.hs +186/−146
- src/Data/Type.hs +119/−193
- src/Transform/Examples/Company.hs +1/−0
- src/Transform/Examples/Imdb.hs +2/−1
- src/Transform/Examples/Women.hs +1/−0
- src/Transform/Rewriting.hs +26/−13
- src/Transform/Rules/Lenses.hs +18/−38
- src/Transform/Rules/Lenses.hs-boot +2/−0
- src/Transform/Rules/Lenses/Combinators.hs +7/−29
- src/Transform/Rules/Lenses/Dists.hs +7/−1
- src/Transform/Rules/Lenses/Lists.hs +58/−53
- src/Transform/Rules/Lenses/Products.hs +8/−0
- src/Transform/Rules/Lenses/Rec.hs +123/−88
- src/Transform/Rules/Lenses/Sums.hs +8/−3
- src/Transform/Rules/PF.hs +16/−34
- src/Transform/Rules/PF.hs-boot +2/−1
- src/Transform/Rules/PF/Combinators.hs +56/−53
- src/Transform/Rules/PF/Dists.hs +11/−1
- src/Transform/Rules/PF/Lists.hs +148/−0
- src/Transform/Rules/PF/Monoids.hs +76/−0
- src/Transform/Rules/PF/Products.hs +19/−6
- src/Transform/Rules/PF/Rec.hs +108/−112
- src/Transform/Rules/PF/Sums.hs +18/−15
- src/Transform/Rules/SYB.hs +2/−10
- src/Transform/Rules/SYB/TP.hs +14/−4
- src/Transform/Rules/SYB/TU.hs +12/−4
- src/Transform/Rules/XPath.hs +96/−0
README view
@@ -2,10 +2,22 @@ This cabal package can be installed with: -$ cabal install pointless-lenses+$ cabal install pointless-rewrite For a manual install, execute: $ runhaskell Setup.lhs configure $ runhaskell Setup.lhs build-$ runhaskell Setup.lhs installed+$ runhaskell Setup.lhs install++Then try to create a test module++module Test where++import.Transform.Examples.Company+import Transform.Examples.Imdb+import Transform.Examples.Women++and interpret it++$ ghci Test.hs
pointless-rewrite.cabal view
@@ -1,5 +1,5 @@ Name: pointless-rewrite-Version: 0.0.2+Version: 0.0.3 License: BSD3 License-file: LICENSE Author: Alcino Cunha <alcino@di.uminho.pt>, Hugo Pacheco <hpacheco@di.uminho.pt>@@ -14,13 +14,15 @@ extra-source-files: README, Test.hs Build-type: Simple-Cabal-Version: >= 1.2.3+Cabal-Version: >= 1.4 Library Hs-Source-Dirs: src- Build-Depends: mtl >= 1, base >= 4 && < 5, pointless-haskell >= 0.0.5, pointless-lenses >= 0.0.7, haskell98, process+ Build-Depends: mtl >= 1, base >= 4 && < 5, pointless-haskell >= 0.0.6, pointless-lenses >= 0.0.8, process, containers exposed-modules:+ Data.Default Data.Type+ Data.Pf Data.Spine Data.Equal Data.Eval@@ -32,6 +34,8 @@ Transform.Rules.PF.Products Transform.Rules.PF.Rec Transform.Rules.PF.Sums+ Transform.Rules.PF.Monoids+ Transform.Rules.PF.Lists Transform.Rules.Lenses Transform.Rules.Lenses.Combinators Transform.Rules.Lenses.Dists@@ -42,8 +46,9 @@ Transform.Rules.SYB.TP Transform.Rules.SYB.TU Transform.Rules.SYB+ Transform.Rules.XPath Transform.Examples.Imdb Transform.Examples.Company Transform.Examples.Women - extensions: ScopedTypeVariables, FlexibleContexts, Rank2Types, TypeOperators, TypeFamilies, GADTs+ extensions: ScopedTypeVariables, FlexibleContexts, Rank2Types, TypeOperators, TypeFamilies, GADTs, ViewPatterns
+ src/Data/Default.hs view
@@ -0,0 +1,68 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.Default+-- Copyright : (c) 2010 University of Minho+-- License : BSD3+--+-- Maintainer : hpacheco@di.uminho.pt+-- Stability : experimental+-- Portability : non-portable+--+-- Pointless Rewrite:+-- automatic transformation system for point-free programs+-- +-- Type-safe representation of types and point-free expressions at the value level, including+-- representation of recursive types as fixpoints of functors.+--+-----------------------------------------------------------------------------++module Data.Default where++import Data.Type+import Data.Spine+import Generics.Pointless.Functors++type Generator = forall a. Type a -> a+type GeneratorF = forall f a. Fctr f -> Type a -> Rep f a++-- | Default generator for representable types+defvalue :: Generator+defvalue Int = 0+defvalue Bool = False+defvalue Char = ' '+defvalue (Prod a b) = (defvalue a,defvalue b)+defvalue (Either a b) = Left $ defvalue a+defvalue (List a) = []+defvalue a@(Data _ f) = inn $ defvalueF f a+defvalue a@(NewData _ f) = Inn $ defvalueF f a+defvalue a = error $ "no default generator for " ++ show a++-- | Default generator for representable functor types+-- important to deal with recursive occurences to avoid infinite values+defvalueF :: GeneratorF+defvalueF I a = defvalue a+defvalueF L a = []+defvalueF (K c) a = defvalue c+defvalueF (f :*!: g) a = (defvalueF f a,defvalueF g a)+defvalueF (f :+!: g) a = if (countId f <= countId g) then Left (defvalueF f a) else Right (defvalueF g a)+defvalueF (I :@!: g) a = defvalueF g a+defvalueF (K c :@!: g) a = defvalue c+defvalueF (L :@!: g) a = []+defvalueF ((f :*!: g) :@!: h) a = defvalueF ((f :@!: h) :*!: (g :@!: h)) a+defvalueF ((f :+!: g) :@!: h) a = defvalueF ((f :@!: h) :+!: (g :@!: h)) a+defvalueF ((f :@!: g) :@!: h) a = defvalueF (f :@!: (g :@!: h)) a++-- | Counts the number of recursive invocations in a functor+countId :: Fctr f -> Int+countId I = 1+countId (K c) = 0+countId L = 0+countId (f :*!: g) = countId f + countId g+countId (f :+!: g) = min (countId f) (countId g)+countId (I :@!: g) = countId g+countId (K c :@!: g) = 0+countId (L :@!: g) = 0 -- as long as we return the empty list, there is no problem with recursive invocations+countId ((f :*!: g) :@!: h) = countId ((f :@!: h) :*!: (g :@!: h))+countId ((f :+!: g) :@!: h) = countId ((f :@!: h) :+!: (g :@!: h))+countId ((f :@!: g) :@!: h) = countId (f :@!: (g :@!: h))+
src/Data/Equal.hs view
@@ -18,75 +18,119 @@ module Data.Equal where import Data.Type+import Data.Pf import Data.Spine import Control.Monad hiding (Functor(..)) import Unsafe.Coerce+import Control.Monad.State as ST hiding (Functor(..))+import Control.Monad.Reader hiding (Functor(..))+import Data.Map as Map+import Data.List as List+import Prelude hiding (Functor(..)) -import Generics.Pointless.Functors+import Generics.Pointless.Functors hiding (rep) data Equal a b where Eq :: Equal a a -teq :: MonadPlus m => Type a -> Type b -> m (Equal a b)-teq Any _ = return (unsafeCoerce Eq)-teq _ Any = return (unsafeCoerce Eq)-teq (Id a) b = teq a b-teq a (Id b) = teq a b-teq One One = return Eq-teq Int Int = return Eq-teq Bool Bool = return Eq-teq Char Char = return Eq-teq (Prod a b) (Prod c d) = do- Eq <- teq a c- Eq <- teq b d+teqBool :: Type a -> Type b -> Bool+teqBool a b = maybe False (const True) (teq a b)++type Vars = Map String DynType++-- type equality where the left-side type may have unbounded variables, representing pattern-matching+teqvar :: MonadPlus m => Type a -> Type b -> StateT Vars m (Equal a b)+teqvar (Var n) a = do+ vars <- ST.get+ case (Map.lookup n vars) of+ { Just (DynT t) -> do+ Eq <- teq t a+ return (unsafeCoerce Eq)+ ; otherwise -> do+ ST.put (Map.insert n (DynT a) vars)+ return (unsafeCoerce Eq)+ }+teqvar Any _ = return (unsafeCoerce Eq)+teqvar _ Any = return (unsafeCoerce Eq)+teqvar (Id a) (Id b) = teqvar a b+teqvar One One = return Eq+teqvar Int Int = return Eq+teqvar Bool Bool = return Eq+teqvar Char Char = return Eq+teqvar (Prod a b) (Prod c d) = do+ Eq <- teqvar a c+ Eq <- teqvar b d return Eq-teq (Either a b) (Either c d) = do- Eq <- teq a c- Eq <- teq b d+teqvar (Either a b) (Either c d) = do+ Eq <- teqvar a c+ Eq <- teqvar b d return Eq-teq (Data s fx) (Data s' fy) = do- guard (s == s')- Eq <- feq fx fy+teqvar (Data s fx) (Data s' fy) = do+ guard (sameName s s')+ Eq <- feqvar fx fy return (unsafeCoerce Eq)-teq (Fun a b) (Fun c d) = do- Eq <- teq a c- Eq <- teq b d+teqvar (NewData s fx) (NewData s' fy) = do+ guard (sameName s s')+ Eq <- feqvar fx fy+ return (unsafeCoerce Eq)+teqvar (List a) (List b) = do+ Eq <- teqvar a b return Eq-teq (Lns a b) (Lns c d) = do- Eq <- teq a c- Eq <- teq b d+teqvar (Fun a b) (Fun c d) = do+ Eq <- teqvar a c+ Eq <- teqvar b d return Eq-teq (Pf a) (Pf b) = do- Eq <- teq a b+teqvar (Lns a b) (Lns c d) = do+ Eq <- teqvar a c+ Eq <- teqvar b d return Eq-teq Dynamic Dynamic = error "dynamic equality"-teq TP TP = return Eq-teq (TU a) (TU b) = do- Eq <- teq a b+teqvar (Pf a) (Pf b) = do+ Eq <- teqvar a b return Eq-teq _ _ = mzero+teqvar Dynamic Dynamic = return Eq+teqvar TP TP = return Eq+teqvar (TU a) (TU b) = do+ Eq <- teqvar a b+ return Eq+teqvar _ _ = mzero -feq :: MonadPlus m => Fctr f -> Fctr g -> m (Equal (Fix f) (Fix g))-feq I I = return Eq-feq (K a) (K b) = do- Eq <- teq a b+teqvars :: MonadPlus m => Type a -> Type b -> m (Equal a b,Vars)+teqvars a b = runStateT (teqvar a b) Map.empty++-- regular type equality+teq :: MonadPlus m => Type a -> Type b -> m (Equal a b)+teq a b = evalStateT (teqvar a b) Map.empty++feqvar :: MonadPlus m => Fctr f -> Fctr g -> StateT Vars m (Equal (Fix f) (Fix g))+feqvar I I = return Eq+feqvar (K a) (K b) = do+ Eq <- teqvar a b return Eq-feq L L = return Eq-feq (f :*!: g) (h :*!: i) = do- Eq <- feq f h- Eq <- feq g i+feqvar L L = return Eq+feqvar (f :*!: g) (h :*!: i) = do+ Eq <- feqvar f h+ Eq <- feqvar g i return Eq-feq (f :+!: g) (h :+!: i) = do- Eq <- feq f h- Eq <- feq g i+feqvar (f :+!: g) (h :+!: i) = do+ Eq <- feqvar f h+ Eq <- feqvar g i return Eq-feq (f :@!: g) (h :@!: i) = do- Eq <- feq f h- Eq <- feq g i+feqvar (f :@!: g) (h :@!: i) = do+ Eq <- feqvar f h+ Eq <- feqvar g i return Eq-feq _ _ = mzero+feqvar AnyF f = return (unsafeCoerce Eq)+feqvar f AnyF = return (unsafeCoerce Eq)+feqvar _ _ = mzero +feq :: MonadPlus m => Fctr f -> Fctr g -> m (Equal (Fix f) (Fix g))+feq f g = evalStateT (feqvar f g) Map.empty++-- | Tests if a functor is recursive or not, by applying it to two distinct types.+isRec :: Fctr f -> Bool+isRec fctr = case teq (rep fctr Int) (rep fctr One) of { Just Eq -> False ; otherwise -> True }+ -- | Syntactic equality, with the exception of protected values. geq :: Type a -> a -> a -> Bool geq (Pf t) (PROTECT x) y = geq (Pf t) x y@@ -123,10 +167,57 @@ aux' t (f1 `Ap` (t1 :| a1)) t' (f2 `Ap` (t2 :| a2)) = aux' (Fun t1 t) f1 (Fun t2 t') f2 && aux t1 t2 a1 a2 aux' _ _ _ _ = False +-- | Explicitly coerce a value of a given type to another given type. coerce :: MonadPlus m => Type a -> Type b -> a -> m b coerce a b x = do Eq <- teq a b return x +collectDyn :: MonadPlus m => Type a -> a -> m DynType+collectDyn a v = case collectDyn' a v of { Just d -> return d; otherwise -> mzero }+collectDyn' :: Type a -> a -> Maybe DynType+collectDyn' = collect q plus+ where q :: MonadPlus m => GenericQ (m DynType)+ q (Pf _) (MKDYN a) = return $ DynT a+ q _ _ = mzero+ plus :: Maybe DynType -> Maybe DynType -> Maybe DynType+ plus (Just (DynT a)) (Just (DynT b)) = teq a b >> return (DynT a)+ plus m Nothing = m+ plus Nothing n = n++collectNewNames :: Type a -> [String]+collectNewNames = List.map fst . Map.toList . collectNewDatas++collectNewDatas :: Type a -> Map String DynFctr+collectNewDatas = maybe Map.empty id . collect q mcat TypeRep+ where q :: MonadPlus m => GenericQ (m (Map String DynFctr))+ q TypeRep (NewData s f) = return $ Map.singleton s (DynF f)+ q _ _ = return Map.empty+ mcat m n = do { x <- m; y <- n; return (x `Map.union` y) }++{-+showDatas :: Type a -> String+showDatas = maybe [] id . collect q mcat TypeRep+ where q :: MonadPlus m => GenericQ (m String)+ q TypeRep d@(isData -> True) = return (showData d ++ "\n")+ q _ _ = return []+ mcat m n = do { x <- m; y <- n; return (x ++ y) }+-}+collectVars :: Type a -> [String]+collectVars = maybe [] id . collect q mcat TypeRep+ where q :: MonadPlus m => GenericQ (m [String])+ q TypeRep (Var s) = return [s]+ q _ _ = return []+ mcat m n = do { x <- m; y <- n; return (x ++ y) }++collect :: MonadPlus m => GenericQ (m r) -> (m r -> m r -> m r) -> Type a -> a -> m r+collect (q :: GenericQ (m r)) plus a x = collectSpine a (toSpine a x)+ where collectSpine :: MonadPlus m => Type a -> Spine a -> m r+ collectSpine t s@(As _ _) = q t (fromSpine s)+ collectSpine t s@(Ap f (a :| v)) = q t (fromSpine s)+ `plus` (collectSpine (Fun a t) f)+ `plus` (collectSpine a (toSpine a v))++-- | Find a value of type b inside a value of type a find :: Type b -> b -> Type a -> a -> Bool find b y a x = findSpine a (toSpine a x) where findSpine :: Type a -> Spine a -> Bool@@ -135,11 +226,201 @@ otherwise -> False } findSpine t s@(Ap f (a :| v)) = (case teq t b of {- Just Eq -> geqt b y (spineVal s);+ Just Eq -> geqt b y (fromSpine s); otherwise -> False }) || findSpine (Fun a t) f || findSpine a (toSpine a v)- spineVal :: Spine a -> a- spineVal (As v con) = v- spineVal (Ap f (t :| v)) = spineVal f v++removeIds :: Type a -> a -> a+removeIds t x = fromSpine $ removeIdSpine t $ toSpine t x++removeIdSpine :: Type a -> Spine a -> Spine a+removeIdSpine TypeRep s@(fromSpine -> (Id a)) = removeIdSpine TypeRep (toSpine TypeRep a)+removeIdSpine t (As v con) = As v con+removeIdSpine t s@(Ap f (a :| v)) = Ap (removeIdSpine (Fun a t) f) (a :| fromSpine (removeIdSpine a (toSpine a v)))++unDyn :: Type a -> Dynamic -> a+unDyn t (Dyn a x) = case teq t a of { Just Eq -> x; otherwise -> error "unDyn failed"}++cast :: Type a -> Type b -> b -> a+cast a Dynamic (Dyn b x) = cast a b x+cast a b@(Data s f) x | isBasic a = case teq (rep f b) a of { Just Eq -> out x; otherwise -> error "type cast failed"}+cast a b@(NewData s f) x | isBasic a = case teq (rep f b) a of { Just Eq -> out x; otherwise -> error "type cast failed"}+cast a b x = case teq a b of { Just Eq -> x; otherwise -> error "type cast failed"}++isInt :: Type a -> Maybe (Equal a Int)+isInt a = teq a Int+isList :: Type a -> Maybe (Equal a [b])+isList a = teq a (List Any)+isNat :: Type a -> Maybe (Equal a Nat)+isNat a = teq a nat++-- infers a new functor for newly created recursive types+reshape :: MonadPlus m => Type a -> m DynType+reshape (NewData s f) = do+ let mark = Id Any+ DynF g <- reshapeF f+ FRep h <- inferFctr mark (rep g mark)+ return $ DynT $ NewData s h+reshape (Prod a b) = do+ DynT c <- reshape a + DynT d <- reshape b+ return $ DynT $ Prod c d+reshape (Either a b) = do+ DynT c <- reshape a + DynT d <- reshape b+ return $ DynT $ Either c d+reshape (List a) = do+ DynT b <- reshape a+ return $ DynT $ List b+reshape a = return $ DynT a+ +reshapeF :: MonadPlus m => Fctr f -> m DynFctr+reshapeF I = return $ DynF I+reshapeF (K a) = do+ DynT b <- reshape a+ return $ DynF $ K b+reshapeF L = return $ DynF L+reshapeF (f :*!: g) = do+ DynF h <- reshapeF f+ DynF i <- reshapeF g+ return $ DynF $ h :*!: i+reshapeF (f :+!: g) = do+ DynF h <- reshapeF f+ DynF i <- reshapeF g+ return $ DynF $ h :+!: i+reshapeF (f :@!: g) = do+ DynF h <- reshapeF f+ DynF i <- reshapeF g+ return $ DynF $ h :@!: i++data FctrRep a b where+ FRep :: (Functor f,Rep f a ~ b) => Fctr f -> FctrRep a b++-- Infers a new functor from a base type and an identity marker+inferFctr :: MonadPlus m => Type a -> Type b -> m (FctrRep a b)+inferFctr a (Prod x y) = do+ FRep f <- inferFctr a x+ FRep g <- inferFctr a y+ return $ FRep $ f :*!: g+inferFctr a (Either x y) = do+ FRep f <- inferFctr a x+ FRep g <- inferFctr a y+ return $ FRep $ f :+!: g+inferFctr a (List x) = do+ FRep f <- inferFctr a x+ return $ FRep $ L :@!: f+inferFctr a x = (do+ Eq <- teq a x+ return $ FRep I)+ `mplus` (do+ return $ FRep (K x))++-- Infers a new constant functor from a base type+-- The functor is always constant, i.e., forall a,b. Rep f a ~ Rep f b, altough this escapes the type-checker.+inferKFctr :: MonadPlus m => Type b -> m (FctrRep Dynamic b)+inferKFctr (Prod x y) = do+ FRep f <- inferKFctr x+ FRep g <- inferKFctr y+ return $ FRep $ f :*!: g+inferKFctr (Either x y) = do+ FRep f <- inferKFctr x+ FRep g <- inferKFctr y+ return $ FRep $ f :+!: g+inferKFctr (List x) = do+ FRep f <- inferKFctr x+ return $ FRep $ L :@!: f+inferKFctr x = return $ FRep (K x)++type TypeRule s = MonadPlus m => forall a. Type a -> StateT s m (Type a)+type FctrRule s = MonadPlus m => forall f. Fctr f -> StateT s m (Fctr f)++-- replaces the variables in an argument type with the concrete instantiations in the context.+replacevar :: MonadPlus m => Type a -> Vars -> m (Type a)+replacevar t vars = evalStateT (replace var none t) vars+ where+ var :: TypeRule Vars+ var (Var s) = do+ ctx <- ST.get+ case (Map.lookup s ctx) of+ { Just (DynT a) -> return (unsafeCoerce a)+ ; otherwise -> mzero }+ var _ = mzero+ none :: FctrRule Vars+ none f = mzero++replacedyn :: Type a -> Type a+replacedyn t = maybe t id $ evalStateT (replace dyn kdyn t) ()+ where dyn :: TypeRule ()+ dyn Dynamic = return Any+ dyn _ = mzero+ kdyn :: FctrRule ()+ kdyn (K Dynamic) = return AnyF+ kdyn _ = mzero++replace,replace' :: TypeRule s -> FctrRule s -> TypeRule s+replace tr fr t = tr t `mplus` replace' tr fr t+replace' tr fr (Var s) = return $ Var s+replace' tr fr (Id a) = do+ x <- replace tr fr a+ return (Id x)+replace' tr fr Int = return Int+replace' tr fr Bool = return Bool+replace' tr fr Char = return Char+replace' tr fr One = return One+replace' tr fr (Either a b) = do+ x <- replace tr fr a+ y <- replace tr fr b+ return (Either x y)+replace' tr fr (Prod a b) = do+ x <- replace tr fr a+ y <- replace tr fr b+ return (Prod x y)+replace' tr fr (Fun a b) = do+ x <- replace tr fr a+ y <- replace tr fr b+ return (Fun x y)+replace' tr fr (Lns a b) = do+ x <- replace tr fr a+ y <- replace tr fr b+ return (Lns x y)+replace' tr fr (List a) = do+ x <- replace tr fr a+ return (List x)+replace' tr fr (Data s f) = do+ g <- replaceF tr fr f+ Eq <- feq f g+ return (Data s g)+replace' tr fr (NewData s f) = do+ g <- replaceF tr fr f+ return (NewData s g)+replace' tr fr (Pf a) = do+ x <- replace tr fr a+ return (Pf x)+replace' tr fr TP = return TP+replace' tr fr (TU a) = do+ x <- replace tr fr a+ return $ TU a+replace' tr fr Any = return Any+replace' tr fr Dynamic = return Dynamic++replaceF,replaceF' :: TypeRule s -> FctrRule s -> FctrRule s+replaceF tr fr f = fr f `mplus` replaceF' tr fr f+replaceF' tr fr I = return I+replaceF' tr fr (K a) = do+ x <- replace tr fr a + return (K x)+replaceF' tr fr L = return L+replaceF' tr fr (f :*!: g) = do+ x <- replaceF tr fr f+ y <- replaceF tr fr g+ return (x :*!: y)+replaceF' tr fr (f :+!: g) = do+ x <- replaceF tr fr f+ y <- replaceF tr fr g+ return (x :+!: y)+replaceF' tr fr (f :@!: g) = do+ x <- replaceF tr fr f+ y <- replaceF tr fr g+ return (x :@!: y)
+ src/Data/Equal.hs-boot view
@@ -0,0 +1,11 @@+module Data.Equal where++import Data.Type+import Generics.Pointless.Functors++data Equal a b where+ Eq :: Equal a a++isInt :: Type a -> Maybe (Equal a Int)+isList :: Type a -> Maybe (Equal a [b])+isNat :: Type a -> Maybe (Equal a Nat)
src/Data/Eval.hs view
@@ -19,22 +19,31 @@ import Prelude hiding (Functor(..)) import Data.Type+import Data.Pf+import Data.Spine import Data.Equal import Data.Monoid+import Data.Char+import Data.List import Generics.Pointless.Combinators import Generics.Pointless.RecursionPatterns-import Generics.Pointless.Functors+import Generics.Pointless.Functors hiding (rep) import qualified Generics.Pointless.Fctrable as F import Generics.Pointless.Lenses import Generics.Pointless.Lenses.Combinators import Generics.Pointless.Lenses.RecursionPatterns+import Generics.Pointless.Lenses.Examples.Examples import Generics.Pointless.Lenses.Examples.Recs +wrap :: a -> [a]+wrap a = [a]+ fctrT :: Functor f => Fctr f -> F.Fctr f fctrT I = F.I fctrT (K c) = F.K+fctrT L = F.L fctrT (f :*!: g) = fctrT f F.:*!: fctrT g fctrT (f :+!: g) = fctrT f F.:+!: fctrT g fctrT (f :@!: g) = fctrT f F.:@!: fctrT g@@ -48,33 +57,31 @@ fmap_lnsF :: Functor f => Fctr f -> Lens c a -> Lens (Rep f c) (Rep f a) fmap_lnsF (f::Fctr f) l = Lens get' put' create' where get' = fmap fix (get l)- put' = fmap fix (put l) . fzip (fctrT f) (create l)+ put' = fmap fix (put l) . fzip (fixF f) (create l) create' = fmap fix (create l) fix = fixF f -ana_lnsF :: (Mu b,Functor (PF b)) => b -> Fctr (PF b) -> Lens a (F b a) -> Lens a b-ana_lnsF (b::b) f l = Lens get' put' create'+ana_lnsF :: (Mu b,Functor (PF b)) => Ann b -> Fctr (PF b) -> Lens a (F b a) -> Lens a b+ana_lnsF (b::Ann b) f l = Lens get' put' create' where get' = ana b (get l)- put' = accum b (put l) (fzip (fctrT g) create' . (id >< get l))+ put' = accum b (put l) (fzip (fixF g) create' . (id >< get l)) create' = cata b (create l) g = f :: Fctr (PF b) -cata_lnsF :: (Mu a,Functor (PF a)) => a -> Fctr (PF a) -> (Lens (F a b) b) -> Lens a b-cata_lnsF (a::a) f l = Lens get' put' create'+cata_lnsF :: (Mu a,Functor (PF a)) => Ann a -> Fctr (PF a) -> (Lens (F a b) b) -> Lens a b+cata_lnsF (a::Ann a) f l = Lens get' put' create' where get' = cata a (get l)- put' = ana a (fzip (fctrT g) create' . (put l . (id >< fmap (fixF f) get') /\ snd) . (id >< out))+ put' = ana a (fzip (fixF g) create' . (put l . (id >< fmap (fixF f) get') /\ snd) . (id >< out)) create' = ana a (create l) g = f :: Fctr (PF a) eval :: Type a -> Pf a -> a-eval _ HOLE = error "hole"+eval _ BOT = error "_L" eval _ TOP = error "top" eval (Fun _ _) (FUN _ f) = f eval (Fun _ _) (CONV _ f) = error "converse evaluation" eval (Lns _ _) (CONV_LNS _ f) = error "converse evaluation" eval (Lns _ _) (LNS _ l) = l-eval (Fun c a) (COMPF fctr x f g) = eval (Fun c a) (COMP (rep fctr x) f g)-eval (Lns c a) (COMPF_LNS fctr x f g) = eval (Lns c a) (COMP_LNS (rep fctr x) f g) eval (Fun a b) (PROTECT f) = eval (Fun a b) f eval (Lns a b) (PROTECT_LNS f) = eval (Lns a b) f eval _ (VAR s) = error s@@ -91,8 +98,13 @@ eval (Fun (Either a b) c) (EITHER f g) = eval (Fun a c) f \/ eval (Fun b c) g eval (Fun (Either a b) (Either c d)) (SUM f g) = eval (Fun a c) f -|- eval (Fun b d) g +eval _ (MKDYN a) = Dyn a+eval _ (UNDYN a) = unDyn a+eval (Fun b _) (CAST a) = cast a b+ eval _ ZERO = const mempty eval _ PLUS = uncurry mappend+eval _ FOLD = mconcat eval (Fun _ _) ID = id eval (Fun _ _) SWAP = swap@@ -109,11 +121,21 @@ eval (Fun _ _) INN = inn eval (Fun _ _) OUT = out eval (Fun _ _) (FMAP fctr (Fun c a) f) = fmap (fixF fctr) (eval (Fun c a) f)-eval (Fun _ _) (FZIP fctr t f) = fzip (fctrT fctr) $ eval t f-eval (Fun a b@(Data _ fctr)) (ANA f) = ana _L (eval (Fun a (rep fctr a)) f)-eval (Fun a@(Data _ fctr) b) (CATA f) = cata _L (eval (Fun (rep fctr b) b) f)-eval (Fun a@(Data _ fctr) b) (PARA f) = para _L (eval (Fun (rep fctr (Prod b a)) b) f)+eval (Fun _ _) (FZIP fctr t f) = fzip (fixF fctr) $ eval t f+eval (Fun a b@(dataFctr -> Just fctr)) (ANA f) = ana _L (eval (Fun a (rep fctr a)) f)+eval (Fun a@(dataFctr -> Just fctr) b) (CATA f) = cata _L (eval (Fun (rep fctr b) b) f)+eval (Fun a@(dataFctr -> Just fctr) b) (PARA f) = para _L (eval (Fun (rep fctr (Prod b a)) b) f)+eval (Fun a (List b)) (ANA f) = ana _L (eval (Fun a (rep (listfctr b) a)) f)+eval (Fun (List a) b) (CATA f) = cata _L (eval (Fun (rep (listfctr a) b) b) f)+eval (Fun la@(List a) b) (PARA f) = para _L (eval (Fun (rep (listfctr a) (Prod b la)) b) f) +eval (Fun (List a) (List b)) (MAP f) = map (eval (Fun a b) f)+eval (Fun _ _) LHEAD = \l -> if (null l) then [] else [head l]+eval (Fun _ _) LTAIL = \l -> if (null l) then [] else tail l+eval (Fun _ _) WRAP = wrap+eval (Fun _ _) LENGTH = get (length_lns _L)+eval (Fun _ _) ONE = const (Nat 1)+ eval (Fun c a) (GET l) = get (eval (Lns c a) l) eval (Fun (Prod a c) _) (PUT l) = put (eval (Lns c a) l) eval (Fun a c) (CREATE l) = create (eval (Lns c a) l)@@ -143,21 +165,26 @@ eval (Lns _ _) COASSOCL_LNS = coassocl_lns eval (Lns _ _) COASSOCR_LNS = coassocr_lns -eval (Lns _ a@(Data _ fctr)) INN_LNS = inn_lnsF fctr-eval (Lns a@(Data _ fctr) _) OUT_LNS = out_lnsF fctr+eval (Lns _ (List a)) INN_LNS = inn_lnsF (listfctr a)+eval (Lns (List a) _) OUT_LNS = out_lnsF (listfctr a)+eval (Lns _ a@(dataFctr -> Just fctr)) INN_LNS = inn_lnsF fctr+eval (Lns a@(dataFctr -> Just fctr) _) OUT_LNS = out_lnsF fctr eval (Lns _ _) (FMAP_LNS fctr (Fun c a) f) = fmap_lnsF fctr (eval (Lns c a) f)-eval (Lns a b@(Data _ fctr)) (ANA_LNS f) = ana_lnsF _L fctr (eval (Lns a (rep fctr a)) f)-eval (Lns a@(Data _ fctr) b) (CATA_LNS f) = cata_lnsF _L fctr (eval (Lns (rep fctr b) b) f)+eval (Lns a (List b)) (ANA_LNS f) = ana_lnsF _L (listfctr b) (eval (Lns a (rep (listfctr b) a)) f)+eval (Lns (List a) b) (CATA_LNS f) = cata_lnsF _L (listfctr a) (eval (Lns (rep (listfctr a) b) b) f)+eval (Lns a b@(dataFctr -> Just fctr)) (ANA_LNS f) = ana_lnsF _L fctr (eval (Lns a (rep fctr a)) f)+eval (Lns a@(dataFctr -> Just fctr) b) (CATA_LNS f) = cata_lnsF _L fctr (eval (Lns (rep fctr b) b) f) -eval (Lns la lb) (MAP_LNS l1) = map_pf (eval (Lns (unlist la) (unlist lb)) l1)-eval (Lns la _) (LENGTH_LNS v) = length_pf v+eval (Lns (List a) (List b)) (MAP_LNS l1) = map_pf (eval (Lns a b) l1)+eval (Lns (List a) _) (LENGTH_LNS v) = length_lns v eval (Lns _ _) FILTER_LEFT_LNS = filter_left_pf eval (Lns _ _) FILTER_RIGHT_LNS = filter_right_pf eval (Lns _ _) CAT_LNS = cat_pf eval (Lns _ _) CONCAT_LNS = concat_pf-eval (Lns _ _) SUML_LNS = suml_pf-eval (Lns _ _) PLUS_LNS = plus_pf+eval (Lns _ _) SUMN_LNS = sum_pf+eval (Lns _ _) PLUSN_LNS = plus_lns +eval p (APPLY Dynamic t) = applyDyn $ \a -> mkDyn a . eval (Fun a a) (APPLY a t) eval p (APPLY a (ALL f)) = eval p (allT a f) eval p (APPLY a (EVERYWHERE f)) = eval p (everywhereEval a f) eval p (APPLY a (EVERYWHERE' f)) = eval p (everywhereEval' a f)@@ -165,45 +192,89 @@ eval p (APPLY a (SEQ f g)) = eval p (APPLY a g) . eval p (APPLY a f) eval p (APPLY a (MKT t f)) = eval p (mkT a t f) eval p (APPLY a NOP) = id++eval q@(Fun _ r) (APPLYQ Dynamic f) = applyDyn $ \a -> eval (Fun a r) (APPLYQ a f) eval q@(Fun a r)(APPLYQ _ (GMAPQ f)) = eval q (gmapQ r a f)-eval q (APPLYQ a (EVERYTHING f)) = eval q (everythingEval a f)+eval q@(Fun _ r) (APPLYQ a (EVERYTHING f)) = eval q (everythingEval a f) eval q (APPLYQ a (EXTQ f t g)) = eval q (extQ a f t g) eval q (APPLYQ t (UNION f g)) = eval q (APPLYQ t f) `mappend` eval q (APPLYQ t g) eval q (APPLYQ a (MKQ t f)) = eval q (mkQ a t f) eval q (APPLYQ a EMPTYQ) = mempty+eval (Fun _ s) (APPLYQ a (SEQQ (q :: Pf (Q r)) f)) = let r = typeof :: Type r in eval (Fun r s) f . eval (Fun a r) (APPLYQ a q)+eval _ (f :?: p) = Q (\t x -> let y = unQ (eval (TU (List Dynamic)) f) t x+ in filter (unQ (eval (TU Bool) p) Dynamic) y)+eval (Fun _ _) NONEMPTY = not . null -everywhereEval t f = APPLY t (f `SEQ` ALL (EVERYWHERE f))-everywhereEval' t f = APPLY t (ALL (EVERYWHERE' f) `SEQ` f)+eval q (APPLYQ a SELF) = if isAtt a then mempty else wrap . mkDyn a+eval q (APPLYQ a ATT) = if isAtt a then wrap . mkDyn a else mempty+eval q (APPLYQ a CHILD) = eval q $ APPLYQ a $ GMAPQ SELF+eval q (APPLYQ a ATTRIBUTE) = eval q $ APPLYQ a $ GMAPQ ATT+eval q (APPLYQ a DESCENDANT) = eval q $ APPLYQ a $ EVERYTHING CHILD+eval q (APPLYQ a DESCSELF) = eval q $ APPLYQ a $ EVERYTHING SELF+eval q (APPLYQ a@(dataName -> Just name) (NAME n)) | sameName name n = eval q (APPLYQ a SELF)+eval q (APPLYQ a@(dataName -> Just name) (NAME n)) | sameName name ("@"++n) = eval q (APPLYQ a ATT)+eval q (APPLYQ a (NAME n)) = mempty+eval (Fun t r) (APPLYQ a (f :/: g)) = mconcat . map (eval (Fun Dynamic r) (APPLYQ Dynamic g)) . eval (Fun t (List Dynamic)) (APPLYQ a f)+eval (TU (Prod a b)) (f :/\: g) = Q (\t x -> (unQ (eval (TU a) f) t x,unQ (eval (TU b) g) t x))++eval t f = error $ "eval undefined for: " ++ show t+everywhereEval t f = APPLY t (ALL (EVERYWHERE f) `SEQ` f)+everywhereEval' t f = APPLY t (f `SEQ` ALL (EVERYWHERE' f)) everythingEval t f = APPLYQ t (f `UNION` GMAPQ (EVERYTHING f)) -- ** Type-preserving specialization +allTF :: Fctr f -> Type a -> Pf T -> Pf (Rep f a -> Rep f a)+allTF I a t = APPLY a t+allTF L a t = MAP $ APPLY a t+allTF (K c) a t = APPLY c t+allTF (f :*!: g) a t = allTF f a t `PROD` allTF g a t+allTF (f :+!: g) a t = allTF f a t `SUM` allTF g a t+allTF (f :@!: g) a t = let ga = rep g a+ in COMP (rep f ga) (allTKF f ga t) (FMAP f (Fun ga ga) (allTF g a t))++allTKF :: Fctr f -> Type a -> Pf T -> Pf (Rep f a -> Rep f a)+allTKF I a t = ID+allTKF L a t = ID+allTKF (K c) a t = APPLY c t+allTKF (f :*!: g) a t = allTKF f a t `PROD` allTKF g a t+allTKF (f :+!: g) a t = allTKF f a t `SUM` allTKF g a t+allTKF (f :@!: g) a t = let ga = rep g a+ in COMP (rep f ga) (allTKF f ga t) (FMAP f (Fun ga ga) (allTKF g a t))+ allT :: Type a -> Pf T -> Pf (a -> a)-allT t@(Data _ fctr) g = let f = rep fctr t in COMP f INN $ COMP f (allTN f g) OUT-allT (Either a b) f = (APPLY a f) `SUM` (APPLY b f)-allT (Prod a b) f = (APPLY a f) `PROD` (APPLY b f)-allT _ _ = ID--- | We do not want it to recurse inside Datas, otherwise we get a full traversal-allTN :: Type a -> Pf T -> Pf (a -> a)-allTN (Either a b) f = (allTN a f) `SUM` (allTN b f)-allTN (Prod a b) f = (allTN a f) `PROD` (allTN b f)-allTN a f = APPLY a f+allT a@(Data s fctr) t = allTRec a fctr t+allT a@(NewData s fctr) t = allTRec a fctr t+allT (List a) t = MAP (APPLY a t)+allT (Either a b) t = (APPLY a t) `SUM` (APPLY b t)+allT (Prod a b) t = (APPLY a t) `PROD` (APPLY b t)+--allT Dynamic +allT a t = ID +allTRec :: (Functor (PF a),Mu a) => Type a -> Fctr (PF a) -> Pf T -> Pf (a -> a)+allTRec a fctr t = let f = rep fctr a+ in COMP f INN $ COMP f (allTF fctr a t) OUT+ -- | bottom-up (cata) everywhereT :: Type a -> Pf T -> Pf (a -> a)-everywhereT t@(Data _ fctr) g = let f = rep fctr t- boxf = rep fctr (Id t)- in CATA $ COMP t (APPLY t g) $ COMP f INN $ APPLY boxf $ EVERYWHERE g-everywhereT (Id t) f = ID-everywhereT t f = APPLY t (ALL (EVERYWHERE f) `SEQ` f)+everywhereT t@(Data n fctr) g = everywhereTRec t fctr g+everywhereT t@(NewData n fctr) g = everywhereTRec t fctr g+everywhereT t g = APPLY t (ALL (EVERYWHERE g) `SEQ` g) +everywhereTRec :: (Functor (PF a),Mu a) => Type a -> Fctr (PF a) -> Pf T -> Pf (a -> a)+everywhereTRec t fctr g = let f = rep fctr t+ in CATA $ COMP t (APPLY t g) $ COMP f INN (allTKF fctr t $ EVERYWHERE g)+ -- | top-down (ana) everywhereT' :: Type a -> Pf T -> Pf (a -> a)-everywhereT' t@(Data _ fctr) g = let f = rep fctr t- boxf = rep fctr (Id t)- in ANA $ COMP f (APPLY boxf $ EVERYWHERE' g) $ COMP t OUT $ APPLY t g-everywhereT' t f = APPLY t (f `SEQ` ALL (EVERYWHERE' f))+everywhereT' t@(Data n fctr) g = everywhereTRec' t fctr g+everywhereT' t@(NewData n fctr) g = everywhereTRec' t fctr g+everywhereT' t g = APPLY t (g `SEQ` ALL (EVERYWHERE' g)) +everywhereTRec' :: (Functor (PF a),Mu a) => Type a -> Fctr (PF a) -> Pf T -> Pf (a -> a)+everywhereTRec' t fctr g = let f = rep fctr t+ in ANA $ COMP f (allTKF fctr t $ EVERYWHERE' g) $ COMP t OUT $ APPLY t g+ mkT :: Type a -> Type x -> Pf (x -> x) -> Pf (a -> a) mkT t t' f = case teq t t' of {Just Eq -> f; otherwise -> ID} @@ -212,31 +283,47 @@ -- ** Type-unifying specialization -gmapQProd :: (Monoid r) => Type r -> Pf (a -> (r,r)) -> Pf (a -> r)-gmapQProd r (p::Pf (a -> (r,r))) = COMP (Prod r r) PLUS p+gmapQF :: Monoid r => Type r -> Fctr f -> Type a -> Pf (Q r) -> Pf (Rep f a -> r)+gmapQF r I a q = case teq r a of { Just Eq -> ID; otherwise -> APPLYQ a q }+gmapQF r L a q = case teq r a of { Just Eq -> FOLD; otherwise -> COMP (List r) FOLD $ MAP $ APPLYQ a q }+gmapQF r (K c) a q = APPLYQ c q+gmapQF r (f :+!: g) a q = gmapQF r f a q `EITHER` gmapQF r g a q+gmapQF r (f :*!: g) a q = COMP (Prod r r) PLUS $ gmapQF r f a q `PROD` gmapQF r g a q+gmapQF r (f :@!: g) a q = let ga = rep g a+ in COMP (rep f r) (gmapQKF r f r q) $ FMAP f (Fun ga r) (gmapQF r g a q) -gmapQId :: (Monoid r) => Type r -> Type r' -> Pf (Q r) -> Pf (r' -> r)-gmapQId r r' (f :: Pf (Q r)) = case teq r' r of {Just Eq -> ID; otherwise -> ZERO}+gmapQKF :: Monoid r => Type r -> Fctr f -> Type a -> Pf (Q r) -> Pf (Rep f a -> r)+gmapQKF r I a q = case teq r a of { Just Eq -> ID; otherwise -> ZERO }+gmapQKF r L a q = case teq r a of { Just Eq -> FOLD; otherwise -> ZERO }+gmapQKF r (K c) a q = APPLYQ c q+gmapQKF r (f :+!: g) a q = gmapQKF r f a q `EITHER` gmapQKF r g a q+gmapQKF r (f :*!: g) a q = COMP (Prod r r) PLUS $ gmapQKF r f a q `PROD` gmapQKF r g a q+gmapQKF r (f :@!: g) a q = let ga = rep g a+ in COMP (rep f r) (gmapQKF r f r q) $ FMAP f (Fun ga r) (gmapQKF r g a q) gmapQ :: (Monoid r) => Type r -> Type a -> Pf (Q r) -> Pf (a -> r)-gmapQ r t@(Data _ fctr) g = let f = rep fctr t in COMP f (gmapQN r f g) OUT+gmapQ r t@(Data _ fctr) g = gmapQRec r t fctr g+gmapQ r t@(NewData _ fctr) g = gmapQRec r t fctr g+gmapQ r (List a) f = COMP (List r) FOLD $ MAP $ APPLYQ a f gmapQ r (Either a b) f = (APPLYQ a f) `EITHER` (APPLYQ b f)-gmapQ r (Prod a b) f = gmapQProd r $ (APPLYQ a f) `PROD` (APPLYQ b f)-gmapQ r (Id a) f = gmapQId r a f+gmapQ r (Prod a b) f = COMP (Prod r r) PLUS $ APPLYQ a f `PROD` APPLYQ b f gmapQ r t f = ZERO --- | We do not want it to recurse inside Datas, otherwise we get a full traversal-gmapQN :: (Monoid r) => Type r -> Type a -> Pf (Q r) -> Pf (a -> r)-gmapQN r (Either a b) f = (gmapQN r a f) `EITHER` (gmapQN r b f)-gmapQN r (Prod a b) f = gmapQProd r $ (gmapQN r a f) `PROD` (gmapQN r b f)-gmapQN r a f = APPLYQ a f+gmapQRec :: (Functor (PF a), Mu a,Monoid r) => Type r -> Type a -> Fctr (PF a) -> Pf (Q r) -> Pf (a -> r)+gmapQRec r t fctr g = COMP (rep fctr t) (gmapQF r fctr t g) OUT everythingQ :: (Monoid r) => Type r -> Type a -> Pf (Q r) -> Pf (a -> r)-everythingQ r t@(Data _ fctr::Type t) (g::Pf (Q r)) = let fr = rep fctr r- boxfr = rep fctr (Id r)- ft = rep fctr t- in PARA $ gmapQProd r $ COMP (Prod fr ft) ((APPLYQ boxfr $ EVERYTHING g) `PROD` (COMP t (APPLYQ t g) INN)) (FMAP fctr (Fun (Prod r t) r) FST `SPLIT` FMAP fctr (Fun (Prod r t) t) SND)-everythingQ r t f = APPLYQ t (f `UNION` GMAPQ (EVERYTHING f))+everythingQ r t@(Data _ fctr) g = everythingQRec r t fctr g+everythingQ r t@(NewData _ fctr) g = everythingQRec r t fctr g+--everythingQ r t@(List a) g = everythingQRec r t (listfctr a) g+everythingQ r t g = APPLYQ t (g `UNION` GMAPQ (EVERYTHING g))++everythingQRec :: (Functor (PF a), Mu a,Monoid r) => Type r -> Type a -> Fctr (PF a) -> Pf (Q r) -> Pf (a -> r)+everythingQRec r t fctr g = let (fr,ft) = (rep fctr r,rep fctr t)+ (rr,rt) = (Prod r r,Prod r t)+ in PARA $ COMP rr PLUS+ $ COMP (Prod fr t) (gmapQKF r fctr r (EVERYTHING g) `PROD` APPLYQ t g)+ $ FMAP fctr (Fun rt r) FST `SPLIT` (COMP ft INN $ FMAP fctr (Fun rt t) SND) mkQ :: Monoid r => Type a -> Type x -> Pf (x -> r) -> Pf (a -> r)
src/Data/Lens.hs view
@@ -18,12 +18,15 @@ module Data.Lens where import Data.Type+import Data.Pf+import Data.Spine import Data.Equal+import Data.Default import Prelude hiding (Functor(..)) import Control.Monad hiding (Functor(..)) -import Generics.Pointless.Functors+import Generics.Pointless.Functors hiding (rep) import Generics.Pointless.Lenses -- | Computes the inverse lens for isomorphic lenses.@@ -55,68 +58,101 @@ inv _ ASSOCR_LNS = return ASSOCL_LNS inv _ COASSOCL_LNS = return COASSOCR_LNS inv _ COASSOCR_LNS = return COASSOCL_LNS-inv (Lns c (a@(Data _ fctr)::Type a)) INN_LNS = case teq c (rep fctr a) of- { Just Eq -> return (OUT_LNS :: (Mu a,Functor (PF a)) => Pf (Lens a (F a a)))+inv (Lns c a@(dataFctr -> Just fctr)) INN_LNS = case teq c (rep fctr a) of+ { Just Eq -> return OUT_LNS ; otherwise -> fail "inv INN_LNS" }-inv (Lns (a@(Data _ fctr)::Type a) c) OUT_LNS = case teq c (rep fctr a) of- { Just Eq -> return (INN_LNS :: (Mu a,Functor (PF a)) => Pf (Lens (F a a) a))+inv (Lns a@(dataFctr -> Just fctr) c) OUT_LNS = case teq c (rep fctr a) of+ { Just Eq -> return INN_LNS ; otherwise -> fail "inv OUT_LNS" } inv _ _ = mzero -- | Lifts a point-free function into a lens (unsafe).-lns :: MonadPlus m => Type (a -> b) -> Pf (a -> b) -> m (Pf (Lens a b))-lns (Fun _ _) (GET l) = return l+lensify :: MonadPlus m => Type (a -> b) -> Pf (a -> b) -> m (Pf (Lens a b))+lensify (Fun _ _) (GET l) = return l -lns (Fun a c) (COMP b f g) = do- f' <- lns (Fun b c) f- g' <- lns (Fun a b) g+lensify (Fun a c) (COMP b f g) = do+ f' <- lensify (Fun b c) f+ g' <- lensify (Fun a b) g return $ COMP_LNS b f' g'-lns (Fun (Prod a b) _) FST = return $ FST_LNS HOLE-lns (Fun (Prod a b) _) SND = return $ SND_LNS HOLE-lns (Fun (Prod a b) (Prod c d)) (f `PROD` g) = do- f' <- lns (Fun a c) f- g' <- lns (Fun b d) g+lensify (Fun (Prod a b) _) FST = return $ FST_LNS (constPf $ defvalue b)+lensify (Fun (Prod a b) _) SND = return $ SND_LNS (constPf $ defvalue a)+lensify (Fun (Prod a b) (Prod c d)) (f `PROD` g) = do+ f' <- lensify (Fun a c) f+ g' <- lensify (Fun b d) g return $ f' ><<< g'-lns (Fun (Either a b) (Either c d)) ((COMP _ INL f) `EITHER` (COMP _ INR g)) = do- f' <- lns (Fun a c) f- g' <- lns (Fun b d) g+lensify (Fun (Either a b) (Either c d)) ((COMP _ INL f) `EITHER` (COMP _ INR g)) = do+ f' <- lensify (Fun a c) f+ g' <- lensify (Fun b d) g return $ f' `SUM_LNS` g'-lns (Fun (Either a b) c) (f `EITHER` g) = do- f' <- lns (Fun a c) f- g' <- lns (Fun b c) g+ +-- Special either expressions+lensify (Fun (Either _ a) e@(Either x y)) (INL `EITHER` f) = do+ f' <- lensify (Fun a e) f+ return $ COMP_LNS (Either (Either x x) y) ((ID_LNS .\/<< ID_LNS) -|-<< ID_LNS)+ $ COMP_LNS (Either x e) COASSOCL_LNS $ ID_LNS -|-<< f'+lensify (Fun (Either a _) e@(Either x y)) (f `EITHER` INR) = do+ f' <- lensify (Fun a e) f+ return $ COMP_LNS (Either x (Either y y)) (ID_LNS -|-<< (ID_LNS \/.<< ID_LNS))+ $ COMP_LNS (Either e y) COASSOCR_LNS $ f' -|-<< ID_LNS+-- Regular either expression+lensify fun@(Fun _ l@(List a)) (ZERO `EITHER` f) = lensify fun+ $ COMP (Either One (Prod a l)) INN+ $ COMP (Either One l) (INL `EITHER` OUT) (BANG `SUM` f)+lensify fun@(Fun _ a@(isNat -> Just Eq)) (ZERO `EITHER` f) = lensify fun+ $ COMP (Either One a) INN+ $ COMP (Either One a) (INL `EITHER` OUT) (BANG `SUM` f)+lensify fun@(Fun _ l@(List a)) (f `EITHER` ZERO) = lensify fun+ $ COMP (Either One (Prod a l)) INN+ $ COMP (Either One l) (INL `EITHER` OUT)+ $ COMP (Either l One) COSWAP (f `SUM` BANG)+lensify fun@(Fun _ a@(isNat -> Just Eq)) (f `EITHER` ZERO) = lensify fun+ $ COMP (Either One a) INN+ $ COMP (Either One a) (INL `EITHER` OUT)+ $ COMP (Either a One) COSWAP (f `SUM` BANG)+ +lensify (Fun (Either a b) c) (f `EITHER` g) = do+ f' <- lensify (Fun a c) f+ g' <- lensify (Fun b c) g return $ EITHER_LNS (COMP One INL BANG) f' g'-lns (Fun (Either a b) (Either c d)) (f `SUM` g) = do- f' <- lns (Fun a c) f- g' <- lns (Fun b d) g+lensify (Fun (Either a b) (Either c d)) (f `SUM` g) = do+ f' <- lensify (Fun a c) f+ g' <- lensify (Fun b d) g return $ f' `SUM_LNS` g'-lns (Fun _ _) BANG = return $ BANG_LNS HOLE+lensify (Fun a _) BANG = return $ BANG_LNS (constPf $ defvalue a)++lensify (Fun _ a@(isList -> Just Eq)) PLUS = return CAT_LNS+lensify (Fun _ a@(isList -> Just Eq)) FOLD = return CONCAT_LNS+lensify (Fun _ a@(isNat -> Just Eq)) PLUS = return PLUSN_LNS+lensify (Fun _ a@(isNat -> Just Eq)) FOLD = return SUMN_LNS+lensify (Fun (List a) _) LENGTH = return $ LENGTH_LNS (defvalue a)+lensify (Fun (List a) (List b)) (MAP f) = do+ f' <- lensify (Fun a b) f+ return $ MAP_LNS f' -lns (Fun _ _) ID = return ID_LNS-lns (Fun _ _) SWAP = return SWAP_LNS-lns (Fun _ _) COSWAP = return COSWAP_LNS-lns (Fun _ _) DISTL = return DISTL_LNS-lns (Fun _ _) UNDISTL = return UNDISTL_LNS-lns (Fun _ _) DISTR = return DISTR_LNS-lns (Fun _ _) UNDISTR = return UNDISTR_LNS-lns (Fun _ _) ASSOCL = return ASSOCL_LNS-lns (Fun _ _) ASSOCR = return ASSOCR_LNS-lns (Fun _ _) COASSOCL = return COASSOCL_LNS-lns (Fun _ _) COASSOCR = return COASSOCR_LNS+lensify (Fun _ _) ID = return ID_LNS+lensify (Fun _ _) SWAP = return SWAP_LNS+lensify (Fun _ _) COSWAP = return COSWAP_LNS+lensify (Fun _ _) DISTL = return DISTL_LNS+lensify (Fun _ _) UNDISTL = return UNDISTL_LNS+lensify (Fun _ _) DISTR = return DISTR_LNS+lensify (Fun _ _) UNDISTR = return UNDISTR_LNS+lensify (Fun _ _) ASSOCL = return ASSOCL_LNS+lensify (Fun _ _) ASSOCR = return ASSOCR_LNS+lensify (Fun _ _) COASSOCL = return COASSOCL_LNS+lensify (Fun _ _) COASSOCR = return COASSOCR_LNS -lns (Fun _ _) INN = return INN_LNS-lns (Fun (a@(Data _ fctr)::Type a) c) OUT = case teq c (rep fctr a) of- { Just Eq -> return (OUT_LNS :: (Mu a,Functor (PF a)) => Pf (Lens a (F a a)))- ; otherwise -> fail "lns OUT" }-lns (Fun _ _) (FMAP fctr t f) = do- f' <- lns t f+lensify (Fun _ _) INN = return INN_LNS+lensify (Fun _ _) OUT = return OUT_LNS+lensify (Fun _ _) (FMAP fctr t f) = do+ f' <- lensify t f return $ FMAP_LNS fctr t f'-lns (Fun a b@(Data s fctr)) (ANA f) = do- f' <- lns (Fun a (rep fctr a)) f+lensify (Fun a b@(Data s fctr)) (ANA f) = do+ f' <- lensify (Fun a (rep fctr a)) f return $ ANA_LNS f'-lns (Fun a@(Data s fctr) b) (CATA f) = do- f' <- lns (Fun (rep fctr b) b) f+lensify (Fun a@(Data s fctr) b) (CATA f) = do+ f' <- lensify (Fun (rep fctr b) b) f return $ CATA_LNS f'-lns _ _ = mzero+lensify t v = fail $ "lensify " ++ gshow (Pf t) v getof :: Type (Lens c a) -> Pf (Lens c a) -> Pf (c -> a) getof (Lns _ _) (LNS s l) = FUN (showL ["get",s]) $ get l@@ -145,13 +181,13 @@ getof (Lns _ _) COASSOCR_LNS = COASSOCR getof (Lns _ _) INN_LNS = INN-getof (Lns (a@(Data _ fctr)::Type a) c) OUT_LNS = case teq c (rep fctr a) of- { Just Eq -> (OUT :: (Mu a,Functor (PF a)) => Pf (a -> F a a))+getof (Lns a@(dataFctr -> Just fctr) c) OUT_LNS = case teq c (rep fctr a) of+ { Just Eq -> OUT ; otherwise -> error "getof OUT" } getof (Lns _ _) (FMAP_LNS fctr (Fun c a) f) = FMAP fctr (Fun c a) $ getof (Lns c a) f-getof (Lns a b@(Data _ fctr)) (ANA_LNS f) = ANA $ getof (Lns a (rep fctr a)) f-getof (Lns a@(Data _ fctr) b) (CATA_LNS f) = CATA $ getof (Lns (rep fctr b) b) f-getof (Lns _ _) HOLE = HOLE+getof (Lns a b@(dataFctr -> Just fctr)) (ANA_LNS f) = ANA $ getof (Lns a (rep fctr a)) f+getof (Lns a@(dataFctr -> Just fctr) b) (CATA_LNS f) = CATA $ getof (Lns (rep fctr b) b) f+getof (Lns _ _) BOT = BOT getof _ f = GET f createof :: Type (Lens c a) -> Pf (Lens c a) -> Pf (a -> c)@@ -185,15 +221,18 @@ createof (Lns _ _) COASSOCR_LNS = COASSOCL createof (Lns _ _) INN_LNS = OUT-createof (Lns (a@(Data _ fctr)::Type a) c) OUT_LNS = case teq c (rep fctr a) of- { Just Eq -> (INN :: (Mu a,Functor (PF a)) => Pf (F a a -> a))+createof (Lns a@(dataFctr -> Just fctr) c) OUT_LNS = case teq c (rep fctr a) of+ { Just Eq -> INN ; otherwise -> error "createof OUT" } createof (Lns _ _) (FMAP_LNS fctr (Fun c a) f) = FMAP fctr (Fun a c) $ createof (Lns c a) f-createof (Lns a b@(Data _ fctr)) (ANA_LNS f) = CATA $ createof (Lns a (rep fctr a)) f-createof (Lns a@(Data _ fctr) b) (CATA_LNS f) = ANA $ createof (Lns (rep fctr b) b) f-createof (Lns _ _) HOLE = HOLE-createof _ f = CREATE f+createof (Lns a b@(dataFctr -> Just fctr)) (ANA_LNS f) = CATA $ createof (Lns a (rep fctr a)) f+createof (Lns a@(dataFctr -> Just fctr) b) (CATA_LNS f) = ANA $ createof (Lns (rep fctr b) b) f +createof (Lns (List a) (List b)) (MAP_LNS f) = MAP $ createof (Lns a b) f++createof (Lns _ _) BOT = BOT+createof t f = CREATE f+ putof :: Type (Lens c a) -> Pf (Lens c a) -> Pf ((a,c) -> c) putof (Lns _ _) (LNS s l) = FUN (showL ["put",s]) $ put l @@ -234,22 +273,22 @@ putof (Lns c a) COASSOCR_LNS = COMP a (createof (Lns c a) COASSOCR_LNS) FST putof (Lns c a) INN_LNS = COMP a OUT FST-putof (Lns (c@(Data _ fctr)::Type c) a) OUT_LNS = case teq a (rep fctr c) of- { Just Eq -> COMP (rep fctr c) (INN :: (Mu c,Functor (PF c)) => Pf (F c c -> c)) FST+putof (Lns c@(dataFctr -> Just fctr) a) OUT_LNS = case teq a (rep fctr c) of+ { Just Eq -> COMP (rep fctr c) INN FST ; otherwise -> error "putof OUT" } putof (Lns _ _) (FMAP_LNS fctr (Fun c a) f) = COMP (rep fctr (Prod a c)) (FMAP fctr (Fun (Prod a c) c) (putof (Lns c a) f)) $ FZIP fctr (Fun a c) (createof (Lns c a) f)-putof x@(Lns a b@(Data _ fctr)) (ANA_LNS f) = COMP (fixof kfctr) g h+putof x@(Lns a b@(dataFctr -> Just fctr)) (ANA_LNS f) = COMP (fixof kfctr) g h where g = CATA $ putof (Lns a (rep fctr a)) f h = ANA $ ((COMP t (FZIP fctr (Fun b a) $ createof x (ANA_LNS f)) (OUT ><= getof (Lns a (rep fctr a)) f)) /\= SND) kfctr = fctr :*!: K a t = Prod (rep fctr b) (rep fctr a)-putof x@(Lns b@(Data _ fctr) a) (CATA_LNS f) = ANA $ COMP t aux1 $ COMP t' aux2 (ID ><= OUT)+putof x@(Lns b@(dataFctr -> Just fctr) a) (CATA_LNS f) = ANA $ COMP t aux1 $ COMP t' aux2 (ID ><= OUT) where aux1 = FZIP fctr (Fun a b) $ createof x (CATA_LNS f) aux2 = COMP t'' (putof (Lns (rep fctr a) a) f) (ID ><= aux3) /\= SND aux3 = FMAP fctr (Fun b a) $ getof x (CATA_LNS f) t = Prod (rep fctr a) (rep fctr b) t' = Prod a (rep fctr b) t'' = Prod a (rep fctr a)-putof (Lns _ _) HOLE = HOLE+putof (Lns _ _) BOT = BOT putof (Lns _ _) f = PUT f
+ src/Data/Pf.hs view
@@ -0,0 +1,252 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.Pf+-- Copyright : (c) 2010 University of Minho+-- License : BSD3+--+-- Maintainer : hpacheco@di.uminho.pt+-- Stability : experimental+-- Portability : non-portable+--+-- Pointless Rewrite:+-- automatic transformation system for point-free programs+-- +-- Type-safe representation of point-free expressions at the value level.+--+-----------------------------------------------------------------------------++module Data.Pf where++-- * Representation of point-free expressions++import Data.Type++import Generics.Pointless.Combinators+import Generics.Pointless.Functors+import Generics.Pointless.Lenses++import Prelude hiding (Functor(..))+import Data.Monoid++data Pf a where+ + -- Variables and pointwise expressions+ VAR :: String -> Pf a+ FUN :: String -> (a -> b) -> Pf (a -> b)+ + -- Internal combinators+ BOT :: Pf a+ TOP :: Pf a+ CONV :: Either One One -> Pf (a -> b) -> Pf (b -> a)+ CONV_LNS :: Either One One -> Pf (Lens c a) -> Pf (Lens a c)+ LNS :: String -> Lens c a -> Pf (Lens c a)+ COMPF :: Functor f => Fctr f -> Type a -> Pf (Rep f a -> b) -> Pf (c -> Rep f a) -> Pf (c -> b)+ COMPF_LNS :: Functor f => Fctr f -> Type a -> Pf (Lens (Rep f a) b) -> Pf (Lens c (Rep f a)) -> Pf (Lens c b)+ -- Internal encapsulators+ PROTECT :: Pf (a -> b) -> Pf (a -> b)+ PROTECT_LNS :: Pf (Lens a b) -> Pf (Lens a b)+ + -- Non-recursive point-free combinators+ PNT :: a -> Pf (One -> a)+ BANG :: Pf (a -> One)+ COMP :: Type b -> Pf (b -> c) -> Pf (a -> b) -> Pf (a -> c)+ FST :: Pf ((a,b) -> a)+ SND :: Pf ((a,b) -> b)+ SPLIT :: Pf (a -> b) -> Pf (a -> c) -> Pf (a -> (b,c))+ PROD :: Pf (a -> c) -> Pf (b -> d) -> Pf ((a,b) -> (c,d))+ INL :: Pf (a -> Either a b)+ INR :: Pf (b -> Either a b)+ EITHER :: Pf (a -> c) -> Pf (b -> c) -> Pf (Either a b -> c)+ SUM :: Pf (a -> c) -> Pf (b -> d) -> Pf (Either a b -> Either c d)+ + MKDYN :: Type a -> Pf (a -> Dynamic)+ UNDYN :: Type a -> Pf (Dynamic -> a)+ CAST :: Type a -> Pf (b -> a)+ + -- Monoids+ ZERO :: Monoid b => Pf (a -> b)+ PLUS :: Monoid a => Pf ((a,a) -> a)+ FOLD :: Monoid a => Pf ([a] -> a)+ + -- Isomorphic point-free combinators+ ID :: Pf (c -> c)+ SWAP :: Pf ((a,b) -> (b,a))+ COSWAP :: Pf ((Either a b) -> (Either b a))+ DISTL :: Pf ((Either a b,c) -> (Either (a,c) (b,c)))+ UNDISTL :: Pf ((Either (a,c) (b,c)) -> (Either a b, c))+ DISTR :: Pf ((c, Either a b) -> (Either (c,a) (c,b)))+ UNDISTR :: Pf ((Either (c,a) (c,b)) -> (c,Either a b))+ ASSOCL :: Pf ((a,(b,c)) -> ((a,b),c))+ ASSOCR :: Pf (((a,b),c) -> (a,(b,c)))+ COASSOCL :: Pf ((Either a (Either b c)) -> (Either (Either a b) c))+ COASSOCR :: Pf ((Either (Either a b) c) -> (Either a (Either b c)))++ -- Recursive point-free combinators+ INN :: (Mu a,Functor (PF a)) => Pf (F a a -> a)+ OUT :: (Mu a,Functor (PF a)) => Pf (a -> F a a)+ FMAP :: Functor f => Fctr f -> Type (c -> a) -> Pf (c -> a) -> Pf (Rep f c -> Rep f a)+ FZIP :: Functor f => Fctr f -> Type (a -> c) -> Pf (a -> c) -> Pf ((Rep f a,Rep f c) -> Rep f (a,c))+ ANA :: (Mu b,Functor (PF b)) => Pf (a -> (F b a)) -> Pf (a -> b)+ CATA :: (Mu a,Functor (PF a)) => Pf (F a b -> b) -> Pf (a -> b)+ PARA :: (Mu a,Functor (PF a)) => Pf (F a (b,a) -> b) -> Pf (a -> b)+ + -- User-defined functions+ WRAP :: Pf (a -> [a])+ MAP :: Pf (a -> b) -> Pf ([a] -> [b])+ LHEAD :: Pf ([a] -> [a]) -- safe head+ LTAIL :: Pf ([a] -> [a]) -- safe tail+ NONEMPTY :: Pf ([a] -> Bool)+ LENGTH :: Pf ([a] -> Nat)+ ONE :: Pf (a -> Nat)+ + -- Lens Point-free functions+ GET :: Pf (Lens c a) -> Pf (c -> a)+ PUT :: Pf (Lens c a) -> Pf ((a,c) -> c)+ CREATE :: Pf (Lens c a) -> Pf (a -> c)+ + -- Non-recursive lenses+ COMP_LNS :: Type b -> Pf (Lens b a) -> Pf (Lens c b) -> Pf (Lens c a)+ FST_LNS :: Pf (a -> b) -> Pf (Lens (a,b) a)+ SND_LNS :: Pf (b -> a) -> Pf (Lens (a,b) b)+ PROD_LNS :: Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (c,d) (a,b))+ EITHER_LNS :: Pf (c -> Either One One) -> Pf (Lens a c) -> Pf (Lens b c) -> Pf (Lens (Either a b) c)+ SUM_LNS :: Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (Either c d) (Either a b))+ SUMW_LNS :: Pf ((a,d) -> c) -> Pf ((b,c) -> d) -> Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (Either c d) (Either a b))+ BANG_LNS :: Pf (One -> c) -> Pf (Lens c One)+ BANGL_LNS :: Pf (Lens c (One,c))+ BANGR_LNS :: Pf (Lens c (c,One))+ + -- Non-recursive isomorphisms+ ID_LNS :: Pf (Lens c c)+ SWAP_LNS :: Pf (Lens (a,b) (b,a))+ COSWAP_LNS :: Pf (Lens (Either a b) (Either b a))+ DISTL_LNS :: Pf (Lens (Either a b,c) (Either (a,c) (b,c)))+ UNDISTL_LNS :: Pf (Lens (Either (a,c) (b,c)) (Either a b,c))+ DISTR_LNS :: Pf (Lens (c, Either a b) (Either (c,a) (c,b)))+ UNDISTR_LNS :: Pf (Lens (Either (c,a) (c,b)) (c,Either a b))+ ASSOCL_LNS :: Pf (Lens (a,(b,c)) ((a,b),c))+ ASSOCR_LNS :: Pf (Lens ((a,b),c) (a,(b,c)))+ COASSOCL_LNS :: Pf (Lens (Either a (Either b c)) (Either (Either a b) c))+ COASSOCR_LNS :: Pf (Lens (Either (Either a b) c) (Either a (Either b c)))+ + -- Recursive lenses+ INN_LNS :: (Mu a,Functor (PF a)) => Pf (Lens (F a a) a)+ OUT_LNS :: (Mu a,Functor (PF a)) => Pf (Lens a (F a a))+ FMAP_LNS :: Functor f => Fctr f -> Type (c -> a) -> Pf (Lens c a) -> Pf (Lens (Rep f c) (Rep f a))+ ANA_LNS :: (Mu b,Functor (PF b)) => Pf (Lens a (F b a)) -> Pf (Lens a b)+ CATA_LNS :: (Mu a,Functor (PF a)) => Pf ((Lens (F a b) b)) -> Pf (Lens a b)+ + -- User-defined lenses+ MAP_LNS :: Pf (Lens a b) -> Pf (Lens [a] [b])+ LENGTH_LNS :: a -> Pf (Lens [a] Nat)+ FILTER_LEFT_LNS :: Pf (Lens [Either a b] [a])+ FILTER_RIGHT_LNS :: Pf (Lens [Either a b] [b])+ CAT_LNS :: Pf (Lens ([a],[a]) [a])+ CONCAT_LNS :: Pf (Lens [[a]] [a])+ SUMN_LNS :: Pf (Lens [Nat] Nat)+ PLUSN_LNS :: Pf (Lens (Nat,Nat) Nat)++ -- Type-preserving strategy combinators+ APPLY :: Type a -> Pf T -> Pf (a -> a)+ MKT :: Type a -> Pf (a -> a) -> Pf T+ NOP :: Pf T+ SEQ :: Pf T -> Pf T -> Pf T+ EXTT :: Pf T -> Type b -> Pf (b -> b) -> Pf T+ ALL :: Pf T -> Pf T+ EVERYWHERE :: Pf T -> Pf T -- bottom-up (catamorphism)+ EVERYWHERE' :: Pf T -> Pf T -- top-down (anamorphism)+ -- Type-unifying strategy combinators+ APPLYQ :: Type a -> Pf (Q r) -> Pf (a -> r)+ MKQ :: Monoid r => Type a -> Pf (a -> r) -> Pf (Q r)+ EMPTYQ :: Monoid r => Pf (Q r)+ UNION :: Monoid r => Pf (Q r) -> Pf (Q r) -> Pf (Q r)+ EXTQ :: Pf (Q r) -> Type a -> Pf (a -> r) -> Pf (Q r)+ GMAPQ :: Monoid r => Pf (Q r) -> Pf (Q r)+ EVERYTHING :: Monoid r => Pf (Q r) -> Pf (Q r) -- bottom-up, right-to-left (paramorphism)+ -- XPath-like strategic combinators+ SELF :: Pf (Q [Dynamic])+ ATT :: Pf (Q [Dynamic]) --auxiliary self attribute, only used for eval of attribute+ CHILD :: Pf (Q [Dynamic])+ ATTRIBUTE :: Pf (Q [Dynamic])+ DESCENDANT :: Pf (Q [Dynamic])+ DESCSELF :: Pf (Q [Dynamic])+ NAME :: String -> Pf (Q [Dynamic])+ (:/:) :: Monoid r => Pf (Q [Dynamic]) -> Pf (Q r) -> Pf (Q r)+ SEQQ :: Typeable r => Pf (Q r) -> Pf (r -> s) -> Pf (Q s)+ (:?:) :: Pf (Q [Dynamic]) -> Pf (Q Bool) -> Pf (Q [Dynamic])+ (:/\:) :: Pf (Q a) -> Pf (Q b) -> Pf (Q (a,b))++constPf :: a -> Pf (b -> a)+constPf v = COMP One (PNT v) BANG ++infix 5 ?=+(?=) :: Type a -> Pf (a -> Either One One) -> Pf (a -> Either a a)+(?=) a p = COMP (Either (Prod One a) (Prod One a)) (SND -|-= SND) $ COMP (Prod (Either One One) a) DISTL $ p /\= ID++infixr 9 .=+(.=) :: Typeable b => Pf (b -> a) -> Pf (c -> b) -> Pf (c -> a)+(.=) f g = COMP typeof f g++infix 6 /\=+(/\=) :: Pf (a -> b) -> Pf (a -> c) -> Pf (a -> (b,c))+(/\=) f g = SPLIT f g++infix 7 ><=+(><=) :: Pf (c -> a) -> Pf (d -> b) -> Pf ((c,d) -> (a,b))+(><=) f g = PROD f g++infix 4 \/=+(\/=) :: Pf (b -> a) -> Pf (c -> a) -> Pf (Either b c -> a)+(\/=) f g = EITHER f g++infix 5 -|-=+(-|-=) :: Pf (c -> a) -> Pf (d -> b) -> Pf ((Either c d) -> (Either a b))+(-|-=) f g = SUM f g++distp_pf :: Pf (((c,d),(a,b)) -> ((c,a),(d,b)))+distp_pf = FST ><= FST /\= SND ><= SND++dists_pf :: Type (Either a b,Either c d) -> Pf ((Either a b,Either c d) -> (Either (Either (a,c) (a,d)) (Either (b,c) (b,d))))+dists_pf (Prod (Either a b) (Either c d)) = COMP t (DISTR -|-= DISTR) DISTL+ where t = Either (Prod a (Either c d)) (Prod b (Either c d))++infixr 9 .<<+(.<<) :: Typeable b => Pf (Lens b a) -> Pf (Lens c b) -> Pf (Lens c a)+(.<<) f g = COMP_LNS typeof f g++infix 7 ><<<+(><<<) :: Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (c,d) (a,b))+(><<<) f g = PROD_LNS f g++infix 5 -|-<<+(-|-<<) :: Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (Either c d) (Either a b))+(-|-<<) f g = SUM_LNS f g++infix 4 \/<<+(\/<<) :: Pf (c -> Either One One) -> Pf (Lens a c) -> Pf (Lens b c) -> Pf (Lens (Either a b) c)+(\/<<) x f g = EITHER_LNS x f g++infix 4 .\/<<+(.\/<<) :: Pf (Lens a c) -> Pf (Lens b c) -> Pf (Lens (Either a b) c)+(.\/<<) f g = EITHER_LNS (COMP One INL BANG) f g++infix 4 \/.<<+(\/.<<) :: Pf (Lens a c) -> Pf (Lens b c) -> Pf (Lens (Either a b) c)+(\/.<<) f g = EITHER_LNS (COMP One INR BANG) f g+++dists_lns :: Type (Either a b,Either c d) -> Pf (Lens (Either a b,Either c d) (Either (Either (a,c) (a,d)) (Either (b,c) (b,d))))+dists_lns (Prod (Either a b) (Either c d)) = COMP_LNS t (DISTR_LNS -|-<< DISTR_LNS) DISTL_LNS+ where t = Either (Prod a (Either c d)) (Prod b (Either c d))++fmap_Lns :: (Functor f,Typeable (c -> a)) => Fctr f -> Pf (Lens c a) -> Pf (Lens (Rep f c) (Rep f a))+fmap_Lns fctr f = FMAP_LNS fctr typeof f++listzip :: Type a -> Type b -> Pf (([a],[b]) -> [(a,b)])+listzip a b = ANA $ COMP t3 (BANG `SUM` distp) $ COMP t2 COASSOCL $ COMP t1 dists $ OUT `PROD` OUT+ where distp = distp_pf+ dists = dists_pf t1+ (la,lb) = (List a,List b)+ t1 = Prod (Either One $ Prod a la) (Either One $ Prod b lb)+ t2 = Either (Either (Prod One One) (Prod One $ Prod b lb)) (Either (Prod (Prod a la) One) (Prod (Prod a la) (Prod b lb)))+ t3 = Either (Either (Either (Prod One One) (Prod One $ Prod b lb)) (Prod (Prod a la) One)) (Prod (Prod a la) (Prod b lb))
+ src/Data/Pf.hs-boot view
@@ -0,0 +1,3 @@+module Data.Pf where++data Pf a where
src/Data/Spine.hs view
@@ -18,10 +18,13 @@ module Data.Spine where import Data.Type+import Data.Pf+import {-# SOURCE #-} Data.Equal import Data.Monoid hiding (Any)+import Control.Monad.State -import Generics.Pointless.Functors+import Generics.Pointless.Functors hiding (rep) import Generics.Pointless.Combinators -- * A spine representation for data values à la SYB revolutions@@ -45,10 +48,64 @@ fromSpine (c `As` _) = c fromSpine (Ap f (_ :| a)) = (fromSpine f) a +showlst :: Type a -> [a] -> String+showlst a l = "[" ++ showlst' a l+showlst' :: Type a -> [a] -> String+showlst' a [] = "]"+showlst' a (x:xs) = gshow a x ++ "," ++ showlst' a xs+ -- | Converting from a value to a spine toSpine :: Type a -> a -> Spine a-toSpine Any x = x `As` (pcon "Any")-toSpine (Id a) x = x `As` (pcon "Id")+toSpine TypeRep Any = Any `As` (pcon "Any")+toSpine TypeRep (Var s) = Var s `As` (pcon $ showL ["Var",show s])+toSpine TypeRep (Id a) = Id `As` (pcon "Id")+ `Ap` (TypeRep :| a)+toSpine TypeRep Int = Int `As` (pcon "Int")+toSpine TypeRep Bool = Bool `As` (pcon "Bool")+toSpine TypeRep Char = Char `As` (pcon "Char")+toSpine TypeRep One = One `As` (pcon "One")+toSpine TypeRep (Either a b) = Either `As` (pcon "Either")+ `Ap` (TypeRep :| a)+ `Ap` (TypeRep :| b)+toSpine TypeRep (Prod a b) = Prod `As` (pcon "Prod")+ `Ap` (TypeRep :| a)+ `Ap` (TypeRep :| b)+toSpine TypeRep (Fun a b) = Fun `As` (pcon "Fun")+ `Ap` (TypeRep :| a)+ `Ap` (TypeRep :| b)+toSpine TypeRep (Lns a b) = Lns `As` (pcon "Lns")+ `Ap` (TypeRep :| a)+ `Ap` (TypeRep :| b)+toSpine TypeRep (Data s fctr) = Data s `As` (pcon $ "Data " ++ show s)+ `Ap` (FctrRep :| fctr)+toSpine TypeRep (NewData s fctr) = NewData s `As` (pcon $ "NewData " ++ show s)+ `Ap` (FctrRep :| fctr)+toSpine TypeRep (List a) = List `As` (pcon "List")+ `Ap` (TypeRep :| a)+toSpine TypeRep Dynamic = Dynamic `As` (pcon "Dynamic")+toSpine TypeRep (Pf a) = Pf `As` (pcon "Pf")+ `Ap` (TypeRep :| a)+toSpine TypeRep TP = TP `As` (pcon "TP")+toSpine TypeRep (TU a) = TU `As` (pcon "TU")+ `Ap` (TypeRep :| a)+toSpine FctrRep I = I `As` (pcon "I")+toSpine FctrRep L = L `As` (pcon "L")+toSpine FctrRep (K c) = K `As` (pcon "K")+ `Ap` (TypeRep :| c)+toSpine FctrRep (f :*!: g) = (:*!:) `As` (icon ":*!:")+ `Ap` (FctrRep :| f)+ `Ap` (FctrRep :| g)+toSpine FctrRep (f :+!: g) = (:+!:) `As` (icon ":+!:")+ `Ap` (FctrRep :| f)+ `Ap` (FctrRep :| g)+toSpine FctrRep (f :@!: g) = (:@!:) `As` (icon ":@!:")+ `Ap` (FctrRep :| f)+ `Ap` (FctrRep :| g)+toSpine FctrRep AnyF = AnyF `As` (pcon "AnyF")++toSpine Any x = x `As` (pcon "Any ")+toSpine (Var s) x = x `As` (pcon $ showL ["Var",show s])+toSpine (Id a) x = x `As` (pcon $ showL ["Id",gshow a x]) toSpine Int n = n `As` (scon n) toSpine Bool n = n `As` (scon n) toSpine Char n = n `As` (scon n)@@ -62,14 +119,28 @@ `Ap` (b :| y) toSpine (Fun a b) f = f `As` (pcon "Fun") toSpine (Lns c a) l = l `As` (pcon "Lns")-toSpine (a@(Data s fctr)) v = inn `As` (pcon $ "innT" ++ s)+toSpine (a@(Data s fctr)) v = inn `As` (pcon $ "inn" ++ s) `Ap` ((rep fctr a) :| out v)+toSpine (a@(NewData s fctr)) v = inn `As` (pcon $ "Inn" ++ s)+ `Ap` ((rep fctr a) :| out v)+toSpine (List Char) str = str `As` (pcon $ show str)+toSpine (List a) l = l `As` (pcon $ showlst a l) toSpine Dynamic (Dyn t x) = Dyn t `As` (pcon "Dyn") `Ap` (t :| x) toSpine TP x = x `As` (pcon "TP") toSpine (TU a) x = x `As` (pcon "TQ") -toSpine (Pf _) HOLE = HOLE `As` (pcon "_L")+toSpine (Pf (Fun c b)) (COMPF fctr a f g) = COMPF `As` (pcon "compf")+ `Ap` (FctrRep :| fctr)+ `Ap` (TypeRep :| a)+ `Ap` ((Pf (Fun (rep fctr a) b)) :| f)+ `Ap` ((Pf (Fun c (rep fctr a))) :| g)+toSpine (Pf (Lns c b)) (COMPF_LNS fctr a f g) = COMPF_LNS `As` (pcon "compf_lns")+ `Ap` (FctrRep :| fctr)+ `Ap` (TypeRep :| a)+ `Ap` ((Pf (Lns (rep fctr a) b)) :| f)+ `Ap` ((Pf (Lns c (rep fctr a))) :| g)+toSpine (Pf _) BOT = BOT `As` (pcon "_L") toSpine (Pf _) TOP = TOP `As` (pcon "T") toSpine (Pf (Fun _ _)) (FUN s f) = (FUN s f) `As` (pcon s) toSpine (Pf (Fun a c)) (CONV e@(Left _) f) = CONV e `As` (pcon "lconv")@@ -81,21 +152,17 @@ toSpine (Pf (Lns a c)) (CONV_LNS e@(Right _) f) = CONV_LNS e `As` (pcon "rconv") `Ap` (Pf (Lns c a) :| f) toSpine (Pf (Lns c a)) (LNS s l) = (LNS s l) `As` (pcon s)-toSpine (Pf (Fun c a)) (COMPF fctr b f g) = (COMPF fctr b) `As` (pcon $ "compf " ++ show fctr)- `Ap` (Pf (Fun (rep fctr b) a) :| f) - `Ap` (Pf (Fun c (rep fctr b)) :| g)-toSpine (Pf (Lns c a)) (COMPF_LNS fctr b f g) = (COMPF_LNS fctr b) `As` (pcon $ "compf_lns " ++ show fctr)- `Ap` (Pf (Lns (rep fctr b) a) :| f) - `Ap` (Pf (Lns c (rep fctr b)) :| g) toSpine (Pf (Fun a b)) (PROTECT f) = PROTECT `As` (pcon "protect") `Ap` (Pf (Fun a b) :| f) toSpine (Pf (Lns a b)) (PROTECT_LNS f) = PROTECT_LNS `As` (pcon "protect_lns") `Ap` (Pf (Lns a b) :| f) toSpine (Pf _) (VAR s) = VAR s `As` (pcon s) -toSpine (Pf (Fun a b)) (PNT vb) = PNT vb `As` (pcon $ showL ["pnt",gshow b vb])+toSpine (Pf (Fun a b)) (PNT vb) = PNT `As` (pcon "pnt")+ `Ap` (b :| vb) toSpine (Pf (Fun _ _)) BANG = BANG `As` (pcon "bang")-toSpine (Pf (Fun a c)) (COMP b f g) = COMP b `As` (icon ".")+toSpine (Pf (Fun a c)) (COMP b f g) = COMP `As` (icon ".")+ `Ap` (TypeRep :| b) `Ap` (Pf (Fun b c) :| f) `Ap` (Pf (Fun a b) :| g) toSpine (Pf (Fun _ _)) FST = FST `As` (pcon "fst")@@ -114,17 +181,20 @@ toSpine (Pf (Fun (Either a b) (Either c d))) (SUM f g) = SUM `As` (icon "-|-") `Ap` (Pf (Fun a c) :| f) `Ap` (Pf (Fun b d) :| g)+toSpine (Pf _) (MKDYN a) = MKDYN `As` (pcon "mkDyn")+ `Ap` (TypeRep :| a)+toSpine (Pf _) (UNDYN a) = UNDYN `As` (pcon "unDyn")+ `Ap` (TypeRep :| a)+toSpine (Pf _) (CAST a) = CAST `As` (pcon "cast")+ `Ap` (TypeRep :| a) toSpine (Pf func) ZERO = aux func where aux :: Monoid y => Type (x -> y) -> Spine (Pf (x -> y)) aux t@(Fun _ (Data "List" fctr)) = ZERO `As` pcon "nil" aux (Fun _ Int) = ZERO `As` pcon "const 0" aux _ = ZERO `As` pcon "mempty"-toSpine (Pf func) PLUS = aux func- where aux :: Monoid a => Type ((a,a) -> a) -> Spine (Pf ((a,a) -> a))- aux (Fun _ (Data "List" fctr)) = PLUS `As` pcon "(++)"- aux (Fun _ Int) = PLUS `As` pcon "(uncurry (+))"- aux _ = PLUS `As` pcon "mappend"+toSpine (Pf func) PLUS = PLUS `As` pcon "mappend"+toSpine (Pf func) (FOLD) = (FOLD `As` pcon "fold") toSpine (Pf (Fun _ _)) ID = ID `As` (pcon "id") toSpine (Pf (Fun _ _)) SWAP = SWAP `As` (pcon "swap") @@ -138,20 +208,33 @@ toSpine (Pf (Fun _ _)) COASSOCL = COASSOCL `As` (pcon "coassocl") toSpine (Pf (Fun _ _)) COASSOCR = COASSOCR `As` (pcon "coassocr") -toSpine (Pf (Fun _ a@(Data s _))) INN = INN `As` (pcon $ "inn" ++ s)-toSpine (Pf (Fun a@(Data s _) _)) OUT = OUT `As` (pcon $ "out" ++ s)-toSpine (Pf (Fun _ _)) (FMAP fctr (Fun a c) f) = FMAP fctr (Fun a c) `As` (pcon $ "fmap")+toSpine (Pf (Fun _ (List a))) INN = INN `As` (pcon $ "innList")+toSpine (Pf (Fun (List a) _)) OUT = OUT `As` (pcon $ "outList")+toSpine (Pf (Fun _ a@(dataName -> Just s))) INN = INN `As` (pcon $ "inn" ++ s)+toSpine (Pf (Fun a@(dataName -> Just s) _)) OUT = OUT `As` (pcon $ "out" ++ s)+toSpine (Pf (Fun _ _)) (FMAP fctr (Fun a c) f) = FMAP `As` (pcon "fmap")+ `Ap` (FctrRep :| fctr)+ `Ap` (TypeRep :| Fun a c) `Ap` (Pf (Fun a c) :| f)-toSpine (Pf (Fun _ _)) (FZIP fctr t f) = FZIP fctr t `As` (pcon $ "fzip")+toSpine (Pf (Fun _ _)) (FZIP fctr t f) = FZIP `As` (pcon "fzip")+ `Ap` (FctrRep :| fctr)+ `Ap` (TypeRep :| t) `Ap` (Pf t :| f)-toSpine (Pf (Fun a b@(Data s fctr))) (ANA f) = ANA `As` (pcon $ "ana" ++ s)+toSpine (Pf (Fun a b@(dataNameFctr -> Just (s,fctr)))) (ANA f) = ANA `As` (pcon $ "ana" ++ s) `Ap` (Pf (Fun a (rep fctr a)) :| f)-toSpine (Pf (Fun a@(Data s fctr) b)) (CATA f) = CATA `As` (pcon $ "cata" ++ s)+toSpine (Pf (Fun a@(dataNameFctr -> Just (s,fctr)) b)) (CATA f) = CATA `As` (pcon $ "cata" ++ s) `Ap` (Pf (Fun (rep fctr b) b) :| f)-toSpine (Pf func) (PARA f) = aux func f- where aux :: Type (a -> c) -> Pf (F a (c,a) -> c) -> Spine (Pf (a -> c))- aux (Fun a@(Data _ fctr) c) f = (PARA `As` pcon ("para")) `Ap` (Pf (Fun (rep fctr (Prod c a)) c) :| f)+toSpine (Pf (Fun a@(dataNameFctr -> Just (s,fctr)) c)) (PARA f) = PARA `As` (pcon $ "para" ++ s)+ `Ap` (Pf (Fun (rep fctr (Prod c a)) c) :| f) +toSpine (Pf _) WRAP = WRAP `As` (pcon "wrap")+toSpine (Pf (Fun (List a) (List b))) (MAP f) = MAP `As` (pcon "map")+ `Ap` (Pf (Fun a b) :| f)+toSpine (Pf _) LHEAD = LHEAD `As` (pcon "lhead")+toSpine (Pf _) LTAIL = LTAIL `As` (pcon "ltail")+toSpine (Pf _) LENGTH = LENGTH `As` (pcon "length")+toSpine (Pf _) ONE = ONE `As` (pcon "one")+ toSpine (Pf (Fun c a)) (GET l) = GET `As` (pcon "get") `Ap` (Pf (Lns c a) :| l) toSpine (Pf (Fun (Prod a c) _)) (PUT l) = PUT `As` (pcon "put")@@ -159,7 +242,8 @@ toSpine (Pf (Fun a c)) (CREATE l) = CREATE `As` (pcon "create") `Ap` (Pf (Lns c a) :| l) -toSpine (Pf (Lns c a)) (COMP_LNS b f g) = (COMP_LNS b) `As` (icon ".<")+toSpine (Pf (Lns c a)) (COMP_LNS b f g) = COMP_LNS `As` (icon ".< ")+ `Ap` (TypeRep :| b) `Ap` (Pf (Lns b a) :| f) `Ap` (Pf (Lns c b) :| g) toSpine (Pf (Lns (Prod a b) _)) (FST_LNS f) = FST_LNS `As` (pcon "fst_lns")@@ -198,54 +282,85 @@ toSpine (Pf (Lns _ _)) COASSOCL_LNS = COASSOCL_LNS `As` (pcon "coassocl_lns") toSpine (Pf (Lns _ _)) COASSOCR_LNS = COASSOCR_LNS `As` (pcon "coassocr_lns") -toSpine (Pf (Lns _ a@(Data s _))) INN_LNS = INN_LNS `As` (pcon $ "inn" ++ s ++ "_lns")-toSpine (Pf (Lns a@(Data s _) _)) OUT_LNS = OUT_LNS `As` (pcon $ "out" ++ s ++ "_lns")-toSpine (Pf (Lns _ _)) (FMAP_LNS fctr (Fun c a) (f)) = FMAP_LNS fctr (Fun c a) `As` (pcon $ "fmap_lns " ++ show fctr)+toSpine (Pf (Lns _ a@(dataName -> Just s))) INN_LNS = INN_LNS `As` (pcon $ "inn" ++ s ++ "_lns")+toSpine (Pf (Lns a@(dataName -> Just s) _)) OUT_LNS = OUT_LNS `As` (pcon $ "out" ++ s ++ "_lns")+toSpine (Pf (Lns _ _)) (FMAP_LNS fctr (Fun c a) (f)) = FMAP_LNS `As` (pcon "fmap_lns")+ `Ap` (FctrRep :| fctr)+ `Ap` (TypeRep :| Fun c a) `Ap` (Pf (Lns c a) :| f)-toSpine (Pf (Lns a b@(Data s fctr))) (ANA_LNS f) = ANA_LNS `As` (pcon $ "ana" ++ s ++ "_lns")+toSpine (Pf (Lns a b@(dataNameFctr -> Just (s,fctr)))) (ANA_LNS f) = ANA_LNS `As` (pcon $ "ana" ++ s ++ "_lns") `Ap` (Pf (Lns a (rep fctr a)) :| f)-toSpine (Pf (Lns a@(Data s fctr) b)) (CATA_LNS f) = CATA_LNS `As` (pcon $ "cata" ++ s ++ "_lns")+toSpine (Pf (Lns a@(dataNameFctr -> Just (s,fctr)) b)) (CATA_LNS f) = CATA_LNS `As` (pcon $ "cata" ++ s ++ "_lns") `Ap` (Pf (Lns (rep fctr b) b) :| f)-toSpine (Pf (Lns la lb)) (MAP_LNS f) = MAP_LNS `As` (pcon "map_lns")- `Ap` (Pf (Lns (unlist la) (unlist lb)) :| f)-toSpine (Pf (Lns la _)) (LENGTH_LNS v) = LENGTH_LNS v `As` (pcon $ showL["length_lns",gshow (unlist la) v])+toSpine (Pf (Lns (List a) (List b))) (MAP_LNS f) = MAP_LNS `As` (pcon "map_lns")+ `Ap` (Pf (Lns a b) :| f)+toSpine (Pf (Lns (List a) _)) (LENGTH_LNS v) = LENGTH_LNS `As` (pcon "length_lns")+ `Ap` (a :| v) toSpine (Pf (Lns _ _)) FILTER_LEFT_LNS = FILTER_LEFT_LNS `As` (pcon "filter_left_lns") toSpine (Pf (Lns _ _)) FILTER_RIGHT_LNS = FILTER_RIGHT_LNS `As` (pcon "filter_right_lns") toSpine (Pf (Lns _ _)) CAT_LNS = CAT_LNS `As` (pcon "cat_lns") toSpine (Pf (Lns _ _)) CONCAT_LNS = CONCAT_LNS `As` (pcon "concat_lns")-toSpine (Pf (Lns _ _)) SUML_LNS = SUML_LNS `As` (pcon "suml_lns")-toSpine (Pf (Lns _ _)) PLUS_LNS = PLUS_LNS `As` (pcon "plus_lns")+toSpine (Pf (Lns _ _)) SUMN_LNS = SUMN_LNS `As` (pcon "sumn_lns")+toSpine (Pf (Lns _ _)) PLUSN_LNS = PLUSN_LNS `As` (pcon "plus_lns") -toSpine (Pf _) (APPLY t f) = (APPLY t `As` pcon ("apT " ++ show t)) `Ap` (Pf TP :| f)-toSpine (Pf _) (MKT t f) = (MKT t `As` pcon ("mkT " ++ show t)) `Ap` (Pf (Fun t t) :| f)+toSpine (Pf _) (APPLY t f) = APPLY `As` (pcon "apT")+ `Ap` (TypeRep :| t)+ `Ap` (Pf TP :| f)+toSpine (Pf _) (MKT t f) = MKT `As` (pcon "mkT")+ `Ap` (TypeRep :| t)+ `Ap` (Pf (Fun t t) :| f) toSpine (Pf _) NOP = NOP `As` pcon "nop"-toSpine (Pf _) (SEQ f g) = (SEQ `As` pcon "seq") `Ap` (Pf TP :| f) `Ap` (Pf TP :| g)-toSpine (Pf _) (EXTT f t g) = ((\x y -> EXTT x t y) `As` pcon "extT") `Ap` (Pf TP :| f) `Ap` (Pf (Fun t t) :| g)+toSpine (Pf _) (SEQ f g) = (SEQ `As` pcon "seq")+ `Ap` (Pf TP :| f)+ `Ap` (Pf TP :| g)+toSpine (Pf _) (EXTT f t g) = EXTT `As` (pcon "extT")+ `Ap` (Pf TP :| f)+ `Ap` (TypeRep :| t)+ `Ap` (Pf (Fun t t) :| g) toSpine (Pf _) (ALL f) = (ALL `As` pcon "gmapT") `Ap` (Pf TP :| f) toSpine (Pf _) (EVERYWHERE f) = (EVERYWHERE `As` pcon "everywhere") `Ap` (Pf TP :| f) toSpine (Pf _) (EVERYWHERE' f) = (EVERYWHERE' `As` pcon "everywhere'") `Ap` (Pf TP :| f)-toSpine (Pf func) (APPLYQ t f) = aux func t f- where aux :: Type (a -> r) -> Type a -> Pf (Q r) -> Spine (Pf (a -> r))- aux (Fun _ r) t f = (APPLYQ t `As` pcon ("apQ " ++ show t)) `Ap` (Pf (TU r) :| f)-toSpine (Pf func) (MKQ t f) = aux func t f- where aux :: Monoid r => Type (Q r) -> Type a -> Pf (a -> r) -> Spine (Pf (Q r))- aux (TU r) t f = (MKQ t `As` pcon ("mkQ " ++ show t)) `Ap` (Pf (Fun t r) :| f)++toSpine (Pf (Fun _ r)) (APPLYQ t f) = APPLYQ `As` (pcon "apQ")+ `Ap` (TypeRep :| t)+ `Ap` (Pf (TU r) :| f)+toSpine (Pf (TU r)) (MKQ t f) = MKQ `As` (pcon "mkQ")+ `Ap` (TypeRep :| t)+ `Ap` (Pf (Fun t r) :| f) toSpine (Pf _) EMPTYQ = EMPTYQ `As` pcon "emptyQ"-toSpine (Pf r) (UNION f g) = (UNION `As` pcon "union") `Ap` (Pf r :| f) `Ap` (Pf r :| g)-toSpine (Pf func) (EXTQ f t g) = aux func f t g- where aux :: Type (Q r) -> Pf (Q r) -> Type a -> Pf (a -> r) -> Spine (Pf (Q r))- aux (TU r) f t g = ((\x y -> EXTQ x t y) `As` pcon "extQ") `Ap` (Pf (TU r) :| f) `Ap` (Pf (Fun t r) :| g)+toSpine (Pf r) (UNION f g) = (UNION `As` icon "`union`") `Ap` (Pf r :| f) `Ap` (Pf r :| g)+toSpine (Pf (TU r)) (EXTQ f t g) = EXTQ `As` (pcon "extQ")+ `Ap` (Pf (TU r) :| f)+ `Ap` (TypeRep :| t)+ `Ap` (Pf (Fun t r) :| g) toSpine (Pf r) (GMAPQ f) = (GMAPQ `As` pcon "gmapQ") `Ap` (Pf r :| f) toSpine (Pf r) (EVERYTHING f) = (EVERYTHING `As` pcon "everything") `Ap` (Pf r :| f) +toSpine (Pf r) SELF = SELF `As` pcon "self"+toSpine (Pf r) ATT = ATT `As` pcon "att"+toSpine (Pf r) CHILD = CHILD `As` pcon "child"+toSpine (Pf r) ATTRIBUTE = ATTRIBUTE `As` pcon "attribute"+toSpine (Pf r) DESCENDANT = DESCENDANT `As` pcon "desc"+toSpine (Pf r) DESCSELF = DESCSELF `As` pcon "descself"+toSpine (Pf r) (NAME s) = NAME s `As` (pcon $ showL["name",show s])+toSpine (Pf r) (f :/: g) = (:/:) `As` (icon "/")+ `Ap` (Pf (TU (List Dynamic)) :| f)+ `Ap` (Pf r :| g)+toSpine (Pf (TU s)) (SEQQ (q :: Pf (Q r)) f) = let r = typeof::Type r in (SEQQ `As` pcon "seqQ") `Ap` (Pf (TU r) :| q) `Ap` (Pf (Fun r s) :| f)+toSpine (Pf _) (f :?: p) = (((:?:) `As` Con {name="?", fixity=Infix}) `Ap` (Pf (TU (List Dynamic)) :| f)) `Ap` (Pf (TU Bool) :| p)+toSpine (Pf _) NONEMPTY = NONEMPTY `As` Con {name = "nonempty", fixity = Prefix}+toSpine (Pf (TU (Prod a b))) (f :/\: g) = (((:/\:) `As` Con {name ="/\\", fixity=Infix}) `Ap` (Pf (TU a) :| f)) `Ap` (Pf (TU b) :| g) toSpine (Pf (Fun Any Any)) e = e `As` (pcon "<anyfunc>") toSpine (Pf (Lns Any Any)) e = e `As` (pcon "<anylens>")-toSpine (Pf t) f = error $ "toSpine: " ++ show t ++ " " ++ safeShow f +toSpine (Pf t) f = error $ "toSpine undefined for " ++ show t+toSpine TypeRep t = error $ "toSpine TypeRep"+ instance Show (Type a) where show Any = "Any"- show (Id a) = showL["Id",show a]+ show (Var s) = showL["Var",show s]+ show (Id x) = showL ["Id",show x] show Int = "Int" show Bool = "Bool" show Char = "Char"@@ -254,15 +369,28 @@ show (Prod x y) = showL ["Prod",show x,show y] show (Fun x y) = showL ["Fun",show x,show y] show (Lns x y) = showL ["Lns",show x,show y]+ show (List a) = "[" ++ show a ++ "]" show (Data s f) = s+ show (NewData s f) = s+ show (Pf a) = showL ["Pf",show a] show (Dynamic) = "Dynamic" show TP = "TP" show (TU a) = showL ["TU",show a]- ++showData :: Type a -> String+showData (Data s fctr) = s ++ " = " ++ show fctr+showData (NewData s fctr) = "New" ++ s ++ " = " ++ show fctr+ instance Show Dynamic where- show (Dyn t v) = gshow t v+ show (Dyn t v) = showL ["Dynamic",gshow t v] +instance Show DynType where+ show (DynT t) = showL ["DynT",show t]++instance Show DynFctr where+ show (DynF f) = showL ["DynF",show f]+ instance Show (Fctr f) where show I = "Id" show (K t) = showL ["K",show t]@@ -270,15 +398,13 @@ show (f:*!:g) = showL [show f,":*:",show g] show (f:+!:g) = showL [show f,":+:",show g] show (f:@!:g) = showL [show f,":@:",show g]+ show AnyF = "AnyF" instance Typeable a => Show (Pf a) where show = gshow typeof gshow :: Type a -> a -> String-gshow (a@(Data s ((K One) :+!: ((K t) :*!: I)))) v = listify a t $ out v- where listify :: Type a -> Type c -> Either One (c,a) -> String- listify a c (Left _) = "[]"- listify a c (Right (x,xs)) = gshow c x ++ ":" ++ gshow a xs+gshow (isNat -> Just Eq) (Nat n) = showL ["Nat",show n] gshow Dynamic (Dyn t x) = gshow t x gshow (Pf t) f@(COMP _ _ _) = "(" ++ showComp (Pf t) f ++ ")" gshow (Pf t) f@(COMP_LNS _ _ _) = "(" ++ showComp (Pf t) f ++ ")"@@ -294,89 +420,3 @@ showComp (Pf (Fun a c)) (COMP b f g) = showComp (Pf $ Fun b c) f ++ " . " ++ showComp (Pf $ Fun a b) g showComp (Pf (Lns a c)) (COMP_LNS b f g) = showComp (Pf $ Lns b c) f ++ " .< " ++ showComp (Pf $ Lns a b) g showComp t f = gshow t f--safeShow :: Pf a -> String-safeShow HOLE = "_L"-safeShow TOP = "T"-safeShow (FUN s f) = s-safeShow (CONV e f) = showL ["conv",show e,safeShow f]-safeShow (CONV_LNS e f) = showL ["lconv",show e,safeShow f]-safeShow (LNS s l) = s-safeShow (COMPF fctr _ f g) = showL ["compf",show fctr,safeShow f,safeShow g]-safeShow (COMPF_LNS fctr _ f g) = showL ["compf_lns",show fctr,safeShow f,safeShow g]-safeShow (PROTECT f) = showL ["protect",safeShow f] -safeShow (PROTECT_LNS f) = showL ["protect_lns",safeShow f]-safeShow (VAR s) = s--safeShow (PNT v) = showL ["pnt"]-safeShow BANG = "bang"-safeShow (COMP _ f g) = showL [safeShow f,".",safeShow g]-safeShow FST = "fst"-safeShow SND = "snd"-safeShow (SPLIT f g) = showL [safeShow f,"/\\",safeShow g]-safeShow (PROD f g) = showL [safeShow f,"><",safeShow g]-safeShow INL = "inl"-safeShow INR = "inr"-safeShow (EITHER f g) = showL [safeShow f,"\\/",safeShow g]-safeShow (SUM f g) = showL [safeShow f,"-|-",safeShow g]--safeShow ID = "id"-safeShow SWAP = "swap" -safeShow COSWAP = "coswap" -safeShow DISTL = "distl"-safeShow UNDISTL = "undistl"-safeShow DISTR = "distr"-safeShow UNDISTR = "undistr"-safeShow ASSOCL = "assocl" -safeShow ASSOCR = "assocr"-safeShow COASSOCL = "coassocl"-safeShow COASSOCR = "coassocr"- -safeShow INN = "inn" -safeShow OUT = "out"-safeShow (FMAP _ _ f) = showL ["fmap",safeShow f]-safeShow (FZIP _ _ f) = showL ["fzip",safeShow f]-safeShow (ANA f) = showL ["ana",safeShow f]-safeShow (CATA f) = showL ["cata",safeShow f]--safeShow (GET f) = showL ["get",safeShow f]-safeShow (PUT f) = showL ["put",safeShow f] -safeShow (CREATE f) = showL ["create",safeShow f]--safeShow (COMP_LNS _ f g) = showL [safeShow f,".<",safeShow g]-safeShow (FST_LNS v) = showL ["fst_lns",safeShow v]-safeShow (SND_LNS v) = showL ["snd_lns",safeShow v] -safeShow (PROD_LNS f g) = showL [safeShow f,"><<",safeShow g]-safeShow (EITHER_LNS x f g) = showL [safeShow x,safeShow f,"\\/<",safeShow g]-safeShow (SUM_LNS f g) = showL [safeShow f,"-|-<",safeShow g] -safeShow (SUMW_LNS x y f g) = showL ["sum_lns",safeShow x,safeShow y,safeShow f,safeShow g] -safeShow (BANG_LNS v) = showL ["bang_lns",safeShow v]-safeShow (BANGL_LNS) = "bangl"-safeShow (BANGR_LNS) = "bangr"- -safeShow ID_LNS = "id_lns"-safeShow SWAP_LNS = "swap_lns"-safeShow COSWAP_LNS = "coswap_lns"-safeShow DISTL_LNS = "distl_lns"-safeShow UNDISTL_LNS = "undistl_lns"-safeShow DISTR_LNS = "distr_lns"-safeShow UNDISTR_LNS = "undistr_lns"-safeShow ASSOCL_LNS = "assocl_lns"-safeShow ASSOCR_LNS = "assocr_lns"-safeShow COASSOCL_LNS = "coassocl_lns"-safeShow COASSOCR_LNS = "coassocr_lns"- -safeShow INN_LNS = "inn_lns"-safeShow OUT_LNS = "out_lns"-safeShow (FMAP_LNS _ _ f) = showL ["fmap",safeShow f] -safeShow (ANA_LNS f) = showL ["ana_lns",safeShow f]-safeShow (CATA_LNS f) = showL ["cata_lns",safeShow f]--safeShow (MAP_LNS f) = showL ["map_lns",safeShow f]-safeShow (LENGTH_LNS f) = showL ["length_lns"] -safeShow FILTER_LEFT_LNS = "filter_left_lns"-safeShow FILTER_RIGHT_LNS = "filter_right_lns"-safeShow CAT_LNS = "cat_lns" -safeShow CONCAT_LNS = "concat_lns"-safeShow PLUS_LNS = "plus_lns"-safeShow (SUML_LNS) = "suml_lns"
src/Data/Type.hs view
@@ -11,7 +11,7 @@ -- Pointless Rewrite: -- automatic transformation system for point-free programs -- --- Type-safe representation of types and point-free expressions at the value level, including+-- Type-safe representation of types at the value level, including -- representation of recursive types as fixpoints of functors. -- -----------------------------------------------------------------------------@@ -19,19 +19,23 @@ module Data.Type where import Prelude hiding (Functor(..))-import Data.Monoid+import Data.Monoid hiding (Any)+import Data.Char+import Data.List +import {-# SOURCE #-} Data.Pf import Generics.Pointless.Combinators-import Generics.Pointless.Functors+import Generics.Pointless.Functors hiding (rep) import Generics.Pointless.Lenses+import Generics.Pointless.Lenses.Examples.Examples -- * Representation of types data Type a where -- Internal representations- Any :: Type a - -- INTERNAL: denotes explicit recursivity, needed in some computations where F a c and c \= a + Var :: String -> Type a+ Any :: Type a Id :: Type a -> Type a -- Non-recursive@@ -44,8 +48,12 @@ Fun :: Type a -> Type b -> Type (a -> b) Lns :: Type a -> Type b -> Type (Lens a b) + -- Built-in+ List :: Type a -> Type [a]+ -- Recursive Data :: (Mu a,Functor (PF a)) => String -> Fctr (PF a) -> Type a+ NewData :: Functor f => String -> Fctr f -> Type (Fix f) Pf :: Type a -> Type (Pf a) Dynamic :: Type Dynamic@@ -53,15 +61,102 @@ -- Types for SYB generic programming TP :: Type T TU :: Type a -> Type (Q a)+ TypeRep :: Type (Type a)+ FctrRep :: Type (Fctr f) +isData :: Type a -> Bool+isData (Data _ _) = True+isData (NewData _ _) = True+isData _ = False++isAtt :: Type a -> Bool+isAtt (dataName -> Just s) = isPrefixOf "@" s+isAtt _ = False++isOne :: Type a -> Bool+isOne One = True+isOne _ = False++isBasic :: Type a -> Bool+isBasic (List Char) = True+isBasic (Data "Nat" _) = True+isBasic Int = True+isBasic Bool = True+isBasic _ = False++-- | Selects the name and functor of a non-based type+dataNameFctr :: Type a -> Maybe (String,Fctr (PF a))+dataNameFctr a = do+ s <- dataName a+ f <- dataFctr a+ return (s,f)++refname :: String -> String+refname s = aux $ span (/= '\'') s+ where aux (x,[]) = x+ aux (x,'\'':y) = x ++ y++nodename :: String -> String+nodename = takeWhile (/= '\'')++-- | Checks if two name strings are equal modulo an arbitrary sufix+sameName :: String -> String -> Bool+sameName n n' = map toLower (takeWhile (/= '\'') n) == map toLower (takeWhile (/= '\'') n')++-- | Selects the name of a non-based type+dataName :: Type a -> Maybe String+dataName (Data s _) = Just s+dataName (NewData s _) = Just s+dataName (List a) = Just "List"+dataName _ = Nothing++-- | Selects the functor of a non-base type+dataFctr :: Type a -> Maybe (Fctr (PF a))+dataFctr (Data _ f) = Just f+dataFctr (NewData _ f) = Just f+dataFctr (List a) = Just $ listfctr a+dataFctr a = Nothing++instance Monoid Bool where+ mempty = False+ mappend = (||)++instance Monoid One where+ mempty = _L+ mappend _ _ = _L+ instance Monoid Int where mempty = 0 mappend = (+)- mconcat = foldr (+) 0 +instance Monoid Nat where+ mempty = nzero+ mappend = curry (get plus_lns)++-- | A generic type encapsulator. data Dynamic where Dyn :: Type a -> a -> Dynamic +-- Convert a regular type to a dynamic type.+mkDyn :: Type a -> a -> Dynamic+mkDyn a v = Dyn a v++-- Apply a generic function to a dynamically typed value.+applyDyn :: (forall a . Type a -> a -> b) -> Dynamic -> b+applyDyn f (Dyn ta a) = f ta a++data DynType where+ DynT :: Type a -> DynType++applyDynT :: (forall a . Type a -> b) -> DynType -> b+applyDynT f (DynT t) = f t++applyDynT2 :: (forall a b . Type a -> Type b -> c) -> DynType -> DynType -> c+applyDynT2 f (DynT a) (DynT b) = f a b++data DynFctr where+ DynF :: Functor f => Fctr f -> DynFctr+ newtype T = T {unT :: GenericT} type GenericT = forall a . Type a -> a -> a @@ -71,6 +166,9 @@ class Typeable a where typeof :: Type a +instance Typeable Dynamic where+ typeof = Dynamic+ instance Typeable Int where typeof = Int @@ -108,16 +206,13 @@ typeof = nat instance Typeable a => Typeable [a] where- typeof = list typeof+ typeof = List typeof nat :: Type Nat nat = Data "Nat" fctrof -list :: Type a -> Type [a]-list a = Data "List" $ K One :+!: (K a :*!: I)--unlist :: Type [a] -> Type a-unlist (Data "List" (K One :+!: (K a :*!: I))) = a+listfctr :: Type a -> Fctr (Const One :+: Const a :*: Id)+listfctr a = K One :+!: (K a :*!: I) instance Typeable a => Typeable (Maybe a) where typeof = Data "Maybe" fctrof@@ -134,14 +229,15 @@ (:*!:) :: (Functor f,Functor g) => Fctr f -> Fctr g -> Fctr (f :*: g) (:+!:) :: (Functor f,Functor g) => Fctr f -> Fctr g -> Fctr (f :+: g) (:@!:) :: (Functor f,Functor g) => Fctr f -> Fctr g -> Fctr (f :@: g)+ AnyF :: Fctr a rep :: Fctr f -> Type a -> Type (Rep f a) rep I a = a+rep L a = List a rep (K c) a = c rep (f:*!:g) a = Prod (rep f a) (rep g a) rep (f:+!:g) a = Either (rep f a) (rep g a) rep (f:@!:g) a = rep f (rep g a)-rep L a = list a -- | Class of representable functors. class (Functor f) => Fctrable (f :: * -> *) where@@ -160,11 +256,14 @@ fctrof = (:@!:) fctrof fctrof fixof :: (Functor f) => Fctr f -> Type (Fix f)-fixof f = Data "" f+fixof f = NewData "Fix" f -fixF :: Fctr f -> Fix f-fixF (_::Fctr f) = (_L :: Fix f)+annT :: Type a -> Ann a+annT (_::Type a) = ann +fixF :: Fctr f -> Ann (Fix f)+fixF (_::Fctr f) = ann+ fctrofF :: Fctrable f => Fix f -> Fctr f fctrofF (_::Fix f) = fctrof :: Fctr f @@ -172,180 +271,7 @@ showL [x] = x showL xs = "(" ++ init (Prelude.foldr (\a b -> a ++ " " ++ b) "" xs) ++ ")" --- * Representation of point-free expressions--data Pf a where- - -- Variables and pointwise expressions- VAR :: String -> Pf a- FUN :: String -> (a -> b) -> Pf (a -> b)- - -- Internal combinators- HOLE :: Pf a- TOP :: Pf a- CONV :: Either One One -> Pf (a -> b) -> Pf (b -> a)- CONV_LNS :: Either One One -> Pf (Lens c a) -> Pf (Lens a c)- LNS :: String -> Lens c a -> Pf (Lens c a)- COMPF :: Functor f => Fctr f -> Type a -> Pf (Rep f a -> b) -> Pf (c -> Rep f a) -> Pf (c -> b)- COMPF_LNS :: Functor f => Fctr f -> Type a -> Pf (Lens (Rep f a) b) -> Pf (Lens c (Rep f a)) -> Pf (Lens c b)- -- Internal encapsulators- PROTECT :: Pf (a -> b) -> Pf (a -> b)- PROTECT_LNS :: Pf (Lens a b) -> Pf (Lens a b)- - -- Non-recursive point-free combinators- PNT :: a -> Pf (One -> a)- BANG :: Pf (a -> One)- COMP :: Type b -> Pf (b -> c) -> Pf (a -> b) -> Pf (a -> c)- FST :: Pf ((a,b) -> a)- SND :: Pf ((a,b) -> b)- SPLIT :: Pf (a -> b) -> Pf (a -> c) -> Pf (a -> (b,c))- PROD :: Pf (a -> c) -> Pf (b -> d) -> Pf ((a,b) -> (c,d))- INL :: Pf (a -> Either a b)- INR :: Pf (b -> Either a b)- EITHER :: Pf (a -> c) -> Pf (b -> c) -> Pf (Either a b -> c)- SUM :: Pf (a -> c) -> Pf (b -> d) -> Pf (Either a b -> Either c d)- - -- Monoids- ZERO :: Monoid b => Pf (a -> b)- PLUS :: Monoid a => Pf ((a,a) -> a)- - -- Isomorphic point-free combinators- ID :: Pf (c -> c)- SWAP :: Pf ((a,b) -> (b,a))- COSWAP :: Pf ((Either a b) -> (Either b a))- DISTL :: Pf ((Either a b,c) -> (Either (a,c) (b,c)))- UNDISTL :: Pf ((Either (a,c) (b,c)) -> (Either a b, c))- DISTR :: Pf ((c, Either a b) -> (Either (c,a) (c,b)))- UNDISTR :: Pf ((Either (c,a) (c,b)) -> (c,Either a b))- ASSOCL :: Pf ((a,(b,c)) -> ((a,b),c))- ASSOCR :: Pf (((a,b),c) -> (a,(b,c)))- COASSOCL :: Pf ((Either a (Either b c)) -> (Either (Either a b) c))- COASSOCR :: Pf ((Either (Either a b) c) -> (Either a (Either b c)))-- -- Recursive point-free combinators- INN :: (Mu a,Functor (PF a)) => Pf (F a a -> a)- OUT :: (Mu a,Functor (PF a)) => Pf (a -> F a a)- FMAP :: Functor f => Fctr f -> Type (c -> a) -> Pf (c -> a) -> Pf (Rep f c -> Rep f a)- FZIP :: Functor f => Fctr f -> Type (a -> c) -> Pf (a -> c) -> Pf ((Rep f a,Rep f c) -> Rep f (a,c))- ANA :: (Mu b,Functor (PF b)) => Pf (a -> (F b a)) -> Pf (a -> b)- CATA :: (Mu a,Functor (PF a)) => Pf (F a b -> b) -> Pf (a -> b)- PARA :: (Mu a,Functor (PF a)) => Pf (F a (c,a) -> c) -> Pf (a -> c)- - -- Lens Point-free functions- GET :: Pf (Lens c a) -> Pf (c -> a)- PUT :: Pf (Lens c a) -> Pf ((a,c) -> c)- CREATE :: Pf (Lens c a) -> Pf (a -> c)- - -- Non-recursive lenses- COMP_LNS :: Type b -> Pf (Lens b a) -> Pf (Lens c b) -> Pf (Lens c a)- FST_LNS :: Pf (a -> b) -> Pf (Lens (a,b) a)- SND_LNS :: Pf (b -> a) -> Pf (Lens (a,b) b)- PROD_LNS :: Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (c,d) (a,b))- EITHER_LNS :: Pf (c -> Either One One) -> Pf (Lens a c) -> Pf (Lens b c) -> Pf (Lens (Either a b) c)- SUM_LNS :: Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (Either c d) (Either a b))- SUMW_LNS :: Pf ((a,d) -> c) -> Pf ((b,c) -> d) -> Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (Either c d) (Either a b))- BANG_LNS :: Pf (One -> c) -> Pf (Lens c One)- BANGL_LNS :: Pf (Lens c (One,c))- BANGR_LNS :: Pf (Lens c (c,One))- - -- Non-recursive isomorphisms- ID_LNS :: Pf (Lens c c)- SWAP_LNS :: Pf (Lens (a,b) (b,a))- COSWAP_LNS :: Pf (Lens (Either a b) (Either b a))- DISTL_LNS :: Pf (Lens (Either a b,c) (Either (a,c) (b,c)))- UNDISTL_LNS :: Pf (Lens (Either (a,c) (b,c)) (Either a b,c))- DISTR_LNS :: Pf (Lens (c, Either a b) (Either (c,a) (c,b)))- UNDISTR_LNS :: Pf (Lens (Either (c,a) (c,b)) (c,Either a b))- ASSOCL_LNS :: Pf (Lens (a,(b,c)) ((a,b),c))- ASSOCR_LNS :: Pf (Lens ((a,b),c) (a,(b,c)))- COASSOCL_LNS :: Pf (Lens (Either a (Either b c)) (Either (Either a b) c))- COASSOCR_LNS :: Pf (Lens (Either (Either a b) c) (Either a (Either b c)))- - -- Recursive lenses- INN_LNS :: (Mu a,Functor (PF a)) => Pf (Lens (F a a) a)- OUT_LNS :: (Mu a,Functor (PF a)) => Pf (Lens a (F a a))- FMAP_LNS :: Functor f => Fctr f -> Type (c -> a) -> Pf (Lens c a) -> Pf (Lens (Rep f c) (Rep f a))- ANA_LNS :: (Mu b,Functor (PF b)) => Pf (Lens a (F b a)) -> Pf (Lens a b)- CATA_LNS :: (Mu a,Functor (PF a)) => Pf ((Lens (F a b) b)) -> Pf (Lens a b)- - -- User-defined lenses- MAP_LNS :: Pf (Lens a b) -> Pf (Lens [a] [b])- LENGTH_LNS :: a -> Pf (Lens [a] Nat)- FILTER_LEFT_LNS :: Pf (Lens [Either a b] [a])- FILTER_RIGHT_LNS :: Pf (Lens [Either a b] [b])- CAT_LNS :: Pf (Lens ([a],[a]) [a])- CONCAT_LNS :: Pf (Lens [[a]] [a])- SUML_LNS :: Pf (Lens [Nat] Nat)- PLUS_LNS :: Pf (Lens (Nat,Nat) Nat)-- -- Type-preserving strategy combinators- APPLY :: Type a -> Pf T -> Pf (a -> a)- MKT :: Type a -> Pf (a -> a) -> Pf T- NOP :: Pf T- SEQ :: Pf T -> Pf T -> Pf T- EXTT :: Pf T -> Type b -> Pf (b -> b) -> Pf T- ALL :: Pf T -> Pf T- EVERYWHERE :: Pf T -> Pf T -- bottom-up (catamorphism)- EVERYWHERE' :: Pf T -> Pf T -- top-down (anamorphism)- -- Type-unifying strategy combinators- APPLYQ :: Type a -> Pf (Q r) -> Pf (a -> r)- MKQ :: Monoid r => Type a -> Pf (a -> r) -> Pf (Q r)- EMPTYQ :: Monoid r => Pf (Q r)- UNION :: Monoid r => Pf (Q r) -> Pf (Q r) -> Pf (Q r)- EXTQ :: Pf (Q r) -> Type a -> Pf (a -> r) -> Pf (Q r)- GMAPQ :: Monoid r => Pf (Q r) -> Pf (Q r)- EVERYTHING :: Monoid r => Pf (Q r) -> Pf (Q r) -- bottom-up, right-to-left (paramorphism)--infix 5 ?=-(?=) :: Type a -> Pf (a -> Either One One) -> Pf (a -> Either a a)-(?=) a p = COMP (Either (Prod One a) (Prod One a)) (SND -|-= SND) $ COMP (Prod (Either One One) a) DISTL $ p /\= ID--infixr 9 .=-(.=) :: Typeable b => Pf (b -> a) -> Pf (c -> b) -> Pf (c -> a)-(.=) f g = COMP typeof f g--infix 6 /\=-(/\=) :: Pf (a -> b) -> Pf (a -> c) -> Pf (a -> (b,c))-(/\=) f g = SPLIT f g--infix 7 ><=-(><=) :: Pf (c -> a) -> Pf (d -> b) -> Pf ((c,d) -> (a,b))-(><=) f g = PROD f g--infix 4 \/=-(\/=) :: Pf (b -> a) -> Pf (c -> a) -> Pf (Either b c -> a)-(\/=) f g = EITHER f g--infix 5 -|-=-(-|-=) :: Pf (c -> a) -> Pf (d -> b) -> Pf ((Either c d) -> (Either a b))-(-|-=) f g = SUM f g--distp_pf :: Pf (((c,d),(a,b)) -> ((c,a),(d,b)))-distp_pf = FST ><= FST /\= SND ><= SND--dists_pf :: Type (Either a b,Either c d) -> Pf ((Either a b,Either c d) -> (Either (Either (a,c) (a,d)) (Either (b,c) (b,d))))-dists_pf (Prod (Either a b) (Either c d)) = COMP t (DISTR -|-= DISTR) DISTL- where t = Either (Prod a (Either c d)) (Prod b (Either c d))--infixr 9 .<<-(.<<) :: Typeable b => Pf (Lens b a) -> Pf (Lens c b) -> Pf (Lens c a)-(.<<) f g = COMP_LNS typeof f g--infix 7 ><<<-(><<<) :: Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (c,d) (a,b))-(><<<) f g = PROD_LNS f g--infix 5 -|-<<-(-|-<<) :: Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (Either c d) (Either a b))-(-|-<<) f g = SUM_LNS f g--infix 4 \/<<-(\/<<) :: Pf (c -> Either One One) -> Pf (Lens a c) -> Pf (Lens b c) -> Pf (Lens (Either a b) c)-(\/<<) x f g = EITHER_LNS x f g--dists_lns :: Type (Either a b,Either c d) -> Pf (Lens (Either a b,Either c d) (Either (Either (a,c) (a,d)) (Either (b,c) (b,d))))-dists_lns (Prod (Either a b) (Either c d)) = COMP_LNS t (DISTR_LNS -|-<< DISTR_LNS) DISTL_LNS- where t = Either (Prod a (Either c d)) (Prod b (Either c d))--fmap_Lns :: (Functor f,Typeable (c -> a)) => Fctr f -> Pf (Lens c a) -> Pf (Lens (Rep f c) (Rep f a))-fmap_Lns fctr f = FMAP_LNS fctr typeof f+showLst :: [String] -> String+showLst [] = "[]"+showLst [x] = x+showLst xs = "[" ++ init (Prelude.foldr (\a b -> a ++ "," ++ b) "" xs) ++ "]"
src/Transform/Examples/Company.hs view
@@ -18,6 +18,7 @@ module Transform.Examples.Company where import Data.Type+import Data.Pf import Data.Eval import Transform.Rewriting import Transform.Rules.SYB
src/Transform/Examples/Imdb.hs view
@@ -18,6 +18,7 @@ module Transform.Examples.Imdb where import Data.Type+import Data.Pf import Data.Lens import Transform.Rewriting import Transform.Rules.Lenses@@ -51,7 +52,7 @@ t' = typeof :: Type [Either (((Year,Title),[Review]),(Director,Value)) (((Year,Title),[Review]),TV)] boxoffices :: Pf (Lens [BoxOffice] Value)-boxoffices = SUML_LNS .<< FILTER_RIGHT_LNS .<< MAP_LNS (OUT_LNS .<< SND_LNS (VAR "dcountry"))+boxoffices = SUMN_LNS .<< FILTER_RIGHT_LNS .<< MAP_LNS (OUT_LNS .<< SND_LNS (VAR "dcountry")) reviews :: Pf (Lens [Review] Nat) reviews = LENGTH_LNS "ccomment" .<< CONCAT_LNS .<< MAP_LNS (SND_LNS (VAR "duser"))
src/Transform/Examples/Women.hs view
@@ -18,6 +18,7 @@ module Transform.Examples.Women where import Data.Type+import Data.Pf import Data.Lens import Transform.Rewriting import Transform.Rules.Lenses
src/Transform/Rewriting.hs view
@@ -18,14 +18,14 @@ module Transform.Rewriting where import Data.Type+import Data.Pf import Data.Spine-import Data.Equal+import Data.Equal hiding (replace) import Data.List import Control.Monad import Control.Monad.RWS import Control.Monad.State-import Debug.Trace import System.IO import Generics.Pointless.Combinators@@ -60,14 +60,16 @@ replace l (b :| x) (a :| y) = do s <- aux (last l) (init l) (toSpine a y) return $ fromSpine s where aux :: MonadPlus m => Int -> Location -> Spine a -> m (Spine a)- aux 0 l (Ap f (a :| y)) = do z <- replace l (b :| x) (a :| y)- return $ Ap f (a :| z)- aux (n) l (Ap f (a :| y)) = do g <- aux (succ n) l f- return $ Ap g (a :| y)+ aux 0 l (Ap f (a :| y)) = do+ z <- replace l (b :| x) (a :| y)+ return $ Ap f (a :| z)+ aux n l (Ap f (a :| y)) = do+ g <- aux (pred n) l f+ return $ Ap g (a :| y) aux _ _ _ = mzero hole :: Type a -> a-hole (Pf _) = HOLE+hole (Pf _) = BOT puthole :: Location -> Dynamic -> Dynamic puthole l (Dyn t x) = Dyn t (xua l (t :| x))@@ -76,7 +78,7 @@ xua l (a :| y) = fromSpine $ aux (last l) (init l) (toSpine a y) aux :: Int -> Location -> Spine a -> Spine a aux 0 l (Ap f (a :| y)) = Ap f (a :| xua l (a :| y))- aux n l (Ap f (a :| y)) = Ap (aux (succ n) l f) (a :| y)+ aux n l (Ap f (a :| y)) = Ap (aux (pred n) l f) (a :| y) -- The basic type of rules type GenericM m = forall a . Type a -> Pf a -> m (Pf a)@@ -94,6 +96,7 @@ let g = fromSpine f y <- local down $ h t x return $ g y)+ aux h _ = mzero gmapMo' :: (MonadReader Location m, MonadPlus m) => GenericM m -> GenericM m gmapMo' h t y = aux h (toSpine (Pf t) y)@@ -106,6 +109,7 @@ `mplus` (do g <- local next $ aux h f return $ g x)+ aux h _ = mzero gmapM :: (MonadReader Location m, MonadPlus m) => GenericM m -> GenericM m gmapM h t y = aux h (toSpine (Pf t) y)@@ -162,6 +166,9 @@ outermost :: Rule -> Rule outermost r = try (many1 (once r)) +outermost1 :: Rule -> Rule+outermost1 r = many1 (once r)+ (>>>) :: Monad m => GenericM m -> GenericM m -> GenericM m (f >>> g) t x = f t x >>= g t @@ -195,12 +202,17 @@ printRule n t v = tell [(n,gshow Dynamic (Dyn t v))] debug :: String -> Type a -> a -> Rewrite ()-debug n t v = trace ("entering " ++ n ++ ": " ++ gshow t v) $ return ()+debug n t v = --trace ("entering " ++ n ++ ": " ++ gshow t v) $+ return () +debugT :: String -> Type a -> Rewrite ()+debugT n t = --trace ("entering " ++ n ++ ": " ++ show t) $+ return ()+ success :: String -> a -> Rewrite a success n x = do z@(Dyn t v) <- get- trace n $ printRule n t v+ --trace n $ printRule n t v return x context :: Rewrite (Typed Dynamic)@@ -227,10 +239,11 @@ reduceIO :: Rule -> Type a -> Pf a -> IO (Pf a) reduceIO s t x = do- let (l,r) = maybe (x,[]) id (evalRWST (s t x) [0] (Dyn (Pf t) x))- putStr $ gshow (Pf t) l- putStrLn ""+ putStrLn "Running optimizations..."+ let (l,r) = maybe (x,[]) id (evalRWST (s t x) [0] (Dyn (Pf t) x)) hPutRuleTree stdout r+ putStrLn ""+-- putStrLn $ gshow (Pf t) l return l writeIO :: FilePath -> Rule -> Type a -> Pf a -> IO (Pf a)
src/Transform/Rules/Lenses.hs view
@@ -18,16 +18,17 @@ module Transform.Rules.Lenses where import Data.Type+import Data.Pf import Data.Equal import Data.Lens import Transform.Rewriting+import {-# SOURCE #-} qualified Transform.Rules.PF as PF import Transform.Rules.Lenses.Combinators import Transform.Rules.Lenses.Products import Transform.Rules.Lenses.Sums import Transform.Rules.Lenses.Dists import Transform.Rules.Lenses.Rec import Transform.Rules.Lenses.Lists-import {-# SOURCE #-} qualified Transform.Rules.PF as PF import Prelude hiding (Functor(..)) import Control.Monad.RWS hiding (Functor(..))@@ -36,44 +37,23 @@ -- * Strategies +optimise_all_lns :: Rule+optimise_all_lns = optimise_lns >>> optimise_list_lns++optimise_list_lns :: Rule+optimise_list_lns = outermost listrules >>> optimise_lns >>> try (once listfuse >>> optimise_list_lns)+ where listrules, listfuse :: Rule+ listrules = top list_cata_cancel_lns ||| top list_ana_cancel_lns+ listfuse = top list_cata_fusion_lns ||| top list_ana_fusion_lns ||| list_hylo_fusion_lns+ optimise_lns :: Rule-optimise_lns = step1- where- step1, right, rules, prot, undef, prods, sums, bangs, dists, convs, recs, lists, fuse :: Rule- step1 = outermost (top comp_assocr_lns ||| rules) >>> right >>> try (once fuse >>> optimise_lns)- right = many (once (top comp_assocr_lns))- rules = top nat_id_lns ||| prot ||| undef ||| prods ||| sums ||| bangs ||| dists ||| convs ||| lists ||| recs- prot = top unprotect_lns- undef = top top_fusion_lns- prods = top prod_functor_id_lns ||| top prod_functor_comp_lns- ||| top fst_nat_lns ||| top snd_nat_lns- ||| top swap_nat_lns ||| top swap_iso_lns ||| top swap_cancel_lns- ||| top assocr_nat_lns ||| top assocr_iso_lns ||| top assocr_fst_cancel_lns ||| top assocr_snd_cancel_lns- ||| top assocl_nat_lns ||| top assocl_iso_lns ||| top assocl_fst_cancel_lns ||| top assocl_snd_cancel_lns- ||| top bangl_cancel_lns ||| top bangr_cancel_lns- sums = top sum_functor_id_lns ||| top sum_functor_comp_lns ||| top sum_absor_lns- ||| top sumw_functor_id_lns ||| top sumw_absor_lns- ||| top coswap_nat_lns ||| top coswap_iso_lns ||| top coswap_cancel_lns- ||| top coassocr_nat_lns ||| top coassocr_iso_lns ||| top coassocl_nat_lns ||| top coassocl_iso_lns- bangs = top bang_reflex_lns ||| top bang_fusion_lns ||| top bang_uniq_lns- dists = top distr_def_lns ||| top undistr_def_lns- ||| top distl_iso_lns ||| top undistl_iso_lns- ||| top distl_fst_cancel_lns ||| top distl_snd_cancel_lns ||| top distl_id_cancel_lns- convs = top rconv_cancel_lns ||| top lconv_cancel_lns ||| top conv_conv_lns ||| top conv_iso_lns- ||| top conv_comp_lns ||| top conv_prod_lns ||| top conv_sum_lns- recs = top in_iso_lns ||| top out_iso_lns- ||| top functor_id_lns ||| top functor_comp_lns ||| top functor_def_lns- ||| top cata_reflex_lns ||| top cata_cancel_lns- ||| top ana_reflex_lns ||| top ana_cancel_lns- lists = top map_id_lns ||| top map_fusion_lns ||| top map_cat_lns ||| top map_concat_lns- ||| top filter_cat_lns ||| top filter_map_lns ||| top filter_concat_lns- ||| top sum_cat_lns ||| top sum_concat_lns- ||| top length_cat_lns ||| top length_map_lns ||| top length_concat_lns- ||| top cata_map_fusion_lns ||| top ana_map_fusion_lns- fuse = top sum_fusion_lns ||| top distl_fusion_lns ||| top distl_nat_lns ||| top distl_sum_nat_lns- ||| top hylo_id_lns ||| top cata_fusion_lns ||| top ana_fusion_lns- ||| top hylo_shift_lns- ||| {-top sumw_def_lns ||| -}top sumw_functor_comp_lns+optimise_lns = outermost rules >>> try ((once fuse1 ||| once fuse2 ||| once fuse3 ||| once fuse4) >>> optimise_lns)+ where rules, fuse1, fuse2, fuse3, fuse4 :: Rule+ rules = primitives ||| prods ||| sums ||| lists ||| bangs ||| convs ||| dists ||| recs+ fuse1 = top cata_fusion_lns ||| top ana_fusion_lns+ fuse2 = top distl_fusion_lns ||| top distl_nat_lns ||| top distl_sum_nat_lns+ fuse3 = top hylo_id_lns ||| top hylo_shift_lns+ fuse4 = top sum_fusion_lns -- * Proofs
src/Transform/Rules/Lenses.hs-boot view
@@ -2,4 +2,6 @@ import Transform.Rewriting +optimise_all_lns :: Rule+optimise_list_lns :: Rule optimise_lns :: Rule
src/Transform/Rules/Lenses/Combinators.hs view
@@ -18,6 +18,7 @@ module Transform.Rules.Lenses.Combinators where import Data.Type+import Data.Pf import Data.Lens import Transform.Rewriting import {-# SOURCE #-} qualified Transform.Rules.PF as PF@@ -27,35 +28,6 @@ -- ** Combinators -protect_lns :: Rule -> Rule-protect_lns r (Lns c a) (PROTECT_LNS f) =- r (Lns c a) f-protect_lns r t f = r t f--unprotect_lns :: Rule-unprotect_lns (Lns c a) (PROTECT_LNS (CATA_LNS l1)) = mzero-unprotect_lns (Lns c a) (PROTECT_LNS (ANA_LNS l1)) = mzero-unprotect_lns (Lns c a) (PROTECT_LNS (MAP_LNS l1)) = mzero-unprotect_lns (Lns c a) (PROTECT_LNS (LENGTH_LNS _)) = mzero-unprotect_lns (Lns c a) (PROTECT_LNS (FILTER_LEFT_LNS)) = mzero-unprotect_lns (Lns c a) (PROTECT_LNS (FILTER_RIGHT_LNS)) = mzero-unprotect_lns (Lns c a) (PROTECT_LNS (CAT_LNS)) = mzero-unprotect_lns (Lns c a) (PROTECT_LNS (CONCAT_LNS)) = mzero-unprotect_lns (Lns c a) (PROTECT_LNS (SUML_LNS)) = mzero-unprotect_lns (Lns c a) (PROTECT_LNS (PLUS_LNS)) = mzero-unprotect_lns (Lns c a) (PROTECT_LNS (COMP_LNS b l1 l2)) =- return $ COMP_LNS b (PROTECT_LNS l1) (PROTECT_LNS l2)-unprotect_lns (Lns (Prod c d) (Prod a b)) (PROTECT_LNS (PROD_LNS l1 l2)) =- return $ PROD_LNS (PROTECT_LNS l1) (PROTECT_LNS l2)-unprotect_lns (Lns (Either c d) (Either a b)) (PROTECT_LNS (SUM_LNS l1 l2)) = do- return $ SUM_LNS (PROTECT_LNS l1) (PROTECT_LNS l2)-unprotect_lns (Lns (Either c d) (Either a b)) (PROTECT_LNS (SUMW_LNS f g l1 l2)) = do- return $ SUMW_LNS f g (PROTECT_LNS l1) (PROTECT_LNS l2)-unprotect_lns (Lns c a) (PROTECT_LNS l1) = do- debug "safeUnprotect" (Pf $ Lns c a) l1- return l1-unprotect_lns _ _ = mzero- -- | Applies a rule inside a composition comp_lns :: Rule -> Rule comp_lns r (Lns d a) (COMP_LNS b f (COMP_LNS c g h)) = do@@ -264,3 +236,9 @@ top_fusion_lns' (Lns _ _) (COMP_LNS _ f TOP) = success "top-Fusion-Lns" TOP top_fusion_lns' _ _ = mzero++primitives :: Rule+primitives = top comp_assocr_lns ||| top nat_id_lns ||| top top_fusion_lns++bangs :: Rule+bangs = top bang_reflex_lns ||| top bang_fusion_lns ||| top bang_uniq_lns
src/Transform/Rules/Lenses/Dists.hs view
@@ -18,6 +18,7 @@ module Transform.Rules.Lenses.Dists where import Data.Type+import Data.Pf import Data.Lens import Transform.Rewriting import Transform.Rules.Lenses.Combinators@@ -100,6 +101,8 @@ distl_nat_lns = postcomp_lns leftmost_prod_lns distl_nat_lns' distl_nat_lns' :: Rule distl_nat_lns' (Lns _ _) (COMP_LNS _ DISTL_LNS (ID_LNS `PROD_LNS` ID_LNS)) = mzero+--distl_nat_lns' (Lns a c) (COMP_LNS b DISTL_LNS (ID_LNS `PROD_LNS` f)) =+-- distl_nat_lns' (Lns a c) (COMP_LNS b DISTL_LNS ((ID_LNS `SUM_LNS` ID_LNS) `PROD_LNS` f)) distl_nat_lns' q@(Lns (Prod (Either a b) c) _) v@(COMP_LNS (Prod (Either a' b') c') DISTL_LNS ((SUM_LNS l1 l2) `PROD_LNS` l3)) = (do debug "distl-Nat-Lns" (Pf q) v inv (Lns c c') l3@@ -128,5 +131,8 @@ success "distl-Sum-Nat-Lns" $ COMP_LNS t DISTL_LNS $ COMP_LNS t' (EITHER_LNS p' (l1 ><<< l3) (l2 ><<< l3)) DISTL_LNS distl_sum_nat_lns' _ _ = mzero -+dists :: Rule+dists = top distr_def_lns ||| top undistr_def_lns+ ||| top distl_iso_lns ||| top undistl_iso_lns+ ||| top distl_fst_cancel_lns ||| top distl_snd_cancel_lns ||| top distl_id_cancel_lns
src/Transform/Rules/Lenses/Lists.hs view
@@ -18,6 +18,7 @@ module Transform.Rules.Lenses.Lists where import Data.Type+import Data.Pf import Data.Eval import Data.Lens import Transform.Rewriting@@ -38,14 +39,14 @@ map_fusion_lns = comp_lns map_fusion_lns' map_fusion_lns' :: Rule-map_fusion_lns' (Lns _ _) (COMP_LNS lc (MAP_LNS l1) (MAP_LNS l2)) =- success "map-Fusion-Lns" $ MAP_LNS $ COMP_LNS (unlist lc) l1 l2+map_fusion_lns' (Lns _ _) (COMP_LNS (List c) (MAP_LNS l1) (MAP_LNS l2)) =+ success "map-Fusion-Lns" $ MAP_LNS $ COMP_LNS c l1 l2 map_fusion_lns' _ _ = mzero leftmost_map_lns :: Rule-leftmost_map_lns (Lns (Data "List" (K One :+!: (K a :*!: I))) (Data "List" (K One :+!: (K b :*!: I)))) (MAP_LNS l1) = do+leftmost_map_lns (Lns (List a) (List b)) (MAP_LNS l1) = do (COMP_LNS c f g) <- leftmost_lns' (Lns a b) l1- return $ COMP_LNS (list c) (MAP_LNS f) (MAP_LNS g)+ return $ COMP_LNS (List c) (MAP_LNS f) (MAP_LNS g) leftmost_map_lns _ _ = mzero map_cat_lns = comp_lns map_cat_lns'@@ -57,7 +58,7 @@ map_concat_lns = comp_lns map_concat_lns' map_concat_lns' :: Rule map_concat_lns' (Lns _ lb) (COMP_LNS _ (MAP_LNS l1) CONCAT_LNS) =- success "map-Concat-Lns" $ COMP_LNS (list lb) CONCAT_LNS $ MAP_LNS $ MAP_LNS l1+ success "map-Concat-Lns" $ COMP_LNS (List lb) CONCAT_LNS $ MAP_LNS $ MAP_LNS l1 map_concat_lns' _ _ = mzero filter_cat_lns = comp_lns filter_cat_lns'@@ -70,83 +71,82 @@ filter_map_lns = postcomp_lns leftmost_map_lns filter_map_lns' filter_map_lns' :: Rule-filter_map_lns' (Lns (Data "List" (K One :+!: (K (Either a b) :*!: I))) _) (COMP_LNS _ FILTER_LEFT_LNS (MAP_LNS (l1 `SUM_LNS` l2))) = do- success "filter-Map-Lns" $ COMP_LNS (list a) (MAP_LNS l1) FILTER_LEFT_LNS-filter_map_lns' (Lns (Data "List" (K One :+!: (K (Either a b) :*!: I))) _) (COMP_LNS _ FILTER_LEFT_LNS (MAP_LNS (SUMW_LNS _ _ l1 l2))) = do- success "filter-Map-Lns" $ COMP_LNS (list a) (MAP_LNS l1) FILTER_LEFT_LNS-filter_map_lns' (Lns (Data "List" (K One :+!: (K (Either a b) :*!: I))) _) (COMP_LNS _ FILTER_RIGHT_LNS (MAP_LNS (l1 `SUM_LNS` l2))) = do- success "filter-Map-Lns" $ COMP_LNS (list b) (MAP_LNS l2) FILTER_RIGHT_LNS-filter_map_lns' (Lns (Data "List" (K One :+!: (K (Either a b) :*!: I))) _) (COMP_LNS _ FILTER_RIGHT_LNS (MAP_LNS (SUMW_LNS _ _ l1 l2))) = do- success "filter-Map-Lns" $ COMP_LNS (list b) (MAP_LNS l2) FILTER_RIGHT_LNS+filter_map_lns' (Lns (List (Either a b)) _) (COMP_LNS _ FILTER_LEFT_LNS (MAP_LNS (l1 `SUM_LNS` l2))) = do+ success "filter-Map-Lns" $ COMP_LNS (List a) (MAP_LNS l1) FILTER_LEFT_LNS+filter_map_lns' (Lns (List (Either a b)) _) (COMP_LNS _ FILTER_LEFT_LNS (MAP_LNS (SUMW_LNS _ _ l1 l2))) = do+ success "filter-Map-Lns" $ COMP_LNS (List a) (MAP_LNS l1) FILTER_LEFT_LNS+filter_map_lns' (Lns (List (Either a b)) _) (COMP_LNS _ FILTER_RIGHT_LNS (MAP_LNS (l1 `SUM_LNS` l2))) = do+ success "filter-Map-Lns" $ COMP_LNS (List b) (MAP_LNS l2) FILTER_RIGHT_LNS+filter_map_lns' (Lns (List (Either a b)) _) (COMP_LNS _ FILTER_RIGHT_LNS (MAP_LNS (SUMW_LNS _ _ l1 l2))) = do+ success "filter-Map-Lns" $ COMP_LNS (List b) (MAP_LNS l2) FILTER_RIGHT_LNS filter_map_lns' _ _ = mzero filter_concat_lns = comp_lns filter_concat_lns' filter_concat_lns' :: Rule filter_concat_lns' (Lns _ la) (COMP_LNS _ FILTER_LEFT_LNS CONCAT_LNS) =- success "filter-Concat-Lns" $ COMP_LNS (list la) CONCAT_LNS $ MAP_LNS FILTER_LEFT_LNS+ success "filter-Concat-Lns" $ COMP_LNS (List la) CONCAT_LNS $ MAP_LNS FILTER_LEFT_LNS filter_concat_lns' (Lns _ lb) (COMP_LNS _ FILTER_RIGHT_LNS CONCAT_LNS) =- success "filter-Concat-Lns" $ COMP_LNS (list lb) CONCAT_LNS $ MAP_LNS FILTER_RIGHT_LNS+ success "filter-Concat-Lns" $ COMP_LNS (List lb) CONCAT_LNS $ MAP_LNS FILTER_RIGHT_LNS filter_concat_lns' _ _ = mzero sum_cat_lns = comp_lns sum_cat_lns' sum_cat_lns' :: Rule-sum_cat_lns' (Lns _ _) (COMP_LNS _ SUML_LNS CAT_LNS) =- success "sum-Cat-Lns" $ COMP_LNS (Prod nat nat) PLUS_LNS (SUML_LNS ><<< SUML_LNS)+sum_cat_lns' (Lns _ _) (COMP_LNS _ SUMN_LNS CAT_LNS) =+ success "sum-Cat-Lns" $ COMP_LNS (Prod nat nat) PLUSN_LNS (SUMN_LNS ><<< SUMN_LNS) sum_cat_lns' _ _ = mzero sum_concat_lns = comp_lns sum_concat_lns' sum_concat_lns' :: Rule-sum_concat_lns' (Lns _ _) (COMP_LNS _ SUML_LNS CONCAT_LNS) =- success "sum-Concat-Lns" $ COMP_LNS (list nat) SUML_LNS (MAP_LNS SUML_LNS)+sum_concat_lns' (Lns _ _) (COMP_LNS _ SUMN_LNS CONCAT_LNS) =+ success "sum-Concat-Lns" $ COMP_LNS (List nat) SUMN_LNS (MAP_LNS SUMN_LNS) sum_concat_lns' _ _ = mzero length_cat_lns = comp_lns length_cat_lns' length_cat_lns' :: Rule length_cat_lns' (Lns _ _) (COMP_LNS _ (LENGTH_LNS f) CAT_LNS) =- success "length-Cat-Lns" $ COMP_LNS (Prod nat nat) PLUS_LNS $ LENGTH_LNS f ><<< LENGTH_LNS f+ success "length-Cat-Lns" $ COMP_LNS (Prod nat nat) PLUSN_LNS $ LENGTH_LNS f ><<< LENGTH_LNS f length_cat_lns' _ _ = mzero length_map_lns = comp_lns length_map_lns' length_map_lns' :: Rule-length_map_lns' t@(Lns la _) v@(COMP_LNS lb (LENGTH_LNS va) (MAP_LNS l1)) = do+length_map_lns' t@(Lns la@(List a) _) v@(COMP_LNS lb@(List b) (LENGTH_LNS va) (MAP_LNS l1)) = do debug "length-Map-Lns" (Pf t) v- let (a,b) = (unlist la,unlist lb)- va' = (eval (Fun b a) (createof (Lns a b) l1)) va+ let va' = (eval (Fun b a) (createof (Lns a b) l1)) va success "length-Map-Lns" $ LENGTH_LNS va' length_map_lns' _ _ = mzero length_concat_lns = comp_lns length_concat_lns' length_concat_lns' :: Rule length_concat_lns' (Lns _ _) (COMP_LNS _ (LENGTH_LNS f) CONCAT_LNS) =- success "length-Concat-Lns" $ COMP_LNS (list nat) SUML_LNS $ MAP_LNS $ LENGTH_LNS f+ success "length-Concat-Lns" $ COMP_LNS (List nat) SUMN_LNS $ MAP_LNS $ LENGTH_LNS f length_concat_lns' _ _ = mzero cata_map_fusion_lns = comp_lns cata_map_fusion_lns' cata_map_fusion_lns' :: Rule-cata_map_fusion_lns' (Lns la c) (COMP_LNS lb (CATA_LNS l1) (MAP_LNS l2)) =- success "cata-Map-Fusion-Lns" $ CATA_LNS $ COMP_LNS (Either One (Prod (unlist lb) c)) l1 $ ID_LNS -|-<< l2 ><<< ID_LNS+cata_map_fusion_lns' (Lns la c) (COMP_LNS lb@(List b) (CATA_LNS l1) (MAP_LNS l2)) =+ success "cata-Map-Fusion-Lns" $ CATA_LNS $ COMP_LNS (Either One (Prod b c)) l1 $ ID_LNS -|-<< l2 ><<< ID_LNS cata_map_fusion_lns' _ _ = mzero ana_map_fusion_lns = comp_lns ana_map_fusion_lns' ana_map_fusion_lns' :: Rule-ana_map_fusion_lns' (Lns a lc) (COMP_LNS lb (MAP_LNS l2) (ANA_LNS l1)) =- success "ana-Map-Fusion-Lns" $ ANA_LNS $ COMP_LNS (Either One (Prod (unlist lb) a)) (ID_LNS -|-<< l2 ><<< ID_LNS) l1+ana_map_fusion_lns' (Lns a lc) (COMP_LNS lb@(List b) (MAP_LNS l2) (ANA_LNS l1)) =+ success "ana-Map-Fusion-Lns" $ ANA_LNS $ COMP_LNS (Either One (Prod b a)) (ID_LNS -|-<< l2 ><<< ID_LNS) l1 ana_map_fusion_lns' _ _ = mzero -- ** Definitions list_defs_lns :: Rule-list_defs_lns = list_catas_lns ||| list_anas_lns ||| list_hylos_lns+list_defs_lns = list_catas_defs_lns ||| list_anas_defs_lns ||| list_hylos_defs_lns -list_catas_lns :: Rule-list_catas_lns = map_cata_def_lns ||| length_cata_def_lns- ||| concat_def_lns ||| sum_def_lns ||| filter_def_lns+list_catas_defs_lns :: Rule+list_catas_defs_lns = top map_cata_def_lns ||| top length_cata_def_lns+ ||| top concat_def_lns ||| top sum_def_lns ||| top filter_def_lns -list_anas_lns :: Rule-list_anas_lns = map_ana_def_lns ||| length_ana_def_lns+list_anas_defs_lns :: Rule+list_anas_defs_lns = top map_ana_def_lns ||| top length_ana_def_lns -list_hylos_lns :: Rule-list_hylos_lns = plus_def_lns ||| cat_def_lns+list_hylos_defs_lns :: Rule+list_hylos_defs_lns = top plus_def_lns ||| top cat_def_lns inle :: Type a -> Type b -> Pf (Lens (Either a (Either a b)) (Either a b)) inle a b = COMP_LNS (Either (Either a a) b) ((EITHER_LNS (COMP One INL BANG) ID_LNS ID_LNS) -|-<< ID_LNS) COASSOCL_LNS@@ -155,22 +155,22 @@ inre a b = COMP_LNS (Either a (Either b b)) (ID_LNS -|-<< (EITHER_LNS (COMP One INR BANG) ID_LNS ID_LNS)) COASSOCR_LNS map_cata_def_lns :: Rule-map_cata_def_lns (Lns _ lb) (MAP_LNS l1) =- success "map-Cata-Def-Lns" $ CATA_LNS $ COMP_LNS (Either One (Prod (unlist lb) lb)) INN_LNS (ID_LNS -|-<< l1 ><<< ID_LNS)+map_cata_def_lns (Lns _ lb@(List b)) (MAP_LNS l1) =+ success "map-Cata-Def-Lns" $ CATA_LNS $ COMP_LNS (Either One (Prod b lb)) INN_LNS (ID_LNS -|-<< l1 ><<< ID_LNS) map_cata_def_lns _ _ = mzero map_ana_def_lns :: Rule-map_ana_def_lns (Lns la _) (MAP_LNS l1) =- success "map-Ana-Def-Lns" $ ANA_LNS $ COMP_LNS (Either One (Prod (unlist la) la)) (ID_LNS -|-<< l1 ><<< ID_LNS) OUT_LNS+map_ana_def_lns (Lns la@(List a) _) (MAP_LNS l1) =+ success "map-Ana-Def-Lns" $ ANA_LNS $ COMP_LNS (Either One (Prod a la)) (ID_LNS -|-<< l1 ><<< ID_LNS) OUT_LNS map_ana_def_lns _ _ = mzero filter_def_lns :: Rule-filter_def_lns (Lns (Data "List" (K One :+!: (K (Either a b) :*!: I))) la) FILTER_LEFT_LNS = do+filter_def_lns (Lns (List (Either a b)) la) FILTER_LEFT_LNS = do let e = (\/<<) (COMP One INL BANG) INN_LNS (SND_LNS TOP) t = Either (Either One (Prod a la)) (Prod b la) t' = Either One (Either (Prod a la) (Prod b la)) success "filter-Def-Lns" $ CATA_LNS $ COMP_LNS t e $ COMP_LNS t' COASSOCL_LNS (ID_LNS -|-<< DISTL_LNS)-filter_def_lns (Lns (Data "List" (K One :+!: (K (Either a b) :*!: I))) lb) FILTER_RIGHT_LNS = do+filter_def_lns (Lns (List (Either a b)) lb) FILTER_RIGHT_LNS = do let e = (\/<<) (COMP One INL BANG) INN_LNS (SND_LNS TOP) t = Either (Either One (Prod b lb)) (Prod a lb) t' = Either One (Either (Prod b lb) (Prod a lb))@@ -185,15 +185,14 @@ length_cata_def_lns _ _ = mzero length_ana_def_lns :: Rule-length_ana_def_lns (Lns la _) (LENGTH_LNS v) = do+length_ana_def_lns (Lns la@(List a) _) (LENGTH_LNS v) = do let f = COMP One (PNT v) BANG- success "length-Ana-Def-Lns" $ ANA_LNS $ COMP_LNS (Either One (Prod (unlist la) la)) (ID_LNS -|-<< SND_LNS f) OUT_LNS+ success "length-Ana-Def-Lns" $ ANA_LNS $ COMP_LNS (Either One (Prod a la)) (ID_LNS -|-<< SND_LNS f) OUT_LNS length_ana_def_lns _ _ = mzero cat_def_lns :: Rule-cat_def_lns (Lns _ la) CAT_LNS = do- let a = unlist la- t = Prod (Either One (Prod a la)) la+cat_def_lns (Lns _ la@(List a)) CAT_LNS = do+ let t = Prod (Either One (Prod a la)) la t' = Either (Prod One la) (Prod (Prod a la) la) t'' = Either (Either One (Prod a la)) (Prod a la) t''' = Either One (Prod a la)@@ -204,14 +203,13 @@ cat_def_lns _ _ = mzero concat_def_lns :: Rule-concat_def_lns (Lns _ la) CONCAT_LNS = do- let a = unlist la- aux = COMP_LNS (Either One (Either One (Prod a la))) (inle One (Prod a la)) (ID_LNS -|-<< (COMP_LNS la OUT_LNS CAT_LNS))+concat_def_lns (Lns _ la@(List a)) CONCAT_LNS = do+ let aux = COMP_LNS (Either One (Either One (Prod a la))) (inle One (Prod a la)) (ID_LNS -|-<< (COMP_LNS la OUT_LNS CAT_LNS)) success "concat-Def-Lns" $ CATA_LNS $ COMP_LNS (Either One (Prod a la)) INN_LNS aux concat_def_lns _ _ = mzero plus_def_lns :: Rule-plus_def_lns (Lns _ _) PLUS_LNS = do+plus_def_lns (Lns _ _) PLUSN_LNS = do let t = Prod (Either One nat) nat t' = Either (Prod One nat) (Prod nat nat) t'' = Either (Either One nat) nat@@ -222,9 +220,16 @@ plus_def_lns _ _ = mzero sum_def_lns :: Rule-sum_def_lns (Lns _ _) SUML_LNS = do+sum_def_lns (Lns _ _) SUMN_LNS = do let t = Either One (Either One nat)- aux = COMP_LNS t (inle One nat) (ID_LNS -|-<< (COMP_LNS nat OUT_LNS PLUS_LNS))+ aux = COMP_LNS t (inle One nat) (ID_LNS -|-<< (COMP_LNS nat OUT_LNS PLUSN_LNS)) success "sum-Def-Lns" $ CATA_LNS $ COMP_LNS (Either One nat) INN_LNS aux sum_def_lns _ _ = mzero++lists :: Rule+lists = top map_id_lns ||| top map_fusion_lns+ ||| top map_cat_lns ||| top map_concat_lns+ ||| top filter_cat_lns ||| top filter_map_lns ||| top filter_concat_lns+ ||| top sum_cat_lns ||| top sum_concat_lns+ ||| top length_cat_lns ||| top length_map_lns ||| top length_concat_lns
src/Transform/Rules/Lenses/Products.hs view
@@ -18,6 +18,7 @@ module Transform.Rules.Lenses.Products where import Data.Type+import Data.Pf import Data.Lens import Data.Equal import Transform.Rewriting@@ -167,3 +168,10 @@ let g = COMP b f FST success "assocl-Snd-Cancel-Lns" $ SND_LNS g assocl_snd_cancel_lns' _ _ = mzero++prods :: Rule+prods = top prod_functor_id_lns ||| top prod_functor_comp_lns+ ||| top fst_nat_lns ||| top snd_nat_lns ||| top bangl_cancel_lns ||| top bangr_cancel_lns+ ||| top swap_nat_lns ||| top swap_iso_lns ||| top swap_cancel_lns+ ||| top assocr_nat_lns ||| top assocr_iso_lns ||| top assocr_fst_cancel_lns ||| top assocr_snd_cancel_lns+ ||| top assocl_nat_lns ||| top assocl_iso_lns ||| top assocl_fst_cancel_lns ||| assocl_snd_cancel_lns
src/Transform/Rules/Lenses/Rec.hs view
@@ -18,21 +18,22 @@ module Transform.Rules.Lenses.Rec where import Data.Type+import Data.Pf import Data.Spine import Data.Lens import Data.Equal import Transform.Rewriting-import Transform.Rules.Lenses.Combinators-import Transform.Rules.Lenses.Lists import qualified Transform.Rules.PF as PF import {-# SOURCE #-} Transform.Rules.Lenses+import Transform.Rules.Lenses.Combinators+import Transform.Rules.Lenses.Lists import Prelude hiding (Functor(..)) import Control.Monad hiding (Functor(..)) import Unsafe.Coerce import Generics.Pointless.Combinators-import Generics.Pointless.Functors+import Generics.Pointless.Functors hiding (rep) import Generics.Pointless.Lenses -- ** In / Out@@ -66,72 +67,71 @@ success "functor-Comp-Lns" $ FMAP_LNS fctr (Fun a c) $ COMP_LNS b f g functor_comp_lns' _ _ = mzero -functor_def_lns :: Rule-functor_def_lns (Lns _ _) (FMAP_LNS I _ f) =- success "functor-Def-Lns" f-functor_def_lns (Lns _ _) (FMAP_LNS (K _) _ f) = - success "functor-Def-Lns" ID_LNS-functor_def_lns (Lns _ _) (FMAP_LNS (g:*!:h) t@(Fun c a) f) = do- l <- functor_def_lns (Lns (rep g c) (rep g a)) (FMAP_LNS g t f)- r <- functor_def_lns (Lns (rep h c) (rep h a)) (FMAP_LNS h t f)- success "functor-Def-Lns" $ l `PROD_LNS` r-functor_def_lns (Lns _ _) (FMAP_LNS (g:+!:h) t@(Fun c a) f) = do- l <- functor_def_lns (Lns (rep g c) (rep g a)) (FMAP_LNS g t f)- r <- functor_def_lns (Lns (rep h c) (rep h a)) (FMAP_LNS h t f)- success "functor-Def-Lns" $ l `SUM_LNS` r-functor_def_lns (Lns _ _) (FMAP_LNS (g:@!:h) t@(Fun c a) f) = do+functor_def_lns, functor_def_lns' :: Rule+functor_def_lns a x = functor_def_lns' a x >>= success "functor-Def-Lns"+functor_def_lns' (Lns _ _) (FMAP_LNS I _ f) =+ return f+functor_def_lns' (Lns _ _) (FMAP_LNS L _ f) =+ return $ MAP_LNS f+functor_def_lns' (Lns _ _) (FMAP_LNS (K _) _ f) = + return $ ID_LNS+functor_def_lns' (Lns _ _) (FMAP_LNS (g:*!:h) t@(Fun c a) f) = do+ l <- functor_def_lns' (Lns (rep g c) (rep g a)) (FMAP_LNS g t f)+ r <- functor_def_lns' (Lns (rep h c) (rep h a)) (FMAP_LNS h t f)+ return $ l `PROD_LNS` r+functor_def_lns' (Lns _ _) (FMAP_LNS (g:+!:h) t@(Fun c a) f) = do+ l <- functor_def_lns' (Lns (rep g c) (rep g a)) (FMAP_LNS g t f)+ r <- functor_def_lns' (Lns (rep h c) (rep h a)) (FMAP_LNS h t f)+ return $ l `SUM_LNS` r+functor_def_lns' (Lns _ _) (FMAP_LNS (g:@!:h) t@(Fun c a) f) = do let (hc,ha) = (rep h c,rep h a)- r <- functor_def_lns (Lns hc ha) (FMAP_LNS h t f)- l <- functor_def_lns (Lns (rep g hc) (rep g ha)) (FMAP_LNS g (Fun hc ha) r)- success "functor-Def-Lns" l-functor_def_lns _ _ = mzero+ r <- functor_def_lns' (Lns hc ha) (FMAP_LNS h t f)+ l <- functor_def_lns' (Lns (rep g hc) (rep g ha)) (FMAP_LNS g (Fun hc ha) r)+ return l+functor_def_lns' _ _ = mzero -- ** Catas +cata_def_lns :: Rule+cata_def_lns (Lns a@(dataFctr -> Just fctr) b) (CATA_LNS g) = do+ guard (not $ isRec fctr)+ Eq <- teq (rep fctr a) (rep fctr b)+ success "cata-Def-Lns" $ COMP_LNS (rep fctr a) g OUT_LNS+cata_def_lns _ _ = mzero+ cata_reflex_lns :: Rule cata_reflex_lns (Lns a b) (CATA_LNS INN_LNS) = do Eq <- teq a b success "cata-Reflex-Lns" ID_LNS cata_reflex_lns _ _ = mzero -list_cata_cancel = try $ protect_lns list_catas_lns cata_cancel_lns = comp_lns cata_cancel_lns' cata_cancel_lns' :: Rule-cata_cancel_lns' (Lns _ b) (COMP_LNS a@(Data _ fctr) f INN_LNS) = do- CATA_LNS g <- list_cata_cancel (Lns a b) f- let fb = rep fctr b- success "cata-Cancel-Lns" $ COMP_LNS fb g $ FMAP_LNS fctr (Fun a b) f-cata_cancel_lns' (Lns _ b) (COMP_LNS a@(Data _ fctr) (PROTECT_LNS f) INN_LNS) = do- CATA_LNS g <- list_cata_cancel (Lns a b) f- let fb = rep fctr b- success "cata-Cancel-Lns" $ COMP_LNS fb g $ FMAP_LNS fctr (Fun a b) (PROTECT_LNS f)-cata_cancel_lns' (Lns _ b) (COMP_LNS a@(Data _ fctr) (ANA_LNS g) INN_LNS) = do- CATA_LNS g' <- ana_shift_lns (Lns a b) (ANA_LNS g)- let fb = rep fctr b- success "cata-Cancel-Lns" $ COMP_LNS fb g' $ FMAP_LNS fctr (Fun a b) (ANA_LNS g)-cata_cancel_lns' (Lns _ b) (COMP_LNS a@(Data _ fctr) (PROTECT_LNS (ANA_LNS g)) INN_LNS) = do- CATA_LNS g' <- ana_shift_lns (Lns a b) (ANA_LNS g)+cata_cancel_lns' (Lns fa b) (COMP_LNS a (ANA_LNS g) INN_LNS) = do+ cata <- ana_shift_lns (Lns a b) (ANA_LNS g)+ cata_cancel_lns' (Lns fa b) (COMP_LNS a cata INN_LNS)+cata_cancel_lns' (Lns _ b) (COMP_LNS a@(dataFctr -> Just fctr) (CATA_LNS f) INN_LNS) = do let fb = rep fctr b- success "cata-Cancel-Lns" $ COMP_LNS fb g' $ FMAP_LNS fctr (Fun a b) $ PROTECT_LNS (ANA_LNS g)+ success "cata-Cancel-Lns" $ COMP_LNS fb f $ FMAP_LNS fctr (Fun a b) (CATA_LNS f) cata_cancel_lns' _ _ = mzero -list_cata_fusion = (comp2_lns list_catas_lns >>> cata_fusion_lns') ||| postcomp_lns list_hylos_lns cata_fusion_lns'-cata_fusion_lns = precomp_lns (rightmost_prod_lns ||| rightmost_sum_lns) list_cata_fusion-cata_fusion_lns' :: Rule-cata_fusion_lns' (Lns _ _) (COMP_LNS _ OUT_LNS (CATA_LNS g)) = mzero-cata_fusion_lns' t@(Lns c@(Data _ fctr) a) v@(COMP_LNS b f (CATA_LNS g)) = do++cata_fusion_lns = precomp_lns (rightmost_prod_lns ||| rightmost_sum_lns) (cata_fusion_lns' optimise_lns)+--cata_fusion_lns = comp_lns (cata_fusion_lns' optimise_lns)+cata_fusion_lns' :: Rule -> Rule+cata_fusion_lns' r (Lns _ _) (COMP_LNS _ OUT_LNS (CATA_LNS g)) = mzero+cata_fusion_lns' r t@(Lns c@(dataFctr -> Just fctr) a) v@(COMP_LNS b f (CATA_LNS g)) = do debug "cata-Fusion-Lns" (Pf t) v let (fa,fb) = (rep fctr a,rep fctr b)- prot = PROTECT_LNS f- h' = COMP_LNS b prot $ COMP_LNS fb g $ FMAP_LNS fctr (Fun a b) (CONV_LNS (Right _L) f)- h <- optimise_lns (Lns fa a) h'+ h' = COMP_LNS b f $ COMP_LNS fb g $ FMAP_LNS fctr (Fun a b) (rconv_lns f)+ h <- r (Lns fa a) h' debug "cataRes" (Pf $ Lns fa a) h- guard $ not $ find (Pf (Lns Any Any)) (CONV_LNS (Right _L) TOP) (Pf (Lns fa a)) h+ guard $ not $ find (Pf (Lns Any Any)) (rconv_lns TOP) (Pf (Lns fa a)) h success "cata-Fusion-Lns" $ CATA_LNS h-cata_fusion_lns' _ _ = mzero+cata_fusion_lns' _ _ _ = mzero cata_shift_lns :: Rule-cata_shift_lns t@(Lns a@(Data _ f) b@(Data _ g)) v@(CATA_LNS (COMP_LNS gb INN_LNS eta)) = do+cata_shift_lns t@(Lns a@(dataFctr -> Just f) b@(dataFctr -> Just g)) v@(CATA_LNS (COMP_LNS gb INN_LNS eta)) = do debug "cata-Shift-Lns" (Pf t) v Eq <- teq (rep g b) gb eta' <- natCoerce_lns f g b eta a@@ -141,54 +141,45 @@ -- ** Anas +ana_def_lns :: Rule+ana_def_lns (Lns a b@(dataFctr -> Just fctr)) (ANA_LNS g) = do+ guard (not $ isRec fctr)+ Eq <- teq (rep fctr b) (rep fctr a)+ success "ana-Def-Lns" $ COMP_LNS (rep fctr b) INN_LNS g+ana_def_lns _ _ = mzero+ ana_reflex_lns :: Rule ana_reflex_lns (Lns a b) (ANA_LNS OUT_LNS) = do Eq <- teq a b success "ana-Reflex-Lns" ID_LNS ana_reflex_lns _ _ = mzero -list_ana_cancel = try $ protect_lns list_anas_lns ana_cancel_lns = comp_lns ana_cancel_lns' ana_cancel_lns' :: Rule-ana_cancel_lns' (Lns b fa) (COMP_LNS a@(Data _ fctr) OUT_LNS g) = do- ANA_LNS h <- list_ana_cancel (Lns b a) g- Eq <- teq fa (rep fctr a)- let fb = rep fctr b- success "ana-Cancel-Lns" $ COMP_LNS fb (FMAP_LNS fctr (Fun b a) g) h-ana_cancel_lns' (Lns b fa) (COMP_LNS a@(Data _ fctr) OUT_LNS (PROTECT_LNS g)) = do- ANA_LNS h <- list_ana_cancel (Lns b a) g- Eq <- teq fa (rep fctr a)- let fb = rep fctr b- success "ana-Cancel-Lns" $ COMP_LNS fb (FMAP_LNS fctr (Fun b a) (PROTECT_LNS g)) h-ana_cancel_lns' (Lns b fa) (COMP_LNS a@(Data _ fctr) OUT_LNS (CATA_LNS h)) = do- ANA_LNS h' <- cata_shift_lns (Lns b a) (CATA_LNS h)- Eq <- teq fa (rep fctr a)- let fb = rep fctr b- success "ana-Cancel-Lns" $ COMP_LNS fb (FMAP_LNS fctr (Fun b a) (PROTECT_LNS (CATA_LNS h))) h'-ana_cancel_lns' (Lns b fa) (COMP_LNS a@(Data _ fctr) OUT_LNS (CATA_LNS h)) = do- ANA_LNS h' <- cata_shift_lns (Lns b a) (CATA_LNS h)- Eq <- teq fa (rep fctr a)+ana_cancel_lns' (Lns b fa) (COMP_LNS a OUT_LNS (CATA_LNS h)) = do+ ana <- cata_shift_lns (Lns b a) (CATA_LNS h)+ ana_cancel_lns' (Lns b fa) (COMP_LNS a OUT_LNS ana)+ana_cancel_lns' (Lns b fa) (COMP_LNS a@(dataFctr -> Just fctr) OUT_LNS (ANA_LNS f)) = do let fb = rep fctr b- success "ana-Cancel-Lns" $ COMP_LNS fb (FMAP_LNS fctr (Fun b a) (PROTECT_LNS (CATA_LNS h))) h'+ success "ana-Cancel-Lns" $ COMP_LNS fb (FMAP_LNS fctr (Fun b a) (ANA_LNS f)) f ana_cancel_lns' _ _ = mzero -list_ana_fusion = (comp1_lns list_anas_lns >>> ana_fusion_lns') ||| precomp_lns list_hylos_lns ana_fusion_lns'-ana_fusion_lns = postcomp_lns (leftmost_prod_lns ||| leftmost_sum_lns) list_ana_fusion-ana_fusion_lns' :: Rule-ana_fusion_lns' (Lns _ _) (COMP_LNS _ (ANA_LNS f) INN_LNS) = mzero-ana_fusion_lns' t@(Lns a c@(Data _ fctr)) v@(COMP_LNS b (ANA_LNS g) f) = do+ana_fusion_lns = postcomp_lns (leftmost_prod_lns ||| leftmost_sum_lns) (ana_fusion_lns' optimise_lns)+--ana_fusion_lns = comp_lns (ana_fusion_lns' optimise_lns)+ana_fusion_lns' :: Rule -> Rule+ana_fusion_lns' r (Lns _ _) (COMP_LNS _ (ANA_LNS f) INN_LNS) = mzero+ana_fusion_lns' r t@(Lns a c@(dataFctr -> Just fctr)) v@(COMP_LNS b (ANA_LNS g) f) = do debug "ana-Fusion-Lns" (Pf t) v let (fa,fb) = (rep fctr a,rep fctr b)- prot = PROTECT_LNS f- h' = COMP_LNS fb (FMAP_LNS fctr (Fun b a) (CONV_LNS (Left _L) f)) $ COMP_LNS b g prot- h <- optimise_lns (Lns a fa) h'+ h' = COMP_LNS fb (FMAP_LNS fctr (Fun b a) (lconv_lns f)) $ COMP_LNS b g f+ h <- r (Lns a fa) h' debug "anaRes" (Pf $ Lns a fa) h- guard $ not $ find (Pf (Lns Any Any)) (CONV_LNS (Left _L) TOP) (Pf (Lns a fa)) h+ guard $ not $ find (Pf (Lns Any Any)) (lconv_lns TOP) (Pf (Lns a fa)) h success "ana-Fusion-Lns" $ ANA_LNS h-ana_fusion_lns' _ _ = mzero+ana_fusion_lns' _ _ _ = mzero ana_shift_lns :: Rule-ana_shift_lns t@(Lns a@(Data _ f) b@(Data _ g)) v@(ANA_LNS (COMP_LNS fa eta OUT_LNS)) = do+ana_shift_lns t@(Lns a@(dataFctr -> Just f) b@(dataFctr -> Just g)) v@(ANA_LNS (COMP_LNS fa eta OUT_LNS)) = do debug "ana-Shift-Lns" (Pf t) v Eq <- teq (rep f a) fa eta' <- natCoerce_lns f g a eta b@@ -211,7 +202,7 @@ hylo_id_lns = comp_lns hylo_id_lns' hylo_id_lns' :: Rule-hylo_id_lns' t@(Lns c a) v@(COMP_LNS b@(Data _ fctr) (CATA_LNS g) (ANA_LNS h)) = do+hylo_id_lns' t@(Lns c a) v@(COMP_LNS b@(dataFctr -> Just fctr) (CATA_LNS g) (ANA_LNS h)) = do Eq <- teq c a debug "hylo-Id-Lns" (Pf t) v ID_LNS <- optimise_lns (Lns c a) (COMP_LNS (rep fctr c) g h)@@ -225,8 +216,8 @@ natProof_lns f g a eta = proof optimise_lns t eq1 eq2 where eq1 = COMP_LNS (rep f a) eta fmapf eq2 = COMP_LNS (rep g a) fmapg eta- fmapf = FMAP_LNS f (Fun a a) HOLE- fmapg = FMAP_LNS g (Fun a a) HOLE+ fmapf = FMAP_LNS f (Fun a a) BOT+ fmapg = FMAP_LNS g (Fun a a) BOT t = Lns (rep f a) (rep g a) -- ^ We need to prove this property in order to identify natural transformations, since we cannot know such from the types. @@ -314,9 +305,11 @@ -- Id and unrecognized cases match here natSplit_lns a b fctr f = mzero - -- ** Internal converses for fusion rules +rconv_lns = CONV_LNS (Right _L)+lconv_lns = CONV_LNS (Left _L)+ -- | f . fº = id rconv_cancel_lns = comp_lns rconv_cancel_lns' rconv_cancel_lns' :: Rule@@ -357,11 +350,10 @@ success "conv-Conv-Lns" f conv_conv_lns _ _ = mzero -conv_iso_lns :: Rule-conv_iso_lns (Lns a c) (CONV_LNS _ f) = do- f' <- inv (Lns c a) f- success "conv-Iso-Lns" f'-conv_iso_lns _ _ = mzero+conv_id_lns :: Rule+conv_id_lns (Lns a c) (CONV_LNS _ ID_LNS) = do+ success "conv-Iso-Lns" ID_LNS+conv_id_lns _ _ = mzero conv_prod_lns :: Rule conv_prod_lns _ (CONV_LNS e (PROD_LNS f g)) =@@ -372,3 +364,46 @@ conv_sum_lns _ (CONV_LNS e (SUM_LNS f g)) = success "conv-Sum-Lns" $ SUM_LNS (CONV_LNS e f) (CONV_LNS e g) conv_sum_lns _ _ = mzero++convs :: Rule+convs = top rconv_cancel_lns ||| top lconv_cancel_lns+ ||| top conv_comp_lns ||| top conv_conv_lns ||| top conv_id_lns+ ||| top conv_prod_lns ||| top conv_sum_lns++recs :: Rule+recs = top in_iso_lns ||| top out_iso_lns+ ||| top functor_id_lns ||| top functor_comp_lns ||| top functor_def_lns+ ||| top cata_def_lns ||| top cata_reflex_lns ||| top cata_cancel_lns+ ||| top ana_def_lns ||| top ana_reflex_lns ||| top ana_cancel_lns++-- ** Lists++list_ana_cancel_lns, list_ana_cancel_lns' :: Rule+list_ana_cancel_lns = comp_lns list_ana_cancel_lns'+list_ana_cancel_lns' (Lns b fa) (COMP_LNS a@(dataFctr -> Just fctr) OUT_LNS ana) = do+ ANA_LNS g <- list_anas_defs_lns (Lns b a) ana+ success "list-ana-Cancel-Lns" $ COMP_LNS (rep fctr b) (FMAP_LNS fctr (Fun b a) ana) g+list_ana_cancel_lns' _ _ = mzero++list_ana_fusion_lns :: Rule+list_ana_fusion_lns = postcomp_lns (leftmost_prod_lns ||| leftmost_sum_lns) $+ comp1_lns list_anas_defs_lns >>> (ana_fusion_lns' optimise_all_lns)++list_cata_cancel_lns, list_cata_cancel_lns' :: Rule+list_cata_cancel_lns = comp_lns list_cata_cancel_lns'+list_cata_cancel_lns' (Lns fa b) (COMP_LNS a@(dataFctr -> Just fctr) cata INN_LNS) = do+ CATA_LNS f <- list_catas_defs_lns (Lns a b) cata+ success "list-cata-Cancel-Lns" $ COMP_LNS (rep fctr b) f $ FMAP_LNS fctr (Fun a b) cata+list_cata_cancel_lns' _ _ = mzero++list_cata_fusion_lns :: Rule+list_cata_fusion_lns = precomp_lns (rightmost_prod_lns ||| rightmost_sum_lns) $+ comp2_lns list_catas_defs_lns >>> (cata_fusion_lns' optimise_all_lns)++list_hylo_fusion_lns :: Rule+list_hylo_fusion_lns =+ (postcomp_lns (leftmost_prod_lns ||| leftmost_sum_lns) $ precomp_lns list_hylos_defs_lns (ana_fusion_lns' optimise_all_lns))+ ||| (precomp_lns (rightmost_prod_lns ||| rightmost_sum_lns) $ postcomp_lns list_hylos_defs_lns (cata_fusion_lns' optimise_all_lns))+++
src/Transform/Rules/Lenses/Sums.hs view
@@ -18,6 +18,7 @@ module Transform.Rules.Lenses.Sums where import Data.Type+import Data.Pf import Data.Lens import Transform.Rewriting import Transform.Rules.Lenses.Combinators@@ -56,13 +57,13 @@ -- ** Lifted sum combinators -{-sumw_def_lns :: Rule+sumw_def_lns :: Rule sumw_def_lns t@(Lns (Either c d) (Either a b)) v@(SUMW_LNS f g l1 l2) = do debug "sumw-Def-Lns" (Pf t) v proof_strat PF.optimise_pf (Fun (Prod a d) c) f (COMP a (createof (Lns c a) l1) FST) proof_strat PF.optimise_pf (Fun (Prod b c) d) g (COMP b (createof (Lns d b) l2) FST) success "sumw-Def-Lns" $ SUM_LNS l1 l2-sumw_def_lns _ _ = mzero-}+sumw_def_lns _ _ = mzero sumw_functor_id_lns :: Rule sumw_functor_id_lns (Lns _ _) (SUMW_LNS _ _ ID_LNS ID_LNS) =@@ -160,4 +161,8 @@ success "coassocl-Iso-Lns" ID_LNS coassocl_iso_lns' _ _ = mzero -+sums :: Rule+sums = top sum_functor_id_lns ||| top sum_functor_comp_lns ||| top sum_absor_lns+ ||| top sumw_functor_id_lns ||| top sumw_absor_lns+ ||| top coswap_nat_lns ||| top coswap_iso_lns ||| top coswap_cancel_lns+ ||| top coassocr_nat_lns ||| top coassocr_iso_lns ||| top coassocl_nat_lns ||| top coassocl_iso_lns
src/Transform/Rules/PF.hs view
@@ -23,42 +23,24 @@ import Transform.Rules.PF.Sums import Transform.Rules.PF.Dists import Transform.Rules.PF.Rec- +import Transform.Rules.PF.Lists+import Transform.Rules.PF.Monoids+import Transform.Rules.PF.Sums++sum_sfusion :: Rule+sum_sfusion = comp2 (prod_wunfusion >>> comp1 unabides) >>> comp sum_fusion'+ optimise_pf :: Rule-optimise_pf = outermost (top comp_assocr ||| rules) >>> right >>> try (once fuse >>> optimise_pf)- where - right, rules, prot, undef, lns, prods, sums, bangs, dists, convs, recs, fuse :: Rule- right = many (once (top comp_assocr))- rules = top nat_id ||| prot ||| undef ||| lns ||| prods ||| sums ||| bangs ||| dists ||| convs ||| recs- prot = top unprotect- undef = top top_fusion- lns = top create_get ||| top put_get ||| top get_put ||| top create_put ||| top put_twice- prods = top prod_functor_id ||| top prod_functor_comp- ||| top prod_cancel ||| top prod_absor ||| top prod_eta- ||| top swap_def ||| top assocl_def ||| top assocr_def- sums = top sum_functor_id ||| top sum_functor_comp ||| top sum_eta- ||| top sum_cancel ||| top sum_absor ||| top abides- ||| top coswap_def ||| top coassocl_def ||| top coassocr_def- bangs = top bang_reflex ||| top bang_fusion ||| top bang_uniq- dists = top distr_def ||| top undistr_def- ||| top distl_iso ||| top undistl_iso ||| top undistl_def- ||| top distl_fst_cancel ||| top distl_snd_cancel ||| top distl_id_cancel- ||| top distl_sum_cancel ||| top distl_bang_cancel ||| top distl_cancel- ||| top distl_distl_fusion- convs = top rconv_cancel ||| top lconv_cancel ||| top conv_conv- ||| top conv_id ||| top conv_comp ||| top conv_inn ||| top conv_out- ||| top conv_prod ||| top conv_sum- recs = top in_iso ||| top out_iso- ||| top functor_id ||| top functor_comp ||| top functor_def ||| top fzip_def- ||| top cata_reflex ||| top cata_cancel- ||| top para_reflex ||| top para_cancel ||| top para_cata- ||| top ana_reflex ||| top ana_cancel- fuse = top prod_fusion ||| top sum_fusion {- ||| top prod_def ||| top sum_def-}- ||| top distl_fusion ||| top distl_nat- {-||| top hylo_id ||| top cata_fusion ||| top ana_fusion- ||| top hylo_shift-}+optimise_pf = outermost rules >>> try ((once fuse1 ||| once fuse2 ||| once fuse3 ||| once fuse4 ||| once fuse5) >>> optimise_pf)+ where rules, fuse1, fuse2, fuse3, fuse4, fuse5 :: Rule+ rules = primitives ||| monoids ||| lists ||| prods ||| sums ||| bangs ||| convs ||| dists ||| recs+ fuse1 = top para_cata ||| top cata_fusion ||| top para_fusion ||| top ana_fusion ||| top cata_zero ||| top cata_cancel ||| top ana_cancel+ fuse2 = top distl_fusion ||| top distl_nat+ fuse3 = top hylo_id ||| top hylo_shift+ fuse4 = top prod_fusion ||| top sum_fusion+ fuse5 = top sum_sfusion -beautify_pf :: Rule +beautify_pf :: Rule beautify_pf = outermost (prods ||| sums) where prods, sums :: Rule
src/Transform/Rules/PF.hs-boot view
@@ -1,5 +1,6 @@ module Transform.Rules.PF where import Transform.Rewriting- ++sum_sfusion :: Rule optimise_pf :: Rule
src/Transform/Rules/PF/Combinators.hs view
@@ -18,6 +18,7 @@ module Transform.Rules.PF.Combinators where import Data.Type+import Data.Pf import Data.Lens import Data.Equal import Transform.Rewriting@@ -27,36 +28,14 @@ -- ** Combinators -protect_lns :: Rule -> Rule-protect_lns r (Fun c a) (PROTECT f) =- r (Fun c a) f-protect_lns r t f = r t f--unprotect :: Rule-unprotect (Fun c a) (PROTECT (CATA l1)) = mzero-unprotect (Fun c a) (PROTECT (ANA l1)) = mzero-unprotect (Fun c a) (PROTECT (COMP b l1 l2)) =- return $ COMP b (PROTECT l1) (PROTECT l2)-unprotect (Fun (Prod c d) (Prod a b)) (PROTECT (PROD l1 l2)) =- return $ PROD (PROTECT l1) (PROTECT l2)-unprotect (Fun (Either c d) (Either a b)) (PROTECT (SUM l1 l2)) = do- return $ SUM (PROTECT l1) (PROTECT l2)-unprotect (Fun c a) (PROTECT l1) = do- debug "safeUnprotect" (Pf $ Fun c a) l1- return l1-unprotect _ _ = mzero- comp :: Rule -> Rule-comp r t@(Fun d a) e = r t e- `mplus` (do- COMP b f (COMP c g h) <- nop t e+comp r (Fun d a) (COMP b f (COMP c g h)) = do fg <- r (Fun c a) (COMP b f g)- return $ COMP c fg h)- `mplus` (do- COMP c (COMP b f g) h <- nop t e+ return $ COMP c fg h+comp r (Fun d a) (COMP c (COMP b f g) h) = do gh <- r (Fun d b) (COMP c g h)- return $ COMP b f gh)-comp _ _ _ = mzero+ return $ COMP b f gh+comp r t f = r t f comp1 :: Rule -> Rule comp1 r (Fun a c) (COMP b f g) = do@@ -172,13 +151,13 @@ rightmost_prod :: Rule rightmost_prod (Fun (Prod a b) (Prod c d)) (PROD ID ID) = mzero-rightmost_prod (Fun (Prod a b) (Prod c d)) (PROD ID g) = do+rightmost_prod t@(Fun (Prod a b) (Prod c d)) v@(PROD ID g) = do COMP y g' g'' <- rightmost' (Fun b d) g return $ COMP (Prod a y) (ID ><= g') (ID ><= g'')-rightmost_prod (Fun (Prod a b) (Prod c d)) (PROD f ID) = do+rightmost_prod t@(Fun (Prod a b) (Prod c d)) v@(PROD f ID) = do COMP x f' f'' <- rightmost' (Fun a c) f return $ COMP (Prod x b) (f' ><= ID) (f'' ><= ID)-rightmost_prod (Fun (Prod a b) (Prod c d)) (PROD f g) = do+rightmost_prod t@(Fun (Prod a b) (Prod c d)) v@(PROD f g) = do COMP x f' f'' <- rightmost' (Fun a c) f COMP y g' g'' <- rightmost' (Fun b d) g return $ COMP (Prod x y) (f' ><= g') (f'' ><= g'')@@ -212,7 +191,7 @@ bang_fusion = comp bang_fusion' bang_fusion' :: Rule-bang_fusion' (Fun a One) (COMP b BANG f) =+bang_fusion' t@(Fun a One) v@(COMP b BANG f) = do success "bang-Fusion" BANG bang_fusion' _ _ = mzero @@ -248,10 +227,6 @@ Eq <- teq a a' guard $ geq (Pf $ Lns c a) f f' success "Create-Get" ID---create_get' (Fun a a') (COMP c (GET f) g) = do--- Eq <- teq a a'--- proof_strat optimise_pf (Fun a c) (createof (Lns c a) f) g--- success "Create-Get" ID create_get' _ _ = mzero put_get = comp put_get'@@ -260,11 +235,6 @@ Eq <- teq a a' guard $ geq (Pf $ Lns c a) f f' success "Put-Get" FST---put_get' (Fun (Prod a c) a') (COMP c' (GET f) g) = do--- Eq <- teq c c'--- Eq <- teq a a'--- proof_strat optimise_pf (Fun (Prod a c) c) (putof (Lns c a) f) g--- success "Put-Get" FST put_get' _ _ = mzero get_put = comp get_put'@@ -299,12 +269,12 @@ -- ** Backtracking sums and products -prod_undef :: Rule-prod_undef t@(Fun a (Prod b c)) (f `SPLIT` g) = do- COMP _ f' FST <- rightmost (Fun a b) f- COMP _ g' SND <- rightmost (Fun a c) g- success "prod-UnDef" $ f' ><= g'-prod_undef _ _ = mzero+prod_wunfusion :: Rule+prod_wunfusion t@(Fun a _) (COMP x f g `SPLIT` COMP y h g') = do+ Eq <- teq x y+ guard $ geq (Pf $ Fun a x) g g'+ success "prod-Unfusion" $ COMP x (f `SPLIT` h) g+prod_wunfusion _ _ = mzero prod_unfusion :: Rule prod_unfusion _ (ID `SPLIT` ID) = mzero@@ -317,13 +287,6 @@ success "prod-UnFusion" res prod_unfusion _ _ = mzero -sum_undef :: Rule-sum_undef t@(Fun (Either a b) c) (f `EITHER` g) = do- COMP _ INL f' <- leftmost (Fun a c) f- COMP _ INR g' <- leftmost (Fun b c) g- success "sum-UnDef" $ f' -|-= g'-sum_undef _ _ = mzero- sum_unfusion :: Rule sum_unfusion _ (ID `EITHER` ID) = mzero sum_unfusion t@(Fun (Either a b) c) w@(f `EITHER` g) = do@@ -345,4 +308,44 @@ success "top-Fusion" TOP top_fusion' _ _ = mzero +dyn_cancel, dyn_cancel' :: Rule+dyn_cancel = comp dyn_cancel'+dyn_cancel' _ (COMP _ (UNDYN a) (MKDYN b)) = do+ Eq <- teq a b+ success "dyn-Cancel" ID+dyn_cancel' _ _ = mzero +cast_cancel, cast_cancel' :: Rule+cast_cancel = comp cast_cancel'+cast_cancel' _ (COMP _ (CAST a) (MKDYN b)) = do+ cast_cancel' (Fun b a) (CAST a)+cast_cancel' (Fun b@(Data s f) _) (CAST a) | isBasic a = do+ Eq <- teq (rep f b) a+ success "cast-Cancel" OUT+cast_cancel' (Fun b@(NewData s f) _) (CAST a) | isBasic a = do+ Eq <- teq (rep f b) a+ success "cast-Cancel" OUT+cast_cancel' (Fun b _) (CAST a) = do+ Eq <- teq a b+ success "cast-Cancel" ID+cast_cancel' _ _ = mzero++primitives :: Rule+primitives = top comp_assocr ||| top nat_id ||| top dyn_cancel ||| top cast_cancel ||| top top_fusion++bangs :: Rule+bangs = top bang_reflex ||| top bang_fusion ||| top bang_uniq++-- ** Relating sums with products++abides = abides'+abides' :: Rule+abides' (Fun _ _) ((f `SPLIT` g) `EITHER` (h `SPLIT` i)) =+ success "abides" $ (f \/= h) /\= (g \/= i)+abides' _ _ = mzero++unabides = unabides'+unabides' :: Rule+unabides' (Fun _ _) ((f `EITHER` h) `SPLIT` (g `EITHER` i)) =+ success "unabides" $ (f /\= g) \/= (h /\= i)+unabides' _ _ = mzero
src/Transform/Rules/PF/Dists.hs view
@@ -18,9 +18,12 @@ module Transform.Rules.PF.Dists where import Data.Type+import Data.Pf import Data.Equal import Transform.Rewriting import Transform.Rules.PF.Combinators+import Transform.Rules.PF.Products+import Transform.Rules.PF.Sums import Prelude hiding (Functor(..)) import Control.Monad hiding (Functor(..))@@ -28,7 +31,7 @@ -- ** Distr distr_def :: Rule-distr_def (Fun (Prod c (Either a b)) _) DISTR =+distr_def t@(Fun (Prod c (Either a b)) _) v@DISTR = do success "distr-Def" $ COMP (Either (Prod a c) (Prod b c)) (SWAP -|-= SWAP) $ COMP (Prod (Either a b) c) DISTL SWAP distr_def _ _ = mzero @@ -151,3 +154,10 @@ let t = Either (Prod a c) (Prod b c) success "distl-Distl-Fusion" $ COMP t ((ID /\= (COMP x f (INL ><= ID))) -|-= (ID /\= (COMP x f (INR ><= ID)))) DISTL distl_distl_fusion' _ _ = mzero++dists :: Rule+dists = top distr_def ||| top undistr_def ||| top undistl_def + ||| top distl_iso ||| top undistl_iso+ ||| top distl_fst_cancel ||| top distl_snd_cancel ||| top distl_id_cancel+ ||| top distl_sum_cancel ||| top distl_bang_cancel ||| top distl_cancel+ ||| top distl_distl_fusion
+ src/Transform/Rules/PF/Lists.hs view
@@ -0,0 +1,148 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Rules.PF.Lists+-- Copyright : (c) 2010 University of Minho+-- License : BSD3+--+-- Maintainer : hpacheco@di.uminho.pt+-- Stability : experimental+-- Portability : non-portable+--+-- Pointless Rewrite:+-- automatic transformation system for point-free programs+-- +-- Combinators for the rewriting of point-free functions involving lists.+--+-----------------------------------------------------------------------------++module Transform.Rules.PF.Lists where++import Transform.Rewriting+import Transform.Rules.PF.Combinators+import Data.Type+import Data.Pf++import Control.Monad++map_id :: Rule+map_id _ (MAP ID) = success "map-Id" ID+map_id _ _ = mzero++map_wrap, map_wrap' :: Rule+map_wrap = comp map_wrap'+map_wrap' (Fun _ (List b)) (COMP _ (MAP f) WRAP) = success "map-Wrap" $ COMP b WRAP f+map_wrap' _ _ = mzero++map_fusion, map_fusion' :: Rule+map_fusion = comp map_fusion'+map_fusion' _ (COMP (List a) (MAP f) (MAP g)) = success "map-Fusion" $ MAP $ COMP a f g+map_fusion' _ _ = mzero++-- Monoids++fold_mapzero, fold_mapzero' :: Rule+fold_mapzero = comp fold_mapzero'+fold_mapzero' _ (COMP _ FOLD (MAP ZERO)) = success "fold-MapZero" ZERO+fold_mapzero' _ _ = mzero++fold_wrap, fold_wrap' :: Rule+fold_wrap = comp fold_wrap'+fold_wrap' _ (COMP _ FOLD WRAP) = success "fold-Wrap" ID+fold_wrap' _ _ = mzero++fold_mapwrap, fold_mapwrap' :: Rule+fold_mapwrap = comp fold_mapwrap'+fold_mapwrap' _ (COMP _ FOLD (MAP WRAP)) = success "fold-MapWrap" $ ID+fold_mapwrap' _ (COMP _ FOLD (MAP (COMP _ WRAP f))) = success "fold-MapWrap" $ MAP f+fold_mapwrap' _ _ = mzero++map_plus, map_plus' :: Rule+map_plus = comp map_plus'+map_plus' (Fun _ r) (COMP _ (MAP f) PLUS) = success "map-Plus" $ COMP (Prod r r) PLUS (MAP f `PROD` MAP f)+map_plus' _ _ = mzero++map_zero, map_zero' :: Rule+map_zero = comp map_zero'+map_zero' _ (COMP _ (MAP f) ZERO) = success "map-Zero" ZERO+map_zero' _ _ = mzero++map_fold, map_fold' :: Rule+map_fold = comp map_fold'+map_fold' (Fun _ r) (COMP _ (MAP f) FOLD) = success "map-Fold" $ COMP (List r) FOLD $ MAP (MAP f)+map_fold' _ _ = mzero++fold_foldmap, fold_foldmap' :: Rule+fold_foldmap = comp fold_foldmap'+fold_foldmap' (Fun _ r) (COMP _ FOLD (COMP (List a) FOLD (MAP f))) = success "fold-FoldMap" $ COMP (List r) FOLD $ MAP (COMP a FOLD f)+fold_foldmap' _ _ = mzero++length_zero, length_zero' :: Rule+length_zero = comp length_zero'+length_zero' (Fun _ _) (COMP _ LENGTH ZERO) = success "length-Zero" ZERO+length_zero' _ _ = mzero++length_wrap, length_wrap' :: Rule+length_wrap = comp length_wrap'+length_wrap' (Fun _ _) (COMP _ LENGTH WRAP) = success "length-Wrap" ONE+length_wrap' _ _ = mzero++fold_mapone, fold_mapone' :: Rule+fold_mapone = comp fold_mapone'+fold_mapone' (Fun _ _) (COMP _ FOLD (MAP ONE)) = success "length" LENGTH+fold_mapone' _ _ = mzero++length_plus = comp length_plus'+length_plus' :: Rule+length_plus' (Fun _ _) (COMP _ LENGTH PLUS) =+ success "length-Plus" $ COMP (Prod nat nat) PLUS $ LENGTH `PROD` LENGTH+length_plus' _ _ = mzero++length_map = comp length_map'+length_map' :: Rule+length_map' t@(Fun la@(List a) _) v@(COMP lb@(List b) LENGTH (MAP l1)) = do+ success "length-Map" LENGTH+length_map' _ _ = mzero++length_fold = comp length_fold'+length_fold' :: Rule+length_fold' (Fun _ _) (COMP _ LENGTH FOLD) =+ success "length-Fold" $ COMP (List nat) FOLD $ MAP LENGTH+length_fold' _ _ = mzero++one_fusion, one_fusion' :: Rule+one_fusion = comp one_fusion'+one_fusion' _ (COMP _ ONE f) = success "one-Fusion" ONE+one_fusion' _ _ = mzero++head_nil, head_nil' :: Rule+head_nil = comp head_nil'+head_nil' _ (COMP _ LHEAD ZERO) = success "head-Zero" ZERO+head_nil' _ _ = mzero++head_wrap, head_wrap' :: Rule+head_wrap = comp head_wrap'+head_wrap' _ (COMP _ LHEAD WRAP) = success "head-Wrap" WRAP+head_wrap' _ _ = mzero++tail_nil, head_nil' :: Rule+tail_nil = comp head_nil'+tail_nil' _ (COMP _ LTAIL ZERO) = success "tail-Zero" ZERO+tail_nil' _ _ = mzero++tail_wrap, head_wrap' :: Rule+tail_wrap = comp head_wrap'+tail_wrap' _ (COMP _ LTAIL WRAP) = success "tail-Wrap" ZERO+tail_wrap' _ _ = mzero++lists :: Rule+lists = top map_id ||| top map_wrap ||| top map_fusion+ ||| top map_plus ||| top map_zero ||| top map_fold+ ||| top fold_mapzero ||| top fold_wrap ||| top fold_mapwrap ||| top fold_foldmap+ ||| top length_zero ||| top length_plus ||| top length_map ||| top length_fold+ ||| top length_wrap ||| top fold_mapone ||| top one_fusion+ ||| top head_nil ||| top head_wrap ||| top tail_nil ||| top tail_wrap+++++
+ src/Transform/Rules/PF/Monoids.hs view
@@ -0,0 +1,76 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Rules.PF.Monoids+-- Copyright : (c) 2010 University of Minho+-- License : BSD3+--+-- Maintainer : hpacheco@di.uminho.pt+-- Stability : experimental+-- Portability : non-portable+--+-- Pointless Rewrite:+-- automatic transformation system for point-free programs+-- +-- Combinators for the rewriting of point-free functions involving monoids.+--+-----------------------------------------------------------------------------++module Transform.Rules.PF.Monoids where++import Generics.Pointless.Functors hiding (rep)+import Transform.Rewriting+import {-# SOURCE #-} Transform.Rules.PF+import Transform.Rules.PF.Combinators+import Transform.Rules.PF.Products+import Transform.Rules.PF.Sums+import Data.Type+import Data.Pf+import Data.Equal++import Control.Monad hiding (Functor)+import Data.Monoid hiding (Any)+import Prelude hiding (Functor)++cata_zero :: Rule+cata_zero (Fun a r@(isList -> Just Eq)) (CATA f) = cata_zero' (Fun a r) (CATA f)+cata_zero (Fun a r@(isInt -> Just Eq)) (CATA f) = cata_zero' (Fun a r) (CATA f)+cata_zero (Fun a r@(isNat -> Just Eq)) (CATA f) = cata_zero' (Fun a r) (CATA f)+cata_zero _ _ = mzero++cata_zero' :: (Mu a,Functor (PF a),Monoid r) => Type (a -> r) -> Pf (a -> r) -> Rewrite (Pf (a -> r))+cata_zero' (Fun a@(dataFctr -> Just fctr) r) (CATA f) = do+ let (fa,fr) = (rep fctr a,rep fctr r)+ g' = COMP fr f (FMAP fctr (Fun a r) ZERO)+ g <- optimise_pf (Fun fa r) g'+ guard $ geq (Pf $ Fun fa r) ZERO g+ success "cata-Zero" ZERO++plus_zero, plus_zero' :: Rule+plus_zero = comp plus_zero'+plus_zero' _ (COMP _ PLUS (ZERO `SPLIT` f)) = success "plus-Zero" f+plus_zero' (Fun (Prod a b) _) (COMP _ PLUS (ZERO `PROD` f)) = success "plus-Zero" $ COMP b f SND+plus_zero' _ (COMP _ PLUS (f `SPLIT` ZERO)) = success "plus-Zero" f+plus_zero' (Fun (Prod a b) _) (COMP _ PLUS (f `PROD` ZERO)) = success "plus-Zero" $ COMP a f FST+plus_zero' _ _ = mzero++zero_fusion, zero_fusion' :: Rule+zero_fusion = comp zero_fusion'+zero_fusion' _ (COMP _ ZERO f) = success "zero-Fusion" ZERO+zero_fusion' _ _ = mzero++zero_either :: Rule+zero_either _ (ZERO `EITHER` ZERO) = success "zero-Either" ZERO+zero_either _ _ = mzero++fold_plus, fold_plus' :: Rule+fold_plus = comp fold_plus'+fold_plus' (Fun _ r) (COMP _ FOLD PLUS) = success "fold-Plus" $ COMP (Prod r r) PLUS (FOLD `PROD` FOLD)+fold_plus' _ _ = mzero++fold_zero, fold_zero' :: Rule+fold_zero = comp fold_zero'+fold_zero' _ (COMP _ FOLD ZERO) = success "fold-Zero" ZERO+fold_zero' _ _ = mzero++monoids :: Rule+monoids = top plus_zero ||| top zero_fusion ||| top fold_plus ||| top fold_zero ||| top zero_either
src/Transform/Rules/PF/Products.hs view
@@ -18,6 +18,7 @@ module Transform.Rules.PF.Products where import Data.Type+import Data.Pf import Data.Equal import Transform.Rewriting import Transform.Rules.PF.Combinators@@ -32,6 +33,13 @@ success "prod-Def" $ (COMP a f FST) `SPLIT` (COMP b g SND) prod_def _ _ = mzero +prod_undef :: Rule+prod_undef t@(Fun a (Prod b c)) (f `SPLIT` g) = do+ COMP _ f' FST <- rightmost (Fun a b) f+ COMP _ g' SND <- rightmost (Fun a c) g+ success "prod-UnDef" $ f' ><= g'+prod_undef _ _ = mzero+ prod_eta :: Rule prod_eta a (SPLIT (COMP b FST f) (COMP c SND g)) = do Eq <- teq b c@@ -48,12 +56,12 @@ prod_functor_comp = comp prod_functor_comp' prod_functor_comp' :: Rule-prod_functor_comp' (Fun _ _) (COMP (Prod c d) (f `PROD` g) (h `PROD` i)) =+prod_functor_comp' t@(Fun a b) v@(COMP (Prod c d) (f `PROD` g) (h `PROD` i)) = do success "prod-Functor-Comp" $ COMP c f h ><= COMP d g i prod_functor_comp' _ _ = mzero +prod_cancel, prod_cancel' :: Rule prod_cancel = comp prod_cancel'-prod_cancel' :: Rule prod_cancel' t (COMP _ FST (SPLIT f g)) = success "prod-Cancel" f prod_cancel' (Fun (Prod a b) _) (COMP _ FST (f `PROD` g)) =@@ -64,22 +72,22 @@ success "prod-Cancel" $ COMP b g SND prod_cancel' _ _ = mzero -prod_fusion = comp prod_fusion'+prod_fusion = comp $ try (comp1 abides) >>> prod_fusion' prod_fusion' :: Rule-prod_fusion' t (COMP c (SPLIT f g) h) =+prod_fusion' t v@(COMP c (SPLIT f g) h) = do success "prod-Fusion" $ (COMP c f h) `SPLIT` (COMP c g h) prod_fusion' _ _ = mzero prod_absor = comp prod_absor' prod_absor' :: Rule-prod_absor' (Fun _ _) (COMP (Prod c d) (f `PROD` g) (h `SPLIT` i)) =+prod_absor' t@(Fun _ _) v@(COMP (Prod c d) (f `PROD` g) (h `SPLIT` i)) = do success "prod-Absor" $ (COMP c f h) /\= (COMP d g i) prod_absor' _ _ = mzero -- ** Isomorphisms swap_def :: Rule-swap_def (Fun (Prod a b) _) SWAP =+swap_def t@(Fun (Prod a b) _) v@SWAP = do success "swap-Def" $ SND /\= FST swap_def _ _ = mzero @@ -92,3 +100,8 @@ assocr_def (Fun (Prod (Prod a b) c) _) ASSOCR = success "assocr-Def" $ (COMP (Prod a b) FST FST) /\= (SND ><= ID) assocr_def _ _ = mzero++prods :: Rule+prods = top prod_functor_id ||| top prod_functor_comp+ ||| top prod_cancel ||| top prod_absor ||| top prod_eta+ ||| top swap_def ||| top assocl_def ||| top assocr_def
src/Transform/Rules/PF/Rec.hs view
@@ -18,11 +18,14 @@ module Transform.Rules.PF.Rec where import Data.Type+import Data.Pf import Data.Equal import Transform.Rewriting import Transform.Rules.PF.Combinators import {-# SOURCE #-} Transform.Rules.PF import Transform.Rules.Lenses.Lists+import Transform.Rules.PF.Sums+import Transform.Rules.PF.Products import Prelude hiding (Functor(..)) import Control.Monad hiding (Functor(..))@@ -30,7 +33,7 @@ import Unsafe.Coerce import Generics.Pointless.Combinators hiding (comp)-import Generics.Pointless.Functors+import Generics.Pointless.Functors hiding (rep) import Generics.Pointless.Lenses -- ** In / Out@@ -64,32 +67,37 @@ success "functor-Comp" $ FMAP fctr (Fun a c) $ COMP b f g functor_comp' _ _ = mzero -functor_def :: Rule-functor_def (Fun _ _) (FMAP I _ f) =- success "functor-Def" f-functor_def (Fun _ _) (FMAP (K _) _ f) = - success "functor-Def" ID-functor_def (Fun _ _) (FMAP (g:*!:h) t@(Fun c a) f) = do- l <- functor_def (Fun (rep g c) (rep g a)) (FMAP g t f)- r <- functor_def (Fun (rep h c) (rep h a)) (FMAP h t f)- success "functor-Def" $ l `PROD` r-functor_def (Fun _ _) (FMAP (g:+!:h) t@(Fun c a) f) = do- l <- functor_def (Fun (rep g c) (rep g a)) (FMAP g t f)- r <- functor_def (Fun (rep h c) (rep h a)) (FMAP h t f)- success "functor-Def" $ l `SUM` r-functor_def (Fun _ _) (FMAP (g:@!:h) t@(Fun c a) f) = do+functor_def, functor_def' :: Rule+functor_def a x = functor_def' a x >>= success "functor-Def"+functor_def' (Fun _ _) (FMAP I _ f) =+ return f+functor_def' (Fun _ _) (FMAP (K _) _ f) = + return ID+functor_def' (Fun _ _) (FMAP L _ f) = + return $ MAP f+functor_def' (Fun _ _) (FMAP (g:*!:h) t@(Fun c a) f) = do+ l <- functor_def' (Fun (rep g c) (rep g a)) (FMAP g t f)+ r <- functor_def' (Fun (rep h c) (rep h a)) (FMAP h t f)+ return $ l `PROD` r+functor_def' (Fun _ _) (FMAP (g:+!:h) t@(Fun c a) f) = do+ l <- functor_def' (Fun (rep g c) (rep g a)) (FMAP g t f)+ r <- functor_def' (Fun (rep h c) (rep h a)) (FMAP h t f)+ return $ l `SUM` r+functor_def' (Fun _ _) (FMAP (g:@!:h) t@(Fun c a) f) = do let hc = rep h c let ha = rep h a- r <- functor_def (Fun hc ha) (FMAP h t f)- l <- functor_def (Fun (rep g hc) (rep g ha)) (FMAP g (Fun hc ha) r)- success "functor-Def" l-functor_def _ _ = mzero+ r <- functor_def' (Fun hc ha) (FMAP h t f)+ l <- functor_def' (Fun (rep g hc) (rep g ha)) (FMAP g (Fun hc ha) r)+ return l+functor_def' _ _ = mzero fzip_def :: Rule fzip_def (Fun _ _) (FZIP I _ f) = success "fzip-Def" ID fzip_def (Fun _ _) (FZIP (K t) _ f) = success "fzip-Def" FST+fzip_def (Fun _ _) (FZIP L (Fun a b) f) =+ success "fzip-Def" $ listzip a b fzip_def (Fun _ _) (FZIP (fctrf :*!: fctrg) (Fun a c) f) = do let (fa,fc) = (rep fctrf a,rep fctrf c) (ga,gc) = (rep fctrg a,rep fctrg c)@@ -117,54 +125,45 @@ -- ** Catas +cata_def :: Rule+cata_def (Fun a@(dataFctr -> Just fctr) b) (CATA g) = do+ guard (not $ isRec fctr)+ Eq <- teq (rep fctr a) (rep fctr b)+ success "cata-Def" $ COMP (rep fctr a) g OUT+cata_def _ _ = mzero+ cata_reflex :: Rule cata_reflex (Fun a b) (CATA INN) = do Eq <- teq a b success "cata-Reflex" ID cata_reflex _ _ = mzero -lns_cata_cancel = try (try (once list_defs_lns) >>> (create_def ||| get_def ||| put_def)) cata_cancel = comp cata_cancel' cata_cancel' :: Rule-cata_cancel' t@(Fun _ b) v@(COMP a@(Data _ fctr) (PROTECT g) INN) = (do- CATA g' <- lns_cata_cancel (Fun a b) g- debug "cata-Cancel" (Pf t) v- let fb = rep fctr b- success "cata-Cancel" $ COMP fb g' $ FMAP fctr (Fun a b) (PROTECT g))- `mplus` (do- ANA g' <- lns_cata_cancel (Fun a b) g- CATA g'' <- ana_shift (Fun a b) (ANA g')- let fb = rep fctr b- success "cata-Cancel" $ COMP fb g'' $ FMAP fctr (Fun a b) (PROTECT g)- )-cata_cancel' t@(Fun _ b) v@(COMP a@(Data _ fctr) g INN) = (do- CATA g' <- lns_cata_cancel (Fun a b) g+cata_cancel' (Fun fa b) (COMP a (ANA g) INN) = do+ cata <- ana_shift (Fun a b) (ANA g)+ cata_cancel' (Fun fa b) (COMP a cata INN)+cata_cancel' t@(Fun _ b) v@(COMP a@(dataFctr -> Just fctr) (CATA g) INN) = do debug "cata-Cancel" (Pf t) v let fb = rep fctr b- success "cata-Cancel" $ COMP fb g' $ FMAP fctr (Fun a b) g)- `mplus` (do- ANA g' <- lns_cata_cancel (Fun a b) g- CATA g'' <- ana_shift (Fun a b) (ANA g')- let fb = rep fctr b- success "cata-Cancel" $ COMP fb g'' $ FMAP fctr (Fun a b) g- )+ success "cata-Cancel" $ COMP fb g $ FMAP fctr (Fun a b) (CATA g) cata_cancel' _ _ = mzero cata_fusion = precomp (rightmost_prod ||| rightmost_sum) cata_fusion' cata_fusion' :: Rule cata_fusion' (Fun _ _) (COMP _ OUT (CATA g)) = mzero-cata_fusion' t@(Fun (Data _ fctr) a) v@(COMP b f (CATA g)) = do+cata_fusion' t@(Fun (dataFctr -> Just fctr) a) v@(COMP b f (CATA g)) = do+ debug "cataFusion" (Pf t) v let (fa,fb) = (rep fctr a,rep fctr b)- prot = PROTECT f- h' = COMP b prot $ COMP fb g $ FMAP fctr (Fun a b) (CONV (Right _L) f)+ h' = COMP b f $ COMP fb g $ FMAP fctr (Fun a b) (rconv f) h <- optimise_pf (Fun fa a) h' debug "cataRes" (Pf $ Fun fa a) h- guard $ not $ find (Pf (Fun Any Any)) (CONV (Right _L) TOP) (Pf (Fun fa a)) h+ guard $ not $ find (Pf (Fun Any Any)) (rconv TOP) (Pf (Fun fa a)) h success "cata-Fusion" $ CATA h cata_fusion' _ _ = mzero cata_shift :: Rule-cata_shift t@(Fun a@(Data _ f) b@(Data _ g)) v@(CATA (COMP gb INN eta)) = do+cata_shift t@(Fun a@(dataFctr -> Just f) b@(dataFctr -> Just g)) v@(CATA (COMP gb INN eta)) = do debug "cata-Shift" (Pf t) v Eq <- teq (rep g b) gb eta' <- natCoerce f g b eta a@@ -173,18 +172,22 @@ -- ** Paras +para_def :: Rule+para_def (Fun a@(dataFctr -> Just fctr) c) (PARA g) = do+ guard (not $ isRec fctr)+ Eq <- teq (rep fctr a) (rep fctr (Prod c a))+ success "para-Def" $ COMP (rep fctr a) g OUT+para_def _ _ = mzero+ para_reflex :: Rule-para_reflex (Fun (a@(Data _ fctr)) (b@(Data _ fctrb))) (PARA (COMP fab INN f)) = do+para_reflex (Fun a b) (PARA (COMP _ INN (FMAP _ _ FST))) = do Eq <- teq a b- let t = Fun (rep fctr (Prod b a)) (rep fctr b)- g = FMAP fctr (Fun (Prod b a) b) FST- proof_strat optimise_pf t f g success "para-Reflex" ID para_reflex _ _ = mzero para_cancel = comp para_cancel' para_cancel' :: Rule-para_cancel' (Fun faa c) (COMP a@(Data _ fctr) (PARA g) INN) = do+para_cancel' (Fun faa c) (COMP a@(dataFctr -> Just fctr) (PARA g) INN) = do Eq <- teq (rep fctr a) faa let p = (PARA g `SPLIT` ID) success "para-Cancel" $ COMP (rep fctr (Prod c a)) g $ FMAP fctr (Fun a (Prod c a)) p@@ -192,67 +195,68 @@ para_cata = comp para_cata' para_cata' :: Rule-para_cata' (Fun a@(Data _ fctr) b) (PARA (COMP fab f g)) = do- Eq <- teq (rep fctr b) fab- let t = Fun (rep fctr (Prod b a)) (rep fctr b)- h = FMAP fctr (Fun (Prod b a) b) FST- proof_strat optimise_pf t g h- success "para-Cata" $ CATA f+para_cata' (Fun a@(dataFctr -> Just fctr) b) (PARA f) = do+ let (fb,fba) = (rep fctr b,rep fctr (Prod b a))+ g' = COMP fba f $ FMAP fctr (Fun b (Prod b a)) (rconv FST)+ g <- optimise_pf (Fun fb b) g'+ guard $ not $ find (Pf $ Fun Any Any) (rconv TOP) (Pf $ Fun fb b) g+ success "para-Cata" $ CATA g para_cata' _ _ = mzero +para_fusion = comp para_fusion'+para_fusion' :: Rule+para_fusion' (Fun _ _) (COMP _ OUT (PARA g)) = mzero+para_fusion' t@(Fun c@(dataFctr -> Just fctr) a) v@(COMP b f (PARA g)) = do+ debug "paraRes!!" (Pf $ Fun c a) v+ let (fbc,fac) = (rep fctr (Prod b c),rep fctr (Prod a c))+ h' = COMP b f $ COMP fbc g $ FMAP fctr (Fun (Prod a c) (Prod b c)) (rconv f `PROD` ID)+ h <- optimise_pf (Fun fac a) h'+ debug "paraRes" (Pf $ Fun fac a) h+ guard $ not $ find (Pf (Fun Any Any)) (rconv TOP) (Pf (Fun fac a)) h+ success "para-Fusion" $ PARA h+para_fusion' _ _ = mzero+ -- ** Anas +ana_def :: Rule+ana_def (Fun a b@(dataFctr -> Just fctr)) (ANA g) = do+ guard (not $ isRec fctr)+ Eq <- teq (rep fctr b) (rep fctr a)+ success "ana-Def" $ COMP (rep fctr b) INN g+ana_def _ _ = mzero+ ana_reflex :: Rule ana_reflex (Fun a b) (ANA OUT) = do Eq <- teq a b success "ana-Reflex" ID ana_reflex _ _ = mzero -lns_ana_cancel = try (try (once list_defs_lns) >>> (create_def ||| get_def ||| put_def)) ana_cancel = comp ana_cancel' ana_cancel' :: Rule-ana_cancel' (Fun b fa) (COMP a@(Data _ fctr) OUT (PROTECT h)) = (do- ANA h' <- lns_ana_cancel (Fun b a) h- Eq <- teq fa (rep fctr a)- let fb = rep fctr b- success "ana-Cancel" $ COMP fb (FMAP fctr (Fun b a) (PROTECT h)) h')- `mplus` (do- CATA h' <- lns_ana_cancel (Fun b a) h- ANA h'' <- cata_shift (Fun b a) (CATA h')- Eq <- teq fa (rep fctr a)- let fb = rep fctr b- success "ana-Cancel" $ COMP fb (FMAP fctr (Fun b a) (PROTECT h)) h''- )-ana_cancel' (Fun b fa) (COMP a@(Data _ fctr) OUT h) = (do- ANA h' <- lns_ana_cancel (Fun b a) h- Eq <- teq fa (rep fctr a)- let fb = rep fctr b- success "ana-Cancel" $ COMP fb (FMAP fctr (Fun b a) h) h')- `mplus` (do- CATA h' <- lns_ana_cancel (Fun b a) h- ANA h'' <- cata_shift (Fun b a) (CATA h')+ana_cancel' (Fun b fa) (COMP a OUT (CATA h)) = do+ ana <- cata_shift (Fun b a) (CATA h)+ ana_cancel' (Fun b fa) (COMP a OUT ana)+ana_cancel' (Fun b fa) (COMP a@(dataFctr -> Just fctr) OUT (ANA h)) = do Eq <- teq fa (rep fctr a) let fb = rep fctr b- success "ana-Cancel" $ COMP fb (FMAP fctr (Fun b a) h) h''- )+ success "ana-Cancel" $ COMP fb (FMAP fctr (Fun b a) (ANA h)) h ana_cancel' _ _ = mzero ana_fusion = postcomp (leftmost_prod ||| leftmost_sum) ana_fusion' ana_fusion' :: Rule ana_fusion' (Fun _ _) (COMP _ (ANA f) INN) = mzero-ana_fusion' t@(Fun a c@(Data _ fctr)) v@(COMP b (ANA g) f) = do+ana_fusion' t@(Fun a c@(dataFctr -> Just fctr)) v@(COMP b (ANA g) f) = do debug "ana-Fusion" (Pf t) v let (fa,fb) = (rep fctr a,rep fctr b)- prot = PROTECT f- h' = COMP fb (FMAP fctr (Fun b a) (CONV (Left _L) f)) $ COMP b g prot+ h' = COMP fb (FMAP fctr (Fun b a) (lconv f)) $ COMP b g f h <- optimise_pf (Fun a fa) h' debug "anaRes" (Pf $ Fun a fa) h- guard $ not $ find (Pf (Fun Any Any)) (CONV (Left _L) TOP) (Pf (Fun a fa)) h+ guard $ not $ find (Pf (Fun Any Any)) (lconv TOP) (Pf (Fun a fa)) h success "ana-Fusion" $ ANA h ana_fusion' _ _ = mzero ana_shift :: Rule-ana_shift t@(Fun a@(Data _ f) b@(Data _ g)) v@(ANA (COMP fa eta OUT)) = do+ana_shift t@(Fun a@(dataFctr -> Just f) b@(dataFctr -> Just g)) v@(ANA (COMP fa eta OUT)) = do debug "ana-Shift" (Pf t) v Eq <- teq (rep f a) fa eta' <- natCoerce f g a eta b@@ -275,7 +279,7 @@ hylo_id = comp hylo_id' hylo_id' :: Rule-hylo_id' t@(Fun c a) v@(COMP b@(Data _ fctr) (CATA g) (ANA h)) = do+hylo_id' t@(Fun c a) v@(COMP b@(dataFctr -> Just fctr) (CATA g) (ANA h)) = do Eq <- teq c a debug "hylo-Id" (Pf t) v ID <- optimise_pf (Fun c a) (COMP (rep fctr c) g h)@@ -288,14 +292,15 @@ natProof f g a eta = proof optimise_pf t eq1 eq2 where eq1 = COMP (rep f a) eta fmapf eq2 = COMP (rep g a) fmapg eta- fmapf = FMAP f (Fun a a) HOLE- fmapg = FMAP g (Fun a a) HOLE+ fmapf = FMAP f (Fun a a) BOT+ fmapg = FMAP g (Fun a a) BOT t = Fun (rep f a) (rep g a) natCoerce :: (MonadPlus m,Functor f,Functor g) => Fctr f -> Fctr g -> Type a -> Pf (Rep f a -> Rep g a) -> Type b -> m (Pf (Rep f b -> Rep g b)) natCoerce f g a eta b = if (natProof f g a eta) then return (unsafeCoerce eta) else mzero +-- Separates the natural part from the type-dependent one in a functor transformation natSplit :: (Functor f) => Type a -> Type b -> Fctr f -> Pf ((Rep f a) -> b) -> Rewrite (Pf ((Rep f a) -> b)) -- Constant natSplit a b _ ID = mzero@@ -372,8 +377,12 @@ -- Id and unrecognized cases match here natSplit a b fctr f = mzero + -- ** Internal converses for fusion rules +rconv = CONV (Right _L)+lconv = CONV (Left _L)+ rconv_cancel = comp rconv_cancel' rconv_cancel' :: Rule rconv_cancel' t@(Fun a a') (COMP c (CATA f) (CONV (Right _) (ANA g))) = do@@ -417,38 +426,25 @@ success "conv-Id" ID conv_id _ _ = mzero -conv_inn :: Rule-conv_inn _ (CONV _ INN) =- success "conv-Inn" OUT-conv_inn _ _ = mzero--conv_out :: Rule-conv_out (Fun fa a@(Data _ fctr)) (CONV _ OUT) = do- Eq <- teq (rep fctr a) fa- success "conv-Out" INN-conv_out _ _ = mzero- conv_prod :: Rule-{-conv_prod (Fun a b) (CONV e s@(f `SPLIT` g)) = (do- COMP x s' h <- prod_unfusion (Fun b a) s- s'' <- conv_prod (Fun a x) (CONV e s')- success "conv-Prod" $ COMP x (CONV e h) s'')- `mplus` (do- PROD f' g' <- prod_undef (Fun b a) s- success "conv-Prod" $ (CONV e f') ><= (CONV e g'))-} conv_prod _ (CONV e (PROD f g)) = success "conv-Prod" $ PROD (CONV e f) (CONV e g) conv_prod _ _ = mzero conv_sum :: Rule-{-conv_sum (Fun a b) (CONV l e@(f `EITHER` g)) = (do- COMP x h e' <- sum_unfusion (Fun b a) e- e'' <- conv_sum (Fun x b) (CONV l e')- success "conv-Sum" $ COMP x e'' $ CONV l h)- `mplus` (do- SUM f' g' <- sum_undef (Fun b a) e- success "conv-Sum" $ (CONV l f') -|-= (CONV l g'))-} conv_sum _ (CONV l (SUM f g)) = success "conv-Sum" $ SUM (CONV l f) (CONV l g) conv_sum _ _ = mzero++convs :: Rule+convs = top rconv_cancel ||| top lconv_cancel+ ||| top conv_comp ||| top conv_conv ||| top conv_id+ ||| top conv_prod ||| top conv_sum++recs :: Rule+recs = top in_iso ||| top out_iso+ ||| top functor_id ||| top functor_comp ||| top functor_def ||| top fzip_def+ ||| top cata_def ||| top cata_reflex+ ||| top para_def ||| top para_reflex ||| top para_cancel+ ||| top ana_def ||| top ana_reflex
src/Transform/Rules/PF/Sums.hs view
@@ -18,6 +18,7 @@ module Transform.Rules.PF.Sums where import Data.Type+import Data.Pf import Data.Equal import Transform.Rewriting import Transform.Rules.PF.Combinators@@ -32,6 +33,13 @@ success "sum-Def" $ (EITHER (COMP a INL f) (COMP b INR g)) sum_def _ _ = mzero +sum_undef :: Rule+sum_undef t@(Fun (Either a b) c) v@(f `EITHER` g) = do+ COMP _ INL f' <- leftmost (Fun a c) f+ COMP _ INR g' <- leftmost (Fun b c) g+ success "sum-UnDef" $ f' -|-= g'+sum_undef _ _ = mzero+ sum_eta :: Rule sum_eta a (EITHER (COMP b1 k1 INL) (COMP b2 k2 INR)) = do Eq <- teq b1 b2@@ -48,7 +56,7 @@ sum_functor_comp = comp sum_functor_comp' sum_functor_comp' :: Rule-sum_functor_comp' (Fun _ _) (COMP (Either c d) (f `SUM` g) (h `SUM` i)) =+sum_functor_comp' t@(Fun _ _) v@(COMP (Either c d) (f `SUM` g) (h `SUM` i)) = do success "sum-Functor-Comp" $ COMP c f h -|-= COMP d g i sum_functor_comp' _ _ = mzero @@ -64,27 +72,18 @@ success "sum-Cancel" $ COMP d INR g sum_cancel' _ _ = mzero -sum_fusion = comp sum_fusion'+sum_fusion = comp $ try (comp2 unabides) >>> sum_fusion' sum_fusion' :: Rule sum_fusion' t (COMP a f (EITHER g h)) =- success "sum-Fusion" $ EITHER (COMP a f g) (COMP a f h)+ success "sum-Fusion" $ COMP a f g `EITHER`COMP a f h sum_fusion' _ _ = mzero sum_absor = comp sum_absor' sum_absor' :: Rule-sum_absor' (Fun _ _) (COMP (Either c d) (f `EITHER` g) (h `SUM` i)) = +sum_absor' t@(Fun _ _) v@(COMP (Either c d) (f `EITHER` g) (h `SUM` i)) = do success "sum-Absor" $ (COMP c f h) \/= (COMP d g i) sum_absor' _ _ = mzero --- ** Relating sums with products----abides = abides' ||| (sum_unfusion >>> comp2 abides')-abides = abides'-abides' :: Rule-abides' (Fun _ _) ((f `SPLIT` g) `EITHER` (h `SPLIT` i)) =- success "abides" $ (f \/= h) /\= (g \/= i)-abides' _ _ = mzero- -- ** Isomorphisms coswap_def :: Rule@@ -93,12 +92,16 @@ coswap_def _ _ = mzero coassocl_def :: Rule-coassocl_def (Fun (Either a (Either b c)) _) COASSOCL =+coassocl_def t@(Fun (Either a (Either b c)) _) v@COASSOCL = do success "coassocl-Def" $ (COMP (Either a b) INL INL) \/= (INR -|-= ID) coassocl_def _ _ = mzero coassocr_def :: Rule-coassocr_def (Fun (Either (Either a b) c) _) COASSOCR =+coassocr_def t@(Fun (Either (Either a b) c) _) v@COASSOCR = do success "coassocr-Def" $ (ID -|-= INL) \/= (COMP (Either b c) INR INR) coassocr_def _ _ = mzero +sums :: Rule+sums = top sum_functor_id ||| top sum_functor_comp ||| top sum_eta+ ||| top sum_cancel ||| top sum_absor+ ||| top coswap_def ||| top coassocl_def ||| top coassocr_def
src/Transform/Rules/SYB.hs view
@@ -25,15 +25,7 @@ optimise_syb = optimise_tp >>> optimise_tu optimise_tp :: Rule-optimise_tp = innermost rules- where rules :: Rule- rules = top nop_applyT ||| top seq_applyT- ||| top gmapT_applyT ||| top everywhere_applyT- ||| top mkT_applyT ||| top extT_applyT+optimise_tp = innermost tp optimise_tu :: Rule-optimise_tu = innermost rules- where rules :: Rule- rules = top emptyQ_applyQ ||| top union_applyQ- ||| top gmapQ_applyQ ||| top everything_applyQ- ||| top mkQ_applyQ ||| top extQ_applyQ+optimise_tu = innermost tu
src/Transform/Rules/SYB/TP.hs view
@@ -18,8 +18,10 @@ module Transform.Rules.SYB.TP where import Data.Type+import Data.Pf import Data.Eval import Transform.Rewriting hiding (gmapQ)+import Transform.Rules.PF.Combinators import Control.Monad nop_applyT :: Rule@@ -31,6 +33,7 @@ seq_applyT _ _ = mzero gmapT_applyT :: Rule+gmapT_applyT _ (APPLY Dynamic (ALL f)) = mzero gmapT_applyT _ (APPLY a (ALL f)) = success "gmapT-applyT" (allT a f) gmapT_applyT _ _ = mzero @@ -40,14 +43,21 @@ everywhere_applyT _ _ = mzero mkT_applyT :: Rule+mkT_applyT _ (APPLY Dynamic (MKT b f)) = mzero mkT_applyT _ (APPLY a (MKT b f)) = success "mkT-applyT" (mkT a b f) mkT_applyT _ _ = mzero extT_applyT :: Rule+extT_applyT _ (APPLY Dynamic (EXTT f t g)) = mzero extT_applyT _ (APPLY a (EXTT f t g)) = success "extT-applyT" (extT a f t g) extT_applyT _ _ = mzero -gmapT_everywhere :: Rule-gmapT_everywhere _ (ALL (EVERYWHERE f)) = success "gmapT-everywhere" (EVERYWHERE f)-gmapT_everywhere _ (ALL (EVERYWHERE' f)) = success "gmapT-everywhere" (EVERYWHERE' f)-gmapT_everywhere _ _ = mzero+dyn_applyT, dyn_applyT' :: Rule+dyn_applyT = comp dyn_applyT'+dyn_applyT' (Fun _ _) (COMP _ (APPLY Dynamic f) (MKDYN a)) = success "dyn-ApplyQ" $ COMP a (MKDYN a) $ APPLY a f+dyn_applyT' _ _ = mzero++tp :: Rule+tp = top nop_applyT ||| top seq_applyT+ ||| top gmapT_applyT ||| top everywhere_applyT+ ||| top mkT_applyT ||| top extT_applyT ||| top dyn_applyT
src/Transform/Rules/SYB/TU.hs view
@@ -18,8 +18,10 @@ module Transform.Rules.SYB.TU where import Data.Type+import Data.Pf import Data.Eval import Transform.Rewriting hiding (gmapQ)+import Transform.Rules.PF.Combinators import Control.Monad emptyQ_applyQ :: Rule@@ -27,10 +29,12 @@ emptyQ_applyQ _ _ = mzero union_applyQ :: Rule-union_applyQ (Fun _ r) (APPLYQ a (UNION (f::Pf (Q r)) g)) = success "union-applyQ" $ gmapQProd r $ (APPLYQ a f) `SPLIT` (APPLYQ a g)+union_applyQ (Fun _ r) (APPLYQ a (UNION (f::Pf (Q r)) g)) =+ success "union-applyQ" $ COMP (Prod r r) PLUS $ (APPLYQ a f) `SPLIT` (APPLYQ a g) union_applyQ _ _ = mzero gmapQ_applyQ :: Rule+gmapQ_applyQ (Fun _ r) (APPLYQ Dynamic (GMAPQ f)) = mzero gmapQ_applyQ (Fun _ r) (APPLYQ a (GMAPQ f)) = success "gmapQ-applyQ" (gmapQ r a f) gmapQ_applyQ _ _ = mzero @@ -39,13 +43,17 @@ everything_applyQ _ _ = mzero mkQ_applyQ :: Rule+mkQ_applyQ _ (APPLYQ Dynamic (MKQ b f)) = mzero mkQ_applyQ _ (APPLYQ a (MKQ b f)) = success "mkQ-applyQ" (mkQ a b f) mkQ_applyQ _ _ = mzero extQ_applyQ :: Rule+extQ_applyQ _ (APPLYQ Dynamic (EXTQ f t g)) = mzero extQ_applyQ _ (APPLYQ a (EXTQ f t g)) = success "extQ-applyQ" (extQ a f t g) extQ_applyQ _ _ = mzero -gmapQ_everything :: Rule-gmapQ_everything _ (GMAPQ (EVERYTHING f)) = success "gmapQ-everything" (EVERYTHING f)-gmapQ_everything _ _ = mzero+tu :: Rule+tu = top emptyQ_applyQ ||| top union_applyQ+ ||| top gmapQ_applyQ ||| top everything_applyQ+ ||| top mkQ_applyQ ||| top extQ_applyQ+
+ src/Transform/Rules/XPath.hs view
@@ -0,0 +1,96 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Rules.XPath+-- Copyright : (c) 2010 University of Minho+-- License : BSD3+--+-- Maintainer : hpacheco@di.uminho.pt+-- Stability : experimental+-- Portability : non-portable+--+-- Pointless Rewrite:+-- automatic transformation system for point-free programs+-- +-- Generic strategy for the rewriting of point-free functions.+--+-----------------------------------------------------------------------------++module Transform.Rules.XPath where++import Transform.Rewriting+import Transform.Rules.SYB.TU+import Transform.Rules.PF.Lists+import Transform.Rules.PF.Monoids+import Transform.Rules.PF.Rec+import Transform.Rules.PF.Products+import Transform.Rules.PF.Combinators+import Transform.Rules.PF+import Data.Type+import Data.Pf+import Data.Equal+import Transform.Rules.PF.Sums++import Control.Monad+import Data.Char++child_def :: Rule+child_def _ CHILD = success "child-Def" $ GMAPQ SELF+child_def _ _ = mzero++attribute_def :: Rule+attribute_def _ ATTRIBUTE = success "attribute-Def" $ GMAPQ ATT+attribute_def _ _ = mzero++descendant_def :: Rule+descendant_def _ DESCENDANT = success "descendant-Def" $ EVERYTHING CHILD+descendant_def _ _ = mzero++descself_def :: Rule+descself_def _ DESCSELF = success "descself-Def" $ EVERYTHING SELF+descself_def _ _ = mzero++self_applyQ :: Rule+self_applyQ _ (APPLYQ Dynamic SELF) = mzero+self_applyQ _ (APPLYQ a SELF) | not (isAtt a) = success "self-ApplyQ" $ COMP Dynamic WRAP (MKDYN a)+ | otherwise = success "self-ApplyQ" ZERO+self_applyQ _ _ = mzero++att_applyQ :: Rule+att_applyQ _ (APPLYQ Dynamic ATT) = mzero+att_applyQ _ (APPLYQ a ATT) | isAtt a = success "att-ApplyQ" $ COMP Dynamic WRAP (MKDYN a)+ | otherwise = success "att-ApplyQ" ZERO+att_applyQ _ _ = mzero++name_applyQ :: Rule+name_applyQ _ (APPLYQ Dynamic (NAME n)) = mzero+name_applyQ _ (APPLYQ a@(dataName -> Just name) (NAME n)) | sameName name n = success "name-ApplyQ" $ APPLYQ a SELF+name_applyQ _ (APPLYQ a@(dataName -> Just name) (NAME n)) | sameName name ("@"++n) = success "name-ApplyQ" $ APPLYQ a ATT+name_applyQ _ (APPLYQ a (NAME n)) = success "name-ApplyQ" ZERO +name_applyQ _ _ = mzero++slash_applyQ :: Rule+slash_applyQ (Fun _ r) (APPLYQ a (f :/: g)) =+ success "comp-ApplyQ" $ COMP (List r) FOLD $ COMP (List Dynamic) (MAP $ APPLYQ Dynamic g) $ APPLYQ a f+slash_applyQ _ _ = mzero++seqQ_applyQ :: Rule+seqQ_applyQ (Fun _ s) (APPLYQ a (SEQQ (q::Pf (Q r)) f)) = let r=typeof::Type r in success "seqQ-ApplyQ" $ COMP r f $ APPLYQ a q+seqQ_applyQ _ _ = mzero++dyn_applyQ, dyn_applyQ' :: Rule+dyn_applyQ = comp dyn_applyQ'+dyn_applyQ' _ (COMP _ (APPLYQ Dynamic f) (MKDYN a)) = success "dyn-ApplyQ" $ APPLYQ a f+dyn_applyQ' _ _ = mzero++optimise_xpath :: Rule+optimise_xpath = outermost rules >>> try ((once fuse1 ||| once fuse2 ||| once sum_sfusion) >>> optimise_xpath)+ where rules, fuse1, fuse2 :: Rule+ rules = primitives ||| xpath ||| tu ||| monoids ||| lists ||| prods ||| sums ||| bangs ||| convs ||| recs+ fuse1 = top prod_fusion ||| top sum_fusion+ fuse2 = top para_cata ||| top cata_fusion ||| top para_fusion ||| top ana_fusion ||| top cata_zero++xpath = top child_def ||| top attribute_def ||| top descendant_def ||| top descself_def+ ||| top self_applyQ ||| top att_applyQ ||| top name_applyQ+ ||| top slash_applyQ ||| top seqQ_applyQ ||| top dyn_applyQ++