1#!/usr/bin/env python 2# -*- coding: utf-8 -*- 3# 4# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 5# 6# SPDX-License-Identifier: BSD-2-Clause 7# 8 9''' 10Basic functionality for constructing apply-style proofs from Python. 11 12Example usage: 13 14 p = Proof('True \\<and> True') 15 p.apply('rule conjI', solves=-1) 16 p.apply('simp') 17 p.apply('simp') 18 p.done() 19 print(p) 20''' 21 22import StringIO 23from .exception import IsaSymbolsException 24 25 26class Proof(object): 27 def __init__(self, statement, name=None, debug=True): 28 self.statement = statement 29 self.name = name 30 self.steps = [] 31 self.subgoals = 1 32 self.completed = None 33 self.debug = debug 34 35 def apply(self, step, solves=0): 36 if self.completed: 37 raise IsaSymbolsException('you cannot apply steps to a completed ' 38 'proof') 39 if solves > self.subgoals: 40 raise IsaSymbolsException('you cannot solve more subgoals (%d) ' 41 'than remain (%d)' % (solves, self.subgoals)) 42 if ' ' in step: 43 step = '(%s)' % step 44 self.steps.append((' ' * (self.subgoals - 1), step)) 45 self.subgoals -= solves 46 47 def done(self): 48 if self.subgoals > 0: 49 raise IsaSymbolsException('%d subgoals remain' % self.subgoals) 50 if self.completed is not None: 51 raise IsaSymbolsException('proof already completed') 52 self.completed = 'done' 53 54 def oops(self): 55 if self.completed is not None: 56 raise IsaSymbolsException('proof already completed') 57 self.completed = 'oops' 58 59 def sorry(self): 60 if self.completed: 61 raise IsaSymbolsException('proof already completed') 62 self.completed = 'sorry' 63 64 def __repr__(self): 65 s = StringIO.StringIO() 66 s.write('lemma ') 67 if self.name is not None: 68 s.write('%s:' % self.name) 69 s.write('"%s"\n' % self.statement) 70 if not self.debug and self.completed == 'done': 71 # Write the lemma out as a monolithic `by` statement to maximise 72 # parallelism. 73 s.write(' by (%s)' % ',\n '.join( 74 '%s%s' % (indent, step) for indent, step in self.steps)) 75 else: 76 if len(self.steps) > 0: 77 s.write('\n'.join( 78 ' %sapply %s' % (indent, step) for indent, step in self.steps)) 79 if self.completed is not None: 80 s.write('\n') 81 if self.completed is not None: 82 if self.subgoals == 0: 83 s.write(' %s' % self.completed) 84 else: 85 s.write(' %s%s' % (' ' * (self.subgoals - 1), self.completed)) 86 return s.getvalue() 87