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

[Thorsten Altenkirch]

This is really bad from a paedagogical perspective if you use agda for teaching!

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

Cheers,
Thorsten

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

Thanks in advance!
  Eduardo Ochs
  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



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.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220202/ef0fe7b9/attachment.html>