[aslspec] imported apply_binop_extremities to aslspec

Author: Roman-Manevich

asllib/doc/SymbolicSubsumptionTesting.tex

@@ -479,101 +479,7 @@ \section{Symbolic Reasoning\label{sec:Symbolic Reasoning}}
 for cases where a binary operation involves two \rangeconstraintsterm.
 \ASLListing{Generating constraints for binary operations}{ApplyBinopExtremities}{\typingtests/TypingRule.ApplyBinopExtremities.asl}
 
-\ProseParagraph
-\OneApplies
-\begin{itemize}
-  \item \AllApplyCase{exact\_exact}
-  \begin{itemize}
-    \item $\vcone$ is a constraint for the expression $\va$;
-    \item $\vctwo$ is a constraint for the expression $\vc$;
-    \item define $\newcs$ as the list containing the constraint for the \binopexpressionterm{} $\AbbrevEBinop{\op}{\va}{\vc}$.
-  \end{itemize}
-
-  \item \AllApplyCase{range\_exact}
-  \begin{itemize}
-    \item $\vcone$ is a range constraint for the expressions $\va$ and $\vb$;
-    \item $\vctwo$ is a constraint for the expression $\vc$;
-    \item applying $\possibleextremitiesleft$ to $\op$, $\va$, and $\vb$ yields $\extpairs$;
-    \item define $\newcs$ as the list containing a constraint $\AbbrevConstraintRange{\AbbrevEBinop{\op}{\vap}{\vc}}{\AbbrevEBinop{\op}{\vbp}{\vc}}$
-          for each pair of expressions $(\vap, \vbp)$ in $\extpairs$.
-  \end{itemize}
-
-  \item \AllApplyCase{exact\_range}
-  \begin{itemize}
-    \item $\vcone$ is a constraint for the expression $\va$;
-    \item $\vctwo$ is a range constraint for the expressions $\vc$ and $\vd$;
-    \item applying $\possibleextremitiesright$ to $\op$, $\vc$, and $\vd$ yields $\extpairs$;
-    \item define $\newcs$ as the list containing a constraint $\AbbrevConstraintRange{\AbbrevEBinop{\op}{\va}{\vcp}}{\AbbrevEBinop{\op}{\va}{\vdp}}$
-          for each pair of expressions $(\vcp, \vdp)$ in $\extpairs$.
-  \end{itemize}
-
-  \item \AllApplyCase{range\_range}
-  \begin{itemize}
-    \item $\vcone$ is a range constraint for the expressions $\va$ and $\vb$;
-    \item $\vctwo$ is a range constraint for the expressions $\vc$ and $\vd$;
-    \item applying $\possibleextremitiesleft$ to $\op$, $\va$, and $\vb$ yields $\extpairsab$;
-    \item applying $\possibleextremitiesright$ to $\op$, $\vc$, and $\vd$ yields $\extpairscd$;
-    \item define $\newcs$ as the list containing a constraint $\AbbrevConstraintRange{\AbbrevEBinop{\op}{\vap}{\vcp}}{\AbbrevEBinop{\op}{\vbp}{\vdp}}$
-          for each pair of expressions
-          $(\vap, \vbp)$ in $\extpairsab$
-          and each pair of expressions
-          $(\vcp, \vdp)$ in $\extpairscd$.
-  \end{itemize}
-\end{itemize}
-
-\FormallyParagraph
-\begin{mathpar}
-\inferrule[exact\_exact]{
-  \vcone = \ConstraintExact(\va)\\
-  \vctwo = \ConstraintExact(\vc)
-}{
-  {
-    \begin{array}{r}
-  \applybinopextremities(\op, \vcone, \vctwo) \typearrow \\
-  \overname{[ \ConstraintExact(\AbbrevEBinop{\op}{\va}{\vc}) ]}{\newcs}
-    \end{array}
-  }
-}
-\end{mathpar}
-
-\begin{mathpar}
-\inferrule[range\_exact]{
-  \vcone = \ConstraintRange(\va, \vb)\\
-  \vctwo = \ConstraintExact(\vc)\hva\\
-  \possibleextremitiesleft(\op, \va, \vb) \typearrow \extpairs\\
-  \newcs \eqdef [(\vap, \vbp) \in \extpairs: \AbbrevConstraintRange{\AbbrevEBinop{\op}{\vap}{\vc}}{\AbbrevEBinop{\op}{\vbp}{\vc}}]
-}{
-  \applybinopextremities(\op, \vcone, \vctwo) \typearrow
-  \newcs
-}
-\end{mathpar}
-
-\begin{mathpar}
-\inferrule[exact\_range]{
-  \vcone = \ConstraintExact(\va)\\
-  \vctwo = \ConstraintRange(\vc, \vd)\hva\\
-  \possibleextremitiesright(\op, \vc, \vd) \typearrow \extpairs\\
-  \newcs \eqdef [(\vcp, \vdp) \in \extpairs: \AbbrevConstraintRange{\AbbrevEBinop{\op}{\va}{\vcp}}{\AbbrevEBinop{\op}{\va}{\vdp}}]
-}{
-  \applybinopextremities(\op, \vcone, \vctwo) \typearrow
-  \newcs
-}
-\end{mathpar}
-
-\begin{mathpar}
-\inferrule[range\_range]{
-  \vcone = \ConstraintRange(\va, \vb)\\
-  \vctwo = \ConstraintRange(\vc, \vd)\hva\\
-  \possibleextremitiesleft(\op, \va, \vb) \typearrow \extpairsab\\
-  \possibleextremitiesright(\op, \vc, \vd) \typearrow \extpairscd\hva\\
-  \newcs \eqdef [(\vap, \vbp) \in \extpairsab, (\vcp, \vdp) \in \extpairscd:
-  \AbbrevConstraintRange{\AbbrevEBinop{\op}{\vap}{\vcp}}{\AbbrevEBinop{\op}{\vbp}{\vdp}}]
-}{
-  \applybinopextremities(\op, \vcone, \vctwo) \typearrow
-  \newcs
-}
-\end{mathpar}
-%\RenderProseAndFormally{apply_binop_extremities}
+\RenderProseAndFormally{apply_binop_extremities}
 
 \TypingRuleDef{PossibleExtremitiesLeft}
 \RenderRelation{possible_extremities_left}

