[initial checkin of new verifier
raph.levien@gmail.com**20090620053022] {
addfile ./testsuite
hunk ./testsuite 1
+# test suite for Ghilbert verifier
+
+# low level syntactic stuff
+!append test.gh
+)
+!reject test.gh Unbalanced parenthesis
+!append test.gh
+()
+!reject test.gh List-valued command
+!append test.gh
+(kind wff)
+!reject test.gh List-valued command
+
+# Empty proof file is valid, if not very interesting
+!append test.gh
+!save
+!accept test.gh
+
+!append test.ghi
+!save
+!accept test.gh
+
+!append test.gh
+import (TEST test.ghi () "")
+!save
+!accept test.gh
+
+!append test.ghi
+kind
+!reject test.gh kind cmd with no args
+
+!append test.ghi
+kind foo
+!reject test.gh kinds must be in list
+
+!append test.ghi
+kind ()
+!reject test.gh reject zero kinds
+
+!append test.ghi
+kind (bar baz)
+!reject test.gh reject more than one kind
+
+!append test.ghi
+(kind wff)
+!reject test.gh List-valued command in interface
+
+!append test.ghi
+kind (wff)
+kind (nat)
+tvar (wff ph ps)
+tvar (nat A B)
+var (nat x y)
+term (wff (= A B))
+term (wff (-> ph ps))
+term (wff (A. x ph))
+!save
+!accept test.gh
+
+!append test.ghi
+kind (wff)
+!reject test.gh Redefinition of kind
+
+!append test.ghi
+stmt (19.21ai ((ph x)) ((-> ph ps)) (-> ph (A. x ps)))
+!save
+!accept test.gh
+
+# thm stuff
+
+!append test.gh
+tvar (wff ph ps)
+var (nat x y)
+tvar (nat A B)
+!save
+!accept test.gh
+
+# simple theorem that should check
+!append test.gh
+thm (19.21ai2 ((ph x)) (hyp (-> ph ps)) (-> ph (A. x ps)) (hyp x 19.21ai))
+!accept test.gh
+
+/!append test.gh
+thm (19.21ai ((ph x)) (hyp (-> ph ps)) (-> ph (A. x ps)) (hyp x 19.21ai))
+!reject test.gh Redefinition of thm label
+
+!append test.gh
+thm (19.21ai2 ((ph x)) (hyp (-> ph ps)) (-> ph (A. x ps)) (hyp 19.21ai))
+!reject test.gh Not enough mand hyps
+
+!append test.gh
+thm (19.21ai2 ((ph x)) (hyp (-> ph ps)) (-> ph (A. x ps)) (hyp x ph 19.21ai))
+!reject test.gh Too many mand hyps
+
+!append test.gh
+thm (19.21ai2 () (hyp (-> ph ps)) (-> ph (A. ph ps)) (hyp ph 19.21ai))
+!reject test.gh Mand hyp has wrong kind
+
+!append test.gh
+thm (19.21ai2 () (hyp (-> ph ps)) (-> ph (A. A ps)) (hyp A 19.21ai))
+!reject test.gh Mand hyp has right kind, but tvar instead of binding var
+
+!append test.gh
+thm (19.21ai2 () (hyp (-> ph ps)) (-> ph (A. x ps)) (hyp x 19.21ai))
+!reject test.gh Missing free var condition
+
+# This one might be too strict
+!append test.gh
+thm (19.21ai2 ((ph x y)) (hyp (-> ph ps)) (-> ph (A. x ps)) (hyp x 19.21ai))
+!reject test.gh Spurious free var condition
+
+!append test.gh
+thm (19.21ai2 (()) (hyp (-> ph ps)) (-> ph (A. x ps)) (hyp x 19.21ai))
+!reject test.gh Malformed free var clause
+
+!append test.gh
+thm (19.21ai2 (ph) (hyp (-> ph ps)) (-> ph (A. x ps)) (hyp x 19.21ai))
+!reject test.gh Malformed free var clause
+
+!append test.gh
+thm (19.21ai2 (((ph) x)) (hyp (-> ph ps)) (-> ph (A. x ps)) (hyp x 19.21ai))
+!reject test.gh Malformed free var clause
+
+!append test.gh
+thm (19.21ai2 ((ph (x))) (hyp (-> ph ps)) (-> ph (A. x ps)) (hyp x 19.21ai))
+!reject test.gh Malformed free var clause
+
+# This one might be too strict
+!append test.gh
+thm (19.21ai2 ((x ph)) (hyp (-> ph ps)) (-> ph (A. x ps)) (hyp x 19.21ai))
+!reject test.gh Wrong order in free var clause
+
+!append test.gh
+thm (19.21ai2 ((ph x)) (hyp (-> ph)) (-> ph (A. x ps)) (hyp x 19.21ai))
+!reject test.gh Arity error in hyp
+
+!append test.gh
+thm (19.21ai2 ((ph x)) (hyp (-> ph ps ph)) (-> ph (A. x ps)) (hyp x 19.21ai))
+!reject test.gh Arity error in hyp
+
+!append test.gh
+thm (19.21ai2 ((ph x)) (hyp (-> ph A)) (-> ph (A. x ps)) (hyp x 19.21ai))
+!reject test.gh Kind error in hyp
+
+!append test.gh
+thm (19.21ai2 ((ph x)) (hyp ph) (-> ph (A. x ps)) (hyp x 19.21ai))
+!reject test.gh Unification error in hyp
+
+!append test.gh
+thm (19.21ai2 ((ph x)) (hyp (A. x ph)) (-> ph (A. x ps)) (hyp x 19.21ai))
+!reject test.gh Unification error in hyp
+
+!append test.gh
+thm (19.21ai2 ((ph x)) (hyp (-> ph ps)) (-> ph (A. x ps)) (x 19.21ai))
+!reject test.gh Stack underflow
+
+!append test.gh
+thm (19.21ai2 ((ph x)) (hyp (-> ph ps)) (-> ph (A. x ps)) (hyp hyp x 19.21ai))
+!reject test.gh Too many terms on stack
+
+!append test.gh
+thm (19.21ai2 ((ph x)) (hyp (-> ph ps)) (-> ph (A. x ps)) (hyp x 19.21ai x))
+!reject test.gh Leftover mand hyp on stack
+
+!append test.gh
+thm (19.21ai2 ((ph x)) (hyp (-> ph ps)) (-> ph (A. x ph)) (hyp x 19.21ai))
+!reject test.gh Stack doesn't match concl
+
addfile ./verify.py
hunk ./verify.py 1
+# Reference implementation for Ghilbert 0.7
+
+import sys
+import os.path
+import array
+
+# for debug printing
+def sexp_to_string(sexp):
+    buf = array.array('c')
+    sexp_to_string_rec(buf, sexp)
+    return buf.tostring()
+def sexp_to_string_rec(buf, sexp):
+    if type(sexp) == type('str'):
+        buf.fromstring(sexp)
+    elif type(sexp) == type([]):
+        buf.fromstring('(')
+	sp_string = ''
+        for el in sexp:
+            buf.fromstring(sp_string)
+            sexp_to_string_rec(buf, el)
+            sp_string = ' '
+        buf.fromstring(')')
+
+class VerifyError(Exception):
+    def __init__(self, why, label = None, stack = None):
+        self.why = why
+        self.label = label
+        self.stack = stack
+        self.step = None
+
+class Scanner:
+    def __init__(self, instream):
+	self.instream = instream
+	self.lineno = 0
+	self.toks = []
+	self.tokix = 0
+    def get_tok(self):
+	while len(self.toks) == self.tokix:
+	    line = self.instream.readline()
+	    self.lineno += 1
+	    if line == '':
+		return None
+            line = line.split('#')[0]
+            line = line.replace('(', ' ( ')
+            line = line.replace(')', ' ) ')
+            self.toks = line.split()
+	    self.tokix = 0
+	result = self.toks[self.tokix]
+	self.tokix += 1
+	return result
+
+def read_sexp(scanner):
+    while 1:
+	tok = scanner.get_tok()
+	if tok == None:
+	    return None
+	if tok == '(':
+	    result = []
+	    while 1:
+		subsexp = read_sexp(scanner)
+		if subsexp == ')':
+		    break
+		elif subsexp == None:
+		    raise SyntaxError('eof inside sexp')
+		result.append(subsexp)
+	    return result
+	else:
+	    return tok
+
+class UrlCtx:
+    def __init__(self, repobase, basefn):
+	self.repobase = repobase
+	self.base = os.path.split(basefn)[0]
+    def resolve(self, url):
+	if url.startswith('/'):
+	    fn = os.path.join(repobase, url[1:])
+	else:
+	    fn = os.path.join(self.base, url)
+	return file(fn)
+
+# I think we probably won't use this.
+class Thm:
+    def __init__(self, dv, hyps, stmt, syms):
+	self.dv = dv
+	self.hyps = hyps
+	self.stmt = stmt
+	self.syms = syms
+
+class ProofCtx:
+    def __init__(self, fvvarmap):
+	self.stack = []
+	self.mandstack = []
+	self.fvvarmap = fvvarmap
+
+class VerifyCtx:
+    def __init__(self, urlctx, run):
+	self.kinds = {}
+	self.terms = {}
+	self.syms = {}
+	self.interfaces = {}
+	self.urlctx = urlctx
+	self.run = run
+    def add_sym(self, label, val):
+	if self.syms.has_key(label):
+	    raise VerifyError('Symbol ' + label + ' already defined')
+	self.syms[label] = val
+    def add_kind(self, kind, val):
+	if self.kinds.has_key(kind):
+	    raise VerifyError('Kind ' + kind + ' already defined')
+	self.kinds[kind] = val
+    def get_kind(self, kind):
+	try:
+	    return self.kinds[kind]
+	except KeyError:
+	    raise VerifyError('Kind not known: ' + kind)
+    def add_term(self, label, kind, argkinds, freemap):
+	if self.terms.has_key(label):
+	    raise VerifyError('Term ' + label + ' already defined')
+	self.terms[label] = (kind, argkinds, freemap)
+    def add_assertion(self, kw, label, fv, hyps, concl, syms):
+	mand = self.allvars(concl)
+	for hyp in hyps:
+	    for var in self.allvars(hyp):
+		if var in mand:
+		    mand.remove(var)
+	mand2 = []
+	for var in mand:
+	    if not (syms.has_key(var) and syms[var][0] in ('var', 'tvar')):
+		raise VerifyError('Variable not defined: ' + var)
+	    mand2.append((var, syms[var]))
+	self.add_sym(label, (kw, fv, hyps, concl, mand2))
+
+    def allvars(self, exp):
+        fv = []
+        self.allvars_rec(exp, fv)
+        return fv
+    def allvars_rec(self, exp, fv):
+        if type(exp) == type('var'):
+            if not exp in fv:
+                fv.append(exp)
+        elif type(exp) == type([]):
+            for subexp in exp[1:]:
+                self.allvars_rec(subexp, fv)
+
+    def free_in(self, var, term, fvvars):
+	if type(term) == str:
+	    tvar = self.syms[term]
+	    if tvar[0] == 'var' or fvvars == None:
+		return var == term
+	    return not term in fvvars
+	else:
+	    freemap = self.terms[term[0]][2]
+	    subterms = term[1:]
+	    for v, m in freemap.items():
+		if term[v + 1] == var:
+		    subterms = [term[i + 1] for i in m]
+	    for subterm in subterms:
+		if self.free_in(var, subterm, fvvars):
+		    return True
+	    return False
+    def kind_of(self, exp, syms = None):
+	if type(exp) == type('var'):
+	    if syms == None:
+		v = self.syms[exp]
+	    else:
+		v = syms[exp]
+	    if v[0] not in ('var', 'tvar'):
+		raise VerifyError('expression not a var: ' + exp)
+	    return self.kinds[v[1]]
+	elif type(exp) == type([]):
+	    v = self.terms[exp[0]]
+	    if len(exp) - 1 != len(v[1]):
+		print exp, v
+                raise VerifyError('arity mismatch: ' + exp[0] + ' has arity ' + `len(v[1])` + ' but was given ' + `len(exp) - 1`)
+            for i in range(len(exp) - 1):
+                child_kind = self.kind_of(exp[i + 1], syms)
+                if child_kind != self.kinds[v[1][i]]:
+                    #print self.kinds
+                    raise VerifyError('kind mismatch: ' + sexp_to_string(exp) + ' wanted ' + self.kinds[v[1][i]] + ' got ' + child_kind)
+            return self.kinds[v[0]]
+
+    def do_cmd(self, cmd, arg):
+	if cmd == 'import':
+	    iname = arg[0]
+	    url = arg[1]
+	    params = arg[2]
+	    prefix = arg[3]
+	    if len(prefix) < 2 or prefix[0] != '"' or prefix[-1] != '"':
+		raise SyntaxError('Namespace prefix must be enclosed in quotes')
+	    prefix = prefix[1:-1]
+	    importctx = ImportCtx(self, prefix)
+	    self.run(self.urlctx, url, importctx)
+	if cmd in ('var', 'tvar'):
+	    kind = self.get_kind(arg[0])
+	    for v in arg[1:]:
+		self.add_sym(v, (cmd, kind))
+	elif cmd == 'kindbind':
+	    self.add_kind(arg[1], self.get_kind(arg[0]))
+	elif cmd == 'thm':
+	    (label, fv, hyps, stmt, proof) = arg
+	    self.check_proof(label, fv, hyps, stmt, proof)
+	    self.add_assertion('thm', label, fv, hyps[1::2], stmt, self.syms)
+
+    def check_proof(self, label, fv, hyps, stmt, proof):
+	if len(hyps) & 1:
+	    raise VerifyError('hyp list must be even')
+	fvmap = {}
+	for var in self.allvars(stmt):
+	    if self.syms[var][0] == 'var':
+		fvmap[var] = {}
+	hypmap = {}
+	for i in range(0, len(hyps), 2):
+	    if type(hyps[i]) != type('label'):
+		raise VerifyError('hyp label must be string')
+	    hypmap[hyps[i]] = hyps[i + 1]
+	    self.kind_of(hyps[i + 1])
+	    for var in self.allvars(hyps[i + 1]):
+		if self.syms[var][0] == 'var':
+		    fvmap[var] = {}
+	for clause in fv:
+	    if type(clause) != type([]) or len(clause) == 0:
+		raise VerifyError('each fv clause must be list of vars')
+	    tvar = clause[0]
+	    if type(tvar) != type('var'):
+		raise VerifyError('var in fv clause must be string')
+	    if not (self.syms.has_key(tvar) and self.syms[tvar][0] == 'tvar'):
+		raise VerifyError('first var in fv clause must be tvar: ' + tvar)
+	    for var in clause[1:]:
+		if type(var) != type('var'):
+		    raise VerifyError('var in fv clause must be string')
+		if not (self.syms.has_key(var) and self.syms[var][0] == 'var'):
+		    raise VerifyError('subsequent var in fv clause must be var: ' + var)
+		if not fvmap.has_key(var):
+		    raise VerifyError('spurious var in fv list: ' + var)
+		fvmap[var][tvar] = 0
+	print 'hypmap =', hypmap
+	print 'fvmap =', fvmap
+	proofctx = ProofCtx(fvmap)
+	for step in proof:
+	    print 'step:', step
+	    self.check_proof_step(hypmap, step, proofctx)
+	if len(proofctx.mandstack) != 0:
+	    raise VerifyError('extra mand hyps on stack at and of proof', label)
+	if len(proofctx.stack) != 1:
+	    raise VerifyError('stack must have one term at end of proof', label, proofctx.stack)
+	if proofctx.stack[0] != stmt:
+	    raise VerifyError('stack has ' + sexp_to_string(proofctx.stack[0]) + ' wanted ' + sexp_to_string(stmt), label)
+
+    # These are really methods of both the verify and proofctx objects, and
+    # are here by tradition.
+    def check_proof_step(self, hypmap, step, proofctx):
+	if type(step) == type([]):
+	    kind = self.kind_of(step)
+	    print 'kind of ' + sexp_to_string(step) + ' = ' + kind
+	    proofctx.mandstack.append((('tvar', kind), step))
+	elif hypmap.has_key(step):
+	    if len(proofctx.mandstack) != 0:
+		raise VerifyError('hyp expected no mand hyps, got %d' % len(proofctx.mandstack))
+	    proofctx.stack.append(hypmap[step])
+	else:
+	    if not self.syms.has_key(step):
+		raise VerifyError('unknown proof step: ' + step)
+	    v = self.syms[step]
+	    if v[0] in ('var', 'tvar'):
+		proofctx.mandstack.append((v, step))
+	    elif v[0] in ('stmt', 'thm'):
+		(fv, hyps, concl, mand) = v[1:]
+		if len(mand) != len(proofctx.mandstack):
+                    raise VerifyError('expected %d mand hyps, got %d' % (len(mand), len(proofctx.mandstack)))
+		env = {}
+		for i in range(len(mand)):
+		    var, tkind = mand[i]
+		    el = proofctx.mandstack[i]
+		    if el[0][1] != tkind[1]:
+			raise VerifyError('kind mismatch for ' + var + ': expected ' + tkind[1] + ' got ' + el[0][1])
+		    if tkind[0] == 'var' and el[0][0] != 'var':
+			raise VerifyError('expected binding variable for ' + var)
+		    self.match(var, el[1], env)
+		sp = len(proofctx.stack) - len(hyps)
+		if sp < 0:
+		    raise VerifyError('stack underflow')
+		for i in range(len(hyps)):
+		    el = proofctx.stack[sp + i]
+		    self.match(hyps[i], el, env)
+		# todo: free var checks here
+		result = self.apply_subst(concl, env)
+		proofctx.stack[sp:] = [result]
+		proofctx.mandstack = []
+		print 'stack:', proofctx.stack
+
+
+    def free_in_proof(self, var, term, proofctx):
+	return self.free_in(var, term, proofctx.fvvarmap.get(var, None))
+
+    def match(self, templ, exp, env):
+	if type(templ) == type('var'):
+	    if env.has_key(templ):
+		if exp != env[templ]:
+		    # todo: more debug detail
+		    raise VerifyError('Unification error')
+	    else:
+		env[templ] = exp
+	elif type(templ) == type([]):
+	    if type(exp) != type([]):
+		raise VerifyError('Unification error, expected ' + sexp_to_string(templ) + ' got ' + exp)
+	    if templ[0] != exp[0]:
+		raise VerifyError('Unification error, expected ' + templ[0] + ' got ' + exp[0])
+	    # todo: next check should never trigger, I think all terms
+	    # given to match are well-formed.
+	    if len(exp) != len(templ):
+		raise VerifyError('Term ' + templ[0] + ' expects earity ' + `len(templ[0])` + ' got ' + `len(exp)`)
+	    for i in range(1, len(templ)):
+		self.match(templ[i], exp[i], env)
+
+    def apply_subst(self, templ, env):
+        if type(templ) == type('var'):
+            return env[templ]
+        elif type(templ) == type([]):
+            return [templ[0]] + [self.apply_subst(el, env) for el in templ[1:]]
+
+# Apply map to (constant) symbols in a term
+def map_syms(sexp, map):
+    if type(sexp) == type('var'):
+        return sexp
+    elif type(sexp) == type([]):
+        return [map[sexp[0]]] + [map_syms(el, map) for el in sexp[1:]]
+
+class ImportCtx:
+    def __init__(self, verify, prefix):
+	self.verify = verify
+	self.prefix = prefix
+	self.vars = {}
+	self.term_map = {}
+	#self.kinds = {}
+    def get_kind(self, rawkind):
+	return self.verify.get_kind(self.prefix + rawkind)
+    def do_cmd(self, cmd, arg):
+	if cmd == 'kind':
+	    if type(arg) != type([]) or len(arg) != 1:
+		raise VerifyError('kind takes one arg')
+	    if type(arg[0]) != type('str'):
+		raise VerifyError('kind must be string')
+	    kind = self.prefix + arg[0]
+	    self.verify.add_kind(kind, kind)
+	elif cmd in ('var', 'tvar'):
+	    kind = self.get_kind(arg[0])
+	    for v in arg[1:]:
+		if self.vars.has_key(v):
+		    raise VerifyError('Variable ' + v + ' already defined')
+		self.vars[v] = (cmd, kind)
+	elif cmd == 'term':
+	    kind = self.get_kind(arg[0])
+	    local_termname = arg[1][0]
+	    termname = self.prefix + local_termname
+	    argkinds = []
+	    freemap = {}
+	    invmap = {}
+	    args = arg[1][1:]
+	    for i in range(len(args)):
+		v = args[i]
+		var = self.vars[v]
+		if v in invmap:
+		    raise VerifyError('Variable ' + v + ' not unique')
+		invmap[v] = i
+		argkinds.append(var[1])
+		if var[0] == 'var':
+		    freemap[i] = []
+	    for freespec in arg[2:]:
+		bv = invmap[freespec[0]]
+		if not freemap.has_key(bv):
+		    print freemap, bv
+		    raise VerifyError('Binding variable ' + bv + ' not found')
+		if freemap[bv] != []:
+		    raise VerifyError('More than one freespec for ' + bv)
+		freemap[bv] = [invmap[x] for x in freespec[1:]]
+	    self.verify.add_term(termname, kind, argkinds, freemap)
+	    self.term_map[local_termname] = termname
+	elif cmd == 'stmt':
+	    (local_label, fv, local_hyps, local_stmt) = arg
+	    label = self.prefix + local_label
+	    stmt = map_syms(local_stmt, self.term_map)
+	    hyps = [map_syms(hyp, self.term_map) for hyp in local_hyps]
+	    # TODO: verify kind consistency
+	    self.verify.add_assertion('stmt', label, fv, hyps, stmt, self.vars)
+
+def run(urlctx, url, ctx):
+    s = Scanner(urlctx.resolve(url))
+    try:
+	while 1:
+	    cmd = read_sexp(s)
+	    if cmd is None:
+		return True
+	    if type(cmd) != str:
+		raise SyntaxError('cmd must be atom')
+	    arg = read_sexp(s)
+	    ctx.do_cmd(cmd, arg)
+    except VerifyError, x:
+	print 'Verify error at %s:%d: %s' % (url, s.lineno, x.why)
+    except SyntaxError, x:
+	print 'Syntax error at line %s:%d: %s' % (url, s.lineno, str(x))
+    return False
addfile ./verify_test.py
hunk ./verify_test.py 1
+import sys
+import verify
+
+class StringStream:
+     def __init__(self, s):
+          self.lines = s.split('\n')
+          self.ix = 0
+     def readline(self):
+          if self.ix >= len(self.lines):
+               return ''
+          else:
+               result = self.lines[self.ix] + '\n'
+               self.ix += 1
+               return result
+
+class TestUrlCtx:
+     def __init__(self):
+          self.d = {}
+     def add(self, url, val):
+          self.d[url] = val
+     def resolve(self, url):
+          return StringStream(self.d[url])
+
+     # additional interface for data-driven tests
+     def open_append(self, url):
+          self.current_url = url
+          if not self.d.has_key(url):
+               self.d[url] = ''
+          self.saved_value = self.d[url]
+     def append_current(self, text):
+          self.d[self.current_url] += text
+     def revert(self):
+          self.d[self.current_url] = self.saved_value
+
+def sexp(s):
+     stream = StringStream(s)
+     return verify.read_sexp(verify.Scanner(stream))
+
+def test_one_fv(verifyctx, expected, var, term, fvctx = None):
+     free = verifyctx.free_in(var, sexp(term), fvctx)
+     if free: explanation = "free in"
+     else: explanation = "not free in"
+     if verbose or free != expected: print var, explanation, term
+     if free != expected:
+          raise verify.VerifyError('fail')
+
+def TestFv():
+     urlctx = TestUrlCtx()
+     urlctx.add('foo.ghi',
+"""kind (wff)
+kind (nat)
+tvar (wff ph ps)
+tvar (nat A B)
+var (nat x y)
+term (wff (= A B))
+term (wff (A. x ph))
+term (wff ([/] A x ph) (x A))
+""")
+     verifyctx = verify.VerifyCtx(urlctx, run_regression)
+     verifyctx.do_cmd('import', ['FOO', 'foo.ghi', [], '""'])
+     verifyctx.do_cmd('tvar', ['nat', 'A', 'B'])
+     verifyctx.do_cmd('var', ['nat', 'x', 'y'])
+     test_one_fv(verifyctx, True, 'x', '(= x y)')
+     test_one_fv(verifyctx, False, 'z', '(= x y)')
+     test_one_fv(verifyctx, False, 'x', '(A. x ph)')
+     test_one_fv(verifyctx, True, 'x', '([/] (= x y) x ph)')
+     test_one_fv(verifyctx, False, 'x', '([/] A x ph)')
+     test_one_fv(verifyctx, True, 'x', 'x')
+     test_one_fv(verifyctx, False, 'x', 'y')
+     fvvars_x = {'A': 0}
+     fvvars_y = {}
+     test_one_fv(verifyctx, False, 'x', 'A', fvvars_x)
+     test_one_fv(verifyctx, True, 'y', 'A', fvvars_y)
+     test_one_fv(verifyctx, False, 'z', 'A')
+     test_one_fv(verifyctx, True, 'x', 'x', fvvars_x)
+     test_one_fv(verifyctx, False, 'x', 'y', fvvars_x)
+
+def TestStmt():
+     urlctx = TestUrlCtx()
+     urlctx.add('foo.ghi',
+"""kind (wff)
+kind (nat)
+tvar (wff ph ps)
+tvar (nat A B)
+var (nat x y)
+term (wff (= A B))
+term (wff (-> ph ps))
+term (wff (A. x ph))
+stmt (19.21ai ((ph x)) ((-> ph ps)) (-> ph (A. x ps)))
+""")     
+     verifyctx = verify.VerifyCtx(urlctx, run_regression)
+     verifyctx.do_cmd('import', ['FOO', 'foo.ghi', [], '"foo."'])
+     print verifyctx.syms
+
+def TestThm():
+     urlctx = TestUrlCtx()
+     urlctx.add('foo.ghi',
+"""kind (wff)
+kind (nat)
+tvar (wff ph ps)
+tvar (nat A B)
+var (nat x y)
+term (wff (= A B))
+term (wff (-> ph ps))
+term (wff (A. x ph))
+stmt (19.21ai ((ph x)) ((-> ph ps)) (-> ph (A. x ps)))
+""")     
+     verifyctx = verify.VerifyCtx(urlctx, run_regression)
+     verifyctx.do_cmd('import', ['FOO', 'foo.ghi', [], '""'])
+     verifyctx.do_cmd('tvar', ['wff', 'ph', 'ps'])
+     verifyctx.do_cmd('var', ['nat', 'x', 'y'])
+     verifyctx.do_cmd('thm', ['19.21ai2', [['ph', 'x']],
+                              ['hyp', ['->', 'ph', 'ps']],
+                              ['->', 'ph', ['A.', 'x', 'ps']],
+                              ['hyp', 'x', '19.21ai']])
+     print verifyctx.syms
+
+# Version of run loop tuned for
+def run_regression(urlctx, url, ctx):
+    s = verify.Scanner(urlctx.resolve(url))
+    while 1:
+         cmd = verify.read_sexp(s)
+         if cmd is None:
+              return True
+         if type(cmd) != str:
+              raise SyntaxError('cmd must be atom')
+         arg = verify.read_sexp(s)
+         ctx.do_cmd(cmd, arg)
+
+def regression(fn):
+     urlctx = TestUrlCtx()
+     lineno = 0
+     for l in file(fn).xreadlines():
+          lineno += 1
+          if l.startswith('!'):
+               cmd = l.split()
+               if cmd[0] == '!append':
+                    urlctx.open_append(cmd[1])
+                    dosave = False
+               elif cmd[0] == '!save':
+                    dosave = True
+               elif cmd[0] in ('!accept', '!reject'):
+                    verifyctx = verify.VerifyCtx(urlctx, run_regression)
+                    error = None
+                    try:
+                         run_regression(urlctx, cmd[1], verifyctx)
+                    except verify.VerifyError, x:
+                         error = "VerifyError: " + x.why
+                    except SyntaxError, x:
+                         error = "SyntaxError: " + str(x)
+                    if error is None and cmd[0] == '!reject':
+                         print str(lineno) + ': Expected error: ' + ' '.join(cmd[2:])
+                    elif error and cmd[0] == '!accept':
+                         print str(lineno) + ': Got unexpected ' + error
+                    if verbose >= 1 and error and cmd[0] == '!reject':
+                         print str(lineno) + ': ok ' + error
+                    if not dosave:
+                         urlctx.revert()
+          elif l.strip() and not l.startswith('#'):
+               urlctx.append_current(l)
+
+verbose = 1
+TestFv()
+TestStmt()
+TestThm()
+if len(sys.argv) > 1:
+     regression(sys.argv[1])
}
