diff --git a/fathom/src/core/binary.rs b/fathom/src/core/binary.rs index 856a203bc..958167723 100644 --- a/fathom/src/core/binary.rs +++ b/fathom/src/core/binary.rs @@ -7,7 +7,7 @@ use std::fmt::Debug; use std::slice::SliceIndex; use std::sync::Arc; -use super::semantics::LocalExprs; +use super::semantics::{EvalMode, LocalExprs}; use crate::core::semantics::{self, ArcValue, Elim, Head, LazyValue, Value}; use crate::core::{Const, Item, Module, Prim, Term, UIntStyle}; use crate::env::{EnvLen, SharedEnv, UniqueEnv}; @@ -284,7 +284,7 @@ impl<'arena, 'data> Context<'arena, 'data> { fn eval_env(&mut self) -> semantics::EvalEnv<'arena, '_> { let elim_env = semantics::ElimEnv::new(&self.item_exprs, [][..].into()); - semantics::EvalEnv::new(elim_env, &mut self.local_exprs) + semantics::EvalEnv::new(elim_env, &mut self.local_exprs).with_mode(EvalMode::Strict) } fn elim_env(&self) -> semantics::ElimEnv<'arena, '_> { @@ -296,7 +296,7 @@ impl<'arena, 'data> Context<'arena, 'data> { for item in module.items { match item { Item::Def { expr, .. } => { - let expr = self.eval_env().delay(expr); + let expr = self.eval_env().delay_or_eval(expr); self.item_exprs.push(expr); } } diff --git a/fathom/src/core/semantics.rs b/fathom/src/core/semantics.rs index a4cf0fb84..37923f045 100644 --- a/fathom/src/core/semantics.rs +++ b/fathom/src/core/semantics.rs @@ -20,6 +20,12 @@ pub type ArcValue<'arena> = Spanned>>; pub type LocalExprs<'arena> = SharedEnv>; pub type ItemExprs<'arena> = SliceEnv>; +#[derive(Debug, Copy, Clone, PartialEq, Eq)] +pub enum EvalMode { + Lazy, + Strict, +} + /// Values in weak-head-normal form, with bindings converted to closures. #[derive(Debug, Clone)] pub enum Value<'arena> { @@ -298,6 +304,7 @@ impl Error { /// Like the [`ElimEnv`], this allows for the running of computations, but /// also maintains a local environment, allowing for evaluation. pub struct EvalEnv<'arena, 'env> { + mode: EvalMode, elim_env: ElimEnv<'arena, 'env>, local_exprs: &'env mut LocalExprs<'arena>, } @@ -308,11 +315,23 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { local_exprs: &'env mut LocalExprs<'arena>, ) -> EvalEnv<'arena, 'env> { EvalEnv { + mode: EvalMode::Lazy, elim_env, local_exprs, } } + pub fn with_mode(self, mode: EvalMode) -> Self { + Self { mode, ..self } + } + + pub fn delay_or_eval(&mut self, term: &'arena Term<'arena>) -> LazyValue<'arena> { + match self.mode { + EvalMode::Lazy => self.delay(term), + EvalMode::Strict => LazyValue::eager(self.eval(term)), + } + } + pub fn delay(&self, term: &'arena Term<'arena>) -> LazyValue<'arena> { LazyValue::delay(self.local_exprs.clone(), term) } @@ -362,7 +381,7 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { } Term::Ann(span, expr, _) => Spanned::merge(*span, self.eval(expr)), Term::Let(span, _, _, def_expr, body_expr) => { - let def_expr = self.delay(def_expr); + let def_expr = self.delay_or_eval(def_expr); self.local_exprs.push(def_expr); let body_expr = self.eval(body_expr); self.local_exprs.pop(); @@ -376,7 +395,7 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { Arc::new(Value::FunType( *plicity, *param_name, - Arc::new(self.delay(param_type)), + Arc::new(self.delay_or_eval(param_type)), Closure::new(self.local_exprs.clone(), body_type), )), ), @@ -390,7 +409,7 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { ), Term::FunApp(span, plicity, head_expr, arg_expr) => { let head_expr = self.eval(head_expr); - let arg_expr = self.delay(arg_expr); + let arg_expr = self.delay_or_eval(arg_expr); Spanned::merge(*span, self.elim_env.fun_app(*plicity, head_expr, &arg_expr)) } @@ -399,7 +418,7 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { Spanned::new(*span, Arc::new(Value::RecordType(labels, types))) } Term::RecordLit(span, labels, exprs) => { - let exprs = exprs.iter().map(|expr| self.delay(expr)).collect(); + let exprs = exprs.iter().map(|expr| self.delay_or_eval(expr)).collect(); Spanned::new(*span, Arc::new(Value::RecordLit(labels, exprs))) } Term::RecordProj(span, head_expr, label) => { @@ -408,7 +427,7 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { } Term::ArrayLit(span, exprs) => { - let exprs = exprs.iter().map(|expr| self.delay(expr)).collect(); + let exprs = exprs.iter().map(|expr| self.delay_or_eval(expr)).collect(); Spanned::new(*span, Arc::new(Value::ArrayLit(exprs))) } @@ -417,7 +436,7 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { Spanned::new(*span, Arc::new(Value::FormatRecord(labels, formats))) } Term::FormatCond(span, name, format, cond) => { - let format = Arc::new(self.delay(format)); + let format = Arc::new(self.delay_or_eval(format)); let cond_expr = Closure::new(self.local_exprs.clone(), cond); Spanned::new(*span, Arc::new(Value::FormatCond(*name, format, cond_expr))) } diff --git a/fathom/src/driver.rs b/fathom/src/driver.rs index e8fe7c931..5db27e069 100644 --- a/fathom/src/driver.rs +++ b/fathom/src/driver.rs @@ -7,6 +7,7 @@ use codespan_reporting::files::SimpleFiles; use codespan_reporting::term::termcolor::{BufferedStandardStream, ColorChoice, WriteColor}; use crate::core::binary::{self, BufferError, ReadError}; +use crate::core::semantics::EvalMode; use crate::files::{FileId, Files}; use crate::source::{ByteRange, ProgramSource, SourceTooBig, Span, StringInterner, MAX_SOURCE_LEN}; use crate::surface::elaboration::ItemEnv; @@ -269,8 +270,14 @@ impl<'surface, 'core> Driver<'surface, 'core> { return Status::Error; } - let term = context.eval_env().normalize(&self.core_scope, &term); - let r#type = context.eval_env().normalize(&self.core_scope, &r#type); + let term = context + .eval_env() + .with_mode(EvalMode::Strict) + .normalize(&self.core_scope, &term); + let r#type = context + .eval_env() + .with_mode(EvalMode::Strict) + .normalize(&self.core_scope, &r#type); self.surface_scope.reset(); // Reuse the surface scope for distillation let mut context = context.distillation_context(&self.surface_scope);