# mmverify.py -- Proof verifier for the Metamath language
# Copyright (C) 2002 Raph Levien raph (at) acm (dot) org
# This program is free software; you can redistribute it and/or modify
# it under the terms of the GNU General Public License

# This program has been tested with python 2.2.1.  It does not run on 1.5.2.

# Before using this program, any compressed proofs must be expanded with the
# Metamath program, e.g. for the set.mm database:
#   $ ./metamath 'read set.mm' 'save proof *' 'write s set.mm' exit > /dev/null
# To run the program, type
#   $ python mmverify.py < set.mm > set.log
# and set.log will have the verification results.

# (nm 27-Jun-2005) mmverify.py requires that a $f hypothesis must not occur
# after a $e hypothesis in the same scope, even though this is allowed by
# the Metamath spec.  This is not a serious limitation since it can be
# met by rearranging the hypothesis order.
# (rl 2-Oct-2006) removed extraneous line found by Jason Orendorff

import string

verbosity = 1

class toks:
    def __init__(self, lines):
        self.lines = lines
        self.tokbuf = []
    def read(self):
        while self.tokbuf == []:
            line = self.lines.readline()
            if line == '':
                return None
            line = line.replace('$(', ' $( ')
            line = line.replace('$)', ' $) ')
            self.tokbuf = line.split()
            self.tokbuf.reverse()
        return self.tokbuf.pop()

class Frame:
    def __init__(self):
        self.c = []
        self.v = []
        self.d = []
        self.f = []
        self.e = []

class FrameStack:
    def __init__(self):
        self.stack = []
    def push(self):
        frame = Frame()
        self.stack.append(frame)
    def pop(self):
        self.stack.pop()
    def add_c(self, tok):
        frame = self.stack[-1]
        if tok in frame.c:
            raise 'const already defined in scope'
        if tok in frame.v:
            raise 'const already defined as var in scope'
        frame.c.append(tok)
    def add_v(self, tok):
        frame = self.stack[-1]
        if tok in frame.v:
            raise 'var already defined in scope'
        if tok in frame.c:
            raise 'var already defined as const in scope'
        frame.v.append(tok)
    def add_f(self, var, kind):
        if not self.lookup_v(var):
            raise ('var in $f not defined: ' + var)
        if not self.lookup_c(kind):
            raise ('const in $f not defined' + kind)
        frame = self.stack[-1]
        for (v, k) in frame.f:
            if v == var:
                raise 'var in $f already defined in scope'
        frame.f.append((var, kind))
    def add_e(self, stat):
        frame = self.stack[-1]
        frame.e.append(stat)
    def add_d(self, stat):
        frame = self.stack[-1]
        for i in range(len(stat)):
            for j in range(i + 1, len(stat)):
                x, y = stat[i], stat[j]
                if x > y:
                    x, y = y, x
                if x != y and not (x, y) in frame.d:
                    frame.d.append((x, y))
    def lookup_c(self, tok):
        for i in range(len(self.stack) - 1, -1, -1):
            if tok in self.stack[i].c:
                return 1
    def lookup_v(self, tok):
        for i in range(len(self.stack) - 1, -1, -1):
            if tok in self.stack[i].v:
                return 1
    def lookup_f(self, var):
        for i in range(len(self.stack) - 1, -1, -1):
            frame = self.stack[i]
            for (v, k) in frame.f:
                if v == var:
                    return k
    def lookup_d(self, x, y):
        # return 1 if disjoint, None if not
        if x > y:
            x, y = y, x
        for i in range(len(self.stack) - 1, -1, -1):
            frame = self.stack[i]
            if (x, y) in frame.d:
                return 1
    def make_assertion(self, stat):
        mand_vars = []
        hyps = []
        for fr in self.stack:
            hyps.extend(fr.e)
        frame = self.stack[-1]
        visible = hyps[:]
        visible.append(stat)
        for hyp in visible:
            for tok in hyp:
                if self.lookup_v(tok) and tok not in mand_vars:
                    mand_vars.append(tok)
        dm = []
        for i in range(len(self.stack)):
            fr = self.stack[i]
            for (x, y) in fr.d:
                if x in mand_vars and y in mand_vars and not (x, y) in dm:
                    dm.append((x, y))
        mand_hyps = []
        for i in range(len(self.stack) - 1, -1, -1):
            fr = self.stack[i]
            for j in range(len(fr.f) - 1, -1, -1):
                (v, k) = fr.f[j]
                if v in mand_vars:
                    mand_hyps.append((k, v))
                    mand_vars.remove(v)
        mand_hyps.reverse()
        if verbosity >= 18:
            print 'ma:', (dm, mand_hyps, hyps, stat)
        return (dm, mand_hyps, hyps, stat)

