#!/usr/bin/env python import re import string import array # The following commands may be useful to split the stdout of this # script to Ghilbert interface and proof files, respectively: # # grep -v -E '^thm' ../raw.gh > set_mm.ghi # grep -E '^(thm|tvar|var)' ../raw.gh > set_mm.gh # # They'll need a bit of manual fixup: # 1. The gh needs to import the ghi verbosity = 0 loose = 0 # The term_renames are because parens are not valid as part # of a token. Currently, thm_renames are doubly not required, because # both Ghilbert has separate names for terms and proof steps, and # because the new policy of set.mm is to enforce such separation # anyway. thm_rename = {} term_rename = {'(.': 'C:', '(_': 'C_', '(/)': '{/}', '(,)': '],[', '(,]': '],]', '[,)': '[,['} def notify(msg): print '!!', msg def sexp_to_string(sexp): buf = array.array('c') sexp_to_string_rec(buf, sexp) return buf.tostring() def sexp_to_string_rec(buf, sexp): if type(sexp) == type('str'): buf.fromstring(sexp) elif type(sexp) == type([]): buf.fromstring('(') if loose: sp_string = ' ' else: sp_string = '' for el in sexp: buf.fromstring(sp_string) sexp_to_string_rec(buf, el) sp_string = ' ' if loose: buf.fromstring(' ') buf.fromstring(')') def flattenrec(result, list): if type(list) == type('string'): result.append(list) else: for el in list: flattenrec(result, el) def flatten(list): result = [] flattenrec(result, list) return result class toks: def __init__(self, lines): self.lines = lines self.line = None self.pos = 0 self.tok_re = re.compile(r'\s*(\$[\(\)]|\S+)') def read(self, re = None): while 1: if self.line == None: self.line = self.lines.readline() if self.line == '': return None self.pos = 0 tok_m = self.tok_re.match(self.line, self.pos) if tok_m: self.pos = tok_m.end() return tok_m.group(1) else: self.line = None def read_comment(self): if self.line == None: self.line = self.lines.readline() if self.line == '': return None self.pos = 0 pos = self.line.find('$)', self.pos) if pos == self.pos: self.pos = pos + 2 result = '$)' elif pos >= 0: result = self.line[self.pos:pos] self.pos = pos else: result = self.line[self.pos:].rstrip() self.line = None return result class Frame: def __init__(self): self.c = [] self.v = [] self.d = [] self.f = [] self.e = [] self.elabels = [] 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: notify('const already defined in scope') frame.c.append(tok) if tok in frame.v: notify('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: notify('var already defined in scope') if tok in frame.c: notify('var already defined as const in scope') frame.v.append(tok) def add_f(self, var, kind): if not self.lookup_v(var): notify('var in $f not defined: ' + var) if not self.lookup_c(kind): notify('const in $f not defined' + kind) frame = self.stack[-1] for (v, k) in frame.f: if v == var: notify('var in $f already defined in scope') frame.f.append((var, kind)) def add_e(self, label, stat): frame = self.stack[-1] frame.e.append(stat) frame.elabels.append(label) 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 get_dv(self, fv): dv = [] for i in range(len(self.stack) - 1, -1, -1): frame = self.stack[i] for d in frame.d: gh_dv = [] for v in d: if v in fv: gh_dv.append(v) if len(gh_dv) >= 2: dv.append(gh_dv) return dv 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: c_conn = ('=', 'e.', '=/=', 'e/', '(_', '(.', 'Po', 'Or', 'Fr', 'We', 'Fn') c_bin = ('\\', 'u.', 'i^i', 'X.', '|`', '"', 'o.', '`', '/.') c_un = ('P~', 'suc', "`'", 'dom', 'ran', '-u') c_pred = ('Tr', 'Ord', 'Lim', 'Rel', 'Fun', 'Er') labelmap = {'weq': 'wceq', 'wel': 'wcel', 'wsb': 'wsbc'} def __init__(self): self.fs = FrameStack() self.labels = {} self.n_mm_steps = 0 self.n_gh_steps = 0 self.seenvar = {} self.seenterm = {} self.seenkind = {} self.flabels = {} self.flabel_ix = 0 self.c_const = [] self.last_comment = None def readc(self, toks): while 1: tok = toks.read() if tok == None: return None if tok == '$(': self.last_comment = [] while 1: tok = toks.read_comment() if tok == '$)': break else: self.last_comment.append(tok) else: return tok def readstat(self, toks): # read out to $. token; return list stat = [] while 1: tok = self.readc(toks) if tok == None: notify('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: notify('$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: notify('$f must have label') self.labels[label] = ('$f', stat[0], stat[1]) self.flabels[stat[1]] = self.flabel_ix, label self.flabel_ix += 1 label = None cmd, kind = 'tvar', stat[0] if kind == 'set': cmd, kind = 'var', 'class' if not self.seenkind.has_key(kind): self.seenkind[kind] = 1 print 'kind', sexp_to_string([kind]) if not self.seenvar.has_key(stat[1]): self.seenvar[stat[1]] = cmd, kind print cmd, sexp_to_string([kind, stat[1]]) elif tok == '$a': stat = self.readstat(toks) if not label: notify('$a must have label') cvlabel = self.labelmap.get(label, label) self.labels[cvlabel] = ('$a', self.fs.make_assertion(stat)) self.a_to_gh(cvlabel, stat) label = None elif tok == '$e': stat = self.readstat(toks) self.fs.add_e(label, stat) if not label: notify('$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: notify('$p must contain proof after $=') if not label: notify('$p must have label') if verbosity >= 1: print '# converting', label # self.verify(stat, proof) hyps = [] fv = [] for fr in self.fs.stack: for i in range(len(fr.e)): hyp = fr.e[i][1:] self.find_vars(hyp, fv) hyps.extend([fr.elabels[i], self.mm_to_sexp(hyp)]) gh_stmt = self.mm_to_sexp(stat[1:]) self.find_vars(stat[1:], fv) if proof[0] == '(': mvars = fv[:] self.find_vars(stat, mvars) # sort in order of $f appearance mvars = [self.flabels[v] for v in mvars] mvars.sort() hyplabels = [v for ix, v in mvars] + hyps[::2] proof = self.decompress_proof(hyplabels, proof) dv = self.dv_to_new_gh(self.fs.get_dv(fv)) gh_proof = self.to_gh(proof) self.n_gh_steps += len(gh_proof) ghlabel = thm_rename.get(label, label) gh_cmd = [ghlabel, dv, hyps, gh_stmt] + gh_proof if stat[0] == '|-': self.format_comment() print 'thm', sexp_to_string(gh_cmd) 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 decompress_proof(self, hyplabels, proof): i = proof.index(')') labels = proof[1:i] compressed = ''.join(proof[i+1:]) newproof = [] savedsteps = hyplabels + labels hi = 0 for c in compressed: if c == 'Z': savedsteps.append(newproof[-1]) elif c < 'U': x = hi * 20 + ord(c) - ord('@') hi = 0 step = savedsteps[x - 1] if x - 1 < len(hyplabels) + len(labels): st = self.labels[step] if st[0] in ('$a', '$p'): (distinct, mand_var, hyp, result) = st[1] nmand = len(mand_var) + len(hyp) if nmand: step = newproof[-nmand:] + [step] del newproof[-nmand:] #print newproof, x, step newproof.append(step) else: hi = hi * 5 + ord(c) - ord('T') return flatten(newproof) 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 = None): if vars == None: vars = [] for x in stat: if not x in vars and self.fs.lookup_v(x): vars.append(x) return vars def dv_to_new_gh(self, dv): # Format dv's to new Ghilbert standards (tv first, followed by vars) new_dv_tvars = [] new_dv_map = {} for clause in dv: tvars = [] vars = [] for v in clause: if self.seenvar[v][0] == 'var': vars.append(v) else: tvars.append(v) if len(vars) and len(tvars): for tv in tvars: if not tv in new_dv_tvars: new_dv_tvars.append(tv) new_dv_map[tv] = [tv] for v in vars: new_dv_map[tv].append(v) new_dv = [] for tv in new_dv_tvars: new_dv.append(new_dv_map[tv]) return new_dv 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: notify('stack underflow') subst = {} for (k, v) in mand_var: entry = stack[sp] if entry[0] != k: print (k, v), entry notify("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: notify("disjoint violation " + gam) x, y = gam, delt if x > y: x, y = y, x if not self.fs.lookup_d(x, y): notify("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 notify("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: notify('stack has >1 entry at end') if stack[0] != stat: notify("assertion proved doesn't match") def to_gh(self, proof): stack = [] gh_proof = [] for label in proof: cvlabel = self.labelmap.get(label, label) step = self.labels[cvlabel] if verbosity >= 10: print label, ':', step if label == 'cv': continue if step[0] == '$f': stack.append(step[2]) elif step[0] in ('$a', '$p'): self.n_mm_steps += 1 (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: notify('stack underflow') step = [] mvs = map(lambda x: x[1], mand_var) hypvars = [] for h in hyp: for tok in h: if tok in mvs and tok not in hypvars: hypvars.append(tok) sortmvs = [] for tok in result: if tok in mvs and tok not in sortmvs: sortmvs.append(tok) #print mvs, 'hypvars:', hypvars mvmap = {} for (k, v) in mand_var: entry = stack[sp] mvmap[v] = entry sp += 1 # ...distinct here for h in hyp: entry = stack[sp] step.append(entry) #gh_proof.append(entry) sp += 1 del stack[len(stack) - npop:] for v in sortmvs: if v not in hypvars: step.append(mvmap[v]) if result[0] == '|-': gh_proof.append(mvmap[v]) if result[0] == '|-': step.append(thm_rename.get(label, label)) gh_proof.append(thm_rename.get(label, label)) elif label != cvlabel: step[0] = step[0] if label != 'wsb': step[1] = step[1] step.insert(0, self.seenterm[cvlabel]) elif self.seenterm.has_key(label): step.insert(0, self.seenterm[label]) else: notify('seenterm fail: ' + `result`) stack.append(step) elif step[0] == '$e': stack.append(label) gh_proof.append(label) if verbosity >= 12: print 'st:', stack if len(stack) != 1: notify('stack has >1 entry at end') return gh_proof def mm_to_sexp_rec(self, mm, i): tok = mm[i] i += 1 (j, a) = self.mm_to_sexp_class(mm, i - 1) if a != None: (k, b) = self.mm_to_sexp_class(mm, j) if b != None: (k, c) = self.mm_to_sexp_class(mm, k) if c != None: return (k, ['br', a, b, c]) op = mm[j] j += 1 if op in self.c_conn: (j, b) = self.mm_to_sexp_class(mm, j) if b == None: raise SyntaxError('expected rhs of c_conn ' + op) return (j, [term_rename.get(op, op), a, b]) elif op == ':': (j, b) = self.mm_to_sexp_class(mm, j) op += mm[j] if not op in (':-->', ':-1-1->', ':-onto->', ':-1-1-onto->'): raise SyntaxError('unknown function connective ' + op) j += 1 (j, c) = self.mm_to_sexp_class(mm, j) return (j, [op, a, b, c]) elif op == 'Isom': (j, b) = self.mm_to_sexp_class(mm, j) if mm[j] != ',': raise SyntaxError('expected , in Isom') j += 1 (j, c) = self.mm_to_sexp_class(mm, j) if mm[j] != '(': raise SyntaxError('expected ( in Isom') j += 1 (j, d) = self.mm_to_sexp_class(mm, j) if mm[j] != ',': raise SyntaxError('expected , in Isom') j += 1 (j, e) = self.mm_to_sexp_class(mm, j) if mm[j] != ')': raise SyntaxError('expected ) in Isom') j += 1 return (j, [op, a, b, c, d, e]) else: raise SyntaxError('unknown class connective ' + op) if tok == '-.': (i, result) = self.mm_to_sexp_rec(mm, i) return (i, ['-.', result]) elif tok in ('A.', 'E.', 'E!', 'E*'): op = tok v = mm[i] i += 1 if mm[i] == 'e.': i += 1 (i, a) = self.mm_to_sexp_class(mm, i) (i, ph) = self.mm_to_sexp_rec(mm, i) return (i, [op + 'e.', v, a, ph]) (i, ph) = self.mm_to_sexp_rec(mm, i) return (i, [op, v, ph]) elif tok == '(': (i, a) = self.mm_to_sexp_rec(mm, i) op = mm[i] i += 1 (i, b) = self.mm_to_sexp_rec(mm, i) if mm[i] == op: i += 1 (i, c) = self.mm_to_sexp_rec(mm, i) if mm[i] != ')': SyntaxError('expected )') i += 1 return (i, [op + op, a, b, c]) if mm[i] != ')': raise SyntaxError('expected )') i += 1 return (i, [op, a, b]) elif tok == '[': (i, a) = self.mm_to_sexp_class(mm, i) tok = mm[i] i += 1 if tok == '/': v = mm[i] i += 1 if mm[i] != ']': raise SyntaxError('expected ]') i += 1 (i, ph) = self.mm_to_sexp_rec(mm, i) return (i, ['[/]', a, v, ph]) else: raise SyntaxError('unknown [ form ' + tok) elif tok in self.c_pred: (i, a) = self.mm_to_sexp_class(mm, i) if a == None: raise SyntaxError('expected class after ' + tok) return (i, [tok, a]) elif self.fs.lookup_v(tok) and self.fs.lookup_f(tok) == 'wff': return (i, tok) else: raise SyntaxError('unknown wff ' + `mm[i:]`) def mm_to_sexp_class(self, mm, i): tok = mm[i] i += 1 if tok in self.c_const: return (i, [term_rename.get(tok, tok)]) elif tok == '(': (i, a) = self.mm_to_sexp_class(mm, i) if a == None: return (i, None) op = mm[i] if op == 'e.': i += 1 (i, b) = self.mm_to_sexp_class(mm, i) if b == None: return (i, None) if mm[i] == '|->': i += 1 (i, c) = self.mm_to_sexp_class(mm, i) if c == None: raise SyntaxError('expected B for ( x e. A |-> B )') if mm[i] != ')': raise SyntaxError('expected ) for ( x e. A |-> B )') i += 1 return (i, ['e.|->', a, b, c]) elif mm[i] == ',': i += 1 (i, c) = self.mm_to_sexp_class(mm, i) if c == None: raise SyntaxError('expected y for ( x e. A , y e. B |-> C )') if mm[i] != 'e.': raise SyntaxError('expected e. for ( x e. A , y e. B |-> C )') i += 1 (i, d) = self.mm_to_sexp_class(mm, i) if d == None: raise SyntaxError('expected B for ( x e. A , y e. B |-> C )') if mm[i] != '|->': raise SyntaxError('expected |-> for ( x e. A , y e. B |-> C )') i += 1 (i, e) = self.mm_to_sexp_class(mm, i) if e == None: raise SyntaxError('expected C for ( x e. A , y e. B |-> C )') if mm[i] != ')': raise SyntaxError('expected ) for ( x e. A |-> B )') i += 1 return (i, ['e.,e.|->', a, b, c, d, e]) else: return (i, None) if op in self.c_bin: i += 1 (i, b) = self.mm_to_sexp_class(mm, i) if b == None: raise SyntaxError('expected rhs for ' + op) if mm[i] != ')': raise SyntaxError('expected ) for c_bin ' + op) i += 1 return (i, [op, a, b]) else: (i, b) = self.mm_to_sexp_class(mm, i) if b == None: return (i, None) (i, c) = self.mm_to_sexp_class(mm, i) if c == None: return (i, None) if mm[i] != ')': return (i, None) i += 1 return (i, ['opr', a, b, c]) elif tok == '{': (i, a) = self.mm_to_sexp_class(mm, i) if a == None: raise SyntaxError('expected class after {') tok = mm[i] i += 1 if tok == '|': (i, ph) = self.mm_to_sexp_rec(mm, i) if mm[i] != '}': raise SyntaxError('expected }') i += 1 if type(a) == type('x'): return (i, ['{|}', a, ph]) elif a[0] == '<,>': if a[1][0] == '<,>': if type(a[1][1]) == type('x') and type(a[1][2]) == type('x') and type(a[2]) == type('x'): return (i, ['{<<,>,>|}', a[1][1], a[1][2], a[2], ph]) if type(a[1]) != type('x') or type(a[2]) != type('x'): raise SyntaxError('unknown pair abstraction ' + `a`) return (i, ['{<,>|}', a[1], a[2], ph]) else: raise SyntaxError('unknown abstraction form: ' + `a`) elif tok == 'e.': (i, b) = self.mm_to_sexp_class(mm, i) if b == None: raise SyntaxError('expected class A in { x e. A | ph }') if mm[i] != '|': raise SyntaxError('expected | in { x e. A | ph }') i += 1 (i, ph) = self.mm_to_sexp_rec(mm, i) if mm[i] != '}': raise SyntaxError('expected }') i += 1 if type(a) == type('x'): return (i, ['{e.|}', a, b, ph]) else: raise SyntaxError('unknown abstraction form: ' + `a`) elif tok == '}': return (i, ['{}', a]) elif tok == ',': (i, b) = self.mm_to_sexp_class(mm, i) if b == None: raise SyntaxError('expected class B in { A , B }') if mm[i] == ',': i += 1 (i, c) = self.mm_to_sexp_class(mm, i) if mm[i] != '}': raise SyntaxError('expected } in { A , B , C }') i += 1 return (i, ['{,,}', a, b, c]) if mm[i] != '}': raise SyntaxError('expected } in { A , B }') i += 1 return (i, ['{,}', a, b]) else: raise SyntaxError('unknown abstraction separator: ' + tok) elif tok == '<.': (i, a) = self.mm_to_sexp_class(mm, i) if a == None: raise SyntaxError('expected class after <.') if mm[i] != ',': raise SyntaxError('expected , after <.') i += 1 (i, b) = self.mm_to_sexp_class(mm, i) if mm[i] != '>.': raise SyntaxError('expected >. after <.') i += 1 return (i, ['<,>', a, b]) elif tok == '[': (i, a) = self.mm_to_sexp_class(mm, i) if a == None: raise SyntaxError('expected class after [') if mm[i] == ']': i += 1 (i, r) = self.mm_to_sexp_class(mm, i) return (i, ['[]', a, r]) return (i, None) elif tok == 'if': if mm[i] != '(': raise SyntaxError('ifexpected (') i += 1 (i, ph) = self.mm_to_sexp_rec(mm, i) if mm[i] != ',': raise SyntaxError('if expected ,') i += 1 (i, a) = self.mm_to_sexp_class(mm, i) if mm[i] != ',': raise SyntaxError('if expected ,') i += 1 (i, b) = self.mm_to_sexp_class(mm, i) if mm[i] != ')': raise SyntaxError('if expected )') i += 1 return (i, ['if', ph, a, b]) elif tok == 'sup': if mm[i] != '(': raise SyntaxError(tok + ' expected (') i += 1 (i, a) = self.mm_to_sexp_class(mm, i) if mm[i] != ',': raise SyntaxError(tok + ' expected ,') i += 1 (i, b) = self.mm_to_sexp_class(mm, i) if mm[i] != ',': raise SyntaxError(tok + ' expected ,') i += 1 (i, r) = self.mm_to_sexp_class(mm, i) if mm[i] != ')': raise SyntaxError(tok + ' expected )') i += 1 return (i, [tok, a, b, r]) elif tok == 'rec': if mm[i] != '(': raise SyntaxError(tok + ' expected (') i += 1 (i, f) = self.mm_to_sexp_class(mm, i) if mm[i] != ',': raise SyntaxError(tok + ' expected ,') i += 1 (i, a) = self.mm_to_sexp_class(mm, i) if mm[i] != ')': raise SyntaxError(tok + ' expected )') i += 1 return (i, [tok, f, a]) elif tok in ('U.', '|^|'): (i, a) = self.mm_to_sexp_class(mm, i) return (i, [tok, a]) elif tok in ('U_', '|^|_', 'X_'): (i, a) = self.mm_to_sexp_class(mm, i) if type(a) == type('x') and mm[i] == 'e.': (j, b) = self.mm_to_sexp_class(mm, i + 1) if b != None: (j, c) = self.mm_to_sexp_class(mm, j) if c != None: return (j, [tok, a, b, c]) elif tok == '[_': (i, a) = self.mm_to_sexp_class(mm, i) tok = mm[i] i += 1 if tok == '/': v = mm[i] i += 1 if mm[i] != ']_': raise SyntaxError('expected ]_') i += 1 (i, b) = self.mm_to_sexp_class(mm, i) return (i, ['[_/]_', a, v, b]) else: raise SyntaxError('unexpected [_ token ' + tok) elif tok == 'sum_': k = mm[i] i += 1 tok = mm[i] i += 1 if tok == 'e.': (i, a) = self.mm_to_sexp_class(mm, i) (i, b) = self.mm_to_sexp_class(mm, i) return (i, ['sum_', k, a, b]) else: raise SyntaxError('unexpected sum_ token ' + tok) elif tok == 'gcd': if mm[i] != '(': raise SyntaxError('expected ( in gcd ( A , B )') i += 1 (i, a) = self.mm_to_sexp_class(mm, i) if mm[i] != ',': raise SyntaxError('expected , in gcd ( A , B )') i += 1 (i, b) = self.mm_to_sexp_class(mm, i) if mm[i] != ')': raise SyntaxError('expected ) in gcd ( A , B )') i += 1 return (i, ['gcd', a, b]) elif tok in self.c_un: (i, a) = self.mm_to_sexp_class(mm, i) return (i, [tok, a]) elif self.fs.lookup_v(tok): k = self.fs.lookup_f(tok) if k == 'class': return (i, tok) elif k == 'set': return (i, tok) return (i, None) def mm_to_sexp(self, mm): if verbosity >= 20: print 'converting', mm (i, result) = self.mm_to_sexp_rec(mm, 0) if i < len(mm): SyntaxError('extra junk: ' + string.join(mm[i:])) return result def a_to_gh(self, label, stat): if stat[0] == '|-': # axiom or definition fv = self.find_vars(stat) hyps = [] for fr in self.fs.stack: for i in range(len(fr.e)): hyp = fr.e[i][1:] fv.extend(self.find_vars(hyp)) hyps.append(self.mm_to_sexp(hyp)) dv = self.dv_to_new_gh(self.fs.get_dv(fv)) gh_cmd = [label, dv, hyps, self.mm_to_sexp(stat[1:])] self.format_comment() print 'stmt', sexp_to_string(gh_cmd) else: # well-formedness definition kind = stat[0] if not self.seenkind.has_key(kind): self.seenkind[kind] = 1 print 'kind', sexp_to_string([kind]) if kind == 'wff': gh_exp = self.mm_to_sexp(stat[1:]) elif kind == 'class': if len(stat) == 2 and not self.fs.lookup_v(stat[1]): # automatically add nullary terms to grammar self.c_const.append(stat[1]) i, gh_exp = self.mm_to_sexp_class(stat, 1) else: print 'unknown kind:', kind print '# axiom:', label, stat return if gh_exp == None: print 'error parsing ' + string.join(stat[1:]) raise SyntaxError('parse error') if not self.seenterm.has_key(label): gh_cmd = [kind, gh_exp] print 'term', sexp_to_string(gh_cmd) self.seenterm[label] = gh_exp[0] def dump(self): print self.labels def format_math(self, mstr): # Convert a Metamath term to Barghest markup str = mstr.strip() l = str.split() try: sexp = self.mm_to_sexp(l) return '#' + sexp_to_string(sexp) + '#' except: pass try: # Sometimes Norm leaves out extra parens; add them and see if # that fixes it. sexp = self.mm_to_sexp(['('] + l + [')']) return '#' + sexp_to_string(sexp) + '#' except: pass try: i, sexp = self.mm_to_sexp_class(l, 0) if i == len(l) and sexp != None: if sexp[0] == 'cv': sexp = sexp[1] return '#' + sexp_to_string(sexp) + '#' except: pass try: i, sexp = self.mm_to_sexp_class(['('] + l + [')'], 0) if i == len(l) + 2 and sexp != None: return '#' + sexp_to_string(sexp) + '#' except: pass if len(str) == 0: str = '@@@' + mstr return '{{{' + str + '}}}' def format_comment(self): # Convert Metamath markup to Barghest markup if self.last_comment == None: return print premode = False mode = 'n' retab = {'n': re.compile(r'(?': print '# }}}' premode = False elif premode: print '# ' + line elif not premode and line.strip() == '
': print '# {{{' premode = True else: rline = '' pos = 0 while pos < len(line): m = retab[mode].search(line, pos) if m: if mode != 'm': rline += line[pos:m.start()] else: mathstr += line[pos:m.start()] g = m.group() #print line #print ' ' * m.start() + g mend = m.end() if g == '`': pos = mend cl_m = clpunct_re.match(line, pos) if mode == 'm': rline += self.format_math(mathstr) mode = 'n' if cl_m: # skip whitespace before close punct pos += 1 else: if oppunct_re.search(rline): rline = rline[:-1] mode = 'm' mathstr = '' elif g == '``': if mode == 'm': mathstr += '`' else: rline += '`' pos = mend elif g == '~': m = lab_re.search(line, mend) if m: if oppunct_re.search(rline): rline = rline[:-1] label = m.group(1) label = label.replace('~~', '~') rline += '[[' + label + ']]' pos = m.end() if clpunct_re.match(line, pos): # skip whitespace before close punct pos += 1 elif g == '~~': rline += '~' pos = mend elif g == '_': mode = {'n': 'u', 'u': 'n'}[mode] rline += '//' pos = mend elif g == '[': rline += '[bib/' pos = mend if pos < mend: rline += g pos = mend else: if mode != 'm': rline += line[pos:] else: mathstr += line[pos:] break print '#', rline self.last_comment = None if __name__ == '__main__': import sys mm = MM() state = 0 while 0: # todo: do better comment preservation line = sys.stdin.readline() line = line.rstrip('\r\n') if state == 0 and len(line) >=6 and line[:6] == 'set.mm': print '#', line state = 1 elif state == 1: if len(line) >= 5 and line[:5] == '=-=-=': state = 2 else: print '#', line elif state == 2: if line == '$)': break mm.read(toks(sys.stdin)) print '# %d Metamath steps converted to %d Ghilbert steps' % (mm.n_mm_steps, mm.n_gh_steps)