Streamline large theory graph definitions

[florian-rabe]

I've looked at the lattice formalization @kohlhase and @Jazzpirate did recently.

I noticed it doesn't look as nice as it should. I think my main concern is that there is way too much boilerplate.

I'm not entirely sure what the problem is - the theory-method, the MMT implementation, the convention with nested theories, or something else. I would like to use this case study to understand what is needed to allow such formalizations to be much more concise.

Do you have any suggestions already?

Here are some first ideas I had:

• document-wide meta-theory
• document-wide includes
• dedicated syntax for internal and external theories
  • automated generation of the needed includes in the external theory
  • no more ad hoc nested theories and "_theory" suffixes
• notations for external counterparts attached to declarations in the internal theory

[Jazzpirate]

• document-wide meta-theory: seconded!
• document-wide includes: sort-of is in conflict with us wanting includes to be minimal. E.g. we only want to include ?Strings if we actually need them in a theory. It's rarely the case that some theory is included everywhere. Maybe subsumed once we have theory graph optimizations.
• dedicated syntax for internal and external theories
  • automated generation of the needed includes in the external theory: <- this is somewhat subsumed by having a "use" operator. A (currently) internal theory would e.g. use (let's say) NaturalNumbers or NaturalDeduction, but not include them (making them part of the resulting Mod-record type).
• notations for external counterparts attached to declarations in the internal theory. <- In principle already doable, except that Mod would then become a derived declaration (to be able to generate the corresponding destructors etc.)

[kohlhase]

I noticed it doesn't look as nice as it should. I think my main concern is that there is way too much boilerplate.

I completely agree. I think the main culprit is the internal/external structure. I suspect that a couple of structural features could help here. Something like

theotype foo // theory + record type definition
   include ?bar // ?bar must be another theotype
   internal <the stuff to add to the internal theory>
   external <the stuff to add to the external theory>
|||

which would elaborate to

theory foo : <meta>
   include ?bar
   theory foo_theory : <meta>
      include ?bar_theory 
      <the stuff to add to the internal theory>
    ||| 
   foo = Mod foo_theory | role = application
   <the stuff to add to the external theory>
|||

[kohlhase]

I think that such a thing (and I am sure that there is more boilerplate we can include into this) would help structure things quite a lot. We might add the usual "accessor methods" for the main structural constants of the internal theory.