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

Linearity check for exist bindings #360

Open
rachitnigam opened this issue Oct 15, 2023 · 0 comments
Open

Linearity check for exist bindings #360

rachitnigam opened this issue Oct 15, 2023 · 0 comments
Labels
bug Something isn't working C: well-formedness Component: A check that is not the interval check

Comments

@rachitnigam
Copy link
Member

When a component defines an existential variable, it must provide exactly one exist binding in every scope. For example, the following program is malformed:

comp Foo[A](...) with {
  exists L;
} {
 if A > 10 {
   exists L = 10
 }
}

If A <= 10, then when monomorphizing, the module will not have a binding for L which will cause compilation failure.

It should be relatively easy to write a well-formedness pass that ensures that all scopes of a program assigns a value to each existential parameter exactly once.

@rachitnigam rachitnigam added bug Something isn't working C: well-formedness Component: A check that is not the interval check labels Oct 15, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working C: well-formedness Component: A check that is not the interval check
Projects
None yet
Development

No branches or pull requests

1 participant