Merge pull request #1399 from informalsystems/1309/to-tla

Author: shonfeder

CHANGELOG.md

@@ -12,6 +12,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Added polymorphic type declarations, allowing abstracting commonly used data
   types like `Option[a]` and `Result[err, ok]`. Note that this is not yet
   supported by `verify`. (#1298)
+- Added `compile` subcommand, allowing compiling specs to TLA+ (via Apalache)
+  and to a JSON format. (#1309, #359)
 
 ### Changed
 

doc/quint.md

@@ -14,6 +14,8 @@ and integration with other tools.
 The main commands of `quint` are as follows:
 
  - [x] `repl` starts the REPL (Read-Eval-Print loop) for Quint
+ - [x] `compile` parses, typechecks, and processes a quint specification
+       into the `--target` format, writing the results to stdout
  - [x] `parse` parses a Quint specification and resolves names
  - [x] `typecheck` infers types in a Quint specification
  - [x] `run` executes a Quint specification via random simulation
@@ -65,6 +67,38 @@ The REPL is especially useful for learning the language. See the
 The verbosity levels 3 and 4 are used to show execution details. They are
 especially useful for debugging complex specifications.
 
+## Command `compile`
+
+```sh
+$  quint compile --help
+quint compile <input>
+
+compile a Quint specification into the target, the output is written to
+stdout
+
+Options:
+  --help       Show help                                               [boolean]
+  --version    Show version number                                     [boolean]
+  --out        output file (suppresses all console output)              [string]
+  --main       name of the main module (by default, computed from filename)
+                                                                        [string]
+  --target     the compilation target. Supported values: tlaplus, json
+                                                      [string] [default: "json"]
+  --verbosity  control how much output is produced (0 to 5)[number] [default: 2]
+```
+
+Given a quint specification as input, this command parses, resolves imports,
+typechecks, and then "flattens" the specification into on module containing just
+the needed definitions.
+
+The following compilation targets are supported
+
+- `json`: The default target, this produces a json representation, in the same
+  format which is described under [`parse`](#command-parse) and
+  [`typecheck`](#command-typecheck), below.
+- `tlaplus`: Quint uses its integration with Apalache to compile the
+  specification into TLA+.
+
 ## Command `parse`
 
 *Warning: The language is still in active development, and breaking changes are

quint/apalache-tests.md

@@ -219,3 +219,54 @@ An example execution:
   __saved_n: 1,
   n: 1
 ```
+
+## Compiling to TLA+
+
+### Test that we can compile to TLA+ of the expected form
+
+<!-- !test in can convert booleans.qnt to TLA+ -->
+```
+quint compile --target tlaplus  ../examples/language-features/booleans.qnt
+```
+
+<!-- !test out can convert booleans.qnt to TLA+ -->
+```
+------------------------------- MODULE booleans -------------------------------
+
+EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache
+
+VARIABLE b
+
+step ==
+  (b \/ TRUE)
+    /\ ~(b /\ FALSE)
+    /\ (b => b)
+    /\ (b <=> b)
+    /\ b = b
+    /\ b /= (~b)
+    /\ b' := (~b)
+
+init == b' := TRUE
+
+================================================================================
+```
+
+### Test that we can compile a module with imports and instances to TLA+
+
+
+<!-- !test in can convert clockSync3.qnt to TLA+ -->
+```
+quint compile --target tlaplus  ../examples/classic/distributed/ClockSync/clockSync3.qnt | head
+```
+
+
+TODO: This is an incorrect result, we are removing all "unused" declarations
+which leaves nothing, thanks to the way clockSync3 is instanced.
+<!-- !test out can convert clockSync3.qnt to TLA+ -->
+```
+------------------------------ MODULE clockSync3 ------------------------------
+
+EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache
+
+================================================================================
+```

quint/io-cli-tests.md

@@ -171,6 +171,38 @@ Trying to unify bool and int
 error: typechecking failed
 ```
 
+## The `compile` commaind
+
+### Reports in error for invalid `--target`
+
+We pipe stderr to `tail` here. Following https://stackoverflow.com/a/52575213/1187277
+This is a clean CLI interface error, but we don't want to put the entire output
+in the test, lest it require fiddling when unrelated things are updated.
+
+<!-- !test exit 1 -->
+<!-- !test in compile to invalid target -->
+```
+quint compile --target invalidTarget ../examples/language-features/booleans.qnt 2> >(tail -1 >&2)
+```
+
+<!-- !test err compile to invalid target -->
+```
+Invalid option for --target: invalidTarget. Valid options: tlaplus, json
+```
+
+
+### Can compile `booleans.qnt` to JSON
+
+<!-- !test in compile booleans.qnt to json -->
+```
+quint compile --target json ../examples/language-features/booleans.qnt  | jq '.modules[0].name'
+```
+
+<!-- !test out compile booleans.qnt to json -->
+```
+"booleans"
+```
+
 ## Use of `repl`, `test`, and `run`
 
 ### Repl loads a file with -r

quint/src/apalache.ts

@@ -69,6 +69,8 @@ type ApalacheConfig = any
 type Apalache = {
   // Run the check command with the given configuration
   check: (c: ApalacheConfig) => Promise<ApalacheResult<void>>
+  // Convert the provided input into formatted TLA
+  tla: (c: ApalacheConfig) => Promise<ApalacheResult<string>>
 }
 
 function handleVerificationFailure(failure: { pass_name: string; error_data: any }): ApalacheError {
@@ -97,28 +99,36 @@ function handleVerificationFailure(failure: { pass_name: string; error_data: any
   }
 }
 
+async function handleResponse(response: RunResponse): Promise<ApalacheResult<any>> {
+  if (response.result == 'success') {
+    const success = JSON.parse(response.success)
+    return right(success)
+  } else {
+    switch (response.failure.errorType) {
+      case 'UNEXPECTED': {
+        const errData = JSON.parse(response.failure.data)
+        return err(errData.msg)
+      }
+      case 'PASS_FAILURE':
+        return left(handleVerificationFailure(JSON.parse(response.failure.data)))
+      default:
+        // TODO handle other error cases
+        return err(`${response.failure.errorType}: ${response.failure.data}`)
+    }
+  }
+}
+
 // Construct the Apalache interface around the cmdExecutor
 function apalache(cmdExecutor: AsyncCmdExecutor): Apalache {
   const check = async (c: ApalacheConfig): Promise<ApalacheResult<void>> => {
-    const response = await cmdExecutor.run({ cmd: 'CHECK', config: JSON.stringify(c) })
-    if (response.result == 'success') {
-      return right(void 0)
-    } else {
-      switch (response.failure.errorType) {
-        case 'UNEXPECTED': {
-          const errData = JSON.parse(response.failure.data)
-          return err(errData.msg)
-        }
-        case 'PASS_FAILURE':
-          return left(handleVerificationFailure(JSON.parse(response.failure.data)))
-        default:
-          // TODO handle other error cases
-          return err(`${response.failure.errorType}: ${response.failure.data}`)
-      }
-    }
+    return cmdExecutor.run({ cmd: 'CHECK', config: JSON.stringify(c) }).then(handleResponse)
+  }
+
+  const tla = async (c: ApalacheConfig): Promise<ApalacheResult<string>> => {
+    return cmdExecutor.run({ cmd: 'TLA', config: JSON.stringify(c) }).then(handleResponse)
   }
 
-  return { check }
+  return { check, tla }
 }
 
 // Alias for an async callback for values of type T used to annotate
@@ -127,17 +137,18 @@ function apalache(cmdExecutor: AsyncCmdExecutor): Apalache {
 type AsyncCallBack<T> = (err: any, result: T) => void
 
 // The core grpc tooling doesn't support generation of typing info,
-// we therefore record the structer we require from the grpc generation
-// in the 6 following types.
+// we therefore record the structure we require from the grpc generation
+// in the following types.
 //
 // The types reflect https://github.com/informalsystems/apalache/blob/main/shai/src/main/protobuf/cmdExecutor.proto
 
 type RunRequest = { cmd: string; config: string }
 
 type RunResponse =
   | { result: 'failure'; failure: { errorType: string; data: string } }
-  // The success data also includes the parsed module, but we don't need it
-  | { result: 'success' }
+  // The success data also includes the parsed module, either as JSON
+  // representing the Apalache IR, or as a TLA string (if the `TLA` command is used)
+  | { result: 'success'; success: string }
 
 // The interface for the CmdExecutor service generated by the gRPC library
 type CmdExecutor = {

quint/src/cli.ts

@@ -9,10 +9,12 @@
  * @author Igor Konnov, Gabriela Moreira, Shon Feder, Informal Systems, 2021-2023
  */
 
+import { fail } from 'assert'
 import yargs from 'yargs/yargs'
 
 import {
   CLIProcedure,
+  compile,
   docs,
   load,
   outputResult,
@@ -58,7 +60,7 @@ const parseCmd = {
       desc: 'name of the source map',
       type: 'string',
     }),
-  handler: async (args: any) => load(args).then(chainCmd(parse)).then(outputResult),
+  handler: (args: any) => load(args).then(chainCmd(parse)).then(outputResult),
 }
 
 // construct typecheck commands with yargs
@@ -69,6 +71,37 @@ const typecheckCmd = {
   handler: (args: any) => load(args).then(chainCmd(parse)).then(chainCmd(typecheck)).then(outputResult),
 }
 
+const supportedTarges = ['tlaplus', 'json']
+// construct the compile subcommand
+const compileCmd = {
+  command: 'compile <input>',
+  desc: 'compile a Quint specification into the target, the output is written to stdout',
+  builder: (yargs: any) =>
+    defaultOpts(yargs)
+      .option('main', {
+        desc: 'name of the main module (by default, computed from filename)',
+        type: 'string',
+      })
+      .option('target', {
+        desc: `the compilation target. Supported values: ${supportedTarges.join(', ')}`,
+        type: 'string',
+        default: 'json',
+      })
+      .coerce('target', (target: string): string => {
+        if (!supportedTarges.includes(target)) {
+          fail(`Invalid option for --target: ${target}. Valid options: ${supportedTarges.join(', ')}`)
+        }
+        return target
+      })
+      .option('verbosity', {
+        desc: 'control how much output is produced (0 to 5)',
+        type: 'number',
+        default: verbosity.defaultLevel,
+      }),
+  handler: (args: any) =>
+    load(args).then(chainCmd(parse)).then(chainCmd(typecheck)).then(chainCmd(compile)).then(outputResult),
+}
+
 // construct repl commands with yargs
 const replCmd = {
   command: ['repl', '*'],
@@ -292,6 +325,7 @@ async function main() {
   await yargs(process.argv.slice(2))
     .command(parseCmd)
     .command(typecheckCmd)
+    .command(compileCmd)
     .command(replCmd)
     .command(runCmd)
     .command(testCmd)