In the spirit of Lessons from Writing a Compiler, we have a roadmap, where we are implementing various transpiler passes feature-by-feature, instead of completely implementing every pass.
- ✅ Completed
- 🟢 Won't get in your way, but there's still work to be done
- ❌ Not implemented yet
| Language feature | Parser | Name resolution | Effects | Type checker | Simulator | To-Apalache | Tutorials |
|---|---|---|---|---|---|---|---|
| Booleans | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ |
| Integers | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ |
| if-then-else | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ |
| Operator definitions | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ |
| Modes | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ |
| Sets | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ |
| nondet | ✅ | ✅ | 🟢 | ✅ | ✅ | ✅ | ✅ |
| Maps | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ❌ |
| Lists | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ❌ |
| Records | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ❌ |
| Tuples | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ |
| Sum types | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ❌ |
| Imports | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ |
| Module definitions | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ |
| Module instances | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ❌ |
| [Multiple files][] | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ |
| Constant declarations | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ❌ |
| Variable definitions | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ |
| Assumptions | ✅ | ✅ | ✅ | ✅ | ❌ 235 | ✅ | ❌ |
| Lambdas | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ |
| Multiline disjunctions | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ |
| Multiline conjunctions | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ |
| Delayed assignment | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ |
| Invariant checking | - | - | - | - | ✅ | ✅ | ✅ |
| Higher-order definitions | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ❌ |
| Runs | ✅ | ✅ | 🟢 | ✅ | ✅ | non-goal | ✅ |
| Temporal operators | ✅ | ✅ | ✅ | ✅ | non-goal | ✅ | ❌ |
| Fairness | ✅ | ✅ | ✅ | ✅ | non-goal | ✅ | ❌ |
| Unbounded quantifiers | ✅ | ✅ | ❌ | ❌ | non-goal | ❌ | ❌ |
| String literals, see #118 | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ | ✅ |
| ✅ | ✅ | ❌ | ❌ | ❌ | ❌ | ❌ |