informalsystems / quint

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
Apache License 2.0
819 stars 31 forks source link

Lambda nesting issue in simulator #1042

Open thpani opened 1 year ago

thpani commented 1 year ago

The following Quint spec produces a weird dynamic error in REPL + simulator:

module test {
  pure def listForall(list: List[a], pred: a => bool): bool = {
    list.foldl(true, (b, elem) => pred(elem))
  }

  pure val ll = [[], [("b", 2)]]
  pure val inv = ll.listForall(l => l.listForall(i => i._2 > 0))
}
$ quint repl -r test.qnt::test
>>> inv
runtime error: error: Out of bounds, nth(1)
  pure val inv = ll.listForall(l => l.listForall(i => i._2 > 0))
                                                      ^^^^

Probably binding related, it goes away if I copy the def of listForall and replace the nested call with the copy:

module test {
  pure def listForall(list: List[a], pred: a => bool): bool = {
    list.foldl(true, (b, elem) => pred(elem))
  }

  pure def listForall2(list: List[a], pred: a => bool): bool = {
    list.foldl(true, (b, elem) => pred(elem))
  }

  pure val ll = [[], [("b", 2)]]
  pure val inv = ll.listForall(l => l.listForall2(i => i._2 > 0))
}
konnov commented 1 year ago

Yep, looks strange