include "polyglot/parse/java12.cup"

package jif.parse;
import polyglot.lex.Lexer;
import polyglot.lex.Identifier;
import polyglot.lex.Token;
import polyglot.frontend.Job;
import polyglot.parse.VarDeclarator;
import polyglot.ast.*;
import jif.ast.*;
import jif.types.*;
import jif.extension.JifBinaryDel;

import java.util.*;

parser Grm extends polyglot.parse.Grm {:

    public final JifNodeFactory nf; /* shadows BaseParser.nf */
    public final JifTypeSystem ts; /* shadows BaseParser.ts */

    public Grm(polyglot.lex.Lexer l, JifTypeSystem t,
	       JifNodeFactory n, ErrorQueue q) {
	super(l,t,n,q);
	ts = t;
	nf = n;
    }

    /**
     * After we parse as usual, the AST may contain reftype_or_expr
     * nodes wrapped in expressions.  These are the _only_
     * reftype_or_expr expressions in the AST at this point, although
     * there may be reftype_or_expr types, qualifiers, etc.  Here, we
     * make a visitor pass over the AST to unwrap these reftype_or_expr
     * nodes and convert them to (possibly reftype_or_expr)
     * expressions.
     *
     * This pass is done after parsing to avoid having to convert
     * expressions into types. */
    public java_cup.runtime.Symbol parse() throws Exception {
        java_cup.runtime.Symbol sym = super.parse();

        if (sym == null || sym.value == null) {
            return null;
        }

        Node n = (Node) sym.value;
        sym.value = n.visit(new UnwrapVisitor());
        return sym;
    }

    // Since there are no inner classes, a type qualifier must be a package.
    public PackageNode exprToPackage(Expr e) throws Exception {
        if (e instanceof Wrapper) {
            return ((Wrapper) e).amb.toPackage();
        }

        if (e instanceof AmbExpr) {
            AmbExpr a = (AmbExpr) e;
            return nf.PackageNode(pos(e), ts.packageForName(a.name()));
        }

        if (e instanceof Field) {
            Field f = (Field) e;
            PackageNode pn = prefixToPackage(f.target());
            return nf.PackageNode(pos(e),
                                ts.packageForName(pn.package_(), f.name()));
        }

        die(pos(e));
        return null;
    }
	
    public PackageNode prefixToPackage(Prefix p) throws Exception {
        if (p instanceof Expr) {
            return exprToPackage((Expr) p);
        }

        if (p instanceof AmbPrefix) {
            AmbPrefix a = (AmbPrefix) p;
            PackageNode pn = prefixToPackage(a.prefix());
            return nf.PackageNode(pos(p),
                                ts.packageForName(pn.package_(), a.name()));
        }

        die(pos(p));
        return null;
    }

    public ParamNode exprToParam(Expr e) throws Exception {
        if (e instanceof Wrapper) {
            Wrapper w = (Wrapper) e;
            if (w.amb instanceof Name) {
                Name a = (Name) w.amb;
                if (a.prefix() == null) {
                    return nf.AmbParam(pos(e), a.toIdentifier());
                }
            }
        }

        die(pos(e));
        return null;
    }

    public TypeNode exprToUninstType(Expr e) throws Exception {
        if (e instanceof Wrapper) {
            return ((Wrapper) e).amb.toUnlabeledType();
        }

        if (e instanceof AmbExpr) {
            AmbExpr a = (AmbExpr) e;
            return nf.AmbTypeNode(pos(e), a.name());
        }

        if (e instanceof Field) {
            Field f = (Field) e;
            Receiver r = f.target();
            return nf.AmbTypeNode(pos(e), prefixToPackage(r), f.name());
        }

        die(pos(e));
        return null;
    }

    public TypeNode exprToType(Expr e) throws Exception {
        if (e instanceof ArrayAccess) {
            ArrayAccess a = (ArrayAccess) e;
            Expr array = a.array();
            Expr index = a.index();

            TypeNode base = exprToUninstType(array);
            ParamNode param = exprToParam(index);

            List l = new LinkedList();
            l.add(param);
            return nf.InstTypeNode(pos(e), base, l);
        }

        return exprToUninstType(e);
    }

    public List toParamList(java.util.List l) throws Exception {
        List params = new TypedList(new LinkedList(), ParamNode.class, false);

        for (Iterator i = l.iterator(); i.hasNext(); ) {
            Object n = i.next();

            if (n instanceof Name) {
                params.add(nf.AmbParam(((Name) n).pos,
                                ((Name) n).toIdentifier()));
            }
            else if (n instanceof ParamNode) {
                params.add(n);
            }
            else if (n instanceof Expr) {
                params.add(nf.AmbParam(((Expr) n).position(),
                                (Expr) n, null));
            }
            else if (n instanceof Node) {
                die(pos((Node) n));
                return null;
            }
            else {
                die(pos());
                return null;
            }
        }

        return params;
    }

    public List makeParamOrExprList(Expr a) {
	List l = new TypedList(new LinkedList(), Object.class, false);

	if (a instanceof Wrapper) {
	    Wrapper w = (Wrapper) a;

	    if (w.amb instanceof Name &&
		((Name) w.amb).prefix == null) {

		// Could be a field, local, principal, or param of the
		// current class. The last three can be used to
		// instantiate a class.
		l.add(w.amb);
	    }
	    else {
		l.add(a);
	    }
	} else {
	    l.add(a);
	}
	return l;
    }

    /**
     * Return the source position of the Parse.
     */
    public static Position pos(Amb n) {
	if (n == null) {
	    return null;
	}
	return n.pos;
    }

    protected Position posForObject(Object o) {
      if (o instanceof Amb) {
          return pos((Amb) o);
      }
      return super.posForObject(o);
    }

    public Position pos(Declarator n) {
        if (n == null) {
            return null;
        }
        return n.position();
    }

    public Position pos() {
        return new Position(lexer.path(), lexer.file());
    }

    public Amb makeAccessOrInst(Amb a, List b) throws Exception {
		if (a instanceof Access) {
		    return new Access(this, pos(a), a, (Expr) b.get(0));
		} else {
		    if (b.size() == 1) {
				if (b.get(0) instanceof ParamNode) {
				    return new Inst(this, pos(a), a.toClassType(), b);
				}
				else {
				    return new InstOrAccess(this, pos(a), a, b.get(0));
				}
		    } else {
				return new Inst(this,pos(a), a.toClassType(), toParamList(b));
		    }
		}
    }

    public static final String TYPE_ANNOTATION = "labeled types";
    public static final String PC_BOUND_ANNOTATION = "pc bound";
    public static final String END_LABEL_ANNOTATION = "end labels";
    public static final String METHOD_AUTH_ANNOTATION = "authority where-constraints";
    public static final String METHOD_CALLER_ANNOTATION = "caller where-constraints";
    public static final String METHOD_AUTO_ENDORSE_ANNOTATION = "auto-endorse where-constraints";
    public static final String METHOD_ACTSFOR_ANNOTATION = "actsfor where-constraints";
    public static final String METHOD_LABEL_ASSERTION_ANNOTATION = "label leq where-constraints";


	private static final Set linesSeen = new HashSet();
    public void countAnnotation(String key, Position pos) {
        Job job = ts.extensionInfo().scheduler().currentJob();
        String countKey = "Jif annotations: " + job + " : " + key;
        String countAllKey = "Jif annotations: all " + key;
        ts.extensionInfo().getStats().accumPassTimes(countKey, 1, 1);
        ts.extensionInfo().getStats().accumPassTimes(countAllKey, 1, 1);
        String posString = new Position(pos.path(), pos.file(), pos.line()).toString();
        // check if the position is already recorded.
        
        if (!linesSeen.contains(posString)) {
        	linesSeen.add(posString);
	        ts.extensionInfo().getStats().accumPassTimes("Jif annotations: TOTAL LINES WITH ANNOTATION", 1, 1);        	
        }
    }

:};

