# ghilbert.py - ghilbert proof verifier model
# -*- coding: UTF-8 -*-

# ghilbert (www.ghilbert.org) is a formal proof verification language
# (and a python implementation of the proof verifier), developed by 
# Raph Levien.  Ghilbert extends metamath (http://metamath.org/), adding
# features for collaborative theorem-proving on the internet.

import array, os, sys
import logging

from gettext import gettext as _

# TRANS: To preserve interoperability, the ghilbert keywords used in proof
# and interface files ('kind', 'term', 'var', 'stmt', 'kindbind', 'equiv',
# 'param', 'thm', 'def', 'import', 'export', and so on) are not to be
# localized.
#
# This string is used as an error message when a proof or interface
# file names a particular kind which does not yet exist,
# in a context where the name of an existing kind is expected:
KIND_X_DOES_NOT_EXIST = _("Kind '%s' does not exist")

class GhError(Exception):
    """Base class for Ghilbert exceptions"""
    def __init__(self, why):
        self.args = (why,)

class GhProofEndError(GhError):
    pass

class GhMissingDvcsError(GhError):
    def __init__(self, why, needed):
        self.args = (why,)
        self.needed = needed

class GhExtraDvcsError(GhError):
    def __init__(self, why, extra):
        self.args = (why,)
        self.extra = extra

class VerifyError(GhError):
    def __init__(self, why):
        self.args = (why,)

class GhCmdExprError(GhError):
    def __init__(self, why, expr, path=()):
        self.args = (why,)
        self.expr = expr
        self.path = path  # sub-expression path in expr, e.g. (3, 1, 0)

class SyntaxError(GhError):
    def __init__(self, why, scanner):
        self.args = (why,)
        self.scanner = scanner

class StreamScanner:
    def __init__(self, instream):
	self.instream = instream
	self.lineno = 0
	self.toks = []
	self.tokix = 0
    def get_token(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):
    """Read an s-expression from the specified scanner

    Note: may return ')' when ')' occurs unmatched; caller should
    check this.
    """
    while 1:
	tok = scanner.get_token()
	if tok is None:
	    return None
	if tok == '(':
	    result = []
	    while 1:
		subsexp = read_sexp(scanner)
		if subsexp == ')':
		    break
		elif subsexp is None:
		    raise SyntaxError(_('Incomplete (...) s-expression.'),
                                      scanner)
		result.append(subsexp)
	    return result
	else:
	    return tok

# Proof in Progress
class Pip():
    def __init__(self):
        self.exprs = [] # main expression stack
        self.wvs = []   # wild variable expression stack
        self.dvreqs = set()
        self.hyps = {} # map from hyp. names to hyp. internal expressions
        self.vdict = {} # map from variable names to (Ghilbert.VARIX, k, ix)
        self.vlist = [] # map from variable indices to (Ghilbert.VAR, k, vname)
        self.hyps_concs = []
        self.nwv = 0
        self.nvars = 0
        self.dvs = None
        self.equivFlag = False
        self.proof = []

def has_var(ix, expr, argmap):
    if expr[0] is Ghilbert.VARIX:
        ix2 = expr[2]
        if argmap is None:
            return (ix == ix2)
        return has_var(ix, argmap[ix2][0], argmap[ix2][1])
    # expr is (Ghilbert.TERM, termid[1], termid, subexp, ...)
    for e in expr[3:]:
        if has_var(ix, e, argmap):
            return True
    return False

def relvarsof(expr, vset):
    if expr[0] is Ghilbert.VARIX:
        vset.add(expr[2])
    else:
        # (Ghilbert.TERM, termid[1], termid, subexp, ...)
        for e in expr[3:]:
            relvarsof(e, vset)

# This one probably doesn't need to be a method...
def hyp_match(e_stack, e_proto, vmap):
    """Match expression e_stack against e_proto, extending vmap

    vmap is either None, or a list that maps variable indices (from
    the applied statement's hypotheses and conclusions) to internal
    expressions. vmap[i] is None if index i hasn't been assigned yet.
    """

    # short cut:
    if vmap is None and e_stack is e_proto:
        return

    if e_proto[0] == Ghilbert.VARIX:
        if vmap is None:
            # (e_stack is e_proto) is ruled out by the shortcut case
            raise VerifyError(_("Expression mismatch for a variable"))
        vi = e_proto[2]  # The index
        mv = vmap[vi]
        if mv is None:
            if e_stack[1][2] is not e_proto[1][2]:
                raise VerifyError(_("Kind mismatch for variable %s") % v)
            vmap[vi] = e_stack
            return
        # exact match of mapped variable against e_stack
        hyp_match(e_stack, mv, None)
        return

    if e_stack[0] != Ghilbert.TERM:
        raise VerifyError(_("Expression mismatch"))

    # Matching terms (Ghilbert.TERM, termid[1], termid, subexp, ...)
    # Check for the exact same termid.
    #   This will have to change to support termbind!
    if e_stack[2] is not e_proto[2]:
        raise VerifyError(_("Term mismatch (%(term1)s vs. %(term2)s)") %
                          {"term1" : e_stack[2][2], "term2" :  e_proto[2][2]})
    # match the subexpressions of the term
    for j in xrange(3, len(e_stack)):
        hyp_match(e_stack[j], e_proto[j], vmap)

# When there are definition dummy variables involved in the
# expansion, we rely upon the equivalence proving well-definedness
# to indicate that the dummy variable could be replaced with any other
# variable of the same kind (that is distinct from the other variables
# in the RHS expansion), without changing the meaning of the RHS expansion
# in any context.  That means that we don't have to worry about the
# distinctness of the dummy variables outside of a given expansion.
#
# match conclusion c against remnant expression e.
# map is either None, in which case variables in c are matched literally
# against e, or is a list used to map each definition variable index to either
# a pair (expr, mapPrime), where expr is the expression substituted for
# that definition variable, and mapPrime is used in turn to interpret
# variables in expr; or to None, for a definition dummy variable that has
# not yet been assigned.
def match_expand(e, c, map):

    # (Ghilbert.TERM, termid[1], termid, subexp, ...)
    if c[0] is Ghilbert.TERM:
        termid = c[2]
        # The next line will need to change to support termbind
        if e[0] is Ghilbert.TERM and e[2] is termid:
            for j in xrange(3, len(c)):
                match_expand(e[j], c[j], map)
            return

        # Not an exact match. Unless c's termid indicates that c is
        # a definition term, we must fail. The termid for a definition
        # looks like this:
        # (Ghilbert.TERMID, kind-tuple, term-name, defn, arg-kind, ...)
        defn = termid[3]
        if defn is None:  # not a definition
            raise VerifyError(_("Conclusion mismatch"))
        # defn is (rhs_expr, ndummies, vtuple, proof)
        # proof is None if ndummies is 0
        nargs = (len(c) - 3)
        argmap = [None] * (nargs + defn[1])
        for i in xrange(nargs):
            argmap[i] = (c[i + 3], map)
        match_expand(e, defn[0], argmap)
        # check definition dummy mappings for distinctness from other
        # variables (including other dummies at the same level) occurring
        # in the expansion. Note, a def dummy may still match against a
        # variable occurring in the hypothesis or conclusion, if that variable
        # doesn't occur in the parts of the definition expansion coming from
        # subtitutions for the definition arguments.  Although odd, the
        # well-definedness proof asserts that such a variable could be replaced
        # by any fresh variable of the same kind without changing the 'meaning'
        # of the expression.
        for i in xrange(nargs, nargs + defn[1]):
            # The mapping expression of a dummy is known to be a VARIX.
            # All dummies of the expansion have been matched already;
            # argmap[i] is not still None.
            dummyix = argmap[i][0][2]
            for j in xrange(i):
                if has_var(dummyix, argmap[j][0], argmap[j][1]):
                    raise VerifyError(
                        _("Definition dummy distinctness failed"))
        return

    # c[0] is Ghilbert.VARIX
    if map is None:
        if e[0] is not Ghilbert.VARIX or e[2] is not c[2]:
            raise VerifyError(_("Conclusion mismatch"))
        return
    mv = map[c[2]]
    if mv is None: #c is definition dummy variable, not assigned yet
        if e[0] is not Ghilbert.VARIX or e[1] != c[1]:
            raise VerifyError(_("Conclusion mismatch"))
        # distinctness checked above.
        map[c[2]] = (e, None) # assign dummy
        return

    match_expand(e, mv[0], mv[1])
            
def substitute(exp, vmap):
    """Return 'exp' with all variables substituted according to vmap

    exp is a conclusion of the statement being applied in a proof.
    Its variables live in the 'namespace' of the interned statement;
    the substitutions for them are expressions in the 'namespace' of the
    theorem being proven.
    """

    if exp[0] == Ghilbert.VARIX:
        # here exp[2] is the index of the variable in the interned stat.
        return vmap[exp[2]]   # not expected to fail!

    # assert exp is (Ghilbert.TERM, termid[1], termid, def, subexp, ...)
    x = [exp[0], exp[1], exp[2]]
    for e in exp[3:]:
        x.append(substitute(e, vmap))
    return x

def match_exact(expr, rhs):
    if rhs[0] is Ghilbert.VARIX:
        return (expr[0] is Ghilbert.VARIX and expr[2] == rhs[2])
    # The next line will have to change to support termbind...
    if expr[0] is not Ghilbert.TERM or expr[2] != rhs[2]:
        return False
    for j in xrange(3, len(rhs)):
        if not match_exact(expr[j], rhs[j]):
            return False
    return True

# TRANS:  This is an error message for an error that occurs when checking
# the two resulting expressions of a definition justification proof for a
# definition with dummy variables.  There are several slightly different
# error cases, but we presently treat most of them with the same message.
DEFINITION_JUSTIFICATION_MISMATCH = _("Definition justification mismatch")

