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

[Ulf Norell]

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

> On Fri, May 16, 2008 at 9:49 AM, Ulf Norell <ulfn at cs.chalmers.se> wrote:
>
> > 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.
>
> [examples snipped]
>
> > 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.
>
> So there would be cases where this would not be possible? I'm having
> trouble thinking of how that would arise...
>

Well, maybe not impossible. In any case, consider

module A (x : X) where
  private f : T

module B where
  open A u public

module C where
  open A v public

Now "A.f w" can be printed as "B.f" if w = u and "C.f" if w = v. To decide
which we need to compute the normal forms of u, v, and w, and that's not
something you really want to do during printing.

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