[Agda] C-c C-c turns issue 64 into a bug

[Ulf Norell]

On Fri, May 16, 2008 at 3:37 PM, Samuel Bronson <naesten at gmail.com> wrote:

> Previously, http://code.google.com/p/agda/issues/detail?id=64 has been
> simply an annoying infelicity... but with C-c C-c, it becomes a bug:
> printing names as if they are not in scope when they are does not
> produce valid code. (It wouldn't produce valid code if the names were
> actually out of scope, either, but that can't be helped ;-)


The problem, which makes the issue tricky to solve, is that open public
doesn't just give you a new name for an existing definition, it creates a
new definition. So technically the name that is being printed is out of
scope. Example:

  module A where
    f = ...

  module B where
    open A public

means the same as

  module A where
    f = ...

  module B where
    f = A.f

So when we see A.f it's not simply a matter of printing B.f instead, we need
to fold the definition of B.f. The reason for things being like this is that
A might be a parameterised module and we might instantiate it when opening
it. In this case B.f will be a more interesting definition. That said,
actually doing the folding should be possible in many cases.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080516/40f02c05/attachment.html