changeset 339:a7d868a5577a

proof_burden: use an output parameter to print to
author Sigurd Meldgaard <stm@daimi.au.dk>
date Wed, 07 Jul 2010 13:22:22 +0200
parents 4d4028b2d6c4
children 2aef103ea501
files pysmcl/proof_burden.py
diffstat 1 files changed, 18 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/pysmcl/proof_burden.py	Wed Jul 07 11:42:23 2010 +0200
+++ b/pysmcl/proof_burden.py	Wed Jul 07 13:22:22 2010 +0200
@@ -1,5 +1,6 @@
 import pysmcl.ast_wrapper as ast
 import pysmcl.pretty_print
+import sys
 
 
 class FindInvariant(ast.NodeVisitor):
@@ -12,9 +13,10 @@
 
 class ProofBurden(ast.NodeVisitor):
 
-    def __init__(self):
+    def __init__(self, output):
         self.openings = []
         self.results = []
+        self.output = output
 
     def visit_While(self, node):
         self.generic_visit(node)
@@ -26,29 +28,32 @@
             if node.func.id == "result":
                 self.results.append(node.args[0])
             elif node.func.id == "precondition":
-                print "  You can assume: " + (node.args[0].s)
+                print >>self.output, "  You can assume: " + (node.args[0].s)
             elif node.func.id == "invariant":
-                print " Invariant"
-                print (node.args[0].s)
+                print >>self.output, " Invariant"
+                print >>self.output, (node.args[0].s)
 
 
-def proof_burden(f):
-    b = ProofBurden()
-    print "For the function: " + f.name
+def proof_burden(f, output=sys.stdout):
+    b = ProofBurden(output)
+    print >>output, "For the function: " + f.name
     b.visit(f)
     if b.openings!=[]:
-        print (" Show that you can compute:")
+        print >>output, " Show that you can compute:"
         for i in b.openings:
-            print("  The value of " + pysmcl.pretty_print.expr_string(i)
+            print >>output, ("  The value of "
+                             + pysmcl.pretty_print.expr_string(i)
                   + " in line " + str(i.lineno))
-        print (" From:")
+        print >>output, (" From:")
         for i in b.results:
-            print("  The value of " + pysmcl.pretty_print.expr_string(i)
-                  + " in line " + str(i.lineno))
+            print >>output, ("  The value of "
+                             + pysmcl.pretty_print.expr_string(i)
+                             + " in line " + str(i.lineno))
     else:
-        print " Nothing has to be proved"
+        print >>output, " Nothing has to be proved"
     return f
 
+
 def main():
     from optparse import OptionParser
     parser = OptionParser(usage="Usage: %prog [options] pysmcl_program")
@@ -60,6 +65,5 @@
         if isinstance(i, ast.FunctionDef):
             proof_burden(i)
 
-    
 if __name__ == "__main__":
     main()