Merge pull request #1 from isahers1/Isaac-GUI

Convert to main

README.md

@@ -1 +1,26 @@
-# global-environment
+# Automated Proof Checker
+
+## Set up
+
+1. Clone the repository using `git clone`
+2. Install packages using preferred installer - need to fix, create pip requirements file
+
+## Codebase
+
+The codebase we have designed seperates the elements of abstract algebra into different environments to make writing proofs a seamless experience. The main files are `proof.py,group.py,element.py,` and `logicObjects.py`. The names are pretty self explanatory, but to learn more about how each of the files work poke around some of the `__init__` calls and member functions of those files to see how they interact together. 
+
+## Usage
+
+There are two options to use our proof-checker, but we **highly** recommend using the first option.
+
++ Using our graphical user interface!
+    1. Run `python gui.py` to open the interface
+    2. The **Enter** button is used to enter new steps. As you type in the black text box the possible functions yoiu could call will appear below so you never make spelling errors! Warnings will appear if you attempt a step that is not valid.
+    3. The **Generate Latex** will take the proof, convert it to a latex file and display the corresponding pdf inside of the GUI in real time!
+    4. The **Undo** button deletes the last step you did - be careful to only use this when you need it!
++ Using our raw language in a python file
+    1. Open a new file called `my_proof_name_here.py`, with a descriptive name for your proof 
+    2. Create a new proof object using the `Proof` function from `proof.py`
+    3. Enter the steps of your proof using the functions in `proof.py`
+    4. Run the command `python my_proof_name_here.py` to see the proof steps in the console.
+

Simple Abelian Proof.tex

@@ -0,0 +1,17 @@
+\documentclass{article}%
+\usepackage[T1]{fontenc}%
+\usepackage[utf8]{inputenc}%
+\usepackage{lmodern}%
+\usepackage{textcomp}%
+\usepackage{lastpage}%
+%
+\title{Simple Abelian Proof}%
+%
+\begin{document}%
+\normalsize%
+\maketitle%
+\textit{Proof:}%
+\begin{enumerate}%
+\addtocounter{enumi}{-1}%
+\end{enumerate}%
+\end{document}

group.py

@@ -64,4 +64,7 @@ def addElementProperty(self, property, elementName):
             print("That element doesn't exist!", property, elementName)
 
     def contains(self, elementName):
-        return elementName in self.elements
+        return elementName in self.elements
+
+    def toLaTeX(self):
+        return self.groupName

gui.py

