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.

saw-script/src/SAWScript/Builtins.hs

Lines 397 to 404 in 7b8c134

	show_term :: Term -> TopLevel String
	show_term t =
	do opts <- getTopLevelPPOpts
	sc <- getSharedContext
	liftIO $ scShowTerm sc opts t
	print_term :: Term -> TopLevel ()
	print_term t = printOutLnTop Info =<< show_term t

However, when a value is written by itself on the REPL, it is printed by function processStmtBind, which calls showsPrecValue on the computed value.

saw-script/src/SAWScript/Interpreter.hs

Lines 316 to 320 in 7b8c134

	-- Print non-unit result if it was not bound to a variable
	case pat of
	SS.PWild _ | printBinds && not (isVUnit result) ->
	printOutLnTop Info (showsPrecValue opts 0 result "")
	_ -> return ()

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...