path: root/spock.py

#! /usr/bin/env python
# spock.py - proof verification activity based upon ghilbert
# -*- 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 logging

import sys, os, array
import gtk
import gtksourceview2
import pango
import logging
import ghilbert
from gettext import gettext as _

logger = logging.getLogger('Spock')

#
# Note about strings and identifier names in spock/ghilbert:
# The gtk interfaces deliver and expect UTF-8 encoded strings.
# Since the only special characters for ghilbert are in the ASCII
# range ('#', '\n', '(', ')', ' ', '\t', '\v', '\f', '\r'),
# we can treat any byte with its high-order bit set as part
# of an identifier, and keep all identifers stored as UTF-8
# encodings, and be blissfully ignorant of multi-byte character
# encoding sequences. Keeping to the UTF-8 encoding will save
# space (compared to storing identifiers as python unicode strings,
# for instance) when handling existing large proof and interface
# files such as set_mm.gh that use exclusively ASCII identifiers.
#

class SpockScanner:
    def __init__(self, spock):
        self.spock = spock    # The Spock object
        sb = self.sb = spock.source_buffer
        self.good_offset = spock.good_offset
        self.i = sb.get_iter_at_offset(self.good_offset)
        self.k = None

    def set_good(self):
        """Called by verifier after servicing command to record
        good position
        """
        self.good_offset = self.i.get_offset()

    def get_token(self):
        self.k = None   # token start
        i = self.i
        sb = self.sb
        while True:
            c = i.get_char()
            if c == '\x00':
                return None
            if c.isspace():
                i.forward_char()
                continue
            if c in '()':
                self.k = i.copy()
                i.forward_char()
                #logger.info ("token: '%c'" % c)
                #print >> sys.stderr, "token: '%c'" % c
                return c
            if c == '#':
                i.forward_line()
                continue
            break

        self.k = i.copy()
        i.forward_char()
        while True:
            c = i.get_char()
            if c == '\x00':
                break
            if c.isspace() or c in '()#':
                break
            i.forward_char()
        tok = self.k.get_text(i)
        #logger.info ("token: '%s'" % tok)
        #print >> sys.stderr, "token: '%s'" % tok
        return tok

    def skip_expr(self):
        tok = self.get_token()
        if tok == None:
            raise ghilbert.GhError('skip_expr 1')
        if tok == ')':
            return ')'
        if tok == '(':
            while True:
                tok = self.skip_expr()
                if tok == ')':
                    return '('
        return tok
        
    def delimitError(self, path):
        #print >> sys.stderr, "path=", path
        j = 0
        while j < len(path):
            #print >> sys.stderr, "j=", j
            x = self.get_token()
            if x != '(':
                raise ghilbert.GhError('delimitError 1')
            n = path[j]
            for i in xrange(n):
                if self.skip_expr() == ')':
                    raise ghilbert.GhError('delimitError 2')
            j = j + 1

        start = self.i.copy()
        if self.skip_expr() == ')':
            raise ghilbert.GhError('delimitError 3')
        return (start, self.i)

class SpockBuffer(gtksourceview2.Buffer):
    
    def __init__(self):
        gtksourceview2.Buffer.__init__(self)
        self.error_tag = self.create_tag("ErrorTag", background="yellow",
                                       editable=False)
        self.good_tag = self.create_tag("GoodTag", background="#e0ffe0")
        self.search_tag = self.create_tag("search", foreground="white", background="blue")

    def search_end(self):
        start, end = self.get_bounds()
        self.remove_tag(self.search_tag, start, end)

    def search(self, text, forward):
        start, end = self.get_bounds()
        self.remove_tag(self.search_tag, start, end)
        
        insert_mark = self.get_insert()
        it = self.get_iter_at_mark(insert_mark)
        if forward:
            if it.get_offset() == end.get_offset():
                it = start
            ret = it.forward_search(text, gtk.TEXT_SEARCH_TEXT_ONLY)
            if ret is None:
                self.place_cursor(end)
                return False
            start, end = ret
            it = end
        else:
            if it.get_offset() == 0:
                it = end
            ret = it.backward_search(text, gtk.TEXT_SEARCH_TEXT_ONLY)
            if ret is None:
                self.place_cursor(start)
                return False
            start, end = ret
            it = start
