Add non-strict evaluation in the program module
//! [`mk_global_env`](./struct.Program.html#method.mk_global_env)). Each such value is added to
//! the global environment before the evaluation of the program.
use crate::error::{Error, ImportError, ParseError, ToDiagnostic, TypecheckError};
+use crate::identifier::Ident;
use crate::parser::lexer::Lexer;
use crate::position::RawSpan;
use crate::stdlib as nickel_stdlib;
-use crate::term::{RichTerm, Term};
+use crate::term::{MetaValue, RichTerm, Term};
use crate::typecheck::type_check;
use crate::types::Types;
use crate::{eval, parser, transformations};
@@ -259,6 +260,41 @@ impl Program {
eval::eval_full(t, &global_env, self).map_err(|e| e.into())
}
+ /// Parse if necessary, typecheck, and evaluate the program until a metavalue is encountered.
+ ///
+ /// As opposed to normal evaluation, it does not try to unwrap the content of a metavalue: the
+ /// evaluation stops as soon as a metavalue is encountered.
+ pub fn eval_meta(&mut self, path: Option<String>) -> Result<Option<MetaValue>, Error> {
+ let (t, global_env) = self.prepare_eval()?;
+
+ let t = if let Some(p) = path {
+ // Parsing `hole.path`
+ let hole = "hole___";
+ let source = format!("{}.{}", hole, p);
+ let file_id = self.files.add("<query path>", source.clone());
+ let new_term = parser::grammar::TermParser::new()
+ .parse(file_id, Lexer::new(&source))
+ .map_err(|err| ParseError::from_lalrpop(err, file_id))?;
+
+ // Substituting `___HOLE` for `t`
+ let mut env = eval::Environment::new();
+ let closure = eval::Closure {
+ body: t,
+ env: eval::Environment::new(),
+ };
+ env.insert(
+ Ident::from(hole),
+ (Rc::new(RefCell::new(closure)), eval::IdentKind::Let()),
+ );
+
+ eval::subst(new_term, &eval::Environment::new(), &env)
+ } else {
+ t
+ };
+
+ Ok(eval::eval_meta(t, &global_env, self)?)
+ }
+
pub fn typecheck(&mut self) -> Result<Types, Error> {
let t = self.parse_with_cache(self.main_id)?;
let global_env = self.mk_global_env()?;
