pointless-rewrite (empty) → 0.0.1
raw patch · 32 files changed
+4838/−0 lines, 32 filesdep +basedep +haskell98dep +mtlsetup-changed
Dependencies added: base, haskell98, mtl, pointless-haskell, pointless-lenses, process
Files
- LICENSE +31/−0
- README +11/−0
- Setup.lhs +3/−0
- Test.hs +5/−0
- pointless-rewrite.cabal +49/−0
- src/Data/Equal.hs +145/−0
- src/Data/Eval.hs +247/−0
- src/Data/Lens.hs +255/−0
- src/Data/Spine.hs +382/−0
- src/Data/Type.hs +351/−0
- src/Transform/Examples/Company.hs +140/−0
- src/Transform/Examples/Imdb.hs +64/−0
- src/Transform/Examples/Women.hs +46/−0
- src/Transform/Rewriting.hs +297/−0
- src/Transform/Rules/Lenses.hs +109/−0
- src/Transform/Rules/Lenses.hs-boot +5/−0
- src/Transform/Rules/Lenses/Combinators.hs +266/−0
- src/Transform/Rules/Lenses/Dists.hs +132/−0
- src/Transform/Rules/Lenses/Lists.hs +230/−0
- src/Transform/Rules/Lenses/Products.hs +169/−0
- src/Transform/Rules/Lenses/Rec.hs +374/−0
- src/Transform/Rules/Lenses/Sums.hs +163/−0
- src/Transform/Rules/PF.hs +63/−0
- src/Transform/Rules/PF.hs-boot +5/−0
- src/Transform/Rules/PF/Combinators.hs +350/−0
- src/Transform/Rules/PF/Dists.hs +153/−0
- src/Transform/Rules/PF/Products.hs +94/−0
- src/Transform/Rules/PF/Rec.hs +454/−0
- src/Transform/Rules/PF/Sums.hs +104/−0
- src/Transform/Rules/SYB.hs +37/−0
- src/Transform/Rules/SYB/TP.hs +53/−0
- src/Transform/Rules/SYB/TU.hs +51/−0
+ LICENSE view
@@ -0,0 +1,31 @@+Copyright (c) 2010, University of Minho++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are+met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * The names of contributors may not be used to endorse or promote+ products derived from this software without specific prior+ written permission. ++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README view
@@ -0,0 +1,11 @@+Pointless Rewrite++This cabal package can be installed with:++$ cabal install pointless-lenses++For a manual install, execute:++$ runhaskell Setup.lhs configure+$ runhaskell Setup.lhs build+$ runhaskell Setup.lhs installed
+ Setup.lhs view
@@ -0,0 +1,3 @@+#!/usr/bin/env runhaskell+> import Distribution.Simple+> main = defaultMain
+ Test.hs view
@@ -0,0 +1,5 @@+module Test where++import.Transform.Examples.Company+import Transform.Examples.Imdb+import Transform.Examples.Women
+ pointless-rewrite.cabal view
@@ -0,0 +1,49 @@+Name: pointless-rewrite+Version: 0.0.1+License: BSD3+License-file: LICENSE+Author: Alcino Cunha <alcino@di.uminho.pt>, Hugo Pacheco <hpacheco@di.uminho.pt>+Maintainer: Hugo Pacheco <hpacheco@di.uminho.pt>+Synopsis: Pointless Rewrite library+Description: Library that implements a rewrite system for point-free expressions. Application scenarios include normal functional programs, strategic combinators (<http://dx.doi.org/10.1016/j.scico.2010.01.003>) and bidirectional lenses (<http://www.di.uminho.pt/~hpacheco/publications/lensopt.pdf>), all encoded with point-free combinators.+ +Homepage: ++Category: Generics++extra-source-files: README, Test.hs++Build-type: Simple+Cabal-Version: >= 1.2.3++Library+ Hs-Source-Dirs: src+ Build-Depends: mtl >= 1, base >= 4 && < 5, pointless-haskell >= 0.0.5, pointless-lenses >= 0.0.7, haskell98, process+ exposed-modules:+ Data.Type+ Data.Spine+ Data.Equal+ Data.Eval+ Data.Lens+ Transform.Rewriting+ Transform.Rules.PF+ Transform.Rules.PF.Combinators+ Transform.Rules.PF.Dists+ Transform.Rules.PF.Products+ Transform.Rules.PF.Rec+ Transform.Rules.PF.Sums+ Transform.Rules.Lenses+ Transform.Rules.Lenses.Combinators+ Transform.Rules.Lenses.Dists+ Transform.Rules.Lenses.Products+ Transform.Rules.Lenses.Rec+ Transform.Rules.Lenses.Sums+ Transform.Rules.Lenses.Lists+ Transform.Rules.SYB.TP+ Transform.Rules.SYB.TU+ Transform.Rules.SYB+ Transform.Examples.Imdb+ Transform.Examples.Company+ Transform.Examples.Women++ extensions: ScopedTypeVariables, FlexibleContexts, Rank2Types, TypeOperators, TypeFamilies, GADTs
+ src/Data/Equal.hs view
@@ -0,0 +1,145 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.Equal+-- 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+-- +-- Implementation of type and function equality at the value-level.+--+-----------------------------------------------------------------------------++module Data.Equal where++import Data.Type+import Data.Spine++import Control.Monad hiding (Functor(..))+import Unsafe.Coerce++import Generics.Pointless.Functors++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+ return Eq+teq (Either a b) (Either c d) = do+ Eq <- teq a c+ Eq <- teq b d+ return Eq+teq (Data s fx) (Data s' fy) = do+ guard (s == s')+ Eq <- feq fx fy+ return (unsafeCoerce Eq)+teq (Fun a b) (Fun c d) = do+ Eq <- teq a c+ Eq <- teq b d+ return Eq+teq (Lns a b) (Lns c d) = do+ Eq <- teq a c+ Eq <- teq b d+ return Eq+teq (Pf a) (Pf b) = do+ Eq <- teq a b+ return Eq+teq Dynamic Dynamic = error "dynamic equality"+teq TP TP = return Eq+teq (TU a) (TU b) = do+ Eq <- teq a b+ return Eq+teq _ _ = 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+ return Eq+feq L L = return Eq+feq (f :*!: g) (h :*!: i) = do+ Eq <- feq f h+ Eq <- feq g i+ return Eq+feq (f :+!: g) (h :+!: i) = do+ Eq <- feq f h+ Eq <- feq g i+ return Eq+feq (f :@!: g) (h :@!: i) = do+ Eq <- feq f h+ Eq <- feq g i+ return Eq+feq _ _ = mzero++-- | 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+geq (Pf t) x (PROTECT y) = geq (Pf t) x y+geq (Pf t) (PROTECT_LNS x) y = geq (Pf t) x y+geq (Pf t) x (PROTECT_LNS y) = geq (Pf t) x y+geq t x y = geq' t x t y++geq' :: Type a -> a -> Type b -> b -> Bool+geq' a x b y = aux a b x y+ where aux :: Type a -> Type b -> a -> b -> Bool+ aux t1 t2 x y = aux' t1 (toSpine t1 x) t2 (toSpine t2 y)+ aux' :: Type a -> Spine a -> Type b -> Spine b -> Bool+ aux' _ (_ `As` c1) _ (_ `As` c2) = name c1 == name c2+ 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++-- | Clone of |geq| with a specific case for top.+geqt :: Type a -> a -> a -> Bool+geqt (Pf t) (PROTECT x) y = geqt (Pf t) x y+geqt (Pf t) x (PROTECT y) = geqt (Pf t) x y+geqt (Pf t) (PROTECT_LNS x) y = geqt (Pf t) x y+geqt (Pf t) x (PROTECT_LNS y) = geqt (Pf t) x y+geqt t x y = geqt' t x t y++geqt' :: Type a -> a -> Type b -> b -> Bool+geqt' a x b y = aux a b x y+ where aux :: Type a -> Type b -> a -> b -> Bool+ aux t1 t2 x y = aux' t1 (toSpine t1 x) t2 (toSpine t2 y)+ aux' :: Type a -> Spine a -> Type b -> Spine b -> Bool+ aux' _ _ (Pf _) (TOP `As` _) = True+ aux' (Pf _) (As TOP _) _ _ = True+ aux' _ (_ `As` c1) _ (_ `As` c2) = name c1 == name c2+ 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++coerce :: MonadPlus m => Type a -> Type b -> a -> m b+coerce a b x = do Eq <- teq a b+ return x++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+ findSpine t (As v con) = case teq t b of {+ Just Eq -> geqt t v y;+ otherwise -> False+ }+ findSpine t s@(Ap f (a :| v)) = (case teq t b of {+ Just Eq -> geqt b y (spineVal 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
+ src/Data/Eval.hs view
@@ -0,0 +1,247 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.Eval+-- 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+-- +-- Evaluation of point-free representations.+--+-----------------------------------------------------------------------------++module Data.Eval where+ +import Prelude hiding (Functor(..))+import Data.Type+import Data.Equal++import Data.Monoid++import Generics.Pointless.Combinators+import Generics.Pointless.RecursionPatterns+import Generics.Pointless.Functors+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.Recs++fctrT :: Functor f => Fctr f -> F.Fctr f+fctrT I = F.I+fctrT (K c) = F.K+fctrT (f :*!: g) = fctrT f F.:*!: fctrT g+fctrT (f :+!: g) = fctrT f F.:+!: fctrT g+fctrT (f :@!: g) = fctrT f F.:@!: fctrT g++inn_lnsF :: Mu a => Fctr f -> Lens (F a a) a+inn_lnsF f = Lens inn (out . fst) out++out_lnsF :: Mu a => Fctr f -> Lens a (F a a)+out_lnsF f = Lens out (inn . fst) inn++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)+ 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'+ where get' = ana b (get l)+ put' = accum b (put l) (fzip (fctrT 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'+ where get' = cata a (get l)+ put' = ana a (fzip (fctrT 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 _ TOP = error "top"+eval (Fun _ _) (FUN _ f) = f+eval (Lns _ _) (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++eval (Fun a b) (PNT v) = const v+eval (Fun _ _) BANG = bang+eval (Fun a c) (COMP b f g) = eval (Fun b c) f . eval (Fun a b) g+eval (Fun _ _) FST = fst+eval (Fun _ _) SND = snd+eval (Fun a (Prod b c)) (SPLIT f g) = eval (Fun a b) f /\ eval (Fun a c) g+eval (Fun (Prod a b) (Prod c d)) (PROD f g) = eval (Fun a c) f >< eval (Fun b d) g+eval (Fun _ _) INL = inl+eval (Fun _ _) INR = inr+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 _ ZERO = const mempty+eval _ PLUS = uncurry mappend++eval (Fun _ _) ID = id+eval (Fun _ _) SWAP = swap+eval (Fun _ _) COSWAP = coswap+eval (Fun _ _) DISTL = distl+eval (Fun _ _) UNDISTL = undistl+eval (Fun _ _) DISTR = distr+eval (Fun _ _) UNDISTR = undistr+eval (Fun _ _) ASSOCL = assocl+eval (Fun _ _) ASSOCR = assocr+eval (Fun _ _) COASSOCL = coassocl+eval (Fun _ _) COASSOCR = coassocr++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 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)++eval (Lns c a) (COMP_LNS b f g) = eval (Lns b a) f .< eval (Lns c b) g+eval (Lns (Prod a b) _) (FST_LNS f) = fst_lns $ eval (Fun a b) f+eval (Lns (Prod a b) _) (SND_LNS f) = snd_lns $ eval (Fun b a) f+eval (Lns (Prod a b) (Prod c d)) (PROD_LNS f g) = eval (Lns a c) f ><< eval (Lns b d) g+eval (Lns (Either a b) c) (EITHER_LNS x f g) = (\/<) (eval (Fun c (Either One One)) x) (eval (Lns a c) f) (eval (Lns b c) g)+eval (Lns (Either a b) (Either c d)) (SUM_LNS f g) = eval (Lns a c) f -|-< eval (Lns b d) g+eval (Lns (Either a b) (Either c d)) (SUMW_LNS f g l1 l2) = sum_lns f' g' (eval (Lns a c) l1) (eval (Lns b d) l2)+ where f' = eval (Fun (Prod c b) a) f+ g' = eval (Fun (Prod d a) b) g+eval (Lns a One) (BANG_LNS f) = (!<) (eval (Fun One a) f)+eval (Lns c _) BANGL_LNS = (!/\<) id_lns+eval (Lns c _) BANGR_LNS = (/\!<) id_lns++eval (Lns _ _) ID_LNS = id_lns+eval (Lns _ _) SWAP_LNS = swap_lns+eval (Lns _ _) COSWAP_LNS = coswap_lns+eval (Lns _ _) DISTL_LNS = distl_lns+eval (Lns _ _) UNDISTL_LNS = undistl_lns+eval (Lns _ _) DISTR_LNS = distr_lns+eval (Lns _ _) UNDISTR_LNS = undistr_lns+eval (Lns _ _) ASSOCL_LNS = assocl_lns+eval (Lns _ _) ASSOCR_LNS = assocr_lns+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 _ _) (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 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 _ _) 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 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)+eval p (APPLY a (EXTT f t g)) = eval p (extT a f t g)+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 a r)(APPLYQ _ (GMAPQ f)) = eval q (gmapQ r a f)+eval q (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++everywhereEval t f = APPLY t (f `SEQ` ALL (EVERYWHERE f))+everywhereEval' t f = APPLY t (ALL (EVERYWHERE' f) `SEQ` f)+everythingEval t f = APPLYQ t (f `UNION` GMAPQ (EVERYTHING f))++-- ** Type-preserving specialization++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++-- | 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)++-- | 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))++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}++extT :: Type x -> Pf T -> Type a -> Pf (a -> a) -> Pf (x -> x)+extT t f x g = case teq t x of {Just Eq -> g; otherwise -> APPLY t f}++-- ** 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++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}++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 (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 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++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))+++mkQ :: Monoid r => Type a -> Type x -> Pf (x -> r) -> Pf (a -> r)+mkQ a x f = case teq a x of {Just Eq -> f; otherwise -> ZERO}++extQ :: Type x -> Pf (Q r) -> Type a -> Pf (a -> r) -> Pf (x -> r)+extQ t f x g = case teq t x of {Just Eq -> g; otherwise -> APPLYQ t f}+
+ src/Data/Lens.hs view
@@ -0,0 +1,255 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.Lens+-- 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+-- +-- Evaluation of point-free lens representations.+--+-----------------------------------------------------------------------------++module Data.Lens where++import Data.Type+import Data.Equal++import Prelude hiding (Functor(..))+import Control.Monad hiding (Functor(..))++import Generics.Pointless.Functors+import Generics.Pointless.Lenses++-- | Computes the inverse lens for isomorphic lenses.+inv :: MonadPlus m => Type (Lens a b) -> Pf (Lens a b) -> m (Pf (Lens b a))+inv _ ID_LNS = return ID_LNS+inv (Lns c a) (COMP_LNS b f g) = do+ g' <- inv (Lns c b) g+ f' <- inv (Lns b a) f+ return $ COMP_LNS b g' f'+inv (Lns (Prod a b) (Prod c d)) (f `PROD_LNS` g) = do+ f' <- inv (Lns a c) f+ g' <- inv (Lns b d) g+ return $ f' ><<< g'+inv (Lns (Either a b) (Either c d)) (f `SUM_LNS` g) = do+ f' <- inv (Lns a c) f+ g' <- inv (Lns b d) g+ return $ f' -|-<< g'+inv (Lns c (Prod One _)) BANGL_LNS =+ return $ SND_LNS BANG+inv (Lns c (Prod _ One)) (BANGR_LNS) =+ return $ FST_LNS BANG+inv _ SWAP_LNS = return SWAP_LNS+inv _ COSWAP_LNS = return COSWAP_LNS+inv _ DISTL_LNS = return UNDISTL_LNS+inv _ UNDISTL_LNS = return DISTL_LNS+inv _ DISTR_LNS = return UNDISTR_LNS+inv _ UNDISTR_LNS = return DISTR_LNS+inv _ ASSOCL_LNS = return ASSOCR_LNS+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)))+ ; 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))+ ; 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++lns (Fun a c) (COMP b f g) = do+ f' <- lns (Fun b c) f+ g' <- lns (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+ 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+ 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+ 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+ return $ f' `SUM_LNS` g'+lns (Fun _ _) BANG = return $ BANG_LNS HOLE+ +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++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+ return $ FMAP_LNS fctr t f'+lns (Fun a b@(Data s fctr)) (ANA f) = do+ f' <- lns (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+ return $ CATA_LNS f'+lns _ _ = mzero++getof :: Type (Lens c a) -> Pf (Lens c a) -> Pf (c -> a)+getof (Lns _ _) (LNS s l) = FUN (showL ["get",s]) $ get l++getof (Lns c a) (COMP_LNS b f g) = COMP b (getof (Lns b a) f) (getof (Lns c b) g)+getof (Lns _ _) (FST_LNS f) = FST+getof (Lns _ _) (SND_LNS f) = SND+getof (Lns (Prod a b) (Prod c d)) (PROD_LNS f g) = getof (Lns a c) f ><= getof (Lns b d) g+getof (Lns (Either a b) c) (EITHER_LNS x f g) = getof (Lns a c) f \/= getof (Lns b c) g+getof (Lns (Either c d) (Either a b)) (SUM_LNS f g) = getof (Lns c a) f -|-= getof (Lns d b) g+getof (Lns (Either c d) (Either a b)) (SUMW_LNS h i f g) = getof (Lns c a) f -|-= getof (Lns d b) g+getof (Lns c One) (BANG_LNS f) = BANG+getof (Lns c (Prod One _)) (BANGL_LNS) = BANG /\= ID+getof (Lns c (Prod _ One)) (BANGR_LNS) = ID /\= BANG++getof (Lns _ _) ID_LNS = ID+getof (Lns _ _) SWAP_LNS = SWAP+getof (Lns _ _) COSWAP_LNS = COSWAP+getof (Lns _ _) DISTL_LNS = DISTL+getof (Lns _ _) UNDISTL_LNS = UNDISTL+getof (Lns _ _) DISTR_LNS = DISTR+getof (Lns _ _) UNDISTR_LNS = UNDISTR+getof (Lns _ _) ASSOCL_LNS = ASSOCL+getof (Lns _ _) ASSOCR_LNS = ASSOCR+getof (Lns _ _) COASSOCL_LNS = COASSOCL+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))+ ; 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 _ f = GET f++createof :: Type (Lens c a) -> Pf (Lens c a) -> Pf (a -> c)+createof (Lns _ _) (LNS s l) = FUN (showL ["create",s]) $ create l++createof (Lns c a) (COMP_LNS b f g) = COMP b (createof (Lns c b) g) (createof (Lns b a) f)+createof (Lns _ _) (FST_LNS f) = ID /\= f+createof (Lns _ _) (SND_LNS f) = f /\= ID+createof (Lns (Prod a b) (Prod c d)) (PROD_LNS f g) = createof (Lns a c) f ><= createof (Lns b d) g+createof (Lns (Either a b) c) (EITHER_LNS x f g) = COMP t' (l -|-= r) $ COMP t DISTL (x /\= ID)+ where l = COMP c (createof (Lns a c) f) SND+ r = COMP c (createof (Lns b c) g) SND+ t = Prod (Either One One) c+ t' = Either (Prod One c) (Prod One c)+createof (Lns (Either c d) (Either a b)) (SUM_LNS f g) = createof (Lns c a) f -|-= createof (Lns d b) g+createof (Lns (Either c d) (Either a b)) (SUMW_LNS h i f g) = createof (Lns c a) f -|-= createof (Lns d b) g+createof (Lns c One) (BANG_LNS f) = f+createof (Lns c (Prod One _)) (BANGL_LNS) = SND+createof (Lns c (Prod _ One)) (BANGR_LNS) = FST++createof (Lns _ _) ID_LNS = ID+createof (Lns _ _) SWAP_LNS = SWAP+createof (Lns _ _) COSWAP_LNS = COSWAP+createof (Lns _ _) DISTL_LNS = UNDISTL+createof (Lns _ _) UNDISTL_LNS = DISTL+createof (Lns _ _) DISTR_LNS = UNDISTR+createof (Lns _ _) UNDISTR_LNS = DISTR+createof (Lns _ _) ASSOCL_LNS = ASSOCR+createof (Lns _ _) ASSOCR_LNS = ASSOCL+createof (Lns _ _) COASSOCL_LNS = COASSOCR+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))+ ; 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++putof :: Type (Lens c a) -> Pf (Lens c a) -> Pf ((a,c) -> c)+putof (Lns _ _) (LNS s l) = FUN (showL ["put",s]) $ put l++putof (Lns c a) (COMP_LNS b f g) = COMP t (putof (Lns c b) g)+ ((COMP t' (putof (Lns b a) f) (ID ><= (getof (Lns c b) g))) /\= SND)+ where t = Prod b c+ t' = Prod a b+putof (Lns _ _) (FST_LNS f) = ID ><= SND+putof (Lns (Prod a b) _) (SND_LNS va) = COMP (Prod b a) SWAP (ID ><= FST)+putof (Lns (Prod a b) (Prod c d)) (PROD_LNS f g) = COMP t (putof (Lns a c) f ><= putof (Lns b d) g) distp_pf+ where t = Prod (Prod c a) (Prod d b)+putof (Lns (Either a b) c) (EITHER_LNS x f g) = COMP t (putof (Lns a c) f -|-= putof (Lns b c) g) DISTR+ where t = Either (Prod c a) (Prod c b)+putof (Lns (Either c d) (Either a b)) (SUM_LNS f g) = COMP t (l -|-= r) (dists_pf (Prod (Either a b) (Either c d)))+ where l = putof (Lns c a) f \/= COMP a (createof (Lns c a) f) FST+ r = COMP b (createof (Lns d b) g) FST \/= putof (Lns d b) g+ t = Either (Either (Prod a c) (Prod a d)) (Either (Prod b c) (Prod b d))+putof (Lns (Either c d) (Either a b)) (SUMW_LNS h i f g) = COMP t (putof (Lns c a) f -|-= putof (Lns d b) g) $+ COMP t' (l -|-= r) (dists_pf (Prod (Either a b) (Either c d)))+ where l = ID \/= (FST /\= h)+ r = (FST /\= i) \/= ID+ t = Either (Prod a c) (Prod b d)+ t' = Either (Either (Prod a c) (Prod a d)) (Either (Prod b c) (Prod b d))+putof (Lns c One) (BANG_LNS f) = SND+putof (Lns c (Prod One _)) (BANGL_LNS) = COMP (Prod One c) SND FST+putof (Lns c (Prod _ One)) (BANGR_LNS) = COMP (Prod c One) FST FST++putof (Lns c a) ID_LNS = COMP a (createof (Lns c a) ID_LNS) FST+putof (Lns c a) SWAP_LNS = COMP a (createof (Lns c a) SWAP_LNS) FST+putof (Lns c a) COSWAP_LNS = COMP a (createof (Lns c a) COSWAP_LNS) FST+putof (Lns c a) DISTL_LNS = COMP a (createof (Lns c a) DISTL_LNS) FST+putof (Lns c a) UNDISTL_LNS = COMP a (createof (Lns c a) UNDISTL_LNS) FST+putof (Lns c a) DISTR_LNS = COMP a (createof (Lns c a) DISTR_LNS) FST+putof (Lns c a) UNDISTR_LNS = COMP a (createof (Lns c a) UNDISTR_LNS) FST+putof (Lns c a) ASSOCL_LNS = COMP a (createof (Lns c a) ASSOCL_LNS) FST+putof (Lns c a) ASSOCR_LNS = COMP a (createof (Lns c a) ASSOCR_LNS) FST+putof (Lns c a) COASSOCL_LNS = COMP a (createof (Lns c a) COASSOCL_LNS) FST+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+ ; 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+ 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)+ 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 _ _) f = PUT f
+ src/Data/Spine.hs view
@@ -0,0 +1,382 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.Spine+-- 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+-- +-- Representation of spines for generic programming a la SYB revolutions.+--+-----------------------------------------------------------------------------++module Data.Spine where++import Data.Type++import Data.Monoid hiding (Any)++import Generics.Pointless.Functors+import Generics.Pointless.Combinators++-- * A spine representation for data values à la SYB revolutions++data Typed a = Type a :| a++data Spine a where+ As :: a -> Con -> Spine a+ Ap :: Spine (a -> b) -> Typed a -> Spine b++data Fixity = Prefix | Infix deriving Eq++data Con = Con {name :: String, fixity :: Fixity}++scon n = Con {name = show n, fixity = Prefix}+pcon s = Con {name = s, fixity = Prefix}+icon s = Con {name = s, fixity = Infix}++-- | Converting from a spine to a value+fromSpine :: Spine a -> a+fromSpine (c `As` _) = c+fromSpine (Ap f (_ :| a)) = (fromSpine f) a++-- | 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 Int n = n `As` (scon n)+toSpine Bool n = n `As` (scon n)+toSpine Char n = n `As` (scon n)+toSpine One x = x `As` (pcon "(_L::One)")+toSpine (Either a _) (Left x) = Left `As` (pcon "Left")+ `Ap` (a :| x)+toSpine (Either _ b) (Right y) = Right `As` (pcon "Right")+ `Ap` (b :| y)+toSpine (Prod a b) (x,y) = (,) `As` (icon ",")+ `Ap` (a :| x)+ `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)+ `Ap` ((rep fctr a) :| out v)+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 _) 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")+ `Ap` (Pf (Fun c a) :| f)+toSpine (Pf (Fun a c)) (CONV e@(Right _) f) = CONV e `As` (pcon "rconv")+ `Ap` (Pf (Fun c a) :| f)+toSpine (Pf (Lns a c)) (CONV_LNS e@(Left _) f) = CONV_LNS e `As` (pcon "lconv")+ `Ap` (Pf (Lns c a) :| f)+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 _ _)) BANG = BANG `As` (pcon "bang")+toSpine (Pf (Fun a c)) (COMP b f g) = COMP b `As` (icon ".")+ `Ap` (Pf (Fun b c) :| f)+ `Ap` (Pf (Fun a b) :| g)+toSpine (Pf (Fun _ _)) FST = FST `As` (pcon "fst")+toSpine (Pf (Fun _ _)) SND = SND `As` (pcon "snd")+toSpine (Pf (Fun a (Prod b c))) (SPLIT f g) = SPLIT `As` (icon "/\\")+ `Ap` (Pf (Fun a b) :| f)+ `Ap` (Pf (Fun a c) :| g)+toSpine (Pf (Fun (Prod a b) (Prod c d))) (PROD f g) = PROD `As` (icon "><")+ `Ap` (Pf (Fun a c) :| f)+ `Ap` (Pf (Fun b d) :| g)+toSpine (Pf (Fun _ _)) INL = INL `As` (pcon "inl")+toSpine (Pf (Fun _ _)) INR = INR `As` (pcon "inr")+toSpine (Pf (Fun (Either a b) c)) (EITHER f g) = EITHER `As` (icon "\\/")+ `Ap` (Pf (Fun a c) :| f)+ `Ap` (Pf (Fun b c) :| g)+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 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 (Fun _ _)) ID = ID `As` (pcon "id") +toSpine (Pf (Fun _ _)) SWAP = SWAP `As` (pcon "swap") +toSpine (Pf (Fun _ _)) COSWAP = COSWAP `As` (pcon "coswap") +toSpine (Pf (Fun _ _)) DISTL = DISTL `As` (pcon "distl")+toSpine (Pf (Fun _ _)) UNDISTL = UNDISTL `As` (pcon "undistl")+toSpine (Pf (Fun _ _)) DISTR = DISTR `As` (pcon "distr") +toSpine (Pf (Fun _ _)) UNDISTR = UNDISTR `As` (pcon "undistr") +toSpine (Pf (Fun _ _)) ASSOCL = ASSOCL `As` (pcon "assocl") +toSpine (Pf (Fun _ _)) ASSOCR = ASSOCR `As` (pcon "assocr") +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")+ `Ap` (Pf (Fun a c) :| f)+toSpine (Pf (Fun _ _)) (FZIP fctr t f) = FZIP fctr t `As` (pcon $ "fzip")+ `Ap` (Pf t :| f)+toSpine (Pf (Fun a b@(Data 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)+ `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 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")+ `Ap` (Pf (Lns c a) :| l)+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 ".<")+ `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")+ `Ap` (Pf (Fun a b) :| f)+toSpine (Pf (Lns (Prod a b) _)) (SND_LNS f) = SND_LNS `As` (pcon "snd_lns")+ `Ap` (Pf (Fun b a) :| f)+toSpine (Pf (Lns (Prod c d) (Prod a b))) (PROD_LNS f g) = PROD_LNS `As` (icon "><<")+ `Ap` (Pf (Lns c a) :| f)+ `Ap` (Pf (Lns d b) :| g)+toSpine (Pf (Lns (Either a b) c)) (EITHER_LNS x f g) = EITHER_LNS `As` (icon "\\/<")+ `Ap` (Pf (Fun c (Either One One)) :| x)+ `Ap` (Pf (Lns a c) :| f)+ `Ap` (Pf (Lns b c) :| g)+toSpine (Pf (Lns (Either c d) (Either a b))) (SUM_LNS f g) = SUM_LNS `As` (icon "-|-<")+ `Ap` (Pf (Lns c a) :| f)+ `Ap` (Pf (Lns d b) :| g)+toSpine (Pf (Lns (Either c d) (Either a b))) (SUMW_LNS x y f g) = SUMW_LNS `As` (pcon "sum_lns")+ `Ap` (Pf (Fun (Prod a d) c) :| x)+ `Ap` (Pf (Fun (Prod b c) d) :| y)+ `Ap` (Pf (Lns c a) :| f)+ `Ap` (Pf (Lns d b) :| g)+toSpine (Pf (Lns c One)) (BANG_LNS f) = BANG_LNS `As` (pcon "(!<)")+ `Ap` (Pf (Fun One c) :| f)+toSpine (Pf (Lns c (Prod One _))) (BANGL_LNS) = BANGL_LNS `As` (pcon "bangl")+toSpine (Pf (Lns c (Prod _ One))) (BANGR_LNS) = BANGR_LNS `As` (pcon "bangr")++toSpine (Pf (Lns _ _)) ID_LNS = ID_LNS `As` (pcon "id_lns")+toSpine (Pf (Lns _ _)) SWAP_LNS = SWAP_LNS `As` (pcon "swap_lns")+toSpine (Pf (Lns _ _)) COSWAP_LNS = COSWAP_LNS `As` (pcon "coswap_lns")+toSpine (Pf (Lns _ _)) DISTL_LNS = DISTL_LNS `As` (pcon "distl_lns")+toSpine (Pf (Lns _ _)) UNDISTL_LNS = UNDISTL_LNS `As` (pcon "undistl_lns")+toSpine (Pf (Lns _ _)) DISTR_LNS = DISTR_LNS `As` (pcon "distr_lns")+toSpine (Pf (Lns _ _)) UNDISTR_LNS = UNDISTR_LNS `As` (pcon "undistr_lns")+toSpine (Pf (Lns _ _)) ASSOCL_LNS = ASSOCL_LNS `As` (pcon "assocl_lns")+toSpine (Pf (Lns _ _)) ASSOCR_LNS = ASSOCR_LNS `As` (pcon "assocr_lns")+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)+ `Ap` (Pf (Lns c a) :| f)+toSpine (Pf (Lns a b@(Data 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")+ `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 _ _)) 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 _) (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 _) 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 _) (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 _) 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) (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 (Fun Any Any)) e = e `As` (pcon "<anyfunc>")+toSpine (Pf (Lns Any Any)) e = e `As` (pcon "<anylens>")+toSpine (Pf t) f = error $ "toSpine: " ++ show t ++ " " ++ safeShow f++instance Show (Type a) where+ show Any = "Any"+ show (Id a) = showL["Id",show a]+ show Int = "Int"+ show Bool = "Bool"+ show Char = "Char"+ show One = "One"+ show (Either x y) = showL ["Either",show x,show y]+ 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 (Data s f) = s+ show (Pf a) = showL ["Pf",show a]+ show (Dynamic) = "Dynamic"+ show TP = "TP"+ show (TU a) = showL ["TU",show a]+ +instance Show Dynamic where+ show (Dyn t v) = gshow t v++instance Show (Fctr f) where+ show I = "Id"+ show (K t) = showL ["K",show t]+ show L = "L"+ show (f:*!:g) = showL [show f,":*:",show g]+ show (f:+!:g) = showL [show f,":+:",show g]+ show (f:@!:g) = showL [show f,":@:",show g]++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 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 ++ ")"+gshow t x = showSpine (toSpine t x)+ where showSpine :: Spine a -> String+ showSpine (Ap f@(Ap (_ `As` c) (a :| x)) (b :| y))+ | fixity c == Infix = showL [gshow a x,name c,gshow b y]+ | otherwise = showL [showSpine f,gshow b y]+ showSpine (_ `As` c) = name c+ showSpine (Ap f (t :| a)) = showL [showSpine f,gshow t a]++showComp :: Type a -> a -> String+showComp (Pf (Fun a c)) (COMP b f g) = showComp (Pf $ Fun b c) f ++ " . " ++ showComp (Pf $ Fun a b) g+showComp (Pf (Lns a c)) (COMP_LNS b f g) = showComp (Pf $ Lns b c) f ++ " .< " ++ showComp (Pf $ Lns a b) g+showComp t f = gshow t f++safeShow :: Pf a -> String+safeShow HOLE = "_L"+safeShow TOP = "T"+safeShow (FUN s f) = s+safeShow (CONV e f) = showL ["conv",show e,safeShow f]+safeShow (CONV_LNS e f) = showL ["lconv",show e,safeShow f]+safeShow (LNS s l) = s+safeShow (COMPF fctr _ f g) = showL ["compf",show fctr,safeShow f,safeShow g]+safeShow (COMPF_LNS fctr _ f g) = showL ["compf_lns",show fctr,safeShow f,safeShow g]+safeShow (PROTECT f) = showL ["protect",safeShow f] +safeShow (PROTECT_LNS f) = showL ["protect_lns",safeShow f]+safeShow (VAR s) = s++safeShow (PNT v) = showL ["pnt"]+safeShow BANG = "bang"+safeShow (COMP _ f g) = showL [safeShow f,".",safeShow g]+safeShow FST = "fst"+safeShow SND = "snd"+safeShow (SPLIT f g) = showL [safeShow f,"/\\",safeShow g]+safeShow (PROD f g) = showL [safeShow f,"><",safeShow g]+safeShow INL = "inl"+safeShow INR = "inr"+safeShow (EITHER f g) = showL [safeShow f,"\\/",safeShow g]+safeShow (SUM f g) = showL [safeShow f,"-|-",safeShow g]++safeShow ID = "id"+safeShow SWAP = "swap" +safeShow COSWAP = "coswap" +safeShow DISTL = "distl"+safeShow UNDISTL = "undistl"+safeShow DISTR = "distr"+safeShow UNDISTR = "undistr"+safeShow ASSOCL = "assocl" +safeShow ASSOCR = "assocr"+safeShow COASSOCL = "coassocl"+safeShow COASSOCR = "coassocr"+ +safeShow INN = "inn" +safeShow OUT = "out"+safeShow (FMAP _ _ f) = showL ["fmap",safeShow f]+safeShow (FZIP _ _ f) = showL ["fzip",safeShow f]+safeShow (ANA f) = showL ["ana",safeShow f]+safeShow (CATA f) = showL ["cata",safeShow f]++safeShow (GET f) = showL ["get",safeShow f]+safeShow (PUT f) = showL ["put",safeShow f] +safeShow (CREATE f) = showL ["create",safeShow f]++safeShow (COMP_LNS _ f g) = showL [safeShow f,".<",safeShow g]+safeShow (FST_LNS v) = showL ["fst_lns",safeShow v]+safeShow (SND_LNS v) = showL ["snd_lns",safeShow v] +safeShow (PROD_LNS f g) = showL [safeShow f,"><<",safeShow g]+safeShow (EITHER_LNS x f g) = showL [safeShow x,safeShow f,"\\/<",safeShow g]+safeShow (SUM_LNS f g) = showL [safeShow f,"-|-<",safeShow g] +safeShow (SUMW_LNS x y f g) = showL ["sum_lns",safeShow x,safeShow y,safeShow f,safeShow g] +safeShow (BANG_LNS v) = showL ["bang_lns",safeShow v]+safeShow (BANGL_LNS) = "bangl"+safeShow (BANGR_LNS) = "bangr"+ +safeShow ID_LNS = "id_lns"+safeShow SWAP_LNS = "swap_lns"+safeShow COSWAP_LNS = "coswap_lns"+safeShow DISTL_LNS = "distl_lns"+safeShow UNDISTL_LNS = "undistl_lns"+safeShow DISTR_LNS = "distr_lns"+safeShow UNDISTR_LNS = "undistr_lns"+safeShow ASSOCL_LNS = "assocl_lns"+safeShow ASSOCR_LNS = "assocr_lns"+safeShow COASSOCL_LNS = "coassocl_lns"+safeShow COASSOCR_LNS = "coassocr_lns"+ +safeShow INN_LNS = "inn_lns"+safeShow OUT_LNS = "out_lns"+safeShow (FMAP_LNS _ _ f) = showL ["fmap",safeShow f] +safeShow (ANA_LNS f) = showL ["ana_lns",safeShow f]+safeShow (CATA_LNS f) = showL ["cata_lns",safeShow f]++safeShow (MAP_LNS f) = showL ["map_lns",safeShow f]+safeShow (LENGTH_LNS f) = showL ["length_lns"] +safeShow FILTER_LEFT_LNS = "filter_left_lns"+safeShow FILTER_RIGHT_LNS = "filter_right_lns"+safeShow CAT_LNS = "cat_lns" +safeShow CONCAT_LNS = "concat_lns"+safeShow PLUS_LNS = "plus_lns"+safeShow (SUML_LNS) = "suml_lns"
+ src/Data/Type.hs view
@@ -0,0 +1,351 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.Type+-- 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.Type where++import Prelude hiding (Functor(..))+import Data.Monoid++import Generics.Pointless.Combinators+import Generics.Pointless.Functors+import Generics.Pointless.Lenses++-- * 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 + Id :: Type a -> Type a++ -- Non-recursive+ Int :: Type Int+ Bool :: Type Bool+ Char :: Type Char+ One :: Type One+ Either :: Type a -> Type b -> Type (Either a b)+ Prod :: Type a -> Type b -> Type (a,b)+ Fun :: Type a -> Type b -> Type (a -> b)+ Lns :: Type a -> Type b -> Type (Lens a b)+ + -- Recursive+ Data :: (Mu a,Functor (PF a)) => String -> Fctr (PF a) -> Type a+ + Pf :: Type a -> Type (Pf a)+ Dynamic :: Type Dynamic+ + -- Types for SYB generic programming+ TP :: Type T+ TU :: Type a -> Type (Q a)++instance Monoid Int where+ mempty = 0+ mappend = (+)+ mconcat = foldr (+) 0++data Dynamic where+ Dyn :: Type a -> a -> Dynamic++newtype T = T {unT :: GenericT}+type GenericT = forall a . Type a -> a -> a++newtype Q r = Q {unQ :: GenericQ r}+type GenericQ r = forall a . Type a -> a -> r++class Typeable a where+ typeof :: Type a++instance Typeable Int where+ typeof = Int+ +instance Typeable Bool where+ typeof = Bool+ +instance Typeable Char where+ typeof = Char+ +instance Typeable One where+ typeof = One++instance (Typeable a,Typeable b) => Typeable (Either a b) where+ typeof = Either typeof typeof+ +instance (Typeable a,Typeable b) => Typeable (a,b) where+ typeof = Prod typeof typeof++instance (Typeable a, Typeable b) => Typeable (a -> b) where+ typeof = Fun typeof typeof++instance (Typeable a,Typeable b) => Typeable (Lens a b) where+ typeof = Lns typeof typeof++instance Typeable a => Typeable (Pf a) where+ typeof = Pf typeof++instance Typeable T where+ typeof = TP++instance Typeable r => Typeable (Q r) where+ typeof = TU typeof++instance Typeable Nat where+ typeof = nat++instance Typeable a => Typeable [a] where+ 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++instance Typeable a => Typeable (Maybe a) where+ typeof = Data "Maybe" fctrof++instance (Fctrable f) => Typeable (Fix f) where+ typeof = fixof fctrof++-- | Functor GADT for polytypic recursive functions.+-- At the moment it does not rely on a @Typeable@ instance for constants.+data Fctr (f :: * -> *) where+ I :: Fctr Id+ K :: Type c -> Fctr (Const c)+ L :: Fctr []+ (:*!:) :: (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)++rep :: Fctr f -> Type a -> Type (Rep f a)+rep I a = 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+ fctrof :: Fctr f+instance Fctrable Id where+ fctrof = I+instance Typeable c => Fctrable (Const c) where+ fctrof = K typeof+instance Fctrable [] where+ fctrof = L+instance (Functor f,Fctrable f,Functor g,Fctrable g) => Fctrable (f :*: g) where+ fctrof = (:*!:) fctrof fctrof+instance (Functor f,Fctrable f,Functor g,Fctrable g) => Fctrable (f :+: g) where+ fctrof = (:+!:) fctrof fctrof+instance (Functor f,Fctrable f,Functor g,Fctrable g) => Fctrable (f :@: g) where+ fctrof = (:@!:) fctrof fctrof++fixof :: (Functor f) => Fctr f -> Type (Fix f)+fixof f = Data "" f++fixF :: Fctr f -> Fix f+fixF (_::Fctr f) = (_L :: Fix f)++fctrofF :: Fctrable f => Fix f -> Fctr f+fctrofF (_::Fix f) = fctrof :: Fctr f++showL :: [String] -> String+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
+ src/Transform/Examples/Company.hs view
@@ -0,0 +1,140 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Examples.Company+-- 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+-- +-- Company strategic specialization example+--+-----------------------------------------------------------------------------++module Transform.Examples.Company where++import Data.Type+import Data.Eval+import Transform.Rewriting+import Transform.Rules.SYB+import Transform.Rules.PF++import Generics.Pointless.Functors++-- * Type Definitions++data Company = C [Dept] deriving Show+data Dept = D Name Manager [Either Employee Dept] deriving Show+data Employee = E Person Salary deriving Show+data Person = P Name Address deriving Show+data Salary = S Int deriving Show+type Manager = Employee +type Name = String +type Address = String++-- * Type Instances++type instance PF Company = Const [Dept]+type instance PF Dept = Const Name :*: (Const Manager :*: ([] :@: (Const Employee :+: Id)))+type instance PF Employee = Const Person :*: Const Salary+type instance PF Person = Const Name :*: Const Address+type instance PF Salary = Const Int++instance Typeable Company where+ typeof = Data "Company" fctrof+instance Mu Company where+ inn l = C l+ out (C l) = l+instance Typeable Dept where+ typeof = Data "Dept" fctrof+instance Mu Dept where+ inn (n,(m,l)) = D n m l+ out (D n m l) = (n,(m,l))+instance Typeable Employee where+ typeof = Data "Employee" fctrof+instance Mu Employee where+ inn (p,s) = E p s+ out (E p s) = (p,s)+instance Typeable Person where+ typeof = Data "Person" fctrof+instance Mu Person where+ inn (n,a) = P n a+ out (P n a) = (n,a)+instance Typeable Salary where+ typeof = Data "Salary" fctrof+instance Mu Salary where+ inn i = S i+ out (S i) = i++genCom :: Company +genCom = C [dralf]+dralf, dblair :: Dept+dralf = D "Research" ralf [Left joost, Left marlow, Right dblair]+dblair = D "Strategy" blair []+ralf, joost, marlow, blair :: Employee +ralf = E (P "Ralf" "Amsterdam") (S 8000) +joost = E (P "Joost" "Amsterdam") (S 1000) +marlow = E (P "Marlow" "Cambridge") (S 2000) +blair = E (P "Blair" "London") (S 100000)+++company :: Type Company+company = typeof+dept :: Type Dept+dept = typeof+person :: Type Person+person = typeof+employee :: Type Employee+employee = typeof+salary :: Type Salary+salary = typeof++-- | Increment Salaries of Employees++incE' :: Int -> Employee -> Employee+incE' k (E p (S i)) = E p $ S $ i*(1+k)+incE :: Int -> Pf (Employee -> Employee)+incE k = FUN "incE" (incE' k)++increaseEmployee :: Int -> Pf (Company -> Company)+increaseEmployee k = APPLY company $ EVERYWHERE $ MKT employee (incE k)++evalIncE = eval typeof (increaseEmployee 1) genCom+reduceIncE = reduceIO (optimise_tp >>> optimise_pf >>> beautify_pf) typeof (increaseEmployee 1)++-- | Increment All Salaries++incS :: Int -> Pf (Salary -> Salary)+incS k = INN .= FUN "incS" (*(1+k)) .= OUT++increaseSalary :: Int -> Pf (Company -> Company)+increaseSalary k = APPLY company $ EVERYWHERE $ MKT salary (incS k)++evalIncS = eval typeof (increaseSalary 1) genCom+reduceIncS = reduceIO (optimise_tp >>> optimise_pf >>> beautify_pf) typeof (increaseSalary 1)++-- | Sum All Salaries++bills :: Pf (Salary -> Int)+bills = OUT++salaryBill :: Pf (Company -> Int)+salaryBill = APPLYQ company $ EVERYTHING $ MKQ salary bills++evalBill = eval typeof salaryBill genCom+reduceBill = reduceIO (optimise_tu >>> optimise_pf >>> beautify_pf) typeof salaryBill++billE' :: Employee -> Int+billE' (E _ (S i)) = i+billE :: Pf (Employee -> Int)+billE = FUN "billE" billE'++salaryBillE :: Pf (Company -> Int)+salaryBillE = APPLYQ company $ EVERYTHING $ MKQ employee billE++evalBillE = eval typeof salaryBillE genCom+reduceBillE = reduceIO (optimise_tu >>> optimise_pf >>> beautify_pf) typeof salaryBillE
+ src/Transform/Examples/Imdb.hs view
@@ -0,0 +1,64 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Examples.Imdb+-- 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+-- +-- Imdb lens example+--+-----------------------------------------------------------------------------++module Transform.Examples.Imdb where++import Data.Type+import Data.Lens+import Transform.Rewriting+import Transform.Rules.Lenses+import Transform.Rules.PF++import Generics.Pointless.Functors+import Generics.Pointless.Lenses+import Generics.Pointless.Lenses.Examples.Imdb hiding (imdb,imdb_opt,movie,reviews,actor,shows,boxoffices,awards)++import Prelude hiding (Show(..),concat,length,shows)++-- ** Specifications++imdb :: Pf (Lens Imdb ([(((Year,Title),Nat),(Director,Value))],[(Name,[Category])]))+imdb = (shows ><<< MAP_LNS actor)++actor :: Pf (Lens Actor (Name,[Category]))+actor = ID_LNS ><<< awards++movie :: Pf (Lens Movie (Director,Value))+movie = ID_LNS ><<< boxoffices++awards :: Pf (Lens [Played] [Category])+awards = MAP_LNS (SND_LNS (VAR "dyear")) .<< CONCAT_LNS .<< MAP_LNS (SND_LNS (VAR "dytrole"))++shows :: Pf (Lens [Show] [(((Year,Title),Nat),(Director,Value))])+shows = COMP_LNS t (MAP_LNS f) $ COMP_LNS t' FILTER_LEFT_LNS $ MAP_LNS DISTR_LNS .<< MAP_LNS g+ where f = (ID_LNS ><<< VAR "reviews") ><<< ID_LNS+ g = ID_LNS ><<< (VAR "movie" -|-<< VAR "tv")+ t = typeof+ 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"))++reviews :: Pf (Lens [Review] Nat)+reviews = LENGTH_LNS "ccomment" .<< CONCAT_LNS .<< MAP_LNS (SND_LNS (VAR "duser"))++-- ** Optimization++imdb_opt = reduceIO optimise_lns typeof imdb++imdbput_opt = imdb_opt >>= reduceIO optimise_pf typeof . putof typeof+
+ src/Transform/Examples/Women.hs view
@@ -0,0 +1,46 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Examples.Women+-- 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+-- +-- Women lens example+--+-----------------------------------------------------------------------------++module Transform.Examples.Women where++import Data.Type+import Data.Lens+import Transform.Rewriting+import Transform.Rules.Lenses+import Transform.Rules.PF+import Transform.Rules.PF.Rec++import Generics.Pointless.Combinators+import Generics.Pointless.Functors+import Generics.Pointless.Lenses+import Generics.Pointless.Lenses.Examples.MapExamples hiding (women_opt)++instance Typeable Gender where+ typeof = Data "Gender" fctrof++men :: Pf (Lens [Person] Nat)+men = LENGTH_LNS _L .<< FILTER_LEFT_LNS .<< MAP_LNS (OUT_LNS .<< SND_LNS (PNT "woman" .= BANG))++women :: Pf (Lens [Person] Nat)+women = LENGTH_LNS _L .<< FILTER_RIGHT_LNS .<< MAP_LNS (OUT_LNS .<< SND_LNS (PNT "woman" .= BANG))++men_opt = reduceIO optimise_lns typeof men+women_opt = reduceIO optimise_lns typeof women++womenput = women_opt >>= reduceIO (many (once (top fzip_def ||| top functor_def))) typeof . putof typeof+womenput_opt = women_opt >>= reduceIO (optimise_pf >>> beautify_pf) typeof . putof typeof+
+ src/Transform/Rewriting.hs view
@@ -0,0 +1,297 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Rewriting+-- 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+-- +-- Point-free type-preserving rewriting.+--+-----------------------------------------------------------------------------++module Transform.Rewriting where++import Data.Type+import Data.Spine+import Data.Equal++import Data.List+import Control.Monad+import Control.Monad.RWS+import Control.Monad.State+import Debug.Trace+import System.IO++import Generics.Pointless.Combinators++-- Generic queries++gmapQ :: GenericQ r -> GenericQ [r]+gmapQ q t x = aux q (toSpine t x)+ where aux :: GenericQ r -> (forall a. Spine a -> [r])+ aux q (_ `As` _) = []+ aux q (Ap f (t :| x)) = aux q f ++ [q t x]++type Query r = forall a . Typed a -> r++everything :: (r -> r -> r) -> GenericQ r -> Query r+everything op q (t :| x) = aux op q t x+ where aux :: (r -> r -> r) -> GenericQ r -> GenericQ r+ aux op q t x = foldl1 op ([q t x] ++ gmapQ (aux op q) t x)+ +-- Locations and contexts++type Location = [Int]++down :: Location -> Location+down = (0:)++next :: Location -> Location+next (h:t) = (h+1):t++replace :: MonadPlus m => Location -> Typed b -> Typed a -> m a+replace [0] (b :| x) (a :| y) = coerce b a x+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+1) l (Ap f (a :| y)) = do g <- aux n l f+ return $ Ap g (a :| y)+ aux _ _ _ = mzero++hole :: Type a -> a+hole (Pf _) = HOLE++puthole :: Location -> Dynamic -> Dynamic+puthole l (Dyn t x) = Dyn t (xua l (t :| x))+ where xua :: Location -> Typed a -> a+ xua [0] (a :| y) = hole a+ 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+1) l (Ap f (a :| y)) = Ap (aux n l f) (a :| y)++-- The basic type of rules+type GenericM m = forall a . Type a -> Pf a -> m (Pf a)++-- Generic one-level map with location update++gmapMo :: (MonadReader Location m, MonadPlus m) => GenericM m -> GenericM m+gmapMo h t y = aux h (toSpine (Pf t) y)+ where aux :: (MonadReader Location m, MonadPlus m) => GenericM m -> Spine a -> m a+ aux h (c `As` _) = mzero+ aux h (Ap f (Pf t :| x)) = (do+ g <- local next $ aux h f+ return $ g x)+ `mplus` (do+ let g = fromSpine f+ y <- local down $ h t x+ return $ g y)++gmapMo' :: (MonadReader Location m, MonadPlus m) => GenericM m -> GenericM m+gmapMo' h t y = aux h (toSpine (Pf t) y)+ where aux :: (MonadReader Location m, MonadPlus m) => GenericM m -> Spine a -> m a+ aux h (c `As` _) = mzero+ aux h (Ap f (Pf t :| x)) = (do+ let g = fromSpine f+ y <- local down $ h t x+ return $ g y)+ `mplus` (do+ g <- local next $ aux h f+ return $ g x)++gmapM :: (MonadReader Location m, MonadPlus m) => GenericM m -> GenericM m+gmapM h t y = aux h (toSpine (Pf t) y)+ where aux :: (MonadReader Location m, MonadPlus m) => GenericM m -> Spine a -> m a+ aux h x@(c `As` _) = return c+ aux h (Ap f (Pf t :| x)) = do + g <- local next $ aux h f+ y <- local down $ h t x+ return $ g y+ aux h (Ap f (t :| x)) = do + g <- local next $ aux h f+ return $ g x++-- Promoting rules to traversals by updating context and propagating the type+top :: (MonadReader Location m, MonadState Dynamic m, MonadPlus m) => GenericM m -> GenericM m+top f t x = do+ y <- f t x+ (Dyn u c) <- get+ l <- ask+ let z = replace l (Pf t :| y) (u :| c)+ case z of+ Just z' -> put (Dyn u z')+ Nothing -> put (Dyn One _L)+ return y++gtop :: (MonadReader Location m, MonadState Dynamic m, MonadPlus m) => Rule -> GenericM m -> GenericM m+gtop r f t x = do+ y <- f t x+ (Dyn (Pf u) c) <- get+ l <- ask+ let Just z = replace l (Pf t :| y) ((Pf u) :| c)+ c' = reducePf r u c+ z' = reducePf r u z+ guard (geq (Pf u) c' z')+ put (Dyn (Pf u) z)+ return y++-- Strategy combinators+once :: (MonadReader Location m, MonadPlus m) => GenericM m -> GenericM m+once f = f ||| gmapMo (once f)++once' :: (MonadReader Location m, MonadPlus m) => GenericM m -> GenericM m+once' f = f ||| gmapMo' (once' f)++everywhere :: (MonadReader Location m, MonadPlus m) => GenericM m -> GenericM m+everywhere f = f >>> gmapM (everywhere f)++everywhere' :: (MonadReader Location m, MonadPlus m) => GenericM m -> GenericM m+everywhere' f = gmapM (everywhere f) >>> f++innermost :: Rule -> Rule+innermost r = gmapM (innermost r) >>> try (r >>> innermost r)++outermost :: Rule -> Rule+outermost r = try (many1 (once r))++(>>>) :: Monad m => GenericM m -> GenericM m -> GenericM m+(f >>> g) t x = f t x >>= g t++(|||) :: MonadPlus m => GenericM m -> GenericM m -> GenericM m+(f ||| g) t x = f t x `mplus` g t x++many :: MonadPlus m => GenericM m -> GenericM m+many r = (r >>> many r) ||| nop++many1 :: MonadPlus m => GenericM m -> GenericM m+many1 r = r >>> many r++many2 :: MonadPlus m => GenericM m -> GenericM m+many2 r = r >>> r >>> many r++nop :: Monad m => GenericM m+nop t = return++try :: MonadPlus m => GenericM m -> GenericM m+try x = x ||| nop++-- Rewriting monad++type Log = [(String,String)]++type Rewrite = RWST Location Log Dynamic Maybe++type Rule = GenericM Rewrite++printRule :: String -> Type a -> a -> Rewrite ()+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 ()++success :: String -> a -> Rewrite a+success n x =+ do z@(Dyn t v) <- get+ trace n $ printRule n t v+ return x++context :: Rewrite (Typed Dynamic)+context =+ do l <- ask+ y <- get+ return (Dynamic :| puthole l y)++-- Simplification wrapers++simplify :: Typeable a => Bool -> Rule -> Pf a -> IO (Pf a)+simplify = rewrite typeof++rewrite :: Type a -> Bool -> Rule -> Pf a -> IO (Pf a)+rewrite t b s e = do+ Just (x,l) <- return $ evalRWST (s t e) [0] (Dyn (Pf t) e)+ when b $ sequence_ (map aux l)+ putStrLn (" "++(gshow (Pf t) x))+ return x+ where aux (n,y) =putStrLn (" "++y) >> putStrLn ("= { "++n++" }") ++reduce :: Rule -> Type a -> Pf a -> (Pf a,[String])+reduce s t x = maybe (x,[]) (id >< map fst) (evalRWST (s t x) [0] (Dyn (Pf t) x))++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 ""+ hPutRuleTree stdout r+ return l++writeIO :: FilePath -> Rule -> Type a -> Pf a -> IO (Pf a)+writeIO f s t x = do+ h <- openFile f WriteMode+ let (l,r) = maybe (x,[]) id (evalRWST (s t x) [0] (Dyn (Pf t) x))+ putStr $ gshow (Pf t) l+ putStrLn ""+ hPutRuleTree h r+ return l++reducePfMb :: Rule -> Type a -> Pf a -> Maybe (Pf a)+reducePfMb s t x = liftM fst (evalRWST (s t x) [0] (Dyn (Pf t) x))++reducePf :: Rule -> Type a -> Pf a -> Pf a+reducePf s t x = maybe x fst (evalRWST (s t x) [0] (Dyn (Pf t) x))++reduceCount :: Rule -> Type a -> Pf a -> (Pf a,Int)+reduceCount s t x = maybe (x,0) (id >< length) (evalRWST (s t x) [0] (Dyn (Pf t) x))++hPutRuleTree :: Handle -> Log -> IO ()+hPutRuleTree h l = evalStateT (hPutRuleTree' h l) 0++hPutRuleTree' :: Handle -> Log -> StateT Int IO ()+hPutRuleTree' _ [] = return ()+hPutRuleTree' h ((r,e):xs) = do+ if (isSuffixOf ":" r)+ then do+ i <- get+ liftIO $ hPutStrLn h $ printRuleNode i True (init r)+ modify succ+ else if (isPrefixOf ":" r)+ then do+ modify pred+ i <- get+ liftIO $ hPutStrLn h $ printRuleNode i False (tail r)+ else do+ i <- get+ liftIO $ hPutStrLn h $ printRuleNode i True r+ hPutRuleTree' h xs+ +printRuleNode :: Int -> Bool -> String -> String+printRuleNode n True s = replicate n ' ' ++ "|- " ++ s+printRuleNode n False s = replicate n ' ' ++ "/- " ++ s++proof_strat :: Rule -> Type a -> Pf a -> Pf a -> Rewrite ()+proof_strat r t f g = do+ eq1 <- r t f+ eq2 <- r t g+ debug "proof1: " (Pf t) eq1+ debug "proof2: " (Pf t) eq2+ guard $ (geq (Pf t) eq1 eq2)++proof_strat' :: Rule -> Type a -> Pf a -> Type b -> Pf b -> Rewrite ()+proof_strat' r a f b g = do+ eq1 <- r a f+ eq2 <- r b g+ guard $ (geq' (Pf a) eq1 (Pf b) eq2)++proof :: Rule -> Type a -> Pf a -> Pf a -> Bool+proof r t f g = maybe False (const True) $ evalRWST (proof_strat r t f g) [0] (Dyn (Pf t) f)++proof' :: Rule -> Type a -> Pf a -> Type b -> Pf b -> Bool+proof' r a f b g = maybe False (const True) $ evalRWST (proof_strat' r a f b g) [0] (Dyn (Pf a) f)
+ src/Transform/Rules/Lenses.hs view
@@ -0,0 +1,109 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Rules.Lenses+-- 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 lenses.+--+-----------------------------------------------------------------------------++module Transform.Rules.Lenses where++import Data.Type+import Data.Equal+import Data.Lens+import Transform.Rewriting+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(..))++import Generics.Pointless.Lenses++-- * Strategies++optimise_lns :: Rule+optimise_lns = step1+ where+ 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++-- * Proofs++proveLns :: Type (Lens c a) -> Pf (Lens c a) -> IO ()+proveLns t@(Lns c a) l = do+ putStr "Proving CreateGet"+ eq1 <- reduceIO PF.optimise_pf (Fun a a) (COMP c (getof t l) (createof t l))+ print $ geq (Pf $ Fun a a) eq1 ID+ putStr "Proving PutGet"+ eq2 <- reduceIO PF.optimise_pf (Fun (Prod a c) a) (COMP c (getof t l) (putof t l))+ print $ geq (Pf $ Fun (Prod a c) a) eq2 FST+ putStr "Proving GetPut"+ eq3 <- reduceIO PF.optimise_pf (Fun c c) (COMP (Prod a c) (putof t l) ((getof t l) /\= ID))+ print $ geq (Pf $ Fun c c) eq3 ID++proveLnsRule :: Type (Lens c a) -> Pf (Lens c a) -> Rule -> IO ()+proveLnsRule t@(Lns c a) l r = case (evalRWST (r t l) [0] (Dyn (Pf t) l)) of+ { Just (l',_) -> do+ putStr "Proving get: \n"+ getl <- reduceIO PF.optimise_pf (Fun c a) $ getof t l+ putStrLn "="+ getl' <- reduceIO PF.optimise_pf (Fun c a) $ getof t l'+ print $ geq (Pf $ Fun c a) getl getl'+ putStr "Proving create: \n"+ createl <- reduceIO PF.optimise_pf (Fun a c) $ createof t l+ putStrLn "="+ createl' <- reduceIO PF.optimise_pf (Fun a c) $ createof t l'+ print $ geq (Pf $ Fun a c) createl createl'+ putStr "Proving put: \n"+ putl <- writeIO "put.txt" nop (Fun (Prod a c) c) $ putof t l+ putStrLn "="+ putl' <- writeIO "put2.txt" nop (Fun (Prod a c) c) $ putof t l'+ print $ geq (Pf $ Fun (Prod a c) c) putl putl'+ ; otherwise -> putStrLn "non-matching rule" }
+ src/Transform/Rules/Lenses.hs-boot view
@@ -0,0 +1,5 @@+module Transform.Rules.Lenses where++import Transform.Rewriting++optimise_lns :: Rule
+ src/Transform/Rules/Lenses/Combinators.hs view
@@ -0,0 +1,266 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Rules.Lenses.Combinators+-- 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 lenses.+--+-----------------------------------------------------------------------------++module Transform.Rules.Lenses.Combinators where++import Data.Type+import Data.Lens+import Transform.Rewriting+import {-# SOURCE #-} qualified Transform.Rules.PF as PF++import Prelude hiding (Functor(..))+import Control.Monad hiding (Functor(..))++-- ** 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+ fg <- r (Lns c a) (COMP_LNS b f g)+ return $ COMP_LNS c fg h+comp_lns r (Lns d a) (COMP_LNS c (COMP_LNS b f g) h) = do+ gh <- r (Lns d b) (COMP_LNS c g h)+ return $ COMP_LNS b f gh+comp_lns r t f = r t f++-- | Applies a rule to the left of a composition+comp1_lns :: Rule -> Rule+comp1_lns r (Lns a c) (COMP_LNS b f g) = do+ f' <- r (Lns b c) f+ return $ COMP_LNS b f' g+comp1_lns _ _ _ = mzero++-- | Applies a rule to the right of a composition+comp2_lns :: Rule -> Rule+comp2_lns r (Lns a c) (COMP_LNS b f g) = do+ g' <- r (Lns a b) g+ return $ COMP_LNS b f g'+comp2_lns _ _ _ = mzero++prod1_lns :: Rule -> Rule+prod1_lns r (Lns (Prod a b) (Prod c d)) (f `PROD_LNS` g) = do+ f' <- r (Lns a c) f+ return $ f' `PROD_LNS` g+prod1_lns _ _ _ = mzero++prod2_lns :: Rule -> Rule+prod2_lns r (Lns (Prod a b) (Prod c d)) (f `PROD_LNS` g) = do+ g' <- r (Lns b d) g+ return $ f `PROD_LNS` g'+prod2_lns _ _ _ = mzero++sum1_lns :: Rule -> Rule+sum1_lns r (Lns (Either a b) (Either c d)) (f `SUM_LNS` g) = do+ f' <- r (Lns a c) f+ return $ f' `SUM_LNS` g+sum1_lns r (Lns (Either a b) (Either c d)) (SUMW_LNS f g l1 l2) = do+ l1' <- r (Lns a c) l1+ return $ SUMW_LNS f g l1' l2+sum1_lns _ _ _ = mzero++sum2_lns :: Rule -> Rule+sum2_lns r (Lns (Either a b) (Either c d)) (f `SUM_LNS` g) = do+ g' <- r (Lns b d) g+ return $ f `SUM_LNS` g'+sum2_lns r (Lns (Either a b) (Either c d)) (SUMW_LNS f g l1 l2) = do+ l2' <- r (Lns b d) l2+ return $ SUMW_LNS f g l1 l2'+sum2_lns _ _ _ = mzero++-- | Rearranges the left of a composition before applying a rule+precomp_lns :: Rule -> Rule -> Rule+precomp_lns r1 r2 = comp_lns $ r2 ||| (comp1_lns r1 >>> comp_assocr_lns >>> comp2_lns r2)++-- | Rearranges the right of a composition before applying a rule+postcomp_lns :: Rule -> Rule -> Rule+postcomp_lns r1 r2 = comp_lns $ r2 ||| (comp2_lns r1 >>> comp_assocl_lns >>> comp1_lns r2)++-- | Extracts the leftmost element of a nested composition+leftmost_lns :: Rule+leftmost_lns (Lns a c) (COMP_LNS b f g) = do+ f' <- leftmost_lns' (Lns b c) f+ try comp_assocr_lns (Lns a c) $ COMP_LNS b f' g+leftmost_lns (Lns a c) f =+ return $ COMP_LNS a f ID_LNS+leftmost_lns _ _ = mzero+leftmost_lns' :: Rule+leftmost_lns' (Lns a c) (COMP_LNS b f g) = do+ f' <- leftmost_lns' (Lns b c) f+ try comp_assocr_lns (Lns a c) $ COMP_LNS b f' g+leftmost_lns' (Lns a c) f = return f+leftmost_lns' _ _ = mzero++-- | Extracts the rightmost element of a nested composition+rightmost_lns :: Rule+rightmost_lns (Lns a c) (COMP_LNS b f g) = do+ g' <- rightmost_lns' (Lns a b) g+ try comp_assocl_lns (Lns a c) $ COMP_LNS b f g'+rightmost_lns (Lns a c) f =+ return $ COMP_LNS c ID_LNS f+rightmost_lns _ _ = mzero+rightmost_lns' :: Rule+rightmost_lns' (Lns a c) (COMP_LNS b f g) = do+ g' <- rightmost_lns' (Lns a b) g+ try comp_assocl_lns (Lns a c) $ COMP_LNS b f g'+rightmost_lns' (Lns a c) f = return f+rightmost_lns' _ _ = mzero++leftmost_sum_lns :: Rule+leftmost_sum_lns (Lns (Either a b) (Either c d)) (SUM_LNS ID_LNS ID_LNS) = mzero+leftmost_sum_lns (Lns (Either a b) (Either c d)) (SUM_LNS ID_LNS g) = do+ COMP_LNS y g' g'' <- leftmost_lns' (Lns b d) g+ return $ COMP_LNS (Either a y) (ID_LNS -|-<< g') (ID_LNS -|-<< g'')+leftmost_sum_lns (Lns (Either a b) (Either c d)) (SUM_LNS f ID_LNS) = do+ COMP_LNS x f' f'' <- leftmost_lns' (Lns a c) f+ return $ COMP_LNS (Either x b) (f' -|-<< ID_LNS) (f'' -|-<< ID_LNS)+leftmost_sum_lns (Lns (Either a b) (Either c d)) (SUM_LNS f g) = do+ COMP_LNS x f' f'' <- leftmost_lns' (Lns a c) f+ COMP_LNS y g' g'' <- leftmost_lns' (Lns b d) g+ return $ COMP_LNS (Either x y) (f' -|-<< g') (f'' -|-<< g'')+leftmost_sum_lns _ _ = mzero++rightmost_sum_lns :: Rule+rightmost_sum_lns (Lns (Either a b) (Either c d)) (SUM_LNS ID_LNS ID_LNS) = mzero+rightmost_sum_lns (Lns (Either a b) (Either c d)) (SUM_LNS ID_LNS g) = do+ COMP_LNS y g' g'' <- rightmost_lns' (Lns b d) g+ return $ COMP_LNS (Either a y) (ID_LNS -|-<< g') (ID_LNS -|-<< g'')+rightmost_sum_lns (Lns (Either a b) (Either c d)) (SUM_LNS f ID_LNS) = do+ COMP_LNS x f' f'' <- rightmost_lns' (Lns a c) f+ return $ COMP_LNS (Either x b) (f' -|-<< ID_LNS) (f'' -|-<< ID_LNS)+rightmost_sum_lns (Lns (Either a b) (Either c d)) (SUM_LNS f g) = do+ COMP_LNS x f' f'' <- rightmost_lns' (Lns a c) f+ COMP_LNS y g' g'' <- rightmost_lns' (Lns b d) g+ return $ COMP_LNS (Either x y) (f' -|-<< g') (f'' -|-<< g'')+rightmost_sum_lns _ _ = mzero++leftmost_prod_lns :: Rule+leftmost_prod_lns (Lns (Prod a b) (Prod c d)) (PROD_LNS ID_LNS ID_LNS) = mzero+leftmost_prod_lns (Lns (Prod a b) (Prod c d)) (PROD_LNS ID_LNS g) = do+ COMP_LNS y g' g'' <- leftmost_lns' (Lns b d) g+ return $ COMP_LNS (Prod a y) (ID_LNS ><<< g') (ID_LNS ><<< g'')+leftmost_prod_lns (Lns (Prod a b) (Prod c d)) (PROD_LNS f ID_LNS) = do+ COMP_LNS x f' f'' <- leftmost_lns' (Lns a c) f+ return $ COMP_LNS (Prod x b) (f' ><<< ID_LNS) (f'' ><<< ID_LNS)+leftmost_prod_lns (Lns (Prod a b) (Prod c d)) (PROD_LNS f g) = do+ COMP_LNS x f' f'' <- leftmost_lns' (Lns a c) f+ COMP_LNS y g' g'' <- leftmost_lns' (Lns b d) g+ return $ COMP_LNS (Prod x y) (f' ><<< g') (f'' ><<< g'')+leftmost_prod_lns _ _ = mzero++rightmost_prod_lns :: Rule+rightmost_prod_lns (Lns (Prod a b) (Prod c d)) (PROD_LNS ID_LNS ID_LNS) = mzero+rightmost_prod_lns (Lns (Prod a b) (Prod c d)) (PROD_LNS ID_LNS g) = do+ COMP_LNS y g' g'' <- rightmost_lns' (Lns b d) g+ return $ COMP_LNS (Prod a y) (ID_LNS ><<< g') (ID_LNS ><<< g'')+rightmost_prod_lns (Lns (Prod a b) (Prod c d)) (PROD_LNS f ID_LNS) = do+ COMP_LNS x f' f'' <- rightmost_lns' (Lns a c) f+ return $ COMP_LNS (Prod x b) (f' ><<< ID_LNS) (f'' ><<< ID_LNS)+rightmost_prod_lns (Lns (Prod a b) (Prod c d)) (PROD_LNS f g) = do+ COMP_LNS x f' f'' <- rightmost_lns' (Lns a c) f+ COMP_LNS y g' g'' <- rightmost_lns' (Lns b d) g+ return $ COMP_LNS (Prod x y) (f' ><<< g') (f'' ><<< g'')+rightmost_prod_lns _ _ = mzero++-- ** Identity and Composition++nat_id_lns = comp_lns nat_id_lns'+nat_id_lns' :: Rule+nat_id_lns' (Lns _ _) (COMP_LNS _ f ID_LNS) =+ return f+nat_id_lns' (Lns _ _) (COMP_LNS _ ID_LNS f) =+ return f+nat_id_lns' _ _ = mzero++comp_assocr_lns :: Rule+comp_assocr_lns _ (COMP_LNS a (COMP_LNS b l1 l2) l3) =+ return $ COMP_LNS b l1 (COMP_LNS a l2 l3)+comp_assocr_lns _ _ = mzero++comp_assocl_lns :: Rule+comp_assocl_lns _ (COMP_LNS a l1 (COMP_LNS b l2 l3)) =+ return $ COMP_LNS b (COMP_LNS a l1 l2) l3+comp_assocl_lns _ _ = mzero++-- ** Bangs++bang_reflex_lns :: Rule+bang_reflex_lns (Lns One One) (BANG_LNS f) =+ success "bang-Reflex-Lns" ID_LNS+bang_reflex_lns _ _ = mzero++bang_fusion_lns = comp_lns bang_fusion_lns'+bang_fusion_lns' :: Rule+bang_fusion_lns' t@(Lns a One) v@(COMP_LNS b (BANG_LNS f) l1) = do+ debug "bang-Fusion-Lns" (Pf t) v+ g <- PF.optimise_pf (Fun One a) $ COMP b (createof (Lns a b) l1) f+ success "bang-Fusion-Lns" $ BANG_LNS g+bang_fusion_lns' _ _ = mzero++bang_uniq_lns :: Rule+bang_uniq_lns (Lns _ _) ID_LNS = mzero+bang_uniq_lns (Lns _ _) (BANG_LNS _) = mzero+bang_uniq_lns t@(Lns a One) l1 = do+ debug "bang-Uniq-Lns" (Pf t) l1+ g <- PF.optimise_pf (Fun One a) $ createof (Lns a One) l1+ success "bang-Uniq-Lns" $ BANG_LNS g+bang_uniq_lns _ _ = mzero++-- ** Backtracking sums and products++sum_unreflex_lns :: Rule+sum_unreflex_lns (Lns (Either a b) (Either c d)) ID_LNS =+ success "sum-UnReflex-Lns" $ ID_LNS -|-<< ID_LNS+sum_unreflex_lns _ _ = mzero++-- ** Tops and Bottoms++top_fusion_lns = comp_lns top_fusion_lns'+top_fusion_lns' :: Rule+top_fusion_lns' (Lns _ _) (COMP_LNS _ TOP f) =+ success "top-Fusion-Lns" TOP+top_fusion_lns' (Lns _ _) (COMP_LNS _ f TOP) =+ success "top-Fusion-Lns" TOP+top_fusion_lns' _ _ = mzero
+ src/Transform/Rules/Lenses/Dists.hs view
@@ -0,0 +1,132 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Rules.Lenses.Dists+-- 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 lenses involving distribution of products over sums and vice-versa.+--+-----------------------------------------------------------------------------++module Transform.Rules.Lenses.Dists where++import Data.Type+import Data.Lens+import Transform.Rewriting+import Transform.Rules.Lenses.Combinators+import {-# SOURCE #-} qualified Transform.Rules.PF as PF++import Prelude hiding (Functor(..))+import Control.Monad hiding (Functor(..))++-- ** Distr++distr_def_lns :: Rule+distr_def_lns (Lns (Prod c (Either a b)) _) DISTR_LNS = do+ let t = Either (Prod a c) (Prod b c)+ t' = Prod (Either a b) c+ success "distr-Def-Lns" $ COMP_LNS t (SWAP_LNS -|-<< SWAP_LNS) $ COMP_LNS t' DISTL_LNS SWAP_LNS+distr_def_lns _ _ = mzero++undistr_def_lns :: Rule+undistr_def_lns (Lns _ (Prod c (Either a b))) UNDISTR_LNS = do+ let t = Prod (Either a b) c+ t' = Either (Prod a c) (Prod b c)+ success "undistr-Def-Lns" $ COMP_LNS t SWAP_LNS $ COMP_LNS t' UNDISTL_LNS $ (SWAP_LNS -|-<< SWAP_LNS)+undistr_def_lns _ _ = mzero++-- ** Distl++distl_iso_lns = comp_lns distl_iso_lns'+distl_iso_lns' :: Rule+distl_iso_lns' _ (COMP_LNS _ DISTL_LNS UNDISTL_LNS) =+ success "distl-Iso-Lns" ID_LNS+distl_iso_lns' _ _ = mzero++undistl_iso_lns = comp_lns undistl_iso_lns'+undistl_iso_lns' :: Rule+undistl_iso_lns' _ (COMP_LNS _ UNDISTL_LNS DISTL_LNS) =+ success "undistl-Iso-Lns" ID_LNS+undistl_iso_lns' _ _ = mzero++distl_fst_cancel_lns = comp_lns distl_fst_cancel_lns'+distl_fst_cancel_lns' :: Rule+distl_fst_cancel_lns' (Lns (Prod _ c) _) (COMP_LNS _ (SUMW_LNS (ID `PROD` SND) (ID `PROD` SND) (FST_LNS f) (FST_LNS g)) DISTL_LNS) =+ success "distl-Fst-Cancel-Lns" $ FST_LNS (f \/= g)+distl_fst_cancel_lns' _ _ = mzero++distl_snd_cancel_lns = comp_lns distl_snd_cancel_lns'+distl_snd_cancel_lns' :: Rule+distl_snd_cancel_lns' q@(Lns (Prod (Either a b) c) _) v@(COMP_LNS _ (EITHER_LNS p (SND_LNS f) (SND_LNS g)) DISTL_LNS) = do+ debug "distl-Snd-Cancel-Lns" (Pf q) v+ let h = COMP (Either c c) (f -|-= g) $ (?=) c p+ h' <- PF.optimise_pf (Fun c (Either a b)) h + success "distl-Snd-Cancel-Lns" $ SND_LNS h'+distl_snd_cancel_lns' _ _ = mzero++distl_id_cancel_lns = comp_lns distl_id_cancel_lns'+distl_id_cancel_lns' :: Rule+distl_id_cancel_lns' (Lns _ _) (COMP_LNS _ (EITHER_LNS (COMP _ p FST) ID_LNS ID_LNS) DISTL_LNS) = do+ success "distl-Id-Cancel-Lns" $ (EITHER_LNS p ID_LNS ID_LNS) ><<< ID_LNS+distl_id_cancel_lns' _ _ = mzero++distl_fusion_lns = comp_lns distl_fusion_lns'+distl_fusion_lns' :: Rule+distl_fusion_lns' (Lns _ _) (COMP_LNS _ DISTL_LNS (f `PROD_LNS` ID_LNS)) = mzero+distl_fusion_lns' q@(Lns (Prod a c) _) v@(COMP_LNS (Prod (Either a' b') c') DISTL_LNS (l1 `PROD_LNS` l3)) = (do+ let (t,t') = (Either (Prod a' c) (Prod b' c),Prod (Either a' b') c)+ inv (Lns c c') l3+ debug "distl-Fusion-Lns" (Pf q) v+ success "distl-Fusion-Lns" $ COMP_LNS t (ID_LNS ><<< l3 -|-<< ID_LNS ><<< l3) $ COMP_LNS t' DISTL_LNS $ (l1 ><<< ID_LNS))+ `mplus` (do+ debug "distl-Fusion-Lns" (Pf q) v+ let (t,t') = (Either (Prod a' c) (Prod b' c),Prod (Either a' b') c)+ h = COMP (Prod (Prod a' b') (Prod c' c)) (FST ><= putof (Lns c c') l3) distp_pf+ i = COMP (Prod (Prod b' a') (Prod c' c)) (FST ><= putof (Lns c c') l3) distp_pf+ debug "distlFusionH" (Pf $ (Fun (Prod (Prod a' c') (Prod b' c)) (Prod a' c))) h+ h' <- PF.optimise_pf (Fun (Prod (Prod a' c') (Prod b' c)) (Prod a' c)) h+ i' <- PF.optimise_pf (Fun (Prod (Prod b' c') (Prod a' c)) (Prod b' c)) i+ success "distl-Fusion-Lns" $ COMP_LNS t (SUMW_LNS h' i' (ID_LNS ><<< l3) (ID_LNS ><<< l3)) $ COMP_LNS t' DISTL_LNS $ l1 ><<< ID_LNS+ )+distl_fusion_lns' _ _ = mzero++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' 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+ success "distl-Nat-Lns" $ COMP_LNS (Either (Prod a c) (Prod b c)) ((l1 ><<< l3) -|-<< (l2 ><<< l3)) DISTL_LNS)+ `mplus` (do+ debug "distl-Nat-Lns" (Pf q) v+ let h = COMP (Prod (Prod a' b) (Prod c' c)) (COMP a' (createof (Lns a a') l1) FST ><= (putof (Lns c c') l3)) distp_pf+ i = COMP (Prod (Prod b' a) (Prod c' c)) (COMP b' (createof (Lns b b') l2) FST ><= (putof (Lns c c') l3)) distp_pf+ h' <- PF.optimise_pf (Fun (Prod (Prod a' c') (Prod b c)) (Prod a c)) h+ i' <- PF.optimise_pf (Fun (Prod (Prod b' c') (Prod a c)) (Prod b c)) i+ success "distl-Nat-Lns" $ COMP_LNS (Either (Prod a c) (Prod b c)) (SUMW_LNS h' i' (l1 ><<< l3) (l2 ><<< l3)) DISTL_LNS)+distl_nat_lns' q@(Lns (Prod (Either a b) c) _) v@(COMP_LNS (Prod (Either a' b') c') DISTL_LNS ((SUMW_LNS f g l1 l2) `PROD_LNS` l3)) = do+ debug "distl-Nat-Lns" (Pf q) v+ let h = COMP (Prod (Prod a' b) (Prod c' c)) (f ><= (putof (Lns c c') l3)) distp_pf+ i = COMP (Prod (Prod b' a) (Prod c' c)) (g ><= (putof (Lns c c') l3)) distp_pf+ h' <- PF.optimise_pf (Fun (Prod (Prod a' c') (Prod b c)) (Prod a c)) h+ i' <- PF.optimise_pf (Fun (Prod (Prod b' c') (Prod a c)) (Prod b c)) i+ success "distl-Nat-Lns" $ COMP_LNS (Either (Prod a c) (Prod b c)) (SUMW_LNS h' i' (l1 ><<< l3) (l2 ><<< l3)) DISTL_LNS+distl_nat_lns' _ _ = mzero++distl_sum_nat_lns = comp_lns distl_sum_nat_lns'+distl_sum_nat_lns' :: Rule+distl_sum_nat_lns' (Lns (Prod (Either a b) c) _) (COMP_LNS (Prod (Either d e) f) DISTL_LNS ((EITHER_LNS p l1 l2) `PROD_LNS` l3)) = do+ let (t,t') = (Prod (Either d e) f,Either (Prod a c) (Prod b c))+ p' = COMP (Either d e) p FST+ 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+++
+ src/Transform/Rules/Lenses/Lists.hs view
@@ -0,0 +1,230 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Rules.Lenses.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 lenses involving lists.+--+-----------------------------------------------------------------------------++module Transform.Rules.Lenses.Lists where++import Data.Type+import Data.Eval+import Data.Lens+import Transform.Rewriting+import Transform.Rules.Lenses.Combinators++import Prelude hiding (Functor(..))+import Control.Monad hiding (Functor(..))++import Generics.Pointless.Functors+import Generics.Pointless.Lenses++-- ** List laws++map_id_lns :: Rule+map_id_lns (Lns _ _) (MAP_LNS ID_LNS) =+ success "map-Id-Lns" $ ID_LNS+map_id_lns _ _ = mzero++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' _ _ = 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+ (COMP_LNS c f g) <- leftmost_lns' (Lns a b) l1+ return $ COMP_LNS (list c) (MAP_LNS f) (MAP_LNS g)+leftmost_map_lns _ _ = mzero++map_cat_lns = comp_lns map_cat_lns'+map_cat_lns' :: Rule+map_cat_lns' (Lns _ lb) (COMP_LNS _ (MAP_LNS l1) CAT_LNS) =+ success "map-Cat-Lns" $ COMP_LNS (Prod lb lb) CAT_LNS (MAP_LNS l1 ><<< MAP_LNS l1)+map_cat_lns' _ _ = mzero++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+map_concat_lns' _ _ = mzero++filter_cat_lns = comp_lns filter_cat_lns'+filter_cat_lns' :: Rule+filter_cat_lns' (Lns _ la) (COMP_LNS _ FILTER_LEFT_LNS CAT_LNS) =+ success "filter-Cat-Lns" $ COMP_LNS (Prod la la) CAT_LNS (FILTER_LEFT_LNS ><<< FILTER_LEFT_LNS)+filter_cat_lns' (Lns _ lb) (COMP_LNS _ FILTER_RIGHT_LNS CAT_LNS) =+ success "filter-Cat-Lns" $ COMP_LNS (Prod lb lb) CAT_LNS (FILTER_RIGHT_LNS ><<< FILTER_RIGHT_LNS)+filter_cat_lns' _ _ = mzero++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' _ _ = 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+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+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' _ _ = 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' _ _ = 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+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+ 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+ 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+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' _ _ = 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' _ _ = mzero++-- ** Definitions++list_defs_lns :: Rule+list_defs_lns = list_catas_lns ||| list_anas_lns ||| list_hylos_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_anas_lns :: Rule+list_anas_lns = map_ana_def_lns ||| length_ana_def_lns++list_hylos_lns :: Rule+list_hylos_lns = plus_def_lns ||| 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++inre :: Type a -> Type b -> Pf (Lens (Either (Either a b) b) (Either a b))+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 _ _ = 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 _ _ = mzero++filter_def_lns :: Rule+filter_def_lns (Lns (Data "List" (K One :+!: (K (Either a b) :*!: I))) 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+ 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))+ t'' = Either (Prod a lb) (Prod b lb)+ success "filter-Def-Lns" $ CATA_LNS $ COMP_LNS t e $ COMP_LNS t' COASSOCL_LNS (ID_LNS -|-<< COMP_LNS t'' COSWAP_LNS DISTL_LNS)+filter_def_lns _ _ = mzero++length_cata_def_lns :: Rule+length_cata_def_lns (Lns _ _) (LENGTH_LNS v) = do+ let f = COMP One (PNT v) BANG+ success "length-Cata-Def-Lns" $ CATA_LNS $ COMP_LNS (Either One nat) INN_LNS (ID_LNS -|-<< SND_LNS f)+length_cata_def_lns _ _ = mzero++length_ana_def_lns :: Rule+length_ana_def_lns (Lns la _) (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+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+ 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)+ g = CATA_LNS $ COMP_LNS t''' INN_LNS $ COMP_LNS t'' (inre One (Prod a la)) (OUT_LNS -|-<< ID_LNS)+ h = ANA_LNS $ COMP_LNS t' (SND_LNS BANG -|-<< ASSOCR_LNS) $ COMP_LNS t DISTL_LNS (OUT_LNS ><<< ID_LNS)+ f = fixof (K la :+!: (K a :*!: I))+ success "cat-Def-Lns" $ COMP_LNS f g h+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))+ 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+ let t = Prod (Either One nat) nat+ t' = Either (Prod One nat) (Prod nat nat)+ t'' = Either (Either One nat) nat+ l1 = COMP_LNS (Either One nat) INN_LNS $ COMP_LNS t'' (inre One nat) (OUT_LNS -|-<< ID_LNS)+ l2 = COMP_LNS t' (SND_LNS BANG -|-<< ID_LNS) $ COMP_LNS t DISTL_LNS (OUT_LNS ><<< ID_LNS)+ f = typeof :: Type (Fix (Const Nat :+: Id))+ success "plus-Def-Lns" $ COMP_LNS f (CATA_LNS l1) (ANA_LNS l2)+plus_def_lns _ _ = mzero++sum_def_lns :: Rule+sum_def_lns (Lns _ _) SUML_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))+ success "sum-Def-Lns" $ CATA_LNS $ COMP_LNS (Either One nat) INN_LNS aux+sum_def_lns _ _ = mzero+
+ src/Transform/Rules/Lenses/Products.hs view
@@ -0,0 +1,169 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Rules.Lenses.Products+-- 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 lenses involving products.+--+-----------------------------------------------------------------------------++module Transform.Rules.Lenses.Products where++import Data.Type+import Data.Lens+import Data.Equal+import Transform.Rewriting+import Transform.Rules.Lenses.Combinators+import {-# SOURCE #-} qualified Transform.Rules.PF as PF++import Prelude hiding (Functor(..))+import Control.Monad hiding (Functor(..))++-- ** Product combinators++prod_functor_id_lns :: Rule+prod_functor_id_lns _ (PROD_LNS ID_LNS ID_LNS) =+ success "prod-Functor-Id-Lns" ID_LNS+prod_functor_id_lns _ _ = mzero++prod_functor_comp_lns = comp_lns prod_functor_comp_lns'+prod_functor_comp_lns' :: Rule+prod_functor_comp_lns' (Lns _ _) (COMP_LNS (Prod c d) (f `PROD_LNS` g) (h `PROD_LNS` i)) =+ success "prod-Functor-Comp-Lns" $ (COMP_LNS c f h) `PROD_LNS` (COMP_LNS d g i)+prod_functor_comp_lns' _ _ = mzero++fst_nat_lns = comp_lns fst_nat_lns'+fst_nat_lns' :: Rule+fst_nat_lns' q@(Lns (Prod c d) _ ) v@(COMP_LNS (Prod a b) (FST_LNS f) (l1 `PROD_LNS` l2)) = do+ debug "fst-Nat-Lns" (Pf q) v+ let g = COMP b (createof (Lns d b) l2) $ COMP a f (getof (Lns c a) l1)+ g' <- PF.optimise_pf (Fun c d) g+ success "fst-Nat-Lns" $ COMP_LNS c l1 $ FST_LNS g'+fst_nat_lns' _ _ = mzero++snd_nat_lns = comp_lns snd_nat_lns'+snd_nat_lns' :: Rule+snd_nat_lns' q@(Lns (Prod c d) _ ) v@(COMP_LNS (Prod a b) (SND_LNS f) (l1 `PROD_LNS` l2)) = do+ debug "Snd-Nat-Lns" (Pf q) v+ let g = COMP a (createof (Lns c a) l1) $ COMP b f (getof (Lns d b) l2)+ g' <- PF.optimise_pf (Fun d c) g+ success "snd-Nat-Lns" $ COMP_LNS d l2 $ SND_LNS g'+snd_nat_lns' _ _ = mzero+ +-- ** Isomorphisms involving products++bangl_cancel_lns = comp_lns bangl_cancel_lns'+bangl_cancel_lns' :: Rule+bangl_cancel_lns' (Lns _ _) (COMP_LNS _ (SND_LNS f) BANGL_LNS) =+ success "bangl-Cancel-Lns" ID_LNS+bangl_cancel_lns' _ _ = mzero+ +bangr_cancel_lns = comp_lns bangr_cancel_lns'+bangr_cancel_lns' :: Rule+bangr_cancel_lns' (Lns _ _) (COMP_LNS _ (FST_LNS f) BANGR_LNS) =+ success "bangr-Cancel-Lns" ID_LNS+bangr_cancel_lns' _ _ = mzero++swap_nat_lns = comp_lns swap_nat_lns'+swap_nat_lns' :: Rule+swap_nat_lns' (Lns (Prod a b) _) (COMP_LNS _ SWAP_LNS (PROD_LNS f g)) =+ success "swap-Nat-Lns" $ COMP_LNS (Prod b a) (g `PROD_LNS` f) SWAP_LNS+swap_nat_lns' _ _ = mzero++swap_iso_lns = comp_lns swap_iso_lns'+swap_iso_lns' :: Rule+swap_iso_lns' (Lns _ _) (COMP_LNS _ SWAP_LNS SWAP_LNS) =+ success "swap-Iso-Lns" ID_LNS+swap_iso_lns' _ _ = mzero++swap_cancel_lns = comp_lns swap_cancel_lns'+swap_cancel_lns' :: Rule+swap_cancel_lns' (Lns _ _) (COMP_LNS _ (FST_LNS f) SWAP_LNS) = + success "swap-Cancel-Lns" $ SND_LNS f+swap_cancel_lns' (Lns _ _) (COMP_LNS _ (SND_LNS f) SWAP_LNS) = + success "swap-Cancel-Lns" $ FST_LNS f+swap_cancel_lns' _ _ = mzero++assocr_nat_lns = comp_lns assocr_nat_lns'+assocr_nat_lns' :: Rule+assocr_nat_lns' (Lns _ (Prod a (Prod b c))) (COMP_LNS _ (f `PROD_LNS` (g `PROD_LNS` h)) ASSOCR_LNS) =+ success "assocr-Nat-Lns" $ COMP_LNS (Prod (Prod a b) c) ASSOCR_LNS $ (f ><<< g) ><<< h+assocr_nat_lns' _ _ = mzero++assocr_iso_lns = comp_lns assocr_iso_lns'+assocr_iso_lns' :: Rule+assocr_iso_lns' (Lns _ _) (COMP_LNS _ ASSOCR_LNS ASSOCL_LNS) =+ success "assocr-Iso-Lns" ID_LNS+assocr_iso_lns' _ _ = mzero++assocr_fst_cancel_lns = comp_lns assocr_fst_cancel_lns'+assocr_fst_cancel_lns' :: Rule+assocr_fst_cancel_lns' q@(Lns _ _) v@(COMP_LNS (Prod a (Prod b c)) (FST_LNS f) ASSOCR_LNS) = do+ debug "assocr-Fst-Cancel-Lns" (Pf q) v+ let h = COMP (Prod b c) SND $ COMP a f FST+ g = COMP (Prod b c) FST f+ h' <- PF.optimise_pf (Fun (Prod a b) c) h+ g' <- PF.optimise_pf (Fun a b) g+ success "assocr-Fst-Cancel-Lns" $ COMP_LNS (Prod a b) (FST_LNS g') (FST_LNS h')+assocr_fst_cancel_lns' (Lns _ _) (COMP_LNS (Prod a (Prod b c)) (ID_LNS `PROD_LNS` (FST_LNS f)) ASSOCR_LNS) = do+ let g = COMP b f SND+ success "assocr-Fst-Cancel-Lns" $ FST_LNS g+assocr_fst_cancel_lns' _ _ = mzero++assocr_snd_cancel_lns = comp_lns assocr_snd_cancel_lns'+assocr_snd_cancel_lns' :: Rule+assocr_snd_cancel_lns' (Lns _ _) (COMP_LNS _ (SND_LNS (COMP _ g FST)) ASSOCR_LNS) =+ success "assocr-Snd-Cancel-Lns" $ (SND_LNS g) ><<< ID_LNS+assocr_snd_cancel_lns' (Lns _ _) (COMP_LNS (Prod a (Prod b c)) (ID_LNS `PROD_LNS` (SND_LNS (COMP _ f BANG))) ASSOCR_LNS) = do+ let g = COMP One f BANG+ success "assocr-Snd-Cancel-Lns" $ (FST_LNS g) ><<< ID_LNS+assocr_snd_cancel_lns' (Lns _ _) (COMP_LNS (Prod a (Prod b c)) (ID_LNS `PROD_LNS` (SND_LNS f)) ASSOCR_LNS) = do+ Eq <- teq c a+ success "assocr-Snd-Cancel-Lns" $ (FST_LNS f) ><<< ID_LNS+assocr_snd_cancel_lns' _ _ = mzero++assocl_nat_lns = comp_lns assocl_nat_lns'+assocl_nat_lns' :: Rule+assocl_nat_lns' (Lns _ (Prod (Prod a b) c)) (COMP_LNS _ ((f `PROD_LNS` g) `PROD_LNS` h) ASSOCL_LNS) =+ success "assocl-Nat-Lns" $ COMP_LNS (Prod a (Prod b c)) ASSOCL_LNS $ f ><<< (g ><<< h)+assocl_nat_lns' _ _ = mzero++assocl_iso_lns = comp_lns assocl_iso_lns'+assocl_iso_lns' :: Rule+assocl_iso_lns' (Lns _ _) (COMP_LNS _ ASSOCL_LNS ASSOCR_LNS) =+ success "assocl-Iso-Lns" ID_LNS+assocl_iso_lns' _ _ = mzero++assocl_fst_cancel_lns = comp_lns assocl_fst_cancel_lns'+assocl_fst_cancel_lns' :: Rule+assocl_fst_cancel_lns' (Lns _ _) (COMP_LNS _ (FST_LNS (COMP _ g SND)) ASSOCL_LNS) =+ success "assocl-Fst-Cancel-Lns" $ ID_LNS ><<< FST_LNS g+assocl_fst_cancel_lns' (Lns _ _) (COMP_LNS _ ((FST_LNS (COMP _ f BANG)) `PROD_LNS` ID_LNS) ASSOCL_LNS) = do+ let g = COMP One f BANG+ success "assocl-Fst-Cancel-Lns" $ ID_LNS ><<< SND_LNS g+assocl_fst_cancel_lns' (Lns _ _) (COMP_LNS (Prod (Prod a b) c) ((FST_LNS f) `PROD_LNS` ID_LNS) ASSOCL_LNS) = do+ Eq <- teq a c+ success "assocl-Fst-Cancel-Lns" $ ID_LNS ><<< SND_LNS f+assocl_fst_cancel_lns' _ _ = mzero++assocl_snd_cancel_lns = comp_lns assocl_snd_cancel_lns'+assocl_snd_cancel_lns' :: Rule+assocl_snd_cancel_lns' q@(Lns _ _) v@(COMP_LNS (Prod (Prod a b) c) (SND_LNS f) ASSOCL_LNS) = do+ debug "assocl-Snd-Cancel-Lns" (Pf q) v+ let h = COMP (Prod a b) FST $ COMP c f SND+ g = COMP (Prod a b) SND f+ h' <- PF.optimise_pf (Fun (Prod b c) a) h+ g' <- PF.optimise_pf (Fun c b) g+ success "assocl-Snd-Cancel-Lns" $ COMP_LNS (Prod b c) (SND_LNS g') (SND_LNS h')+assocl_snd_cancel_lns' (Lns _ _) (COMP_LNS (Prod (Prod a b) c) ((SND_LNS f) `PROD_LNS` ID_LNS) ASSOCL_LNS) = do+ let g = COMP b f FST+ success "assocl-Snd-Cancel-Lns" $ SND_LNS g+assocl_snd_cancel_lns' _ _ = mzero
+ src/Transform/Rules/Lenses/Rec.hs view
@@ -0,0 +1,374 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Rules.Lenses.Rec+-- 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 lenses involving recursion.+--+-----------------------------------------------------------------------------++module Transform.Rules.Lenses.Rec where++import Data.Type+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 Prelude hiding (Functor(..))+import Control.Monad hiding (Functor(..))+import Unsafe.Coerce++import Generics.Pointless.Combinators+import Generics.Pointless.Functors+import Generics.Pointless.Lenses++-- ** In / Out++in_iso_lns = comp_lns in_iso_lns'+in_iso_lns' :: Rule+in_iso_lns' (Lns a b) (COMP_LNS _ INN_LNS OUT_LNS) = do+ Eq <- teq a b+ success "in-Iso-Lns" ID_LNS+in_iso_lns' _ _ = mzero++out_iso_lns = comp_lns out_iso_lns'+out_iso_lns' :: Rule+out_iso_lns' (Lns a b) (COMP_LNS _ OUT_LNS INN_LNS) = do+ Eq <- teq a b+ success "out-Iso-Lns" ID_LNS+out_iso_lns' _ _ = mzero++-- ** Functors++functor_id_lns :: Rule+functor_id_lns (Lns _ _) (FMAP_LNS fctr (Fun a _) ID_LNS) =+ success "functor-Id-Lns" ID_LNS+functor_id_lns _ _ = mzero++functor_comp_lns = comp_lns functor_comp_lns'+functor_comp_lns' :: Rule+functor_comp_lns' (Lns fa fc) (COMP_LNS fb (FMAP_LNS fctr (Fun b c) f) (FMAP_LNS fctr' (Fun a b') g)) = do+ Eq <- feq fctr fctr'+ Eq <- teq b b'+ 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+ 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++-- ** Catas++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)+ let fb = rep fctr b+ success "cata-Cancel-Lns" $ COMP_LNS fb g' $ FMAP_LNS fctr (Fun a b) $ PROTECT_LNS (ANA_LNS g)+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+ 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'+ debug "cataRes" (Pf $ Lns fa a) h+ guard $ not $ find (Pf (Lns Any Any)) (CONV_LNS (Right _L) TOP) (Pf (Lns fa a)) h+ success "cata-Fusion-Lns" $ CATA_LNS h+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+ debug "cata-Shift-Lns" (Pf t) v+ Eq <- teq (rep g b) gb+ eta' <- natCoerce_lns f g b eta a+ success "cata-Shift-Lns" $ ANA_LNS $ COMP_LNS (rep f a) eta' OUT_LNS+cata_shift_lns _ _ = mzero+++-- ** Anas++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)+ 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' _ _ = 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+ 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'+ debug "anaRes" (Pf $ Lns a fa) h+ guard $ not $ find (Pf (Lns Any Any)) (CONV_LNS (Left _L) TOP) (Pf (Lns a fa)) h+ success "ana-Fusion-Lns" $ ANA_LNS h+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+ debug "ana-Shift-Lns" (Pf t) v+ Eq <- teq (rep f a) fa+ eta' <- natCoerce_lns f g a eta b+ success "ana-Shift-Lns" $ CATA_LNS $ COMP_LNS (rep g b) INN_LNS eta'+ana_shift_lns _ _ = mzero++-- ** Hylos++hylo_shift_lns = comp_lns hylo_shift_lns'+hylo_shift_lns' :: Rule+hylo_shift_lns' q@(Lns a c) v@(COMP_LNS (Data _ fctrf) (CATA_LNS g) (ANA_LNS h)) = do+ debug "hylo-Shift-Lns" (Pf q) v+ COMPF_LNS fctrg c' gold geta <- natSplit_lns c c fctrf g+ Eq <- teq c c'+ let t = Lns (rep fctrf c) (rep fctrg c)+ debug "hyloSplit" (Pf t) geta+ heta <- natCoerce_lns fctrf fctrg c geta a+ success "hylo-Shift-Lns" $ COMP_LNS (fixof fctrg) (CATA_LNS gold) (ANA_LNS $ COMP_LNS (rep fctrf a) heta h)+hylo_shift_lns' _ _ = mzero++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+ 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)+ success "hylo-Id-Lns" ID_LNS+hylo_id_lns' _ _ = mzero++-- ** Natural transformations++-- | n . F f = F f . n+natProof_lns :: (Functor f,Functor g) => Fctr f -> Fctr g -> Type a -> Pf (Lens (Rep f a) (Rep g a)) -> Bool+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+ 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.++-- | Convert a natural transformation applied to some type into a natural transformation over another type+natCoerce_lns :: (MonadPlus m,Functor f,Functor g) => Fctr f -> Fctr g -> Type a+ -> Pf (Lens (Rep f a) (Rep g a)) -> Type b -> m (Pf (Lens (Rep f b) (Rep g b)))+natCoerce_lns f g a eta b = do+ guard (natProof_lns f g a eta)+ return (unsafeCoerce eta)++natSplit_lns :: (Functor f) => Type a -> Type b -> Fctr f -> Pf (Lens (Rep f a) b) -> Rewrite (Pf (Lens (Rep f a) b))+-- Constant+natSplit_lns a b _ ID_LNS = mzero+natSplit_lns a b (K t) f = do+ return $ COMPF_LNS (K b) a ID_LNS f +-- Sums+natSplit_lns a b fctr@(fctrf :+!: fctrg) v@(EITHER_LNS p f g) = (do+ COMPF_LNS fctrx a' fold feta <- natSplit_lns a b fctrf f+ COMPF_LNS fctry a'' gold geta <- natSplit_lns a b fctrg g+ Eq <- teq a a'+ Eq <- teq a a''+ return $ COMPF_LNS (fctrx :+!: fctry) a (EITHER_LNS p fold gold) (feta -|-<< geta))+ `mplus` (do+ COMPF_LNS fctrx a' fold feta <- natSplit_lns a b fctrf f+ Eq <- teq a a'+ return $ COMPF_LNS (fctrx :+!: fctrg) a (EITHER_LNS p fold g) (feta -|-<< ID_LNS))+ `mplus` (do+ COMPF_LNS fctry a'' gold geta <- natSplit_lns a b fctrg g+ Eq <- teq a a''+ return $ COMPF_LNS (fctrf :+!: fctry) a (EITHER_LNS p f gold) (ID_LNS -|-<< geta))+natSplit_lns a (Either b c) fctr@(fctrf :+!: fctrg) v@(f `SUM_LNS` g) = (do+ COMPF_LNS fctrx a' fold feta <- natSplit_lns a b fctrf f+ COMPF_LNS fctry a'' gold geta <- natSplit_lns a c fctrg g+ Eq <- teq a a'+ Eq <- teq a a''+ return $ COMPF_LNS (fctrx :+!: fctry) a (fold -|-<< gold) (feta -|-<< geta))+ `mplus` (do+ COMPF_LNS fctrx a' fold feta <- natSplit_lns a b fctrf f+ Eq <- teq a a'+ return $ COMPF_LNS (fctrx :+!: fctrg) a (fold -|-<< g) (feta -|-<< ID_LNS))+ `mplus` (do+ COMPF_LNS fctry a'' gold geta <- natSplit_lns a c fctrg g+ Eq <- teq a a''+ return $ COMPF_LNS (fctrf :+!: fctry) a (f -|-<< gold) (ID_LNS -|-<< geta))+-- Products+natSplit_lns a b (fctrf :*!: fctrg) (FST_LNS v) = do+ let old = ID_LNS+ eta = FST_LNS v+ return $ COMPF_LNS fctrf a old eta+natSplit_lns a b (fctrf :*!: fctrg) (SND_LNS v) = do+ let old = ID_LNS+ eta = SND_LNS v+ return $ COMPF_LNS fctrg a old eta+natSplit_lns a (Prod b c) fctr@(fctrf :*!: fctrg) v@(f `PROD_LNS` g) = (do+ COMPF_LNS fctrx a' fold feta <- natSplit_lns a b fctrf f+ COMPF_LNS fctry a'' gold geta <- natSplit_lns a c fctrg g+ Eq <- teq a a'+ Eq <- teq a a''+ return $ COMPF_LNS (fctrx :*!: fctry) a (fold ><<< gold) (feta ><<< geta))+ `mplus` (do+ COMPF_LNS fctrx a' fold feta <- natSplit_lns a b fctrf f+ Eq <- teq a a'+ return $ COMPF_LNS (fctrx :*!: fctrg) a (fold ><<< g) (feta ><<< ID_LNS))+ `mplus` (do+ COMPF_LNS fctry a'' gold geta <- natSplit_lns a c fctrg g+ Eq <- teq a a''+ return $ COMPF_LNS (fctrf :*!: fctry) a (f ><<< gold) (ID_LNS ><<< geta))+-- Composition+natSplit_lns a b fctr e@(COMP_LNS _ _ _) = (do+ COMP_LNS c f g <- rightmost_lns (Lns (rep fctr a) b) e+ COMPF_LNS fctrx a' gold geta <- natSplit_lns a c fctr g+ Eq <- teq a a'+ COMPF_LNS fctry a'' fold feta <- natSplit_lns a b fctrx (COMP_LNS c f gold)+ Eq <- teq a a''+ let old = fold+ eta = COMP_LNS (rep fctrx a) feta geta+ return $ COMPF_LNS fctry a old eta)+ `mplus` (do+ COMP_LNS c f g <- rightmost_lns (Lns (rep fctr a) b) e+ COMPF_LNS fctrx a' gold geta <- natSplit_lns a c fctr g+ Eq <- teq a a'+ let old = COMP_LNS c f gold+ eta = geta+ return $ COMPF_LNS fctrx a old eta)+-- Id and unrecognized cases match here+natSplit_lns a b fctr f = mzero+++-- ** Internal converses for fusion rules++-- | f . fº = id+rconv_cancel_lns = comp_lns rconv_cancel_lns'+rconv_cancel_lns' :: Rule+rconv_cancel_lns' t@(Lns a a') (COMP_LNS c (CATA_LNS f) (CONV_LNS (Right _) (ANA_LNS g))) = do+ f' <- ana_shift_lns (Lns c a) (ANA_LNS g)+ rconv_cancel_lns' t (COMP_LNS c (CATA_LNS f) (CONV_LNS (Right _L) f'))+rconv_cancel_lns' t@(Lns a a') (COMP_LNS c (ANA_LNS f) (CONV_LNS (Right _) (CATA_LNS g))) = do+ f' <- cata_shift_lns (Lns c a) (CATA_LNS g)+ rconv_cancel_lns' t (COMP_LNS c (ANA_LNS f) (CONV_LNS (Right _L) f'))+rconv_cancel_lns' t@(Lns a a') v@(COMP_LNS c f (CONV_LNS (Right _) f')) = do+ Eq <- teq a a'+ guard $ geq (Pf (Lns c a)) f f'+ success "rconv-Cancel-Lns" $ ID_LNS+rconv_cancel_lns' _ _ = mzero++-- | fº . f = id+lconv_cancel_lns = comp_lns lconv_cancel_lns'+lconv_cancel_lns' :: Rule+lconv_cancel_lns' t@(Lns a a') (COMP_LNS c (CONV_LNS (Left _) (ANA_LNS g)) (CATA_LNS f)) = do+ f' <- ana_shift_lns (Lns a' c) (ANA_LNS g)+ lconv_cancel_lns' t $ COMP_LNS c (CONV_LNS (Left _L) f') (CATA_LNS f)+lconv_cancel_lns' t@(Lns a a') v@(COMP_LNS c (CONV_LNS (Left _) (CATA_LNS g)) (ANA_LNS f)) = do+ f' <- cata_shift_lns (Lns a' c) (CATA_LNS g)+ lconv_cancel_lns' t $ COMP_LNS c (CONV_LNS (Left _L) f') (ANA_LNS f)+lconv_cancel_lns' (Lns c c') (COMP_LNS a (CONV_LNS (Left _) f') f) = do+ Eq <- teq c c'+ guard $ geq (Pf (Lns c a)) f f'+ success "lconv-Cancel-Lns" $ ID_LNS+lconv_cancel_lns' _ _ = mzero++conv_comp_lns :: Rule+conv_comp_lns (Lns _ _) (CONV_LNS e (COMP_LNS b f g)) =+ success "conv-Comp-Lns" $ COMP_LNS b (CONV_LNS e g) (CONV_LNS e f)+conv_comp_lns _ _ = mzero++conv_conv_lns :: Rule+conv_conv_lns _ (CONV_LNS _ (CONV_LNS _ f)) =+ 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_prod_lns :: Rule+conv_prod_lns _ (CONV_LNS e (PROD_LNS f g)) =+ success "conv-Prod-Lns" $ PROD_LNS (CONV_LNS e f) (CONV_LNS e g)+conv_prod_lns _ _ = mzero++conv_sum_lns :: Rule+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
+ src/Transform/Rules/Lenses/Sums.hs view
@@ -0,0 +1,163 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Rules.Lenses.Sums+-- 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 lenses involving sums.+--+-----------------------------------------------------------------------------++module Transform.Rules.Lenses.Sums where++import Data.Type+import Data.Lens+import Transform.Rewriting+import Transform.Rules.Lenses.Combinators+import {-# SOURCE #-} qualified Transform.Rules.PF as PF++import Prelude hiding (Functor(..))+import Control.Monad hiding (Functor(..))++-- ** Sum combinators++sum_functor_id_lns :: Rule+sum_functor_id_lns (Lns _ _) (SUM_LNS ID_LNS ID_LNS) =+ success "sum-Functor-Id-Lns" ID_LNS+sum_functor_id_lns _ _ = mzero++sum_functor_comp_lns = comp_lns sum_functor_comp_lns'+sum_functor_comp_lns' :: Rule+sum_functor_comp_lns' (Lns _ _) (COMP_LNS (Either c d) (f `SUM_LNS` g) (h `SUM_LNS` i)) =+ success "sum-Functor-Comp-Lns" $ (COMP_LNS c f h) `SUM_LNS` (COMP_LNS d g i)+sum_functor_comp_lns' _ _ = mzero++sum_absor_lns = comp_lns sum_absor_lns'+sum_absor_lns' :: Rule+sum_absor_lns' (Lns (Either a b) e) (COMP_LNS (Either c d) (EITHER_LNS p f g) (h `SUM_LNS` i)) =+ success "sum-Absor-Lns" $ EITHER_LNS p (COMP_LNS c f h) (COMP_LNS d g i)+sum_absor_lns' _ _ = mzero++sum_fusion_lns = comp_lns sum_fusion_lns'+sum_fusion_lns' :: Rule+sum_fusion_lns' q@(Lns _ d) v@(COMP_LNS c l1 (EITHER_LNS p l2 l3)) = do+ debug "sum-Fusion-Lns" (Pf q) v+ let p' = COMP c p $ createof (Lns c d) l1+ p'' <- PF.optimise_pf (Fun d (Either One One)) p'+ success "sum-Fusion-Lns" $ EITHER_LNS p'' (COMP_LNS c l1 l2) (COMP_LNS c l1 l3)+sum_fusion_lns' _ _ = mzero++-- ** Lifted sum combinators++{-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_functor_id_lns :: Rule+sumw_functor_id_lns (Lns _ _) (SUMW_LNS _ _ ID_LNS ID_LNS) =+ success "sumw-Functor-Id-Lns" ID_LNS+sumw_functor_id_lns _ _ = mzero++sumw_functor_comp_lns = comp_lns sumw_functor_comp_lns'+sumw_functor_comp_lns' :: Rule+sumw_functor_comp_lns' t@(Lns (Either ta tb) (Either te tf)) v@(COMP_LNS (Either tc td) (SUM_LNS l1 l2) (SUMW_LNS h i l3 l4)) = do+ debug "sumw-Functor-Comp-Lns" (Pf t) v+ let j = COMP (Prod tc tb) h $ ((createof (Lns tc te) l1) ><= ID)+ k = COMP (Prod td ta) i $ ((createof (Lns td tf) l2) ><= ID)+ j' <- PF.optimise_pf (Fun (Prod te tb) ta) j+ k' <- PF.optimise_pf (Fun (Prod tf ta) tb) k+ success "sumw-Functor-Comp" $ SUMW_LNS j' k' (COMP_LNS tc l1 l3) (COMP_LNS td l2 l4)+sumw_functor_comp_lns' t@(Lns (Either ta tb) (Either te tf)) v@(COMP_LNS (Either tc td) (SUMW_LNS f g l1 l2) (SUM_LNS l3 l4)) = do+ debug "sumw-Functor-Comp-Lns" (Pf t) v+ let j = COMP tc (createof (Lns ta tc) l3) $ COMP (Prod te td) f $ ID ><= (getof (Lns tb td) l4)+ k = COMP td (createof (Lns tb td) l4) $ COMP (Prod tf tc) g $ ID ><= (getof (Lns ta tc) l3)+ j' <- PF.optimise_pf (Fun (Prod te tb) ta) j+ k' <- PF.optimise_pf (Fun (Prod tf ta) tb) k+ success "sumw-Functor-Comp" $ SUMW_LNS j' k' (COMP_LNS tc l1 l3) (COMP_LNS td l2 l4)+sumw_functor_comp_lns' t@(Lns (Either ta tb) (Either te tf)) v@(COMP_LNS (Either tc td) (SUMW_LNS f g l1 l2) (SUMW_LNS h i l3 l4)) = do+ debug "sumw-Functor-Comp-Lns" (Pf t) v+ let j = COMP (Prod tc tb) h $ (COMP (Prod te td) f (ID ><= (getof (Lns tb td) l4))) /\= SND+ k = COMP (Prod td ta) i $ (COMP (Prod tf tc) g (ID ><= (getof (Lns ta tc) l3))) /\= SND+ j' <- PF.optimise_pf (Fun (Prod te tb) ta) j+ k' <- PF.optimise_pf (Fun (Prod tf ta) tb) k+ success "sumw-Functor-Comp" $ SUMW_LNS j' k' (COMP_LNS tc l1 l3) (COMP_LNS td l2 l4)+sumw_functor_comp_lns' _ _ = mzero++sumw_absor_lns = comp_lns sumw_absor_lns'+sumw_absor_lns' :: Rule+sumw_absor_lns' (Lns (Either a b) e) (COMP_LNS (Either c d) (EITHER_LNS p f g) (SUMW_LNS x y h i)) =+ success "sumw-Absor-Lns" $ EITHER_LNS p (COMP_LNS c f h) (COMP_LNS d g i)+sumw_absor_lns' _ _ = mzero++-- ** Isomorphisms involving sums++coswap_nat_lns = comp_lns coswap_nat_lns'+coswap_nat_lns' :: Rule+coswap_nat_lns' (Lns (Either a b) _) (COMP_LNS _ COSWAP_LNS (SUM_LNS l1 l2)) = do+ success "coswap-Nat-Lns" $ COMP_LNS (Either b a) (SUM_LNS l2 l1) COSWAP_LNS+coswap_nat_lns' (Lns (Either a b) _) (COMP_LNS _ COSWAP_LNS (SUMW_LNS f g l1 l2)) = do+ success "coswap-Nat-Lns" $ COMP_LNS (Either b a) (SUMW_LNS g f l2 l1) COSWAP_LNS+coswap_nat_lns' _ _ = mzero++coswap_iso_lns = comp_lns coswap_iso_lns'+coswap_iso_lns' :: Rule+coswap_iso_lns' (Lns _ _) (COMP_LNS _ COSWAP_LNS COSWAP_LNS) = do+ success "coswap-Iso-Lns" $ ID_LNS+coswap_iso_lns' _ _ = mzero++coswap_cancel_lns = comp_lns coswap_cancel_lns'+coswap_cancel_lns' :: Rule+coswap_cancel_lns' (Lns _ _) (COMP_LNS _ (EITHER_LNS p l1 l2) COSWAP_LNS) = do+ let p' = COMP (Either One One) COSWAP p+ success "coswap-Cancel-Lns" $ EITHER_LNS p' l2 l1+coswap_cancel_lns' _ _ = mzero++coassocr_nat_lns = postcomp_lns leftmost_sum_lns coassocr_nat_lns'+coassocr_nat_lns' :: Rule+coassocr_nat_lns' (Lns (Either (Either a b) c) _) (COMP_LNS _ COASSOCR_LNS ((f `SUM_LNS` g) `SUM_LNS` h)) = do+ success "coassocr-Nat-Lns" $ COMP_LNS (Either a (Either b c)) (f `SUM_LNS` (g `SUM_LNS` h)) COASSOCR_LNS+coassocr_nat_lns' (Lns _ _) (COMP_LNS _ COASSOCR_LNS (f `SUM_LNS` ID_LNS)) = mzero+coassocr_nat_lns' q@(Lns (Either a b) _) v@(COMP_LNS (Either (Either c d) e) COASSOCR_LNS (f `SUM_LNS` g)) = do+ debug "coassocr-Nat-Lns" (Pf q) v+ let t = Either c (Either d b)+ t' = Either (Either c d) b+ success "coassocr-Nat-Lns" $ COMP_LNS t (ID_LNS -|-<< (ID_LNS -|-<< g)) $ COMP_LNS t' COASSOCR_LNS (f -|-<< ID_LNS)+coassocr_nat_lns' _ _ = mzero++coassocr_iso_lns = comp_lns coassocr_iso_lns'+coassocr_iso_lns' :: Rule+coassocr_iso_lns' (Lns _ _) (COMP_LNS _ COASSOCR_LNS COASSOCL_LNS) =+ success "coassocr-Iso-Lns" ID_LNS+coassocr_iso_lns' _ _ = mzero++coassocl_nat_lns = postcomp_lns leftmost_sum_lns coassocl_nat_lns'+coassocl_nat_lns' :: Rule+coassocl_nat_lns' (Lns (Either a (Either b c)) _) (COMP_LNS _ COASSOCL_LNS (f `SUM_LNS` (g `SUM_LNS` h))) = do+ success "coassocl-Nat-Lns" $ COMP_LNS (Either (Either a b) c) ((f `SUM_LNS` g) `SUM_LNS` h) COASSOCL_LNS+coassocl_nat_lns' q@(Lns (Either a (Either b c)) _) v@(COMP_LNS (Either a' (Either b' c')) COASSOCL_LNS (f `SUM_LNS` (SUMW_LNS x y g h))) = do+ debug "coassocl-Nat-Lns" (Pf q) v+ let z' = COMP (Either (Prod a' c) (Prod b' c)) ((COMP a' (createof (Lns a a') f) FST) -|-= x) DISTL+ w' = COMP (Either (Prod c' a) (Prod c' b)) ((COMP c' (createof (Lns c c') h) FST) \/= y) DISTR+ z'' <- PF.optimise_pf (Fun (Prod (Either a' b') c) (Either a b)) z'+ w'' <- PF.optimise_pf (Fun (Prod c' (Either a b)) c) w'+ success "coassocl-Nat-Lns" $ COMP_LNS (Either (Either a b) c) (SUMW_LNS z'' w'' (f `SUM_LNS` g) h) COASSOCL_LNS+coassocl_nat_lns' _ _ = mzero++coassocl_iso_lns = comp_lns coassocl_iso_lns'+coassocl_iso_lns' :: Rule+coassocl_iso_lns' (Lns _ _) (COMP_LNS _ COASSOCL_LNS COASSOCR_LNS) =+ success "coassocl-Iso-Lns" ID_LNS+coassocl_iso_lns' _ _ = mzero++
+ src/Transform/Rules/PF.hs view
@@ -0,0 +1,63 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Rules.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+-- +-- Generic strategy for the rewriting of point-free functions.+--+-----------------------------------------------------------------------------++module Transform.Rules.PF where++import Transform.Rewriting+import Transform.Rules.PF.Combinators+import Transform.Rules.PF.Products+import Transform.Rules.PF.Sums+import Transform.Rules.PF.Dists+import Transform.Rules.PF.Rec+ +optimise_pf :: Rule+optimise_pf = outermost (top comp_assocr ||| rules) >>> right >>> try (once fuse >>> optimise_pf)+ where + 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-}+ +beautify_pf = outermost (prods ||| sums)+ where+ prods = top prod_unfusion ||| top prod_undef+ sums = top sum_unfusion ||| top sum_undef
+ src/Transform/Rules/PF.hs-boot view
@@ -0,0 +1,5 @@+module Transform.Rules.PF where+ +import Transform.Rewriting+ +optimise_pf :: Rule
+ src/Transform/Rules/PF/Combinators.hs view
@@ -0,0 +1,350 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Rules.PF.Combinators+-- 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.+--+-----------------------------------------------------------------------------++module Transform.Rules.PF.Combinators where++import Data.Type+import Data.Lens+import Data.Equal+import Transform.Rewriting++import Prelude hiding (Functor(..))+import Control.Monad hiding (Functor(..))++-- ** 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+ 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+ gh <- r (Fun d b) (COMP c g h)+ return $ COMP b f gh)+comp _ _ _ = mzero++comp1 :: Rule -> Rule+comp1 r (Fun a c) (COMP b f g) = do+ f' <- r (Fun b c) f+ return $ COMP b f' g+comp1 _ _ _ = mzero++comp2 :: Rule -> Rule+comp2 r (Fun a c) (COMP b f g) = do+ g' <- r (Fun a b) g+ return $ COMP b f g'+comp2 _ _ _ = mzero++prod1 :: Rule -> Rule+prod1 r (Fun (Prod a b) (Prod c d)) (f `PROD` g) = do+ f' <- r (Fun a c) f+ return $ f' `PROD` g+prod1 _ _ _ = mzero++prod2 :: Rule -> Rule+prod2 r (Fun (Prod a b) (Prod c d)) (f `PROD` g) = do+ g' <- r (Fun b d) g+ return $ f `PROD` g'+prod2 _ _ _ = mzero++sum1 :: Rule -> Rule+sum1 r (Fun (Either a b) (Either c d)) (f `SUM` g) = do+ f' <- r (Fun a c) f+ return $ f' `SUM` g+sum1 _ _ _ = mzero++sum2 :: Rule -> Rule+sum2 r (Fun (Either a b) (Either c d)) (f `SUM` g) = do+ g' <- r (Fun b d) g+ return $ f `SUM` g'+sum2 _ _ _ = mzero++precomp :: Rule -> Rule -> Rule+precomp r1 r2 = comp $ r2 ||| (comp1 r1 >>> comp_assocr >>> comp2 r2)++postcomp :: Rule -> Rule -> Rule+postcomp r1 r2 = comp $ r2 ||| (comp2 r1 >>> comp_assocl >>> comp1 r2)++rightmost :: Rule+rightmost (Fun a c) (COMP b f g) = do+ g' <- rightmost' (Fun a b) g+ try comp_assocl (Fun a c) $ COMP b f g'+rightmost (Fun a c) f =+ return $ COMP c ID f+rightmost _ _ = mzero+rightmost' :: Rule+rightmost' (Fun a c) (COMP b f g) = do+ g' <- rightmost' (Fun a b) g+ try comp_assocl (Fun a c) $ COMP b f g'+rightmost' (Fun a c) f = return f+rightmost' _ _ = mzero++leftmost :: Rule+leftmost (Fun a c) (COMP b f g) = do+ f' <- leftmost' (Fun b c) f+ try comp_assocr (Fun a c) $ COMP b f' g+leftmost (Fun a c) f =+ return $ COMP a f ID+leftmost _ _ = mzero+leftmost' :: Rule+leftmost' (Fun a c) (COMP b f g) = do+ f' <- leftmost' (Fun b c) f+ try comp_assocr (Fun a c) $ COMP b f' g+leftmost' (Fun a c) f = return f+leftmost' _ _ = mzero++leftmost_sum :: Rule+leftmost_sum (Fun (Either a b) (Either c d)) (SUM ID ID) = mzero+leftmost_sum (Fun (Either a b) (Either c d)) (SUM ID g) = do+ COMP y g' g'' <- leftmost' (Fun b d) g+ return $ COMP (Either a y) (ID -|-= g') (ID -|-= g'')+leftmost_sum (Fun (Either a b) (Either c d)) (SUM f ID) = do+ COMP x f' f'' <- leftmost' (Fun a c) f+ return $ COMP (Either x b) (f' -|-= ID) (f'' -|-= ID)+leftmost_sum (Fun (Either a b) (Either c d)) (SUM f g) = do+ COMP x f' f'' <- leftmost' (Fun a c) f+ COMP y g' g'' <- leftmost' (Fun b d) g+ return $ COMP (Either x y) (f' -|-= g') (f'' -|-= g'')+leftmost_sum _ _ = mzero++rightmost_sum :: Rule+rightmost_sum (Fun (Either a b) (Either c d)) (SUM ID ID) = mzero+rightmost_sum (Fun (Either a b) (Either c d)) (SUM ID g) = do+ COMP y g' g'' <- rightmost' (Fun b d) g+ return $ COMP (Either a y) (ID -|-= g') (ID -|-= g'')+rightmost_sum (Fun (Either a b) (Either c d)) (SUM f ID) = do+ COMP x f' f'' <- rightmost' (Fun a c) f+ return $ COMP (Either x b) (f' -|-= ID) (f'' -|-= ID)+rightmost_sum (Fun (Either a b) (Either c d)) (SUM f g) = do+ COMP x f' f'' <- rightmost' (Fun a c) f+ COMP y g' g'' <- rightmost' (Fun b d) g+ return $ COMP (Either x y) (f' -|-= g') (f'' -|-= g'')+rightmost_sum _ _ = mzero++leftmost_prod :: Rule+leftmost_prod (Fun (Prod a b) (Prod c d)) (PROD ID ID) = mzero+leftmost_prod (Fun (Prod a b) (Prod c d)) (PROD ID g) = do+ COMP y g' g'' <- leftmost' (Fun b d) g+ return $ COMP (Prod a y) (ID ><= g') (ID ><= g'')+leftmost_prod (Fun (Prod a b) (Prod c d)) (PROD f ID) = do+ COMP x f' f'' <- leftmost' (Fun a c) f+ return $ COMP (Prod x b) (f' ><= ID) (f'' ><= ID)+leftmost_prod (Fun (Prod a b) (Prod c d)) (PROD f g) = do+ COMP x f' f'' <- leftmost' (Fun a c) f+ COMP y g' g'' <- leftmost' (Fun b d) g+ return $ COMP (Prod x y) (f' ><= g') (f'' ><= g'')+leftmost_prod _ _ = mzero++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+ 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+ 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+ 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'')+rightmost_prod _ _ = mzero+++-- ** Identity and Composition++nat_id = comp nat_id'+nat_id' :: Rule+nat_id' _ (COMP _ ID f) = return f+nat_id' _ (COMP _ f ID) = return f+nat_id' _ _ = mzero++comp_assocr :: Rule+comp_assocr _ (COMP a (COMP b f g) h) =+ return $ (COMP b f (COMP a g h))+comp_assocr _ _ = mzero++comp_assocl :: Rule+comp_assocl _ (COMP a f (COMP b g h)) =+ return $ (COMP b (COMP a f g) h)+comp_assocl _ _ = mzero++-- ** Bangs++bang_reflex :: Rule+bang_reflex (Fun One One) BANG =+ success "bang-Reflex" ID+bang_reflex _ _ = mzero++bang_fusion = comp bang_fusion'+bang_fusion' :: Rule+bang_fusion' (Fun a One) (COMP b BANG f) =+ success "bang-Fusion" BANG+bang_fusion' _ _ = mzero++bang_uniq :: Rule+bang_uniq (Fun _ _) ID = mzero+bang_uniq (Fun _ _) BANG = mzero+bang_uniq (Fun a One) l1 =+ success "bang-Uniq" BANG+bang_uniq _ _ = mzero+ +-- ** Lens laws++create_def :: Rule+create_def t@(Fun a c) (CREATE l) = do+ success "create-Def" $ createof (Lns c a) l+create_def _ _ = mzero++get_def :: Rule+get_def (Fun c a) (GET l) = do+ success "get-Def" $ getof (Lns c a) l+get_def _ _ = mzero++put_def :: Rule+put_def (Fun (Prod a c) _) (PUT l) = do+ success "put-Def" $ putof (Lns c a) l+put_def _ _ = mzero++-- * Lens laws++create_get = comp create_get'+create_get' :: Rule+create_get' (Fun a a') (COMP c (GET f) (CREATE f')) = do+ 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'+put_get' :: Rule+put_get' (Fun (Prod a c) a') (COMP _ (GET f) (PUT f')) = do+ 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'+get_put' :: Rule+get_put' (Fun c c') (COMP (Prod a _) (PUT f) (GET f' `SPLIT` ID)) = do+ Eq <- teq c c'+ guard $ geq (Pf $ Lns c a) f f'+ success "Get-Put" ID+get_put' _ _ = mzero++create_put = comp create_put'+create_put' :: Rule+create_put' (Fun a c) (COMP (Prod _ c') (PUT f) (ID `SPLIT` CREATE f')) = do+ Eq <- teq c c'+ guard $ geq (Pf $ Lns c a) f f'+ success "Create-Put" $ CREATE f+create_put' _ _ = mzero++put_twice = comp put_twice'+put_twice' :: Rule+put_twice' (Fun (Prod a c) c') (COMP _ (PUT l) (FST `SPLIT` PUT l')) = do+ Eq <- teq c c'+ guard $ geq (Pf $ Lns c a) l l'+ success "Put-Twice" $ PUT l+put_twice' (Fun a c) (COMP (Prod b _) (PUT l) (f `SPLIT` (COMP (Prod b' c') (PUT l') (f' `SPLIT` g)))) = do+ Eq <- teq b b'+ Eq <- teq c c'+ guard $ geq (Pf $ Fun a b) f f'+ guard $ geq (Pf $ Lns c b) l l'+ success "Put-Twice" $ COMP (Prod b c) (PUT l) $ f /\= g +put_twice' _ _ = mzero++-- ** 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_unfusion :: Rule+prod_unfusion _ (ID `SPLIT` ID) = mzero+prod_unfusion t@(Fun a (Prod b c)) w@(f `SPLIT` g) = do+ let r = sum_unfusion ||| rightmost+ COMP x f' h <- r (Fun a b) f+ COMP y g' h' <- r (Fun a c) g+ Eq <- teq x y+ guard $ geq (Pf $ Fun a x) h h'+ res <- try (comp1 prod_unfusion >>> comp_assocr) t (COMP x (f' /\= g') h)+ 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+ let r = prod_unfusion ||| leftmost+ COMP x h f' <- r (Fun a c) f+ COMP y h' g' <- r (Fun b c) g+ Eq <- teq x y+ guard $ geq (Pf $ Fun x c) h h'+ res <- try (comp2 sum_unfusion >>> comp_assocl) t (COMP x h (f' \/= g'))+ success "sum-UnFusion" res+sum_unfusion _ _ = mzero ++-- ** Tops and Bottoms++top_fusion = comp top_fusion'+top_fusion' :: Rule+top_fusion' (Fun _ _) (COMP _ TOP f) =+ success "top-Fusion" TOP+top_fusion' (Fun _ _) (COMP _ f TOP) =+ success "top-Fusion" TOP+top_fusion' _ _ = mzero++
+ src/Transform/Rules/PF/Dists.hs view
@@ -0,0 +1,153 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Rules.PF.Dists+-- 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 distribution of sums over products and vice-versa.+--+-----------------------------------------------------------------------------++module Transform.Rules.PF.Dists where+ +import Data.Type+import Data.Equal+import Transform.Rewriting+import Transform.Rules.PF.Combinators++import Prelude hiding (Functor(..))+import Control.Monad hiding (Functor(..))++-- ** Distr++distr_def :: Rule+distr_def (Fun (Prod c (Either a b)) _) DISTR =+ success "distr-Def" $ COMP (Either (Prod a c) (Prod b c)) (SWAP -|-= SWAP) $ COMP (Prod (Either a b) c) DISTL SWAP+distr_def _ _ = mzero++undistr_def :: Rule+undistr_def (Fun _ _) UNDISTR =+ success "undistr-Def" $ (ID ><= INL) \/= (ID ><= INR)+undistr_def _ _ = mzero+ +-- ** Distl+ +undistl_def :: Rule+undistl_def (Fun _ _) UNDISTL =+ success "undistl-Def" $ INL ><= ID \/= INR ><= ID+undistl_def _ _ = mzero++distl_iso = comp distl_iso'+distl_iso' :: Rule+distl_iso' _ (COMP _ DISTL UNDISTL) =+ success "distl-Iso" ID+distl_iso' _ _ = mzero++undistl_iso = comp distl_iso'+undistl_iso' :: Rule+undistl_iso' _ (COMP _ UNDISTL DISTL) =+ success "distl-Iso" ID+undistl_iso' _ _ = mzero++distl_fst_cancel = comp distl_fst_cancel'+distl_fst_cancel' :: Rule+distl_fst_cancel' (Fun (Prod (Either a b) c) d) (COMP _ (FST `SUM` FST) DISTL) = do+ success "distl-Fst-Cancel" FST+distl_fst_cancel' _ _ = mzero++distl_snd_cancel = comp distl_snd_cancel'+distl_snd_cancel' :: Rule+distl_snd_cancel' (Fun _ _) (COMP _ (SND `EITHER` SND) DISTL) =+ success "distl-Snd-Cancel" SND+distl_snd_cancel' _ _ = mzero++distl_id_cancel = comp distl_id_cancel'+distl_id_cancel' :: Rule+distl_id_cancel' t@(Fun (Prod (Either a b) c) d) x@(COMP y (f `EITHER` g) DISTL) = (do+ Eq <- teq a b+ guard $ geq (Pf (Fun (Prod a c) d)) f g+ success "distl-Id-Cancel" $ COMP (Prod a c) f $ (ID \/= ID) ><= ID)+distl_id_cancel' _ _ = mzero++distl_sum_cancel = comp distl_sum_cancel'+distl_sum_cancel' :: Rule+distl_sum_cancel' (Fun _ _) (COMP _ DISTL ((f `SUM` g) `SPLIT` (h `EITHER` i))) =+ success "distl-Sum-Cancel" $ (f /\= h) -|-= (g /\= i)+distl_sum_cancel' (Fun _ _) (COMP _ DISTL (((COMP _ INL f) `EITHER` (COMP _ INR g)) `SPLIT` (h `EITHER` i))) =+ success "distl-Sum-Cancel" $ (f /\= h) -|-= (g /\= i)+distl_sum_cancel' _ _ = mzero++distl_bang_cancel = comp distl_bang_cancel'+distl_bang_cancel' :: Rule+distl_bang_cancel' (Fun _ _) (COMP _ DISTL (ID `SPLIT` (COMP c h BANG))) =+ success "distl-Bang-Cancel" $ ID /\= (COMP c h BANG) -|-= ID /\= (COMP c h BANG)+distl_bang_cancel' (Fun _ _) (COMP _ DISTL ((f `SUM` g) `SPLIT` (COMP c h BANG))) =+ success "distl-Bang-Cancel" $ f /\= (COMP c h BANG) -|-= g /\= (COMP c h BANG)+distl_bang_cancel' _ _ = mzero++distl_cancel = comp distl_cancel'+distl_cancel' :: Rule+distl_cancel' (Fun _ _) (COMP (Prod (Either a b) c) DISTL (INL `SPLIT` g)) =+ success "distl-Cancel" $ COMP (Prod a c) INL (ID /\= g)+distl_cancel' (Fun _ _) (COMP (Prod (Either a b) c) DISTL ((COMP _ INL f) `SPLIT` g)) =+ success "distl-Cancel" $ COMP (Prod a c) INL (f /\= g)+distl_cancel' (Fun _ _) (COMP (Prod (Either a b) c) DISTL (INR `SPLIT` g)) =+ success "distl-Cancel" $ COMP (Prod b c) INR (ID /\= g)+distl_cancel' (Fun _ _) (COMP (Prod (Either a b) c) DISTL ((COMP _ INR f) `SPLIT` g)) =+ success "distl-Cancel" $ COMP (Prod b c) INR (f /\= g)+distl_cancel' (Fun _ _) (COMP (Prod (Either a b) c) DISTL (INL `PROD` g)) =+ success "distl-Cancel" $ COMP (Prod a c) INL (ID ><= g)+distl_cancel' (Fun _ _) (COMP (Prod (Either a b) c) DISTL ((COMP _ INL f) `PROD` g)) =+ success "distl-Cancel" $ COMP (Prod a c) INL (f ><= g)+distl_cancel' (Fun _ _) (COMP (Prod (Either a b) c) DISTL (INR `PROD` g)) =+ success "distl-Cancel" $ COMP (Prod b c) INR (ID ><= g)+distl_cancel' (Fun _ _) (COMP (Prod (Either a b) c) DISTL ((COMP _ INR f) `PROD` g)) =+ success "distl-Cancel" $ COMP (Prod b c) INR (f ><= g)+distl_cancel' _ _ = mzero++proj :: Pf (a -> b) -> Bool+proj (f `SPLIT` g) = True+proj FST = True+proj SND = True+proj _ = False++distl_fusion = comp distl_fusion'+distl_fusion' :: Rule+distl_fusion' (Fun _ _) (COMP _ DISTL (f `SPLIT` ID)) = mzero+distl_fusion' (Fun a _) (COMP (Prod (Either b1 b2) d) DISTL (f `SPLIT` c)) = do+ COMP c g h <- leftmost (Fun a d) c+ guard $ not $ proj g+ let t = Either (Prod b1 c) (Prod b2 c)+ t' = Prod (Either b1 b2) c+ success "distl-Fusion" $ COMP t (ID ><= g -|-= ID ><= g) $ COMP t' DISTL $ f /\= h+distl_fusion' (Fun _ _) (COMP _ DISTL (f `PROD` ID)) = mzero+distl_fusion' (Fun (Prod a c) _) (COMP (Prod (Either a' b') c') DISTL (f `PROD` h)) = do+ let t = Either (Prod a' c) (Prod b' c)+ success "distl-Fusion" $ COMP t (ID ><= h -|-= ID ><= h) $ COMP (Prod (Either a' b') c) DISTL $ f ><= ID+distl_fusion' _ _ = mzero++distl_nat = comp $ comp2 ((try prod_undef) >>> prod1 (try sum_undef)) >>> distl_nat'+distl_nat' :: Rule+distl_nat' (Fun _ _) (COMP _ DISTL (ID `PROD` ID)) = mzero+distl_nat' (Fun (Prod (Either a b) c) _) (COMP _ DISTL ((f `SUM` g) `PROD` h)) = do+ let t = Either (Prod a c) (Prod b c)+ success "distl-Nat" $ COMP t (f ><= h -|-= g ><= h) DISTL+distl_nat' (Fun (Prod (Either a b) c) _) (COMP (Prod (Either a' b') c') DISTL ((f `EITHER` g) `PROD` h)) = do+ let t = Prod (Either a' b') c'+ t' = Either (Prod a c) (Prod b c)+ success "distl-Sum-Nat" $ COMP t DISTL $ COMP t' ((f ><= h) \/= (g ><= h)) DISTL+distl_nat' _ _ = mzero++distl_distl_fusion = comp distl_distl_fusion'+distl_distl_fusion' :: Rule+distl_distl_fusion' (Fun x@(Prod (Either a b) c) _) (COMP _ DISTL (SPLIT DISTL f)) = do+ 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
+ src/Transform/Rules/PF/Products.hs view
@@ -0,0 +1,94 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Rules.PF.Products+-- 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 products.+--+-----------------------------------------------------------------------------++module Transform.Rules.PF.Products where+ +import Data.Type+import Data.Equal+import Transform.Rewriting+import Transform.Rules.PF.Combinators++import Prelude hiding (Functor(..))+import Control.Monad hiding (Functor(..))++-- ** Products++prod_def :: Rule+prod_def t@(Fun (Prod a b) _) (PROD f g) =+ success "prod-Def" $ (COMP a f FST) `SPLIT` (COMP b g SND)+prod_def _ _ = mzero++prod_eta :: Rule+prod_eta a (SPLIT (COMP b FST f) (COMP c SND g)) = do+ Eq <- teq b c+ guard (geq (Pf a) f g)+ success "prod-Eta" f+prod_eta _ _ = mzero++prod_functor_id :: Rule+prod_functor_id _ (SPLIT FST SND) =+ success "prod-Functor-Id" ID+prod_functor_id _ (PROD ID ID) =+ success "prod-Functor-Id" ID+prod_functor_id _ _ = mzero++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)) =+ success "prod-Functor-Comp" $ COMP c f h ><= COMP d g i+prod_functor_comp' _ _ = mzero++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)) =+ success "prod-Cancel" $ COMP a f FST+prod_cancel' t (COMP _ SND (SPLIT f g)) =+ success "prod-Cancel" g+prod_cancel' (Fun (Prod a b) _) (COMP _ SND (f `PROD` g)) =+ success "prod-Cancel" $ COMP b g SND+prod_cancel' _ _ = mzero++prod_fusion = comp prod_fusion'+prod_fusion' :: Rule+prod_fusion' t (COMP c (SPLIT f g) h) =+ 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)) =+ 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 =+ success "swap-Def" $ SND /\= FST+swap_def _ _ = mzero++assocl_def :: Rule+assocl_def (Fun (Prod a (Prod b c)) _) ASSOCL =+ success "assocl-Def" $ (ID ><= FST) /\= (COMP (Prod b c) SND SND)+assocl_def _ _ = mzero++assocr_def :: Rule+assocr_def (Fun (Prod (Prod a b) c) _) ASSOCR =+ success "assocr-Def" $ (COMP (Prod a b) FST FST) /\= (SND ><= ID)+assocr_def _ _ = mzero
+ src/Transform/Rules/PF/Rec.hs view
@@ -0,0 +1,454 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Rules.PF.Rec+-- 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 recursion.+--+-----------------------------------------------------------------------------++module Transform.Rules.PF.Rec where+ +import Data.Type+import Data.Equal+import Transform.Rewriting+import Transform.Rules.PF.Combinators+import {-# SOURCE #-} Transform.Rules.PF+import Transform.Rules.Lenses.Lists++import Prelude hiding (Functor(..))+import Control.Monad hiding (Functor(..))+import Control.Monad.RWS hiding (Functor(..),Any)+import Unsafe.Coerce++import Generics.Pointless.Combinators hiding (comp)+import Generics.Pointless.Functors+import Generics.Pointless.Lenses++-- ** In / Out++in_iso = comp in_iso'+in_iso' :: Rule+in_iso' (Fun a b) (COMP _ INN OUT) = do+ Eq <- teq a b+ success "in-Iso" ID+in_iso' _ _ = mzero++out_iso = comp out_iso'+out_iso' :: Rule+out_iso' (Fun a b) (COMP _ OUT INN) = do+ Eq <- teq a b+ success "out-Iso" ID+out_iso' _ _ = mzero++-- ** Functors++functor_id :: Rule+functor_id (Fun _ _) (FMAP fctr (Fun a _) ID) =+ success "functor-Id" ID+functor_id _ _ = mzero++functor_comp = comp functor_comp'+functor_comp' :: Rule+functor_comp' (Fun fa fc) (COMP fb (FMAP fctr (Fun b c) f) (FMAP fctr' (Fun a b') g)) = do+ Eq <- feq fctr fctr'+ Eq <- teq b b'+ 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+ 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++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 (fctrf :*!: fctrg) (Fun a c) f) = do+ let (fa,fc) = (rep fctrf a,rep fctrf c)+ (ga,gc) = (rep fctrg a,rep fctrg c)+ t = (Prod (Prod fa fc) (Prod ga gc))+ f' <- fzip_def (Fun (Prod fa fc) (rep fctrf (Prod a c))) (FZIP fctrf (Fun a c) f)+ g' <- fzip_def (Fun (Prod ga gc) (rep fctrg (Prod a c))) (FZIP fctrg (Fun a c) f)+ success "fzip-Def" $ COMP t (f' ><= g') distp_pf+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)+ t = (Either (Either (Prod fa fc) (Prod fa gc)) (Either (Prod ga fc) (Prod ga gc)))+ f' <- fzip_def (Fun (Prod fa fc) (rep fctrf (Prod a c))) (FZIP fctrf (Fun a c) f)+ g' <- fzip_def (Fun (Prod ga gc) (rep fctrg (Prod a c))) (FZIP fctrg (Fun a c) f)+ let l = f' \/= (COMP fa (FMAP fctrf (Fun a (Prod a c)) (ID /\= f)) FST)+ r = (COMP ga (FMAP fctrg (Fun a (Prod a c)) (ID /\= f)) FST) \/= g'+ success "fzip-Def" $ COMP t (l -|-= r) $ dists_pf $ Prod (Either fa ga) (Either fc gc)+fzip_def (Fun _ _) (FZIP (fctrf :@!: fctrg) (Fun a c) f) = do+ let (fa,fc,fac) = (rep fctrf a,rep fctrf c,rep fctrf (Prod a c))+ (ga,gc,gac) = (rep fctrg a,rep fctrg c,rep fctrg (Prod a c))+ t = (rep fctrf (Prod ga gc))+ f' <- fzip_def (Fun (Prod (rep fctrf ga) (rep fctrf gc)) t) (FZIP fctrf (Fun ga gc) (FMAP fctrg (Fun a c) f))+ g' <- fzip_def (Fun (Prod ga gc) gac) (FZIP fctrg (Fun a c) f)+ success "fzip-Def" $ COMP t (FMAP fctrf (Fun (Prod ga gc) gac) g') f'+fzip_def _ _ = mzero++-- ** Catas++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+ 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+ )+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+ 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 <- 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+ 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+ debug "cata-Shift" (Pf t) v+ Eq <- teq (rep g b) gb+ eta' <- natCoerce f g b eta a+ success "cata-Shift" $ ANA $ COMP (rep f a) eta' OUT+cata_shift _ _ = mzero++-- ** Paras++para_reflex :: Rule+para_reflex (Fun (a@(Data _ fctr)) (b@(Data _ fctrb))) (PARA (COMP fab INN f)) = 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+ 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+para_cancel' _ _ = mzero++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' _ _ = mzero++-- ** Anas++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')+ Eq <- teq fa (rep fctr a)+ let fb = rep fctr b+ success "ana-Cancel" $ COMP fb (FMAP fctr (Fun b a) 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+ 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 <- 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+ 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+ debug "ana-Shift" (Pf t) v+ Eq <- teq (rep f a) fa+ eta' <- natCoerce f g a eta b+ success "ana-Shift" $ CATA $ COMP (rep g b) INN eta'+ana_shift _ _ = mzero++-- ** Hylos++hylo_shift = comp hylo_shift'+hylo_shift' :: Rule+hylo_shift' q@(Fun a c) v@(COMP b@(Data _ fctrf) (CATA g) (ANA h)) = do+ debug "hylo-Shift" (Pf q) v+ COMPF fctrg c' gold geta <- natSplit c c fctrf g+ Eq <- teq c c'+ let t = Fun (rep fctrf c) (rep fctrg c)+ debug "hyloSplit" (Pf t) geta+ heta <- natCoerce fctrf fctrg c geta a+ success "hylo-Shift" $ COMP (fixof fctrg) (CATA gold) (ANA $ COMP (rep fctrf a) heta h)+hylo_shift' _ _ = mzero++hylo_id = comp hylo_id'+hylo_id' :: Rule+hylo_id' t@(Fun c a) v@(COMP b@(Data _ 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)+ success "hylo-Id" ID+hylo_id' _ _ = mzero++-- ** Natural transformations++natProof :: (Functor f,Functor g) => Fctr f -> Fctr g -> Type a -> Pf (Rep f a -> Rep g a) -> Bool+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+ 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++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+natSplit a b (K t) f = do+ return $ COMPF (K b) a ID f +-- Sums+natSplit a b fctr@(fctrf :+!: fctrg) v@(EITHER f g) = (do+ COMPF fctrx a' fold feta <- natSplit a b fctrf f+ COMPF fctry a'' gold geta <- natSplit a b fctrg g+ Eq <- teq a a'+ Eq <- teq a a''+ return $ COMPF (fctrx :+!: fctry) a (EITHER fold gold) (feta -|-= geta))+ `mplus` (do+ COMPF fctrx a' fold feta <- natSplit a b fctrf f+ Eq <- teq a a'+ return $ COMPF (fctrx :+!: fctrg) a (EITHER fold g) (feta -|-= ID))+ `mplus` (do+ COMPF fctry a'' gold geta <- natSplit a b fctrg g+ Eq <- teq a a''+ return $ COMPF (fctrf :+!: fctry) a (EITHER f gold) (ID -|-= geta))+natSplit a (Either b c) fctr@(fctrf :+!: fctrg) v@(f `SUM` g) = (do+ COMPF fctrx a' fold feta <- natSplit a b fctrf f+ COMPF fctry a'' gold geta <- natSplit a c fctrg g+ Eq <- teq a a'+ Eq <- teq a a''+ return $ COMPF (fctrx :+!: fctry) a (fold -|-= gold) (feta -|-= geta))+ `mplus` (do+ COMPF fctrx a' fold feta <- natSplit a b fctrf f+ Eq <- teq a a'+ return $ COMPF (fctrx :+!: fctrg) a (fold -|-= g) (feta -|-= ID))+ `mplus` (do+ COMPF fctry a'' gold geta <- natSplit a c fctrg g+ Eq <- teq a a''+ return $ COMPF (fctrf :+!: fctry) a (f -|-= gold) (ID -|-= geta))+-- Products+natSplit a b (fctrf :*!: fctrg) FST = do+ return $ COMPF fctrf a ID FST+natSplit a b (fctrf :*!: fctrg) SND = do+ return $ COMPF fctrg a ID SND+natSplit a b fctr v@(_ `SPLIT` _) = do+ v' <- (prod_undef ||| (prod_unfusion >>> comp1 (try prod_undef))) (Fun (rep fctr a) b) v+ natSplit a b fctr v'+natSplit a (Prod b c) fctr@(fctrf :*!: fctrg) v@(f `PROD` g) = (do+ COMPF fctrx a' fold feta <- natSplit a b fctrf f+ COMPF fctry a'' gold geta <- natSplit a c fctrg g+ Eq <- teq a a'+ Eq <- teq a a''+ return $ COMPF (fctrx :*!: fctry) a (fold ><= gold) (feta ><= geta))+ `mplus` (do+ COMPF fctrx a' fold feta <- natSplit a b fctrf f+ Eq <- teq a a'+ return $ COMPF (fctrx :*!: fctrg) a (fold ><= g) (feta ><= ID))+ `mplus` (do+ COMPF fctry a'' gold geta <- natSplit a c fctrg g+ Eq <- teq a a''+ return $ COMPF (fctrf :*!: fctry) a (f ><= gold) (ID ><= geta))+-- Composition+natSplit a b fctr e@(COMP _ _ _) = (do+ COMP c f g <- rightmost (Fun (rep fctr a) b) e+ COMPF fctrx a' gold geta <- natSplit a c fctr g+ Eq <- teq a a'+ COMPF fctry a'' fold feta <- natSplit a b fctrx (COMP c f gold)+ Eq <- teq a a''+ let old = fold+ eta = COMP (rep fctrx a) feta geta+ return $ COMPF fctry a old eta)+ `mplus` (do+ COMP c f g <- rightmost (Fun (rep fctr a) b) e+ COMPF fctrx a' gold geta <- natSplit a c fctr g+ Eq <- teq a a'+ let old = COMP c f gold+ eta = geta+ return $ COMPF fctrx a old eta)+-- Id and unrecognized cases match here+natSplit a b fctr f = mzero++-- ** Internal converses for fusion rules++rconv_cancel = comp rconv_cancel'+rconv_cancel' :: Rule+rconv_cancel' t@(Fun a a') (COMP c (CATA f) (CONV (Right _) (ANA g))) = do+ f' <- ana_shift (Fun c a) (ANA g)+ rconv_cancel' t (COMP c (CATA f) (CONV (Right _L) f'))+rconv_cancel' t@(Fun a a') (COMP c (ANA f) (CONV (Right _) (CATA g))) = do+ f' <- cata_shift (Fun c a) (CATA g)+ rconv_cancel' t (COMP c (ANA f) (CONV (Right _L) f'))+rconv_cancel' (Fun a a') (COMP c f (CONV (Right _) f')) = do+ Eq <- teq a a'+ guard $ geq (Pf (Fun c a)) f f'+ success "rconv-Cancel" ID+rconv_cancel' _ _ = mzero++lconv_cancel = comp lconv_cancel'+lconv_cancel' :: Rule+lconv_cancel' t@(Fun a a') (COMP c (CONV (Left _) (ANA g)) (CATA f)) = do+ f' <- ana_shift (Fun a' c) (ANA g)+ lconv_cancel' t $ COMP c (CONV (Left _L) f') (CATA f)+lconv_cancel' t@(Fun a a') v@(COMP c (CONV (Left _) (CATA g)) (ANA f)) = do+ f' <- cata_shift (Fun a' c) (CATA g)+ lconv_cancel' t $ COMP c (CONV (Left _L) f') (ANA f)+lconv_cancel' (Fun c c') (COMP a (CONV (Left _) f') f) = do+ Eq <- teq c c'+ guard $ geq (Pf (Fun c a)) f f'+ success "rconv-Cancel" ID+lconv_cancel' _ _ = mzero++conv_comp :: Rule+conv_comp (Fun _ _) (CONV e (COMP b f g)) =+ success "conv-Comp" $ COMP b (CONV e g) (CONV e f)+conv_comp _ _ = mzero++conv_conv :: Rule+conv_conv _ (CONV _ (CONV _ f)) =+ success "conv-Conv" f+conv_conv _ _ = mzero++conv_id :: Rule+conv_id _ (CONV _ ID) =+ 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
+ src/Transform/Rules/PF/Sums.hs view
@@ -0,0 +1,104 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Rules.PF.Sums+-- 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 sums.+--+-----------------------------------------------------------------------------++module Transform.Rules.PF.Sums where++import Data.Type+import Data.Equal+import Transform.Rewriting+import Transform.Rules.PF.Combinators++import Prelude hiding (Functor(..))+import Control.Monad hiding (Functor(..))++-- ** Sums++sum_def :: Rule+sum_def t@(Fun _ (Either a b)) (SUM f g) =+ success "sum-Def" $ (EITHER (COMP a INL f) (COMP b INR g))+sum_def _ _ = mzero++sum_eta :: Rule+sum_eta a (EITHER (COMP b1 k1 INL) (COMP b2 k2 INR)) = do+ Eq <- teq b1 b2+ guard (geq (Pf a) k1 k2)+ success "sum-Eta" k1+sum_eta _ _ = mzero++sum_functor_id :: Rule+sum_functor_id _ (EITHER INL INR) =+ success "sum-Functor-Id" ID+sum_functor_id _ (SUM ID ID) =+ success "sum-Functor-Id" ID+sum_functor_id _ _ = mzero++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)) =+ success "sum-Functor-Comp" $ COMP c f h -|-= COMP d g i+sum_functor_comp' _ _ = mzero++sum_cancel = comp sum_cancel'+sum_cancel' :: Rule+sum_cancel' t (COMP _ (EITHER f g) INL) =+ success "sum-Cancel" f+sum_cancel' (Fun _ (Either c d)) (COMP _ (f `SUM` g) INL) =+ success "sum-Cancel" $ COMP c INL f+sum_cancel' t (COMP _ (EITHER f g) INR) =+ success "sum-Cancel" g+sum_cancel' (Fun _ (Either c d)) (COMP _ (f `SUM` g) INR) =+ success "sum-Cancel" $ COMP d INR g+sum_cancel' _ _ = mzero++sum_fusion = comp 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)+sum_fusion' _ _ = mzero++sum_absor = comp sum_absor'+sum_absor' :: Rule+sum_absor' (Fun _ _) (COMP (Either c d) (f `EITHER` g) (h `SUM` i)) = + 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+coswap_def (Fun (Either a b) _) COSWAP =+ success "coswap-Def" $ INR \/= INL+coswap_def _ _ = mzero++coassocl_def :: Rule+coassocl_def (Fun (Either a (Either b c)) _) COASSOCL =+ 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 =+ success "coassocr-Def" $ (ID -|-= INL) \/= (COMP (Either b c) INR INR)+coassocr_def _ _ = mzero+
+ src/Transform/Rules/SYB.hs view
@@ -0,0 +1,37 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Rules.SYB+-- 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 strategic combinators.+--+-----------------------------------------------------------------------------++module Transform.Rules.SYB where++import Transform.Rewriting+import Transform.Rules.SYB.TP+import Transform.Rules.SYB.TU++optimise_syb :: Rule+optimise_syb = optimise_tp >>> optimise_tu++optimise_tp :: Rule+optimise_tp = innermost rules+ where rules = top nop_applyT ||| top seq_applyT+ ||| top gmapT_applyT ||| top everywhere_applyT+ ||| top mkT_applyT ||| top extT_applyT++optimise_tu :: Rule+optimise_tu = innermost rules+ where rules = top emptyQ_applyQ ||| top union_applyQ+ ||| top gmapQ_applyQ ||| top everything_applyQ+ ||| top mkQ_applyQ ||| top extQ_applyQ
+ src/Transform/Rules/SYB/TP.hs view
@@ -0,0 +1,53 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Rules.SYB.TP+-- 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+-- +-- Specialization rules for type-preserving strategy combinators.+--+-----------------------------------------------------------------------------++module Transform.Rules.SYB.TP where++import Data.Type+import Data.Eval+import Transform.Rewriting hiding (gmapQ)+import Control.Monad++nop_applyT :: Rule+nop_applyT _ (APPLY _ NOP) = success "nop-applyT" ID+nop_applyT _ _ = mzero++seq_applyT :: Rule+seq_applyT _ (APPLY t (SEQ f g)) = success "seq-applyT" (COMP t (APPLY t f) (APPLY t g))+seq_applyT _ _ = mzero++gmapT_applyT :: Rule+gmapT_applyT _ (APPLY a (ALL f)) = success "gmapT-applyT" (allT a f)+gmapT_applyT _ _ = mzero++everywhere_applyT :: Rule+everywhere_applyT _ (APPLY a (EVERYWHERE f)) = success "everywhere-applyT" (everywhereT a f)+everywhere_applyT _ (APPLY a (EVERYWHERE' f)) = success "everywhere-applyT" (everywhereT' a f)+everywhere_applyT _ _ = mzero++mkT_applyT :: Rule+mkT_applyT _ (APPLY a (MKT b f)) = success "mkT-applyT" (mkT a b f)+mkT_applyT _ _ = mzero++extT_applyT :: Rule+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
+ src/Transform/Rules/SYB/TU.hs view
@@ -0,0 +1,51 @@+-----------------------------------------------------------------------------+-- |+-- Module : Transform.Rules.SYB.TU+-- 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+-- +-- Specialization rules for type-unifying strategy combinators.+--+-----------------------------------------------------------------------------++module Transform.Rules.SYB.TU where++import Data.Type+import Data.Eval+import Transform.Rewriting hiding (gmapQ)+import Control.Monad++emptyQ_applyQ :: Rule+emptyQ_applyQ _ (APPLYQ _ EMPTYQ) = success "emptyQ-applyQ" ZERO+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 _ _ = mzero++gmapQ_applyQ :: Rule+gmapQ_applyQ (Fun _ r) (APPLYQ a (GMAPQ f)) = success "gmapQ-applyQ" (gmapQ r a f)+gmapQ_applyQ _ _ = mzero++everything_applyQ :: Rule+everything_applyQ (Fun a r) (APPLYQ _ (EVERYTHING f)) = success "everything-applyQ" (everythingQ r a f)+everything_applyQ _ _ = mzero++mkQ_applyQ :: Rule+mkQ_applyQ _ (APPLYQ a (MKQ b f)) = success "mkQ-applyQ" (mkQ a b f)+mkQ_applyQ _ _ = mzero++extQ_applyQ :: Rule+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