*** empty log message ***

1 files changed, 46 insertions, 19 deletions

diff --git a/doc/reference/ScalaReference.tex b/doc/reference/ScalaReference.tex
index 5c106a3e58..586daf401c 100644
--- a/doc/reference/ScalaReference.tex
+++ b/doc/reference/ScalaReference.tex
@@ -304,7 +304,7 @@ referenced entity in $T$.
   Type          ::=  Type1 `=>' Type
                   |  `(' [Types] `)' `=>' Type
                   |  Type1
-  Type1         ::=  SimpleType {with SimpleType} 
+  Type1         ::=  SimpleType {with SimpleType} [Refinement]
   SimpleType    ::=  StableId
                   |  SimpleType `#' id
                   |  Path `.' type
@@ -318,12 +318,14 @@ take type parameters and yield types. A subset of first-order types
 called {\em value types} represents sets of (first-class) values.
 Value types are either {\em concrete} or {\em abstract}. Every
 concrete value type can be represented as a {\em class type}, i.e.\ a
-type designator (\sref{sec:type-desig}) that refers to a
-class\footnote{We assume that objects and packages also implicitly
-define a class (of the same name as the object or package, but
-inaccessible to user programs).} (\sref{sec:classes}), or as a {\em
-compound type} (\sref{sec:compound-types}) of class types.
-\todo{verify whether operands need to be class types}
+type designator (\sref{sec:type-desig}) that refers to a 
+class\footnote{We assume that objects and packages also
+implicitly define a class (of the same name as the object or package,
+but inaccessible to user programs).} (\sref{sec:classes}), 
+or as a {\em compound type} (\sref{sec:compound-types}) 
+consisting of class types and possibly
+also a refinement (\sref{sec:refinements}) that further constrains the
+types of its members.
 
 A shorthand exists for denoting function types
 (\sref{sec:function-types}).  Abstract value types are introduced by
@@ -472,14 +474,25 @@ the following types are ill-formed:
 \label{sec:compound-types}
 
 \syntax\begin{lstlisting}
-  Type            ::=  SimpleType {with SimpleType} 
+  Type            ::=  SimpleType {with SimpleType} [Refinement]
+  Refinement      ::=  `{' [RefineStat {`;' RefineStat}] `}'
+  RefineStat      ::=  Dcl
+                    |  type TypeDef {`,' TypeDef}
+                    |
 \end{lstlisting}
 
-A compound type ~\lstinline@$T_1$ with $\ldots$ with $T_n$ {$R\,$}@~
-represents objects with members as given in the component types $T_1
-\commadots T_n$. Each component type $T_i$ must be a class type and
-the base class sequence generated by types $T_1 \commadots T_n$ must
-be well-formed (\sref{sec:basetypes-wf}). 
+A compound type ~\lstinline@$T_1$ with $\ldots$ with $T_n$ {$R\,$}@~  represents
+objects with members as given in the component types $T_1 \commadots
+T_n$ and the refinement \lstinline@{$R\,$}@. Each component type $T_i$ must be a
+class type and the base class sequence generated by types $T_1
+\commadots T_n$ must be well-formed (\sref{sec:basetypes-wf}). A
+refinement \lstinline@{$R\,$}@ contains declarations and type
+definitions. Each declaration or definition in a refinement must
+override a declaration or definition in one of the component types
+$T_1 \commadots T_n$. The usual rules for overriding (\sref{})
+apply. If no refinement is given, the empty refinement is implicitly
+added, i.e. ~\lstinline@$T_1$ with $\ldots$ with $T_n$@~ is a shorthand for
+~\lstinline@$T_1$ with $\ldots$ with $T_n$ {}@.
  
 \subsection{Function Types}
 \label{sec:function-types}
@@ -745,7 +758,10 @@ consisting only of package or object selectors and ending in $O$, then
 ~\lstinline@$O$.this.type $\equiv p$.type@.
 \item
 Two compound types are equivalent if their component types are
-pairwise equivalent.
+pairwise equivalent and their refinements are equivalent. Two
+refinements are equivalent if they bind the same names and the
+modifiers, types and bounds of every declared entity are equivalent in
+both refinements.
 \item
 Two method types are equivalent if they have equivalent result
 types, both have the same number of parameters, and corresponding
@@ -922,8 +938,9 @@ the expression is typed and evaluated is if it was
 \end{lstlisting}
 
 A {\em declaration} introduces names and assigns them types. It can
-only appear as one of the statements of a class definition
-(\sref{sec:templates}).
+appear as one of the statements of a class definition
+(\sref{sec:templates}) or as part of a refinement in a compound
+type (\sref{sec:refinements}).
 
 A {\em definition} introduces names that denote terms or types. It can
 form part of an object or class definition or it can be local to a
@@ -2703,7 +2720,13 @@ constructor invocations (of types $S, T_1 \commadots T_n$, say) and
 $stats$ is a statement sequence containing initializer statements and
 member definitions (\sref{sec:members}). The type of such an instance
 creation expression is then the compound type
-\lstinline@$S$ with $T_1$ with $\ldots$ with $T_n$@.
+\lstinline@$S$ with $T_1$ with $\ldots$ with $T_n$ {$R\,$}@,
+where \lstinline@{$R\,$}@ is
+a refinement (\sref{sec:compound-types}) which declares exactly those
+members of $stats$ that override a member of $S$ or $T_1 \commadots
+T_n$. \todo{what about methods and overloaded defs?}  For this type to
+be well-formed, $R$ may not reference types defined in $stats$ which
+do not themselves form part of $R$.
 
 The instance creation expression is evaluated by creating a fresh
 object, which is initialized by evaluating the expression template.
@@ -3375,7 +3398,7 @@ Concretely, we distinguish the following kinds of patterns.
 A {\em wild-card pattern} \_ matches any value. 
 
 A {\em typed pattern} $\_: T$ matches values of type $T$. The type $T$ may be
- a class type or a compound type.
+ a class type or a compound type; it may not contain a refinement (\sref{sec:refinements}).  
 This pattern matches any non-null value of type $T$. $T$ must conform to the pattern's expected
 type. A pattern $x:T$ is treated the same way as $x @ (_:T)$
 
@@ -4238,7 +4261,7 @@ grammar.
   Type           ::=  Type1 `=>' Type
                    |  `(' [Types] `)' `=>' Type
                    |  Type1
-  Type1          ::=  SimpleType {with SimpleType} 
+  Type1          ::=  SimpleType {with SimpleType} [Refinement]
   SimpleType     ::=  SimpleType TypeArgs
                    |  SimpleType `#' id
                    |  StableId
@@ -4246,6 +4269,10 @@ grammar.
                    |  `(' Type ')'
   TypeArgs        ::=  `[' Types `]'
   Types           ::=  Type {`,' Type}
+  Refinement      ::=  `{' [RefineStat {`;' RefineStat}] `}'
+  RefineStat      ::=  Dcl
+                    |  type TypeDef {`,' TypeDef}
+                    |
 
   Exprs           ::=  Expr {`,' Expr}
   Expr            ::=  Bindings `=>' Expr