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

Same internal name used for functor parameters and their instantiations #1556

Closed
qsctr opened this issue Jul 25, 2023 · 0 comments · Fixed by #1559
Closed

Same internal name used for functor parameters and their instantiations #1556

qsctr opened this issue Jul 25, 2023 · 0 comments · Fixed by #1559
Assignees
Labels
bug Something not working correctly parameterized modules Related to Cryptol's parameterized modules

Comments

@qsctr
Copy link
Contributor

qsctr commented Jul 25, 2023

While implementing a solution to #1455, we found that functor instantiations use the same internal names as the corresponding parameters in the functor. Specifically, if we have

interface module I where
  x : [8]
module F where
  import interface I
  y = x + 1
module M where
  x = 2
module N = F { M }

then N::x reuses the exact same internal name as F::x (the full name being in this example F::I::x_5244) rather than a fresh name.

Currently, this does not present an immediate issue with evaluating expressions at the REPL, since the instantiated parameters are not accessible from outside of the instantiated module, and we can only ever look inside a single module in the REPL at once, so the REPL does not get confused by the duplicate names. However, the OrigName of the instantiated parameter would be wrong and could cause issues elsewhere.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something not working correctly parameterized modules Related to Cryptol's parameterized modules
Projects
None yet
1 participant