public final AntlrPilarParser.expExtension_return expExtension()
      throws RecognitionException {
    AntlrPilarParser.expExtension_return retval = new AntlrPilarParser.expExtension_return();
    retval.start = input.LT(1);
    int expExtension_StartIndex = input.index();
    Object root_0 = null;

    Token t = null;
    Token ID185 = null;
    Token char_literal186 = null;
    Token char_literal188 = null;
    Token char_literal190 = null;
    AntlrPilarParser.typeVarTuple_return typeVarTuple183 = null;

    AntlrPilarParser.type_return type184 = null;

    AntlrPilarParser.extParamList_return extParamList187 = null;

    AntlrPilarParser.annotationList_return annotationList189 = null;

    Object t_tree = null;
    Object ID185_tree = null;
    Object char_literal186_tree = null;
    Object char_literal188_tree = null;
    Object char_literal190_tree = null;
    RewriteRuleTokenStream stream_170 = new RewriteRuleTokenStream(adaptor,
        "token 170");
    RewriteRuleTokenStream stream_175 = new RewriteRuleTokenStream(adaptor,
        "token 175");
    RewriteRuleTokenStream stream_ID = new RewriteRuleTokenStream(adaptor,
        "token ID");
    RewriteRuleTokenStream stream_169 = new RewriteRuleTokenStream(adaptor,
        "token 169");
    RewriteRuleTokenStream stream_191 = new RewriteRuleTokenStream(adaptor,
        "token 191");
    RewriteRuleSubtreeStream stream_annotationList = new RewriteRuleSubtreeStream(
        adaptor, "rule annotationList");
    RewriteRuleSubtreeStream stream_extParamList = new RewriteRuleSubtreeStream(
        adaptor, "rule extParamList");
    RewriteRuleSubtreeStream stream_typeVarTuple = new RewriteRuleSubtreeStream(
        adaptor, "rule typeVarTuple");
    RewriteRuleSubtreeStream stream_type = new RewriteRuleSubtreeStream(
        adaptor, "rule type");
    try {
      if (state.backtracking > 0 && alreadyParsedRule(input, 49)) {
        return retval;
      }
      // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:417:2: (t= 'expdef' ( typeVarTuple )? ( type )? ID ( '(' extParamList ')' )? annotationList ';' -> ^( EXP_EXT[$t] ^( OPTION ( typeVarTuple )? ) ^( OPTION ( type )? ) ID ^( OPTION ( extParamList )? ) annotationList ) )
      // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:417:4: t= 'expdef' ( typeVarTuple )? ( type )? ID ( '(' extParamList ')' )? annotationList ';'
      {
        t = (Token) match(input, 191, FOLLOW_191_in_expExtension3515);
        if (state.failed) return retval;
        if (state.backtracking == 0) stream_191.add(t);

        // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:417:15: ( typeVarTuple )?
        int alt52 = 2;
        int LA52_0 = input.LA(1);

        if ((LA52_0 == 167)) {
          alt52 = 1;
        }
        switch (alt52) {
          case 1:
          // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:0:0: typeVarTuple
          {
            pushFollow(FOLLOW_typeVarTuple_in_expExtension3517);
            typeVarTuple183 = typeVarTuple();

            state._fsp--;
            if (state.failed) return retval;
            if (state.backtracking == 0)
              stream_typeVarTuple.add(typeVarTuple183.getTree());

          }
            break;

        }

        // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:417:29: ( type )?
        int alt53 = 2;
        int LA53_0 = input.LA(1);

        if ((LA53_0 == TYPEVARID || LA53_0 == 169 || LA53_0 == 177)) {
          alt53 = 1;
        } else if ((LA53_0 == ID)) {
          int LA53_2 = input.LA(2);

          if ((LA53_2 == ID || LA53_2 == 167 || LA53_2 == 177 || LA53_2 == 202
              || (LA53_2 >= 215 && LA53_2 <= 216) || LA53_2 == 225)) {
            alt53 = 1;
          }
        }
        switch (alt53) {
          case 1:
          // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:0:0: type
          {
            pushFollow(FOLLOW_type_in_expExtension3520);
            type184 = type();

            state._fsp--;
            if (state.failed) return retval;
            if (state.backtracking == 0) stream_type.add(type184.getTree());

          }
            break;

        }

        ID185 = (Token) match(input, ID, FOLLOW_ID_in_expExtension3523);
        if (state.failed) return retval;
        if (state.backtracking == 0) stream_ID.add(ID185);

        // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:418:4: ( '(' extParamList ')' )?
        int alt54 = 2;
        int LA54_0 = input.LA(1);

        if ((LA54_0 == 169)) {
          alt54 = 1;
        }
        switch (alt54) {
          case 1:
          // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:418:6: '(' extParamList ')'
          {
            char_literal186 = (Token) match(
                input,
                169,
                FOLLOW_169_in_expExtension3531);
            if (state.failed) return retval;
            if (state.backtracking == 0) stream_169.add(char_literal186);

            pushFollow(FOLLOW_extParamList_in_expExtension3533);
            extParamList187 = extParamList();

            state._fsp--;
            if (state.failed) return retval;
            if (state.backtracking == 0)
              stream_extParamList.add(extParamList187.getTree());
            char_literal188 = (Token) match(
                input,
                170,
                FOLLOW_170_in_expExtension3535);
            if (state.failed) return retval;
            if (state.backtracking == 0) stream_170.add(char_literal188);

          }
            break;

        }

        pushFollow(FOLLOW_annotationList_in_expExtension3543);
        annotationList189 = annotationList();

        state._fsp--;
        if (state.failed) return retval;
        if (state.backtracking == 0)
          stream_annotationList.add(annotationList189.getTree());
        char_literal190 = (Token) match(
            input,
            175,
            FOLLOW_175_in_expExtension3545);
        if (state.failed) return retval;
        if (state.backtracking == 0) stream_175.add(char_literal190);

        // AST REWRITE
        // elements: extParamList, annotationList, ID, type, typeVarTuple
        // token labels: 
        // rule labels: retval
        // token list labels: 
        // rule list labels: 
        // wildcard labels: 
        if (state.backtracking == 0) {
          retval.tree = root_0;
          RewriteRuleSubtreeStream stream_retval = new RewriteRuleSubtreeStream(
              adaptor, "rule retval", retval != null ? retval.tree : null);

          root_0 = (Object) adaptor.nil();
          // 419:41: -> ^( EXP_EXT[$t] ^( OPTION ( typeVarTuple )? ) ^( OPTION ( type )? ) ID ^( OPTION ( extParamList )? ) annotationList )
          {
            // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:419:44: ^( EXP_EXT[$t] ^( OPTION ( typeVarTuple )? ) ^( OPTION ( type )? ) ID ^( OPTION ( extParamList )? ) annotationList )
            {
              Object root_1 = (Object) adaptor.nil();
              root_1 = (Object) adaptor.becomeRoot(
                  (Object) adaptor.create(EXP_EXT, t),
                  root_1);

              // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:419:58: ^( OPTION ( typeVarTuple )? )
              {
                Object root_2 = (Object) adaptor.nil();
                root_2 = (Object) adaptor.becomeRoot(
                    (Object) adaptor.create(OPTION, "OPTION"),
                    root_2);

                // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:419:67: ( typeVarTuple )?
                if (stream_typeVarTuple.hasNext()) {
                  adaptor.addChild(root_2, stream_typeVarTuple.nextTree());

                }
                stream_typeVarTuple.reset();

                adaptor.addChild(root_1, root_2);
              }
              // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:419:82: ^( OPTION ( type )? )
              {
                Object root_2 = (Object) adaptor.nil();
                root_2 = (Object) adaptor.becomeRoot(
                    (Object) adaptor.create(OPTION, "OPTION"),
                    root_2);

                // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:419:91: ( type )?
                if (stream_type.hasNext()) {
                  adaptor.addChild(root_2, stream_type.nextTree());

                }
                stream_type.reset();

                adaptor.addChild(root_1, root_2);
              }
              adaptor.addChild(root_1, stream_ID.nextNode());
              // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:419:101: ^( OPTION ( extParamList )? )
              {
                Object root_2 = (Object) adaptor.nil();
                root_2 = (Object) adaptor.becomeRoot(
                    (Object) adaptor.create(OPTION, "OPTION"),
                    root_2);

                // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:419:110: ( extParamList )?
                if (stream_extParamList.hasNext()) {
                  adaptor.addChild(root_2, stream_extParamList.nextTree());

                }
                stream_extParamList.reset();

                adaptor.addChild(root_1, root_2);
              }
              adaptor.addChild(root_1, stream_annotationList.nextTree());

              adaptor.addChild(root_0, root_1);
            }

          }

          retval.tree = root_0;
        }
      }

      retval.stop = input.LT(-1);

      if (state.backtracking == 0) {

        retval.tree = (Object) adaptor.rulePostProcessing(root_0);
        adaptor.setTokenBoundaries(retval.tree, retval.start, retval.stop);
      }
    } catch (RecognitionException re) {
      reportError(re);
      recover(input, re);
      retval.tree = (Object) adaptor.errorNode(
          input,
          retval.start,
          input.LT(-1),
          re);

    } finally {
      if (state.backtracking > 0) {
        memoize(input, 49, expExtension_StartIndex);
      }
    }
    return retval;
  }