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

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

{- |

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

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

A let-elaboration via "Data.Yoko.InDT".

-}
module Examples.TermInner where

import Examples.TermBase
import Examples.InnerBase (Inner)
import qualified Examples.InnerBase as I
import qualified Examples.TermGeneric as G
import Examples.InnerGeneric ()

import Type.Yoko

import Data.Yoko.InDT
import Data.Yoko.Reflect





elaborate :: Term -> Inner; elaborate = apply (Elab :: Elab IdM Term)

data Elab m t = Elab
type instance Unwrap (Elab m) t = Elab m t
instance Wrapper (Elab m) where wrap = id; unwrap = id

type instance Dom (Elab m) t = Med m t
type instance Rng (Elab m) t = Med m (TApp (Elab m) t)

type instance TApp (Elab m) Term = Inner

instance (IdM ~ m) => Term ::: Domain (Elab m) where
  inhabits = AppBy $ \_ -> dcDispatch $
    eachOrNT (oneF $ RMNTo elab_Let) $ NT $ imageInDTU Elab

elab_Let (G.Let ds tm) =
  foldr (\(Decl ty tm) x -> I.Lam ty x `I.App` elaborate tm) (elaborate tm) ds





ex0 = Let [Decl TInt (Var 111), Decl TBool (Var 222)] (Var 0)

ex1 = elaborate ex0