formalism: Fix typed con rules with mode change

hazelgrove · Oct 9, 2023 · f18d541 · f18d541
1 parent 5c501dd
commit f18d541
Showing 1 changed file with 14 additions and 30 deletions.
diff --git 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}
-  }{
-    \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}
-  }{
-    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPlusL{\ZCCursor{\ECEHole}}{\ECMV}}{\TNum}{\SPlusR}
-  }
-
-  \inferrule[ASEConPlusR2]{
-    \inconsistent{\TMV}{\TNum}
+  \inferrule[ASEConPlusL]{
+    \ctxAnaFixedInto{\ctx}{\ECMV}{\ECMV'}{\TNum}
   }{
-    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPlusL{\ZCCursor{\ECEHole}}{\ECInconType{\ECMV}}}{\TNum}{\SPlusR}
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPlusR{\ECMV'}{\ZCCursor{\ECEHole}}}{\TNum}{\SPlusL}
   }
 
-  \inferrule[ASEConIfC1]{
-    \consistent{\TMV}{\TBool}
+  \inferrule[ASEConPlusR]{
+    \ctxAnaFixedInto{\ctx}{\ECMV}{\ECMV'}{\TNum}
   }{
-    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCIfL{\ECMV}{\ZCCursor{\ECEHole}}{\ECEHole}}{\TUnknown}{\SIfC}
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPlusL{\ZCCursor{\ECEHole}}{\ECMV'}}{\TNum}{\SPlusR}
   }
 
-  \inferrule[ASEConIfC2]{
-    \inconsistent{\TMV}{\TBool}
+  \inferrule[ASEConIfC]{
+    \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]{ }{
@@ -639,7 +623,7 @@ \subsubsection{Synthetic expression actions}
     \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPairR{\ECEHole}{\ZCCursor{\ECMV}}}{\TProd{\TUnknown}{\TMV}}{\SPairR}
   }
 
-  \inferrule[ASEConProjL1]{
+  \inferrule[ASEConProjL]{
     \matchedProd{\TMV}{\TMV_1}{\TMV_2}
   }{
     \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCProjL{\ZCCursor{\ECMV}}}{\TMV_1}{\SProjL}