Fix REPL issue when evaluating a variable that was never referenced

quint/src/repl.ts

@@ -272,26 +272,28 @@ export function quintRepl(
 
     const newState = loadFromFile(out, state, filename)
     if (!newState) {
-      return state
+      return
     }
 
     state.lastLoadedFileAndModule[0] = filename
 
-    const moduleNameToLoad = moduleName ?? getMainModuleAnnotation(newState.moduleHist) ?? '__repl__'
-    if (moduleNameToLoad === '__repl__') {
+    const moduleNameToLoad = moduleName ?? getMainModuleAnnotation(newState.moduleHist)
+    if (!moduleNameToLoad) {
       // No module to load, introduce the __repl__ module
       newState.addReplModule()
     }
 
-    if (tryEvalModule(out, newState, moduleNameToLoad)) {
+    if (tryEvalModule(out, newState, moduleNameToLoad ?? '__repl__')) {
       state.lastLoadedFileAndModule[1] = moduleNameToLoad
     } else {
       out(chalk.yellow('Pick the right module name and import it (the file has been loaded)\n'))
-      return newState
+      return
     }
 
     if (newState.exprHist) {
-      newState.exprHist.forEach(expr => {
+      const expressionsToEvaluate = newState.exprHist
+      newState.exprHist = []
+      expressionsToEvaluate.forEach(expr => {
         tryEvalAndClearRecorder(out, newState, expr)
       })
     }
@@ -441,13 +443,14 @@ export function quintRepl(
 
 function saveToFile(out: writer, state: ReplState, filename: string) {
   // 1. Write the previously loaded modules.
-  // 2. Write the definitions in the special module called __repl__.
+  // 2. Write the definitions in the loaded module (or in __repl__ if no module was loaded).
   // 3. Wrap expressions into special comments.
   try {
-    const text =
-      `// @mainModule ${state.lastLoadedFileAndModule[1]}\n` +
-      `${state.moduleHist}` +
-      state.exprHist.map(s => `/*! ${s} !*/\n`).join('\n')
+    const mainModuleAnnotation = state.moduleHist.startsWith('// @mainModule')
+      ? ''
+      : `// @mainModule ${state.lastLoadedFileAndModule[1] ?? '__repl__'}\n`
+
+    const text = mainModuleAnnotation + `${state.moduleHist}` + state.exprHist.map(s => `/*! ${s} !*/\n`).join('\n')
 
     writeFileSync(filename, text)
     out(`Session saved to: ${filename}\n`)
@@ -572,6 +575,7 @@ function tryEval(out: writer, state: ReplState, newInput: string): boolean {
       return false
     }
 
+    state.exprHist.push(newInput.trim())
     const evalResult = state.evaluator.evaluate(parseResult.expr)
 
     evalResult.map(ex => {
@@ -616,6 +620,7 @@ function tryEval(out: writer, state: ReplState, newInput: string): boolean {
     if (state.nameResolver.errors.length > 0) {
       printErrorMessages(out, state, 'static analysis error', newInput, state.nameResolver.errors)
       out('\n')
+
       parseResult.decls.forEach(decl => {
         if (isDef(decl)) {
           state.nameResolver.collector.deleteDefinition(decl.name)
@@ -644,6 +649,7 @@ function tryEval(out: writer, state: ReplState, newInput: string): boolean {
     }
 
     state.compilationState.analysisOutput = analysisOutput
+    state.moduleHist = state.moduleHist.slice(0, state.moduleHist.length - 1) + newInput + '\n}' // update the history
 
     out('\n')
   }

quint/src/runtime/impl/builder.ts

@@ -23,7 +23,7 @@ import { QuintError } from '../../quintError'
 import { RuntimeValue, rv } from './runtimeValue'
 import { builtinLambda, builtinValue, lazyBuiltinLambda, lazyOps } from './builtins'
 import { CachedValue, Context, Register } from './Context'
-import { QuintApp, QuintEx } from '../../ir/quintIr'
+import { QuintApp, QuintEx, QuintVar } from '../../ir/quintIr'
 import { LookupDefinition, LookupTable } from '../../names/base'
 import { NamedRegister, VarStorage, initialRegisterValue } from './VarStorage'
 import { List } from 'immutable'
@@ -85,15 +85,16 @@ export class Builder {
   /**
    * Gets the register for a variable by its id and the namespaces in scope (tracked by this builder).
    *
-   * @param id
+   * @param def - The variable to get the register for.
    *
    * @returns the register for the variable
    */
-  getVar(id: bigint): NamedRegister {
-    const key = [id, ...this.namespaces].join('#')
+  getVar(def: QuintVar): NamedRegister {
+    const key = [def.id, ...this.namespaces].join('#')
     const result = this.varStorage.vars.get(key)
     if (!result) {
-      throw new Error(`Variable not found: ${key}`)
+      this.discoverVar(def.id, def.name)
+      return this.varStorage.vars.get(key)!
     }
 
     return result
@@ -341,7 +342,7 @@ function buildDefCore(builder: Builder, def: LookupDefinition): EvalFunction {
     case 'var': {
       // Every variable has a single register, and we just change this register's value at each state
       // So, a reference to a variable simply evaluates to the value of the register.
-      const register = builder.getVar(def.id)
+      const register = builder.getVar(def)
       return _ => {
         return register.value
       }