rework proof printing

Author: daniyal1249

README.md

@@ -38,9 +38,10 @@ Select logic (TFL, FOL, MLK, MLT, MLS4, MLS5): TFL
 Enter premises (separated by "," or ";"), or "NA" if none: P -> Q, P
 Enter conclusion: Q
 
- 1 | P → Q      PR
- 2 | P          PR
-   |---
+ 1 │ P → Q      PR
+   │
+ 2 │ P          PR
+   ├───
 
 1 - Add a new line
 2 - Begin a new subproof
@@ -51,10 +52,11 @@ Enter conclusion: Q
 Select action: 1
 Enter line: Q ; ->E, 1,2
 
- 1 | P → Q      PR
- 2 | P          PR
-   |---
- 3 | Q          →E, 1,2
+ 1 │ P → Q      PR
+   │
+ 2 │ P          PR
+   ├───
+ 3 │ Q          →E, 1,2
 
 Proof complete! 🎉
 ```
@@ -63,18 +65,23 @@ A proof of the law of excluded middle (LEM) using ND-Prover:
 
 ```
 Proof of  ∴ P ∨ ¬P
-------------------
-
- 1 | | ¬(P ∨ ¬P)       AS
-   | |-----------      
- 2 | | | P             AS
-   | | |---            
- 3 | | | P ∨ ¬P        ∨I, 2
- 4 | | | ⊥             ¬E, 1,3
- 5 | | ¬P              ¬I, 2-4
- 6 | | P ∨ ¬P          ∨I, 5
- 7 | | ⊥               ¬E, 1,6
- 8 | P ∨ ¬P            IP, 1-7
+──────────────────
+
+ 1 │ │ ¬(P ∨ ¬P)       AS
+   │ ├───────────      
+ 2 │ │ │ P             AS
+   │ │ ├───            
+ 3 │ │ │ P ∨ ¬P        ∨I, 2
+   │ │ │               
+ 4 │ │ │ ⊥             ¬E, 1,3
+   │ │                 
+ 5 │ │ ¬P              ¬I, 2-4
+   │ │                 
+ 6 │ │ P ∨ ¬P          ∨I, 5
+   │ │                 
+ 7 │ │ ⊥               ¬E, 1,6
+   │                   
+ 8 │ P ∨ ¬P            IP, 1-7
 
 Proof complete! 🎉
 ```
@@ -83,15 +90,19 @@ A proof that identity is symmetric:
 
 ```
 Proof of  ∴ ∀x∀y(x = y → y = x)
--------------------------------
-
- 1 | | a = b                  AS
-   | |-------
- 2 | | a = a                  =I
- 3 | | b = a                  =E, 1,2
- 4 | a = b → b = a            →I, 1-3
- 5 | ∀y(a = y → y = a)        ∀I, 4
- 6 | ∀x∀y(x = y → y = x)      ∀I, 5
+───────────────────────────────
+
+ 1 │ │ a = b                  AS
+   │ ├───────                 
+ 2 │ │ a = a                  =I
+   │ │                        
+ 3 │ │ b = a                  =E, 1,2
+   │                          
+ 4 │ a = b → b = a            →I, 1-3
+   │                          
+ 5 │ ∀y(a = y → y = a)        ∀I, 4
+   │                          
+ 6 │ ∀x∀y(x = y → y = x)      ∀I, 5
 
 Proof complete! 🎉
 ```
@@ -100,19 +111,23 @@ A proof in modal logic S5:
 
 ```
 Proof of ♢□A ∴ □A
------------------
-
- 1 | ♢□A          PR
-   |-----         
- 2 | ¬□¬□A        Def♢, 1
- 3 | | ¬□A        AS
-   | |-----       
- 4 | | | □        AS
-   | | |---       
- 5 | | | ¬□A      R5, 3
- 6 | | □¬□A       □I, 4-5
- 7 | | ⊥          ¬E, 2,6
- 8 | □A           IP, 3-7
+─────────────────
+
+ 1 │ ♢□A          PR
+   ├─────         
+ 2 │ ¬□¬□A        Def♢, 1
+   │              
+ 3 │ │ ¬□A        AS
+   │ ├─────       
+ 4 │ │ │ □        AS
+   │ │ ├───       
+ 5 │ │ │ ¬□A      R5, 3
+   │ │            
+ 6 │ │ □¬□A       □I, 4-5
+   │ │            
+ 7 │ │ ⊥          ¬E, 2,6
+   │              
+ 8 │ □A           IP, 3-7
 
 Proof complete! 🎉
 ```

interactive.py

@@ -242,7 +242,7 @@ async def send_proof_msg(ctx, session):
     """
     premises = ', '.join(str(p) for p in session.premises)
     first_line = f'Proof of {premises} ∴ {session.conclusion}'
-    content = f'{first_line}\n{'-' * len(first_line)}\n\n{session.proof}'
+    content = f'{first_line}\n{'─' * len(first_line)}\n\n{session.proof}'
 
     # Delete previous proof message, if it exists
     if session.proof_msg:

nd_prover/__init__.py

@@ -1,4 +1,4 @@
-__version__ = '0.1.0'
+__version__ = '1.0.0'
 __author__ = 'Daniyal Akif'
 __email__ = '[email protected]'
 __license__ = 'MIT'

nd_prover/logic.py

@@ -824,27 +824,24 @@ def _begin_subproof_current(self, assumption):
         self.seq.append(subproof)
 
     def _collect_lines(self, depth=0):
-        indent = ' '.join('|' * (depth + 1))
-        assumptions = self.seq[:1] if self.assumption else self.context
-        lines = []
-
-        for a in assumptions:
-            line = (a.idx, f'{indent} {a.formula}', a.justification)
-            lines.append(line)
-
-        if assumptions:
-            bar_len = len(str(assumptions[-1].formula)) + 2
-            line = ('', f'{indent}{'-' * bar_len}', '')
-            lines.append(line)
+        indent = '│ ' * depth
+        seq = self.seq if self.assumption else self.context + self.seq
+        bar_idx = 0 if self.assumption else len(self.context) - 1
 
-        i = 1 if self.assumption else 0
-        for obj in self.seq[i:]:
+        lines = []
+        for idx, obj in enumerate(seq):
             if obj.is_line():
+                formula = str(obj.formula)
                 j = obj.justification
-                line = (obj.idx, f'{indent} {obj.formula}', j)
-                lines.append(line)
+                lines.append((obj.idx, f'{indent}│ {formula}', j))
             else:
                 lines.extend(obj._collect_lines(depth + 1))
+
+            if idx == bar_idx:
+                bar = f'{indent}├{'─' * (len(formula) + 2)}'
+                lines.append(('', bar, ''))
+            elif idx != len(seq) - 1:
+                lines.append(('', f'{indent}│', ''))
         return lines
 
 

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "setuptools.build_meta"
 
 [project]
 name = "nd-prover"
-version = "0.1.0"
+version = "1.0.0"
 description = "An interactive Fitch-style proof checker"
 authors = [{ name = "Daniyal Akif", email = "[email protected]" }]
 readme = "README.md"
@@ -22,7 +22,7 @@ keywords = [
 ]
 
 classifiers = [
-    "Development Status :: 3 - Alpha",
+    "Development Status :: 5 - Production/Stable",
     "Intended Audience :: Science/Research",
     "License :: OSI Approved :: MIT License",
     "Programming Language :: Python :: 3",