[fixes to js; it now successfully verifies peano_thms
raph.levien@gmail.com**20091101035048] {
hunk ./js/ghilbert.html 7
+<script src="sandbox.js" type="text/javascript"></script>
hunk ./js/ghilbert.html 11
-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);
hunk ./js/ghilbert.html 12
-uc = new GH.XhrUrlCtx();
-text = uc.resolve('set_mm.ghi');
-//window.console.log(text);
+url = '../peano/peano_thms.gh';
+uc = new GH.XhrUrlCtx('../', url);
+v = new GH.VerifyCtx(uc, run);
+run(uc, url, v);
hunk ./js/ghilbert.html 17
-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');
addfile ./js/sandbox.js
hunk ./js/sandbox.js 1
+// various stuff for testing Ghilbert verifier
+
+log = function(str) {
+    window.console.log(str);  // Safari - FF needs something different
+};
+
+function run(urlctx, url, ctx) {
+    var s = new GH.Scanner(urlctx.resolve(url).split(/\r?\n/));
+    //try {
+	while (true) {
+	    var cmd = GH.read_sexp(s);
+	    if (cmd == null) {
+		return true;
+	    }
+	    if (typeof cmd != 'string') {
+		throw 'Cmd must be atom';
+	    }
+	    var arg = GH.read_sexp(s);
+	    //log(cmd + ' ' + GH.sexp_to_string(arg));
+	    ctx.do_cmd(cmd, arg);
+	}
+	//} catch (e) {
+	//log(url + ':' + s.lineno + ': ' + e);
+	//}
+    return false;
+}
hunk ./js/verify.js 72
-GH.XhrUrlCtx = function () {
+// Similar semantics as Python's os.path.split
+GH.pathsplit = function(path) {
+    var i = path.lastIndexOf('/');
+    if (i == -1) {
+	return ['', path];
+    } else if (i == 0) {
+	return ['/', path.slice(1)];
+    } else {
+	return [path.slice(0, i), path.slice(i + 1)];
+    }
+};
+
+// Similar semantics as Python's os.path.join. Could be vararg, but we only use
+// with 2.
+GH.pathjoin = function(path1, path2) {
+    if (path2.charAt(0) == '/' || path1.length == 0) {
+	return path2;
+    } else if (path1.charAt(path1.length - 1) == '/') {
+	return path1 + path2;
+    } else {
+	return path1 + '/' + path2;
+    }
+};
+
+// Is there not a builtin JS technique for this?
+GH.sexp_equals = function(a, b) {
+    if (typeof a == 'undefined') {
+	throw 'whoa!'
+    }
+    if (typeof a == 'string') return a == b;
+    if (typeof b == 'string' || a.length != b.length) return false;
+    for (var i = 0; i < a.length; i++) {
+	if (!GH.sexp_equals(a[i], b[i])) return false;
+    }
+    return true;
+};
+
+GH.XhrUrlCtx = function (repobase, basefn) {
+    this.repobase = repobase;
+    this.base = GH.pathsplit(basefn)[0];
hunk ./js/verify.js 117
+    if (url.slice(0, 7) == 'http://') {
+	// absolute url, no change
+    } else if (url.charAt(0) == '/') {
+	url = GH.pathjoin(this.repobase, url.slice(1));
+    } else {
+	url = GH.pathjoin(this.base, url);
+    }
hunk ./js/verify.js 168
-    if (label in self.terms) {
+    if (label in this.terms) {
hunk ./js/verify.js 176
-    for (var hyp in hyps) {
-	for (var v in this.allvars(hyp)) {
-	    if (v in mand) {
-		delete mand[v];
+    for (var i = 0; i < hyps.length; i++) {
+	var vars = this.allvars(hyps[i]);
+	for (var j = 0; j < vars.length; j++) {
+	    var ix = mand.indexOf(vars[j]);
+	    if (ix >= 0) {
+		mand.splice(ix, 1);
hunk ./js/verify.js 189
-    var fv = {};
+    var fv = [];
hunk ./js/verify.js 192
-	    fv[exp] = 0;
+	    if (fv.indexOf(exp) == -1) {
+		fv.push(exp);
+	    }
hunk ./js/verify.js 216
-	    if (term[fv + 1] == v) {
+	    if (term[fv * 1 + 1] == v) {
hunk ./js/verify.js 224
-	    if (this.free_in(v, subterm, fvvars)) {
+	    if (this.free_in(v, subterms[i], fvvars)) {
hunk ./js/verify.js 282
-	this.add_kind(arg[1].this.get_kind(arg[0]));
+	this.add_kind(arg[1], this.get_kind(arg[0]));
hunk ./js/verify.js 289
-	var hyps = args[2];
-	var stmt = args[3];
-	var proof = args.slice(4);
+	var hyps = arg[2];
+	var stmt = arg[3];
+	var proof = arg.slice(4);
+	log('checking ' + label);
hunk ./js/verify.js 294
+	var new_hyps = [];
+	for (i = 1; i < hyps.length; i += 2) {
+	    new_hyps.push(hyps[i]);
+	}
+	this.add_assertion('thm', label, fv, new_hyps, stmt, this.syms);
hunk ./js/verify.js 314
-	    fvmap[var] = {};
+	    fvmap[v] = {};
hunk ./js/verify.js 323
-	var vars = self.allvars(hyps[i + 1]);
+	var vars = this.allvars(hyps[i + 1]);
hunk ./js/verify.js 371
-    if (proofctx.stack[i] != stmt)
+    if (!GH.sexp_equals(proofctx.stack[0], stmt))
hunk ./js/verify.js 394
-	    var concol = v[3];
+	    var concl = v[3];
hunk ./js/verify.js 398
-		throw 'Expected ' + mand.length ' mand hyps, got ' + proofctx.mandstack.length;
+		throw 'Expected ' + mand.length + ' mand hyps, got ' + proofctx.mandstack.length;
hunk ./js/verify.js 435
-			throw 'Expected binding variable for ' v + '; ' + exp + ' is term variable';
+			throw 'Expected binding variable for ' + v + '; ' + exp + ' is term variable';
hunk ./js/verify.js 443
-	    var result = self.apply_subst(concl, env);
+	    var result = this.apply_subst(concl, env);
hunk ./js/verify.js 457
-	if (templ in inv) {
-	    if (exp != env[templ]) {
+	if (templ in env) {
+	    if (!GH.sexp_equals(exp, env[templ])) {
+		log(GH.sexp_to_string(exp) + " -- " + GH.sexp_to_string(env[templ]));
hunk ./js/verify.js 499
-	    result.push(GH.map_syms(sexp[i], env));
+	    result.push(GH.map_syms(sexp[i], map));
hunk ./js/verify.js 543
-	if (typeof arg[1] == 'string'	var args) {
+	if (typeof arg[1] == 'string') {
hunk ./js/verify.js 559
-	    if (vv[0] = 'var') {
-		freemap[i] = [];
+	    if (vv[0] == 'var') {
+		freemap[i - 1] = [];
hunk ./js/verify.js 563
-	for (i = 0; i < arg[2].length; i++) {
-	    var freespec = arg[2][i];
+	for (i = 2; i < arg.length; i++) {
+	    var freespec = arg[i];
hunk ./js/verify.js 577
-	this.verify_add_term(termname, kind, argkinds, freemap);
+	this.verify.add_term(termname, kind, argkinds, freemap);
hunk ./js/verify.js 594
-	    hyps.push(GH.map_syms(hyp, this.term_map));
+	    hyps.push(GH.map_syms(local_hyps[i], this.term_map));
hunk ./js/verify.js 598
+    } else if (cmd == 'param') {
+	// todo: nyi
}