def match_defjust(expr, rhs, nvars, ndummies, vmap, image):
    if rhs[0] is Ghilbert.VARIX:
        if expr[0] is not Ghilbert.VARIX:
            raise VerifyError(DEFINITION_JUSTIFICATION_MISMATCH)
        if rhs[2] < nvars:
            # explicit definition argument variable must match exactly.
            if expr[2] != rhs[2]:
                raise VerifyError(DEFINITION_JUSTIFICATION_MISMATCH)
            return
        # rhs[2] is a dummy variable.
        ix = rhs[2] - nvars
        vm = vmap[ix]
        if vm is None:
            # This dummy is not mapped yet. Kinds must match.
            if expr[1][2] != rhs[1][2]:
                raise VerifyError(DEFINITION_JUSTIFICATION_MISMATCH)
            eix = expr[2]
            # The (eix < nvars + ndummies) check makes sure that the
            # dummy is mapped to a variable not in the original expression.
            # The (eix in image) check ensures a 1-1 map.
            if (eix < nvars + ndummies) or (eix in image):
                raise VerifyError(
                    _("Definition justification: 2nd expresson requires "
                      "distinct dummy variables!"))
            vmap[ix] = eix
            image.add(eix)
            return
        if vm != expr[2]:
            raise VerifyError(DEFINITION_JUSTIFICATION_MISMATCH)
        return
    # rhs is a term
    if expr[0] is not Ghilbert.TERM or expr[2] is not rhs[2]:
        raise VerifyError(DEFINITION_JUSTIFICATION_MISMATCH)
    for j in xrange(3, len(rhs)):
        match_defjust(expr[j], rhs[j], nvars, ndummies, vmap, image)
            

def iexpr_to_string(expr, vtuple):
    buf = array.array('c')
    iexpr_to_string_rec(expr, vtuple, buf)
    return buf.tostring()

def iexpr_to_string_rec(expr, vtuple, buf):
    if expr[0] is Ghilbert.VARIX:
        buf.fromstring(vtuple[expr[2]][2])
        return
    buf.fromstring('(')
    buf.fromstring(expr[2][2])  # term name
    for e in expr[3:]:
        buf.fromstring(' ')
        iexpr_to_string_rec(e, vtuple, buf)
    buf.fromstring(')')

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 isinstance(sexp, basestring):
        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(')')

def sexp_subexp_substr(sexp, path):
    buf = array.array('c')
    start, stop = sexp_subexp_substr_rec(buf, sexp, path, 0)
    return (buf.tostring(), start, stop)

def sexp_subexp_substr_rec(buf, sexp, path, depth):
    start = len(buf)
    if isinstance(sexp, basestring):
        buf.fromstring(sexp)
        stop = len(buf)
        return (start, stop)
    stop = start
    # sexp is a list
    buf.fromstring('(')
    space = ''
    i = -1
    if depth < len(path):
        i = path[depth]
    for j in xrange(len(sexp)):
        buf.fromstring(space)
        space = ' '
        p = sexp_subexp_substr_rec(buf, sexp[j], path, depth + 1)
        if i == j:
            start, stop = p
    buf.fromstring(')')
    if depth == len(path):
        stop = len(buf)
    return (start, stop)

def dvs_to_string(dvs, vtuple):
    buf = array.array('c')
    space = ''
    for v, w in dvs:
        buf.fromstring(space)
        buf.fromstring('(')
        buf.fromstring(vtuple[v][2])
        buf.fromstring(' ')
        buf.fromstring(vtuple[w][2])
        buf.fromstring(')')
        space = ' '
    return buf.tostring()

def proof_to_string(steps, vtuple):
    buf = array.array('c')
    space = ''
    buf.fromstring(' (')
    for step in steps:
        buf.fromstring(space)
        space = ' '
        if isinstance(step, basestring): # hypothesis name
            buf.fromstring(step)
        elif step[0] is Ghilbert.TERM:
            buf.fromstring(iexpr_to_string(step, vtuple))
        elif step[0] is Ghilbert.VAR:
            buf.fromstring(step[2])
        else: # statement application
            buf.fromstring(step[1])
    buf.fromstring(')')
    return buf.tostring()



def get_stream(path, curdir, fpath, log):
    # paths in 'import' or 'export' starting with '/' are treated
    # as relative to any of the paths in fpath
    log.info("get_stream %s, %s", path, curdir)
    if path[0] == '/':
        log.info("fpath=%s", repr(fpath))
        for p in fpath:
            # don't use os.path.join()
            while p != '' and p[-1] == '/':
                p = p[:-1]
            rpath = p + path
            try:
                log.info(_("get_stream trying %s"), rpath)
                istream = open(rpath, "rb")
                break
            except IOError:
                continue
        else:
            raise GhError(_('Failed to open %s') % path)

        res = (istream, os.path.dirname(os.path.abspath(rpath)))
        return res
        
    if path[:5] == 'http:':
        raise GhError(_("http: URLs are not supported yet."))
    elif path[:8] == 'file:///':
        rpath = path[7:]
    elif path[:7] == 'file://':
        raise GhError(_("file://host/... URLs not supported."))
    else:
        rpath = os.path.join(curdir, path)

    try:
        log.info(_("get_stream try %s"), rpath)
        istream = open(rpath, "rb")
    except IOError:
        raise GhError(_('Failed to open %s') % rpath)

    res = (istream, os.path.dirname(os.path.abspath(rpath)))
    return res

class Ghilbert():
    STMT = 0
    EQUIV = 1
    TERMID = 2
    VARIX = 3
    VAR = 4
    KIND = 5
    KINDBIND = 6
    IMPORT = 7
    EXPORT = 8
    COMMENT = 9
    TERMBIND = 10
    TERM = 11           # Term expression instance

    def __init__(self, logger):
        # kinds is a mapping of kind names to kind names used to test
        # for kind equivalence
        self.kinds = {}
        self.terms = {}
        # statements and variables. These occur in the same namespace
        # (used as proof steps), but we could separate them, allowing
        # overlaps with some precedence rule... For now, we don't.
        self.syms = {}
        self.interfaces = {}
        self.history = []
        self.history_cb = None
        self.log = logger
        # The parent and prefix attributes are used in interface file context.
        # The parent is the proof file context.  The prefix is the prefix
        # specified in the import or export command.
        self.parent = None
        self.prefix = ''
        # Search path for .gh/.ghi files
        self.fpath = []
        self.curdir = '.'   # ha!
        self.file = ''
        # These are used only by interface files. (Subclass?)
        self.params = []
        self.params_used = 0
        self.mykinds = {}       # kinds introduced by this interface
        self.myterms = {}       # terms introduced by this interface
        self.verbosity = 0
        self.pip = None

    def push_history(self, item):
        self.history.append(item)
        # print self.hist_item_to_string(item)
        if self.history_cb:
            self.history_cb(True) # True indicates 'push'

    def pop_history(self):
        try:
            t = self.history.pop()
        except IndexError:
            raise GhError(_('No history left!'))

        if self.history_cb:
            self.history_cb(False) # False indicates 'pop'

        code = t[0]
        if code == Ghilbert.STMT or code == Ghilbert.EQUIV:
            # (Ghilbert.STMT, namepf, nhyps, hyps_concs, vlist, dvs)
            if len(t) > 7:
                del self.syms[t[1]]
            else:
                del self.parent.syms[t[1]]
        elif code == Ghilbert.COMMENT:
            pass  # That's all.
        elif code == Ghilbert.TERMID:
            # (Ghilbert.TERMID, kind-tuple, term-name, defn, arg-kind, ...)
            plen = len(self.prefix)
            pfname = t[2]
            if t[3] is None:
                del self.parent.terms[pfname]
            del self.terms[pfname[plen:]]
        elif code == Ghilbert.VAR:
            # If we allow variable redefinitions some time in the future,
            # we'll have to remember whether there is a previous overridden
            # definition, and restore it if so.
            for v in t[2]:
                del self.syms[v]
        elif code == Ghilbert.KIND:
            # [Ghilbert.KIND, OrigKind, RepresentativeKind]
            kind, kindrep = t[1:]
            assert kind == kindrep
            del self.kinds[kind]
            del self.parent.kinds[kind]
        elif code == Ghilbert.KINDBIND:
            k1, k2, modkinds, k2oldrep = t[1:]
            # modkinds is None for a kindbind done in the proof file
            if not modkinds:
                del self.kinds[k2]
                return
            for k in modkinds:
                self.kinds[k][2] = k2oldrep
        elif code == Ghilbert.IMPORT:
            child = t[1]
            child.hist_revert(0)
        elif code == Ghilbert.EXPORT:
            child = t[1]
            child.hist_revert(0)
            pass
        elif code == Ghilbert.TERMBIND:
            pass
        else:
            raise GhError(_('Unknown code %d') % code)

    def hist_revert(self, ix):
        self.log.warning ('hist_revert %d %d', ix, len(self.history))
        while len(self.history) > ix:
            self.pop_history()

    def hist_item_to_string(self, t):
        code = t[0]
        if code == Ghilbert.STMT or code == Ghilbert.EQUIV:
            # t = (Ghilbert.[STMT|EQUIV], namepf, nhyps, tuple(hyps_concs),
            #      tuple(vlist), nwv, dvs [, hypnames, proof, extravars])
            nhyps = t[2]
            hyps_concs = t[3]
            vtuple = t[4]
            l = []
            proofstr = ''
            if len(t) > 7:
                hypnames = t[7]
                cmd = 'thm'
                for j in xrange(nhyps):
                    h = hyps_concs[j]
                    hnam = hypnames[j]
                    l.append('(%s %s)' % (hnam, iexpr_to_string(h, vtuple)))
                hyps = ' '.join(l)
                proofstr = proof_to_string(t[8], vtuple + t[9])