@@ -0,0 +1,161 @@
+from tkinter import PhotoImage
+from tkinter import ttk
+from tkinter import *
+from turtle import undo
+from proof import *
+from tkinter.scrolledtext import ScrolledText
+import fitz
+from ttkwidgets.autocomplete import AutocompleteCombobox
+
+
+proof_methods = ['MultElem', 'accessAssumption', 'andElim', 'breakPower', 'cancelLeft', 
+'cancelRight', 'closure', 'combinePower', 'concludeSubproof', 'forAllIntroduction', 'forallElim',
+'identleft', 'identright', 'impliesIntroduction', 'introAssumption', 'introCases', 'introElement',
+'introGroup', 'introReflexive', 'introSubproof', 'inverseElimLHS', 'inverseElimRHS', 'leftMult',
+'leftSidesEq', 'modus', 'notElim', 'qed', 'reduceLogic', 'rightMult', 'rightSidesEq', 'show',
+'showReturn', 'splitPowerAddition', 'splitPowerMult', 'substituteLHS', 'substituteRHS',
+'switchSidesOfEqual', 'thereexistsElim', 'undo', 'writeLaTeXfile']
+
+class PDFViewer(ScrolledText):
+    def show(self, pdf_file):
+        self.delete('1.0', 'end') # clear current content
+        pdf = fitz.open(pdf_file) # open the PDF file
+        self.images = []   # for storing the page images
+        for page in pdf:
+            pix = page.get_pixmap()
+            pix1 = fitz.Pixmap(pix, 0) if pix.alpha else pix
+            photo = PhotoImage(data=pix1.tobytes('ppm'))
+            # insert into the text box
+            self.image_create('end', image=photo)
+            self.insert('end', '\n')
+            # save the image to avoid garbage collected
+            self.images.append(photo)
+
+
+def enter(*args):
+    input = entry.get()
+    input = "p."+input
+    print(input)
+    try:
+        exec(input)
+    except:
+        messagebox.showerror('Syntax Error', 'You have either called a function that does not exist or passed a variable that is not defined - or both!')
+    showing.set(p.showReturn())
+    entry_bar.delete(0,"end")
+
+
+def generateLaTeX(*args):
+    p.writeLaTeXfile()
+    pdf1.show('Simple Abelian Proof.pdf')
+
+G = group('G','*')
+abelianG = forall(['x', 'y'], G, Eq(Mult(['x', 'y']), Mult(['y','x']),G))
+p = Proof('Simple Abelian Proof', forall(['x'], G, Eq(Mult(['x', 'x']), G.elements['e'],G)), goal=abelianG)
+
+root = Tk()
+root.title("Proof-Check")
+
+mainframe = ttk.Frame(root, padding="3 3 12 12")
+mainframe.grid(column=0, row=0, sticky=(N, W, E, S))
+root.columnconfigure(0, weight=1)
+root.rowconfigure(0, weight=1)
+
+pdf1 = PDFViewer(mainframe, width=80, height=30, spacing3=5, bg='blue')
+pdf1.grid(row=5, column=1, sticky='nsew')
+pdf1.show('Simple Abelian Proof.pdf')
+
+
+def match_string():
+    hits = []
+    got = entry_bar.get()
+    for item in proof_methods:
+        if item.startswith(got):
+            hits.append(item)
+    return hits   
+
+def match_string_del():
+    hits = []
+    got = entry_bar.get()[:-1]
+    for item in proof_methods:
+        if item.startswith(got):
+            hits.append(item)
+    return hits 
+
+def check_empty(event):
+    if len(entry_bar.get()) == 1:
+        suggestions.set("") 
+    else:
+        hits = match_string_del()
+        show_hit(hits)
+
+def get_typed(event):
+    if len(event.keysym) == 1:
+        hits = match_string()
+        show_hit(hits)
+
+def show_hit(lst):
+    suggestions.set(lst)
+    if len(lst) == 1:
+        entry.set(lst[0])
+        detect_pressed.filled = True
+        entry_bar.icursor(END)
+
+def detect_pressed(event):    
+    key = event.keysym
+    if len(key) == 1 and detect_pressed.filled is True:
+        pos = entry_bar.index(INSERT)
+        entry_bar.delete(pos, END)
+
+detect_pressed.filled = False
+
+
+entry = StringVar()
+entry_bar = Entry(
+    mainframe, 
+    width = 50,
+    bg='black',
+    insertbackground='white',
+    fg='white',
+    textvariable=entry)
+entry_bar.grid(column=1, row=3, sticky=(W, E))
+entry_bar.focus_set()
+entry_bar.bind('<KeyRelease>', get_typed)
+entry_bar.bind('<Key>', detect_pressed)
+entry_bar.bind('<BackSpace>', check_empty)
+
+def undo(*args):
+    p.undo()
+    showing.set(p.showReturn())
+
+
+#entry_bar = AutocompleteCombobox(mainframe, width=50, textvariable=entry, completevalues = proof_methods)
+
+
+showing = StringVar()
+showing.set("Proof : Simple Abelian Proof\n--------------------------------")
+
+showProof = ttk.Label(mainframe, background="white", textvariable=showing).grid(column=1, row=2, sticky=(W, E))
+
+ttk.Button(mainframe, text="Enter", command=enter).grid(column=3, row=3, sticky=W)
+
+ttk.Button(mainframe, text="Undo", command=undo).grid(column=3, row=2, sticky=W)
+
+ttk.Button(mainframe, text="Generate Latex", command=generateLaTeX).grid(column=3, row=4, sticky=W)
+
+suggestions = StringVar()
+showSuggestions = ttk.Label(mainframe, width = 50, background="white", textvariable=suggestions).grid(column=1, row=4, sticky=(W, E))
+
+for child in mainframe.winfo_children(): 
+    child.grid_configure(padx=5, pady=5)
+
+entry_bar.focus()
+root.bind("<Return>", enter)
+
+# creating object of ShowPdf from tkPDFViewer.
+#v1 = pdf.ShowPdf().pdf_view(mainframe, pdf_location = r"Simple Abelian Proof.pdf").grid(column=1, row=4, sticky=W)
+
+
+# Placing Pdf in my gui.
+#v2.grid(column=1, row=4, sticky=W)
+
+root.mainloop()

