From ef92642b2173e886c71bed968113f5c68c163e2a Mon Sep 17 00:00:00 2001 From: Chris Date: Sat, 14 Mar 2015 09:50:30 -0400 Subject: [PATCH] exercises --- ...reduction.ml => _reduction_with_substitution.ml | 0 code/_reduction_with_environments.ml | 96 ++++++++++++++++++++++ code/reduction_with_environments.ml | 82 ++++++++++++++++++ exercises/_assignment6.mdwn | 44 ++++++++-- .../reduction.ml => reduction_with_substitution.ml | 2 +- 5 files changed, 215 insertions(+), 9 deletions(-) rename code/_reduction.ml => _reduction_with_substitution.ml (100%) create mode 100644 code/_reduction_with_environments.ml create mode 100644 code/reduction_with_environments.ml rename code/reduction.ml => reduction_with_substitution.ml (99%) diff --git a/code/_reduction.ml b/_reduction_with_substitution.ml similarity index 100% rename from code/_reduction.ml rename to _reduction_with_substitution.ml diff --git a/code/_reduction_with_environments.ml b/code/_reduction_with_environments.ml new file mode 100644 index 00000000..db406c75 --- /dev/null +++ b/code/_reduction_with_environments.ml @@ -0,0 +1,96 @@ +(* 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 diff --git a/code/reduction_with_environments.ml b/code/reduction_with_environments.ml new file mode 100644 index 00000000..fecac134 --- /dev/null +++ b/code/reduction_with_environments.ml @@ -0,0 +1,82 @@ +(* 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 + + diff --git a/exercises/_assignment6.mdwn b/exercises/_assignment6.mdwn index f6a48030..9431edfe 100644 --- a/exercises/_assignment6.mdwn +++ b/exercises/_assignment6.mdwn @@ -40,17 +40,45 @@ We're not going to ask you to write the entire program yourself. 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. diff --git a/code/reduction.ml b/reduction_with_substitution.ml similarity index 99% rename from code/reduction.ml rename to reduction_with_substitution.ml index 188a90b6..93755b38 100644 --- a/code/reduction.ml +++ b/reduction_with_substitution.ml @@ -49,7 +49,7 @@ let rec substitute (term:lambdaTerm) (ident:identifier) (replacement:lambdaTerm) | 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)) -- 2.11.0