content: {-# LANGUAGE RankNTypes, FlexibleContexts, GADTs, PatternGuards #-}
  
  -- An implementation of interpreter stacking, to check whether we have achieved
  -- true lazy specialization.  This represents terms of λ-calculus in itself as
  -- Church-encoded deBruijn-encoded terms. 
  
  module Main where
  
  import HOAS
  import DeBruijn
  import qualified BUBS
  import qualified Reference
  import qualified Thyer
  import qualified Naive
  import System.Environment (getArgs)
  import qualified Data.Char as Char
  import Data.List (intercalate)
  
  data Value
      = VPlus
      | VAdd Integer
      | VInt Integer
      deriving Show
  
  instance Primitive Value where
      apply VPlus (VInt x) = VAdd x
      apply (VAdd x) (VInt y) = VInt (x+y)
      apply x y = error $ "Type error when applying (" ++ show x ++ ") to (" ++ show y ++ ")"
  
  quote :: (Term t) => (forall u. (Term u) => u) -> t
  quote expr = 
      let_ (fun (\f -> fun (\x -> x))) $ \zero ->
      let_ (fun (\n -> fun (\f -> fun (\x -> f % (n % f % x))))) $ \succ ->
  
      let_ (fun (\body -> fun (\l -> fun (\a -> fun (\v -> l % (body % l % a % v)))))) $ \mkLam ->
      let_ (fun (\left -> fun (\right -> fun (\l -> fun (\a -> fun (\v -> a % (left % l % a % v) % (right % l % a % v))))))) $ \mkApp -> 
      let_ (fun (\num -> fun (\l -> fun (\a -> fun (\v -> v % num))))) $ \mkVar -> 
  
      let quote (ELam body) = mkLam % quote body
          quote (EApp l r) = mkApp % quote l % quote r
          quote (EVar v)   = mkVar % (iterate (succ %) zero !! fromIntegral v) in
      quote (getDeBruijn expr)
  
  interp :: (Term t) => t
  interp = 
      let_ (fun (\x -> x)) $ \id -> 
  
      let_ (fun (\n -> fun (\c -> n))) $ \nil ->
      let_ (fun (\x -> fun (\xs -> fun (\n -> fun (\c -> c % x % xs))))) $ \cons ->
  
      let_ (fun (\l -> l % id % fun (\x -> fun (\xs -> x)))) $ \head ->
      let_ (fun (\l -> l % id % fun (\x -> fun (\xs -> xs)))) $ \tail ->
  
      let_ (fun (\l -> fun (\n -> head % (n % tail % l)))) $ \nth -> 
      
      let_ (fun (\term ->
          term % fun (\body -> fun (\env -> fun (\x -> body % (cons % x % env))))
               % fun (\left -> fun (\right -> fun (\env -> left % env % (right % env))))
               % fun (\n    -> fun (\env -> nth % env % n))
               % nil)) $ \eval -> 
      eval
  
  program :: (Term t) => t
  program = 
      let_ (fun (\f -> fun (\x -> x))) $ \zero ->
      let_ (fun (\n -> fun (\f -> fun (\x -> f % (n % f % x))))) $ \succ ->
      let_ (fun (\n -> fun (\m -> n % succ % m))) $ \plus -> 
      let_ (fun (\n -> fun (\m -> n % (plus % m) % zero))) $ \times ->
      let_ (succ % (succ % (succ % zero))) $ \three -> 
      times % three % three
  
  go :: Int -> (PrimTerm Value t) => t
  go n = 
      let_ (fun (\n -> n % prim (VAdd 1) % prim (VInt 0))) $ \toPrim ->
      toPrim % (foldl (%) interp (replicate n (quote interp)) % quote program)
  
  
  -- This one loops in naive, returns 0 in all others
  {-
  go n = fix % fun (\f -> fun (\b -> fun (\x -> fun (\y -> b % x % (fun (\x -> f % false % x) % y % y))))) % true % true % prim (VInt 0)
      where
      fix = fun (\f -> fun (\x -> x % x) % fun (\x -> f % (x % x)))
      false = fun (\a -> fun (\b -> a))
      true = fun (\a -> fun (\b -> b))
  -}
  
      
  interpreters :: [ (String, Int -> IO Value) ]
  interpreters = [ "bubs"  --> BUBS.eval . go
                 , "thyer" --> Thyer.eval . go
                 , "ref"   --> return . Reference.eval . go
                 , "naive" --> \n -> return (Naive.eval (go n))
                 ]
      where
      infix 0 -->
      (-->) = (,)
  
  main :: IO ()
  main = do
      args <- getArgs
      case args of
          [i, n] | Just interp <- lookup i interpreters, all Char.isDigit n 
              -> print =<< interp (read n)
          _   -> fail $ "Usage: InterpreterStack <interp> <levels>, <interp> is one of " 
                     ++ intercalate "," (map fst interpreters) ++ ", and <levels> is a natural"
  