Terms can be difficult to read

[bboston7]

print_term often emits something that's closer to machine readable than human readable. It might be helpful for debugging and learning to have a term pretty printer that makes it easier to understand what a term does at first glance, even if it comes at the cost of some information. For example, perhaps

\(x : Prelude.Vec 8 Prelude.Bool) ->
  Prelude.bvAdd 8 (Prelude.bvMul 8 x (Prelude.bvNat 8 2))
    (Prelude.bvNat 8 1)

Could be pretty printed as (keeping with the non-inline operators)

\(x : [8]) -> (+ (* x 2) 1)

This omits that the multiplication and addition operators are over 8 bit numbers, but I think it's clear from the type annotation on x anyway.

[brianhuffman]

One thing we could do to improve readability without losing any information would be to finally implement GaloisInc/saw-core#17, which would give us something like this:

\(x : Vec 8 Bool) ->
  bvAdd 8 (bvMul 8 x (bvNat 8 2)) (bvNat 8 1)

As for omitting some type arguments to saw-core functions in the pretty printer: Implicit arguments are a feature that a lot of dependently-typed languages have, and they might be useful to have in saw-core. Supporting implicit arguments or underscores in terms to be parsed would be a lot of work to implement, but for printing only it might be easy to do. But I certainly wouldn't want to have a feature like that unless there was a way to switch it off.

[bboston7]

Terms/goals remain difficult to read for new users.

[bboston7]

One idea is to keep print_goal and print_term as-is, but to add some kind of pretty_print_{goal, term} command that would be more readable, with the understanding that the output is less precise than print_{goal, term}

[sauclovian-g]

In coq, "Show Implicit Arguments" is rarely necessary but vital when needed, so unless our world is much uglier I think hiding implicit arguments should be the default.