Skip to content

Commit

Permalink
Update command \flatten to \Flatten
Browse files Browse the repository at this point in the history
  • Loading branch information
eernstg committed Nov 25, 2024
1 parent ed08d91 commit 8f0fb8e
Showing 1 changed file with 41 additions and 41 deletions.
82 changes: 41 additions & 41 deletions specification/dartLangSpec.tex
Original file line number Diff line number Diff line change
Expand Up @@ -2058,7 +2058,7 @@ \section{Functions}
that the returned object will not be used
(\ref{return}).%
}
\item The function is asynchronous, \flatten{T} is not \VOID,
\item The function is asynchronous, \Flatten{T} is not \VOID,
and it would have been a compile-time error
to declare the function with the body
\code{\ASYNC{} \{ \RETURN{} $e$; \}}
Expand Down Expand Up @@ -11789,7 +11789,7 @@ \subsection{Function Expressions}
\commentary{%
There is no rule for the case where $T$ is of the form \code{$X$\,\&\,$S$}
because this will never occur
(this concept is only used in \flattenName, which is defined below).%
(this concept is only used in \FlattenName, which is defined below).%
}
\end{itemize}

Expand Down Expand Up @@ -11844,7 +11844,7 @@ \subsection{Function Expressions}

\LMHash{}%
We define the auxiliary function
\IndexCustom{\flatten{T}}{flatten(t)@\emph{flatten}$(T)$}
\IndexCustom{\Flatten{T}}{flatten(t)@\emph{flatten}$(T)$}
as follows, using the first applicable case:

\begin{itemize}
Expand All @@ -11853,60 +11853,60 @@ \subsection{Function Expressions}
for some type variable $X$ and type $S$ then
\begin{itemize}
\item if $S$ derives a future type $U$
then \DefEquals{\flatten{T}}{\code{\flatten{U}}}.
then \DefEquals{\Flatten{T}}{\code{\Flatten{U}}}.
\item otherwise,
\DefEquals{\flatten{T}}{\code{\flatten{X}}}.
\DefEquals{\Flatten{T}}{\code{\Flatten{X}}}.
\end{itemize}

\item If $T$ derives a future type \code{Future<$S$>}
or \code{FutureOr<$S$>}
then \DefEquals{\flatten{T}}{S}.
then \DefEquals{\Flatten{T}}{S}.

\item If $T$ derives a future type \code{Future<$S$>?}\ or
\code{FutureOr<$S$>?}\ then \DefEquals{\flatten{T}}{\code{$S$?}}.
\code{FutureOr<$S$>?}\ then \DefEquals{\Flatten{T}}{\code{$S$?}}.

\item Otherwise, \DefEquals{\flatten{T}}{T}.
\item Otherwise, \DefEquals{\Flatten{T}}{T}.
\end{itemize}

