From 6ea6f0bb6e3e93a82d7067f610f006a22a9898df Mon Sep 17 00:00:00 2001
From: Karl Meakin <karl.meakin@arm.com>
Date: Thu, 2 Feb 2023 14:05:52 +0000
Subject: [PATCH] Use strict evaluation in `fathom norm` and `fathom data`

---
 fathom/src/core/binary.rs |  6 +++---
 fathom/src/driver.rs      | 11 +++++++++--
 2 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/fathom/src/core/binary.rs b/fathom/src/core/binary.rs
index 26a9eda5a..8c8a0516b 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/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);