trying some new rules... (wip)

new_system2.tex

@@ -9,16 +9,13 @@
 \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{U-Expr} &u &::=& x x\alt \tcase{x}{t}{e}{e}\alt \pi_i x\\[.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: Only allow variables and both sides of a application / projection? It would simplify
-rules...
-
 TODO: the then and else expressions of typecases have no associated variable,
 altough the env refinement rules could refine their types...
 Is this an issue? Should we require an atomic in the then and else branchs
@@ -55,8 +52,8 @@ TODO: Which restrictions on types? (cannot test a precise arrow type, etc)
 { }
 \qquad
 \Infer[Proj]
-{\Gamma \vdash a:\pair{t_1}{t_2}}
-{\Gamma \vdash \pi_i a:t_i}
+{\Gamma \vdash x:\pair{t_1}{t_2}}
+{\Gamma \vdash \pi_i x:t_i}
 { }
 \qquad
 \Infer[Pair]
@@ -66,19 +63,18 @@ TODO: Which restrictions on types? (cannot test a precise arrow type, etc)
 \\
 \Infer[App]
 {
-  \Gamma \vdash a_1: \arrow {t_1}{t_2}\quad
-  \Gamma \vdash a_2: t_1
+  \Gamma \vdash x_1: \arrow {t_1}{t_2}\quad
+  \Gamma \vdash x_2: t_1
 }
-{ \Gamma \vdash {a_1}{a_2}: t_2 }
+{ \Gamma \vdash {x_1}{x_2}: t_2 }
 { }
 \\
 \Infer[Case]
 {
-x\in\dom\Gamma\\  
 \Gamma\subst{x}{\Gamma(x)\land t} \vdash e_1:t'\\
 \Gamma\subst{x}{\Gamma(x)\land \neg t} \vdash e_2:t'}
 {\Gamma\vdash \tcase {x} t {e_1}{e_2}: t'}
-{ }
+{ x\in\dom\Gamma }
 \\
 \Infer[AbsBase]
   {
@@ -135,21 +131,21 @@ x\in\dom\Gamma\\
 \end{mathpar}
 
 \begin{mathpar}
-\Infer[Proj]
+\Infer[ProjC]
 {\Gamma \vdash x:\textstyle\bigcup_{j\in J}\pair{t_1^j}{t_2^j}}
 {\Gamma \cvdash \pi_i x: \{(t_i^j, \Gamma\subst{x}{\pair{t_1^j}{t_2^j}})\ \alt\ j\in J\}}
 { }
 \\
-\Infer[App]
+\Infer[AppC]
 {
   \Gamma \vdash x: \textstyle\bigcup_{i\in I}t_i\quad
   \forall i\in I.\ t_i\leq \arrow{t}{s_i}\quad
-  \Gamma \vdash a: t
+  \Gamma \vdash y: t
 }
-{ \Gamma \cvdash {x}{a}: \{(s_i, \Gamma\subst{x}{t_i})\ \alt\ i\in I\} }
+{ \Gamma \cvdash {x}{y}: \{(s_i, \Gamma\subst{x}{t_i})\ \alt\ i\in I\} }
 { }
 \\
-\Infer[Case]
+\Infer[CaseC]
 {
 \Gamma_1 = \Gamma\subst{x}{\Gamma(x)\land t}\\
 \Gamma_2 = \Gamma\subst{x}{\Gamma(x)\land \neg t}\\
@@ -158,9 +154,9 @@ x\in\dom\Gamma\\
 {\Gamma\cvdash \tcase {x} t {e_1}{e_2}: \{(t_1, \Gamma_1), (t_2, \Gamma_2)\}}
 { }
 \\
-\Infer[NoChoice]
-{\Gamma \vdash p:t}
-{\Gamma \cvdash p: \{(t, \Gamma)\}}
+\Infer[AtomicC]
+{\Gamma \vdash a:t}
+{\Gamma \cvdash a: \{(t, \Gamma)\}}
 { }
 \end{mathpar}
 
@@ -168,6 +164,9 @@ TODO: Inter rule needed?
 
 TODO: Algorithmic rules
 
+TODO: AppC rule: what about the argument? We could loose precision there...
+In the end, these rules look quite similar to the candidate generation rules.
+
 \subsection{Candidates generation rules}
 
 \begin{mathpar}
@@ -213,15 +212,15 @@ TODO: Algorithmic rules
           {\Gamma \vdash (a_1,a_2)\triangleright_x \dt}
           {}
   \hfill
-  \Infer[ProjVar]
+  \Infer[ProjX]
           {\Gamma \vdash x:\textstyle{\bigvee_{i \in I}t_i}}
           {\Gamma \vdash \pi_i x\triangleright_x\textstyle{\bigcup_{i\in I} \{t_i\}}}
           {}
   \hfill
    \Infer[Proj]
-          {\Gamma \vdash a\triangleright_x\dt}
-          {\Gamma \vdash \pi_i a\triangleright_x\dt}
-          {}
+          { }
+          {\Gamma \vdash \pi_i y\triangleright_x\{\}}
+          {y\neq x}
   \\        
   \Infer[CaseTest]
         { }
@@ -245,20 +244,19 @@ TODO: Algorithmic rules
   {
     \Gamma \vdash x : \textstyle{\bigvee_{i \in I}t_i}
   }
-  { \Gamma \vdash x a\triangleright_x\textstyle{\bigcup_{i\in I} \{t_i\}}}
+  { \Gamma \vdash x y\triangleright_x\textstyle{\bigcup_{i\in I} \{t_i\}}}
   {}
 \qquad
   \Infer[AppVar2]
       {
-        \Gamma \vdash a : \textstyle{\bigwedge_{i \in I}s_i\to t_i}
+        \Gamma \vdash y : \textstyle{\bigwedge_{i \in I}s_i\to t_i}
       }
-      { \Gamma \vdash a x\triangleright_x\textstyle{\bigcup_{i\in I} \{s_i\}}}
+      { \Gamma \vdash y x\triangleright_x\textstyle{\bigcup_{i\in I} \{s_i\}}}
       {}
 \qquad
   \Infer[App]
-      { i\in\{1,2\}\\
-      \Gamma \vdash a_i\triangleright_x\dt }
-      { \Gamma \vdash a_1 a_2\triangleright_x\dt}
+      { }
+      { \Gamma \vdash y z\triangleright_x\{\}}
       {}
   \\
 \Infer[LetBase]
@@ -294,6 +292,9 @@ TODO: Algorithmic rules
   TODO: Candidates for a variable should be a special "all splits".
   Otherwise, $\letexp{x}{\cdots}{x}$ will never be splitted.
 
+  TODO: Proj: Actually, all the possible types of the first component should be candidates
+  (similar to the Var case)
+
 \subsection{Forward refinement rules}
 
 \subsection{Backward refinement rules}