From f4a1a6b8d4de5f83649b2ddd90d65f6e6d76e5e1 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 13 Mar 2020 21:29:08 +0000
Subject: Nir::normalize isn't useful

It pretends to normalize but actually can't normalize under lambdas. The
correct way to normalize a Nir is to convert it to Hir.
---
 dhall/src/lib.rs                   |  4 +-
 dhall/src/semantics/builtins.rs    |  7 ----
 dhall/src/semantics/nze/nir.rs     | 76 --------------------------------------
 dhall/src/semantics/resolve/hir.rs |  6 ---
 4 files changed, 3 insertions(+), 90 deletions(-)

diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index 07df2b2..caaf260 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -42,6 +42,8 @@ pub(crate) struct Typed {
 }
 
 /// A normalized expression.
+///
+/// This is actually a lie, because the expression will only get normalized on demand.
 #[derive(Debug, Clone)]
 pub(crate) struct Normalized(Nir);
 
@@ -112,7 +114,7 @@ impl Typed {
     }
     /// Reduce an expression to its normal form, performing beta reduction
     pub fn normalize(&self) -> Normalized {
-        Normalized(self.hir.rec_eval_closed_expr())
+        Normalized(self.hir.eval_closed_expr())
     }
 
     /// Converts a value back to the corresponding AST expression.
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index 7fbb933..ef375b8 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -30,13 +30,6 @@ impl BuiltinClosure {
         let args = self.args.iter().cloned().chain(once(a)).collect();
         apply_builtin(self.b, args, self.env.clone())
     }
-    /// This doesn't break the invariant because we already checked that the appropriate arguments
-    /// did not normalize to something that allows evaluation to proceed.
-    pub fn normalize(&self) {
-        for x in self.args.iter() {
-            x.normalize();
-        }
-    }
     pub fn to_hirkind(&self, venv: VarEnv) -> HirKind {
         HirKind::Expr(self.args.iter().fold(
             ExprKind::Builtin(self.b),
diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
index e6482fc..5fccbf1 100644
--- a/dhall/src/semantics/nze/nir.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -146,9 +146,6 @@ impl Nir {
     pub(crate) fn to_expr_tyenv(&self, tyenv: &TyEnv) -> Expr {
         self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
     }
-    pub(crate) fn normalize(&self) {
-        self.0.normalize()
-    }
 
     pub(crate) fn app(&self, v: Nir) -> Nir {
         Nir::from_kind(apply_any(self.clone(), v))
@@ -286,9 +283,6 @@ impl NirInternal {
     fn kind(&self) -> &NirKind {
         &self.kind
     }
-    fn normalize(&self) {
-        self.kind().normalize();
-    }
 }
 
 impl NirKind {
@@ -296,66 +290,6 @@ impl NirKind {
         Nir::from_kind(self)
     }
 
-    pub(crate) fn normalize(&self) {
-        match self {
-            NirKind::Var(..)
-            | NirKind::Const(_)
-            | NirKind::Num(_)
-            | NirKind::BuiltinType(..) => {}
-
-            NirKind::EmptyOptionalLit(v)
-            | NirKind::EmptyListLit(v)
-            | NirKind::OptionalType(v)
-            | NirKind::ListType(v) => {
-                v.normalize();
-            }
-
-            NirKind::NEOptionalLit(v) => {
-                v.normalize();
-            }
-            NirKind::LamClosure { annot, closure, .. }
-            | NirKind::PiClosure { annot, closure, .. } => {
-                annot.normalize();
-                closure.normalize();
-            }
-            NirKind::AppliedBuiltin(closure) => closure.normalize(),
-            NirKind::NEListLit(elts) => {
-                for x in elts.iter() {
-                    x.normalize();
-                }
-            }
-            NirKind::RecordLit(kvs) => {
-                for x in kvs.values() {
-                    x.normalize();
-                }
-            }
-            NirKind::RecordType(kvs) => {
-                for x in kvs.values() {
-                    x.normalize();
-                }
-            }
-            NirKind::UnionType(kts) | NirKind::UnionConstructor(_, kts) => {
-                for x in kts.values().flatten() {
-                    x.normalize();
-                }
-            }
-            NirKind::UnionLit(_, v, kts) => {
-                v.normalize();
-                for x in kts.values().flatten() {
-                    x.normalize();
-                }
-            }
-            NirKind::TextLit(tlit) => tlit.normalize(),
-            NirKind::Equivalence(x, y) => {
-                x.normalize();
-                y.normalize();
-            }
-            NirKind::PartialExpr(e) => {
-                e.map_ref(Nir::normalize);
-            }
-        }
-    }
-
     pub(crate) fn from_builtin(b: Builtin) -> NirKind {
         NirKind::from_builtin_env(b, NzEnv::new())
     }
@@ -408,9 +342,6 @@ impl Closure {
         }
     }
 
-    // TODO: somehow normalize the body. Might require to pass an env.
-    pub fn normalize(&self) {}
-
     /// Convert this closure to a Hir expression
     pub fn to_hir(&self, venv: VarEnv) -> Hir {
         self.apply_var(NzVar::new(venv.size()))
@@ -474,13 +405,6 @@ impl TextLit {
     pub fn iter(&self) -> impl Iterator<Item = &InterpolatedTextContents<Nir>> {
         self.0.iter()
     }
-    /// Normalize the contained values. This does not break the invariant because we have already
-    /// ensured that no contained values normalize to a TextLit.
-    pub fn normalize(&self) {
-        for x in self.0.iter() {
-            x.map_ref(Nir::normalize);
-        }
-    }
 }
 
 impl lazy::Eval<NirKind> for Thunk {
diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs
index 22abaaf..3934bbb 100644
--- a/dhall/src/semantics/resolve/hir.rs
+++ b/dhall/src/semantics/resolve/hir.rs
@@ -85,12 +85,6 @@ impl Hir {
     pub fn eval_closed_expr(&self) -> Nir {
         self.eval(NzEnv::new())
     }
-    /// Eval a closed Hir fully and recursively;
-    pub fn rec_eval_closed_expr(&self) -> Nir {
-        let val = self.eval_closed_expr();
-        val.normalize();
-        val
-    }
 }
 
 fn hir_to_expr(hir: &Hir, opts: ToExprOptions, env: &mut NameEnv) -> Expr {
-- 
cgit v1.2.3