terminal Token WHERE;
terminal Token MEET;
terminal Token PRINCIPAL;
terminal Token LABEL;
terminal Token COVARIANT;
terminal Token INVARIANT;
terminal Token AUTHORITY;
terminal Token CALLER;
terminal Token ACTSFOR;
terminal Token ACTSFOR_LOWER;
terminal Token EQUIV;
terminal Token DECLASSIFY;
terminal Token ENDORSE;
terminal Token TO;

terminal Token JOIN;
terminal Token RIGHTARROW;
terminal Token LEFTARROW;

non terminal DeclassifyExpr declassify;
non terminal DeclassifyStmt declassify_statement;
non terminal EndorseExpr endorse;
non terminal EndorseStmt endorse_statement;
non terminal LabelNode downgrade_to_label_opt;
non terminal TypeNode labeled_primitive_type;
non terminal LabelNode label, label_opt, return_label_opt, label_flexible;
non terminal List join_component_list;
non terminal Object join_label_component; // either a LabelNode or PolicyNode
non terminal List meet_component_list;
non terminal Object label_component; // either a LabelNode or PolicyNode
non terminal PolicyNode label_component_policy;
non terminal PrincipalNode principal, principal_conjunctive, principal_disjunctive, principal_base;
non terminal Token actsfor;
non terminal Expr accesspath;
non terminal Receiver accesspath_receiver;
non terminal Expr accesspath_no_id;
non terminal List principal_list, principal_list_opt;

non terminal List parameters_opt, parameters;
non terminal ParamDecl parameter;
non terminal List constraints, constraints_opt;
non terminal List authority, authority_opt;
non terminal ConstraintNode constraint;
non terminal Amb reftype_or_expr, objtype_or_expr;
non terminal List param_or_expr_list;
non terminal Expr primary_no_array;
non terminal TypeNode primitive_array_type;
non terminal ConstructorCall explicit_super_constructor_invocation;
non terminal Token leftarrow, rightarrow;

start with goal;

// Jif labels
label ::=
                    // LabelNode
        LBRACE:x RBRACE:y
            {: RESULT = parser.nf.CanonicalLabelNode(parser.pos(x, y),
                                        parser.ts.noComponentsLabel(parser.pos(x, y))); :}
    |   LBRACE:x join_component_list:a RBRACE:y
            {: LabelNode ln;
               ln = parser.nf.JoinLabelNode(parser.pos(x, y), a);
               RESULT = ln; :}
    |   LBRACE:x join_component_list:a RBRACE:y MEET label:c
            {: LabelNode ln;
               ln = parser.nf.JoinLabelNode(parser.pos(x, y), a);
               List col = new ArrayList(2);
               col.add(ln);
               col.add(c);
               LabelNode mn = parser.nf.MeetLabelNode(parser.pos(x,c), col);
               RESULT = mn; :}
    |   LBRACE:x join_component_list:a RBRACE:y JOIN label:c
            {: LabelNode ln;
               ln = parser.nf.JoinLabelNode(parser.pos(x, y), a);
               List col = new ArrayList(2);
               col.add(ln);
               col.add(c);
               LabelNode mn = parser.nf.JoinLabelNode(parser.pos(x,c), col);
               RESULT = mn; :}
    |    LBRACE label:l RBRACE
            {: RESULT = l; :}
    ;
