[gently hacking on javascript implementation
raph.levien@gmail.com**20090626055224] {
adddir ./js
addfile ./js/ghilbert.html
hunk ./js/ghilbert.html 1
+<title>Ghilbert</title>
+
+<body>
+<h1>Ghilbert test page</h1>
+
+<script src="verify.js" type="text/javascript"></script>
+
+<p>
+<script type="text/javascript">
+s = new GH.Scanner(['(a1i () (a1i.1 ph) (-> ps ph) (a1i.1 ph ps ax-1 ax-mp))']);
+v = GH.read_sexp(s);
+//window.console.log(v);
+
+uc = new GH.XhrUrlCtx();
+text = uc.resolve('set_mm.ghi');
+//window.console.log(text);
+
+s = new GH.Scanner(text.split(/\r?\n/));
+count = 0;
+while (1) {
+  v = GH.read_sexp(s);
+  if (v == null) { break; }
+  count++;
+  //window.console.log(sexp_to_string(v));
+}
+//window.console.log('' + count + ' sexps');
+alert('' + count + ' sexps');
+</script>
addfile ./js/verify.js
hunk ./js/verify.js 1
+// JavaScript implementation of Ghilbert verifier
+// by Raph Levien, 2009
+// Apache 2 license
+
+// Put everything into a namespace defined by one variable.
+if (typeof GH == 'undefined') {
+  var GH = {};
+}
+
+GH.Scanner = function (lines) {
+    this.lines = lines;
+    this.lineno = 0;
+    this.toks = [];
+    this.tokix = 0;
+}
+
+GH.Scanner.prototype.get_tok = function() {
+    while (this.tokix >= this.toks.length) {
+	if (this.lineno == this.lines.length) {
+	    return null;
+	}
+	var line = this.lines[this.lineno];
+	this.lineno++;
+	line = line.split('#')[0];
+	line = line.replace(/\(|\)/g, ' $& ');
+	this.toks = line.split(/ +/);
+	this.tokix = this.toks[0] == '' ? 1 : 0;
+	if (this.toks[this.toks.length - 1] == '') { this.toks.pop(); }
+    }
+    var result = this.toks[this.tokix];
+    this.tokix++;
+    return result;
+};
+
+GH.read_sexp = function(scanner) {
+    while (1) {
+	var tok = scanner.get_tok();
+	if (tok === null) {
+	    return null
+	}
+	if (tok == '(') {
+	    var result = [];
+	    while (1) {
+		var subsexp = GH.read_sexp(scanner);
+		if (subsexp == ')') {
+		    break;
+		} else if (subsexp == null) {
+		    throw 'eof inside sexp';
+		}
+		result.push(subsexp);
+	    }
+	    return result;
+	} else {
+	    return tok;
+	}
+    }
+};
+
+GH.sexp_to_string = function(sexp) {
+    if (typeof sexp == 'string') {
+	return sexp;
+    } else {
+	// map would of course be shorter, but how available is it?
+	var result = [];
+	for (var i = 0; i < sexp.length; i++) {
+	    result.push(GH.sexp_to_string(sexp[i]));
+	}
+    }
+    return '(' + result.join(' ') + ')';
+};
+
+GH.XhrUrlCtx = function () {
+};
+
+GH.XhrUrlCtx.prototype.resolve = function (url) {
+    var x = new XMLHttpRequest();
+    // Sync is bad, it blocks the ui, but async is more complicated...
+    x.open('GET', url, false);
+    x.overrideMimeType("text/plain");
+    x.send(null);
+    return x.responseText;
+};
+
+GH.ProofCtx = function (fvvarmap) {
+    this.stack = [];
+    this.mandstack = [];
+    this.fvvarmap = fvvarmap;
+};
+
+GH.VerifyCtx = function(urlctx, run) {
+    this.kinds = {};
+    this.terms = {};
+    this.syms = {};
+    this.interfaces = {};
+    this.urlctx = urlctx;
+    this.run = run;
+};
+
+GH.VerifyCtx.prototype.add_sym = function(label, val) {
+    if (label in this.syms) {
+	throw 'Symbol ' + label + ' already defined';
+    }
+    this.syms[label] = val;
+};
hunk ./verify.py 75
-	if url.startswith('/'):
-	    fn = os.path.join(repobase, url[1:])
+	# need to be careful about security if used on malicious inputs
+	if url.startswith('file://'):
+	    fn = url[7:]
+	elif url.startswith('/'):
+	    fn = os.path.join(self.repobase, url[1:])
hunk ./verify.py 314
-		raise VerifyError('Term ' + templ[0] + ' expects earity ' + `len(templ[0])` + ' got ' + `len(exp)`)
+		raise VerifyError('Term ' + templ[0] + ' expects arity ' + `len(templ[0])` + ' got ' + `len(exp)`)
hunk ./verify.py 406
+if __name__ == '__main__':
+    fn = sys.argv[1]
+    urlctx = UrlCtx('', fn)
+    ctx = VerifyCtx(urlctx, run)
+    url = 'file://' + fn
+    ctx.run(urlctx, url, ctx)
+
+
hunk ./verify_test.py 118
-# Version of run loop tuned for
+# Version of run loop tuned for regression testing
}
