ProofJavaParser.PrimaryPrefixReturnValue (KeY API Documentation)

java.lang.Object
- de.uka.ilkd.key.parser.proofjava.ProofJavaParser.PrimaryPrefixReturnValue

Enclosing class:

ProofJavaParser
```
static class ProofJavaParser.PrimaryPrefixReturnValue
extends java.lang.Object
```
inner class that is only used to return results from primary prefix syntax rule

Author:

RN

Field Summary

Fields
Modifier and Type	Field and Description
`(package private) static int`	`ADT_CONSTRUCT` production was something like "&93;seq_reverse(" Expression ")".
`(package private) static int`	`ALLOCATION_EXPR` production was AllocationExpression
`(package private) static int`	`CLASS_REF` production was ResultType "."
`(package private) Expression`	`expr` valid iff `type` is `PARENTHESED_EXPR` or `ALLOCATION_EXPR`
`(package private) Literal`	`literal` valid iff `type` is `LITERAL`
`(package private) static int`	`LITERAL` production was Literal
`(package private) UncollatedReferenceQualifier`	`name` valid iff `type` is `QUALIFIED_NAME` or `SUPER_MEMBER`
`(package private) static int`	`PARENTHESIZED_EXPR` production was "(" Expression ")"
`(package private) static int`	`PASSIVE_EXPR` production was "@(" Expression ")"
`(package private) static int`	`QUALIFIED_NAME` production was Name
`(package private) static int`	`SUPER_MEMBER` production was "super" "."
`(package private) static int`	`THIS` production was "this"
`(package private) int`	`type` indicates the type of the result
`(package private) TypeReference`	`typeref` valid iff `type` is `CLASS_REF`
`(package private) static int`	`UNDEFINED` indicates that the result is currently undefined

Constructor Summary

Constructors
Constructor and Description

PrimaryPrefixReturnValue()

Constructors
Constructor and Description
`PrimaryPrefixReturnValue()`

Method Summary
- Methods inherited from class java.lang.Object
  clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- Field Detail
  - UNDEFINED
```
static final int UNDEFINED
```
    indicates that the result is currently undefined
    
    See Also:
    
    Constant Field Values
  - LITERAL
```
static final int LITERAL
```
    production was
```
Literal
```
    See Also:
    
    Constant Field Values
  - THIS
```
static final int THIS
```
    production was
```
"this"
```
    See Also:
    
    Constant Field Values
  - SUPER_MEMBER
```
static final int SUPER_MEMBER
```
    production was
```
"super" "." 
```
    See Also:
    
    Constant Field Values
  - PARENTHESIZED_EXPR
```
static final int PARENTHESIZED_EXPR
```
    production was
```
"(" Expression ")"
```
    See Also:
    
    Constant Field Values
  - ALLOCATION_EXPR
```
static final int ALLOCATION_EXPR
```
    production was
```
AllocationExpression
```
    See Also:
    
    Constant Field Values
  - CLASS_REF
```
static final int CLASS_REF
```
    production was
```
ResultType "." "class"
```
    See Also:
    
    Constant Field Values
  - QUALIFIED_NAME
```
static final int QUALIFIED_NAME
```
    production was
```
Name
```
    See Also:
    
    Constant Field Values
  - PASSIVE_EXPR
```
static final int PASSIVE_EXPR
```
    production was
```
"@(" Expression ")"
```
    See Also:
    
    Constant Field Values
  - ADT_CONSTRUCT
```
static final int ADT_CONSTRUCT
```
    production was something like
```
"&93;seq_reverse(" Expression ")"
```
    . Extension to Java/JML with ADTs.
    Since:
    
    1.7.2118
    
    See Also:
    
    Constant Field Values
  - type
```
int type
```
    indicates the type of the result
  - literal
```
Literal literal
```
    valid iff type is LITERAL
  - expr
```
Expression expr
```
    valid iff type is PARENTHESED_EXPR or ALLOCATION_EXPR
  - typeref
```
TypeReference typeref
```
    valid iff type is CLASS_REF
  - name
```
UncollatedReferenceQualifier name
```
    valid iff type is QUALIFIED_NAME or SUPER_MEMBER
- Constructor Detail
  - PrimaryPrefixReturnValue
```
PrimaryPrefixReturnValue()
```

Class ProofJavaParser.PrimaryPrefixReturnValue

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

UNDEFINED

LITERAL

THIS

SUPER_MEMBER

PARENTHESIZED_EXPR

ALLOCATION_EXPR

CLASS_REF

QUALIFIED_NAME

PASSIVE_EXPR

ADT_CONSTRUCT

type

literal

expr

typeref

name

Constructor Detail

PrimaryPrefixReturnValue