tweak lambda evaluator
authorJim Pryor <profjim@jimpryor.net>
Thu, 23 Sep 2010 06:48:03 +0000 (02:48 -0400)
committerJim Pryor <profjim@jimpryor.net>
Thu, 23 Sep 2010 06:48:03 +0000 (02:48 -0400)
Signed-off-by: Jim Pryor <profjim@jimpryor.net>
code/lambda.js
code/parse.js
code/tokens.js
lambda_evaluator.mdwn

index 7dcb53d..f87b355 100644 (file)
 /*jslint bitwise: true,
-       eqeqeq: true,
-       immed: true,
-       newcap: true,
-       nomen: true,
-       onevar: true,
-       plusplus: true,
-       regexp: true,
-       rhino: true,
-       browser: false,
-       undef: true,
-       white: true,
-
-       evil: false,
-       regexp: false,
-       sub: true,
-       laxbreak: true,
-       onevar: false,
-       debug: true */
+    eqeqeq: true,
+    immed: true,
+    newcap: true,
+    nomen: true,
+    onevar: true,
+    plusplus: true,
+    regexp: true,
+    rhino: true,
+    browser: false,
+    undef: true,
+    white: true,
+
+    evil: false,
+    regexp: false,
+    sub: true,
+    laxbreak: true,
+    onevar: false,
+    debug: true */
 
 
 // DeBruijn terms
 // substitution and translation algorithms from Chris Hankin, An Introduction to Lambda Calculi for Comptuer Scientists
 //
 function Db_free(variable) {
-       this.variable = variable;
-       this.subst = function (m, new_term) {
-               return this;
-       };
-       this.renumber = function (m, i) {
-               return this;
-       };
-       // we assume that other will have variable iff it's a Db_free
-       this.equal = function (other) {
-               return other.variable && this.variable.equal(other.variable);
-       };
-       this.contains = this.equal;
+    this.variable = variable;
+    this.subst = function (m, new_term) {
+        return this;
+    };
+    this.renumber = function (m, i) {
+        return this;
+    };
+    // we assume that other will have variable iff it's a Db_free
+    this.equal = function (other) {
+        return other.variable && this.variable.equal(other.variable);
+    };
+    this.contains = this.equal;
 }
 
 function Db_index(i) {
-       this.index = i;
-       this.subst = function (m, new_term) {
-               if (this.index < m) {
-                       return this;
-               } else if (this.index > m) {
-                       return new Db_index(this.index - 1);
-               } else {
-                       return new_term.renumber(this.index, 1);
-               }
-       };
-       this.renumber = function (m, i) {
-               if (this.index < i) {
-                       return this;
-               } else {
-                       return new Db_index(this.index + m - 1);
-               }
-       };
-       // we assume that other will have index iff it's a Db_index
-       this.equal = function (other) {
-               return this.index === other.index;
-       };
-       this.contains = this.equal;
+    this.index = i;
+    this.subst = function (m, new_term) {
+        if (this.index < m) {
+            return this;
+        } else if (this.index > m) {
+            return new Db_index(this.index - 1);
+        } else {
+            return new_term.renumber(this.index, 1);
+        }
+    };
+    this.renumber = function (m, i) {
+        if (this.index < i) {
+            return this;
+        } else {
+            return new Db_index(this.index + m - 1);
+        }
+    };
+    // we assume that other will have index iff it's a Db_index
+    this.equal = function (other) {
+        return this.index === other.index;
+    };
+    this.contains = this.equal;
 }
 
 function Db_app(left, right) {
-       this.left = left;
-       this.right = right;
-       this.subst = function (m, new_term) {
-               return new Db_app(this.left.subst(m, new_term), this.right.subst(m, new_term));
-       };
-       this.renumber = function (m, i) {
-               return new Db_app(this.left.renumber(m, i), this.right.renumber(m, i));
-       };
-       // we assume that other will have left iff it's a Db_app
-       this.equal = function (other) {
-               return other.left && this.left.equal(other.left) && this.right.equal(other.right);
-       };
-       this.contains = function (other) {
-               if (other.left && this.left.equal(other.left) && this.right.equal(other.right)) {
-                       return true;
-               } else {
-                       return this.left.contains(other) || this.right.contains(other);
-               }
-       };
+    this.left = left;
+    this.right = right;
+    this.subst = function (m, new_term) {
+        return new Db_app(this.left.subst(m, new_term), this.right.subst(m, new_term));
+    };
+    this.renumber = function (m, i) {
+        return new Db_app(this.left.renumber(m, i), this.right.renumber(m, i));
+    };
+    // we assume that other will have left iff it's a Db_app
+    this.equal = function (other) {
+        return other.left && this.left.equal(other.left) && this.right.equal(other.right);
+    };
+    this.contains = function (other) {
+        if (other.left && this.left.equal(other.left) && this.right.equal(other.right)) {
+            return true;
+        } else {
+            return this.left.contains(other) || this.right.contains(other);
+        }
+    };
 }
 
 function Db_lam(body) {
-       this.body = body;
-       this.subst = function (m, new_term) {
-               return new Db_lam(this.body.subst(m + 1, new_term));
-       };
-       this.renumber = function (m, i) {
-               return new Db_lam(this.body.renumber(m, i + 1));
-       };
-       // we assume that other will have body iff it's a Db_lam
-       this.equal = function (other) {
-               return other.body && this.body.equal(other.body);
-       };
-       this.contains = function (other) {
-               if (other.body && this.body.equal(other.body)) {
-                       return true;
-               } else {
-                       return this.body.contains(other);
-               }
-       };
+    this.body = body;
+    this.subst = function (m, new_term) {
+        return new Db_lam(this.body.subst(m + 1, new_term));
+    };
+    this.renumber = function (m, i) {
+        return new Db_lam(this.body.renumber(m, i + 1));
+    };
+    // we assume that other will have body iff it's a Db_lam
+    this.equal = function (other) {
+        return other.body && this.body.equal(other.body);
+    };
+    this.contains = function (other) {
+        if (other.body && this.body.equal(other.body)) {
+            return true;
+        } else {
+            return this.body.contains(other);
+        }
+    };
 }
 
 
