search

tnelson / Forge

Forge: A Tool and Language for Teaching Formal Methods
https://forge-fm.org/
MIT License
67 stars 9 forks source link

fix: last check: multiple decls in one quantifier, minus operator RHS #198

Closed tnelson closed 7 months ago

tnelson commented 1 year ago

(1) Quantifiers can contain multiple declarations. E.g., some x: A, y: B | ... However, since A and B are arbitrary expressions, B can technically use the variable x. Our last-checker module does not currently add (x A) to the environment used for checking the expression B, resulting in a confusing error. This PR rolls the expanded environment forward across all decl domains, from left to right.

(2) Our last-checker module wasn't ever checking the right-hand side of a minus expression. Now if that exists, it's subjected to last-checker scrutiny.

tnelson commented 7 months ago

This will be fixed in #247 as part of the AST testing improvements; closing this PR.