Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[New module system] Type/constraint synonyms always warn as unused #1372

Closed
Tracked by #1363
m-yac opened this issue Jun 21, 2022 · 1 comment
Closed
Tracked by #1363

[New module system] Type/constraint synonyms always warn as unused #1372

m-yac opened this issue Jun 21, 2022 · 1 comment
Labels
language Changes or extensions to the language parameterized modules Related to Cryptol's parameterized modules

Comments

@m-yac
Copy link
Contributor

m-yac commented Jun 21, 2022

In #1363 type and constraint synonyms seem to always generate unused warnings. For example, in the REPL:

Loading module Cryptol
Cryptol> type X = [8]
Cryptol> 5 : X
[warning] at <interactive>:1:6--1:7
    Unused name: X
0x05

This can also be seen in tests/examples/allexamples.icry.stdout, for example.

Like #1371, this appears to be a renamer bug but I wasn't able to find anything after a quick first pass.

@m-yac m-yac added parameterized modules Related to Cryptol's parameterized modules language Changes or extensions to the language labels Jun 21, 2022
@m-yac
Copy link
Contributor Author

m-yac commented Jul 14, 2022

The issue in allexamples.icry ended up being specific to functor instances. A more minimal example is:

interface module I where
  type n : #
module A where
  import interface I
  type T = 5
module M where
  submodule N where
    type n = 7
  submodule B = A { submodule N }
  import submodule B as B
  type MyT = B::T

Compare this to the following example:

module M where
  submodule B where
    type T = 5
  import submodule B as B
  type MyT = B::T

Recall that when warnUnused is called, it generates a warning for each name which has exactly one usage counted in the current module. In both examples, the declaration type MyT = T adds one to the usage count of B::T in M. In the second example the declaration of T in the submodule B also adds one to B::T's usage count in M, but in the first example there is no such declaration. Thus, the first example generates an unused warning for B::T (rendered confusingly as an unused warning for T in A.cry, since the location of B::T remains in A.cry) but the second example does not.

This is fixed in 2c179b1 by keeping track of which names came from functor instances, and ignoring them in warnUnused. I did this by simply adding a new constructor to the new OrigSource datatype, which already keeps track of whether a name came from a definition or a module parameter.

One idea I did not implement was simply adding one to the usage count of every definition when instantiating a module. This change would mean requiring the user to use every definition in an instantiated module if they want no warnings, which doesn't seem like what we want.

@m-yac m-yac closed this as completed Jul 14, 2022
@m-yac m-yac mentioned this issue Jul 14, 2022
8 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
language Changes or extensions to the language parameterized modules Related to Cryptol's parameterized modules
Projects
None yet
Development

No branches or pull requests

1 participant