Evaluate private definitions (toplevel interaction)

[andreasabel]

Private definitions cannot be evaluated in interaction top level:

open import Agda.Builtin.Nat
private n = 5

Then C-c C-n n gives an error complaining that n is not in scope.
The same problem arises with non-public open.

Here is Thorsten Altenkirch's original feature request:

I have come across this little nuisance when using agda especially when doing life hacking in lectures or talks.

I try to evaluate an expression which depends on opening some modules which I have opened in my file but agda is not aware of this. E.g.

record Stream (A : Set) : Set where
  constructor _∷_
  coinductive
  field
    hd : A
    tl : Stream A

open Stream

from : ℕ → Stream ℕ
hd (from n) = n
tl (from n) = from (suc n)

And then I say C-c C-n hd (from 0) and agda responds

1,1-3
Not in scope:
  hd at 1,1-3 (did you mean 'Stream.hd'?)
when scope checking hd

Ok I can just introduce a shed

x = {!!}

and evaluate inside there but this is a bit clumsy. Isn’t there a better way to do this?

Ok I can say open Stream public – but do I want this?

[gallais]

May be worth having a distinct command "evaluate in context at cursor".
This way we can evaluate things on the RHS or inside a local module with
local let-bound definitions.

[jespercockx]

May be worth having a distinct command "evaluate in context at cursor".
This way we can evaluate things on the RHS or inside a local module with
local let-bound definitions.

That would require us to store the context of every subterm, which I don't think is really feasible.

[UlfNorell]

I do believe we have the "inside scope" available, that is the scope that would be used for any new definitions at the end of the module. It ought not be too difficult to use this instead of the "outside scope", which is what other modules importing this module sees.

[xekoukou]

I mean, what @gallais proposes is the holy grail of interactive theorem provers.
Which means that all the internal data structures need to be reconsidered with this in mind.

[nad]

Related: #317. I wrote that 'I think the parameters should be in scope when "top-level" commands are executed, because these commands should behave in the same way as commands executed in a top-level goal at the end of the module'.

[andreasabel]

@UlfNorell :

I do believe we have the "inside scope" available, that is the scope that would be used for any new definitions at the end of the module. It ought not be too difficult to use this instead of the "outside scope", which is what other modules importing this module sees.

We do use the inside scope. However, the private definitions are removed from the insideScope:

agda/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs

Lines 1232 to 1236 in bc8feec

	(insideScope, insideDecl) <- scopeCheckModule r m am tel $
	toAbstract insideDecls
	let scope = over scopeModules (fmap $ restrictLocalPrivate am) insideScope
	setScope scope
	return $ TopLevelInfo (outsideDecls ++ [ insideDecl ]) scope

You changed this in the course of the "deadcode" optimizations:

• In c823aa9 you include a test case that defines "Not in scope" for evaluating private definitions as the specified behavior of Agda.
• In 7f47d51 the release notes for Agda 2.4.4 state:

Private definitions of a module are no longer in scope at the Emacs mode top-level.
The reason for this change is that .agdai-files are stripped of unused private definitions (which can yield significant performance improvements for module-heavy code).
To test private definitions you can create a hole at the bottom of the module, in which private definitions will be visible.

So while the OP used to work, there was a decision made to sacrifice it for the sake of performance.

It seems there are three interest pursued which cannot all be integrated with the current architecture:

1. The OP.
2. To use the current module in its optimized form after serialization and deserialization.
3. The deadcode optimization in interface files to reduce the memory consumption.

A possible fix (Alt A) could look like this: There are two different formats of the interface file, one that includes the private definitions (2) (say .agdatop) and one that doesn't (1) (.agdai). In interaction mode, the current module is then deserialized from the interface file (2), but recursive deserialization refers to the interfaces of type (1). The interactive command C-c C-l (load) would create an interface of type (2), all other instances of processing a file would create an ordinary interface (1).

An alternative fix (Alt B) would drop goal 2 and remove private definition only just before serialization. The current main module (in its internal representation) would then always be created from source, rather than loaded from an interface. However, this has the drawback that switching file in emacs would always mean that the whole file is type-checked again from scratch. @nad has complained about such behavior in the past. Yet currently, rechecking is anyway often needed because the highlighting is not reliably loaded from the interface file, see issue #3549.

Input needed from @UlfNorell (defined the current specified behavior) and @nad (expertise on import and interaction logic).

[UlfNorell]

What about Alt B, but we add an emacs command to switch between "evaluation mode" (not using the interface for the current file) and "regular mode" (the normal behaviour). This should solve the drawback when switching files, if we reset the to regular mode when changing buffer.

[andreasabel]

C-c C-n could switch automatically to evaluation mode.
Automatically resetting to regular mode when changing buffer makes sense, but keeping in mind that the first C-c C-n requires rechecking then. Anyway, I suppose C-c C-n is more used in demonstration situations of Agda than in serious development (I very very rarely use it at all), thus extra checking caused by C-c C-n is likely harmless!?

[UlfNorell]

Also checking should be quick due to caching, no?

[andreasabel]

Note: It seems the present issue is a duplicate of #1804.

[txa]

The other option seems to be not to strip private definitions. Why is this so important?

[andreasabel]

For performance: #1804 (comment)

[nad]

Another option is perhaps to switch to some kind of structured signature so that the optimisation is not necessary. This may also have other performance benefits (#4331).

[andreasabel]

@nad:

Another option is perhaps to switch to some kind of structured signature so that the optimisation is not necessary. This may also have other performance benefits (#4331).

The problem isn't in the signature but in the scope. The private declarations get removed from the ScopeInfo when the top level module is finished scope checking. This is what I am addressing here.

@UlfNorell :

What about Alt B, but we add an emacs command to switch between "evaluation mode" (not using the interface for the current file) and "regular mode" (the normal behaviour). This should solve the drawback when switching files, if we reset the to regular mode when changing buffer.

I am implementing this, but this will be disruptive to some interaction tests that accumulate solutions for metas (e.g. Long). A top-level command, triggering a reload, will now lose these solutions since they are not written to a file. Maybe this isn't such a problem. We have a similiar problem already with the case-splitting command, which does not actually feed back to the state since it would require a reload from the updated source file.

[andreasabel]

PR #4652 for review.

[nad]

With this change in place, if I load the file, edit it, and use a top-level command to (say) normalise an expression, will Agda reload the file (and possibly fail)? In that case I am opposed to this change.

[andreasabel]

I have merged the PR to subject it to testing in practice.

@nad : Please use Agda "naturally" (as you always use it) and see if any disruption of your workflows happens in practice. There is an "emergency brake", option --top-level-interaction-no-private that brings back the old behavior, should you get irritated by the new one. Please report situations where the new behavior is disrupting.

[andreasabel]

I undid the fix. A workaround (in many cases) is to leave a hole in the file one wants to issue top-level interaction commands.