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

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

data Constants = N Int | O Operation | If deriving Eq
data Operation = Plus | Times | Leq       deriving Eq

--- 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 (s, e, ((Var i):c), d)              
        = ((val i e):s, e, c, d)
transform (s, e, ((Lam i b):c), d)              
        = ((Closure (Lam i b) e):s,e, c, d)
transform (s, e, ((App e1 e2):c), d)  
        = (s, e, e2:e1:Ap:c, d)
transform (((Closure (Lam n exp) env):cl:s), e, (Ap:c), d)  
        = ([], (add env n cl), [exp], (s,e,c):d)
transform ((res:s),  e, [], ((ds,de,dc):d)) 
        = (res:ds, de, dc, d)
-- Konstantenauswertung        
transform (s, e, (Con x):c, d)
    = ((Closure (Con x) []):s, e, c, d)   
transform (((Closure (Con (O op)) []):
            (Closure (Con (N n)) []):
            (Closure (Con (N m)) []):s), e, (Ap:Ap:c), d) 
    = ((Closure (Con (N (apply op n m))) []):s, e, c, d)
transform ((Closure (Con If) []):
           (Closure (Con (N x)) []):cl1:cl2:s, e, (Ap:Ap:Ap:c), d) 
    = if x == 1 then (cl1:s, e, c, d) else (cl2:s, e, c, d)
transform (((Closure exp env):(Closure exp2 env2):s), e, (Ap:c), d)  
    = ( (Closure (App exp exp2) (env++env2)):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))

-- Konstantenauswertung 
apply :: Operation -> Int -> Int -> Int 
apply Plus  n m = n+m
apply Times n m = n*m
apply Leq   n m = if n <= m then 1 else 0
 
---- 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 (Lam i e) n list = (Lam n newe,n1)
    where (newe,n1)  = new e (n+1) ((i,n):list)
new (Con c)     n list = (Con c,n)

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
instance Show Expr where
    show (App e1 e2) = "(" ++ show e1 ++ " " ++ show e2 ++ ")"
    show (Var n)     = [varlist!!n]
    show (Lam n e) = "lam " ++ [varlist!!n] ++ ". " ++ show e 
    show (Con c)     = show c
    show Ap          = "Ap" 

instance Show Constants 
 where show (N x)  = show x
       show (O op) = show op
       show If     = "If "
       
instance Show Operation 
 where show Plus  = "+"
       show Times = "*"
       show Leq   = "<=" 

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

--- Einige Beispiele fuer Lam Ausdruecke
bsp = App fun (Lam 1 (App (App (Con (O Times)) (Var 1)) (Var 1)))
fun = Lam 1 (App (App (Con (O Plus)) (App (Var 1) (Con (N 3)))) 
                                     (App (Var 1) (Con (N 4))))
i = (Lam 1 (Var 1))
k = (Lam 1 (Lam 2 (Var 1)))
s = (Lam 1 (Lam 2 (Lam 3 (App (App (Var 1) (Var 3)) 
                                       (App (Var 2) (Var 3))))))
suc = (Lam 1 (Lam 2 (Lam 3 (App (App (Var 1) (Var 2))
                                         (App (Var 2) (Var 3))
      )         )         )         )
num0 = (Lam 1 (Lam 2 (Var 2)))
num1 = (Lam 4 (Lam 5 (App (Var 4) (Var 5))))