Skip to content

Commit 455a7b2

Browse files
eernstgeernstg
committed
Rebase
1 parent 56d2ce1 commit 455a7b2

File tree

1 file changed

+37
-33
lines changed

1 file changed

+37
-33
lines changed

‎specification/dartLangSpec.tex

Lines changed: 37 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -22883,104 +22883,108 @@ \subsection{Subtypes}
2288322883
\begin{figure}[p]
2288422884
\def\VSP{\vspace{4mm}}
2288522885
\def\ExtraVSP{\vspace{2mm}}
22886-
\def\Axiom#1#2#3#4{\centerline{\inference[#1]{}{\SubtypeStd{#3}{#4}}}\VSP}
22887-
\def\Rule#1#2#3#4#5#6{\centerline{\inference[#1]{\SubtypeStd{#3}{#4}}{\SubtypeStd{#5}{#6}}}\VSP}
22888-
\def\RuleTwo#1#2#3#4#5#6#7#8{%
22889-
\centerline{\inference[#1]{\SubtypeStd{#3}{#4} & \SubtypeStd{#5}{#6}}{\SubtypeStd{#7}{#8}}}\VSP}
22890-
\def\RuleRaw#1#2#3#4#5{%
22891-
\centerline{\inference[#1]{#3}{\SubtypeStd{#4}{#5}}}\VSP}
22892-
\def\RuleRawRaw#1#2#3#4{\centerline{\inference[#1]{#3}{#4}}\VSP}
22886+
\def\Axiom#1#2#3{\centerline{\inference[#1]{}{\SubtypeStd{#2}{#3}}}\VSP}
22887+
\def\Rule#1#2#3#4#5{%
22888+
\centerline{\inference[#1]{\SubtypeStd{#2}{#3}}{\SubtypeStd{#4}{#5}}}\VSP}
22889+
\def\RuleTwo#1#2#3#4#5#6#7{%
22890+
\centerline{\inference[#1]{\SubtypeStd{#2}{#3} & %
22891+
\SubtypeStd{#4}{#5}}{\SubtypeStd{#6}{#7}}}\VSP}
22892+
\def\RuleRaw#1#2#3#4{%
22893+
\centerline{\inference[#1]{#2}{\SubtypeStd{#3}{#4}}}\VSP}
22894+
\def\RuleRawRaw#1#2#3{\centerline{\inference[#1]{#2}{#3}}\VSP}
2289322895
%
2289422896
% ----------------------------------------------------------------------
2289522897
% Omitted rules stated here, with justification for
2289622898
% the omission.
2289722899
% ------------------------------------------------ Right Object 1
2289822900
% Not needed unless algorithmic: Instance of
2289922901
% \SrnLeftVariableBound.
22900-
% \RuleRaw{\SrnRightObjectOne}{Right Object 1}{%
22902+
% \RuleRaw{\SrnRightObjectOne}{%
2290122903
% \code{$X$\,\EXTENDS\,$B$} & \SubtypeStd{B}{\code{Object}}%
2290222904
% }{X}{\code{Object}}
2290322905
% ------------------------------------------------ Right Object 2
2290422906
% Not needed unless algorithmic: Instance of
2290522907
% \SrnLeftPromotedVariable.
22906-
% \RuleRaw{\SrnRightObjectTwo}{}{%
22907-
% \SubtypeStd{S}{\code{Object}}}{\code{$X$\,\&\,$S$}}{\code{Object}}
22908+
% \RuleRaw{\SrnRightObjectTwo}{%
22909+
% \SubtypeStd{S}{\code{Object}}}{%
22910+
% \code{$X$\,\&\,$S$}}{\code{Object}}
2290822911
% ------------------------------------------------ Right Object 3
2290922912
% Not needed unless algorithmic: Derivable from
2291022913
% \SrnLeftFutureOr{} and \SrnRightObjectFour{} (to get
2291122914
% Future<S> <: Object).
22912-
% \RuleRaw{\SrnRightObjectThree}{}{%
22913-
% \SubtypeStd{S}{\code{Object}}}{\code{FutureOr<$S$>}}{\code{Object}}
22915+
% \RuleRaw{\SrnRightObjectThree}{%
22916+
% \SubtypeStd{S}{\code{Object}}}{%
22917+
% \code{FutureOr<$S$>}}{\code{Object}}
2291422918
% ----------------------------------------------------------------------
2291522919
\begin{minipage}[c]{0.49\textwidth}
2291622920
% ------------------------------------------------ Reflexivity
22917-
\Axiom{\SrnReflexivity}{}{T}{T}
22921+
\Axiom{\SrnReflexivity}{T}{T}
2291822922
\ExtraVSP
2291922923
% ------------------------------------------------ Left Top
2292022924
% Non-algorithmic justification for this rule: Needed
2292122925
% to prove dynamic/void <: FutureOr<Object>?.
22922-
\RuleRaw{\SrnLeftTop}{}{%
22926+
\RuleRaw{\SrnLeftTop}{%
2292322927
S \in \{\DYNAMIC, \VOID\}\\
2292422928
\SubtypeStd{\code{Object?}}{T}}{S}{T}
2292522929
% ------------------------------------------------ Left Bottom
22926-
\Axiom{\SrnBottom}{}{\code{Never}}{T}
22930+
\Axiom{\SrnBottom}{\code{Never}}{T}
2292722931
% ------------------------------------------------ Left Null 1
22928-
\Axiom{\SrnNullOne}{}{\code{Null}}{\code{$T$?}}
22932+
\Axiom{\SrnNullOne}{\code{Null}}{\code{$T$?}}
2292922933
\end{minipage}
2293022934
\begin{minipage}[c]{0.49\textwidth}
2293122935
% ------------------------------------------------ Right Top
22932-
\RuleRaw{\SrnRightTop}{}{%
22936+
\RuleRaw{\SrnRightTop}{%
2293322937
T \in \{\code{Object?}, \DYNAMIC, \VOID\}}{S}{T}
2293422938
% ------------------------------------------------ Right Object 4
22935-
\RuleRaw{\SrnRightObjectFour}{}{%
22939+
\RuleRaw{\SrnRightObjectFour}{%
2293622940
$S$\,\not\in \{\code{Null}, \DYNAMIC, \VOID\}\\
2293722941
\mbox{$S$ is not of the form \code{$U$?}, $X$,}\\
2293822942
\mbox{\code{$X$\,\&\,$U$}, %
2293922943
or \code{FutureOr<$U$>}}}{S}{\code{Object}}
2294022944
% ------------------------------------------------ Left Null 2
22941-
\Rule{\SrnNullTwo}{}{\code{Null}}{T}{%
22945+
\Rule{\SrnNullTwo}{\code{Null}}{T}{%
2294222946
\code{Null}}{\code{FutureOr<$T$>}}
2294322947
\end{minipage}
2294422948

2294522949
\begin{minipage}[c]{0.49\textwidth}
2294622950
% ------------------------------------------------ Left FutureOr
22947-
\RuleTwo{\SrnLeftFutureOr}{}{%
22951+
\RuleTwo{\SrnLeftFutureOr}{%
2294822952
\code{Future<$S$>}}{T}{S}{T}{%
2294922953
\code{FutureOr<$S$>}}{T}
2295022954
% ------------------------------------------------ Right Promoted Variable
22951-
\RuleTwo{\SrnRightPromotedVariable}{}{S}{X}{S}{T}{%
22955+
\RuleTwo{\SrnRightPromotedVariable}{S}{X}{S}{T}{%
2295222956
S}{X \& T}
2295322957
% ------------------------------------------------ Right FutureOr B
22954-
\Rule{\SrnRightFutureOrB}{}{S}{T}{S}{%
22958+
\Rule{\SrnRightFutureOrB}{S}{T}{S}{%
2295522959
\code{FutureOr<$T$>}}
2295622960
% ------------------------------------------------ Right Nullable 2
22957-
\Rule{\SrnRightNullableTwo}{}{S}{\code{Null}}{S}{%
22961+
\Rule{\SrnRightNullableTwo}{S}{\code{Null}}{S}{%
2295822962
\code{$T$?}}
2295922963
% ------------------------------------------------ Left Variable Bound
2296022964
\Rule{\SrnLeftVariableBound}{}{\Delta(X)}{T}{X}{T}
2296122965
\end{minipage}
2296222966
\begin{minipage}[c]{0.49\textwidth}
2296322967
% ------------------------------------------------ Left Nullable
22964-
\RuleTwo{\SrnLeftNullable}{}{S}{T}{\code{Null}}{T}{%
22968+
\RuleTwo{\SrnLeftNullable}{S}{T}{\code{Null}}{T}{%
2296522969
\code{$S$?}}{T}
2296622970
% ------------------------------------------------ Left Promoted Variable A
22967-
\Axiom{\SrnTypeVariableReflexivityA}{}{X \& S}{X}
22971+
\Axiom{\SrnTypeVariableReflexivityA}{X \& S}{X}
2296822972
% ------------------------------------------------ Right FutureOr A
22969-
\Rule{\SrnRightFutureOrA}{}{S}{%
22973+
\Rule{\SrnRightFutureOrA}{S}{%
2297022974
\code{Future<$T$>}}{S}{\code{FutureOr<$T$>}}
2297122975
% ------------------------------------------------ Right Nullable 1
22972-
\Rule{\SrnRightNullableOne}{}{S}{T}{S}{\code{$T$?}}
22976+
\Rule{\SrnRightNullableOne}{S}{T}{S}{\code{$T$?}}
2297322977
% ------------------------------------------------ Left Promoted Variable B
22974-
\Rule{\SrnLeftPromotedVariable}{}{S}{T}{X \& S}{T}
22978+
\Rule{\SrnLeftPromotedVariable}{S}{T}{X \& S}{T}
2297522979
% ------------------------------------------------ Right Function
22976-
\RuleRaw{\SrnRightFunction}{}{%
22980+
\RuleRaw{\SrnRightFunction}{%
2297722981
T\mbox{ is a function type}}{T}{\FUNCTION}
2297822982
\end{minipage}
2297922983
%
2298022984
\ExtraVSP
2298122985
% ------------------------------------------------ Positional Function Type
2298222986
\RuleRawRaw{\SrnPositionalFunctionType}{}{%
22983-
\Gamma' = \Delta\uplus\{X_i\mapsto{}B_i\,|\,1 \leq i \leq s\} &
22987+
\Delta' = \Delta\uplus\{X_i\mapsto{}B_i\,|\,1 \leq i \leq s\} &
2298422988
\Subtype{\Delta'}{S_0}{T_0} \\
2298522989
n_1 \leq n_2 &
2298622990
n_1 + k_1 \geq n_2 + k_2 &
@@ -22992,7 +22996,7 @@ \subsection{Subtypes}
2299222996
\ExtraVSP\ExtraVSP
2299322997
% ------------------------------------------------ Named Function Type
2299422998
\RuleRawRaw{\SrnNamedFunctionType}{}{%
22995-
\Gamma' = \Delta\uplus\{X_i\mapsto{}B_i\,|\,1 \leq i \leq s\} &
22999+
\Delta' = \Delta\uplus\{X_i\mapsto{}B_i\,|\,1 \leq i \leq s\} &
2299623000
\Subtype{\Delta'}{S_0}{T_0} &
2299723001
\forall j \in 1 .. n\!:\;\Subtype{\Gamma'}{T_j}{S_j} \\
2299823002
\{\,\List{y}{n+1}{n+k_2}\,\} \subseteq \{\,\List{x}{n+1}{n+k_1}\,\} \\
@@ -23005,13 +23009,13 @@ \subsection{Subtypes}
2300523009
%
2300623010
\ExtraVSP
2300723011
% ------------------------------------------------ Covariance
23008-
\RuleRaw{\SrnCovariance}{}{%
23012+
\RuleRaw{\SrnCovariance}{%
2300923013
\mbox{$C$ is an interface type with $s$ type parameters} &
2301023014
\SubtypeStd{S_j}{T_j}\mbox{, for each $j \in 1..s$}}{%
2301123015
\code{$C$<\List{S}{1}{s}>}}{\code{$C$<\List{T}{1}{s}>}}
2301223016
\ExtraVSP
2301323017
% ------------------------------------------------ Superinterface
23014-
\RuleRaw{\SrnSuperinterface}{}{%
23018+
\RuleRaw{\SrnSuperinterface}{%
2301523019
\mbox{$C$ is an interface type with type parameters \List{X}{1}{s}}\\
2301623020
\Superinterface{\code{$D$<\List{T}{1}{m}>}}{C} &
2301723021
\SubtypeStd{[S_1/X_1,\ldots,S_s/X_s]\code{$D$<\List{T}{1}{m}>}}{T}}{%

0 commit comments

Comments
 (0)