-- Implementierung der Stackmachine für rekursive Programme
-- VLFP 2006
--
-- Jost Berthold, FB12, Philipps-Universität Marburg
---------------------------------------------------------

import Data.List
import Data.Maybe

-- Maschinenbefehle
data Instr = Jmp [Int]
	   | Jmc [Int]
	   | Load Int
	   | Exec BaseVal
	   | Create Int [Int]
	   | Ret
	   | Noop -- no operation
	     deriving (Eq,Show)

      -- omega, erweiterbar nach Bedarf
data BaseVal = N Int | B Bool
	     | Q Double
	     | Plus | Minus | Times | Div -- arithmetisch (Int)
	     | LessEq               -- Zahl -> boolean
	     | And | Or | Not       -- boolesch
	     | If                   -- built-in conditional
    deriving (Eq,Show) 

----------------------------------------------

-- Maschinenzustand
--    Kellerspitze jeweils links!
--    auf DK und FK befinden sich nur (N Int) und (B Bool)!
--    (natürliche Zahlen auf FK werden als N <zahl> codiert)
type MachState = (Int , [BaseVal], [BaseVal])

-- Semantik der Basisoperationen, liefert Resultat-DK zurück
doOp :: BaseVal -> [BaseVal] -> [BaseVal]
doOp (N n) dk = (N n):dk
doOp (B b) dk = (B b):dk
doOp (Q b) dk = (Q b):dk
-- Q
doOp Plus  ((Q k):(Q l):rest) = Q (k+l):rest
doOp Minus ((Q k):(Q l):rest) = Q (l-k):rest
doOp Times ((Q k):(Q l):rest) = Q (k*l):rest
doOp Div   ((Q k):(Q l):rest) = Q (l / k):rest
doOp LessEq ((Q k):(Q l):rest) = B (l<=k):rest
-- N
doOp Plus  ((N k):(N l):rest) = N (k+l):rest
doOp Minus ((N k):(N l):rest) = N (l-k):rest
doOp Times ((N k):(N l):rest) = N (k*l):rest
doOp Div   ((N k):(N l):rest) = Q (fromIntegral l / fromIntegral k):rest
doOp LessEq ((N k):(N l):rest) = B (l<=k):rest

-- typecasts
doOp Plus  ((Q k):(N l):rest) = Q (k+fromIntegral l):rest
doOp Plus  ((N l):(Q k):rest) = Q (k+fromIntegral l):rest
doOp Minus ((N k):(Q l):rest) = Q (l-fromIntegral k):rest
doOp Minus ((Q k):(N l):rest) = Q (fromIntegral l - k):rest
doOp Times ((Q k):(N l):rest) = Q (k*fromIntegral l):rest
doOp Times ((N l):(Q k):rest) = Q (k*fromIntegral l):rest
doOp Div   ((N k):(Q l):rest) = Q (l / fromIntegral k):rest
doOp Div   ((Q k):(N l):rest) = Q (fromIntegral l / k):rest
doOp LessEq ((Q k):(N l):rest) = B (fromIntegral l <= k):rest
doOp LessEq ((N k):(Q l):rest) = B (l <= fromIntegral k):rest

-- Bool
doOp And ((B x):(B y):rest) = B (x && y):rest
doOp Or  ((B x):(B y):rest) = B (x || y):rest
doOp Not ((B x):rest) = B (not x):rest
doOp If ((B x):a1:a2:rest) = (if x then a1 else a2):rest

doOp op dk = error ("Operation " ++ show op 
		      ++ " undefiniert mit DK " 
		      ++ shownDK ++ "...")
    where shownDK = unwords $ map show $ take 3 dk

-- Semantik der Maschinenbefehle
exec :: Instr -> MachState -> MachState 
exec (Jmp [n]) (_,d,fk) = (n,d,fk)
exec (Jmc [n]) (m,(B b):d,fk) | not b = (n,d,fk)
			     | b     = (m+1,d,fk)
exec (Load k) (m,d,fk)  | 1 <= k && k < 1+ length fk 
        = (m+1,(fk!!(k+1)):d,fk)
exec (Exec op) (m,d,fk) = (m+1,doOp op d, fk)
exec (Create k [r]) (m,d,fk) | length d >= k 
	= (m+1, drop k d, (N r):(N (k+1)):(take k d) ++ fk)
exec Ret (m,d,((N ra):(N dl):fk)) = (ra, d, drop (dl-1) fk)
exec Noop (m,d,fk) = (m+1,d,fk) 
exec instr state = error ( "Befehl " ++ show instr 
			   ++ "undefiniert  im Zustand " 
			   ++ show state)

-----------------------------------------------
-- Programme:
type SCTree = [([Int],Instr)]  --  Baum-artige Adressen
type SC     = [Instr]          --  Lineare Adressen (Instr.sequenz)

-- Programmsemantik: single step
ea :: SC -> MachState -> MachState
ea is state@(m,_,_) | 1 <= m && m <= length is = exec (is!!(m-1)) state
		    | otherwise = state

-- Programmsemantik: iteration
ia is state@(m,_,_) | m == 0    = state
		    | otherwise = ia is (ea is state)

iaTrace :: SC -> MachState -> [MachState]
iaTrace is = (takeWhile (not . isStopState)) . (iterate (ea is))
    where isStopState (m,_,_) = m == 0

input :: [Int] -> MachState
input inNums = (1,[],N 0:N (1+length inNums):map N inNums)

output :: MachState -> [String]
output (0,dk,[]) =  map fromB dk
    where fromB (N k) = show k
	  fromB (Q q) = show q
	  fromB  x    = error ("fromB: unerwarteter Wert " 
				  ++ show x)
