(* Abstrakte Syntax von F (Typdeklarationen) *)

datatype con = False | True | IC of int     (* constants *) 
type     id  = string                       (* identifiers *)
datatype opr = Add | Sub | Mul | Leq        (* operators *)

datatype ty  =                              (* types *)
    Bool 
  | Int 
  | Arrow of ty * ty                        (* procedure type *)

datatype exp =                              (* expressions *)
    Con of con                              (* constant *)
  | Id  of id                               (* identifier *)
  | Opr of opr * exp * exp                  (* operator application *)
  | If  of exp * exp * exp                  (* conditional *)
  | Abs of id  * ty  * exp                  (* abstraction *)
  | App of exp * exp                        (* procedure application *)



(* Implementierung der statischen Semantik von F *)

type 'a env = id -> 'a  (* environments *)
exception Unbound of id

fun empty x = raise Unbound x
fun update env x a y = if y=x then a else env y

exception Error of string

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

fun elabOpr Add Int Int = Int
  | elabOpr Sub Int Int = Int
  | elabOpr Mul Int Int = Int
  | elabOpr Leq Int Int = Bool
  | elabOpr _   _   _   = raise Error "T Opr"

fun elab f (Con c) = elabCon c
  | elab f (Id x) = f x 
  | elab f (Opr(opr,e1,e2)) = elabOpr opr (elab f e1) (elab f e2)
  | elab f (If(e1,e2,e3)) = 
              (case (elab f e1, elab f e2, elab f e3) of  
                 (Bool, t2, t3) => if t2=t3 then t2 
                                   else raise Error "T If1"
               |  _ => raise Error "T If2")
  | elab f (Abs(x,t,e)) = Arrow(t, elab (update f x t) e)
  | elab f (App(e1,e2)) = (case elab f e1 of
                 Arrow(t,t') => if t = elab f e2 then t' 
                                else raise Error "T App1"
               | _  => raise Error "T App2")


(* Implementierung der dynamischen Semantik von F *)

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 evalOpr Add (IV x1) (IV x2) = IV(x1+x2)
  | evalOpr Sub (IV x1) (IV x2) = IV(x1-x2)
  | evalOpr Mul (IV x1) (IV x2) = IV(x1*x2)
  | evalOpr Leq (IV x1) (IV x2) = IV(if x1<=x2 then 1 else 0)
  | evalOpr  _      _   _       = raise Error "R Opr"

fun eval f (Con c) = evalCon c
  | eval f (Id x) = f x
  | eval f (Opr(opr,e1,e2)) = evalOpr opr (eval f e1) (eval f e2)
  | eval f (If(e1,e2,e3)) = (case eval f e1 of
                 IV 1 => eval f e2 
               | IV 0 => eval f e3 
               |  _   => raise Error "R If")
  | eval f (Abs(x,t,e)) = Proc(x, e, f)
  | eval f (App(e1,e2)) = (case (eval f e1, eval f e2) of
                 (Proc(x,e,f'), v) =>  eval (update f' x v) e
               | _ => raise Error "R App")



(* Tests *)
val f1 = update (update empty "x" Int) "y" Bool
val e1 = Abs("y", Int, Opr(Leq, Id"x", Id"y"))
val test1 = elab f1 e1

val f2 = update empty "x" (IV 5)
val e2 = Opr(Leq, Id"x", Con(IC 7))
val test2 = eval f2 e2