diff options
Diffstat (limited to 'src/www/syntax-editor')
| -rw-r--r-- | src/www/syntax-editor/ast.js | 66 | ||||
| -rw-r--r-- | src/www/syntax-editor/editor.js | 26 |
2 files changed, 67 insertions, 25 deletions
diff --git a/src/www/syntax-editor/ast.js b/src/www/syntax-editor/ast.js index 5a80930d9..b73448f93 100644 --- a/src/www/syntax-editor/ast.js +++ b/src/www/syntax-editor/ast.js @@ -5,10 +5,12 @@ function NodeID(x) { // Initialize from input if (x) { - switch (typeof x) { - case "number": this.id = [x]; break; - case "string": this.id = map(function(s){return parseInt(s)}, x.split(",")); break; - case "object": this.id = Array.clone(x.get()); break; // another NodeID + var type = Object.prototype.toString.call(x); + switch (type) { + case "[object Number]": this.id = [x]; break; + case "[object String]": this.id = map(function(s){return parseInt(s)}, x.split(",")); break; + case "[object Array]" : this.id = Array.clone(x); break; + case "[object Object]": this.id = Array.clone(x.get()); break; // another NodeID } } @@ -28,6 +30,11 @@ function NodeID(x) { return JSON.stringify(this.id)==JSON.stringify(other.id); } + // clone + this.clone = function() { + return new NodeID( this ); + } + } /* --- Abstract Syntax Tree (with state)------------------------------------- */ @@ -62,6 +69,7 @@ function AST(fun, cat) { return new ASTNode({ "fun": fun, "cat": cat, + "deps": {}, // dependent types "children": [] }); } @@ -70,6 +78,9 @@ function AST(fun, cat) { this.current = new NodeID(); // current id in tree + this.getCurrent = function() { + return this.find(this.current); + } this.getFun = function() { return this.find(this.current).fun; } @@ -83,9 +94,24 @@ function AST(fun, cat) { this.find(this.current).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; + + // Add actual type dep node + var node = newNode(k, type); + node.depid = k; // links to dep in parent + this._add(this.current, node); + return node; + } + // Add a single fun at current node this.add = function(fun, cat) { - this._add(this.current, newNode(fun,cat)); + var node = newNode(fun,cat); + this._add(this.current, node); + return node; } // add node as child of id @@ -117,14 +143,12 @@ function AST(fun, cat) { } - // id should be a list of child indices [0,1,0] - // or a string separated by commas "0,1,0" this.find = function(id) { var lid = undefined - switch (typeof id) { - case "number": lid = [id]; break; - case "string": lid = id.split(","); break; - case "object": lid = Array.clone(id.get()); break; // clone NodeID array + if (Object.prototype.toString.call(id) == "[object Object]") { + lid = Array.clone( id.get() ); + } else { + alert("non-NodeID passed to AST.find()"); } var node = this.root; if (lid[0] == 0) lid.shift(); @@ -165,6 +189,13 @@ function AST(fun, cat) { } } + // Return parent of current node + this.getParent = function(i) { + var parent_id = this.current.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); @@ -219,20 +250,27 @@ AST.parse_type_signature = function(str) { var ix = str.indexOf(":"); // judgement type - var bits = str.substr(0, ix).split(" "); + var bits = str.substr(0, ix).trim().split(" "); obj.type = bits[0]; // name (possibly with constructors) obj.name = bits.slice(1); // function args (possibly with type dependency) + var regex_dep = new RegExp(/\(\s*(.+?)\s*:\s*(.+?)\s*\)/); var bits = map(function(s){return s.trim()}, str.substr(ix+1).split("->")); for (var i=0 ; i<bits.length-1; i++) { var bit = bits[i]; - obj.args.push(bit); + var m = regex_dep.exec(bit); + if (m == null) { + obj.args.push(bit); + } else { + // We have a type dependency + obj.deps.push({ "id": m[1], "type": m[2] }); + } } - // return type + //return type obj.ret = bits[bits.length-1]; return obj; diff --git a/src/www/syntax-editor/editor.js b/src/www/syntax-editor/editor.js index b2936e898..6290ebd18 100644 --- a/src/www/syntax-editor/editor.js +++ b/src/www/syntax-editor/editor.js @@ -100,15 +100,11 @@ Editor.prototype.get_startcat=function() { return this.gm.startcat; } -// TODO -// Editor.prototype.initialize_from=function(opts) { -// var t=this; -// if (opts.startcat) -// t.options.initial_startcat=opts.startcat; -// t.change_grammar(); -// if (opts.abstr) -// t.import_ast(opts.abstr); -// } +Editor.prototype.initialize_from=function(opts) { + var t=this; + if (opts.abstr) + t.import_ast(opts.abstr); +} // Called after changing grammar or startcat Editor.prototype.start_fresh=function () { @@ -125,6 +121,7 @@ Editor.prototype.start_fresh=function () { Editor.prototype.get_refinements=function(cat) { var t = this; + t.ui.refinements.innerHTML = "..."; if (cat == undefined) cat = t.ast.getCat(); var args = { @@ -192,7 +189,6 @@ Editor.prototype.get_refinements=function(cat) { Editor.prototype.select_refinement=function(fun) { var t = this; - t.ui.refinements.innerHTML = "..."; t.ast.removeChildren(); t.ast.setFun(fun); @@ -200,8 +196,15 @@ Editor.prototype.select_refinement=function(fun) { var def = t.grammar_constructors.funs[fun].def; var typeobj = AST.parse_type_signature(def); + // Add dependent type placeholders + if (typeobj.deps.length > 0) { + for (var i in typeobj.deps) { + t.ast.addDep(typeobj.deps[i].id, typeobj.deps[i].type); + } + } + + // Add function argument placeholders if (typeobj.args.length > 0) { - // Add placeholders for (var i in typeobj.args) { t.ast.add(null, typeobj.args[i]); } @@ -212,6 +215,7 @@ Editor.prototype.select_refinement=function(fun) { t.update_linearisation(); // Select next hole & get its refinements + t.ui.refinements.innerHTML = "..."; t.ast.toNextHole(); t.update_current_node(); } |