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