/*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 */


// 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;
}

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;
}

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);
        }
    };
}

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);
        }
    };
}


// lambda terms
// substitution and normal-order evaluator based on Haskell version by Oleg Kisleyov
// 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);
		var s = this.name;
		for (var count = 0; count < this.tag; count += 1) {
			s += "'";
		}
		return s;
    };
    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];
}

function subst(v, new_term, expr) {
    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([]));
}

function contains(expr1, expr2) {
    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);
//             }
			var res = left, x;
			while (stack.length) {
				x = stack.shift();
				// res = new Lambda_app(res, x.eval_loop([], eta));
				res = new Lambda_app(res, reduce(x, eta, false));
			}
			return res;
        }
        // return unwind(this, stack);
		// trampoline to, args
		return [null, 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);
		// trampoline to, args
		return [this.left, 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);
        }
    };
}


//     (* 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 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);
            // 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));
			var term = new Lambda_lam(this.bound, reduce(this.body, eta, false));
			if (eta) {
				return [null, term.check_eta()];
			} else {
				return [null, term];
			}
        } else {
            var x = stack[0];
            var xs = stack.slice(1);
            // return subst(this.bound, x, this.body).eval_loop(xs, eta);
			// trampoline to, args
			return [subst(this.bound, x, this.body), 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";
//         }
		var res = 0, s = this.bound, z, cursor;
		if (this.body.variable && s.equal(this.body.variable)) {
			return 1;
		} else if (this.body.bound) {
			z = this.body.bound;
			cursor = this.body.body;
			while (cursor.left && cursor.left.variable && s.equal(cursor.left.variable)) {
				res += 1;
				cursor = cursor.right;
			}
			if (cursor.variable && z.equal(cursor.variable)) {
				return res;
			}
		}
		return "not a church numeral";
    };
}



///////////////////////////////////////////////////////////////////////////////////

// cbv is false: use call-by-name
// 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);
		var to_eval = expr, res = [[], eta];
		while (to_eval !== null) {
			res = to_eval.eval_loop.apply(to_eval, res);
			to_eval = res.shift();
		}
		return res[0];
    }
}

function make_var(name) {
    return new Variable(name);
}
function make_app(aa, bb) {
    return new Lambda_app(aa, bb);
}
function make_lam(a, aa) {
    return new Lambda_lam(a, aa);
}

try {
    if (console && console.debug) {
        function print() {
            console.debug.apply(this, arguments);
        }
    }
} catch (e) {}

/*
let true = K in
let false = \x y. y in
let and = \l r. l r false in
let or = \l r. l true r in
let pair = \u v f. f u v in
let triple = \u v w f. f u v w in
let succ = \n s z. s (n s z) in
let pred = \n s z. n (\u v. v (u s)) (K z) I in
let ifzero = \n. n (\u v. v (u succ)) (K 0) (\n withp whenz. withp n) in
let add = \m n. n succ m in
let mul = \m n. n (\z. add m z) 0 in
let mul = \m n s. m (n s) in
let sub = (\mzero msucc mtail. \m n. n mtail (m msucc mzero) true) (pair 0 I) (\d. d (\a b. pair (succ a) (K d))) (\d. d false d) in
let min = \m n. sub m (sub m n) in
let max = \m n. add n (sub m n) in
let lt = (\mzero msucc mtail. \n m. n mtail (m msucc mzero) true (\x. true) false) (pair 0 I) (\d. d (\a b. pair (succ a) (K d))) (\d. d false d) in
let leq = (\mzero msucc mtail. \m n. n mtail (m msucc mzero) true (\x. false) true) (pair 0 I) (\d. d (\a b. pair (succ a) (K d))) (\d. d false d) in
let eq = (\mzero msucc mtail. \m n. n mtail (m msucc mzero) true (\x. false) true) (pair 0 (K (pair 1 I))) (\d. d (\a b. pair (succ a) (K d))) (\d. d false d) in
let divmod = (\mzero msucc mtail. \n divisor.
               (\dhead. n (mtail dhead) (\sel. dhead (sel 0 0)))
              (divisor msucc mzero (\a b c. c x))
              (\d m a b c. pair d m) )
          (triple succ (K 0) I)
          (\d. triple I succ (K d))
          (\dhead d. d (\dz mz df mf drest sel. drest dhead (sel (df dz) (mf mz)))) in
let div = \n d. divmod n d true in
let mod = \n d. divmod n d false in
let Y = \f. (\y. f(y y)) (\y. f(y y)) in
let Z = (\u f. f(u u f)) (\u f. f(u u f)) in
let fact = \y. y (\f n. ifzero n (\p. mul n (f p)) 1) in
fact Z 3
*/



// // Basic data structure, essentially a LISP/Scheme-like cons
// // pre-terminal nodes are expected to be of the form new cons(null, "string")
// function cons(car, cdr) {
//   this.car = car;
//   this.cdr = cdr;
// }

// // takes a stack of symbols, returns a pair: a tree and the remaining symbols
// function parse(split) {
//   if (split == null) return (new cons (null, null));
//   if (split.length == 0) return (new cons (null, null));
//   var token = split.shift();
//   if (token == ")") return (new cons (null, split));
//   var next = parse(split);
//   if (token == "(") {
//     var nextnext = parse(next.cdr);
//     return (new cons ((new cons (next.car, nextnext.car)),
//                       nextnext.cdr));
//   }
//   return (new cons ((new cons ((new cons (null, token)),
//                                next.car)),
//                     next.cdr))
// }

// // substitute arg in for v in tree
// function sub(tree, v, arg) {
//   if (tree == null) return (null);
//   if (tree.car == null) if (tree.cdr == v) return (arg);
//   if (tree.car == null) return (tree);