logicObjects.py

@@ -37,6 +37,9 @@ def replace(self, var, expr):
                     new_products.append(self.products[i])
                     i+=1
         return Mult(new_products)
+
+    def toLaTeX(self):
+        return "".join(self.elemList)
 
 
 class And:
@@ -57,6 +60,9 @@ def __eq__(self,other):
 
     def __repr__(self):
         return "("+ str(self.arg1)+" and "+str(self.arg2)+ ")"
+
+    def toLaTeX(self):
+        return self.arg1.toLaTeX() + r" and " + self.arg2.toLaTeX()
 
 class Or:
     def __init__(self, arg1, arg2):
@@ -69,6 +75,9 @@ def elim(self,num,implies1,implies2):
         check2 = isinstance(implies2, Implies) and implies2.assum==self.arg2
         if check1 and check2 and implies1.conc==implies2.conc:
             return implies1.conc
+
+    def toLaTeX(self):
+        return self.arg1.toLaTeX() + r" or " + self.arg2.toLaTeX()
 
 class Implies: # expand a little more functionality
     def __init__(self, assum, conc):
@@ -86,6 +95,9 @@ def __eq__(self, other):
 
     def __repr__(self):
         return  str(self.assum) + " → " +  str(self.conc)
+
+    def toLaTeX(self):
+        return self.arg1.toLaTeX() + r" \implies " + self.arg2.toLaTeX()
 
 class Not:
     def __init__(self, arg):
@@ -97,13 +109,19 @@ def elim(self, contradiction):
 
     def __repr__(self):
         return "Not " + str(self.arg)
+
+    def toLaTeX(self):
+        return r"\lnot " + self.arg.toLaTeX()
 
 class Bottom:
     def elim(self, conclusion):
         return conclusion
 
     def __repr__(self):
         return "⊥"
+
+    def toLaTeX(self):
+        return r"\bot"
 
 class In:
     def __init__(self, elem, grp):
@@ -112,6 +130,9 @@ def __init__(self, elem, grp):
 
     def __repr__(self):
         return str(self.elem) + " ∈ " + str(self.group)
+
+    def toLaTeX(self):
+        return str(self.elem) + r" \in " + str(self.group)
 
 class Eq:
     def __init__(self,LHS,RHS,pg):
@@ -132,6 +153,9 @@ def __eq__(self,other):
 
     def replace(self, var, expr):
         return Eq(self.LHS.replace(var,expr), self.RHS.replace(var,expr), self.group)
+
+    def toLaTeX(self):
+        return str(self.LHS) + r" = " + str(self.RHS)
 
 def reduce(exp):
     if isinstance(exp, Eq):
@@ -172,6 +196,9 @@ def __eq__(self,other):
         else:
             return False
 
+    def toLaTeX(self):
+        return r"\forall " + ",".join(self.arbelems) + r" \in " + str(self.group) + r"\ " + self.eq.toLaTeX()
+
 
     def replace(self, replacements): # replacements = ['x','y'] - strings of the elements
         if len(replacements) == len(self.arbelems):
@@ -211,6 +238,9 @@ def replace(self, replacements):
         else:
             print("Replacements is not the same length as the list of existential elements")
 
+    def toLaTeX(self):
+        return r"\exists " + ",".join(self.existelems) + r" \in " + str(self.group)  + r"\ " + self.toLaTeX(self.eq)
+
 ## Unique class - idk if we need this
 
 class uniqueElementProperty: