Don't show memory references in pretty-printed values

[xsebek]

Currently, we store sub-results as "memory cells" printed as @1. Ideally, players would never see them and there would always be a way to print a value so that it could be reconstructed.

Consider for example simple let, which is printed fine:

> let f = \i.i in f
\i. i : ∀ a2. a2 -> a2

But recursive let is printed with the memory cell:

> let fix = \f. f (fix f) in fix
let fix = @33 in \f. f (force fix f) : ∀ a6. (a6 -> a6) -> a6

Similarly using other definitions uses memory cells:

> def f = 1 end
> let g = \_.f in g
let f = @51 in \_. force f : ∀ a2. a2 -> int

We could keep the original definitions and their dependencies and print those so that after overwriting f we could still print g:

// PROPOSED BEHAVIOUR BELOW
> def f = 1 end
> def g = \_.f end
> g
\_.f : ∀ a0. a0 -> int
> def f = 2 end
> g
def f = 1 end
\_.f : ∀ a0. a0 -> int

• keeping the original definition would help with Ability to save definitions typed at the REPL to a .sw file #7

[xsebek]

Hey @byorgey, do you think this would be possible generally or at least in common cases?

Maybe we could keep the Term and Env in VRef from VDelay?

[byorgey]

Hmm, good question!

Ideally, players would never see them and there would always be a way to print a value so that it could be reconstructed.

Totally agree on this point. But off the top of my head I am not sure how difficult this would be. Intuitively it strikes me as one of those things that seems reasonable on the surface but hides some weird difficulties. I will give it some more thought and see if I can come up with a reasonable proposal.

[byorgey]

So some of this is due to the way closures get printed. When we evaluate a TLam we generate a VClo (a closure containing the bound variable, the lambda body, and the environment). In order to pretty-print a value, we first convert it back into a Term using the valueToTerm function, which turns VClo into a TLet that represents the environment. However, in these specific examples, the let is unnecessary, because the let-bound thing is actually already in the ambient environment. I wonder if we could pass the existing top-level Env to valueToTerm, and have it omit let-binding things that are already in the top-level environment (with the same value!) as in the closure environment, when converting a VClo.

This would not eliminate memory references from ever showing up in pretty-printed terms (I think that is a tricky problem in general), but it would solve the def g example. However, it would not solve the let fix ... example.

I think the way to do this would be to add a Maybe Env argument to valueToTerm (we need Maybe since I think there are places we use valueToTerm where we don't have, or it would be awkward to obtain, an Env); if given an Env, when translating VClo, we will omit let bindings for variables in the closure environment with the same value as in the given Env. Then in the TUI.Controller.updateUI function, when printing the result of a REPL evaluation, we get the topValCtx (i.e. gameState . robotMap . ix 0 . robotContext . defVals) and pass it along to valueToTerm.

[byorgey]

So in order to solve #7 I think we are definitely going to have to save definitions somewhere. So every time a def is executed (and maybe for let as well?), it will save both the source code of the definition as well as its value. Concretely, perhaps Env can store both. The thing I am still unsure about is how best to use this information for pretty-printing. Maybe it's good enough to (1) try pretty-printing the value of each binding, but (2) if something is bound to a VRef, then pretty-print its definition instead.

[byorgey]

#1949 pretty much solved this. The given examples no longer generate memory references:

> let fix = \f. f (fix f) in fix
it0 : ∀ a. (a -> a) -> a = \f. f (fix f)
> def f = 1 end
> let g = \_.f in g
it1 : ∀ a. a -> Int = let f = 1 in \_. f

The only thing that could still be improved is what I discussed in a comment above: in the second example above, g does not need to be printed as let f = 1 in \_. f, it could just be printed as \_. f since f is in the ambient context. I'm going to close this and split that out into a separate issue.