Add option for strings to appear in structured judgments

[joshcbrown]

This is a WIP so will add more detail later, but the gist is that we want to allow string terms to appear in the structured part of their judgments to allow for e.g. carrying through identifiers into a built up parse tree:

Have implemented this by parameterising SExp over a Symbol module, which in the case of bare S-expressions is just a thin wrapper around string, and in the case of string term judgments is a wrapper around string | StringTerm.t.

[joshcbrown]

Still not at a point where this is quite ready to be merged yet, but enough to report in a bit more detail, and to see whether this direction is worth pursuing further.
So as I said above, the main idea is parameterising SExp over a module Symbol which implements capabilities for:

• Parsing
• Unification
• Substitution

So, in effect, most of the things that a regular Term needs. Other capabilities are mainly required to interface between SExp-y things and Symbol-y things, like translating an SExp.Schematic to Symbol.schematic so that unification works as one would expect.

There are a few immediately exciting effects of this change:

• There's no need for the specialised string term judgments with one unstructured string part and one structured SExp part. Now, the SExp module instantiated with a symbol type that can be a regular symbol or a string symbol is much more powerful, and also can represent both a term and a judgment, eliminating the need for this extra judgment module. Indeed, if we don't think any term in the future will need to be representationally different than its corresponding judgment, we can rid ourselves entirely of the somewhat bloated JUDGMENT signature and accompanying TermAsJudgment.Make functor.
• Speaking of the relative power of the new functorised module, below is an example showing how we can prove theorems involving string arithmetic which would not have been possible previously.

• The above uses a hacky rule to parse "3" into (S (S (S Z))), but we could in theory use a symbol type which has direct support for integers or naturals so that this parsing could be done automagically on the level of implementation of symbols. What I envision is having a module functor in the style of CombineMethodView which takes in two symbols and combines them in much the same way that StringSymbol is currently doing manually (though, there is some special casing there right now which we might need to account for in a more fleshed out solution). My point is, these symbol types should be able to compose arbitrarily provided some invariants.
• As far as I can see (which isn't very far, to be fair), there's nothing particularly stopping us from applying this same parameterisation over symbols to HOTerms, too. Whether that's worthwhile doing is a conversation worth having. I'm not sure whether there'd be theorems you could express with HOTerms you both a) cannot express in the equivalent SExp and b) would want to prove in an introductory PL course.

[liamoc]

Minor changes to substDeBruijn interface

Substitution must now potentially throw an exception (which is part of the signature).

this means unification will discard solutions that lead to throwing substitutions.
proof method apply() will fail for throwing substitutions
when substitution is applied to the entire proof after a method is selected, if substitution fails THEN (unlikely but possible), an error must be reported to the user.