##                 buf = array.array('c')
##                 space = ''
##                 buf.fromstring(' (')
##                 for step in t[8]:
##                     buf.fromstring(space)
##                     space = ' '
##                     if isinstance(step, basestring): # hypothesis name
##                         buf.fromstring(step)
##                     elif step[0] is Ghilbert.TERM:
##                         buf.fromstring(iexpr_to_string(step, vtuple + t[9]))
##                     elif step[0] is Ghilbert.VAR:
##                         buf.fromstring(step[2])
##                     else: # statement application
##                         buf.fromstring(step[1])
##                 buf.fromstring(')')
##                 proofstr = buf.tostring()
            else:
                cmd = 'stmt'
                if code == Ghilbert.EQUIV:
                    cmd = 'equiv'
                for h in hyps_concs[:nhyps]:
                    l.append(iexpr_to_string(h, vtuple))
                hyps = ' '.join(l)
            l = []
            for h in hyps_concs[nhyps:]:
                l.append(iexpr_to_string(h, vtuple))
            concs = ' '.join(l)
            dvs = t[6]
            dv = ''
            if dvs is not None:
                dv = dvs_to_string(dvs, vtuple)
            return ('%s (%s (%s) (%s) (%s)%s)' % 
                    (cmd, t[1], dv, hyps, concs, proofstr))
        elif code == Ghilbert.COMMENT:
            return t[1]
        elif code == Ghilbert.TERMID:
            # (Ghilbert.TERMID, resultKind, term-name, defn, arg-kind, ...)
            defn = t[3]
            nargs = len(t) - 4
            space = ''
            if nargs != 0:
                space = ' '
            if defn is None:
                result = ' '.join([ak[1] for ak in t[4:]])
                return 'term (%s (%s%s%s))' % (t[1][1], t[2], space, result)
            rhs, ndummies, vtuple, proof = defn
            args = ' '.join([arg[2] for arg in vtuple[:nargs]])
            rhs_str = iexpr_to_string(rhs, vtuple)
            if proof == None:
                return 'def ((%s%s%s) %s)' % (t[2], space, args, rhs_str)
            proofstr = proof_to_string(proof, vtuple)
            return 'def ((%s%s%s) %s%s)' % \
                   (t[2], args, space, rhs_str, proofstr)
        elif code == Ghilbert.VAR:
            result = ''
            for v in t[2]:
                result = result + ' ' + v
            return 'var (%s%s)' % (t[1][1], result)
        elif code == Ghilbert.KIND:
            return 'kind (%s)' % (t[1])
        elif code == Ghilbert.KINDBIND:
            return 'kindbind (%s %s)' % (t[1:3])
        elif code == Ghilbert.IMPORT or code == Ghilbert.EXPORT:
            child = t[1]
            params = ' '.join([x.ifname for x in child.params])
            cmd = ('import', 'export')[code == Ghilbert.EXPORT]
            return ('%s (%s %s (%s) "%s")' %
                    (cmd, child.ifname, t[2], params, child.prefix))
        elif code == Ghilbert.TERMBIND:
            return ''
        else:
            raise GhError(_('Unknown code %d' % code))

    def add_kind(self, expr):
        """Add the specified new kind name."""
        if len(expr) != 1 or not isinstance(expr[0], basestring):
                raise GhCmdExprError(_("Expected 'kind (KINDNAME)'"), expr, ())
        kind = expr[0]
        kindpf = self.prefix + kind
        if self.parent.kinds.has_key(kindpf):
            raise GhCmdExprError(
                    _("Kind '%s' already exists in proof context") % kindpf,
                    expr, (0,))
        # Suppose kind is 'wff' and self.prefix is 'p', and there is
        # an earlier param command using prefix 'w' for an interface that
        # defines a kind 'ff'.  Then we could already have 'wff' in self.kinds
        # although 'pwff' is not in self.parent.kinds.
        if self.kinds.has_key(kind):
            raise GhCmdExprError(
                    _("Kind '%s' already exists in interface context") % kind,
                    expr, (0,))
        # t must be mutable to allow kindbind; use list rather than tuple
        t = [Ghilbert.KIND, kindpf, kindpf]
        self.parent.kinds[kindpf] = t
        self.kinds[kind] = t
        # XXX Pre-existing kinds may be equivalent in the parent (proof file
        # context) without being _visibly_ equivalent in the interface file
        # context. (The equivalence would be 'visible' if it were the result
        # of kindbinds seen either earlier in the interface file itself or
        # its param interfaces.)  Invisible kind equivalence can occur
        # if some earlier imported interface, which is not one of the
        # parameters of the current interface, did the kindbind. Both
        # kinds may be visible although the kindbind isn't, since we allow
        # an import to kindbind two kinds, neither of which it introduced
        # itself. Kindbind transitivity can also cause something similar.
        # This could result in a use elsewhere of the interface file
        # giving a kind mismatch error, even though its use in the current
        # environment (where the kinds are equivalent) does not generate
        # an error. Since the interface file depends upon the two visible
        # kinds being equivalent, and since none of its parameter interfaces
        # provides this, the interface file itself should contain a kindbind
        # for the two kinds before it uses an expression requiring their
        # equivalence.  But, we don't enforce this.  The problem would only
        # be seen when the interface file is used in a context that doesn't
        # provide the kindbind.  The error would be caught, just not
        # proactively. (This can occur for an export as well as an import;
        # export is supposed to verify that the exported file could
        # subsequently be used as an import, but it doesn't catch the above
        # sort of kindbind issue.)

        # self.kinds is all the kinds visible in the interface file kind
        # namespace. self.mykinds is the kinds added by this interface
        # file (rather than received via a 'param' command)
        self.mykinds[kind] = t
        self.push_history(t) # may not need

    def kind_bind_if(self, expr):
        """Make two existing kinds equivalent. Used in an interface file."""

        if len(expr) != 2 or not isinstance(expr[0], basestring) \
               or not isinstance(expr[1], basestring):
            raise GhCmdExprError(_("Expected 'kindbind (KIND1 KIND2)'"),
                                 expr, ())
        try:
            k1 = self.kinds[expr[0]]
        except KeyError:
            raise VerifyError(KIND_X_DOES_NOT_EXIST % expr[0])
        try:
            k2 = self.kinds[expr[1]]
        except KeyError:
            raise VerifyError(KIND_X_DOES_NOT_EXIST % expr[1])

        # [Ghilbert.KIND, OrigKind, RepresentativeKind]
        k1r = k1[2]
        k2r = k2[2]
        if k1r is k2r:        # already equivalent
            return
        modkinds = []
        # Note, we need to look at self.parent.kinds here rather than
        # self.kinds, since there may be kinds equivalent to k2 in the parent
        # that this interface file doesn't know about.
        for k in self.parent.kinds.itervalues():
            if k[2] == k2r:
                modkinds.append(k[1])
                k[2] = k1r
        self.push_history((Ghilbert.KINDBIND, k1[1], k2[1], modkinds, k2r))

    def kind_bind_pf(self, expr):
        """Add an alias for an old kind. Used in a proof file."""

        if len(expr) != 2 or not isinstance(expr[0], basestring) \
               or not isinstance(expr[1], basestring):
            raise GhCmdExprError(_("Expected 'kindbind (KIND1 KIND2)'"),
                                 expr, ())
        try:
            k1 = self.kinds[expr[0]]
        except KeyError:
            raise VerifyError(KIND_X_DOES_NOT_EXIST % expr[0])
        new_kind = expr[1]
        if self.kinds.has_key(new_kind):
            raise VerifyError(_("Kind '%s' already exists") % new_kind)
        self.kinds[new_kind] = [Ghilbert.KIND, new_kind, k1[2]]
        t = (Ghilbert.KINDBIND, k1[1], new_kind, None, None)
        self.push_history(t)

    def add_vars(self, expr):
        """Add a variable."""
        try:
            kind = expr[0]
        except IndexError:
            raise GhCmdExprError(_("Expected 'var (KINDNAME VARNAME ...)'"),
                                 expr, (0,))
        try:
            kt = self.kinds[kind]
        except KeyError:
            raise GhCmdExprError(KIND_X_DOES_NOT_EXIST % kind,
                                 expr, (0,))
        for j in xrange(1, len(expr)):
            var = expr[j]
            if not isinstance(var, basestring):
                raise GhCmdExprError(
                    _("Expected 'var (KINDNAME VARNAME ...)'"), expr, (j,))
                
            if self.syms.has_key(var):
                valu = self.syms[var]
                # Clean up vars added earlier in this command...
                for i in xrange(1, j):
                    del self.syms[expr[i]]
                if valu[0] == Ghilbert.VAR:
                    raise GhCmdExprError(
                        _("Variable '%s' already exists") % var, expr, (j,))
                else:
                    raise GhCmdExprError(
                        _("'%s' already exists as a statement") % var,
                        expr, (j,))
            # We put 'var' as the [2] element of the tuple to accomplish
            # interning of symbols.
            self.syms[var] = (Ghilbert.VAR, kt, var)

        self.push_history((Ghilbert.VAR, kt, expr[1:]))

    def add_term(self, sexpr):
        """Add a term."""
        errpath = None
        if len(sexpr) != 2:
            errpath = ()
        elif not isinstance(sexpr[0], basestring):
            errpath = (0,)
        elif type(sexpr[1]) != type([]) or len(sexpr[1]) < 1:
            errpath = (1,)

        if errpath != None:
            raise GhCmdExprError(
                    _("Expected 'term (TERMKIND (TERMNAME ARGKIND ...))'"),
                    sexpr, errpath)
        try:
            kr = self.kinds[sexpr[0]]
        except KeyError:
            raise GhCmdExprError(KIND_X_DOES_NOT_EXIST % sexpr[0],
                                 sexpr, (0,))
        expr = sexpr[1]
        term = expr[0]
        pfterm = self.prefix + term
        if pfterm in self.parent.terms:
            raise GhCmdExprError(
                _("(Prefixed) term '%s' already exists") % pfterm, sexpr,
                (1,0))
        tl = [Ghilbert.TERMID, kr, pfterm, None]
        for j in xrange(1, len(expr)):
            try:
                kt = self.kinds[expr[j]]
            except KeyError:
                raise GhCmdExprError(KIND_X_DOES_NOT_EXIST % expr[j],
                                     sexpr, (1,j))
            tl.append(kt)
        t = tuple(tl)
        self.parent.terms[pfterm] = t
        self.terms[term] = t
        # self.myterms is specifically those terms introduced in this
        # interface file (rather than by a previous 'param' interface)
        self.myterms[term] = t
        self.push_history(t)

    def expr_convert(self, expr, vardict, varlist, maketuple=True):
        """Convert an s-expression to internal form, and check well-formedness

        As they are encountered in the s-expression expr, new variables are
        added to the dictionalry 'vardict', mapped to the internal form
        expression which is a (Ghilbert.VARIX, k, index) tuple; the 'index'
        value increments each time a variable is added.  Variables are also
        added to varlist sequentially as (Ghilbert.VAR, k, vname) tuples.
        The 'varlist' will hold the hypothesis/conclusion/dummy variables of
        a statement or theorem, or the argument or dummy variables of a
        definition.

        Term s-expressions are replaced with nested tuples
        of the form (Ghilbert.TERM, resultKind, termid, termargexp, ...)
        where termid is a (Ghilbert.TERMID, resultKind, termname, def,
                           argkind, ...)
        and each termargexp is an internal (term or variable) expression form.
        Returns the internal tuple form of the expression.

        It's worth it to tuple-ize the hypotheses and conclusions of the
        theorem or statement, since this will save space when storing them,
        important on the XO.
        It's likely not worth it to tuple-ize all the expressions that occur
        on the proof stack or wild variable substitution stack during the
        course of a proof; tuples and lists don't have much performance
        difference as far as indexing goes.

        May need to revisit this if we store proofs.
        We now store proofs and tuplize terms that occur as wild variable
        substitutions.
        """
        if isinstance(expr, basestring):
            try:
                vix = vardict[expr]
            except KeyError:
                try:
                    var = self.syms[expr]
                except KeyError:
                    raise GhCmdExprError(_("Unknown variable '%s'") % expr,
                                         expr, ())
                if var[0] != Ghilbert.VAR:
                    raise GhCmdExprError(
                        _("Symbol '%s' denotes a statement, not a variable") %
                        expr, expr, ())

                varlist.append(var)
                vix = (Ghilbert.VARIX, var[1], len(vardict))
                vardict[var[2]] = vix
            return vix

        try:
            termid = self.terms[expr[0]]
        except IndexError:
            raise GhCmdExprError(_("Expected term, got ()"), expr, ())
        except KeyError:
            raise GhCmdExprError(_("Unknown term name '%s'") % expr[0],
                                 expr, (0,))
        except TypeError:
            raise GhCmdExprError(_("Expected term name, got term expression"),
                                 expr, (0,))
        # (Ghilbert.TERMID, kind-tuple, term-name, def, arg-kind, ...)
        if len(expr) != len(termid) - 3:
            raise GhCmdExprError(
                _("Wrong number of arguments for '%s'") % termid[2], expr, ())
        # termid[1] here is separated out here just to make the [1] element
        # of all expressions be the kind tuple, for easier kind comparison.
        # May revisit.
        le = [Ghilbert.TERM, termid[1], termid]
        for j in xrange(1, len(expr)):
            try:
                e = self.expr_convert(expr[j], vardict, varlist, maketuple)
            except GhCmdExprError, x:
                (why,) = x.args
                raise GhCmdExprError(why, expr, (j,) + x.path)
            if e[1][2] is not termid[j + 3][2]:
                raise GhCmdExprError(_("Expected expression of kind '%s'") %
                                     termid[j + 3][1], expr, (j,))
            le.append(e)
        if maketuple:
            return tuple(le)
        return le

    def add_def(self, sexpr):
        """Add a definition."""
        # def ((NAME ARGVAR ...) EXPR [(STEP ... EQUIV)])
        errpath = None
        if len(sexpr) < 2:
            errpath = ()
        else:
            lhs = sexpr[0]
            if not isinstance(lhs, list):
                errpath = (0,)
            else:
                for j in xrange(len(lhs)):
                    if not isinstance(lhs[j], basestring):
                        errpath = (0, j)
                        break
        if errpath != None:
            raise GhCmdExprError(
               _("Expected 'def ((NAME ARGVAR ...) EXPR [(STEP ... EQUIV)])'"),
               sexpr, errpath)
        tname = lhs[0]
        if self.terms.has_key(tname):
            raise GhCmdExprError(_("A term named '%s' already exists") % tname,
                                 sexpr, (0,0))
        vdict = {}
        vlist = []
        termid = [Ghilbert.TERMID, None, tname, None]
        try:
            for j in xrange(1, len(lhs)):
                vname = lhs[j]
                var = self.syms[vname]
                if var[0] != Ghilbert.VAR:
                    raise GhError(_("'%s' is not a variable symbol") % vname)
                if vdict.has_key(var[2]):
                    raise GhError(
                        _("Repeated definition variable '%s'") % var[2])
                vdict[var[2]] = (Ghilbert.VARIX, var[1], j - 1)
                termid.append(var[1])   # The argument kind
                vlist.append(var)
        except KeyError:
            raise GhCmdExprError(_("Unknown variable '%s'") % vname,
                                 sexpr, (0, j))
        except GhError, x:
            (why,) = x.args
            raise GhCmdExprError(why, sexpr, (0, j))

        nvars = len(vlist)
        try:
            rhs = self.expr_convert(sexpr[1], vdict, vlist, True)
        except GhCmdExprError, x:
            (why,) = x.args
            raise GhCmdExprError(why, sexpr, (1,) + x.path)
            
        ndummies = len(vlist) - nvars
        proof = None
        if ndummies:
            if len(sexpr) != 3:
                errpath = ()
            elif not isinstance(sexpr[2], list):
                errpath = (2,)
            if errpath != None:
                raise GhCmdExprError(_("Definition has dummy variables, "
                  "expected 'def ((NAME ARGVAR ...) EXPR (STEP ... EQUIV))'"),
                                     sexpr, errpath)
            
            pip = Pip()
            self.pip = pip  # remember it for error display
            # use the same variable mappings in the proof...
            pip.vlist = vlist
            pip.vdict = vdict
            try:
                for j in xrange(len(sexpr[2])):
                    step = sexpr[2][j]
                    self.thm_step(pip, step)
            except GhError, x:
                (why,) = x.args
                raise GhCmdExprError(why, expr, (2, j))

            # End of proof checking.
            if len(pip.wvs):
                raise VerifyError(_("Wild variable substitutions remain at "
                                    "end of definition justification"))
            if not pip.equivFlag:
                raise VerifyError(_("Definition justification proof does "
                                    "not end with an equivalence"))
            exprs = pip.exprs
            if len(exprs) != 2:
                raise VerifyError(
                   _("Expected exactly two expressions on proof stack for "
                     "equivalence. Found %d.") % len(exprs))
            # The first expression on the proof stack must match the
            # definition RHS exactly. The second expression must be the
            # same as the first, except that all dummy variables must be
            # replaced with new variables (of the same kinds) not occurring
            # in the first expression.
            if not match_exact(exprs[0], rhs):
                raise VerifyError(
                    _("Expression 0 does not match definition RHS"))
            vmap = [None] * ndummies
            image = set()
            match_defjust(exprs[1], rhs, nvars, ndummies, vmap, image)

            # Now we must check that the only distinct variables conditions
            # required are those that involve either the original or new
            # set of dummy variables. No distinct variable conditions are
            # allowed between the explicit argument variables of the
            # definition.

            for v, w in pip.dvreqs:
                if v < nvars and w < nvars:
                    raise VerifyError(
                        _("Definition arguments '%(arg1)s' and '%(arg2)s' "
                          "are required to be distinct by the "
                          "definition justification proof") %
                        {"arg1" : vlist[v][2], "arg2" : vlist[w][2]})
            proof = tuple(pip.proof)
        else:
            if len(sexpr) != 2:
                raise GhCmdExprError(
                    _("Definition has no dummy variables, "
                      "expected 'def ((NAME ARGVAR ...) EXPR)'"),
                    sexpr, ())

        termid[1] = rhs[1]      # the term kind
        termid[3] = (rhs, ndummies, tuple(vlist), proof)

        self.terms[tname] = termid
        self.push_history(termid)
        

    def dv_canonical(self, cexpr, vdict):
        """Parse and canonicalize a distinct variables list for stmt or thm

        cexpr is the s-expression for the 'thm' or 'stmt' or 'equiv' command
        vdict is a dictionary of variable names occurring in the hypotheses
          or conclusions of the thm or stmt command; vdict maps these names
          to (Ghilbert.VARIX, k, ix) tuples.

        Returns a set to which this function adds distinct variable pairs
          (tuples). Only relevant variables (occurring in the hypotheses
          or conclusions) are added, and these are represented by the
          corresponding variable index (ix), so the returned set is a set
          of pairs of integer indices.
        """

        # for both stmt and thm, the distinct variables list is cexpr[1]
        i = 0
        dvs = None
        try:
            for dvc in cexpr[1]:
                if not isinstance(dvc, list):
                    raise GhCmdExprError(
                        _("Distinct Variables Condition must be list"),
                        cexpr, (1, i))
                if dvs is None:
                    dvs = set()
                rec = [None] * len(dvc)
                for j in xrange(len(dvc)):
                    vname = dvc[j]
                    # This line may generate TypeError
                    vix = vdict.get(vname)
                    if vix is None:
                        # This line may generate KeyError:
                        sym = self.syms[vname]
                        if sym[0] != Ghilbert.VAR:
                            raise GhCmdExprError(
                                _("'%s' is a statement, not a variable") %
                                vname, cexpr, (1, i, j))
                        v = sym[2]  # == vname
                    else:
                        v = vix[2] # The index
                    rec[j] = v
                    for k in xrange(0, j):
                        w = rec[k]
                        if v == w:
                            raise GhCmdExprError(
                                _("Variable '%s' occurs twice in "
                                  "distinct variables condition") % vname,
                                cexpr, (1, i, j))
                        # ignore if either member is irrelevant
                        if vix is None or isinstance(w, basestring):
                            continue
                        if w < v:
                            v, w = w, v
                        dvs.add((v, w))
                i = i + 1

        except TypeError:
            raise GhCmdExprError(_("Expected (VAR ...)"), cexpr, (1, i, j))
        except KeyError:
            raise GhCmdExprError(_("Unknown variable '%s'") % v1,
                                  cexpr, (1, i, j))
        return dvs

    def add_stmt(self, expr, equiv):
        """Add a statement or equivalence

        stmt (name ((x ...) ...) (hyp ...) (conc ...))
        equiv (name ((x ...) ...) (hyp ...) (expr1 expr2))

        Multiple conclusion syntax is required.
        The 'equiv' argument is False when adding a statement and
        True when adding an equivalence.
        
        Presently, equivalences are allowed and used only for justifying
        the well-definedness of definitions having dummy variables on the
        RHS (the definiens). expr1 and expr2 must be expressions of the
        same kind. The equivalence means that provided the hypotheses
        and the distinct variables conditions are met, the substituted
        values of expr1 and expr2 are equivalent to each other, meaning
        that any occurrence of one of them anywhere in a larger expression
        may be substituted by the other one, regardless of context, without
        changing the 'meaning' in any way significant to the theory.
        As of now, such 'arbitrarily deep' substitutions are only made
        use of during definition expansion at the end of a proof.
        Example: equiv (wff_equiv () ((-> ph ps) (-> ps ph)) (ph ps))

        """
        errpath = None
        if not isinstance(expr, list) or len(expr) != 4:
            errpath = ()
        elif not isinstance(expr[0], basestring):
            errpath = (0,)
        elif not isinstance(expr[1], list):
            errpath = (1,)
        elif not isinstance(expr[2], list):
            errpath = (2,)
        # for now, don't allow single-conclusion syntax, as the determination
        # is not foolproof; a multi-conclusion theorem whose first conclusion
        # is a variable with a name equal to a term identifier may look like
        # a term with that identifier (although the proof isn't likely to work)
        elif not isinstance(expr[3], list):
            errpath = (3,)

        if errpath != None:
            raise GhCmdExprError(
                 _("Expected "
                   "'%s (NAME ((DV1 DV2 ...) ...) (HYP ...) (CONC ...))'") %
                   ('stmt', 'equiv')[equiv], expr, errpath)
        namepf = self.prefix + expr[0]
        if self.parent.syms.has_key(namepf):
            raise GhCmdExprError(_("(Prefixed) symbol '%s' already exists"),
                                 namepf, (0,))

        vdict = {}
        vlist = []
        hyps_concs = []
        try:
            for hyp in expr[2]:
                ihyp = self.expr_convert(hyp, vdict, vlist)
                hyps_concs.append(ihyp)
        except GhCmdExprError, x:
            (why,) = x.args
            raise GhCmdExprError(why, expr, (2, len(hyps_concs)) + x.path)

        nhyps = len(hyps_concs)
        nhv = len(vlist)
        try:
            for conc in expr[3]:
                iconc = self.expr_convert(conc, vdict, vlist)
                hyps_concs.append(iconc)
        except GhCmdExprError, x:
            (why,) = x.args
            raise GhCmdExprError(why, expr,
                                 (3, len(hyps_concs) - nhyps) + x.path)
        tag = Ghilbert.STMT
        if equiv:
            nconcs = len(hyps_concs) - nhyps
            if (nconcs != 2 or 
                hyps_concs[nhyps][1][2] != hyps_concs[nhyps+1][1][2]):
                raise GhCmdExprError(
                    _("Equivalences must have exactly two 'conclusions'"),
                    expr, (3,))
            tag = Ghilbert.EQUIV

        dvs = self.dv_canonical(expr, vdict)

        # Note, a statement with more (or less) than one conclusion
        # doesn't have a single kind, but a possibly empty tuple of kinds
        t = (tag, namepf, nhyps, tuple(hyps_concs),
             tuple(vlist), len(vlist) - nhv, dvs)
        self.parent.syms[namepf] = t
        self.push_history(t)

    def thm_step(self, pip, step):
        """Apply one step in the proof of a theorem."""

        if pip.equivFlag:
            raise VerifyError(
                _("An equivalence was used. No more proof steps allowed."))
        if isinstance(step, list):
            # step represents a term expression which is to be substituted
            # for one of the applied statement's wild variables.
            # Do we want to add variables in step (that haven't already been
            # added from the hypothesis/conclusion processing) to the
            # theorem's variable list? Perhaps not...  But if such
            # 'proof dummy' variables occur in the remnant, there may be
            # issues with definition dummies/distinct variables conditions
            # in the end-of-proof processing. (There aren't, really.)
            #
            # Convert this expression to tuple form now that we save proofs.
            e = self.expr_convert(step, pip.vdict, pip.vlist, True)
            pip.wvs.append(e)
            pip.proof.append(e)
            return

        nwv = len(pip.wvs)
        p = pip.hyps.get(step)
        if p != None:
            nam, e = p
            if nwv != 0:
                raise VerifyError(
                    _("Hypotheses may be pushed only when the "
                      "wild variable substitution stack is empty"))
            pip.exprs.append(e)
            pip.proof.append(nam)
            return

        try:
            e = self.syms[step]
        except KeyError:
            raise VerifyError(_("Unrecognized proof step '%s'") % step)

        if e[0] == Ghilbert.VAR:
            try:
                vix = pip.vdict[e[2]]
            except:
                vix = (Ghilbert.VARIX, e[1], len(pip.vdict))
                pip.vdict[e[2]] = vix
                pip.vlist.append(e)
            pip.wvs.append(vix)
            pip.proof.append(e)
            return

        # Apply an existing statement
        # e is (Ghilbert.[STMT|EQUIV], namepf, nhyps, hyps_concs,
        #       vlist, nwv, dvs, ...)
        nhyps = e[2]
        pip_exprs = pip.exprs
        nstack = len(pip_exprs)
        if nstack < nhyps:
            raise VerifyError(
                _("There are too few hypotheses on the proof stack"))
        # e[5] is the number of wild variable substitutions that the statement
        # requires.
        if e[5] != nwv:
            raise VerifyError(_("%(stmt)s requires exactly %(num)d wild "
                                "variable substitutions") %
                              {"stmt" : e[1], "num" : e[5]})

        j = nstack - nhyps
        hyps_concs = e[3]  # tuple of hypotheses & conclusions for statement
        vlist = e[4]       # tuple of variables used in hyps_concs
        vmap = [None] * len(vlist)
        for i in xrange(nhyps):
            hyp_match(pip_exprs[j], hyps_concs[i], vmap)
            j = j + 1

        j = len(vlist) - nwv  # index of first wild variable of applied stat.
        pip_wvs = pip.wvs
        for i in xrange(nwv):
            x = pip_wvs[i]
            v = vlist[j]
            # check for kind equivalence
            if x[1][2] is not v[1][2]:
                raise VerifyError(
                    _("Value substituted for wild variable %(var)s "
                      "of %(stmt)s is %(kind1)s, but it should be "
                      "%(kind2)s") %
                    {"var" : v[2], "stmt" : e[1], "kind1" : x[1][1],
                     "kind2" : v[1][1]})
            vmap[j] = x
            j = j + 1

        # Disjoint variable handling
        # Only worry about variables that occur in the hypotheses or
        # conclusions of the theorem.
        # But suppose the statement we are applying requires the variables
        # in the substitutions for two of its variables to be disjoint,
        # but they are not, but the intersection involves only variables
        # that are not in the hypotheses or conclusions of the theorem
        # being proven. We still want to prevent such a use.
        relvars = pip.nvars
        dvs = e[6]
        if dvs != None:
            dvarsmap = [None] * len(vlist)
            for v, w in dvs:
                vset1 = dvarsmap[v]
                if vset1 is None:
                    vset1 = set()
                    relvarsof(vmap[v], vset1)
                    dvarsmap[v] = vset1
                vset2 = dvarsmap[w]
                if vset2 is None:
                    vset2 = set()
                    relvarsof(vmap[w], vset2)
                    dvarsmap[w] = vset2
                for u1 in vset1:
                    for u2 in vset2:
                        if u1 == u2:
                            u = pip.vlist[u1][2]
                            raise VerifyError(
                                _("Disjoint variable violation for "
                                  "(%(var1)s, %(var2)s) applying %(stmt)s :"
                                  "substitutions for both contain %(var3)s")
                                % {"var1" : vlist[v][2], "var2" : vlist[w][2],
                                   "stmt" : e[1], "var3" : u})
                        if u1 >= relvars or u2 >= relvars:
                            continue
                        if u1 < u2:
                            pip.dvreqs.add((u1, u2))
                        else:
                            pip.dvreqs.add((u2, u1))

        # Everything's OK with this application; wipe out the used hypotheses
        # and the wild variable substitutions in the Pip, and add the
        # substituted conclusions
        pip.wvs = []
        pip.exprs[(nstack - nhyps):] = []

        if e[0] is Ghilbert.EQUIV:
            pip.equivFlag = True

        for c in hyps_concs[nhyps:]:
            x = substitute(c, vmap)
            pip.exprs.append(x)
        pip.proof.append(e)


    def add_thm(self, expr, stop_cond):
        """Initial processing for a thm statement

        expr is the thm's s-expression
        pip must be a newly created Pip.
        """

        pip = Pip()
        self.pip = pip  # remember it for error output

        # Expect (THM_NAME ((VAR ...) ...)
        #                  ((HYP_NAME HYP_EXPR) ...)
        #                  (CONC ...)
        #                  (STEP ...))
        errpath = None
        if not isinstance(expr, list) or len(expr) != 5:
            errpath = ()
        elif not isinstance(expr[0], basestring):
            errpath = (0,)
        elif not isinstance(expr[1], list):
            errpath = (1,)
        elif not isinstance(expr[2], list):
            errpath = (2,)
        # for now, don't allow single-conclusion syntax, as the determination
        # is not foolproof; a multi-conclusion theorem whose first conclusion
        # is a variable with a name equal to a term identifier may look like
        # a term with that identifier (although the proof isn't likely to work)
        elif not isinstance(expr[3], list):
            errpath = (3,)
        elif not isinstance(expr[4], list):
            errpath = (4,)

        if errpath != None:
            raise GhCmdExprError(_("Expected "
                                   "'thm (NAME ((VAR ...) ...) "
                                              "((HYPNAME HYP) ...) "
                                              "(CONC ...) (STEP ...))'"),
                                 expr, errpath)

        if self.syms.has_key(expr[0]):
            raise GhCmdExprError(_("Symbol '%s' already exists") % expr[0],
                                 expr, (0,))
        pip_vdict = pip.vdict
        pip_vlist = pip.vlist
        hyps_concs = pip.hyps_concs
        hypnames = []
        try:
            for hp in expr[2]:
                if not isinstance(hp, list) or len(hp) != 2 or \
                       not isinstance(hp[0], basestring):
                    raise GhCmdExprError(
                        _("Expected hypothesis form '(HYP_NAME HYP_EXPR)'"),
                        expr, ())
                hypnam = hp[0]
                if pip.hyps.has_key(hypnam):
                    raise GhCmdExprError(
                        _("Repeated hypothesis name '%s'") % hypnam,
                        expr, (0,))
                try:
                    e = self.expr_convert(hp[1], pip_vdict, pip_vlist)
                except GhCmdExprError, x:
                    (why,) = x.args
                    raise GhCmdExprError(why, None, (1,) + x.path)
                pip.hyps[hypnam] = (hypnam, e)
                hypnames.append(hypnam)
                hyps_concs.append(e)
        except GhCmdExprError, x:
            (why,) = x.args
            raise GhCmdExprError(why, expr, (2, len(hyps_concs)) + x.path)

        nhyps = len(hyps_concs)
        nhypvars = len(pip_vlist)

        try:
            for conc in expr[3]:
                e = self.expr_convert(conc, pip_vdict, pip_vlist)
                hyps_concs.append(e)
        except GhCmdExprError, x:
            (why,) = x.args
            raise GhCmdExprError(why, expr,
                                 (3, len(hyps_concs) - nhyps) + x.path)

        nconcs = len(hyps_concs) - nhyps
        pip.nvars = len(pip_vlist)
        pip.nwv = pip.nvars - nhypvars

        # Note, by the end of the proof, we may have more relevant distinct
        # variable pairs that we need to add.
        pip.dvs = self.dv_canonical(expr, pip_vdict)

        try:
            nsteps = len(expr[4])
            for j in xrange(nsteps):
                if j == stop_cond:
                    raise GhError(_("Step."))
                step = expr[4][j]
                self.thm_step(pip, step)
        except GhError, x:
            (why,) = x.args
            raise GhCmdExprError(why, expr, (4, j))

        # End of proof checking.
        if len(pip.wvs):
            raise GhProofEndError(_("Wild variable substitutions remain at "
                                    "end of proof"))
        if pip.equivFlag:
            raise GhProofEndError(_("Only definition justification proofs may "
                                    "end with an equivalence step."))
        exprs = pip.exprs
        nexprs = len(exprs)
        if nexprs != nconcs:
            raise GhProofEndError(_("%(nexprs)d expressions remain on proof "
                                    "stack; %(nconcs)d expected.") %
                                  {"nexprs" : nexprs, "nconcs" : nconcs})

        for j in xrange(nexprs):
            match_expand(exprs[j], hyps_concs[nhyps + j], None)

        # Check distinct variables
        dvreqs = pip.dvreqs
        dvs = pip.dvs
        if dvs is None:
            needed = dvreqs
        else:
            needed = dvreqs - dvs

        if needed:
            raise GhCmdExprError(
                _("Missing distinct variable conditions:%s") %
                dvs_to_string(needed, pip.vlist), expr, (1,len(expr[1])))

        if dvs is not None:
            extra = dvs - dvreqs
            if extra:
                #print 'Theorem %s has unneeded distinct ' \
                #      'variables conditions:' % expr[0]
                #print dvs_to_string(extra, pip_vlist)
                pass
                #raise GhExtraDvcsError("Extra distinct variables conditions",
                #                       extra)

        # Presently we do keep the proofs, and pip_vlist is restricted
        # to only the variables that occur in the hypothesis or conclusions
        # (Ghilbert.STMT, name, nhyps, hyps_concs, vtuple, nwv, dvs,
        #  hypnames, proof, proof_dummy_vars)
        t = (Ghilbert.STMT, expr[0], nhyps, tuple(hyps_concs),
             tuple(pip_vlist[:pip.nvars]), pip.nwv, dvs, tuple(hypnames),
             tuple(pip.proof), tuple(pip_vlist[pip.nvars:]))
        self.syms[expr[0]] = t
        self.push_history(t)

    def param(self, expr):
        # param (IFACE_NAME PATH (IFACE_NAME ...) "PREFIX")
        errpath = None
        if len(expr) != 4:
            errpath = ()
        elif not isinstance(expr[0], basestring):
            errpath = (0,)
        elif not isinstance(expr[1], basestring):
            errpath = (1,)
        elif not isinstance(expr[2], list):
            errpath = (2,)
        else:
            prefix = expr[3]
            if not isinstance(prefix, basestring) or len(prefix) < 2 or \
                   prefix[0] != '"' or prefix[-1] != '"':
                errpath = (3,)
            prefix = prefix[1:-1]

        if errpath is not None:
            raise GhCmdExprError(
              _('Expected param (IFACE_NAME PATH (PARAM_IFACE ...) "PREFIX")'),
              expr, errpath)
        
        ifname = expr[0]
        if self.interfaces.has_key(ifname):
            raise GhCmdExprError(_("Interface '%s' already exists") % ifname,
                                 expr, (0,))

        # We presently ignore the PATH specified in the 'param' command.
        params = []
        try:
            for j in xrange(len(expr[2])):
                ifn = expr[2][j]
                params.append(self.interfaces[ifn])
        except KeyError:
            raise GhCmdExprError(_("Unknown interface name '%s'") % ifn,
                                 expr, (2,j))
        except TypeError:
            raise GhCmdExprError(_("Interface parameter must be an "
                                   "interface identifier"), expr, (2,j))
        
        try:
            n = self.params_used
            iface = self.params[n]
        except IndexError:
            raise GhCmdExprError(_("There are more 'param' commands in the "
                                   "interface file than interface parameters "
                                   "passed in the 'import' command"), expr, ())

        #
        # From the parameter interface we need to incorporate all
        # kinds and terms that the interface provided itself.
        # Variables, statements, and equivalences from the parameter
        # interface are not incorporated. kindbinds and termbinds
        # done in the parameter interface will still have effect
        # on the kinds and terms (all present in the proof file context),
        # so need not be explicitly handled.
        #
        for k, v in iface.mykinds.iteritems():
            pk = prefix + k
            if self.kinds.has_key(pk):
                raise VerifyError(
                    _("Kind '%(kind)s' provided by '%(iface)s' is already "
                      "visible") % {"kind" : pk, "iface" : ifname})
            self.kinds[pk] = v

        for t, v in iface.myterms.iteritems():
            pt = prefix + t
            if self.terms.has_key(pt):
                raise VerifyError(
                    _("Term '%(term)s' provided by '%(iface)s' is already "
                      "visible") % {"term" : pt, "iface" : ifname})
            self.terms[pt] = v

        self.interfaces[ifname] = iface
        self.params_used = n + 1


    def gh_import(self, expr):
        # import (IFACE_NAME PATH (IFACE_NAME ...) "PREFIX")
        errpath = None
        if len(expr) != 4:
            errpath = ()
        elif not isinstance(expr[0], basestring):
            errpath = (0,)
        elif not isinstance(expr[1], basestring):
            errpath = (1,)
        elif not isinstance(expr[2], list):
            errpath = (2,)
        else:
            prefix = expr[3]
            if not isinstance(prefix, basestring) or len(prefix) < 2 or \
                   prefix[0] != '"' or prefix[-1] != '"':
                errpath = (3,)
            prefix = prefix[1:-1]

        if errpath is not None:
            raise GhCmdExprError(
                _('Expected import (IFACE_NAME PATH (PARAM_IFACE ...) "PREFIX")'),
                expr, errpath)

        ifname = expr[0]
        if self.interfaces.has_key(ifname):
            raise GhCmdExprError(_("Interface '%s' already exists") % ifname,
                                 expr, (0,))

        if self.verbosity:
            print _('Importing %s') % ifname

        ifs = expr[2]
        nifs = len (ifs)
        params = [None] * nifs
        try:
            for j in xrange(nifs):
                params[j] = self.interfaces[ifs[j]]
        except KeyError:
            raise GhCmdExprError(_("Unknown interface name '%s'") % ifs[j],
                                 expr, (2,j))
        except TypeError:
            raise GhCmdExprError(_("Interface parameter must be an "
                                   "interface identifier"), expr, (2,j))

        try:
            (istream, curdir) = get_stream(expr[1], self.curdir,
                                           self.fpath, self.log)
        except GhError:
            raise GhCmdExprError(_("Cannot open interface file at '%s'") %
                                 expr[1], (1,))
        
        try:
            child = Ghilbert(self.log)
            child.parent = self
            child.prefix = prefix
            child.params = params
            child.ifname = ifname
            child.curdir = curdir
            child.file = expr[1]

            scanner = StreamScanner(istream)
            while (1):
                word = scanner.get_token()
                if word is None:
                    break
                if word == '(' or word == ')':
                    raise VerifyError(
                        _("Expected command word, got '%(char)s' "
                          "at line '%(line)d'") %
                        {"char" : word, "line" : scanner.lineno})
                sexpr = read_sexp(scanner)
                if not isinstance(sexpr, list):
                    raise VerifyError(
                        _("Expected s-expression (...) command "
                          "argument at line %d") % scanner.lineno)
                if word == 'stmt':
                    child.add_stmt(sexpr, False)
                elif word == 'term':
                    child.add_term(sexpr)
                elif word == 'var':
                    child.add_vars(sexpr)
                elif word == 'kind':
                    child.add_kind(sexpr)
                elif word == 'kindbind':
                    child.kind_bind_if(sexpr)
                elif word == 'equiv':
                    child.add_stmt(sexpr, True)
                elif word == 'param':
                    child.param(sexpr)
                elif word in ['thm', 'def', 'import', 'export']:
                    raise VerifyError(
                        _("Proof file command '%(cmd)s' encountered "
                          "in interface file at line %(line)d") %
                        {"cmd" : word, "line" : scanner.lineno})
                else:
                    child.log.warning(
                        _("Skipping unknown command '%(cmd)s' "
                          "at line '%(line)d'") %
                        {"cmd" : word, "line" : scanner.lineno})

            if child.params_used != len(params):
                raise VerifyError(
                    _("'import' provided %(num1)d parameters, but only "
                      "%(num2)d were used") %
                    {"num1" : len(params), "num2" : child.params_used})

        except GhError, x:
            msg = _("Error in import: %(file)s line %(line)d") % \
                  {"file" : child.file, "line" : scanner.lineno}
            print >> sys.stderr, msg
            # Forget kinds, etc., introduced by the import.
            child.hist_revert(0)
            (why,) = x.args
            raise GhError (msg + '\n' + why)
        finally:
            istream.close()

        # We should no longer need child.terms and child.kinds. Free
        # them to save memory. (If this interface is used later via 'param',
        # .myterms and .mykinds will still be available.)
        child.terms = None
        child.kinds = None

        self.interfaces[ifname] = child
        self.push_history((Ghilbert.IMPORT, child, expr[1]))

    def xprt_expr_compare(self, expr, proto, vdict, vlist):
        """Compare an s-expr from exported stmt with corresp. proof ctx expr

        This function compares the s-expression <expr> with the prototype
        expression <proto> which is the corresponding hypothesis or conclusion
        of an existing statement or equivalence in the proof context.
        vdict is a dictionary mapping variable names to Ghilbert.VARIX tuples;
        vlist is a list mapping variable indices to Ghilbert.VAR tuples.
        vdict and vlist are grown by this routine, which checks for a
        bijective map from the (indexed) variables in the hypotheses and
        conclusions of the statement being exported, and those variables
        provided by the corresponding s-expressions in the stmt or equiv
        command from the export file.
        """
        if proto[0] is Ghilbert.VARIX:
            var = vlist[proto[2]]
            if var != None:
                if expr != var[2]:
                    raise GhCmdExprError(_("Expression mismatch"), expr, ())
                return
            try:
                var = self.syms[expr]
            except (TypeError, KeyError):
                raise GhCmdExprError(_("Expression mismatch"), expr, ())
            if var[0] != Ghilbert.VAR:
                raise GhCmdExprError(
                    _("Expected variable name, got other symbol"),  expr, ())
            if var[1][2] != proto[1][2]:
                raise GhCmdExprError(_("Kind mismatch"), expr, ())
            if vdict.has_key(var[2]):
                # make sure the map is 1-1
                raise GhCmdExprError(_("Expression mismatch"), expr, ())
            vlist[proto[2]] = var
            vdict[var[2]] = proto
            return

        # proto is (Ghilbert.TERM, resultKind, termid, termargexp, ...)
        nargs = len(proto) - 3
        if (not isinstance(expr, list) or len(expr) != nargs + 1):
            raise GhCmdExprError(_("Expression mismatch"), expr, ())

        # Have to make sure that the term used is actually available in
        # the export context at this point.
        try:
            t = self.terms[expr[0]]
        except (TypeError, KeyError):
            raise GhCmdExprError(_("Unknown term identifier '%s'") % expr[0],
                                 expr, (0,))

        if t is not proto[2]:
            raise GhCmdExprError(_("Expression mismatch"), expr, ())

        try:
            for j in xrange(nargs):
                self.xprt_expr_compare(expr[j+1], proto[j+3], vdict, vlist)
        except GhCmdExprError, x:
            (why,) = x.args
            raise GhCmdExprError(why, expr, (j+1,) + x.path)

    def xprt_stmt(self, expr, equiv):
        """Add a statement or equivalence to an export interface

        stmt (name ((x ...) ...) (hyp ...) (conc ...))
        equiv (name ((x ...) ...) (hyp ...) (expr1 expr2))

        Multiple conclusion syntax is required.
        The 'equiv' argument is False when adding a statement and
        True when adding an equivalence.
        
        Presently, equivalences are allowed and used only for justifying
        the well-definedness of definitions having dummy variables on the
        RHS (the definiens). expr1 and expr2 must be expressions of the
        same kind. The equivalence means that provided the hypotheses
        and the distinct variables conditions are met, the substituted
        values of expr1 and expr2 are equivalent to each other, meaning
        that any occurrence of one of them anywhere in a larger expression
        may be substituted by the other one, regardless of context, without
        changing the 'meaning' in any way significant to the theory.
        As of now, such 'arbitrarily deep' substitutions are only made
        use of during definition expansion at the end of a proof.
        Example: equiv (wff_equiv () ((-> ph ps) (-> ps ph)) (ph ps))

        """
        errpath = None
        if not isinstance(expr, list) or len(expr) != 4:
            errpath = ()
        elif not isinstance(expr[0], basestring):
            errpath = (0,)
        elif not isinstance(expr[1], list):
            errpath = (1,)
        elif not isinstance(expr[2], list):
            errpath = (2,)
        # for now, don't allow single-conclusion syntax, as the determination
        # is not foolproof; a multi-conclusion theorem whose first conclusion
        # is a variable with a name equal to a term identifier may look like
        # a term with that identifier (although the proof isn't likely to work)
        elif not isinstance(expr[3], list):
            errpath = (3,)

        if errpath != None:
            raise GhCmdExprError(
                _("Expected "
                  "'%s (NAME ((DV1 DV2 ...) ...) (HYP ...) (CONC ...))'") %
                ('stmt', 'equiv')[equiv], expr, errpath)

        # Check for conflicts with existing variable names, doubly exported
        # statements, etc.
        if self.syms.has_key(expr[0]):
            raise GhCmdExprError(_("Symbol '%s' already exists in export") %
                                 expr[0], expr, (0,))

        namepf = self.prefix + expr[0]
        try:
            stmt = self.parent.syms[namepf]
        except KeyError:
            # TRANS: The first %s will be either 'stmt' or 'equiv'.
            raise GhCmdExprError(_("%(keyword)s '%(name)s' does not exist") %
                                 {"keyword" : ('stmt', 'equiv')[equiv],
                                  "name" : namepf},
                                 expr, (0,))

        # Note, stmt might be a stmt, a var, or an equiv.
        if equiv:
            if stmt[0] != Ghilbert.EQUIV:
                raise GhCmdExprError(_("'%s' is not an 'equiv'") % namepf,
                                     expr, (0,))
        else:
            if stmt[0] != Ghilbert.STMT:
                raise GhCmdExprError(_("'%s' is not a 'stmt'") % namepf,
                                     expr, (0,))

        # (Ghilbert.[STMT|EQUIV], name, nhyps, hyps_concs, vtuple, nwv, dvs,
        #  [hypnames])

        nhyps = stmt[2]
        hyps = expr[2]
        if len(hyps) != nhyps:
            raise GhCmdExprError(
                _("'%(stmt)s' has %(nhyps)d hypotheses but the export "
                  "interface file provided %(num)d") %
                {"stmt" : namepf, "nhyps" : nhyps, "num" : len(hyps)},
                expr, (2,))

        hyps_concs = stmt[3]
        concs = expr[3]
        nconcs = len(hyps_concs) - nhyps
        if len(concs) != nconcs:
            raise GhCmdExprError(
                _("'%(stmt)s' has %(nconcs)d conclusions but the export "
                  "interface file provided %(num)d") %
                {"stmt" : namepf, "nconcs" : nconcs, "num" : len(concs)},
                expr, (3,))
            
        vdict = {}
        vlist = [None] * len(stmt[4])
        try:
            for j in xrange(nhyps):
                self.xprt_expr_compare(hyps[j], hyps_concs[j], vdict, vlist)
        except GhCmdExprError, x:
            (why,) = x.args
            raise GhCmdExprError(why, expr, (2, j) + x.path)

        nhv = len(vlist)
        try:
            for j in xrange(nconcs):
                self.xprt_expr_compare(concs[j], hyps_concs[j + nhyps],
                                       vdict, vlist)
        except GhCmdExprError, x:
            (why,) = x.args
            raise GhCmdExprError(why, expr, (3, j) + x.path)

        dvs = self.dv_canonical(expr, vdict)

        # stmt[6] is the dvs from the existing statement/equivalence
        dvsproto = stmt[6]
        missing = dvsproto
        extra = dvs
        if dvsproto is not None and dvs is not None:
            missing = dvsproto - dvs
            extra = dvs - dvsproto
        if missing:
            raise VerifyError(
                _("Missing distinct variables pairs (%s)") %
                dvs_to_string(missing, vlist))
        if extra:
            print _("Warning: extra distinct variables pairs (%s)") % \
                  dvs_to_string(extra, vlist)
            pass

        # During the export, save the unprefixed statement name to
        # detect conflicts later
        self.syms[expr[0]] = stmt

    def xprt_term(self, expr):
        """export 'term' command handling

        term (KIND (TERMID KIND ...))
        """
        errpath = None
        try:
            kid, texp = expr
            if not isinstance(kid, basestring):
                errpath = (0,)
            elif (not isinstance(texp, list) or len(texp) < 1 or
                  not isinstance(texp[0], basestring)):
                errpath = (1,)
        except ValueError:
            errpath = ()

        if errpath is not None:
            raise GhCmdExprError(
                _('Expected term (KIND (TERMID KIND ...)'), expr, errpath)

        prefix = self.prefix
        parent = self.parent
        pkid = prefix + kid
        try:
            kr = parent.kinds[pkid]
        except KeyError:
            raise GhCmdExprError(_("Unknown kind '%s'") % pkid, expr, (0,))

        tid = texp[0]
        ptid = prefix + tid

        if self.terms.has_key(tid):
            raise GhCmdExprError(_("Term '%s' already exists in export") % tid,
                                 expr, (1, 0))
        try:
            t = parent.terms[ptid]
        except KeyError:
            raise GhCmdExprError(_("Unknown term '%s'") % ptid, expr, (1, 0))

        # t is (Ghilbert.TERMID, kind-tuple, term-name, def, arg-kind, ...)
        nargs = len(t) - 4

        if len(texp) != nargs + 1:
            raise GhCmdExprError(_("Term arity mismatch for '%s'") % ptid,
                                 expr, (1,))

        # There's an issue regarding the effect of kindbinds in an exported
        # interface file.  The exported file may itself give no indication
        # that two kinds that it uses were equivalent in the proof file,
        # yet may depend upon this equvalence in its terms and statements.
        # If the exported file is subsequently imported by a different proof
        # file, that import might give itself or lead to kind mismatch errors.
        # Perhaps there should be a test that an export file either declares
        # itself, or obtains from its parameter interfaces, all kindbinds
        # necessary to reflect the equivalences in effect in the proof context
        # between the kinds that the export file exports.
        # Ignore this for now.

        # Check that all the argument kinds are correct.
        try:
            for j in xrange(nargs):
                pakn = prefix + texp[j+1]
                ak = parent.kinds[pakn]
                k = t[j+4]
                if ak[2] != k[2]:
                    raise GhError(_("Argument kind mismatch"))
        except (TypeError, KeyError, GhError):
            raise GhCmdExprError(_("Term argument kind incorrect for '%s'") %
                                 ptid, expr, (1, j+1))
        self.myterms[tid] = t
        self.terms[tid] = t

    def xprt_kind(self, expr):
        try:
            (kindn,) = expr
            pkindn = self.prefix + kindn
            if self.kinds.has_key(kindn):
                raise GhCmdExprError(_("Kind '%s' already exists in export") %
                                     kindn, expr, (0,))
            k = self.parent.kinds[pkindn]
        except ValueError:
            raise GhCmdExprError(_("Expected 'kind (KIND)'"), expr, ())
        except KeyError:
            raise GhCmdExprError(_("Unknown kind '%s'") % pkindn, expr, (0,))

        self.kinds[kindn] = k   # for add_vars()
        self.mykinds[kindn] = k

    def kind_bind_ef(self, expr):
        prefix = self.prefix
        parent = self.parent
        try:
            (k1n, k2n) = expr
        except ValueError:
            raise GhCmdExprError(_("Expected 'kindbind (KIND1 KIND2)'"),
                                 expr, ())

        try:
            kn = k1n
            j = 0
            k1 = self.kinds[kn]
            kn = k2n
            j = 1
            k2 = self.kinds[kn]
        except KeyError:
            raise GhCmdExprError(
                _("Kind '%s' not available in export context") %
                kn, expr, (j,))
        except TypeError:
            raise GhCmdExprError(_("Expected 'kindbind (KIND1 KIND2)'"),
                                 expr, (j,))

        if k1[2] != k2[2]:
            raise VerifyError(
                _("Kinds '%(kind1)s' and '%(kind2)s' are not equivalent") %
                {"kind1" : k1n, "kind2" : k2n})
        # Indicate that the two kinds are equivalent not just in the proof
        # file context, but in the export context also? If we do that
        # we could check that kindbinds done in the export file occur early
        # enough that kind equivalence uses in the export file are valid
        # when they occur... ?

    def gh_export(self, expr):
        # export (IFACE_NAME PATH (IFACE_NAME ...) "PREFIX")
        errpath = None
        try:
            ifname, path, plist, prefix = expr
            if not isinstance(ifname, basestring):
                errpath = (0,)
            elif not isinstance(path, basestring):
                errpath = (1,)
            elif not isinstance(plist, list):
                errpath = (2,)
            elif (not isinstance(prefix, basestring) or len(prefix) < 2 or
                  prefix[0] != '"' or prefix[-1] != '"'):
                errpath = (3,)
        except ValueError:
            errpath = ()

        if errpath is not None:
            raise GhCmdExprError(
                _('Expected import (IFACE_NAME PATH (PARAM_IFACE ...) "PREFIX")'),
                expr, errpath)

        prefix = prefix[1:-1]

        if self.interfaces.has_key(ifname):
            raise GhCmdExprError(_("Interface '%s' already exists") % ifname,
                                 expr, (0,))

        if self.verbosity:
            print _('Exporting %s') % ifname

        np = len(plist)
        params = [None] * np
        try:
            for j in xrange(np):
                params[j] = self.interfaces[plist[j]]
        except KeyError:
            raise GhCmdExprError(_("Unknown interface name '%s'") % plist[j],
                                 expr, (2,j))
        except TypeError:
            raise GhCmdExprError(_("Interface parameter must be an "
                                   "interface identifier"), expr, (2,j))

        try:
            (istream, curdir) = get_stream(path, self.curdir,
                                           self.fpath, self.log)
        except GhError:
            raise GhCmdExprError(_("Cannot open interface file at '%s'") %
                                 path, (1,))
        
        try:
            child = Ghilbert(self.log)
            child.parent = self
            child.prefix = prefix
            child.params = params
            child.ifname = ifname
            child.curdir = curdir
            child.file = path

            scanner = StreamScanner(istream)
            while (1):
                word = scanner.get_token()
                if word is None:
                    break
                if word == '(' or word == ')':
                    raise VerifyError(
                        _("Expected command word, got '%(char)s' "
                          "at line %(line)d") %
                        {"char" : word, "line" : scanner.lineno})
                sexpr = read_sexp(scanner)
                if not isinstance(sexpr, list):
                    raise VerifyError(
                        _("Expected s-expression (...) command "
                          "argument at line %d") % scanner.lineno)
                if word == 'stmt':
                    child.xprt_stmt(sexpr, False)
                elif word == 'term':
                    child.xprt_term(sexpr)
                elif word == 'var':
                    child.add_vars(sexpr)
                elif word == 'kind':
                    child.xprt_kind(sexpr)
                elif word == 'kindbind':
                    child.kind_bind_ef(sexpr)
                elif word == 'equiv':
                    child.xprt_stmt(sexpr, True)
                elif word == 'param':
                    child.param(sexpr)
                elif word in ['thm', 'def', 'import', 'export']:
                    raise VerifyError(
                        _("Proof file command '%(cmd)s' encountered "
                          "in interface file at line %(line)d") %
                        {"cmd" : word, "line" : scanner.lineno})
                else:
                    child.log.warning(
                        _("Skipping unknown command '%(cmd)s' at "
                          "line '%(line)d'") %
                        {"cmd" : word, "line" : scanner.lineno})

            if child.params_used != len(params):
                raise VerifyError(
                    _("'export' provided %(num1)d parameters, but only "
                      "%(num2)d were used") %
                    {"num1" :  len(params), "num2" : child.params_used})

        except GhError, x:
            msg = _("Error in export: %(file)s line %(linenum)d") % \
                  {"file" : child.file, "linenum" : scanner.lineno}
            print >> sys.stderr, msg
            # Note, we don't undo history here, as we don't affect the
            # parent.
            (why,) = x.args
            raise GhError(msg + '\n' + why)
        finally:
            istream.close()

        # We should no longer need child.terms and child.kinds. Free
        # them to save memory. (If this interface is used later via 'param',
        # .myterms and .mykinds will still be available.)
        # We also don't need child.syms, since an exported interface
        # introduces no _new_ statements/equivs, we get the debug variable
        # names from the interface that originally introduced statements.
        child.terms = None
        child.kinds = None
        child.syms = None

        self.interfaces[ifname] = child
        self.push_history((Ghilbert.EXPORT, child, path))

    def read_proof_file_from_scanner(self, scanner, stop_cond):

        while (1):
            self.pip = None
            word = scanner.get_token()
            if word is None:
                break
            if word == '(' or word == ')':
                raise VerifyError(_("Expected command word, got '%s'") % word)
            sexpr = read_sexp(scanner)
            if not isinstance(sexpr, list):
                raise VerifyError(
                    _("Expected s-expression (...) command argument"))
            if word == 'thm':
                self.add_thm(sexpr, stop_cond)
            elif word == 'def':
                self.add_def(sexpr)
            elif word == 'var':
                self.add_vars(sexpr)
            elif word == 'kindbind':
                self.kind_bind_pf(sexpr)
            elif word == 'import':
                self.gh_import(sexpr)
            elif word == 'export':
                self.gh_export(sexpr)
            elif word in ['stmt', 'term', 'kind', 'param', 'equiv']:
                raise VerifyError(
                  _("Interface file command '%s' encountered in proof file") %
                  word)
            else:
                self.log.warning(_("Skipping unknown command '%s'") % word)

            scanner.set_good()
            if stop_cond >= -1:
                break


