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

Persist name resolution for measure names #2456

Merged
merged 14 commits into from
Dec 4, 2024

Conversation

facundominguez
Copy link
Collaborator

@facundominguez facundominguez commented Dec 3, 2024

Another step for #2169

Name resolution of measures is now remembered when importing specs.

Measures now use the same module aliases as the modules from which they are imported. For instance, foo is not in scope in module Test, but M.foo is.

module ModuleBar where
{-@ measure foo :: Bool @-}

---
module Test where
import qualified ModuleBar as M
{-@ lemma :: { foo } @-}
lemma :: ()
lemma = ()

import qualified ModuleBar as M brings into scope M.foo and any other measure exported or reexported from M with alias M.. Measures exported from module M_LHAssumptions are also exposed with alias M. if M_LHAssumptions is not imported explicitly.

Ambiguities are reported if multiple measures are in scope with the same name when the name is used.

@facundominguez facundominguez force-pushed the fd/measure-name-resolution branch from d7fdd16 to a85a214 Compare December 3, 2024 20:38
@facundominguez facundominguez force-pushed the fd/measure-name-resolution branch from a85a214 to 9f9b687 Compare December 3, 2024 20:51
@facundominguez facundominguez merged commit 99404d7 into develop Dec 4, 2024
4 checks passed
@facundominguez facundominguez deleted the fd/measure-name-resolution branch December 4, 2024 12:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant