summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/lib.rs4
-rw-r--r--dhall/src/semantics/builtins.rs7
-rw-r--r--dhall/src/semantics/nze/nir.rs76
-rw-r--r--dhall/src/semantics/resolve/hir.rs6
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 {