Skip to content

Provide safe and unsafe methods for looking up variables #29

@jorisdral

Description

@jorisdral

Both findVars and lookUpGVar assume that the variable to look up is (i) in the environment, and (ii) that evaluation of the op associated with the variable must succeed. Assuming the user uses the default test precondition, then (i) is guaranteed in general, but (ii) is not. For (i), all methods of obtaining variables are safe, except for variables created using unsafeMkGVar. For (ii), evaluation is only guaranteed for variables as they appear in an Action.

As an example of why evaluation can fail, consider a variable of type v :: GVar op (Either a b), for which evaluation succeeds. We can map this variable to v' :: GVar op a using mapGVar. If v pointed to a value that was a Left, then if evaluation of v' will also succeed, otherwise it will not.

So the problem is this: if the user uses mapGVar on a variable that is not part of action that is checked by the default precondition, then the user risks failures because evaluation does not succeed.

#25 and #28 exacerbate the problem because those PRs introduce more ways to create variables and more locations in the code where variables can be looked up (which involves evaluation). However, the problem existed before #25 and #28 already: a user could already use mapGVar erroneously before looking up a variable.

We should probably provide both a safe (returning something equivalent to Maybe a) and unsafe version (returning something equivalent to a using fromJust), and document under which circumstances a use of the unsafe version can be considered a safe use.

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't workingtriageNeeds triage

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions