-----------------------------------------------------------------
--
-- Implementierung der SECD-Maschine mit Auswertung zur 
-- Normalform und Pretty-Print Ausgabe
-- 
-----------------------------------------------------------------


data Expr = App Expr Expr | Var Int | Lambda Int Expr | Ap | Lam Int
            deriving (Eq,Show)
 
data Closure = Closure Expr [(Expr,Closure)] 
               deriving (Eq)

instance Show Closure 
  where show (Closure exp env) = "Closure " ++ show exp ++ "[...]"
               
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"

-- für Normalformauswertung
remove :: [(Expr,a)] -> Int -> [(Expr,a)]
remove [] n = []
remove ((Var m,e):envlist) n 
            = if n==m then (remove envlist n) else (Var m,e):(remove envlist n)

--- 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)
-- Version mit nur Top Level Auswertung:
--transform (s,                         e, ((Lambda i b):c), d)              
--        = ((Closure (Lambda i b) e):s,e, c,                d)
-- Version mit Normalform-Auswertung
transform (s,  e,         ((Lambda i b):c), d)  
        = ([], varenv++e, [b,(Lam i)],      (s,e,c):d)
           where varenv = [(Var i, Closure (Var i) varenv)]
-- Achtung: geänderte Reihenfolge
transform (s, e, ((App e1 e2):c), d)  
        = (s, e, e1:e2:Ap:c,      d)
transform ((cl:(Closure (Lambda n exp) env):s), e,             (Ap:c), d)  
        = ([],                                 (add env n cl), [exp], (s,e,c):d)
-- nur fuer Version mit Normalformauswertung
transform (((Closure exp2 env2):(Closure exp env):s), e, (Ap:c), d)  
        = ( (Closure (App exp exp2) (env++env2)):s,   e, c,      d)
transform (((Closure exp env):s),                 e, ((Lam i):c),((ds,de,dc):d))
        = ((Closure (Lambda i exp) (remove env i)):ds, de, dc,         d)
        
---- Startfunktion
evaluate :: Expr -> (S,E,C,D)
evaluate exp = run ([],[],[rename exp],[])

evalseq :: Expr -> IO ()
evalseq exp  = putStr (unlines (map myshow (stateseq 0 ([],[],[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 
-- mit Schrittzaehler
myshow :: (Int, (S,E,C,D)) -> String
myshow (i,(s,e,c,d)) = "\nStep " ++ show i ++
                       "\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))
-- mit Schrittzähler: 
stateseq :: Int -> (S,E,C,D) -> [(Int, (S,E,C,D))]
stateseq i (s,e,c,d)  = if c == [] && d == [] then [(i,(s,e,c,d))]
                        else (i,(s,e,c,d)): stateseq (i+1) (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

--- vordefinierte 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)))))
                  
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)))))


-- 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 = ['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 _) | null (free e)  = e
                   | otherwise      = error "cl2e not defined" 

free :: Expr -> [Int]
free (Var i) = [i]
free (Lambda i e) = [j | j <- free e, j /= i]
free (App e1 e2)  = free e1 ++ free e2
free _            = []