content: {-# LANGUAGE TupleSections, FlexibleInstances, MultiParamTypeClasses #-}
  
  -- Compiler from HOAS to Thyer's depth notation.
  
  module Depth 
      ( Exp(..), ExpNode, Depth, prim, getDepth )
  where
  
  import HOAS
  import qualified Data.Map as Map
  import Control.Monad.Trans.Class
  import Control.Monad.Trans.Reader
  import Control.Monad.Trans.State
  import Control.Applicative
  import Control.Arrow
  
  type ExpNode a = (Int, Exp a)
  
  data Exp a
      = Lambda (ExpNode a)
      | Apply (ExpNode a) (ExpNode a)
      | Var
      | Prim a
      deriving Show
  
  newtype Depth a = Depth { runDepth :: ReaderT Int (State Int) (ExpNode a) }
  
  instance Term (Depth a) where
      Depth t % Depth u = Depth $ liftA2 ap t u
          where
          ap tt@(dt,_) tu@(du,_) = (max dt du, Apply tt tu)
      fun f = Depth $ do
          varid <- lift get
          lift $ put (succ varid)
          depth <- ask
          local succ . fmap ((depth,) . Lambda) . runDepth . f . Depth . return $ (succ depth, Var)
  
  instance PrimTerm a (Depth a) where
      prim = Depth . return . (0,) . Prim
  
  getDepth :: Depth a -> ExpNode a
  getDepth d = evalState (runReaderT (runDepth d) 0) 0
  