Use strict evaluation in fathom norm and fathom data

Author: Kmeakin

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);
                 }
             }

fathom/src/core/semantics.rs

@@ -20,6 +20,12 @@ pub type ArcValue<'arena> = Spanned<Arc<Value<'arena>>>;
 pub type LocalExprs<'arena> = SharedEnv<LazyValue<'arena>>;
 pub type ItemExprs<'arena> = SliceEnv<LazyValue<'arena>>;
 
+#[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)))
             }

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);