Unwrapping values known to exist

[flupe]

Hello there,

I have been using Quint for a few months now and it's been quite enjoyable, great work!
I had a question about a design problem that I have quite often in my ongoing specification.

I have several (pure) definitions that compute some data based on my global state, wrapped in an Option because this data may not be available or ready.

In my actions, I usually start by computing said predicates/data extractors.
Then, I need to check that they are all actually satisfied. If such is the case, I need to extract their value to enact the action/transition.

However, Quint doesn't let me extract a value from Option[a] to a, even though an earlier precondition in the all { block asserted that isSome is satisfied and that I can thus always extract the value. This forces me to use a succession of match statements that makes everything much less readable.

module demo {

  type Option[a] = None | Some(a)

  pure def isNone(o : Option[a]) : bool = o == None
  pure def isSome(o : Option[a]) : bool = o != None

  type GlobalState
  type Data
  const getData : GlobalState => Option[Data]
  const applyData : (GlobalState, Data) => GlobalState

  var state : GlobalState

  // ...
}

See for example this simple action:

  action doSomething = {
    val odata = getData(state)
    match (odata) {
      | Some(data) => state' = state.applyData(data)

      | None       => all { false, state' = state }
    }
  }

With a simple match statement I can extract the data, but I need to take care of the other branch and always put all { false, state' = state } so that Quint discards the action if we reach the branch, and picks another one (I think?).

If I have many such predicates/data extractors, I have to nest as many match statements, which makes everything completely unreadable. Even if I assert that odata is not None, I (rightfully) cannot extract data with something other than a match statement.

  action doSomething = {
    val odata = getData(state)
    all {
      odata.isSome(),
      {
        match (odata) {
        | Some(data) => state' = state.applyData(data)

        // And need to come up with bogus branches that are never satisfied.
        | None       => state' = state
        }
      }

    }
  }

So we get rid of the all { false } blocks, but we still have to deal with nesting and extraneous branches that are provably unreachable.

We could imagine implementing some monadic operations for Option, like andThen : (Option[a], f : a => Option[b]) => Option[b], but without builtin support for a Haskell-like do-notation I don't expect it to be very readable.

But I'm wondering: is there a secret Quint instruction that fails an action? The same way all { false } always skips the action, could we imagine a built-in action fail : a operator that does the same? It could inhabit any type, and would allow me to define:

action extract(o: Option[a]): a =
  match (o) {
  | Some(x) => x
  | None    => fail
  }

Therefore extract would only be allowed in actions, but would avoid this nesting. And it looks safe? Let me know what you think or if you have any advice for handling this pattern.