asllib/doc/asl.spec

@@ -13930,7 +13930,54 @@ typing function apply_binop_extremities(op: binop, c1: int_constraint, c2: int_c
   {op} yields a \dynamicerrorterm{}.",
   prose_application = "the range constraints for {c1} and {c2}",
   prose_transition = "computing the range constraints for {c1} and {c2} yields",
-};
+} =
+  case exact_exact {
+    c1 =: Constraint_Exact(a);
+    c2 =: Constraint_Exact(c);
+    --
+    make_singleton_list(Constraint_Exact(AbbrevEBinop(op, a, c)));
+  }
+
+  case range_exact {
+    c1 =: Constraint_Range(a, b);
+    c2 =: Constraint_Exact(c);
+    possible_extremities_left(op, a, b) -> extpairs;
+    extpairs =: list_combine(ext_a, ext_b);
+    ext_a_c := list_map(i, indices(extpairs), AbbrevEBinop(op, ext_a[i], c));
+    ext_b_c := list_map(i, indices(extpairs), AbbrevEBinop(op, ext_b[i], c));
+    new_cs := list_map(i, indices(extpairs), AbbrevConstraintRange(ext_a_c[i], ext_b_c[i]));
+    --
+    new_cs;
+  }
+
+  case exact_range {
+    c1 =: Constraint_Exact(a);
+    c2 =: Constraint_Range(c, d);
+    possible_extremities_right(op, c, d) -> extpairs;
+    extpairs =: list_combine(ext_c, ext_d);
+    ext_a_c := list_map(i, indices(extpairs), AbbrevEBinop(op, a, ext_c[i]));
+    ext_a_d := list_map(i, indices(extpairs), AbbrevEBinop(op, a, ext_d[i]));
+    new_cs := list_map(i, indices(extpairs), AbbrevConstraintRange(ext_a_c[i], ext_a_d[i]));
+    --
+    new_cs;
+  }
+
+  case range_range {
+    c1 =: Constraint_Range(a, b);
+    c2 =: Constraint_Range(c, d);
+    possible_extremities_left(op, a, b) -> extpairs_a_b;
+    possible_extremities_right(op, c, d) -> extpairs_c_d;
+    ext_cross := list_cross(extpairs_a_b, extpairs_c_d);
+    ext_cross =: list_combine(cross_a_b, cross_c_d);
+    cross_a_b =: list_combine(ext_a, ext_b);
+    cross_c_d =: list_combine(ext_c, ext_d);
+    new_a_c := list_map(i, indices(ext_cross), AbbrevEBinop(op, ext_a[i], ext_c[i]));
+    new_b_d := list_map(i, indices(ext_cross), AbbrevEBinop(op, ext_b[i], ext_d[i]));
+    new_cs := list_map(i, indices(ext_cross), AbbrevConstraintRange(new_a_c[i], new_b_d[i]));
+    --
+    new_cs;
+  }
+;
 
 typing function possible_extremities_left(op: binop, a: expr, b: expr) ->
          (extpairs: list0((expr, expr)))