##         print "search: '%s' cursor %d start %d end %d\n" % \
##               (text[:10], it.get_offset(), start.get_offset(), end.get_offset())
        self.apply_tag(self.search_tag, start, end)
        self.place_cursor(it)
        return True


class Spock:

    def verify(self, only_one):
        # If we don't have a Ghilbert object any more (probably we moved
        # self.good_offset back to the start of the file), create a fresh one
        if self.gh == None:
            self.gh = ghilbert.Ghilbert(logger)
            self.gh.fpath = self.file_roots()
            self.gh.curdir = self.curdir
            self.gh.file = self.current_file

        self.clear_error()

        # Hmm, could make Spock support the Scanner API's (i.e. get_token())
        # directly, would that be better?
        logger.debug ("SpockScanner")
        scanner = SpockScanner(self)
        gh = self.gh

        err = None
        start = None
        try:
            logger.debug ("read_proof_file_from_scanner")
            gh.read_proof_file_from_scanner (scanner, only_one)
            logger.debug ("read_proof_file_from_scanner done")
            self.good_offset = scanner.good_offset
            self.tag_good()
            self.statuslabel.set_text('OK')
            return
        except ghilbert.GhCmdExprError, x:
            (msg,) = x.args
            print >> sys.stderr, "GhCmdExprError ", msg
            # Get a secondary scanner to parse the erring expression
            # While keeping the current scanner unchanged.
            save_offset = self.good_offset
            self.good_offset = scanner.good_offset
            scan2 = SpockScanner(self)
            cmd = scan2.get_token()
            if cmd == None or cmd == '(' or cmd == ')':
                raise ghilbert.GhError('Internal error parsing GhCmdExprError')
            (start, end) = scan2.delimitError(x.path)
            # restore original good_offset
            self.good_offset = save_offset

