Typeclass system to make saw-core more readable

[m-yac]

If I understand my SAW history correctly, the saw-core language was originally intended as a purely intermediary language, only meant to be read by machines and devs. However, with all the recent development on rewriting proofs, saw-core is increasingly becoming a user-facing language. One major difficulty users have with the language is just how verbose it is – in particular, all the scaffolding of the typeclass system of Cryptol becomes explicit in saw-core, resulting in lots of terms starting with "P" (e.g. PSignedCmpSeq) cluttering up saw-core terms and making them harder to understand.

One way we could address this is to add a typeclass system to saw-core, and translate all the various Cryptol typeclasses into saw-core typeclasses. This would make the saw-core terms which are generated from Cryptol smaller, and therefore hopefully easier for users to read and work with.

Relevant to #1844, this change would also enable us to remove the ad-hoc isort and qsort syntax without compromising any of the brevity of the existing saw-core Prelude functions – instead, we would simply add Inhabited and QuantType typeclasses.

There is a larger discussion to be had about what other steps we might want to take to make saw-core a easier for humans to use, but this would be a good first step.

[sauclovian-g]

This is part of a broader question of which type system frobs saw-core should have; for example, one way to retire #2119 is to add record types to saw-core, but we haven't done that sort of thing in the past because we also want saw-core to remain simple.

The consensus of the issue backlog seems to be that the mapping from Cryptol types to saw-core types needs to be injective (currently it isn't), and adding type system features to saw-core is one of the ways to get there. However, a different and also possibly feasible approach is to carry around enough information to lift terms back out of saw-core when they need to be user-facing. More thought is needed...