From 5f0d69671b44ba1dff6becb9ebc7f6e74241e3e2 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 16 Aug 2019 18:14:55 +0200
Subject: Remove dead code

---
 dhall/src/core/context.rs    | 31 -----------------------
 dhall/src/core/thunk.rs      | 59 +++++++++++++-------------------------------
 dhall/src/core/value.rs      |  5 +++-
 dhall/src/core/var.rs        |  6 -----
 dhall/src/phase/mod.rs       |  8 ------
 dhall/src/phase/normalize.rs | 22 +----------------
 dhall/src/phase/typecheck.rs | 10 ++++----
 7 files changed, 27 insertions(+), 114 deletions(-)

(limited to 'dhall/src')

diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index 9230a2e..3c07c1c 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -18,9 +18,6 @@ enum CtxItem<T> {
 #[derive(Debug, Clone)]
 struct Context<T>(Rc<Vec<(Label, CtxItem<T>)>>);
 
-#[derive(Debug, Clone)]
-pub(crate) struct NormalizationContext(Context<()>);
-
 #[derive(Debug, Clone)]
 pub(crate) struct TypecheckContext(Context<Type>);
 
@@ -117,22 +114,6 @@ impl<T> Context<T> {
     }
 }
 
-impl NormalizationContext {
-    pub fn new() -> Self {
-        NormalizationContext(Context::new())
-    }
-    pub fn skip(&self, x: &Label) -> Self {
-        NormalizationContext(self.0.insert_kept(x, ()))
-    }
-    pub fn lookup(&self, var: &V<Label>) -> Value {
-        match self.0.lookup(var) {
-            Ok(CtxItem::Replaced(t, ())) => t.to_value(),
-            Ok(CtxItem::Kept(newvar, ())) => Value::Var(newvar.clone()),
-            Err(var) => Value::Var(AlphaVar::from_var(var)),
-        }
-    }
-}
-
 impl TypecheckContext {
     pub fn new() -> Self {
         TypecheckContext(Context::new())
@@ -180,12 +161,6 @@ impl<T: Clone + Shift> Shift for Context<T> {
     }
 }
 
-impl Shift for NormalizationContext {
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
-        Some(NormalizationContext(self.0.shift(delta, var)?))
-    }
-}
-
 impl<T: Subst<Typed>> Subst<Typed> for CtxItem<T> {
     fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
         match self {
@@ -209,12 +184,6 @@ impl<T: Clone + Subst<Typed>> Subst<Typed> for Context<T> {
     }
 }
 
-impl Subst<Typed> for NormalizationContext {
-    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
-        NormalizationContext(self.0.subst_shift(var, val))
-    }
-}
-
 impl PartialEq for TypecheckContext {
     fn eq(&self, _: &Self) -> bool {
         // don't count contexts when comparing stuff
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index 54a5442..87541d3 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -4,13 +4,11 @@ use std::rc::Rc;
 
 use dhall_syntax::{Const, ExprF};
 
-use crate::core::context::{NormalizationContext, TypecheckContext};
+use crate::core::context::TypecheckContext;
 use crate::core::value::Value;
 use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::error::{TypeError, TypeMessage};
-use crate::phase::normalize::{
-    apply_any, normalize_one_layer, normalize_whnf, InputSubExpr, OutputSubExpr,
-};
+use crate::phase::normalize::{apply_any, normalize_one_layer, OutputSubExpr};
 use crate::phase::typecheck::type_of_const;
 use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed};
 
@@ -25,8 +23,6 @@ use Marker::{NF, WHNF};
 
 #[derive(Debug)]
 enum ThunkInternal {
-    /// Non-normalized value alongside a normalization context
-    Unnormalized(NormalizationContext, InputSubExpr),
     /// Partially normalized value whose subexpressions have been thunked (this is returned from
     /// typechecking). Note that this is different from `Value::PartialExpr` because there is no
     /// requirement of WHNF here.
@@ -63,12 +59,6 @@ impl ThunkInternal {
 
     fn normalize_whnf(&mut self) {
         match self {
-            ThunkInternal::Unnormalized(ctx, e) => {
-                *self = ThunkInternal::Value(
-                    WHNF,
-                    normalize_whnf(ctx.clone(), e.clone()),
-                )
-            }
             ThunkInternal::PartialExpr(e) => {
                 *self =
                     ThunkInternal::Value(WHNF, normalize_one_layer(e.clone()))
@@ -80,8 +70,7 @@ impl ThunkInternal {
 
     fn normalize_nf(&mut self) {
         match self {
-            ThunkInternal::Unnormalized(_, _)
-            | ThunkInternal::PartialExpr(_) => {
+            ThunkInternal::PartialExpr(_) => {
                 self.normalize_whnf();
                 self.normalize_nf();
             }
@@ -97,8 +86,7 @@ impl ThunkInternal {
     // Always use normalize_whnf before
     fn as_whnf(&self) -> &Value {
         match self {
-            ThunkInternal::Unnormalized(_, _)
-            | ThunkInternal::PartialExpr(_) => unreachable!(),
+            ThunkInternal::PartialExpr(_) => unreachable!(),
             ThunkInternal::Value(_, v) => v,
         }
     }
@@ -106,19 +94,15 @@ impl ThunkInternal {
     // Always use normalize_nf before
     fn as_nf(&self) -> &Value {
         match self {
-            ThunkInternal::Unnormalized(_, _)
-            | ThunkInternal::PartialExpr(_)
-            | ThunkInternal::Value(WHNF, _) => unreachable!(),
+            ThunkInternal::PartialExpr(_) | ThunkInternal::Value(WHNF, _) => {
+                unreachable!()
+            }
             ThunkInternal::Value(NF, v) => v,
         }
     }
 }
 
 impl Thunk {
-    pub(crate) fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk {
-        ThunkInternal::Unnormalized(ctx, e).into_thunk()
-    }
-
     pub(crate) fn from_value(v: Value) -> Thunk {
         ThunkInternal::Value(WHNF, v).into_thunk()
     }
@@ -141,8 +125,7 @@ impl Thunk {
     fn do_normalize_whnf(&self) {
         let borrow = self.0.borrow();
         match &*borrow {
-            ThunkInternal::Unnormalized(_, _)
-            | ThunkInternal::PartialExpr(_) => {
+            ThunkInternal::PartialExpr(_) => {
                 drop(borrow);
                 self.0.borrow_mut().normalize_whnf();
             }
@@ -154,9 +137,7 @@ impl Thunk {
     fn do_normalize_nf(&self) {
         let borrow = self.0.borrow();
         match &*borrow {
-            ThunkInternal::Unnormalized(_, _)
-            | ThunkInternal::PartialExpr(_)
-            | ThunkInternal::Value(WHNF, _) => {
+            ThunkInternal::PartialExpr(_) | ThunkInternal::Value(WHNF, _) => {
                 drop(borrow);
                 self.0.borrow_mut().normalize_nf();
             }
@@ -183,7 +164,10 @@ impl Thunk {
         self.as_value().clone()
     }
 
-    pub(crate) fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr {
+    pub(crate) fn normalize_to_expr_maybe_alpha(
+        &self,
+        alpha: bool,
+    ) -> OutputSubExpr {
         self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
     }
 
@@ -222,7 +206,10 @@ impl TypedThunk {
         self.clone().into_typed()
     }
 
-    pub(crate) fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr {
+    pub(crate) fn normalize_to_expr_maybe_alpha(
+        &self,
+        alpha: bool,
+    ) -> OutputSubExpr {
         self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
     }
 
@@ -302,9 +289,6 @@ impl Shift for Thunk {
 impl Shift for ThunkInternal {
     fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
         Some(match self {
-            ThunkInternal::Unnormalized(ctx, e) => {
-                ThunkInternal::Unnormalized(ctx.shift(delta, var)?, e.clone())
-            }
             ThunkInternal::PartialExpr(e) => ThunkInternal::PartialExpr(
                 e.traverse_ref_with_special_handling_of_binders(
                     |v| Ok(v.shift(delta, var)?),
@@ -342,10 +326,6 @@ impl Subst<Typed> for Thunk {
 impl Subst<Typed> for ThunkInternal {
     fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
         match self {
-            ThunkInternal::Unnormalized(ctx, e) => ThunkInternal::Unnormalized(
-                ctx.subst_shift(var, val),
-                e.clone(),
-            ),
             ThunkInternal::PartialExpr(e) => ThunkInternal::PartialExpr(
                 e.map_ref_with_special_handling_of_binders(
                     |v| v.subst_shift(var, val),
@@ -404,11 +384,6 @@ impl std::fmt::Debug for Thunk {
             ThunkInternal::PartialExpr(e) => {
                 f.debug_tuple("Thunk@PartialExpr").field(e).finish()
             }
-            ThunkInternal::Unnormalized(ctx, e) => f
-                .debug_tuple("Thunk@Unnormalized")
-                .field(ctx)
-                .field(e)
-                .finish(),
         }
     }
 }
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 61a8eea..d3d017d 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -66,7 +66,10 @@ impl Value {
     }
     /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize
     /// if alpha is `true`
-    pub(crate) fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr {
+    pub(crate) fn normalize_to_expr_maybe_alpha(
+        &self,
+        alpha: bool,
+    ) -> OutputSubExpr {
         match self {
             Value::Lam(x, t, e) => rc(ExprF::Lam(
                 x.to_label_maybe_alpha(alpha),
diff --git a/dhall/src/core/var.rs b/dhall/src/core/var.rs
index 4ef1b93..5e7bf05 100644
--- a/dhall/src/core/var.rs
+++ b/dhall/src/core/var.rs
@@ -61,12 +61,6 @@ impl AlphaVar {
             _ => self.normal.clone(),
         }
     }
-    pub(crate) fn from_var(normal: V<Label>) -> Self {
-        AlphaVar {
-            normal,
-            alpha: None,
-        }
-    }
     pub(crate) fn from_var_and_alpha(normal: V<Label>, alpha: usize) -> Self {
         AlphaVar {
             normal,
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index 778f990..5a6d4db 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -76,11 +76,6 @@ impl Resolved {
     pub fn typecheck_with(self, ty: &Type) -> Result<Typed, TypeError> {
         typecheck::typecheck_with(self, ty)
     }
-    /// Pretends this expression has been typechecked. Use with care.
-    #[allow(dead_code)]
-    pub(crate) fn skip_typecheck(self) -> Typed {
-        typecheck::skip_typecheck(self)
-    }
 }
 
 impl Typed {
@@ -168,9 +163,6 @@ impl Normalized {
     pub(crate) fn to_type(&self) -> Type {
         self.0.to_type()
     }
-    pub(crate) fn to_value(&self) -> Value {
-        self.0.to_value()
-    }
     pub(crate) fn into_typed(self) -> Typed {
         self.0
     }
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index fd0197d..2a2bf3e 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -5,13 +5,11 @@ use dhall_syntax::{
     NaiveDouble,
 };
 
-use crate::core::context::NormalizationContext;
 use crate::core::thunk::{Thunk, TypedThunk};
 use crate::core::value::Value;
 use crate::core::var::{Shift, Subst};
-use crate::phase::{Normalized, NormalizedSubExpr, ResolvedSubExpr, Typed};
+use crate::phase::{Normalized, NormalizedSubExpr, Typed};
 
-pub(crate) type InputSubExpr = ResolvedSubExpr;
 pub(crate) type OutputSubExpr = NormalizedSubExpr;
 
 // Ad-hoc macro to help construct closures
@@ -381,24 +379,6 @@ pub(crate) fn squash_textlit(
     ret
 }
 
-/// Reduces the imput expression to a Value. Evaluates as little as possible.
-pub(crate) fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value {
-    match expr.as_ref() {
-        ExprF::Embed(e) => return e.to_value(),
-        ExprF::Var(v) => return ctx.lookup(v),
-        _ => {}
-    }
-
-    // Thunk subexpressions
-    let expr: ExprF<Thunk, Normalized> =
-        expr.as_ref().map_ref_with_special_handling_of_binders(
-            |e| Thunk::new(ctx.clone(), e.clone()),
-            |x, e| Thunk::new(ctx.skip(x), e.clone()),
-        );
-
-    normalize_one_layer(expr)
-}
-
 // Small helper enum to avoid repetition
 enum Ret<'a> {
     Value(Value),
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 7bbad38..dd6da70 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -4,7 +4,7 @@ use dhall_syntax::{
     rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, SubExpr,
 };
 
-use crate::core::context::{NormalizationContext, TypecheckContext};
+use crate::core::context::TypecheckContext;
 use crate::core::thunk::{Thunk, TypedThunk};
 use crate::core::value::Value;
 use crate::core::var::{Shift, Subst};
@@ -1009,11 +1009,11 @@ pub(crate) fn typecheck(e: Resolved) -> Result<Typed, TypeError> {
     type_of(e.0)
 }
 
-pub(crate) fn typecheck_with(e: Resolved, ty: &Type) -> Result<Typed, TypeError> {
+pub(crate) fn typecheck_with(
+    e: Resolved,
+    ty: &Type,
+) -> Result<Typed, TypeError> {
     let expr: SubExpr<_> = e.0;
     let ty: SubExpr<_> = ty.to_expr();
     type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty)))
 }
-pub(crate) fn skip_typecheck(e: Resolved) -> Typed {
-    Typed::from_thunk_untyped(Thunk::new(NormalizationContext::new(), e.0))
-}
-- 
cgit v1.2.3