##             cmd, start, end = ghilbert.sexp_subexp_substr(x.expr, x.path)
##             l = len(x.cmdword) + 1
##             start = start + l
##             end = end + l
##             err = '%s %s\n' % (x.cmdword, cmd)
        except ghilbert.SyntaxError, x:
            (msg,) = x.args
            print >> sys.stderr, "SyntaxError"
            start = scanner.k
            end = scanner.i
        except ghilbert.GhError, x:
            print >> sys.stderr, "GhError"
            (msg,) = x.args

        if start != None:
            self.source_buffer.select_range(start, end)

        #print >> sys.stderr, "self.good_offset=", self.good_offset, "scanner.good_offset=", scanner.good_offset
        if (self.good_offset != scanner.good_offset):
            self.good_offset = scanner.good_offset
            self.tag_good()

        self.init_error(scanner.i, msg)

        if err:
            self.add_error(err)

        pip = gh.pip
        if pip:
            self.show_pip(pip)

        self.tag_error()

        self.scroll_to_error()
        self.statuslabel.set_text(msg)
        logger.error(_('Error reading proof file: %s'), msg)

    def tag_good(self):
        #print >> sys.stderr, "tag_good: good_offset=", self.good_offset
        off = self.good_offset
        if off != 0:
            sb = self.source_buffer
            modified = sb.get_modified()
            i1 = sb.get_iter_at_offset(0)
            i2 = sb.get_iter_at_offset(off)
            sb.apply_tag_by_name("GoodTag", i1, i2)
            sb.set_modified(modified)

    def clear_good(self):
        off = self.good_offset
        if off != 0:
            sb = self.source_buffer
            modified = sb.get_modified()
            i1 = sb.get_iter_at_offset(0)
            i2 = sb.get_iter_at_offset(off)
            sb.remove_tag_by_name("GoodTag", i1, i2)
            self.good_offset = 0
            sb.set_modified(modified)

    def tag_error(self):
        sb = self.source_buffer
        modified = sb.get_modified()
        i1 = sb.get_iter_at_mark(self.error_beg)
        i2 = sb.get_iter_at_mark(self.error_end)
        sb.apply_tag_by_name("ErrorTag", i1, i2)
        self.error_set = True
        sb.set_modified(modified)

    def clear_error(self):
        if self.error_set:
            sb = self.source_buffer
            # Don't let removing the error message affect the 'modified'
            # flag, since the error message text isn't saved.
            # Ugh, this doesn't prevent the modified_changed signal from
            # being emitted.
            modified = sb.get_modified()
            i1 = sb.get_iter_at_mark(self.error_beg)
            i2 = sb.get_iter_at_mark(self.error_end)
            sb.delete(i1, i2)
            self.error_set = False
            sb.set_modified(modified)


    def init_error(self, i1, msg):
        sb = self.source_buffer
        modified = sb.get_modified()
        sb.move_mark(self.error_end, i1)
        sb.insert(i1, _("\n<--- Oops! %s\n") % msg)
        i2 = sb.get_iter_at_mark(self.error_end)
        sb.move_mark(self.error_end, i1)
        sb.move_mark(self.error_beg, i2)
        sb.set_modified(modified)
        
    def add_error(self, msg):
        sb = self.source_buffer
        modified = sb.get_modified()
        i1 = sb.get_iter_at_mark(self.error_end)
        sb.insert(i1, msg)
        sb.move_mark(self.error_end, i1)
        sb.set_modified(modified)

    def show_pip(self, pip):
        sb = self.source_buffer
        modified = sb.get_modified()
        i1 = sb.get_iter_at_mark(self.error_end)
        sb.insert(i1, '\n')
        n = 0
        vlist = pip.vlist
        for e in pip.exprs:
            es = ghilbert.iexpr_to_string(e, vlist)
            sb.insert(i1, 'P%d: %s\n' % (n, es))
            n = n + 1
        n = 0
        for e in pip.wvs:
            es = ghilbert.iexpr_to_string(e, vlist)
            sb.insert(i1, 'W%d: %s\n' % (n, es))
            n = n + 1
        sb.move_mark(self.error_end, i1)
        sb.set_modified(modified)

    def scroll_to_error(self):
        sv = self.source_view
        sv.scroll_mark_onscreen(self.error_end)

    def scroll_to_end(self):
        sv = self.source_view
        sv.scroll_to_iter(self.source_buffer.get_end_iter(), 0.05)

    def shortcut_button_callback(self, widget, data):
        sv = self.source_view
        sb = self.source_buffer
        mi = sb.get_insert()
        it = sb.get_iter_at_mark(mi)
        if it.editable(True):
            # Keep track of the start position of the insertion. Is there
            # a better way to do this?
            begin = self.begin_mark
            sb.move_mark(begin, it)
            sb.insert(it, data)
            # it is revalidated at the end of the inserted text by the
            # insert_text signal handler
            sb.insert(it, '\n')
            it = sb.get_iter_at_mark(begin)
            j = data.index('(') + 1
            it.forward_chars(j)
            k = j + 1
            l = len(data)
            while k < l and not data[k] in '() #':
                k = k + 1
            it2 = it.copy()
            it2.forward_chars(k - j)
##            sb.place_cursor(it)
##            sb.move_mark(mi, it2)
            sb.select_range(it2, it)
            sv.grab_focus()

    def verify_button_callback(self, widget, data=None):
        self.verify(False)

    def verify_one_button_callback(self, widget, data=None):
        self.verify(True)
        if not self.error_set:
            sv = self.source_view
            it = self.source_buffer.get_iter_at_offset(self.good_offset)
            sv.scroll_to_iter(it, 0.0)

    def find(self):
        if not self.searching:
            self.searching = True
            self.statuslabel.set_text("")
            self.search_entry.grab_focus()
        else:
            self.searching = False
            self.source_buffer.search_end()
            self.source_view.grab_focus()

    def search_op(self, forward):
        self.searching = True
        self.statuslabel.set_text("")
        self.search_entry.grab_focus()
        self.search_dir_forward = forward
        sb = self.source_buffer
        res = sb.search(self.search_entry.get_text(), forward)
        self.source_view.scroll_mark_onscreen(sb.get_insert())
        if not res:
            self.statuslabel.set_text(_("*** Text not found, will wrap ***"))

    def search_activate_callback(self, entry):
        """ Search text entry activate callback """
        self.search_op(self.search_dir_forward)

    def search_lose_focus_callback(self, widget, event):
        self.searching = False
        self.source_buffer.search_end()

