projects
/
lambda.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
update intensionality.ml
[lambda.git]
/
code
/
untyped_evaluator.ml
diff --git
a/code/untyped_evaluator.ml
b/code/untyped_evaluator.ml
index
92efa6e
..
5ccecb5
100644
(file)
--- a/
code/untyped_evaluator.ml
+++ b/
code/untyped_evaluator.ml
@@
-1,5
+1,5
@@
(*
(*
- This is a simplified version of the code at
...
+ This is a simplified version of the code at
http://lambda.jimpryor.net/code/untyped_full-1.7.tgz
You can use this code as follows:
1. First, use a text editor to fill in the (* COMPLETE THIS *) portions.
You can use this code as follows:
1. First, use a text editor to fill in the (* COMPLETE THIS *) portions.
@@
-15,9
+15,9
@@
`reduce (App(Lambda("x",Var "x"),Lambda("y",Var "y")))`
`evaluate (App(Lambda("x",Var "x"),Lambda("y",Var "y")))`
`reduce (App(Lambda("x",Var "x"),Lambda("y",Var "y")))`
`evaluate (App(Lambda("x",Var "x"),Lambda("y",Var "y")))`
- The two interpreters presented below are (V
1) a substitute-and-replace
- interpreter, and (V
2
) an environment-based interpreter. We discuss the
- differences between these in the notes.
+ The two interpreters presented below are (V
ersionA) a substitute-and-repeat
+ interpreter, and (V
ersionB
) an environment-based interpreter. We discuss the
+ differences between these in the
course
notes.
The implementeations we provide make both of these call-by-value. When given
a term `App(head, arg)`, the steps are: first, reduce or evaluate
The implementeations we provide make both of these call-by-value. When given
a term `App(head, arg)`, the steps are: first, reduce or evaluate
@@
-30,14
+30,14
@@
Additionally, these implementations assume that free variables are "stuck"
terms rather than result values. That is a bit inconvenient with this
Additionally, these implementations assume that free variables are "stuck"
terms rather than result values. That is a bit inconvenient with this
- simplified program: it means that Lambdas (or Closures, in V
2
) are the only
+ simplified program: it means that Lambdas (or Closures, in V
B
) are the only
result values. But in the fuller code from which this is simplified, it
makes more sense, because there we also have literal number and boolean
values as results, too.
result values. But in the fuller code from which this is simplified, it
makes more sense, because there we also have literal number and boolean
values as results, too.
- The environments play absolutely no role in the simplified V
1
interpreter
- presented here. In the fuller code, they have a limited role in the V
1
- interpreter. In the V
2
interpreter, the environments are essential.
+ The environments play absolutely no role in the simplified V
A
interpreter
+ presented here. In the fuller code, they have a limited role in the V
A
+ interpreter. In the V
B
interpreter, the environments are essential.
*)
type identifier = string
*)
type identifier = string
@@
-45,10
+45,10
@@
type identifier = string
type term =
| Var of identifier
| App of term * term
type term =
| Var of identifier
| App of term * term
- | Lambda of identifier * term (* in V
2
, never used as a result *)
+ | Lambda of identifier * term (* in V
B
, never used as a result *)
| Let of identifier * term * term
| If of term * term * term
| Let of identifier * term * term
| If of term * term * term
- (* the following variant is never used as a term, only as a V
2
result *)
+ (* the following variant is never used as a term, only as a V
B
result *)
| Closure of identifier * term * env
(* in the fuller code, we separate the term and result types *)
| Closure of identifier * term * env
(* in the fuller code, we separate the term and result types *)
@@
-61,7
+61,7
@@
and env = (identifier * term) list
(* Operations for environments *)
let empty = []
let shift (ident : identifier) binding env = (ident,binding) :: env
(* Operations for environments *)
let empty = []
let shift (ident : identifier) binding env = (ident,binding) :: env
-let rec lookup (sought_ident : ident) (env : env) : term option =
+let rec lookup (sought_ident : ident
ifier
) (env : env) : term option =
match env with
| [] -> None
| (ident, binding) :: _ when ident = sought_ident -> Some binding
match env with
| [] -> None
| (ident, binding) :: _ when ident = sought_ident -> Some binding
@@
-72,17
+72,17
@@
let rec lookup (sought_ident : ident) (env : env) : term option =
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 `x y`. The
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 `x y`. The
-
reduction-based
interpreter just signals this with a normal
+
substitute-and-repeat
interpreter just signals 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
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 V
1
, since we lack
+ exception to report a failed term in V
A
, since we lack
the resources to print the term instead, as the full code does.
*)
exception Stuck of term
the resources to print the term instead, as the full code does.
*)
exception Stuck of term
-module V
1
= struct
+module V
A
= struct
(* ---------------------------------------------------------------
Interpreter that reduces by substituting, using:
val reduce_head_once : term -> env -> reduceOutcome
(* ---------------------------------------------------------------
Interpreter that reduces by substituting, using:
val reduce_head_once : term -> env -> reduceOutcome
@@
-198,7
+198,7
@@
module V1 = struct
| Lambda _ -> AlreadyResult term
| Var var -> failwith ("Unbound variable `" ^ var ^ "`")
| Lambda _ -> AlreadyResult term
| Var var -> failwith ("Unbound variable `" ^ var ^ "`")
- | Closure _ -> assert false (* no Closures in V
1
*)
+ | Closure _ -> assert false (* no Closures in V
A
*)
(* In this simplified version there are no Bool Literals, so If terms are always stuck
| If(Literal(Bool true),yes,no) -> ReducedTo yes
(* In this simplified version there are no Bool Literals, so If terms are always stuck
| If(Literal(Bool true),yes,no) -> ReducedTo yes
@@
-249,9
+249,9
@@
module V1 = struct
| StuckAt subterm -> raise (Stuck subterm)
| ReducedTo term' -> reduce term' env (* keep trying *)
| StuckAt subterm -> raise (Stuck subterm)
| ReducedTo term' -> reduce term' env (* keep trying *)
-end (* module V
1
*)
+end (* module V
A
*)
-module V
2
= struct
+module V
B
= struct
(* ---------------------------------------------------------------
Interpreter that employs an "environment" or assignment
function of results, using:
(* ---------------------------------------------------------------
Interpreter that employs an "environment" or assignment
function of results, using:
@@
-304,8
+304,8
@@
module V2 = struct
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 *)
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 V
2
*)
+end (* module V
B
*)
-let reduce term = V
1
.reduce term empty
-let evaluate term = V
2
.evaluate term empty
+let reduce term = V
A
.reduce term empty
+let evaluate term = V
B
.evaluate term empty