From 596cd4d473d380db94b2a442398981f4eec00ed0 Mon Sep 17 00:00:00 2001 From: "john.j.camilleri" Date: Fri, 30 Nov 2012 15:08:46 +0000 Subject: [PATCH] Syntax editor: internal optimizations by pre-computing certain stuff --- src/www/syntax-editor/README.md | 7 +- src/www/syntax-editor/ast.js | 71 +++++++++++--------- src/www/syntax-editor/editor.js | 111 +++++++++++--------------------- 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 - } -} -