#    def search_key_press_callback(self, widget, event):
#        if event.string == '\x1b':
#            self.source_view.grab_focus()

    def addShortcutButton(self, box, name, expansion):
        button = gtk.Button(name)
        button.connect('clicked', self.shortcut_button_callback, name + ' ' + expansion)
        button.show()
        box.pack_start(button, True, True, 0)

    def delete_range_cb(self, sb, start, end):
        start_off = start.get_offset()
        if start_off < self.good_offset:
            self.clear_good()
            self.gh = None
##         end_off = end.get_offset()
##         print >> sys.stderr, 'start_off=', start_off, ' end_off=', end_off

    def insert_text_cb(self, sb, iter, text, length):
        i_off= iter.get_offset()
        if i_off < self.good_offset:
            self.clear_good()
            self.gh = None
##         print >> sys.stderr, 'i_off=', i_off, ' len=', length, ' text=', \
##               text[:20]


    def apply_tag_cb(self, sb, tag, start, stop):
        start_off = start.get_offset()
        stop_off = stop.get_offset()
##         tagname = tag.get_property('name')
##         print >> sys.stderr, 'tag=', tagname, 'start_off=', start_off, 'stop_off =', stop_off
        if tag == self.good_tag:
            if start_off != 0 or stop_off != self.good_offset:
                self.source_buffer.stop_emission('apply-tag')
        elif tag == self.error_tag:
            sb = self.source_buffer
            err_beg = sb.get_iter_at_mark(self.error_beg).get_offset()
            err_end = sb.get_iter_at_mark(self.error_end).get_offset()
            if (start_off != err_beg or stop_off != err_end):
                self.source_buffer.stop_emission('apply-tag')

    def create_source_view(self):
        self.error_set = False