\rationale{%
This definition guarantees that for any type $T$,
\code{$T <:$ FutureOr<$\flatten{T}$>}. The proof is by induction on the
\code{$T <:$ FutureOr<$\Flatten{T}$>}. The proof is by induction on the
structure of $T$:

\begin{itemize}
\item If $T$ is \code{$X$\,\&\,$S$} then
\begin{itemize}
\item if $S$ derives a future type $U$,
then \code{$T <: S$} and \code{$S <: U$}, so \code{$T <: U$}.
By the induction hypothesis, \code{$U <:$ FutureOr<$\flatten{U}$>}.
Since \code{$\flatten{T} = \flatten{U}$} in this case, it follows that
\code{$U <:$ FutureOr<$\flatten{T}$>}, and so
\code{$T <:$ FutureOr<$\flatten{T}$>}.
By the induction hypothesis, \code{$U <:$ FutureOr<$\Flatten{U}$>}.
Since \code{$\Flatten{T} = \Flatten{U}$} in this case, it follows that
\code{$U <:$ FutureOr<$\Flatten{T}$>}, and so
\code{$T <:$ FutureOr<$\Flatten{T}$>}.
\item otherwise, \code{$T <: X$}.
By the induction hypothesis, \code{$X <:$ FutureOr<$\flatten{X}$>}.
Since \code{$\flatten{T} = \flatten{X}$} in this case, it follows that
\code{$U <:$ FutureOr<$\flatten{T}$>}, and so
\code{$T <:$ FutureOr<$\flatten{T}$>}.
By the induction hypothesis, \code{$X <:$ FutureOr<$\Flatten{X}$>}.
Since \code{$\Flatten{T} = \Flatten{X}$} in this case, it follows that
\code{$U <:$ FutureOr<$\Flatten{T}$>}, and so
\code{$T <:$ FutureOr<$\Flatten{T}$>}.
\end{itemize}

\item If $T$ derives a future type \code{Future<$S$>}
or \code{FutureOr<$S$>}, then, since \code{Future<$S$> $<:$ FutureOr<$S$>},
it follows that \code{$T <:$ FutureOr<$S$>}. Since \code{$\flatten{T} = S$}
in this case, it follows that \code{$T <:$ FutureOr<$\flatten{T}$>}.
it follows that \code{$T <:$ FutureOr<$S$>}. Since \code{$\Flatten{T} = S$}
in this case, it follows that \code{$T <:$ FutureOr<$\Flatten{T}$>}.

\item If $T$ derives a future type \code{Future<$S$>?} or
\code{FutureOr<$S$>?}, then, since \code{Future<$S$>? $<:$ FutureOr<$S$>?},
it follows that \code{$T <:$ FutureOr<$S$>?}.
\code{FutureOr<$S$>? $<:$ FutureOr<$S$?>} for any type $S$ (this can be shown
using the union type subtype rules and from
\code{Future<$S$> $<:$ Future<$S$?>} by covariance), so by transivitity,
\code{$T <:$ FutureOr<$S$?>}. Since \code{$\flatten{T} = S$?} in this case,
it follows that \code{$T <:$ FutureOr<$\flatten{T}$>}.
\code{$T <:$ FutureOr<$S$?>}. Since \code{$\Flatten{T} = S$?} in this case,
it follows that \code{$T <:$ FutureOr<$\Flatten{T}$>}.

\item Otherwise, \code{$\flatten{T} = T$}, so
\code{FutureOr<$\flatten{T}$> $=$ FutureOr<$T$>}. Since
\item Otherwise, \code{$\Flatten{T} = T$}, so
\code{FutureOr<$\Flatten{T}$> $=$ FutureOr<$T$>}. Since
\code{$T <:$ FutureOr<$T$>}, it follows that
\code{$T <:$ FutureOr<$\flatten{T}$>}.
\code{$T <:$ FutureOr<$\Flatten{T}$>}.
\end{itemize}
}

Expand Down Expand Up @@ -11941,7 +11941,7 @@ \subsection{Function Expressions}

\noindent
is
\FunctionTypePositionalStdCr{\code{Future<\flatten{T_0}>}},
\FunctionTypePositionalStdCr{\code{Future<\Flatten{T_0}>}},

\noindent
where $T_0$ is the static type of $e$.
Expand Down Expand Up @@ -11977,7 +11977,7 @@ \subsection{Function Expressions}

\noindent
is
\FunctionTypeNamedStdCr{\code{Future<\flatten{T_0}>}},
\FunctionTypeNamedStdCr{\code{Future<\Flatten{T_0}>}},

\noindent
where $T_0$ is the static type of $e$.
Expand Down Expand Up @@ -16765,13 +16765,13 @@ \subsection{Await Expressions}
\BlindDefineSymbol{a, e, S}%
Let $a$ be an expression of the form \code{\AWAIT\,\,$e$}.
Let $S$ be the static type of $e$.
The static type of $a$ is then \flatten{S}
The static type of $a$ is then \Flatten{S}
(\ref{functionExpressions}).

\LMHash{}%
Evaluation of $a$ proceeds as follows:
First, the expression $e$ is evaluated to an object $o$.
Let \DefineSymbol{T} be \flatten{S}.
Let \DefineSymbol{T} be \Flatten{S}.
If the run-time type of $o$ is a subtype of \code{Future<$T$>},
then let \DefineSymbol{f} be $o$;
otherwise let $f$ be the result of creating
Expand All @@ -16792,7 +16792,7 @@ \subsection{Await Expressions}
If $f$ completes with an object $v$, $a$ evaluates to $v$.

