Skip to content

Commit 6ea6f0b

Browse files
committed
Use strict evaluation in fathom norm and fathom data
1 parent 7a11837 commit 6ea6f0b

File tree

2 files changed

+12
-5
lines changed

2 files changed

+12
-5
lines changed

fathom/src/core/binary.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ use std::fmt::Debug;
77
use std::slice::SliceIndex;
88
use std::sync::Arc;
99

10-
use super::semantics::LocalExprs;
10+
use super::semantics::{EvalMode, LocalExprs};
1111
use crate::core::semantics::{self, ArcValue, Elim, Head, LazyValue, Value};
1212
use crate::core::{Const, Item, Module, Prim, Term, UIntStyle};
1313
use crate::env::{EnvLen, SharedEnv, UniqueEnv};
@@ -284,7 +284,7 @@ impl<'arena, 'data> Context<'arena, 'data> {
284284

285285
fn eval_env(&mut self) -> semantics::EvalEnv<'arena, '_> {
286286
let elim_env = semantics::ElimEnv::new(&self.item_exprs, [][..].into());
287-
semantics::EvalEnv::new(elim_env, &mut self.local_exprs)
287+
semantics::EvalEnv::new(elim_env, &mut self.local_exprs).with_mode(EvalMode::Strict)
288288
}
289289

290290
fn elim_env(&self) -> semantics::ElimEnv<'arena, '_> {
@@ -296,7 +296,7 @@ impl<'arena, 'data> Context<'arena, 'data> {
296296
for item in module.items {
297297
match item {
298298
Item::Def { expr, .. } => {
299-
let expr = self.eval_env().delay(expr);
299+
let expr = self.eval_env().delay_or_eval(expr);
300300
self.item_exprs.push(expr);
301301
}
302302
}

fathom/src/driver.rs

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ use codespan_reporting::files::SimpleFiles;
77
use codespan_reporting::term::termcolor::{BufferedStandardStream, ColorChoice, WriteColor};
88

99
use crate::core::binary::{self, BufferError, ReadError};
10+
use crate::core::semantics::EvalMode;
1011
use crate::files::{FileId, Files};
1112
use crate::source::{ByteRange, ProgramSource, SourceTooBig, Span, StringInterner, MAX_SOURCE_LEN};
1213
use crate::surface::elaboration::ItemEnv;
@@ -269,8 +270,14 @@ impl<'surface, 'core> Driver<'surface, 'core> {
269270
return Status::Error;
270271
}
271272

272-
let term = context.eval_env().normalize(&self.core_scope, &term);
273-
let r#type = context.eval_env().normalize(&self.core_scope, &r#type);
273+
let term = context
274+
.eval_env()
275+
.with_mode(EvalMode::Strict)
276+
.normalize(&self.core_scope, &term);
277+
let r#type = context
278+
.eval_env()
279+
.with_mode(EvalMode::Strict)
280+
.normalize(&self.core_scope, &r#type);
274281

275282
self.surface_scope.reset(); // Reuse the surface scope for distillation
276283
let mut context = context.distillation_context(&self.surface_scope);

0 commit comments

Comments
 (0)