Commit 2f394a80 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

let rules (wip, not yet functionnal)

parent 7f9f5dff
......@@ -119,11 +119,6 @@ TODO: Theorems and proof: no need for rule Inter, etc.
{\Gamma \vdash_\ct e : \{(\Empty,\Gamma)\}}
{ }
\qquad
% \Infer[Backtrack]
% {\Gamma \vdash_e e : \bt\{t_i,\Gamma_i\}_{i\in I}}
% {\Gamma \vdash_e e : \{(t_i,\Gamma_i)\}_{i\in I}}
% { }
% \\
\Infer[Const]
{ }
{\Gamma\vdash_\ct c: \{(\basic{c},\Gamma)\}}
......@@ -240,23 +235,27 @@ rules, because one branch is already unreachable and retyping only occurs with s
% {\Gamma\vdash\lambda x:s.e: t}
% { }
% \\
% \Infer[Let]
% {\Gamma\vdash_e a:\{(t_i,\Gamma_i)\}_{i\in I}\\
% x\not\in\dom\Gamma \text{ or } \forall i.\ t_i\leq\Gamma(x)\\
% \forall i\in I.\ \Gamma_i,(x:t_i)\vdash_e e' : \{(u_j,\Gamma_j)\}_{j\in J_i}}
% {
% \Gamma\vdash_e\letexp x a e' : \{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\}
% }
% { }
% \\
% \Infer[LetRefine]
% {\Gamma\vdash_e a:\{(t_i,\Gamma_i)\}_{i\in I}\\
% \Gamma\bvdash{a}{\Gamma(x)}\{(t_j,\Gamma_j)\}_{j\in J}\\
% \forall j\in J.\ \Gamma_j,(x:t_j)\vdash_e e : \{(u_k,\Gamma_k)\}_{k\in K_j}}
% {
% \Gamma\vdash_e\letexp x a e' : \bt\{(u_k,\Gamma_k)\,\alt\,j\in J,\ k\in K_j\}
% }
% { }
\Infer[Let]
{\Gamma\vdash_\ct a:\{(t_i,\Gamma_i)\}_{i\in I}\\
x\not\in\dom\Gamma \text{ or } \forall i.\ t_i\leq\Gamma(x)\\
\forall i\in I.\ \Gamma_i,(x:t_i)\vdash_{\ct[\letexp x a {[]}]} e : \{(u_j,\Gamma_j)\}_{j\in J_i}}
{
\Gamma\vdash_\ct\letexp x a e : \{(u_j,\Gamma_j)\,\alt\,i\in I,\ j\in J_i\}
}
{ }
\\
\Infer[LetRefine]
{\Gamma\vdash_\ct a:\{(t_i,\Gamma_i)\}_{i\in I}\\
\forall i\in I.\ \Gamma_i\bvdash{a}{\Gamma(x)}\{(t_j,\Gamma_j)\}_{j\in J_i}\\
\forall i\in I.\ \forall j\in J_i.\ \Gamma_j,(x:t_j)\vdash_{[]} \ct[\letexp x a e] : \{(u_k,\Gamma_k)\}_{k\in K_j}}
{
\Gamma\vdash_\ct\letexp x a e : \{(u_k,\Gamma_k)\,\alt\,i\in I,\ j\in J_i,\ k\in K_j\}
}
{ }
\end{mathpar}
TODO: Abs and Let rules
TODO: Let rules: not well-founded: we have to store only
hypotheses in the left-hand-side Gamma, and "wanted" types in
another Gamma (underscript?)
TODO: Abs rules
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