Commit f3017d62 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

add an appendix for the new system

parent b916f997
......@@ -345,4 +345,9 @@ The authors thank Paul-André Melliès for his help on type ranking.
\section{New function refinement rules}
\input{refining2}
\newpage
\section{Full new system with normal form}
\input{new_system}
\end{document}
\subsection{Syntax}
\[
\begin{array}{lrcl}
\textbf{Types} & t & ::= & b\alt t\to t\alt t\times t\alt t\vee t \alt \neg t \alt \Empty
\end{array}
\]
\begin{equation}\label{expressions2}
\begin{array}{lrclr}
\textbf{Atomic Expr} &a &::=& c\alt x\alt\lambda x:t.e\alt (a,a)\\[.3mm]
\textbf{U-Expr} &u &::=& a a\alt \tcase{x}{t}{e}{e}\alt \pi_i a\\[.3mm]
\textbf{P-Expr} &p &::=& u\alt a\\[.3mm]
\textbf{Expressions} &e &::=& \letexp{x}{p}{e}\alt p \\[.3mm]
\textbf{Values} &v &::=& c\alt\lambda x:t.e\alt (v,v)\\
\end{array}
\end{equation}
TODO: Which restrictions on types? (cannot test a precise arrow type, etc)
\subsection{Typing rules}
\subsection{Candidates generation rules}
\subsection{Forward refinement rules}
\subsection{Backward refinement rules}
......@@ -179,4 +179,7 @@ which environments can surely lead to $e$ having the type $t$?
TODO: Should we totally remove the Abs- rule and the type schemes from the paper
(and from the proof) and restricts the arrow type tests accordingly?
It would simplify a lot, it would match the implementation,
and we wouldn't have to bother with weird completeness results.
\ No newline at end of file
and we wouldn't have to bother with weird completeness results.
TODO: With control flow, we can get rid of occurences in the environment if we
work with a normal form.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment