Create "certified term" type

[atomb]

Currently, it's possible to construct SharedTerm objects in SAWScript that are not well-typed. They can be checked after the fact, but this can be expensive for large terms. Better would be to have an abstract type for terms that are guaranteed to be well-typed, along with functions to combine them with the minimum additional checking to ensure that the result is well-typed.

[brianhuffman]

Based on some discussions with @eddywestbrook, here is what I have in mind for how to implement certified terms in saw-core:

• Rename the existing Term datatype to something else, like RawTerm. A RawTerm is not guaranteed to be type-correct.
• Create a new abstract Term type for certified terms, which are guaranteed to be well-formed and type-correct.
• The Verifier.SAW.SharedTerm module should export mostly the same operations with the same type signatures that they have now, except that they will work on the new Term type.

Here's how I would implement the new Term type: It will be a single-constructor datatype with the following fields:

• A pointer to the context of the term. (This could be IORef SharedContext, or just IORef Module, or something else.) It at least needs to be comparable for equality, and it must point to all the context needed for type checking.
• The body of the term, represented as a RawTerm.
• The type of the term, represented as a RawTerm.

Functions that combine Terms to create new ones should make the following assertions:

• All input terms should point to the same typing context.
• The types of the input terms must be compatible with each other (e.g. for function application, the types must be of the form a -> b and a).

There are a couple of ways we could handle making lambda expressions and de Bruijn variables:

1. Certified terms would be required to be closed terms. Making lambda abstractions would require us to generate fresh global variables with scFreshGlobal and then abstract over them with e.g. scAbstractExts.
2. Certified terms could also include open terms. The implementation of type Term would need another field for the de Bruijn typing context. Term-combining operations would then have to check compatibility of the de Bruijn typing contexts for each input term.