exception Unimplemented exception BadArgument type exp = Var of string | Lam of string * exp | Apply of exp * exp | Closure of string * exp * env and env = (string * exp) list (* large-step environment based semantics *) let rec interp env e = match e with Var s -> List.assoc s env (* do the lookup *) | Lam(s,e2) -> Closure(s,e2,env) (* store env! *) | Closure _ -> e (* closures are values *) | Apply(e1,e2) -> let v1 = interp env e1 in let v2 = interp env e2 in match v1 with Closure(s,e3,env2) -> interp((s,v2)::env2) e3 | _ -> failwith "impossible" (* small-step substitution semantics *) type exp2 = V of string | L of string*exp2 | A of exp2 * exp2 let subst e1_with e2_for s = raise Unimplemented let rec interp_one e = match e with V _ -> failwith "interp_one"(*unbound var*) | L _ -> failwith "interp_one"(*already done*) | A(L(s1,e1),L(s2,e2)) -> subst e1 (L(s2,e2)) s1 | A(L(s1,e1),e2) -> A(L(s1,e1),interp_one e2) | A(e1,e2) -> A(interp_one e1, e2) let rec interp_small e = match e with V _ -> failwith "interp_small" (*unbound var*) | L _ -> e | A(e1,e2) -> interp_small (interp_one e) (* now context-based semantics *) (* ectxt represents "where" the next step "is" *) type ectxt = Hole | Left of ectxt * exp2 | Right of exp2 * ectxt (*exp a value*) let rec split e = (*return ctxt & what's in it*) match e with A(L(s1,e1),L(s2,e2)) -> (Hole,e) | A(L(s1,e1),e2) -> let (ctx2,e3) = split e2 in (Right(L(s1,e1),ctx2), e3) | A(e1,e2) -> let (ctx1,e3) = split e1 in (Left(ctx1,e2), e3) | _ -> raise BadArgument let rec fill ctx e = (* plug the hole *) match ctx with Hole -> e | Left(ctx2,e2) -> A(fill ctx2 e, e2) | Right(e2,ctx2) -> A(e2, fill ctx2 e) let rec interp_small e = match e with V _ -> failwith "interp_small"(*unbound var*) | L _ -> e | _ -> match split e with (ctx, A(L(s3,e3),v)) -> interp_small(fill ctx (subst e3 v s3)) | _ -> failwith "bad split" (* now context-based semantics including Letcc (here with reusing A for a "throw" rather than a separate Throw *) type exp3 = V of string | L of string*exp3 | A of exp3 * exp3 | Letcc of string * exp3 (* new *) | Cont of ectxt2 (* new *) and ectxt2 = Hole (* no change *) | Left of ectxt2 * exp3 | Right of exp3 * ectxt2 let isValue e = match e with L _ -> true | Cont _ -> true | _ -> false let rec split e = match e with Letcc(s1,e1) -> (Hole,e) (* new *) | A(e1,e2) -> if isValue e1 && isValue e2 then (Hole,e) else if isValue e1 then let (ctx2,e3) = split e2 in (Right(e1,ctx2),e3) else let (ctx1,e3) = split e1 in (Left(ctx1,e2), e3) | _ -> failwith "bad args to split" let rec fill ctx e = (* plug the hole *) match ctx with Hole -> e | Left(ctx2,e2) -> A(fill ctx2 e, e2) | Right(e2,ctx2) -> A(e2, fill ctx2 e) let rec interp_small e = match e with V _ -> failwith "interp_small"(*unbound var*) | L _ -> e | _ -> match split e with (ctx, A(L(s3,e3), v)) -> interp_small(fill ctx (subst e3 v s3)) |(ctx, Letcc(s3,e3)) -> interp_small(fill ctx (*woah!!!*) (subst e3 (Cont ctx) s3)) |(ctx, A(Cont c3, v)) -> interp_small(fill c3 v) (*woah!!!*) | _ -> failwith "bad split"