formalism: Fix and add missing analytic zipper rules for zippered mar…

…ked lambda
hazelgrove · Oct 10, 2023 · fabbbec · fabbbec
1 parent bbb6a30
commit fabbbec
Showing 1 changed file with 53 additions and 4 deletions.
diff --git a/formalism/typed.tex b/formalism/typed.tex
@@ -997,7 +997,7 @@ \subsubsection{Analytic expression actions}
     \notMatchedArrow{\TMV} \\
     \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TUnknown}}{\erase{\ECMV}}{\ECMV'}{\TUnknown}
   }{
-    \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCInconType{\ZCLamT{x}{\ZTCursor{\TUnknown}}{\ECMV'}}}{\TMV}{\SLam{x}}
+    \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCLamAnaNonMatchedArrowT{x}{\ZTCursor{\TUnknown}}{\ECMV'}}{\TMV}{\SLam{x}}
   }
 
   \inferrule[AAEConLetL]{
@@ -1079,15 +1079,51 @@ \subsubsection{Analytic expression actions}
     \notEqual{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV'}} \\
     \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\\\
     \inconsistent{\cursorErase{\ZTMV_3'}}{\TMV_1} \\
-    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TMV_1}}{\erase{\ECMV}}{\ECMV'}{\TMV_2}
+    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV_3'}}}{\erase{\ECMV}}{\ECMV'}{\TMV_2}
   }{
-    \AAAction{\ctx}{\ZCLamT{x}{\ZTMV_3}{\ECMV}}{\ZCInconType{\ZCLamT{x}{\ZTMV_3'}{\ECMV'}}}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCLamT{x}{\ZTMV_3}{\ECMV}}{\ZCLamInconAscT{x}{\ZTMV_3'}{\ECMV'}}{\TMV}{\AMV}
   }
 
   \inferrule[AAEZipLamT4]{
     \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\
+    \equal{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}}
+  }{
+    \AAAction{\ctx}{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV_3}{\ECMV}}{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV_3'}{\ECMV}}{\TMV}{\AMV}
+  }
+
+  \inferrule[AAEZipLamT5]{
+    \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\
+    \notEqual{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}} \\\\
+    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV_3'}}}{\erase{\ECMV}}{\ECMV'}{\TUnknown}
+  }{
+    \AAAction{\ctx}{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV_3}{\ECMV}}{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV_3'}{\ECMV}}{\TMV}{\AMV}
+  }
+
+  \inferrule[AAEZipLamT6]{
+    \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\
+    \equal{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}}
+  }{
+    \AAAction{\ctx}{\ZCLamInconAscT{x}{\ZTMV_3}{\ECMV}}{\ZCLamInconAscT{x}{\ZTMV_3'}{\ECMV}}{\TMV}{\AMV}
+  }
+
+  \inferrule[AAEZipLamT7]{
+    \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\
+    \notEqual{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}} \\
+    \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\\\
+    \consistent{\cursorErase{\ZTMV_3'}}{\TMV_1} \\
+    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV_3'}}}{\erase{\ECMV}}{\ECMV'}{\TMV_2}
+  }{
+    \AAAction{\ctx}{\ZCLamInconAscT{x}{\ZTMV_3}{\ECMV}}{\ZCLamT{x}{\ZTMV_3'}{\ECMV'}}{\TMV}{\AMV}
+  }
+
+  \inferrule[AAEZipLamT8]{
+    \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\
+    \notEqual{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}} \\
+    \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\\\
+    \inconsistent{\cursorErase{\ZTMV_3'}}{\TMV_1} \\
+    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV_3'}}}{\erase{\ECMV}}{\ECMV'}{\TMV_2}
   }{
-    \AAAction{\ctx}{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV_3}{\ECMV}}{\ZCLamT{x}{\ZTMV_3'}{\ECMV}}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCLamInconAscT{x}{\ZTMV_3}{\ECMV}}{\ZCLamInconAscT{x}{\ZTMV_3'}{\ECMV'}}{\TMV}{\AMV}
   }
 
   \inferrule[AAEZipLamE1]{
@@ -1097,6 +1133,19 @@ \subsubsection{Analytic expression actions}
     \AAAction{\ctx}{\ZCLamE{x}{\TMV_3}{\ZCMV}}{\ZCLamE{x}{\TMV_3}{\ZCMV'}}{\TMV}{\AMV}
   }
 
+  \inferrule[AAEZipLamE2]{
+    \AAAction{\extendCtx{\ctx}{x}{\TMV_3}}{\ZCMV}{\ZCMV'}{\TUnknown}{\AMV}
+  }{
+    \AAAction{\ctx}{\ZCLamAnaNonMatchedArrowE{x}{\TMV_3}{\ZCMV}}{\ZCLamAnaNonMatchedArrowE{x}{\TMV_3}{\ZCMV'}}{\TMV}{\AMV}
+  }
+
+  \inferrule[AAEZipLamE3]{
+    \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\
+    \AAAction{\extendCtx{\ctx}{x}{\TMV_3}}{\ZCMV}{\ZCMV'}{\TMV_2}{\AMV}
+  }{
+    \AAAction{\ctx}{\ZCLamInconAscE{x}{\TMV_3}{\ZCMV}}{\ZCLamInconAscE{x}{\TMV_3}{\ZCMV'}}{\TMV}{\AMV}
+  }
+
   \inferrule[AAEZipLetL1]{
     \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV_1} \\
     \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\