Skip to content

Commit

Permalink
Merge pull request #1039 from informalsystems/gabriela/repl-module-on…
Browse files Browse the repository at this point in the history 
…ly-when-needed

Only create a `__repl__` module when a main module is not available
  • Loading branch information
@bugarela
bugarela authored Jul 12, 2023
2 parents 123a237 + 248cafd commit 7f814b7
Show file tree
Hide file tree
Showing 3 changed files with 87 additions and 100 deletions.
25 changes: 18 additions & 7 deletions quint/io-cli-tests.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -195,7 +195,6 @@ echo "init" | quint -r ../examples/language-features/counters.qnt::counters 2>&1

<!-- !test out repl loads a file and a module -->
```
>>> true
>>>
```
Expand All @@ -210,8 +209,7 @@ echo ".load ../examples/language-features/counters.qnt counters" \

<!-- !test out repl loads a file with .load -->
```
>>>
>>> >>>
>>> >>> >>>
```

### Repl saves a file with .save and loads it back
Expand All @@ -230,13 +228,29 @@ rm tmp-counters.qnt

<!-- !test out repl saves a file with .save and loads it back -->
```
>>> Session saved to: tmp-counters.qnt
>>> >>>
>>> true
>>>
```

### Repl loads a module directly without wrapping it in a new module

` MyF::ExportedBasics::double(2)` should be available only in the `G` module. If `G` is imported in a
`__repl__` module, this wouldn't work.

<!-- !test in repl loads a module directly -->
```
echo -e "init\nMyF::ExportedBasics::double(2)" | quint -r ../examples/language-features/imports.qnt::imports 2>&1 | tail -n +3
```

<!-- !test out repl loads a module directly -->
```
>>> true
>>> 4
>>>
```

### Tests works as expected

The command `test` finds failing tests and prints error messages.
Expand Down Expand Up @@ -379,7 +393,6 @@ EOF

<!-- !test out repl evaluates coin -->
```
>>> true
>>> Map("alice" -> 0, "bob" -> 0, "charlie" -> 0, "eve" -> 0, "null" -> 0)
>>>
Expand Down Expand Up @@ -755,7 +768,6 @@ echo "init" | quint -r ../examples/language-features/imports.qnt::imports 2>&1 |

<!-- !test out compile imports -->
```
>>> true
>>>
```
Expand All @@ -769,7 +781,6 @@ echo -e "A1::f(1)\nA2::f(1)" | quint -r ../examples/language-features/instances.

<!-- !test out compile instances -->
```
>>> 34
>>> 16
>>>
Expand Down
161 changes: 69 additions & 92 deletions quint/src/repl.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ import { version } from './version'
import { fileSourceResolver } from './parsing/sourceResolver'
import { cwd } from 'process'
import { newIdGenerator } from './idGenerator'
import { definitionToString } from './IRprinting'
import { moduleToString } from './IRprinting'
import { EvaluationState, newEvaluationState } from './runtime/impl/compilerImpl'

