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

Quint -> TLA+ transpilation fixes #3041

Merged
merged 10 commits into from
Dec 4, 2024
Merged

Quint -> TLA+ transpilation fixes #3041

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
b6d8824
Change unit type representation for compatibility with TLC
bugarela Nov 29, 2024
6f61e23
Apply `{}` instead of `[]` to the default eliminator
bugarela Nov 29, 2024
65686e1
Remove case that resulted in incorrect printing of `map[<<1>>]` when …
bugarela Nov 29, 2024
8056710
Prevent LET..IN to be printed as an operator argument
bugarela Nov 29, 2024
cb5ee57
Update existing tests
bugarela Nov 29, 2024
bb746fc
Add test for LET-IN extraction
bugarela Nov 29, 2024
ce5e61e
Fix formatting
bugarela Nov 29, 2024
f28e16e
Add CHANGELOG entry
bugarela Nov 29, 2024
7b4e7db
Merge branch 'main' into gabriela/quint-to-tla-improvements
bugarela Nov 29, 2024
9598c3e
Merge branch 'main' into gabriela/quint-to-tla-improvements
konnov Dec 2, 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
Next Next commit
Change unit type representation for compatibility with TLC
  • Loading branch information
@bugarela
bugarela committed Nov 29, 2024
commit b6d8824788cbafee7e035ca4360cd2be61b5f9a1
2 changes: 1 addition & 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 @@ -573,7 +573,7 @@ class Quint(quintOutput: QuintOutput) {
case "Tup" =>
if (quintArgs.isEmpty) {
// Translate empty tuples to values of type UNIT
(_) => Reader((_) => tla.const("U", ConstT1(("UNIT"))))
(_) => Reader((_) => tla.rowRec(None, "tag" -> tla.str("UNIT")))
} else {
variadicApp(args => tla.tuple(args: _*))
}
Expand Down
5 changes: 4 additions & 1 deletion tla-io/src/main/scala/at/forsyte/apalache/io/quint/QuintTypeConverter.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,7 +97,10 @@ private class QuintTypeConverter extends LazyLogging {
case QuintFunT(arg, res) => FunT1(convert(arg), convert(res))
case QuintOperT(args, res) => OperT1(args.map(convert), convert(res))
case QuintTupleT(Row.Nil() | Row.Cell(Seq(), _)) =>
ConstT1("UNIT") // Use the Unit type for empty tuples, since they are the unit type in Quint
// Use the Unit type for empty tuples, since they are the unit type in Quint
// The unit type is a record like [ "tag" |-> "UNIT" ] so it can be compared to other constructed types.
// This is relevant when we produce a TLA+ file to be used with TLC.
RecRowT1(RowT1("tag" -> StrT1))
case QuintTupleT(row) => rowToTupleT1(row)
case QuintRecordT(row) => RecRowT1(rowToRowT1(row))
case QuintSumT(row) => VariantT1(rowToRowT1(row))
Expand Down