Skip to content

Commit

Permalink
Merge branch 'logikken-og-mere-om-implementationen' of github.com:tor…
Browse files Browse the repository at this point in the history 
…urz/PEPM2023 into logikken-og-mere-om-implementationen
  • Loading branch information
@tossenxD
tossenxD committed Oct 3, 2022
2 parents dc00943 + b35eeb1 commit d9f859f
Showing 1 changed file with 67 additions and 65 deletions.
132 changes: 67 additions & 65 deletions paper/sections/implementing.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,9 @@ \section{Implementing the editor calculus}
The implementation of the editor calculus requires

\begin{itemize}
\item implementing the semantics of the calculus and allowing for an
appropriate visualization of editing
\item implementing a type checker based on the type system
\item implementing the semantics of the calculus and allowing for an
appropriate visualization of editing
\item implementing a type checker based on the type system
\end{itemize}

but perhaps surprisingly, it involves finding a way to script editor
Expand All @@ -28,9 +28,55 @@ \subsection{Implementing the editor calculus semantics}
| Child Ast.Child
| Parent
\end{lstlisting}

The rest of the formation rules are defined similarly.


\begin{figure*}
\center
\renewcommand{\arraystretch}{2}
\begin{tabular}{llllll}
\scriptsize(AT-VAR) & $\AtVar$ & \scriptsize(AT-CONST) & $\AtConst$ & \scriptsize(AT-HOLE) & $\AtHole$ \\
\scriptsize(AT-APP) & $\AtApp$ & \scriptsize(AT-ABS) & $\AtAbs$ & \scriptsize(AT-BREAK) & $\AtBreak$ \\
\scriptsize(POS-TRIVIAL) & $\PosTrivial$ % & \scriptsize(POS-ABS) & $\PosAbs$ & \scriptsize(POS-BREAK) & $\PosBreak$ \\
\scriptsize(POS-APP-1) & $\PosAppOne$ & \scriptsize(POS-APP-2) & $\PosAppTwo$ % & \scriptsize(NEC-TRIVIAL) & $\NecTrivial$ \\
%\scriptsize(NEC-APP) & $\NecApp$ & \scriptsize(NEC-ABS) & $\NecAbs$ & \scriptsize(NEC-BREAK) & $\NecBreak$
\end{tabular}
\caption{Selected condition reduction rules}
\label{fig:conditionreductionrules}
\end{figure*}


With regards to conditions, the checks for the three modalities are implemented
in the functions $\elm{isEquivalent}$, $\elm{possibly}$ and $\elm{necessarily}$,
and checks the current AST under the cursor.

For the $\elm{isEquivalent}$ function the
\hyperref[fig:conditionreductionrules]{(AT-...)} rules are implemented by a
pattern match over the parameters.
The function applies the rules very straightforwardly such that if one of the
clauses holds then it returns $\elm{True}$ and if not then it returns
$\elm{False}$, where the only addition is the usual $\elm{never}$ function
for a node modifier hole. In rule
\hyperref[fig:conditionreductionrules]{(AT-CONST)} it is not clear whether the
constants have to be equal or just some constant in order for $\at(\const c)$ to
hold. We chose that the constants must be equal.
For all three of the functions, we discard unused parameters of the term
constructors, such as variable IDs and type annotations.

The $\elm{possibly}$ function is reduced by first checking whether we have the
trivial case \hyperref[fig:conditionreductionrules]{(POS-TRIVIAL)}. If we do
not, we check whether any of the other rules holds, i.e. if we are at an
application, abstraction or breakpoint, it calls recursively on the children of
the AST node. It deviates from the rules in that it combine the rules
\hyperref[fig:conditionreductionrules]{(POS-APP-1) and (POS-APP-2)} by a logical
or-operator.

The $\elm{necessarily}$ function is implemented in the same manner as
$\elm{possible}$, with the only difference being if it is not the trivial case
and the AST node is an application, then it uses a logical and-operator instead
of a logical or-operator.


\subsection{Abstract syntax trees}

We are interested in visualizing the AST to make the editor intuitive
Expand All @@ -42,13 +88,13 @@ \subsection{Abstract syntax trees}
as seen in figure \ref{fig:ast-in-text-form}.

