[aslspec] changes following review comments

Author: Roman-Manevich

asllib/doc/ASLFormal.tex

@@ -249,6 +249,8 @@ \subsection{Lists}
 The \emph{length} of a list is the number of elements in that list:
 $\listlen{\emptylist} \triangleq 0$ and $\listlen{v_1,\ldots,v_k}=k$.
 \end{definition}
+\texthypertarget{relation-samelength}
+We write $\samelengthop[H]{a}{b}$ to denote that two lists $a$ and $b$ have the same length.
 
 We use the notation $a..b$, where $a,b\in\Z$ as a shorthand for the interval $[a\ldots b]$
 (counting up when $a \leq b$ and counting down when $a \geq b$).
@@ -1097,18 +1099,34 @@ \subsection{Checked Transitions\label{sec:Checked Transitions}}
 \hva\and
 \inferrule[de\_check\_false]{}{ \decheck(\False, \vcode) \evalarrow \DynamicError(\vcode) }
 \end{mathpar}
-} % END_OF_BACKUP_RULE
+} % END_OF_BACKUP_ORIGINAL_RULE
 \RenderRule{de_check}
 
 \subsection{Boolean Transition Judgments}
 \RenderRelation{bool_transition}
-We define the following rules to allow us to treat Boolean values as transition judgments,
-which in turn allow us to employ \shortcircuitrulemacros{}:
+We use this function defined by the following trivial rule to allow us to treat Boolean values as transition judgments,
+which in turn allows us to employ \shortcircuitrulemacros{}:
+\BackupOriginalRule{
 \begin{mathpar}
 \inferrule[bool\_trans\_true]{}{ \booltrans(\overname{\True}{\cond}) \booltransarrow \overname{\True}{\vresult} }
 \hva\and
 \inferrule[bool\_trans\_false]{}{ \booltrans(\overname{\False}{\cond}) \booltransarrow \overname{\False}{\vresult} }
 \end{mathpar}
+} % END_OF_BACKUP_ORIGINAL_RULE
+\RenderRule{bool_transition}
+
+This is useful in defining functions that return a Boolean value, where if a condition does not hold,
+there is no need to consider the rest of the premises, and the function can simply return $\False$:
+\begin{mathpar}
+\inferrule{
+  \booltrans(\vx > \vy) \booltransarrow \True\ \terminateas\ \False\\\\
+  p_2\\\\
+  \ldots\\\\
+  p_k
+}{
+  \textfunc{complex\_condition}(\vx, \vy) \booltransarrow \vb
+}
+\end{mathpar}
 
 \subsection{Judgments Over Optional Data Types}
 \hypertarget{def-mapopt}{}

asllib/doc/ASLmacros.tex

@@ -542,33 +542,45 @@
 
 \newcommand\makelist[1]{\left[{#1}\right]} % A list of expressions
 \newcommand\listlen[1]{\hyperlink{relation-listlen}{|}#1\hyperlink{relation-listlen}{|}}
+\newcommand\samelengthname[0]{\hyperlink{relation-samelength}{\textfunc{same\_length}}}
+\newcommand\samelengthop[3][H]{
+  \ifthenelse{\equal{#1}{H}}{
+    \samelengthname\left({#2}, {#3}\right)
+  }{
+    \samelengthname
+    \left(\begin{array}{l}
+    {#2},\\
+    {#3}\\
+    \end{array}\right)
+  }
+}
 \newcommand\concat[0]{\hyperlink{relation-concat}{\mathbin{+}}}
 \newcommand\concatlist[1]{\hyperlink{relation-concatlist}{\textfunc{concat\_list}}(#1)}
 \newcommand\cons[0]{\hyperlink{relation-cons}{\mathbin{{+}{+}}}}
 \newcommand\listfstname[0]{\hyperlink{relation-listfst}{\textfunc{list\_fst}}}
 \newcommand\listfst[1]{\listfstname(#1)}
 \newcommand\listcombine[3][H]{
   \ifthenelse{\equal{#1}{H}}
-    {{#2} \mathbin{\hyperlink{relation-listcombine}{\times}} {#3}}
+    {{#2} \mathbin{\hyperlink{relation-listcombine}{\otimes}} {#3}}
     {
     \left(\begin{array}{l}
-    {#2} \hyperlink{relation-listcombine}{\times}\\
+    {#2} \hyperlink{relation-listcombine}{\otimes}\\
     {#3}\\
     \end{array}\right)}
 }
-\newcommand\listcrossop[0]{\hyperlink{relation-listcross}{\otimes}}
 \newcommand\listcombinethree[4][H]{
   \ifthenelse{\equal{#1}{H}}{
-    {#2} \mathbin{\hyperlink{relation-listcombinethree}{\times_3}} {#3} \mathbin{\hyperlink{relation-listcombinethree}{\times_3}} {#4}
+    {#2} \mathbin{\hyperlink{relation-listcombinethree}{\otimes_3}} {#3} \mathbin{\hyperlink{relation-listcombinethree}{\otimes_3}} {#4}
   }{
     \hyperlink{relation-listcombinethree}{\textfunc{list\_combine\_3}}
     \left(\begin{array}{l}
-    {#2} \hyperlink{relation-listcombinethree}{\times_3}\\
-    {#3} \hyperlink{relation-listcombinethree}{\times_3}\\
+    {#2} \hyperlink{relation-listcombinethree}{\otimes_3}\\
+    {#3} \hyperlink{relation-listcombinethree}{\otimes_3}\\
     {#4}\\
     \end{array}\right)
   }
 }
+\newcommand\listcrossop[0]{\hyperlink{relation-listcross}{\times}}
 
 \newcommand\parallelcomp[0]{\hyperlink{def-parallel}{\mathbin{\parallel}}}
 \newcommand\parallelgraphs[1]{\hyperlink{def-parallellist}{\mathbin{\mathchoice{\Big\|}{\big\|}{\|}{\|}}}{#1}}