Changeset 4312

Timestamp:

11/04/09 05:56:40 (3 weeks ago)

Author:

sukyoungryu

Message:

[spec] Added the advanced part.

Location:

trunk/Specification

Files:

• advanced/defining-dimensions.tex (modified) (1 diff)
• advanced/domain-specific-languages.tex (modified) (1 diff)
• advanced/operator-definitions.tex (modified) (1 diff)
• advanced/overloading.tex (modified) (1 diff)
• advanced/parallelism-locality/arrays-distributed.tex (modified) (1 diff)
• advanced/parallelism-locality/defining-generators.tex (modified) (1 diff)
• advanced/parallelism-locality/distributions.tex (modified) (1 diff)
• advanced/parallelism-locality/early-termination.tex (modified) (1 diff)
• advanced/parallelism-locality/intro.tex (modified) (1 diff)
• advanced/parallelism-locality/primitives-distributions.tex (modified) (1 diff)
• advanced/parallelism-locality/regions-threads.tex (modified) (1 diff)
• advanced/parallelism-locality/shared-local.tex (modified) (1 diff)
• advanced/parallelism-locality/transactions.tex (modified) (1 diff)
• advanced/subscripting.tex (modified) (1 diff)
• basic/overloading.tex (modified) (1 diff)
• fortress/fortress.bib (modified) (2 diffs)

trunk/Specification/advanced/defining-dimensions.tex

@@ -18 +18 @@
 \chapter{Dimension and Unit Declarations}
 \chaplabel{declaring-dimunits}