\begin{figure}[H]
\Large
\begin{equation*}
\cursor{(\app{\breakpoint{(\lambda{x}{(\app{x}{x})})}}
\Large
\begin{equation*}
\cursor{(\app{\breakpoint{(\lambda{x}{(\app{x}{x})})}}
{(\lambda{x}{(\app{x}{x})})})}
\end{equation*}
\caption{An AST visualized in textual form.}
\label{fig:ast-in-text-form}
\end{equation*}
\caption{An AST visualized in textual form.}
\label{fig:ast-in-text-form}
\end{figure}

The notation used for this representation follows that of Godiksen
Expand Down Expand Up @@ -137,18 +183,18 @@ \subsection{Implementing a type checker}
\subsection{Building editor expressions}
Editor expressions written in a text field would have to be lexed and parsed.
This introduces syntax errors to the editor with regards to editor expressions,
which goes against the spirit of the editor. Hence we created an builder to
which goes against the spirit of the editor. Hence we created a way to
build editor expressions in a similar manner to ASTs.

To build editor expressions, we need to introduce holes to the editor
In order to build them, we need to introduce holes to the editor
expressions. We define a hole term constructor for each type of editor
expression, as seen in figure \ref{fig:editorexpressionswithholes}

\begin{figure}[H]
\center
\begin{tabular}{llll}
\center
\begin{tabular}{llll}

\begin{lstlisting}[language=elm,%
\begin{lstlisting}[language=elm,%
gobble=8,%
mathescape,%
]
Expand All @@ -158,7 +204,7 @@ \subsection{Building editor expressions}
| AepHole
\end{lstlisting} &

\begin{lstlisting}[language=elm,%
\begin{lstlisting}[language=elm,%
gobble=8,%
mathescape,%
]
Expand All @@ -168,7 +214,7 @@ \subsection{Building editor expressions}
| EedHole
\end{lstlisting} \\

\begin{lstlisting}[language=elm,%
\begin{lstlisting}[language=elm,%
gobble=8,%
mathescape,%
]
Expand All @@ -178,7 +224,7 @@ \subsection{Building editor expressions}
| EdtHole
\end{lstlisting} &

\begin{lstlisting}[language=elm,%
\begin{lstlisting}[language=elm,%
gobble=8,%
mathescape,%
]
Expand All @@ -187,9 +233,9 @@ \subsection{Building editor expressions}
$\vdots$
| AamHole
\end{lstlisting}
\end{tabular}
\caption{Editor expression definitions with holes}
\label{fig:editorexpressionswithholes}
\end{tabular}
\caption{Editor expression definitions with holes}
\label{fig:editorexpressionswithholes}
\end{figure}

We are now able to build editor expressions by initializing the editor
Expand Down Expand Up @@ -274,48 +320,4 @@ \subsection{The user interface}
%%% TeX-master: "../pepm2023"
%%% End:

\subsection{Conditions}

\begin{figure*}
\center
\renewcommand{\arraystretch}{2}
\begin{tabular}{llllll}
\scriptsize(AT-VAR) & $\AtVar$ & \scriptsize(AT-CONST) & $\AtConst$ & \scriptsize(AT-HOLE) & $\AtHole$ \\
\scriptsize(AT-APP) & $\AtApp$ & \scriptsize(AT-ABS) & $\AtAbs$ & \scriptsize(AT-BREAK) & $\AtBreak$ \\
\scriptsize(POS-TRIVIAL) & $\PosTrivial$ & \scriptsize(POS-ABS) & $\PosAbs$ & \scriptsize(POS-BREAK) & $\PosBreak$ \\
\scriptsize(POS-APP-1) & $\PosAppOne$ & \scriptsize(POS-APP-2) & $\PosAppTwo$ & \scriptsize(NEC-TRIVIAL) & $\NecTrivial$ \\
\scriptsize(NEC-APP) & $\NecApp$ & \scriptsize(NEC-ABS) & $\NecAbs$ & \scriptsize(NEC-BREAK) & $\NecBreak$
\end{tabular}
\caption{Condition reduction rules}
\label{fig:conditionreductionrules}
\end{figure*}

The checks for the three modalities are implemented in the functions
$\elm{isEquivalent}$, $\elm{possibly}$ and $\elm{necessarily}$, and checks the
current AST under the cursor.

For the $\elm{isEquivalent}$ function the
\hyperref[fig:conditionreductionrules]{(AT-...)} rules are implemented by a
pattern match over the parameters.
The function applies the rules very straightforwardly such that if one of the
clauses holds then it returns $\elm{True}$ and if not then it returns
$\elm{False}$, where the only addition is the usual $\elm{never}$ function
for a node modifier hole. In rule
\hyperref[fig:conditionreductionrules]{(AT-CONST)} it is not clear whether the
constants have to be equal or just some constant in order for $\at(\const c)$ to
hold. We chose that the constants must be equal.
For all three of the functions, we discard unused parameters of the term
constructors, such as variable IDs and type annotations.

The $\elm{possibly}$ function is reduced by first checking whether we have the
trivial case \hyperref[fig:conditionreductionrules]{(POS-TRIVIAL)}. If we do
not, we check whether any of the other rules holds, i.e. if we are at an
application, abstraction or breakpoint, it calls recursively on the children of
the AST node. It deviates from the rules in that it combine the rules
\hyperref[fig:conditionreductionrules]{(POS-APP-1) and (POS-APP-2)} by a logical
or-operator.

The $\elm{necessarily}$ function is implemented in the same manner as
$\elm{possible}$, with the only difference being if it is not the trivial case
and the AST node is an application, then it uses a logical and-operator instead
of a logical or-operator.

0 comments on commit d9f859f

Please sign in to comment.