label_opt ::=
                    // LabelNode
            {: RESULT = null; :}
    |   label:a
            {: RESULT = a; :}
    ;

label_flexible ::=
      // LabelNode
      label:a
            {: RESULT = a; :}
    | accesspath:a
            {: RESULT = parser.nf.AmbDynamicLabelNode(parser.pos(a), a); :}
    ;
join_component_list ::=
                    // List of LabelNode or PolicyNode. Implicitly a join
                    // between them
        join_label_component:a
            {: List l = new TypedList(new LinkedList(), Node.class, false);
               l.add(a);
               RESULT = l; :}
    |   join_component_list:a SEMICOLON join_label_component:b
            {: RESULT = a;
               a.add(b); :}
        ;
join_label_component ::=
                    // LabelNode or PolicyNode
        meet_component_list:a
            {: Object o;
               if (a.size() > 1) {
                  o = parser.nf.MeetLabelNode(parser.pos(a), a);
               }
               else o = a.iterator().next();
               RESULT = o;
               :}
         ;
meet_component_list ::=
                    // List of LabelNode or PolicyNode
        label_component:a
            {: List l = new ArrayList();
               l.add(a);
               RESULT = l; :}
    |   meet_component_list:a MEET label_component:b
            {: RESULT = a;
               a.add(b); :}
    ;
label_component ::=
                    // LabelNode or PolicyNode
        label_component_policy:a
            {: RESULT = a; :}
    |   MULT:x accesspath:a
            {: RESULT = parser.nf.AmbDynamicLabelNode(parser.pos(x, a),
						      a); :}
    |   THIS:a
            {: RESULT = parser.nf.AmbThisLabelNode(parser.pos(a)); :}
    |   IDENTIFIER:a
            {: RESULT = parser.nf.AmbVarLabelNode(parser.pos(a),
						  parser.nf.Id(parser.pos(a), a.getIdentifier())); :}
    ;

rightarrow ::= COLON:a 
            {: RESULT = a; :}     
     | RIGHTARROW:a 
            {: RESULT = a; :}     
     | MINUS GT:a 
            {: RESULT = a; :}     
     ;
leftarrow ::= NOT COLON:a
            {: RESULT = a; :}     
     | LEFTARROW:a 
            {: RESULT = a; :}     
     | LT MINUS:a 
            {: RESULT = a; :}     
     ;

label_component_policy ::=
                    // PolicyNode
        principal_disjunctive:a rightarrow:arr principal_list_opt:b
            {: RESULT = parser.nf.ReaderPolicyNode(parser.pos(a, parser.pos(b)==null?arr:b), a, b); :}
    |   principal_disjunctive:a leftarrow:arr principal_list_opt:b
            {: RESULT = parser.nf.WriterPolicyNode(parser.pos(a, parser.pos(b)==null?arr:b), a, b); :}
    ;

principal_list_opt ::=
                    // List of PrincipalNode
            {: RESULT = new TypedList(new LinkedList(), PrincipalNode.class,
				      false); :}
    |   principal_list:a
            {: RESULT = a; :}
    ;
principal_list ::=
                    // List of PrincipalNode
        principal_conjunctive:a
            {: List l = new TypedList(new LinkedList(), PrincipalNode.class, false);
           l.add(a);
               RESULT = l; :}
    |   principal_list:a COMMA principal_conjunctive:b
            {: RESULT = a;
               a.add(b); :}
    ;
principal ::=
       principal_conjunctive:a
            {: RESULT = a; :}
    ;
principal_disjunctive ::=
       principal_conjunctive:a
            {: RESULT = a; :}
    |  principal:a COMMA principal_conjunctive:b
            {: RESULT = parser.nf.AmbDisjunctivePrincipalNode(parser.pos(a,b),a,b); :}
    ;
principal_conjunctive ::=
       principal_base:a
            {: RESULT = a; :}
    |  principal_conjunctive:a AND principal_base:b
            {: RESULT = parser.nf.AmbConjunctivePrincipalNode(parser.pos(a,b),a,b); :}
    ;
principal_base ::=
                    // PrincipalNode
        accesspath_no_id:a
            {: RESULT = parser.nf.AmbPrincipalNode(parser.pos(a), a); :}
    |  MULT:a // top principal
            {: RESULT = parser.nf.CanonicalPrincipalNode(parser.pos(a), parser.ts.topPrincipal(parser.pos(a))); :}
    |  IDENTIFIER:a
            {: RESULT = parser.nf.AmbPrincipalNode(parser.pos(a), parser.nf.Id(parser.pos(a), a.getIdentifier())); :}
    |  LPAREN:a principal_disjunctive:b RPAREN:c
            {: RESULT = b; :}
    ;

accesspath ::=
        THIS:a {:  RESULT = parser.nf.This(parser.pos(a));  :}
    |   IDENTIFIER:a {: RESULT = new Name(parser, parser.pos(a), a.getIdentifier()).toExpr(); :}
    | accesspath_receiver:a DOT IDENTIFIER:b
             {: RESULT = parser.nf.Field(parser.pos(a, b),
	                     a,
			        b.getIdentifier()); :}
     ;

accesspath_receiver ::=
        THIS:a {:  RESULT = parser.nf.This(parser.pos(a));  :}
    |   IDENTIFIER:a {: RESULT = new Name(parser, parser.pos(a), a.getIdentifier()).toReceiver(); :}
    | accesspath_receiver:a DOT IDENTIFIER:b
             {: RESULT = parser.nf.Field(parser.pos(a, b),
	                     a,
			        b.getIdentifier()); :}
     ;

