From 9e7cc77b6a25569b61340f39a2058e23cdc4a437 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 23 Jan 2020 22:22:01 +0000
Subject: Implement basic env-based normalization for Value-based TyExpr

---
 dhall/src/semantics/tck/tyexpr.rs | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'dhall/src/semantics/tck')

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>(
-- 
cgit v1.2.3