Commit 1b2a70f6 by Mickael Laurent

### update refining2

parent e7742460
 ... ... @@ -64,7 +64,7 @@ improves these two points. {e\text{ a variable or constant}} \hfill \Infer[Abs] {\Gamma,y:s\vdash e\triangleright_x\psi} {\Gamma,(y:s)\vdash e\triangleright_x\psi} { \Gamma\vdash\lambda y:s.e\triangleright_x\psi } ... ... @@ -120,8 +120,9 @@ improves these two points. % \vspace{-2.3mm}\\ \Infer[OverLet] { \Gamma \vdash e_2\triangleright_x\psi_x\\ \Gamma \vdash e_2\triangleright_y\psi_y\\ \Gamma \vdash e_1: t\\ \Gamma, (y:t) \vdash e_2\triangleright_x\psi_x\\ \Gamma, (y:t) \vdash e_2\triangleright_y\psi_y\\ \forall u\in \psi_y.\ \Gamma\evdash{e_1}{u}\{\Gamma_u^i\}_{i\in I_u} } { \Gamma \vdash\textstyle ... ... @@ -150,14 +151,26 @@ improves these two points. } \end{array}\] Typing rule for the LET: \begin{mathpar} \Infer[Let] { \Gamma \vdash e_1: t_1\\ \Gamma,y:t_1\vdash e_2\triangleright_y \psi\\ \psi' = \psi\cup\{t_1\setminus(\bigvee_{u\in\psi}u)\}\\ \forall u\in\psi'.\ \Gamma\evdash{e_1}{u}\{\Gamma_u^i\}_{i\in I_u}\\ \forall u\in\psi'.\ \forall i\in I_u.\ \Gamma_u^i, (y:u)\vdash e_2:t } { \Gamma \vdash\textstyle \texttt{let }y\texttt{\,=\,}e_1\texttt{\,in\,}e_2:t} {} \vspace{-1.4mm} \end{mathpar} TODO: $\triangleright$ should return a set of environments (mapping variables only) instead of a set of types for a given variable? TODO: typing rule for the let. If we want full control flow, it should compute $e_2 \triangleright_y \psi$ and, for all $t$ in $\psi$, type $e_2$ under the hypothesis that $e_1$ has type $t$ (and, finally, under the hypothesis that $e_1$ has type $\tyof{e_1}{\Gamma}\setminus\bigcup_{t\in\psi}t$). TODO: The $\evdash e t$ operator is used in the Case, OverApp and OverLet rules, but what we would actually need is an operator that computes the other direction: which environments can surely lead to $e$ having the type $t$? ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!