#        sb = gtksourceview2.Buffer()
        sb = SpockBuffer()
        self.source_buffer = sb
        sv = gtksourceview2.View(sb)
        self.source_view = sv
        sv.set_flags(gtk.CAN_FOCUS)
        pfont = pango.FontDescription("Monospace 10")
        sv.modify_font(pfont)
        sb.set_highlight_matching_brackets(True)
        self.error_tag = sb.error_tag
        self.good_tag = sb.good_tag
        # good_offset marks the point up to which the text has been validated
        # correct
        self.good_offset = 0
        self.begin_mark = sb.create_mark("begin", sb.get_end_iter(), True)
        self.error_beg = sb.create_mark("error_beg", sb.get_end_iter(), False)
        #self.error_beg.set_visible(True)
        self.error_end = sb.create_mark("error_end", sb.get_end_iter(), True)
        #self.error_end.set_visible(True)

        sb.connect('insert-text', self.insert_text_cb)
        sb.connect('delete-range', self.delete_range_cb)

        sb.connect('apply-tag', self.apply_tag_cb)

        sv.set_editable(True)  # for now
        sv.set_cursor_visible(True)
        # will add scrolled window
        sv.set_wrap_mode(gtk.WRAP_WORD) # WRAP_NONE, WRAP_CHAR, WRAP_WORD, WRAP_WORD_CHAR
        #sv.set_justification (gtk.JUSTIFY_LEFT)
        tw = gtk.ScrolledWindow()
        self.text_window = tw
        tw.add(sv)
        tw.show_all()

    def marks_positions(self):
        sb = self.source_buffer
        m = self.error_beg
        i1 = sb.get_iter_at_mark(m)
        print >> sys.stderr, "error_beg line", i1.get_line(), "off", i1.get_line_offset()

        m = self.error_end
        i1 = sb.get_iter_at_mark(m)
        print >> sys.stderr, "error_end line", i1.get_line(), "off", i1.get_line_offset()

    def file_roots(self):
        roots = ['.', '/']
        if os.environ.has_key('SUGAR_ACTIVITY_ROOT'):
            roots.append(os.path.join(os.environ['SUGAR_ACTIVITY_ROOT'],
                                      'data'))
        if os.environ.has_key('SUGAR_BUNDLE_PATH'):
            roots.append(os.environ['SUGAR_BUNDLE_PATH'])

        if os.environ.has_key('GHILBERT_PATH'):
            roots.extend(os.environ['GHILBERT_PATH'].split(':'))
        return roots


    def __init__(self, vbox):

        self.current_file = None
        self.curdir = '.'
        self.gh = ghilbert.Ghilbert(logger)
        self.gh.fpath = self.file_roots()

        self.main_view = vbox
        hbox = gtk.HBox()

        self.addShortcutButton (hbox, 'import',
            '(INTERFACE_NAME IFACE_FILE_URI (PARAMS ...) "")')
        self.addShortcutButton (hbox, 'thm',
            '(THM_NAME ((DVAR1 DVAR2 ...) ...) ((HYPNAME HYPEXPR) ...) (CONC ...) (PROOFSTEP ...))')
        self.addShortcutButton (hbox, 'def',
                                '((DEF_TERMNAME VAR ...) DEF_EXPANSION)')
        self.addShortcutButton (hbox, 'export',
            '(INTERFACE_NAME IFACE_FILE_URI (PARAMS ...) "")')
        hbox.pack_start(gtk.VSeparator(), True, True, 0)
        self.addShortcutButton (hbox, 'var', '(KIND VARNAME ...)')
        self.addShortcutButton (hbox, 'kindbind', '(KIND1 KIND2)')
        self.addShortcutButton (hbox, 'termbind', '(TERM_NAME1 TERM_NAME2)')

        hbox.pack_start(gtk.VSeparator(), True, True, 0)
        
        self.addShortcutButton (hbox, 'kind', '(KIND)')
        self.addShortcutButton (hbox, 'term', '(KIND (TERMNAME KIND ...))')
        self.addShortcutButton (hbox, 'stmt',
            '(STMT_NAME ((DVAR1 DVAR2 ...) ...) (HYPEXPR ...) (CONC ...))')
        self.addShortcutButton (hbox, 'param',
            '(INTERFACE_NAME IFACE_FILE_URI (PARAMS ...) "")')

        self.main_view.pack_end(hbox, expand=False)

        hbox = gtk.HBox()

        button = gtk.Button('_Verify')
        button.set_property('use-underline', True)
        button.connect('clicked', self.verify_button_callback)
        button.show()
        hbox.pack_start (button, expand=False)

        button = gtk.Button('_One')
        button.set_property('use-underline', True)
        button.connect('clicked', self.verify_one_button_callback)
        button.show()
        hbox.pack_start (button, expand=False)

        self.search_dir_forward = True
        self.searching = False
        entry = gtk.Entry()
        self.search_entry = entry
        entry.set_width_chars (10)
        entry.show()
        entry.connect('activate', self.search_activate_callback)
        entry.connect('focus-out-event', self.search_lose_focus_callback)
#        entry.connect('key-press-event', self.search_key_press_callback)
        hbox.pack_start (entry, expand=False)

        self.statuslabel = gtk.Label('OK')
        self.statuslabel.set_alignment(1.0, 0.0)
        self.statuslabel.show()
        hbox.pack_start (self.statuslabel, True, True, 0)

        hbox.show()
        self.main_view.pack_end (hbox, expand=False)

        self.create_source_view()
        self.source_view.grab_focus()
        self.main_view.pack_start(self.text_window, True, True, 0)

        self.scroll_to_end()
        self.main_view.show()


    def write_file(self, file_path):

        # Check 'modified' status of file, and only save
        # it if it is modified, or if the file path changed.
        # (Should we also check if the file contents changed on disk,
        # due to the action of some other context?)

        sb = self.source_buffer
        if not sb.get_modified() and file_path == self.current_file:
            print >> sys.stderr, "Not writing to %s, already up to date" % \
                  file_path
            return

        print >> sys.stderr, "in write_file, file_path is %s " % file_path
        self.clear_error()

        try:
            f = open(file_path, 'wb')
        except:
            print >> sys.stderr, ("Could not open '%s' to save it" % file_path)
            return

        # Ugh.
        text = sb.get_text(sb.get_start_iter(), sb.get_end_iter())
        f.write(text)
        f.close()
        sb.set_modified (False)
        self.current_file = file_path

    def read_file(self, file_path):

        self.current_file = file_path  # for now.

        gh = self.gh
        try:
            (f, gh.curdir) = ghilbert.get_stream(file_path, gh.curdir,
                                                 gh.fpath, gh.log)
        except:
            self.statuslabel.set_text("Cannot open '%s'" % file_path)
            logger.error("Cannot open '%s'" % file_path)
            return

        self.curdir = gh.curdir

        # Ugh! For now...
        string = f.read()
        sb = self.source_buffer
        sb.set_text(string)
        f.close()

        sb.set_modified(False)

        gh.file = file_path

        print >> sys.stderr, "Spock read ", file_path

        self.verify(False)

