tweaks to save space in triples

papers/icfp2021/figure-queue-invariant.tex

@@ -91,7 +91,7 @@
                         \}
                     \end{array}\right)
                 }
-            \cr \begin{array}{@{\!\!}c@{}l@{\;}c@{\;}l} % array for aligning the formulas of the two big-stars
+            \cr \begin{array}{@{\!\!}c@{}l@{\;}c@{\;}l@{}} % array for aligning the formulas of the two big-stars
             % cells which are empty or being emptied:
                 \displaystyle\Sep_{\head-\capacity \leq \idx < \tail}&
                     % cell bearing no value, available for next round:

papers/icfp2021/figure-queue-spec.tex

 \begin{figure}
-\[\begin{array}{@{}l@{}}
+\[\small\begin{array}{@{}l@{}}
 
   \hoareV
     {\seen\view_0}
@@ -13,7 +13,7 @@
 
   \lahoareV
     {\begin{array}{@{}l@{}}\Forall \tview, \hview, \nbelems, \elemViewList*[].
-    \\ \hphantom{\Lam\Unit.}
+        \\  \hphantom{\Lam\Unit.}
             \isQueue \tview {\hphantom(\hview\hphantom{{}\viewjoin\view)}} \elemViewList
             \hphantom{, \pair\elem\view}
       \isep \seen\view
@@ -28,7 +28,7 @@
 
   \lahoareV
     {\begin{array}{@{}l@{}}\Forall \tview, \hview, \nbelems, \elemViewList*[].
-    \\ \hphantom{\Lam\elem.}
+        \\  \hphantom{\Lam\elem.}
             \isQueue {\hphantom(\tview\hphantom{{}\viewjoin\view)}} \hview \elemViewList
       \isep \seen\view
     \end{array}}
@@ -40,24 +40,25 @@
       %  \cr \seen(\tview \sqcup \eview_0)
       %}
             \isQueue {(\tview \sqcup \view)} \hview {\elemViewList<1>*}
-      \isep \seen(\tview \sqcup \eview_0)
-      \isep \elem = \elem_0
+      %\isep \seen (\tview \sqcup \eview_0)
+      \isep \seen \tview
+      \isep \seen \eview_0
       \isep 1 \leq \nbelems
+      \isep \elem = \elem_0
     }
 
 \\\\\\
 
   \lahoareV
     {\begin{array}{@{}l@{}}\Forall \tview, \hview, \nbelems, \elemViewList*[].
-        %\\ \hspace{118pt}
-        \\ \hspace{23pt}
+        \\  \hspace{2.9em}
             \isQueue \tview {\hphantom(\hview\hphantom{{}\viewjoin\view)}} \elemViewList
             \hphantom{, \pair\elem\view}
       \isep \seen\view
     \end{array}}
     {\tryenqueue~\queue~\elem}
     {\Lam \boolval.
-      \matchwith{\boolval}
+      \matchwithnobinder{\boolval}
         {\False}{\isQueue \tview {\hphantom(\hview\hphantom{{}\viewjoin\view)}} \elemViewList}
         {\True }{%
                 \isQueue \tview {(\hview \sqcup \view)} {\elemListSnoc \elemViewList {\pair\elem\view}}
@@ -69,25 +70,26 @@
 
   \lahoareV
     {\begin{array}{@{}l@{}}\Forall \tview, \hview, \nbelems, \elemViewList*[].
-        %\\ \hspace{127pt}
-        \\ \hspace{26pt}
+        \\  \hspace{3.13em}
             \isQueue {\hphantom(\tview\hphantom{{}\viewjoin\view)}} \hview \elemViewList
       \isep \seen\view
     \end{array}}
     {\trydequeue~\queue}
     {\Lam \elemopt.
-      \matchwith{\elemopt}
+      \matchwithnobinder{\elemopt}
         {\None     }{\isQueue {\hphantom(\tview\hphantom{{}\viewjoin\view)}} \hview \elemViewList}
-        {\Some\elem}{%
+        {\Some{\elem_0}}{%
           %\ISep{%
           %      1 \leq \nbelems \isep \elem = \elem_0
           %  \cr \isQueue {(\tview \sqcup \view)} \hview {\elemViewList<1>*}
           %  \cr \seen(\tview \sqcup \eview_0)
           %}
                 \isQueue {(\tview \sqcup \view)} \hview {\elemViewList<1>*}
-          \isep \seen(\tview \sqcup \eview_0)
-          \isep \elem = \elem_0
+          %\isep \seen (\tview \sqcup \eview_0)
+          \isep \seen \tview
+          \isep \seen \eview_0
           \isep 1 \leq \nbelems
+          %\isep \elem = \elem_0
         }
     }
 

papers/icfp2021/notations.tex

@@ -280,12 +280,18 @@
 %  \end{array}\right.
 %}
 \newcommand{\matchwith}[5]{%
-  %\mathord\lor
   \left[\begin{array}{@{\,}ll@{}}
     #3 & \text{if }#1 = #2 \\
     #5 & \text{if }#1 = #4
   \end{array}\right.
 }
+\newcommand{\matchwithnobinder}[5]{%
+  \mathord\lor
+  \left[\begin{array}{@{\,}l@{}l@{}}
+    #3 &{}\isep #1 = #2 \\
+    #5 &{}\isep #1 = #4
+  \end{array}\right.
+}
 
 % the “valid view” predicate:
 \newcommand{\valid}[1]{\mathit{valid}\,#1}
@@ -707,7 +713,8 @@
 \newcommand{\capacity}{\ensuremath{C}}
 \newcommand{\queue}{\ensuremath{q}}
 \newcommand{\boolval}{\ensuremath{b}}
-\newcommand{\elemopt}{\ensuremath{v^?}}
+%\newcommand{\elemopt}{\ensuremath{v^{\!?}}}
+\newcommand{\elemopt}{\ensuremath{v^{\!\!\:\raisebox{-0.3ex}{\scriptsize?}}}}
 \newcommand{\elem}{\ensuremath{v}}
 \newcommand{\status}{\ensuremath{s}}
 \newcommand{\tail}{\ensuremath{t}}