public static Symbol generateOperator(Proposition self) {
    { GeneralizedSymbol operator = self.operator;

      if (operator == null) {
        return (Logic.SYM_STELLA_NULL);
      }
      { Surrogate testValue000 = Stella_Object.safePrimaryType(operator);

        if (Surrogate.subtypeOfSurrogateP(testValue000)) {
          { Surrogate operator000 = ((Surrogate)(operator));

            { NamedDescription description = Logic.getDescription(operator000);
              Symbol symbol = Symbol.internSymbolInModule(operator000.symbolName, ((Module)(operator000.homeContext)), false);

              if (description != null) {
                return (Logic.internalStellaOperatorToKif(symbol));
              }
              else {
                return (symbol);
              }
            }
          }
        }
        else if (Surrogate.subtypeOfSymbolP(testValue000)) {
          { Symbol operator000 = ((Symbol)(operator));

            return (operator000);
          }
        }
        else {
          { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

            stream000.nativeStream.print("`" + testValue000 + "' is not a valid case option");
            throw ((StellaException)(StellaException.newStellaException(stream000.theStringReader()).fillInStackTrace()));
          }
        }
      }
    }
  }