--- /dev/null
+(* 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) -> let argval = eval arg r in eval body (push bound_ident argval saved_r)
+ | 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
--- /dev/null
+(* evaluation1.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 *)
+
+type value = LiteralV of literal (* | Closure ... *)
+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
+ 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
+ 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
+ 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))))
+ | Let(bound_var, arg, body) -> (match eval arg r with
+ | value -> eval body (push bound_var value r))
+ | App(head, arg) -> let headval = eval head r
+ in let argval = eval arg r
+ in (match (headval, argval) with
+ | (LiteralV lit, _) -> raise (Stuck (App(Constant(LiteralC lit), arg)))
+ | (_,_) -> failwith "not yet implemented")
+ | 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 _) -> failwith "not yet implemented"
+ | Abstract (_,_) -> failwith "not yet implemented"
+
+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
+
+
Instead, we're going to give you [[the complete program, minus a few
little bits of glue|code/reduction.ml]]. What you need to do is
understand how it all fits together. When you do, you'll understand
-how to add the last little bits to make functioning program. Here's a
-first target for when you get it working:
-
- # reduce (App (Abstract ("x", Var "x"), Constant (Num 3)));;
- - : lambdaTerm = Constant (Num 3)
+how to add the last little bits to make functioning program.
1. In the previous homework, you built a function that took an
identifier and a lambda term and returned a boolean representing
whether that identifier occured free inside of the term. Your first
-task is to adapt your previous solution as necessary to work with the
-code base. Once you have your function working, you should be able to
-run queries such as this:
+task is to complete the `free_in` function, which has been crippled in
+the code base (look for lines that say `COMPLETE THIS LINE`). Once
+you have your function working, you should be able to run queries such
+as this:
+
+ # free_in "x" (App (Abstract ("x", Var "x"), Var "x"));;
+ - : bool = true
+
+2. Once you get the `free_in` function working, you'll need to
+complete the `substitute` function. You'll see a new wrinkle on
+OCaml's pattern-matching construction: `| PATTERN when x = 2 ->
+RESULT`. This means that a match with PATTERN is only triggered if
+the boolean condition in the `when` clause evaluates to true.
+Sample target:
+
+ # substitute (App (Abstract ("x", ((App (Abstract ("x", Var "x"), Var "y")))), Constant (Num 3))) "y" (Constant (Num 4));;
+ - : lambdaTerm = App (Abstract ("x", App (Abstract ("x", Var "x"), Constant (Num 4))), Constant (Num 3))
+
+3. Once you have completed the previous two problems, you'll have a
+complete evaluation program. Here's a simple sanity check for when you
+get it working:
+
+ # reduce (App (Abstract ("x", Var "x"), Constant (Num 3)));;
+ - : lambdaTerm = Constant (Num 3)
+
+What kind of evaluation strategy does this evaluator use? In
+particular, what are the answers to the three questions about
+evaluation strategy as given in the discussion of [[evaluation
+strategies|topics/week3_evaluation_order]] as Q1, Q2, and Q3?
+
+## Evaluation in the untyped calculus: environments
+
+Ok, the previous strategy sucked: tracking free and bound variables,
+computing fresh variables, it's all super complicated.
+Here's a better strategy.
| Abstract(bound_ident, body) when not (free_in bound_ident replacement) ->
(* can substitute without renaming bound_ident *)
let body' = substitute body ident replacement
- in Abstract(bound_ident, body')
+ in (* COMPLETE THIS LINE *)
| Abstract(bound_ident, body) ->
(* find a fresh variable unused in either body or replacement (which we hack by specifying their App) *)
let bound_ident' = fresh_var bound_ident (App(body,replacement))