From 64d55d73c66ff53bd1ffc6995b0a1f88d28a77ce Mon Sep 17 00:00:00 2001
From: Eric Zhao <21zhaoe@protonmail.com>
Date: Mon, 9 Oct 2023 02:35:20 -0400
Subject: [PATCH] formalism: Fix typed con rules with mode change

---
 formalism/typed.tex | 40 ++++++++++++----------------------------
 1 file changed, 12 insertions(+), 28 deletions(-)

diff --git a/formalism/typed.tex b/formalism/typed.tex
index ab04484..61c57f0 100644
--- a/formalism/typed.tex
+++ b/formalism/typed.tex
@@ -569,8 +569,10 @@ \subsubsection{Synthetic expression actions}
     \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCApL{\ECInconType{\ECMV}}{\ZCCursor{\ECEHole}}}{\TUnknown}{\SApL}
   }
 
-  \inferrule[ASEConApR]{ }{
-    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCApR{\ZCCursor{\ECEHole}}{\ECMV}}{\TUnknown}{\SApR}
+  \inferrule[ASEConApR]{
+    \ctxAnaFixedInto{\ctx}{\ECMV}{\ECMV'}{\TUnknown}
+  }{
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCApR{\ZCCursor{\ECEHole}}{\ECMV'}}{\TUnknown}{\SApR}
   }
 
   \inferrule[ASEConLet1]{ }{
@@ -587,40 +589,22 @@ \subsubsection{Synthetic expression actions}
     \ASCon{\ctx}{\ZCCursor{\ECEHole}}{\TUnknown}{\ZCCursor{\ENumMV}}{\TNum}{\SLit{\ENumMV}}
   }
 
-  \inferrule[ASEConPlusL1]{
-    \consistent{\TMV}{\TNum}
+  \inferrule[ASEConPlusL]{
+    \ctxAnaFixedInto{\ctx}{\ECMV}{\ECMV'}{\TNum}
   }{
-    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPlusR{\ECMV}{\ZCCursor{\ECEHole}}}{\TNum}{\SPlusL}
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPlusR{\ECMV'}{\ZCCursor{\ECEHole}}}{\TNum}{\SPlusL}
   }
 
-  \inferrule[ASEConPlusL2]{
-    \inconsistent{\TMV}{\TNum}
-  }{
-    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPlusR{\ECInconType{\ECMV}}{\ZCCursor{\ECEHole}}}{\TNum}{\SPlusL}
-  } \\
-
-  \inferrule[ASEConPlusR1]{
-    \consistent{\TMV}{\TNum}
+  \inferrule[ASEConPlusR]{
+    \ctxAnaFixedInto{\ctx}{\ECMV}{\ECMV'}{\TNum}
   }{
-    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPlusL{\ZCCursor{\ECEHole}}{\ECMV}}{\TNum}{\SPlusR}
-  }
-
-  \inferrule[ASEConPlusR2]{
-    \inconsistent{\TMV}{\TNum}
-  }{
-    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPlusL{\ZCCursor{\ECEHole}}{\ECInconType{\ECMV}}}{\TNum}{\SPlusR}
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPlusL{\ZCCursor{\ECEHole}}{\ECMV'}}{\TNum}{\SPlusR}
   }
 
   \inferrule[ASEConIfC1]{
-    \consistent{\TMV}{\TBool}
-  }{
-    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCIfL{\ECMV}{\ZCCursor{\ECEHole}}{\ECEHole}}{\TUnknown}{\SIfC}
-  }
-
-  \inferrule[ASEConIfC2]{
-    \inconsistent{\TMV}{\TBool}
+    \ctxAnaFixedInto{\ctx}{\ECMV}{\ECMV'}{\TBool}
   }{
-    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCIfL{\ECInconType{\ECMV}}{\ZCCursor{\ECEHole}}{\ECEHole}}{\TUnknown}{\SIfC}
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCIfL{\ECMV'}{\ZCCursor{\ECEHole}}{\ECEHole}}{\TUnknown}{\SIfC}
   }
 
   \inferrule[ASEConIfL]{ }{