-
Notifications
You must be signed in to change notification settings - Fork 1
/
main.py
63 lines (54 loc) · 2.56 KB
/
main.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
from textwrap import fill
from sequent import Sequent
from openpyxl import Workbook
from openpyxl.styles.alignment import Alignment
from openpyxl.styles import PatternFill
class SequentTreePrinter:
sequent_root: Sequent
color: str
def __init__(self, sequent_root: Sequent, is_proved) -> None:
if not sequent_root.is_calculated == True:
raise SequentNotCalculatedException()
self.sequent_root = sequent_root
self.color = "0042f569" if is_proved else "00f55142"
def print_in_workbook(self):
wb = Workbook()
sheet = wb.active
self.generate_sheet(sheet)
wb.close()
wb.save("SequentTree.xlsx")
def generate_sheet(self, sheet):
self.sequent_root.cal_size()
self.sequent_root.cal_children_space_before()
max_length = self.sequent_root.cal_max_length()
self.put_sequent_in_sheet(self.sequent_root, max_length, sheet, self.color)
@classmethod
def put_sequent_in_sheet(cls, sequent: Sequent, max_length, sheet, color):
if sequent.size > 1:
sheet.merge_cells(
start_row=sequent.level, end_row=sequent.level,
start_column=sequent.space_before+1,
end_column=sequent.space_before+sequent.size
)
cell = sheet.cell(sequent.level, sequent.space_before+1)
cell.alignment = Alignment(horizontal='center', vertical="center")
cell.fill = PatternFill(start_color=color, end_color=color, fill_type='solid')
cell.value = str(sequent)
if not sequent.children:
sheet.column_dimensions[cell.column_letter].width = int(3 * len(str(sequent)))
for ch in sequent.children:
cls.put_sequent_in_sheet(ch, max_length, sheet, color)
class SequentNotCalculatedException(Exception):
pass
print("""***Welcome to Sequent Calculus Program.***
Try to write your formula below.
Note: You can use connectives like 'and' by '/\\', 'or' by '\\/', 'negation' by '~' and 'imply' by '->'.
Note: Surround all of your formula with parens to make it well-formed!
Note: The sequent tree will be outputed in file 'SequentTree.xlsx'!
Note: If the formula has been proved, xl file will be shown by green background and otherwise it will be red.
Note: Use spaces between connectives and atomics. It will output wrong if you don't do this.
""")
root = Sequent.init_by_formula(input("Type your formula: "))
is_proved = root.calculate()
printer = SequentTreePrinter(root, is_proved)
printer.print_in_workbook()