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