MMT seem to not recognize structural features

[ColinRothgang]

MMT seems to ignore the defined structural features during parsing despite the existence of a corresponding StructuralFeatureRule, included in the theory containing an example declaration using the structural feature. Concretely, "inductive" is not recognized as a keyword in MMT/examples/source/inductive.mmt, even though it is justified by the InductiveFeatureRule in lf/Induction/InductiveTypes.scala.

Both files can be found in the devel branches on github.

[florian-rabe]

We'll have to debug this together next week.

[Jazzpirate]

First guess: The correpsonding feature has to be added to the controller as an extension. Does that happen?

[Jazzpirate]

To more more precise: A structural feature is an extension, which is "legitimized" in content via a structuralfeature rule. But the rule itself does nothing but tell the parser/typechecker to consider the structural feature. If the feature itself has not been added to the controller, then MMT doesn't know about it, even if the class exists in the class path and the rule is parsed correctly; hence (possibly) no errors are thrown.

[florian-rabe]

That's probably it.

@ColinRothgang Try adding the extension in the msl file.

@Jazzpirate The current design is awkward. I've added a Class argument to StructuralFeatureRule so that we can automatically add the extension when the rule is encountered. But I'm not sure where in the code that should happen. Suggestions?

[Jazzpirate]

We had discussed that before; it would violate the principle that content shouldn't change the controller state (paraphrasing for a lack of memory accuracy :D ). In the case of a rule probably in the structure checker or structure simplifier?

[florian-rabe]

Rules shouldn't be stateful because they are content. But the controller may change its state when encountering a rule.

Note that StructuralFeatureRules could be loaded from .omdoc, in which case they are never checked.

[Jazzpirate]

but the structure simplifier is always called, right?

[florian-rabe]

Actually, structural features can be registered just like rules. I had forgotten I implemented that already.

[Jazzpirate]

Reopened, because e.g. rule generators are not structural features, and I don't want this to be swept under the rug again

[florian-rabe]

Yes, this only works for structural features so far.

Rule generators have so far been covered by the 'semantics' config entry. We should discuss whether that feature should be removed in favor of declaring extensions in theories instead.