(* Abstract Syntax *)

datatype con = False | True | IC of int
type     id  = string

datatype ops = Add | Sub | Mul | Leq

datatype ty  = Bool | Int | Arrow of ty * ty

datatype exp = Con of con
             | Id  of id
             | Op  of exp * ops * exp
	     | If  of exp * exp * exp
	     | Abs of id  * ty  * exp
	     | App of exp * exp

(* Error Messages *)

exception Error of string

(* Environments *)

signature Env = 
  sig
    type 'a env
    exception Unbound of id
    val empty  : 'a env
    val insert : id * 'a * 'a env -> 'a env
    val lookup : id * 'a env -> 'a  (* Unbound *)
  end

structure Env :> Env =
  struct
    type 'a env = (id * 'a) list

    exception Unbound of id

    val empty = nil

    fun insert (x, a, nil         ) = [(x,a)]
      | insert (x, a, (x',a')::env) = if x=x' then (x,a)::env
				      else (x',a') :: insert(x,a,env)

    fun lookup (x, nil        ) = raise Unbound x
      | lookup (x, (x',a)::env) = if x=x' then a else lookup(x,env)
  end

open Env

(* Elaboration *)

fun elabCon True   = Bool
  | elabCon False  = Bool
  | elabCon (IC _) = Int

fun elabOp Int Add Int = Int
  | elabOp Int Sub Int = Int
  | elabOp Int Mul Int = Int
  | elabOp Int Leq Int = Bool
  | elabOp _   _   _   = raise Error "ill-typed operation"

fun elab T (Con c)         = elabCon c
  | elab T (Id  s)         = lookup(s,T)
  | elab T (Op(e1,ops,e2)) = elabOp (elab T e1) ops (elab T e2)
  | elab T (If(e1,e2,e3))  = let val t1 = elab T e1
				 val t2 = elab T e2
				 val t3 = elab T e3
			     in  if t1=Bool andalso t2=t3 then t2
				 else raise Error "ill-typed conditional"
			     end
  | elab T (App(e1,e2))    = let val t1 = elab T e1
				 val t2 = elab T e2
				 val s  = "ill-typed application"
			     in  case t1 of
			           Arrow(t,t') => if t=t2 then t'
						  else raise Error s
				 | _           => raise Error s
			     end
  | elab T (Abs(s,t,e))    = Arrow(t, elab (insert(s,t,T)) e)

(* Evaluation *)

datatype value = IV    of int
               | Proc  of id * exp * value env

fun evalCon False  = IV 0
  | evalCon True   = IV 1
  | evalCon (IC x) = IV x

fun evalOp (IV x1) Add (IV x2) = IV(x1+x2)
  | evalOp (IV x1) Sub (IV x2) = IV(x1-x2)
  | evalOp (IV x1) Mul (IV x2) = IV(x1*x2)
  | evalOp (IV x1) Leq (IV x2) = IV(if x1<=x2 then 1 else 0)
  | evalOp  _      _   _       = raise Error "Impossible"

fun eval V (Con c)         = evalCon c
  | eval V (Id  s)         = lookup(s,V)
  | eval V (Op(e1,ops,e2)) = evalOp (eval V e1) ops (eval V e2)
  | eval V (If(e1,e2,e3))  = (case eval V e1 of
				IV 1 => eval V e2 
			      | IV 0 => eval V e3 
			      |  _   => raise Error "Impossible")
  | eval V (Abs(s,t,e))    = Proc(s,e,V)
  | eval V (App(e1,e2))    = (case (eval V e1, eval V e2) of
				(Proc(s,e,V'), v) => 
				  eval (insert(s,v,V')) e
			      | _ => raise Error "Impossible")