Skip to content

Specify null safety: Sections 'Variables' and 'Local Variable Declarations' #2052

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 15 commits into from
Jul 19, 2023
Merged

Specify null safety: Sections 'Variables' and 'Local Variable Declarations' #2052

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
78c57f2
Update section Variables
eernstg Jan 7, 2022
ff63e83
Rebasing
eernstg Jan 7, 2022
2c1e6cb
Update section Local Variable Declaration, update \Gamma to \Delta
eernstg Jan 7, 2022
218ac7f
Remove duplicate definition of DefEquals
eernstg Sep 27, 2022
863bc18
WIP
eernstg Sep 27, 2022
9947908
WIP
eernstg Sep 27, 2022
b244329
Review response
eernstg Sep 28, 2022
c930867
Further improvements (introduce cases for different kinds of variables)
eernstg Sep 30, 2022
30d0da7
Improved the local variable section similarly
eernstg Sep 30, 2022
910f0af
Review response, consisting of many small changes
eernstg Jun 14, 2023
3c47ea0
Improved comment
eernstg Jun 14, 2023
77717eb
Review response
eernstg Jul 18, 2023
8544c41
Now using non-local variable where possible, and "static or library v…
eernstg Jul 19, 2023
e171e47
Changed one occurrence of "static function" to "static method", which…
eernstg Jul 19, 2023
3285049
Eliminate the words mutable and immutable (instead spell out in each …
eernstg Jul 19, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
258 changes: 214 additions & 44 deletions specification/dart.sty
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,9 @@
\def\WITH{\keyword{with}}
\def\YIELD{\keyword{yield}}

% Used for inline code snippets.
\newcommand{\code}[1]{\texttt{#1}}

% Used to specify syntactic sugar.
\def\LET{\keyword{let}}
\newcommand{\Let}[3]{\code{\LET\,\,{#1}\,=\,{#2}\ \IN\ {#3}}}
Expand All @@ -78,8 +81,8 @@
\newcommand{\LetMany}[5]{%
\code{\LET\,\,{#1}\,=\,{#2},\ $\cdots$,\ {#3}\,=\,{#4}\ \IN\ {#5}}}

% Used for inline code snippets.
\def\code#1{\texttt{#1}}
% Used for inline meta-code snippets
\newcommand{\metaCode}[1]{{\color{metaColor}\texttt{#1}}}

% `call` has no special lexical status, so we just use \code{}.
\def\CALL{\code{call}}
Expand Down Expand Up @@ -112,6 +115,7 @@
\definecolor{normativeColor}{rgb}{0,0,0}
\definecolor{commentaryColor}{rgb}{0.5,0.5,0.5}
\definecolor{rationaleColor}{rgb}{0.5,0.5,0.5}
\definecolor{metaColor}{rgb}{0,0,1}

% Environments for different kinds of text.
\newenvironment{Q}[1]{{\bf{}Upcoming: {#1}}}{}
Expand All @@ -132,22 +136,35 @@
\newcommand{\Case}[1]{\textbf{Case }$\langle\hspace{0.1em}${#1}$\hspace{0.1em}\rangle$\textbf{.}}
\newcommand{\EndCase}{\mbox{}\hfill$\scriptscriptstyle\Box$\xspace}

\newenvironment{dartCode}[1][!ht] {%
% Used for source code examples.
\newenvironment{dartCode}[1][!ht]{%
\def\@programcr{\@addfield\strut}%
\let\\=\@programcr%
\relax\@vobeyspaces\obeylines%
\ttfamily\color{commentaryColor}%
\vspace{1em}%
}{\normalcolor\vspace{1em}}

\newenvironment{normativeDartCode}[1][!ht] {%
% Used for normative code snippets (mainly desugaring).
\newenvironment{normativeDartCode}[1][!ht]{%
\def\@programcr{\@addfield\strut}%
\let\\=\@programcr%
\relax\@vobeyspaces\obeylines%
\ttfamily\color{normativeColor}%
\vspace{1em}%
}{\normalcolor\vspace{1em}}

% Used for meta-level code, such as the code transformations used
% to specify the semantics of "null shorting" in expressions like
% `a?.b.c`.
\newenvironment{metaLevelCode}[1][!ht]{%
\def\@programcr{\@addfield\strut}%
\let\\=\@programcr%
\relax\@vobeyspaces\obeylines%
\ttfamily\color{metaColor}%
\vspace{1em}%
}{\normalcolor\vspace{1em}}

% Used for comments in a code context.
\def\comment#1{\textsf{#1}}

Expand All @@ -157,7 +174,7 @@

% Used for defining occurrence of phrase, with customized index entry.
\newcommand{\IndexCustom}[2]{%
\leavevmode\marginpar{\ensuremath{\diamond}}\emph{#1}\index{#2}}
\leavevmode\marginpar{\ensuremath{_{^\vartriangle}}}\emph{#1}\index{#2}}

% Used for the defining occurrence of a local symbol.
\newcommand{\DefineSymbol}[1]{%
Expand All @@ -178,7 +195,11 @@

% Same appearance, but not adding an entry to the index.
\newcommand{\NoIndex}[1]{%
\leavevmode\marginpar{\quad\ensuremath{\diamond}}\emph{#1}}
\leavevmode\marginpar{\ensuremath{_{^\vartriangle}}}\emph{#1}}

% Mark a compile-time error in the margin.
\newcommand{\Error}[1]{%
\leavevmode\marginpar{\ensuremath{_{^\ominus}}}{#1}}

% Used to specify comma separated lists of similar symbols.
\newcommand{\List}[3]{\ensuremath{{#1}_{#2},\,\ldots,\ {#1}_{#3}}}
Expand All @@ -190,6 +211,39 @@
\newcommand{\PairList}[4]{\ensuremath{%
{#1}_{#3}\ {#2}_{#3},\,\ldots,\ {#1}_{#4}\ {#2}_{#4}}}

% A sequence of labeled arguments with the same label and expression,
% only differing by subscript.
% Parameters: Argument label, argument expression, start index,
% end index.
%
% For example, \NamedArgumentList{n}{e}{1}{k} yields approximately
% "n1: e1, n2: e2, ... nk: ek".
\newcommand{\NamedArgumentList}[4]{\PairList{#1}{\!\!:\,\,{#2}}{#3}{#4}}

% A sequence of unlabeled and labeled arguments with the same expression and
% (for all labeled arguments) the same label, only differing by subscript.
% Parameters: Argument name, number of positional arguments, labeled parameter
% label, number of labeled arguments.
%
% For example, \ArgumentList{a}{n}{x}{k} yields approximately
% "a1, .. an, xn+1: an+1, .. xn+k: an+k".
\newcommand{\ArgumentList}[4]{%
\List{#1}{1}{#2},\ \NamedArgumentList{#3}{#1}{{#2}+1}{{#2}+{#4}}}

% Used to specify a standard argument list, that is, an argument list
% which uses the symbols that we prefer to use for that purpose
% whenever possible.
%
% Approximately "a1 .. an, xn+1: an+1 .. xn+k: an+k".
\newcommand{\ArgumentListStd}{\ArgumentList{a}{n}{x}{k}}

% Used to specify a standard type argument list, that is, a type
% argument list which uses the symbols we prefer to use for that
% purpose whenever possible.
%
% Approximately "A1 .. Ar".
\newcommand{\TypeArgumentListStd}{\List{A}{1}{r}}

% Used to specify a list of tuples of the form $(K_j, V_j)$ which are
% used with collection literals.
\newcommand{\KeyValueTypeList}[4]{\ensuremath{%
Expand Down Expand Up @@ -224,7 +278,11 @@
\newcommand{\TypeParametersNoBounds}[2]{\ensuremath{%
{#1}_1\,\EXTENDS\,\ldots,\ \ldots,\ {#1}_{#2}\,\EXTENDS\,\ldots}}

% For consistency, we may as well use this whenever possible.
% Used to specify a standard type parameter list, that is, a type
% parameter declaration list which uses the symbols we prefer to use
% for that purpose whenever possible.
%
% Approximately "X1 extends B1, .. Xs extends Bs".
\newcommand{\TypeParametersStd}{\TypeParameters{X}{B}{s}}

% Used to specify comma separated lists of pairs of symbols
Expand Down Expand Up @@ -256,78 +314,140 @@

% Used to specify function type parameter lists with positional optionals.
% Arguments: Parameter type, number of required parameters,
% number of optional parameters.
\newcommand{\FunctionTypePositionalArguments}[3]{%
% number of optional parameters.
%
% For example, \FunctionTypePositionalParameters{T}{n}{k} yields
% approximately "T1, .. Tn, [Tn+1, .. Tn+k]".
\newcommand{\FunctionTypePositionalParameters}[3]{%
\List{#1}{1}{#2},\ [\List{#1}{{#2}+1}{{#2}+{#3}}]}

\newcommand{\FunctionTypePositionalArgumentsStd}{%
\FunctionTypePositionalArguments{T}{n}{k}}
% Used to specify a standard positional function type, that is, a function
% type with positional optional parameters which uses the symbols we prefer
% to use for that purpose whenever possible.
%
% Approximately "T1, .. Tn, [Tn+1, .. Tn+k]".
\newcommand{\FunctionTypePositionalParametersStd}{%
\FunctionTypePositionalParameters{T}{n}{k}}

% Used to specify function type parameter lists with named optionals.
% Arguments: Parameter type, number of required parameters,
% name of optional parameters, number of optional parameters.
%
% For example \FunctionTypeNamedParameters{T}{n}{x}{k}{r} yields approximately
% "T1, .. Tn, {rn+1 Tn+1 xn+1, .. rn+k Tn+k xn+k}".
\newcommand{\FunctionTypeNamedParameters}[5]{%
\List{#1}{1}{#2},\ \{\TripleList{#5}{#1}{#3}{{#2}+1}{{#2}+{#4}}\}}

% Variant of \FunctionTypeNamedParameters that uses the standard symbols,
% that is, a list of function type parameter declarations with named
% parameters which uses the symbols that we prefer to use for that purpose
% whenever possible.
%
% Approximately "T1, .. Tn, {rn+1 Tn+1 xn+1, .. rn+k Tn+k xn+k}".
\newcommand{\FunctionTypeNamedParametersStd}{%
\FunctionTypeNamedParameters{T}{n}{x}{k}{r}}

% Used to specify function types with positional optionals:
% Arguments: Return type, spacer, type parameter name, bound name,
% number of type parameters, parameter type, number of required parameters,
% number of optional parameters.
%
% For example, \FunctionTypePositional{R}{ }{X}{B}{s}{T}{n}{k} yields
% approximately
% "R Function<X1 extends B1, .. Xs extends Bs>(T1, .. Tn, [Tn+1, .. Tn+k])".
\newcommand{\FunctionTypePositional}[8]{%
\FunctionType{#1}{#2}{#3}{#4}{#5}{%
\FunctionTypePositionalArguments{#6}{#7}{#8}}}
\FunctionTypePositionalParameters{#6}{#7}{#8}}}

% Same as \FunctionTypePositional except suitable for inline usage,
% hence omitting the spacer argument.
\newcommand{\RawFunctionTypePositional}[7]{%
\RawFunctionType{#1}{#2}{#3}{#4}{%
\FunctionTypePositionalArguments{#5}{#6}{#7}}}
\FunctionTypePositionalParameters{#5}{#6}{#7}}}

% A variant of \FunctionTypePositional that uses the standard symbols,
% that is, a function type with positional optional parameters which
% uses the symbols that we prefer to use for that purpose whenever
% possible.
%
% For example, \FunctionTypePositionalStd{R} yields approximately
% "R Function<X1 extends B1, .. Xs extends Bs>(T1, T2, .. Tn, [Tn+1 .. Tn+k])".
\newcommand{\FunctionTypePositionalStd}[1]{%
\FunctionTypePositional{#1}{ }{X}{B}{s}{T}{n}{k}}

% Used to specify function type parameter lists with named optionals.
% Arguments: Parameter type, number of required parameters,
% name of optional parameters, number of optional parameters.
\newcommand{\FunctionTypeNamedArguments}[4]{%
\List{#1}{1}{#2},\ \{\PairList{#1}{#3}{{#2}+1}{{#2}+{#4}}\}}
% Same as \FunctionTypePositionalStd except suitable for inline usage,
% hence omitting the spacer argument.
\newcommand{\RawFunctionTypePositionalStd}[1]{%
\RawFunctionTypePositional{#1}{X}{B}{s}{T}{n}{k}}

\newcommand{\FunctionTypeNamedArgumentsStd}{%
\FunctionTypeNamedArguments{T}{n}{x}{k}}
% Same as \FunctionTypePositionalStd except that it includes a newline, hence
% suitable for function types that are too long to fit in one line.
\newcommand{\FunctionTypePositionalStdCr}[1]{%
\FunctionTypePositional{#1}{\\}{X}{B}{s}{T}{n}{k}}

% Used to specify function types with named parameters:
% Arguments: Return type, spacer, type parameter name, bound name,
% number of type parameters, parameter type, number of required parameters,
% name of optional parameters, number of optional parameters.
% The name of the `required` symbol is always `r` (because we can't have
% 10 arguments in a LaTeX command, and `r` is always OK in practice).
%
% For example, \FunctionTypeNamed{R}{ }{X}{B}{s}{T}{n}{x}{k} yields
% approximately "R Function<X1 extends B1, .. Xs extends Bs>(
% T1, T2, .. Tn, {rn+1 Tn+1 xn+1, .. rn+k Tn+k xn+k])".
\newcommand{\FunctionTypeNamed}[9]{%
\FunctionType{#1}{#2}{#3}{#4}{#5}{%
\FunctionTypeNamedArguments{#6}{#7}{#8}{#9}}}
\FunctionType{#1}{#2}{#3}{#4}{#5}{\\
\mbox{}\qquad\FunctionTypeNamedParameters{#6}{#7}{#8}{#9}{r}}}

% Same as \FunctionType except suitable for inline usage, hence omitting
% Same as \FunctionTypeNamed except suitable for inline usage, hence omitting
% the spacer argument.
\newcommand{\RawFunctionTypeNamed}[8]{%
\RawFunctionType{#1}{#2}{#3}{#4}{%
\FunctionTypeNamedArguments{#5}{#6}{#7}{#8}}}
\FunctionTypeNamedParameters{#5}{#6}{#7}{#8}{r}}}

% A variant of \FunctionTypeNamed that uses the standard symbols,
% that is, a function type with positional optional parameters which
% uses the symbols that we prefer to use for that purpose whenever
% possible.
%
% For example, \FunctionTypeNamedStd{R} yields approximately
% "R Function<X1 extends B1, .. Xs extends Bs>(
% T1, T2, .. Tn, {rn+1 Tn+1 xn+1, .. rn+k Tn+k xn+k})".
\newcommand{\FunctionTypeNamedStd}[1]{%
\FunctionTypeNamed{#1}{ }{X}{B}{s}{T}{n}{x}{k}}

% Same as \FunctionTypeNamedStd except suitable for inline usage, hence
% omitting the spacer argument.
\newcommand{\RawFunctionTypeNamedStd}[1]{%
\RawFunctionTypeNamed{#1}{X}{B}{s}{T}{n}{x}{k}{r}}

% Same as \FunctionTypeNamedStd except that it includes a newline, hence
% suitable for function types that are too long to fit in one line.
\newcommand{\FunctionTypeNamedStdCr}[1]{%
\FunctionTypeNamed{#1}{\\}{X}{B}{s}{T}{n}{x}{k}}

% Used to specify function types with no optional parameters:
% Arguments: Return type, spacer, type parameter name, bound name,
% number of type parameters, parameter type,
% number of parameters (all required).
%
% For example, \FunctionTypeAllRequired{R}{ }{X}{B}{s}{T}{n} yields
% approximately "R Function<X1 extends B1, .. Xs extends Bs>(T1, T2, .. Tn)".
\newcommand{\FunctionTypeAllRequired}[7]{%
\FunctionType{#1}{#2}{#3}{#4}{#5}{\List{#6}{1}{#7}}}

\newcommand{\FunctionTypePositionalStd}[1]{%
\FunctionTypePositional{#1}{ }{X}{B}{s}{T}{n}{k}}

\newcommand{\RawFunctionTypePositionalStd}[1]{%
\RawFunctionTypePositional{#1}{X}{B}{s}{T}{n}{k}}

\newcommand{\FunctionTypeNamedStd}[1]{%
\FunctionTypeNamed{#1}{ }{X}{B}{s}{T}{n}{x}{k}}

\newcommand{\RawFunctionTypeNamedStd}[1]{%
\RawFunctionTypeNamed{#1}{X}{B}{s}{T}{n}{x}{k}}

% A variant of \FunctionTypeAllRequired that uses the standard symbols,
% that is, a function type with positional optional parameters which
% uses the symbols that we prefer to use for that purpose whenever
% possible.
%
% For example, \FunctionTypeAllRequiredStd{R} yields approximately
% "R Function<X1 extends B1, .. Xs extends Bs>(T1, T2, .. Tn)".
\newcommand{\FunctionTypeAllRequiredStd}[1]{%
\FunctionTypeAllRequired{#1}{ }{X}{B}{s}{T}{n}}

\newcommand{\FunctionTypePositionalStdCr}[1]{%
\FunctionTypePositional{#1}{\\}{X}{B}{s}{T}{n}{k}}

\newcommand{\FunctionTypeNamedStdCr}[1]{%
\FunctionTypeNamed{#1}{\\}{X}{B}{s}{T}{n}{x}{k}}

% Same as \FunctionTypeAllRequiredStd except that it includes a newline, hence
% suitable for function types that are too long to fit in one line.
\newcommand{\FunctionTypeAllRequiredStdCr}[1]{%
\FunctionTypeAllRequired{#1}{\\}{X}{B}{s}{T}{n}}

Expand All @@ -342,13 +462,13 @@

% Judgment expressing that a subtype relation exists.
\newcommand{\Subtype}[3]{\ensuremath{{#1}\vdash{#2}\,<:\,{#3}}}
\newcommand{\SubtypeStd}[2]{\Subtype{\Gamma}{#1}{#2}}
\newcommand{\SubtypeStd}[2]{\Subtype{\Delta}{#1}{#2}}
% Subtype judgment where the environment is omitted (NE: "no environment").
\newcommand{\SubtypeNE}[2]{\ensuremath{{#1}\,<:\,{#2}}}

% Judgment expressing that a supertype relation exists.
\newcommand{\Supertype}[3]{\ensuremath{{#1}\vdash{#2}\,:>\,{#3}}}
\newcommand{\SupertypeStd}[2]{\Supertype{\Gamma}{#1}{#2}}
\newcommand{\SupertypeStd}[2]{\Supertype{\Delta}{#1}{#2}}

% Judgment expressing that an assignability relation exists.
\newcommand{\AssignableRelationSymbol}{\ensuremath{\Longleftrightarrow}}
Expand Down Expand Up @@ -394,6 +514,56 @@
\ensuremath{{#2}}%
}

\newcommand{\FlattenName}{\metavar{flatten}}
\newcommand{\Flatten}[1]{\ensuremath{\FlattenName(\code{#1})}}

\newcommand{\NominalTypeDepthName}{\metavar{nominalTypeDepth}}
\newcommand{\NominalTypeDepth}[1]{%
\ensuremath{\NominalTypeDepthName(\code{#1})}}

\newcommand{\TopMergeTypeName}{\metavar{topMergeType}}
\newcommand{\TopMergeType}[2]{%
\ensuremath{\TopMergeTypeName(\code{{#1},\,\,{#2}})}}

\newcommand{\NonNullTypeName}{\metavar{nonNullType}}
\newcommand{\NonNullType}[1]{\ensuremath{\NonNullTypeName(\code{#1})}}

\newcommand{\IsTopTypeName}{\metavar{isTopType}}
\newcommand{\IsTopType}[1]{\ensuremath{\IsTopTypeName(\code{#1})}}

\newcommand{\IsObjectTypeName}{\metavar{isObjectType}}
\newcommand{\IsObjectType}[1]{\ensuremath{\IsObjectTypeName(\code{#1})}}

\newcommand{\IsBottomTypeName}{\metavar{isBottomType}}
\newcommand{\IsBottomType}[1]{\ensuremath{\IsBottomTypeName(\code{#1})}}

\newcommand{\IsNullTypeName}{\metavar{isNullType}}
\newcommand{\IsNullType}[1]{\ensuremath{\IsNullTypeName(\code{#1})}}

\newcommand{\IsMoreTopTypeName}{\metavar{isMoreTopType}}
\newcommand{\IsMoreTopType}[2]{%
\ensuremath{\IsMoreTopTypeName(\code{{#1},\,\,{#2}})}}

\newcommand{\IsMoreBottomTypeName}{\metavar{isMoreBottomType}}
\newcommand{\IsMoreBottomType}[2]{%
\ensuremath{\IsMoreBottomTypeName(\code{{#1},\,\,{#2}})}}

\newcommand{\NormalizedTypeOfName}{\metavar{normalizedType}}
\newcommand{\NormalizedTypeOf}[1]{%
\ensuremath{\NormalizedTypeOfName(\code{#1})}}

\newcommand{\FutureValueTypeOfName}{\metavar{futureValueType}}
\newcommand{\FutureValueTypeOf}[1]{%
\ensuremath{\FutureValueTypeOfName(\code{#1})}}

\newcommand{\UpperBoundTypeName}{\metavar{standardUpperBound}}
\newcommand{\UpperBoundType}[2]{%
\ensuremath{\UpperBoundTypeName(\code{{#1},\,\,{#2}})}}

\newcommand{\LowerBoundTypeName}{\metavar{standardLowerBound}}
\newcommand{\LowerBoundType}[2]{%
\ensuremath{\LowerBoundTypeName(\code{{#1},\,\,{#2}})}}

% ----------------------------------------------------------------------
% Support for hash valued Location Markers

Expand Down
Loading