//   // perform alpha reduction to prevent variable collision
//   if (isBindingForm(tree)) 
//     return (new cons (tree.car, 
//                       sub(sub(tree.cdr,         // inner sub = alpha reduc.
//                               tree.cdr.car.cdr, 
//                               fresh(tree.cdr.car.cdr)),
//                           v,
//                           arg)));

//   return (new cons ((sub (tree.car, v, arg)),
//                     (sub (tree.cdr, v, arg))))
// }

// // Guaranteed unique for each call as long as string is not empty.
// var i = 0;
// function fresh(string) {
//   i = i+1;
//   if (typeof(string) != "string") return (string);
//   return (new cons (null,  
//                     string.substring(0,1) + (i).toString()));
// }

// // Keep reducing until there is no more change
// function fixedPoint (tree) {
//   var t2 = reduce(tree);
//   if (treeToString(tree) == treeToString(t2)) return (tree);
//   return (fixedPoint (t2));
// }

// // Reduce all the arguments, then try to do beta conversion on the whole
// function reduce(tree) {
//   if (tree == null) return (tree);
//   if (typeof(tree) == "string") return (tree);
//   return (convert (new cons (reduce (tree.car), mapReduce (tree.cdr))));
// }

// // Reduce all the arguments in a list
// function mapReduce(tree) {
//   if (tree == null) return (tree);
//   if (tree.car == null) return (tree);
//   return (new cons (reduce (tree.car), mapReduce(tree.cdr )));
// }

// // If the list is of the form ((lambda var body) arg), do beta reduc.
// function convert(tree) {
//     if (isLet(tree)) {
//       return (sub(tree.cdr.car, tree.car.cdr.car.cdr, tree.car.cdr.cdr.car));}
//     else 
//       if (isConvertable(tree)) {
//         return (sub(tree.car.cdr.cdr.car, tree.car.cdr.car.cdr, tree.cdr.car));}
//       else return(tree);
// } 

// // Is of form ((let var arg) body)?
// function isLet(tree) {
//   if (tree == null) return (false);
//   if (!(isBindingForm(tree.car))) return (false);
//   if (tree.car.car.cdr != "let") return (false);
//   if (tree.cdr == null) return (false);
//   if (tree.cdr.car == null) return (false);
//   return(true);
// }  

// // Is of form ((lambda var body) arg)?
// function isConvertable(tree) {
//   if (tree == null) return (false);
//   if (!(isBindingForm(tree.car))) return (false);
//   if (tree.car.car.cdr != "lambda") return (false);
//   if (tree.cdr == null) return (false);
//   if (tree.cdr.car == null) return (false);
//   return(true);
// }  

// // Is of form (lambda var body)?
// function isBindingForm(tree) {
//   if (tree == null) return (false);
//   if (tree.car == null) return (false);
//   if (tree.car.car != null) return (false);
//   if ((tree.car.cdr != "lambda") 
//       && (tree.car.cdr != "let")
//       && (tree.car.cdr != "exists")
//       && (tree.car.cdr != "forall")
//       && (tree.car.cdr != "\u03BB")
//       && (tree.car.cdr != "\u2200")
//       && (tree.car.cdr != "\u2203")
//      )
//     return (false);
//   if (tree.car.cdr == null) return (false);
//   if (tree.cdr.car == null) return (false);
//   if (tree.cdr.car.car != null) return (false);
//   if (tree.cdr.cdr == null) return (false);
//   return (true);
// }

// function treeToString(tree) {
//   if (tree == null) return ("")
//   if (tree.car == null) return (tree.cdr)
//   if ((tree.car).car == null) 
//     return (treeToString(tree.car) + " " + treeToString(tree.cdr))
//   return ("(" + treeToString(tree.car) + ")" + treeToString(tree.cdr))
// }

// // use this instead of treeToString if you want to see the full structure
// function treeToStringRaw(tree) {
//   if (tree == null) return ("@")
//   if (typeof(tree) == "string") return (tree);
//   return ("(" + treeToStringRaw(tree.car) + "." + 
//                 treeToStringRaw(tree.cdr) + ")")
// }

// // Make sure each paren will count as a separate token
// function stringToTree(input) {
//   input = input.replace(/let/g, " ( ( let ");
//   input = input.replace(/=/g, " ");
//   input = input.replace(/in/g, " ) ");
//   input = input.replace(/\(/g, " ( ");
//   input = input.replace(/\)/g, " ) ");
//   input = input.replace(/;.*\n/g," ");
//   input = input.replace(/\^/g, " ^ ");
//   input = input.replace(/[\\]/g, " lambda ");
//   input = input.replace(/\u03BB/g, " lambda ");
//   return ((parse(input.split(/[ \f\n\r\t\v]+/))).car)
// }

// // Adjust spaces to print pretty
// function formatTree(tree) {
//   output = treeToStringRaw (tree);
//   output = output.replace(/^[ \f\n\r\t\v]+/, "");
//   output = output.replace(/[ \f\n\r\t\v]+$/, "");
//   output = output.replace(/[ \f\n\r\t\v]+\)/g, ")");
//   output = output.replace(/\)([^)(])/g, ") $1");
//   output = output.replace(/lambda/g, "\\");
// //  output = output.replace(/lambda/g, "\u03BB");
// //  output = output.replace(/exists/g, "\u2203");
// //  output = output.replace(/forall/g, "\u2200");
//   return (output)
// }

// function mytry(form) { 
//   i = 0;
//   form.result.value = formatTree((stringToTree(form.input.value)));
//   // form.result.value = formatTree(fixedPoint(stringToTree(form.input.value)));
// }