From 59fc7cc631dd8dc7f5c6239fe1d974cab5366c53 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jasper=20Clemens=20Gr=C3=A4flich?= <jasper.graeflich@ptb.de>
Date: Thu, 18 Aug 2022 12:10:12 +0200
Subject: [PATCH] Change the rest of lstlistings to minted
---
thesis/1-1-2-borrowing.tex | 4 ----
thesis/1-1-5-reborrows.tex | 3 ---
thesis/1-2-2-refinement-types.tex | 32 +++++++++++++++++++------------
thesis/1-introduction.tex | 4 ++--
4 files changed, 22 insertions(+), 21 deletions(-)
diff --git a/thesis/1-1-2-borrowing.tex b/thesis/1-1-2-borrowing.tex
index b05384a..dcb02a1 100644
--- a/thesis/1-1-2-borrowing.tex
+++ b/thesis/1-1-2-borrowing.tex
@@ -8,10 +8,6 @@ As we have seen, ownership and move semantics ensure memory safety. But they are
That is where references and borrowing come in. Instead of taking ownership of a value, a function can only borrow it through a reference. Then the drop responsibility stays with the caller. References, of course, can not be used for everything, but for our case it is sufficient. We mark the argument to \inline{print_value} as a reference using \inline{&}, and creating a reference from a value works the same.
-\begin{lstlisting}[language=Rust, caption={}, label={}]
-
-\end{lstlisting}
-
\begin{listing}[H]
\begin{minted}{rust}
fn print_value(ptr: &Box<i32>) {
diff --git a/thesis/1-1-5-reborrows.tex b/thesis/1-1-5-reborrows.tex
index eaaa853..e33f11a 100644
--- a/thesis/1-1-5-reborrows.tex
+++ b/thesis/1-1-5-reborrows.tex
@@ -55,9 +55,6 @@ But why does the code in \autoref{lst:moved-borrow} work? The compiler can inser
Reborrows won’t solve every problem, though. Consider the code in \autoref{lst:two-phase-borrow}. Here we create a vector and then push its length onto it.
-\begin{lstlisting}[language=Rust, caption={}, label={}]
-
-\end{lstlisting}
\begin{listing}[H]
\begin{minted}{rust}
diff --git a/thesis/1-2-2-refinement-types.tex b/thesis/1-2-2-refinement-types.tex
index 6538b94..ea011d1 100644
--- a/thesis/1-2-2-refinement-types.tex
+++ b/thesis/1-2-2-refinement-types.tex
@@ -73,10 +73,14 @@ Since the inception of set theory, mathematicians used \emph{set comprehension}
\noindent\inline{Prop} is a helper type which can only be created from a true value. We need this so that we can proof that \inline{val} makes \inline{prop} true. This would now allow us to create constants that have certain proven properties like in \autoref{lst:proven-const}.
-\begin{lstlisting}[language=Rust, caption={Constants with proven properties}, label={lst:proven-const}]
-const PRIME: Subtype<i32, is_prime> = Subtype::new(17);
-const SMALL: Subtype<u32, |x| x <= 255> = Subtype::new(9);
-\end{lstlisting}
+\begin{listing}[H]
+ \begin{minted}{rust}
+ const PRIME: Subtype<i32, is_prime> = Subtype::new(17);
+ const SMALL: Subtype<u32, |x| x <= 255> = Subtype::new(9);
+ \end{minted}
+ \caption{Constants with proven properties}
+ \label{lst:proven-const}
+\end{listing}
\noindent Because this is cumbersome, it would also be nice to extend the syntax for easier definition of a refinement type and let the compiler automatically insert the \inline{Subtype::new}.
@@ -95,14 +99,18 @@ const SMALL: Subtype<u32, |x| x <= 255> = Subtype::new(9);
In the previous example, the predicate only took one input, namely the comprehension variable itself. And as long as only simple types are refined, this is the only possibility. But refinement types really shine when they depend on multiple inputs. The prime example is a function concatenating two arrays:
-\begin{lstlisting}[language=Rust, caption={Concatenate two arrays, with a deprendent output type}, label={lst:concat-refined}]
-fn concat<T, const N: usize, const M: usize>(
- first: &[T; N],
- second: &[T; M],
-) -> [T; N + M] {
- // ...
-}
-\end{lstlisting}
+\begin{listing}[H]
+ \begin{minted}{rust}
+ fn concat<T, const N: usize, const M: usize>(
+ first: &[T; N],
+ second: &[T; M],
+ ) -> [T; N + M] {
+ // ...
+ }
+ \end{minted}
+ \caption{Concatenate two arrays, with a deprendent output type}
+ \label{lst:concat-refined}
+\end{listing}
\noindent Here, the type of the return value depends on the generic values of the inputs. This, again, only works if \inline{N} and \inline{M} are known at compile time.
diff --git a/thesis/1-introduction.tex b/thesis/1-introduction.tex
index 952072f..b02b29d 100644
--- a/thesis/1-introduction.tex
+++ b/thesis/1-introduction.tex
@@ -99,7 +99,7 @@ In this section, we will focus on two related approaches of specifying contracts
\todo[inline]{Intermediate Representations and MIR}
\todo[inline]{Flow-sensitive typing; for example: \inline{extract: \{x: Option<T> | x.is_some()\} -> T} or the \inline{?} operator using extract if possible}
-\begin{lstlisting}[language=Rust]
+\begin{verbatim}
// Note that the return type is `()`
fn do_stuff_if_some<T : Debug>(x : Option<T>) {
if x.is_none() {
@@ -107,6 +107,6 @@ fn do_stuff_if_some<T : Debug>(x : Option<T>) {
}
println!("{:?}", x?); // Infallible at this point
}
-\end{lstlisting}
+\end{verbatim}
\end{document}
\ No newline at end of file
--
GitLab