(* Simple imperative language with loops and exceptions
   sestoft@dina.kvl.dk 2001-03-17, 2002-04-02
*)

app load ["Int", "Naivestore"];

open Naivestore;

fun int2bool 0 = false
  | int2bool _ = true

fun bool2int false = 0
  | bool2int true  = 1

(* A store is just a mapping from ints to ints; no lvalue/rvalue distinction *)

type sto = int naivesto

(* A computation may terminate normally or throw an exception: *)

datatype answer =
    Success 
  | Failure of string;

datatype exn = 
    Exn of string

datatype expr = 
   CstI of int
 | Var of string
 | Prim of string * expr list

datatype stmt = 
    Asgn of string * expr
  | If of expr * stmt * stmt
  | Block of stmt list
  | For of string * expr * expr * stmt
  | While of expr * stmt
  | Print of expr
  | Throw of exn
  | TryCatch of stmt * exn * stmt

(* Evaluation of expressions without side effects and exceptions *)

fun eval e (sto : sto) : int =
    case e of 
        CstI i => i
      | Var x  => get sto x
      | Prim(ope, [e1, e2]) =>
            let val i1 = eval e1 sto
                val i2 = eval e2 sto
            in 
                case ope of
                    "*"  => i1 * i2
                  | "+"  => i1 + i2
                  | "-"  => i1 - i2
                  | "==" => bool2int (i1 = i2)
                  | "<"  => bool2int (i1 < i2)
                  | _    => raise Fail "unknown primitive"
            end
      | Prim _ => raise Fail "unknown primitive"

(* This interpreter coExec1 takes the following arguments:

   * A statement stmt to execute.
   * A naive store mapping names to values.
   * A success continuation cont, for normal termination.  By
     discarding the continuation, it can terminate abnormally (when
     executing a Throw statement), but it cannot handle thrown
     exceptions (because it has no error continuation).  
*)

local 
fun coExec1 stmt sto (cont : sto -> answer) : answer =
    case stmt of
        Asgn(x, e) => 
            cont (set sto (x, eval e sto))
      | If(e1, stmt1, stmt2) => 
            if int2bool(eval e1 sto) then 
                coExec1 stmt1 sto cont
            else
                coExec1 stmt2 sto cont
      | Block stmts => 
            let fun loop []       sto = cont sto
                  | loop (s1::sr) sto = coExec1 s1 sto (fn sto => loop sr sto) 
            in loop stmts sto end
      | For(x, estart, estop, body) => 
            let val start = eval estart sto
                val stop  = eval estop  sto
                fun loop i sto = 
                    if i <= stop then
                        coExec1 body (set sto (x, i)) (loop (i+1))
                    else 
                        cont sto
            in loop start sto end
      | While(e, body) => 
            let fun loop sto =
                    if int2bool(eval e sto) then
                        coExec1 body sto loop
                    else
                        cont sto
            in loop sto end
      | Print e => 
            (print (Int.toString (eval e sto)); print "\n"; cont sto)
      | Throw (Exn s) => 
            Failure ("Uncaught exception: " ^ s)
      | TryCatch _ => 
            Failure "TryCatch is not implemented"
in

fun run1 stmt : answer = 
    coExec1 stmt empty (fn sto => Success)
end;


(* This interpreter coExec2 takes the following arguments:

   * A statement stmt to execute.
   * A naive store mapping names to values.
   * A success continuation cont, for normal termination.  By
     discarding the continuation, it can terminate abnormally (when
     executing a Throw statement), but it cannot handle thrown
     exceptions (because it has no error continuation).  
   * An error continuation econt for abnormal termination.  The error
     continuation receives the exception and the store, and decides
     whether it wants to handle the exception or not.  In the former
     case it executes the handler's statement body; in the latter case
     it re-raises the exception, by applying the handler's own error
     continuation.  
*)

local 

fun coExec2 stmt sto 
         (cont : sto -> answer) (econt : exn * sto -> answer) : answer =
    case stmt of
        Asgn(x, e) => 
            cont (set sto (x, eval e sto))
      | If(e1, stmt1, stmt2) => 
            if int2bool(eval e1 sto) then 
                coExec2 stmt1 sto cont econt
            else
                coExec2 stmt2 sto cont econt
      | Block stmts => 
            let fun loop []       sto = cont sto
                  | loop (s1::sr) sto = coExec2 s1 sto (loop sr) econt
            in loop stmts sto end
      | For(x, estart, estop, stmt) => 
            let val start = eval estart sto
                val stop  = eval estop  sto
                fun loop i sto = 
                    if i <= stop then
                        coExec2 stmt (set sto (x, i)) (loop (i+1)) econt
                    else 
                        cont sto
            in loop start sto end
      | While(e, stmt) => 
            let fun loop sto =
                    if int2bool(eval e sto) then
                        coExec2 stmt sto loop econt
                    else
                        cont sto
            in loop sto end
      | Print e => 
            (print (Int.toString (eval e sto)); print "\n"; cont sto)
      | Throw exn => 
            econt(exn, sto)
      | TryCatch(stmt1, exn, stmt2) =>
            let fun econt1 (exn1, sto1) =
                    if exn1 = exn then coExec2 stmt2 sto1 cont econt
                                  else econt (exn1, sto1)
            in coExec2 stmt1 sto cont econt1 end
in 

fun run2 stmt : answer = 
    coExec2 stmt empty 
          (fn sto => Success) 
          (fn (Exn s, sto) => Failure ("Uncaught exception: " ^ s))
end;


(* Example programs *)

(* Abruptly terminating a for loop *)

val ex1 = 
    For("i", CstI 0, CstI 10,
        If(Prim("==", [Var "i", CstI 7]),
           Throw (Exn "seven"),
           Print (Var "i")));

(* Abruptly terminating a while loop *)

val ex2 = 
    Block[Asgn("i", CstI 0),
          While (CstI 1,
                 Block[Asgn("i", Prim("+", [Var "i", CstI 1])),
                       Print (Var "i"),
                       If(Prim("==", [Var "i", CstI 7]),
                          Throw (Exn "seven"),
                          Block [])]),
          Print (CstI 333333)];

(* Abruptly terminating a while loop, and handling the exception *)

val ex3 = 
    Block[Asgn("i", CstI 0),
          TryCatch(Block[While (CstI 1,
                                Block[Asgn("i", Prim("+", [Var "i", CstI 1])),
                                      Print (Var "i"),
                                      If(Prim("==", [Var "i", CstI 7]),
                                         Throw (Exn "seven"),
                                         Block [])]),
                         Print (CstI 111111)],
                   Exn "seven", 
		   Print (CstI 222222)),
          Print (CstI 333333)];