Sat Dec 6 20:26:19 WET 2008 hpacheco@di.uminho.pt
* Initial import
{
addfile ./DrHylo.cabal
addfile ./LICENSE
addfile ./README
addfile ./Sample.hs
addfile ./Setup.lhs
adddir ./lib
adddir ./lib/Language
adddir ./lib/Language/Pointfree
addfile ./lib/Language/Pointfree/Parser.hs
addfile ./lib/Language/Pointfree/Pretty.hs
addfile ./lib/Language/Pointfree/Syntax.hs
adddir ./lib/Language/Pointwise
addfile ./lib/Language/Pointwise/Matching.hs
addfile ./lib/Language/Pointwise/Parser.hs
addfile ./lib/Language/Pointwise/Pretty.hs
addfile ./lib/Language/Pointwise/Syntax.hs
adddir ./src
addfile ./src/DrHylo.hs
addfile ./src/FunctorOf.hs
addfile ./src/Hylos.hs
addfile ./src/Matching.hs
addfile ./src/PwPf.hs
hunk ./DrHylo.cabal 1
+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
hunk ./LICENSE 1
+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.
hunk ./README 1
+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
+
+
+
hunk ./Sample.hs 1
+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))
+
+
hunk ./Setup.lhs 1
+#!/usr/bin/env runhaskell
+> import Distribution.Simple
+> main = defaultMain
hunk ./lib/Language/Pointfree/Parser.hs 1
+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"
hunk ./lib/Language/Pointfree/Pretty.hs 1
+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
hunk ./lib/Language/Pointfree/Syntax.hs 1
+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
+
hunk ./lib/Language/Pointwise/Matching.hs 1
+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))
hunk ./lib/Language/Pointwise/Parser.hs 1
+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
hunk ./lib/Language/Pointwise/Pretty.hs 1
+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
+
hunk ./lib/Language/Pointwise/Syntax.hs 1
+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")])
hunk ./src/DrHylo.hs 1
+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
hunk ./src/FunctorOf.hs 1
+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')
hunk ./src/Hylos.hs 1
+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)
+
hunk ./src/Matching.hs 1
+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')
+-}
hunk ./src/PwPf.hs 1
+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)
}