From e1626ef4172d63a6bd74cbd8ab0fe56bb8ef8775 Mon Sep 17 00:00:00 2001 From: Jim Date: Fri, 20 Mar 2015 18:45:27 -0400 Subject: [PATCH] provide simplified untyped_evaluator (complete version) --- code/_reduction_with_substitution.ml | 143 ----------------- code/reduction_with_closures.ml | 96 ------------ code/reduction_with_environments.ml | 82 ---------- code/reduction_with_substitution.ml | 142 ----------------- code/untyped_evaluator.ml | 296 +++++++++++++++++++++++++++++++++++ 5 files changed, 296 insertions(+), 463 deletions(-) delete mode 100644 code/_reduction_with_substitution.ml delete mode 100644 code/reduction_with_closures.ml delete mode 100644 code/reduction_with_environments.ml delete mode 100644 code/reduction_with_substitution.ml create mode 100644 code/untyped_evaluator.ml diff --git a/code/_reduction_with_substitution.ml b/code/_reduction_with_substitution.ml deleted file mode 100644 index 3882c7fb..00000000 --- a/code/_reduction_with_substitution.ml +++ /dev/null @@ -1,143 +0,0 @@ -type primFunction = Succ | Pred | IsZero | Leq | Leq_partially_applied of int - -type constant = Num of int | Bool of bool | Funct 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 - -let rec free_in (ident:identifier) (term:lambdaTerm) : bool = - match term with - | Constant _ -> false - | Var(var_ident) -> var_ident = ident - | Abstract(bound_ident, body) -> bound_ident <> ident && free_in ident body - | App(head, arg) -> free_in ident head || free_in ident arg - | IfThenElse(test, yes, no) -> free_in ident test || free_in ident yes || free_in ident no - | Let(bound_ident, arg, body) -> free_in ident arg || (bound_ident <> ident && free_in ident body) - -let fresh_var (base : identifier) (term:lambdaTerm) = - let rec all_vars term vs = match term with - | Constant _ -> vs - | Var(var_ident) -> var_ident :: vs - | Abstract(bound_ident, body) -> all_vars body (bound_ident :: vs) - | App(head, arg) -> let vs' = all_vars head vs - in all_vars arg vs' - | IfThenElse(test, yes, no) -> let vs' = all_vars test vs - in let vs'' = all_vars yes vs' - in all_vars no vs'' - | Let(bound_ident, arg, body) -> let vs' = all_vars arg vs - in all_vars body (bound_ident :: vs') - in let current = all_vars term [] - in let rec check ident = if List.mem ident current then check (ident ^ "'") else ident - in check (base ^ "'") (* keep adding primes until we find a variable unused (either free or bound) in term *) - -let rec substitute (term:lambdaTerm) (ident:identifier) (replacement:lambdaTerm) : lambdaTerm = - match term with - | Constant _ -> term - | Var(var_ident) when var_ident = ident -> replacement - | Var _ -> term - | App(head, arg) -> let head' = substitute head ident replacement - in let arg' = substitute arg ident replacement - in App(head', arg') - | IfThenElse(test, yes, no) -> let test' = substitute test ident replacement - in let yes' = substitute yes ident replacement - in let no' = substitute no ident replacement - in IfThenElse(test', yes', no') - | Abstract(bound_ident, body) when bound_ident = ident || not (free_in ident body) -> - (* vacuous substitution *) - term - | 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') - | 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)) - in let body' = substitute body bound_ident (Var bound_ident') - in let body'' = substitute body' ident replacement - in Abstract(bound_ident', body'') - | Let(bound_ident, arg, body) when bound_ident = ident || not (free_in ident body) -> - let arg' = substitute arg ident replacement - in Let(bound_ident, arg', body) - | Let(bound_ident, arg, body) when not (free_in bound_ident replacement) -> - (* can substitute without renaming bound_ident *) - let body' = substitute body ident replacement - in let arg' = substitute arg ident replacement - in Let(bound_ident, arg', body') - | Let(bound_ident, arg, 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)) - in let body' = substitute body bound_ident (Var bound_ident') - in let body'' = substitute body' ident replacement - in let arg' = substitute arg ident replacement - in Let(bound_ident', arg', body'') - -type reduceOutcome = AlreadyResult | ReducedTo of lambdaTerm | StuckAt of lambdaTerm - -exception Stuck of lambdaTerm - -let rec reduce1 (term:lambdaTerm) : reduceOutcome = - match term with - (* notice we never evaluate a yes/np branch until it is chosen *) - | IfThenElse(Constant(Bool true), yes, _) -> ReducedTo yes - | IfThenElse(Constant(Bool false), _, no) -> ReducedTo no - | IfThenElse(test, yes, no) -> (match reduce1 test with - | AlreadyResult -> StuckAt term (* if test was not reducible, neither is IfThenElse *) - | ReducedTo test' -> ReducedTo (IfThenElse (test', yes, no)) - | StuckAt _ as outcome -> outcome) - (* notice we never evaluate the body except after substituting, and that happens only after arg is reduced to a result *) - | Let(bound_var, arg, body) -> (match reduce1 arg with - | AlreadyResult -> (* if arg was not reducible, we can substitute *) - ReducedTo (substitute body bound_var arg) - | ReducedTo arg' -> ReducedTo (Let(bound_var, arg', body)) - | StuckAt _ as outcome -> outcome) - (* notice we only substitute after arg is reduced to a result *) - | App(Abstract(bound_var, body) as head, arg) -> (match reduce1 arg with - | AlreadyResult -> (* if arg was not reducible, we can substitute *) - ReducedTo (substitute body bound_var arg) - | ReducedTo arg' -> ReducedTo (App(head, arg')) - | StuckAt _ as outcome -> outcome) - (* applications of primFunctions are reduced only when their arguments have been reduced to THE RIGHT TYPES of result *) - | App(Constant(Funct Succ), Constant(Num n)) -> ReducedTo (Constant(Num (n+1))) - | App(Constant(Funct Pred), Constant(Num n)) -> ReducedTo (Constant(Num (if n = 0 then 0 else n-1))) - | App(Constant(Funct IsZero), Constant(Num n)) -> ReducedTo (Constant(Bool (n=0))) - (* binary primFunctions are curried, have to be reduced in two steps *) - | App(Constant(Funct Leq), Constant(Num n)) -> ReducedTo (Constant(Funct (Leq_partially_applied n))) - | App(Constant(Funct (Leq_partially_applied m)), Constant(Num n)) -> ReducedTo (Constant(Bool (m<=n))) - (* first the head should be reduced, next the arg *) - | App(head, arg) -> (match reduce1 head with - | ReducedTo head' -> ReducedTo (App(head', arg)) - | StuckAt _ as outcome -> outcome - | AlreadyResult -> (* head was not reducible, was arg? *) - (match reduce1 arg with - | ReducedTo arg' -> ReducedTo (App(head, arg')) - (* else the reducible cases of App(result, result) were caught above; this must be stuck *) - | AlreadyResult -> StuckAt term - | StuckAt _ as outcome -> outcome)) - | Var _ -> StuckAt term (* free variables are stuck *) - | Constant _ -> AlreadyResult - | Abstract(_, _) -> AlreadyResult - -let rec check_numbers (term:lambdaTerm) : unit = - match term with - | Constant(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 reduce (term:lambdaTerm) : lambdaTerm = - (* scan to verify that term doesn't have any Const(Num (negative)) *) - let () = check_numbers term - in let rec aux term = match reduce1 term with - | AlreadyResult -> term - | ReducedTo term' -> aux term' (* keep trying *) - | StuckAt stuck_term -> raise (Stuck stuck_term) (* fail by raising exception *) - in aux term - 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 diff --git a/code/reduction_with_environments.ml b/code/reduction_with_environments.ml deleted file mode 100644 index fecac134..00000000 --- a/code/reduction_with_environments.ml +++ /dev/null @@ -1,82 +0,0 @@ -(* 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/code/reduction_with_substitution.ml b/code/reduction_with_substitution.ml deleted file mode 100644 index 184081e9..00000000 --- a/code/reduction_with_substitution.ml +++ /dev/null @@ -1,142 +0,0 @@ -type primFunction = Succ | Pred | IsZero | Leq | Leq_partially_applied of int - -type constant = Num of int | Bool of bool | Funct 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 - -let rec free_in (ident:identifier) (term:lambdaTerm) : bool = - match term with - | Constant _ -> false - | Var(var_ident) -> var_ident = ident -(* | Abstract(bound_ident, body) -> COMPLETE THIS LINE *) -(* | App(head, arg) -> COMPLETE THIS LINE *) - | IfThenElse(test, yes, no) -> free_in ident test || free_in ident yes || free_in ident no - | Let(bound_ident, arg, body) -> free_in ident arg || (bound_ident <> ident && free_in ident body) - -let fresh_var (base : identifier) (term:lambdaTerm) = - let rec all_vars term vs = match term with - | Constant _ -> vs - | Var(var_ident) -> var_ident :: vs - | Abstract(bound_ident, body) -> all_vars body (bound_ident :: vs) - | App(head, arg) -> let vs' = all_vars head vs - in all_vars arg vs' - | IfThenElse(test, yes, no) -> let vs' = all_vars test vs - in let vs'' = all_vars yes vs' - in all_vars no vs'' - | Let(bound_ident, arg, body) -> let vs' = all_vars arg vs - in all_vars body (bound_ident :: vs') - in let current = all_vars term [] - in let rec check ident = if List.mem ident current then check (ident ^ "'") else ident - in check (base ^ "'") (* keep adding primes until we find a variable unused (either free or bound) in term *) - -let rec substitute (term:lambdaTerm) (ident:identifier) (replacement:lambdaTerm) : lambdaTerm = - match term with - | Constant _ -> term - | Var(var_ident) when var_ident = ident -> replacement - | Var _ -> term - | App(head, arg) -> let head' = substitute head ident replacement - in let arg' = substitute arg ident replacement - in App(head', arg') - | IfThenElse(test, yes, no) -> let test' = substitute test ident replacement - in let yes' = substitute yes ident replacement - in let no' = substitute no ident replacement - in IfThenElse(test', yes', no') - | Abstract(bound_ident, body) when bound_ident = ident || not (free_in ident body) -> - (* vacuous substitution *) - term - | Abstract(bound_ident, body) when not (free_in bound_ident replacement) -> - (* can substitute without renaming bound_ident *) - let body' = substitute body ident replacement - 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)) - in let body' = substitute body bound_ident (Var bound_ident') - in let body'' = substitute body' ident replacement - in Abstract(bound_ident', body'') - | Let(bound_ident, arg, body) when bound_ident = ident || not (free_in ident body) -> - let arg' = substitute arg ident replacement - in Let(bound_ident, arg', body) - | Let(bound_ident, arg, body) when not (free_in bound_ident replacement) -> - (* can substitute without renaming bound_ident *) - let body' = substitute body ident replacement - in let arg' = substitute arg ident replacement - in Let(bound_ident, arg', body') - | Let(bound_ident, arg, 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)) - in let body' = substitute body bound_ident (Var bound_ident') - in let body'' = substitute body' ident replacement - in let arg' = substitute arg ident replacement - in Let(bound_ident', arg', body'') - -type reduceOutcome = AlreadyResult | ReducedTo of lambdaTerm | StuckAt of lambdaTerm - -exception Stuck of lambdaTerm - -let rec reduce1 (term:lambdaTerm) : reduceOutcome = - match term with - (* notice we never evaluate a yes/np branch until it is chosen *) - | IfThenElse(Constant(Bool true), yes, _) -> ReducedTo yes - | IfThenElse(Constant(Bool false), _, no) -> ReducedTo no - | IfThenElse(test, yes, no) -> (match reduce1 test with - | AlreadyResult -> StuckAt term (* if test was not reducible, neither is IfThenElse *) - | ReducedTo test' -> ReducedTo (IfThenElse (test', yes, no)) - | StuckAt _ as outcome -> outcome) - (* notice we never evaluate the body except after substituting, and that happens only after arg is reduced to a result *) - | Let(bound_var, arg, body) -> (match reduce1 arg with - | AlreadyResult -> (* if arg was not reducible, we can substitute *) - ReducedTo (substitute body bound_var arg) - | ReducedTo arg' -> ReducedTo (Let(bound_var, arg', body)) - | StuckAt _ as outcome -> outcome) - (* notice we only substitute after arg is reduced to a result *) - | App(Abstract(bound_var, body) as head, arg) -> (match reduce1 arg with - | AlreadyResult -> (* if arg was not reducible, we can substitute *) - ReducedTo (substitute body bound_var arg) - | ReducedTo arg' -> ReducedTo (App(head, arg')) - | StuckAt _ as outcome -> outcome) - (* applications of primFunctions are reduced only when their arguments have been reduced to THE RIGHT TYPES of result *) - | App(Constant(Funct Succ), Constant(Num n)) -> ReducedTo (Constant(Num (n+1))) - | App(Constant(Funct Pred), Constant(Num n)) -> ReducedTo (Constant(Num (if n = 0 then 0 else n-1))) - | App(Constant(Funct IsZero), Constant(Num n)) -> ReducedTo (Constant(Bool (n=0))) - (* binary primFunctions are curried, have to be reduced in two steps *) - | App(Constant(Funct Leq), Constant(Num n)) -> ReducedTo (Constant(Funct (Leq_partially_applied n))) - | App(Constant(Funct (Leq_partially_applied m)), Constant(Num n)) -> ReducedTo (Constant(Bool (m<=n))) - (* first the head should be reduced, next the arg *) - | App(head, arg) -> (match reduce1 head with - | ReducedTo head' -> ReducedTo (App(head', arg)) - | StuckAt _ as outcome -> outcome - | AlreadyResult -> (* head was not reducible, was arg? *) - (match reduce1 arg with - | ReducedTo arg' -> ReducedTo (App(head, arg')) - (* else the reducible cases of App(result, result) were caught above; this must be stuck *) - | AlreadyResult -> StuckAt term - | StuckAt _ as outcome -> outcome)) - | Var _ -> StuckAt term (* free variables are stuck *) - | Constant _ -> AlreadyResult - | Abstract(_, _) -> AlreadyResult - -let rec check_numbers (term:lambdaTerm) : unit = - match term with - | Constant(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 reduce (term:lambdaTerm) : lambdaTerm = - (* scan to verify that term doesn't have any Const(Num (negative)) *) - let () = check_numbers term - in let rec aux term = match reduce1 term with - | AlreadyResult -> term - | ReducedTo term' -> aux term' (* keep trying *) - | StuckAt stuck_term -> raise (Stuck stuck_term) (* fail by raising exception *) - in aux term diff --git a/code/untyped_evaluator.ml b/code/untyped_evaluator.ml new file mode 100644 index 00000000..5323dcb9 --- /dev/null +++ b/code/untyped_evaluator.ml @@ -0,0 +1,296 @@ +(* + This is a simplified version of the code at ... + You can use this code as follows: + + 1. First, use a text editor to fill in the uncompleted portions. + 2. Then see if OCaml will compile it, by typing `ocamlc -c simple.ml` in a Terminal. + 3. If it doesn't work, go back to step 1. + 4. If it does work, then you can start up the OCaml toplevel using `ocaml -I DIRECTORY`, + where DIRECTORY is the name of the folder that contains your `simple.ml` file. + (Alternatively, if OCaml is already started, you can type `#directory "DIRECTORY";;` + 5. Then once OCaml is started, you can either: (a) type `#load "simple.cmo";;`, then type + `open Simple;;` (this has to be on a separate line from step (a), it seems); + or (b) instead you can type `#use "simple.ml";;` + 6. Now you can try commands like `interpret (App(Lambda("x",Var "x"),Lambda("y",Var "y"))) empty` + Or V1.reduce (App(Lambda("x",Var "x"),Lambda("y",Var "y"))) empty` + Or V1.evaluate (App(Lambda("x",Var "x"),Lambda("y",Var "y"))) empty` + + The environments play absolutely no role in this simplified V1 interpreter. In the + fuller code, they have a limited role in the V1 interpreter. In the V2 interpreter, + the environments are essential. This simplified code just provides a single + implementation of environments; but the fuller code provides more. +*) + +type identifier = string + +type term = + | Var of identifier + | App of term * term + | Lambda of identifier * term + | Let of identifier * term * term + | If of term * term * term + | Closure of identifier * term * env + +and result = term + +and env = identifier -> term option + +let empty = fun _ -> None +let push (ident : identifier) binding env = + fun (sought_ident : identifier) -> + if ident = sought_ident + then Some binding + else env sought_ident +let lookup sought_ident env = env sought_ident + + +(* + eval raises this exception when it fails to reduce/evaluate + a term, because it has components for which no + reduction/evaluation is defined, such as `succ false`. The + reduction-based interpreter just signaled this with a normal + return value; but the environment- based interpreter uses an + exception to abort prematurely. + + In this simplified version of the code, we also use this + exception to report a failed term in V1, since we lack + the resources to print the term instead, as the full code does. +*) +exception Stuck of term + +module V1 = struct + (* --------------------------------------------------------------- + Interpreter that reduces by substituting, using: + val reduce_head_once : term -> env -> reduceOutcome + val reduce : term -> env -> result + + reduce_head_once is similiar to reduce_if_redex in the + combinatory logic interpreter, except that the latter only + performed a reduction if its argument was exactly a redex. + It had to rely on its caller to detect cases where the term + was instead a longer sequence of applications that had a + redex at its head. In the present code, on the other hand, + we have reduce_head_once take care of this itself, by + calling itself recursively where appropriate. Still, it will + only perform at most one reduction per invocation. + *) + + + (* Search term and find a variable that isn't used in it, + either free or bound. We do this by appending primes to base + until we find an unused or "fresh" variable. *) + let fresh_var (base : identifier) (term : term) : identifier = + let rec aux term vars = + match term with + | Var(var_ident) -> + var_ident :: vars + | App(head, arg) -> + let vars' = aux head vars in + aux arg vars' + | Lambda(bound_ident, body) -> + aux body (bound_ident :: vars) + | Let(bound_ident, arg, body) -> + let vars' = aux arg vars in + aux body (bound_ident :: vars') + | If(test, yes, no) -> + let vars' = aux test vars in + let vars'' = aux yes vars' in + aux no vars'' + | Closure _ -> assert false in + let used_vars = aux term [] in + let rec check ident = + if List.mem ident used_vars + then check (ident ^ "'") + else ident in + check (base ^ "'") + + let rec free_in (ident : identifier) (term : term) : bool = + match term with + | Var(var_ident) -> + var_ident = ident + | App(head, arg) -> + free_in ident head || free_in ident arg + | Lambda(bound_ident, body) -> + bound_ident <> ident && free_in ident body + | Let(bound_ident, arg, body) -> + free_in ident arg || (bound_ident <> ident && free_in ident body) + | If(test, yes, no) -> + free_in ident test || free_in ident yes || free_in ident no + | Closure _ -> assert false + + let rec substitute (ident:identifier) (replacement : term) (original : term) = + match original with + | Var(var_ident) when var_ident = ident -> replacement + | Var _ as orig -> orig + | App(head, arg) -> + let head' = substitute ident replacement head in + let arg' = substitute ident replacement arg in + App(head', arg') + | Lambda(bound_ident, body) as orig + when bound_ident = ident || not (free_in ident body) -> + (* vacuous substitution *) + orig + | Lambda(bound_ident, body) + when not (free_in bound_ident replacement) -> + (* can substitute without renaming bound_ident *) + let body' = substitute ident replacement body in + Lambda(bound_ident, body') + | Lambda(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)) in + let body' = substitute bound_ident (Var bound_ident') body in + let body'' = substitute ident replacement body' in + Lambda(bound_ident', body'') + | Let(bound_ident, arg, body) + when bound_ident = ident || not (free_in ident body) -> + let arg' = substitute ident replacement arg in + Let(bound_ident, arg', body) + | Let(bound_ident, arg, body) + when not (free_in bound_ident replacement) -> + (* can substitute without renaming bound_ident *) + let body' = substitute ident replacement body in + let arg' = substitute ident replacement arg in + Let(bound_ident, arg', body') + | Let(bound_ident, arg, 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)) in + let body' = substitute bound_ident (Var bound_ident') body in + let body'' = substitute ident replacement body' in + let arg' = substitute ident replacement arg in + Let(bound_ident', arg', body'') + | If(test, yes, no) -> + let test' = substitute ident replacement test in + let yes' = substitute ident replacement yes in + let no' = substitute ident replacement no in + If(test', yes', no') + | Closure _ -> assert false + + type reduceOutcome = AlreadyResult of result | StuckAt of term | ReducedTo of term + + let rec reduce_head_once (term : term) (env : env) : reduceOutcome = + match term with + | Lambda _ -> AlreadyResult term + + | Var var -> failwith ("Unbound variable `" ^ var ^ "`") + | Closure _ -> assert false (* no Closures in V1 *) + +(* In this simplified version there are no Bool Literals, so If terms are always stuck + | If(Literal(Bool true),yes,no) -> ReducedTo yes + | If(Literal(Bool false),yes,no) -> ReducedTo no +*) + | If(test,yes,no) -> + (match reduce_head_once test env with + | AlreadyResult _ -> StuckAt term (* if test was not reducible to a bool, the if-term is not reducible at all *) + | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *) + | ReducedTo test' -> ReducedTo(If(test',yes,no))) + + (* notice we never evaluate the body except after substituting + and that happens only after arg is reduced to a result *) + | Let(bound_var,arg,body) -> + (match reduce_head_once arg env with + | AlreadyResult _ -> + (* if arg was not reducible, we can substitute *) + ReducedTo (substitute bound_var arg body) + | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *) + | ReducedTo arg' -> ReducedTo (Let(bound_var,arg',body))) + + (* notice we only substitute after arg is reduced to a result *) + | App(Lambda(bound_var, body) as head, arg) -> + (match reduce_head_once arg env with + | AlreadyResult _ -> + (* if arg was not reducible, we can substitute *) + ReducedTo (substitute bound_var arg body) + | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *) + | ReducedTo arg' -> ReducedTo (App(head, arg'))) + + (* first the head should be reduced, next the arg *) + | App(head, arg) -> + (match reduce_head_once head env with + | AlreadyResult _ -> (* head was not reducible, was arg? *) + (match reduce_head_once arg env with + | ReducedTo arg' -> ReducedTo (App(head, arg')) + (* reducible cases of App(result, result) were caught above; so here we're stuck *) + | AlreadyResult _ -> StuckAt term + | StuckAt _ as outcome -> outcome) (* propagate Stuck subterm *) + | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *) + | ReducedTo head' -> ReducedTo (App(head', arg))) + + + + + let rec reduce (term : term) (env : env) = + match reduce_head_once term env with + | AlreadyResult res -> res + | StuckAt subterm -> raise (Stuck subterm) + | ReducedTo term' -> reduce term' env (* keep trying *) + +end (* module V1 *) + +module V2 = struct + (* --------------------------------------------------------------- + Interpreter that employs an "environment" or assignment + function of results, using: + val eval term -> env -> result, or may raise (Stuck term) + val evaluate term -> env -> result + Now `env` contains local as well as toplevel bindings. + *) + + let rec eval (term : term) (env : env) : result = + match term with + | Closure _ -> term + + | Lambda(bound_var, body) -> Closure(bound_var, body, env) + + | Var var -> + (match lookup var env with + (* the first case is different from V1.reduce_head_once *) + | Some res -> res + | None -> failwith ("Unbound variable `" ^ var ^ "`")) + + | If(test, yes, no) -> + (match eval test env with +(* In this simplified version there are no Bool Literals, so If terms are always stuck + | Literal(Bool true) -> eval yes env + | Literal(Bool false) -> eval no env +*) + | res -> raise (Stuck(If(res,yes,no)))) + + | Let(bound_var, arg, body) -> + (* evaluate body under a new env where bound_var has been + bound to the result of evaluating arg under the + current env *) + let arg' = eval arg env in + let env' = push bound_var arg' env in + eval body env' + + | App(head, arg) -> + (match eval head env with + | Closure(bound_var, body, saved_env) -> + (* argument gets evaluated in current env *) + let arg' = eval arg env in + (* evaluate body under saved_env to govern its free + variables, except that we add a binding of + bound_var to arg' *) + let saved_env' = push bound_var arg' saved_env in + eval body saved_env' + | head' -> raise (Stuck(App(head',arg)))) + + + + let evaluate (term : term) (env : env) : result = + eval term env (* in the fuller code, this function catches the Stuck errors and prints them more nicely *) + +end (* module V2 *) + + +(* Put comment (* *)s around exactly one of the following two pairs of lines. *) + +let version = "version 1 (reduce by substituting)" +let interpret = V1.reduce + +(* +let version = "version 2 (use environment for local bindings)" +let interpret = V2.evaluate +*) -- 2.11.0