diff options
| -rw-r--r-- | dhall/src/semantics/phase/mod.rs | 4 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/tyexpr.rs | 10 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 12 |
3 files changed, 16 insertions, 10 deletions
diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 0f8194c..2727a61 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -102,9 +102,7 @@ impl Resolved { impl Typed { /// Reduce an expression to its normal form, performing beta reduction pub fn normalize(&self) -> Normalized { - let mut val = self.0.normalize_whnf_noenv(); - val.normalize_mut(); - Normalized(val) + Normalized(self.0.normalize_nf_noenv()) } /// Converts a value back to the corresponding AST expression. diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 9e8dc47..e4108ad 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -67,7 +67,15 @@ impl TyExpr { normalize_tyexpr_whnf(self, env) } pub fn normalize_whnf_noenv(&self) -> Value { - normalize_tyexpr_whnf(self, &NzEnv::new()) + self.normalize_whnf(&NzEnv::new()) + } + pub fn normalize_nf(&self, env: &NzEnv) -> Value { + let mut val = self.normalize_whnf(env); + val.normalize_mut(); + val + } + pub fn normalize_nf_noenv(&self) -> Value { + self.normalize_nf(&NzEnv::new()) } } diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 5880d92..abb36e1 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -150,7 +150,7 @@ fn type_one_layer( text_type } ExprKind::EmptyListLit(t) => { - let t = t.normalize_whnf(env.as_nzenv()); + let t = t.normalize_nf(env.as_nzenv()); match &*t.as_whnf() { ValueKind::AppliedBuiltin(Builtin::List, args, _, _) if args.len() == 1 => {} @@ -250,7 +250,7 @@ fn type_one_layer( }, // TODO: branch here only when scrut.get_type() is a Const _ => { - let scrut_nf = scrut.normalize_whnf(env.as_nzenv()); + let scrut_nf = scrut.normalize_nf(env.as_nzenv()); let scrut_nf_borrow = scrut_nf.as_whnf(); match &*scrut_nf_borrow { ValueKind::UnionType(kts) => match kts.get(x) { @@ -324,7 +324,7 @@ fn type_one_layer( )); } - let arg_nf = arg.normalize_whnf(env.as_nzenv()); + let arg_nf = arg.normalize_nf(env.as_nzenv()); closure.apply(arg_nf) } _ => return mkerr(format!("apply to not Pi: {:?}", tf_borrow)), @@ -387,7 +387,7 @@ fn type_one_layer( ); let ty = type_one_layer(env, &ekind)?; TyExpr::new(TyExprKind::Expr(ekind), Some(ty), Span::Artificial) - .normalize_whnf(env.as_nzenv()) + .normalize_nf(env.as_nzenv()) } ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => { let x_val = x.normalize_whnf(env.as_nzenv()); @@ -622,7 +622,7 @@ pub(crate) fn type_with( }, ExprKind::Lam(binder, annot, body) => { let annot = type_with(env, annot)?; - let annot_nf = annot.normalize_whnf(env.as_nzenv()); + let annot_nf = annot.normalize_nf(env.as_nzenv()); let body_env = env.insert_type(&binder, annot_nf.clone()); let body = type_with(&body_env, body)?; let body_ty = body.get_type()?; @@ -660,7 +660,7 @@ pub(crate) fn type_with( }; let val = type_with(env, &val)?; - let val_nf = val.normalize_whnf(&env.as_nzenv()); + let val_nf = val.normalize_nf(&env.as_nzenv()); let body = type_with(&env.insert_value(&binder, val_nf), body)?; let body_ty = body.get_type().ok(); ( |