mirror of
https://github.com/thufschmitt/tix-papers.git
synced 2024-08-16 16:20:47 +03:00
[WIP] Refactor everything into one big document
This commit is contained in:
regnat
parent
241bdd5e17
commit
d25edab8f9
33
combined/main.tex
Normal file
33
combined/main.tex
Normal file
@ -0,0 +1,33 @@
|
||||
\input{common/header.tex}
|
||||
|
||||
\title{A type system for nix}
|
||||
|
||||
\begin{document}
|
||||
\maketitle
|
||||
|
||||
In order to lighten the type system, we will not work on the full nix language
|
||||
(presented in section~\ref{sec:nix-grammar}), but on a simplified version
|
||||
called nix-light (roughly a subset of the original one) that we also presents
|
||||
in this document.
|
||||
|
||||
We also present a compilation from nix to nix-light.
|
||||
|
||||
\section{grammar}
|
||||
\input{grammar/grammar}
|
||||
|
||||
\section{semantics}
|
||||
|
||||
\subsection{nix-light semantics}
|
||||
\input{semantics/semantics}
|
||||
|
||||
\subsection{From nix to nix-light}
|
||||
|
||||
\todo{Write the semantic of the compilation}
|
||||
|
||||
\section{typing}
|
||||
|
||||
\todo{Finish and include the typing rules}
|
||||
|
||||
\todos{}
|
||||
|
||||
\end{document}
|
||||
@ -86,3 +86,5 @@
|
||||
\newcommand{\σ}{\sigma}
|
||||
\newcommand{\recleq}{\sqsubsetleq}
|
||||
\newcommand{\discrete}[2]{\left\{ #1, \ldots{}, #2 \right\}}
|
||||
|
||||
\newcommand{\pref}[1]{\ref{#1} at page~\pageref{#1}}
|
||||
|
||||
36
grammar/expressions.tex
Normal file
36
grammar/expressions.tex
Normal file
@ -0,0 +1,36 @@
|
||||
\begin{grammar}
|
||||
\bfseries
|
||||
<e> ::=
|
||||
\x/ \| \c/
|
||||
\alt \e/.\a/ \| \e/.\a/ or \e/
|
||||
\alt \p/:\e/ \| \e/ \e/
|
||||
\alt \{ \e/ = \e/; \}
|
||||
\alt with \e/; \e/
|
||||
\alt (\e/ $\bm{\in}$ \t/) ? \e/ : \e/
|
||||
\alt let \x/ = \e/; $\cdots{}$; \x/ = \e/; in \e/
|
||||
\alt \o/
|
||||
|
||||
<o> ::= attrNames(\e/) \| listToAttrs(\e/)
|
||||
\alt \e/ + \e/ \| \e/ $\orthplus$ \e/ \| \e/ \textbackslash \e/
|
||||
\alt deepSeq(\e/, \e/) \| seq(\e/, \e/)
|
||||
\alt functionArgs(\e/)
|
||||
% Maybe this can be typed as a function, but it is rather unlikely
|
||||
\alt Cons(\e/, \e/)
|
||||
|
||||
<a> ::= \b/. $\cdots{}$ .\b/
|
||||
|
||||
<b> ::= \$\{\e/\} \| \meta{l}
|
||||
|
||||
<c> ::= \meta{s} \| \meta{i} \| $\cdots{}$
|
||||
\alt nil
|
||||
\alt $\cdots{}$
|
||||
|
||||
<p> ::= \q/ \| \q/@\x/ \| \x/
|
||||
|
||||
<q> ::= \{ \f/, $\cdots{}$, \f/ \} \| \{ \f/, $\cdots{}$, \f/ , \ldots{}\}
|
||||
\alt Cons(\x/, \x/) \| nil
|
||||
\alt \c/
|
||||
|
||||
<f> ::= \x/ \| \x/ ? \e/
|
||||
|
||||
\end{grammar}
|
||||
@ -1,61 +1,26 @@
|
||||
\input{common/header}
|
||||
\subsection{Nix grammar}
|
||||
\label{sec:nix-grammar}
|
||||
|
||||
\title{Nix simplified grammar}
|
||||
\begin{document}
|
||||
\todo{Write the nix grammar}
|
||||
|
||||
\maketitle{}
|
||||
\subsection{nix-light}
|
||||
\label{sec:nix-light-grammar}
|
||||
|
||||
\section{expressions}
|
||||
The grammar of nix-light is given in the
|
||||
figures~\pref{grammar::expressions},~\pref{grammar::values}
|
||||
and~\pref{grammar::types}.
|
||||
|
||||
\begin{grammar}
|
||||
\bfseries
|
||||
<e> ::=
|
||||
\x/ \| \c/
|
||||
\alt \e/.\a/ \| \e/.\a/ or \e/
|
||||
\alt \p/:\e/ \| \e/ \e/
|
||||
\alt \{ \e/ = \e/; \}
|
||||
\alt with \e/; \e/
|
||||
\alt (\e/ $\bm{\in}$ \t/) ? \e/ : \e/
|
||||
\alt let \x/ = \e/; $\cdots{}$; \x/ = \e/; in \e/
|
||||
\alt \o/
|
||||
\begin{figure}[h]
|
||||
\input{grammar/expressions}
|
||||
\caption{\label{grammar::expressions}The nix-light grammar for expressions}
|
||||
\end{figure}
|
||||
|
||||
<o> ::= attrNames(\e/) \| listToAttrs(\e/)
|
||||
\alt \e/ + \e/ \| \e/ $\orthplus$ \e/ \| \e/ \textbackslash \e/
|
||||
\alt deepSeq(\e/, \e/) \| seq(\e/, \e/)
|
||||
\alt functionArgs(\e/)
|
||||
% Maybe this can be typed as a function, but it is rather unlikely
|
||||
\alt Cons(\e/, \e/)
|
||||
\begin{figure}[h]
|
||||
\input{grammar/values}
|
||||
\caption{\label{grammar::values}The nix-light grammar for values}
|
||||
\end{figure}
|
||||
|
||||
<a> ::= \b/. $\cdots{}$ .\b/
|
||||
|
||||
<b> ::= \$\{\e/\} \| \meta{l}
|
||||
|
||||
<c> ::= \meta{s} \| \meta{i} \| $\cdots{}$
|
||||
\alt nil
|
||||
\alt $\cdots{}$
|
||||
|
||||
<p> ::= \q/ \| \q/@\x/ \| \x/
|
||||
|
||||
<q> ::= \{ \f/, $\cdots{}$, \f/ \} \| \{ \f/, $\cdots{}$, \f/ , \ldots{}\}
|
||||
\alt Cons(\x/, \x/) \| nil
|
||||
\alt \c/
|
||||
|
||||
<f> ::= \x/ \| \x/ ? \e/
|
||||
|
||||
\end{grammar}
|
||||
|
||||
The grammar for types (\t/) is given in the \texttt{type-system} document.
|
||||
|
||||
|
||||
\section{values}
|
||||
|
||||
\begin{grammar}
|
||||
\bfseries
|
||||
|
||||
<v> ::=
|
||||
\c/
|
||||
\alt \p/:\e/
|
||||
\alt \{ \v/ = \e/; \} $\orthplus \cdots{} \orthplus$ \{ \v/ = \e/; \}
|
||||
\alt Cons(\e/, \e/) \| nil
|
||||
\end{grammar}
|
||||
\end{document}
|
||||
\begin{figure}[h]
|
||||
\input{grammar/types}
|
||||
\caption{\label{grammar::types}The nix-light grammar for types}
|
||||
\end{figure}
|
||||
|
||||
19
grammar/types.tex
Normal file
19
grammar/types.tex
Normal file
@ -0,0 +1,19 @@
|
||||
\begin{grammar}
|
||||
\bfseries
|
||||
<t> ::= \c/ \| \t/ $\bm{\rightarrow}$ \t/
|
||||
\alt \t/ $\bm{\vee}$ \t/ \| \t/ $\bm{\wedge}$ \t/ \| \t/ $\bm{\backslash}$ \t/
|
||||
\alt [\meta{R}]
|
||||
\alt \{ \s/ = \u/; \ldots{}; \s/ = \u/; _ = \u/ \}
|
||||
|
||||
<u> ::= \t/ \| ?\t/
|
||||
|
||||
<R> ::= \t/ \| \meta{R^{\bm{+}}} \| \meta{R}?
|
||||
\| \meta{R} $\bm{\vee}$ \meta{R} \| \meta{R} $\bm{\wedge}$ \meta{R}
|
||||
|
||||
<\τ> ::= \t/ % No polymorphism for now
|
||||
\end{grammar}
|
||||
|
||||
We write \textbf{\{ \s/ = \u/; \ldots{}; \s/ = \u/; \}} as syntactic
|
||||
sugar for \textbf{\{ \s/ = \u/; \ldots{}; \s/ = \u/; _ = $\undef$ \}}, and
|
||||
\textbf{\{ \s/ = \u/; \ldots{}; \s/ = \u/; .. \}} as syntactic sugar for
|
||||
\textbf{\{ \s/ = \u/; \ldots{}; \s/ = \u/; _ = \textmd{\emph{Any}} \}})
|
||||
9
grammar/values.tex
Normal file
9
grammar/values.tex
Normal file
@ -0,0 +1,9 @@
|
||||
\begin{grammar}
|
||||
\bfseries
|
||||
|
||||
<v> ::=
|
||||
\c/
|
||||
\alt \p/:\e/
|
||||
\alt \{ \v/ = \e/; \} $\orthplus \cdots{} \orthplus$ \{ \v/ = \e/; \}
|
||||
\alt Cons(\e/, \e/) \| nil
|
||||
\end{grammar}
|
||||
@ -1,66 +1,66 @@
|
||||
\input{common/header}
|
||||
The reduction rules are presented in figure~\pref{fig:semantics:nix-light} and
|
||||
the evaluation contexts in
|
||||
figure~\pref{fig:semantics:nix-light:reduction-contexts}.
|
||||
|
||||
\title{Nix simplified semantics}
|
||||
The rules for the pattern-matching are in
|
||||
figure~\pref{fig:semantics:nix-light:patterns}
|
||||
|
||||
\begin{document}
|
||||
|
||||
\maketitle{}
|
||||
|
||||
\section{Reduction rules}
|
||||
|
||||
\begin{tabular}{rl}
|
||||
\dstepa{v.s}{e}{if $\vdash v : \{ e : \lnot\undef; .. \}$ and v(s) = e}
|
||||
\dstepa{v.s or e'}{e}{if $\vdash v : \{ e : \lnot\undef; .. \}$ and v(s) = e}
|
||||
\dstepa{v.s or e'}{e'}{if $\vdash v : \lnot\{ e : \lnot\undef; .. \}$}
|
||||
\dstepa{(x:e1) e2}{\substp{x}{e2}{e1}}{}
|
||||
\dstepa{(p:e1) v} {\substp{p}{v} {e1}}{}
|
||||
\dstepa{with v; e}{
|
||||
e[\assign{\xone}{\eone}; ...; \assign{\xn}{\en}]
|
||||
}{
|
||||
\parbox[t]{10cm}{
|
||||
if $\vdash v : \{ \xone : \lnot\undef; .. ; \xn : \not\undef; \}$ \\
|
||||
\begin{figure}
|
||||
\begin{tabular}{rl}
|
||||
\dstepa{v.s}{e}{if $\vdash v : \{ e : \lnot\undef; .. \}$ and v(s) = e}
|
||||
\dstepa{v.s or e'}{e}{if $\vdash v : \{ e : \lnot\undef; .. \}$ and v(s) = e}
|
||||
\dstepa{v.s or e'}{e'}{if $\vdash v : \lnot\{ e : \lnot\undef; .. \}$}
|
||||
\dstepa{(x:e1) e2}{\substp{x}{e2}{e1}}{}
|
||||
\dstepa{(p:e1) v} {\substp{p}{v} {e1}}{}
|
||||
\dstepa{with v; e}{
|
||||
e[\assign{\xone}{\eone}; ...; \assign{\xn}{\en}]
|
||||
}{
|
||||
\parbox[t]{10cm}{
|
||||
if $\vdash v : \{ \xone : \lnot\undef; .. ; \xn : \not\undef; \}$ \\
|
||||
and $\forall i \in \discrete{1}{n}, v(x_i) = e_i$
|
||||
}
|
||||
}
|
||||
\dstepa{raise e}{$\bot$}{}
|
||||
\dstepa{($v \in \τ$ ? \eone : $e_2$)}{\eone}{if $\vdash v : \τ$}
|
||||
\dstepa{($v \in \τ$ ? \eone : $e_2$)}{$e_2$}{if $\vdash v : \lnot\τ$}
|
||||
\dstepa{let $x$ = $e$; in $e'$}{%
|
||||
\subst{x}{\text{let $x$ = $e$; in $x$}}{$e'$}
|
||||
}{}
|
||||
\dstepa{let \xone = \eone; ...; \xn = \en; in e}{%
|
||||
\parbox[t]{10cm}{%
|
||||
(let $r$ = \{ $x'_1$ = \eone; \} $\orthplus \cdots \orthplus$ \{ $x'_n$ = \en \}; in e)
|
||||
\dstepa{raise e}{$\bot$}{}
|
||||
\dstepa{($v \in \τ$ ? \eone : $e_2$)}{\eone}{if $\vdash v : \τ$}
|
||||
\dstepa{($v \in \τ$ ? \eone : $e_2$)}{$e_2$}{if $\vdash v : \lnot\τ$}
|
||||
\dstepa{let $x$ = $e$; in $e'$}{%
|
||||
\subst{x}{\text{let $x$ = $e$; in $x$}}{$e'$}
|
||||
}{}
|
||||
\dstepa{let \xone = \eone; ...; \xn = \en; in e}{%
|
||||
\parbox[t]{10cm}{%
|
||||
(let $r$ = \{ $x'_1$ = \eone; \} $\orthplus \cdots \orthplus$ \{ $x'_n$ = \en \}; in e)
|
||||
[ \\ \assign{\xone}{r.x'_1}; \ldots{}; \assign{\xn}{r.x'_n} \\ ]
|
||||
}
|
||||
}{}
|
||||
\end{tabular}
|
||||
}{}
|
||||
\end{tabular}
|
||||
\caption{Nix-light reduction rules\label{fig:semantics:nix-light}}
|
||||
\end{figure}
|
||||
|
||||
\section{Pattern matching}
|
||||
\begin{figure}
|
||||
% TODO Rewrite in a clear way. Exlpain the fact that we can reordonate stuff because we got a
|
||||
% commutative monoid.
|
||||
|
||||
\begin{tabular}{rl}
|
||||
\eqdefa{\assignp{q@x}{e}}{\assign{x}{e}; \assignp{q}{e}}{}
|
||||
\eqdefa{\assignp{(\{ x \} \orthplus q)}{(\{ x = e; \} \orthplus v)}}{\assignp{x}{e}; \assignp{q}{v}}{}
|
||||
\eqdefa{\assignp{(\{ x ? e' \} \orthplus q)}{(\{ x = e; \} \orthplus v)}}{\assignp{x}{e}; \assignp{q}{v}}{}
|
||||
\eqdefa{\assignp{(\{ x ? e \} \orthplus q)}{(v_1 \orthplus v_2)}}{\assignp{x}{e}; \assignp{q}{\left( v_1 \orthplus v_2\right)}}{if $v_1 \neq \{ x = e'; \}$}
|
||||
\eqdefa{\assignp{\{\}}{\{ \}}}{ø}{}
|
||||
\eqdefa{\assignp{\{ .. \}}{v}}{ø}{}
|
||||
\eqdefa{\assignp{Cons(x, x')}{Cons(e, e')}}{\assign{x}{e}; \assign{x'}{e'}}{}
|
||||
\end{tabular}
|
||||
\begin{tabular}{rl}
|
||||
\eqdefa{\assignp{q@x}{e}}{\assign{x}{e}; \assignp{q}{e}}{}
|
||||
\eqdefa{\assignp{(\{ x \} \orthplus q)}{(\{ x = e; \} \orthplus v)}}{\assignp{x}{e}; \assignp{q}{v}}{}
|
||||
\eqdefa{\assignp{(\{ x ? e' \} \orthplus q)}{(\{ x = e; \} \orthplus v)}}{\assignp{x}{e}; \assignp{q}{v}}{}
|
||||
\eqdefa{\assignp{(\{ x ? e \} \orthplus q)}{(v_1 \orthplus v_2)}}{\assignp{x}{e}; \assignp{q}{\left( v_1 \orthplus v_2\right)}}{if $v_1 \neq \{ x = e'; \}$}
|
||||
\eqdefa{\assignp{\{\}}{\{ \}}}{ø}{}
|
||||
\eqdefa{\assignp{\{ .. \}}{v}}{ø}{}
|
||||
\eqdefa{\assignp{Cons(x, x')}{Cons(e, e')}}{\assign{x}{e}; \assign{x'}{e'}}{}
|
||||
\end{tabular}
|
||||
\caption{Semantic of the pattern-matching in nix-light\label{fig:semantics:nix-light:patterns}}
|
||||
\end{figure}
|
||||
|
||||
\section{Reduction contexts}
|
||||
|
||||
\begin{grammar}
|
||||
\bfseries
|
||||
<E> ::= [] \| \meta{E e}
|
||||
\alt \meta{E.w} \| \meta{E.w} or \meta{e} \| \meta{v.F} \| \meta{v.F} or \meta{e}
|
||||
\alt \{ \x/ = \e/; \ldots{}; \x/ = \e/; \E/ = \e/; \ldots{}; \e/ = \e/ \}
|
||||
\alt with \E/; \e/ | if \E/ then \e/ else \e/
|
||||
|
||||
<F> ::= \E/.\a/ \| \v/.\meta{F}
|
||||
\end{grammar}
|
||||
|
||||
\end{document}
|
||||
\begin{figure}
|
||||
\begin{grammar}
|
||||
\bfseries
|
||||
<E> ::= [] \| \meta{E e}
|
||||
\alt \meta{E.w} \| \meta{E.w} or \meta{e} \| \meta{v.F} \| \meta{v.F} or \meta{e}
|
||||
\alt \{ \x/ = \e/; \ldots{}; \x/ = \e/; \E/ = \e/; \ldots{}; \e/ = \e/ \}
|
||||
\alt with \E/; \e/ | if \E/ then \e/ else \e/
|
||||
|
||||
<F> ::= \E/.\a/ \| \v/.\meta{F}
|
||||
\end{grammar}
|
||||
\caption{Reduction contexts for nix-light\label{fig:semantics:nix-light:reduction-contexts}}
|
||||
\end{figure}
|
||||
|
||||
@ -7,25 +7,8 @@
|
||||
\maketitle{}
|
||||
|
||||
\section{Types}
|
||||
\begin{grammar}
|
||||
\bfseries
|
||||
<t> ::= \c/ \| \t/ $\bm{\rightarrow}$ \t/
|
||||
\alt \t/ $\bm{\vee}$ \t/ \| \t/ $\bm{\wedge}$ \t/ \| \t/ $\bm{\backslash}$ \t/
|
||||
\alt [\meta{R}]
|
||||
\alt \{ \s/ = \u/; \ldots{}; \s/ = \u/; _ = \u/ \}
|
||||
|
||||
<u> ::= \t/ \| ?\t/
|
||||
|
||||
<R> ::= \t/ \| \meta{R^{\bm{+}}} \| \meta{R}?
|
||||
\| \meta{R} $\bm{\vee}$ \meta{R} \| \meta{R} $\bm{\wedge}$ \meta{R}
|
||||
|
||||
<\τ> ::= \t/ % No polymorphism for now
|
||||
\end{grammar}
|
||||
|
||||
\textbf{\{ \s/ = \u/; \ldots{}; \s/ = \u/; \}} (\emph{resp}. \textbf{\{ \s/ =
|
||||
\u/; \ldots{}; \s/ = \u/; .. \}}) is syntactic sugar for \textbf{\{ \s/ = \u/;
|
||||
\ldots{}; \s/ = \u/; _ = $\undef$ \}} (\emph{resp}. \textbf{\{ \s/ = \u/;
|
||||
\ldots{}; \s/ = \u/; _ = \textmd{\emph{Any}} \}})
|
||||
\include{grammar/types}
|
||||
|
||||
\section{Typing rules}
|
||||
\subsection{$\lambda\&$-calculus}
|
||||
|
||||
Loading…
Reference in New Issue
Block a user