thufschmitt/tix-papers
1
1
Fork 0
mirror of https://github.com/thufschmitt/tix-papers.git synced 2024-08-16 16:20:47 +03:00
Code Issues Projects Releases Wiki Activity

Add type annotations for lambdas and let-recs

Browse Source 
Those were already present in the typing rules, they are now added in
the syntax and the semantics

Fixes #5
This commit is contained in:
regnat 2017-04-25 08:53:28 +02:00
parent b4d0e36856
commit 75d164c873
4 changed files with 10 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
common/header.tex
View File

@ -82,7 +82,7 @@
\newcommand{\ofTypeP}[2]{\UseCollection{xfrac}{plainmath}\sfrac{#1}{#2}}
\newcommand{\Γ}{\Gamma}
\newcommand{\τ}{\tau}
\newcommand{\τ}{\ensuremath{\tau}}
\newcommand{\σ}{\sigma}
\newcommand{\λ}{\lambda}
\newcommand{\recleq}{\sqsubsetleq}

4
grammar/expressions.tex
View File

@ -3,12 +3,12 @@
<e> ::=
\x/ \| \c/
\alt \e/.\a/ \| \e/.\a/ or \e/
\alt $\λ$\p/.\e/ \| \e/ \e/
\alt $\λ$\p/:\τ.\e/ \| \e/ \e/
\alt \{ \e/ = \e/ \}
\alt with \e/; \e/
\alt (\x/ := \e/ $\bm{\in}$ \t/) ? \e/ : \e/
\alt let \x/ = \e/; $\cdots{}$; \x/ = \e/; in \e/
\alt let rec \x/ = \e/; $\cdots{}$; \x/ = \e/; in \e/
\alt let rec \x/:\τ = \e/; $\cdots{}$; \x/:\τ/ = \e/; in \e/
\alt \o/
<o> ::= attrNames(\e/) \| listToAttrs(\e/)

2
grammar/values.tex
View File

@ -3,7 +3,7 @@
<v> ::=
\c/
\alt $\λ$\p/.\e/
\alt $\λ$\p/:\τ.\e/
\alt \{ \v/ = \e/ \} $\orthplus \cdots{} \orthplus$ \{ \v/ = \e/ \}
\alt Cons(\e/, \e/) \| nil
\end{grammar}

11
semantics/semantics.tex
View File

@ -10,8 +10,8 @@ figure~\pref{fig:semantics:nix-light:patterns}
\dstepa{\{ \s/ = \e/; $\ldots{}$\}.\s/}{$e$}{}
\dstepa{\{ \s/ = \e/; $\ldots{}$\}.\s/ or $e'$}{$e$}{}
\dstepa{$v.s \text{ or } e'$}{$e'$}{if $\v/ \neq$ \{ \s/ = \e/; $\ldots{}$ \}}
\dstepa{$(\λ x.e_1) e_2$}{$\substp{x}{e_2}{e_1}$}{}
\dstepa{$(\λ p.e_1) v$} {$\substp{p}{v}{e_1}$}{if $p \neq x$}
\dstepa{$(\λ x : \τ .e_1) e_2$}{$\substp{x}{e_2}{e_1}$}{}
\dstepa{$(\λ p : \τ .e_1) v$} {$\substp{p}{v}{e_1}$}{if $p \neq x$}
\dstepa{with \{ $l_1$ = $e_1$; $\cdots{}$; $l_n$ = $e_n$; \} ; \e/}{
\e/[\assign{l_1}{\eone}; ...; \assign{l_n}{\en}]
}{}
@ -21,12 +21,13 @@ figure~\pref{fig:semantics:nix-light:patterns}
\dstepa{let \xone = \eone; $\cdots{}$; \xn = \en; in \e/}{%
\e/[\assign{x_1}{\eone}; ...; \assign{x_n}{\en}]
}{}
\dstepa{let rec $x$ = $e$; in $e'$}{%
\dstepa{let rec $x$ : $\τ$ = $e$; in $e'$}{%
\subst{x}{\text{let $x$ = $e$; in $x$}}{$e'$}
}{}
\dstepa{let rec \xone = \eone; $\cdots{}$; \xn = \en; in \e/}{%
\dstepa{let rec \xone : $\τ_1$ = \eone; $\cdots{}$; \xn : $\τ_n$ = \en; in \e/}{%
\parbox[t]{10cm}{%
(let rec $r$ = \{ $x'_1$ = \eone; \} $\orthplus \cdots \orthplus$ \{ $x'_n$ = \en \}; in e)
(let rec $r$ : \{ $x'_1$ = $\τ_1$; $\cdots$; $x'_n$ = $\τ_n$; \} = \\
\{ $x'_1$ = \eone; $\cdots$; $x'_n$ = \en \}; in e)
[ \\ \assign{\xone}{r.x'_1}; \ldots{}; \assign{\xn}{r.x'_n} \\ ]
}
}{}