Specify null safety subtyping

specification/dart.sty

@@ -20,6 +20,7 @@
 \def\MIXIN{\builtinId{mixin}}
 \def\OPERATOR{\builtinId{operator}}
 \def\PART{\builtinId{part}}
+\def\RECORD{\builtinId{Record}}
 \def\REQUIRED{\builtinId{required}}
 \def\SET{\builtinId{set}}
 \def\STATIC{\builtinId{static}}
@@ -124,11 +125,11 @@
 \newenvironment{commentary}[1]{{\color{commentaryColor}\sf{#1}}}{}
 
 % Auxiliary functions.
-\newcommand{\flattenName}{\mbox{\it flatten}}
+\newcommand{\flattenName}{\metavar{flatten}}
 \newcommand{\flatten}[1]{\ensuremath{\flattenName({#1})}}
-\newcommand{\futureOrBase}[1]{\ensuremath{\mbox{\it futureOrBase}({#1})}}
-\newcommand{\overrides}[1]{\ensuremath{\mbox{\it overrides}({#1})}}
-\newcommand{\inherited}[1]{\ensuremath{\mbox{\it inherited}({#1})}}
+\newcommand{\futureOrBase}[1]{\ensuremath{\metavar{futureOrBase}({#1})}}
+\newcommand{\overrides}[1]{\ensuremath{\metavar{overrides}({#1})}}
+\newcommand{\inherited}[1]{\ensuremath{\metavar{inherited}({#1})}}
 
 % Used as a mini-section marker, indicating visibly that a range of
 % text (usually just a couple of paragraphs) are concerned with one
@@ -173,9 +174,12 @@
 \newcommand{\id}{\metavar{id}}
 \newcommand{\op}{\metavar{op}}
 
+% Used in margin to indicate that a term is being defined here.
+\newcommand{\IndexMarker}{\ensuremath{^\vartriangle}}
+
 % Used for defining occurrence of phrase, with customized index entry.
 \newcommand{\IndexCustom}[2]{%
-  \leavevmode\marginpar{\ensuremath{_{^\vartriangle}}}\emph{#1}\index{#2}}
+  \leavevmode\marginpar{\IndexMarker}\emph{#1}\index{#2}}
 
 % Used for the defining occurrence of a local symbol.
 \newcommand{\DefineSymbol}[1]{%
@@ -196,11 +200,15 @@
 
 % Same appearance, but not adding an entry to the index.
 \newcommand{\NoIndex}[1]{%
-  \leavevmode\marginpar{\ensuremath{_{^\vartriangle}}}\emph{#1}}
+  \leavevmode\marginpar{\IndexMarker}\emph{#1}}
 
 % Mark a compile-time error in the margin.
 \newcommand{\Error}[1]{%
-  \leavevmode\marginpar{\ensuremath{_{^\ominus}}}{#1}}
+  \leavevmode\marginpar{\ensuremath{\textcolor{red}{\ominus}}}{#1}}
+
+% Mark a dynamic error in the margin.
+\newcommand{\DynamicError}[1]{%
+  \leavevmode\marginpar{\textcolor{red}{\Lightning}}{#1}}
 
 % Used to specify comma separated lists of similar symbols.
 \newcommand{\List}[3]{\ensuremath{{#1}_{#2},\,\ldots,\ {#1}_{#3}}}
@@ -402,9 +410,9 @@
 
 % Same as \FunctionTypeNamed except suitable for inline usage, hence omitting
 % the spacer argument.
-\newcommand{\RawFunctionTypeNamed}[8]{%
+\newcommand{\RawFunctionTypeNamed}[9]{%
   \RawFunctionType{#1}{#2}{#3}{#4}{%
-    \FunctionTypeNamedParameters{#5}{#6}{#7}{#8}{r}}}
+    \FunctionTypeNamedParameters{#5}{#6}{#7}{#8}{#9}}}
 
 % A variant of \FunctionTypeNamed that uses the standard symbols,
 % that is, a function type with positional optional parameters which
@@ -466,17 +474,14 @@
 \newcommand{\SubtypeStd}[2]{\Subtype{\Delta}{#1}{#2}}
 % Subtype judgment where the environment is omitted (NE: "no environment").
 \newcommand{\SubtypeNE}[2]{\ensuremath{{#1}\,<:\,{#2}}}
+\newcommand{\MutualSubtype}[3]{\ensuremath{{#1}\vdash{#2}\,<:>\,{#3}}}
+\newcommand{\MutualSubtypeStd}[2]{\MutualSubtype{\Delta}{#1}{#2}}
+\newcommand{\MutualSubtypeNE}[2]{\ensuremath{{#1}\,<:>\,{#2}}}
 
 % Judgment expressing that a supertype relation exists.
 \newcommand{\Supertype}[3]{\ensuremath{{#1}\vdash{#2}\,:>\,{#3}}}
 \newcommand{\SupertypeStd}[2]{\Supertype{\Delta}{#1}{#2}}
 
-% Judgment expressing that an assignability relation exists.
-\newcommand{\AssignableRelationSymbol}{\ensuremath{\Longleftrightarrow}}
-\newcommand{\Assignable}[3]{%
-  \ensuremath{{#1}\vdash{#2}\,\AssignableRelationSymbol\,{#3}}}
-\newcommand{\AssignableStd}[2]{\Assignable{\Gamma}{#1}{#2}}
-
 % Semantic function delivering the superinterfaces of a class.
 \newcommand{\Superinterfaces}[1]{\ensuremath{\metavar{Superinterfaces}({#1})}}
 \newcommand{\Superinterface}[2]{{#1}\in\Superinterfaces{#2}}