HaRe-0.6: refactorer/PwPf/PwPfConversion.hs
-----------------------------------------------------------------------------
-- |
-- Module : PwPfConversion
-- Copyright : (c) Jose Proenca 2005
-- License : GPL
--
-- Maintainer : jproenca@di.uminho.pt
-- Stability : experimental
-- Portability : portable
--
-- Translations between pointwise and point-free expressions, expressed in
-- the modules "PWCore" and "PointFree".
--
-----------------------------------------------------------------------------
module PwPfConversion (
-- * Translation from "Pointfree" to "PWCore"
pf2core,
-- * Translation from "PWCore" to "Pointfree"
core2Pf
) where
import PWCore
import Pointfree
{- | Applies a simple transformation from a 'PFTerm' to a 'PWTerm', in an automated manner.
-}
pf2core :: PFTerm -> PWTerm
pf2core BANG = Abstr "x" Unit
pf2core ID = Abstr "x" (Var' "x")
pf2core APP = Abstr "x" ((Fst $ Var'"x") :@:
(Snd $ Var' "x"))
pf2core (Curry t1) = Abstr "x" (Abstr "y"
((pf2core t1):@:((Var' "y"):><:(Var' "x"))) )
pf2core (t1 :.: t2) = Abstr "x" ((pf2core t1):@:((pf2core t2):@:(Var' "x")))
pf2core (t1 :\/: t2) = Abstr "x" (Case (Var' "x")
("y" , (pf2core t1):@:(Var' "y"))
("z" , (pf2core t2):@:(Var' "z")))
pf2core (t1 :/\: t2) = Abstr "x" ((pf2core t1):><:(pf2core t2))
pf2core FST = Abstr "x" (Fst $ Var' "x")
pf2core SND = Abstr "x" (Snd $ Var' "x")
pf2core INL = Abstr "x" (Inl $ Var' "x")
pf2core INR = Abstr "x" (Inr $ Var' "x")
pf2core (IN str) = Abstr "x" (In str $ Var' "x")
pf2core (OUT str) = Abstr "x" (Out str $ Var' "x")
pf2core FIX = Abstr "x" (Fix $ Var' "x")
pf2core (Macro x) = Var' x
-- | A context will be a left-nested pair, where the most to the
-- right value will be a never used constant
type Context = PWTerm
-- | Calculates a "path" to a variable in a context by composing the
-- "fst" and "snd" functions
path :: Context -> PWTerm -> PFTerm
path (t:><:(Var' y)) (Var' x)
| x == y = SND
| otherwise = (path t (Var' x)) :.: FST
path _ (Var' x) = Macro x
-- | Given a Context, it calculates the translation from Core
-- to Point-free
core2pf :: Context -> PWTerm -> PFTerm
{- | Applies the conversion of a pointwise expression of type @A@ and obtains
a pointfree expression of type @1->A@, to which is applied a poinfree macro
to get the correct type again.
-}
-- (unpnt f = app . (f . bang /\ id))
core2Pf :: PWTerm -> PFTerm
core2Pf t = APP :.: (((core2pf Unit t) :.: BANG) :/\: ID)
-- paramorphisms for Int
core2pf cont ((((Fix (Abstr r1 (Abstr n1 (Abstr f1 (Abstr z1
(Case (Out typ (Var' n2))
(_,Var' z2)
(y1,(Var' f2 :@: Var' y2) :@: (((Var' r2 :@: Var' y3) :@: Var' f3)
:@: Var' z3)))))))) :@: n) :@: f) :@: z)
| r1==r2 && n1==n2 && f1==f2 && f2==f3 &&
z1==z2 && z2==z3 && y1==y2 && y2==y3 &&
isClosed f && isClosed z =
(PARA typ (unpoint $ g(f,z))) :.: (core2pf cont n)
where
unpoint f = APP :.: ((f :.: BANG) :/\: ID)
g (f,z) = let y = getFV f; x = getFV (z:><:Var' y)
in core2pf Unit $
Abstr x $
Case (Var' x) ("_",z)
(y,f :@: (Snd$Var' y) :@: (Fst$Var' y))
----------------------------- pred ^ - recursive result ^
-- paramorphisms for [a]
core2pf cont ((((Fix (Abstr r1 (Abstr l1 (Abstr f1 (Abstr z1
(Case (Out typ (Var' l2))
(_,Var' z2)
(y1,Var' f2 :@: (Fst (Var' y2)) :@: (Snd (Var' y3)) :@:
(Var' r2 :@: (Snd (Var' y4)) :@: Var' f3 :@: Var' z3))))))))
:@: n) :@: f) :@: z)
| r1==r2 && l1==l2 && f1==f2 && f2==f3 &&
z1==z2 && z2==z3 && y1==y2 && y2==y3 && y3==y4 &&
isClosed f && isClosed z =
(PARA typ (unpoint $ g(f,z))) :.: (core2pf cont n)
where
unpoint f = APP :.: ((f :.: BANG) :/\: ID)
g (f,z) = let y = getFV f; x = getFV (z:><:Var' y)
in core2pf Unit $
Abstr x $
Case (Var' x) ("_",z)
(y,f :@: (Fst$Var' y) :@: (Snd$Snd$Var' y) :@: (Fst$Snd$Var' y))
------------------------- head ^ --------- tail ^ --- recursive result ^
core2pf _ Unit = BANG
core2pf cont var@(Var' x) = path cont var
core2pf cont (t1:><:t2) = (core2pf cont t1):/\:(core2pf cont t2)
core2pf cont (Fst t) = FST :.: (core2pf cont t)
core2pf cont (Snd t) = SND :.: (core2pf cont t)
core2pf cont (Abstr x t) = Curry (core2pf (cont:><:(Var' x)) t)
core2pf cont (t1:@:t2) = APP :.: ((core2pf cont t1):/\:(core2pf cont t2))
core2pf cont (Inl t) = INL :.: (core2pf cont t)
core2pf cont (Inr t) = INR :.: (core2pf cont t)
core2pf cont (Case t (x,u) (y,v)) =
APP :.: ((Curry (((core2pf (cont:><:(Var' x)) u) :\/:
(core2pf (cont:><:(Var' y)) v)) :.: (Macro "distr")))
:/\: (core2pf cont t))
core2pf cont (In str t) = IN str :.: (core2pf cont t)
core2pf cont (Out str t) = OUT str :.: (core2pf cont t)
core2pf cont (Fix t) = FIX :.: (core2pf cont t)
-- get the free variables
getFV :: PWTerm -> String
getFV = (\x->x++"_").maximum.getVars
getVars :: PWTerm -> [String]
getVars (Var' str) = [str]
getVars Unit = []
getVars (t1:><:t2) = (getVars t1) ++ (getVars t2)
getVars (Abstr str t) = str:(getVars t)
getVars (t1:@:t2) = (getVars t1) ++ (getVars t2)
getVars (Case t1 (str1,t2) (str2,t3)) =
str1:str2:(getVars t1++getVars t2++getVars t3)
getVars (Fst t) = getVars t
getVars (Snd t) = getVars t
getVars (Inl t) = getVars t
getVars (Inr t) = getVars t
getVars (In _ t) = getVars t
getVars (Out _ t) = getVars t
getVars (Fix t) = getVars t
isClosed :: PWTerm -> Bool
isClosed t = closed t []
where
closed Unit _ = True
closed (Var' str) ac = str `elem` ac
closed (t1:><:t2) ac = (closed t1 ac) && (closed t2 ac)
closed (Abstr str t) ac = closed t (str:ac)
closed (t1:@:t2) ac = (closed t1 ac) && (closed t2 ac)
closed (Case t1 (str1,t2) (str2,t3)) ac =
(closed t1 ac) && (closed t2 (str1:ac)) && (closed t3 (str2:ac))
closed (Fst t) ac = closed t ac
closed (Snd t) ac = closed t ac
closed (Inl t) ac = closed t ac
closed (Inr t) ac = closed t ac
closed (In _ t) ac = closed t ac
closed (Out _ t) ac = closed t ac
closed (Fix t) ac = closed t ac