{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
--
-- |
-- Module      : F1_Eval
-- Authors     : Sean Seefried (http://www.cse.unsw.edu.au/~sseefried)
-- Copyright   : (c) 2007
-- License     : BSD3
-- Created     : 15 Apr 2007
--

module F1_Eval
where

import F0_Alpha

data Exp_1 (cxt :: * -> *) = 
  LetE String (Exp cxt) (Exp cxt)

instance  ( Sat (EvalD cxt (Exp   (EvalD cxt)))
          , Sat (EvalD cxt (Exp_0 (EvalD cxt)))
          , Sat (EvalD cxt (Exp_1 (EvalD cxt)))
          ) => Alpha (EvalD cxt) (Exp_1 (EvalD cxt)) 
 where
  alpha  (_::P (EvalD cxt)) 
         (LetE name body exp :: Exp_1 (EvalD cxt)) =
    \  (s::(String, String)) ->
       letE  (u::P (EvalD cxt)) (swap s name) 
             (alpha (u::P (EvalD cxt)) body s)
             (alpha (u::P (EvalD cxt)) exp s)

class  ( Sat (EvalD cxt b)
       , Alpha (EvalD cxt) b) => Eval cxt b where
  eval   ::  P (EvalD cxt) -> b -> Env (EvalD cxt) -> 
             Exp (EvalD cxt)
  apply  ::  P (EvalD cxt) -> b -> Env (EvalD cxt) -> 
             Exp (EvalD cxt) -> Exp (EvalD cxt)

data EvalD cxt b = 
  EvalD  { eval'    ::  P (EvalD cxt) -> b -> 
                        Env (EvalD cxt) -> 
                        Exp (EvalD cxt)
         , apply'   ::  P (EvalD cxt) -> b -> 
                        Env (EvalD cxt) -> 
                        Exp (EvalD cxt) -> 
                        Exp (EvalD cxt)
         , evalExt  ::  cxt b } 

instance Sat (EvalD cxt (Exp (EvalD cxt))) =>
         Eval cxt (Exp (EvalD cxt)) where
  eval  (_::P (EvalD cxt)) 
        (MkExp e :: Exp (EvalD cxt)) =
    \  (x1:: Env (EvalD cxt)) -> 
       eval' dict (u::P (EvalD cxt)) e x1
  apply  (_::P (EvalD cxt)) 
         (MkExp e :: Exp (EvalD cxt)) =
    \  (x1::Env (EvalD cxt)) (x2::Exp (EvalD cxt)) -> 
       apply' dict (u::P (EvalD cxt)) e x1 x2 

instance  ( Sat (EvalD cxt (Exp   (EvalD cxt)))
          , Sat (EvalD cxt (Exp_0 (EvalD cxt)))
          , Sat (EvalD cxt (Exp_1 (EvalD cxt)))
          ) => Eval cxt (Exp_0 (EvalD cxt)) where
  eval  (_::P (EvalD cxt)) 
        (Var name::Exp_0 (EvalD cxt)) =
    \(env::Env (EvalD cxt)) -> lookupEnv env name
  eval  (_::P (EvalD cxt)) 
        (Lam name body::Exp_0 (EvalD cxt)) =
    \  (env::Env (EvalD cxt)) -> 
       lam (u::P (EvalD cxt)) name body
  eval  (_::P (EvalD cxt)) 
        (App f x::Exp_0 (EvalD cxt)) =
   \  (env::Env (EvalD cxt)) -> 
      apply'  dict (u::P (EvalD cxt)) x env 
              (eval' dict (u::P (EvalD cxt)) f env)
  apply  (_::P (EvalD cxt)) 
         (Var v::Exp_0 (EvalD cxt)) =
    \  (env::Env (EvalD cxt)) 
       (x::Exp (EvalD cxt)) -> 
       error "Function expected"
  apply  (_::P (EvalD cxt)) 
         (Lam name body::Exp_0 (EvalD cxt)) =
    \  (env::Env (EvalD cxt)) 
       (x::Exp (EvalD cxt)) -> 
       eval'  dict (u::P (EvalD cxt)) body 
         (extEnv env  (name, 
                      eval'  dict (u::P (EvalD cxt))
                             x env))
  apply  (_::P (EvalD cxt)) 
         (App f x::Exp_0 (EvalD cxt)) = 
    \  (env::Env (EvalD cxt)) 
       (x::Exp (EvalD cxt)) -> 
       error "Function expected"

instance  ( Sat (EvalD cxt (Exp (EvalD cxt)))
          , Sat (EvalD cxt (Exp_0 (EvalD cxt)))
          , Sat (EvalD cxt (Exp_1 (EvalD cxt)))
          ) => Eval cxt (Exp_1 (EvalD cxt)) where
  eval  (_::P (EvalD cxt)) 
        (LetE name body exp::Exp_1 (EvalD cxt)) =
    \  (env::Env (EvalD cxt)) -> 
       eval'  dict (u::P (EvalD cxt)) 
              (app  (u::P (EvalD cxt)) 
                    (lam (u::P (EvalD cxt)) name exp) 
                    body) env
  apply  (_::P (EvalD cxt)) 
         (LetE name body exp::Exp_1 (EvalD cxt)) =
    \  (env::Env (EvalD cxt)) 
       (x::Exp (EvalD cxt)) ->
       error "Function expected"

data EvalEnd b 

class Eval EvalEnd b => EvalCap b

instance EvalCap (Exp   (EvalD EvalEnd))
instance EvalCap (Exp_0 (EvalD EvalEnd))
instance EvalCap (Exp_1 (EvalD EvalEnd))

instance EvalCap b => Sat (EvalD EvalEnd b) where
    dict = EvalD  { eval'   = eval
                  , apply'  = apply
                  , evalExt = error "Capped at Eval" }


letE ::  forall cxt.  
         ( Sat (EvalD cxt (Exp   (EvalD cxt)))
         , Sat (EvalD cxt (Exp_0 (EvalD cxt)))
         , Sat (EvalD cxt (Exp_1 (EvalD cxt)))) => 
         P (EvalD cxt) -> String -> Exp (EvalD cxt) -> 
         Exp (EvalD cxt) -> Exp (EvalD cxt) 
letE (_::P (EvalD cxt)) = 
    \  (x1::String) (x2::Exp (EvalD cxt)) 
       (x3::Exp (EvalD cxt)) -> 
       MkExp (LetE x1 x2 x3::Exp_1 (EvalD cxt))

type Env cxt = [(String, Exp cxt)]

lookupEnv ::  Env (EvalD cxt) -> String -> 
              Exp (EvalD cxt)
lookupEnv ([]::Env (EvalD cxt)) =
  \(name::String) ->  
   error (  "lookupEnv : Variable " ++ 
            show name ++ " not found")
lookupEnv (hd:tl :: Env (EvalD cxt)) =
    \(name'::String) -> lookupEnvAux hd tl name'

lookupEnvAux:: (String, Exp (EvalD cxt)) -> 
               Env (EvalD cxt) -> String -> 
               Exp (EvalD cxt)
lookupEnvAux (name, term) =
  \(rest::Env (EvalD cxt)) (name'::String) ->
      if name==name' 
      then term else lookupEnv rest name'
    

extEnv ::  Env (EvalD cxt) -> 
           (String, Exp (EvalD cxt)) -> Env (EvalD cxt)
extEnv =  \(env::Env (EvalD cxt)) 
          (x::(String, Exp (EvalD cxt))) -> x : env

--
-- Tests
--

test5 :: 
  forall cxt.  ( Sat (EvalD cxt (Exp (EvalD cxt)))
               , Sat (EvalD cxt (Exp_0 (EvalD cxt))) 
               , Sat (EvalD cxt (Exp_1 (EvalD cxt)))
               ) => Exp (EvalD cxt)
test5 = 
  let p = u :: P (EvalD cxt) 
  in letE p "x" (lam p "y" (var p "y")) (app p (var p "x") (var p "x"))

etest0, etest1, etest2, etest3, etest4, etest5 :: Exp (EvalD EvalEnd)
etest0 = test0
etest1 = test1
etest2 = test2
etest3 = test3
etest4 = test4
etest5 = test5

eeval :: Exp (EvalD EvalEnd) -> Env (EvalD EvalEnd) -> Exp (EvalD EvalEnd)
eeval = eval (u::P (EvalD EvalEnd))

eNil = [] :: Env (EvalD EvalEnd)