Yet more type system tests

src/types.h

 // Copyright 2014 the V8 project authors. All rights reserved.
 // Use of this source code is governed by a BSD-style license that can be
 // found in the LICENSE file.
 
 #ifndef V8_TYPES_H_
 #define V8_TYPES_H_
 
 #include "handles.h"
 
 namespace v8 {
 namespace internal {
 
+// SUMMARY
+//
 // A simple type system for compiler-internal use. It is based entirely on
 // union types, and all subtyping hence amounts to set inclusion. Besides the
 // obvious primitive types and some predefined unions, the type language also
 // can express class types (a.k.a. specific maps) and singleton types (i.e.,
 // concrete constants).
 //
 // Types consist of two dimensions: semantic (value range) and representation.
 // Both are related through subtyping.
 //
+// SEMANTIC DIMENSION
+//
 // The following equations and inequations hold for the semantic axis:
 //
 //   None <= T
 //   T <= Any
 //
 //   Number = Signed32 \/ Unsigned32 \/ Double
 //   Smi <= Signed32
 //   Name = String \/ Symbol
 //   UniqueName = InternalizedString \/ Symbol
 //   InternalizedString < String
 //
 //   Receiver = Object \/ Proxy
 //   Array < Object
 //   Function < Object
 //   RegExp < Object
 //   Undetectable < Object
 //   Detectable = Receiver \/ Number \/ Name - Undetectable
 //
 //   Class(map) < T   iff instance_type(map) < T
 //   Constant(x) < T  iff instance_type(map(x)) < T
 //
 // Note that Constant(x) < Class(map(x)) does _not_ hold, since x's map can
 // change! (Its instance type cannot, however.)
 // TODO(rossberg): the latter is not currently true for proxies, because of fix,
 // but will hold once we implement direct proxies.
 //
+// REPRESENTATIONAL DIMENSION
+//
 // For the representation axis, the following holds:
 //
 //   None <= R
 //   R <= Any
 //
 //   UntaggedInt <= UntaggedInt8 \/ UntaggedInt16 \/ UntaggedInt32)
 //   UntaggedFloat <= UntaggedFloat32 \/ UntaggedFloat64
 //   UntaggedNumber <= UntaggedInt \/ UntaggedFloat
 //   Untagged <= UntaggedNumber \/ UntaggedPtr
 //   Tagged <= TaggedInt \/ TaggedPtr
 //
 // Subtyping relates the two dimensions, for example:
 //
 //   Number <= Tagged \/ UntaggedNumber
 //   Object <= TaggedPtr \/ UntaggedPtr
 //
 // That holds because the semantic type constructors defined by the API create
 // types that allow for all possible representations, and dually, the ones for
 // representation types initially include all semantic ranges. Representations
 // can then e.g. be narrowed for a given semantic type using intersection:
 //
 //   SignedSmall /\ TaggedInt       (a 'smi')
 //   Number /\ TaggedPtr            (a heap number)
 //
+// PREDICATES
+//
 // There are two main functions for testing types:
 //
 //   T1->Is(T2)     -- tests whether T1 is included in T2 (i.e., T1 <= T2)
 //   T1->Maybe(T2)  -- tests whether T1 and T2 overlap (i.e., T1 /\ T2 =/= 0)
 //
 // Typically, the former is to be used to select representations (e.g., via
 // T->Is(SignedSmall())), and the latter to check whether a specific case needs
 // handling (e.g., via T->Maybe(Number())).
 //
 // There is no functionality to discover whether a type is a leaf in the
 // lattice. That is intentional. It should always be possible to refine the
 // lattice (e.g., splitting up number types further) without invalidating any
 // existing assumptions or tests.
 // Consequently, do not use pointer equality for type tests, always use Is!
 //
+// PROPERTIES
+//
+// Various formal properties hold for constructors, operators, and predicates
+// over types. For example, constructors are injective, subtyping is a partial
+// order, and union and intersection satisfy the usual algebraic properties.
+//
+// See test/cctest/test-typing.cc for a comprehensive executable specification,

[Benedikt Meurer, 2014/04/10 10:54:50]

Nit: test-types.cc

+// especially with respect to the more exotic temporal constructors and
+// predicates (prefixed 'Now').
+//
+// IMPLEMENTATION
+//
 // Internally, all 'primitive' types, and their unions, are represented as
 // bitsets. Class is a heap pointer to the respective map. Only Constant's, or
 // unions containing Class'es or Constant's, currently require allocation.
 // Note that the bitset representation is closed under both Union and Intersect.
 //
 // There are two type representations, using different allocation:
 //
 // - class Type (zone-allocated, for compiler and concurrent compilation)
 // - class HeapType (heap-allocated, for persistent types)
 //
@@ skipping 404 matching lines @@
   bool Narrows(BoundsImpl that) {
     return that.lower->Is(this->lower) && this->upper->Is(that.upper);
   }
 };
 
 typedef BoundsImpl<ZoneTypeConfig> Bounds;
 
 } }  // namespace v8::internal
 
 #endif  // V8_TYPES_H_