Case-split generates code containing internal module name

[UlfNorell]

From ren...@informatik.uni-marburg.de on September 06, 2013 18:08:54

What's the problem?

I have two modules, each in a separate file, as follows:

module Other (parameter : Set) where data Foo : Set where foo : Foo

module Bug where postulate something : Set

open import Other something

bar : Foo → Foo bar x = {!x!} -- I do C-c C-c here -- bar .#Other-230273218.foo = ? -- I get this -- bar foo = ? -- I want this

Problem: If I do a case split in the hole in module Bug, I get some internal name instead of just foo. Seems to be related to "open import" vs "open" and then "import" as well as importing a module with parameters.

What version of Agda are you using?

Agda HEAD (Agda version 2.3.3).

Original issue: http://code.google.com/p/agda/issues/detail?id=896

[UlfNorell]

From nils.anders.danielsson on September 17, 2013 02:09:57

For some reason the bug is not triggered if the code above is put in a single file (under "module M where") and "import" is removed.

Summary: Case-split generates code containing internal module name (was: C-c C-c generates invalid code)
Status: Accepted
Labels: CaseSplitting Type-Defect Priority-High Milestone-2.3.4 Modules

[UlfNorell]

From andreas....@gmail.com on October 29, 2013 09:31:02

Mmh, one reason is probably that "open import Module parameter" is implemented at the level of parsing instead at the level of scope checking. See issue 481 for some context concerning the addition of this syntax.

open import Module parameter

is implemented as

import Module as .Fresh private open module _ = .Fresh parameter

It could be that Agda sees the need to print the constructor as qualified since it thinks that there are several constructors with name foo in place.

.Fresh.foo ._.foo

(The anon. module). If I do the manual decomposition of open import into

import Common.Issue481ParametrizedModule as M123

private open module M4711 = M123 Set

bar : Foo → Foo bar x = {! x !} -- I do C-c C-c here

then x is replace by M123.foo instead of foo, clearly not what I want.

Seems that disdisambiguation for constructors is not implemented properly. In patterns, we could really have ambiguous constructors without problems, so proper ambiguation should be applied here.

Labels: Display

[UlfNorell]

From andreas....@gmail.com on October 29, 2013 10:29:49

Since I have no clue how constructor QNames are translated from abstract to concrete, I should leave this issue to Ulf, or get some tutorial from him about this...

Owner: ulf.nor...@gmail.com

[UlfNorell]

From andreas....@gmail.com on October 29, 2013 13:41:58

Mmh, now I found that inverseScopeLookup does not do its job correctly for constructors. This function is already to blame for issue 719 .

Here is the scope for the case above

* scope (top-level-module)
  private
    names
      Bla --> [M4711.Bla]
      Foo --> [M4711.Foo]
      foo --> [M4711.Foo.foo]
      id --> [M4711.id]
    modules
      Foo --> [M4711.Foo]
      M123 --> [Common.Issue481ParametrizedModule]
      M4711 --> [M4711]
  public
    names
      bar --> [bar]

* scope M4711
  public
    names
      Bla --> [M4711.Bla]
      Foo --> [M4711.Foo]
      foo --> [M4711.Foo.foo]
      id --> [M4711.id]
    modules
      Foo --> [M4711.Foo]

* scope M4711.Foo
  public
    names
      foo --> [M4711.Foo.foo]

-- inverse looking up abstract name Common.Issue481ParametrizedModule.Foo.foo -- yields Just M123.foo

Thus, the original constructor that is stored in the pattern is Common.Issue481ParametrizedModule.Foo.foo but we would like to recover M4711.Foo.foo which is printed as just foo.

[UlfNorell]

From andreas....@gmail.com on October 29, 2013 15:00:59

We do not even need import or parameterized modules. It is sufficient to trigger a section application by the following code:

module Other where data Foo : Set where foo : Foo

module M = Other -- triggers a section application open M

bar : Foo → Foo bar x = {!x!} -- I do C-c C-c here -- bar Other.foo = ? -- I get this -- bar foo = ? -- I want this

after module Issue896b ScopeInfo current = context = TopCtx modules * scope * scope Issue896b private names Foo --> [Issue896b.M.Foo] foo --> [Issue896b.M.Foo.foo] modules Foo --> [Issue896b.M.Foo] public names bar --> [Issue896b.bar] modules M --> [Issue896b.M] Other --> [Issue896b.Other] * scope Issue896b.Other public names Foo --> [Issue896b.Other.Foo] foo --> [Issue896b.Other.Foo.foo] modules Foo --> [Issue896b.Other.Foo] * scope Issue896b.Other.Foo public names foo --> [Issue896b.Other.Foo.foo] * scope Issue896b.M public names Foo --> [Issue896b.M.Foo] foo --> [Issue896b.M.Foo.foo] modules Foo --> [Issue896b.M.Foo] * scope Issue896b.M.Foo public names foo --> [Issue896b.M.Foo.foo]

applying section Other ptel = tel = tel' = tel''= eta = applySection M = Other defs: fromList [(Issue896b.Other.Foo,Issue896b.M.Foo),(Issue896b.Other.Foo.foo,Issue896b.M.Foo.foo)] mods: fromList [(Issue896b.Other.Foo,Issue896b.M.Foo)] inverse looking up abstract name Issue896b.Other.Foo.foo yields Just Other.foo inverse looking up abstract name Issue896b.M.Foo yields Just Foo

[UlfNorell]

From ulf.nor...@gmail.com on November 01, 2013 06:37:57

In order to make this work we need type directed pretty printing. Plan: refactor CheckInternal to make it possible to use it to define arbitrary type directed traversals, and then implement reify for typed terms (pair of a term and its type).

Labels: -CaseSplitting