if __name__ == "__main__":
    i = 1
    try:
        fpath = os.environ['GHILBERT_PATH'].split(':')
    except KeyError:
        fpath = ['/']
    file = ''
    convert = False
    verbosity = 1
    while i < len(sys.argv):
        arg = sys.argv[i]
        if arg[0] != '-':
            break
        if arg == '--':
            i = i + 1
            break
        if arg[:2] == '-v':
            if len(arg) > 2:
                param = arg[2:]
            else:
                i += 1
                param = sys.argv[i]
            verbosity = int(param)
        elif arg[:2] == '-c':
            convert = True
        else:
            print >> sys.stderr, 'Unknown argument:', arg
        i += 1
    if i < len(sys.argv):
        file = sys.argv[i]
        if i + 1 < len(sys.argv):
            print >> sys.stderr, 'Warning, ignoring extra arguments'

    gh = Ghilbert(logging.getLogger())
    gh.fpath = fpath
    gh.curdir = os.getcwd()
    gh.verbosity = verbosity
    if file:
        gh.file = file
        (instream, gh.curdir) = get_stream(file, gh.curdir, gh.fpath, gh.log)
    else:
        # TRANS: This is a fake filename used in some error messages when
        # the proof file is read from standard input:
        gh.file = _('<standard input>')
        instream = sys.stdin
    if convert: # convert to multi-conclusion form
        scanner = StreamScanner(instream)
        while True:
            word = scanner.get_token()
            if word == None:
                break
            arg = read_sexp(scanner)
            if word == 'stmt' or word == 'thm':
                c = arg[3]
                arg[3] = [c]
            s = sexp_to_string(arg)
            sys.stdout.write(word + ' ' + s + '\n')
    else:
        scanner = StreamScanner(instream)
        try:
            gh.read_proof_file_from_scanner(scanner, False)
        except GhCmdExprError, x:
            (why,) = x.args
            print >> sys.stderr, 'GhCmdExprError path:', x.path
            print >> sys.stderr, 'expr: ', x.expr
            print >> sys.stderr, 'at %s line %d' % (self.file, scanner.lineno)
            raise
        #print "Enter a line to continue:"
        #sys.stdin.readline()