diff --git a/lib/parser/agda.js b/lib/parser/agda.js index 3efcd4d5..57128a2a 100644 --- a/lib/parser/agda.js +++ b/lib/parser/agda.js @@ -1,6 +1,5 @@ "use strict"; var _ = require("lodash"); -var lispToArray = require("lisp-to-array"); function parseAgdaResponse(raw) { var tokens = parseSExpression(raw); switch (tokens[0]) { @@ -141,8 +140,53 @@ function parseInfoActionType(s) { //////////////////////////////////////////////////////////////////////////////// // Parsing S-Expressions //////////////////////////////////////////////////////////////////////////////// +function parse_sexp(string) { + var sexp = [[]]; + var word = ''; + var in_str = false; + function pushLastWord(word) { + var n = parseInt(word); + if (isNaN(n)) { + pushInLast(word); + } + else { + pushInLast(n); + } + } + function pushInLast(elem) { + sexp[sexp.length - 1].push(elem); + } + for (var i = 0; i < string.length; i++) { + var char = string[i]; + if (char == '\'' && !in_str) { + } + else if (char == '(' && !in_str) { + sexp.push([]); + } + else if (char == ')' && !in_str) { + if (word != '') { + pushLastWord(word); + word = ''; + } + pushInLast(sexp.pop()); + } + else if (char == ' ' && !in_str) { + if (word != '') { + pushLastWord(word); + word = ''; + } + } + else if (char == '\"') { + in_str = !in_str; + } + else { + word += char; + } + } + return sexp[0]; +} function parseSExpression(s) { - return postprocess(lispToArray(preprocess(s))); + return parse_sexp(preprocess(s))[0]; } function preprocess(chunk) { // polyfill String::startsWith @@ -157,35 +201,6 @@ function preprocess(chunk) { chunk = chunk.substring(12); chunk = "(agda2-parse-error" + chunk + ")"; } - // make it friendly to 'lisp-to-array' package - chunk = chunk.replace(/'\(/g, '(__number__ '); - chunk = chunk.replace(/\("/g, '(__string__ "'); - chunk = chunk.replace(/\(\)/g, '(__nil__)'); return chunk; } -// recursive cosmetic surgery -function postprocess(node) { - if (node instanceof Array) { - switch (node[0]) { - case "`": - return postprocess(node[1]); - case "__number__": // ["__number__", 1, 2, 3] => [1, 2, 3] - case "__string__": // ["__string__", 1, 2, 3] => [1, 2, 3] - case "__nil__": - node.shift(); - return postprocess(node); - default: - return node.map(function (x) { return postprocess(x); }); - } - } - else { - if (typeof node === "string") { - // some ()s in strings were replaced with (__nil__) when preprocessing - return node.replace("(__nil__)", "()"); - } - else { - return node; - } - } -} //# sourceMappingURL=agda.js.map \ No newline at end of file diff --git a/lib/parser/stream/agda-response.js b/lib/parser/stream/agda-response.js deleted file mode 100644 index da8800da..00000000 --- a/lib/parser/stream/agda-response.js +++ /dev/null @@ -1,114 +0,0 @@ -"use strict"; -var __extends = (this && this.__extends) || function (d, b) { - for (var p in b) if (b.hasOwnProperty(p)) d[p] = b[p]; - function __() { this.constructor = d; } - d.prototype = b === null ? Object.create(b) : (__.prototype = b.prototype, new __()); -}; -var stream_1 = require('stream'); -var _ = require('lodash'); -var types_1 = require('../../types'); -var ParseAgdaResponse = (function (_super) { - __extends(ParseAgdaResponse, _super); - function ParseAgdaResponse() { - _super.call(this, { objectMode: true }); - } - ParseAgdaResponse.prototype._transform = function (tokens, encoding, next) { - this.push(parseAgdaResponse(tokens)); - next(); - }; - return ParseAgdaResponse; -}(stream_1.Transform)); -exports.ParseAgdaResponse = ParseAgdaResponse; -function parseAgdaResponse(tokens) { - switch (tokens[0]) { - case "agda2-info-action": - var type = parseInfoActionType(tokens[1]); - var content = tokens.length === 3 ? [] : _.compact(tokens[2].split("\\n")); - return { - type: type, - content: content - }; - case "agda2-status-action": - return { - content: tokens.slice(1, 2) - }; - case "agda2-goals-action": - return { - content: tokens.slice(1, 2) - }; - case "agda2-give-action": - var index = parseInt(tokens[1]); - switch (tokens[2]) { - case "'paren": return { - index: index, - content: [], - hasParenthesis: true - }; - case "'no-paren": return { - index: index, - content: [], - hasParenthesis: false - }; - default: return { - index: index, - content: tokens.slice(2), - hasParenthesis: false - }; - } - case "agda2-parse-error": - return { - content: tokens.slice(1) - }; - case "agda2-goto": - case "agda2-maybe-goto": - return { - filepath: tokens[1][0], - position: tokens[1][2] - }; - case "agda2-solveAll-action": - return { - solution: _.chunk(tokens[1], 2) - }; - case "agda2-make-case-action": - return { - content: tokens[1] - }; - case "agda2-make-case-action-extendlam": - return { - content: tokens[1] - }; - case "agda2-highlight-clear": - return { - content: tokens - }; - case "agda2-highlight-add-annotations": - return { - content: tokens - }; - case "agda2-highlight-load-and-delete-action": - return { - content: tokens[1] - }; - default: - return { - content: tokens - }; - } -} -function parseInfoActionType(s) { - switch (s) { - case "*All Goals*": return types_1.InfoActionType.AllGoals; - case "*Error*": return types_1.InfoActionType.Error; - case "*Type-checking*": return types_1.InfoActionType.TypeChecking; - case "*Current Goal*": return types_1.InfoActionType.CurrentGoal; - case "*Inferred Type*": return types_1.InfoActionType.InferredType; - case "*Module contents*": return types_1.InfoActionType.ModuleContents; - case "*Context*": return types_1.InfoActionType.Context; - case "*Goal type etc.*": return types_1.InfoActionType.GoalTypeEtc; - case "*Normal Form*": return types_1.InfoActionType.NormalForm; - case "*Intro*": return types_1.InfoActionType.Intro; - case "*Auto*": return types_1.InfoActionType.Auto; - case "*Constraints*": return types_1.InfoActionType.Constraints; - case "*Scope Info*": return types_1.InfoActionType.ScopeInfo; - } -} diff --git a/lib/parser/stream/s-expression.js b/lib/parser/stream/s-expression.js deleted file mode 100644 index b878cfbb..00000000 --- a/lib/parser/stream/s-expression.js +++ /dev/null @@ -1,58 +0,0 @@ -"use strict"; -var __extends = (this && this.__extends) || function (d, b) { - for (var p in b) if (b.hasOwnProperty(p)) d[p] = b[p]; - function __() { this.constructor = d; } - d.prototype = b === null ? Object.create(b) : (__.prototype = b.prototype, new __()); -}; -var stream_1 = require('stream'); -var lispToArray = require('lisp-to-array'); -var SExpression = (function (_super) { - __extends(SExpression, _super); - function SExpression() { - _super.call(this, { objectMode: true }); - } - SExpression.prototype._transform = function (chunk, encoding, next) { - this.push(postprocess(lispToArray(preprocess(chunk)))); - next(); - }; - return SExpression; -}(stream_1.Transform)); -exports.SExpression = SExpression; -function preprocess(chunk) { - if (chunk.startsWith("((last")) { - var index = chunk.indexOf("(agda"); - var length_1 = chunk.length; - chunk = chunk.substring(index, length_1 - 1); - } - if (chunk.startsWith("cannot read: ")) { - chunk = chunk.substring(12); - chunk = "(agda2-parse-error" + chunk + ")"; - } - chunk = chunk.replace(/'\(/g, '(__number__ '); - chunk = chunk.replace(/\("/g, '(__string__ "'); - chunk = chunk.replace(/\(\)/g, '(__nil__)'); - return chunk; -} -function postprocess(node) { - if (node instanceof Array) { - switch (node[0]) { - case "`": - return postprocess(node[1]); - case "__number__": - case "__string__": - case "__nil__": - node.shift(); - return postprocess(node); - default: - return node.map(function (x) { return postprocess(x); }); - } - } - else { - if (typeof node === "string") { - return node.replace("(__nil__)", "()"); - } - else { - return node; - } - } -} diff --git a/package.json b/package.json index b9b3fce2..162f9ac4 100644 --- a/package.json +++ b/package.json @@ -22,7 +22,6 @@ "dependencies": { "bluebird": "^3.4.1", "classnames": "^2.2.5", - "lisp-to-array": "^0.2", "lodash": "^4.13.1", "parsimmon": "^0.9.0", "react": "^15.3.1", diff --git a/src/parser/agda.ts b/src/parser/agda.ts index fe180afd..b7a3ffce 100644 --- a/src/parser/agda.ts +++ b/src/parser/agda.ts @@ -1,6 +1,5 @@ import * as _ from "lodash"; import { Agda } from "../types"; -var lispToArray = require("lisp-to-array"); function parseAgdaResponse(raw: string): Agda.Response { @@ -145,8 +144,51 @@ function parseInfoActionType(s: String): string { //////////////////////////////////////////////////////////////////////////////// // Parsing S-Expressions //////////////////////////////////////////////////////////////////////////////// +function parse_sexp(string: string): any { + var sexp = [[]]; + var word = ''; + var in_str = false; + + function pushLastWord(word) { + var n = parseInt(word); + if (isNaN(n)) { + pushInLast(word); + } else { + pushInLast(n); + } + } + + function pushInLast(elem) { + sexp[sexp.length - 1].push(elem); + } + + for (var i = 0; i < string.length; i++) { + var char = string[i]; + if (char == '\'' && !in_str) { + } else if (char == '(' && !in_str) { + sexp.push([]); + } else if (char == ')' && !in_str) { + if (word != '') { + pushLastWord(word); + word = ''; + } + pushInLast(sexp.pop()); + } else if (char == ' ' && !in_str) { + if (word != '') { + pushLastWord(word); + word = ''; + } + } else if (char == '\"') { + in_str = !in_str; + } else { + word += char; + } + } + return sexp[0]; +} + function parseSExpression(s: string): any { - return postprocess(lispToArray(preprocess(s))); + return parse_sexp(preprocess(s))[0]; } function preprocess(chunk: string): string { @@ -154,7 +196,7 @@ function preprocess(chunk: string): string { if (chunk.substr(0, 6) === "((last") { // drop wierd prefix like ((last . 1)) let index = chunk.indexOf("(agda"); - let length = chunk.length + let length = chunk.length; chunk = chunk.substring(index, length - 1); } if (chunk.substr(0, 13) === "cannot read: ") { @@ -162,38 +204,10 @@ function preprocess(chunk: string): string { chunk = chunk.substring(12); chunk = `(agda2-parse-error${chunk})`; } - // make it friendly to 'lisp-to-array' package - chunk = chunk.replace(/'\(/g, '(__number__ '); - chunk = chunk.replace(/\("/g, '(__string__ "'); - chunk = chunk.replace(/\(\)/g, '(__nil__)'); return chunk; } -// recursive cosmetic surgery -function postprocess(node: string | string[]): any { - if (node instanceof Array) { - switch (node[0]) { - case "`": // ["`", "some string"] => "some string" - return postprocess(node[1]); - case "__number__": // ["__number__", 1, 2, 3] => [1, 2, 3] - case "__string__": // ["__string__", 1, 2, 3] => [1, 2, 3] - case "__nil__": // ["__nil__"] => [] - node.shift(); - return postprocess(node); - default: // keep traversing - return node.map(function(x) { return postprocess(x); }); - } - } else { - if (typeof node === "string") { - // some ()s in strings were replaced with (__nil__) when preprocessing - return node.replace("(__nil__)", "()"); - } else { - return node; - } - } -} - export { parseAgdaResponse }