diff options
author | Nadrieril | 2020-03-13 21:29:08 +0000 |
---|---|---|
committer | Nadrieril | 2020-03-31 21:44:01 +0100 |
commit | f4a1a6b8d4de5f83649b2ddd90d65f6e6d76e5e1 (patch) | |
tree | 4430f8e81cc8d451ed16c8b45d6f2ce8ed2f8c56 /dhall/src | |
parent | ef3734a3e9381b2e91552089774126f58f560bc3 (diff) |
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.
Diffstat (limited to 'dhall/src')
-rw-r--r-- | dhall/src/lib.rs | 4 | ||||
-rw-r--r-- | dhall/src/semantics/builtins.rs | 7 | ||||
-rw-r--r-- | dhall/src/semantics/nze/nir.rs | 76 | ||||
-rw-r--r-- | 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 { |