[asl] Fix definition of Lowest Common Ancestor on tuples.

Removed the requirement that elements of types must type-satisfy
each other.
This means that the type of `if cond then (0, 63) else (0, 31)`
is `(integer{0}, integer{63,31})`.

asllib/doc/ASLTypingReference.tex

@@ -2834,29 +2834,13 @@ \subsection{Prose}
       \item the result is a type error indicating the lack of a lowest common ancestor.
     \end{itemize}
 
-    \item All of the following apply (\textsc{t\_tuple\_different\_length}):
-    \begin{itemize}
-      \item $\vt$ is a tuple type with type list $\vlit$;
-      \item $\vs$ is a tuple type with type list $\vlis$;
-      \item $\vlit$ and $vlis$ differ in their number of elements;
-      \item the result is a type error indicating the lack of a lowest common ancestor.
-    \end{itemize}
-
-    \item All of the following apply (\textsc{t\_tuple\_error}):
-    \begin{itemize}
-      \item $\vt$ is a tuple type with type list $\vlit$;
-      \item $\vs$ is a tuple type with type list $\vlis$;
-      \item $\vlit$ and $\vlis$ have the same number of elements;
-      \item there exists an index $\vi$ such that either $\vlit[\vi]$ does not \typesatisfy\ $\vlis[\vi]$ or vice versa;
-      \item the result is a type error indicating the lack of a lowest common ancestor.
-    \end{itemize}
-
     \item All of the following apply (\textsc{t\_tuple}):
     \begin{itemize}
       \item $\vt$ is a tuple type with type list $\vlit$;
       \item $\vs$ is a tuple type with type list $\vlis$;
-      \item $\vlit$ and $\vlis$ have the same number of elements;
-      \item for every index $\vi$, $\vlit[\vi]$ \typesatisfies\ $\vlis[\vi]$ and vice versa;
+      \item checking whether $\vlit$ and $\vlis$ have the same number of elements yields $\True$
+            or a type error, which short-circuits the entire rule (indicating that the number of elements in both tuples is expected
+            to be the same and thus there is no lowest common ancestor);
       \item $\vli[\vi]$ is the of types lowest common ancestor of $\vlit[\vi]$ and $\vlis[\vi]$, for every position of $\vlit$;
       \item $\tty$ is the tuple type with list of types $\vli$, that is, $\TTuple(\vli)$.
     \end{itemize}
@@ -3000,35 +2984,12 @@ \subsection{Formally}
 \end{mathpar}
 
 \begin{mathpar}
-\inferrule[t\_tuple\_different\_length]{
-  \typeequal(\tenv, \vt, \vs) \typearrow \False\\
-  \vt \eqname \TTuple(\vlit)\\
-  \vs \eqname \TTuple(\vlis)\\
-  \equallength(\vlit, \vlis) \typearrow \False
-}{
-  \lca(\tenv, \vt, \vs) \typearrow \TypeErrorVal{NoLCA}
-}
-\and
-\inferrule[t\_tuple\_error]{
-  \typeequal(\tenv, \vt, \vs) \typearrow \False\\
-  \vt \eqname \TTuple(\vlit)\\
-  \vs \eqname \TTuple(\vlis)\\
-  \equallength(\vlit, \vlis) \typearrow \True\\
-  \vi\in\listrange(\vlit)\\
-  \typesat(\tenv, \vlit[\vi], \vlis[\vi]) \typearrow \vbone\\
-  \typesat(\tenv, \vlis[\vi], \vlit[\vi]) \typearrow \vbtwo\\
-  \vbone = \False \lor \vbtwo = \False
-}{
-  \lca(\tenv, \vt, \vs) \typearrow \TypeErrorVal{NoLCA}
-}
-\and
 \inferrule[t\_tuple]{
   \typeequal(\tenv, \vt, \vs) \typearrow \False\\
   \vt \eqname \TTuple(\vlit)\\
   \vs \eqname \TTuple(\vlis)\\
-  \equallength(\vlit, \vlis) \typearrow \True\\
-  \vi\in\listrange(\vlit): \typesat(\tenv, \vlit[\vi], \vlis[\vi]) \typearrow \True\\
-  \vi\in\listrange(\vlit): \typesat(\tenv, \vlis[\vi], \vlit[\vi]) \typearrow \True\\
+  \equallength(\vlit, \vlis) \typearrow \vb\\
+  \checktrans{\vb}{NoLCA, TuplesHaveDifferentLengths} \typearrow \True \OrTypeError\\\\
   \vi\in\listrange(\vlit): \lca(\tenv, \vlit[\vi], \vlis[\vi]) \typearrow \vli[\vi] \OrTypeError\\
   \vli \eqdef [\vi\in\listrange(\vlit): \vli[\vi]]
 }{

asllib/tests/lca.t

@@ -159,14 +159,11 @@
   $ cat >lca.asl <<EOF
   > func main () => integer
   > begin
-  >   let - = if UNKNOWN: boolean then (3, 2) else (1, 4);
+  >   let v : (integer{3,1}, integer{2,4}) = if UNKNOWN: boolean then (3, 2) else (1, 4);
+  >   return 0;
   > end
 
   $ aslref lca.asl
-  File lca.asl, line 3, characters 10 to 53:
-  ASL Typing error: cannot find a common ancestor to those two types
-    (integer {3}, integer {2}) and (integer {1}, integer {4}).
-  [1]
 
   $ cat >lca.asl <<EOF
   > type T1 of integer;
@@ -182,6 +179,3 @@
   File lca.asl, line 7, characters 2 to 18:
   ASL Typing error: a subtype of real was expected, provided array [4] of T1.
   [1]
-
-
-

asllib/types.ml

@@ -756,14 +756,10 @@ let rec lowest_common_ancestor env s t =
       let+ t = lowest_common_ancestor env ty_s ty_t in
       T_Array (width_s, t) |> add_dummy_pos
   | T_Tuple li_s, T_Tuple li_t
-    when List.compare_lengths li_s li_t = 0
-         && List.for_all2 (type_satisfies env) li_s li_t
-         && List.for_all2 (type_satisfies env) li_t li_s ->
-      (* If S and T both are tuple types with the same number of elements and
-         the types of elements of S type-satisfy the types of the elements of T
-         and vice-versa: the tuple type with the type of each element the
-         lowest common ancestor of the types of the corresponding elements of S
-         and T. *)
+    when List.compare_lengths li_s li_t = 0 ->
+      (* If S and T both are tuple types with the same number of elements:
+         the tuple type with the type of each element the lowest common ancestor
+         of the types of the corresponding elements of S and T. *)
       let+ li =
         List.map2 (lowest_common_ancestor env) li_s li_t |> unpack_options
       in