Use numbers instead of primes to distinguish shadowed names in prettyprinted saw-core

[brianhuffman]

Currently, the saw-core prettyprinter adds primes (') to bound variable names during printing to avoid name shadowing when it encounters a bound name that was already bound in an outer scope. In some terms this can get really out of hand: For example, I'm looking at some saw-core terms coming from heapster, and when printed they contain names like z''''''''''''''''''''''''''''' and z''''''''''''''''''''''''''''''. Are those the same name, or not? I don't know!

Instead of adding primes, we should switch to appending numbers. So instead of x, x', x'', x''' we would do x, x1, x2, x3. There's already code for doing this kind of unique name variant generation in the saw-core-coq package, which we could copy.

saw-script/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs

Lines 481 to 488 in 87ab2f3

	nextVariant :: Coq.Ident -> Coq.Ident
	nextVariant = reverse . go . reverse
	where
	go :: String -> String
	go (c : cs)
	| c == '9' = '0' : go cs
	| isDigit c = succ c : cs
	go cs = '1' : cs