Deprecate adjoin_to_theory

[xrchz]

Adjoin to theory is a pain when trying to better modularise HOL4 theories and libraries, and isn't really a necessity: better practice is to put the code in a library and expect that library to be loaded alongside the theory as a matter of convention.

See further discussion in #381 to which this issue can be considered a prerequisite.

This issue is to remove adjoin_to_theory by deleting the API entry and revising the small number of uses in the repository to a cleaner convention.

[xrchz]

@mn200 How would you suggest to remove the use of adjoin_to_theory and adjoin_after_completion in Parse.sml specficially Parse.setup_grammars?

[mn200]

Good question. This facility is used to give every theory a binding of val <thyname>_grammars in the signature and structure file so that it's easy to refer to the value of the grammars belonging to the given theory. These values are available through API calls so it's a "nice to have" rather than a "must have".

If you do

grep -r --include="*.sml" --exclude='*Theory.sml' _grammars *

from the head of the HOL repo you'll see that that it's used quite a lot.

In the short term, I'd let the parser be privileged and leave its uses of the calls.

[xrchz]

What's the long term solution? Use the Parse APIs where these bindings were used? I'd rather jump straight to that (or something else that allows me to remove adjoin_to_theory API entirely).

[mn200]

I think that's right. The call to use is grammarDB {thyname="foo"}

[xrchz]

OK the adjoin branch currently builds up to big use of adjoin_to_theory in pairScript.sml -- I think the plan for that one is to move it to pairLib.sml and make sure that's open whenever it's needed?

EDIT: I have gone ahead in this way and it seems to work.

[xrchz]

OK so now the problem is src/ring/src/abstraction.sml -- would love any pointers/suggestions on how to get rid of that one. @mn200 looks like you're the git blame for it so might remember what it's about.

[xrchz]

What are we doing with EmitML here? Should we also get rid of it?

[mn200]

I haven't looked at what it's trying to do yet. If possible, I think it might be nice to keep it.