Syntax editor: internal optimizations by pre-computing certain stuff

3 files changed, 83 insertions, 106 deletions

diff --git a/src/www/syntax-editor/README.md b/src/www/syntax-editor/README.md
index 19e408b1a..ef9758e71 100644
--- a/src/www/syntax-editor/README.md
+++ b/src/www/syntax-editor/README.md
@@ -38,11 +38,10 @@ See `editor.html` and `editor_online.js`.
 - Wrap a subtree
 - Compatibility with grammars with dependent category types
 - Clicking on tokens to select tree node
-- Use local caching
 - Clipboard of trees
 - Usage of printnames
 - Enter string/float/int literals
 - more prominence to Disamb-linearizations
-- ambiguity: (optionally) parse all the resulting linearizations/variants and point out those which are ambiguous
-- add undo/redo (or back/forward) navigation
-- structure fridge magnets some more (eg newline before the magnet whose first letter is different)
+- show all resulting linearizations/variants
+- undo/redo (or back/forward) navigation
+- structure fridge magnets more (eg newline before the magnet whose first letter is different)
diff --git a/src/www/syntax-editor/ast.js b/src/www/syntax-editor/ast.js
index 178bc920a..20e0c7019 100644
--- a/src/www/syntax-editor/ast.js
+++ b/src/www/syntax-editor/ast.js
@@ -40,9 +40,9 @@ function NodeID(x) {
 /* --- Abstract Syntax Tree (with state)------------------------------------- */
 
 function ASTNode(data) {
-    for(var d in data) this[d]=data[d];
+    for (var d in data) this[d]=data[d];
     this.children = [];
-    for (c in data.children) {
+    for (var c in data.children) {
         this.children.push( new ASTNode(data.children[c]) );
     }
     this.hasChildren = function(){
@@ -53,7 +53,7 @@ function ASTNode(data) {
     this.traverse = function(f) {
         function visit(node) {
             f(node);
-            for (i in node.children) {
+            for (var i in node.children) {
                 visit(node.children[i]);
             }
         }
@@ -76,41 +76,49 @@ function AST(fun, cat) {
 
     this.root = newNode(fun, cat);
     
-    this.current = new NodeID(); // current id in tree
+    this.currentID = new NodeID(); // current id in tree
+    this.currentNode = this.root; // current node in tree
 
-    this.getCurrent = function() {
-        return this.find(this.current);
+    this.getCurrentNode = function() {
+        return this.currentNode;
     }
+    this.getCurrentID = function() {
+        return this.currentID;
+    }
+    this.setCurrentID = function(id) {
+        this.currentID = id; // new new NodeID(id);
+        this.currentNode = this.find(this.currentID);
+    }
+
     this.getFun = function() {
-        return this.find(this.current).fun;
+        return this.currentNode.fun;
     }
     this.setFun = function(f) {
-        this.find(this.current).fun = f;
+        this.currentNode.fun = f;
     }
     this.getCat = function() {
-        return this.find(this.current).cat;
+        return this.currentNode.cat;
     }
     this.setCat = function(c) {
-        this.find(this.current).cat = c;
+        this.currentNode.cat = c;
     }
 
     // Add a single type dependency at current node
     this.addDep = function(k, type) {
         // Add unassigned type variable to current
-        var cur = this.getCurrent();
-        cur.deps[k] = null;
+        this.currentNode.deps[k] = null;
 
         // Add actual type dep node
         var node = newNode(k, type);
         node.depid = k; // links to dep in parent
-        this._add(this.current, node);
+        this._add(this.currentID, node);
         return node;
     }
 
     // Add a single fun at current node
     this.add = function(fun, cat) {
         var node = newNode(fun,cat);
-        this._add(this.current, node);
+        this._add(this.currentID, node);
         return node;
     }
 
@@ -122,30 +130,30 @@ function AST(fun, cat) {
 
     // Determine if current node is writable (empty/no children)
     this.is_writable=function() {
-        var current = this.getCurrent();
-        var blank = current.fun == null || current.children.length == 0;
+        var cn = this.currentNode;
+        var blank = cn.fun == null || cn.children.length == 0;
         return blank;
     }
 
     // Determine if a fun would fit in a current hole
     this.fits_in_place=function(typeobj) {
-        var current = this.getCurrent();
+        var cn = this.currentNode;
 
         var inplace = false;
-        if (typeobj.args.length == current.children.length) {
+        if (typeobj.args.length == cn.children.length) {
             var matches = 0;
             for (var i in typeobj.args) {
-                if (typeobj.args[i] == current.children[i].cat)
+                if (typeobj.args[i] == cn.children[i].cat)
                     matches++;
             }
-            inplace = matches == current.children.length;
+            inplace = matches == cn.children.length;
         }
         return inplace;
     }
 
     // Set entire subtree at current node
     this.setSubtree = function(node) {
-        this._setSubtree(this.current, node);
+        this._setSubtree(this.currentID, node);
     }
     
     // set tree at given id
@@ -185,24 +193,24 @@ function AST(fun, cat) {
     
     // Clear children of current node
     this.removeChildren = function() {
-        this.find(this.current).children = [];
+        this.currentNode.children = [];
     }
 
     // Move current ID to next hole
     this.toNextHole = function() {
-        var id = new NodeID(this.current);
+        var id = new NodeID(this.currentID);
         
         // loop until we're at top
         while (id.get().length > 0) {
             var node = this.find(id);
 
             // first check children
-            for (i in node.children) {
+            for (var i in node.children) {
                 var child = node.children[i];
                 if (!child.fun) {
                     var newid = new NodeID(id);
                     newid.add(i);
-                    this.current = newid;
+                    this.setCurrentID(newid);
                     return;
                 }
             }
@@ -213,15 +221,18 @@ function AST(fun, cat) {
     }
 
     // Return parent of current node
-    this.getParent = function(i) {
-        var parent_id = this.current.clone();
+    this.getParent = function() {
+        var parent_id = this.currentID.clone();
         parent_id.get().pop();
         return this.find(parent_id);
     }
 
     // Move current id to child number i
     this.toChild = function(i) {
-        this.current.add(i);
+        if (i < this.currentNode.children.length) {
+            this.currentID.add(i);
+            this.currentNode = this.currentNode.children[i];
+        }
     }
 
     // generic HOF for traversing tree
@@ -231,7 +242,7 @@ function AST(fun, cat) {
     this.traverse = function(f) {
         function visit(id, node) {
             f(node);
-            for (i in node.children) {
+            for (var i in node.children) {
                 var newid = new NodeID(id);
                 newid.add(parseInt(i));
                 visit(newid, node.children[i]);
@@ -248,7 +259,7 @@ function AST(fun, cat) {
             if (!node.hasChildren())
 //            if (node.children.length == 0)
                 return;
-            for (i in node.children) {
+            for (var i in node.children) {
                 s += " (";
                 visit(node.children[i]);
                 s += ")";
diff --git a/src/www/syntax-editor/editor.js b/src/www/syntax-editor/editor.js
index 355c44082..fc60443ef 100644
--- a/src/www/syntax-editor/editor.js
+++ b/src/www/syntax-editor/editor.js
@@ -52,7 +52,7 @@ function Editor(gm,opts) {
             format: "json"
         };
         var cont = function(data){
-            t.grammar_constructors = data;
+            t.process_grammar_constructors(data);
             t.start_fresh();
         };
         t.server.browse(args, cont);
@@ -90,6 +90,30 @@ function Editor(gm,opts) {
 
 }
 
+/* --- Pre-processed grammar information ------------------------------------ */
+
+Editor.prototype.process_grammar_constructors=function(data) {
+    var t = this;
+    t.grammar_constructors=data;
+    for (var fun in t.grammar_constructors.funs) {
+        var def = t.grammar_constructors.funs[fun].def;
+        var typeobj = AST.parse_type_signature(def);
+        t.grammar_constructors.funs[fun] = typeobj;
+    }
+}
+
+// Look up information for a category
+Editor.prototype.lookup_cat = function(cat) {
+    var t = this;
+    return t.grammar_constructors.cats[cat];
+}
+
+// Look up information for a function
+Editor.prototype.lookup_fun = function(fun) {
+    var t = this;
+    return t.grammar_constructors.funs[fun];
+}
+
 /* --- API for getting and setting state ------------------------------------ */
 
 Editor.prototype.get_ast=function() {
@@ -101,9 +125,8 @@ Editor.prototype.get_startcat=function() {
 }
 
 Editor.prototype.initialize_from=function(opts) {
-    var t=this;
     if (opts.abstr)
-        t.import_ast(opts.abstr);
+        this.import_ast(opts.abstr);
 }
 
 // Called after changing grammar or startcat
@@ -131,7 +154,9 @@ Editor.prototype.get_refinements=function(cat) {
     };
     var cont = function(data){
         clear(t.ui.refinements);
-        for (pi in data.producers) {
+        for (var pi in data.producers) {
+            // hide refinement if identical to current fun?
+            
             var fun = data.producers[pi];
             var opt = span_class("refinement", text(fun));
             opt.onclick = bind(function(){
@@ -140,8 +165,7 @@ Editor.prototype.get_refinements=function(cat) {
 
             // If refinement would be destructive, disable it
             var blank = t.ast.is_writable();
-            var def = t.grammar_constructors.funs[fun].def;
-            var typeobj = AST.parse_type_signature(def);
+            var typeobj = t.lookup_fun(fun);
             var inplace = t.ast.fits_in_place(typeobj);
             if (!blank && !inplace) {
                 opt.classList.add("disabled");
@@ -157,48 +181,6 @@ Editor.prototype.get_refinements=function(cat) {
     t.server.browse(args, cont, err);
 }
 
-// Editor.prototype.select_refinement=function(fun) {
-//     var t = this;
-//     t.ui.refinements.innerHTML = "...";
-//     t.ast.removeChildren();
-//     t.ast.setFun(fun);
-//     var args = {
-//         id: fun,
-//         format: "json"
-//     };
-//     var err = function(data){
-//         alert("Error");
-//     };
-//     t.server.browse(args, bind(t.complete_refinement,this), err);
-// }
-
-// Editor.prototype.complete_refinement=function(data) {
-//     if (!data) return;
-
-//     with (this) {
-//         // Parse out function arguments
-//         var def = data.def;
-//         def = def.substr(def.lastIndexOf(":")+1);
-//         var fun_args = map(function(s){return s.trim()}, def.split("->"))
-//         fun_args = fun_args.slice(0,-1);
-
-//         if (fun_args.length > 0) {
-//             // Add placeholders
-//             for (ci in fun_args) {
-//                 ast.add(null, fun_args[ci]);
-//             }
-//         }
-        
-//         // Update ui
-//         redraw_tree();
-//         update_linearisation();
-
-//         // Select next hole & get its refinements
-//         ast.toNextHole();
-//         update_current_node();
-//     }
-// }
-
 // Select refinement now by default replaces "in-place"
 // Case 1: current node is blank/no kids
 // Case 2: kids have all same types, perform an in-place replacement
@@ -210,12 +192,11 @@ Editor.prototype.select_refinement=function(fun) {
     var blank = t.ast.is_writable();
 
     // Check if we can replace in-place (case 2)
-    var def = t.grammar_constructors.funs[fun].def;
-    var typeobj = AST.parse_type_signature(def);
+    var typeobj = t.lookup_fun(fun);
     var inplace = !blank && t.ast.fits_in_place(typeobj);
 
     if (!blank && !inplace) {
-        alert("use clear first if you want to replace the subtree");
+        alert("Use 'Clear' first if you want to replace the subtree.");
         return;
     }
 
@@ -224,10 +205,6 @@ Editor.prototype.select_refinement=function(fun) {
     if (blank) {
         t.ast.removeChildren();
 
-        // Get new function arguments
-        var def = t.grammar_constructors.funs[fun].def;
-        var typeobj = AST.parse_type_signature(def);
-
         // Add dependent type placeholders
         if (typeobj.deps.length > 0) {
             alert("the syntax editor current doesn't support dependent types");
@@ -255,7 +232,7 @@ Editor.prototype.select_refinement=function(fun) {
 Editor.prototype.update_current_node=function(newID) {
     with(this) {
         if (newID)
-            ast.current = new NodeID(newID);
+            ast.setCurrentID(newID);
         redraw_tree();
         get_refinements();
     }
@@ -269,14 +246,14 @@ Editor.prototype.redraw_tree=function() {
         var label =
             ((node.fun) ? node.fun : "?") + " : " +
             ((node.cat) ? node.cat : "?");
-        var current = id.equals(t.ast.current);
+        var current = id.equals(t.ast.getCurrentID());
         var element = elem("a", {class:(current?"current":"")}, [text(label)]);
         element.onclick = function() {
             t.update_current_node(id);
         }
         container2.appendChild( element );
 
-        for (i in node.children) {
+        for (var i in node.children) {
             var newid = new NodeID(id);
             newid.add(parseInt(i));
             visit(container2, newid, node.children[i]);
@@ -311,7 +288,7 @@ Editor.prototype.update_linearisation=function(){
     t.server.linearize(args, function(data){
         clear(t.ui.lin);
 	var tbody=empty("tbody");
-        for (i in data) {
+        for (var i in data) {
             var lang = data[i].to;
             if (t.gm.languages.length < 1 || elem(lang, t.gm.languages)) {
                 tbody.appendChild(row(lang, data[i].text))
@@ -327,7 +304,7 @@ Editor.prototype.clear_node = function() {
     t.ast.removeChildren();
     t.ast.setFun(null);
     t.redraw_tree();
-//    t.get_refinements();
+    t.get_refinements();
 }
 
 // Generate random subtree from current node
@@ -364,8 +341,8 @@ Editor.prototype.import_ast = function(abstr) {
         /// TODO: traverse only subtree, not everything!
         t.ast.traverse(function(node){
             if (!node.fun) return;
-            var info = t.lookup_fun(node.fun);
-            node.cat = info.cat;
+            var typeobj = t.lookup_fun(node.fun);
+            node.cat = typeobj.ret;
         });
         t.redraw_tree();
         t.update_linearisation();
@@ -373,13 +350,3 @@ Editor.prototype.import_ast = function(abstr) {
     server.pgf_call("abstrjson", args, cont);
 }
 
-// Look up information for a function
-Editor.prototype.lookup_fun = function(fun) {
-    var t = this;
-    var def = t.grammar_constructors.funs[fun].def;
-    var typeobj = AST.parse_type_signature(def);
-    return {
-        cat: typeobj.ret
-    }
-}
-