module Main where
import Char

-- Syntax

type Var = String

data N  =  Nzero | Nsucc N | Nvar Var
data B  =  Btrue | Bnot B | Blt N N
data C  =  Cskip | Cseq C C | Cfor N C | Cif B C C | Cwhile B C | Cassign Var N

-- Pretty-printing

instance Show N where
  showsPrec p Nzero = ("0" ++)
  showsPrec p (Nsucc n) = ("succ " ++) . showsPrec p n
  showsPrec p (Nvar x) = (x ++)

instance Show B where
  showsPrec p Btrue = ("true" ++)
  showsPrec p (Bnot b) = ("not " ++) . showsPrec p b
  showsPrec p (Blt n1 n2) = showsPrec p n1 . (" < " ++) . showsPrec p n2

instance Show C where
  showsPrec p Cskip = ("skip" ++)
  showsPrec p (Cseq c1 c2) =
    showParen (p > 0) (showsPrec 1 c1 . ("; " ++) . showsPrec 0 c2)
  showsPrec p (Cfor n c) =
    ("for " ++) . showsPrec p n . (" do " ++) . showsPrec 1 c
  showsPrec p (Cif b c1 c2) =
    ("if " ++) . showsPrec p b . (" then " ++) . showsPrec 1 c1 .
                                 (" else " ++) . showsPrec 1 c2
  showsPrec p (Cwhile b c) =
    ("while " ++) . showsPrec p b . (" do " ++) . showsPrec 1 c
  showsPrec p (Cassign x n) = (x ++) . (" := " ++) . showsPrec p n

-- Parsing

isVar x = all isAlpha x && not (x `elem` keywords)
  where keywords = ["zero", "succ", "true", "not", "skip",
                    "for", "if", "then", "else", "while", "do"]

instance Read N where
  readsPrec p s =
    [(Nzero, r)    |  ("0", r) <- lex s ] ++
    [(Nsucc n, r)  |  ("succ", t) <- lex s, (n, r) <- readsPrec p t ] ++
    [(Nvar x, r)   |  (x, r) <- lex s, isVar x ]

instance Read B where
  readsPrec p s =
    [(Btrue, r)     |  ("true", r) <- lex s ] ++
    [(Bnot b, r)    |  ("not", t) <- lex s, (b, r) <- readsPrec p t ] ++
    [(Blt n1 n2, r) |  (n1, t) <- readsPrec p s, ("<", t') <- lex t, (n2, r) <- readsPrec p t' ]

instance Read C where
  readsPrec p s = take 1 $
    [(Cseq c1 c2, r)  |  (c1, t) <- readsPrecHelp 1 s, (";", t') <- lex t, (c2, r) <- readsPrec 0 t' ] ++
    readsPrecHelp p s
; readsPrecHelp p s =
    [(Cskip, r)       |  ("skip", r) <- lex s] ++
    [(Cfor n c, r)    |  ("for", t) <- lex s, (n, t') <- readsPrec p t,
                         ("do", t'') <- lex t', (c, r) <- readsPrec 1 t'' ] ++
    [(Cif b c1 c2, r) |  ("if", t) <- lex s, (b, t') <-readsPrec p t, ("then", t'') <- lex t',
                         (c1, t''') <- readsPrec 1 t'', ("else", t'''') <- lex t''', (c2, r) <- readsPrec 1 t'''' ] ++
    [(Cwhile b c, r)  |  ("while", t) <- lex s, (b, t') <- readsPrec p t,
                         ("do", t'') <- lex t', (c, r) <- readsPrec 1 t'' ] ++
    [(Cassign x n, r) |  (x, t) <- lex s, isVar x, (":=", t') <- lex t, (n, r) <- readsPrec 1 t' ] ++
    [(c, r)           |  ("(", t) <- lex s, (c, t'') <- readsPrec p t, (")", r) <- lex t'' ]

-- Fixed point combinator
fix f = f (fix f)

-- Semantics

type S = Var -> Int
initial x = error ("uninitialized variable: " ++ x)

semN Nzero s = 0
semN (Nsucc n) s = semN n s + 1
semN (Nvar x) s = s x


semB Btrue s = True
semB (Bnot b) s = not ((semB b) s) 
semB (Blt n1 n2) s = if ( (semN n1) s) < ((semN n2) s ) then True else False


semC Cskip s = s
semC (Cseq c1 c2) s = semC c2 (semC c1 s)
semC (Cfor n c) s = compose (semN n s) (semC c) s
  where compose 0 f = id
        compose (n+1) f = f . compose n f
semC (Cassign x n) s = update s x (semN n s)
  where update f x y = f'
          where f' z = if z == x then y else f z
semC (Cif b c1 c2) s = if ((semB b) s) == True then ((semC c1) s) else ((semC c2) s)
semC (Cwhile b c) s = fix fb s
  where fb f s = if (semB b) s == True then f ((semC c) s) else s

-- Main function: interpreter

main = do  input <- getContents
           let c = (read input)::C
           let s = semC c initial
           -- I'm assuming that every program must calculate a value
           -- in the special variable "result"
           putStr "result = "
           print (s "result")