Skip to content

Commit

Permalink
Add debug utility function
Browse files Browse the repository at this point in the history
The `debug` function is a utility designed to aid in debugging
specifications by allowing the spec developer to print out a
contextual message while executing a specification, whether in
a run or in a test, along with a formatted representation of a value.

This can be useful when trying to understand the state of
variables at specific points during the spec execution or
while tracking down issues.

The `debug` function has the following signature:

```
def debug(header: str, value: a) -> a
```

The `debug` function prints both header and the value on the same line,
preceded by a `>` character, and then returns the given value,
which makes it easy to debug nested expressions without
having the extract them into a variable first.

Example usage in the REPL:

```
>>> debug("a number:", 42)
> a number: 42
42

>>> debug("a record:", { foo: 32, bar: true })
> a record: { bar: true, foo: 32 }
{ bar: true, foo: 32 }

>>> debug("large record:", largeRecord)
> large record: {
  hello:
    {
      world:
        { foo: { bar: { baz: 42 }, toto: { tata: { tutu: "Hello, World" } } } }
    }
}
{
  hello:
    {
      world:
        { foo: { bar: { baz: 42 }, toto: { tata: { tutu: "Hello, World" } } } }
    }
}

>>> if (a * debug("nested", a + b) == 10) true else false
> nested 5
true
```
  • Loading branch information
romac committed Nov 24, 2023
1 parent 814fca6 commit e3e4bdc
Show file tree
Hide file tree
Showing 6 changed files with 27 additions and 0 deletions.
1 change: 1 addition & 0 deletions quint/src/effects/builtinSignatures.ts
Original file line number Diff line number Diff line change
Expand Up @@ -223,6 +223,7 @@ const otherOperators = [
{ name: 'reps', effect: parseAndQuantify('(Pure, (Read[r1]) => Read[r2] & Update[u]) => Read[r1, r2] & Update[u]') },
{ name: 'fail', effect: propagateComponents(['read', 'update'])(1) },
{ name: 'assert', effect: propagateComponents(['read'])(1) },
{ name: 'debug', effect: propagateComponents(['read'])(2) },
{
name: 'ite',
effect: parseAndQuantify('(Read[r1], Read[r2] & Update[u], Read[r3] & Update[u]) => Read[r1, r2, r3] & Update[u]'),
Expand Down
1 change: 1 addition & 0 deletions quint/src/ir/quintIr.ts
Original file line number Diff line number Diff line change
Expand Up @@ -140,6 +140,7 @@ export const builtinOpCodes = [
'chooseSome',
'concat',
'contains',
'debug',
'enabled',
'eq',
'eventually',
Expand Down
1 change: 1 addition & 0 deletions quint/src/names/base.ts
Original file line number Diff line number Diff line change
Expand Up @@ -196,6 +196,7 @@ export const builtinNames = [
'reps',
'fail',
'assert',
'debug',
'orKeep',
'mustChange',
'enabled',
Expand Down
12 changes: 12 additions & 0 deletions quint/src/runtime/impl/compilerImpl.ts
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,10 @@ import { RuntimeValue, RuntimeValueLambda, RuntimeValueVariant, rv } from './run
import { ErrorCode, QuintError } from '../../quintError'

import { inputDefName, lastTraceName } from '../compile'
import { prettyQuintEx, terminalWidth } from '../../graphics'
import { format } from '../../prettierimp'
import { unreachable } from '../../util'
import { zerog } from '../../idGenerator'
import { chunk } from 'lodash'

// Internal names in the compiler, which have special treatment.
Expand Down Expand Up @@ -914,6 +917,15 @@ export class CompilerVisitor implements IRVisitor {
this.translateAllOrThen(app)
break

case 'debug':
this.applyFun(app.id, 2, (header, value) => {
let columns = terminalWidth()
let valuePretty = format(columns, 0, prettyQuintEx(value.toQuintEx(zerog)))
console.log('>', header.toStr(), valuePretty.toString())
return just(value)
})
break

case 'fail':
this.applyFun(app.id, 1, result => {
return just(rv.mkBool(!result.toBool()))
Expand Down
1 change: 1 addition & 0 deletions quint/src/types/builtinSignatures.ts
Original file line number Diff line number Diff line change
Expand Up @@ -125,6 +125,7 @@ const otherOperators = [
{ name: 'reps', type: '(int, int => bool) => bool' },
{ name: 'fail', type: '(bool) => bool' },
{ name: 'assert', type: '(bool) => bool' },
{ name: 'debug', type: '(str, a) => a' },
]

function uniformArgsWithResult(argsType: string, resultType: string): Signature {
Expand Down
11 changes: 11 additions & 0 deletions quint/test/runtime/compile.test.ts
Original file line number Diff line number Diff line change
Expand Up @@ -978,6 +978,17 @@ describe('compiling specs to runtime values', () => {
evalVarAfterCall('n', 'run1', input).mapRight(m => assert.fail(`Expected an error, found: ${m}`))
})

it('debug', () => {
// `debug(s, a)` returns `a`
const input = dedent(
`var n: int
|run run1 = (n' = 1).then(n' = debug("n plus one", n + 1))
`
)

assertVarAfterCall('n', '2', 'run1', input)
})

it('unsupported operators', () => {
assertResultAsString('allLists(1.to(3))', undefined)

Expand Down

0 comments on commit e3e4bdc

Please sign in to comment.