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/semantics/builtins.rs | 7 ---- dhall/src/semantics/nze/nir.rs | 76 -------------------------------------- dhall/src/semantics/resolve/hir.rs | 6 --- 3 files changed, 89 deletions(-) (limited to 'dhall/src/semantics') 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> { 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 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