From 11f1969176f2d8fbc6f8977ee242da546b0c2feb Mon Sep 17 00:00:00 2001 From: Yann Hamdaoui Date: Fri, 8 Mar 2024 16:34:53 +0100 Subject: [PATCH] Fix unbound identifier when querying in REPL Following a refactoring that landed in 1.4, the current environment of a REPL session wasn't taken into account when querying an expression. This mean that any value introduced by a toplevel let during the session would evaluate fine but raise an unbound identifier error if one tries to query it with `:query some_id`. This commit fixes this by correctly propagating the environment in the subfunctions involved in querying. --- core/src/eval/mod.rs | 44 ++++++++++++++++++++++---------------------- core/src/program.rs | 8 +++++--- 2 files changed, 27 insertions(+), 25 deletions(-) diff --git a/core/src/eval/mod.rs b/core/src/eval/mod.rs index 2ef753c02..6ebd951db 100644 --- a/core/src/eval/mod.rs +++ b/core/src/eval/mod.rs @@ -256,36 +256,36 @@ impl VirtualMachine { /// /// For example, extracting `foo.bar.baz` on a term `exp` will evaluate `exp` to a record and /// try to extract the field `foo`. If anything goes wrong (the result isn't a record or the - /// field `bar` doesn't exist), a proper error is raised. Otherwise, [Self::extract_field] - /// applies the same recipe recursively and evaluate the content of the `foo` field extracted - /// from `exp` to a record, tries to extract `bar`, and so on. - pub fn extract_field( + /// field `bar` doesn't exist), a proper error is raised. Otherwise, + /// [Self::extract_field_closure] applies the same recipe recursively and evaluate the content + /// of the `foo` field extracted from `exp` to a record, tries to extract `bar`, and so on. + pub fn extract_field_closure( &mut self, - t: RichTerm, + closure: Closure, path: &FieldPath, ) -> Result<(Field, Environment), EvalError> { - self.extract_field_impl(t, path, false) + self.extract_field_impl(closure, path, false) } - /// Same as [Self::extract_field], but also requires that the field value is defined and - /// returns the value directly. + /// Same as [Self::extract_field_closure], but also requires that the field value is defined + /// and returns the value directly. /// /// This method also applies potential pending contracts to the value. /// /// In theory, extracting the value could be done manually after calling to - /// [Self::extract_field], instead of needing a separate method. + /// [Self::extract_field_closure], instead of needing a separate method. /// - /// However, once [Self::extract_field] returns, most contextual information required to raise - /// a proper error if the field is missing (e.g. positions) has been lost. So, if the returned - /// field's value is `None`, we would have a hard time reporting a good error message. On the - /// other hand, [Self::extract_field_value] raises the error earlier, when the context is still - /// available. - pub fn extract_field_value( + /// However, once [Self::extract_field_closure] returns, most contextual information required + /// to raise a proper error if the field is missing (e.g. positions) has been lost. So, if the + /// returned field's value is `None`, we would have a hard time reporting a good error message. + /// On the other hand, [Self::extract_field_value_closure] raises the error earlier, when the + /// context is still available. + pub fn extract_field_value_closure( &mut self, - t: RichTerm, + closure: Closure, path: &FieldPath, ) -> Result { - let (field, env) = self.extract_field_impl(t, path, true)?; + let (field, env) = self.extract_field_impl(closure, path, true)?; // unwrap(): by definition, extract_field_impl(_, _, true) ensure that // `field.value.is_some()` @@ -305,15 +305,15 @@ impl VirtualMachine { fn extract_field_impl( &mut self, - t: RichTerm, + closure: Closure, path: &FieldPath, require_defined: bool, ) -> Result<(Field, Environment), EvalError> { - let mut prev_pos = t.pos; + let mut prev_pos = closure.body.pos; - let mut field: Field = t.into(); + let mut field: Field = closure.body.into(); let mut path = path.0.iter().peekable(); - let mut env = Environment::new(); + let mut env = closure.env; let Some(mut prev_id) = path.peek().cloned() else { return Ok((field, env)); @@ -399,7 +399,7 @@ impl VirtualMachine { ) -> Result { // extract_field does almost what we want, but for querying, we evaluate the content of the // field as well in order to print a potential default value. - let (mut field, env) = self.extract_field(closure.body, path)?; + let (mut field, env) = self.extract_field_closure(closure, path)?; if let Some(value) = field.value.take() { let pos = value.pos; diff --git a/core/src/program.rs b/core/src/program.rs index ce238755c..0325345ad 100644 --- a/core/src/program.rs +++ b/core/src/program.rs @@ -343,7 +343,7 @@ impl Program { fn prepare_eval_impl(&mut self, for_query: bool) -> Result { // If there are no overrides, we avoid the boilerplate of creating an empty record and // merging it with the current program - let prepared = if self.overrides.is_empty() { + let prepared_body = if self.overrides.is_empty() { self.vm.prepare_eval(self.main_id)? } else { let mut record = builder::Record::new(); @@ -372,10 +372,12 @@ impl Program { mk_term::op2(BinaryOp::Merge(Label::default().into()), t, built_record) }; + let prepared = Closure::atomic_closure(prepared_body); + let result = if for_query { - Closure::atomic_closure(prepared) + prepared } else { - self.vm.extract_field_value(prepared, &self.field)? + self.vm.extract_field_value_closure(prepared, &self.field)? }; Ok(result)