accesspath_no_id ::=
        THIS:a {:  RESULT = parser.nf.This(parser.pos(a));  :}
    | accesspath_receiver:a DOT IDENTIFIER:b
             {: RESULT = parser.nf.Field(parser.pos(a, b), a, b.getIdentifier()); :};

// 19.4) Types, Values, and Variables

drop { type ::= primitive_type | reference_type; }
extend type ::=
                    // TypeNode
        labeled_primitive_type:a
            {: RESULT = a; :}
    |   reftype_or_expr:a
            {: RESULT = a.toType(); :}
    |   primitive_array_type:a
            {: RESULT = a; :}
    |   primitive_array_type:a label:b
            {: RESULT = parser.nf.LabeledTypeNode(parser.pos(a,b), a, b); :}
    ;

extend primitive_type ::=
                    // TypeNode
        LABEL:a
            {: RESULT = parser.nf.CanonicalTypeNode(parser.pos(a), parser.ts.Label()); :}
    |   PRINCIPAL:a
            {: RESULT = parser.nf.CanonicalTypeNode(parser.pos(a), parser.ts.Principal()); :}
    ;

labeled_primitive_type  ::=
        primitive_type:a
            {: RESULT = a; :}
    |   primitive_type:a label:b
            {: RESULT = parser.nf.LabeledTypeNode(parser.pos(a, b), a, b);
               parser.countAnnotation(parser.TYPE_ANNOTATION, RESULT.position());
            :}
    ;

drop { reference_type ::= array_type | class_or_interface_type; }
extend reference_type ::=
                    // TypeNode
        primitive_array_type:a
            {: RESULT = a; :}
    |   reftype_or_expr:a
            {: RESULT = a.toType(); :}
    ;
override class_or_interface_type ::=
                    // TypeNode
        reftype_or_expr:a
            {: RESULT = a.toType(); :}
    ;
drop { array_type }

primitive_array_type ::=
                    // TypeNode
        labeled_primitive_type:a LBRACK RBRACK:y
            {: RESULT = new Array(parser, parser.pos(a,y), a).toType(); :}
    |   labeled_primitive_type:a CONST LBRACK RBRACK:y
            {: RESULT = new Array(parser, parser.pos(a,y), a, true).toType(); :}
    |   primitive_array_type:a label_opt:b LBRACK RBRACK:y
            {: if (b != null) {
                   a = parser.nf.LabeledTypeNode(parser.pos(a, b), a, b);
               }
               RESULT = new Array(parser, parser.pos(a,y), a).toType();
               if (b != null) parser.countAnnotation(parser.TYPE_ANNOTATION, RESULT.position());
            :};
// 19.5) Names
override simple_name ::=
                    // Name
        IDENTIFIER:a
            {: RESULT = new Name(parser, parser.pos(a), a.getIdentifier()); :}
    ;
override qualified_name ::=
                    // Name
        name:a DOT IDENTIFIER:b
            {: RESULT = new Name(parser, parser.pos(a, b), a, b.getIdentifier()); :}
    ;

// 19.6) Packages
// 19.7) Productions used only in the LALR(1) grammar
// 19.8) Classes

// 19.8.1) Class Declarations
drop { class_declaration ::=
        modifiers_opt CLASS IDENTIFIER
	super_opt interfaces_opt class_body; }

extend class_declaration ::=
                    // ClassDecl
        modifiers_opt:a CLASS:n IDENTIFIER:b
                parameters_opt:p super_opt:c
                interfaces_opt:d authority_opt:u class_body:e
            {: RESULT = parser.nf.JifClassDecl(parser.pos(n, b),
                                               a, parser.nf.Id(parser.pos(b), b.getIdentifier()),
                                               p, c, d, u, e); :}
    ;

drop { super ::= EXTENDS class_type; }
extend super ::=
                    // TypeNode
        EXTENDS objtype_or_expr:a
            {: RESULT = a.toUnlabeledType(); :}
    ;

drop { interface_type_list ::= interface_type
			    |  interface_type_list COMMA interface_type; }
interface_type_list ::=
                    // List of TypeNode
        objtype_or_expr:a
            {: List l = new TypedList(new LinkedList(), TypeNode.class, false);
               l.add(a.toUnlabeledType());
               RESULT = l; :}
    |   interface_type_list:a COMMA objtype_or_expr:b
            {: RESULT = a;
               a.add(b.toUnlabeledType()); :}
    ;

authority_opt ::=
            {: RESULT = new TypedList(new LinkedList(), PrincipalNode.class,
	       false); :}
    |   authority:a
            {: RESULT = a; :}
    ;
authority ::=
        AUTHORITY:n LPAREN principal_list:a RPAREN
        {: RESULT = a; :}
    ;
drop { class_body_declaration ::= block | static_initializer ; }
extend class_body_declaration ::=
      block:a 
          {: 
              parser.report_error ("Jif does not currently support initializer blocks.", parser.pos(a));
              if (true) throw new Exception();
           :}
    | static_initializer:a
          {: 
              parser.report_error ("Jif does not currently support initializer blocks.", parser.pos(a));
              if (true) throw new Exception();
           :}    
    ;
drop {
    class_member_declaration ::=
	modifiers_opt:a CLASS:n IDENTIFIER:b
	super_opt:c interfaces_opt:d class_body:e
    |   interface_declaration:a
    ;
}

