From 5a835d9db35bf76858e178e1bd66e60128879629 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 27 Jan 2020 18:45:09 +0000
Subject: Fix a bunch of bugs and more tck

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

(limited to 'dhall/src/semantics/tck/tyexpr.rs')

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index c8be3a3..a42265d 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -5,6 +5,7 @@ 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};
+use crate::semantics::tck::typecheck::TyEnv;
 use crate::semantics::Value;
 use crate::syntax::{ExprKind, Label, Span, V};
 
@@ -48,6 +49,15 @@ impl TyExpr {
     pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
         tyexpr_to_expr(self, opts, &mut Vec::new())
     }
+    pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
+        let opts = ToExprOptions {
+            normalize: true,
+            alpha: false,
+        };
+        let env = env.as_nameenv().names();
+        let mut env = env.iter().collect();
+        tyexpr_to_expr(self, opts, &mut env)
+    }
     // TODO: temporary hack
     pub fn to_value(&self) -> Value {
         todo!()
-- 
cgit v1.2.3