output state = error ("output: Zustand " ++ show state)

run :: SC -> [Int] -> [String]
run prog ins = output (ia prog (input ins))

trace :: SC -> [Int] -> ([MachState],[String])
trace prog ins = (states, output (ea prog  (last states)))
    where states = iaTrace prog (input ins)

-----------------------------------------------

-- F x = if 1 <= x then x-1 else F (F (x+2))
example :: [([Int],Instr)]
example =  ([1],Exec (N 1)):
	   ([] , Load 1):
	   ([] , Exec LessEq):
	   ([] , Jmc [3,1]):
	   ([] , Load 1):
	   ([] , Exec (N 1)):
	   ([] , Exec Minus):
	   ([] , Jmp [4,1]):
	   ([3,1] , Load 1):
	   ([] , Exec (N 2)):
	   ([] , Exec Plus):
	   ([] , Create 1 [0,1,3,1]):
	   ([] , Jmp [1]):
	   ([0,1,3,1], Create 1 [0,3,1]):
	   ([0,3,1]  , Noop):
	   ([1,4]    , Noop):
	   ([] , Ret):
	   []
	   
-- pretty printer für Maschinenprogramme
ppProgT :: SCTree -> String
ppProgT p = unlines (map (ppInstT indent) p)
    where indent = 1+ 2 * maximum (map (length . fst) p)
ppInstT :: Int -> ([Int],Instr) -> String
ppInstT indent (lb,i) = (replicate (indent - length showLb) ' ')
			++ showLb ++ show i
    where showLb = tail ((concatMap (('.':) . show) lb) ++ ": ")
		   
ppProg :: SC -> String
ppProg is = unlines (zipWith (\n i -> show n ++ ":\t" ++ show i) [1..] is)

-- conversion to std. addresses:
convert :: SCTree -> SC
convert ts = error "Schreib mich!"

------------------------------------------------

-- rekursive Programme:
data Program = Rek [(Int,Expr)] -- Stelligkeit der F für pretty-printer angeben
data Expr = Var Int
	  | F Int [Expr] -- Int = Index von F im zugeh.GlS
          | Con BaseVal [Expr]
        deriving Eq

instance Show Expr where 
    show (Var i) = "x_" ++ show i
    show (F i args) = "F_" ++ show i ++ "("
		      ++ arglist
		      ++ ") "
	where arglist = drop 2 (concatMap (\e -> ", "++ show e) args)
    show (Con (N b) []   ) = show b
    show (Con (B b) []   ) = show b
-- waere schoener mit pattern match passend zu Funktionen in BaseVal
    show (Con b args ) = show b ++ "(" ++ arglist ++ ")"
	where arglist = drop 2 (concatMap (\e -> ", "++ show e) args)

instance Show Program where
    show (Rek defs) = unlines (zipWith showF [1..] defs)

showF :: Int -> (Int,Expr) -> String
showF k (args,expr) = "F"++ show k 
		      ++ varString  ++ " = "
		      ++ show expr
    where varString = concatMap (\i -> " x_"++ show i) [1..args]

------------------------------------

-- Übersetzung
transConv :: Program -> SC
transConv = convert . trans

trans :: Program -> SCTree
trans (Rek defs) = concatMap
			 ( (++ [([],Ret)]) . uncurry exptrans)
		         (zip (map snd defs) (map (:[]) [1..]))

exptrans :: Expr -> [Int] -> SCTree
exptrans (Var i)      l = [(l,Load i)]
exptrans (Con b [])   l = [(l,Exec b)]
exptrans (Con b args) l = (l,Noop):
			  concatMap (uncurry exptrans) 
			            (zip  args (map (:l) [1..]) )
			  ++ [([],Exec b)]
exptrans (Con If [e,e1,e2]) l = (l,Noop):
				exptrans e (1:l)
				++ ([],Jmc (3:l)):
				   exptrans e1 (2:l)
				++ ([],Jmp (4:l)):
				   (3:l,Noop):
				   exptrans e2 (3:l)
				++ [(4:l,Noop)] -- jump target only
exptrans (F j args)   l = (l,Noop):
			  concatMap (uncurry exptrans) 
			            (zip args (map (:l) [1..j])  )
			  ++ ([],Create j (0:l)):
			     ([],Jmp [j]):
			    [(0:l,Noop)]

exF :: Program 
exF = Rek -- F x = if 1 <= x then x-1 else F (F (x+2))
      [(1, Con If [Con LessEq [Con (N 1) [],Var 1]
		   , Con Minus [Var 1,Con (N 1) []]
		   , F 1 [F 1 [Con Minus [Var 1, Con (N 2) []]]]]
       )]
       

{-
  F x_1 = G x_1 x_1 (A 0 x_1)
  G x_1 x_2 x_3 = if (x_2 - x_3 < 0.001) 
                    then x_3 
		    else G x_1 x_3 (A x_1 x_3))
  A x_1 x_2 = (x_2 + x_1/x_2) / 2
-}
ex2 :: Program
ex2 = Rek
      [ -- F
	(1,F 2 [Var 1,Var 1, F 3 [Con (N 0) [], Var 1]])
	-- G
       ,(3, Con If [Con LessEq [Con Minus [Var 2,Var 3],Con (Q 0.001 ) []]
                   ,Var 3
                   ,F 2 [Var 1, Var 3, F 3 [Var 1,Var 3]] 
		   ])
	-- A
       ,(2, Con Div [Con Plus [Var 2
			       , Con Div [Var 1,Var 2]]
		     ,Con (N 2) []]) 
      ]