{- |

Module      :  Examples.LLDirect
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

Lambda-lifts 'Examples.InnerBase.Inner' to 'Examples.LLBase.LL' without using
@yoko@. Compare to "Examples.LL0" and "Examples.LL".

-}
module Examples.LLDirect where

import Examples.TermBase (Type(..))
import Examples.InnerBase (Inner)
import qualified Examples.InnerBase as I
import Examples.LLBase

import qualified Data.Set as Set; import Data.Set (Set)
import qualified Data.IntMap as IM; import Data.IntMap (IntMap)



fvs :: Inner -> Set Int
fvs (I.Lam ty tm) = Set.map (subtract 1) $ Set.filter (> 0) $ fvs tm
fvs (I.Var i) = Set.singleton i
fvs (I.App tm1 tm2) = fvs tm1 `Set.union` fvs tm2

bump :: Set Int -> Set Int
bump = Set.map (subtract 1) . Set.filter (> 0)

renm :: IntMap Int -> Int -> Term -> Term
renm m dv tm@(Var i) = maybe tm Var $ IM.lookup i m
renm m dv (App tm1 tm2) = App (renm m dv tm1) (renm m dv tm2)
renm _ dv (DVar i) = DVar (i + dv)

renmP :: IntMap Int -> Int -> Prog -> Prog
renmP m dv (Prog tlds main) = Prog (map each tlds) (renm m dv main) where
  each (tys, ty, tm) = (tys, ty, renm m dv tm)




type Env = [Type]

lambdaLift :: Inner -> Env -> Prog
lambdaLift (I.Lam ty tm) rho = newTLD ty rho (fvs tm) $ lambdaLift tm (ty : rho)
lambdaLift (I.Var i) rho = Prog [] $ Var i
lambdaLift (I.App tm1 tm2) rho = Prog (tlds1 ++ tlds2) $ App main1 main2 where
  Prog tlds1 main1 = lambdaLift tm1 rho
  Prog tlds2 main2 = renmP IM.empty (length tlds1) $ lambdaLift tm2 rho



newTLD :: Type -> Env -> Set Int -> Prog -> Prog
-- NB could check if such a TLD already exists; lambdaLift@I.App would need to handle
-- that too
newTLD ty rho fvs (Prog tlds main) =
  Prog ((map (rho !!) fvs', ty, renm rn 0 main) : tlds) $
  foldl ((. Var) . App) (DVar 0) fvs'
  where rn = IM.fromDistinctAscList $ zip (Set.toAscList fvs) [0..]
        fvs' = reverse $ Set.toAscList $ bump fvs





env0 = [TBool, TBool, TArrow TInt TInt, TInt]
ex0 = I.Lam TInt $ I.Lam TInt $ I.Var 4 `I.App` I.Var 1 `I.App` I.Var 0
ex1 = ex0 `I.App` I.Var 3
ex2 = (I.Lam (TArrow TInt TInt `TArrow` TArrow TInt TInt) $ I.Var 0) `I.App`
      (I.Lam (TArrow TInt TInt) $ I.Var 0)


-- *LL> ll ex1 env0
-- Prog [([TArrow TInt TInt],TInt,App (App (DVar 0) (Var 1)) (Var 0)),
--       ([TArrow TInt TInt,TInt],TInt,App (App (Var 2) (Var 1)) (Var 0))
--      ] (App (App (DVar 0) (Var 2)) (Var 3))