// 19.8.2) Field Declarations
// 19.8.3) Method Declarations
drop {
    method_header ::=
        modifiers_opt type IDENTIFIER LPAREN
                formal_parameter_list_opt RPAREN dims_opt throws_opt
    |   modifiers_opt VOID IDENTIFIER LPAREN
                formal_parameter_list_opt RPAREN throws_opt
    ;
}
method_header ::=
                    // JifMethodNode
        modifiers_opt:a type:b IDENTIFIER:c label_opt:i
        LPAREN formal_parameter_list_opt:d RPAREN
        dims_opt:e return_label_opt:r throws_opt:f constraints_opt:w
            {: RESULT = parser.nf.JifMethodDecl(parser.pos(b,c,c), a,
                        parser.array(b, e.intValue()),
                        parser.nf.Id(parser.pos(c), c.getIdentifier()),
                                                i, d, r, f, w, null);
               if (i != null) parser.countAnnotation(parser.PC_BOUND_ANNOTATION, RESULT.position());
             :}
    |   modifiers_opt:a VOID:b IDENTIFIER:c label_opt:i
        LPAREN formal_parameter_list_opt:d RPAREN
        dims_opt:e return_label_opt:r throws_opt:f constraints_opt:w
            {: RESULT = parser.nf.JifMethodDecl(parser.pos(b,c), a,
                        parser.nf.CanonicalTypeNode(parser.pos(b),
                                   parser.ts.Void()),
                                   parser.nf.Id(parser.pos(c), c.getIdentifier()),
                                                i, d, r, f, w, null);
               if (i != null) parser.countAnnotation(parser.PC_BOUND_ANNOTATION, RESULT.position());
            :}
    ;

override formal_parameter ::=
                    // Formal
        type:a variable_declarator_id:b
            {: RESULT = parser.nf.Formal(parser.pos(a,b), Flags.NONE,
                                         parser.array(a, b.dims), b.name); :}
    |   FINAL:x type:a variable_declarator_id:b
            {: RESULT = parser.nf.Formal(parser.pos(x, b), Flags.FINAL,
                     parser.array(a, b.dims), b.name); :}
    ;

override throws ::=
                    // List of TypeNode
        THROWS LPAREN class_type_list:a RPAREN
            {: RESULT = a; :}
    |   THROWS interface_type_list:a
            {: RESULT = a; :}
    ;

return_label_opt ::=
                    // LabelNode
            {: RESULT = null; :}
    |   COLON label:a
            {:
               RESULT = a;
               parser.countAnnotation(parser.END_LABEL_ANNOTATION, RESULT.position());
            :}
    ;

// 19.8.4) Static Initializers

// drop { static_initializer }

// 19.8.5) Constructor Declarations

drop {constructor_declaration ::=
        modifiers_opt simple_name LPAREN formal_parameter_list_opt RPAREN
            throws_opt constructor_body
    ;
}

constructor_declaration ::=
                    // ConstructorDecl
        modifiers_opt:a reftype_or_expr:q
        LPAREN formal_parameter_list_opt:c RPAREN:y return_label_opt:r
        throws_opt:d constraints_opt:w constructor_body:e
            {: Id b; LabelNode i;
               // Pick apart the reftype_or_expr node.
               // It can be either an identifier "a" or an
               // identifier and label "a{L}".
               if (q instanceof LabeledExpr) {
                   b = ((LabeledExpr) q).prefix.toIdentifier();
                   i = ((LabeledExpr) q).label;
               }
               else {
                   b = q.toIdentifier();
                   i = null;
               }
           RESULT = parser.nf.JifConstructorDecl(parser.pos(q, y),
                             a, b, i, r, c, d, w, e); :}
    ;
drop { constructor_body ::= LBRACE block_statements RBRACE | LBRACE RBRACE; }

extend constructor_body ::=
                    // Block
        LBRACE:x block_statements:a explicit_super_constructor_invocation:b RBRACE:y
            {: List l = new TypedList(new LinkedList(), Stmt.class, false);
               l.addAll(a);
               l.add(b);
               RESULT = parser.nf.Block(parser.pos(x,y), l); :}
    |   LBRACE:x block_statements:a explicit_super_constructor_invocation:b block_statements:c RBRACE:y
            {: List l = new TypedList(new LinkedList(), Stmt.class, false);
               l.addAll(a);
               l.add(b);
               l.addAll(c);
               RESULT = parser.nf.Block(parser.pos(x,y), l); :}
    |   LBRACE:x block_statements:a RBRACE:y
            {: a.add(0, parser.nf.SuperCall(parser.pos(x),
                Collections.EMPTY_LIST));
               RESULT = parser.nf.Block(parser.pos(a,y), a); :}
    |   LBRACE:x RBRACE:y
            {: RESULT = parser.nf.Block(parser.pos(x,y),
                parser.nf.SuperCall(parser.pos(x),
                Collections.EMPTY_LIST)); :}
    ;

explicit_super_constructor_invocation ::=
                    // Stmt
        SUPER:a LPAREN argument_list_opt:b RPAREN:y SEMICOLON
            {: RESULT = parser.nf.SuperCall(parser.pos(a,y), b); :}
    ;
drop {
    explicit_constructor_invocation ::=
        SUPER LPAREN argument_list_opt RPAREN SEMICOLON
    |   primary DOT THIS LPAREN argument_list_opt RPAREN SEMICOLON
    |   primary DOT SUPER LPAREN argument_list_opt RPAREN SEMICOLON
    ;
}
extend explicit_constructor_invocation ::=
        explicit_super_constructor_invocation:a
            {: RESULT = a; :}
    ;

// 19.9) Interfaces

