formalism: Fix typed con rules with mode change

hazelgrove · Oct 9, 2023 · 64d55d7 · 64d55d7
1 parent 5c501dd
commit 64d55d7
Showing 1 changed file with 12 additions and 28 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}
+  \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]{ }{