-Added the annotated_beta_reduction

logic.py

@@ -236,3 +236,87 @@ def to_string(terme):
     elif isAbstraction(terme):
         return to_string_abs(terme)
     return to_string_app(terme)
+
+counters = 0
+def counter():
+    global counters
+    counters += 1
+    return counters
+
+def annotate_beta_reduction(terme):
+    if isVariable(terme): return None
+    elif isAbstraction(terme):
+        x = getInputFromAbs(terme)
+        A = getOutputFromAbs(terme)
+        B = beta_reduction(A)
+        if B != None:
+            return new_abs(x,annotate_beta_reduction(A)) 
+        else:
+            return None
+    elif isApplication(terme):
+        A1 = getFirstTerm(terme)
+        B1 = getSecondTerm(terme)
+        A2 = beta_reduction(A1)
+        B2 = beta_reduction(B1)
+        if isAbstraction(A1):
+            if A2 != None and B2 != None:
+                x1 = getInputFromAbs(A1)
+                C = getOutputFromAbs(A1)
+                communBoundVars = [i for i in getBoundVariables(C) if i in getVariables(B1)]
+                if communBoundVars == []:     
+            
+                    return new_app(annotate_beta_reduction(A1),annotate_beta_reduction(B1)) + [substitute(x1,B1,C)] + [counter()]
+                else: 
+                    t=A1
+                    for var in communBoundVars:
+                        t=alpha_rename(t,new_var(var))
+                
+                        return new_app(annotate_beta_reduction(A1),annotate_beta_reduction(B1)) + [substitute(getInputFromAbs(t),B1,getOutputFromAbs(t))] + [counter()]
+            if A2 != None and B2 == None:
+                x1 = getInputFromAbs(A1)
+                C = getOutputFromAbs(A1)
+                communBoundVars = [i for i in getBoundVariables(C) if i in getVariables(B1)]
+                if communBoundVars == []:     
+            
+                    return new_app(annotate_beta_reduction(A1),B1) + [substitute(x1,B1,C)] + [counter()]
+                else: 
+                    t=A1
+                    for var in communBoundVars:
+                        t=alpha_rename(t,new_var(var))
+                
+                    return new_app(annotate_beta_reduction(A1),B1) + [substitute(getInputFromAbs(t),B1,getOutputFromAbs(t))] + [counter()]
+            if A2 == None and B2 != None:
+                x1 = getInputFromAbs(A1)
+                C = getOutputFromAbs(A1)
+                communBoundVars = [i for i in getBoundVariables(C) if i in getVariables(B1)]
+                if communBoundVars == []:     
+            
+                    return new_app(A1,annotate_beta_reduction(B1)) + [substitute(x1,B1,C)] + [counter()]
+                else: 
+                    t=A1
+                    for var in communBoundVars:
+                        t=alpha_rename(t,new_var(var))
+                
+                        return new_app(A1,annotate_beta_reduction(B1)) + [substitute(getInputFromAbs(t),B1,getOutputFromAbs(t))] + [counter()]
+            else:
+                x1 = getInputFromAbs(A1)
+                C = getOutputFromAbs(A1)
+                communBoundVars = [i for i in getBoundVariables(C) if i in getVariables(B1)]
+                if communBoundVars == []:
+            
+                    return new_app(A1,B1) + [substitute(x1,B1,C)] + [counter()]
+                else: 
+                    t=A1
+                    for var in communBoundVars:
+                        t=alpha_rename(t,new_var(var))
+                
+                        return new_app(A1,B1) + [substitute(getInputFromAbs(t),B1,getOutputFromAbs(t))] + [counter()]
+        else:
+            if A2 != None and B2 != None:
+                return new_app(annotate_beta_reduction(A1),annotate_beta_reduction(B1))
+            if A2 != None and B2 == None:
+                return new_app(annotate_beta_reduction(A1),B1)
+            if A2 == None and B2 != None:
+                return new_app(A1,annotate_beta_reduction(B1))
+            if A2 == None and B2 == None:
+                return None
\ No newline at end of file