Skip to content

Commit b9c009e

Browse files
eernstgeernstg
committed
Rebase
1 parent 3c30bdf commit b9c009e

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
@@ -22432,104 +22432,108 @@ \subsection{Subtypes}
2243222432
\begin{figure}[p]
2243322433
\def\VSP{\vspace{4mm}}
2243422434
\def\ExtraVSP{\vspace{2mm}}
22435-
\def\Axiom#1#2#3#4{\centerline{\inference[#1]{}{\SubtypeStd{#3}{#4}}}\VSP}
22436-
\def\Rule#1#2#3#4#5#6{\centerline{\inference[#1]{\SubtypeStd{#3}{#4}}{\SubtypeStd{#5}{#6}}}\VSP}
22437-
\def\RuleTwo#1#2#3#4#5#6#7#8{%
22438-
\centerline{\inference[#1]{\SubtypeStd{#3}{#4} & \SubtypeStd{#5}{#6}}{\SubtypeStd{#7}{#8}}}\VSP}
22439-
\def\RuleRaw#1#2#3#4#5{%
22440-
\centerline{\inference[#1]{#3}{\SubtypeStd{#4}{#5}}}\VSP}
22441-
\def\RuleRawRaw#1#2#3#4{\centerline{\inference[#1]{#3}{#4}}\VSP}
22435+
\def\Axiom#1#2#3{\centerline{\inference[#1]{}{\SubtypeStd{#2}{#3}}}\VSP}
22436+
\def\Rule#1#2#3#4#5{%
22437+
\centerline{\inference[#1]{\SubtypeStd{#2}{#3}}{\SubtypeStd{#4}{#5}}}\VSP}
22438+
\def\RuleTwo#1#2#3#4#5#6#7{%
22439+
\centerline{\inference[#1]{\SubtypeStd{#2}{#3} & %
22440+
\SubtypeStd{#4}{#5}}{\SubtypeStd{#6}{#7}}}\VSP}
22441+
\def\RuleRaw#1#2#3#4{%
22442+
\centerline{\inference[#1]{#2}{\SubtypeStd{#3}{#4}}}\VSP}
22443+
\def\RuleRawRaw#1#2#3{\centerline{\inference[#1]{#2}{#3}}\VSP}
2244222444
%
2244322445
% ----------------------------------------------------------------------
2244422446
% Omitted rules stated here, with justification for
2244522447
% the omission.
2244622448
% ------------------------------------------------ Right Object 1
2244722449
% Not needed unless algorithmic: Instance of
2244822450
% \SrnLeftVariableBound.
22449-
% \RuleRaw{\SrnRightObjectOne}{Right Object 1}{%
22451+
% \RuleRaw{\SrnRightObjectOne}{%
2245022452
% \code{$X$\,\EXTENDS\,$B$} & \SubtypeStd{B}{\code{Object}}%
2245122453
% }{X}{\code{Object}}
2245222454
% ------------------------------------------------ Right Object 2
2245322455
% Not needed unless algorithmic: Instance of
2245422456
% \SrnLeftPromotedVariable.
22455-
% \RuleRaw{\SrnRightObjectTwo}{}{%
22456-
% \SubtypeStd{S}{\code{Object}}}{\code{$X$\,\&\,$S$}}{\code{Object}}
22457+
% \RuleRaw{\SrnRightObjectTwo}{%
22458+
% \SubtypeStd{S}{\code{Object}}}{%
22459+
% \code{$X$\,\&\,$S$}}{\code{Object}}
2245722460
% ------------------------------------------------ Right Object 3
2245822461
% Not needed unless algorithmic: Derivable from
2245922462
% \SrnLeftFutureOr{} and \SrnRightObjectFour{} (to get
2246022463
% Future<S> <: Object).
22461-
% \RuleRaw{\SrnRightObjectThree}{}{%
22462-
% \SubtypeStd{S}{\code{Object}}}{\code{FutureOr<$S$>}}{\code{Object}}
22464+
% \RuleRaw{\SrnRightObjectThree}{%
22465+
% \SubtypeStd{S}{\code{Object}}}{%
22466+
% \code{FutureOr<$S$>}}{\code{Object}}
2246322467
% ----------------------------------------------------------------------
2246422468
\begin{minipage}[c]{0.49\textwidth}
2246522469
% ------------------------------------------------ Reflexivity
22466-
\Axiom{\SrnReflexivity}{}{T}{T}
22470+
\Axiom{\SrnReflexivity}{T}{T}
2246722471
\ExtraVSP
2246822472
% ------------------------------------------------ Left Top
2246922473
% Non-algorithmic justification for this rule: Needed
2247022474
% to prove dynamic/void <: FutureOr<Object>?.
22471-
\RuleRaw{\SrnLeftTop}{}{%
22475+
\RuleRaw{\SrnLeftTop}{%
2247222476
S \in \{\DYNAMIC, \VOID\}\\
2247322477
\SubtypeStd{\code{Object?}}{T}}{S}{T}
2247422478
% ------------------------------------------------ Left Bottom
22475-
\Axiom{\SrnBottom}{}{\code{Never}}{T}
22479+
\Axiom{\SrnBottom}{\code{Never}}{T}
2247622480
% ------------------------------------------------ Left Null 1
22477-
\Axiom{\SrnNullOne}{}{\code{Null}}{\code{$T$?}}
22481+
\Axiom{\SrnNullOne}{\code{Null}}{\code{$T$?}}
2247822482
\end{minipage}
2247922483
\begin{minipage}[c]{0.49\textwidth}
2248022484
% ------------------------------------------------ Right Top
22481-
\RuleRaw{\SrnRightTop}{}{%
22485+
\RuleRaw{\SrnRightTop}{%
2248222486
T \in \{\code{Object?}, \DYNAMIC, \VOID\}}{S}{T}
2248322487
% ------------------------------------------------ Right Object 4
22484-
\RuleRaw{\SrnRightObjectFour}{}{%
22488+
\RuleRaw{\SrnRightObjectFour}{%
2248522489
$S$\,\not\in \{\code{Null}, \DYNAMIC, \VOID\}\\
2248622490
\mbox{$S$ is not of the form \code{$U$?}, $X$,}\\
2248722491
\mbox{\code{$X$\,\&\,$U$}, %
2248822492
or \code{FutureOr<$U$>}}}{S}{\code{Object}}
2248922493
% ------------------------------------------------ Left Null 2
22490-
\Rule{\SrnNullTwo}{}{\code{Null}}{T}{%
22494+
\Rule{\SrnNullTwo}{\code{Null}}{T}{%
2249122495
\code{Null}}{\code{FutureOr<$T$>}}
2249222496
\end{minipage}
2249322497

2249422498
\begin{minipage}[c]{0.49\textwidth}
2249522499
% ------------------------------------------------ Left FutureOr
22496-
\RuleTwo{\SrnLeftFutureOr}{}{%
22500+
\RuleTwo{\SrnLeftFutureOr}{%
2249722501
\code{Future<$S$>}}{T}{S}{T}{%
2249822502
\code{FutureOr<$S$>}}{T}
2249922503
% ------------------------------------------------ Right Promoted Variable
22500-
\RuleTwo{\SrnRightPromotedVariable}{}{S}{X}{S}{T}{%
22504+
\RuleTwo{\SrnRightPromotedVariable}{S}{X}{S}{T}{%
2250122505
S}{X \& T}
2250222506
% ------------------------------------------------ Right FutureOr B
22503-
\Rule{\SrnRightFutureOrB}{}{S}{T}{S}{%
22507+
\Rule{\SrnRightFutureOrB}{S}{T}{S}{%
2250422508
\code{FutureOr<$T$>}}
2250522509
% ------------------------------------------------ Right Nullable 2
22506-
\Rule{\SrnRightNullableTwo}{}{S}{\code{Null}}{S}{%
22510+
\Rule{\SrnRightNullableTwo}{S}{\code{Null}}{S}{%
2250722511
\code{$T$?}}
2250822512
% ------------------------------------------------ Left Variable Bound
2250922513
\Rule{\SrnLeftVariableBound}{}{\Delta(X)}{T}{X}{T}
2251022514
\end{minipage}
2251122515
\begin{minipage}[c]{0.49\textwidth}
2251222516
% ------------------------------------------------ Left Nullable
22513-
\RuleTwo{\SrnLeftNullable}{}{S}{T}{\code{Null}}{T}{%
22517+
\RuleTwo{\SrnLeftNullable}{S}{T}{\code{Null}}{T}{%
2251422518
\code{$S$?}}{T}
2251522519
% ------------------------------------------------ Left Promoted Variable A
22516-
\Axiom{\SrnTypeVariableReflexivityA}{}{X \& S}{X}
22520+
\Axiom{\SrnTypeVariableReflexivityA}{X \& S}{X}
2251722521
% ------------------------------------------------ Right FutureOr A
22518-
\Rule{\SrnRightFutureOrA}{}{S}{%
22522+
\Rule{\SrnRightFutureOrA}{S}{%
2251922523
\code{Future<$T$>}}{S}{\code{FutureOr<$T$>}}
2252022524
% ------------------------------------------------ Right Nullable 1
22521-
\Rule{\SrnRightNullableOne}{}{S}{T}{S}{\code{$T$?}}
22525+
\Rule{\SrnRightNullableOne}{S}{T}{S}{\code{$T$?}}
2252222526
% ------------------------------------------------ Left Promoted Variable B
22523-
\Rule{\SrnLeftPromotedVariable}{}{S}{T}{X \& S}{T}
22527+
\Rule{\SrnLeftPromotedVariable}{S}{T}{X \& S}{T}
2252422528
% ------------------------------------------------ Right Function
22525-
\RuleRaw{\SrnRightFunction}{}{%
22529+
\RuleRaw{\SrnRightFunction}{%
2252622530
T\mbox{ is a function type}}{T}{\FUNCTION}
2252722531
\end{minipage}
2252822532
%
2252922533
\ExtraVSP
2253022534
% ------------------------------------------------ Positional Function Type
2253122535
\RuleRawRaw{\SrnPositionalFunctionType}{}{%
22532-
\Gamma' = \Delta\uplus\{X_i\mapsto{}B_i\,|\,1 \leq i \leq s\} &
22536+
\Delta' = \Delta\uplus\{X_i\mapsto{}B_i\,|\,1 \leq i \leq s\} &
2253322537
\Subtype{\Delta'}{S_0}{T_0} \\
2253422538
n_1 \leq n_2 &
2253522539
n_1 + k_1 \geq n_2 + k_2 &
@@ -22541,7 +22545,7 @@ \subsection{Subtypes}
2254122545
\ExtraVSP\ExtraVSP
2254222546
% ------------------------------------------------ Named Function Type
2254322547
\RuleRawRaw{\SrnNamedFunctionType}{}{%
22544-
\Gamma' = \Delta\uplus\{X_i\mapsto{}B_i\,|\,1 \leq i \leq s\} &
22548+
\Delta' = \Delta\uplus\{X_i\mapsto{}B_i\,|\,1 \leq i \leq s\} &
2254522549
\Subtype{\Delta'}{S_0}{T_0} &
2254622550
\forall j \in 1 .. n\!:\;\Subtype{\Gamma'}{T_j}{S_j} \\
2254722551
\{\,\List{y}{n+1}{n+k_2}\,\} \subseteq \{\,\List{x}{n+1}{n+k_1}\,\} \\
@@ -22554,13 +22558,13 @@ \subsection{Subtypes}
2255422558
%
2255522559
\ExtraVSP
2255622560
% ------------------------------------------------ Covariance
22557-
\RuleRaw{\SrnCovariance}{}{%
22561+
\RuleRaw{\SrnCovariance}{%
2255822562
\mbox{$C$ is an interface type with $s$ type parameters} &
2255922563
\SubtypeStd{S_j}{T_j}\mbox{, for each $j \in 1..s$}}{%
2256022564
\code{$C$<\List{S}{1}{s}>}}{\code{$C$<\List{T}{1}{s}>}}
2256122565
\ExtraVSP
2256222566
% ------------------------------------------------ Superinterface
22563-
\RuleRaw{\SrnSuperinterface}{}{%
22567+
\RuleRaw{\SrnSuperinterface}{%
2256422568
\mbox{$C$ is an interface type with type parameters \List{X}{1}{s}}\\
2256522569
\Superinterface{\code{$D$<\List{T}{1}{m}>}}{C} &
2256622570
\SubtypeStd{[S_1/X_1,\ldots,S_s/X_s]\code{$D$<\List{T}{1}{m}>}}{T}}{%

0 commit comments

Comments
 (0)