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 ModelTypePragma extends TypeDeclElemPragma
032    {
033      public /*@ non_null @*/ TypeDecl decl;
034    
035      public int loc;
036    
037    
038      public void setParent(/*@non_null*/TypeDecl p) {
039        super.setParent(p);
040        if (decl != null) 
041            decl.setParent(p);
042      }
043    
044      //@ public represents startLoc <- loc;
045      public /*@ pure @*/ int getStartLoc() { return loc; }
046      /*@ also
047        @ public normal_behavior
048        @ ensures \result == decl.getEndLoc();
049        @*/
050      public /*@ pure @*/ int getEndLoc() { return decl.getEndLoc(); }
051      public void decorate(ModifierPragmaVec modifierPragmas) {
052        if (decl.pmodifiers == null) {
053            decl.pmodifiers = modifierPragmas;
054            // FIXME - should be prepen???
055        } else if (modifierPragmas != null) {
056            decl.pmodifiers.append(modifierPragmas); 
057        }
058      }
059    
060    
061    // Generated boilerplate constructors:
062    
063      //@ ensures this.decl == decl;
064      //@ ensures this.loc == loc;
065      protected ModelTypePragma(/*@ non_null @*/ TypeDecl decl, int loc) {
066         this.decl = decl;
067         this.loc = loc;
068      }
069    
070    // Generated boilerplate methods:
071    
072      public final int childCount() {
073         return 1;
074      }
075    
076      public final Object childAt(int index) {
077              /*throws IndexOutOfBoundsException*/
078         if (index < 0)
079            throw new IndexOutOfBoundsException("AST child index " + index);
080         int indexPre = index;
081    
082         int sz;
083    
084         if (index == 0) return this.decl;
085         else index--;
086    
087         throw new IndexOutOfBoundsException("AST child index " + indexPre);
088      }   //@ nowarn Exception;
089    
090      public final /*@non_null*/String toString() {
091         return "[ModelTypePragma"
092            + " decl = " + this.decl
093            + " loc = " + this.loc
094            + "]";
095      }
096    
097      public final int getTag() {
098         return TagConstants.MODELTYPEPRAGMA;
099      }
100    
101      public final void accept(javafe.ast.Visitor v) { 
102        if (v instanceof Visitor) ((Visitor)v).visitModelTypePragma(this);
103      }
104    
105      public final Object accept(javafe.ast.VisitorArgResult v, Object o) { 
106        if (v instanceof VisitorArgResult) return ((VisitorArgResult)v).visitModelTypePragma(this, o); else return null;
107      }
108    
109      public void check() {
110         this.decl.check();
111      }
112    
113      //@ ensures \result != null;
114      public static ModelTypePragma make(/*@ non_null @*/ TypeDecl decl, int loc) {
115         ModelTypePragma result = new ModelTypePragma(decl, loc);
116         return result;
117      }
118    }