Use proper names for datatypes, constructors, and recursors in saw-core term AST

[brianhuffman]

The saw-core AST currently uses the NameInfo type to represent structured names for defined constants, primitives, and free variables (ExtCns). These are registered in a SAWNamingEnv, which can be used to determine the shortest unambiguous version of each NameInfo during pretty printing.

However, the names of datatypes (DataTypeApp), data constructors (CtorApp), and recursors (RecursorApp) are represented with only an Ident instead of a full NameInfo. Among other problems, this means that pretty printing of these names cannot use the shortest unambiguous version; they have to be printed always with a fully qualified name.

We should change the representation of these term AST constructors so that each name comes with a NameInfo and a unique VarIndex. To this end, it might be useful to introduce a new type (probably called just Name) in Verifier/SAW/Name.hs that pairs a NameInfo with a VarIndex; then we can replace Ident with Name in all those places.

[robdockins]

This impacts some stuff I'm working on, so I'll take this on.

[brianhuffman]

Commit 02f2be2, which replaced the GlobalDef constructor (which used Ident) with Primitive (which uses ExtCns), will probably be relevant. This was part of the PR GaloisInc/saw-core#163.

[robdockins]

An annoying aspect of this is that the Nat datatype is deeply built-in. A variety of internal operations (conversions and matchers and such) want to recognize that datatype and its constructors in a context where the SharedContext and its naming environment aren't available.

[robdockins]

I believe this is fixed via #1310