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

Author: eernstg

specification/dart.sty

@@ -465,6 +465,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

@@ -22556,18 +22556,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}\,\}\\
@@ -22577,13 +22579,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
@@ -22748,7 +22753,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
@@ -22782,7 +22788,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.
@@ -23011,9 +23017,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}
@@ -23171,7 +23185,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.
@@ -23236,7 +23251,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}).
@@ -23250,8 +23266,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}}.
@@ -23260,8 +23277,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}}.
@@ -23271,8 +23288,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}}.
@@ -23281,8 +23299,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}}.
@@ -23299,8 +23317,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.%
@@ -23379,7 +23397,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'}).