+++ /dev/null
-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
-
+++ /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) -> 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
+++ /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
-
-
+++ /dev/null
-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
--- /dev/null
+(*
+ 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
+*)