\rationale{%
The use of \flattenName{} to find $T$ and hence determine the dynamic type test
The use of \FlattenName{} to find $T$ and hence determine the dynamic type test
implies that we await a future in every case where this choice is sound.%
}

Expand All @@ -16808,7 +16808,7 @@ \subsection{Await Expressions}
However, the second kind could be a \code{Future<Object?>}.
This object isn't a \code{Future<Object>}, and it isn't \NULL,
so it \emph{must} be considered to be in the second group.
Nevertheless, \flatten{\code{FutureOr<Object>?}} is \code{Object?},
Nevertheless, \Flatten{\code{FutureOr<Object>?}} is \code{Object?},
so we \emph{will} await a \code{Future<Object?>}.
We have chosen this semantics because it was the smallest breaking change
relative to the semantics in earlier versions of Dart,
Expand Down Expand Up @@ -19240,7 +19240,7 @@ \subsection{Return}
%
% Returning without an object is only ok for async-"voidy" return types.
It is a compile-time error if $s$ is \code{\RETURN;},
unless \flatten{T}
unless \Flatten{T}
(\ref{functionExpressions})
is \VOID, \DYNAMIC, or \code{Null}.
%
Expand All @@ -19253,26 +19253,26 @@ \subsection{Return}
% Returning with an object in an void async function only ok
% when that value is async-"voidy".
It is a compile-time error if $s$ is \code{\RETURN{} $e$;},
\flatten{T} is \VOID,
and \flatten{S} is neither \VOID, \DYNAMIC, nor \code{Null}.
\Flatten{T} is \VOID,
and \Flatten{S} is neither \VOID, \DYNAMIC, nor \code{Null}.
%
% Returning async-void in a "non-async-voidy" function is an error.
It is a compile-time error if $s$ is \code{\RETURN{} $e$;},
\flatten{T} is neither \VOID, \DYNAMIC, nor \code{Null},
and \flatten{S} is \VOID.
\Flatten{T} is neither \VOID, \DYNAMIC, nor \code{Null},
and \Flatten{S} is \VOID.
%
% Otherwise, returning an un-deasync-assignable value is an error.
It is a compile-time error if $s$ is \code{\RETURN{} $e$;},
\flatten{S} is not \VOID,
and \code{Future<\flatten{S}>} is not assignable to $T$.
\Flatten{S} is not \VOID,
and \code{Future<\Flatten{S}>} is not assignable to $T$.

\commentary{%
Note that \flatten{T} cannot be \VOID, \DYNAMIC, or \code{Null}
Note that \Flatten{T} cannot be \VOID, \DYNAMIC, or \code{Null}
in the last case,
because then \code{Future<$U$>} is assignable to $T$ for \emph{all} $U$.
In particular, when $T$ is \code{FutureOr<Null>}
(which is equivalent to \code{Future<Null>}),
\code{Future<\flatten{S}>} is assignable to $T$ for all $S$.
\code{Future<\Flatten{S}>} is assignable to $T$ for all $S$.
This means that no compile-time error is raised,
but \emph{only} the null object (\ref{null})
or an instance of \code{Future<Null>} can successfully be returned at run time.
Expand All @@ -19283,7 +19283,7 @@ \subsection{Return}

An error will not be raised if $f$ has no declared return type,
since the return type would be \DYNAMIC,
and \code{Future<\flatten{S}>} is assignable to \DYNAMIC{} for all $S$.
and \code{Future<\Flatten{S}>} is assignable to \DYNAMIC{} for all $S$.
However, an asynchronous non-generator function
that declares a return type which is not ``voidy''
must return an expression explicitly.%
Expand Down Expand Up @@ -19334,7 +19334,7 @@ \subsection{Return}
let $T$ be the actual return type of $f$
(\ref{actualTypes}).
If the body of $f$ is marked \ASYNC{} (\ref{functions})
and $S$ is a subtype of \code{Future<\flatten{T}>}
and $S$ is a subtype of \code{Future<\Flatten{T}>}
then let $r$ be the result of evaluating \code{await $v$}
where $v$ is a fresh variable bound to $o$.
Otherwise let $r$ be $o$.
Expand Down

0 comments on commit 8f0fb8e

Please sign in to comment.