Commit 53a14714 authored by Michael Banken's avatar Michael Banken

added stuff to integration

parent a645b394
......@@ -5,4 +5,6 @@
author={Rupprecht, Marcel and Kohlhase, Michael and M{\"u}ller, Dennis},
journal={MathUI},
year={2017}
}
\ No newline at end of file
}
@misc{MMTapi, title={{MMT API Documentation}}, howpublished = {\url{https://uniformal.github.io/apidoc/index.html}}, journal={MMT Documentation}, publisher={uniformal.github.io}, note={Accessed: 2018-06-14}}
\ No newline at end of file
img/placeholder.png

3.68 KB | W: | H:

img/placeholder.png

11.4 KB | W: | H:

img/placeholder.png
img/placeholder.png
img/placeholder.png
img/placeholder.png
  • 2-up
  • Swipe
  • Onion skin
\chapter{Algorithm}
\label{chap:alg}
\section{Idea}
Since our approach to identifying candidates is large based on set theory, the algorithms for finding are also making heavy use of set operations, using essentially the same construction method for creating the set of optimization candidates as the definitions presented in \autoref{chap:candidates}.
......@@ -114,7 +115,7 @@ To somewhat mitigate the effect this has on the performance, the future is creat
\section{Pseudo Code}
\subsection{Optimizing graph}
\label{sec:optgraph}
The following code applies the optimizations to the entire theory graph.
\begin{algorithm}[H]
......@@ -139,7 +140,7 @@ The following code applies the optimizations to the entire theory graph.
\end{algorithm}
\subsection{Optimizing theory}
\label{sec:opttheo}
The following pseudo code applies optimizations to a given theory.
\begin{algorithm}[H]
......
\chapter{Conclusion}
\section{State of the project}
\section{Future Work}
\ No newline at end of file
\section{Future Work}
\label{sec:futurework}
While the tool in its current state fulfils our goal to automate large parts of the optimization process, there are still many improvements that could be made.
The most important future goal is to further automate the optimization process. Most importantly actually applying the changes to the graph and its source files. While the tool in its current state is capable of making fully automated suggestions, all the suggestions need to be applied to the sources by hand. This is less than ideal.
Another important step is providing a proper interface for calling the optimizer. Preferably in a way that would seamlessly integrate with other MMT components.
Finally the runtime of the algorithm is a concern, as we discussed in \autoref{sec:runtime}. While it seems to run fine on small graphs, this could easily blow up for larger graphs. So any optimizations to the algorithm itself could be a welcome improvement.
\ No newline at end of file
\chapter{Implementation}
\label{chap:implementation}
\section{Integration}
The intended interface for programmers accessing the graph optimizations corresponds more or less directly to the routines presented in \autoref{chap:alg}. They are implemented as methods of the class GraphOptimizationTool, which itself is a subclass of info.kwarc.mmt.api.frontend.Extension\cite{MMTapi}.
At the moment calling these functions is the only way to access the optimization functions, but this should change at some point in the future (see \autoref{sec:futurework}).
\subsection{Programming Interface}
\label{sec:api}
\begin{lstlisting}[language=scala]
/** Find simply redundant inclusions
*
* This method finds inclusions that are redundant, since they are already part of a different inclusion
......@@ -16,6 +20,8 @@
def findRedundantIncludes(theoryPath : MPath, replacementmap : HashMap[MPath, HashMap[Path, HashSet[MPath]]] = HashMap[MPath, HashMap[Path, HashSet[MPath]]]()) : List[Path]
\end{lstlisting}
The method findRedundantIncludes is implementing simplyRedundantIncludes i.e the second pass from \autoref{sec:alg_sri}.
\begin{lstlisting}[language=scala]
/** Finds superfluous inclusions
*
......@@ -28,6 +34,8 @@ def findRedundantIncludes(theoryPath : MPath, replacementmap : HashMap[MPath, Ha
def findUnusedIncludeReplacements(theoryPath : MPath, replacementmap : HashMap[MPath, HashMap[Path, HashSet[MPath]]] = HashMap[MPath, HashMap[Path, HashSet[MPath]]](), futureUse : HashMap[MPath, HashSet[MPath]] = HashMap[MPath, HashSet[MPath]]()) : HashMap[Path, HashSet[MPath]]
\end{lstlisting}
The method findUnusedIncludeReplacements is implementing superfluousIncludes(theory, futureUse) i.e the first pass from \autoref{sec:alg_si}.
\begin{lstlisting}[language=scala]
/** Optimizes multiple theories
*
......@@ -39,6 +47,14 @@ def findUnusedIncludeReplacements(theoryPath : MPath, replacementmap : HashMap[M
def findReplacements(theories: Iterable[MPath], interactive : Boolean) : HashMap[MPath, HashMap[Path, HashSet[MPath]]]
\end{lstlisting}
This method findReplacements is similar to optimize(theory, futureUse)(\autoref{sec:opttheo}) and optimizeGraph(theorygraph)(\autoref{sec:optgraph}). The difference is that the method takes a an Iterable of theories, for which to apply the graph optimization algorithm. In other words it is applying the optimizations not to the entire graph, but a given subset.
The boolean parameter interactive chooses whether to launch the interactive mode or not.
If true is selected the method will open a dialogue window (see \autoref{sec:ui}) that allows the user to select the changes he wants to apply to the graph, from those suggested by the algorithm.
If false is selected all suggested changes will be applied.
\begin{lstlisting}[language=scala]
/** Optimizes all known theories
*
......@@ -48,6 +64,10 @@ def findReplacements(theories: Iterable[MPath], interactive : Boolean) : HashMap
def findReplacements(interactive : Boolean = false) : HashMap[MPath, HashMap[Path, HashSet[MPath]]]
\end{lstlisting}
This method findReplacements(theories, interactive) is implementing optimizeGraph(theorygraph)from \autoref{sec:optgraph}. De facto it is a wrapper that calls the earlier findReplacements method on an Iterable over every theory it can find.
This method also comes with an optional boolean parameter to choose between interactive and non-interactive mode (defaults to false).
\begin{lstlisting}[language=scala]
/** Converts map to xml
*
......@@ -58,13 +78,38 @@ def findReplacements(interactive : Boolean = false) : HashMap[MPath, HashMap[Pat
def toXML(map : HashMap[MPath, HashMap[Path, HashSet[MPath]]]) : String
\end{lstlisting}
The method toXML is used to convert the output from the findReplacements methods into human readable xml. The specification of the xml output can be found in \autoref{sec:xml}.
\subsection{User Interface}
In its current form the user interface is limited to the dialogue window created by the findReplacement procedure. The dialogue will provide the user with a suggested change to the theory graph.
\label{sec:ui}
\begin{figure}[!htb]
\centering
\includegraphics[scale=.5]{styler_window}
\caption{A screenshot of the styler dialog}
\label{fig:dialog}
\caption{A screenshot of a suggestion to remove a simply redundant inclusion}
\label{fig:dialogsri}
\end{figure}
\subsection{UML}
\label{sec:uml}
\ No newline at end of file
In \autoref{fig:dialogsri} we can see the suggestion for removing a simply redundant inclusion. The dialogue offers the user 4 options.
\begin{itemize}
\item yes: apply the change
\item no: do not apply this change
\item never: never apply changes to this theory
\item later: ask again later
\end{itemize}
\begin{figure}[!htb]
\centering
\includegraphics[scale=.5]{styler_window_replace}
\caption{A screenshot of a suggestion to replace a partially superfluous inclusion}
\label{fig:dialogsi}
\end{figure}
In \autoref{fig:dialogsi} we can see a similar suggestion for removing a partially superfluous inclusion. It differs from the former in that it not only lists a theory to be replaced, but also what to replace it with.
The functionality of the buttons remains the same as in the case above.
\subsection{XML}
\label{sec:xml}
\chapter{Introduction}
\section{Motivation}
Knowledge is complex and so is its representation.
Knowledge is complicated and so is its representation.
\begin{figure}[!htb]
\centering
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment