Implement basic env-based normalization for Value-based TyExpr

1 files changed, 8 insertions, 0 deletions

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 983f3f8..c8be3a3 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,6 +1,7 @@
 #![allow(dead_code)]
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::core::var::AlphaVar;
+use crate::semantics::phase::normalize::{normalize_tyexpr_whnf, NzEnv};
 use crate::semantics::phase::typecheck::rc;
 use crate::semantics::phase::Normalized;
 use crate::semantics::phase::{NormalizedExpr, ToExprOptions};
@@ -51,6 +52,13 @@ impl TyExpr {
     pub fn to_value(&self) -> Value {
         todo!()
     }
+
+    pub fn normalize_whnf(&self, env: &NzEnv) -> Value {
+        normalize_tyexpr_whnf(self, env)
+    }
+    pub fn normalize_whnf_noenv(&self) -> Value {
+        normalize_tyexpr_whnf(self, &NzEnv::new())
+    }
 }
 
 fn tyexpr_to_expr<'a>(