DrHylo (empty) → 0.0.1
raw patch · 17 files changed
+1424/−0 lines, 17 filesdep +arraydep +basedep +containerssetup-changed
Dependencies added: array, base, containers, haskell-src-exts, mtl, pointless-haskell, pretty, syb
Files
- DrHylo.cabal +53/−0
- LICENSE +31/−0
- README +37/−0
- Sample.hs +57/−0
- Setup.lhs +3/−0
- lib/Language/Pointfree/Parser.hs +95/−0
- lib/Language/Pointfree/Pretty.hs +146/−0
- lib/Language/Pointfree/Syntax.hs +28/−0
- lib/Language/Pointwise/Matching.hs +63/−0
- lib/Language/Pointwise/Parser.hs +139/−0
- lib/Language/Pointwise/Pretty.hs +55/−0
- lib/Language/Pointwise/Syntax.hs +105/−0
- src/DrHylo.hs +176/−0
- src/FunctorOf.hs +215/−0
- src/Hylos.hs +127/−0
- src/Matching.hs +63/−0
- src/PwPf.hs +31/−0
+ DrHylo.cabal view
@@ -0,0 +1,53 @@+Name: DrHylo+Version: 0.0.1+License: BSD3+License-file: LICENSE+Author: Alcino Cunha <alcino@di.uminho.pt>, Hugo Pacheco <hpacheco@di.uminho.pt>+Maintainer: Hugo Pacheco <hpacheco@di.uminho.pt>+Synopsis: A tool for deriving hylomorphisms+Description:+ DrHylo is a tool for deriving hylomorphisms from a restricted Haskell syntax. It is based on the algorithm first presented in the paper Deriving Structural Hylomorphisms From Recursive Definitions at ICFP'96 by Hu, Iwasaki, and Takeichi.+ The generated code can be run with Pointless Haskell (<http://hackage.haskell.org/cgi-bin/hackage-scripts/package/pointless-haskell>), allowing the visualization of the recursion trees of Haskell functions.+Homepage: http://haskell.di.uminho.pt/wiki/DrHylo++Category: Language++extra-source-files: README, Sample.hs+Data-files: ++Build-type: Simple+Cabal-Version: >=1.2++Flag splitBase+ Description: Choose the new smaller, split-up base package.++Library+ Hs-Source-Dirs: lib+ Build-Depends: base >= 4, pointless-haskell, mtl, haskell-src-exts >= 0.4.4, syb+ exposed-modules:+ Language.Pointwise.Matching,+ Language.Pointwise.Parser,+ Language.Pointwise.Pretty,+ Language.Pointwise.Syntax,+ Language.Pointfree.Parser,+ Language.Pointfree.Pretty,+ Language.Pointfree.Syntax+ extensions: DeriveDataTypeable++Executable DrHylo+ Main-is: DrHylo.hs+ Hs-Source-Dirs: src, lib+ Build-Depends: containers+ if flag(splitBase)+ Build-Depends: base >= 3, array >= 0.1, pretty >= 1.0+ else+ Build-Depends: base < 3+ other-modules:+ DrHylo,+ FunctorOf,+ Hylos,+ Matching,+ PwPf+ other-modules:++ extensions: DeriveDataTypeable
+ LICENSE view
@@ -0,0 +1,31 @@+Copyright (c) 2008, University of Minho++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are+met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * The names of contributors may not be used to endorse or promote+ products derived from this software without specific prior+ written permission. ++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README view
@@ -0,0 +1,37 @@+DrHylo++This cabal package can be installed with:++$ cabal install DrHylo++For a manual install, execute:++$ runhaskell Setup.lhs configure+$ runhaskell Setup.lhs build+$ runhaskell Setup.lhs install++DrHylo derives point-free hylomorphisms from restricted Haskell syntax.++Usage: DrHylo [OPTION...]+ -o[FILE] --output[=FILE] output FILE+ -i[FILE] --input[=FILE] input FILE+ -f --fix use fixpoints instead of hylomorphisms+ -w --pointwise do not convert to point-free+ -O --observable generate observable hylomorphisms++The module Sample.hs defines some Haskell definitions that are compliant with the DrHylo supported syntax.+As an example, we can generate observable hylomorphisms for the functions frm Sample.hs into some file Out.hs:++$ DrHylo -iSample.hs -oOut.hs -O++The resulting file Out.hs can be normally interpreted with GHC as long as we have the Pointless Haskell library installed.++$ ghci Out.hs -fglasgow-exts -XUndecidableInstances++Since we asked for observable hylomorphisms, we can inspect the recursion tree for hylomorphisms via GHood. Just make sure that you have the GHood library installed (available on Hackage). A sample execution is:++> let four = Succ $ Succ $ Succ $ Succ Zero+> runO $ print $ fact four+++
+ Sample.hs view
@@ -0,0 +1,57 @@+module Sample where++comp :: (b->c, a->b) -> (a->c)+comp (f,g) y = f (g y)++swap :: (a,b) -> (b,a)+swap (x,y) = (y,x)++assocr :: ((a,b),c) -> (a,(b,c))+assocr ((x,y),z) = (x,(y,z))++distr :: (a, Either b c) -> Either (a,b) (a,c)+distr (x, Left y) = Left (x,y)+distr (x, Right y) = Right (x,y)++coswap :: Either a b -> Either b a+coswap (Left y) = Right y+coswap (Right y) = Left y++undistr :: Either (a,b) (a,c) -> (a, Either b c)+undistr (Left (y,z)) = (y, Left z)+undistr (Right (x,z)) = (x, Right z)++data Nat = Zero | Succ Nat deriving Show++plus :: (Nat, Nat) -> Nat+plus (Zero, z) = z+plus (Succ n, z) = Succ (plus (n,z))++mult :: (Nat, Nat) -> Nat+mult (Zero, x) = Zero+mult (Succ n, x) = plus (x, mult (n, x))++fact :: Nat -> Nat+fact Zero = Succ Zero+fact (Succ n) = mult (Succ n, fact n)++len :: [a] -> Nat+len [] = Zero+len (h:t) = Succ (len t)++fib :: Nat -> Nat+fib Zero = Succ Zero+fib (Succ Zero) = Succ Zero+fib (Succ (Succ x)) = plus (fib x, fib (Succ x))++cat :: [a] -> [a] -> [a]+cat [] l = l+cat (h:t) l = h:(cat t l)++data Tree a = Leaf | Node a (Tree a) (Tree a)++inorder :: Tree a -> [a]+inorder Leaf = []+inorder (Node x l r) = cat (inorder l) (x:(inorder r))++
+ Setup.lhs view
@@ -0,0 +1,3 @@+#!/usr/bin/env runhaskell+> import Distribution.Simple+> main = defaultMain
+ lib/Language/Pointfree/Parser.hs view
@@ -0,0 +1,95 @@+module Language.Pointfree.Parser where++import Language.Pointfree.Syntax+import Language.Haskell.Exts.Syntax++hs2pf (Paren e) = hs2pf e+hs2pf (Var (UnQual (Ident "id"))) = return ID+hs2pf (Var (UnQual (Ident "fst"))) = return FST+hs2pf (Var (UnQual (Ident "snd"))) = return SND+hs2pf (Var (UnQual (Ident "inl"))) = return INL+hs2pf (Var (UnQual (Ident "inr"))) = return INR+hs2pf (Con (UnQual (Ident "Left"))) = return INL+hs2pf (Con (UnQual (Ident "Right"))) = return INR+hs2pf (Var (UnQual (Ident "app"))) = return AP+hs2pf (Var (UnQual (Ident "bang"))) = return BANG+hs2pf (Var (UnQual (Ident "inn"))) = return IN+hs2pf (Var (UnQual (Ident "out"))) = return OUT+hs2pf (Var (UnQual (Ident str))) = return $ Macro str []+hs2pf (InfixApp e1 (QVarOp (UnQual (Symbol "."))) e2)+ = do t1 <- hs2pf e1+ t2 <- hs2pf e2+ return $ t1 :.: t2+hs2pf (InfixApp e1 (QVarOp (UnQual (Symbol "/\\"))) e2)+ = do t1 <- hs2pf e1+ t2 <- hs2pf e2+ return $ t1 :/\: t2+-- hs2pf (App (App (Var (UnQual (Ident "either"))) e1) e2)+hs2pf (InfixApp e1 (QVarOp (UnQual (Symbol "\\/"))) e2)+ = do t1 <- hs2pf e1+ t2 <- hs2pf e2+ return $ t1 :\/: t2+hs2pf (InfixApp e1 (QVarOp (UnQual (Symbol sym))) e2)+ = do t1 <- hs2pf e1+ t2 <- hs2pf e2+ return $ Macro ('(':sym++")") [t1,t2]+hs2pf (App (Var (UnQual (Ident "curry"))) e) + = hs2pf e >>= return . Curry+hs2pf (App (App (App (Var (UnQual (Ident "hylo")))+ (Paren (ExpTypeSig _ (Var (UnQual (Ident "_L")))+ typ))) e1) e2)+ = do typ' <- hs2type typ+ t1 <- hs2pf e1+ t2 <- hs2pf e2+ return $ Hylo typ' t1 t2+hs2pf (App (App (App (Var (UnQual (Ident "hyloO")))+ (Paren (ExpTypeSig _ (Var (UnQual (Ident "_L")))+ typ))) e1) e2)+ = do typ' <- hs2type typ+ t1 <- hs2pf e1+ t2 <- hs2pf e2+ return $ HyloO typ' t1 t2+---- when "Point String" becomes "Point Pointwise.Term":+--hs2pf (App (Var (UnQual (Ident "pnt"))) pw) +-- = hs2pw pw >>= return . Point+hs2pf (App x y) -- has to be a parametrized macro+ = do term1 <- hs2pf x+ term2 <- hs2pf y+ case term1 of (Macro v lst) -> return (Macro v (lst++[term2]))+ x -> fail "macro expected"+hs2pf x = fail "not a valid pf term"++++hs2type (TyCon (UnQual (Ident "One"))) = return One+hs2type (TyTuple _ [e1,e2])+ = do t1 <- hs2type e1+ t2 <- hs2type e2+ return $ t1 :*: t2+hs2type (TyApp (TyApp (TyCon (UnQual (Ident "Either"))) e1) e2)+ = do t1 <- hs2type e1+ t2 <- hs2type e2+ return $ t1 :+: t2+hs2type (TyFun e1 e2)+ = do t1 <- hs2type e1+ t2 <- hs2type e2+ return $ t1 :-> t2+hs2type (TyVar (Ident v)) = return $ Base v+hs2type (TyApp (TyCon (UnQual (Ident "Fix"))) e)+ = hs2func e >>= return . Fix+ where+ hs2func (TyCon (UnQual (Ident "Id"))) = return Id+ hs2func (TyApp (TyCon (UnQual (Ident "Const"))) e)+ = hs2type e >>= return . Const+ -- grammar not rich enough to allow infix constructors+ hs2func (TyApp (TyApp (TyCon (UnQual (Symbol ":*:"))) e1) e2)+ = do t1 <- hs2func e1+ t2 <- hs2func e2+ return $ t1 :**: t2+ hs2func (TyApp (TyApp (TyCon (UnQual (Symbol ":+:"))) e1) e2)+ = do t1 <- hs2func e1+ t2 <- hs2func e2+ return $ t1 :++: t2+ hs2func _ = fail "not a valid type"++hs2type _ = fail "not a valid type"
+ lib/Language/Pointfree/Pretty.hs view
@@ -0,0 +1,146 @@+module Language.Pointfree.Pretty+ ( pf2hs+ , type2hs+ ) where++import Language.Pointfree.Syntax as Pointfree+import Language.Haskell.Exts.Syntax as Exts+++instance Show Term where+ showsPrec d (ID) = showString "id"+ showsPrec d (BANG) = showString "bang"+ showsPrec d (AP) = showString "app"+ showsPrec d (Curry aa) = -- showParen (d >= 10)+ (showString "curry" . showChar ' ' . showsPrec 10 aa)+ showsPrec d (aa :.: ab@(_ :.: _)) = showParen (d >= 10)+ (showsPrec 10 aa . showChar '.' . showsPrec 0 ab)+ showsPrec d (aa :.: ab) = showParen (d >= 10)+ (showsPrec 10 aa . showChar '.' . showsPrec 10 ab)+ showsPrec d (aa@(_ :\/: _) :\/: ab) = showParen (d >= 10)+ (showsPrec 0 aa . showString " \\/ " . showsPrec 10 ab)+ showsPrec d (aa :\/: ab) = showParen (d >= 10)+ (showsPrec 10 aa . showString " \\/ " . showsPrec 10 ab)+ showsPrec d (aa@(_ :/\: _) :/\: ab) = showParen (d >= 10)+ (showsPrec 0 aa . showString " /\\ " . showsPrec 10 ab)+ showsPrec d (aa :/\: ab) = showParen (d >= 10)+ (showsPrec 10 aa . showString " /\\ " . showsPrec 10 ab)+ showsPrec d (FST) = showString "fst"+ showsPrec d (SND) = showString "snd"+ showsPrec d (INL) = showString "inl"+ showsPrec d (INR) = showString "inr"+ showsPrec d (Point aa) = showParen (d >= 10)+ (showString "pnt" . showChar ' ' . showsPrec 10 aa)+ showsPrec d (IN) = showString "inn"+ showsPrec d (OUT) = showString "out"+ showsPrec d (Hylo typ aa ab) = showParen (d >= 10)+ (showString "hylo_{" . showsPrec 0 typ . showString "} " .+ showsPrec 10 aa . showChar ' ' . showsPrec 10 ab)+ showsPrec d (HyloO typ aa ab) = showParen (d >= 10)+ (showString "hyloO_{" . showsPrec 0 typ . showString "} " .+ showsPrec 10 aa . showChar ' ' . showsPrec 10 ab)+ showsPrec d (Macro ('(':sym) [aa,ab]) = showParen (d >= 10)+ (showsPrec 10 aa . showString (" "++(init sym)++" ") . showsPrec 10 ab)+-- showsPrec d (Macro "sum" [aa,ab]) = showParen (d >= 10)+-- (showsPrec 10 aa . showString " -|- " . showsPrec 10 ab)+ showsPrec d (Macro aa []) =+ showChar '\'' . showString aa . showChar '\''+ showsPrec d (Macro aa lst) = showParen (d >= 10)+ (showChar '\'' . showString aa . showString "' " .+ showsPrec 10 lst)++instance Show Pointfree.Type+ where+ show One = "One"+ show (Base s) = s+ show (Fix (Const One :++: Const One)) = "Bool"+ show (Fix (Const One :++: Id)) = "Int"+ show (Fix (Const One :++: (Const a :**: Id))) = "["++(show a)++"]"+ show (Fix t) = "Fix ("++(show t)++")"+ show (t :*: u) = "("++(show t)++","++(show u)++")"+ show (t :+: u) = "Either ("++(show t)++") ("++(show u)++")"+ show (t :-> u) = "("++(show t)++" -> "++(show u)++")"++instance Show Funct+ where+ show Id = "Id"+ show (Const t) = "Const ("++(show t)++")"+ show (f :**: g) = "("++(show f)++" :*: "++(show g)++")"+ show (f :++: g) = "("++(show f)++" :+: "++(show g)++")"+++pf2hs :: Term -> Exp+pf2hs ID = mkVar "id"+pf2hs (t1 :.: t2) = InfixApp (mbParen$ pf2hs t1)+ (mkOp ".") (mbParen$ pf2hs t2)+pf2hs FST = mkVar "fst"+pf2hs SND = mkVar "snd"+pf2hs (t1 :/\: t2) = InfixApp (mbParen$ pf2hs t1) (mkOp "/\\")+ (mbParen$ pf2hs t2)+pf2hs INL = mkCon "inl"+pf2hs INR = mkCon "inr"+pf2hs (t1 :\/: t2) = InfixApp (mbParen$ pf2hs t1) (mkOp "\\/")+ (mbParen$ pf2hs t2)++pf2hs AP = mkVar "app"+pf2hs (Curry t1) = App (mkVar "curry") (mbParen$ pf2hs t1)++pf2hs BANG = mkVar "bang"+pf2hs (Macro ('(':sym) [t1,t2]) = InfixApp (mbParen $ pf2hs t1)+ (QVarOp (UnQual (Symbol (init sym))))+ (mbParen $ pf2hs t2)+pf2hs (Macro str []) = mkVar str+pf2hs (Macro str lst) = App (pf2hs $ Macro str (init lst))+ (mbParen $ pf2hs $ last lst)+pf2hs (Point str) = App (mkVar "pnt") (mkVar str)++pf2hs IN = mkVar "inn"+pf2hs OUT = mkVar "out"++pf2hs (Hylo typ t1 t2) = -- hylo (_L::typ) t1 t2+ App (App (App + (mkVar "hylo") (Paren $ ExpTypeSig mkLoc+ (mkVar "_L") (type2hs typ)))+ (mbParen $ pf2hs t1))+ (mbParen $ pf2hs t2)++pf2hs (HyloO typ t1 t2) = -- hyloO (_L::typ) t1 t2+ App (App (App + (mkVar "hyloO") (Paren $ ExpTypeSig mkLoc+ (mkVar "_L") (type2hs typ)))+ (mbParen $ pf2hs t1))+ (mbParen $ pf2hs t2)+++type2hs :: Pointfree.Type -> Exts.Type+type2hs One = mkTCon "One"+type2hs (Base s) = TyVar (Ident s)+type2hs (t1 :*: t2) = TyTuple Boxed [type2hs t1, type2hs t2]+type2hs (t1 :+: t2) = TyApp (TyApp (mkTCon "Either")+ (type2hs t1)) (type2hs t2)+type2hs (t1 :-> t2) = TyFun (type2hs t1) (type2hs t2)+type2hs (Fix t) = TyApp (mkTCon "Fix") (func2hs t)+ where+ func2hs Id = mkTCon "Id"+ func2hs (Const t) = TyApp (mkTCon "Const") (type2hs t)+ -- grammar not rich enough to allow infix constructors+ func2hs (f :**: g) = TyApp (TyApp (mkTCon "(:*:)")+ (func2hs f)) (func2hs g)+ func2hs (f :++: g) = TyApp (TyApp (mkTCon "(:+:)")+ (func2hs f)) (func2hs g)+++-- Auxiliary functions --+mkLoc = SrcLoc "" 0 0+mkOp = QVarOp . UnQual . Symbol+mkCon = Con . UnQual . Ident+mkVar = Var . UnQual . Ident+mkTCon = TyCon . UnQual . Ident++-- places parentisis in an expression only if it is necessary+mbParen :: Exp -> Exp+mbParen e@(App _ _) = Paren e+mbParen e@(InfixApp _ _ _) = Paren e+mbParen e@(Case _ _) = Paren e+mbParen e@(Lambda _ _ _) = Paren e+mbParen x = x
+ lib/Language/Pointfree/Syntax.hs view
@@ -0,0 +1,28 @@+module Language.Pointfree.Syntax where++data Type = One+ | Base String+ | Fix Funct+ | Type :*: Type+ | Type :+: Type+ | Type :-> Type+ deriving Eq++data Funct = Id+ | Const Type+ | Funct :**: Funct+ | Funct :++: Funct+ deriving Eq++data Term = ID | Term :.: Term + | FST | SND | Term :/\: Term+ | INL | INR | Term :\/: Term+ | AP | Curry Term+ | BANG + | Macro String [Term]+ | Point String+ | IN | OUT+ | Hylo Type Term Term+ | HyloO Type Term Term+ deriving Eq+
+ lib/Language/Pointwise/Matching.hs view
@@ -0,0 +1,63 @@+module Language.Pointwise.Matching where++import Language.Pointwise.Syntax+import Data.Generics hiding (Unit,(:*:),Inl,Inr)+import Control.Monad+import Control.Monad.State+import Generics.Pointless.Combinators+import Data.List++-- Patterm matching elimination++-- Does not detect repeated variables in patterns+-- It can be improved in the pair case: does not detect equalities up to alpha+-- conversion, neither renanes variables appearing both at the pattern and the+-- term subject to matching++getVar :: String -> StateT Int Maybe String+getVar x = do seed <- get+ modify (+1)+ return (x ++ (show seed))+ +nomatch :: Term -> StateT Int Maybe Term+nomatch (Match e []) = fail "Should not hapen given the premises"+nomatch (Match e [(Var x, rhs)]) =+ do rhs' <- nomatch rhs+ return (subst [(x,e)] rhs')+nomatch (Match e [(Unit, rhs)]) = + nomatch rhs+nomatch (Match e l) + | isPair (fst (head l)) =+ do guard (all isPair (map fst l))+ guard (all null (map (\(x :&: y, _) -> free x `intersect` free y) l))+ guard (null (free e `intersect` concat (map free (map fst l))))+ let aux = mygroup (\x y -> pwFst (fst x) == pwFst (fst y)) l+ left = map (pwFst . fst . head) aux+ rightmatch = map (nomatch . (Match (Snd e)) . map (pwSnd . fst /\ snd)) aux+ right <- sequence rightmatch+ nomatch (Match (Fst e) (zip left right))+nomatch (Match e l)+ | isInlr (fst (head l)) =+ do guard (all isInlr (map fst l))+ let left' = map (\ (Inl t, p) -> (t,p)) (filter (isInl . fst) l)+ right' = map (\ (Inr t, p) -> (t,p)) (filter (isInr . fst) l)+ var <- getVar "_v"+ left <- nomatch (Lam var (Match (Var var) left'))+ right <- nomatch (Lam var (Match (Var var) right'))+ return (Case e left right)+nomatch (Match e l)+ | isIn (fst (head l)) =+ do guard (all isIn (map fst l))+ let pats = map (\(In t,p) -> (t,p)) l+ nomatch (Match (Out e) pats)+nomatch (Match t alts) = + fail "Not possible to eliminate pattern matching!"+nomatch e = gmapM (mkM nomatch) e+++ +-- Auxiliary definitions++mygroup :: Eq a => (a -> a -> Bool) -> [a] -> [[a]]+mygroup f [] = []+mygroup f (h:t) = (h : filter (\x -> f x h) t):(mygroup f (filter (\x -> not (f x h)) t))
+ lib/Language/Pointwise/Parser.hs view
@@ -0,0 +1,139 @@+module Language.Pointwise.Parser where++import Language.Pointwise.Syntax as Pointwise+import Language.Haskell.Exts.Syntax as Exts+import Language.Haskell.Exts.Pretty+import Data.Char++{- +Parsing of a Exp to a pointwise term.+It recognizes:+ G, G1, G2 ::=+ (G) | undefined | _L | inn G | out G+ | 'literal' | 'var' | fix G | (G1,G2)+ | fst G | snd G | Left G | RightG | G1 G2 | \ 'var' -> G + | case G of Left var1 -> G1 ; Right var2 -> G2+ | case G of Right var1 -> G1 ; Left var2 -> G2+ | case G of ... +-}++mkVar = Exts.Var . UnQual . Ident++hs2pw :: Exp -> Maybe Term++hs2pw (Paren e) = hs2pw e++-- unit -> "undefined" or "_L"+hs2pw (Exts.Var(UnQual(Ident "undefined"))) = return $ Unit+hs2pw (Exts.Var(UnQual(Ident "_L"))) = return $ Unit++-- Constants+hs2pw (App (Exts.Var (UnQual (Ident "inn"))) exp)+ = hs2pw exp >>= return . In+hs2pw (App (Exts.Var (UnQual (Ident "out"))) exp)+ = hs2pw exp >>= return . Out+hs2pw (Lit lit) = return $ Const $ prettyPrint lit+hs2pw (Exts.Var(UnQual(Ident str))) = return $ Pointwise.Var str+hs2pw (InfixApp e1 (QConOp (Special Cons)) e2)+ = do t1 <- hs2pw e1+ t2 <- hs2pw e2+ return $ ((Const ":") :@: t1) :@: t2+hs2pw (List []) = return $ Const "[]"+hs2pw (List (x:xs))+ = do e <- hs2pw x+ es <- hs2pw (List xs)+ return $ ((Const ":") :@: e) :@: es++-- Recursion+hs2pw (App (Exts.Var (UnQual (Ident "fix"))) exp) =+ do term <- hs2pw exp+ return $ Fix term++-- remaining+hs2pw (Tuple [e1,e2]) =+ do t1 <- hs2pw e1+ t2 <- hs2pw e2+ return $ t1 :&: t2+hs2pw (App (Exts.Var (UnQual (Ident "fst"))) e) =+ do t <- hs2pw e+ return $ Fst t+hs2pw (App (Exts.Var (UnQual (Ident "snd"))) e) =+ do t <- hs2pw e+ return $ Snd t+hs2pw (App (Con (UnQual (Ident "Left"))) e) =+ do t <- hs2pw e+ return $ Inl t+hs2pw (App (Con (UnQual (Ident "Right"))) e) =+ do t <- hs2pw e+ return $ Inr t+hs2pw (App e1 e2) =+ do t1 <- hs2pw e1+ t2 <- hs2pw e2+ return $ t1 :@: t2+hs2pw (Lambda _ [PVar(Ident str)] e) =+ do t <- hs2pw e+ return $ Lam str t+-- in "case of"'s, guards fail and declarations are lost+hs2pw (Exts.Case e1+ [Alt _ (PApp (UnQual(Ident "Left"))+ [PVar(Ident str2)]) (UnGuardedAlt e2) _,+ Alt _ (PApp (UnQual(Ident "Right"))+ [PVar(Ident str3)]) (UnGuardedAlt e3) _]) =+ do t1 <- hs2pw e1+ t2 <- hs2pw e2+ t3 <- hs2pw e3+ return $ Pointwise.Case t1 (Lam str2 t2) (Lam str3 t3)+hs2pw (Exts.Case e1+ [Alt _ (PApp (UnQual(Ident "Right"))+ [PVar(Ident str3)]) (UnGuardedAlt e3) _,+ Alt _ (PApp (UnQual(Ident "Left"))+ [PVar(Ident str2)]) (UnGuardedAlt e2) _]) =+ do t1 <- hs2pw e1+ t2 <- hs2pw e2+ t3 <- hs2pw e3+ return $ Pointwise.Case t1 (Lam str2 t2) (Lam str3 t3)+hs2pw (Exts.Case e alts) =+ do t1 <- hs2pw e+ ts <- mapM alt2pws alts+ return $ Pointwise.Match t1 ts+ where alt2pws (Alt _ pat (UnGuardedAlt e) _) =+ do tp <- pat2pw pat+ te <- hs2pw e+ return (tp,te)+ alt2pws _ = fail "No guards allowed."+hs2pw (Con (UnQual (Ident x))) = return $ Const x+hs2pw t = fail $ "'"++prettyPrint t+++ "' is not a valid pointwise term."+++hsPat2Exp :: Pat -> Exp+hsPat2Exp (Exts.PVar hsName) = Exts.Var $ UnQual hsName+hsPat2Exp (PLit hsLiteral) = Lit hsLiteral+hsPat2Exp (PNeg hsPat) = NegApp . hsPat2Exp $ hsPat+hsPat2Exp (PInfixApp hsPat1 hsQName hsPat2) =+ let hsExp1 = hsPat2Exp hsPat1+ hsExp2 = hsPat2Exp hsPat2+ hsQOp = (if f hsQName then QConOp else QVarOp) hsQName+ in InfixApp hsExp1 hsQOp hsExp2+ where+ f (Qual _ name) = g name+ f (UnQual name) = g name+ f (Special _ ) = True+ g (Ident name) = isUpper $ head name+ g (Symbol str) = isUpper $ head str+hsPat2Exp (PApp hsQName []) = Con hsQName+hsPat2Exp (PApp hsQName lPat) =+ foldl App (Con hsQName) . map hsPat2Exp $ lPat+hsPat2Exp (PTuple lPat) = Tuple $ map hsPat2Exp lPat+hsPat2Exp (PList lPat) = List $ map hsPat2Exp lPat+hsPat2Exp (PParen hsPat) = Paren $ hsPat2Exp hsPat+hsPat2Exp (PRec hsQName lPatField) =+ RecConstr hsQName (map f lPatField)+ where+ f (PFieldPat hsQName hsPat) = FieldUpdate hsQName $ hsPat2Exp hsPat+--hsPat2Exp (PAsPat hsName hsPat) = AsPat hsName (hsPat2Exp hsPat)+hsPat2Exp (PWildCard) = mkVar "_L"+--hsPat2Exp (PIrrPat hsPat) = IrrPat $ hsPat2Exp hsPat++-- this approach may be changed...+pat2pw = hs2pw . hsPat2Exp
+ lib/Language/Pointwise/Pretty.hs view
@@ -0,0 +1,55 @@+module Language.Pointwise.Pretty where++import Language.Pointwise.Syntax as Pointwise+import Language.Haskell.Exts.Syntax as Exts++pw2hs :: Term -> Exp+pw2hs (Pointwise.Var str) = mkVar str+pw2hs Unit = mkVar "_L"+pw2hs (Const str) = mkVar str+pw2hs (t1 :&: t2) = Tuple [pw2hs t1,pw2hs t2]+pw2hs (Fst t) = App (mkVar "fst") (mbParen$ pw2hs t)+pw2hs (Snd t) = App (mkVar "snd") (mbParen$ pw2hs t)+pw2hs (Pointwise.Case t1 (Lam str2 t2) (Lam str3 t3)) =+ Exts.Case (pw2hs t1)+ [Alt mkLoc (PApp (UnQual$ Ident "Left") [mkPVar str2])+ (UnGuardedAlt$ mbParen$ pw2hs t2) (BDecls []),+ Alt mkLoc (PApp (UnQual$ Ident "Right") [mkPVar str3])+ (UnGuardedAlt$ mbParen$ pw2hs t3) (BDecls [])]+pw2hs (Inl t) = App (mkCon "Left") (mbParen$ pw2hs t)+pw2hs (Inr t) = App (mkCon "Right") (mbParen$ pw2hs t)+pw2hs (Lam str t) = Lambda mkLoc [mkPVar str] (mbParen (pw2hs t))+pw2hs (t1 :@: t2) = App (mbParen$ pw2hs t1) (mbParen$ pw2hs t2)+pw2hs (In term) = App (mkVar "inn") (mbParen$ pw2hs term)+pw2hs (Out term) = App (mkVar "out") (mbParen$ pw2hs term)+pw2hs (Fix term) = App (mkVar "fix") (mbParen$ pw2hs term)+pw2hs (Pointwise.Match t alts)= Exts.Case (pw2hs t) (map pw2alt alts)+ where+ pw2alt (t1,t2) = Alt mkLoc (pw2pat t1) (UnGuardedAlt $ pw2hs t2) $ BDecls []+ pw2pat (Pointwise.Var s) = mkPVar s+ pw2pat Unit = PWildCard+ pw2pat (Const s) = mkPVar s+ pw2pat (t1 :&: t2) = PTuple [pw2pat t1,pw2pat t2]+ pw2pat (Inl t) = PApp (UnQual $ Ident "Left") [mbPParen$ pw2pat t]+ pw2pat (Inr t) = PApp (UnQual $ Ident "Right") [mbPParen$ pw2pat t]+ pw2pat ((Pointwise.Var str) :@: t2) =+ PApp (UnQual $ Ident str) [mbPParen$ pw2pat t2]+ pw2pat t = error $ "not a valid pattern - " ++ show t+++mkLoc = SrcLoc "" 0 0+mkCon = Con . UnQual . Ident+mkVar = Exts.Var . UnQual . Ident+mkPVar = PVar . Ident+-- places parentisis only if it is necessary+mbParen :: Exp -> Exp+mbParen e@(App _ _) = Paren e+mbParen e@(InfixApp _ _ _) = Paren e+mbParen e@(Exts.Case _ _) = Paren e+mbParen e@(Lambda _ _ _) = Paren e+mbParen e@(ExpTypeSig _ _ _) = Paren e+mbParen x = x+mbPParen :: Pat -> Pat+mbPParen p@(PApp _ _) = PParen p+mbPParen p = p+
+ lib/Language/Pointwise/Syntax.hs view
@@ -0,0 +1,105 @@+module Language.Pointwise.Syntax where++import Data.Generics hiding (Unit,(:*:),Inl,Inr)+import Data.List+import Data.Maybe+import Generics.Pointless.Combinators++data Term = Var String+ | Unit+ | Const String -- Is this really necessary? + | Term :&: Term+ | Fst Term+ | Snd Term+ | Case Term Term Term+ | Match Term [(Term,Term)]+ | Inl Term+ | Inr Term+ | Lam String Term+ | Term :@: Term+ | In Term+ | Out Term+ | Fix Term+ deriving (Eq,Show,Data,Typeable)++isPair :: Term -> Bool+isPair (_ :&: _) = True+isPair _ = False++pwFst :: Term -> Term+pwFst (l :&: r) = l++pwSnd :: Term -> Term+pwSnd (l :&: r) = r++isInl :: Term -> Bool+isInl (Inl _) = True+isInl _ = False++isInr :: Term -> Bool+isInr (Inr _) = True+isInr _ = False++isInlr :: Term -> Bool+isInlr t = isInl t || isInr t++isIn :: Term -> Bool+isIn (In _) = True+isIn _ = False+++-- Free variables+-- only works correctly when there are no Match constructors in Term++free :: Term -> [String]+free (Var v) = [v]+free (Lam v x) = delete v (free x)+free e = nub (concat (gmapQ (mkQ [] free) e))++-- Substitution+-- only works correctly when there are no Match constructors in Term++subst :: [(String, Term)] -> Term -> Term+subst s (Var y) = + case lookup y s+ of Nothing -> Var y+ Just t -> t+subst s (Lam y e) = + let x = concat (concat (map free (e : map snd s)))+ in Lam x (subst ((y, Var x) : s) e)+subst s t = + gmapT (mkT (subst s)) t++-- single traversal (bottom-up) beta reduction++step :: Term -> Term+step = everywhere (mkT aux)+ where aux ((Lam v t) :@: m) = subst [(v,m)] t+ aux t = t++-- Replacing constant by definition++replace :: [(String, Term)] -> Term -> Term+replace defs = everywhere (mkT aux)+ where aux (Const x) = fromMaybe (Const x) (lookup x defs)+ aux t = t++-- Examples++distr :: Term+distr = Lam "x" (Match (Var "x") [(Var "y" :&: (Inl (Var "z")),Inl (Var "y" :&: Var "z")),(Var "y" :&: (Inr (Var "z")),Inr (Var "y" :&: Var "z"))])++swap :: Term+swap = Lam "x" (Match (Var "x") [(Var "w" :&: Var "y", Var "y" :&: Var "w")])++coswap :: Term+coswap = Lam "x" (Match (Var "x") [(Inl (Var "y"), Inr (Var "y")),(Inr (Var "y"), Inl (Var "y"))])++assocr :: Term+assocr = Lam "w" (Match (Var "w") [((Var "x" :&: Var "y") :&: Var "z", Var "x" :&: (Var "y" :&: Var "z"))])++coassocr :: Term+coassocr = Lam "w" (Match (Var "w") [(Inl (Inl (Var "x")), Inl (Var "x")),(Inl (Inr (Var "x")), Inr (Inl (Var "x"))),(Inr (Var "x"), Inr (Inr (Var "x")))])++test :: Term+test = Lam "x" (Match (Var "x") [(Var "y", Var "y")])
+ src/DrHylo.hs view
@@ -0,0 +1,176 @@+module Main where++import System.IO+import System.Console.GetOpt+import System.Environment+import Language.Haskell.Exts.Syntax as Exts+import Language.Haskell.Exts.Parser+import Language.Haskell.Exts.Pretty+import Data.Maybe+import Data.List+import PwPf+import Matching+import FunctorOf+import Hylos+import Language.Pointfree.Pretty+import Language.Pointfree.Syntax as Pf+import Language.Pointwise.Syntax as Pw+import Language.Pointwise.Pretty+import Language.Pointwise.Parser+import Language.Pointwise.Matching+import Generics.Pointless.Combinators+import Control.Monad.State+import Data.Generics.Schemes+import Data.Generics.Aliases++-- Managing Options++data Flag = Input String | Output String | Fixify | Pointwise | Observable+ deriving Eq++options :: [OptDescr Flag]+options = [Option ['o'] ["output"] (OptArg outp "FILE") "output FILE",+ Option ['i'] ["input"] (OptArg inp "FILE") "input FILE",+ Option ['f'] ["fix"] (NoArg Fixify) "use fixpoints instead of hylomorphisms",+ Option ['w'] ["pointwise"] (NoArg Pointwise) "do not convert to point-free",+ Option ['O'] ["observable"] (NoArg Observable) "generate observable hylomorphisms"+ ]++inp,outp :: Maybe String -> Flag+outp = Output . fromMaybe "stdout"+inp = Input . fromMaybe "stdin"++parseOpts :: [String] -> IO [Flag]+parseOpts opts = case (getOpt Permute options opts) + of (l,[],[]) -> return l+ (_,_,errs) -> fail (concat errs ++"\n"++ usageInfo header options)+ where header = "DrHylo derives point-free hylomorphisms from restricted Haskell syntax\n\nUsage: DrHylo [OPTION...]"++getInput :: [Flag] -> IO Handle+getInput [] = return stdin+getInput ((Input i):_) | i=="stdin" = return stdin+ | otherwise = openFile i ReadMode+getInput (_:l) = getInput l++getOutput :: [Flag] -> IO Handle+getOutput [] = return stdout+getOutput ((Output i):_) | i=="stdout" = return stdout+ | otherwise = openFile i WriteMode+getOutput (_:l) = getOutput l++fixrequired :: [Flag] -> Bool+fixrequired = elem Fixify++pwrequired :: [Flag] -> Bool+pwrequired = elem Pointwise++obrequired :: [Flag] -> Bool+obrequired = elem Observable++-- Parsing++parse :: String -> IO Module+parse s = case (parseModule s) + of ParseOk m -> return m+ ParseFailed l d -> fail ((show l)++": "++d)++-- Generation of Observable function contexts++isTypeSig :: String -> Decl -> Bool+isTypeSig name (TypeSig _ x _) = elem (Ident name) x+isTypeSig _ _ = False++getTypeVars :: Exts.Type -> [Name]+getTypeVars = everything (++) ([] `mkQ` getVar)+ where getVar :: Exts.Type -> [Name]+ getVar (TyVar v) = [v]+ getVar _ = []++observableTypeSig :: Decl -> Decl+observableTypeSig (TypeSig loc names t) = TypeSig loc names (aux t)+ where+ aux (TyForall mb ctx (TyFun a b)) = TyForall mb (ctx++obs a b) (TyFun a b)+ aux (TyFun a b) = TyForall Nothing (obs a b) (TyFun a b)+ vars a b = nub $ intersect (getTypeVars a) (getTypeVars b)+ obs a b = map mkObservableIns (vars a b)++mkObservableIns :: Name -> Asst+mkObservableIns n = ClassA (UnQual (Ident "Observable")) [TyVar n]++addObservableIns :: String -> [Decl] -> [Decl]+addObservableIns n [] = []+addObservableIns n (d:ds) = if (isTypeSig n d) then observableTypeSig d : ds else d : addObservableIns n ds++-- From Pointwise to Point-free (or not)++pwpfModule :: [Flag] -> [(String,Pw.Term)] -> Module -> Module+pwpfModule f c (Module loc name warnings exports imports decls) = Module loc name warnings exports imports decls''+ where+ (decls',obs) = (id >< catMaybes) $ unzip $ map aux decls+ decls'' = foldr addObservableIns decls' obs+ aux d = case pwpfDecl f c d + of Just (d',mb) -> (d',mb)+ Nothing -> (d,Nothing)++consts :: [(String,Pw.Term)]+consts = [("[]", In (Inl Unit)),(":", Lam "h" (Lam "t" (In (Inr (Pw.Var "h" :&: Pw.Var "t")))))]++pwpfDecl :: [Flag] -> [(String,Pw.Term)] -> Decl -> Maybe (Decl,Maybe String)+pwpfDecl f d (PatBind loc (PVar (Ident name)) (UnGuardedRhs rhs) (BDecls [])) =+ do pw <- hs2pw rhs+ pw0 <- return (step (replace (d++consts) pw))+ pw1 <- evalStateT (nomatch pw0) 0+ pw2 <- return (if (name `elem` free pw1) + then Pw.Fix (Lam name pw1)+ else pw1)+ pw3 <- return (subst (map (\v -> (v, Pw.Const v)) (free pw2)) pw2)+ (rhs',ob) <- return (if (pwrequired f)+ then (pw2hs pw3,Nothing)+ else if (not (fixrequired f)) && (derivable pw3)+ then let (Pw.Fix (Lam nam (Lam x z))) = pw3 + t = fun z nam+ a = Lam "__" (alg z nam (Pw.Var "__"))+ c = Lam x (coa z nam)+ hyl = if (obrequired f) then HyloO else Hylo+ in (pf2hs (hyl (Pf.Fix t) (unpoint (pwpf [] a)) (unpoint (pwpf [] c))),Just name)+ else (pf2hs (unpoint (pwpf [] pw3)),Nothing))+ return (PatBind loc (PVar (Ident name)) (UnGuardedRhs rhs') (BDecls []),ob)+pwpfDecl _ _ _ = fail "The transformation must be applied to simple declarations"+++-- Handle imports++loc0 :: SrcLoc+loc0 = SrcLoc "" 0 0++mkImportDecl :: String -> ImportDecl+mkImportDecl n = ImportDecl loc0 (ModuleName n) False False Nothing Nothing++getImportName :: ImportDecl -> String+getImportName (ImportDecl _ (ModuleName n) _ _ _ _) = n++handleImports :: Bool -> Module -> Module+handleImports b (Module loc name warnings exports imports decls) =+ let aux True = ["Generics.Pointless.Combinators", "Generics.Pointless.Functors", "Generics.Pointless.RecursionPatterns", "Debug.Observe","Generics.Pointless.Observe.Functors", "Generics.Pointless.Observe.RecursionPatterns"]+ aux False = ["Generics.Pointless.Combinators", "Generics.Pointless.Functors", "Generics.Pointless.RecursionPatterns"]+ aux' = aux b \\ (map getImportName imports) + imports' = imports++(map mkImportDecl aux')+ in Module loc name warnings exports imports' decls+++-- Main++main :: IO ()+main = do opts <- getArgs+ flags <- parseOpts opts+ let ob = obrequired flags+ ihandle <- getInput flags+ ohandle <- getOutput flags+ source <- hGetContents ihandle+ hsModule <- parse source+ hsModule0 <- return (casificate hsModule)+ hsModule1 <- return (functorOfInst ob hsModule0)+ hsModule2 <- return (pwpfModule flags (getCtx hsModule0) hsModule1)+ hPutStrLn ohandle (prettyPrint (handleImports ob hsModule2))+ hClose ihandle+ hClose ohandle
+ src/FunctorOf.hs view
@@ -0,0 +1,215 @@+module FunctorOf (+ getCtx+ , functorOfInst+ , getSeed+ , hsPat2Exp+ ) where++import Data.Map hiding (map) +import Data.List+import Data.Maybe+import Language.Haskell.Exts.Syntax as Exts++import Control.Monad.State+import Data.Char (isUpper)+import Data.Generics hiding (Unit,(:*:),Inl,Inr)++import Language.Haskell.Exts.Parser+import Language.Haskell.Exts.Pretty++import Language.Pointwise.Parser (hsPat2Exp)+import Language.Pointwise.Syntax as Pointwise hiding (swap)++-- Associates a constructor to definition++type Ctx = [(String,Term)]++getCtx :: Module -> Ctx+getCtx (Module _ _ _ _ _ decls)+ = concat $ catMaybes $ map getCtxDecl decls++getCtxDecl :: Decl -> Maybe Ctx+getCtxDecl (DataDecl _ _ _ _ _ cons _) = getCtxCons cons In+getCtxDecl _ = fail "Only applies to data declarations"++getCtxCons :: [QualConDecl] -> (Term -> Term) -> Maybe Ctx+getCtxCons [QualConDecl _ _ _ (ConDecl (Ident name) l)] f = + return [(name, buildArgs f (length l))]+getCtxCons ((QualConDecl _ _ _ (ConDecl (Ident name) l)):t) f =+ do t' <- getCtxCons t (f . Inr)+ return ((name, buildArgs (f . Inl) (length l)):t')+getCtxCons _ _ = fail "Case not covered"++buildArgs :: (Term -> Term) -> Int -> Term+buildArgs f 0 = f Unit+buildArgs f 1 = Lam "x1" (f (Pointwise.Var "x1"))+buildArgs f n = let v = "x"++(show n)+ in Lam v (buildArgs (f . (\t -> (Pointwise.Var v :&: t))) (n-1))++{- Calculation of the instances of FunctorOf, when possible. -}++type St = StateT (String,Int) Maybe++conDecl :: QualConDecl -> ConDecl+conDecl (QualConDecl _ _ _ con) = con++functorOfInst :: Bool -> Module -> Module+functorOfInst ob (Module a b c d i decls)+ = let seed = "v" --getSeed decls+ newDecls = concat $ catMaybes $+ map (\x -> evalStateT (getInstances ob x) (seed,0)) decls+ in Module a b c d i (decls ++ newDecls)++g :: Type -> QualConDecl -> St Type+g arg = gCon arg . conDecl++gCon :: Type -> ConDecl -> St Type+gCon arg (ConDecl _ []) = return constNil+gCon arg (ConDecl _ lBangType) = mapM (h arg) lBangType >>= return . foldr1 timesType+gCon arg (RecDecl hsName l ) = gCon arg (ConDecl hsName (concatMap unRec l))+-- fail "data types records not yet supported"++h :: Type -> BangType -> St Type+h arg (BangedTy hsType ) = ii arg hsType+h arg (UnBangedTy hsType ) = ii arg hsType+-- what's the diference between Banged and UnBanged?++i :: Type -> Type -> St Type+i arg (TyFun hsType1 hsType2) = fail "TyFun not yet supported"+i arg (TyTuple _ lType) = mapM (ii arg) lType >>= return . foldr1 timesType+i arg (TyApp hsType1 hsType2) = i arg hsType2 >>= return . appType hsType1+-- fail "TyApp not yet supported" --g :@: h+i arg t@(TyVar hsName) = return $ TyApp (TyCon $ UnQual $ Ident "Const") t+i arg t@(TyCon hsQName) = return $ TyApp (TyCon $ UnQual $ Ident "Const") t++ii :: Type -> Type -> St Type+ii arg typ | typ == arg = return $ TyCon $ UnQual $ Ident "Id"+ | otherwise = i arg typ++genInOut :: Type -> [QualConDecl] -> St [(Pat, Pat)]+genInOut arg [] = fail "empty list of constructors"+genInOut arg l = mapM (g' arg) l >>= return . genPat++genPat :: [(Pat, Pat)] -> [(Pat, Pat)]+genPat [] = error "empty list found when generating instance of 'Mu' "+genPat l = genPatAux id l++genPatAux ac [(a,b)] = [(ac a, b)]+genPatAux ac ((a,b):t) = (ac . inl $ a, b) : genPatAux (ac . inr) t++g' :: Type -> QualConDecl -> St (Pat,Pat)+g' arg = g'Con arg . conDecl++g'Con :: Type -> ConDecl -> St (Pat, Pat)+g'Con arg (ConDecl hsName []) = return (constPNil,PApp (UnQual hsName) [])+g'Con arg (ConDecl hsName lBangType) = do+ (l2,l3) <- mapAndUnzipM (h' arg) lBangType+ return (foldr1 times l2,PApp (UnQual hsName) l3)+g'Con arg (RecDecl hsName l) = g'Con arg (ConDecl hsName (concatMap unRec l))+--fail "data types records not yet supported"++h' :: Type -> BangType -> St (Pat, Pat)+h' arg (BangedTy hsType) = ii' arg hsType+h' arg (UnBangedTy hsType) = ii' arg hsType+-- what's the diference between Banged and UnBanged?++i' :: Type -> Type -> St (Pat, Pat)+i' arg (TyFun hsType1 hsType2) = fail "TyFun not yet supported"+i' arg (TyTuple _ lType) = do+ (l1,l2) <- mapAndUnzipM (ii' arg) lType+ return (foldr1 times l1,PTuple l2)+i' arg (TyApp hsType1 hsType2) = do+ a <- getFreshVar+ let av = PVar a+ return (av,av)+i' arg t@(TyVar hsName) = do+ a <- getFreshVar+ let av = PVar a+ return (av,av)+i' arg t@(TyCon hsQName) = do+ a <- getFreshVar+ let av = case hsQName of+ Special _ -> PApp hsQName []+ _ -> PVar a+ return (av,av)++ii' :: Type -> Type -> St (Pat, Pat)+ii' arg typ | typ == arg = do+ a <- getFreshVar+ let av = PVar a+ return (av,av)+ | otherwise = i' arg typ++mkDataName :: Decl -> Type+mkDataName (DataDecl _ _ _ hsName lName _ _) = foldl TyApp (TyCon $ UnQual hsName) . map TyVar $ lName++getDataDeclFunctor :: Type -> [QualConDecl] -> St Type+getDataDeclFunctor arg lConDecl = do+ l1 <- mapM (g arg) lConDecl+ let functor = foldr1 plusType l1+ return functor++getInstances :: Bool -- ^ Observable or not+ -> Decl -- ^ Data types+ -> St [Decl] -- ^ Instances for functor representation+getInstances ob d@(DataDecl loc _ [] hsName lName lConDecl _) = do+ let arg = mkDataName d+ functor <- getDataDeclFunctor arg lConDecl+ l <- genInOut arg lConDecl+ let innOut = [InsDecl (FunBind (map inMatch l)), InsDecl (FunBind (map outMatch l))]+ let pfTInst = TypeInsDecl loc (TyApp pfType arg) functor+ let muInst = InstDecl loc [] mu [arg] innOut+ let observableInst = getObservableInst loc arg+ if ob then return [pfTInst,muInst,observableInst]+ else return [pfTInst,muInst]+ where+ match str (a,b) = Exts.Match mkLoc (Ident str) [a]+ (UnGuardedRhs $ hsPat2Exp b) (BDecls [])+ mkLoc = SrcLoc "" 0 0+ inMatch = match "inn"+ outMatch = match "out" . swap++getInstances _ (DataDecl _ _ _ _ _ _ _ ) =+ fail "type context not treated"+getInstances _ _ = fail "not a data declaration"++-- types+opType op a b = TyApp (TyApp (TyVar $ Symbol op) a ) b+plusType = opType ":+:"+timesType = opType ":*:"+appType = opType ":@:"+constNil = TyApp (TyCon $ UnQual $ Ident "Const") (TyCon $ UnQual $ Ident "One")+mu = UnQual $ Ident "Mu"+pfType = TyCon $ UnQual $ Ident "PF"++-- patterns+constPNil = PWildCard+inl = PApp (UnQual $ Ident "Left") . singl . PParen+inr = PApp (UnQual $ Ident "Right") . singl . PParen+singl = (:[])+times a b = PTuple [a,b]++unRec (a,b) = replicate (length a) b++getFreshVar = do+ (seed,n) <- gets id+ modify (\_->(seed,n+1))+ return $ Ident $ seed ++ show (n+1)++getObservableInst :: SrcLoc -> Type -> Decl+getObservableInst loc a = InstDecl loc [ClassA (UnQual (Ident "FunctorO")) [TyApp (TyCon (UnQual (Ident "PF"))) a]] (UnQual (Ident "Observable")) [a] [InsDecl (FunBind [Exts.Match loc (Ident "observer") [PVar (Ident "x")] (UnGuardedRhs (App (App (Exts.Var (UnQual (Ident "send"))) (Lit (String ""))) (Paren (InfixApp (InfixApp (App (App (App (Exts.Var (UnQual (Ident "omap"))) (Paren (ExpTypeSig loc (Exts.Var (UnQual (Ident "_L"))) a))) (Exts.Var (UnQual (Ident "thk")))) (Paren (App (Exts.Var (UnQual (Ident "out"))) (Exts.Var (UnQual (Ident "x")))))) (QVarOp (UnQual (Symbol ">>="))) (Exts.Var (UnQual (Ident "return")))) (QVarOp (UnQual (Symbol "."))) (Exts.Var (UnQual (Ident "inn"))))))) (BDecls [PatBind loc (PVar (Ident "thk")) (UnGuardedRhs (ExpTypeSig loc (Exts.Var (UnQual (Ident "thunk"))) (TyFun a (TyApp (TyCon (UnQual (Ident "ObserverM"))) a)))) (BDecls [])])])]++++---- auxiliary functions+swap (a,b) = (b,a)++showName (Ident s) = s+showQName (UnQual (Ident s)) = s+showQName (Qual (ModuleName s1) (Ident s2)) = s1++('.':s2)++getSeed :: Data a => a -> String+getSeed = flip replicate 'x' .+ maximum . (1:) .+ everything (++) (mkQ [] aux)+ where aux = (:[]) . (+1) . length . takeWhile (=='x')
+ src/Hylos.hs view
@@ -0,0 +1,127 @@+module Hylos where++import Language.Pointwise.Syntax as Pointwise+import Language.Pointfree.Syntax as Pointfree hiding (Term)+import Data.List+import Control.Monad.State+++-- Hylomorphism derivation a la Hu, Iwasaki, and Takeichi++derivable :: Term -> Bool+derivable (Pointwise.Fix (Lam f (Lam x l))) = branch l+ where branch (Case m (Lam _ n) (Lam _ o)) = + (f `notElem` free m) && (branch n) && (branch o)+ branch n = leaf n+ leaf Unit = True+ leaf (Pointwise.Const _) = True+ leaf (Var y) = (y /= f)+ leaf (Var g :@: n) | (g == f) = leaf n && (f `notElem` free n)+ | otherwise = leaf n+ leaf (n :@: m) = leaf n && leaf m+ leaf (n :&: m) = leaf n && leaf m+ leaf (Fst n) = leaf n+ leaf (Snd n) = leaf n+ leaf (Inl n) = leaf n+ leaf (Inr n) = leaf n+ leaf (In n) = leaf n+ leaf (Out n) = leaf n+ leaf _ = False+derivable _ = False++getVar :: String -> State Int String+getVar x = do seed <- get+ modify (+1)+ return (x ++ (show seed))++fun :: Term -> String -> Funct+fun l r = evalState (aux l) 0+ where aux (Case _ (Lam x m) (Lam y n)) =+ do f <- aux m+ g <- aux n+ return (f :++: g)+ aux Unit = return (Pointfree.Const One)+ aux (Pointwise.Const _) = return (Pointfree.Const One)+ aux (Var x) = getVar "a" >>= return . Pointfree.Const . Base+ aux (Var x :@: n) | x == r = return Id+ aux (m :@: n) | null (free n) = aux m+ | null (free m) = aux n+ | otherwise = do f <- aux m+ g <- aux n+ return (f :**: g)+ aux (m :&: n) | null (free n) = aux m+ | null (free m) = aux n+ | otherwise = do f <- aux m+ g <- aux n+ return (f :**: g)+ aux (Fst n) = aux n+ aux (Snd n) = aux n+ aux (Inl n) = aux n+ aux (Inr n) = aux n+ aux (In n) = aux n+ aux (Out n) = aux n++coa :: Term -> String -> Term+coa t r = aux t+ where aux (Case l (Lam x m) (Lam y n)) =+ let f = aux m+ g = aux n+ in (Case l (Lam x (Inl f)) (Lam y (Inr g)))+ aux Unit = Unit+ aux (Pointwise.Const _) = Unit+ aux (Var x) = Var x+ aux (Var x :@: n) | x == r = n+ aux (m :@: n) | null (free n) = aux m+ | null (free m) = aux n+ | otherwise = let f = aux m+ g = aux n+ in (f :&: g)+ aux (m :&: n) | null (free n) = aux m+ | null (free m) = aux n+ | otherwise = let f = aux m+ g = aux n+ in (f :&: g)+ aux (Fst n) = aux n+ aux (Snd n) = aux n+ aux (Inl n) = aux n+ aux (Inr n) = aux n+ aux (In n) = aux n+ aux (Out n) = aux n++alg :: Term -> String -> Term -> Term+alg t r p = aux t p+ where aux (Case l (Lam x m) (Lam y n)) (Var p) =+ let vl = p++"l"+ vr = p++"r"+ f = aux m (Var vl)+ g = aux n (Var vr)+ in (Case (Var p) (Lam vl f) (Lam vr g))+ aux Unit _ = Unit+ aux (Pointwise.Const f) _ = Pointwise.Const f+ aux (Var x) p = p+ aux (Var x :@: n) p | x == r = p+ aux (m :@: n) p | null (free n) = let f = aux m p+ g = aux n p+ in (f :@: g)+ | null (free m) = let f = aux m p+ g = aux n p+ in (f :@: g)+ | otherwise = let f = aux m (Fst p)+ g = aux n (Snd p)+ in (f :@: g)+ aux (m :&: n) p | null (free n) = let f = aux m p+ g = aux n p+ in (f :&: g)+ | null (free m) = let f = aux m p+ g = aux n p+ in (f :&: g)+ | otherwise = let f = aux m (Fst p)+ g = aux n (Snd p)+ in (f :&: g)+ aux (Fst n) p = Fst (aux n p)+ aux (Snd n) p = Snd (aux n p)+ aux (Inl n) p = Inl (aux n p)+ aux (Inr n) p = Inr (aux n p)+ aux (In n) p = In (aux n p)+ aux (Out n) p = Out (aux n p)+
+ src/Matching.hs view
@@ -0,0 +1,63 @@+module Matching (casificate) where++import Language.Haskell.Exts.Syntax+import Control.Monad.State+++{- Convert arguments in functions to "case of"'s, as in the example:+ f 0 y = e1 \ ---> / f v = case v of (1,y) -> e1+ f x y = e2 / \ (x,y) -> e2+-}+casificate :: Module -> Module+casificate (Module a b c d i decls) =+ let seed = "v"+ newDecls = evalState (mapM cas_decl decls) seed+ in Module a b c d i newDecls+++type ST a = State String a++cas_decl :: Decl -> ST Decl+cas_decl (FunBind ms)+ = do newMs <- cas_matches ms+ return $ PatBind mkLoc (PVar $ getName $ head ms)+ (UnGuardedRhs newMs) (BDecls [])+ where getName (Match _ name _ _ _) = name+cas_decl x = return x ++cas_matches :: [Match] -> ST Exp+cas_matches ms@((Match _ _ pats _ _):_)+ = do alts <- mapM cas_alt ms+ seed <- gets id+ let npats = length pats+ return $ buildPVars npats seed $+ Case (buildVars npats seed) alts+ where buildPVars 1 v = Lambda mkLoc [mkPVar $ v ++ "1"]+ buildPVars n v = Lambda mkLoc [mkPVar $ v ++ show n] . (buildPVars (n-1) v)+ buildVars 1 v = mkVar $ v++"1"+ buildVars n v = Tuple $ [mkVar $ v++show n,buildVars (n-1) v]++cas_alt :: Match -> ST Alt+cas_alt (Match l _ pats expRhs (BDecls ds))+ = do ds' <- mapM cas_decl ds+ return $ Alt l (pat pats) altRhs (BDecls ds')+ where pat [x] = x+ pat (x:xs) = PTuple [x,pat xs]+ altRhs = case expRhs of + UnGuardedRhs exp -> UnGuardedAlt exp+ GuardedRhss x -> GuardedAlts (map aux x)+ aux (GuardedRhs l x y) = (GuardedAlt l x y)+++-- auxiliary functions+mkVar = Var . UnQual . Ident+mkPVar = PVar . Ident+mkLoc = SrcLoc "" 0 0++{-+getSeed :: Data a => a -> String+getSeed = flip replicate 'x' .+ maximum . (1:) .+ everything (++) (mkQ [] aux)+ where aux = (:[]) . (+1) . length . takeWhile (=='x')+-}
+ src/PwPf.hs view
@@ -0,0 +1,31 @@+module PwPf where++import Language.Pointwise.Syntax as Pointwise+import Language.Pointfree.Syntax as Pointfree hiding (Const)++type Ctx = [String]++path :: Ctx -> String -> Pointfree.Term+path [] x = Point x+path (x:xs) y | x==y = SND+ | otherwise = path xs y :.: FST++pwpf :: Ctx -> Pointwise.Term -> Pointfree.Term +pwpf e (Var x) = path e x+pwpf e (Lam x t) = Curry (pwpf (x:e) t)+pwpf e (l :@: r) = AP :.: (pwpf e l :/\: pwpf e r)+pwpf e Unit = BANG+pwpf e (Const s) = Point s :.: BANG+pwpf e (l :&: r) = pwpf e l :/\: pwpf e r+pwpf e (Fst t) = FST :.: pwpf e t+pwpf e (Snd t) = SND :.: pwpf e t+pwpf e (Case t l r) = + AP :.: ((Macro "eithr" [] :.: (pwpf e l :/\: pwpf e r)) :/\: pwpf e t)+pwpf e (Inl t) = INL :.: pwpf e t+pwpf e (Inr t) = INR :.: pwpf e t+pwpf e (In t) = IN :.: pwpf e t+pwpf e (Out t) = OUT :.: pwpf e t+pwpf e (Pointwise.Fix t) = Macro "fix" [] :.: pwpf e t++unpoint :: Pointfree.Term -> Pointfree.Term+unpoint f = AP :.: ((f :.: BANG) :/\: ID)