diff --git a/README b/README --- a/README +++ b/README @@ -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 diff --git a/pointless-rewrite.cabal b/pointless-rewrite.cabal --- a/pointless-rewrite.cabal +++ b/pointless-rewrite.cabal @@ -1,5 +1,5 @@ Name: pointless-rewrite -Version: 0.0.2 +Version: 0.0.3 License: BSD3 License-file: LICENSE Author: Alcino Cunha , Hugo Pacheco @@ -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 diff --git a/src/Data/Default.hs b/src/Data/Default.hs new file mode 100644 --- /dev/null +++ b/src/Data/Default.hs @@ -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)) + diff --git a/src/Data/Equal.hs b/src/Data/Equal.hs --- a/src/Data/Equal.hs +++ b/src/Data/Equal.hs @@ -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) diff --git a/src/Data/Equal.hs-boot b/src/Data/Equal.hs-boot new file mode 100644 --- /dev/null +++ b/src/Data/Equal.hs-boot @@ -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) diff --git a/src/Data/Eval.hs b/src/Data/Eval.hs --- a/src/Data/Eval.hs +++ b/src/Data/Eval.hs @@ -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) diff --git a/src/Data/Lens.hs b/src/Data/Lens.hs --- a/src/Data/Lens.hs +++ b/src/Data/Lens.hs @@ -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 diff --git a/src/Data/Pf.hs b/src/Data/Pf.hs new file mode 100644 --- /dev/null +++ b/src/Data/Pf.hs @@ -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)) diff --git a/src/Data/Pf.hs-boot b/src/Data/Pf.hs-boot new file mode 100644 --- /dev/null +++ b/src/Data/Pf.hs-boot @@ -0,0 +1,3 @@ +module Data.Pf where + +data Pf a where diff --git a/src/Data/Spine.hs b/src/Data/Spine.hs --- a/src/Data/Spine.hs +++ b/src/Data/Spine.hs @@ -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 "") toSpine (Pf (Lns Any Any)) e = e `As` (pcon "") -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" diff --git a/src/Data/Type.hs b/src/Data/Type.hs --- a/src/Data/Type.hs +++ b/src/Data/Type.hs @@ -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) ++ "]" diff --git a/src/Transform/Examples/Company.hs b/src/Transform/Examples/Company.hs --- a/src/Transform/Examples/Company.hs +++ b/src/Transform/Examples/Company.hs @@ -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 diff --git a/src/Transform/Examples/Imdb.hs b/src/Transform/Examples/Imdb.hs --- a/src/Transform/Examples/Imdb.hs +++ b/src/Transform/Examples/Imdb.hs @@ -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")) diff --git a/src/Transform/Examples/Women.hs b/src/Transform/Examples/Women.hs --- a/src/Transform/Examples/Women.hs +++ b/src/Transform/Examples/Women.hs @@ -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 diff --git a/src/Transform/Rewriting.hs b/src/Transform/Rewriting.hs --- a/src/Transform/Rewriting.hs +++ b/src/Transform/Rewriting.hs @@ -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) diff --git a/src/Transform/Rules/Lenses.hs b/src/Transform/Rules/Lenses.hs --- a/src/Transform/Rules/Lenses.hs +++ b/src/Transform/Rules/Lenses.hs @@ -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 diff --git a/src/Transform/Rules/Lenses.hs-boot b/src/Transform/Rules/Lenses.hs-boot --- a/src/Transform/Rules/Lenses.hs-boot +++ b/src/Transform/Rules/Lenses.hs-boot @@ -2,4 +2,6 @@ import Transform.Rewriting +optimise_all_lns :: Rule +optimise_list_lns :: Rule optimise_lns :: Rule diff --git a/src/Transform/Rules/Lenses/Combinators.hs b/src/Transform/Rules/Lenses/Combinators.hs --- a/src/Transform/Rules/Lenses/Combinators.hs +++ b/src/Transform/Rules/Lenses/Combinators.hs @@ -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 diff --git a/src/Transform/Rules/Lenses/Dists.hs b/src/Transform/Rules/Lenses/Dists.hs --- a/src/Transform/Rules/Lenses/Dists.hs +++ b/src/Transform/Rules/Lenses/Dists.hs @@ -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 diff --git a/src/Transform/Rules/Lenses/Lists.hs b/src/Transform/Rules/Lenses/Lists.hs --- a/src/Transform/Rules/Lenses/Lists.hs +++ b/src/Transform/Rules/Lenses/Lists.hs @@ -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 diff --git a/src/Transform/Rules/Lenses/Products.hs b/src/Transform/Rules/Lenses/Products.hs --- a/src/Transform/Rules/Lenses/Products.hs +++ b/src/Transform/Rules/Lenses/Products.hs @@ -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 diff --git a/src/Transform/Rules/Lenses/Rec.hs b/src/Transform/Rules/Lenses/Rec.hs --- a/src/Transform/Rules/Lenses/Rec.hs +++ b/src/Transform/Rules/Lenses/Rec.hs @@ -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)) + + + diff --git a/src/Transform/Rules/Lenses/Sums.hs b/src/Transform/Rules/Lenses/Sums.hs --- a/src/Transform/Rules/Lenses/Sums.hs +++ b/src/Transform/Rules/Lenses/Sums.hs @@ -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 diff --git a/src/Transform/Rules/PF.hs b/src/Transform/Rules/PF.hs --- a/src/Transform/Rules/PF.hs +++ b/src/Transform/Rules/PF.hs @@ -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 diff --git a/src/Transform/Rules/PF.hs-boot b/src/Transform/Rules/PF.hs-boot --- a/src/Transform/Rules/PF.hs-boot +++ b/src/Transform/Rules/PF.hs-boot @@ -1,5 +1,6 @@ module Transform.Rules.PF where import Transform.Rewriting - + +sum_sfusion :: Rule optimise_pf :: Rule diff --git a/src/Transform/Rules/PF/Combinators.hs b/src/Transform/Rules/PF/Combinators.hs --- a/src/Transform/Rules/PF/Combinators.hs +++ b/src/Transform/Rules/PF/Combinators.hs @@ -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 diff --git a/src/Transform/Rules/PF/Dists.hs b/src/Transform/Rules/PF/Dists.hs --- a/src/Transform/Rules/PF/Dists.hs +++ b/src/Transform/Rules/PF/Dists.hs @@ -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 diff --git a/src/Transform/Rules/PF/Lists.hs b/src/Transform/Rules/PF/Lists.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Rules/PF/Lists.hs @@ -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 + + + + + diff --git a/src/Transform/Rules/PF/Monoids.hs b/src/Transform/Rules/PF/Monoids.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Rules/PF/Monoids.hs @@ -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 diff --git a/src/Transform/Rules/PF/Products.hs b/src/Transform/Rules/PF/Products.hs --- a/src/Transform/Rules/PF/Products.hs +++ b/src/Transform/Rules/PF/Products.hs @@ -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 diff --git a/src/Transform/Rules/PF/Rec.hs b/src/Transform/Rules/PF/Rec.hs --- a/src/Transform/Rules/PF/Rec.hs +++ b/src/Transform/Rules/PF/Rec.hs @@ -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 diff --git a/src/Transform/Rules/PF/Sums.hs b/src/Transform/Rules/PF/Sums.hs --- a/src/Transform/Rules/PF/Sums.hs +++ b/src/Transform/Rules/PF/Sums.hs @@ -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 diff --git a/src/Transform/Rules/SYB.hs b/src/Transform/Rules/SYB.hs --- a/src/Transform/Rules/SYB.hs +++ b/src/Transform/Rules/SYB.hs @@ -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 diff --git a/src/Transform/Rules/SYB/TP.hs b/src/Transform/Rules/SYB/TP.hs --- a/src/Transform/Rules/SYB/TP.hs +++ b/src/Transform/Rules/SYB/TP.hs @@ -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 diff --git a/src/Transform/Rules/SYB/TU.hs b/src/Transform/Rules/SYB/TU.hs --- a/src/Transform/Rules/SYB/TU.hs +++ b/src/Transform/Rules/SYB/TU.hs @@ -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 + diff --git a/src/Transform/Rules/XPath.hs b/src/Transform/Rules/XPath.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Rules/XPath.hs @@ -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 + +