content: -----------------------------------------------------------------------------
  -- |
  -- 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
  