@@ -111,156 +111,156 @@ function Db_lam(body) {
 // http://okmij.org/ftp/Computation/lambda-calc.html#lambda-calculator-haskell
 //
 function Variable(name, tag) {
-       this.name = name;
-       this.tag = tag || 0;
-       this.to_string = function () {
-               // append count copies of str to accum
-               function markup(accum, count) {
-                       if (count === 0) {
-                               return accum;
-                       } else {
-                               return markup(accum + "'", count - 1);
-                       }
-               }
-               return markup(this.name, this.tag);
-       };
-       this.equal = function (other) {
-               return (this.tag === other.tag) && (this.name === other.name);
-       };
-       // position of this in seq
-       this.position = function (seq) {
-               for (var i = 0; i < seq.length; i += 1) {
-                       if (this.equal(seq[i])) {
-                               return new Db_index(i + 1);
-                       }
-               }
-               return new Db_free(this);
-       };
+    this.name = name;
+    this.tag = tag || 0;
+    this.to_string = function () {
+        // append count copies of str to accum
+        function markup(accum, count) {
+            if (count === 0) {
+                return accum;
+            } else {
+                return markup(accum + "'", count - 1);
+            }
+        }
+        return markup(this.name, this.tag);
+    };
+    this.equal = function (other) {
+        return (this.tag === other.tag) && (this.name === other.name);
+    };
+    // position of this in seq
+    this.position = function (seq) {
+        for (var i = 0; i < seq.length; i += 1) {
+            if (this.equal(seq[i])) {
+                return new Db_index(i + 1);
+            }
+        }
+        return new Db_free(this);
+    };
 }
 
 // if v occurs free_in term, returns Some v' where v' is the highest-tagged
 // variable with the same name as v occurring (free or bound) in term
 //
 function free_in(v, term) {
-       var res = term.has_free(v);
-       return res[0] && res[1];
+    var res = term.has_free(v);
+    return res[0] && res[1];
 }
 
 function subst(v, new_term, expr) {
-       if (new_term.variable && new_term.variable.equal(v)) {
-               return expr;
-       } else {
-               return expr.subst(v, new_term);
-       }
+    if (new_term.variable && new_term.variable.equal(v)) {
+        return expr;
+    } else {
+        return expr.subst(v, new_term);
+    }
 }
 
 function equal(expr1, expr2) {
-       return expr1.debruijn([]).equal(expr2.debruijn([]));
+    return expr1.debruijn([]).equal(expr2.debruijn([]));
 }
 
 function contains(expr1, expr2) {
-       return expr1.debruijn([]).contains(expr2.debruijn([]));
+    return expr1.debruijn([]).contains(expr2.debruijn([]));
 }
 
 
 function Lambda_var(variable) {
-       this.variable = variable;
-       this.debruijn = function (seq) {
-               return this.variable.position(seq);
-       };
-       this.to_string = function (as_atom) {
-               return this.variable.to_string();
-       };
-       this.has_free = function (v) {
-               if (v.name !== this.variable.name) {
-                       return [false, v];
-               } else if (v.tag === this.variable.tag) {
-                       return [true, v];
-               } else {
-                       return [false, this.variable];
-               }
-       };
-       this.subst = function (v, new_term) {
-               if (this.variable.equal(v)) {
-                       return new_term;
-               } else {
-                       return this;
-               }
-       };
-       this.check_eta = function () {
-               return this;
-       };
-       this.eval_loop = function (stack, eta) {
-               function unwind(left, stack) {
-                       if (stack.length === 0) {
-                               return left;
-                       } else {
-                               var x = stack[0];
-                               var xs = stack.slice(1);
-                               return unwind(new Lambda_app(left, x.eval_loop([], eta)), xs);
-                       }
-               }
-               return unwind(this, stack);
-       };
-       this.eval_cbv = function (aggressive) {
-               return this;
-       };
+    this.variable = variable;
+    this.debruijn = function (seq) {
+        return this.variable.position(seq);
+    };
+    this.to_string = function (as_atom) {
+        return this.variable.to_string();
+    };
+    this.has_free = function (v) {
+        if (v.name !== this.variable.name) {
+            return [false, v];
+        } else if (v.tag === this.variable.tag) {
+            return [true, v];
+        } else {
+            return [false, this.variable];
+        }
+    };
+    this.subst = function (v, new_term) {
+        if (this.variable.equal(v)) {
+            return new_term;
+        } else {
+            return this;
+        }
+    };
+    this.check_eta = function () {
+        return this;
+    };
+    this.eval_loop = function (stack, eta) {
+        function unwind(left, stack) {
+            if (stack.length === 0) {
+                return left;
+            } else {
+                var x = stack[0];
+                var xs = stack.slice(1);
+                return unwind(new Lambda_app(left, x.eval_loop([], eta)), xs);
+            }
+        }
+        return unwind(this, stack);
+    };
+    this.eval_cbv = function (aggressive) {
+        return this;
+    };
 }
 
 function Lambda_app(left, right) {
-       this.left = left;
-       this.right = right;
-       this.debruijn = function (seq) {
-               return new Db_app(this.left.debruijn(seq), this.right.debruijn(seq));
-       };
-       this.to_string = function (as_atom) {
-               var base;
-               if (this.left.left) {
-                       base = this.left.to_string() + " " + this.right.to_string(true);
-               } else {
-                       base = this.left.to_string(true) + " " + this.right.to_string(true);
-               }
-               if (as_atom) {
-                       return "(" + base + ")";
-               } else {
-                       return base;
-               }
-       };
-       this.has_free = function (v) {
-               var left_res = this.left.has_free(v);
-               var right_res = this.right.has_free(v);
-               var left_bool = left_res[0];
-               var right_bool = right_res[0];
-               var left_tag = left_res[1].tag;
-               var right_tag = right_res[1].tag;
-               var res;
-               if (left_tag > right_tag) {
-                       res = left_res[1];
-               } else {
-                       res = right_res[1];
-               }
-               return [left_bool || right_bool, res];
-       };
-       this.subst = function (v, new_term) {
-               return new Lambda_app(subst(v, new_term, this.left), subst(v, new_term, this.right));
-       };
-       this.check_eta = function () {
-               return this;
-       };
-       this.eval_loop = function (stack, eta) {
-               var new_stack = stack.slice(0);
-               new_stack.unshift(this.right);
-               return this.left.eval_loop(new_stack, eta);
-       };
-       this.eval_cbv = function (aggressive) {
-               var left = this.left.eval_cbv(aggressive);
-               var right = this.right.eval_cbv(aggressive);
-               if (left.body) {
-                       return subst(left.bound, right, left.body).eval_cbv(aggressive);
-               } else {
-                       return new Lambda_app(left, right);
-               }
-       };
+    this.left = left;
+    this.right = right;
+    this.debruijn = function (seq) {
+        return new Db_app(this.left.debruijn(seq), this.right.debruijn(seq));
+    };
+    this.to_string = function (as_atom) {
+        var base;
+        if (this.left.left) {
+            base = this.left.to_string() + " " + this.right.to_string(true);
+        } else {
+            base = this.left.to_string(true) + " " + this.right.to_string(true);
+        }
+        if (as_atom) {
+            return "(" + base + ")";
+        } else {
+            return base;
+        }
+    };
+    this.has_free = function (v) {
+        var left_res = this.left.has_free(v);
+        var right_res = this.right.has_free(v);
+        var left_bool = left_res[0];
+        var right_bool = right_res[0];
+        var left_tag = left_res[1].tag;
+        var right_tag = right_res[1].tag;
+        var res;
+        if (left_tag > right_tag) {
+            res = left_res[1];
+        } else {
+            res = right_res[1];
+        }
+        return [left_bool || right_bool, res];
+    };
+    this.subst = function (v, new_term) {
+        return new Lambda_app(subst(v, new_term, this.left), subst(v, new_term, this.right));
+    };
+    this.check_eta = function () {
+        return this;
+    };
+    this.eval_loop = function (stack, eta) {
+        var new_stack = stack.slice(0);
+        new_stack.unshift(this.right);
+        return this.left.eval_loop(new_stack, eta);
+    };
+    this.eval_cbv = function (aggressive) {
+        var left = this.left.eval_cbv(aggressive);
+        var right = this.right.eval_cbv(aggressive);
+        if (left.body) {
+            return subst(left.bound, right, left.body).eval_cbv(aggressive);
+        } else {
+            return new Lambda_app(left, right);
+        }
+    };
 }
 
 
@@ -269,112 +269,112 @@ function Lambda_app(left, right) {
 
 
 function Lambda_lam(variable, body) {
-       this.bound = variable;
-       this.body = body;
-       this.debruijn = function (seq) {
-               var new_seq = seq.slice(0);
-               new_seq.unshift(this.bound);
-               return new Db_lam(this.body.debruijn(new_seq));
-       };
-       this.to_string = function (as_atom) {
-               var base = "\\" + this.to_string_funct();
-               if (as_atom) {
-                       return "(" + base + ")";
-               } else {
-                       return base;
-               }
-       };
-       this.to_string_funct = function () {
-               if (this.body.to_string_funct) {
-                       return this.bound.to_string() + " " + this.body.to_string_funct();
-               } else {
-                       return this.bound.to_string() + ". " + this.body.to_string();
-               }
-       };
-       this.has_free = function (v) {
-               if (this.bound.equal(v)) {
-                       return [false, v];
-               } else {
-                       return this.body.has_free(v);
-               }
-       };
-       this.subst = function (v, new_term) {
-               function bump_tag(v1, v2) {
-                       var max;
-                       if (v1.tag > v2.tag) {
-                               max = v1.tag;
-                       } else {
-                               max = v2.tag;
-                       }
-                       return new Variable(v1.name, max + 1);
-               }
-               function bump_tag2(v1, v2) {
-                       if (v1.name !== v2.name) {
-                               return v1;
-                       } else {
-                               return bump_tag(v1, v2);
-                       }
-               }
-               if (this.bound.equal(v)) {
-                       return this;
-               } else {
-                       var res = free_in(this.bound, new_term);
+    this.bound = variable;
+    this.body = body;
+    this.debruijn = function (seq) {
+        var new_seq = seq.slice(0);
+        new_seq.unshift(this.bound);
+        return new Db_lam(this.body.debruijn(new_seq));
+    };
+    this.to_string = function (as_atom) {
+        var base = "\\" + this.to_string_funct();
+        if (as_atom) {
+            return "(" + base + ")";
+        } else {
+            return base;
+        }
+    };
+    this.to_string_funct = function () {
+        if (this.body.to_string_funct) {
+            return this.bound.to_string() + " " + this.body.to_string_funct();
+        } else {
+            return this.bound.to_string() + ". " + this.body.to_string();
+        }
+    };
+    this.has_free = function (v) {
+        if (this.bound.equal(v)) {
+            return [false, v];
+        } else {
+            return this.body.has_free(v);
+        }
+    };
+    this.subst = function (v, new_term) {
+        function bump_tag(v1, v2) {
+            var max;
+            if (v1.tag > v2.tag) {
+                max = v1.tag;
+            } else {
+                max = v2.tag;
+            }
+            return new Variable(v1.name, max + 1);
+        }
+        function bump_tag2(v1, v2) {
+            if (v1.name !== v2.name) {
+                return v1;
+            } else {
+                return bump_tag(v1, v2);
+            }
+        }
+        if (this.bound.equal(v)) {
+            return this;
+        } else {
+            var res = free_in(this.bound, new_term);
             // if x is free in the inserted term new_term, a capture is possible
-                       if (res) {
-                               // this.bound is free in new_term, need to alpha-convert
-                               var uniq_x = bump_tag2(bump_tag(this.bound, res), v);
-                               var res2 = free_in(uniq_x, this.body);
-                               if (res2) {
-                                       uniq_x = bump_tag(uniq_x, res2);
-                               }
-                               var body2 = subst(this.bound, new Lambda_var(uniq_x), this.body);
-                               return new Lambda_lam(uniq_x, subst(v, new_term, body2));
-                       } else {
-                               // this.bound not free in new_term, can substitute new_term for v without any captures
-                               return new Lambda_lam(this.bound, subst(v, new_term, this.body));
-                       }
-               }
-       };
-       this.check_eta = function () {
-               if (this.body.right && this.body.right.variable && this.bound.equal(this.body.right.variable) && !free_in(this.bound, this.body.left)) {
-                       return this.body.left;
-               } else {
-                       return this;
-               }
-       };
-       this.eval_loop = function (stack, eta) {
-               if (stack.length === 0) {
-                       var term = new Lambda_lam(this.bound, this.body.eval_loop([], eta));
-                       if (eta) {
-                               return term.check_eta();
-                       } else {
-                               return term;
-                       }
-               } else {
-                       var x = stack[0];
-                       var xs = stack.slice(1);
-                       return subst(this.bound, x, this.body).eval_loop(xs, eta);
-               }
-       };
-       this.eval_cbv = function (aggressive) {
-               if (aggressive) {
-                       return new Lambda_lam(this.bound, this.body.eval_cbv(aggressive));
-               } else {
-                       return this;
-               }
-       };
-       this.to_int = function (sofar) {
-               if (this.body.body && this.body.body.variable && this.body.bound.equal(this.body.body.variable)) {
-                       return 0 + sofar;
-               } else if (this.body.variable && this.bound.equal(this.body.variable)) {
-                       return 1 + sofar;
-               } else if (this.body.body && this.body.body.left && this.body.body.left.variable && this.bound.equal(this.body.body.left.variable)) {
-                       var new_int = new Lambda_lam(this.bound, new Lambda_lam(this.body.bound, this.body.body.right));
-                       return new_int.to_int(1 + sofar);
-               } else {
-                       return "not a church numeral";
-               }
-       };
+            if (res) {
+                // this.bound is free in new_term, need to alpha-convert
+                var uniq_x = bump_tag2(bump_tag(this.bound, res), v);
+                var res2 = free_in(uniq_x, this.body);
+                if (res2) {
+                    uniq_x = bump_tag(uniq_x, res2);
+                }
+                var body2 = subst(this.bound, new Lambda_var(uniq_x), this.body);
+                return new Lambda_lam(uniq_x, subst(v, new_term, body2));
+            } else {
+                // this.bound not free in new_term, can substitute new_term for v without any captures
+                return new Lambda_lam(this.bound, subst(v, new_term, this.body));
+            }
+        }
+    };
+    this.check_eta = function () {
+        if (this.body.right && this.body.right.variable && this.bound.equal(this.body.right.variable) && !free_in(this.bound, this.body.left)) {
+            return this.body.left;
+        } else {
+            return this;
+        }
+    };
+    this.eval_loop = function (stack, eta) {
+        if (stack.length === 0) {
+            var term = new Lambda_lam(this.bound, this.body.eval_loop([], eta));
+            if (eta) {
+                return term.check_eta();
+            } else {
+                return term;
+            }
+        } else {
+            var x = stack[0];
+            var xs = stack.slice(1);
+            return subst(this.bound, x, this.body).eval_loop(xs, eta);
+        }
+    };
+    this.eval_cbv = function (aggressive) {
+        if (aggressive) {
+            return new Lambda_lam(this.bound, this.body.eval_cbv(aggressive));
+        } else {
+            return this;
+        }
+    };
+    this.to_int = function (sofar) {
+        if (this.body.body && this.body.body.variable && this.body.bound.equal(this.body.body.variable)) {
+            return 0 + sofar;
+        } else if (this.body.variable && this.bound.equal(this.body.variable)) {
+            return 1 + sofar;
+        } else if (this.body.body && this.body.body.left && this.body.body.left.variable && this.bound.equal(this.body.body.left.variable)) {
+            var new_int = new Lambda_lam(this.bound, new Lambda_lam(this.body.bound, this.body.body.right));
+            return new_int.to_int(1 + sofar);
+        } else {
+            return "not a church numeral";
+        }
+    };
 }
 
 
@@ -385,29 +385,29 @@ function Lambda_lam(variable, body) {
 // cbv is 1: use call-by-value, don't descend inside lambda
 // cbv is 2: applicative order
 function reduce(expr, eta, cbv) {
-       if (cbv) {
-               return expr.eval_cbv(cbv > 1);
-       } else {
-               return expr.eval_loop([], eta);
-       }
+    if (cbv) {
+        return expr.eval_cbv(cbv > 1);
+    } else {
+        return expr.eval_loop([], eta);
+    }
 }
 
 function make_var(name) {
-       return new Variable(name);
+    return new Variable(name);
 }
 function make_app(aa, bb) {
-       return new Lambda_app(aa, bb);
+    return new Lambda_app(aa, bb);
 }
 function make_lam(a, aa) {
-       return new Lambda_lam(a, aa);
+    return new Lambda_lam(a, aa);
 }
 
 try {
-       if (console && console.debug) {
-               function print() {
-                       console.debug.apply(this, arguments);
-               }
-       }
+    if (console && console.debug) {
+        function print() {
+            console.debug.apply(this, arguments);
+        }
+    }
 } catch (e) {}
 
 
index fe079dc..dfa0640 100644 (file)
@@ -1,8 +1,17 @@
 // Parser for lambda with let written in Simplified JavaScript
-//             by Jim Pryor 2010-09-22
-//             Stripped down from Top Down Operator Precedence : parse.js
-//             http://javascript.crockford.com/tdop/index.html
-//             Douglas Crockford 2010-06-26
+//      by Jim Pryor 2010-09-22
+//      Stripped down from Top Down Operator Precedence : parse.js
+//      http://javascript.crockford.com/tdop/index.html
+//      Douglas Crockford 2010-06-26
+
+/*jslint onevar: false
+ */
+
+/*   members create, error, message, name, prototype, stringify, toSource,
+    toString, write
+*/
+
+/*global make_var, make_app, make_lam, Lambda_var */
 
 var make_parse = function () {
     var symbol_table = {};
@@ -24,12 +33,12 @@ var make_parse = function () {
         v = t.value;
         a = t.type;
         if (a === "name") {
-                       o = symbol_table[v];
-                       if (o && typeof o !== 'function' ) {
-                               a = "keyword";
-                       } else {
-                               o = symbol_table["(name)"];
-                       }
+            o = symbol_table[v];
+            if (o && typeof o !== 'function') {
+                a = "keyword";
+            } else {
+                o = symbol_table["(name)"];
+            }
         } else if (a ===  "number") {
             o = symbol_table["(literal)"];
             a = "literal";
@@ -38,7 +47,7 @@ var make_parse = function () {
             if (!o) {
                 t.error("Unknown operator.");
             }
-                       a = "keyword";
+            a = "keyword";
         } else {
             t.error("Unexpected token.");
         }
@@ -53,7 +62,7 @@ var make_parse = function () {
     var original_symbol = {
         handler: function () {
             this.error("Undefined.");
-        },
+        }
     };
 
     var symbol = function (id) {
@@ -80,171 +89,171 @@ var make_parse = function () {
         return this;
     };
 
-       var var_table = {};
-       var name_table = {};
-
-       var name_handler = function () {
-               var n = name_table[this.value];
-               if (!n) {
-                       n = make_var(this.value);
-                       var_table[this.value] = n;
-                       n = new Lambda_var(n);
-                       name_table[this.value] = n;
-               }
-               if (this.first) {
-                       return make_app(this.first.handler(), n);
-               } else {
-                       return n;
-               }
-       };
+    var var_table = {};
+    var name_table = {};
 
-       var branch_handler = function () {
-               var n = this.second.handler();
-               if (this.first) {
-                       return make_app(this.first.handler(), n);
-               } else {
-                       return n;
-               }
-       };
+    var name_handler = function () {
+        var n = name_table[this.value];
+        if (!n) {
+            n = make_var(this.value);
+            var_table[this.value] = n;
+            n = new Lambda_var(n);
+            name_table[this.value] = n;
+        }
+        if (this.first) {
+            return make_app(this.first.handler(), n);
+        } else {
+            return n;
+        }
+    };
 
-       var lambda_handler = function () {
-               var body = this.second.handler();
-               var n, v;
-               while (this.first.length) {
-                       n = this.first.pop().value;
-                       v = var_table[n];
-                       if (!v) {
-                               v = make_var(n);
-                               var_table[n] = v;
-                               name_table[n] = new Lambda_var(v);
-                       }
-                       body = make_lam(v, body);
-               }
-               return body;
-       };
+    var branch_handler = function () {
+        var n = this.second.handler();
+        if (this.first) {
+            return make_app(this.first.handler(), n);
+        } else {
+            return n;
+        }
+    };
+
+    var lambda_handler = function () {
+        var body = this.second.handler();
+        var n, v;
+        while (this.first.length) {
+            n = this.first.pop().value;
+            v = var_table[n];
+            if (!v) {
+                v = make_var(n);
+                var_table[n] = v;
+                name_table[n] = new Lambda_var(v);
+            }
+            body = make_lam(v, body);
+        }
+        return body;
+    };
 
     symbol("(end)");
-       symbol("(name)").handler = name_handler;
+    symbol("(name)").handler = name_handler;
     symbol("(literal)").handler = itself;
-       symbol("let").handler = lambda_handler;
-       symbol("=").handler = branch_handler;
-       symbol("in");
-       symbol(")").handler = branch_handler;
-       symbol("(");
-       symbol("\\").handler = lambda_handler;
-       symbol("lambda").handler = lambda_handler;
-       symbol(".");
-
-       var expression = function (in_let) {
-               var t, n;
-               if (token.id === "\\" || token.id === "lambda") {
-                       token.value = "lambda";
-                       t = token;
-                       advance();
-                       n = token;
-                       if (n.arity !== "name") {
-                               n.error("Expected a variable name.");
-                       }
-                       advance();
-                       if (token.id === "(") {
-                               t.first = [n];
-                               advance();
-                               t.second = expression(false);
-                               advance(")");
-                               return t;
-                       } else {
-                               t.first = [];
-                               while (token.arity === "name") {
-                                       t.first.push(n);
-                                       n = token;
-                                       advance();
-                               }
-                               if (token.id === ".") {
-                                       t.first.push(n);
-                                       advance();
-                                       t.second = expression(in_let);
-                               } else if (t.first.length === 1) {
-                                       t.second = n;
-                               } else {
-                                       t.first.push(n);
-                                       t.error("Can't parse lambda abstract.");
-                               }
-                               return t;
-                       };
-               } else {
-                       n = null;
-                       while (token.id === "(") {
-                               advance();
-                               t = expression(false);
-                               token.first = n;
-                               token.second = t;
-                               n = token;
-                               advance(")");
-                               if (in_let && token.id === "let" || token.id === "(end)" || token.id === ")") {
-                                       return n;
-                               }
-                       }
-                       if (token.arity != "name") {
-                               token.error("Expected a variable name.");
-                       }
-                       token.first = n;
-                       n = token;
-                       advance();
-                       while (true) {
-                               if (in_let && token.id === "in" || token.id === "(end)" || token.id === ")") {
-                                       return n;
-                               } else if (token.id === "(") {
-                                       advance();
-                                       t = expression(false);
-                                       token.first = n;
-                                       token.second = t;
-                                       n = token;
-                                       advance(")");
-                               } else {
-                                       if (token.arity != "name") {
-                                               token.error("Expected a variable name.");
-                                       }
-                                       token.first = n;
-                                       n = token;
-                                       advance();
-                               }
-                       }
-               }
-       }
+    symbol("let").handler = lambda_handler;
+    symbol("=").handler = branch_handler;
+    symbol("in");
+    symbol(")").handler = branch_handler;
+    symbol("(");
+    symbol("\\").handler = lambda_handler;
+    symbol("lambda").handler = lambda_handler;
+    symbol(".");
+
+    var expression = function (in_let) {
+        var t, n;
+        if (token.id === "\\" || token.id === "lambda") {
+            token.value = "lambda";
+            t = token;
+            advance();
+            n = token;
+            if (n.arity !== "name") {
+                n.error("Expected a variable name.");
+            }
+            advance();
+            if (token.id === "(") {
+                t.first = [n];
+                advance();
+                t.second = expression(false);
+                advance(")");
+                return t;
+            } else {
+                t.first = [];
+                while (token.arity === "name") {
+                    t.first.push(n);
+                    n = token;
+                    advance();
+                }
+                if (token.id === ".") {
+                    t.first.push(n);
+                    advance();
+                    t.second = expression(in_let);
+                } else if (t.first.length === 1) {
+                    t.second = n;
+                } else {
+                    t.first.push(n);
+                    t.error("Can't parse lambda abstract.");
+                }
+                return t;
+            }
+        } else {
+            n = null;
+            while (token.id === "(") {
+                advance();
+                t = expression(false);
+                token.first = n;
+                token.second = t;
+                n = token;
+                advance(")");
+                if (in_let && token.id === "let" || token.id === "(end)" || token.id === ")") {
+                    return n;
+                }
+            }
+            if (token.arity !== "name") {
+                token.error("Expected a variable name.");
+            }
+            token.first = n;
+            n = token;
+            advance();
+            while (true) {
+                if (in_let && token.id === "in" || token.id === "(end)" || token.id === ")") {
+                    return n;
+                } else if (token.id === "(") {
+                    advance();
+                    t = expression(false);
+                    token.first = n;
+                    token.second = t;
+                    n = token;
+                    advance(")");
+                } else {
+                    if (token.arity !== "name") {
+                        token.error("Expected a variable name.");
+                    }
+                    token.first = n;
+                    n = token;
+                    advance();
+                }
+            }
+        }
+       };
 
     return function (source) {
-               tokens = source.tokens();
+        tokens = source.tokens();
         token_nr = 0;
         advance();
-               
-               // let n = c in b
-               // (\n. b) c
-
-               var t = null, eq, c, base = {};
-               var target = base;
-
-               while (token.id == "let") {
-                       t = token;
-                       advance();
-                       if (token.arity !== "name") {
-                               token.error("Expected a variable name.");
-                       }
-                       t.first = [token];
-                       advance();
-                       eq = token; // token.id === "="
-                       advance("=");
-                       c = expression(true);
-                       c.first = eq;
-                       eq.second = t;
-                       target.second = c;
-                       target = t;
-                       advance("in");
-               }
-       
-               target.second = expression(false);
+        
+        // let n = c in b
+        // (\n. b) c
+
+        var t = null, eq, c, base = {};
+        var target = base;
+
+        while (token.id === "let") {
+            t = token;
+            advance();
+            if (token.arity !== "name") {
+                token.error("Expected a variable name.");
+            }
+            t.first = [token];
+            advance();
+            eq = token; // token.id === "="
+            advance("=");
+            c = expression(true);
+            c.first = eq;
+            eq.second = t;
+            target.second = c;
+            target = t;
+            advance("in");
+        }
+    
+        target.second = expression(false);
 
         advance("(end)");
-               return base.second;
+        return base.second;
     };
 
 };
index 98277a0..b83c36d 100644 (file)
@@ -1,25 +1,26 @@
 // Based on tokens.js
-//             2009-05-17
-//             (c) 2006 Douglas Crockford
+//      2009-05-17
+//      (c) 2006 Douglas Crockford
 
-//             Produce an array of simple token objects from a string.
-//             A simple token object contains these members:
-//                  type: 'name', 'string', 'number', 'operator'
-//                  value: string or number value of the token
-//                  from: index of first character of the token
-//                  to: index of the last character + 1
+//      Produce an array of simple token objects from a string.
+//      A simple token object contains these members:
+//           type: 'name', 'string', 'number', 'operator'
+//           value: string or number value of the token
+//           from: index of first character of the token
+//           to: index of the last character + 1
 
-//             Comments of the ; type are ignored.
-
-//             Operators are by default single characters. Multicharacter
-//             operators can be made by supplying a string of prefix and
-//             suffix characters.
-//             characters. For example,
-//                  '<>+-&', '=>&:'
-//             will match any of these:
-//                  <=  >>  >>>  <>  >=  +: -: &: &&: &&
+//      Comments of the ; type are ignored.
 
+//      Operators are by default single characters. Multicharacter
+//      operators can be made by supplying a string of prefix and
+//      suffix characters.
+//      characters. For example,
+//           '<>+-&', '=>&:'
+//      will match any of these:
+//           <=  >>  >>>  <>  >=  +: -: &: &&: &&
 
+/*jslint onevar: false
+ */
 
 String.prototype.tokens = function (prefix, suffix) {
     var c;                      // The current character.
@@ -53,10 +54,10 @@ String.prototype.tokens = function (prefix, suffix) {
 // If prefix and suffix strings are not provided, supply defaults.
 
     if (typeof prefix !== 'string') {
-               prefix = '';
+        prefix = '';
     }
     if (typeof suffix !== 'string') {
-               suffix = '';
+        suffix = '';
     }
 
 
@@ -111,7 +112,7 @@ String.prototype.tokens = function (prefix, suffix) {
 
 // Make sure the next character is not a letter.
 
-            if (c >= 'a' && c <= 'z' || c >= 'A' && c <= 'Z' || c == '_') {
+            if (c >= 'a' && c <= 'z' || c >= 'A' && c <= 'Z' || c === '_') {
                 str += c;
                 i += 1;
                 make('number', str).error("Bad number");
@@ -129,7 +130,7 @@ String.prototype.tokens = function (prefix, suffix) {
 
 // comment.
 
-               } else if (c === ';') {
+        } else if (c === ';') {
             for (;;) {
                 c = this.charAt(i);
                 if (c === '\n' || c === '\r' || c === '') {
index afcf926..6d0866c 100644 (file)
@@ -39,9 +39,9 @@ let and = \l r. l r false in
 </textarea>
 <input id="PARSE" value="Normalize" type="button">
 <noscript><p>You may not see it because you have JavaScript turned off. Uffff!</p></noscript>
+<script src="code/lambda.js"></script>
 <script src="code/tokens.js"></script>
 <script src="code/parse.js"></script>
-<script src="code/lambda.js"></script>
 <script src="code/json2.js"></script>
 <pre id="OUTPUT">
 </pre>