From 26d4975a4c94c2b9fd0c075ad94c2588e3cf24e8 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 29 Jan 2020 21:29:53 +0000
Subject: Use NameEnv in tyexpr_to_expr

---
 dhall/src/semantics/nze/nzexpr.rs | 31 ++++++++++++++-----------------
 dhall/src/semantics/tck/tyexpr.rs | 27 +++++++++------------------
 2 files changed, 23 insertions(+), 35 deletions(-)

diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs
index 043840e..7263cac 100644
--- a/dhall/src/semantics/nze/nzexpr.rs
+++ b/dhall/src/semantics/nze/nzexpr.rs
@@ -35,9 +35,6 @@ impl NameEnv {
             size: self.names.len(),
         }
     }
-    pub fn names(&self) -> &[Binder] {
-        &self.names
-    }
 
     pub fn insert(&self, x: &Binder) -> Self {
         let mut env = self.clone();
@@ -47,9 +44,9 @@ impl NameEnv {
     pub fn insert_mut(&mut self, x: &Binder) {
         self.names.push(x.clone())
     }
-    // pub fn remove_mut(&mut self) {
-    //     self.names.pop();
-    // }
+    pub fn remove_mut(&mut self) {
+        self.names.pop();
+    }
 
     pub fn unlabel_var(&self, var: &V<Binder>) -> Option<AlphaVar> {
         let V(name, idx) = var;
@@ -62,17 +59,17 @@ impl NameEnv {
             .nth(*idx)?;
         Some(AlphaVar::new(V((), idx)))
     }
-    // pub fn label_var(&self, var: &AlphaVar) -> V<Binder> {
-    //     let name = &self.names[self.names.len() - 1 - var.idx()];
-    //     let idx = self
-    //         .names
-    //         .iter()
-    //         .rev()
-    //         .take(var.idx())
-    //         .filter(|n| *n == name)
-    //         .count();
-    //     V(name.clone(), idx)
-    // }
+    pub fn label_var(&self, var: &AlphaVar) -> V<Binder> {
+        let name = &self.names[self.names.len() - 1 - var.idx()];
+        let idx = self
+            .names
+            .iter()
+            .rev()
+            .take(var.idx())
+            .filter(|n| *n == name)
+            .count();
+        V(name.clone(), idx)
+    }
 }
 
 // TODO: rename to VarEnv
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index abb6fa8..b64c519 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,12 +1,13 @@
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::core::var::AlphaVar;
+use crate::semantics::nze::nzexpr::NameEnv;
 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};
+use crate::syntax::{ExprKind, Span, V};
 
 pub(crate) type Type = Value;
 
@@ -46,15 +47,14 @@ impl TyExpr {
 
     /// Converts a value back to the corresponding AST expression.
     pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
-        tyexpr_to_expr(self, opts, &mut Vec::new())
+        tyexpr_to_expr(self, opts, &mut NameEnv::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();
+        let mut env = env.as_nameenv().clone();
         tyexpr_to_expr(self, opts, &mut env)
     }
 
@@ -77,30 +77,21 @@ impl TyExpr {
 fn tyexpr_to_expr<'a>(
     tyexpr: &'a TyExpr,
     opts: ToExprOptions,
-    ctx: &mut Vec<&'a Label>,
+    env: &mut NameEnv,
 ) -> NormalizedExpr {
     rc(match tyexpr.kind() {
         TyExprKind::Var(v) if opts.alpha => {
             ExprKind::Var(V("_".into(), v.idx()))
         }
-        TyExprKind::Var(v) => {
-            let name = ctx[ctx.len() - 1 - v.idx()];
-            let idx = ctx
-                .iter()
-                .rev()
-                .take(v.idx())
-                .filter(|l| **l == name)
-                .count();
-            ExprKind::Var(V(name.clone(), idx))
-        }
+        TyExprKind::Var(v) => ExprKind::Var(env.label_var(v)),
         TyExprKind::Expr(e) => {
             let e = e.map_ref_maybe_binder(|l, tye| {
                 if let Some(l) = l {
-                    ctx.push(l);
+                    env.insert_mut(l);
                 }
-                let e = tyexpr_to_expr(tye, opts, ctx);
+                let e = tyexpr_to_expr(tye, opts, env);
                 if let Some(_) = l {
-                    ctx.pop();
+                    env.remove_mut();
                 }
                 e
             });
-- 
cgit v1.2.3