From 0682a84eadc383e1d5747576298c9160737e0e99 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 18 Apr 2019 22:20:40 +0200
Subject: Label is redundant in EnvItem::Skip

---
 dhall/src/normalize.rs | 52 +++++++++++++++++++++++---------------------------
 dhall/src/typecheck.rs |  5 +++--
 2 files changed, 27 insertions(+), 30 deletions(-)

(limited to 'dhall/src')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 4dc5156..7a9ca2f 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -216,34 +216,10 @@ where
     Continue(ExprF::App(ret, rest))
 }
 
-// Small enum to help with being DRY
-enum WhatNext<'a, N, E> {
-    // Recurse on this expression
-    Continue(Expr<N, E>),
-    // The following expression is the normal form
-    Done(Expr<N, E>),
-    DoneRef(&'a Expr<N, E>),
-    DoneSub(SubExpr<N, E>),
-    DoneRefSub(&'a SubExpr<N, E>),
-    // The current expression is already in normal form
-    DoneAsIs,
-}
-
 #[derive(Debug, Clone)]
 enum EnvItem {
     Expr(SubExpr<X, X>),
-    Skip(Label, usize),
-}
-
-impl EnvItem {
-    fn shift0(&self, delta: isize, label: &Label) -> Self {
-        use EnvItem::*;
-        match self {
-            Expr(e) => Expr(shift0(delta, label, e)),
-            Skip(l, n) if l == label => Skip(l.clone(), *n + 1),
-            Skip(l, n) => Skip(l.clone(), *n),
-        }
-    }
+    Skip(usize),
 }
 
 struct NormalizationContext(Context<Label, EnvItem>);
@@ -258,20 +234,40 @@ impl NormalizationContext {
     fn skip(&self, x: &Label) -> NormalizationContext {
         NormalizationContext(
             self.0
-                .map(|e| e.shift0(1, x))
-                .insert(x.clone(), EnvItem::Skip(x.clone(), 0)),
+                .map(|l, e| {
+                    use EnvItem::*;
+                    match e {
+                        Expr(e) => Expr(shift0(1, x, e)),
+                        Skip(n) if l == x => Skip(*n + 1),
+                        Skip(n) => Skip(*n),
+                    }
+                })
+                .insert(x.clone(), EnvItem::Skip(0)),
         )
     }
     fn lookup(&self, var: &V<Label>) -> SubExpr<X, X> {
         let V(x, n) = var;
         match self.0.lookup(x, *n) {
             Some(EnvItem::Expr(e)) => e.clone(),
-            Some(EnvItem::Skip(_, m)) => rc(ExprF::Var(V(x.clone(), *m))),
+            Some(EnvItem::Skip(m)) => rc(ExprF::Var(V(x.clone(), *m))),
             None => rc(ExprF::Var(V(x.clone(), *n))),
         }
     }
 }
 
+// Small enum to help with being DRY
+enum WhatNext<'a, N, E> {
+    // Recurse on this expression
+    Continue(Expr<N, E>),
+    // The following expression is the normal form
+    Done(Expr<N, E>),
+    DoneRef(&'a Expr<N, E>),
+    DoneSub(SubExpr<N, E>),
+    DoneRefSub(&'a SubExpr<N, E>),
+    // The current expression is already in normal form
+    DoneAsIs,
+}
+
 fn normalize_value(
     ctx: &NormalizationContext,
     expr: SubExpr<X, Normalized<'static>>,
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 186384d..65128cd 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -378,7 +378,8 @@ fn type_with(
     let ret = match e.as_ref() {
         Lam(x, t, b) => {
             let t = mktype(ctx, t.clone())?;
-            let ctx2 = ctx.insert(x.clone(), t.clone()).map(|e| e.shift0(1, x));
+            let ctx2 =
+                ctx.insert(x.clone(), t.clone()).map(|_, e| e.shift0(1, x));
             let b = type_with(&ctx2, b.clone())?;
             Ok(RetExpr(Pi(
                 x.clone(),
@@ -394,7 +395,7 @@ fn type_with(
             );
 
             let ctx2 =
-                ctx.insert(x.clone(), ta.clone()).map(|e| e.shift0(1, x));
+                ctx.insert(x.clone(), ta.clone()).map(|_, e| e.shift0(1, x));
             let tb = type_with(&ctx2, tb.clone())?;
             let kB = ensure_is_const!(
                 &tb.get_type()?,
-- 
cgit v1.2.3