X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;ds=sidebyside;f=code%2Freduction_with_closures.ml;fp=code%2Freduction_with_closures.ml;h=0000000000000000000000000000000000000000;hb=e1626ef4172d63a6bd74cbd8ab0fe56bb8ef8775;hp=dc3d8fa284b186fe60eab63bf62e4b0073d212f8;hpb=6ee4185debd7b5401900080ace6d0445c08853f5;p=lambda.git diff --git a/code/reduction_with_closures.ml b/code/reduction_with_closures.ml deleted file mode 100644 index dc3d8fa2..00000000 --- a/code/reduction_with_closures.ml +++ /dev/null @@ -1,96 +0,0 @@ -(* evaluation2.ml: evaluation-based interpreter *) - -type literal = Num of int | Bool of bool (* intersection of values and Constant terms *) -type primFunction = Succ | Pred | IsZero | Leq (* | Leq_partially_applied of int *) - -(* these have to be declared later, inside the Env modules ... -type value = LiteralV of literal | Closure of lambdaTerm * env -type bound_value = value (* for now, "x" is bound to the same type of thing that Var "x" expresses, but in later stages that won't always be true *) -*) - -type constant = LiteralC of literal | FunctC of primFunction -type identifier = string - -type lambdaTerm = Constant of constant | Var of identifier | Abstract of identifier * lambdaTerm | App of lambdaTerm * lambdaTerm | IfThenElse of lambdaTerm * lambdaTerm * lambdaTerm | Let of identifier * lambdaTerm * lambdaTerm - -module type Env = sig - type env - type value = LiteralV of literal | Closure of lambdaTerm * env - type bound_value = value - val empty: env - val push: identifier -> bound_value -> env -> env - val lookup: identifier -> env -> bound_value option -end - -module Env1: Env = struct - type env = (identifier * bound_value) list - and value = LiteralV of literal | Closure of lambdaTerm * env - and bound_value = value - let empty = [] - let push ident value env = (ident,value)::env - let rec lookup ident' env = match env with - | [] -> None - | (ident,value)::_ when ident = ident' -> Some value - | _::env' -> lookup ident' env' -end - -module Env2: Env = struct - type env = identifier -> bound_value option - and value = LiteralV of literal | Closure of lambdaTerm * env - and bound_value = value - let empty = fun _ -> None - let push ident value env = fun ident' -> if ident = ident' then Some value else env ident' - let lookup ident' env = env ident' -end - -open Env1 - -exception Stuck of lambdaTerm - -let rec eval (term:lambdaTerm) (r:env) : value = - match term with - | IfThenElse(test, yes, no) -> (match eval test r with - | LiteralV(Bool true) -> eval yes r - | LiteralV(Bool false) -> eval no r - | LiteralV lit -> raise (Stuck (IfThenElse(Constant(LiteralC lit),yes,no))) - | Closure(term, _) -> raise (Stuck (IfThenElse(term,yes,no)))) - | Let(bound_ident, arg, body) -> (match eval arg r with - | value -> eval body (push bound_ident value r)) - | App(head, arg) -> (match eval head r with - | LiteralV lit -> raise (Stuck (App(Constant(LiteralC lit), arg))) - | Closure (Abstract(bound_ident, body), saved_r) -> eval body (push bound_ident arg saved_r) (* FIX ME *) - | Closure (Constant (FunctC Leq), saved_r) -> failwith "not yet implemented" - | Closure (Constant (FunctC (_ as prim)), saved_r) -> - (match (prim, eval arg r) with - | (Succ, LiteralV(Num n)) -> LiteralV(Num (n+1)) - | (Pred, LiteralV(Num n)) -> LiteralV(Num (if n = 0 then 0 else n-1)) - | (IsZero, LiteralV(Num n)) -> LiteralV(Bool (n=0)) - | (_, LiteralV lit) -> raise (Stuck (App(Constant(FunctC prim), Constant(LiteralC lit)))) - | (_, Closure(term, _)) -> raise (Stuck (App(Constant(FunctC prim), term)))) - | Closure (term, _) -> raise (Stuck (App(term, arg)))) - | Var ident -> (match lookup ident r with - | Some v -> v - | None -> raise (Stuck term)) (* free variables are stuck *) - | Constant (LiteralC lit) -> LiteralV lit - | Constant (FunctC _) -> Closure(term, empty) (* primFunctions evaluate as Closures with empty environments *) - | Abstract (_,_) -> Closure(term, r) (* Abstracts evaluate as Closures with the current environment; a more efficient implementation would save only that part of the environment that binds variables that are free in the Abstract *) - -let rec check_numbers (term:lambdaTerm) : unit = - match term with - | Constant(LiteralC(Num n)) when n < 0 -> failwith ("Bad Number: " ^ string_of_int n) - | Constant _ -> () - | Var _ -> () - | Abstract(_, body) -> check_numbers body - | App(head, arg) -> let () = check_numbers head - in check_numbers arg - | Let(_, arg, body) -> let () = check_numbers arg - in check_numbers body - | IfThenElse(test, yes, no) -> let () = check_numbers test - in let () = check_numbers yes - in check_numbers no - -let evaluate (term:lambdaTerm) : value = - (* scan to verify that term doesn't have any Const(Num (negative)) *) - let () = check_numbers term - (* evaluate starting with empty env *) - in eval term empty