[Agda] Quirk: C-c C-n thinks that some symbols are not in scope

[Eduardo Ochs]

Hello list,

I think that I found a quirk on the behavior of `C-c C-n'. When I was
trying to write a minimal example that showed the problem I wrote
this, that isn't really minimal but that should be minimal enough...

  module NameOfThisFile where

  open import Agda.Builtin.String
  open import Agda.Builtin.String.Properties

  infixl 4 _++_
  _++_ : String -> String -> String
  _++_ str1 str2 = primStringAppend str1 str2

  module Add (i : String) where
    infixl 4 _+++_
    add   : String -> String -> String
    add   a b = "(" ++ a ++ " +_" ++ i ++ " " ++ b ++ ")"
    _+++_ : String -> String -> String
    _+++_ a b = add a b

  module Add0 = Add "0"
  module Add1 = Add "1"
  -- open Add0
  open          Add "2"

  aa : String
  aa = "AAA"
  bb : String
  bb = "BBB"
  cc : String
  cc = aa +++ bb

  -- (find-agdanorm "aa ++ bb")
  -- (find-agdanorm "Add.add   \"4\" aa bb")
  -- (find-agdanorm "Add0.add        aa bb")
  -- (find-agdanorm "Add._+++_ \"9\" aa bb")
  -- (find-agdanorm "Add0._+++_      aa bb")
  -- (find-agdanorm "aa Add0.+++ bb")
  -- (find-agdanorm "aa +++ bb")
  -- (find-agdanorm "_+++_")
  -- (find-agdatype "_+++_")
  -- (find-agdanorm "cc")

The sexps like (find-agdanorm "<expr>") in comments use a hack that I
wrote that is simple to explain. The docstring of find-agdanorm is:

  (find-agdanorm AGDAEXPR &rest REST)

  Show the normalized value  of AGDAEXPR in the buffer "*Normal Form*".
  This function goes to the beginning of the Agda comment in the
  current line, i.e., to the first occurrence of "--" in the
  current line, and the runs ‘C-c C-n AGDAEXPR RET’ there.
  This only works in agda2-mode. This is a quick hack!

If I go to the beginning of the line with the

  -- (find-agdanorm "aa +++ bb")

and I type `C-c C-n aa +++ bb RET' there - or if I execute the sexp -
Agda tells me that the _+++_ is not in scope, and the same happens
with this one here:

  -- (find-agdanorm "_+++_")

I get the same "Not in scope" if I use `C-c C-d _+++_' to get the type
of _+++_... but the last sexp,

  -- (find-agdanorm "cc")

works, and it shows that the normalized value of cc is this:

  "(AAA +_2 BBB)"

All the other sexps work as expected without errors.

Is that behavior documented? It seems that `C-c C-n' and `C-c C-d' are
ignoring some symbols that were brought into scope by this line,

  open          Add "2"

and for me this is unexpected & bad.

I am using Agda 2.6.1.3 - I don't have the current version here.
I've put more info, links, and a screenshot in this page:

  http://angg.twu.net/eev-agda.html

Thanks in advance!
  Eduardo Ochs
  http://angg.twu.net/#eev
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220201/f65dd112/attachment.html>