parameters_opt ::=
            // List of ParamDecl
            {: RESULT = new TypedList(new LinkedList(), ParamDecl.class, false); :}
    |
        LBRACK parameters:p RBRACK
            {: RESULT = p; :}
    ;

parameters ::=
            // List of ParamDecl
        parameter:a
            {: List l = new TypedList(new LinkedList(), ParamDecl.class, false);
               l.add(a);
               RESULT = l; :}
    |   parameters:a COMMA parameter:b
            {: RESULT = a;
               a.add(b); :}
    ;
parameter ::=
            // ParamDecl
    LABEL:x IDENTIFIER:a
        {: RESULT = parser.nf.ParamDecl(parser.pos(x, a),
                                        ParamInstance.INVARIANT_LABEL,
                                        parser.nf.Id(parser.pos(a), a.getIdentifier()));
                                        :}
    |   COVARIANT:x LABEL IDENTIFIER:a
        {: RESULT = parser.nf.ParamDecl(parser.pos(x, a),
                                        ParamInstance.COVARIANT_LABEL,
                                        parser.nf.Id(parser.pos(a), a.getIdentifier()));
                                        :}
    |   PRINCIPAL:x IDENTIFIER:a
        {: RESULT = parser.nf.ParamDecl(parser.pos(x, a),
                                        ParamInstance.PRINCIPAL,
                                        parser.nf.Id(parser.pos(a), a.getIdentifier()));
                                        :}
    ;


constraints_opt ::=
        // List of ConstraintNode
            {: RESULT = new TypedList(new LinkedList(), ConstraintNode.class, false); :}
    |   WHERE constraints:a
            {: RESULT = a; :}
    ;

constraints ::=
        // List of ConstraintNode
        constraint:a
            {: List l = new TypedList(new LinkedList(), ConstraintNode.class, false);
               l.add(a); RESULT = l; :}
    |   constraints:a COMMA constraint:b
            {: RESULT = a;
               a.add(b); :}
    ;

constraint ::=
        // ConstraintNode
        AUTHORITY:x LPAREN principal_list:a RPAREN:y
        {: RESULT = parser.nf.AuthConstraintNode(parser.pos(x,y), a);
           parser.countAnnotation(parser.METHOD_AUTH_ANNOTATION, RESULT.position());
        :}
    |   CALLER:x LPAREN principal_list:a RPAREN:y
        {: RESULT = parser.nf.CallerConstraintNode(parser.pos(x,y), a);
           parser.countAnnotation(parser.METHOD_CALLER_ANNOTATION, RESULT.position());
        :}
    |   ENDORSE:x LPAREN label_flexible:a RPAREN:y
        {: RESULT = parser.nf.AutoEndorseConstraintNode(parser.pos(x,y), a);
           parser.countAnnotation(parser.METHOD_AUTO_ENDORSE_ANNOTATION, RESULT.position());
        :}
    |   principal:a actsfor principal:b
        {: RESULT = parser.nf.ActsForConstraintNode(parser.pos(a,b), a, b);
           parser.countAnnotation(parser.METHOD_ACTSFOR_ANNOTATION, RESULT.position());
        :}
    |   principal:a EQUIV principal:b
        {: RESULT = parser.nf.ActsForConstraintNode(parser.pos(a,b), a, b, true);
           parser.countAnnotation(parser.METHOD_ACTSFOR_ANNOTATION, RESULT.position());
        :}
    |   label_flexible:a LTEQ label_flexible:b
        {: RESULT = parser.nf.LabelLeAssertionNode(parser.pos(a,b), a, b, false);
           parser.countAnnotation(parser.METHOD_LABEL_ASSERTION_ANNOTATION, RESULT.position());
        :}
    |   label:a EQUIV label:b
        {: RESULT = parser.nf.LabelLeAssertionNode(parser.pos(a,b), a, b, true);
           parser.countAnnotation(parser.METHOD_LABEL_ASSERTION_ANNOTATION, RESULT.position());
        :}
    ;

// 19.9.1) Interface Declarations
override interface_declaration ::=
        // ClassDecl
        modifiers_opt:a INTERFACE:n IDENTIFIER:b
                parameters_opt:p
                extends_interfaces_opt:d authority_opt:u interface_body:e
            {: RESULT = parser.nf.JifClassDecl(parser.pos(n,b),
		    a.set(Flags.INTERFACE), parser.nf.Id(parser.pos(b), b.getIdentifier()),
		    p, null, d, u, e); :}
    ;
drop { extends_interfaces ::=
        EXTENDS interface_type:a
    |   extends_interfaces:a COMMA interface_type:b
    ;
}
drop { interface_type }

extends_interfaces ::=
                    // List of TypeNode
        EXTENDS objtype_or_expr:a
            {: List l = new TypedList(new LinkedList(), TypeNode.class, false);
               l.add(a.toUnlabeledType());
               RESULT = l; :}
    |   extends_interfaces:a COMMA objtype_or_expr:b
            {: RESULT = a;
               a.add(b.toUnlabeledType()); :}
    ;

drop { interface_member_declaration ::=
	      class_declaration
	    | interface_declaration
	    ;
}

// 19.10) Arrays

// 19.11) Blocks and Statements
drop { block_statement ::= class_declaration ; }
override identifier_opt ::=
                    // Name
            {: RESULT = null; :}
    |   IDENTIFIER:a
            {: RESULT = new Name(parser, parser.pos(a), 
                a.getIdentifier()); :}
    ;

extend statement ::=
                    // Stmt
       declassify_statement:a
            {: RESULT = a; :}
    |  endorse_statement:a
            {: RESULT = a; :}
    ;
