formalism: Add mising analytic con rules for typed model

hazelgrove · Oct 9, 2023 · a08f294 · a08f294
1 parent 4c57d92
commit a08f294
Showing 1 changed file with 46 additions and 11 deletions.
diff --git a/formalism/typed.tex b/formalism/typed.tex
@@ -950,19 +950,19 @@ \subsubsection{Analytic expression actions}
   \inferrule[AAEInconsistentTypes1]{
     \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV'} \\
     \ASAction{\ctx}{\ZCMV}{\TMV'}{\ZCMV'}{\TMV''}{\AMV} \\\\
-    \inconsistent{\TMV}{\TMV''} \\
+    \consistent{\TMV}{\TMV''} \\
     \subsumable{\cursorErase{\ZCMV}}
   }{
-    \AAAction{\ctx}{\ZCInconType{\ZCMV}}{\ZCInconType{\ZCMV'}}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCInconType{\ZCMV}}{\ZCMV'}{\TMV}{\AMV}
   }
 
   \inferrule[AAEInconsistentTypes2]{
     \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV'} \\
     \ASAction{\ctx}{\ZCMV}{\TMV'}{\ZCMV'}{\TMV''}{\AMV} \\\\
-    \consistent{\TMV}{\TMV''} \\
+    \inconsistent{\TMV}{\TMV''} \\
     \subsumable{\cursorErase{\ZCMV}}
   }{
-    \AAAction{\ctx}{\ZCInconType{\ZCMV}}{\ZCMV'}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCInconType{\ZCMV}}{\ZCInconType{\ZCMV'}}{\TMV}{\AMV}
   }
 \end{mathpar}
 
@@ -986,20 +986,22 @@ \subsubsection{Analytic expression actions}
 \begin{mathparpagebreakable}
   \inferrule[AAEConLam1]{
     \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\
-    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TMV_1}}{\ECMV}{\ECMV'}{\TMV_2}
+    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TMV_1}}{\erase{\ECMV}}{\ECMV'}{\TMV_2}
   }{
     \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCLamT{x}{\ZTCursor{\TMV_1}}{\ECMV'}}{\TMV}{\SLam{x}}
   }
 
   \inferrule[AAEConLam2]{
     \notMatchedArrow{\TMV} \\
-    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TUnknown}}{\ECMV}{\ECMV'}{\TUnknown}
+    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TUnknown}}{\erase{\ECMV}}{\ECMV'}{\TUnknown}
   }{
     \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCInconType{\ZCLamT{x}{\ZTCursor{\TUnknown}}{\ECMV'}}}{\TMV}{\SLam{x}}
   }
 
-  \inferrule[AAEConLetL]{ }{
-    \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCLetL{x}{\ECMV}{\ZCCursor{\ECEHole}}}{\TMV}{\SLetL{x}}
+  \inferrule[AAEConLetL]{
+    \ctxSynFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TMV}
+  }{
+    \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCLetL{x}{\ECMV'}{\ZCCursor{\ECEHole}}}{\TMV}{\SLetL{x}}
   }
 
   \inferrule[AAEConLetR]{
@@ -1008,13 +1010,46 @@ \subsubsection{Analytic expression actions}
     \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCLetR{x}{\ZCCursor{\ECEHole}}{\ECMV'}}{\TMV}{\SLetR{x}}
   }
 
+  \inferrule[AAEConIfC]{
+    \ctxAnaFixedInto{\ctx}{\ECMV}{\ECMV'}{\TBool}
+  }{
+    \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCIfL{\ECMV'}{\ZCCursor{\ECEHole}}{\ECEHole}}{\TMV}{\SIfC}
+  }
+
   \inferrule[AAEConIfL]{ }{
-    \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCIfC{\ZCCursor{\ECEHole}}{\ECMV}{\ECEHole}}{\TMV}{\SIfL}
+    \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCIfC{\ZCCursor{\ECEHole}}{\ECMV'}{\ECEHole}}{\TMV}{\SIfL}
   }
 
-  \inferrule[AAEConIfR]{
+  \inferrule[AAEConIfR]{ }{
+    \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCIfC{\ZCCursor{\ECEHole}}{\ECEHole}{\ECMV'}}{\TMV}{\SIfR}
+  }
+
+  \inferrule[AAEConPairL1]{
+    \matchedProd{\TMV}{\TMV_1}{\TMV_2} \\
+    \ctxAnaFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TMV_1}
+  }{
+    \AACon{\ctx}{\ZCursor{\ECMV}}{\ZCPairL{\ECMV'}{\ZCursor{\ECEHole}}}{\TMV}{\SPairL}
+  }
+
+  \inferrule[AAEConPairL2]{
+    \notMatchedProd{\TMV} \\
+    \ctxAnaFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TUnknown}
+  }{
+    \AACon{\ctx}{\ZCursor{\ECMV}}{\ZCPairAnaNonMatchedProdL{\ECMV'}{\ZCursor{\ECEHole}}}{\TMV}{\SPairL}
+  }
+
+  \inferrule[AAEConPairR1]{
+    \matchedProd{\TMV}{\TMV_1}{\TMV_2} \\
+    \ctxAnaFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TMV_2}
+  }{
+    \AACon{\ctx}{\ZCursor{\ECMV}}{\ZCPairR{\ZCursor{\ECEHole}}{\ECMV'}}{\TMV}{\SPairR}
+  }
+
+  \inferrule[AAEConPairR2]{
+    \notMatchedProd{\TMV} \\
+    \ctxAnaFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TUnknown}
   }{
-    \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCIfC{\ZCCursor{\ECEHole}}{\ECEHole}{\ECMV}}{\TMV}{\SIfR}
+    \AACon{\ctx}{\ZCursor{\ECMV}}{\ZCPairAnaNonMatchedProdR{\ZCursor{\ECEHole}}{\ECMV'}}{\TMV}{\SPairR}
   }
 \end{mathparpagebreakable}