001    // -*- mode: java -*-
002    /* Copyright 2000, 2001, Compaq Computer Corporation */
003    
004    /* IF THIS IS A JAVA FILE, DO NOT EDIT IT!  
005    
006       Most Java files in this directory which are part of the Javafe AST
007       are automatically generated using the astgen comment (see
008       ESCTools/Javafe/astgen) from the input file 'hierarchy.h'.  If you
009       wish to modify AST classes or introduce new ones, modify
010       'hierarchy.j.'
011     */
012    
013    package javafe.ast;
014    
015    import javafe.util.Assert;
016    import javafe.util.Location;
017    import javafe.util.ErrorSet;
018    
019    // Convention: unless otherwise noted, integer fields named "loc" refer
020    // to the location of the first character of the syntactic unit
021    
022    
023    /**
024     * Represents a ObjectDesignator of the form "TypeName . " 
025     *
026     * <p> Is created from AmbiguousVariableAccess/AmbiguousMethodInvocation
027     * by the name resolution code.  
028     * The <code>type</code> must be an instance of either <code>TypeName</code>
029     * or <code>TypeSig</code>  (found in <code>javafe.tc</code>).
030     * If <code>type</code> is a <code>TypeName</code>, then an explicit
031     * type name was given in the program text; if <code>type</code> 
032     * is a <code>TypeSig</code>, then the type was inferred.
033     */
034    
035    public class TypeObjectDesignator extends ObjectDesignator
036    {
037      //@ invariant type instanceof TypeName || type instanceof javafe.tc.TypeSig;
038      public /*@ non_null @*/ Type type;
039    
040    
041      private void postCheck() {
042        Assert.notNull(type);       
043      }
044    
045      //@ public represents startLoc <- (type instanceof javafe.tc.TypeSig) ? locDot : type.getStartLoc();
046        public /*@ pure @*/ int getStartLoc() {
047            if (!(type instanceof javafe.tc.TypeSig))
048                return type.getStartLoc();
049    
050            return locDot;
051        }
052    
053      public /*@ pure @*/ Type type() { return type; }
054    
055      //* Manual maker to ensure invariant on type satisfied
056      //@ requires type instanceof TypeName || type instanceof javafe.tc.TypeSig;
057      //
058      //@ requires locDot != javafe.util.Location.NULL;
059      public static /*@non_null*/ TypeObjectDesignator make(int locDot, 
060                                              /*@ non_null @*/ Type type) {
061         TypeObjectDesignator result = new TypeObjectDesignator(locDot, type);
062         return result;
063      }
064    
065    
066    // Generated boilerplate constructors:
067    
068      //@ ensures this.locDot == locDot;
069      //@ ensures this.type == type;
070      protected TypeObjectDesignator(int locDot, /*@ non_null @*/ Type type) {
071         super(locDot);
072         this.type = type;
073      }
074    
075    // Generated boilerplate methods:
076    
077      public final int childCount() {
078         return 1;
079      }
080    
081      public final Object childAt(int index) {
082              /*throws IndexOutOfBoundsException*/
083         if (index < 0)
084            throw new IndexOutOfBoundsException("AST child index " + index);
085         int indexPre = index;
086    
087         int sz;
088    
089         if (index == 0) return this.type;
090         else index--;
091    
092         throw new IndexOutOfBoundsException("AST child index " + indexPre);
093      }   //@ nowarn Exception;
094    
095      public final /*@non_null*/String toString() {
096         return "[TypeObjectDesignator"
097            + " locDot = " + this.locDot
098            + " type = " + this.type
099            + "]";
100      }
101    
102      public final int getTag() {
103         return TagConstants.TYPEOBJECTDESIGNATOR;
104      }
105    
106      public final void accept(Visitor v) { v.visitTypeObjectDesignator(this); }
107    
108      public final Object accept(VisitorArgResult v, Object o) {return v.visitTypeObjectDesignator(this, o); }
109    
110      public void check() {
111         super.check();
112         this.type.check();
113         postCheck();
114      }
115    
116    }