Skip to content

Commit

Permalink
reformat the code
Browse files Browse the repository at this point in the history
  • Loading branch information
konnov committed Sep 12, 2023
1 parent 466f841 commit aed68e9
Show file tree
Hide file tree
Showing 4 changed files with 9 additions and 11 deletions.
6 changes: 2 additions & 4 deletions quint/src/graphics.ts
Original file line number Diff line number Diff line change
Expand Up @@ -268,10 +268,8 @@ export function printExecutionFrameRec(box: ConsoleBox, frame: ExecutionFrame, i

// format the call with its arguments and place it right after the tree art
let argsDoc =
(frame.args.length === 0)
? text('')
: group(textify(['(', nest(' ', [linebreak, group(args)]), linebreak, ')']))
// draw proper branches in the indentation
frame.args.length === 0 ? text('') : group(textify(['(', nest(' ', [linebreak, group(args)]), linebreak, ')']))
// draw proper branches in the indentation
const indentTreeArt = isLast.map(il => (il ? ' ' : '│ ')).join('')
// pretty print the arguments and the result
const callDoc = group(
Expand Down
4 changes: 2 additions & 2 deletions quint/src/runtime/impl/compilerImpl.ts
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ import { unreachable } from '../../util'
// Internal names in the compiler, which have special treatment.
// For some reason, if we replace 'q::input' with inputDefName, everything breaks.
// What kind of JS magic is that?
const specialNames = [ 'q::input', 'q::runResult', 'q::nruns', 'q::nsteps', 'q::init', 'q::next', 'q::inv' ]
const specialNames = ['q::input', 'q::runResult', 'q::nruns', 'q::nsteps', 'q::init', 'q::next', 'q::inv']

/**
* Returns a Map containing the built-in Computable objects for the Quint language.
Expand Down Expand Up @@ -255,7 +255,7 @@ export class CompilerVisitor implements IRVisitor {
// Both input1 and input2 wrap step, but in their individual computables.
const unwrappedValue = boundValue
const app: ir.QuintApp = { id: opdef.id, kind: 'app', opcode: opdef.name, args: [] }
const evalApp: ir.QuintApp = { id: 0n, kind: 'app', opcode: '_', args: [ app ] }
const evalApp: ir.QuintApp = { id: 0n, kind: 'app', opcode: '_', args: [app] }
boundValue = {
eval: () => {
if (app.opcode === inputDefName) {
Expand Down
8 changes: 4 additions & 4 deletions quint/src/runtime/trace.ts
Original file line number Diff line number Diff line change
Expand Up @@ -21,10 +21,10 @@ import { rv } from './impl/runtimeValue'
* A snapshot of how a single operator (e.g., an action) was executed.
* In stack-based languages, this usually corresponds to a stack frame.
* In Quint, it is simply the applied operator and the arguments.
*
*
* In addition to that, we use a top-level execution frame to represent
* the execution history:
*
*
* - `subframes` stores the executed actions, e.g., `init` and `step`
* - `result` stores the result of the overall computation:
* just(false), just(true), or none().
Expand Down Expand Up @@ -228,7 +228,7 @@ class TraceRecorderImpl implements TraceRecorder {
const newFrame = { app: app, args: [], result: none(), subframes: [] }
if (this.frameStack.length == 0) {
// this should not happen, as there is always bottomFrame, but let's handle it
this.frameStack = [ newFrame ]
this.frameStack = [newFrame]
} else if (this.frameStack.length === 2 && this.frameStack[1].app.opcode === '_') {
// A placeholder frame created from `q::input` or `then`. Modify in place.
const frame = this.frameStack[1]
Expand Down Expand Up @@ -309,7 +309,7 @@ class TraceRecorderImpl implements TraceRecorder {
const dummy: QuintApp = { id: 0n, kind: 'app', opcode: '_', args: [] }
const newFrame = { app: dummy, args: [], result: none(), subframes: [] }
// forget the frames, except the bottom one, and push the new one
this.frameStack = [ this.frameStack[0], newFrame ]
this.frameStack = [this.frameStack[0], newFrame]
// connect the new frame to the topmost frame, which effects in a new step
this.frameStack[0].subframes.push(newFrame)
}
Expand Down
2 changes: 1 addition & 1 deletion quint/test/repl.test.ts
Original file line number Diff line number Diff line change
Expand Up @@ -665,7 +665,7 @@ describe('repl ok', () => {
|>>> `
)
await assertRepl(input, output)
})
})

it('run q::test, q::testOnce, and q::lastTrace', async () => {
const input = dedent(
Expand Down

0 comments on commit aed68e9

Please sign in to comment.