diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README b/README new file mode 100644 --- /dev/null +++ b/README @@ -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 diff --git a/Setup.lhs b/Setup.lhs new file mode 100644 --- /dev/null +++ b/Setup.lhs @@ -0,0 +1,3 @@ +#!/usr/bin/env runhaskell +> import Distribution.Simple +> main = defaultMain diff --git a/Test.hs b/Test.hs new file mode 100644 --- /dev/null +++ b/Test.hs @@ -0,0 +1,5 @@ +module Test where + +import.Transform.Examples.Company +import Transform.Examples.Imdb +import Transform.Examples.Women diff --git a/pointless-rewrite.cabal b/pointless-rewrite.cabal new file mode 100644 --- /dev/null +++ b/pointless-rewrite.cabal @@ -0,0 +1,49 @@ +Name: pointless-rewrite +Version: 0.0.1 +License: BSD3 +License-file: LICENSE +Author: Alcino Cunha , Hugo Pacheco +Maintainer: Hugo Pacheco +Synopsis: Pointless Rewrite library +Description: Library that implements a rewrite system for point-free expressions. Application scenarios include normal functional programs, strategic combinators () and bidirectional lenses (), 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 diff --git a/src/Data/Equal.hs b/src/Data/Equal.hs new file mode 100644 --- /dev/null +++ b/src/Data/Equal.hs @@ -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 diff --git a/src/Data/Eval.hs b/src/Data/Eval.hs new file mode 100644 --- /dev/null +++ b/src/Data/Eval.hs @@ -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} + diff --git a/src/Data/Lens.hs b/src/Data/Lens.hs new file mode 100644 --- /dev/null +++ b/src/Data/Lens.hs @@ -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 diff --git a/src/Data/Spine.hs b/src/Data/Spine.hs new file mode 100644 --- /dev/null +++ b/src/Data/Spine.hs @@ -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 "") +toSpine (Pf (Lns Any Any)) e = e `As` (pcon "") +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" diff --git a/src/Data/Type.hs b/src/Data/Type.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type.hs @@ -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 diff --git a/src/Transform/Examples/Company.hs b/src/Transform/Examples/Company.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Examples/Company.hs @@ -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 diff --git a/src/Transform/Examples/Imdb.hs b/src/Transform/Examples/Imdb.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Examples/Imdb.hs @@ -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 + diff --git a/src/Transform/Examples/Women.hs b/src/Transform/Examples/Women.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Examples/Women.hs @@ -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 + diff --git a/src/Transform/Rewriting.hs b/src/Transform/Rewriting.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Rewriting.hs @@ -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) diff --git a/src/Transform/Rules/Lenses.hs b/src/Transform/Rules/Lenses.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Rules/Lenses.hs @@ -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" } diff --git a/src/Transform/Rules/Lenses.hs-boot b/src/Transform/Rules/Lenses.hs-boot new file mode 100644 --- /dev/null +++ b/src/Transform/Rules/Lenses.hs-boot @@ -0,0 +1,5 @@ +module Transform.Rules.Lenses where + +import Transform.Rewriting + +optimise_lns :: Rule diff --git a/src/Transform/Rules/Lenses/Combinators.hs b/src/Transform/Rules/Lenses/Combinators.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Rules/Lenses/Combinators.hs @@ -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 diff --git a/src/Transform/Rules/Lenses/Dists.hs b/src/Transform/Rules/Lenses/Dists.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Rules/Lenses/Dists.hs @@ -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 + + + diff --git a/src/Transform/Rules/Lenses/Lists.hs b/src/Transform/Rules/Lenses/Lists.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Rules/Lenses/Lists.hs @@ -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 + diff --git a/src/Transform/Rules/Lenses/Products.hs b/src/Transform/Rules/Lenses/Products.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Rules/Lenses/Products.hs @@ -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 diff --git a/src/Transform/Rules/Lenses/Rec.hs b/src/Transform/Rules/Lenses/Rec.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Rules/Lenses/Rec.hs @@ -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 diff --git a/src/Transform/Rules/Lenses/Sums.hs b/src/Transform/Rules/Lenses/Sums.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Rules/Lenses/Sums.hs @@ -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 + + diff --git a/src/Transform/Rules/PF.hs b/src/Transform/Rules/PF.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Rules/PF.hs @@ -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 diff --git a/src/Transform/Rules/PF.hs-boot b/src/Transform/Rules/PF.hs-boot new file mode 100644 --- /dev/null +++ b/src/Transform/Rules/PF.hs-boot @@ -0,0 +1,5 @@ +module Transform.Rules.PF where + +import Transform.Rewriting + +optimise_pf :: Rule diff --git a/src/Transform/Rules/PF/Combinators.hs b/src/Transform/Rules/PF/Combinators.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Rules/PF/Combinators.hs @@ -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 + + diff --git a/src/Transform/Rules/PF/Dists.hs b/src/Transform/Rules/PF/Dists.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Rules/PF/Dists.hs @@ -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 diff --git a/src/Transform/Rules/PF/Products.hs b/src/Transform/Rules/PF/Products.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Rules/PF/Products.hs @@ -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 diff --git a/src/Transform/Rules/PF/Rec.hs b/src/Transform/Rules/PF/Rec.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Rules/PF/Rec.hs @@ -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 diff --git a/src/Transform/Rules/PF/Sums.hs b/src/Transform/Rules/PF/Sums.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Rules/PF/Sums.hs @@ -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 + diff --git a/src/Transform/Rules/SYB.hs b/src/Transform/Rules/SYB.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Rules/SYB.hs @@ -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 diff --git a/src/Transform/Rules/SYB/TP.hs b/src/Transform/Rules/SYB/TP.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Rules/SYB/TP.hs @@ -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 diff --git a/src/Transform/Rules/SYB/TU.hs b/src/Transform/Rules/SYB/TU.hs new file mode 100644 --- /dev/null +++ b/src/Transform/Rules/SYB/TU.hs @@ -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