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

[Andreas Abel]

Hi Thorsten,

On 2022-02-02 12:19, Thorsten Altenkirch wrote:
> This is really bad from a paedagogical perspective if you use agda for 
> teaching!

I agree.  This issue is reported again and again, e.g.

   https://github.com/agda/agda/issues/5666

I attempted to fix this issue once, but this caused inconveniences for 
power users (costly reloads).

   https://github.com/agda/agda/issues/4959

> Is there nobody who could implement a read-eval-print loop for agda? It 
> shouldn’t be that difficult?

The current REPL fell into repair:

   https://github.com/agda/agda/issues/5100

But otherwise, would agda --interactive meet your expectations of a REPL?

Cheers,
Andreas

> *From: *Agda <agda-bounces at lists.chalmers.se> on behalf of Jesper Cockx 
> <Jesper at sikanda.be>
> *Date: *Tuesday, 1 February 2022 at 20:01
> *To: *Eduardo Ochs <eduardoochs at gmail.com>
> *Cc: *agda list <agda at lists.chalmers.se>
> *Subject: *Re: [Agda] Quirk: C-c C-n thinks that some symbols are not in 
> scope
> 
> Hi Eduardo,
> 
> C-c c-n evaluates the given expression in the scope of the current 
> module as it looks like from the outside (i.e. as if you import the 
> module somewhere else). In particular, this scope does not include 
> symbols from modules you have opened, unless they have been opened 
> publicly. So I expect you can solve your problem by adding 'public' to 
> the end of your open statements, e.g. 'open Add "2" public'.
> 
> -- Jesper
> 
> On Tue, Feb 1, 2022 at 8:12 PM Eduardo Ochs <eduardoochs at gmail.com 
> <mailto:eduardoochs at gmail.com>> wrote:
> 
>     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 <http://angg.twu.net/eev-agda.html>
> 
>     Thanks in advance!
>        Eduardo Ochs
>     http://angg.twu.net/#eev <http://angg.twu.net/#eev>
> 
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
> 
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
> 
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda