From ef5b2c837dc859a7f790f38e259cb85f577bbbbc Mon Sep 17 00:00:00 2001
From: regnat <rg@regnat.ovh>
Date: Mon, 24 Apr 2017 17:08:51 +0200
Subject: [PATCH] Add variable substitution in typecases

This allows to explicit how to do occurence typing

Fixes #6
---
 grammar/expressions.tex | 2 +-
 semantics/semantics.tex | 4 ++--
 typing/type-system.tex  | 9 +++------
 3 files changed, 6 insertions(+), 9 deletions(-)

diff --git a/grammar/expressions.tex b/grammar/expressions.tex
index 42a271a..b0d4c29 100644
--- a/grammar/expressions.tex
+++ b/grammar/expressions.tex
@@ -6,7 +6,7 @@
     \alt \p/:\e/ \| \e/ \e/
     \alt \{ \e/ = \e/ \}
     \alt with \e/; \e/
-    \alt (\e/ $\bm{\in}$ \t/) ? \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 \o/
diff --git a/semantics/semantics.tex b/semantics/semantics.tex
index 10e0d5f..ef27f03 100644
--- a/semantics/semantics.tex
+++ b/semantics/semantics.tex
@@ -16,8 +16,8 @@ figure~\pref{fig:semantics:nix-light:patterns}
       \e/[\assign{l_1}{\eone}; ...; \assign{l_n}{\en}]
     }{}
     \dstepa{raise \e/}{$\bot$}{}
-    \dstepa{($v \in \τ$ ? \eone : $e_2$)}{\eone}{if $\vdash v : \τ$}
-    \dstepa{($v \in \τ$ ? \eone : $e_2$)}{$e_2$}{if $\vdash v : \lnot\τ$}
+    \dstepa{($x := v \in \τ$ ? \eone : $e_2$)}{\subst{x}{v}{\eone}}{if $\vdash v : \τ$}
+    \dstepa{($x := v \in \τ$ ? \eone : $e_2$)}{\subst{x}{v}{$e_2$}}{if $\vdash v : \lnot\τ$}
     \dstepa{let \xone = \eone; $\cdots{}$; \xn = \en; in \e/}{%
       \e/[\assign{x_1}{\eone}; ...; \assign{x_n}{\en}]
     }{}
diff --git a/typing/type-system.tex b/typing/type-system.tex
index b625cf2..3b466b0 100644
--- a/typing/type-system.tex
+++ b/typing/type-system.tex
@@ -28,13 +28,10 @@
   \and
   \inferrule{%
     \Gamma \vdash e : \tau \\
-    % TODO: fix display of cases here
-    \begin{cases}
-      \tau \not\subtype \lnot t \Rightarrow \Gamma \vdash e_1 : \sigma_1 &
-      \tau \not\subtype t \Rightarrow \Gamma \vdash e_2 : \sigma_2
-    \end{cases}
+      \Γ; x : \τ \wedge t \vdash e_1 : \sigma_1 \\
+      \Γ; x : \τ \wedge \lnot t \vdash e_2 : \sigma_2
   }{%
-    \Gamma \vdash ((e \in t) ? e_1 : e_2) : \sigma_1 \vee \sigma_2
+    \Gamma \vdash ((x := e \in t) ? e_1 : e_2) : \sigma_1 \vee \sigma_2
   }
   (Tcase)