code/reduction_with_closures.ml

   1 (* evaluation2.ml: evaluation-based interpreter *)
   2
   3 type literal = Num of int | Bool of bool (* intersection of values and Constant terms *)
   4 type primFunction = Succ | Pred | IsZero | Leq (* | Leq_partially_applied of int *)
   5
   6 (* these have to be declared later, inside the Env modules ...
   7 type value = LiteralV of literal | Closure of lambdaTerm * env
   8 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 *)
   9 *)
  10
  11 type constant = LiteralC of literal | FunctC of primFunction
  12 type identifier = string
  13
  14 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
  15
  16 module type Env = sig
  17   type env
  18   type value = LiteralV of literal | Closure of lambdaTerm * env
  19   type bound_value = value
  20   val empty: env
  21   val push: identifier -> bound_value -> env -> env
  22   val lookup: identifier -> env -> bound_value option
  23 end
  24
  25 module Env1: Env = struct
  26   type env = (identifier * bound_value) list
  27   and value = LiteralV of literal | Closure of lambdaTerm * env
  28   and bound_value = value
  29   let empty = []
  30   let push ident value env = (ident,value)::env
  31   let rec lookup ident' env = match env with
  32     | [] -> None
  33     | (ident,value)::_ when ident = ident' -> Some value
  34     | _::env' -> lookup ident' env'
  35 end
  36
  37 module Env2: Env = struct
  38   type env = identifier -> bound_value option
  39   and value = LiteralV of literal | Closure of lambdaTerm * env
  40   and bound_value = value
  41   let empty = fun _ -> None
  42   let push ident value env = fun ident' -> if ident = ident' then Some value else env ident'
  43   let lookup ident' env = env ident'
  44 end
  45
  46 open Env1
  47
  48 exception Stuck of lambdaTerm
  49
  50 let rec eval (term:lambdaTerm) (r:env) : value =
  51   match term with
  52     | IfThenElse(test, yes, no) -> (match eval test r with
  53                                       | LiteralV(Bool true) -> eval yes r
  54                                       | LiteralV(Bool false) -> eval no r
  55                                       | LiteralV lit -> raise (Stuck (IfThenElse(Constant(LiteralC lit),yes,no)))
  56                                       | Closure(term, _) -> raise (Stuck (IfThenElse(term,yes,no))))
  57     | Let(bound_ident, arg, body) -> (match eval arg r with
  58                                       | value -> eval body (push bound_ident value r))
  59     | App(head, arg) -> (match eval head r with
  60                            | LiteralV lit -> raise (Stuck (App(Constant(LiteralC lit), arg)))
  61                            | Closure (Abstract(bound_ident, body), saved_r) -> eval body (push bound_ident arg saved_r) (* FIX ME *)
  62                            | Closure (Constant (FunctC Leq), saved_r) -> failwith "not yet implemented"
  63                            | Closure (Constant (FunctC (_ as prim)), saved_r) ->
  64                                      (match (prim, eval arg r) with
  65                                         | (Succ, LiteralV(Num n)) -> LiteralV(Num (n+1))
  66                                         | (Pred, LiteralV(Num n)) -> LiteralV(Num (if n = 0 then 0 else n-1))
  67                                         | (IsZero, LiteralV(Num n)) -> LiteralV(Bool (n=0))
  68                                         | (_, LiteralV lit) -> raise (Stuck (App(Constant(FunctC prim), Constant(LiteralC lit))))
  69                                         | (_, Closure(term, _)) -> raise (Stuck (App(Constant(FunctC prim), term))))
  70                            | Closure (term, _) -> raise (Stuck (App(term, arg))))
  71     | Var ident -> (match lookup ident r with
  72                               | Some v -> v
  73                               | None -> raise (Stuck term)) (* free variables are stuck *)
  74     | Constant (LiteralC lit) -> LiteralV lit
  75     | Constant (FunctC _) -> Closure(term, empty) (* primFunctions evaluate as Closures with empty environments *)
  76     | 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 *)
  77
  78 let rec check_numbers (term:lambdaTerm) : unit =
  79   match term with
  80     | Constant(LiteralC(Num n)) when n < 0 -> failwith ("Bad Number: " ^ string_of_int n)
  81     | Constant _ -> ()
  82     | Var _ -> ()
  83     | Abstract(_, body) -> check_numbers body
  84     | App(head, arg) -> let () = check_numbers head
  85                         in check_numbers arg
  86     | Let(_, arg, body) -> let () = check_numbers arg
  87                            in check_numbers body
  88     | IfThenElse(test, yes, no) -> let () = check_numbers test
  89                            in let () = check_numbers yes
  90                            in check_numbers no
  91
  92 let evaluate (term:lambdaTerm) : value =
  93   (* scan to verify that term doesn't have any Const(Num (negative)) *)
  94   let () = check_numbers term
  95   (* evaluate starting with empty env *)
  96   in eval term empty