{-
 -   The Lambda Shell, an interactive environment for evaluating pure untyped lambda terms.
 -   Copyright (C) 2005-2011, Robert Dockins
 -
 -   This program is free software; you can redistribute it and/or modify
 -   it under the terms of the GNU General Public License as published by
 -   the Free Software Foundation; either version 2 of the License, or
 -   (at your option) any later version.
 -
 -   This program is distributed in the hope that it will be useful,
 -   but WITHOUT ANY WARRANTY; without even the implied warranty of
 -   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 -   GNU General Public License for more details.
 -
 -   You should have received a copy of the GNU General Public License
 -   along with this program; if not, write to the Free Software
 -   Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA
 -}

{- |
  This module defines CPS transformations on lambda terms.
-}

module CPS
( simple_cps
, eta_cps
, onepass_cps
, CPS
) where

import Lambda

type CPS m
     = Bindings () String
    -> PureLambda () String
    -> m (PureLambda () String)

-- | The simple CPS transform defined by Plotkin
simple_cps :: Monad m => CPS m

simple_cps b t = do
    x <- do_simple_cps b t
    return (App () x (Lam () "q" (Var () 0)))

do_simple_cps :: Monad m => CPS m

do_simple_cps b (Binding _ name) =
    lookupBindingM name b >>=
       maybe (return (Lam () "k" $ App () (Var () 0) $ (Binding () name)))
             (do_simple_cps b)

do_simple_cps b (Var _ i) =
    return (Lam () "k" $ App () (Var () 0) $ (Var () (i+1)))

do_simple_cps b (Lam _ l t) = do
    t' <- do_simple_cps b (lamShift 1 1 t)
    return
      (Lam () "k" $ App () (Var () 0) $ Lam () l t')

do_simple_cps b (App _ t1 t2) = do
    t1' <- do_simple_cps b (lamShift 0 1 t1)
    t2' <- do_simple_cps b (lamShift 0 2 t2)
    return
      (Lam () "k" $ App () t1' $
         Lam () "m" $ App () t2' $
           Lam () "n" $
             App () (App () (Var () 1) (Var () 0)) (Var () 2))


-- | A version of Plotkin's CPS transform with additional
--   eta expansions, preparing for the one-pass
--   simplifying transform
eta_cps :: Monad m => CPS m
eta_cps b t = do
   x <- do_eta_cps b t
   return (App () x (Lam () "q" (Var () 0)))

do_eta_cps :: Monad m => CPS m

do_eta_cps b (Binding _ name) =
    lookupBindingM name b >>=
      maybe (return (Lam () "k" $ App () (Var () 0) $ (Binding () name)))
            (do_simple_cps b)

do_eta_cps b (Var _ i) =
    return (Lam () "k" $ App () (Var () 0) $ (Var () (i+1)))


do_eta_cps b (Lam _ l t) = do
    t' <- do_eta_cps b (lamShift 2 1 (lamShift 0 1 t))
    return
      (Lam () "k" $ App () (Var () 0) $
        Lam () l $
          Lam () "kk" $ App () t' $
            Lam () "m" $ App () (Var () 1) (Var () 0)
      )


do_eta_cps b (App _ t1 t2) = do
    t1' <- do_eta_cps b (lamShift 0 1 t1)
    t2' <- do_eta_cps b (lamShift 0 2 t2)
    return
      (Lam () "k" $ App () t1' $
        Lam () "m" $ App () t2' $
          Lam () "n" $
            App () (App () (Var () 1) (Var () 0)) $
              Lam () "a" $ App () (Var () 3) (Var () 0)
      )




-- | The \"one-pass\" properly-tail-recursive CPS tranform due to Danvy and Filinski,
--   from the paper \"Representing Control: A Study of the CPS Transformation\",
--   in /Mathematical Structures in Computer Science/, 1991.
--
--   Here is is actually implemented as a two-pass tranform.
--   In the first pass we create the eta-expanded version and note
--   which redexes are adminstrative.  In the second pass all administrative
--   redexes are reduced, leaving only the dynamic redexes.

onepass_cps :: Monad m => CPS m
onepass_cps b t = do
   x <- do_onepass_cps b t
   simplify_onepass (App True x (Lam True "q" (Var True 0)))


simplify_onepass
    :: Monad m
    => PureLambda Bool String
    -> m (PureLambda () String)

simplify_onepass (Binding _ _) = fail "bug: binding found in simplify_onepass"

simplify_onepass (Var False i)     = return (Var () i)
simplify_onepass (Lam False l t)   = simplify_onepass t >>= \t' -> return (Lam () l t')
simplify_onepass (App False t1 t2) = do
    t1' <- simplify_onepass t1
    t2' <- simplify_onepass t2
    return (App () t1' t2')

simplify_onepass (App True (Lam True _ t) s) = simplify_onepass (lamSubst s t)
simplify_onepass t  = fail $ "bug: found unexpected administrative terms in simplify_onepass\n"++(show t)


do_onepass_cps
    :: Monad m
    => Bindings () String
    -> PureLambda () String
    -> m (PureLambda Bool String)

do_onepass_cps b (Binding _ name) =
     lookupBindingM name b >>= 
        maybe (return (Lam True "k" $ App True (Var True 0) $ (Binding False name)))
              (do_onepass_cps b)

do_onepass_cps b (Var _ i) =
     return (Lam True "k" $ App True (Var True 0) $ (Var False (i+1)))

do_onepass_cps b (Lam _ l t) = do
    t' <- do_onepass_cps_tail b (lamShift 2 1 (lamShift 0 1 t))
    return
       (Lam True "k0" $ App True (Var True 0) $
          Lam False l $ Lam False "k" $ App True t' $ (Var False 0)
       )

do_onepass_cps b (App _ t1 t2) = do
    t1' <- do_onepass_cps b (lamShift 0 1 t1)
    t2' <- do_onepass_cps b (lamShift 0 2 t2)
    return
        (Lam True "k0" $ App True t1' $
           Lam True "m0" $ App True t2' $
             Lam True "n" $
               App False (App False (Var True 1) (Var True 0)) $
                 Lam False "a" $ App True (Var True 3) (Var False 0)
        )


do_onepass_cps_tail
    :: Monad m
    => Bindings () String
    -> PureLambda () String
    -> m (PureLambda Bool String)

do_onepass_cps_tail b (Binding _ name) =
     lookupBindingM name b >>=
       maybe (return (Lam True "k0" (App False (Var True 0) (Binding False name))))
             (do_onepass_cps_tail b)

do_onepass_cps_tail b (Var _ i) =
    return (Lam True "k0" (App False (Var True 0) (Var False (i+1))))

do_onepass_cps_tail b (Lam _ l t) = do
    t' <- do_onepass_cps_tail b (lamShift 2 1 (lamShift 0 1 t))
    return
      (Lam True "k0" $ App False (Var True 0) $
         Lam False l $ Lam False "k" $ App True t' $ (Var False 0)
      )

do_onepass_cps_tail b (App _ t1 t2) = do
    t1' <- do_onepass_cps b (lamShift 0 1 t1)
    t2' <- do_onepass_cps b (lamShift 0 2 t2)
    return
      (Lam True "k0" $ App True t1' $
         Lam True "m" $ App True t2' $
           Lam True "n" $
             App False (App False (Var True 1) (Var True 0))
               (Var True 2)
      )