-- syntax of While

type Var = String

data AExpr = Var Var | Num Integer 
          | AExpr :+ AExpr | AExpr :- AExpr | AExpr :* AExpr

data BExpr = T | F | AExpr :== AExpr | AExpr :<= AExpr 
          | Not BExpr | BExpr :&& BExpr | BExpr :|| BExpr 

data Stm  = Var ::= AExpr | Skip | Stm :\ Stm 
          | If BExpr Stm Stm | While BExpr Stm



-- semantic categories for denotational semantics

{-
type Store = Var -> Integer

empty :: Store
empty x = error ("variable " ++ x ++ " has no value")
-- empty x = undefined

lkp :: Var -> Store -> Integer
lkp x st = st x

upd :: Var -> Integer -> Store -> Store
upd x n st = st' where
                 st' x' | x' == x   = n
                        | otherwise = st x'
-}

type Store = [(Var, Integer)]

empty :: Store
empty = []

lkp :: Var -> Store -> Integer
lkp x [] = undefined
lkp x ((x',n) : st) = if x' == x then n else lkp x st

upd :: Var -> Integer -> Store -> Store
upd x n [] = [(x, n)]
upd x n ((x', m) : st) = if x' == x then (x', n) : st else (x', m) : upd x n st 



-- syntax of AM

data Inst = Push Integer | Add | Mult | Sub | TT | FF | EQ | LE | And | Neg
          | Fetch Var | Store Var | Branch Code Code | Loop Code 
          deriving (Eq, Show)

data Value = I Integer | B Bool
          
instance Show Value where
  --show  :: Value -> String
  show (I n) = show n
  show (B b) = show b

type Code = [Inst]

type Stack = [Value]

type Conf = (Code, Stack, Store)

-- operation of AM

trans :: Conf -> Conf
trans (Push n : c, vs, st) = (c, I n : vs, st)
trans (Add : c, I n1 : I n2 : vs, st) = (c, I (n2 + n1) : vs, st)
trans (Mult : c, I n1 : I n2 : vs, st) = (c, I (n2 * n1) : vs, st)
trans (Sub : c, I n1 : I n2 : vs, st) = (c, I (n2 - n1) : vs, st)
trans (TT : c, vs, st) = (c, B True : vs, st)
trans (FF : c, vs, st) = (c, B False : vs, st)
trans (EQ : c, I n1 : I n2 : vs, st) = (c, B (n2 == n1) : vs, st)
trans (LE : c, I n1 : I n2 : vs, st) = (c, B (n2 <= n1) : vs, st)
trans (And : c, B b1 : B b2 : vs, st) = (c, B (b2 && b1) : vs, st)
trans (Neg : c, B b : vs, st) = (c, B (not b) : vs, st)
trans (Fetch x : c, vs, st) = (c, I (lkp x st) : vs, st)
trans (Store x : c, I n : vs, st) = (c, vs, upd x n st)
trans (Branch c1 c2 : c, B True  : vs, st) = (c1 ++ c, vs, st)
trans (Branch c1 c2 : c, B False : vs, st) = (c2 ++ c, vs, st)
trans (Loop cc : c, vs, st) = (Branch (cc ++ [Loop cc]) [] : c, vs, st)

{-
run :: Conf -> Conf
run conf = case conf of 
                ([], _, _)    -> conf 
                (_ : _, _, _) -> run (trans conf)
-}

run :: Conf -> IO Conf
run conf = do printconf conf
              case conf of 
                ([], _, _)    -> return conf 
                (_ : _, _, _) -> run (trans conf)

printconf :: Conf -> IO () 
printconf (c, vs, st) = do print vs
                           print st
                           if c == [] then putStrLn "done" else print (head c)

-- compilation

compA :: AExpr -> Code
compA (Var x) = [Fetch x]
compA (Num n) = [Push n]
compA (a1 :+ a2) = compA a1 ++ compA a2 ++ [Add]
compA (a1 :* a2) = compA a1 ++ compA a2 ++ [Mult]
compA (a1 :- a2) = compA a1 ++ compA a2 ++ [Sub]


compB :: BExpr -> Code
compB T = [TT]
compB F = [FF]
compB (a1 :== a2) = compA a1 ++ compA a2 ++ [EQ]
compB (a1 :<= a2) = compA a1 ++ compA a2 ++ [LE]
compB (b1 :&& b2) = compB b1 ++ compB b2 ++ [And]
compB (Not b) = compB b ++ [Neg]


compS :: Stm -> Code
compS (x ::= a) = compA a ++ [Store x]
compS Skip = []
compS (s1 :\ s2) = compS s1 ++ compS s2
compS (If b s1 s2) = compB b ++ [Branch (compS s1) (compS s2)]
compS (While b s) = compB b ++ [Loop (compS s ++ compB b)]


fact :: Stm
fact =     ("y" ::= Num 1) :\
           (While (Not (Var "x" :== Num 1))
                  (("y" ::= (Var "y" :* Var "x")) :\
                   ("x" ::= (Var "x" :- Num 1))
                  )
           )

{-
testfact :: Integer -> (Integer, Integer)
testfact n =  case run (compS fact, [], upd "x" n empty) of
                 (_, _, st) -> (lkp "x" st, lkp "y" st)
-}

testfact :: Integer -> IO ()
testfact n = do run (compS fact, [], upd "x" n empty)
                return ()



-- a more realistic abstract machine AM'

{-
type Label = Integer

data Inst' = Push' Integer | Add' | Mult' | Sub' | TT' | FF' 
          | EQ' | LE' | And' | Neg'
          | Fetch' Var | Store' Var | JumpF Label | Jump Label
          deriving (Eq, Show)

type Code' = [(Label, Inst')]
-}


-- write trans, run for AM'

-- write a converter from AM code to AM' code