From 8f3fe06142867c9f2d2015723d1bbc41dd0f01ca Mon Sep 17 00:00:00 2001
From: Dan Krejsa <dan.krejsa@gmail.com>
Date: Sun, 13 Sep 2009 22:56:14 +0000
Subject: Initial support for stepping through a proof.

---
diff --git a/ghilbert.py b/ghilbert.py
index 19e7bef..cb4f106 100755
--- a/ghilbert.py
+++ b/ghilbert.py
@@ -1354,7 +1354,7 @@ class Ghilbert():
         pip.proof.append(e)
 
 
-    def add_thm(self, expr):
+    def add_thm(self, expr, stop_cond):
         """Initial processing for a thm statement
 
         expr is the thm's s-expression
@@ -1445,7 +1445,10 @@ class Ghilbert():
         pip.dvs = self.dv_canonical(expr, pip_vdict)
 
         try:
-            for j in xrange(len(expr[4])):
+            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:
@@ -2150,7 +2153,7 @@ class Ghilbert():
         self.interfaces[ifname] = child
         self.push_history((Ghilbert.EXPORT, child, path))
 
-    def read_proof_file_from_scanner(self, scanner, one_only):
+    def read_proof_file_from_scanner(self, scanner, stop_cond):
 
         while (1):
             self.pip = None
@@ -2164,7 +2167,7 @@ class Ghilbert():
                 raise VerifyError(
                     _("Expected s-expression (...) command argument"))
             if word == 'thm':
-                self.add_thm(sexpr)
+                self.add_thm(sexpr, stop_cond)
             elif word == 'def':
                 self.add_def(sexpr)
             elif word == 'var':
@@ -2183,7 +2186,7 @@ class Ghilbert():
                 self.log.warning(_("Skipping unknown command '%s'") % word)
 
             scanner.set_good()
-            if one_only:
+            if stop_cond >= -1:
                 break
 
 
diff --git a/spock.py b/spock.py
index e7b9e8f..151ab98 100755
--- a/spock.py
+++ b/spock.py
@@ -33,7 +33,7 @@ logger = logging.getLogger('Spock')
 # files such as set_mm.gh that use exclusively ASCII identifiers.
 #
 
-class SpockScanner:
+class SpockScanner(object):
     def __init__(self, spock):
         self.spock = spock    # The Spock object
         sb = self.sb = spock.source_buffer
@@ -159,9 +159,9 @@ class SpockBuffer(gtksourceview2.Buffer):
         return True
 
 
-class Spock:
+class Spock(object):
 
-    def verify(self, only_one):
+    def verify(self, stop_cond):
         # 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:
@@ -175,16 +175,16 @@ class Spock:
 
         # Hmm, could make Spock support the Scanner API's (i.e. get_token())
         # directly, would that be better?
-        logger.debug ("SpockScanner")
+        #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")
+            #logger.debug ("read_proof_file_from_scanner")
+            gh.read_proof_file_from_scanner (scanner, stop_cond)
+            #logger.debug ("read_proof_file_from_scanner done")
             self.good_offset = scanner.good_offset
             self.tag_good()
             self.statuslabel.set_text('OK')
@@ -218,6 +218,11 @@ class Spock:
             print >> sys.stderr, "GhError"
             (msg,) = x.args
 
+        if msg == _("Step."):
+            self.step = self.step + 1
+        else:
+            self.step = 0
+
         if start != None:
             self.source_buffer.select_range(start, end)
 
@@ -361,15 +366,27 @@ class Spock:
             sv.grab_focus()
 
     def verify_button_callback(self, widget, data=None):
-        self.verify(False)
+        self.verify(-2)
+        self.step = 0
 
     def verify_one_button_callback(self, widget, data=None):
-        self.verify(True)
+        self.source_view.grab_focus()
+        self.verify(-1)
+        self.step = 0
         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 verify_step_button_callback(self, widget, data=None):
+        self.source_view.grab_focus()
+        self.verify(self.step)
+        if not self.error_set:
+            self.step = 0
+            sv = self.source_view
+            it = self.source_buffer.get_iter_at_offset(self.good_offset)
+            sv.scroll_to_iter(it, 0.0)
+
     def search_stop(self, restorePos=False):
         if self.searching:
             self.searching = False
@@ -557,18 +574,25 @@ class Spock:
 
         hbox = gtk.HBox()
 
-        button = gtk.Button('_Verify')
+        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 = 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)
 
+        button = gtk.Button(_('_Step'))
+        button.set_property('use-underline', True)
+        button.connect('clicked', self.verify_step_button_callback)
+        button.show()
+        hbox.pack_start (button, expand=False)
+        self.step = 0;
+
         self.search_dir_forward = True
         self.searching = False
         entry = gtk.Entry()
@@ -653,7 +677,7 @@ class Spock:
 
         print >> sys.stderr, "Spock read ", file_path
 
-        self.verify(False)
+        self.verify(-2)
 
 class SpockWindow(gtk.Window):
     def __init__(self):
--
cgit v0.9.1