class SpockWindow(gtk.Window):
    def __init__(self):

        gtk.Window.__init__(self)

        self.connect("delete_event", self.delete_event_cb)
        self.connect("destroy", self.destroy)

        self.vbox = gtk.VBox()
        self.add(self.vbox)

        g = gtk.ActionGroup("Global")
        self.action_group = g

        actions = [
            # Name, stock id, label, accelerator, tooltip, callback
            ("FileMenu", None, "_File", None, None, None),
            ("FileSave", gtk.STOCK_SAVE, _("_Save"), _("<Ctrl>S"), _("Save work now"),
                         self.do_save),
            ("FileQuit", gtk.STOCK_QUIT, _("_Quit"), _("<Ctrl>Q"), _("Q-Tip"),
                         self.do_quit),
            ("EditMenu", None, "_Edit", None, None, None),
            ("EditFind", gtk.STOCK_FIND, _("_Find"), _("<Ctrl>F"), _("Find"),
                         self.do_search),
            ("EditFindNext", gtk.STOCK_GO_DOWN, _("  _Next"), _("<Alt>N"), _("Find next occurrence"),
                         self.do_search_forward),
            ("EditFindPrevious", gtk.STOCK_GO_UP, _("  _Previous"), _("<Alt>P"), _("Find previous occurrence"),
                         self.do_search_backward),
            ]
        g.add_actions(actions)

        # How do we associate these actions with handlers??

        uidef = '''
        <ui>
          <menubar>
            <menu name="FileMenu" action="FileMenu">
              <menuitem name="FileSave" action="FileSave" />
              <separator/>
              <menuitem name="FileQuit" action="FileQuit" />
            </menu>
            <menu name="EditMenu" action="EditMenu">
              <menuitem name="EditFind" action="EditFind" />
              <separator/>
              <menuitem name="EditFindNext" action="EditFindNext" />
              <menuitem name="EditFindPrevious" action="EditFindPrevious" />
            </menu>
          </menubar>
        </ui>
        '''

        ui = gtk.UIManager()
        self.uiManager = ui
        accelgroup = ui.get_accel_group()
        self.add_accel_group(accelgroup)
        ui.insert_action_group(g, -1)
        ui.add_ui_from_string(uidef)
        ui.ensure_update()

        menubar = ui.get_widget("/menubar")
        self.vbox.pack_start(menubar, False, False, 0)

        spock = Spock(self.vbox)
        self.spock = spock

        self.show_all()

        if len(sys.argv) > 1:
            spock.read_file(sys.argv[1])


    def destroy(self, widget, data=None):
        print "destroy signal occurred"
        gtk.main_quit()

    def do_save(self, widget):
        if self.spock.current_file != None:
            self.spock.write_file(self.spock.current_file)
        else:
            # For now. Eventually bring up file-save dialog.
            print >> sys.stderr, "No file name yet, can't save."
        
    def do_quit(self, widget):
        logger.info("quitting...")
        if self.spock.current_file != None:
            self.spock.write_file(self.spock.current_file)
        self.destroy(widget)

    def do_search(self, widget):
        self.spock.find()

    def do_search_forward(self, widget):
        self.spock.search_op(True)

    def do_search_backward(self, widget):
        self.spock.search_op(False)

    def delete_event_cb(self, widget, event, data=None):
        logger.info("delete_event_cb")
        return False

    def main(self):
        gtk.main()


if __name__ == "__main__":
    spockW = SpockWindow()
    spockW.main()