(* An explicitly typed strict first-order functional language. 
   sestoft@dina.kvl.dk 2000-09-20, 2002-02-24

   Does not admit mutually recursive function bindings.

   Every function takes exactly one argument.

   Performs tail recursion in constant space (because Moscow ML does).

   Type checking.  Explicit types on the argument and result of each
   declared function.  Expressions and variables may have type int or
   bool or a functional type.  Functions are monomorphically and
   explicitly typed.  

   There is no lexer or parser specification for this explicitly typed
   language because next week we shall infer types rather than check
   them.  
*)

app load ["Env"];
open Env;

fun int2bool 0 = false
  | int2bool _ = true

fun bool2int false = 0
  | bool2int true  = 1

(* Types:*)

datatype typ =
    TypI                                (* int                         *)
  | TypB                                (* bool                        *)
  | TypF of typ * typ                   (* (argumenttype, resulttype)  *)

(* New abstract syntax with explicit types: *)

datatype tyexpr = 
    CstI of int
  | CstB of bool
  | Var of string
  | Let of string * tyexpr * tyexpr
  | Prim of string * tyexpr list
  | If of tyexpr * tyexpr * tyexpr
  | Letfun of string * string * typ * tyexpr * typ * tyexpr
          (* (f,       x,       xty,  fbody,   rty,  ebody  *)
  | Call of tyexpr * tyexpr

(* Runtime representation of values, as before: *)

datatype value = 
    Int of int
  | RClo of string * string * tyexpr * vfenv  (* (f, x, body, bodyenv) *)
withtype vfenv = (string, value) env

fun eval (e : tyexpr) (env : vfenv) : int =
    case e of 
        CstI i => i
      | CstB b => bool2int b
      | Var x  => (case lookup env x of 
                       Int i => i 
                     | _     => raise Fail "eval Var")
      | Prim(ope, [e1, e2]) => 
            let val i1 = eval e1 env
                val i2 = eval e2 env
            in 
                case ope of
                    "*" => i1 * i2
                  | "+" => i1 + i2
                  | "-" => i1 - i2
                  | "=" => bool2int (i1 = i2)
                  | "<" => bool2int (i1 < i2)
                  | _   => raise Fail "unknown primitive"
            end
      | Let(x, erhs, ebody) => 
            let val xval = eval erhs env
                val env1 = bind1 env (x, Int xval)
            in eval ebody env1 end
      | If(e1, e2, e3) => 
            let val b = eval e1 env
            in
                if int2bool b then eval e2 env else eval e3 env
            end
      | Letfun(f, x, _, fbody, _, ebody) => 
            let val env1 = bind1 env (f, RClo(f, x, fbody, env))
            in eval ebody env1 end
      | Call(Var f, earg) => 
            (case lookup env f of
                 fclosure as RClo (f, x, fbody, env1) =>
                     let val argv = Int(eval earg env)
                         val env2 = bind1 env1 (f, fclosure)
                         val env3 = bind1 env2 (x, argv)
                     in eval fbody env3 end
               | _ => raise Fail "eval Call")
      | Call _ => raise Fail "illegal function in Call"


(* Type checking for the first-order functional language: *)

exception Type of string

type tyenv = (string, typ) env

fun typ (env : tyenv) (e : tyexpr) : typ =
    case e of 
        CstI i => TypI
      | CstB b => TypB
      | Var x  => lookup env x 
      | Prim(ope, [e1, e2]) => 
            let fun chk ta tb tr = 
                    if typ env e1=ta andalso typ env e2=tb then tr 
                    else raise Type "Prim"
            in 
                case ope of
                    "*" => chk TypI TypI TypI
                  | "+" => chk TypI TypI TypI
                  | "-" => chk TypI TypI TypI
                  | "=" => chk TypI TypI TypB
                  | "<" => chk TypI TypI TypB
                  | "&" => chk TypB TypB TypB
                  | _   => raise Fail "unknown primitive"
            end
      | Let(x, erhs, ebody) => 
            let val xty  = typ env erhs
                val env1 = bind1 env (x, xty)
            in 
                typ env1 ebody 
            end
      | If(e1, e2, e3) => 
            (case typ env e1 of
                 TypB => let val e2ty = typ env e2
                             val e3ty = typ env e3
                         in 
                             if e2ty = e3ty then e2ty
                             else raise Type "If: e2 and e3 different types"
                         end
               | _    => raise Type "If: e1 not boolean")
      | Letfun(f, x, xty, fbody, rty, ebody) => 
            let val env1 = bind1 env (f, TypF(xty, rty))
                val env2 = bind1 env1 (x, xty)
            in 
                if typ env2 fbody = rty then typ env1 ebody 
                else raise Type ("Letfun: wrong type given " ^ f)
            end
      | Call(e, earg) => 
            (case typ env e of
                 TypF(xty, fty) =>
                     if typ env earg = xty then fty
                     else raise Type "Call: wrong argument type"
               | _ => raise Type "Call: attempt to apply non-function")

fun tychk e = typ Env.empty e;


(* Examples in abstract syntax *)

val ex1 = Letfun("f1", "x", TypI, Prim("+", [Var "x", CstI 1]), TypI,
                 Call(Var "f1", CstI 12));

(* Factorial *)

val ex2 = Letfun("fac", "x", TypI,
                 If(Prim("=", [Var "x", CstI 0]),
                    CstI 1,
                    Prim("*", [Var "x", 
                               Call(Var "fac", 
                                    Prim("-", [Var "x", CstI 1]))])),
                 TypI,
                 Let("n", CstI 7, Call(Var "fac", Var "n")));

val fac10 = eval ex2 Env.empty;

val ex3 = Let("b", Prim("=", [CstI 1, CstI 2]),
              If(Var "b", CstI 3, CstI 4));

val ex4 = Let("b", Prim("=", [CstI 1, CstI 2]),
              If(Var "b", Var "b", CstB false));

val ex5 = If(Prim("=", [CstI 11, CstI 12]), CstI 111, CstI 666);

val ex6 = Letfun("inf", "x", TypI, Call(Var "inf", Var "x"), TypI,
                 Call(Var "inf", CstI 0));

val types = map tychk [ex1, ex2, ex3, ex4, ex5, ex6];

(* Example type errors: *)

val exerr1 = Let("b", Prim("=", [CstI 1, CstI 2]),
              If(Var "b", Var "b", CstI 6));

val exerr2 = Letfun("f", "x", TypB, If(Var "x", CstI 11, CstI 22), TypI,
                    Call(Var "f", CstI 0));

val exerr3 = Letfun("f", "x", TypB, Call(Var "f", CstI 22), TypI,
                    Call(Var "f", CstB true));