import re from ghestalt.app.models import Log import ghestalt.app.views from ghestalt.app.verify import VerifyGh, Scanner, VerifyError, read_sexp, ProofCtx, sexp_to_string from ghestalt.app.templatetags.ghmarkup import htmlquote # Render a thm into a dictionary suitable for templating class Readliner: def __init__(self, str): self.lines = str.split('\n') self.ix = 0 def readline(self): try: result = self.lines[self.ix] self.ix += 1 return result except IndexError: return '' class Lazysyms: def __init__(self, vg): self.vg = vg self.dict = {} self.lazy = {} def __getitem__(self, key): try: return self.dict[key] except KeyError: #print 'loading', key, 'from', self.lazy[key] thm = Log.objects.filter(what = self.lazy[key]).latest() sc = Scanner(Readliner(thm.ldata)) cmd = read_sexp(sc) arg = read_sexp(sc) #print cmd, arg del self.lazy[key] #print 'wha?', {'stmt': 'ax'}.get(cmd, cmd) hyps = arg[2] if cmd == 'thm': hyps = [hyp[1] for hyp in hyps] self.vg.add_assertion({'stmt': 'ax'}.get(cmd, cmd), key, arg[1], hyps, arg[3], self.vg.syms) #print self.dict[key] return self.dict[key] def __setitem__(self, key, val): self.dict[key] = val def __contains__(self, key): return self.dict.__contains__(key) or self.lazy.__contains__(key) def has_key(self, key): return self.__contains__(key) def addlazy(self, key, where): self.lazy[key] = where class GhestaltVerifyGh(VerifyGh): def __init__(self, base): VerifyGh.__init__(self) self.base = base self.syms = Lazysyms(self) def do_cmd(self, cmd, arg): if cmd == 'thm' and isinstance(arg, basestring): self.syms.addlazy(arg, self.base + '/' + arg + '/_thm') elif cmd == 'export': pass else: VerifyGh.do_cmd(self, cmd, arg) def do_import_stmt(self, arg, pref, local_syms, sym_map): if isinstance(arg, basestring): what = self.stashedname + '/' + arg + '/_stmt' self.syms.addlazy(pref + arg, what) else: VerifyGh.do_import_stmt(self, arg, pref, local_syms, sym_map) def resolve_interface(self, name): if name == 'zfc/set_mm_ax': name = 'mm/set_ax' # Hack, todo deleteme when rename is done self.stashedname = name ghi = Log.objects.filter(what = name + '/_ghi').latest() return Scanner(Readliner(ghi.ldata)) def get_base_vg(data, base): vg = GhestaltVerifyGh(base) sc = Scanner(Readliner(data)) while 1: cmd = sc.get_tok() if cmd == None: break else: try: arg = read_sexp(sc) vg.do_cmd(cmd, arg) except VerifyError, x: print 'Verify error', x break return vg # adapted from ghilbert app # split string into tokens with ranges def splitrange(str): result = [] beg = 0 for i in range(len(str)): c = str[i] if c == ' ': if i != beg: result.append((str[beg:i], beg, i)) beg = i + 1 elif c in '()': if i != beg: result.append((str[beg:i], beg, i)) result.append((str[i:i+1], i, i+1)) beg = i + 1 elif c in '#': if i != beg: result.append((str[beg:i], beg, i)) beg = len(str) break if beg != len(str): result.append((str[beg:], beg, len(str))) return result # adapted from ghilbert app class thmctx: def __init__(self, vg): self.thmname = None self.sexpstack = [] self.hypmap = {} self.state = 0 self.proofctx = ProofCtx() self.vg = vg def tok(self, tok): thestep = None if self.state == 0: if tok == 'thm': self.state = 1 else: return 'expected thm' elif self.state == 1: if tok == '(': self.state = 2 else: return 'expected (' elif self.state == 2: if tok in '()': return 'expected thm name' else: self.thmname = tok self.state = 3 elif self.state == 3: if tok == '(': self.sexpstack.append([]) self.state = 5 else: return 'expected ( to open dv''s' elif self.state == 4: if tok == '(': self.sexpstack.append([]) self.state = 7 else: return 'expected ( to open hyps' elif self.state == 6: if tok == '(': self.sexpstack.append([]) self.state = 9 elif tok == ')': return 'expected proof stmt' else: thestep = tok self.state = 8 elif self.state == 8: if tok == '(': self.state = 10 else: return 'expected ( to open proof' elif self.state == 10: if tok == '(': self.sexpstack.append([]) self.state = 11 elif tok == ')': self.state = 12 else: thestep = tok elif self.state in (5, 7, 9, 11): if tok == '(': self.sexpstack.append([]) elif tok == ')': if len(self.sexpstack) == 1: thestep = self.sexpstack[0] self.sexpstack = [] self.state -= 1 else: last = self.sexpstack[-1] del(self.sexpstack[-1]) self.sexpstack[-1].append(last) else: self.sexpstack[-1].append(tok) elif self.state == 12: if tok == ')': self.state = 13 else: return 'expected )' elif self.state == 13: return 'extra junk after proof' if self.state == 6: for hyp in thestep: self.hypmap[hyp[0]] = hyp[1] elif self.state == 8: self.stmt = thestep elif thestep != None and self.state == 10: #try: self.vg.check_proof_step(self.hypmap, thestep, self.proofctx) #except VerifyError, x: # return str(x) #except Exception, x: # return `x` # stolen from trac versioncontrol/diff.py space_re = re.compile(' ( +)|^ ') def htmlify(match): div, mod = divmod(len(match.group(0)), 2) return div * '  ' + mod * ' ' # norm and thm are model objs def render_thm(what, norm, thm): base = what.rsplit('/', 1)[0] #print base gh = Log.objects.filter(what= base + '/_gh').latest() vg = get_base_vg(gh.ldata, base) tc = thmctx(vg) render = [''] lsl = lmsl = 0 for line in thm.ldata.split('\n'): render.append('') show_stack = False sline = splitrange(line) for tok, beg, end in sline: status = tc.tok(tok) sl, msl = len(tc.proofctx.stack), len(tc.proofctx.mandstack) if sl != lsl or msl < lmsl: show_stack = True lsl, lmsl = sl, msl #print tok, tc.proofctx.stack, tc.proofctx.mandstack if show_stack: stackline = line[0: sline[0][1]] stackstr = htmlquote(sexp_to_string(tc.proofctx.stack[-1])) stackline += '' + stackstr + '' render.append('') render.append('
' + space_re.sub(htmlify, htmlquote(line)) + '
' + space_re.sub(htmlify, stackline) + '
') return {'title': ghestalt.app.views.wikititle(what), 'norm': norm, 'render': '\n'.join(render)}