Short names are not always used for pretty-printing terms

[brianhuffman]

PR GaloisInc/saw-core#126 implemented a namespace-aware prettyprinter for saw-core, which uses the shortest unambiguous form of names, so we don't have to see fully-qualified names everywhere.

The print_goal proof command uses the namespace-aware prettyprinter, as does the print_term command.

sawscript> prove do { print_goal; assume_unsat; } {{ \(x:Bit) -> ~ x }}
[23:56:52.297] Goal prove (goal number 0):
[23:56:52.298] (x : Bool)
-> EqTrue (ecCompl Bool PLogicBit x)
[23:56:52.298] WARNING: assuming goal prove is unsat
[23:56:52.298] Valid
sawscript> print_term {{ \(x:Bit) -> ~ x }}
[23:57:02.808] \(x : Bool) -> ecCompl Bool PLogicBit x

However, if a term is just written directly on the REPL, it is printed with all qualified names:

sawscript> {{ \(x:Bit) -> ~ x }}
[23:57:09.145] \(x : Prelude.Bool) ->
  Cryptol.ecCompl Prelude.Bool Cryptol.PLogicBit x

We should always be using the namespace-aware prettyprinter.

[brianhuffman]

The print_term function is implemented using scShowTerm, which runs in the IO monad and uses a SharedContext to obtain naming information. https://github.com/GaloisInc/saw-script/blob/7b8c134a1a2fad07620af1f17b246d3012744e80/src/SAWScript/Builtins.hs#L397-L404

However, when a value is written by itself on the REPL, it is printed by function processStmtBind, which calls showsPrecValue on the computed value. https://github.com/GaloisInc/saw-script/blob/7b8c134a1a2fad07620af1f17b246d3012744e80/src/SAWScript/Interpreter.hs#L316-L320

To fix the problem, we'll have to replace or modify showsPrecValue so that it takes a SharedContext argument and can run in the IO monad.

[brianhuffman]

We might just try removing the Show instance for the saw-script Value type and see what breaks.

[brianhuffman]

See also #1608.

[robdockins]

Some progress has been made on this in #1689

[sauclovian-g]

And see #747. Arguably, this is a duplicate...