Java error when calling an auxiliary from an axiom

[joeseibel]

If an axiom calls an auxiliary, then the generated Java code will have a compile error. Consider the following Xsemantics snippet:

auxiliary {
    exampleAuxiliary(Object obj): Object
}

judgments {
    exampleJudgement ||- Object obj : output Object
}

auxiliary exampleAuxiliary(Object obj) {
    obj
}

axiom ExampleAxiom
    G ||- Object obj : exampleAuxiliary(obj)

This produces the following Java method for the axiom:

private Object _applyRuleExampleAxiom_1(final RuleEnvironment G, final Object obj) throws RuleFailedException {
  Object _exampleAuxiliary = this.exampleAuxiliaryInternal(_trace_, obj);
  return _exampleAuxiliary;
}

The generated Java has the error: _trace_ cannot be resolved to a variable.

The problem is that _trace_ is not defined for methods generated from axioms, yet the auxiliary method expects a RuleApplicationTrace to be passed to it. If it doesn't make sense to call an auxiliary from an axiom, then there should be a validation error on the Xsemantics file. If it does make sense, then _trace_ should also be generated for axiom methods.

[LorenzoBettini]

Thanks for the report! I guess that generated code for axioms should have a trace parameter, like rules. I think I had never considered this use case. I'll try to fix this ASAP