+
+\note{Dimensions and units are not yet supported.}
+
+\begin{Grammar}
+\emph{DimUnitDecl}
+&::=&
+\KWD{dim} \emph{Id} \options{\EXP{=} \emph{Type}}
+(\KWD{unit} $|$ \KWD{SI\_unit}) \emph{Id}$^+$
+\options{\EXP{=} \emph{Expr}}\\
+&$|$&
+\KWD{dim} \emph{Id}
+\options{\EXP{=} \emph{Type}} \options{\KWD{default} \emph{Id}}\\
+&$|$&
+(\KWD{unit} $|$ \KWD{SI\_unit})
+\emph{Id}$^+$ \options{\EXP{\mathrel{\mathtt{:}}} \emph{Type}}
+ \options{\EXP{=} \emph{Expr}}\\
+\end{Grammar}
+
+\section{Dimension Declarations}
+Dimensions may be explicitly declared;
+every declared dimension must be declared at the top level
+of a program component,
+not within a block expression or trait.
+Other dimensions may be constructed by multiplying and dividing other dimensions,
+as described in \chapref{dimunits}.
+An explicitly declared dimension may be a \emph{base dimension} (with no definition specified)
+or a \emph{derived dimension} (with a definition specified in the form of an initialization expression).
+
+The set of all dimensions has the algebraic structure of a free abelian group.
+The identity element of this group is the dimension \TYP{Unity}, which represents dimensionlessness.
+
+For every two dimensions \VAR{D} and \VAR{E}, there is a
+dimension \EXP{D E} (which may also be written \EXP{D \cdot E}),
+corresponding to the product of the dimensions \VAR{D} and \VAR{E} and a
+dimension \EXP{D/E}, corresponding to the quotient of the
+dimensions \VAR{D} and \VAR{E}. The syntactic sugar \EXP{1/D} is equivalent
+to \EXP{\TYP{Unity}/D} for all dimensions \VAR{D}.
+A dimension can be raised to a rational power where both
+the numerator and the denominator of the rational power
+must be a valid \emph{\KWD{nat} parameter} instantiation;
+\EXP{D^{0}} is the same as \TYP{Unity},
+\EXP{D^{1}} is the same as \VAR{D}, and
+\EXP{D^{m+n}} is the same as \EXP{D^{m} D^{n}}.
+The syntactic sugar \EXP{D^{-n}} is the same as \EXP{\TYP{Unity}/D^{n}}.
+
+Here are some examples of base dimension declarations:
+%% dim Length
+%% dim Mass
+%% dim Time
+%% dim ElectricCurrent
+\begin{Fortress}
+\(\KWD{dim} \TYP{Length}\)\\
+\(\KWD{dim} \TYP{Mass}\)\\
+\(\KWD{dim} \TYP{Time}\)\\
+\(\KWD{dim} \TYP{ElectricCurrent}\)
+\end{Fortress}
+Here are some examples of computed dimensions:
+%% Length / Time
+%% Velocity / Time
+%% Length \cdot Mass / Time^2
+%% Length Mass Time^(-2)
+%% ElectricCurrent / Length^2
+\begin{Fortress}
+\(\TYP{Length} / \TYP{Time}\)\\
+\(\TYP{Velocity} / \TYP{Time}\)\\
+\(\TYP{Length} \cdot \TYP{Mass} / \TYP{Time}^{2}\)\\
+\(\TYP{Length}\mskip 4mu plus 4mu\TYP{Mass}\mskip 4mu plus 4mu\TYP{Time}^{-2}\)\\
+\(\TYP{ElectricCurrent} / \TYP{Length}^{2}\)
+\end{Fortress}
+and here some of these computed dimensions are given names through the use of
+derived dimension declarations:
+%% dim Velocity = Length / Time
+%% dim Acceleration = Velocity / Time
+%% dim CurrentDensity = ElectricCurrent / Length^2
+\begin{Fortress}
+\(\KWD{dim} \TYP{Velocity} = \TYP{Length} / \TYP{Time}\)\\
+\(\KWD{dim} \TYP{Acceleration} = \TYP{Velocity} / \TYP{Time}\)\\
+\(\KWD{dim} \TYP{CurrentDensity} = \TYP{ElectricCurrent} / \TYP{Length}^{2}\)
+\end{Fortress}
+
+\section{Unit Declarations}
+Every unit belongs to exactly one dimension, which is the type of the unit.
+A dimension may have more than one unit,
+but one of these units may be singled out as the \emph{default unit} for that dimension
+by adding a \KWD{default} clause:
+%% dim Length default meter
+%% dim Mass default kilogram
+%% dim Time default second
+\begin{Fortress}
+\(\KWD{dim} \TYP{Length} \KWD{default} \TYP{meter}\)\\
+\(\KWD{dim} \TYP{Mass} \KWD{default} \TYP{kilogram}\)\\
+\(\KWD{dim} \TYP{Time} \KWD{default} \TYP{second}\)
+\end{Fortress}
+The default unit is used when a numerical type is multiplied by a
+dimension to produce a new type (see \chapref{dimunits}).
+If no default clause is specified for a base dimension, then it has
+no default unit.  If no default clause is specified for a derived
+dimension, then it has a default unit if and only if all the
+dimensions mentioned in its initialization expression have defaults,
+in which case its default unit is calculated using the initialization
+expression with each dimension replaced by its default unit.
+
+Some units are explicitly declared;
+every declared unit must be declared at the top level of
+a program component, not
+within a block expression or trait.
+Other units may be constructed by multiplying and dividing other units.
+An explicitly declared unit may be a \emph{base unit} (with no definition specified)
+or a \emph{derived unit} (with a definition specified in the form of an initialization expression).
+
+The set of all units, like the set of all dimensions, has the algebraic structure of a free abelian group.
+The identity element of this group is the unit \TYP{dimensionless}, of
+dimension \TYP{Unity}.
+Note that there may be other units of dimension \TYP{Unity}, such as
+\TYP{radian} and \TYP{steradian}, but only \TYP{dimensionless} is the
+identity of the group of all units.
+(Note that there is a straightforward homomorphism of units onto
+dimensions, wherein every unit is mapped to its dimension.)
+
+Here are some examples of base unit declarations:
+%% unit meter : Length
+%% unit kilogram : Mass
+%% unit second : Time
+%% unit ampere : ElectricCurrent
+\begin{Fortress}
+\(\KWD{unit} \TYP{meter} \mathrel{\mathtt{:}} \TYP{Length}\)\\
+\(\KWD{unit} \TYP{kilogram} \mathrel{\mathtt{:}} \TYP{Mass}\)\\
+\(\KWD{unit} \TYP{second} \mathrel{\mathtt{:}} \TYP{Time}\)\\
+\(\KWD{unit} \TYP{ampere} \mathrel{\mathtt{:}} \TYP{ElectricCurrent}\)
+\end{Fortress}
+Here are some examples of computed units:
+%% meter / second
+%% (meter / second) / second
+%% meter \cdot kilogram / second^2
+%% meter kilogram second^(-2)
+%% ampere / meter^2
+\begin{Fortress}
+\(\TYP{meter} / \TYP{second}\)\\
+\((\TYP{meter} / \TYP{second}) / \TYP{second}\)\\
+\(\TYP{meter} \cdot \TYP{kilogram} / \TYP{second}^{2}\)\\
+\(\TYP{meter}\mskip 4mu plus 4mu\TYP{kilogram}\mskip 4mu plus 4mu\TYP{second}^{-2}\)\\
+\(\TYP{ampere} / \TYP{meter}^{2}\)
+\end{Fortress}
+and here some computed units are given names through the use of
+derived unit declarations:
+%% unit newton: Force = meter \cdot kilogram / second^2
+%% unit joule: Energy = newton meter
+%% unit pascal: Pressure = newton / meter^2
+\begin{Fortress}
+\(\KWD{unit} \TYP{newton}\COLON \TYP{Force} = \TYP{meter} \cdot \TYP{kilogram} / \TYP{second}^{2}\)\\
+\(\KWD{unit} \TYP{joule}\COLON \TYP{Energy} = \TYP{newton}\mskip 4mu plus 4mu\TYP{meter}\)\\
+\(\KWD{unit} \TYP{pascal}\COLON \TYP{Pressure} = \TYP{newton} / \TYP{meter}^{2}\)
+\end{Fortress}
+In the preceding examples, the initialization expression for each unit
+is itself a unit.  It is also permitted for the initialization
+expression to be a dimensioned numerical value, in which case
+the unit being declared is related to the unit of the dimensioned
+numerical value by a numerical conversion factor.
+
+As with an ordinary variable declaration, one may omit the dimension for a unit
+if there is an initialization expression; the dimension of the declared unit is
+the dimension of the unit of the expression.
+
+\note{COMMENTED TEXT; I like the explanation below better. -- Eric
+
+Every unit can be reduced to a canonical unit as follows.  A base unit is
+canonical; a \KWD{unit} parameter is canonical; a defined unit is replaced
+by its initialization expression,
+but only if the value of the expression
+is a unit and not a dimensioned value, where every unit in that expression
+is replaced by its canonical unit;
+and finally all arithmetic is performed
+so as to reduce the expression to a single unit. Two units are considered
+equivalent if their canonical units are identical.
+
+Now here is a slightly different process.
+}
+
+Every unit can be reduced to a canonical value as follows.  A base unit is
+multiplied by the value \EXP{1}; a \KWD{unit} parameter is multiplied by
+the value \EXP{1}; a defined unit is replaced by its initialization
+expression and then every unit in that expression is replaced by its
+canonical form;
+and finally all arithmetic is performed so as to reduce the
+units to a single unit and the
+numerical values to a single numerical value.  A dimensioned value with unit
+\VAR{U} is convertible by the \KWD{in} operator to a value with unit
+\VAR{V} if the canonical values for \VAR{U} and \VAR{V} have the same
+unit; the conversion involves multiplying the numerical value by the
+ratio of the numerical value of the canonical form
+of \VAR{V} to the numerical value of the canonical form of \VAR{U}.
+
+For example, given the declarations:
+%% dim Length
+%% unit meter: Length; unit meters = meter
+%% unit kilometer: Length = 10^3 meter; unit kilometers = kilometer
+%% unit inch: Length = 2.54 \times 10^(-2) meter; unit inches = inch
+%% unit foot: Length = 12 inch; unit feet = foot
+%% unit mile: Length = 5280 foot; unit miles = mile
+\begin{Fortress}
+\(\KWD{dim} \TYP{Length}\)\\
+\(\KWD{unit} \TYP{meter}\COLON \TYP{Length}; \KWD{unit} \TYP{meters} = \TYP{meter}\)\\
+\(\KWD{unit} \TYP{kilometer}\COLON \TYP{Length} = 10^{3} \TYP{meter}; \KWD{unit} \TYP{kilometers} = \TYP{kilometer}\)\\
+\(\KWD{unit} \TYP{inch}\COLON \TYP{Length} = 2.54 \times 10^{-2} \TYP{meter}; \KWD{unit} \TYP{inches} = \TYP{inch} \)\\
+\(\KWD{unit} \TYP{foot}\COLON \TYP{Length} = 12\,\TYP{inch}; \KWD{unit} \TYP{feet} = \TYP{foot}\)\\
+\(\KWD{unit} \TYP{mile}\COLON \TYP{Length} = 5280\,\TYP{foot}; \KWD{unit} \TYP{miles} = \TYP{mile}\)
+\end{Fortress}
+then one can say \EXP{3\,\TYP{miles}\, \KWD{in}\, \TYP{kilometers}} and
+the \KWD{in} operator will multiply the numerical value \EXP{3} by
+the amount of
+\EXP{((2.54 \times 10^{-2})(12)(5280)/10^{3})},
+or \EXP{25146/15625}.
+
+Notice the subtle difference between these two declarations:
+%% unit radian = meter/meter
+%% unit radian = 1 meter/meter
+\begin{Fortress}
+\(\KWD{unit} \TYP{radian} = \TYP{meter}/\TYP{meter}\)\\
+\(\KWD{unit} \TYP{radian} = 1\,\TYP{meter}/\TYP{meter}\)
+\end{Fortress}
+The first declaration defines \TYP{radian} to be equivalent to
+\TYP{dimensionless}, and so a value with unit \TYP{radian} can be used
+anywhere a dimensionless value can be used, and vice versa.
+The second declaration defines \TYP{radian} to be convertible to
+\TYP{dimensionless} but not equivalent, and so it is necessary to use
+the \KWD{in} operator (or multiplication and division by \TYP{radian})
+to convert between values in radians and truly dimensionless values.
+
+
+\section{Abbreviating Dimension and Unit Declarations}
+\seclabel{abbrev-dimunits}
+
+For convenience, three forms of syntactic sugar are provided when declaring
+dimensions and units.
+First, in a \KWD{unit} declaration one may mention more than one name
+before the colon, and the extra names are defined to be synonyms for the
+first name; thus
+%% unit foot feet ft_: Length
+\begin{Fortress}
+\(\KWD{unit} \TYP{foot}\mskip 4mu plus 4mu\TYP{feet}\mskip 4mu plus 4mu\mathrm{ft}\COLON \TYP{Length}\)
+\end{Fortress}
+means exactly the same thing as
+%% unit foot: Length
+%% unit feet: Length = foot
+%% unit ft_: Length = foot
+\begin{Fortress}
+\(\KWD{unit} \TYP{foot}\COLON \TYP{Length}\)\\
+\(\KWD{unit} \TYP{feet}\COLON \TYP{Length} = \TYP{foot}\)\\
+\(\KWD{unit} \mathrm{ft}\COLON \TYP{Length} = \TYP{foot}\)
+\end{Fortress}
+Second, instead of the reserved word \KWD{unit} one may use the reserved
+word \KWD{SI\_unit}, which has the effect of defining not only the
+specified names but also names with the various SI prefixes attached.
+If more than one name is specified, then the last name is assumed
+to be a symbol and has symbol prefixes (such as \TYP{M} and \TYP{n})
+attached; all other names have the full prefixes (such as
+\TYP{mega} and \TYP{nano}) attached.
+Thus
+%% SI_unit name1 name2 name3: ...
+\begin{Fortress}
+\(\KWD{SI{\char'137}unit} {name}_{1}\;\;{name}_{2}\;\;{name}_{3}\COLON \ldots\)
+\end{Fortress}
+may be regarded as an abbreviation for
+%% unit~name1~name2~name3: ...
+%% unit yotta~name1~yotta name2~Y name3 = 10^24~name1
+%% unit zetta~name1~zetta name2~Z name3 = 10^21 ~name1
+%% unit exa~name1~exa name2~E name3 = 10^18 ~name1
+%% unit peta~name1~peta name2~P name3 = 10^15 ~name1
+%% unit tera~name1~tera name2~T name3 = 10^12 ~name1
+%% unit giga~name1~giga name2~G name3 = 10^9 ~name1
+%% unit mega~name1~mega name2~M name3 = 10^6 ~name1
+%% unit kilo~name1~kilo name2~k name3 = 10^3 ~name1
+%% unit hecto~name1~hecto name2~h name3 = 10^2 ~name1
+%% unit deka~name1~deka name2~da name3 = 10 ~name1
+%% unit deci~name1~deci name2~d name3 = 10^(-1) ~name1
+%% unit centi~name1~centi name2~c name3 = 10^(-2) ~name1
+%% unit milli~name1~milli name2~m name3 = 10^(-3) ~name1
+%% unit micro~name1~micro name2~micro name3 = 10^(-6) ~name1
+%% unit nano~name1~nano name2~n name3 = 10^(-9) ~name1
+%% unit pico~name1~pico name2~p name3 = 10^(-12) ~name1
+%% unit femto~name1~femto name2~f name3 = 10^(-15) ~name1
+%% unit atto~name1~atto name2~a name3 = 10^(-18) ~name1
+%% unit zepto~name1~zepto name2~z name3 = 10^(-21) ~name1
+%% unit yocto~name1~yocto name2~y name3 = 10^(-24) ~name1
+\begin{Fortress}
+\(\KWD{unit} {name}_{1}~{name}_{2}~{name}_{3}\COLON \ldots\)\\
+\(\KWD{unit} \TYP{yotta} {name}_{1}~\TYP{yotta} {name}_{2}~ \TYP{Y} {name}_{3} = 10^{24} {name}_{1}\)\\
+\(\KWD{unit} \TYP{zetta} {name}_{1}~\TYP{zetta} {name}_{2}~ \TYP{Z} {name}_{3} = 10^{21}  {name}_{1}\)\\
+\(\KWD{unit} \TYP{exa} {name}_{1}~\TYP{exa} {name}_{2}~ \TYP{E} {name}_{3} = 10^{18}  {name}_{1}\)\\
+\(\KWD{unit} \TYP{peta} {name}_{1}~\TYP{peta} {name}_{2}~ \TYP{P} {name}_{3} = 10^{15}  {name}_{1}\)\\
+\(\KWD{unit} \TYP{tera} {name}_{1}~\TYP{tera} {name}_{2}~ \TYP{T} {name}_{3} = 10^{12}  {name}_{1}\)\\
+\(\KWD{unit} \TYP{giga} {name}_{1}~\TYP{giga} {name}_{2}~ \TYP{G} {name}_{3} = 10^{9}  {name}_{1}\)\\
+\(\KWD{unit} \TYP{mega} {name}_{1}~\TYP{mega} {name}_{2}~ \TYP{M} {name}_{3} = 10^{6}  {name}_{1}\)\\
+\(\KWD{unit} \TYP{kilo} {name}_{1}~\TYP{kilo} {name}_{2}~ \TYP{k} {name}_{3} = 10^{3}  {name}_{1}\)\\
+\(\KWD{unit} \TYP{hecto} {name}_{1}~\TYP{hecto} {name}_{2}~ \TYP{h} {name}_{3} = 10^{2}  {name}_{1}\)\\
+\(\KWD{unit} \TYP{deka} {name}_{1}~\TYP{deka} {name}_{2}~ \TYP{da} {name}_{3} = 10  {name}_{1}\)\\
+\(\KWD{unit} \TYP{deci} {name}_{1}~\TYP{deci} {name}_{2}~ \TYP{d} {name}_{3} = 10^{-1}  {name}_{1}\)\\
+\(\KWD{unit} \TYP{centi} {name}_{1}~\TYP{centi} {name}_{2}~ \TYP{c} {name}_{3} = 10^{-2}  {name}_{1}\)\\
+\(\KWD{unit} \TYP{milli} {name}_{1}~\TYP{milli} {name}_{2}~ \TYP{m} {name}_{3} = 10^{-3}  {name}_{1}\)\\
+\(\KWD{unit} \TYP{micro} {name}_{1}~\TYP{micro} {name}_{2}~ \mu {name}_{3} = 10^{-6}  {name}_{1}\)\\
+\(\KWD{unit} \TYP{nano} {name}_{1}~\TYP{nano} {name}_{2}~ \TYP{n} {name}_{3} = 10^{-9}  {name}_{1}\)\\
+\(\KWD{unit} \TYP{pico} {name}_{1}~\TYP{pico} {name}_{2}~ \TYP{p} {name}_{3} = 10^{-12}  {name}_{1}\)\\
+\(\KWD{unit} \TYP{femto} {name}_{1}~\TYP{femto} {name}_{2}~ \TYP{f} {name}_{3} = 10^{-15}  {name}_{1}\)\\
+\(\KWD{unit} \TYP{atto} {name}_{1}~\TYP{atto} {name}_{2}~ \TYP{a} {name}_{3} = 10^{-18}  {name}_{1}\)\\
+\(\KWD{unit} \TYP{zepto} {name}_{1}~\TYP{zepto} {name}_{2}~ \TYP{z} {name}_{3} = 10^{-21}  {name}_{1}\)\\
+\(\KWD{unit} \TYP{yocto} {name}_{1}~\TYP{yocto} {name}_{2}~ \TYP{y} {name}_{3} = 10^{-24}  {name}_{1}\)
+\end{Fortress}
+where $\mu$ is the Unicode character U+00B5 MICRO SIGN.
+Third, a \KWD{dim} declaration and a \KWD{unit} or
+\EXP{\KWD{SI{\char'137}unit}} declaration
+may be collapsed into a single declaration by writing the \KWD{unit}
+or \EXP{\KWD{SI{\char'137}unit}}
+declaration in place of the \KWD{default} clause in the \KWD{dim} declaration
+and omitting the colon and dimension from the \KWD{unit} declaration.
+Thus
+%% dim Length  SI_unit meter meters m_
+%% dim Power = Energy/Time  SI_unit watt watts W_ = joule/second
+\begin{Fortress}
+\(\KWD{dim} \TYP{Length}  \KWD{SI{\char'137}unit} \TYP{meter}\mskip 4mu plus 4mu\TYP{meters}\mskip 4mu plus 4mu\mathrm{m}\)\\
+\(\KWD{dim} \TYP{Power} = \TYP{Energy}/\TYP{Time}  \KWD{SI{\char'137}unit} \TYP{watt}\mskip 4mu plus 4mu\TYP{watts}\mskip 4mu plus 4mu\mathrm{W} = \TYP{joule}/\TYP{second}\)
+\end{Fortress}
+is understood to abbreviate
+%% dim Length default meter; SI_unit meter meters m_: Length
+%% dim Power = Energy/Time default watt; SI_unit watt watts W_: Power = joule/second
+\begin{Fortress}
+\(\KWD{dim} \TYP{Length} \KWD{default} \TYP{meter}; \KWD{SI{\char'137}unit} \TYP{meter}\mskip 4mu plus 4mu\TYP{meters}\mskip 4mu plus 4mu\mathrm{m}\COLON \TYP{Length}\)\\
+\(\KWD{dim} \TYP{Power} = \TYP{Energy}/\TYP{Time} \KWD{default} \TYP{watt}; \KWD{SI{\char'137}unit} \TYP{watt}\mskip 4mu plus 4mu\TYP{watts}\mskip 4mu plus 4mu\mathrm{W}\COLON \TYP{Power} = \TYP{joule}/\TYP{second}\)
+\end{Fortress}
+In this way the names of the seven SI base units, along with all
+possible plural and prefixed forms, may be concisely defined as follows:
+%% dim Length  SI_unit meter meters m_
+%% dim Mass default kilogram; SI_unit gram grams g_: Mass
+%% dim Time  SI_unit second seconds s_
+%% dim ElectricCurrent  SI_unit ampere amperes A_
+%% dim Temperature  SI_unit kelvin kelvins K_
+%% dim AmountOfSubstance  SI_unit mole moles mol_
+%% dim LuminousIntensity  SI_unit candela candelas cd_
+\begin{Fortress}
+\(\KWD{dim} \TYP{Length}  \KWD{SI{\char'137}unit} \TYP{meter}\mskip 4mu plus 4mu\TYP{meters}\mskip 4mu plus 4mu\mathrm{m} \)\\
+\(\KWD{dim} \TYP{Mass} \KWD{default} \TYP{kilogram}; \KWD{SI{\char'137}unit} \TYP{gram}\mskip 4mu plus 4mu\TYP{grams}\mskip 4mu plus 4mu\mathrm{g}\COLON \TYP{Mass}\)\\
+\(\KWD{dim} \TYP{Time}  \KWD{SI{\char'137}unit} \TYP{second}\mskip 4mu plus 4mu\TYP{seconds}\mskip 4mu plus 4mu\mathrm{s}\)\\
+\(\KWD{dim} \TYP{ElectricCurrent}  \KWD{SI{\char'137}unit} \TYP{ampere}\mskip 4mu plus 4mu\TYP{amperes}\mskip 4mu plus 4mu\mathrm{A}\)\\
+\(\KWD{dim} \TYP{Temperature}  \KWD{SI{\char'137}unit} \TYP{kelvin}\mskip 4mu plus 4mu\TYP{kelvins}\mskip 4mu plus 4mu\mathrm{K}\)\\
+\(\KWD{dim} \TYP{AmountOfSubstance}  \KWD{SI{\char'137}unit} \TYP{mole}\mskip 4mu plus 4mu\TYP{moles}\mskip 4mu plus 4mu\mathrm{mol}\)\\
+\(\KWD{dim} \TYP{LuminousIntensity}  \KWD{SI{\char'137}unit} \TYP{candela}\mskip 4mu plus 4mu\TYP{candelas}\mskip 4mu plus 4mu\mathrm{cd}\)
+\end{Fortress}
+Note the subtle difference in the declaration of \TYP{Mass} that
+allows the default unit to be \TYP{kilogram} rather than \TYP{gram}.
+
+
+\section{Absorbing Units}
+\seclabel{absorbing-units}
+
+\begin{Grammar}
+\emph{StaticParam}
+&::=& \emph{Id} \option{\emph{Extends}} \options{\KWD{absorbs} \KWD{unit}} \\
+&$|$& \KWD{unit} \emph{Id} \options{\EXP{\mathrel{\mathtt{:}}} \emph{Type}}
+ \options{\KWD{absorbs} \KWD{unit}}\\
+\end{Grammar}
+
+The declaration of a type parameter or a \KWD{unit} parameter for
+a parameterized trait may contain a clause
+``\EXP{\KWD{absorbs}\;\;\KWD{unit}}''; at
+most one static parameter of a trait may have this clause.  An
+instance of a parameterized trait
+with a static parameter that ``\EXP{\KWD{absorbs}\;\;\KWD{unit}}'' may
+be multiplied
+or divided by a unit, the result being another instance of that
+parameterized trait in which the static argument corresponding to
+the unit-absorbing parameter has been multiplied or divided by the unit.
+
+A few examples should make this clear.  Given the declaration
+%% trait Vector[\EltType extends Number absorbs unit, nat len\] \ldots end
+\begin{Fortress}
+\(\KWD{trait} \TYP{Vector}\llbracket\TYP{EltType} \KWD{extends} \TYP{Number} \KWD{absorbs}\;\;\KWD{unit}, \KWD{nat} \VAR{len}\rrbracket \ldots \KWD{end}\)
+\end{Fortress}
+then \EXP{\TYP{Vector}\llbracket\TYP{Float}, 3\rrbracket \TYP{meter}}
+means the same as
+\EXP{\TYP{Vector}\llbracket\TYP{Float}\mskip 4mu plus 4mu\TYP{meter}, 3\rrbracket},
+and \EXP{\TYP{Vector}\llbracket\TYP{Float}, 3\rrbracket /
+  \TYP{second}} means the same as
+\EXP{\TYP{Vector}\llbracket\TYP{Float} / \TYP{second}, 3\rrbracket}.
+Therefore,
+%[(3 m_) (2 m_) (5 m_)]
+\EXP{[(3\,\mathrm{m}) (2\,\mathrm{m}) (5\,\mathrm{m})]}
+means the same as
+%[3 2 5] m_
+\EXP{[3\;2\;5] \mathrm{m}}.
+%
+Similarly, given the declaration
+%% trait Float[\unit U absorbs unit, nat e, nat s\] \ldots end
+\begin{Fortress}
+\(\KWD{trait} \TYP{Float}\llbracket\KWD{unit} U \KWD{absorbs}\;\;\KWD{unit}, \KWD{nat} e, \KWD{nat} s\rrbracket \ldots \KWD{end}\)
+\end{Fortress}
+then \EXP{\TYP{Float}\llbracket\TYP{meter}, 11, 53\rrbracket /
+  \TYP{second}} means the same as
+\EXP{\TYP{Float}\llbracket\TYP{meter} / \TYP{second}, 11, 53\rrbracket}, and
+\begin{Fortress}
+%% Float[\dimensionless, 8, 24\] meter kilogram / second^2
+\EXP{\TYP{Float}\llbracket\mathbin{\TYP{dimensionless}}, 8, 24\rrbracket \TYP{meter}\mskip 4mu plus 4mu\TYP{kilogram} / \TYP{second}^{2}}
+\end{Fortress}
+means the same as
+\begin{Fortress}
+%% Float[\dimensionless meter kilogram / second^2, 8, 24\]
+\EXP{\TYP{Float}\llbracket\mathbin{\TYP{dimensionless}}\, \TYP{meter}\mskip 4mu plus 4mu\TYP{kilogram} / \TYP{second}^{2}, 8, 24\rrbracket},
+\end{Fortress}
+which is the same as
+%% Float[\meter kilogram / second^2, 8, 24\]
+\begin{Fortress}
+\EXP{\TYP{Float}\llbracket\TYP{meter}\mskip 4mu plus 4mu\TYP{kilogram} / \TYP{second}^{2}, 8, 24\rrbracket}.
+\end{Fortress}
+This is the mechanism by which meaning is given to the multiplication
+and division of library-defined types by units.

trunk/Specification/advanced/domain-specific-languages.tex

@@ -18 +18 @@
 \chapter{Support for Domain-Specific Languages}
 \chaplabel{syntax-expanders}
+
+\note{This chapter will include the Fortress syntactic abstraction mechanism
+described in ~\cite{fool09}.}

trunk/Specification/advanced/operator-definitions.tex

@@ -18 +18 @@
 \chapter{Operator Declarations}
 \chaplabel{operatordefs}
+
+\note{Multifix operators and keyword parameters are not yet supported.}
+
+An operator declaration may appear anywhere a top-level function or
+method declaration may appear.  Operator declarations are like other
+function or method declarations in all respects except that an
+operator declaration has \KWD{opr} and has
+an operator name (see \secref{operator-names} for a discussion of
+valid operator names) instead of an identifier.  The precise placement
+of the operator name within the declaration depends on the fixity of
+the operator.  Like other functionals, operators may have overloaded
+declarations (see \chapref{multiple-dispatch} for a discussion of
+overloading).  These overloadings may be of the same or differing
+fixities.
+
+\begin{Grammar}
+\emph{FnDecl}
+&::=& \option{\emph{FnMods}} \emph{FnHeaderFront} \emph{FnHeaderClause}
+\options{\EXP{=} \emph{Expr}} \\
+
+\emph{FnHeaderFront}  &::=& \emph{OpHeaderFront} \\
+
+\emph{OpHeaderFront}
+&::=& \KWD{opr} \option{\KWD{BIG}}
+(\{\EXP{\mapsto} $|$ \emph{LeftEncloser} $|$ \emph{Encloser}) \option{\emph{StaticParams}}
+\option{\emph{Params}} \\
+&&(\emph{RightEncloser} $|$ \emph{Encloser}) \\
+&$|$& \KWD{opr} \emph{ValParam}
+(\emph{Op} $|$ \emph{ExponentOp}) \option{\emph{StaticParams}} \\
+&$|$& \KWD{opr} \option{\KWD{BIG}}
+(\emph{Op} $|$ \texttt{\^} $|$ \emph{Encloser} $|$ $\sum$ $|$ $\prod$)
+ \option{\emph{StaticParams}} \emph{ValParam} \\
+
+\emph{MdDecl} &::=& \emph{MdDef} \\
+&$|$& \option{\KWD{abstract}}
+\option{\emph{MdMods}} \emph{MdHeaderFront}
+\emph{FnHeaderClause} \\
+
+\emph{MdHeaderFront}  &::=& \emph{OpMdHeaderFront} \\
+
+\emph{OpMdHeaderFront}
+&::=& \KWD{opr} \option{\KWD{BIG}}
+(\{\EXP{\mapsto} $|$ \emph{LeftEncloser} $|$ \emph{Encloser}) \option{\emph{StaticParams}}
+\option{\emph{Params}} \\
+&&(\emph{RightEncloser} $|$ \emph{Encloser}) \\
+&&\options{\EXP{\ASSIGN} \texttt( \emph{SubscriptAssignParam} \texttt)}
+\\
+&$|$& \KWD{opr} \emph{ValParam}
+(\emph{Op} $|$ \emph{ExponentOp}) \option{\emph{StaticParams}} \\
+&$|$& \KWD{opr} \option{\KWD{BIG}}
+(\emph{Op} $|$ \texttt{\^} $|$ \emph{Encloser} $|$ $\sum$ $|$ $\prod$)
+ \option{\emph{StaticParams}} \emph{ValParam} \\
+
+\emph{SubscriptAssignParam}
+&::=& \emph{Varargs}\\
+&$|$& \emph{Param}\\
+\end{Grammar}
+
+An operator declaration has one of eight
+forms:
+multifix operator declaration,
+infix operator declaration,
+prefix operator declaration, postfix operator declaration,
+nofix operator declaration,
+bracketing operator declaration,
+subscripting operator method declaration,
+and subscripted assignment operator method declaration.
+Each is invoked according to specific rules of syntax.
+An operator method declaration must be a functional method declaration,
+a subscripting operator method declaration, or a subscripted assignment
+operator method declaration.
+
+\section{Multifix Operator Declarations}
+
+A multifix operator declaration has \KWD{opr}
+and then an operator name where a
+functional declaration would have an identifier.
+The declaration must not have any keyword parameters, and must
+be capable of accepting at least two arguments.  It is permissible
+to use a varargs parameter; in fact, this is a good way to
+define a multifix operator.
+Static parameters (described in \chapref{trait-parameters})
+ may also be present, between the operator and
+the parameter list.
+
+An expression consisting of a multifix operator applied to
+an expression will invoke a multifix operator declaration.
+The compiler considers all multifix operator declarations for that
+operator that are both
+accessible and applicable, and the most specific operator declaration
+is chosen according to the usual rules for overloaded functionals.
+The invocation will pass more than two arguments.
+
+A multifix operator declaration may also be invoked
+by an infix, a prefix, or nofix (but not a postfix) operator application if
+the declaration is applicable.
+
+Example:
+\note{Example is commented out because it is not supported nor run by the interpreter yet.}
+%\input{\home/advanced/examples/OprDecl.Multifix.tex}
+
+\section{Infix Operator Declarations}
+
+An infix operator declaration has \KWD{opr}
+and then an operator name where a
+functional declaration would have an identifier.
+The declaration must have two value parameter,
+which must not be a keyword parameter or varargs parameter.
+Static parameters may also be present,
+between the operator and the parameter list.
+
+An expression consisting of an infix operator applied to
+an expression will invoke an infix operator declaration.
+The compiler considers all infix and multifix
+operator declarations for that
+operator that are both
+accessible and applicable, and the most specific operator declaration
+is chosen according to the usual rules for overloaded functionals.
+
+Note that superscripting (\txt{{\char'136}}) may be defined using
+an infix operator declaration even though it has very high precedence
+and cannot be used as a multifix operator.
+
+Example:
+\input{\home/advanced/examples/OprDecl.Infix.tex}
+
+\section{Prefix Operator Declarations}
+
+A prefix operator declaration has \KWD{opr}
+and then an operator name where a
+functional declaration would have an identifier.
+The declaration must have one value parameter, which must not be a keyword parameter
+or varargs parameter.
+Static parameters may also be present, between the operator and the parameter list.
+
+An expression consisting of a prefix operator applied to
+an expression will invoke a prefix operator declaration.
+The compiler considers all prefix and multifix
+operator declarations for that
+operator that are both
+accessible and applicable, and the most specific operator declaration
+is chosen according to the usual rules for overloaded functionals.
+
+Example:
+\input{\home/advanced/examples/OprDecl.Prefix.tex}
+
+\section{Postfix Operator Declarations}
+\seclabel{postfix-opr-decl}
+
+A postfix operator declaration has \KWD{opr} where a
+functional declaration would have an identifier;
+the operator name itself \emph{follows} the parameter list.
+The declaration must have one value parameter, which must not be a keyword parameter
+or varargs parameter.
+Static parameters may also be present, between \KWD{opr}
+and the parameter list.
+
+An expression consisting of a postfix operator applied to
+an expression will invoke a postfix operator declaration.
+The compiler considers all postfix operator declarations for that
+operator that are both
+accessible and applicable, and the most specific operator declaration
+is chosen according to the usual rules for overloaded functionals.
+
+Example:
+\input{\home/advanced/examples/OprDecl.Postfix.tex}
+
+
+\section{Nofix Operator Declarations}
+
+A nofix operator declaration has \KWD{opr}
+and then an operator name where a functional declaration would have an
+identifier.  The declaration must have no parameters.
+
+An expression consisting only of a nofix operator
+will invoke a nofix operator declaration.
+The compiler considers all nofix and multifix
+operator declarations
+for that operator that are both
+accessible and applicable, and the most specific operator declaration
+is chosen according to the usual rules for overloaded functionals.
+
+Uses for nofix operators are rare, but those rare examples are very useful.
+For example, if the \EXP{@} operator is used to construct subscripting ranges,
+and it is the nofix declaration of \EXP{@} that allows a lone \EXP{@} to be
+used as a subscript:
+\input{\home/advanced/examples/OprDecl.Nofix.tex}
+
+
+\section{Bracketing Operator Declarations}
+\seclabel{bracketing-opr-decl}
+
+A bracketing operator declaration has \KWD{opr}
+where a functional declaration would have an identifier.
+The value parameter list, rather than being surrounded by parentheses,
+is surrounded by the brackets being defined.  A bracketing operator
+declaration may have any number of parameters, keyword parameters,
+and varargs parameters in the value parameter list.  Static parameters may
+also be present, between \KWD{opr} and the parameter list.  Any paired
+Unicode brackets
+may be so defined \emph{except} ordinary parentheses
+and white square brackets.
+
+An expression consisting of zero or more comma-separated expressions
+surrounded by a  bracket pair will invoke a bracketing operator
+declaration.  The compiler considers all bracketing operator
+declarations for that type of bracket pair that are both accessible and applicable, and the most
+specific operator declaration is chosen according to the usual rules for
+overloaded functionals.
+For example, the expression \EXP{\langle p,q \rangle} might invoke the
+following bracketing method declaration:
+\input{\home/advanced/examples/OprDecl.Bracketing.tex}

trunk/Specification/advanced/overloading.tex

@@ -18 +18 @@
 \chapter{Overloaded Functional Declarations}
 \chaplabel{overloaded-declarations}
+
+\note{Keyword and varargs parameters are not yet supported.}
+
+Fortress allows multiple functional declarations to be in scope of a
+particular program point.  We call this overloading.
+\chapref{multiple-dispatch} describes
+how to determine which overloaded declarations are
+applicable to a particular functional call, and when several
+are applicable, how to select the most specific one among them.
+In this chapter, we give a
+set of rules on overloaded declarations that guarantee there
+exists a most specific declaration for any given functional call.
+These rules are complicated by the presence of coercion, which may
+enlarge the set of declarations that are applicable to a functional
+call, as discussed in \chapref{conversions-coercions}.
+
+
+
+\section{Principles of Overloading}
+\seclabel{principles-overloading}
+
+Fortress allows multiple functional declarations of the same name to
+be declared in a single scope.  However, recall from \chapref{names}
+the following shadowing rules:
+\begin{itemize}
+\item
+dotted method declarations shadow top-level function declarations with
+the same name, and
+\item
+dotted method declarations provided by a trait or object declaration
+or object expression
+shadow functional method declarations with the same name that are
+provided by a different trait or object declaration
+or object expression.
+\end{itemize}
+Also, note that a trait or object declaration
+or object expression must not have a
+functional method declaration and a dotted method declaration with the
+same name, either directly or by inheritance.
+Therefore, top-level functions can overload
+with other top-level functions and functional methods, dotted methods with
+other dotted methods, and functional methods with other functional methods
+and top-level functions.
+
+Overloading functional declarations allows the benefits of polymorphic
+declarations.  However, with these benefits comes the potential for
+ambiguous calls at run time.  Fortress provides overloading rules for the
+\emph{declarations} of functionals to eliminate the \emph{possibility}
+of ambiguous calls at run time, whether or not these calls actually
+appear in the program.
+
+For each functional application expression, it should be a static error
+if there does not exist a statically most applicable declaration for
+that expression.
+Furthermore, these rules are checked statically.
+In fact, the overloading rules
+in Fortress allow the compiler to identify the
+statically most specific declaration for a particular call.  Therefore
+an implementation strategy may be used in which the statically most
+specific declaration is identified statically, and the runtime
+dispatch mechanism need only consider dispatching among that
+declaration plus declarations that are more specific than that
+declaration (proof of this is given in \secref{proof-overloading-resolution}).
+
+This chapter outlines several criteria for valid functional
+overloading.  At any given program point, there is a set of overloaded
+declarations that are in scope.  Fortress determines whether there is
+a possibility for ambiguous calls from this set by comparing
+declarations pairwise.  The following three sections each describes a
+rule to accept a pair of overloaded functional declarations.  If a
+pair of overloaded declarations satisfies any one of the three rules,
+it is considered a valid overloading.
+
+The overloading rules given in this chapter are disjoint.  That is, at
+most one rule applies to each pair of overloaded declarations.  It is
+possible for new rules to be added which allow additional
+overloadings.
+
+\label{adv-over-kwd}
+Overloaded declarations must have static parameters that are identical
+(up to $\alpha$-equivalence).  Also, valid overloadings for
+declarations that contain keyword or
+varargs parameters are determined
+by analyzing the expansion of these declarations as described in
+\secref{applicability-with-special-params}.  Therefore, static
+parameters, keyword parameters,
+and varargs parameters are ignored in
+the remainder of this chapter.
+
+An operator method declaration whose name is one of the operator parameters
+(described in \secref{opr-ident})
+of its enclosing trait or object may be overloaded with other operator
+declarations in the same component.  Therefore, such an operator method
+declaration must satisfy the overloading rules
+with every operator declaration in the same component.
+
+
+
+In addition, a functional which takes a single parameter of type
+a naked type parameter of bound \TYP{Any} cannot be
+overloaded.  This restriction prevents ambiguous overloadings such as
+the following:
+%makeSet[\T extends Any\](x: T): Set[\T\]
+%makeSet[\T extends Any\](x: T, y: T): Set[\T\]
+\begin{Fortress}
+\(\VAR{makeSet}\llbracket{}T \KWD{extends}\mskip 4mu plus 4mu\TYP{Any}\rrbracket(x\COLON T)\COLON \TYP{Set}\llbracket{}T\rrbracket\)\\
+\(\VAR{makeSet}\llbracket{}T \KWD{extends}\mskip 4mu plus 4mu\TYP{Any}\rrbracket(x\COLON T, y\COLON T)\COLON \TYP{Set}\llbracket{}T\rrbracket\)
+\end{Fortress}
+The type parameter of \EXP{\VAR{makeSet}} may be instantiated with
+\TYP{(\mathbb{Z}, \mathbb{Z})} or \TYP{\mathbb{Z}}.  If this is the
+case then the call \EXP{\VAR{makeSet}(3, 4)}, where 3 and 4 have type
+\TYP{\mathbb{Z}}, is ambiguous.
+
+\secref{subtype-rule} states the \emph{Subtype Rule}, which stipulates
+that the parameter type of one declaration be a subtype of the
+parameter type of the other.  In this case, there is no possibility of
+ambiguous calls, because one declaration is more specific than the
+other.  This section also places a restriction on the return types of
+the overloaded declarations to ensure that type safety is not
+violated.  \secref{incompatibility-rule} defines the \emph{
+Incompatibility Rule} that, if satisfied by a pair of declarations,
+guarantees that neither declaration is applicable to the same
+functional call.  In \secref{more-specific-rule}, the \emph{Meet Rule}
+requires the existence of a declaration that is more specific than
+both overloaded declarations in the situation that both are applicable
+to a given call.
+
+In the remainder of this chapter, we build on the terminology and
+notation defined in \chapref{multiple-dispatch}
+and \chapref{conversions-coercions}.
+
+
+
+\section{Subtype Rule}
+\seclabel{subtype-rule}
+
+If the parameter type of one declaration is a subtype of the parameter
+type of another (and they are not the same) then there is no
+ambiguity between these two declarations: for every call to which both
+are applicable, the first is more specific.  This is the basis of the
+Subtype Rule.
+
+The Subtype Rule also requires a relationship between the return types
+of the two declarations.  Without such a requirement, a program may
+violate type safety.
+
+\paragraph{The Subtype Rule for Functions and Functional Methods:}
+Suppose that $\f(\Ps) : \Us$ and $\f(\Qs) : \Vs$ are two distinct
+function or functional method declarations in a single scope.
+If $\Ps \strictsubtype \Qs$ and $\Us \Ovrsubtype \Vs$ then $\f(\Ps)$ and
+$\f(\Qs)$ are a valid overloading.
+
+\paragraph{The Subtype Rule for Dotted Methods:}
+Suppose that $\Ps_0.\f(\Ps) : \Us$ and $\Qs_0.\f(\Qs) : \Vs$ are two
+distinct dotted method declarations provided by a trait or object $C$.
+If $\Ps_0 \strictsubtype \Qs_0$, $\Ps \strictsubtype \Qs$,
+and $\Us \Ovrsubtype
+\Vs$ then $\Ps_0.\f(\Ps)$ and $\Qs_0.\f(\Qs)$ are a valid overloading.
+
+\section{Incompatibility Rule}
+\seclabel{incompatibility-rule}
+
+The basic idea behind the Incompatibility Rule is that if there is no
+call to which two overloaded declarations are both applicable
+then there is no potential for ambiguous calls.  In such a case, we say
+that the declarations are incompatible.
+Without coercion, incompatibility is equivalent to exclusion.
+However, the presence of coercion complicates the definition of
+incompatibility.  To formally define incompatibility we first define the
+following notation.
+%
+For types $T$ and $U$,
+we say that $T$ and $U$ \emph{do not share coercions}, and write
+$T \noshare U$, if any type that coerces to $T$ excludes any type
+that coerces to $U$:
+\[
+T \noshare U \iff \forall A,B: A \coercedefto T \logicand B \coercedefto U
+                               \implies A \excludes B.
+\]
+%
+We say that $T$ \emph{is incompatible with} $U$, and write $T
+\incompatible U$, if $T$ and $U$ exclude, reject each other, and do
+not share coercions:
+\begin{align*}
+T \incompatible U \iff
+&T \excludes U \logicand T \rejects U \logicand U \rejects T \logicand  T \noshare U \\
+\iff
+&\phantom{\logicand\ } T \excludes U \\
+&\logicand\ (\forall A: A \coercedefto T \implies A \excludes U) \\
+&\logicand\ (\forall B: B \coercedefto U \implies B \excludes T) \\
+&\logicand\ (\forall A,B: A \coercedefto T \logicand B \coercedefto U
+                          \implies A \excludes B)
+\end{align*}
+Note that if $T \incompatible U$ then no type is substitutable for
+both $T$ and $U$.
+
+\paragraph{The Incompatibility Rule for Functions and Functional Methods:}
+
+Suppose that $\f(\Ps)$ and $\f(\Qs)$ are two distinct function or
+functional method declarations in a single scope.
+If $\Ps \incompatible \Qs$ then $\f(\Ps)$ and $\f(\Qs)$ are a valid overloading.
+
+\paragraph{The Incompatibility Rule for Dotted Methods:}
+Suppose that $\Ps_0.\f(\Ps)$ and $\Qs_0.\f(\Qs)$ are two distinct
+dotted method declarations provided by a trait or object $C$.  If
+$\Ps \incompatible \Qs$ then $\Ps_0.\f(\Ps)$ and $\Qs_0.\f(\Qs)$ are
+a valid overloading.
+
+\section{Meet Rule}
+\seclabel{more-specific-rule}
+
+If neither the Subtype Rule nor the Incompatibility Rule holds for a
+pair of overloaded declarations then the declarations introduce the
+possibility of ambiguity.  To avoid this ambiguity, we require a
+\emph{disambiguating declaration}; this is, for every call to which
+both declarations are applicable, there must be a third, more
+specific, declaration that is also applicable.  Thus, at run time,
+neither of the pair of declarations is executed because the
+disambiguating declaration is also applicable, and it is more specific
+than both.
+
+\note{What is "an intersection of two declarations"?
+-- Sukyoung
+
+For function declarations we require that the disambiguating
+declaration be the intersection of the pair of overloaded
+declarations.}
+
+\paragraph{The Meet Rule for Functions:}
+Suppose that $\f(\Ps)$ and $\f(\Qs)$ are two function
+declarations in a single scope
+such that neither $\Ps$ nor $\Qs$ is a subtype of the other and $\Ps$ and
+$\Qs$ are not incompatible with one another.
+Let $\mathpzc{S}$ be the set of types that $\Ps$ defines coercions from
+and $\mathpzc{T}$ be the set of types that $\Qs$ defines coercions from.
+$\f(\Ps)$ and $\f(\Qs)$ are a valid overloading if
+there is a declaration $\f(\Ps \inter \Qs)$ in the scope.
+
+all of the following hold:
+\begin{itemize}
+\item
+either $\Ps \excludes \Qs$ or there is a declaration $\f(\Ps \inter
+\Qs)$ in the scope,
+and
+\item
+either $\Ps \morespecific \Qs$ or $\Qs \morespecific \Ps$ or for all
+$\Ps' \in \mathpzc{S}$ and $\Qs' \in \mathpzc{T}$ one of the two
+conditions holds:
+\begin{itemize}
+\item
+$\Ps' \excludes \Qs'$, or
+\item
+there is a declaration $\f(\Ps' \inter \Qs')$ in the scope.
+\end{itemize}
+\end{itemize}
+
+Recall that $\Ps \inter \Qs$ is the intersection of types $\Ps$ and $\Qs$
+as defined in \secref{internal-types}.
+We write $\Ps \inter \Qs$ to denote the intersection of types $\Ps$ and $\Qs$.
+If for some type $S$ we have $S \Ovrsubtype P$ and $S \Ovrsubtype Q$ then
+$S \Ovrsubtype (P \intersect Q)$, but it is not necessarily the
+case that $S = (P \intersect Q)$ since another type may be more
+specific than both $P$ and $Q$.
+\label{adv-over-comprises}
+For example, suppose the following:
+%trait S comprises {U,V} end
+%trait T comprises {V,W} end
+%trait U extends S excludes W end
+%trait V extends {S,T} end
+%trait W extends T end
+%
+%f(s:S) = 1
+%f(t:T) = 1
+%f(v:V) = 1
+\begin{Fortress}
+\(\KWD{trait} S \KWD{comprises} \{U,V\} \KWD{end}\)\\
+\(\KWD{trait} T \KWD{comprises} \{V,W\} \KWD{end}\)\\
+\(\KWD{trait} U \KWD{extends} S \KWD{excludes} W \KWD{end}\)\\
+\(\KWD{trait} V \KWD{extends} \{S,T\} \KWD{end}\)\\
+\(\KWD{trait} W \KWD{extends} T \KWD{end}\)\\[4pt]
+\(f(s\COLONOP{}S) = 1\)\\
+\(f(t\COLONOP{}T) = 1\)\\
+\(f(v\COLONOP{}V) = 1\)
+\end{Fortress}
+Because of the \KWD{comprises} clauses of $S$ and $T$ and the \KWD{excludes}
+clause of $U$, any subtype of both $S$ and $T$ must be a subtype of
+$V$.  Thus, $V = S \inter T$, and the declaration $f(V)$
+``disambiguates'' $f(S)$ and $f(T)$, i.e., it is applicable to and more
+specific for any call to which both $f(S)$ and $f(T)$ are applicable.
+
+The Meet Rule shall not be difficult to obey, especially because
+the compiler can give useful feedback.  For example:
+
+%  foo(x:Number, y:ZZ64) = ...
+%  foo(x:ZZ64, y:Number) = ...
+\begin{Fortress}
+{\tt~~}\pushtabs\=\+\(  \VAR{foo}(x\COLONOP\TYP{Number}, y\COLONOP\mathbb{Z}64) = \ldots\)\\
+\(  \VAR{foo}(x\COLONOP\mathbb{Z}64, y\COLONOP\TYP{Number}) = \ldots\)\-\\\poptabs
+\end{Fortress}
+
+Assuming that \(\hbox{\ZZ64} \prec \hbox{\TYP{Number}}\), the compiler
+reports that these two declarations are a problem because of ambiguity
+and suggests that a new declaration for \EXP{\VAR{foo}({\ZZ64},
+{\ZZ64})} would resolve the ambiguity. As another example, consider:
+
+% bar(x:Printable) = ...
+% bar(x:Throwable) = ...
+\begin{Fortress}
+{\tt~}\pushtabs\=\+\( \VAR{bar}(x\COLONOP\TYP{Printable}) = \ldots\)\\
+\( \VAR{bar}(x\COLONOP\TYP{Throwable}) = \ldots\)\-\\\poptabs
+\end{Fortress}
+
+Assuming that $\hbox{\TYP{Printable}}$ and $\hbox{\TYP{Throwable}}$
+are neither comparable by the subtyping relation nor disjoint, the
+compiler reports that these two declarations are a problem because
+\TYP{Printable} and \TYP{Throwable} are incomparable but possibly
+overlapping types.
+As a result, these two declarations are statically rejected.
+
+Unlike for functions, the Meet Rule for dotted methods only applies to
+dotted methods that are provided by the same trait or object.  This is
+possible because two dotted methods are applicable to a given call
+$\As_0.f(\As)$ only if they are both provided by the trait or object
+$\As_0$.
+
+\paragraph{The Meet Rule for Dotted Methods:}
+Suppose that $\Ps_0.\f(\Ps)$ and $\Qs_0.\f(\Qs)$ are two dotted method
+declarations provided by a trait or object $C$ such that neither
+$(\Ps_0, \Ps)$ nor $(\Qs_0, \Qs)$ is a subtype of the other and $\Ps$
+and $\Qs$ are not incompatible with one another.
+Let $\mathpzc{S}$ be the set of
+types that $\Ps$ defines coercions from and $\mathpzc{T}$ be the set
+of types that $\Qs$ defines coercions from.
+$\Ps_0.\f(\Ps)$ and
+$\Qs_0.\f(\Qs)$ are a valid overloading if
+there is a declaration $\Rs_0.\f(\Ps
+\inter \Qs)$ provided by $C$ with $\Rs_0 \Ovrsubtype (\Ps_0 \inter
+\Qs_0)$.
+
+all of the following hold:
+\begin{itemize}
+\item
+either $\Ps \excludes \Qs$ or there is a declaration $\Rs_0.\f(\Ps
+\inter \Qs)$ provided by $C$ with $\Rs_0 \Ovrsubtype (\Ps_0 \inter
+\Qs_0)$, and
+\item
+either $\Ps \morespecific \Qs$ or $\Qs \morespecific \Ps$ or
+for all $\Ps' \in \mathpzc{S}$ and
+$\Qs' \in \mathpzc{T}$ one of the two conditions holds:
+\begin{itemize}
+\item
+$\Ps' \excludes \Qs'$, or
+\item
+there is a declaration $\Rs_0.\f(\Ps' \inter \Qs')$ provided by $C$
+with $\Rs_0 \Ovrsubtype (\Ps_0 \inter \Qs_0)$.
+\end{itemize}
+\end{itemize}
+
+Recall that functional methods can be viewed semantically as top-level
+functions, as described in \secref{methods}.  However, treating
+functional methods as top-level functions for determining valid
+overloading is too restrictive.  In the following example:
+\input{\home/advanced/examples/Overloading.tex}
+if the functional methods were interpreted as top-level functions then
+this program would define two top-level functions with parameter types
+\EXP{\mathbb{Z}} and \EXP{\mathbb{R}}.
+These declarations would be
+statically rejected as
+an invalid overloading because there is no
+relation between \EXP{\mathbb{Z}} and \EXP{\mathbb{R}}; another trait
+may extend them both without declaring its own version of the
+functional method which may lead to an ambiguous call at run time.
+However, notice that declaraions are ambiguous only for calls on
+arguments that extend both \EXP{\mathbb{Z}} and \EXP{\mathbb{R}}, and
+any type that extends both can include a new declaration that
+disambiguates them.  We use this intuition to allow such overloadings.
+
+\paragraph{The Meet Rule for Functional Methods:}
+Suppose that $\f(\Ps)$ and $\f(\Qs)$ are two functional method
+declarations occurring in trait or object declarations or object expressions
+such that neither $\Ps$ nor $\Qs$ is a subtype of the other and $\Ps$ and $\Qs$
+are not incompatible with one another.  Let $\f(\Ps)$ and $\f(\Qs)$
+have self parameters at $i$ and $j$ respectively.
+$\f(\Ps)$ and $\f(\Qs)$ are a valid
+overloading if all of the following hold:
+\begin{itemize}
+\item
+$i = j$
+\item if there exists a trait or object $C$
+that provides both $\f(\Ps)$ and $\f(\Qs)$ then $\Ps \neq \Qs$ and
+there is a declaration $\f(\Ps \inter \Qs)$ provide by $C$
+having self parameter at $i$.
+\end{itemize}
+
+Also, let $\mathpzc{S}$ be the set of types that $\Ps$
+defines coercions from and $\mathpzc{T}$ be the set of types that
+$\Qs$ defines coercions from.  $\f(\Ps)$ and $\f(\Qs)$ are a valid
+overloading if all of the following hold:
+\begin{itemize}
+\item
+$i = j$
+\item
+either $\Ps \excludes \Qs$ or if there exists a trait or object $C$
+that provides both $\f(\Ps)$ and $\f(\Qs)$ then $\Ps \neq \Qs$ and
+there is a declaration $\f(\Ps \inter \Qs)$ provide by $C$, and
+\item
+either $\Ps \morespecific \Qs$ or $\Qs \morespecific \Ps$ or
+for all $\Ps' \in \mathpzc{S}$ and
+$\Qs' \in \mathpzc{T}$ one of the two conditions holds:
+\begin{itemize}
+\item
+$\Ps' \excludes \Qs'$, or
+\item
+there is a declaration $\f(\Ps' \inter \Qs')$ provided by $C$.
+\end{itemize}
+\end{itemize}
+
+Notice that the Meet Rule for functional methods requires the self
+parameters of two overloaded declarations to be in the same position.
+This requirement guarantees that no ambiguity is caused by the
+position of the self parameter.  Two declarations which differ in the
+position of the self parameter must satisfy either the Subtype Rule or
+the Incompatibility Rule to be a valid overloading.
+
+Functional method declarations can overload with function declaraions.
+A valid overloading between a functional method declaration and
+a function declaration is
+determined by applying the (more restrictive) Meet Rule for functions
+to both declarations.
+
+\section{Coercion and Overloading Resolution}
+
+The overloading rules given in this chapter are
+sufficient to prove the following two facts:
+\begin{enumerate}
+\item
+If no declaration is applicable to a static call but there is a
+declaration that is applicable with coercion then there exists a
+single most specific declaration that is applicable with coercion to
+the static call.
+\item
+If any declaration is applicable to a static call then there exists a
+single most specific declaration that is applicable to the static call
+and a single most specific declaration that is applicable to the
+corresponding dynamic call.
+\end{enumerate}
+
+Moreover, we can prove that the most specific declaration that is
+applicable to a dynamic call is more specific than the most specific
+declaration that is applicable to the corresponding static call.
+
+\appref{overloaded-functional} formally proves that
+the rules discussed in the previous sections guarantee the static resolution of
+coercion (described in \secref{resolving-coercion}) is well defined
+for functions (the case for methods is analogous).  Also in
+\appref{overloaded-functional} is a proof that
+the overloading rules for
+ function declarations are sufficient to guarantee no
+undefined nor ambiguous calls at run time (again,
+the case for methods is analogous).

trunk/Specification/advanced/parallelism-locality/arrays-distributed.tex

@@ -18 +18 @@
 \section{Distributed Arrays}
 \seclabel{arrays}
+
+\note{Distributions, array comprehensions, and
+\TYP{HeapSequence} are not yet supported.}
+
+Arrays, vectors, and matrices in Fortress are assumed to be spread out
+across the machine.  As in Fortran, Fortress arrays are complex data
+structures; simple linear storage is encapsulated by the
+\TYP{HeapSequence} type, which is used in the implementation of arrays
+(see \secref{parallelism-fundamentals}).
+The default distribution of
+an array is determined by the Fortress libraries; in general it
+depends on the size of the array, and on the size and locality
+characteristics of the machine running the program.
+For advanced
+users, the distribution library (introduced in \secref{distributions})
+provides a way of combining and pivoting distributions, or of
+redistributing two arrays so that their distributions match.
+Programmers must create arrays by using
+an array comprehension (\secref{comprehensions}) or
+an aggregate expression (\secref{aggregate-expr}), or by using one of
+the factory functions at the top of \figref{arrayFactories}.  After calling
+any of these factories, the elements of the resulting array must be
+initialized using either indexed assignment or using one of the
+initialization methods described at the bottom of the figure.
+
+\begin{figure}
+\begin{tabular}{|m{2.0in}|m{4.0in}|}
+\hline
+  \EXP{\VAR{array}\llbracket{}E\rrbracket(\emph{size}\COLONOP{}I)\COLONOP\TYP{Array}\llbracket{}E,I\rrbracket} & {Creates an uninitialized 0-indexed array of the specified runtime-determined size.  The size is an integer for a 1-dimensional array, a 2-tuple for a two-dimensional array, and so forth.} \\
+\hline
+  \EXP{{array}_{1}\llbracket{}E,n\rrbracket()} & {Creates an uninitialized 0-indexed 1-dimensional array of statically determined size $n$.} \\
+\hline
+  \EXP{{array}_{2}\llbracket{}E,n,m\rrbracket()} & {Creates an uninitialized 0-indexed 2-dimensional array of statically determined size $n$ by $m$.} \\
+\hline
+  \EXP{{array}_{3}\llbracket{}E,n,m,p\rrbracket()} & {Creates an uninitialized 0-indexed 3-dimensional array of statically determined size $n$ by $m$ by $p$.} \\
+\hline
+\end{tabular}
+\begin{tabular}{|m{2.0in}|m{4.0in}|}
+\hline
+\EXP{\VAR{a}.\VAR{fill}(v\COLONOP{}E)} & {Initializes all elements with value \VAR{v}.} \\
+\hline
+\EXP{\VAR{a}.\VAR{fill}(f\COLONOP{}I\rightarrow{}E)} & {Calls \VAR{f} at each index and initializes the corresponding element with the result of the call.} \\
+\hline
+\EXP{\VAR{a}.\VAR{init}(i\COLONOP{}I, v\COLONOP{}E)} & {Initializes element at index \VAR{i} with value \VAR{v}.} \\
+\hline
+\end{tabular}
+\caption{\figlabel{arrayFactories}Factories for creating arrays and methods for initializing their elements}
+\end{figure}
+
+Each array element may be initialized at most once using the methods of \figref{arrayFactories}; the programmer must assure that this initialization completes before any other access to the corresponding array element.  The programmer must also assure that an element is initialized before it is first read.\footnote{The present implementation signals a fatal error in case of duplicate initialization, or if an uninitialized element is read.}  Note that these factories and methods are intended to be used to library programmers to build higher-level functionality (for example, the \VAR{fill} methods themselves are defined in terms of calls to \VAR{init}, and the \VAR{array} factory is defined in terms of \EXP{{array}_{1}}, \EXP{{array}_{2}}, and so forth).
+
+Because the elements of a fortress array may reside in multiple
+regions of the machine, there is an additional method
+\EXP{a.\VAR{region}(i)} which returns the region in which the array
+element \EXP{a_i} resides.  An element of an array is always local to
+the region in which the array as a whole is contained, so
+\EXP{(a.\VAR{region}(i)).\VAR{isLocalTo}(\VAR{region}(a))} must always
+return \VAR{true}.  When an array contains reference objects, the
+programmer must be careful to distinguish the region in which the
+array element \EXP{a_i} resides, \EXP{a.\VAR{region}(i)}, from the
+region in which the object referred to by the array element resides,
+\EXP{\VAR{region}(a_i)}.  The former describes the region of the array
+itself; the latter describes the region of the data referred to by the
+array.  These may differ.

trunk/Specification/advanced/parallelism-locality/defining-generators.tex

@@ -18 +18 @@
 \section{Use and Definition of Generators}
 \seclabel{defining-generators}
+
+Several expressions in Fortress make use of \emph{generator clause
+  lists} to express parallel iteration (see \secref{generators}).  A
+generator clause list binds a series of variables to the values produced by a
+series of objects that extend the trait \TYP{Generator}.  A generator clause
+list is simply syntactic sugar for a nested series of invocations of
+methods on these objects.
+
+A type that extends \EXP{\TYP{Generator}\llbracket{}E\rrbracket} acts
+as a generator of elements of type \VAR{E}.  An instance of
+\EXP{\TYP{Generator}\llbracket{}E\rrbracket} only needs to define the
+\VAR{generate} method:
+%    generate[\R\](r:Reduction[\R\], body: E->R): R
+\begin{Fortress}
+{\tt~~~~}\pushtabs\=\+\(    \VAR{generate}\llbracket{}R\rrbracket(r\COLONOP\TYP{Reduction}\llbracket{}R\rrbracket, \VAR{body}\COLON E\rightarrow{}R)\COLON R\)\-\\\poptabs
+\end{Fortress}
+The mechanics of object generation are embedded entirely in the
+\VAR{generate} method.  This method takes two arguments.  The \VAR{generate} method invokes \VAR{body} once for each
+object which is to be generated, passing the generated object as an
+argument.  Each call to \VAR{body} returns a result of type \VAR{R}; these results are combined using the reduction \VAR{r}, which encapsulates a monoidal operator on objects of type \VAR{R}.    \emph{All the parallelism provided by a
+  particular generator is specified by definition of the \VAR{generate} method.}
+
+In practice, calls to \VAR{generate} are produced by desugaring
+expressions with generator clause lists, as described below
+(\secref{desugaring-generators}).  However it is possible to call the
+\VAR{generate} method directly, as in the following example:
+\input{\home/advanced/examples/Generators.ReductionClass.tex}
+
+Any reduction must define two methods: an associative binary operation
+\VAR{join}, and \VAR{empty}, a method that returns the identity of
+this operation.  Here we define reduction \TYP{SumZZ32} representing integer
+addition.  We use this to compute the sum of \EXP{3 x + 2} for \VAR{x}
+drawn from the range \EXP{1\mathinner{\hbox{\tt\char'43}}100},
+yielding the expected answer of 15350.
+
+\begin{figure}
+\input{\home/advanced/examples/Generators.GeneratorDefn.tex}
+\caption{\figlabel{generatorDefn}Sample \TYP{Generator} definition: blocked integer ranges.}
+\end{figure}
+
+For non-commutative reductions such as the \TYP{Concat} reduction used for
+list comprehensions in \figref{generatedExpressions}, it is important to
+note that results must be combined in the natural order of the
+generator.  If \VAR{join} is not associative, or \VAR{empty} is not
+the identity of \VAR{join}, passing the reduction to \VAR{generate}
+will produce unpredictable results.  A generator is permitted to group
+reduction operations in any way it likes consistent with its natural
+order, and insert an arbitrary number of \VAR{empty} elements.
+
+\figref{generatorDefn} defines a generator that generates the integers
+between \VAR{lo} and \VAR{hi} in sequential blocks of size at most
+\VAR{b}.  In this example, we divide the range in half if it is larger
+than the block size \VAR{b}; these two halves are computed in parallel
+(recall that the arguments to the method call
+\EXP{\VAR{reduction}.\VAR{join}} are evaluated in parallel).  If the
+range is smaller than \VAR{b}, then it is enumerated serially using a
+\KWD{while} loop, accumulating the result \VAR{r} as it goes.  Observe
+that the parallelism obtained from a generator is \emph{dictated by
+  the code of the \VAR{generate} method}.  While programmers using a
+generator should assume that calls to \VAR{body} may occur in
+parallel, the library programmer is free to choose the amount of
+parallelism that is actually exposed.
+
+This example uses \emph{recursive subdivision} to divide a blocked
+range into approximately equal-sized chunks of work.  Recursive
+subdivision is the recommended technique for exposing large amounts of
+parallelism in a Fortress program because it adjusts easily to varying
+machine sizes and can be dynamically load balanced.
+
+\TYP{Generator} defines the functional method
+\EXP{\VAR{seq}(\KWD{self})} that returns an equivalent generator that
+runs iterations of the body sequentially in natural order.  In most
+cases (such as in this example), it is prudent to override the default
+definition of this method; the default implementation of \VAR{seq}
+effectively collects the generated elements together in parallel and
+traverses the result sequentially.
+
+\note{
+Note that at the moment there is no way to tell the compiler for
+performance reasons that we really mean it when we ask for
+sequentiality, as opposed to saying that we should preserve sequential
+semantics.  Future versions of this specification may use the
+\TYP{Local} distribution for this purpose, or provide additional
+functions on generators which guarantee serial execution (rather than
+simply providing sequential semantics).
+}
+
+The remainder of this section describes in detail the desugaring of
+expressions with generator clause lists into invocations of the
+\VAR{generate} methods of the generators in the
+generator clause list.
+\note{
+It then outlines how method overloading may be used
+to specialize the behavior of particular combinations of generators
+and reductions.}
+
+\subsection{Simple Desugaring of Expressions with Generators}
+\seclabel{desugaring-generators}
+
+\note{NOTE: tweaked by hand by Jan, as above.}
+
+\begin{figure}
+\begin{tabular}{l@{\:\emph{body}\;\;=\;\;}l}
+%BIG OP[ ]
+\(\mathcal{C}[\;\;]\)
+&
+%u(body)
+\(u(\emph{body})\)
+\\
+%BIG OP[ x <- g, gs ]
+\(\mathcal{C}[\,x \leftarrow g, \emph{gs}\,]\)
+&
+%g.generate(r, fn (x) => BIG OP [gs] body)
+\(g.\VAR{generate}(r, \KWD{fn} (x) \Rightarrow \mathcal{C}[\emph{gs}]\:\emph{body})\)
+\\
+%BIG OP[ p, gs ]
+\(\mathcal{C}[\,p, \emph{gs}\,]\)
+&
+%p.generate(r, fn () => BIG OP [gs] body)
+\(p.\VAR{generate}(r, \KWD{fn} () \Rightarrow \mathcal{C} [\emph{gs}]\:\emph{body})\)
+\end{tabular}
+\caption{\figlabel{simpleDesugar}Simple syntax-directed desugaring of
+  a generator clause list.  Here the reduction $r$ and unit $u$ are
+  variables chosen by the desugarer to be distinct from the variables
+  in \emph{gs} and \emph{body}. }
+\end{figure}
+
+\begin{figure}
+%%\begin{tabular}{ll|ll>{$\;\;\llbracket$}c<{$\rrbracket$}}
+\begin{tabular}{ll|llc}
+expr & type & \VAR{wrapper} & \EXP{u(\VAR{body})} & $r$ \\
+\hline
+
+% SUM [ gs ] e
+\EXP{\sum\limits_{\VAR{gs}} e}
+&
+$N$
+&
+\EXP{\OPR{SUM}\llbracket{}N\rrbracket}
+&
+\EXP{\VAR{identity}\llbracket{}N\rrbracket(e)}
+&
+\EXP{\TYP{SumReduction}\llbracket{}N\rrbracket}
+\\
+
+% <| e | gs |>
+\( \langle\,e \mid \VAR{gs}\,\rangle\)
+&
+% List[\E\]
+\( \TYP{List}\llbracket{}E\rrbracket\)
+&
+\EXP{\OPR{BIG} \langle\llbracket{}E\rrbracket\,\rangle}
+&
+\( \VAR{singleton\llbracket{}E\rrbracket}(e)\)
+&
+\EXP{\TYP{Concat}\llbracket{}E\rrbracket}
+\\
+
+% lv := e, gs
+\( \VAR{lv} \ASSIGN e, \VAR{gs}\)
+&
+\EXP{()}
+&
+built in
+&
+$\VAR{ignore}(\VAR{lv} \ASSIGN e)$
+&
+\TYP{NoReduction}
+
+\end{tabular}
+\caption{Examples of wrappers for expressions with generator clause
+  lists.  Top to bottom: big operators (here \EXP{\sum} is used as an
+  example; the appropriate library function is called on the
+  right-hand side), comprehensions (here list comprehensions are
+  shown; other comprehensions are similar to list comprehensions) and
+  generated assignment.}
+\figlabel{generatedExpressions}
+\end{figure}
+
+An expression with a generator clause list \emph{gs} and body expression \emph{body} is desugared into the following general form:
+\note{
+NOTE: tweaked by hand by Jan.  Replaced BIG OP by $\mathcal{C}$,
+emph'd gs and body.}
+%wrapper(fn (r, u) => BIG OP[gs] body)
+\begin{Fortress}
+\( \VAR{wrapper}(\KWD{fn} (r, u) \Rightarrow \mathcal{C}[\emph{gs}]\:\emph{body})\)
+\end{Fortress}
+The generator clause list and body can be desugared using the
+syntax-directed desugaring $\mathcal{C}$ defined in
+\figref{simpleDesugar}.  This yields a function that is in turn passed
+as an argument to \VAR{wrapper}.  The particular choice of the
+function \VAR{wrapper} depends upon the construct that is being
+desugared.  For a reduction or a comprehension, the wrapper function
+is the corresponding big operator definition; see
+\secref{reduction-expr} and \secref{comprehensions}.  For a \KWD{for}
+loop (\secref{for-expr}) or a generated expression
+(\secref{generated}), a special built-in wrapper is used.
+Examples are shown in \figref{generatedExpressions}.
+A wrapper function always has the following type:
+%% wrapper( g:(Reduction[\R0\],T->R0)->R0): R
+\begin{Fortress}
+\(\VAR{wrapper}( g\COLONOP(\TYP{Reduction}\llbracket{}R_{0}\rrbracket,T\rightarrow{}R_{0})\rightarrow{}R_{0})\COLON R\)
+\end{Fortress}
+Here the type $T$ is the type of values returned by the body expression,
+and \EXP{R_{0}} and \VAR{R} are arbitrary types chosen by the wrapper function.
+
+Note that the function $g$ passed to the wrapper has essentially the
+same type signature as the \VAR{generate} method itself.  It is
+instructive to think of \VAR{wrapper} as having the following similar
+type signature:\footnote{In future, it is likely that Fortress will use
+  a desugaring that in fact yields a \TYP{Generator} rather than a
+  higher-order function.  This permits type-directed nesting and
+  composition of generators.}
+%% wrapper'( g: Generator[\T\] ): R  (* NOT THE ACTUAL TYPE *)
+\begin{Fortress}
+\(\VAR{wrapper}'( g\COLON \TYP{Generator}\llbracket{}T\rrbracket )\COLON R  \mathtt{(*}\;\hbox{\rm  NOT THE ACTUAL TYPE \unskip}\;\mathtt{*)}\)
+\end{Fortress}
+
+\note{From here till the end of this chapter, copied from F1.0$\beta$.}
+
+An array comprehension simply desugars into a factory function call
+and a series of assignments:
+\begin{center}
+\begin{tabular}[c]{@{}l@{}}
+% [ i1 = e1 | gs1
+%   i2 = e2 | gs2
+%   ...
+%   i_n = e_n | gs_n ]
+\EXP{[\,\,\,i_{1} = e_{1} \mid {gs}_{1}}\\
+~~~\EXP{i_{2} = e_{2} \mid {gs}_{2}} \\
+~~~$\ldots$ \\
+~~~\EXP{i_n = e_n \mid \VAR{gs}_n\,]}
+\end{tabular}
+\hspace{6em}
+$\longrightarrow$
+\hspace{6em}
+\begin{tabular}[c]{@{}l@{}}
+\( \KWD{do}\;a = \VAR{array}()\)\\
+~~~~~~\(    a[i_{1}] \ASSIGN e_{1}, {gs}_{1}\)\\
+~~~~~~\(    a[i_{2}] \ASSIGN e_{2}, {gs}_{2}\)\\
+~~~~~~\(    \ldots\)\\
+~~~~~~\(    a[i_n] \ASSIGN e_n, \VAR{gs}_n\)\\
+~~~~~~\(    a\) \\
+\( \KWD{end}\)
+\end{tabular}
+\end{center}
+
+The desugaring of a \KWD{for} loop depends upon the set of reduction
+variables.
+We conceptually desugar the \KWD{for} loop with reduction variables,
+$r_1$, $r_2$, $\ldots$, $r_n$, reduced using the reduction operator
+\EXP{\oplus} for type \EXP{(T_{1}, T_{2}, \ldots T_n)}
+%% with the identity \EXP{(z_{1}, z_{2}, \ldots z_n)}
+as follows:
+\begin{center}
+\EXP{\KWD{for} \VAR{gs} \KWD{do} \VAR{block} \KWD{end}}
+\\
+$\longrightarrow$
+\\[2em]
+\begin{tabular}[c]{l@{}l@{}l@{}l}
+\EXP{(r_{1}, r_{2}, \ldots r_n)\; \mathord{\oplus}\!\!= }&
+\EXP{\mathcal{T}
+\llbracket(T_{1}, T_{2}, \ldots T_n), \oplus
+\rrbracket[\VAR{gs}]} &\EXP{(\KWD{do}}&\\
+&&&\EXP{(r_{1}, r_{2}, \ldots r_{\mathrm{n}}) \mathrel{\mathtt{:}} (T_{1}, T_{2}, \ldots T_{\mathrm{n}}) \ASSIGN \TYP{Identity}\llbracket\oplus\rrbracket} \\
+&&&\EXP{\VAR{block}} \\
+&&&\EXP{(r_{1}, r_{2}, \ldots r_n)}\\
+&&\EXP{\;\KWD{end})}\\
+\end{tabular}
+\end{center}
+In practice, a tuple type is not a monoid.  If there is only one
+reduction variable, this is not a problem.  If there are no reduction
+variables, we simply use the type \TYP{NoReduction} used in desugaring
+assignments.  When there are multiple reduction variables, we use
+nested applications of types extending the trait \TYP{ReductionPair}.
+These types encode the common properties of the variables being
+reduced.  Recall that every reduction variable must at least have type
+\TYP{Monoid}, so it is not difficult to guarantee that
+\TYP{ReductionPair} itself also extends \TYP{Monoid}.
+
+\subsection{Accounting for Dependencies among Generators}
+\seclabel{generators-dependencies}
+
+The naive desugaring for generator lists in
+\figref{simpleDesugar} assumes there are always data
+dependencies among generators.  The actual desugaring makes use of the
+\VAR{join} method in the \TYP{Generator} trait to group together
+generators that have no data dependencies.  The goal is to permit
+library code to define more efficient merged generators for generator
+pairs.  For example, it is possible for the \VAR{join} method to take
+the generator list \EXP{i \leftarrow
+  1\mathinner{\hbox{\tt\char'43}}100, j \leftarrow
+  2\mathinner{\hbox{\tt\char'43}}200} and generate a blocked
+two-dimensional traversal.  This could then be joined with \EXP{k
+  \leftarrow 3\mathinner{\hbox{\tt\char'43}}300} to obtain a
+three-dimensional blocked traversal.
+
+However, most generators will simply make use of the default
+definition of \VAR{join} which calls \TYP{SimplePairGenerator}:
+% object SimplePairGenerator[\ A extends Any, B extends Any \]
+%         (outer : Generator[\ A \], inner : Generator[\ B \]) extends Generator[\ (A, B) \]
+%   size : ZZ64 = outer.size DOT inner.size
+%   generate[\ R extends Monoid[\ R, OPLUS \], opr OPLUS \](body : (A, B) -> R):R =
+%     outer.generate(fn (a : A) => inner.generate(fn (b : B) => body (a,b)))
+%   join[\ N extends Any \](other : Generator[\ N \]) : Generator[\ ((A,B), N) \] =
+%     SimpleMapGenerator(outer.join(inner.join(other)),
+%                        (fn (a,(b,n)) => ((a,b),n)))
+% end
+\begin{Fortress}
+{\tt~}\pushtabs\=\+\( \KWD{object}\mskip 4mu plus 4mu\TYP{SimplePairGenerator}\llbracket\,A \KWD{extends}\mskip 4mu plus 4mu\TYP{Any}, B \KWD{extends}\mskip 4mu plus 4mu\TYP{Any}\,\rrbracket\)\\
+{\tt~~~~~~~~}\pushtabs\=\+\(         (\VAR{outer} \mathrel{\mathtt{:}}\mskip 4mu plus 4mu\TYP{Generator}\llbracket\,A\,\rrbracket, \VAR{inner} \mathrel{\mathtt{:}}\mskip 4mu plus 4mu\TYP{Generator}\llbracket\,B\,\rrbracket) \KWD{extends}\mskip 4mu plus 4mu\TYP{Generator}\llbracket\,(A, B)\,\rrbracket\)\-\\\poptabs
+{\tt~~}\pushtabs\=\+\(   \VAR{size} \mathrel{\mathtt{:}}\mskip 4mu plus 4mu\mathbb{Z}64 = \VAR{outer}.\VAR{size} \cdot \VAR{inner}.\VAR{size}\)\\
+\(   \VAR{generate}\llbracket\,R \KWD{extends}\mskip 4mu plus 4mu\TYP{Monoid}\llbracket\,R, \oplus\,\rrbracket, \KWD{opr} \mathord{\oplus}\,\rrbracket(\VAR{body} \mathrel{\mathtt{:}} (A, B) \rightarrow R)\COLONOP{}R =\)\\
+{\tt~~}\pushtabs\=\+\(     \VAR{outer}.\VAR{generate}(\KWD{fn} (a \mathrel{\mathtt{:}}\mskip 4mu plus 4mu{A}) \Rightarrow \VAR{inner}.\VAR{generate}(\KWD{fn} (b \mathrel{\mathtt{:}}\mskip 4mu plus 4mu{B}) \Rightarrow \VAR{body} (a,b)))\)\-\\\poptabs
+\(   \VAR{join}\llbracket\,N \KWD{extends}\mskip 4mu plus 4mu\TYP{Any}\,\rrbracket(\VAR{other} \mathrel{\mathtt{:}}\mskip 4mu plus 4mu\TYP{Generator}\llbracket\,N\,\rrbracket) \mathrel{\mathtt{:}}\mskip 4mu plus 4mu\TYP{Generator}\llbracket\,((A,B), N)\,\rrbracket =\)\\
+{\tt~~}\pushtabs\=\+\(     \TYP{SimpleMapGenerator}( \null\)\pushtabs\=\+\(\VAR{outer}.\VAR{join}(\VAR{inner}.\VAR{join}(\VAR{other})),\)\\
+\(                        (\KWD{fn} (a,(b,n)) \Rightarrow ((a,b),n)))\)\-\-\-\\\poptabs\poptabs\poptabs
+\( \KWD{end}\)\-\\\poptabs
+\end{Fortress}
+Note how \TYP{SimplePairGenerator} itself overrides the \VAR{join}
+method.  When we attempt to join an existing pair of joined
+generators, we first attempt to \VAR{join} the \VAR{inner} generator
+of the pair with the \VAR{other} generator (the new innermost
+generator) passed in.  This means that every generator will have the
+opportunity to combine with both its left and right neighbors if
+neither has a dependency which prevents it.  Note that we use a
+\TYP{SimpleMapGenerator}, which simply applies a function to the
+result of another generator, to re-nest the tuples produced by the
+nested \VAR{join} operation.
+
+Which pairs of adjacent traversals are combined using \VAR{join}?
+This question is complicated by examples such as
+% i<-1:100, j<-1:100, k<-i:100, l<-j:100.
+\EXP{i\leftarrow{}1\COLONOP{}100, j\leftarrow{}1\COLONOP{}100,
+  k\leftarrow{}i\COLONOP{}100, l\leftarrow{}j\COLONOP{}100}.  We can
+either combine \VAR{i} and \VAR{j} traversals, or we can combine
+\VAR{j} and \VAR{k} traversals.  In the former case we can also
+combine \VAR{k} and \VAR{l} traversals.  The Fortress compiler is free
+to choose any grouping subject to the following constraints:
+\begin{itemize}
+\item Two generators may not be combined using \VAR{join} if the second is data dependent upon the first.
+\item Generator order must be preserved when invoking \VAR{join}.
+\item When a chain of three or more generators is joined, the
+  traversals must be combined left-associatively.
+\end{itemize}
+We can obtain a simple greedy desugaring which joins together
+traversals in accordance with the above rules by simply adding the
+following desugaring rule which takes precedence over those given in
+\figref{simpleDesugar} when each variable bound in $v_1$ does not occur free in $g_2$.
+\begin{center}
+%T[\R,BOXPLUS\][ v1 <- g1, v2 <- g2, gs ] body
+\EXP{\mathcal{T}\llbracket{}R,\boxplus\rrbracket[\,v_{1} \leftarrow g_{1}, v_{2} \leftarrow g_{2}, \VAR{gs}\,]\;\VAR{body}
+\;\;=\;\;
+%T[\R,BOXPLUS\][ (v1,v2) <- g1.join(g2), gs ] body
+\mathcal{T}\llbracket{}R,\boxplus\rrbracket[\,(v_{1},v_{2}) \leftarrow g_{1}.\VAR{join}(g_{2}), \VAR{gs}\,]\;\VAR{body}}
+%%\\
+%%\hfill when $\VAR{BV}[v_{1}]$ does not intersect $\VAR{FV}[g_2]$
+\end{center}
+%where the set of bound variables in $v_1$ does not intersect with the set of
+%free variables in $g_2$.
+
+
+\subsection{Using Overloading to Adapt Generators and Traversals}
+
+Overloaded instances of the \VAR{generate} method can be used to adapt
+a generator to the particular properties of the reduction being
+performed.  For example, a commutative monoid need only maintain a
+single variable \VAR{result} containing the reduced value so far:
+% value object BlockedRange(lo: ZZ64, hi: ZZ64, b: ZZ64) extends Generator[\ZZ64\]
+%   ...
+%   generate[\R extends CommutativeMonoid[\ R, OPLUS\], opr OPLUS\](body : ZZ64 -> R) : R = do
+%     result : R = Identity[\OPLUS\]
+%     traverse(l,u) =
+%       if u-l+1 <= max(b,1) then
+%         i : ZZ64 = l
+%         while i <= u do
+%           t = body(i)
+%           atomic result := result OPLUS t
+%           i += 1
+%         end
+%         ()
+%       else
+%         mid = LC l/2 RC + LF u/2 RF
+%         (traverse(l,mid), traverse(mid+1,u))
+%         ()
+%       end
+%     traverse(lo, hi)
+%     result
+%   end
+% end
+\begin{Fortress}
+{\tt~}\pushtabs\=\+\( \KWD{value}\;\;\KWD{object} \TYP{BlockedRange}(\VAR{lo}\COLON \mathbb{Z}64, \VAR{hi}\COLON \mathbb{Z}64, b\COLON \mathbb{Z}64) \KWD{extends} \TYP{Generator}\llbracket\mathbb{Z}64\rrbracket\)\\
+{\tt~~}\pushtabs\=\+\(   \ldots\)\\
+\(   \VAR{generate}\llbracket{}R \KWD{extends} \TYP{CommutativeMonoid}\llbracket\,R, \oplus\rrbracket, \KWD{opr} \mathord{\oplus}\rrbracket(\VAR{body} \mathrel{\mathtt{:}} \mathbb{Z}64 \rightarrow R) \mathrel{\mathtt{:}} R = \;\KWD{do}\)\\
+{\tt~~}\pushtabs\=\+\(     \VAR{result} \mathrel{\mathtt{:}} R = \TYP{Identity}\llbracket\mathord{\oplus}\rrbracket\)\\
+\(     \VAR{traverse}(l,u) =\)\\
+{\tt~~}\pushtabs\=\+\(       \KWD{if} u-l+1 \leq \max(b,1) \KWD{then}\)\\
+{\tt~~}\pushtabs\=\+\(         i \mathrel{\mathtt{:}} \mathbb{Z}64 = l\)\\
+\(         \KWD{while} i \leq u \KWD{do}\)\\
+{\tt~~}\pushtabs\=\+\(           t = \VAR{body}(i)\)\\
+\(           \KWD{atomic} \VAR{result} \ASSIGN \VAR{result} \oplus t\)\\
+\(           i \mathrel{+}= 1\)\-\\\poptabs
+\(         \KWD{end}\)\\
+\(         ()\)\-\\\poptabs
+\(       \KWD{else}\)\\
+{\tt~~}\pushtabs\=\+\(         \VAR{mid} = \lceil l/2 \rceil + \lfloor u/2 \rfloor\)\\
+\(         (\VAR{traverse}(l,\VAR{mid}), \VAR{traverse}(\VAR{mid}+1,u))\)\\
+\(         ()\)\-\\\poptabs
+\(       \KWD{end}\)\-\\\poptabs
+\(     \VAR{traverse}(\VAR{lo}, \VAR{hi})\)\\
+\(     \VAR{result}\)\-\\\poptabs
+\(   \KWD{end}\)\-\\\poptabs
+\( \KWD{end}\)\-\\\poptabs
+\end{Fortress}
+
+The choice of whether to apply this transformation is left up to the
+author of the generator; when many iterations run in parallel the
+\VAR{result} variable becomes a scalability bottleneck and this
+technique should not be used.
+
+Various other properties of the reduction operator can be exploited:
+\begin{itemize}
+\item Idempotent reductions permit redundant computation.  For
+  example, when computing the maximum element of a set it might be
+  simpler to enumerate set elements more than once.
+
+\item On the other hand, sometimes a more efficient non-idempotent
+  operator can be used for a reduction if the generator promises never
+  to produce duplicates---this fact can be used to advantage in set,
+  multiset, or map comprehensions.
+
+\item If the reduction operator has a zero, this can be used to exit
+  early from a partial computation.  This requires that the body
+  expression have no visible side effects such as writes or \KWD{io} actions.
+\end{itemize}
+
+At the moment, the author of a \TYP{Generator} is responsible for
+taking advantage of opportunities such as these.  In future, we expect
+some standardized support for efficient versions of various traversals
+based on experience with the definitions provided here.
+
+\subsection{Making a Serial Version of a Generator or Distribution}
+\seclabel{serial-generator}
+
+\note{
+TODO: the mechanism for generator serialization is once again magic.
+Formerly we constrained generator structure so the serialization was
+straightforward (but this probably made things slow).}
+
+A generator \VAR{g} can be made sequential simply by calling the builtin function \VAR{sequential} as follows:
+%v <- sequential(g)
+\begin{Fortress}
+\(v \leftarrow \VAR{sequential}(g)\)
+\end{Fortress}
+The resulting generator yields its elements in the natural order
+specified by the original generator.  Several builtin generators (such
+as those for array indices) have an associated distribution.  For
+these generators, \VAR{sequential} function simply re-distributes the
+underlying object as follows:
+%sequential(r) = Sequential.distribute(r)
+\begin{Fortress}
+\(\VAR{sequential}(r) = \TYP{Sequential}.\VAR{distribute}(r)\)
+\end{Fortress}
+As a convenient shorthand, the \VAR{sequential} function is also
+defined to work for distributions themselves.  The complete declarations of
+the overloaded \VAR{sequential} function are as follows:
+%sequential[\ E extends Any \](g : Generator[\E\]) : Generator[\E\]
+%sequential[\ E extends Any \](d : Distribution) : Distribution
+\begin{Fortress}
+\(\VAR{sequential}\llbracket\,E \KWD{extends}\mskip 4mu plus 4mu\TYP{Any}\,\rrbracket(g \mathrel{\mathtt{:}}\mskip 4mu plus 4mu\TYP{Generator}\llbracket{}E\rrbracket) \mathrel{\mathtt{:}}\mskip 4mu plus 4mu\TYP{Generator}\llbracket{}E\rrbracket\)\\
+\(\VAR{sequential}\llbracket\,E \KWD{extends}\mskip 4mu plus 4mu\TYP{Any}\,\rrbracket(d \mathrel{\mathtt{:}}\mskip 4mu plus 4mu\TYP{Distribution}) \mathrel{\mathtt{:}}\mskip 4mu plus 4mu\TYP{Distribution}\)
+\end{Fortress}
+The \VAR{sequential} function has special meaning to the Fortress
+implementation; there is no need to distinguish reduction variables in
+loops for which generator is surrounded by a direct call to
+\VAR{sequential}.

trunk/Specification/advanced/parallelism-locality/distributions.tex

@@ -18 +18 @@
 \section{Distributions}
 \seclabel{distributions}
+
+\note{Distributions are not yet supported.
+Examples in this section are not tested.}
+
+Most of the heavy lifting in mapping threads and arrays to regions is performed
+by \emph{distributions}.  An instance of the trait
+\TYP{Distribution} describes the parallel structure of ranges and
+other numeric generators (such as the generators for the index space
+of an array), and provides for the allocation and distribution of
+arrays on the machine:
+%trait Distribution
+%  distribute[\E, B extends ArrayIndex\](Range[\B\]):Range[\B\]
+%  distribute[\E, B extends ArrayIndex\](a:Array[\E,B\]):Array[\E,B\] =
+%    distributeFromTo[\E,B\](a,a.distribution,self)
+%end
+\begin{Fortress}
+\(\KWD{trait}\mskip 4mu plus 4mu\TYP{Distribution}\)\\
+{\tt~~}\pushtabs\=\+\(  \VAR{distribute}\llbracket{}E, B \KWD{extends}\mskip 4mu plus 4mu\TYP{ArrayIndex}\rrbracket(\TYP{Range}\llbracket{}B\rrbracket)\COLONOP\TYP{Range}\llbracket{}B\rrbracket\)\\
+\(  \VAR{distribute}\llbracket{}E, B \KWD{extends}\mskip 4mu plus 4mu\TYP{ArrayIndex}\rrbracket(a\COLONOP\TYP{Array}\llbracket{}E,B\rrbracket)\COLONOP\TYP{Array}\llbracket{}E,B\rrbracket =\)\\
+{\tt~~}\pushtabs\=\+\(    \VAR{distributeFromTo}\llbracket{}E,B\rrbracket(a,a.\VAR{distribution},\KWD{self})\)\-\-\\\poptabs\poptabs
+\(\KWD{end}\)
+\end{Fortress}
+
+Abstractly, a \TYP{Distribution} acts as a transducer for generators
+and arrays.  The \VAR{distribute} method applied to a multidimensional
+\TYP{Range} organizes its indices into the leaves of a tree whose
+inner nodes correspond to potential levels of parallelism and locality
+in the underlying computation, producing a fresh \TYP{Range} whose
+behavior as a \TYP{Generator} may differ from that of the passed-in
+\TYP{Range}.  The \VAR{distribute} method applied to an array creates
+a copy of that array distributed according to the given distribution.
+This is specified in terms of a call to the overloaded function
+\VAR{distributeFromTo}.  This permits the definition of specialized
+versions of this function for particular pairs of distributions.
+
+The intention of distributions is to separate the task of data
+distribution and program correctness.  That is, it should be possible
+to write and debug a perfectly acceptable parallel program using only
+the default data distribution provided by the system.  Imposing a
+distribution on particular computations, or designing and implementing
+distributions from scratch, is a task best left for performance
+tuning, and one which should not affect the correctness of a working
+program.
+
+There is a \TYP{DefaultDistribution} which is defined by the
+underlying system.  This distribution is designed to be reasonably
+adaptable to different system scales and architectures, at the cost of
+some runtime efficiency.  Arrays and generators that are not
+explicitly allocated through a distribution are given the
+\TYP{DefaultDistribution}.
+
+There is a generator, \VAR{indices},
+associated with every array.  This generator is distributed in the
+same way as the array itself.  When we re-distribute an array, we also
+re-distribute the generator; thus
+\EXP{d.\VAR{distribute}(a.\VAR{indices})} is equivalent to
+\EXP{(d.\VAR{distribute}(a)).\VAR{indices}}.
+
+There are a number of built-in distributions:
+\begin{tabbing}
+\begin{tabular}{ll}
+\TYP{DefaultDistribution}        &       Name for distribution chosen by system. \\
+\TYP{Sequential}
+&       Sequential distribution.
+       Arrays are allocated in one contiguous piece of memory. \\
+\TYP{Local}          &       Equivalent to \TYP{Sequential}. \\
+\TYP{Par}            &       Blocked into chunks of size 1. \\
+\TYP{Blocked}        &       Blocked into roughly equal chunks. \\
+\EXP{\TYP{Blocked}(n)}   &   Blocked into \VAR{n} roughly equal chunks. \\
+\TYP{Subdivided}     &       Chopped into $2^k$-sized chunks, recursively. \\
+\EXP{\TYP{Interleaved}(d_{1}, d_{2},\ldots d_{n})}
+&       The first \VAR{n} dimensions are distributed according to \EXP{d_{1} \ldots d_{n}}, \\
+&       with subdivision alternating among
+dimensions. \\
+\EXP{\TYP{Joined}(d_{1}, d_{2},\ldots d_{n})}
+&       The first \VAR{n} dimensions are distributed according to \EXP{d_{1} \ldots d_{n}}, \\
+&       subdividing completely in each
+dimension before proceeding to the next.
+\end{tabular}
+\end{tabbing}
+From these, a number of composed distributions are provided:
+\begin{tabbing}
+\begin{tabular}{ll}
+\EXP{\TYP{Morton}}
+&       Bit-interleaved Morton order~\cite{morton}, recursive subdivision
+       in all dimensions.\\
+\EXP{\TYP{Blocked}(x_{1}, x_{2}, \ldots x_{n})}
+&       Blocked in \VAR{n} dimensions into chunks of size \EXP{x_{i}} in dimension \VAR{i}; \\
+&       remaining dimensions (if any) are local.
+\end{tabular}
+\end{tabbing}
+
+To allocate an array which is local to a single thread (and most
+likely allocated in contiguous storage), the \TYP{Local}
+distribution can be used:
+%a = Local.distribute [ 1 0 0 ; 0 1 0 ; 0 0 1 ]
+\begin{Fortress}
+\(a = \TYP{Local}.\VAR{distribute} [\,1\;0\;0 ; 0\;1\;0 ; 0\;0\;1\,]\)
+\end{Fortress}
+Other distributions can be requested in a similar way.
+
+
+Distributions can be constructed and given names:
+%spatialDist = Blocked(n,n,1)     (* Pencils along the $z$ axis *)
+\begin{Fortress}
+\(\VAR{spatialDist} = \TYP{Blocked}(n,n,1)     \mathtt{(*}\;\hbox{\rm  Pencils along the $z$ axis \unskip}\;\mathtt{*)}\)
+\end{Fortress}
+The system will lay out arrays with the same distribution in the same
+way in memory (as much as this is feasible), and will run loops with
+the same distribution in the same way (as much as this is feasible).
+By contrast, if we replace every occurrence of \VAR{spatialDist} by
+\EXP{\TYP{Blocked}(n,n,1)}, this code will likely divide up arrays and
+ranges into the same-sized pieces as above, but these pieces need not
+be collocated.

trunk/Specification/advanced/parallelism-locality/early-termination.tex

@@ -18 +18 @@
 \section{Early Termination of Threads}
 \seclabel{early-termination}
+
+As noted in \secref{threads-parallelism}, an implicit thread
+can be terminated if its group is going to throw an exception.
+Similarly, a spawned thread \VAR{t} may be terminated by calling
+\EXP{t.\VAR{stop}()}.  A successful attempt to terminate a thread causes the
+thread to complete asynchronously.  There is no guarantee that
+termination attempts will be prompt, or that they will occur at all;
+the implementation will make its best effort.  If a thread completes
+normally or exceptionally before an attempt to terminate it succeeds,
+the result is retained and the termination attempt is simply dropped.
+
+At present stopping a thread immediately causes it to cease execution;
+no outstanding \KWD{finally} blocks are run and the thread is not
+considered to return a result.
+
+\note{From here till the end of this section, copied from F1.0$\beta$.}
+
+A termination attempt acts as if a special hidden \emph{stop
+  exception} is thrown in that thread.  This exception cannot be
+thrown by \KWD{throw} or caught by \KWD{catch}; however, \KWD{finally}
+clauses are run as with any other exception.  If the stopped thread
+was in the middle of an \KWD{atomic} expression, the effects of that
+expression are rolled back just as with an ordinary \KWD{throw}.  A
+special wrapper around every spawned thread is provided by the
+Fortress implementation; it catches the stop exception and transforms
+it into a deferred \TYP{Stopped} exception.  This is visible to the
+programmer and should be caught by invoking the \VAR{val} method on
+the thread object.  Implicit threads are terminated only if another
+thread in the group completes abruptly, and the threads that are
+terminated are ignored for the purposes of the completion of the
+group.
+
+Typical code for stopping a thread looks something like the following
+example:
+%x : ZZ64 := 0
+%t = spawn do
+%      try
+%        atomic if x=0 then abort() else () end
+%      finally
+%        x := 1
+%      end
+%    end
+%t.stop()
+%try
+%  t.val()
+%catch s
+%  Stopped => x += 2; x
+%end
+\begin{Fortress}
+\(x \mathrel{\mathtt{:}} \mathbb{Z}64 \ASSIGN 0\)\\
+\(t = \null\)\pushtabs\=\+\(\KWD{spawn}\;\;\KWD{do}\)\\
+{\tt~~~~~~}\pushtabs\=\+\(      \KWD{try}\)\\
+{\tt~~}\pushtabs\=\+\(        \KWD{atomic}\;\;\KWD{if} x=0 \KWD{then} \VAR{abort}() \KWD{else} () \KWD{end}\)\-\\\poptabs
+\(      \KWD{finally}\)\\
+{\tt~~}\pushtabs\=\+\(        x \ASSIGN 1\)\-\\\poptabs
+\(      \KWD{end}\)\-\\\poptabs
+\(    \KWD{end}\)\-\\\poptabs
+\(t.\VAR{stop}()\)\\
+\(\KWD{try}\)\\
+{\tt~~}\pushtabs\=\+\(  t.\VAR{val}()\)\-\\\poptabs
+\(\KWD{catch} s\)\\
+{\tt~~}\pushtabs\=\+\(  \TYP{Stopped} \Rightarrow x \mathrel{+}= 2; x\)\-\\\poptabs
+\(\KWD{end}\)
+\end{Fortress}
+Here the spawned thread \VAR{t} blocks until it is killed by the call
+to \EXP{\VAR{t}.\VAR{stop}()}; it sets \VAR{x} to 1 in the
+\KWD{finally} clause before exiting.  In this case, the call to
+\EXP{\VAR{t}.\VAR{val}()} will throw \TYP{Stopped}, which is caught,
+causing 2 to be added to \VAR{x} and returning 3.
+
+Note that there is a race in the above code, so the \KWD{try} block in
+\VAR{t} may not have been entered when \EXP{\VAR{t}.\VAR{stop}()} is
+called, causing $x$ to be 2 at the end of execution.  Note also that
+the call to \EXP{\VAR{t}.\VAR{stop}()} occurs asynchronously; in the
+absence of the call to \EXP{\VAR{t}.\VAR{val}()}, the spawning thread
+would not have waited for \VAR{t} to complete.

trunk/Specification/advanced/parallelism-locality/intro.tex

@@ -16 +16 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+\note{Distributions are not yet supported.}
+
 \label{parallel-intro}
+Fortress is designed to make parallel programming as simple and as
+painless as possible.  This chapter describes the internals of
+Fortress parallelism designed for use by authors of library code (such as
+\emph{distributions}, generators, and arrays).  We adopt a multi-tiered
+approach to parallelism:
+\begin{itemize}
+
+\item At the highest level, we provide libraries that allocate
+locality-aware distributed
+shared arrays (\secref{arrays}) and implicitly
+  parallel constructs such as tuples and loops.  Synchronization is
+  accomplished through the use of atomic sections (\secref{atomic}).
+  More complex synchronization makes use of abortable atomicity,
+  described in \secref{transactions}.
+
+\item There is an extensive library of distributions, which
+  permits the programmer to specify locality and data distribution
+  explicitly (\secref{distributions}).
+
+\item
+Immediately below that, the \KWD{at} expression requests that a
+computation take place in a particular region of the machine
+(\secref{parallelism-fundamentals}).
+  We also provide a mechanism to
+  terminate a spawned thread early (\secref{early-termination}).
+
+\item Finally, there are mechanisms for constructing new generators
+  via recursive subdivision into tree structures with individual
+  elements at the leaves.
+  \secref{defining-generators} explains how
+  iterative constructs such as \KWD{for} loops and comprehensions
+  are desugared into calls to methods of trait \TYP{Generator}, and how
+  new instances of this trait may be defined.
+
+\end{itemize}
+
+We begin by describing the abstraction of \emph{regions}, which Fortress
+uses to describe the machine on which a program is run.

trunk/Specification/advanced/parallelism-locality/primitives-distributions.tex

@@ -18 +18 @@
 \section{Placing Threads}
 \seclabel{parallelism-fundamentals}
+
+A thread can be placed in a particular region by using an \KWD{at}
+expression:
+\input{\home/advanced/examples/Parallel.At.a.tex}
+
+In this example, two implicit threads are created; the first computes
+\EXP{a_i} locally, the second computes \EXP{a_j} in the region where
+the $j^{th}$ element of $a$ resides, specified by
+\EXP{a.\VAR{region}(j)}.  The expression after \KWD{at} must return a
+value of type \TYP{Region}, and the block immediately following
+\KWD{do} is run in that region; the result of the block is the result
+of the \KWD{at} expression as a whole.  Often it is more graceful to
+use the \EXP{\KWD{also}\;\KWD{do}} construct
+(described in\secref{also-block})
+in these cases:
+\input{\home/advanced/examples/Parallel.At.b.tex}
+
+We can also use \KWD{at} with a \KWD{spawn} expression:
+\input{\home/advanced/examples/Parallel.At.c.tex}
+
+Finally, note that it is possible to use an \KWD{at} expression within
+a block:
+\input{\home/advanced/examples/Parallel.At.d.tex}
+We can think of this as the degenerate case of \EXP{\KWD{also}\;
+  \KWD{do}}: a thread group is created with a single implicit thread
+running the contents of the \KWD{at} expression in the given region; when
+this thread completes control returns to the original location.
+
+Note that the regions given in an \KWD{at} expression are non-binding:
+the Fortress implementation may choose to run the computations
+elsewhere---for example, thread migration might not be possible within
+an \KWD{atomic} expression, or load balancing might cause code to be
+executed in a different region.  In general, however, implementations
+should attempt to respect thread placement annotations when they are
+given.

trunk/Specification/advanced/parallelism-locality/regions-threads.tex

@@ -18 +18 @@
 \section{Regions}
 \seclabel{regions}
+
+Every thread (either explicit or implicit) and every object in Fortress,
+and every element of a Fortress array (the physical storage for that array
+element), has an associated \emph{region}.
+The Fortress libraries provide a function \VAR{region}
+which returns the region in which a given object resides.
+Regions abstractly describe the structure of
+the machine on which a Fortress program is running.  They are
+organized hierarchically to form a tree, the \emph{region hierarchy},
+reflecting in an abstract way the degree of locality which those
+regions share.  The distinguished region \TYP{Global} represents the root
+of the region hierarchy.\footnote{Note: the initial implementation of the Fortress language assumes a single machine with shared memory and exposes only the \TYP{Global} region.}
+The different levels of this tree reflect underlying
+machine structure, such as execution engines within a CPU, memory
+shared by a group of processors, or resources distributed across the
+entire machine.  The function \EXP{\VAR{here}()} returns the region in which execution is currently occurring.  Objects which reside in regions near the leaves of
+the tree are local entities; those which reside at higher levels of
+the region tree are logically spread out.
+The method call
+\EXP{r.\VAR{isLocalTo}(s)} returns \VAR{true} if \VAR{r} is contained
+within the region tree rooted at \VAR{s}.
+
+It is important to understand that regions and the structures
+(such as distributions, \secref{distributions})
+ built on top of them exist
+purely for performance purposes.  The placement of a thread or an
+object does not have any semantic effect on the meaning of a program;
+it is simply an aid to enable the implementation to make informed
+decisions about data placement.
+
+It might not be possible for an object or a thread to reside in a given
+region.  Threads of execution reside at the \emph{execution level} of
+the region hierarchy, generally the bottommost level in the region
+tree.  Each thread is generally associated with some region at the
+execution level, indicating where it will preferentially be run.
+The programmer can affect the choice of region by using an \KWD{at}
+expression (\secref{parallelism-fundamentals}) when the thread is
+created.  A thread may have an associated region which is not at
+the execution level of the region hierarchy, either because a higher
+region was requested with an \KWD{at} expression or because scheduling
+decisions permit the thread to run in several possible execution
+regions.  The region to which a thread is assigned may also change
+over time due to scheduling decisions.
+For the object associated with a spawned thread,
+the \VAR{region} function provided by the Fortress libraries
+returns the region of the associated thread.
+
+
+The \emph{memory level} of the region hierarchy is where individual
+reference objects reside; on a machine with nodes composed of multiple
+processor cores sharing a single memory, this generally will not be a
+leaf of the region hierarchy.
+Imagine a constructor for a reference
+object is called by a thread residing in region \VAR{r}, yielding an
+object \VAR{o}.  Except in very rare circumstances (for example when a
+local node is out of memory) either
+%r.isLocalTo(region(o))
+\EXP{r.\VAR{isLocalTo}(\VAR{region}(o))} or
+%region(o).isLocalTo(r)
+\EXP{\VAR{region}(o).\VAR{isLocalTo}(r)} ought to hold: data is
+allocated locally to the thread which runs the constructor.  For a value object
+\VAR{v} being manipulated by a thread residing in region \VAR{r} either
+%region(v).isLocalTo(r)
+\EXP{\VAR{region}(v).\VAR{isLocalTo}(r)} or
+%r.isLocalTo(region(v))
+\EXP{r.\VAR{isLocalTo}(\VAR{region}(v))}
+(value objects always appear to be local).
+
+Note that \VAR{region} is a top-level function provided by the Fortress libraries
+and can be overridden by any functional method.
+The chief example of this is arrays, which are
+generally composed from many reference objects; the \VAR{region} function
+can be
+overridden to return the location of the array as a
+whole---the region which contains all of its constituent reference objects.

trunk/Specification/advanced/parallelism-locality/shared-local.tex

@@ -18 +18 @@
 \section{Shared and Local Data}
 \seclabel{threadlocal}
+
+\note{The method \VAR{copy} is not yet supported.}
+
+Every object in a Fortress program is considered to be either
+\emph{shared} or \emph{local} (collectively referred to as the
+\emph{sharedness} of the object).  A local object must be transitively
+reachable (through zero or more object references) from the variables
+of at most one running thread.  A local object may be accessed more
+cheaply than a shared object, particularly in the case of atomic reads
+and writes.  Sharedness is ordinarily managed implicitly by the
+Fortress implementation.
+Control over sharedness is intended to be a
+performance optimization; however, functions such as \VAR{isShared} and
+\VAR{localize} provided by the Fortress libraries
+can affect program semantics, and must be used with care.
+
+The sharedness of an object must be contrasted with its region.  The
+region of an object describes where that object is located on the
+machine.  The sharedness of an object describes whether the object is
+visible to one thread or to many.  A local object need not actually
+reside in a region near the thread to which it is visible (though
+ordinarily it will).
+
+The following rules govern sharedness:
+\begin{itemize}
+\item Reference objects are initially local when they are constructed.
+\item The sharedness of an object may change as the program executes.\footnote{Note, for example, that the present Fortress implementation immediately makes every object shared after construction, so that \VAR{isShared()} will always return \VAR{true}.}
+\item If an object is currently transitively reachable from more than
+  one running thread, it must be shared.
+\item When a reference to a local object is stored into a field of a
+  shared object, the local object must be \emph{published}: Its
+  sharedness is changed to shared, and all of the data to which it
+  refers is also published.
+\item The value of a local variable referenced by a thread must be
+  published before that thread may be run in parallel with the thread
+  which created it.  Values assigned to the variable while the
+  threads run in parallel must also be published.
+\item A field with value type is assigned by copying, and thus has the
+   sharedness of the containing object or closure.
+\end{itemize}
+
+Publishing can be expensive, particularly if the structure being
+broadcast is large and heavily nested; this can cause an apparently
+short \KWD{atomic} expression (a single write, say) to run arbitrarily
+long.  To avoid this, the library programmer can request that an
+object be published by calling the semantically transparent function
+\VAR{shared} provided by the Fortress libraries:
+\input{\home/advanced/examples/Parallel.Shared.a.tex}
+A local copy of an object can be obtained by calling \VAR{copy}, a
+method on trait \TYP{Any}:
+\note{Example is commented out because it is not yet supported nor run by the interpreter.}
+% %localVar := sharedVar.copy()
+% \begin{Fortress}
+% \(\VAR{localVar} \ASSIGN \VAR{sharedVar}.\VAR{copy}()\)
+% \end{Fortress}
+
+Two additional functions are provided which permit different choices of
+program behavior based on the sharedness of objects:
+\begin{itemize}
+\item The function \EXP{\VAR{isShared}(o)} returns \VAR{true} when
+\VAR{o} is shared, and \VAR{false} when it is local.  This permits
+the program to take different actions based on sharedness.
+\item The function \EXP{\VAR{localize}(o)} is provided that attempts to make a local version of object \VAR{o}, by copying if necessary
+equivalent to the following expression:
+\note{Example is commented out because it is not yet supported nor run by the interpreter.}
+%% \input{\home/advanced/examples/Parallel.Shared.b.tex}
+%% %% %if o.isShared then o.copy() else o end
+%% %% \begin{Fortress}
+%% %% \(\KWD{if} o.\VAR{isShared} \KWD{then} o.\VAR{copy}() \KWD{else} o \KWD{end}\)
+%% %% \end{Fortress}
+\end{itemize}
+These functions must be used with extreme caution.  For example,
+\VAR{localize} should be used only when there is a unique
+reference to the object being localized.  The \VAR{localize} function
+can have unexpected behavior if there is a reference to \VAR{o} from
+another local object \VAR{p}.  Updates to \VAR{o} will be visible
+through \VAR{p}; subsequent publication of \VAR{p} will publish
+\VAR{o}.  By contrast, if \VAR{o} was already shared, and referred to
+by another shared object, the newly-localized copy will be entirely
+distinct; changes to the copy will not be visible through \VAR{p}, and
+publishing \VAR{p} will not affect the locality of the copy.

trunk/Specification/advanced/parallelism-locality/transactions.tex

@@ -18 +18 @@
 \section{Abortable Atomicity}
 \seclabel{transactions}
+
+Fortress provides a user-level \EXP{\VAR{abort}()} function which
+abandons execution of the innermost \KWD{atomic} expression and rolls back its
+changes, requiring the \KWD{atomic} expression to execute again from
+the beginning.  This permits an atomic section to perform consistency
+checks as it runs.
+Invoking the \VAR{abort} function not within an \KWD{atomic} expression has
+no effect.
+The functionality provided by
+\EXP{\VAR{abort}()} can be abused; it is possible to induce deadlock
+or livelock by creating an atomic section that always fails.  Here is
+a simple example of a program using \EXP{\VAR{abort}()} which is
+incorrect because Fortress does not guarantee that the two implicit
+threads (created by evaluating the two elements of the tuple) will
+always run in parallel; it is possible for the first element of the
+tuple to continually abort without ever running the second element of
+the tuple:
+\note{The example is commented out because it is not yet supported nor run by the interpreter.}
+%% \input{\home/advanced/examples/Parallel.Abort.a.tex}
+
+Fortress also includes a \KWD{tryatomic} expression, which attempts to
+run its body expression atomically.  If it succeeds, the result is returned;
+if it aborts due to a call to \VAR{abort} or due to conflict
+(as described in \secref{atomic}),
+the checked exception \TYP{TryAtomicFailure} is thrown.  In addition, \KWD{tryatomic} is permitted to throw \TYP{TryAtomicFailure} in the absence of conflict; however, it is not permitted to fail unless some other thread performs an access to shared state while the body is being run.
+Conceptually \KWD{atomic} can be defined in terms of \KWD{tryatomic} as follows:
+\input{\home/advanced/examples/Parallel.Abort.b.tex}
+Unlike the above definition, an implementation may choose to suspend a
+thread running an \KWD{atomic} expression which invokes \VAR{abort},
+re-starting it at a later time when it may be possible to make further
+progress.  The above definition restarts the body of the \KWD{atomic}
+expression immediately without suspending.

trunk/Specification/advanced/subscripting.tex

@@ -18 +18 @@
 \section{Subscripting Operator Method Declarations}
 \seclabel{subscripting-ops}
+
+A subscripting operator method declaration has
+\KWD{opr} where a method declaration would have an identifier.
+The value parameter list, rather than being surrounded by parentheses,
+is surrounded by a pair of brackets.  A subscripting operator method
+declaration may have any number of value parameters, keyword parameters,
+and varargs  parameters in that
+value parameter list.  Static parameters may also be present, between
+\KWD{opr} and the left bracket.  Any paired
+Unicode brackets may be so defined \emph{except} ordinary
+parentheses and white square brackets; in particular, the square
+brackets ordinarily used for indexing may be used.
+
+An expression consisting of a subexpression immediately
+followed (with no intervening whitespace) by zero or more
+comma-separated expressions surrounded by brackets will
+invoke a subscripting operator method declaration.  Methods
+for the expression preceding the bracketed expression list are
+considered.  The compiler considers all subscripting operator method
+declarations that are both accessible and applicable, and the most
+specific method declaration is chosen according to the usual overloading
+rules.  For example, the expression \EXP{\VAR{foo}_p} might invoke the
+following subscripting method declaration because expressions in the square
+brackets are rendered as subscripts:
+\input{\home/advanced/examples/OprDecl.Subscripting.tex}
+
+
+
 \section{Subscripted Assignment Operator Method Declarations}
 \seclabel{subscripted-assignment}
+
+A subscripted assignment operator method declaration has
+\KWD{opr} where a method declaration would have an identifier.  The value
+parameter list, rather than being surrounded by parentheses, is
+surrounded by a pair of brackets; this is then followed by the
+operator \txt{:=} and then a second value parameter list in parentheses,
+which must contain exactly one non-keyword
+value parameter.  A subscripted
+assignment operator method declaration may have any number of value
+parameters within the brackets; these value parameters may include
+keyword parameters and
+varargs parameters.  A result type
+may appear after the second value parameter list, but it must be \TYP{()}.
+Static parameters may also be present, between \KWD{opr}
+and the left bracket.  Any paired Unicode brackets may be so
+defined \emph{except} ordinary parentheses and white square brackets; in
+particular, the square brackets ordinarily used for indexing may
+be used.
+
+An assignment expression consisting of an expression immediately
+followed (with no intervening whitespace) by zero or more
+comma-separated expressions surrounded by brackets, followed by the
+assignment operator \txt{:=}, followed by another expression, will
+invoke a subscripted assignment operator method declaration.  Methods
+for the expression preceding the bracketed expression list are
+considered.  The compiler considers all subscript operator method
+declarations that are both accessible and applicable, and the most
+specific method declaration is chosen according to the usual overloading
+rules.  When a compound assignment operator (described in
+\secref{operator-app-expr}) is used with a subscripting operator and
+a subscripted assignment operator, for example \EXP{a_{3} \mathrel{+}= k},
+both a subscripting operator declaration and a subscripted assignment
+operator declaration are required.
+For example, the assignment \EXP{\VAR{foo}_p \ASSIGN \VAR{myWidget}} might
+invoke the following subscripted assignment method declaration:
+\input{\home/advanced/examples/OprDecl.SubscriptedAssignment.tex}
+
+
+
+
 \section{Conditional Operator Declarations}
 \seclabel{conditional-operators-impl}
+
+A \emph{conditional operator} is a binary operator (other than `\txt{:}' and
+`\txt{::}') that
+is immediately followed by `\txt{:}'; see \secref{conditional-operators}.
+A conditional operator expression \EXP{x@\COLONOP{}y} is syntactic sugar for
+\EXP{x@(\KWD{fn} () \Rightarrow y)}; that is, the right-hand operand
+is converted to a ``thunk''
+(zero-parameter function) that then becomes the right-hand operand of the
+corresponding unconditional operator.  Therefore a conditional
+operator is simply implemented as an overloading of the operator that
+accepts a thunk.
+
+
+It is also permitted for a conditional operator to have a preceding as
+well as a following colon.  A conditional operator expression
+\EXP{x\COLONOP@\COLONOP{}y} is syntactic sugar for \EXP{(\KWD{fn} ()
+  \Rightarrow x)@(\KWD{fn} () \Rightarrow y)};
+that is, each operand is converted to a thunk.  This mechanism  is
+used, for example, to define the results-comparison operator
+\txt{:$\sim$:}, which takes exceptions into account.
+
+
+The conditional $\wedge$ and $\vee$ operators for
+boolean values, for example, are implemented as follows:
+\input{\home/library/examples/ConditionalOps.tex}
+
+
+
 \section{Big Operator Declarations}
 \seclabel{big-operators-impl}
+
+A \emph{big operator} such as $\sum$ or $\prod$ is declared as a usual
+operator declaration.
+See \secref{defining-generators} for an example declaration of a big operator.
+A big operator application is either a \emph{reduction expression}
+described in \secref{reduction-expr} or a \emph{comprehension}
+described in \secref{comprehensions}.

trunk/Specification/basic/overloading.tex

@@ -18 +18 @@
 \chapter{Overloading and Multiple Dispatch}
 \chaplabel{multiple-dispatch}
+
+\section{Terminology and Notation}
+\seclabel{overloading-terms}
+\section{Applicability to Named Functional Calls}
+\seclabel{functional-applicability}
+\section{Applicability to Dotted Method Calls}
+\seclabel{dotted-method-applicability}
+\section{Applicability for Functionals with Varargs
+%and Keyword
+Parameters}
+\seclabel{applicability-with-special-params}
+\section{Overloading Resolution}
+\seclabel{resolving-overloading}

trunk/Specification/fortress/fortress.bib

@@ -48 +48 @@
 }
 
+@InProceedings{fool09,
+  title = "Growing a Syntax",
+  author = "Eric Allen and Ryan Culpepper and Janus Dam Nielsen and Jon Rafkind and Sukyoung Ryu",
+  booktitle = "Foundations of Object-Oriented Languages",
+  year = 2009
+}
+
 @misc{FortressInterpreter,
   author = "Sun's Programming Language Research Group",
@@ -91 +98 @@
 }
 
+@techreport{morton,
+  author = "G. M. Morton",
+  title = "A computer oriented geodetic data base and a new technique in file sequencing",
+  institution = "IBM Ltd.",
+  month = mar,
+  year = 1966
+}
+
 @techreport{nistSP811,
   author = "Barry N. Taylor",