-----------------------------------------------------------------
--
-- Implementierung der SECD-Maschine 
-- mit Pretty-Print Ausgabe
-- 
-----------------------------------------------------------------
module SECD_PP where

data Expr = App Expr Expr | Var Int | Lambda Int Expr | Ap 
            deriving (Eq,Show)
 
data Closure = Closure Expr [(Expr,Closure)] 
               deriving (Eq,Show)
               
type S = [Closure]
type E = [(Expr,Closure)]
type C = [Expr]
type D = [(S,E,C)]

--- Funktionen zur Umgebungsverwaltung
add :: [(Expr,a)] -> Int -> a -> [(Expr,a)]
add envlist n e = (Var n,e):envlist

val :: Int -> [(Expr,a)] -> a
val n ((Var m,e):rest) = if n==m then e else val n rest 
val n []               = error "ungebundene Variable"

--- Transitionen der secd Maschine
transform :: (S,E,C,D) -> (S,E,C,D)
transform ((res:s),     e, [],          ((ds,de,dc):d)) 
        = (res:ds,     de, dc,          d)
transform (s,           e, ((Var i):c), d)              
        = ((val i e):s, e, c,           d)
transform (s,                         e, ((Lambda i b):c), d)              
        = ((Closure (Lambda i b) e):s,e, c,                d)
transform (s, e, ((App e1 e2):c), d)  
        = (s, e, e2:e1:Ap:c,      d)
transform (((Closure (Lambda n exp) env):cl:s), e,             (Ap:c), d)  
        = ([],                                 (add env n cl), [exp], (s,e,c):d)
                
---- Startfunktion
evaluate :: Expr -> (S,E,C,D)
evaluate exp = run ([],[],[rename exp],[])

evalseq :: Expr -> IO ()
evalseq  exp  = putStr (unlines (map myshow (stateseq ([],[],[rename exp],[]))))

myshow :: (S,E,C,D) -> String
myshow (s,e,c,d) = "\nStack:   " ++ show s ++ "\nEnv:     " ++ show e ++
                      "\nControl: " ++ show c ++ "\nDump:    " ++ show d 

---- Einzelschrittfunktion
run :: (S,E,C,D) -> (S,E,C,D)
run (s,e,c,d)  = if c == [] && d == [] then (s,e,c,d)
                 else run (transform (s,e,c,d))

stateseq :: (S,E,C,D) -> [(S,E,C,D)]
stateseq (s,e,c,d)  = if c == [] && d == [] then [(s,e,c,d)]
                      else (s,e,c,d): stateseq (transform (s,e,c,d))

---- Umbenennung gebundener Variablen, 
---- damit keine Variablenkonflikte auftreten
rename :: Expr -> Expr
rename exp = e where (e,n) = new exp 0 []

new :: Expr -> Int -> [(Int,Int)] -> (Expr,Int)
new (Var i)     n list = (Var (get i list),n)
new (App e1 e2) n list = (App newe1 newe2,n2)
    where (newe1,n1) = new e1 n  list
          (newe2,n2) = new e2 n1 list
new (Lambda i e) n list = (Lambda n newe,n1)
    where (newe,n1)  = new e (n+1) ((i,n):list)

get :: Eq a => a -> [(a,b)] -> b 
get i []        = error "freie Variable bei Umbenennung entdeckt"
get i ((j,n):l) = if i==j then n else get i l


-- Pretty Printer
showexp :: Expr -> String
showexp (App e1 e2) = "(" ++ showexp e1 ++ " " ++ showexp e2 ++ ")"
showexp (Var n)     = [varlist!!n]
showexp (Lambda n e) = "lam " ++ [varlist!!n] ++ ". " ++ showexp e 

varlist :: String
varlist = ['a'..'z'] ++ varlist


result :: (S,E,C,D) -> Closure
result (s,e,c,d) = (head s)

showres :: (S,E,C,D) -> String
showres = showexp . cl2e . result

cl2e :: Closure -> Expr 
cl2e (Closure e []) = e
cl2e cl = error "cl2e not defined" 

--- Beispiel Lambda Ausdruecke
i = (Lambda 1 (Var 1))
k = (Lambda 1 (Lambda 2 (Var 1)))
s = (Lambda 1 (Lambda 2 (Lambda 3 (App (App (Var 1) (Var 3)) 
                                       (App (Var 2) (Var 3))))))
suc = (Lambda 1 (Lambda 2 (Lambda 3 (App (App (Var 1) (Var 2))
                                         (App (Var 2) (Var 3))
      )         )         )         )
num0 = (Lambda 1 (Lambda 2 (Var 2)))
num1 = (Lambda 4 (Lambda 5 (App (Var 4) (Var 5))))

y = Lambda 1 (App (Lambda 2 (App (Var 1) (App (Var 2) (Var 2))))
                  (Lambda 3 (App (Var 1) (App (Var 3) (Var 3)))))
theta = (App (Lambda 1 (Lambda 2 (App (Var 2) (App (App (Var 1) (Var 1)) (Var 2)))))
             (Lambda 1 (Lambda 2 (App (Var 2) (App (App (Var 1) (Var 1)) (Var 2)))))
        )     
                  
tt = (Lambda 1 (Lambda 2 (Var 1)))
ff = (Lambda 1 (Lambda 2 (Var 2)))
iff = (Lambda 1 (Lambda 2 (Lambda 3 (App (App (Var 1) (Var 2)) (Var 3)))))

g = Lambda 1 (Lambda 2 (App (App (App iff tt) num0) (App (Var 1) num0)))