Add annotations to rewrite rules and simpsets

[robdockins]

This allows users to add metadata their rewrite rules,
and have rewriting steps record and return the metadata
for rules what were actually used in rewriting.

The intention is to use these annotations to link rewrite rules
back to theorems/axioms that generated them so proof steps
can determine the dependencies of a proof.

[robdockins]

I'll plan to meld this into the corresponding saw-script PR GaloisInc/saw-script#1216.

[brianhuffman]

Ah, I was wondering what application this feature was meant to support. If it's for proof summaries, that makes a lot of sense.

[brianhuffman]

This looks like a good design to me. I imagine that the planned usage of this in saw-script always instantiates parameter a with the same type, but it's conceivable that someone might like to use different types here? Maybe a Functor instance for RewriteRule or Simpset would be a useful addition?

[robdockins]

Indeed, the plan is to instantiate with a particular type. But Functor, Foldable and Traversable are probably all potentially useful. Looks like we'll need the corresponding instances for Net as well.

[robdockins]

These changes have been incorporated into the SAWScript PR mentioned above.