class MM:
    def __init__(self):
        self.fs = FrameStack()
        self.labels = {}
    def readc(self, toks):
        while 1:
            tok = toks.read()
            if tok == None:
                return None
            if tok == '$(':
                while 1:
                    tok = toks.read()
                    if tok == '$)':
                        break
            else:
                return tok
    def readstat(self, toks):
        # read out to $. token; return list
        stat = []
        while 1:
            tok = self.readc(toks)
            if tok == None:
                raise 'EOF before $.'
            elif tok == '$.':
                break
            stat.append(tok)
        return stat
    def read(self, toks):
        self.fs.push()
        label = None
        while 1:
            tok = self.readc(toks)
            if tok == None or tok == '$}':
                break
            elif tok == '$c':
                for tok in self.readstat(toks):
                    self.fs.add_c(tok)
            elif tok == '$v':
                for tok in self.readstat(toks):
                    self.fs.add_v(tok)
            elif tok == '$f':
                stat = self.readstat(toks)
                if len(stat) != 2: raise '$f must have be length 2'
                if verbosity >= 15: print label, '$f', stat[0], stat[1], '$.'
                self.fs.add_f(stat[1], stat[0])
                if not label: raise '$f must have label'
                self.labels[label] = ('$f', stat[0], stat[1])
                label = None
            elif tok == '$a':
                stat = self.readstat(toks)
                if not label: raise '$a must have label'
                self.labels[label] = ('$a', self.fs.make_assertion(stat))
                label = None
            elif tok == '$e':
                stat = self.readstat(toks)
                self.fs.add_e(stat)
                if not label: raise '$e must have label'
                self.labels[label] = ('$e', stat)
                label = None
            elif tok == '$p':
                stat = self.readstat(toks)
                proof = None
                try:
                    i = stat.index('$=')
                    proof = stat[i + 1:]
                    stat = stat[:i]
                except ValueError:
                    raise '$p must contain proof after $='
                if not label: raise '$p must have label'
                if verbosity >= 1: print 'verifying', label
                self.verify(stat, proof)
                self.labels[label] = ('$p', self.fs.make_assertion(stat))
                label = None
            elif tok == '$d':
                stat = self.readstat(toks)
                self.fs.add_d(stat)
            elif tok == '${':
                self.read(toks)
            elif tok[0] != '$':
                label = tok
            else:
                print 'tok:', tok
        self.fs.pop()
    def apply_subst(self, stat, subst):
        result = []
        for tok in stat:
            if subst.has_key(tok):
                result.extend(subst[tok])
            else:
                result.append(tok)
        if verbosity >= 20: print 'apply_subst', (stat, subst), '=', result
        return result
    def find_vars(self, stat):
        vars = []
        for x in stat:
            if not x in vars and self.fs.lookup_v(x):
                vars.append(x)
        return vars
    def verify(self, stat, proof):
        stack = []
        for label in proof:
            step = self.labels[label]
            if verbosity >= 10: print label, ':', step
            if step[0] == '$f':
                stack.append([step[1], step[2]])
            elif step[0] in ('$a', '$p'):
                (distinct, mand_var, hyp, result) = step[1]
                if verbosity >= 12: print (distinct, mand_var, hyp, result)
                npop = len(mand_var) + len(hyp)
                sp = len(stack) - npop
                if sp < 0: raise 'stack underflow'
                subst = {}
                for (k, v) in mand_var:
                    entry = stack[sp]
                    if entry[0] != k:
                        print (k, v), entry
                        raise "stack entry doesn't match mandatory var hyp"
                    subst[v] = entry[1:]
                    sp += 1
                if verbosity >= 15: print 'subst:', subst
                for x, y in distinct:
                    if verbosity >= 16:
                        print 'dist', x, y, subst[x], subst[y]
                    x_vars = self.find_vars(subst[x])
                    y_vars = self.find_vars(subst[y])
                    if verbosity >= 16:
                        print 'V(x) =', x_vars
                        print 'V(y) =', y_vars
                    for gam in x_vars:
                        for delt in y_vars:
                            if gam == delt:
                                raise "disjoint violation " + gam
                            x, y = gam, delt
                            if x > y:
                                x, y = y, x
                            if not self.fs.lookup_d(x, y):
                                raise "disjoint violation " + x + ", " + y
                for h in hyp:
                    entry = stack[sp]
                    subst_h = self.apply_subst(h, subst)
                    if entry != subst_h:
                        print 'st:', entry
                        print 'hy:', subst_h
                        raise "stack entry doesn't match hypothesis"
                    sp += 1
                del stack[len(stack) - npop:]
                stack.append(self.apply_subst(result, subst))
            elif step[0] == '$e':
                stack.append(step[1])
            if verbosity >= 12: print 'st:', stack
        if len(stack) != 1: raise 'stack has >1 entry at end'
        if stack[0] != stat: raise "assertion proved doesn't match"

    def dump(self):
        print self.labels

import sys
mm = MM()
mm.read(toks(sys.stdin))
#mm.dump()