declassify_statement ::=
                    // DeclassifyStmt
        DECLASSIFY:n LPAREN label:b downgrade_to_label_opt:a RPAREN statement:c
            {: RESULT = parser.nf.DeclassifyStmt(parser.pos(n, c), a==null?null:b, a==null?b:a, c); :}
    ;

endorse_statement ::=
                    // EndorseStmt
        ENDORSE:n LPAREN label:b downgrade_to_label_opt:a RPAREN statement:c
            {: RESULT = parser.nf.EndorseStmt(parser.pos(n, c), a==null?null:b, a==null?b:a, c); :}
    |   ENDORSE:n LPAREN expression:e COMMA label:b downgrade_to_label_opt:a RPAREN if_then_statement:its
            {: RESULT = parser.nf.CheckedEndorseStmt(parser.pos(n, its), e, a==null?null:b, a==null?b:a, its); :}
    |   ENDORSE:n LPAREN expression:e COMMA label:b downgrade_to_label_opt:a RPAREN if_then_else_statement:its
            {: RESULT = parser.nf.CheckedEndorseStmt(parser.pos(n, its), e, a==null?null:b, a==null?b:a, its); :}
    |   ENDORSE:n LPAREN expression:e COMMA label:b downgrade_to_label_opt:a RPAREN LBRACE if_then_statement:its RBRACE:z
            {: RESULT = parser.nf.CheckedEndorseStmt(parser.pos(n, z), e, a==null?null:b, a==null?b:a, its); :}
    |   ENDORSE:n LPAREN expression:e COMMA label:b downgrade_to_label_opt:a RPAREN LBRACE if_then_else_statement:its RBRACE:z
            {: RESULT = parser.nf.CheckedEndorseStmt(parser.pos(n, z), e, a==null?null:b, a==null?b:a, its); :}
    ;

downgrade_to_label_opt ::=
        TO label:a {: RESULT = a; :}
    | {: RESULT = null; :}
    ;

// 19.12) Expr           // Expr
extend primary ::=
        NEW:n LABEL label:a
            {: RESULT = parser.nf.NewLabel(parser.pos(n, a), a); :}
    |   NEW:n PRINCIPAL LPAREN principal_disjunctive:a RPAREN:z
            {: RESULT = parser.nf.PrincipalExpr(parser.pos(n, z), a); :}
    |   NEW:n objtype_or_expr:a dims_opt:b
            {: RESULT = a.toNewArray(parser.pos(n, a), b); :}
    ;
extend primary_no_new_array ::=
        primary_no_array:a
            {: RESULT = a; :}
    ;
primary_no_array ::=
       declassify:a
            {: RESULT = a; :}
    |  endorse:a
            {: RESULT = a; :}
    ;
transfer primary_no_new_array to primary_no_array {
	literal | THIS | LPAREN expression RPAREN |
	class_instance_creation_expression | field_access |
        method_invocation
}

extend relational_expression ::=
     relational_expression:a actsfor shift_expression:b {:
                RESULT = parser.nf.Binary(parser.pos(a, b), a, JifBinaryDel.ACTSFOR, b);
                :}
  |  relational_expression:a EQUIV shift_expression:b {:
                RESULT = parser.nf.Binary(parser.pos(a, b), a, JifBinaryDel.EQUIV, b);
                :}
    ;

actsfor ::= ACTSFOR | ACTSFOR_LOWER ;

drop { /* no reflection */
primary_no_new_array ::=
	primitive_type DOT CLASS
    |   VOID DOT CLASS
    |   array_type DOT CLASS
    |   name DOT CLASS
    |   name DOT THIS
    ;
}
drop { /* no inner classes... */
    class_instance_creation_expression ::=
        NEW class_type LPAREN argument_list_opt RPAREN
    |   NEW class_type LPAREN argument_list_opt RPAREN class_body
    |   primary DOT NEW simple_name LPAREN argument_list_opt RPAREN
    |   primary DOT NEW simple_name LPAREN argument_list_opt RPAREN class_body
    |   name DOT NEW simple_name LPAREN argument_list_opt RPAREN
    |   name DOT NEW simple_name LPAREN argument_list_opt RPAREN class_body
    ;
}

class_instance_creation_expression ::=
                    // NewObjectExpr
        NEW:x objtype_or_expr:a label_opt:l LPAREN argument_list_opt:b RPAREN:y
            {:  TypeNode tn = a.toUnlabeledType();
		if (l != null)
		    tn = parser.nf.LabeledTypeNode(parser.pos(a,l), tn, l);
		RESULT = parser.nf.New(parser.pos(x,y), tn, b); :}
    ;

override array_creation_expression ::=
        NEW:n objtype_or_expr:a dims:b array_initializer:c
            {: RESULT = parser.nf.NewArray(parser.pos(n,c), a.toType(),
                                       b.intValue(), c); :}
    |   NEW:n primitive_type:a dim_exprs:b dims_opt:c
            {: RESULT = parser.nf.NewArray(parser.pos(n,b), a, b,
                                           c.intValue()); :}
    |   NEW:n primitive_type:a dims:b array_initializer:c
            {: RESULT = parser.nf.NewArray(parser.pos(n,c), a,
                                           b.intValue(), c); :}
    ;
drop { field_access ::=
	primary DOT IDENTIFIER
    |   name DOT SUPER DOT IDENTIFIER
    ;
}
extend field_access ::=
        primary_no_new_array:a DOT IDENTIFIER:b
        {: RESULT = parser.nf.Field(parser.pos(a, b), a,
                    b.getIdentifier()); :}
    ;
