Skip to content
Snippets Groups Projects
Commit 59fc7cc6 authored by Jasper Clemens Gräflich's avatar Jasper Clemens Gräflich
Browse files

Change the rest of lstlistings to minted

parent 69969e32
No related branches found
No related tags found
No related merge requests found
Pipeline #86584 failed
...@@ -8,10 +8,6 @@ As we have seen, ownership and move semantics ensure memory safety. But they are ...@@ -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. 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{listing}[H]
\begin{minted}{rust} \begin{minted}{rust}
fn print_value(ptr: &Box<i32>) { fn print_value(ptr: &Box<i32>) {
......
...@@ -55,9 +55,6 @@ But why does the code in \autoref{lst:moved-borrow} work? The compiler can inser ...@@ -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. 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{listing}[H]
\begin{minted}{rust} \begin{minted}{rust}
......
...@@ -73,10 +73,14 @@ Since the inception of set theory, mathematicians used \emph{set comprehension} ...@@ -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}. \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}] \begin{listing}[H]
const PRIME: Subtype<i32, is_prime> = Subtype::new(17); \begin{minted}{rust}
const SMALL: Subtype<u32, |x| x <= 255> = Subtype::new(9); const PRIME: Subtype<i32, is_prime> = Subtype::new(17);
\end{lstlisting} 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}. \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); ...@@ -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: 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}] \begin{listing}[H]
fn concat<T, const N: usize, const M: usize>( \begin{minted}{rust}
first: &[T; N], fn concat<T, const N: usize, const M: usize>(
second: &[T; M], first: &[T; N],
) -> [T; N + M] { second: &[T; M],
// ... ) -> [T; N + M] {
} // ...
\end{lstlisting} }
\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. \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.
......
...@@ -99,7 +99,7 @@ In this section, we will focus on two related approaches of specifying contracts ...@@ -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]{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} \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 `()` // Note that the return type is `()`
fn do_stuff_if_some<T : Debug>(x : Option<T>) { fn do_stuff_if_some<T : Debug>(x : Option<T>) {
if x.is_none() { if x.is_none() {
...@@ -107,6 +107,6 @@ fn do_stuff_if_some<T : Debug>(x : Option<T>) { ...@@ -107,6 +107,6 @@ fn do_stuff_if_some<T : Debug>(x : Option<T>) {
} }
println!("{:?}", x?); // Infallible at this point println!("{:?}", x?); // Infallible at this point
} }
\end{lstlisting} \end{verbatim}
\end{document} \end{document}
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment