4b684f4eeb22d9ff3da97828003fa732d5fdcd16
1 // Basic data structure, essentially a LISP/Scheme-like cons
2 // pre-terminal nodes are expected to be of the form new cons(null, "string")
3 function cons(car, cdr) {
4   this.car = car;
5   this.cdr = cdr;
6 }
8 // takes a stack of symbols, returns a pair: a tree and the remaining symbols
9 function fold(split) {
10   if (split == null) return (new cons (null, null));
11   if (split.length == 0) return (new cons (null, null));
12   var token = split.shift();
13   if (token == ")") return (new cons (null, split));
14   var next = fold(split);
15   if (token == "(") {
16     var nextnext = fold(next.cdr);
17     return (new cons ((new cons (next.car, nextnext.car)),
18                       nextnext.cdr));
19   }
20   return (new cons ((new cons ((new cons (null, token)),
21                                next.car)),
22                     next.cdr))
23 }
25 // substitute arg in for v in tree
26 function sub(tree, v, arg) {
27   if (tree == null) return (null);
28   if (tree.car == null) if (tree.cdr == v) return (arg);
29   if (tree.car == null) return (tree);
31   // perform alpha reduction to prevent variable collision
32   if (isBindingForm(tree))
33     return (new cons (tree.car,
34                       sub(sub(tree.cdr,         // inner sub = alpha reduc.
35                               tree.cdr.car.cdr,
36                               fresh(tree.cdr.car.cdr)),
37                           v,
38                           arg)));
40   return (new cons ((sub (tree.car, v, arg)),
41                     (sub (tree.cdr, v, arg))))
42 }
44 // Guaranteed unique for each call as long as string is not empty.
45 var i = 0;
46 function fresh(string) {
47   i = i+1;
48   if (typeof(string) != "string") return (string);
49   return (new cons (null,
50                     string.substring(0,1) + (i).toString()));
51 }
53 // Keep reducing until there is no more change
54 function fixedPoint (tree) {
55   var t2 = reduce(tree);
56   if (treeToString(tree) == treeToString(t2)) return (tree);
57   return (fixedPoint (t2));
58 }
60 // Reduce all the arguments, then try to do beta conversion on the whole
61 function reduce(tree) {
62   if (tree == null) return (tree);
63   if (typeof(tree) == "string") return (tree);
64   return (convert (new cons (reduce (tree.car), mapReduce (tree.cdr))));
65 }
67 // Reduce all the arguments in a list
68 function mapReduce(tree) {
69   if (tree == null) return (tree);
70   if (tree.car == null) return (tree);
71   return (new cons (reduce (tree.car), mapReduce(tree.cdr )));
72 }
74 // If the list is of the form ((lambda var body) arg), do beta reduc.
75 function convert(tree) {
76     if (isLet(tree)) {
77       return (sub(tree.cdr.car, tree.car.cdr.car.cdr, tree.car.cdr.cdr.car));}
78     else
79       if (isConvertable(tree)) {
80         return (sub(tree.car.cdr.cdr.car, tree.car.cdr.car.cdr, tree.cdr.car));}
81       else return(tree);
82
84 // Is of form ((let var arg) body)?
85 function isLet(tree) {
86   if (tree == null) return (false);
87   if (!(isBindingForm(tree.car))) return (false);
88   if (tree.car.car.cdr != "let") return (false);
89   if (tree.cdr == null) return (false);
90   if (tree.cdr.car == null) return (false);
91   return(true);
92 }
94 // Is of form ((lambda var body) arg)?
95 function isConvertable(tree) {
96   if (tree == null) return (false);
97   if (!(isBindingForm(tree.car))) return (false);
98   if (tree.car.car.cdr != "lambda") return (false);
99   if (tree.cdr == null) return (false);
100   if (tree.cdr.car == null) return (false);
101   return(true);
102 }
104 // Is of form (lambda var body)?
105 function isBindingForm(tree) {
106   if (tree == null) return (false);
107   if (tree.car == null) return (false);
108   if (tree.car.car != null) return (false);
109   if ((tree.car.cdr != "lambda")
110       && (tree.car.cdr != "let")
111       && (tree.car.cdr != "exists")
112       && (tree.car.cdr != "forall")
113       && (tree.car.cdr != "\u03BB")
114       && (tree.car.cdr != "\u2200")
115       && (tree.car.cdr != "\u2203")
116      )
117     return (false);
118   if (tree.car.cdr == null) return (false);
119   if (tree.cdr.car == null) return (false);
120   if (tree.cdr.car.car != null) return (false);
121   if (tree.cdr.cdr == null) return (false);
122   return (true);
123 }
125 function treeToString(tree) {
126   if (tree == null) return ("")
127   if (tree.car == null) return (tree.cdr)
128   if ((tree.car).car == null)
129     return (treeToString(tree.car) + " " + treeToString(tree.cdr))
130   return ("(" + treeToString(tree.car) + ")" + treeToString(tree.cdr))
131 }
133 // use this instead of treeToString if you want to see the full structure
134 function treeToStringRaw(tree) {
135   if (tree == null) return ("@")
136   if (typeof(tree) == "string") return (tree);
137   return ("(" + treeToStringRaw(tree.car) + "." +
138                 treeToStringRaw(tree.cdr) + ")")
139 }
141 // Make sure each paren will count as a separate token
142 function stringToTree(input) {
143   input = input.replace(/let/g, " ( ( let ");
144   input = input.replace(/=/g, " ");
145   input = input.replace(/in/g, " ) ");
146   input = input.replace(/\(/g, " ( ");
147   input = input.replace(/\)/g, " ) ");
148   input = input.replace(/\^/g, " ^ ");
149   input = input.replace(/[\\]/g, " lambda ");
150   input = input.replace(/\u03BB/g, "lambda");
151   return ((fold(input.split(/[ \f\n\r\t\v]+/))).car)
152 }
154 // Adjust spaces to print pretty
155 function formatTree(tree) {
156   output = treeToString (tree);
157   output = output.replace(/^[ \f\n\r\t\v]+/, "");
158   output = output.replace(/[ \f\n\r\t\v]+\$/, "");
159   output = output.replace(/[ \f\n\r\t\v]+\)/g, ")");
160   output = output.replace(/\)([^)(])/g, ") \$1");
161 //  output = output.replace(/lambda/g, "\u03BB");
162 //  output = output.replace(/exists/g, "\u2203");
163 //  output = output.replace(/forall/g, "\u2200");
164   return (output)
165 }
167 function mytry(form) {
168   i = 0;
169   form.result.value = formatTree(fixedPoint(stringToTree(form.input.value)));
170 }