At present, the atom AST node is used by the evaluator to bind atoms used in queries. However, these atoms carry no typing information, requiring a workaround to avoid triggering the new typechecking on predicates. E.g.,
pred invariant[n: Node] { ... }
// This evaluator query would fail in v. 3.3
// invariant[Node0]
// This workaround is needed in v. 3.3
// some n: Node | {invariant[n] and n = Node0}
With this PR, Forge looks at the Kodkod bounds for this atom and infers it must be a Node if it exists.
Note that the code also includes an experimental inference from the last Sterling instance. However, this isn't yet used because of questions about temporality (can an atom change most-specific sig membership across states? Very likely if the sigs are var).
At present, the
atomAST node is used by the evaluator to bind atoms used in queries. However, these atoms carry no typing information, requiring a workaround to avoid triggering the new typechecking on predicates. E.g.,With this PR, Forge looks at the Kodkod bounds for this atom and infers it must be a
Nodeif it exists.Note that the code also includes an experimental inference from the last Sterling instance. However, this isn't yet used because of questions about temporality (can an atom change most-specific sig membership across states? Very likely if the sigs are
var).