mirror of
https://github.com/thufschmitt/tix-papers.git
synced 2024-09-11 13:00:34 +03:00
grammar: add typing annotations to patterns
And remove them from lambdas
This commit is contained in:
parent
864957720a
commit
51468d4d15
@ -37,6 +37,7 @@
|
|||||||
\def\o/{\meta{o}}
|
\def\o/{\meta{o}}
|
||||||
\def\p/{\meta{p}}
|
\def\p/{\meta{p}}
|
||||||
\def\q/{\meta{q}}
|
\def\q/{\meta{q}}
|
||||||
|
\def\r/{\meta{r}}
|
||||||
\def\s/{\meta{s}}
|
\def\s/{\meta{s}}
|
||||||
\def\t/{\meta{t}}
|
\def\t/{\meta{t}}
|
||||||
\def\u/{\meta{u}}
|
\def\u/{\meta{u}}
|
||||||
@ -72,6 +73,7 @@
|
|||||||
\newcommand{\quasiconst}[1]{\overset{#1}{\twoheadrightarrow}}
|
\newcommand{\quasiconst}[1]{\overset{#1}{\twoheadrightarrow}}
|
||||||
\DeclareMathOperator\dom{dom}
|
\DeclareMathOperator\dom{dom}
|
||||||
\DeclareMathOperator\deff{def}
|
\DeclareMathOperator\deff{def}
|
||||||
|
\DeclareMathOperator\var{\mathcal{V}}
|
||||||
\newcommand{\orthsum}{\oplus^\bot}
|
\newcommand{\orthsum}{\oplus^\bot}
|
||||||
\newcommand{\orthplus}{\diamond}
|
\newcommand{\orthplus}{\diamond}
|
||||||
\newcommand{\subtype}{\leq}
|
\newcommand{\subtype}{\leq}
|
||||||
|
@ -3,12 +3,12 @@
|
|||||||
<e> ::=
|
<e> ::=
|
||||||
\x/ \| \c/
|
\x/ \| \c/
|
||||||
\alt \e/.\a/ \| \e/.\a/ or \e/
|
\alt \e/.\a/ \| \e/.\a/ or \e/
|
||||||
\alt $\λ$\p/:\τ.\e/ \| \e/ \e/
|
\alt $\λ$\p/.\e/ \| \e/ \e/
|
||||||
\alt \{ \e/ = \e/ \}
|
\alt \{ \e/ = \e/ \}
|
||||||
\alt with \e/; \e/
|
\alt with \e/; \e/
|
||||||
\alt (\x/ := \e/ $\bm{\in}$ \t/) ? \e/ : \e/
|
\alt (\x/ := \e/ $\bm{\in}$ \t/) ? \e/ : \e/
|
||||||
\alt let \x/ = \e/; $\cdots{}$; \x/ = \e/; in \e/
|
\alt let \x/ = \e/; $\cdots{}$; \x/ = \e/; in \e/
|
||||||
\alt let rec \x/:\τ = \e/; $\cdots{}$; \x/:\τ/ = \e/; in \e/
|
\alt let rec \r/ = \e/; $\cdots{}$; \r/ = \e/; in \e/
|
||||||
\alt \o/
|
\alt \o/
|
||||||
|
|
||||||
<o> ::= attrNames(\e/) \| listToAttrs(\e/)
|
<o> ::= attrNames(\e/) \| listToAttrs(\e/)
|
||||||
@ -24,12 +24,14 @@
|
|||||||
\alt nil
|
\alt nil
|
||||||
\alt $\cdots{}$
|
\alt $\cdots{}$
|
||||||
|
|
||||||
<p> ::= \q/ \| \q/@\x/ \| \x/
|
<p> ::= \q/ \| \q/@\x/ \| \r/
|
||||||
|
|
||||||
<q> ::= \{ \f/, $\cdots{}$, \f/ \} \| \{ \f/, $\cdots{}$, \f/ , \ldots{}\}
|
<q> ::= \{ \f/, $\cdots{}$, \f/ \} \| \{ \f/, $\cdots{}$, \f/ , \ldots{}\}
|
||||||
\alt Cons(\x/, \x/) \| nil
|
\alt Cons(\r/, \r/) \| nil
|
||||||
\alt \c/
|
\alt \q/:\τ
|
||||||
|
|
||||||
<f> ::= \x/ \| \x/ ? \c/
|
<r> ::= \x/ | \x/:\τ
|
||||||
|
|
||||||
|
<f> ::= \r/ \| \r/ ? \c/
|
||||||
|
|
||||||
\end{grammar}
|
\end{grammar}
|
||||||
|
@ -36,47 +36,48 @@ figure~\pref{fig:semantics:nix-light:patterns}
|
|||||||
\end{figure}
|
\end{figure}
|
||||||
|
|
||||||
\begin{figure}
|
\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}
|
\begin{tabular}{rl}
|
||||||
|
\eqdefa{$\sfrac{x:t}{e}$}{$\sfrac{x}{e}$}{}
|
||||||
\eqdefa{$\sfrac{x}{e}$}{$\sfrac{x}{e}$}{}
|
\eqdefa{$\sfrac{x}{e}$}{$\sfrac{x}{e}$}{}
|
||||||
\eqdefa{$\sfrac{q@x}{e}$}{$\sfrac{x}{e}; \sfrac{q}{x}$}{}
|
\eqdefa{$\sfrac{q@x}{e}$}{$\sfrac{x}{e}; \sfrac{q}{e}$}{}
|
||||||
\eqdefa{$\sfrac{\{\}}{\{ x_1 ? c_1, \cdots, x_n ? c_n \}}$}{%
|
\eqdefa{$\sfrac{q:t}{e}$}{$\sfrac{q}{e}$}{}
|
||||||
$\sfrac{x_1}{c_1}; \cdots; \sfrac{x_n}{c_n}$}{}
|
\eqdefa{$\sfrac{\{\}}{\{ r_1 ? c_1, \cdots, r_n ? c_n \}}$}{%
|
||||||
|
$\sfrac{r_1}{c_1}; \cdots; \sfrac{r_n}{c_n}$}{}
|
||||||
\eqdefa{%
|
\eqdefa{%
|
||||||
$\sfrac{%
|
$\sfrac{%
|
||||||
\{ s_1 = e_1; \cdots; s_m = e_m; \}%
|
\{ s_1 = e_1; \cdots; s_m = e_m; \}%
|
||||||
}{%
|
}{%
|
||||||
\{x_1 ? c_1, \cdots, x_n ? c_n, \textbf{\ldots}\}%
|
\{r_1 ? c_1, \cdots, r_n ? c_n, \textbf{\ldots}\}%
|
||||||
}$%
|
}$%
|
||||||
}{%
|
}{%
|
||||||
$\sfrac{x_1}{c_1}; \cdots; \sfrac{x_n}{c_n}$%
|
$\sfrac{r_1}{c_1}; \cdots; \sfrac{r_n}{c_n}$%
|
||||||
}{%
|
}{%
|
||||||
if %
|
if %
|
||||||
$\forall (i,j) \in \discrete{1}{m} \times \discrete{1}{n}, s_i \neq s_j$%
|
$\forall (i,j) \in \discrete{1}{m} \times \discrete{1}{n}, s_i \neq \var(r_j)$%
|
||||||
}
|
}
|
||||||
\eqdefa{$\sfrac{\{ s = e;\}}{\{ x \}}$}{$\sfrac{x}{e}$}{if $s = x$}
|
\eqdefa{$\sfrac{\{ s = e;\}}{\{ r \}}$}{$\sfrac{r}{e}$}{if $s = \var(r)$}
|
||||||
\eqdefa{$\sfrac{\{ s = e;\}}{\{ x ? c \}}$}{$\sfrac{x}{e}$}{if $s = x$}
|
\eqdefa{$\sfrac{\{ s = e;\}}{\{ r ? c \}}$}{$\sfrac{r}{e}$}{if $s = \var(r)$}
|
||||||
\eqdefa{$%
|
\eqdefa{$%
|
||||||
\sfrac{\{ s_1 = e_1; \cdots; s_n = e_n \}}{\{ x, f_1, \cdots, f_m \}}%
|
\sfrac{\{ s_1 = e_1; \cdots; s_n = e_n \}}{\{ r, f_1, \cdots, f_m \}}%
|
||||||
$}{$%
|
$}{$%
|
||||||
\sfrac{x}{e};%
|
\sfrac{r}{e};%
|
||||||
\sfrac{\{ s_2 = e_2; \cdots; s_n = e_n \}}{\{ f_1, \cdots, f_m \}}%
|
\sfrac{\{ s_2 = e_2; \cdots; s_n = e_n \}}{\{ f_1, \cdots, f_m \}}%
|
||||||
$}{if $s_1 = x$}
|
$}{if $s_1 = \var(r)$}
|
||||||
\eqdefa{
|
\eqdefa{
|
||||||
$\sfrac{%
|
$\sfrac{%
|
||||||
\{ s_1 = e_1; \cdots; s_n = e_n \}}%
|
\{ s_1 = e_1; \cdots; s_n = e_n \}}%
|
||||||
{\{ x ? c, f_1 \cdots, f_m \}}$%
|
{\{ r ? c, f_1 \cdots, f_m \}}$%
|
||||||
}{%
|
}{%
|
||||||
$\sfrac{x}{e};%
|
$\sfrac{r}{e};%
|
||||||
\sfrac{\{ s_2 = e_2; \cdots; s_n = e_n \}}%
|
\sfrac{\{ s_2 = e_2; \cdots; s_n = e_n \}}%
|
||||||
{\{ f_1, \cdots, f_m \}}$%
|
{\{ f_1, \cdots, f_m \}}$%
|
||||||
}{if $s_1 = x$}
|
}{if $s_1 = \var(r)$}
|
||||||
\eqdefa{%
|
\eqdefa{%
|
||||||
$\sfrac{\text{Cons}(e_1, e_2)}{\text{Cons}(x_1, x_2)}$%
|
$\sfrac{\text{Cons}(e_1, e_2)}{\text{Cons}(r_1, r_2)}$%
|
||||||
}{$\sfrac{x_1}{e_1}; \sfrac{x_2}{e_2}$}{}
|
}{$\sfrac{r_1}{e_1}; \sfrac{r_2}{e_2}$}{}
|
||||||
\end{tabular}
|
\end{tabular}
|
||||||
|
|
||||||
|
Where we define $\var(r)$ as $\var(x) = \var(x:t) = x$
|
||||||
\caption{Semantic of the pattern-matching in nix-light\label{fig:semantics:nix-light:patterns}}
|
\caption{Semantic of the pattern-matching in nix-light\label{fig:semantics:nix-light:patterns}}
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user