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 escjava.ast;
014    
015    import java.util.Hashtable;
016    import java.util.Set;
017    import java.util.ArrayList;
018    
019    import javafe.ast.*;
020    import javafe.util.Assert;
021    import javafe.util.Location;
022    import escjava.ParsedRoutineSpecs;
023    
024    // Convention: unless otherwise noted, integer fields named "loc" refer
025    // to the location of the first character of the syntactic unit
026    
027    //# TagBase javafe.tc.TagConstants.LAST_TAG + 1
028    //# VisitorRoot javafe.ast.Visitor
029    
030    
031    public class ModelConstructorDeclPragma extends TypeDeclElemPragma
032    {
033      public /*@ non_null @*/ ConstructorDecl decl;
034    
035      public int loc;
036    
037      public /*@ non_null @*/ SimpleName id;
038    
039    
040      public void setParent(/*@non_null*/TypeDecl p) {
041        super.setParent(p);
042        if (decl != null) 
043            decl.setParent(p);
044      }
045    
046      //@ public represents startLoc <- loc;
047      public /*@ pure @*/ int getStartLoc() { return loc; }
048      /*@ also
049        @ public normal_behavior
050        @ ensures \result == decl.getEndLoc();
051        @*/
052      public /*@ pure @*/ int getEndLoc() { return decl.getEndLoc(); }
053      public void decorate(ModifierPragmaVec modifierPragmas) {
054        if (decl.pmodifiers == null) {
055            decl.pmodifiers = modifierPragmas;
056        } else if (modifierPragmas != null) {
057            // FIXME - should be prepen???
058            decl.pmodifiers.append(modifierPragmas); 
059        }
060      }
061    
062    
063    // Generated boilerplate constructors:
064    
065      //@ ensures this.decl == decl;
066      //@ ensures this.loc == loc;
067      //@ ensures this.id == id;
068      protected ModelConstructorDeclPragma(/*@ non_null @*/ ConstructorDecl decl, int loc, /*@ non_null @*/ SimpleName id) {
069         this.decl = decl;
070         this.loc = loc;
071         this.id = id;
072      }
073    
074    // Generated boilerplate methods:
075    
076      public final int childCount() {
077         return 2;
078      }
079    
080      public final Object childAt(int index) {
081              /*throws IndexOutOfBoundsException*/
082         if (index < 0)
083            throw new IndexOutOfBoundsException("AST child index " + index);
084         int indexPre = index;
085    
086         int sz;
087    
088         if (index == 0) return this.decl;
089         else index--;
090    
091         if (index == 0) return this.id;
092         else index--;
093    
094         throw new IndexOutOfBoundsException("AST child index " + indexPre);
095      }   //@ nowarn Exception;
096    
097      public final /*@non_null*/String toString() {
098         return "[ModelConstructorDeclPragma"
099            + " decl = " + this.decl
100            + " loc = " + this.loc
101            + " id = " + this.id
102            + "]";
103      }
104    
105      public final int getTag() {
106         return TagConstants.MODELCONSTRUCTORDECLPRAGMA;
107      }
108    
109      public final void accept(javafe.ast.Visitor v) { 
110        if (v instanceof Visitor) ((Visitor)v).visitModelConstructorDeclPragma(this);
111      }
112    
113      public final Object accept(javafe.ast.VisitorArgResult v, Object o) { 
114        if (v instanceof VisitorArgResult) return ((VisitorArgResult)v).visitModelConstructorDeclPragma(this, o); else return null;
115      }
116    
117      public void check() {
118         this.decl.check();
119         this.id.check();
120      }
121    
122      //@ ensures \result != null;
123      public static ModelConstructorDeclPragma make(/*@ non_null @*/ ConstructorDecl decl, int loc, /*@ non_null @*/ SimpleName id) {
124         ModelConstructorDeclPragma result = new ModelConstructorDeclPragma(decl, loc, id);
125         return result;
126      }
127    }