(* Modellimplementierung von F *)
 
(* Abstrakte Syntax *)

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 *)

(* Umgebungen und Ausnahmen *)

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

(* Statische Semantik *)

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")

(* Beispielanwendungen *)

val f = update (update empty "x" Int) "y" Bool
val e = Opr(Add, Id"x", Con(IC 7))
val t = elab f e

(* Umschlag für elab *)

datatype elab = T of ty | SE of string
fun elab' f e = T(elab f e) handle 
    Unbound s => SE("Unbound: "^s)
  | Error s => SE("Error: "^s)

(* Dynamische Semantik *)

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")

(* Beispielanwendungen *)

val f = update empty "x" (IV 5)
val e = Opr(Leq, Id"x", Con(IC 7))
val v = eval f e