drop {
    method_invocation ::=
        name LPAREN argument_list_opt RPAREN
    |   primary DOT IDENTIFIER LPAREN argument_list_opt RPAREN
    |   name DOT SUPER DOT IDENTIFIER LPAREN argument_list_opt RPAREN
    ;
}
extend method_invocation ::=
                    // MethodExpr
        reftype_or_expr:a LPAREN argument_list_opt:b RPAREN:y
        {: if (! (a instanceof Name)) parser.die(parser.pos(a));
           Name n = (Name) a;
               RESULT = parser.nf.Call(parser.pos(a,y),
                       n.prefix == null ? null
					: n.prefix.toReceiver(),
                       n.name, b); :}
    |   primary_no_new_array:a DOT IDENTIFIER:b LPAREN argument_list_opt:c RPAREN:y
            {: RESULT = parser.nf.Call(parser.pos(a,y), a,
                                       b.getIdentifier(), c); :}
    ;

declassify ::=
                    // DeclassifyExpr
        DECLASSIFY:x LPAREN expression:a COMMA label:c downgrade_to_label_opt:b RPAREN:y
            {: RESULT = parser.nf.DeclassifyExpr(parser.pos(x,y), a, b==null?null:c, b==null?c:b); :}
    ;

endorse ::=
                    // DeclassifyExpr
        ENDORSE:x LPAREN expression:a COMMA label:c downgrade_to_label_opt:b RPAREN:y
            {: RESULT = parser.nf.EndorseExpr(parser.pos(x,y), a, b==null?null:c, b==null?c:b); :}
    ;

param_or_expr_list ::=
        // List of Object (Expr or Identifier or ParamNode)
        expression:a
        {: RESULT = parser.makeParamOrExprList(a); :}
    |   label:a
	    {: List l = new LinkedList();
	       l.add(a);
	       RESULT = l;
	    :}
    |   param_or_expr_list:a COMMA simple_name:b
	    {: a.add(b); RESULT = a; :}
    |   param_or_expr_list:a COMMA label:b
	    {: a.add(b); RESULT = a; :}
    |  param_or_expr_list:a COMMA accesspath_no_id:b
        {:  a.add(b); RESULT = a;  :}
    ;

/* objtype_or_expr: something that looks like the name of a class or interface
 *  but that may turn out to be an expression.
 */
objtype_or_expr ::=
        IDENTIFIER:a
            {: RESULT = new Name(parser, parser.pos(a), null,
                                 a.getIdentifier()); :}
    |   objtype_or_expr:a DOT IDENTIFIER:b
            {: RESULT = new Name(parser, parser.pos(a,b), a,
                                 b.getIdentifier()); :}
    |   objtype_or_expr:a LBRACK param_or_expr_list:b RBRACK
	    {: RESULT = parser.makeAccessOrInst(a,b); :}
    ;

/* reftype_or_expr: something that looks like a reference type (but not
 * a primitive array type) but might turn out to be an expression. May
 * include a label component.
 */
reftype_or_expr ::=
        IDENTIFIER:a
            {: RESULT = new Name(parser, parser.pos(a), null,
                                 a.getIdentifier()); :}
    |   reftype_or_expr:a DOT IDENTIFIER:b
            {: RESULT = new Name(parser, parser.pos(a,b), a,
                                 b.getIdentifier()); :}
    |   reftype_or_expr:a LBRACK param_or_expr_list:b RBRACK
            {:  RESULT = parser.makeAccessOrInst(a,b); :}
    |   reftype_or_expr:a LBRACK RBRACK:y
            {: RESULT = new Array(parser, parser.pos(a,y), a.toType()); :}
    |   reftype_or_expr:a label:b
            {: RESULT = new LabeledExpr(parser, parser.pos(a,b), a, b);
               parser.countAnnotation(parser.TYPE_ANNOTATION, parser.pos(a,b));
            :}
    |   reftype_or_expr:a CONST LBRACK param_or_expr_list:b RBRACK:y
            {: RESULT = new Array(parser, parser.pos(a,y), a.toType(), true); :}
    |   reftype_or_expr:a CONST LBRACK RBRACK:y
            {: RESULT = new Array(parser, parser.pos(a,y), a.toType(), true); :}
    ;

drop {
    array_access ::=
        name LBRACK expression RBRACK
    |   primary_no_new_array LBRACK expression RBRACK
    ;
}
extend array_access ::=
                    // ArrayAccess
        primary_no_array:a dim_exprs:b
            {: Expr x = a;
               for (Iterator i = b.iterator(); i.hasNext(); ) {
                    Expr e = (Expr) i.next();
                    x = parser.nf.ArrayAccess(parser.pos(a,b), x, e);
               }
               RESULT = (ArrayAccess) x;
	    :}
    ;
drop { postfix_expression ::= name; }
extend postfix_expression ::=
	reftype_or_expr:a
            {: RESULT = a.wrap(); :}
    ;
drop {
    cast_expression ::=
        LPAREN primitive_type dims_opt RPAREN unary_expression
    |   LPAREN name dims RPAREN unary_expression_not_plus_minus
    ;
}
extend cast_expression ::=
                    // Cast
        LPAREN:x labeled_primitive_type:a dims_opt:b RPAREN unary_expression:c
            {: RESULT = parser.nf.Cast(parser.pos(x,c),
                                   parser.array(a, b.intValue()), c); :}
    ;

drop { left_hand_side ::= name; }
extend left_hand_side ::=
                    // Expr
        reftype_or_expr:a
            {: RESULT = a.wrap(); :}
    ;
