Trivial migrations in the frontend and core

[kris-brown]

This PR partially addresses #375 for the special case of literal inclusions (rather than monomorphisms) generally. There are two (noninteracting) components: in the core, there is a method which swaps the theory pointer for a model. In the frontend, there is an attribute inclusions for each Theory which is a list of string ids for which one is licensed to change the theory to (even if formal content has been added). These are hardcoded in theories.tsx.

A future PR will add to this hardcoded data to allow special privileged monomorphisms (for example: the names change from Olog to Schema so we cannot handle this trivial migration yet).

Right now, the theory "group" (e.g. "Knowledge and Data") is still present even if there are no available theories within that group. Unsure if that is a problem.

Changing the theory is in general an irreversible and mutating operation. Some sugar could be added in the future to combine the theory change with a duplication of the model.

[github-actions]

Preview url: https://67a56f2a91be49c6fe5aa64d--catcolab.netlify.app

[epatters]

Thanks Kris! I was going to make a few line-level comments, but then I realized there is a design issue that we haven't fully discussed but I think should be addressed before proceeding further.

Currently, the situation is that you can't push forward models except in the most trivial case, namely from the initial theory to another theory. However, provided you don't have any formal cells in the notebook, you're free to keep the changing the theory, even after choosing a non-initial theory. A mathematical gloss on this intuitively correct behavior is that as long as you have no formal content, starting from any theory, you can pull back to the initial theory then pushforward to any other theory without loss of data.

With this PR, once you change to a theory, you can never undo that. You can only keep changing to bigger theories. As you say in your description, "changing the theory is in general an irreversible and mutating operation." This is quite punishing to the user: if they make a wrong click, they can never get back to the previous state. The aim, I think, should be make these migrations as fluid as possible.

I can imagine some possible strategies to address this problem and I'm sure you can too. Let's discuss more in person.

[kris-brown]

This PR does recover the old behavior (as long as there are only informal cells, then you can switch between any theories reversibly). It's only when you have formal content that changing theory is irreversible. Still, I agree that if one is only using formal cells from a simpler theory that it should be possible to move from more complex to the simpler theory, so happy to talk about ways of doing that!

[epatters]

Oh good, I missed that. Thanks for clarifying. But yes, still worth talking more.

[KevinDCarlson]

I suppose we should just ask for both deltas and sigmas along inclusions, yes? That’ll make the menu design a bit trickier as you need both ancestors and descendants available