@@ -21913,103 +21913,107 @@ \subsection{Subtypes}
21913
21913
\begin{figure}[p]
21914
21914
\def\VSP{\vspace{4mm}}
21915
21915
\def\ExtraVSP{\vspace{2mm}}
21916
- \def\Axiom#1#2#3#4{\centerline{\inference[#1]{}{\SubtypeStd{#3}{#4}}}\VSP}
21917
- \def\Rule#1#2#3#4#5#6{\centerline{\inference[#1]{\SubtypeStd{#3}{#4}}{\SubtypeStd{#5}{#6}}}\VSP}
21918
- \def\RuleTwo#1#2#3#4#5#6#7#8{%
21919
- \centerline{\inference[#1]{\SubtypeStd{#3}{#4} & \SubtypeStd{#5}{#6}}{\SubtypeStd{#7}{#8}}}\VSP}
21920
- \def\RuleRaw#1#2#3#4#5{%
21921
- \centerline{\inference[#1]{#3}{\SubtypeStd{#4}{#5}}}\VSP}
21922
- \def\RuleRawRaw#1#2#3#4{\centerline{\inference[#1]{#3}{#4}}\VSP}
21916
+ \def\Axiom#1#2#3{\centerline{\inference[#1]{}{\SubtypeStd{#2}{#3}}}\VSP}
21917
+ \def\Rule#1#2#3#4#5{%
21918
+ \centerline{\inference[#1]{\SubtypeStd{#2}{#3}}{\SubtypeStd{#4}{#5}}}\VSP}
21919
+ \def\RuleTwo#1#2#3#4#5#6#7{%
21920
+ \centerline{\inference[#1]{\SubtypeStd{#2}{#3} & %
21921
+ \SubtypeStd{#4}{#5}}{\SubtypeStd{#6}{#7}}}\VSP}
21922
+ \def\RuleRaw#1#2#3#4{%
21923
+ \centerline{\inference[#1]{#2}{\SubtypeStd{#3}{#4}}}\VSP}
21924
+ \def\RuleRawRaw#1#2#3{\centerline{\inference[#1]{#2}{#3}}\VSP}
21923
21925
%
21924
21926
% ----------------------------------------------------------------------
21925
21927
% Omitted rules stated here, with justification for
21926
21928
% the omission.
21927
21929
% ------------------------------------------------ Right Object 1
21928
21930
% Not needed unless algorithmic: Instance of
21929
21931
% \SrnLeftVariableBound.
21930
- % \RuleRaw{\SrnRightObjectOne}{Right Object 1}{ %
21932
+ % \RuleRaw{\SrnRightObjectOne}{%
21931
21933
% \code{$X$\,\EXTENDS\,$B$} & \SubtypeStd{B}{\code{Object}}%
21932
21934
% }{X}{\code{Object}}
21933
21935
% ------------------------------------------------ Right Object 2
21934
21936
% Not needed unless algorithmic: Instance of
21935
21937
% \SrnLeftPromotedVariable.
21936
- % \RuleRaw{\SrnRightObjectTwo}{}{%
21937
- % \SubtypeStd{S}{\code{Object}}}{\code{$X$\,\&\,$S$}}{\code{Object}}
21938
+ % \RuleRaw{\SrnRightObjectTwo}{%
21939
+ % \SubtypeStd{S}{\code{Object}}}{%
21940
+ % \code{$X$\,\&\,$S$}}{\code{Object}}
21938
21941
% ------------------------------------------------ Right Object 3
21939
21942
% Not needed unless algorithmic: Derivable from
21940
21943
% \SrnLeftFutureOr{} and \SrnRightObjectFour{} (to get
21941
21944
% Future<S> <: Object).
21942
- % \RuleRaw{\SrnRightObjectThree}{}{%
21943
- % \SubtypeStd{S}{\code{Object}}}{\code{FutureOr<$S$>}}{\code{Object}}
21945
+ % \RuleRaw{\SrnRightObjectThree}{%
21946
+ % \SubtypeStd{S}{\code{Object}}}{%
21947
+ % \code{FutureOr<$S$>}}{\code{Object}}
21944
21948
% ----------------------------------------------------------------------
21945
21949
\begin{minipage}[c]{0.49\textwidth}
21946
21950
% ------------------------------------------------ Reflexivity
21947
- \Axiom{\SrnReflexivity}{}{ T}{T}
21951
+ \Axiom{\SrnReflexivity}{T}{T}
21948
21952
\ExtraVSP
21949
21953
% ------------------------------------------------ Left Top
21950
21954
% Non-algorithmic justification for this rule: Needed
21951
21955
% to prove dynamic/void <: FutureOr<Object>?.
21952
- \RuleRaw{\SrnLeftTop}{}{ %
21956
+ \RuleRaw{\SrnLeftTop}{%
21953
21957
S \in \{\DYNAMIC, \VOID\}\\
21954
21958
\SubtypeStd{\code{Object?}}{T}}{S}{T}
21955
21959
% ------------------------------------------------ Left Bottom
21956
- \Axiom{\SrnBottom}{}{ \code{Never}}{T}
21960
+ \Axiom{\SrnBottom}{\code{Never}}{T}
21957
21961
% ------------------------------------------------ Left Null 1
21958
- \Axiom{\SrnNullOne}{}{ \code{Null}}{\code{$T$?}}
21962
+ \Axiom{\SrnNullOne}{\code{Null}}{\code{$T$?}}
21959
21963
\end{minipage}
21960
21964
\begin{minipage}[c]{0.49\textwidth}
21961
21965
% ------------------------------------------------ Right Top
21962
- \RuleRaw{\SrnRightTop}{}{ %
21966
+ \RuleRaw{\SrnRightTop}{%
21963
21967
T \in \{\code{Object?}, \DYNAMIC, \VOID\}}{S}{T}
21964
21968
% ------------------------------------------------ Right Object 4
21965
- \RuleRaw{\SrnRightObjectFour}{}{ %
21969
+ \RuleRaw{\SrnRightObjectFour}{%
21966
21970
$S$\,\not\in \{\code{Null}, \DYNAMIC, \VOID\}\\
21967
21971
\mbox{$S$ is not of the form \code{$U$?}, $X$,}\\
21968
21972
\mbox{\code{$X$\,\&\,$U$}, %
21969
21973
or \code{FutureOr<$U$>}}}{S}{\code{Object}}
21970
21974
% ------------------------------------------------ Left Null 2
21971
- \Rule{\SrnNullTwo}{}{ \code{Null}}{T}{%
21975
+ \Rule{\SrnNullTwo}{\code{Null}}{T}{%
21972
21976
\code{Null}}{\code{FutureOr<$T$>}}
21973
21977
\end{minipage}
21974
21978
21975
21979
\begin{minipage}[c]{0.49\textwidth}
21976
21980
% ------------------------------------------------ Left FutureOr
21977
- \RuleTwo{\SrnLeftFutureOr}{}{ %
21981
+ \RuleTwo{\SrnLeftFutureOr}{%
21978
21982
\code{Future<$S$>}}{T}{S}{T}{%
21979
21983
\code{FutureOr<$S$>}}{T}
21980
21984
% ------------------------------------------------ Right Promoted Variable
21981
- \RuleTwo{\SrnRightPromotedVariable}{}{ S}{X}{S}{T}{
21985
+ \RuleTwo{\SrnRightPromotedVariable}{S}{X}{S}{T}{
21982
21986
S}{X \& T}
21983
21987
% ------------------------------------------------ Right FutureOr B
21984
- \Rule{\SrnRightFutureOrB}{}{ S}{T}{S}{%
21988
+ \Rule{\SrnRightFutureOrB}{S}{T}{S}{%
21985
21989
\code{FutureOr<$T$>}}
21986
21990
% ------------------------------------------------ Right Nullable 2
21987
- \Rule{\SrnRightNullableTwo}{}{ S}{\code{Null}}{S}{%
21991
+ \Rule{\SrnRightNullableTwo}{S}{\code{Null}}{S}{%
21988
21992
\code{$T$?}}
21989
21993
% ------------------------------------------------ Left Variable Bound
21990
- \Rule{\SrnLeftVariableBound}{}{ \Gamma(X)}{T}{X}{T}
21994
+ \Rule{\SrnLeftVariableBound}{\Gamma(X)}{T}{X}{T}
21991
21995
\end{minipage}
21992
21996
\begin{minipage}[c]{0.49\textwidth}
21993
21997
% ------------------------------------------------ Left Nullable
21994
- \RuleTwo{\SrnLeftNullable}{}{ S}{T}{\code{Null}}{T}{
21998
+ \RuleTwo{\SrnLeftNullable}{S}{T}{\code{Null}}{T}{
21995
21999
\code{$S$?}}{T}
21996
22000
% ------------------------------------------------ Left Promoted Variable A
21997
- \Axiom{\SrnTypeVariableReflexivityA}{}{ X \& S}{X}
22001
+ \Axiom{\SrnTypeVariableReflexivityA}{X \& S}{X}
21998
22002
% ------------------------------------------------ Right FutureOr A
21999
- \Rule{\SrnRightFutureOrA}{}{ S}{%
22003
+ \Rule{\SrnRightFutureOrA}{S}{%
22000
22004
\code{Future<$T$>}}{S}{\code{FutureOr<$T$>}}
22001
22005
% ------------------------------------------------ Right Nullable 1
22002
- \Rule{\SrnRightNullableOne}{}{ S}{T}{S}{\code{$T$?}}
22006
+ \Rule{\SrnRightNullableOne}{S}{T}{S}{\code{$T$?}}
22003
22007
% ------------------------------------------------ Left Promoted Variable B
22004
- \Rule{\SrnLeftPromotedVariable}{}{ S}{T}{X \& S}{T}
22008
+ \Rule{\SrnLeftPromotedVariable}{S}{T}{X \& S}{T}
22005
22009
% ------------------------------------------------ Right Function
22006
- \RuleRaw{\SrnRightFunction}{}{ %
22010
+ \RuleRaw{\SrnRightFunction}{%
22007
22011
T\mbox{ is a function type}}{T}{\FUNCTION}
22008
22012
\end{minipage}
22009
22013
%
22010
22014
\ExtraVSP
22011
22015
% ------------------------------------------------ Positional Function Type
22012
- \RuleRawRaw{\SrnPositionalFunctionType}{}{ %
22016
+ \RuleRawRaw{\SrnPositionalFunctionType}{%
22013
22017
\Gamma' = \Gamma\uplus\{X_i\mapsto{}B_i\,|\,1 \leq i \leq s\} &
22014
22018
\Subtype{\Gamma'}{S_0}{T_0} \\
22015
22019
n_1 \leq n_2 &
@@ -22021,7 +22025,7 @@ \subsection{Subtypes}
22021
22025
\end{array}}
22022
22026
\ExtraVSP\ExtraVSP
22023
22027
% ------------------------------------------------ Named Function Type
22024
- \RuleRawRaw{\SrnNamedFunctionType}{}{
22028
+ \RuleRawRaw{\SrnNamedFunctionType}{
22025
22029
\Gamma' = \Gamma\uplus\{X_i\mapsto{}B_i\,|\,1 \leq i \leq s\} &
22026
22030
\Subtype{\Gamma'}{S_0}{T_0} &
22027
22031
\forall j \in 1 .. n\!:\;\Subtype{\Gamma'}{T_j}{S_j} \\
@@ -22035,13 +22039,13 @@ \subsection{Subtypes}
22035
22039
%
22036
22040
\ExtraVSP
22037
22041
% ------------------------------------------------ Covariance
22038
- \RuleRaw{\SrnCovariance}{}{ %
22042
+ \RuleRaw{\SrnCovariance}{%
22039
22043
\mbox{$C$ is an interface type with $s$ type parameters} &
22040
22044
\SubtypeStd{S_j}{T_j}\mbox{, for each $j \in 1..s$}}{%
22041
22045
\code{$C$<\List{S}{1}{s}>}}{\code{$C$<\List{T}{1}{s}>}}
22042
22046
\ExtraVSP
22043
22047
% ------------------------------------------------ Superinterface
22044
- \RuleRaw{\SrnSuperinterface}{}{ %
22048
+ \RuleRaw{\SrnSuperinterface}{%
22045
22049
\mbox{$C$ is an interface type with type parameters \List{X}{1}{s}}\\
22046
22050
\Superinterface{\code{$D$<\List{T}{1}{m}>}}{C} &
22047
22051
\SubtypeStd{[S_1/X_1,\ldots,S_s/X_s]\code{$D$<\List{T}{1}{m}>}}{T}}{%
0 commit comments