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.

Sign up for GitHub

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

Translate Quint generate #2916

Merged
merged 7 commits into from
Aug 14, 2024
Merged

Translate Quint generate #2916

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
f6a04b8
Translate Quint generate to Apalache!Gen
konnov Jun 26, 2024
fee926c
fix the signature
konnov Jun 26, 2024
7351a7e
properly translate Quint's generate
konnov Jun 27, 2024
74080d8
add release notes
konnov Jun 27, 2024
5b5f6af
fix formatting
konnov Jun 27, 2024
1988ae0
Merge branch 'main' into igor/quint-generate
konnov Aug 13, 2024
4e48675
Merge branch 'main' into igor/quint-generate
konnov Aug 14, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .unreleased/features/translate-generate.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Translate Quint's generate into `Apalache!Gen` (#2916)
29 changes: 28 additions & 1 deletion tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -655,9 +655,13 @@ class Quint(quintOutput: QuintOutput) {

// Convert Quint's nondet variable binding
//
// val nondet name = oneOf(domain); scope
// nondet name = oneOf(domain); scope
// ~~>
// \E name \in domain: scope
//
// nondet name = generate(sz, typeSet); scope
// ~~>
// \E name \in { Apalache!Gen(sz) }: scope
private val nondetBinding: (QuintDef.QuintOpDef, QuintEx) => NullaryOpReader[TBuilderInstruction] = {
case (QuintDef.QuintOpDef(_, name, "nondet", QuintApp(id, "oneOf", Seq(domain))), scope) =>
val elemType = typeConv.convert(types(id).typ)
Expand All @@ -666,6 +670,19 @@ class Quint(quintOutput: QuintOutput) {
tlaDomain <- tlaExpression(domain)
tlaScope <- tlaExpression(scope)
} yield tla.exists(tlaName, tlaDomain, tlaScope)

case (QuintDef.QuintOpDef(_, name, "nondet", QuintApp(id, "generate", Seq(bound, _))), scope) =>
val elemType = typeConv.convert(types(id).typ)
val boundIntConst = intFromExpr(bound)
if (boundIntConst.isEmpty) {
throw new QuintIRParseError(s"nondet $name = generate($bound) ... expects an integer constant")
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why the ...?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There is a nested expression under nondet

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, but it's not relevant for the error here, so at best it will confuse.

Also, afaiu there's a second parameter to generate()? So ellipses inside the parentheses make more sense to me.

}
val genExpr = tla.enumSet(tla.gen(boundIntConst.get, elemType))
val tlaName = tla.name(name, elemType)
for {
tlaScope <- tlaExpression(scope)
} yield tla.exists(tlaName, genExpr, tlaScope)

case invalidValue =>
throw new QuintIRParseError(s"nondet keyword used to bind invalid value ${invalidValue}")
}
Expand Down Expand Up @@ -804,4 +821,14 @@ class Quint(quintOutput: QuintOutput) {
.reverse // Return the declarations to their original order
}
} yield TlaModule(module.name, declarations)

private def intFromExpr(expr: QuintEx): Option[BigInt] = {
expr match {
case QuintInt(_, value) =>
Some(value)

case _ =>
None
}
}
}
16 changes: 14 additions & 2 deletions tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -172,7 +172,15 @@ class TestQuintEx extends AnyFunSuite {
val chooseSomeFromIntSet = app("chooseSome", intSet)(QuintIntT())
val oneOfSet = app("oneOf", intSet)(QuintIntT())
val nondetBinding =
e(QuintLet(uid, d(QuintDef.QuintOpDef(uid, "n", "nondet", oneOfSet), QuintIntT()), nIsGreaterThan0), QuintIntT())
e(QuintLet(uid, d(QuintDef.QuintOpDef(uid, "n", "nondet", oneOfSet), QuintIntT()), nIsGreaterThan0), QuintBoolT())
val generateSet = app("generate", _42, app("Set", _42)(QuintSetT(QuintIntT())))(QuintSetT(QuintIntT()))
val nondetGenerateId = uid
val appGenSet =
app("eq", e(QuintName(uid, "S"), QuintSetT(QuintIntT())), app("Set")(QuintSetT(QuintIntT())))(QuintBoolT())
val nondetGenerate =
e(QuintLet(uid,
d(QuintDef.QuintOpDef(nondetGenerateId, "S", "nondet", generateSet),
QuintOperT(Seq(), QuintSetT(QuintIntT()))), appGenSet), QuintBoolT())
// Requires ID registered with type
val selectGreaterThanZero = app("select", intList, intIsGreaterThanZero)(QuintSeqT(QuintIntT()))
val addOne = app("iadd", name, _1)(QuintIntT())
Expand Down Expand Up @@ -710,10 +718,14 @@ class TestQuintEx extends AnyFunSuite {
assert(convert(Q.app("put", Q.intMap, Q._3, Q._42)(intMapT)) == expected)
}

test("can convert nondet bindings") {
test("can convert nondet...oneOf") {
assert(convert(Q.nondetBinding) == "∃n ∈ {1, 2, 3}: (n > 0)")
}

test("can convert nondet...generate") {
assert(convert(Q.nondetGenerate) == "∃S ∈ {Apalache!Gen(42)}: (S = {})")
}

test("can convert let binding with reference to name in scope") {
assert(convert(Q.letNbe42inNisGreaterThan0) == "LET n ≜ 42 IN n() > 0")
}
Expand Down
Loading