datatype con = False | True | IC of int type id = string datatype opr = Add | Sub | Mul | Leq datatype ty = Bool | Int | Arrow of ty * ty | Pair of ty * ty | List of ty datatype exp = Con of con | Id of id | Op of exp * opr * exp | If of exp * exp * exp | Abs of id * ty * exp | App of exp * exp | Rec of id * id * ty * ty * exp (* Aufgabe 11.1 *) fun closed' (Con _) ids = true | closed' (Id v) ids = List.exists (fn x => x=v) ids | closed' (Op(e,_,e')) ids = closed' e ids andalso closed' e' ids | closed' (If(e,e',e'')) ids = closed' e ids andalso closed' e' ids andalso closed' e'' ids | closed' (Abs(v,_,e)) ids = closed' e (v::ids) | closed' (App(e,e')) ids = closed' e ids andalso closed' e' ids | closed' (Rec(v,v',_,_,e)) ids = closed' e (v::v'::ids) fun closed exp = closed' exp nil fun freeIds' ids (Con _) = nil | freeIds' ids (Id v) = if List.exists (fn x => x=v) ids then nil else [v] | freeIds' ids (Op(e,_,e')) = (freeIds' ids e) @ (freeIds' ids e') | freeIds' ids (If(e,e',e'')) = (freeIds' ids e) @ (freeIds' ids e') @ (freeIds' ids e'') | freeIds' ids (Abs(v,_,e)) = freeIds' (v::ids) e | freeIds' ids (App(e,e')) = (freeIds' ids e) @ (freeIds' ids e') | freeIds' ids (Rec(v,v',_,_,e)) = freeIds' (v::v'::ids) e fun freeIds exp = freeIds' nil exp (* Aufgabe 11.2 *) 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 exception Unbound of id val empty = (fn id => raise (Unbound id)) fun insert (id, v, env) = (fn x => if id=x then v else env x) fun lookup (id, env) = env id end (* Aufgabe 11.3-5 *) datatype exp = Con of con | Id of id | Op of exp * opr * exp | If of exp * exp * exp | Abs of id * ty * exp | App of exp * exp | Rec of id * id * ty * ty * exp | Tup of exp * exp | Fst of exp | Snd of exp | Nil of ty | Cons of exp * exp | Null of exp | Hd of exp | Tl of exp open Env exception Error of string 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,opr,e2)) = elabOp (elab T e1) opr (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) | elab T (Rec(f,x,t',t,e)) = if (elab (insert(x,t',(insert(f,Arrow(t',t),T)))) e) = t then Arrow(t',t) else raise Error("ill-typed recursive procedure") | elab T (Tup(e1,e2)) = let val t1 = elab T e1 val t2 = elab T e2 in Pair(t1, t2) end | elab T (Fst e) = let val t = elab T e in case t of Pair(t,t') => t | _ => raise Error "ill-typed fst" end | elab T (Snd e) = let val t = elab T e in case t of Pair(t,t') => t' | _ => raise Error "ill-typed snd" end | elab T (Nil t) = List t | elab T (Cons(e, e')) = let val t = elab T e val t' = elab T e' in if (List t) = t' then List t else raise Error "ill-typed cons" end | elab T (Null e) = (case elab T e of List _ => Bool | _ => raise Error "ill-typed null") | elab T (Hd e) = (case elab T e of List t => t | _ => raise Error "ill-typed hd") | elab T (Tl e) = (case elab T e of (t as List t') => t | _ => raise Error "ill-typed tl") datatype value = IV of int | Proc of id * exp * value env | RProc of id * id * exp * value env | VPair of value * value | VCons of value * value 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 "type error" fun eval V (Con c) = evalCon c | eval V (Id s) = lookup(s,V) | eval V (Op(e1,opr,e2)) = evalOp (eval V e1) opr (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 "type error") | eval V (Abs(s,_,e)) = Proc(s,e,V) | eval V (Rec(s,s',_,_,e)) = RProc(s,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 | (p as RProc(s,s',e,V'), v') => eval (insert(s', v', insert(s, p, V'))) e | _ => raise Error "type error") | eval V (Tup(e1,e2)) = VPair(eval V e1, eval V e2) | eval V (Fst e) = (case eval V e of VPair(v, _) => v | _ => raise Error "type error") | eval V (Snd e) = (case eval V e of VPair(_, v) => v | _ => raise Error "type error") | eval V (Nil _) = (IV 0) | eval V (Cons(e1,e2)) = VCons(eval V e1, eval V e2) | eval V (Null e) = (case eval V e of IV 0 => IV 1 | _ => IV 0) | eval V (Hd e) = (case eval V e of VCons(v,_) => v | _ => raise Error "type error") | eval V (Tl e) = (case eval V e of VCons(_,v) => v | _ => raise Error "type error") (* Aufgabe 11.6 *) type declaration = id * exp type program = declaration list fun elabPro env nil = env | elabPro env ((id, exp)::es) = let val t = elab env exp in elabPro (insert(id, t, env)) es end fun evalPro env nil = env | evalPro env ((id, exp)::es) = let val v = eval env exp in evalPro (insert(id, v, env)) es end