Use strict evaluation in fathom norm and fathom data

yeslogic · Feb 2, 2023 · a1ff667 · a1ff667
1 parent bbc11e8
commit a1ff667
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 5 deletions.
diff --git 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/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);