code/reduction_with_environments.ml

   1 (* evaluation1.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 type value = LiteralV of literal (* | Closure ... *)
   7 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 *)
   8
   9 type constant = LiteralC of literal | FunctC of primFunction
  10 type identifier = string
  11
  12 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
  13
  14 module type Env = sig
  15   type env
  16   val empty: env
  17   val push: identifier -> bound_value -> env -> env
  18   val lookup: identifier -> env -> bound_value option
  19 end
  20
  21 module Env1: Env = struct
  22   type env = (identifier * bound_value) list
  23   let empty = []
  24   let push ident value env = (ident,value)::env
  25   let rec lookup ident' env = match env with
  26     | [] -> None
  27     | (ident,value)::_ when ident = ident' -> Some value
  28     | _::env' -> lookup ident' env'
  29 end
  30
  31 module Env2: Env = struct
  32   type env = identifier -> bound_value option
  33   let empty = fun _ -> None
  34   let push ident value env = fun ident' -> if ident = ident' then Some value else env ident'
  35   let lookup ident' env = env ident'
  36 end
  37
  38 open Env1
  39
  40 exception Stuck of lambdaTerm
  41
  42 let rec eval (term:lambdaTerm) (r:env) : value =
  43   match term with
  44     | IfThenElse(test, yes, no) -> (match eval test r with
  45                                       | LiteralV(Bool true) -> eval yes r
  46                                       | LiteralV(Bool false) -> eval no r
  47                                       | LiteralV lit -> raise (Stuck (IfThenElse(Constant(LiteralC lit),yes,no))))
  48     | Let(bound_var, arg, body) -> (match eval arg r with
  49                                       | value -> eval body (push bound_var value r))
  50     | App(head, arg) -> let headval = eval head r
  51                         in let argval = eval arg r
  52                         in (match (headval, argval) with
  53                               | (LiteralV lit, _) -> raise (Stuck (App(Constant(LiteralC lit), arg)))
  54                               | (_,_) -> failwith "not yet implemented")
  55     | Var ident -> (match lookup ident r with
  56                               | Some v -> v
  57                               | None -> raise (Stuck term)) (* free variables are stuck *)
  58     | Constant (LiteralC lit) -> LiteralV lit
  59     | Constant (FunctC _) -> failwith "not yet implemented"
  60     | Abstract (_,_) -> failwith "not yet implemented"
  61
  62 let rec check_numbers (term:lambdaTerm) : unit =
  63   match term with
  64     | Constant(LiteralC(Num n)) when n < 0 -> failwith ("Bad Number: " ^ string_of_int n)
  65     | Constant _ -> ()
  66     | Var _ -> ()
  67     | Abstract(_, body) -> check_numbers body
  68     | App(head, arg) -> let () = check_numbers head
  69                         in check_numbers arg
  70     | Let(_, arg, body) -> let () = check_numbers arg
  71                            in check_numbers body
  72     | IfThenElse(test, yes, no) -> let () = check_numbers test
  73                            in let () = check_numbers yes
  74                            in check_numbers no
  75
  76 let evaluate (term:lambdaTerm) : value =
  77   (* scan to verify that term doesn't have any Const(Num (negative)) *)
  78   let () = check_numbers term
  79   (* evaluate starting with empty env *)
  80   in eval term empty
  81
  82