(* Carsten Schuermann *)
(* Machine code simulator *)

let 
  type address = int
  type register = int

  datatype Inst				(* Instructions *)
    = Load of address * register
    | LoadI of register * register
    | Move of register * register
    | Store of register * address
    | Add of register * register 
    | Mult of register * register
    | Const of Content * register
    | Jmp of address
    | Cjmp of address
    | Out of register
    | Halt 

  and Content				(* Content *)
    = Free
    | Inst of Inst
    | Int of int
    | Real of real

  type memory = address -> Content	(* Memory *)

  datatype Prog				(* Programs *)
    = Empty 
    | Address of (address -> Prog)
    | Cons of Inst * Prog


  fun empty a = Free
  fun update m a v = fn x => if x = a then v else m x
  fun lookup m a = m a

  fun instToString (Load (a, i))  = 
        "LOAD  " ^ (Int.toString a) ^ " " ^ (Int.toString i)  
    | instToString (LoadI (i, j))  = 
	"LOADI " ^ (Int.toString i) ^ " " ^ (Int.toString j)  
    | instToString (Move (i, j))  = 
	"MOVE  " ^ (Int.toString i) ^ " " ^ (Int.toString j) 
    | instToString (Store (i, a)) = 
	"STORE " ^ (Int.toString i) ^ " " ^ (Int.toString a)
    | instToString (Add (i, j))   = 
	"ADD   " ^ (Int.toString i) ^ " " ^ (Int.toString j)
    | instToString (Mult (i, j))  = 
	"MULT  " ^ (Int.toString i) ^ " " ^ (Int.toString j)
    | instToString (Const (c, i)) = 
	"CONST " ^ (contentToString c) ^ " " ^ (Int.toString i)
    | instToString (Jmp a)        = 
	"JMP   " ^ (Int.toString a) 
    | instToString (Cjmp a)       = 
	"CJMP  " ^ (Int.toString a) 
    | instToString (Out a)        = 
	"OUT   " ^ (Int.toString a) 
    | instToString (Halt)         = 
	"HALT  "
	
  and contentToString (Inst I)   = instToString I
    | contentToString (Int i)    = Int.toString i
    | contentToString (Real x)   = Real.toString x
    | contentToString (Free)     = "*"

  fun inspect m (n1, n2) = 
      if n1 > n2 then ()
      else (print (Int.toString n1);
	  print "  ";
	    print (contentToString (m n1));
	    print "\n";
	    inspect m (n1+1, n2))
	
	

  (* load a m P = m'

     Invariant:
     m' results from 
     loading program P 
     into memory m
     starting at address a
     *)
  fun load a m Empty = m
    | load a m (Address P) =
        load a m (P a)
    | load a m (Cons (I, P)) =
	load (a+1) (update m a (Inst I)) P

  (* mult C1 C2 = C'

     Invariant:
     C' is the result of multiplying Content C1 and C2.
  *)
  fun mult (Int i)  (Int j)  = Int (i*j)
    | mult (Real x) (Real y) = Real (x*y)

  (* add C1 C2 = C'

     Invariant:
     C' is the result of adding Content C1 and C2.
     *)
  fun add (Int i)  (Int j)  = Int (i+j)
    | add (Real x) (Real y) = Real (x+y)
    
  (* isZero C = B

     Invariant:
     B holds iff Content C is zero.
  *)
  fun isZero (Int i) = (i=0)


  (* initreg () = Rb
 
     Invariant:
     Rb is an initialized and empty register bank 
  *)
  fun initreg () = (Free, Free, Free, Free, Free, Free)

  (* getreg i Rb = Ci
 
     Invariant:
     Ci is the content of register Ri in bank Rb.
  *)
  fun getreg 0 (C0, C1, C2, C3, C4, C5) = C0
    | getreg 1 (C0, C1, C2, C3, C4, C5) = C1
    | getreg 2 (C0, C1, C2, C3, C4, C5) = C2
    | getreg 3 (C0, C1, C2, C3, C4, C5) = C3
    | getreg 4 (C0, C1, C2, C3, C4, C5) = C4
    | getreg 5 (C0, C1, C2, C3, C4, C5) = C5

  (* setreg i C Rb = Rb'
 
     Invariant:
     Rb' is the registerbank on obtains
     by updateing Ri in Rb by C
  *)
  fun setreg 0 C (C0, C1, C2, C3, C4, C5) = 
      ( C, C1, C2, C3, C4, C5)
    | setreg 1 C (C0, C1, C2, C3, C4, C5) = 
      (C0,  C, C2, C3, C4, C5)
    | setreg 2 C (C0, C1, C2, C3, C4, C5) = 
      (C0, C1,  C, C3, C4, C5)
    | setreg 3 C (C0, C1, C2, C3, C4, C5) = 
      (C0, C1, C2,  C, C4, C5)
    | setreg 4 C (C0, C1, C2, C3, C4, C5) = 
      (C0, C1, C2, C3,  C, C5)
    | setreg 5 C (C0, C1, C2, C3, C4, C5) = 
      (C0, C1, C2, C3, C4,  C)
      
  (* run (pc, m, r) = ()

     Invariant:
     If  pc is a the program counter (an address)
     and m is a memory
     and r is a register bank
     then run evalutates the machine program stored in 
        m at address pc
   
     Comment:  The only observable side effects of 
             a machine program is the screen output.
  *)
  fun run (pc, m, r) = run' (m pc) (pc, m, r)
  and run' (Inst (Load (a', i))) (pc, m, r) =
        run (pc+1, m, setreg i (m a') r) 
    | run' (Inst (LoadI (i, j))) (pc, m, r) =
      let 
	val (Int a') =  getreg i r
      in
	run (pc+1, m, setreg j (m a') r) 
      end
    | run' (Inst (Move (i, j))) (pc, m, r) =
      run (pc+1, m, setreg j (getreg i r) r) 
    | run' (Inst (Store (a', 0))) (pc, m, r) =
      run (pc+1, update m a' (getreg 0 r), r)
    | run' (Inst (Add (i, j))) (pc, m, r) =
      run (pc+1, m, setreg 0 (add (getreg i r) (getreg j r)) r)
    | run' (Inst (Mult (i, j))) (pc, m, r) =
      run (pc+1, m, setreg 0 (mult (getreg i r) (getreg j r)) r)
    | run' (Inst (Const (c, i))) (pc, m, r) =
      run (pc+1, m, setreg i c r)
    | run' (Inst (Jmp a')) (pc, m, r) =
      run (a', m, r)
    | run' (Inst (Cjmp a')) (pc, m, r) =
      if isZero (getreg 0 r) then run (a', m, r)
      else run (pc+1, m, r)
    | run' (Inst (Out i)) (pc, m, r) =
      (print (contentToString (getreg i r)  ^ "\n");
       run (pc+1, m, r))
    | run' (Inst (Halt)) (pc, m, r) = ()
      

   (* An example:  The computation of the factorial function *)

  val prog = 
    Address (fn a1 => 
    Cons (Const (Int 5, 0),    (* Init *)
    Cons (Move  (0, 3),
    Cons (Move  (0, 2),
    Cons (Const (Int ~1, 1),   (* Predecessor *)
    Cons (Add   (2, 1),
    Cons (Move  (0, 2),
    Cons (Cjmp  (a1+10),
    Cons (Mult  (0, 3),
    Cons (Move  (0, 3),
    Cons (Jmp   (a1+4),
    Cons (Out 3,
    Cons (Halt, 
    Empty)))))))))))))


  val mem = load 100 empty prog
in
  run (100, mem, initreg ())
end