summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/normalize.rs156
1 files changed, 77 insertions, 79 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index bd479d0..64c17c3 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -157,7 +157,7 @@ where
),
// // fold/build fusion
// (ListFold, [_, App(box Builtin(ListBuild), [_, x, rest..]), rest..]) => {
- // normalize_value(&App(bx(x.clone()), rest.to_vec()))
+ // normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
// }
(OptionalFold, [_, NEOptionalLit(x), _, just, _, rest..]) => {
let x = x.clone();
@@ -169,7 +169,7 @@ where
}
// // fold/build fusion
// (OptionalFold, [_, App(box Builtin(OptionalBuild), [_, x, rest..]), rest..]) => {
- // normalize_value(&App(bx(x.clone()), rest.to_vec()))
+ // normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
// }
(NaturalBuild, [g, rest..]) => {
'ret: {
@@ -226,71 +226,71 @@ where
// expr: SubExpr<X, Normalized<'static>>,
// }
// impl ContextualizedSubExpr {
-// fn normalize_value(self) -> Value {
-// normalize_value(&self.ctx, self.expr)
+// fn normalize_whnf(self) -> WHNF {
+// normalize_whnf(&self.ctx, self.expr)
// }
// fn normalize_expr(self) -> OutputSubExpr {
-// normalize_value(&self.ctx, self.expr).into_expr(&self.ctx)
+// normalize_whnf(&self.ctx, self.expr).into_expr(&self.ctx)
// }
// }
/// A semantic value. This is partially redundant with `dhall_core::Expr`, on purpose. `Expr` should
/// be limited to syntactic expressions: either written by the user or meant to be printed.
/// The rule is the following: we must _not_ construct values of type `Expr` while normalizing or
-/// typechecking, but only construct `Value`s.
+/// typechecking, but only construct `WHNF`s.
///
-/// Values usually store subexpressions unnormalized, to enable lazy normalization. They
-/// approximate what's called Weak Head Normal-Form (WHNF). This means that the expression is
-/// normalized as little as possible, but just enough to know the first constructor of the normal
-/// form. This is identical to full normalization for simple types like integers, but for example
-/// for a record literal this means knowing just the field names.
+/// WHNFs usually store subexpressions unnormalized, to enable lazy normalization. They approximate
+/// what's called Weak Head Normal-Form (WHNF). This means that the expression is normalized as
+/// little as possible, but just enough to know the first constructor of the normal form. This is
+/// identical to full normalization for simple types like integers, but for e.g. a record literal
+/// this means knowing just the field names.
#[derive(Debug, Clone)]
-enum Value {
+enum WHNF {
Closure(Closure),
RecordLit(NormalizationContext, BTreeMap<Label, InputSubExpr>),
UnionType(NormalizationContext, BTreeMap<Label, Option<InputSubExpr>>),
Expr(OutputSubExpr),
}
-impl Value {
+impl WHNF {
/// Convert the value back to a (normalized) syntactic expression
fn normalize_to_expr(self) -> OutputSubExpr {
match self {
- Value::Closure(c) => c.normalize_to_expr(),
- Value::RecordLit(ctx, kvs) => rc(ExprF::RecordLit(
+ WHNF::Closure(c) => c.normalize_to_expr(),
+ WHNF::RecordLit(ctx, kvs) => rc(ExprF::RecordLit(
kvs.into_iter()
.map(|(k, v)| {
- (k, normalize_value(&ctx, v).normalize_to_expr())
+ (k, normalize_whnf(&ctx, v).normalize_to_expr())
})
.collect(),
)),
- Value::UnionType(ctx, kvs) => rc(ExprF::UnionType(
+ WHNF::UnionType(ctx, kvs) => rc(ExprF::UnionType(
kvs.into_iter()
.map(|(k, v)| {
(
k,
v.map(|v| {
- normalize_value(&ctx, v).normalize_to_expr()
+ normalize_whnf(&ctx, v).normalize_to_expr()
}),
)
})
.collect(),
)),
- Value::Expr(e) => e,
+ WHNF::Expr(e) => e,
}
}
fn shift0(self, delta: isize, label: &Label) -> Self {
match self {
- Value::Closure(c) => Value::Closure(c.shift0(delta, label)),
- Value::Expr(e) => Value::Expr(shift0(delta, label, &e)),
- Value::RecordLit(ctx, kvs) => Value::RecordLit(
+ WHNF::Closure(c) => WHNF::Closure(c.shift0(delta, label)),
+ WHNF::Expr(e) => WHNF::Expr(shift0(delta, label, &e)),
+ WHNF::RecordLit(ctx, kvs) => WHNF::RecordLit(
ctx,
kvs.into_iter()
.map(|(k, v)| (k, shift0(delta, label, &v)))
.collect(),
),
- Value::UnionType(ctx, kvs) => Value::UnionType(
+ WHNF::UnionType(ctx, kvs) => WHNF::UnionType(
ctx,
kvs.into_iter()
.map(|(k, v)| (k, v.map(|v| shift0(delta, label, &v))))
@@ -303,7 +303,7 @@ impl Value {
#[derive(Debug, Clone)]
enum Closure {
Lam(NormalizationContext, Label, InputSubExpr, InputSubExpr),
- AppliedBuiltin(NormalizationContext, Builtin, Vec<Value>),
+ AppliedBuiltin(NormalizationContext, Builtin, Vec<WHNF>),
UnionConstructor(
NormalizationContext,
Label,
@@ -313,11 +313,11 @@ enum Closure {
impl Closure {
/// Apply the closure to a value
- fn app(self, val: Value) -> Value {
+ fn app(self, val: WHNF) -> WHNF {
match self {
Closure::Lam(ctx, x, _, e) => {
let ctx2 = ctx.insert(&x, val);
- normalize_value(&ctx2, e)
+ normalize_whnf(&ctx2, e)
}
Closure::AppliedBuiltin(ctx, b, mut args) => {
args.push(val);
@@ -328,7 +328,7 @@ impl Closure {
match apply_builtin(b, &args_unrolled).into_value(&ctx) {
Some(v) => v,
None => {
- Value::Closure(Closure::AppliedBuiltin(ctx, b, args))
+ WHNF::Closure(Closure::AppliedBuiltin(ctx, b, args))
}
}
}
@@ -339,16 +339,12 @@ impl Closure {
(
k,
v.map(|v| {
- normalize_value(&ctx, v).normalize_to_expr()
+ normalize_whnf(&ctx, v).normalize_to_expr()
}),
)
})
.collect();
- Value::Expr(rc(ExprF::UnionLit(
- l,
- val.normalize_to_expr(),
- kts,
- )))
+ WHNF::Expr(rc(ExprF::UnionLit(l, val.normalize_to_expr(), kts)))
}
}
}
@@ -360,8 +356,8 @@ impl Closure {
let ctx2 = ctx.skip(&x);
rc(ExprF::Lam(
x.clone(),
- normalize_value(&ctx, t).normalize_to_expr(),
- normalize_value(&ctx2, e).normalize_to_expr(),
+ normalize_whnf(&ctx, t).normalize_to_expr(),
+ normalize_whnf(&ctx2, e).normalize_to_expr(),
))
}
Closure::AppliedBuiltin(_ctx, b, args) => {
@@ -382,7 +378,7 @@ impl Closure {
(
k,
v.map(|v| {
- normalize_value(&ctx, v).normalize_to_expr()
+ normalize_whnf(&ctx, v).normalize_to_expr()
}),
)
})
@@ -418,7 +414,7 @@ impl Closure {
#[derive(Debug, Clone)]
enum EnvItem {
- Expr(Value),
+ Expr(WHNF),
Skip(usize),
}
@@ -429,7 +425,7 @@ impl NormalizationContext {
fn new() -> NormalizationContext {
NormalizationContext(Context::new())
}
- fn insert(&self, x: &Label, e: Value) -> NormalizationContext {
+ fn insert(&self, x: &Label, e: WHNF) -> NormalizationContext {
NormalizationContext(self.0.insert(x.clone(), EnvItem::Expr(e)))
}
fn skip(&self, x: &Label) -> NormalizationContext {
@@ -446,14 +442,14 @@ impl NormalizationContext {
.insert(x.clone(), EnvItem::Skip(0)),
)
}
- fn lookup(&self, var: &V<Label>) -> Value {
+ fn lookup(&self, var: &V<Label>) -> WHNF {
let V(x, n) = var;
match self.0.lookup(x, *n) {
Some(EnvItem::Expr(e)) => e.clone(),
Some(EnvItem::Skip(m)) => {
- Value::Expr(rc(ExprF::Var(V(x.clone(), *m))))
+ WHNF::Expr(rc(ExprF::Var(V(x.clone(), *m))))
}
- None => Value::Expr(rc(ExprF::Var(V(x.clone(), *n)))),
+ None => WHNF::Expr(rc(ExprF::Var(V(x.clone(), *n)))),
}
}
}
@@ -471,10 +467,10 @@ enum WhatNext<'a, N, E> {
}
impl<'a> WhatNext<'a, X, X> {
- fn into_value(self, ctx: &NormalizationContext) -> Option<Value> {
+ fn into_value(self, ctx: &NormalizationContext) -> Option<WHNF> {
use WhatNext::*;
match self {
- Continue(e) => Some(normalize_value(ctx, e.embed_absurd().roll())),
+ Continue(e) => Some(normalize_whnf(ctx, e.embed_absurd().roll())),
Done(e) => Some(reval(ctx, e.roll())),
DoneRef(e) => Some(reval(ctx, e.roll())),
DoneRefSub(e) => Some(reval(ctx, e.clone())),
@@ -483,28 +479,29 @@ impl<'a> WhatNext<'a, X, X> {
}
}
-fn reval(ctx: &NormalizationContext, expr: OutputSubExpr) -> Value {
+fn reval(ctx: &NormalizationContext, expr: OutputSubExpr) -> WHNF {
match expr.as_ref().embed_absurd() {
ExprF::Lam(x, t, e) => {
- Value::Closure(Closure::Lam(ctx.clone(), x, t, e))
+ WHNF::Closure(Closure::Lam(ctx.clone(), x, t, e))
}
ExprF::Builtin(b) => {
- Value::Closure(Closure::AppliedBuiltin(ctx.clone(), b, vec![]))
+ WHNF::Closure(Closure::AppliedBuiltin(ctx.clone(), b, vec![]))
}
- ExprF::RecordLit(kvs) => Value::RecordLit(ctx.clone(), kvs),
- ExprF::UnionType(kvs) => Value::UnionType(ctx.clone(), kvs),
- _ => Value::Expr(expr),
+ ExprF::RecordLit(kvs) => WHNF::RecordLit(ctx.clone(), kvs),
+ ExprF::UnionType(kvs) => WHNF::UnionType(ctx.clone(), kvs),
+ _ => WHNF::Expr(expr),
}
}
-fn normalize_value(ctx: &NormalizationContext, expr: InputSubExpr) -> Value {
+/// Reduces the imput expression to WHNF. See doc on `WHNF` for details.
+fn normalize_whnf(ctx: &NormalizationContext, expr: InputSubExpr) -> WHNF {
let e = match expr.as_ref() {
ExprF::Let(x, _, r, b) => {
- let r = normalize_value(ctx, r.clone());
- return normalize_value(&ctx.insert(x, r), b.clone());
+ let r = normalize_whnf(ctx, r.clone());
+ return normalize_whnf(&ctx.insert(x, r), b.clone());
}
ExprF::Lam(x, t, e) => {
- return Value::Closure(Closure::Lam(
+ return WHNF::Closure(Closure::Lam(
ctx.clone(),
x.clone(),
t.clone(),
@@ -512,26 +509,26 @@ fn normalize_value(ctx: &NormalizationContext, expr: InputSubExpr) -> Value {
))
}
ExprF::Builtin(b) => {
- return Value::Closure(Closure::AppliedBuiltin(
+ return WHNF::Closure(Closure::AppliedBuiltin(
ctx.clone(),
*b,
vec![],
))
}
ExprF::RecordLit(kvs) => {
- return Value::RecordLit(ctx.clone(), kvs.clone())
+ return WHNF::RecordLit(ctx.clone(), kvs.clone())
}
ExprF::UnionType(kvs) => {
- return Value::UnionType(ctx.clone(), kvs.clone())
+ return WHNF::UnionType(ctx.clone(), kvs.clone())
}
e => e,
};
// Recursively normalize all subexpressions
- let expr: ExprF<Value, Label, X, Normalized<'static>> = e
+ let expr: ExprF<WHNF, Label, X, Normalized<'static>> = e
.map_ref_with_special_handling_of_binders(
- |e| normalize_value(ctx, e.clone()),
- |x, e| normalize_value(&ctx.skip(x), e.clone()),
+ |e| normalize_whnf(ctx, e.clone()),
+ |x, e| normalize_whnf(&ctx.skip(x), e.clone()),
X::clone,
Normalized::clone,
Label::clone,
@@ -543,8 +540,8 @@ fn normalize_value(ctx: &NormalizationContext, expr: InputSubExpr) -> Value {
/// When all sub-expressions have been (partially) normalized, eval the remaining toplevel layer.
fn normalize_last_layer(
ctx: &NormalizationContext,
- expr: ExprF<Value, Label, X, Normalized<'static>>,
-) -> Value {
+ expr: ExprF<WHNF, Label, X, Normalized<'static>>,
+) -> WHNF {
use dhall_core::BinOp::*;
use dhall_core::ExprF::*;
use WhatNext::*;
@@ -553,25 +550,26 @@ fn normalize_last_layer(
Var(v) => return ctx.lookup(&v),
Annot(x, _) => return x,
Note(_, e) => return e,
- App(Value::Closure(c), a) => return c.app(a),
- Field(Value::UnionType(ctx, kts), l) => {
- return Value::Closure(Closure::UnionConstructor(ctx, l, kts))
+ App(WHNF::Closure(c), a) => return c.app(a),
+ Field(WHNF::UnionType(ctx, kts), l) => {
+ return WHNF::Closure(Closure::UnionConstructor(ctx, l, kts))
+ }
+ Field(WHNF::RecordLit(record_ctx, mut kvs), l) => {
+ match kvs.remove(&l) {
+ Some(r) => return normalize_whnf(&record_ctx, r),
+ // Return ownership
+ None => Field(WHNF::RecordLit(record_ctx, kvs), l),
+ }
}
- Field(Value::RecordLit(record_ctx, mut kvs), l) => match kvs.remove(&l)
- {
- Some(r) => return normalize_value(&record_ctx, r),
- // Return ownership
- None => Field(Value::RecordLit(record_ctx, kvs), l),
- },
// Always simplify `x.{}` to `{}`
Projection(_, ls) if ls.is_empty() => {
- return Value::RecordLit(
+ return WHNF::RecordLit(
ctx.clone(),
std::collections::BTreeMap::new(),
)
}
- Projection(Value::RecordLit(record_ctx, mut kvs), ls) => {
- return Value::RecordLit(
+ Projection(WHNF::RecordLit(record_ctx, mut kvs), ls) => {
+ return WHNF::RecordLit(
record_ctx,
ls.into_iter()
.filter_map(|l| kvs.remove(&l).map(|x| (l, x)))
@@ -579,15 +577,15 @@ fn normalize_last_layer(
)
}
Merge(
- Value::RecordLit(record_ctx, mut handlers),
- Value::Closure(Closure::UnionConstructor(ctor_ctx, l, kts)),
+ WHNF::RecordLit(record_ctx, mut handlers),
+ WHNF::Closure(Closure::UnionConstructor(ctor_ctx, l, kts)),
t,
) => match handlers.remove(&l) {
- Some(h) => return normalize_value(ctx, h),
+ Some(h) => return normalize_whnf(ctx, h),
// Return ownership
None => Merge(
- Value::RecordLit(record_ctx, handlers),
- Value::Closure(Closure::UnionConstructor(ctor_ctx, l, kts)),
+ WHNF::RecordLit(record_ctx, handlers),
+ WHNF::Closure(Closure::UnionConstructor(ctor_ctx, l, kts)),
t,
),
},
@@ -667,7 +665,7 @@ fn normalize_last_layer(
/// leave ill-typed sub-expressions unevaluated.
///
fn normalize(e: InputSubExpr) -> OutputSubExpr {
- normalize_value(&NormalizationContext::new(), e).normalize_to_expr()
+ normalize_whnf(&NormalizationContext::new(), e).normalize_to_expr()
}
#[cfg(test)]
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 03:04:00 +0000