Corrected function type subtype rule (bounds); corrected "math" index entries

Author: eernstg

specification/dart.sty

@@ -381,6 +381,9 @@
 \newcommand{\SubtypeStd}[2]{\Subtype{\Delta}{#1}{#2}}
 % Subtype judgment where the environment is omitted (NE: "no environment").
 \newcommand{\SubtypeNE}[2]{\ensuremath{{#1}\,<:\,{#2}}}
+\newcommand{\MutualSubtype}[3]{\ensuremath{{#1}\vdash{#2}\,<:>\,{#3}}}
+\newcommand{\MutualSubtypeStd}[2]{\MutualSubtype{\Delta}{#1}{#2}}
+\newcommand{\MutualSubtypeNE}[2]{\ensuremath{{#1}\,<:>\,{#2}}}
 
 % Judgment expressing that a supertype relation exists.
 \newcommand{\Supertype}[3]{\ensuremath{{#1}\vdash{#2}\,:>\,{#3}}}

specification/dartLangSpec.tex

@@ -6267,7 +6267,7 @@ \subsection{Explicit Invocation of an Instance Member of an Extension}
 \IndexCustom{instantiated \ON{} type}{extension!instantiated \ON{} type}
 of $a$ as $[T_1/X_1, \ldots, T_s/X_s]T$.
 We define the
-\IndexCustom{instantiation-to-bound \ON{} type}{
+\IndexCustom{instantiation-to-bound \ON{} type}{%
   extension!instantiation-to-bound \ON{} type}
 of $a$ as $[U_1/X_1, \ldots, U_s/X_s]T$,
 where \List{U}{1}{s} is the result of instantiation to bound
@@ -6342,7 +6342,7 @@ \subsection{Explicit Invocation of an Instance Member of an Extension}
 
 \LMHash{}%
 The member signature $s_1$ is called the
-\IndexCustom{invocation member signature}{
+\IndexCustom{invocation member signature}{%
   extension!invocation member signature}
 of $i$.
 The static type of $i$ is the return type of
@@ -13953,7 +13953,7 @@ \subsection{Member Invocations}
 expression $r$ is an expression of
 one of the forms shown in Fig.~\ref{fig:memberInvocations}.
 Each member invocation has a
-\IndexCustom{corresponding member name}{
+\IndexCustom{corresponding member name}{%
   member invocation!corresponding member name}
 as shown in the figure.
 
@@ -14557,7 +14557,7 @@ \subsubsection{Superinvocations}
 
 \LMHash{}%
 An
-\IndexCustom{implicit \CALL{} superinvocation}{
+\IndexCustom{implicit \CALL{} superinvocation}{%
   method superinvocation!implicit \CALL}
 has the form
 
@@ -21663,7 +21663,7 @@ \subsection{Type Aliases}
 we say that the parameterized type $U$ of the form
 \code{$F$<\List{U}{1}{s}>}
 in a scope where $F$ resolves to $D$
-\IndexCustom{alias expands in one step to}{
+\IndexCustom{alias expands in one step to}{%
   type alias!alias expands in one step}
 $[U_1/X_1, \ldots, U_s/X_s]T$.
 
@@ -21678,7 +21678,7 @@ \subsection{Type Aliases}
 by its alias expansion in one step
 (\commentary{including the non-generic case where there are no type arguments}).
 When no further steps are possible we say that the resulting type is the
-\IndexCustom{transitive alias expansion}{
+\IndexCustom{transitive alias expansion}{%
   type alias!transitive alias expansion}
 of $U$.
 
@@ -22017,18 +22017,20 @@ \subsection{Subtypes}
   % ------------------------------------------------ Positional Function Type
   \RuleRawRaw{\SrnPositionalFunctionType}{%
     \Delta' = \Delta\uplus\{X_i\mapsto{}B_i\,|\,1 \leq i \leq s\} &
+    \forall i \in 1..s\!:\;\MutualSubtype{\Delta'}{B_i}{B'\!_i} &
     \Subtype{\Delta'}{S_0}{T_0} \\
     n_1 \leq n_2 &
     n_1 + k_1 \geq n_2 + k_2 &
     \forall j \in 1 .. n_2 + k_2\!:\;\Subtype{\Delta'}{T_j}{S_j}}{%
     \begin{array}{c}
       \Delta\vdash\RawFunctionTypePositional{S_0}{X}{B}{s}{S}{n_1}{k_1}\;<:\;\\
-      \RawFunctionTypePositional{T_0}{X}{B}{s}{T}{n_2}{k_2}
+      \RawFunctionTypePositional{T_0}{X}{B'\!}{s}{T}{n_2}{k_2}
     \end{array}}
   \ExtraVSP\ExtraVSP
   % ------------------------------------------------ Named Function Type
   \RuleRawRaw{\SrnNamedFunctionType}{
     \Delta' = \Delta\uplus\{X_i\mapsto{}B_i\,|\,1 \leq i \leq s\} &
+    \forall i \in 1..s\!:\;\MutualSubtype{\Delta'}{B_i}{B'\!_i} &
     \Subtype{\Delta'}{S_0}{T_0} &
     \forall j \in 1 .. n\!:\;\Subtype{\Delta'}{T_j}{S_j}\\
     \{\,\List{y}{n+1}{n+k_2}\,\} \subseteq \{\,\List{x}{n+1}{n+k_1}\,\}\\
@@ -22038,13 +22040,16 @@ \subsection{Subtypes}
     (r_{n+q} = \REQUIRED{} \Rightarrow r'_{n+p} = \REQUIRED)}{%
     \begin{array}{c}
       \Delta\vdash\RawFunctionTypeNamed{S_0}{X}{B}{s}{S}{n}{x}{k_1}{r}\;<:\;\\
-      \RawFunctionTypeNamed{T_0}{X}{B}{s}{T}{n}{y}{k_2}{r'}
+      \RawFunctionTypeNamed{T_0}{X}{B'\!}{s}{T}{n}{y}{k_2}{r'}
     \end{array}}
   %
   \ExtraVSP
   % ------------------------------------------------ Covariance
+  %% TODO(eernst): Type aliases have been expanded so there is no other
+  %% variance than covariance, but there will be in/out/inout in classes,
+  %% and then we'll need to handle variance here.
   \RuleRaw{\SrnCovariance}{%
-    \mbox{$C$ is an interface type with $s$ type parameters} &
+    \mbox{$C$ is an interface type with $s$ type parameters.} &
     \SubtypeStd{S_j}{T_j}\mbox{, for each $j \in 1..s$}}{%
     \code{$C$<\List{S}{1}{s}>}}{\code{$C$<\List{T}{1}{s}>}}
   \ExtraVSP
@@ -22209,7 +22214,8 @@ \subsubsection{Subtype Rules}
 In this specification we frequently refer to
 subtype relationships and assignability
 without mentioning the environment explicitly,
-as in \Index{\SubtypeNE{S}{T}}.
+as in
+\IndexCustom{\SubtypeNE{S}{T}}{$<:$@\SubtypeNE{S}{T}}.
 This is only done when a specific location in code is in focus,
 and it means that the environment is that which is obtained
 by mapping each type variable in scope at that location
@@ -22243,7 +22249,7 @@ \subsubsection{Being a Subtype}
 A type $S$ is shown to be a \Index{subtype} of another type $T$
 in an environment $\Delta$ by providing
 an instantiation of a rule $R$ whose conclusion is
-\IndexCustom{\SubtypeStd{S}{T}}{$\Delta$@\SubtypeStd{S}{T}},
+\IndexCustom{\SubtypeStd{S}{T}}{$\Delta<:$@\SubtypeStd{S}{T}},
 along with rule instantiations showing
 each of the premises of $R$,
 continuing until a rule with no premises is reached.
@@ -22472,9 +22478,17 @@ \subsubsection{Additional Subtyping Concepts}
 
 \LMHash{}%
 $S$ is a \Index{supertype} of $T$ in a given environment $\Delta$,
-written \SupertypeStd{S}{T},
+written
+\IndexCustom{\SupertypeStd{S}{T}}{$\Delta:>$@\SupertypeStd{S}{T}},
 if{}f \SubtypeStd{T}{S}.
 
+\LMHash{}%
+$S$ and $T$ are \Index{mutual subtypes} of each other
+in a given environment $\Delta$,
+written
+\IndexCustom{\MutualSubtypeStd{S}{T}}{$\Delta<:>$@\MutualSubtypeStd{S}{T}},
+if{}f both \SubtypeStd{T}{S} and \SubtypeStd{S}{T}.
+
 \LMHash{}%
 A type $T$
 \Index{may be assigned}
@@ -22632,7 +22646,8 @@ \subsection{Functions Dealing with Extreme Types}
 the first applicable case must be used.
 
 \LMHash{}%
-The \Index{\TopMergeTypeName} of two types computes
+The \IndexCustom{\TopMergeTypeName}{topMergeType@\TopMergeTypeName}
+of two types computes
 a canonical type which represents both of them,
 in the case where they are structurally identical
 modulo the choice among top types.
@@ -22697,7 +22712,8 @@ \subsection{Functions Dealing with Extreme Types}
 \commentary{The ordering of the arguments makes no difference.}
 
 \LMHash{}%
-The \Index{\IsTopTypeName} predicate is true for any type which is in
+The \IndexCustom{\IsTopTypeName}{isTopType@\IsTopTypeName}
+predicate is true for any type which is in
 the equivalence class of top types.
 It is a syntactic characterization of top types
 (\ref{superBoundedTypes}).
@@ -22711,8 +22727,9 @@ \subsection{Functions Dealing with Extreme Types}
 \end{itemize}
 
 \noindent
-The \Index{\IsObjectTypeName} predicate is true if{}f
-the argument is a subtype and a supertype of \code{Object}.
+The \IndexCustom{\IsObjectTypeName}{isObjectType@\IsObjectTypeName}
+predicate is true if{}f the argument is
+a subtype and a supertype of \code{Object}.
 
 \begin{itemize}
 \item \DefEquals{\IsObjectType{Object}}{\metavar{true}}.
@@ -22721,8 +22738,8 @@ \subsection{Functions Dealing with Extreme Types}
 \end{itemize}
 
 \noindent
-The \Index{\IsBottomTypeName} predicate is true if{}f
-the argument is a subtype of \code{Never}.
+The \IndexCustom{\IsBottomTypeName}{isBottomType@\IsBottomTypeName}
+predicate is true if{}f the argument is a subtype of \code{Never}.
 
 \begin{itemize}
 \item \DefEquals{\IsBottomType{Never}}{\metavar{true}}.
@@ -22732,8 +22749,9 @@ \subsection{Functions Dealing with Extreme Types}
 \end{itemize}
 
 \noindent
-The \Index{\IsNullTypeName} predicate is true if{}f
-the argument is a subtype and a supertype of \code{Null}.
+The \IndexCustom{\IsNullTypeName}{isNullType@\IsNullTypeName}
+predicate is true if{}f the argument is
+a subtype and a supertype of \code{Null}.
 
 \begin{itemize}
 \item \DefEquals{\IsNullType{Null}}{\metavar{true}}.
@@ -22742,8 +22760,8 @@ \subsection{Functions Dealing with Extreme Types}
 \end{itemize}
 
 \noindent
-The \Index{\IsMoreTopTypeName} predicate defines a total order on
-top and \code{Object} types.
+The \IndexCustom{\IsMoreTopTypeName}{isMoreTopType@\IsMoreTopTypeName}
+predicate defines a total order on top and \code{Object} types.
 
 \begin{itemize}
 \item \DefEquals{\IsMoreTopType{\VOID}{$T$}}{\metavar{true}}.
@@ -22760,8 +22778,8 @@ \subsection{Functions Dealing with Extreme Types}
 \end{itemize}
 
 \noindent
-The \Index{\IsMoreBottomTypeName} predicate defines an almost total order on
-bottom and \code{Null} types.
+The \IndexCustom{\IsMoreBottomTypeName}{isMoreBottomType@\IsMoreBottomTypeName}
+predicate defines an almost total order on bottom and \code{Null} types.
 \commentary{%
 This does not consistently order
 two different type variables with the same bound.%
@@ -22840,7 +22858,9 @@ \subsection{Type Normalization}
 }
 
 \LMHash{}%
-The function \Index{\NormalizedTypeOfName} is then defined as follows:
+The function
+\IndexCustom{\NormalizedTypeOfName}{normalizedType@\NormalizedTypeOfName}
+is then defined as follows:
 \BlindDefineSymbol{T_a, T_u, T_r}%
 Let $T_a$ be a type
 (\commentary{where `a' stands for `argument'}).