summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/normalize.rs310
1 files changed, 144 insertions, 166 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 26d062b..6d071f2 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -123,7 +123,7 @@ fn apply_builtin(
(OptionalBuild, [t, g]) => g
.clone()
.app(AppliedBuiltin(ctx.clone(), Optional, vec![]).app(t.clone()))
- .app(SomeConstructorClosure(Now::from_whnf(t.clone())))
+ .app(OptionalSomeClosure(Now::from_whnf(t.clone())))
.app(EmptyOptionalLit(Now::from_whnf(t.clone()))),
(OptionalFold, [_, EmptyOptionalLit(_), _, _, nothing]) => {
nothing.clone()
@@ -225,9 +225,9 @@ enum WHNF {
Lam(Label, Now, (NormalizationContext, InputSubExpr)),
AppliedBuiltin(NormalizationContext, Builtin, Vec<WHNF>),
/// `λ(x: a) -> Some x`
- SomeConstructorClosure(Now),
- /// `λ(x : a) -> λ(xs : List a) -> [ x ] # xs
- /// `λ(xs : List a) -> [ x ] # xs
+ OptionalSomeClosure(Now),
+ /// `λ(x : a) -> λ(xs : List a) -> [ x ] # xs`
+ /// `λ(xs : List a) -> [ x ] # xs`
ListConsClosure(Now, Option<Now>),
/// `λ(x : Natural) -> x + 1`
NaturalSuccClosure,
@@ -275,7 +275,7 @@ impl WHNF {
}
e.normalize_to_expr()
}
- WHNF::SomeConstructorClosure(n) => {
+ WHNF::OptionalSomeClosure(n) => {
let a = n.normalize().normalize_to_expr();
dhall::subexpr!(λ(x: a) -> Some x)
}
@@ -410,7 +410,7 @@ impl WHNF {
None => WHNF::AppliedBuiltin(ctx, b, args),
}
}
- (WHNF::SomeConstructorClosure(_), val) => {
+ (WHNF::OptionalSomeClosure(_), val) => {
WHNF::NEOptionalLit(Now::from_whnf(val))
}
(WHNF::ListConsClosure(t, None), val) => {
@@ -448,8 +448,8 @@ impl WHNF {
b,
args.into_iter().map(|e| e.shift0(delta, label)).collect(),
),
- WHNF::SomeConstructorClosure(n) => {
- WHNF::SomeConstructorClosure(n.shift0(delta, label))
+ WHNF::OptionalSomeClosure(n) => {
+ WHNF::OptionalSomeClosure(n.shift0(delta, label))
}
WHNF::ListConsClosure(t, v) => WHNF::ListConsClosure(
t.shift0(delta, label),
@@ -557,206 +557,184 @@ impl Now {
/// Reduces the imput expression to WHNF. See doc on `WHNF` for details.
fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
- let expr = match expr.as_ref() {
- ExprF::Var(v) => return ctx.lookup(&v),
- ExprF::Annot(x, _) => return normalize_whnf(ctx, x.clone()),
- ExprF::Note(_, e) => return normalize_whnf(ctx, e.clone()),
+ match expr.as_ref() {
+ ExprF::Var(v) => ctx.lookup(&v),
+ ExprF::Annot(x, _) => normalize_whnf(ctx, x.clone()),
+ ExprF::Note(_, e) => normalize_whnf(ctx, e.clone()),
// TODO: wasteful to retraverse everything
- ExprF::Embed(e) => return normalize_whnf(ctx, e.0.embed_absurd()),
+ ExprF::Embed(e) => normalize_whnf(ctx, e.0.embed_absurd()),
ExprF::Let(x, _, r, b) => {
let r = normalize_whnf(ctx.clone(), r.clone());
- return normalize_whnf(ctx.insert(x, r), b.clone());
+ normalize_whnf(ctx.insert(x, r), b.clone())
}
- ExprF::Lam(x, t, e) => {
- return WHNF::Lam(
- x.clone(),
- Now::new(ctx.clone(), t.clone()),
- (ctx, e.clone()),
- )
- }
- ExprF::Builtin(b) => return WHNF::AppliedBuiltin(ctx, *b, vec![]),
- ExprF::BoolLit(b) => return WHNF::BoolLit(*b),
- ExprF::NaturalLit(n) => return WHNF::NaturalLit(*n),
+ ExprF::Lam(x, t, e) => WHNF::Lam(
+ x.clone(),
+ Now::new(ctx.clone(), t.clone()),
+ (ctx, e.clone()),
+ ),
+ ExprF::Builtin(b) => WHNF::AppliedBuiltin(ctx, *b, vec![]),
+ ExprF::BoolLit(b) => WHNF::BoolLit(*b),
+ ExprF::NaturalLit(n) => WHNF::NaturalLit(*n),
ExprF::OldOptionalLit(None, e) => {
- return WHNF::EmptyOptionalLit(Now::new(ctx, e.clone()))
+ WHNF::EmptyOptionalLit(Now::new(ctx, e.clone()))
}
ExprF::OldOptionalLit(Some(e), _) => {
- return WHNF::NEOptionalLit(Now::new(ctx, e.clone()))
+ WHNF::NEOptionalLit(Now::new(ctx, e.clone()))
}
ExprF::EmptyOptionalLit(e) => {
- return WHNF::EmptyOptionalLit(Now::new(ctx, e.clone()))
+ WHNF::EmptyOptionalLit(Now::new(ctx, e.clone()))
}
ExprF::NEOptionalLit(e) => {
- return WHNF::NEOptionalLit(Now::new(ctx, e.clone()))
- }
- ExprF::EmptyListLit(e) => {
- return WHNF::EmptyListLit(Now::new(ctx, e.clone()))
- }
- ExprF::NEListLit(elts) => {
- return WHNF::NEListLit(
- elts.iter()
- .map(|e| Now::new(ctx.clone(), e.clone()))
- .collect(),
- )
- }
- ExprF::RecordLit(kvs) => {
- return WHNF::RecordLit(
- kvs.iter()
- .map(|(k, e)| (k.clone(), Now::new(ctx.clone(), e.clone())))
- .collect(),
- )
- }
- ExprF::UnionType(kvs) => return WHNF::UnionType(ctx, kvs.clone()),
- ExprF::UnionLit(l, x, kts) => {
- return WHNF::UnionLit(
- l.clone(),
- Now::new(ctx.clone(), x.clone()),
- (ctx, kts.clone()),
- )
- }
- ExprF::TextLit(elts) => {
- return WHNF::TextLit(
- elts.iter()
- .map(|contents| {
- use InterpolatedTextContents::{Expr, Text};
- match contents {
- Expr(n) => Expr(Now::new(ctx.clone(), n.clone())),
- Text(s) => Text(s.clone()),
- }
- })
- .collect(),
- )
+ WHNF::NEOptionalLit(Now::new(ctx, e.clone()))
}
+ ExprF::EmptyListLit(e) => WHNF::EmptyListLit(Now::new(ctx, e.clone())),
+ ExprF::NEListLit(elts) => WHNF::NEListLit(
+ elts.iter()
+ .map(|e| Now::new(ctx.clone(), e.clone()))
+ .collect(),
+ ),
+ ExprF::RecordLit(kvs) => WHNF::RecordLit(
+ kvs.iter()
+ .map(|(k, e)| (k.clone(), Now::new(ctx.clone(), e.clone())))
+ .collect(),
+ ),
+ ExprF::UnionType(kvs) => WHNF::UnionType(ctx, kvs.clone()),
+ ExprF::UnionLit(l, x, kts) => WHNF::UnionLit(
+ l.clone(),
+ Now::new(ctx.clone(), x.clone()),
+ (ctx, kts.clone()),
+ ),
+ ExprF::TextLit(elts) => WHNF::TextLit(
+ elts.iter()
+ .map(|contents| {
+ use InterpolatedTextContents::{Expr, Text};
+ match contents {
+ Expr(n) => Expr(Now::new(ctx.clone(), n.clone())),
+ Text(s) => Text(s.clone()),
+ }
+ })
+ .collect(),
+ ),
ExprF::BoolIf(b, e1, e2) => {
let b = normalize_whnf(ctx.clone(), b.clone());
match b {
- WHNF::BoolLit(true) => return normalize_whnf(ctx, e1.clone()),
- WHNF::BoolLit(false) => return normalize_whnf(ctx, e2.clone()),
- _ => expr,
+ WHNF::BoolLit(true) => normalize_whnf(ctx, e1.clone()),
+ WHNF::BoolLit(false) => normalize_whnf(ctx, e2.clone()),
+ _ => normalize_last_layer(ExprF::BoolIf(
+ b,
+ normalize_whnf(ctx.clone(), e1.clone()),
+ normalize_whnf(ctx, e2.clone()),
+ )),
}
}
- _ => expr,
- };
-
- // Recursively normalize all subexpressions
- let expr: ExprF<WHNF, Label, X, X> =
- expr.as_ref().map_ref_with_special_handling_of_binders(
- |e| normalize_whnf(ctx.clone(), e.clone()),
- |x, e| normalize_whnf(ctx.skip(x), e.clone()),
- X::clone,
- |_| unreachable!(),
- Label::clone,
- );
+ expr => {
+ // Recursively normalize subexpressions
+ let expr: ExprF<WHNF, Label, X, X> = expr
+ .map_ref_with_special_handling_of_binders(
+ |e| normalize_whnf(ctx.clone(), e.clone()),
+ |x, e| normalize_whnf(ctx.skip(x), e.clone()),
+ X::clone,
+ |_| unreachable!(),
+ Label::clone,
+ );
- normalize_last_layer(ctx, expr)
+ normalize_last_layer(expr)
+ }
+ }
}
/// When all sub-expressions have been (partially) normalized, eval the remaining toplevel layer.
-fn normalize_last_layer(
- ctx: NormalizationContext,
- expr: ExprF<WHNF, Label, X, X>,
-) -> WHNF {
+fn normalize_last_layer(expr: ExprF<WHNF, Label, X, X>) -> WHNF {
use dhall_core::BinOp::*;
use WHNF::*;
- let expr = match expr {
- ExprF::App(v, a) => return v.app(a),
+ match expr {
+ ExprF::App(v, a) => v.app(a),
- ExprF::BinOp(BoolAnd, BoolLit(true), y) => return y,
- ExprF::BinOp(BoolAnd, x, BoolLit(true)) => return x,
- ExprF::BinOp(BoolAnd, BoolLit(false), _) => return BoolLit(false),
- ExprF::BinOp(BoolAnd, _, BoolLit(false)) => return BoolLit(false),
- ExprF::BinOp(BoolOr, BoolLit(true), _) => return BoolLit(true),
- ExprF::BinOp(BoolOr, _, BoolLit(true)) => return BoolLit(true),
- ExprF::BinOp(BoolOr, BoolLit(false), y) => return y,
- ExprF::BinOp(BoolOr, x, BoolLit(false)) => return x,
- ExprF::BinOp(BoolEQ, BoolLit(true), y) => return y,
- ExprF::BinOp(BoolEQ, x, BoolLit(true)) => return x,
- ExprF::BinOp(BoolNE, BoolLit(false), y) => return y,
- ExprF::BinOp(BoolNE, x, BoolLit(false)) => return x,
- ExprF::BinOp(BoolEQ, BoolLit(x), BoolLit(y)) => return BoolLit(x == y),
- ExprF::BinOp(BoolNE, BoolLit(x), BoolLit(y)) => return BoolLit(x != y),
+ ExprF::BinOp(BoolAnd, BoolLit(true), y) => y,
+ ExprF::BinOp(BoolAnd, x, BoolLit(true)) => x,
+ ExprF::BinOp(BoolAnd, BoolLit(false), _) => BoolLit(false),
+ ExprF::BinOp(BoolAnd, _, BoolLit(false)) => BoolLit(false),
+ ExprF::BinOp(BoolOr, BoolLit(true), _) => BoolLit(true),
+ ExprF::BinOp(BoolOr, _, BoolLit(true)) => BoolLit(true),
+ ExprF::BinOp(BoolOr, BoolLit(false), y) => y,
+ ExprF::BinOp(BoolOr, x, BoolLit(false)) => x,
+ ExprF::BinOp(BoolEQ, BoolLit(true), y) => y,
+ ExprF::BinOp(BoolEQ, x, BoolLit(true)) => x,
+ ExprF::BinOp(BoolNE, BoolLit(false), y) => y,
+ ExprF::BinOp(BoolNE, x, BoolLit(false)) => x,
+ ExprF::BinOp(BoolEQ, BoolLit(x), BoolLit(y)) => BoolLit(x == y),
+ ExprF::BinOp(BoolNE, BoolLit(x), BoolLit(y)) => BoolLit(x != y),
- ExprF::BinOp(NaturalPlus, NaturalLit(0), y) => return y,
- ExprF::BinOp(NaturalPlus, x, NaturalLit(0)) => return x,
- ExprF::BinOp(NaturalTimes, NaturalLit(0), _) => return NaturalLit(0),
- ExprF::BinOp(NaturalTimes, _, NaturalLit(0)) => return NaturalLit(0),
- ExprF::BinOp(NaturalTimes, NaturalLit(1), y) => return y,
- ExprF::BinOp(NaturalTimes, x, NaturalLit(1)) => return x,
+ ExprF::BinOp(NaturalPlus, NaturalLit(0), y) => y,
+ ExprF::BinOp(NaturalPlus, x, NaturalLit(0)) => x,
+ ExprF::BinOp(NaturalTimes, NaturalLit(0), _) => NaturalLit(0),
+ ExprF::BinOp(NaturalTimes, _, NaturalLit(0)) => NaturalLit(0),
+ ExprF::BinOp(NaturalTimes, NaturalLit(1), y) => y,
+ ExprF::BinOp(NaturalTimes, x, NaturalLit(1)) => x,
ExprF::BinOp(NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
- return NaturalLit(x + y)
+ NaturalLit(x + y)
}
ExprF::BinOp(NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
- return NaturalLit(x * y)
+ NaturalLit(x * y)
}
- ExprF::BinOp(ListAppend, EmptyListLit(_), y) => return y,
- ExprF::BinOp(ListAppend, x, EmptyListLit(_)) => return x,
+ ExprF::BinOp(ListAppend, EmptyListLit(_), y) => y,
+ ExprF::BinOp(ListAppend, x, EmptyListLit(_)) => x,
ExprF::BinOp(ListAppend, NEListLit(mut xs), NEListLit(mut ys)) => {
xs.append(&mut ys);
- return NEListLit(xs);
+ NEListLit(xs)
}
ExprF::BinOp(TextAppend, TextLit(mut x), TextLit(mut y)) => {
x.append(&mut y);
- return TextLit(x);
+ TextLit(x)
}
- ExprF::Field(UnionType(ctx, kts), l) => {
- return UnionConstructor(ctx, l, kts)
- }
- ExprF::Field(RecordLit(mut kvs), l) => {
- match kvs.remove(&l) {
- Some(r) => return r.normalize(),
- // Return ownership
- None => ExprF::Field(RecordLit(kvs), l),
+ ExprF::Field(UnionType(ctx, kts), l) => UnionConstructor(ctx, l, kts),
+ ExprF::Field(RecordLit(mut kvs), l) => match kvs.remove(&l) {
+ Some(r) => r.normalize(),
+ None => {
+ // Couldn't do anything useful, so just normalize subexpressions
+ Expr(rc(ExprF::Field(RecordLit(kvs).normalize_to_expr(), l)))
}
- }
- // Always simplify `x.{}` to `{}`
+ },
ExprF::Projection(_, ls) if ls.is_empty() => {
- return RecordLit(std::collections::BTreeMap::new())
+ RecordLit(std::collections::BTreeMap::new())
}
- ExprF::Projection(RecordLit(mut kvs), ls) => {
- return RecordLit(
- ls.into_iter()
- .filter_map(|l| kvs.remove(&l).map(|x| (l, x)))
- .collect(),
- )
+ ExprF::Projection(RecordLit(mut kvs), ls) => RecordLit(
+ ls.into_iter()
+ .filter_map(|l| kvs.remove(&l).map(|x| (l, x)))
+ .collect(),
+ ),
+ ExprF::Merge(RecordLit(mut handlers), e, t) => {
+ let e = match e {
+ UnionConstructor(ctor_ctx, l, kts) => match handlers.remove(&l)
+ {
+ Some(h) => return h.normalize(),
+ None => UnionConstructor(ctor_ctx, l, kts),
+ },
+ UnionLit(l, v, (kts_ctx, kts)) => match handlers.remove(&l) {
+ Some(h) => {
+ let h = h.normalize();
+ let v = v.normalize();
+ return h.app(v);
+ }
+ None => UnionLit(l, v, (kts_ctx, kts)),
+ },
+ e => e,
+ };
+ // Couldn't do anything useful, so just normalize subexpressions
+ Expr(rc(ExprF::Merge(
+ RecordLit(handlers).normalize_to_expr(),
+ e.normalize_to_expr(),
+ t.map(WHNF::normalize_to_expr),
+ )))
}
- ExprF::Merge(
- RecordLit(mut handlers),
- UnionConstructor(ctor_ctx, l, kts),
- t,
- ) => match handlers.remove(&l) {
- Some(h) => return h.normalize(),
- // Return ownership
- None => ExprF::Merge(
- RecordLit(handlers),
- UnionConstructor(ctor_ctx, l, kts),
- t,
- ),
- },
- ExprF::Merge(
- RecordLit(mut handlers),
- UnionLit(l, v, (kts_ctx, kts)),
- t,
- ) => match handlers.remove(&l) {
- Some(h) => {
- let h = h.normalize();
- let v = v.normalize();
- return normalize_last_layer(ctx, ExprF::App(h, v));
- }
- // Return ownership
- None => ExprF::Merge(
- RecordLit(handlers),
- UnionLit(l, v, (kts_ctx, kts)),
- t,
- ),
- },
- expr => expr,
- };
-
- // Couldn't do anything useful, so just normalize subexpressions
- Expr(rc(expr.map_ref_simple(|e| e.clone().normalize_to_expr())))
+ // Couldn't do anything useful, so just normalize subexpressions
+ expr => {
+ Expr(rc(expr.map_ref_simple(|e| e.clone().normalize_to_expr())))
+ }
+ }
}
/// Reduce an expression to its normal form, performing beta reduction