// tunable settings
Expand All @@ -56,8 +56,6 @@ type writer = (_text: string) => void
class ReplState {
// the history of module definitions loaded from external sources
moduleHist: string
// definitions history
defsHist: string
// expressions history (for saving and loading)
exprHist: string[]
// filename and module name that were loaded with .load filename module
Expand All @@ -69,29 +67,33 @@ class ReplState {

constructor(verbosityLevel: number, rng: Rng) {
this.moduleHist = ''
this.defsHist = ''
this.exprHist = []
this.lastLoadedFileAndModule = [undefined, undefined]
this.compilationState = this.newCompilationState()
this.compilationState = newCompilationState()
this.evaluationState = newEvaluationState(newTraceRecorder(verbosityLevel, rng))
}

clone() {
const copy = new ReplState(this.verbosity, newRng(this.rng.getState()))
copy.moduleHist = this.moduleHist
copy.defsHist = this.defsHist
copy.exprHist = this.exprHist
copy.lastLoadedFileAndModule = this.lastLoadedFileAndModule
copy.compilationState = this.compilationState
return copy
}

addReplModule() {
const replModule = { name: '__repl__', defs: simulatorBuiltins(this.compilationState), id: 0n }
this.compilationState.modules.push(replModule)
this.compilationState.originalModules.push(replModule)
this.moduleHist += moduleToString(replModule)
}

clear() {
this.moduleHist = ''
this.exprHist = []
this.compilationState = this.newCompilationState()
this.compilationState = newCompilationState()
this.evaluationState = newEvaluationState(newTraceRecorder(this.verbosity, this.rng))
this.defsHist = this.compilationState.modules[0].defs.map(def => definitionToString(def)).join('\n')
}

get recorder(): TraceRecorder {
Expand All @@ -118,14 +120,6 @@ class ReplState {
set seed(newSeed: bigint) {
this.rng.setState(newSeed)
}

private newCompilationState(): CompilationState {
// Introduce the __repl__ module to the compilation state so new expressions
// are pushed to it.
const state = newCompilationState()
const modules = [{ name: '__repl__', defs: simulatorBuiltins(state), id: 0n }]
return { ...state, modules: modules, originalModules: modules }
}
}

// The default exit terminates the process.
Expand Down Expand Up @@ -169,10 +163,6 @@ export function quintRepl(
// the state
const state: ReplState = new ReplState(options.verbosity, newRng())

// Add the builtins to the text history as well
state.defsHist = state.compilationState.modules[0].defs.map(def => definitionToString(def)).join('\n')

tryEvalHistory(out, state)
// we let the user type a multiline string, which is collected here:
let multilineText = ''
// when recyclingOwnOutput is true, REPL is receiving its older output
Expand Down Expand Up @@ -245,16 +235,37 @@ export function quintRepl(
// load the code from a filename and optionally import a module
function load(filename: string, moduleName: string | undefined) {
state.clear()
if (loadFromFile(out, state, filename)) {
state.lastLoadedFileAndModule[0] = filename
if (moduleName !== undefined) {
if (tryEvalAndClearRecorder(out, state, `import ${moduleName}.*`)) {
state.lastLoadedFileAndModule[1] = moduleName
} else {
out(chalk.yellow('Pick the right module name and import it (the file has been loaded)\n'))
}
}

const newState = loadFromFile(out, state, filename)
if (!newState) {
return state
}

state.lastLoadedFileAndModule[0] = filename

const moduleNameToLoad = moduleName ?? getMainModuleAnnotation(newState.moduleHist) ?? '__repl__'
if (moduleNameToLoad === '__repl__') {
// No module to load, introduce the __repl__ module
newState.addReplModule()
}

if (tryEvalModule(out, newState, moduleNameToLoad)) {
state.lastLoadedFileAndModule[1] = moduleNameToLoad
} else {
out(chalk.yellow('Pick the right module name and import it (the file has been loaded)\n'))
return newState
}

if (newState.exprHist) {
newState.exprHist.forEach(expr => {
tryEvalAndClearRecorder(out, newState, expr)
})
}

state.moduleHist = newState.moduleHist
state.exprHist = newState.exprHist
state.compilationState = newState.compilationState
state.evaluationState = newState.evaluationState
}

// the read-eval-print loop
Expand Down Expand Up @@ -393,20 +404,16 @@ export function quintRepl(
return rl
}

// private definitions
const replBegin = 'module __repl__ {'
const replEnd = '} //-- __repl__'

function saveToFile(out: writer, state: ReplState, filename: string) {
// 1. Write the previously loaded modules.
// 2. Write the definitions in the special module called __repl__.
// 3. Wrap expressions into special comments.
try {
const text =
`${state.moduleHist}
${replBegin}
${state.defsHist}
${replEnd}\n` + state.exprHist.map(s => `/*! ${s} !*/\n`).join('\n')
`// @mainModule ${state.lastLoadedFileAndModule[1]}\n` +
`${state.moduleHist}` +
state.exprHist.map(s => `/*! ${s} !*/\n`).join('\n')

writeFileSync(filename, text)
out(`Session saved to: ${filename}\n`)
} catch (error) {
Expand All @@ -415,53 +422,23 @@ ${replEnd}\n` + state.exprHist.map(s => `/*! ${s} !*/\n`).join('\n')
}
}

function loadFromFile(out: writer, state: ReplState, filename: string): boolean {
function loadFromFile(out: writer, state: ReplState, filename: string): ReplState | undefined {
try {
const data = readFileSync(filename, 'utf8')
const modules = readFileSync(filename, 'utf8')
const newState: ReplState = state.clone()
const modulesAndRepl = data.split(replBegin)
// whether an error occurred at some step
newState.moduleHist = modulesAndRepl[0]
if (modulesAndRepl.length > 1) {
// found a REPL session
const defsAndExprs = modulesAndRepl[1].split(replEnd)

// save the definition history
newState.defsHist = defsAndExprs[0]
const isError = !tryEvalHistory(out, newState)
if (isError) {
return false
}
newState.moduleHist = modules + newState.moduleHist

if (defsAndExprs.length > 1) {
// unwrap the expressions from the specially crafted comments
const exprs = (defsAndExprs[1] ?? '').matchAll(/\/\*! (.*?) !\*\//gms) ?? []
// and replay them one by one
// unwrap the expressions from the specially crafted comments
const exprs = Array.from((modules ?? '').matchAll(/\/\*! (.*?) !\*\//gms) ?? []).map(groups => groups[1])
// and replay them one by one

for (const groups of exprs) {
if (!tryEvalAndClearRecorder(out, newState, groups[1])) {
return false
}
}
}
} else {
const isError = !tryEvalHistory(out, newState)
if (isError) {
return false
}
}
newState.exprHist = exprs

state.moduleHist = newState.moduleHist
state.defsHist = newState.defsHist
state.exprHist = newState.exprHist
state.compilationState = newState.compilationState
state.evaluationState = newState.evaluationState

return true
return newState
} catch (error) {
out(chalk.red(error))
out('\n')
return false
return
}
}

Expand Down Expand Up @@ -516,24 +493,14 @@ function parseDefOrThrow(compilationState: CompilationState, text: string): Flat
}
}

// Compose the text input. This is not evaluated, it's only used to
// report errors, as the error locs are relative to the input.
function prepareModulesText(state: ReplState, textToAdd: string): string {
return `${state.moduleHist}
module __repl__ {
${state.defsHist}
${textToAdd}
}`
}

function tryEvalHistory(out: writer, state: ReplState): boolean {
const modulesText = prepareModulesText(state, '')
function tryEvalModule(out: writer, state: ReplState, mainName: string): boolean {
const modulesText = state.moduleHist
const mainPath = fileSourceResolver().lookupPath(cwd(), 'repl.ts')

const context = compileFromCode(
newIdGenerator(),
modulesText,
'__repl__',
mainName,
mainPath,
state.evaluationState.listener,
state.rng.next
Expand Down Expand Up @@ -569,6 +536,11 @@ function tryEvalAndClearRecorder(out: writer, state: ReplState, newInput: string

// try to evaluate the expression in a string and print it, if successful
function tryEval(out: writer, state: ReplState, newInput: string): boolean {
if (state.compilationState.modules.length === 0) {
state.addReplModule()
tryEvalModule(out, state, '__repl__')
}

const parseResult = parseExpressionOrUnit(
newInput,
'<input>',
Expand Down Expand Up @@ -628,7 +600,7 @@ function tryEval(out: writer, state: ReplState, newInput: string): boolean {
}

out('\n') // be nice to external programs
state.defsHist = state.defsHist + '\n' + newInput // update the history
state.moduleHist = state.moduleHist.slice(0, state.moduleHist.length - 1) + newInput + '\n}' // update the history

// Save compilation state
state.compilationState = context.compilationState
Expand All @@ -655,10 +627,10 @@ function printErrorMessages(
messages: ErrorMessage[],
color: (_text: string) => string = chalk.red
) {
const modulesText = prepareModulesText(state, inputText)
const modulesText = state.moduleHist + inputText
// display the error messages and highlight the error places
messages.forEach(e => {
const text = e.locs[0].source === '<input>' ? inputText : modulesText
const text = e.locs[0]?.source === '<input>' ? inputText : modulesText
const finder = lineColumn(text)
const msg = formatError(text, finder, e, none())
out(color(`${kind}: ${msg}\n`))
Expand Down Expand Up @@ -764,3 +736,8 @@ function evalExpr(state: ReplState, out: writer): Either<string, QuintEx> {
})
.join()
}

function getMainModuleAnnotation(moduleHist: string): string | undefined {
const moduleName = moduleHist.match(/^\/\/ @mainModule\s+(\w+)\n/)
return moduleName?.at(1)
}
1 change: 0 additions & 1 deletion tutorials/repl/replTestOut.txt
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@

4
Set(2, 4, 6)
32
Expand Down

0 comments on commit 7f814b7

Please sign in to comment.