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

u = undefined

data P d 

class Sat a where
    dict :: a

data Exp (cxt :: * -> *) = 
  forall b. Alpha cxt b => MkExp b

class Sat (cxt b) => Alpha cxt b where
    alpha :: P cxt -> b -> (String, String) -> Exp cxt

data Exp_0 cxt  = Var String
                | Lam String (Exp cxt)
                | App (Exp cxt) (Exp cxt)


instance  (Sat (cxt (Exp cxt))
          , Sat (cxt (Exp_0 cxt))
          ) => Alpha cxt (Exp_0 cxt) where
  alpha (_::P cxt) (Var v :: Exp_0 cxt) = 
    \(s::(String, String)) -> var (u::P cxt) (swap s v)
  alpha (_::P cxt) (Lam v body :: Exp_0 cxt) = 
     \(s::(String,String)) -> 
        lam (u::P cxt)  (swap s v) 
                        (alpha (u::P cxt) body s)
  alpha (_::P cxt) (App a b :: Exp_0 cxt) = 
    \(s::(String,String)) ->
       app (u::P cxt) 
         (alpha (u::P cxt) a s) (alpha (u::P cxt) b s) 

instance  Sat (cxt (Exp cxt)) 
          => Alpha cxt (Exp cxt) where
    alpha (_::P cxt) (MkExp e :: Exp cxt) = 
      \(s::(String, String)) -> alpha (u::P cxt) e s


data AlphaEnd b

class Alpha AlphaEnd b => AlphaCap b

instance AlphaCap (Exp_0 AlphaEnd)
instance AlphaCap (Exp AlphaEnd)


instance AlphaCap b => Sat (AlphaEnd b) where
    dict = error "Capped at Alpha"

var ::  forall cxt.  (Sat (cxt (Exp cxt))
                     , Sat (cxt (Exp_0 cxt))) => 
        P cxt -> String -> Exp cxt 
var (_::P cxt) = 
  \(x1::String) -> MkExp (Var x1::Exp_0 cxt)

lam ::  forall cxt.  ( Sat (cxt (Exp cxt))
                     , Sat (cxt (Exp_0 cxt))) =>
        P cxt -> String -> Exp cxt -> Exp cxt 
lam (_::P cxt) =  \(x1::String) (x2::Exp cxt) -> 
                  MkExp (Lam x1 x2 :: Exp_0 cxt)

app ::  forall cxt.  ( Sat (cxt (Exp cxt))
                     , Sat (cxt (Exp_0 cxt))) =>
        P cxt -> Exp cxt -> Exp cxt -> Exp cxt 
app (_::P cxt) =  \(x1::Exp cxt) (x2::Exp cxt) -> 
                  MkExp (App x1 x2::Exp_0 cxt)

swap :: (String, String) -> String -> String
swap ((a,b) :: (String,String)) = 
  \(o::String) -> if a == o then b else o


--
-- Some tests
--

test0, test1, test2, test3, test4 ::
  forall cxt.( Sat (cxt (Exp cxt))
             , Sat (cxt (Exp_0 cxt))) => Exp cxt
test0  = lam  (u::P cxt) "x" (var (u::P cxt) "x")
test1  = lam  (u::P cxt)"v" (var  (u::P cxt) "v")
test2  = (app (u::P cxt) test0 test1)
test3  = (app (u::P cxt) (var (u::P cxt) "x") (var (u::P cxt) "y"))
test4  = var (u::P cxt) "z"

btest0, btest1, btest2, btest3, btest4:: Exp AlphaEnd
btest0 = test0
btest1 = test1
btest2 = test2
btest3 = test3
btest4 = test4