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