{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses,
  FlexibleInstances, UndecidableInstances #-}

{-# OPTIONS_GHC -fcontext-stack=200 #-}

module Examples.LL where

import qualified Examples.InnerBase as I

import qualified Data.Set as Set
import qualified Data.IntMap as IM

import Examples.LLBasics

import qualified Examples.InnerGeneric as IG
import qualified Examples.LLGeneric ()

import Data.Yoko





lambdaLift :: Inner -> [Type] -> Prog
lambdaLift x e = Prog (reverse tlds) main where
  (main, tlds) = runMnd (ll x) (e, IM.empty, 0)

llLam (IG.Lam ty tm) = newTLD ty (fvs tm) $ local updE $ ll tm where
  updE (rho, rn) = (ty : rho, support `prepend` rn) where
    support =
      IM.fromDistinctAscList . flip zip [0..] . Set.toAscList . fvs $ tm
llVar (IG.Var i) = asks $ \(_, rn) -> Var $ lookupRN rn i

---------------------------------------- default
ll :: Inner -> Mnd Term; ll = applyA (LL :: LL IdM Inner)

data LL m t = LL; type instance Idiom (LL m) = Mnd
type instance Unwrap (LL m) t = LL m t
instance Wrapper (LL m) where wrap = id; unwrap = id

type instance Dom (LL m) t = Med m t
type instance Rng (LL m) t = Med m (TApp (LL m) t)
type instance TApp (LL m) Inner = Term -- instance for each type in binding group

instance (IdM ~ m) => Inner ::: DomainA (LL m) where
  inhabits = AppABy $ \_ -> dcDispatch $
    eachOrNT (oneF (RMNTo llLam) ||. llVar) $ NT $ imageInDTAD LL
--  eachOrNT (one_ [qP|RMNTo m (Mnd Term) :: *->*|] llLam ||. llVar) $ NT $ imageInDTAD LL





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> lambdaLift 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))