From e7785dbb8884966cd1298bd624eaaf496668d47f Mon Sep 17 00:00:00 2001
From: Morris Kyn <morris.kyn@gmail.com>
Date: Tue, 12 Apr 2022 13:52:47 -0700
Subject: [PATCH] Returns after every error message(so function doesn't
 continue)

---
 proof.py | 18 +++++++++++++++---
 1 file changed, 15 insertions(+), 3 deletions(-)

diff --git a/proof.py b/proof.py
index 759b737..228b562 100644
--- a/proof.py
+++ b/proof.py
@@ -16,7 +16,6 @@ def __init__(self, label, assumption, goal=None, steps=[], justifications = []):
         self.depth = 0
     
     def qed(self, lineNum):
-        print(self.goal, self.steps[lineNum])
         if self.goal == self.steps[lineNum]:
             self.steps+=["□"]
             self.justifications += ["QED"]
@@ -156,6 +155,7 @@ def inverseElimRHS(self,lineNum):
                     break
             if lawApplied==False:
                 print (f"Inverse laws can't be applied on line {lineNum}")
+                return
         self.steps += [newProducts]
         self.justifications += [f'Right hand side inverse elimination on line {lineNum}'] 
         self.show()
@@ -184,6 +184,7 @@ def inverseElimLHS(self,lineNum):
                     break
             if lawApplied==False:
                 print (f"Inverse laws can't be applied on line {lineNum}")
+                return
         self.steps += [newProducts]
         self.justifications += [f'Left hand side inverse elimination on line {lineNum}'] 
         self.show()
@@ -230,6 +231,7 @@ def leftMult (self, elem, lineNum):
         eq = copy.deepcopy(self.steps[lineNum])
         if isinstance(eq, Eq) == False:
             print (f"Line {lineNum} is not an equation")
+            return
         product = self.MultElem(elem, eq.LHS)
         result = Eq(product, self.MultElem(elem,eq.RHS), eq.parentgroup)
         self.steps += [result]
@@ -245,6 +247,7 @@ def rightMult (self, elem, lineNum):
         eq = copy.deepcopy(self.steps[lineNum])
         if isinstance(eq, Eq) == False:
             print (f"Line {lineNum} is not an equation")
+            return
         product = self.MultElem(eq.LHS, elem)
         result = Eq(product, self.MultElem(eq.RHS,elem), eq.parentgroup)
         self.steps += [result]
@@ -276,6 +279,7 @@ def combinePower(self, mult):
         for i in multList: 
             if i != e: 
                 print ("Need a single element but given multiple")
+                return
         result=power(e,len(multList)) 
         self.steps += [result]
         self.justifications += ['Convert multiplications to equivalent powers'] 
@@ -290,7 +294,8 @@ def splitPowerAddition(self,power):
         exp=self.exponent
         l=exp.split("+")
         if len(l)==1:
-            print ("No power addition to be split apart") 
+            print ("No power addition to be split apart")
+            return
         multList=[]
         for i in l: 
             elem=power(element,i)
@@ -309,7 +314,8 @@ def splitPowerMult(self,power):
         exp=self.exponent
         l=exp.split("*")
         if len(l)==1:
-            print ("No power multiplication to be split apart") 
+            print ("No power multiplication to be split apart")
+            return
         elem=element
         for i in l: 
             e=power(elem,i)
@@ -333,6 +339,7 @@ def rightSidesEq(self, lineNum1, lineNum2):
             self.show()
         else:
             print (f"The equations on lines {str(lineNum1)}, {str(lineNum2)} do not have the same right sides")
+            return
 
     def leftSidesEq(self, lineNum1, lineNum2):
         """
@@ -348,6 +355,7 @@ def leftSidesEq(self, lineNum1, lineNum2):
             self.show()
         else:
             print (f"The equations on lines {str(lineNum1)}, {str(lineNum2)} do not have the same left sides")
+            return
 
     def identleft(self, lineNum):
         """
@@ -372,6 +380,7 @@ def identleft(self, lineNum):
                 # else we can't apply identity elimination 
             if l1==[]:
                 print ("identity can't be applied")
+                return
             newProduct = Mult(l1)
             ret = Eq(newProduct,evidence.RHS,evidence.parentgroup)
 
@@ -402,6 +411,7 @@ def identright(self, lineNum):
                 # else we can't apply identity elimination 
             if l1==[]:
                 print ("identity can't be applied")
+                return
             newProduct = Mult(l1)
             ret = Eq(evidence.LHS,newProduct,evidence.parentgroup)
 
@@ -499,8 +509,10 @@ def forAllIntroduction(self, equationLine, vars, elemIntroLines):
             l = elemIntroLines[i]
             if self.steps[l].elem!=vars[i]:
                 print("Line", l, "does not introduce variable", v)
+                return
             if self.steps[l].grp!=G:
                 print("Element", v, "is not in group", G)
+                return
         #If you make it here, this is a valid for all intro
         self.steps+=[forall(vars,G,self.steps[equationLine])]
         self.justifications+=["For all introduction"]