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

Missing Apalache support for Quint-definable operators #1568

Open
bugarela opened this issue Dec 23, 2024 · 0 comments
Open

Missing Apalache support for Quint-definable operators #1568

bugarela opened this issue Dec 23, 2024 · 0 comments
Labels
tla+ transpilation Quint to TLA+ transpiler

Comments

@bugarela
Copy link
Collaborator

bugarela commented Dec 23, 2024

Some operators like getOnlyElement and foldr are not supported by Apalache. However, they can be easily defined in Quint itself. The reason they are built-ins is to provide better performance and error messages.

q::debug also is not supported. We could add support it on the Apalache side, but it just seems more scalable in terms of maintainability to add a def like this on Quint:

pure def q::debug(s, a) = a

I hacked a first version with these:

  const builtInDefs = [
    `pure def reverse(l: List[a]): List[a] = {
    pure val len = l.length()
    l.indices().fold(l, (acc, i) => acc.replaceAt(i, l[len - i - 1]))
  }`,

    `pure def foldr(l: List[a], init: b, op: (a, b) => b): b = {
    l.reverse().foldl(init, (acc, e) => op(e, acc))
  }`,

    `pure def getOnlyElement(s: Set[a]): a = {
     pure val hack = s.map(e => ("value", e)).setToMap()
     if (s.size() != 1) {
       hack.get("error: expected singleton")
     } else {
       hack.get("value")
     }
   }`,

    `pure def allListsUpTo(s, l) = {
    1.to(l).fold(Set([]), (acc, i) => {
      pure val kms = 0.to(i - 1).setOfMaps(s)
      pure val lists = kms.map(km => range(0, i).foldl([], (acc, i) => acc.append(km.get(i))))
      acc.union(lists)
    })
  }`,

    `pure def q::debug(s, a) = a`,
  ]

But we should probably have this in a standard library (see #1314).

We also want unwrap() included like this (but this one was not even added to the spells yet)

@bugarela bugarela added the tla+ transpilation Quint to TLA+ transpiler label Dec 23, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
tla+ transpilation Quint to TLA+ transpiler
Projects
None yet
Development

No branches or pull requests

1 participant