[Agda] parsing reports
Serge D. Mechveliani
mechvel at botik.ru
Mon Jan 28 16:00:57 CET 2013
On Mon, Jan 28, 2013 at 03:32:11PM +0100, Nils Anders Danielsson wrote:
> On 2013-01-01 13:38, Serge D. Mechveliani wrote:
> >A minor note on Agda-2.3.2 MAlonzo:
> >when a type constructor is not in scope, the type checker reports
> >"could not parse this expression ...",
> >-- without explaining the reason any more precisely.
> >Why the checker does not report, say, "... not in scope" ?
> >For example,
> > open import Data.Maybe using (Maybe) -- `just' is forgotten
> > f : Maybe Bool -> Bool
> > f (just _) = true
> > f _ = false
> >causes "could not parse (just _)"
> >rather than "not in scope: just"
> >For the examples with a complex expression this leads to difficulty in
> >finding the source of this kind of error.
> In many cases it is hard to determine what the problem is. Let me modify
> your example:
> f : Maybe Bool -> Bool
> f (just x) = true
> f _ = false
> The problem could be that "just" is not in scope, but it could also be
> that "_x" is not in scope.
Respectively, a natural report is:
Cannot parse (just x).
1) "just" is an operator being not in scope,
2) "_x" is an operator being not in scope
(only 2-3 probable reasons to print).
Seeing "1)", the programmer guesses to import "just".
But suppose that in 99% cases it occurs that the printed reasons are
not relevant ...
One needs to estimate, how often the reported reasons will occur
I am not so sure about this.
More information about the Agda