summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/lib.rs1
-rw-r--r--dhall/src/normalize.rs299
2 files changed, 179 insertions, 121 deletions
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index 544df6e..c85b962 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -3,6 +3,7 @@
#![feature(slice_patterns)]
#![feature(label_break_value)]
#![feature(non_exhaustive)]
+#![feature(bind_by_move_pattern_guards)]
#![cfg_attr(test, feature(custom_inner_attributes))]
#![allow(
clippy::type_complexity,
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 7a9ca2f..90c6841 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -216,6 +216,39 @@ where
Continue(ExprF::App(ret, rest))
}
+#[derive(Debug, Clone, PartialEq, Eq)]
+enum Value {
+ Expr(SubExpr<X, X>),
+ Lam(
+ Label,
+ SubExpr<X, Normalized<'static>>,
+ SubExpr<X, Normalized<'static>>,
+ ),
+ // App(
+ // SubExpr<X, Normalized<'static>>,
+ // Vec<SubExpr<X, Normalized<'static>>>,
+ // ),
+}
+
+impl Value {
+ fn into_expr(self, ctx: &NormalizationContext) -> SubExpr<X, X> {
+ match self {
+ Value::Expr(e) => e,
+ Value::Lam(x, t, e) => rc(ExprF::Lam(
+ x.clone(),
+ normalize_value(ctx, t).into_expr(ctx),
+ normalize_value(&ctx.skip(&x), e).into_expr(&ctx.skip(&x)),
+ )),
+ // Value::App(f, args) => rc(ExprF::App(
+ // normalize_value(ctx, f).into_expr(ctx),
+ // args.into_iter()
+ // .map(|e| normalize_value(ctx, e).into_expr(ctx))
+ // .collect(),
+ // )),
+ }
+ }
+}
+
#[derive(Debug, Clone)]
enum EnvItem {
Expr(SubExpr<X, X>),
@@ -268,138 +301,161 @@ enum WhatNext<'a, N, E> {
DoneAsIs,
}
+fn reval(expr: SubExpr<X, X>) -> Value {
+ match expr.as_ref() {
+ ExprF::Lam(x, t, e) => {
+ Value::Lam(x.clone(), t.embed_absurd(), e.embed_absurd())
+ }
+ _ => Value::Expr(expr),
+ }
+}
+
fn normalize_value(
ctx: &NormalizationContext,
expr: SubExpr<X, Normalized<'static>>,
-) -> SubExpr<X, X> {
+) -> Value {
use dhall_core::BinOp::*;
use dhall_core::ExprF::*;
- match expr.as_ref() {
+ let e = match expr.as_ref() {
Let(x, _, r, b) => {
- let r = normalize_value(ctx, r.clone());
- normalize_value(&ctx.insert(x, r.clone()), b.clone())
- }
- e => {
- // Recursively normalize all subexpressions
- let expr: ExprF<Expr<X, X>, Label, X, Normalized<'static>> = e
- .map_ref_with_special_handling_of_binders(
- |e| normalize_value(ctx, e.clone()).unroll(),
- |x, e| normalize_value(&ctx.skip(x), e.clone()).unroll(),
- X::clone,
- Normalized::clone,
- Label::clone,
- );
+ let r = normalize_value(ctx, r.clone()).into_expr(ctx);
+ return normalize_value(&ctx.insert(x, r.clone()), b.clone());
+ }
+ Lam(x, t, e) => return Value::Lam(x.clone(), t.clone(), e.clone()),
+ e => e,
+ };
- use WhatNext::*;
- let what_next = match &expr {
- Let(_, _, _, _) => unreachable!(),
- Embed(e) => DoneRefSub(&e.0),
- Var(v) => DoneSub(ctx.lookup(v)),
- Annot(x, _) => DoneRef(x),
- Note(_, e) => DoneRef(e),
- App(f, args) if args.is_empty() => DoneRef(f),
- App(App(f, args1), args2) => Continue(App(
- f.clone(),
- args1
- .iter()
- .cloned()
- .chain(args2.iter().map(ExprF::roll))
- .collect(),
- )),
- App(Builtin(b), args) => apply_builtin(*b, args),
- App(Lam(x, _, b), args) => {
- let mut iter = args.iter();
- // We know args is nonempty
- let a = iter.next().unwrap();
- // Beta reduce
- let vx0 = &V(x.clone(), 0);
- let b2 = subst_shift(vx0, &a.roll(), &b);
- Continue(App(b2, iter.map(ExprF::roll).collect()))
- }
- App(UnionConstructor(l, kts), args) => {
- let mut iter = args.iter();
- // We know args is nonempty
- let a = iter.next().unwrap();
- let e = rc(UnionLit(l.clone(), rc(a.clone()), kts.clone()));
- Continue(App(e, iter.map(ExprF::roll).collect()))
- }
- BoolIf(BoolLit(true), t, _) => DoneRef(t),
- BoolIf(BoolLit(false), _, f) => DoneRef(f),
- // TODO: interpolation
- // TextLit(t) =>
- OldOptionalLit(None, t) => Done(EmptyOptionalLit(t.roll())),
- OldOptionalLit(Some(x), _) => Done(NEOptionalLit(x.roll())),
- BinOp(BoolAnd, BoolLit(x), BoolLit(y)) => {
- Done(BoolLit(*x && *y))
- }
- BinOp(BoolOr, BoolLit(x), BoolLit(y)) => {
- Done(BoolLit(*x || *y))
- }
- BinOp(BoolEQ, BoolLit(x), BoolLit(y)) => Done(BoolLit(x == y)),
- BinOp(BoolNE, BoolLit(x), BoolLit(y)) => Done(BoolLit(x != y)),
- BinOp(NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
- Done(NaturalLit(x + y))
- }
- BinOp(NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
- Done(NaturalLit(x * y))
- }
- BinOp(TextAppend, TextLit(x), TextLit(y)) => {
- Done(TextLit(x + y))
- }
- BinOp(ListAppend, EmptyListLit(_), y) => DoneRef(y),
- BinOp(ListAppend, x, EmptyListLit(_)) => DoneRef(x),
- BinOp(ListAppend, NEListLit(xs), NEListLit(ys)) => {
- let xs = xs.iter().cloned();
- let ys = ys.iter().cloned();
- Done(NEListLit(xs.chain(ys).collect()))
- }
- Merge(RecordLit(handlers), UnionLit(l, v, _), _) => {
- match handlers.get(&l) {
- Some(h) => Continue(App(h.clone(), vec![v.clone()])),
- None => DoneAsIs,
- }
- }
- Merge(RecordLit(handlers), UnionConstructor(l, _), _) => {
- match handlers.get(&l) {
- Some(h) => DoneRefSub(h),
- None => DoneAsIs,
- }
- }
- Field(RecordLit(kvs), l) => match kvs.get(&l) {
- Some(r) => DoneRefSub(r),
- None => DoneAsIs,
- },
- Field(UnionType(kts), l) => {
- Done(UnionConstructor(l.clone(), kts.clone()))
- }
- Projection(_, ls) if ls.is_empty() => {
- Done(RecordLit(std::collections::BTreeMap::new()))
- }
- Projection(RecordLit(kvs), ls) => Done(RecordLit(
- ls.iter()
- .filter_map(|l| {
- kvs.get(l).map(|x| (l.clone(), x.clone()))
- })
- .collect(),
- )),
- _ => DoneAsIs,
- };
+ // Recursively normalize all subexpressions
+ let expr: ExprF<Value, 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()),
+ X::clone,
+ Normalized::clone,
+ Label::clone,
+ );
- match what_next {
- Continue(e) => normalize_value(ctx, e.embed_absurd().roll()),
- Done(e) => e.roll(),
- DoneRef(e) => e.roll(),
- DoneSub(e) => e,
- DoneRefSub(e) => e.clone(),
- DoneAsIs => rc(expr.map_ref_simple(ExprF::roll).map_ref(
- SubExpr::clone,
- X::clone,
- |_| unreachable!(),
- Label::clone,
- )),
+ let expr = match expr {
+ App(v, args) if args.is_empty() => return v,
+ App(Value::Lam(x, _, b), args) => {
+ let mut iter = args.into_iter();
+ // We know args is nonempty
+ let a = iter.next().unwrap();
+ // Beta reduce
+ let ctx2 = ctx.insert(&x, a.into_expr(ctx));
+ let b2 = normalize_value(&ctx2, b).into_expr(&ctx2);
+ return normalize_value(
+ ctx,
+ App(b2, iter.map(|val| val.into_expr(ctx)).collect())
+ .embed_absurd()
+ .roll(),
+ );
+ }
+ expr => expr,
+ };
+
+ let expr: ExprF<Expr<X, X>, Label, X, Normalized<'static>> = expr
+ .map_ref_with_special_handling_of_binders(
+ |e| e.clone().into_expr(ctx).unroll(),
+ |x, e| e.clone().into_expr(&ctx.skip(x)).unroll(),
+ X::clone,
+ Normalized::clone,
+ Label::clone,
+ );
+
+ use WhatNext::*;
+ let what_next = match &expr {
+ Embed(e) => DoneRefSub(&e.0),
+ Var(v) => DoneSub(ctx.lookup(v)),
+ Annot(x, _) => DoneRef(x),
+ Note(_, e) => DoneRef(e),
+ App(_, args) if args.is_empty() => unreachable!(),
+ Let(_, _, _, _) => unreachable!(),
+ Lam(_, _, _) => unreachable!(),
+ App(App(f, args1), args2) => Continue(App(
+ f.clone(),
+ args1
+ .iter()
+ .cloned()
+ .chain(args2.iter().map(ExprF::roll))
+ .collect(),
+ )),
+ App(Builtin(b), args) => apply_builtin(*b, args),
+ App(Lam(_, _, _), _) => unreachable!(),
+ App(UnionConstructor(l, kts), args) => {
+ let mut iter = args.iter();
+ // We know args is nonempty
+ let a = iter.next().unwrap();
+ let e = rc(UnionLit(l.clone(), rc(a.clone()), kts.clone()));
+ Continue(App(e, iter.map(ExprF::roll).collect()))
+ }
+ BoolIf(BoolLit(true), t, _) => DoneRef(t),
+ BoolIf(BoolLit(false), _, f) => DoneRef(f),
+ // TODO: interpolation
+ // TextLit(t) =>
+ OldOptionalLit(None, t) => Done(EmptyOptionalLit(t.roll())),
+ OldOptionalLit(Some(x), _) => Done(NEOptionalLit(x.roll())),
+ BinOp(BoolAnd, BoolLit(x), BoolLit(y)) => Done(BoolLit(*x && *y)),
+ BinOp(BoolOr, BoolLit(x), BoolLit(y)) => Done(BoolLit(*x || *y)),
+ BinOp(BoolEQ, BoolLit(x), BoolLit(y)) => Done(BoolLit(x == y)),
+ BinOp(BoolNE, BoolLit(x), BoolLit(y)) => Done(BoolLit(x != y)),
+ BinOp(NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
+ Done(NaturalLit(x + y))
+ }
+ BinOp(NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
+ Done(NaturalLit(x * y))
+ }
+ BinOp(TextAppend, TextLit(x), TextLit(y)) => Done(TextLit(x + y)),
+ BinOp(ListAppend, EmptyListLit(_), y) => DoneRef(y),
+ BinOp(ListAppend, x, EmptyListLit(_)) => DoneRef(x),
+ BinOp(ListAppend, NEListLit(xs), NEListLit(ys)) => {
+ let xs = xs.iter().cloned();
+ let ys = ys.iter().cloned();
+ Done(NEListLit(xs.chain(ys).collect()))
+ }
+ Merge(RecordLit(handlers), UnionLit(l, v, _), _) => {
+ match handlers.get(&l) {
+ Some(h) => Continue(App(h.clone(), vec![v.clone()])),
+ None => DoneAsIs,
+ }
+ }
+ Merge(RecordLit(handlers), UnionConstructor(l, _), _) => {
+ match handlers.get(&l) {
+ Some(h) => DoneRefSub(h),
+ None => DoneAsIs,
}
}
+ Field(RecordLit(kvs), l) => match kvs.get(&l) {
+ Some(r) => DoneRefSub(r),
+ None => DoneAsIs,
+ },
+ Field(UnionType(kts), l) => {
+ Done(UnionConstructor(l.clone(), kts.clone()))
+ }
+ Projection(_, ls) if ls.is_empty() => {
+ Done(RecordLit(std::collections::BTreeMap::new()))
+ }
+ Projection(RecordLit(kvs), ls) => Done(RecordLit(
+ ls.iter()
+ .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone())))
+ .collect(),
+ )),
+ _ => DoneAsIs,
+ };
+
+ match what_next {
+ Continue(e) => normalize_value(ctx, e.embed_absurd().roll()),
+ Done(e) => reval(e.roll()),
+ DoneRef(e) => reval(e.roll()),
+ DoneSub(e) => reval(e),
+ DoneRefSub(e) => reval(e.clone()),
+ DoneAsIs => reval(rc(expr.map_ref_simple(ExprF::roll).map_ref(
+ SubExpr::clone,
+ X::clone,
+ |_| unreachable!(),
+ Label::clone,
+ ))),
}
}
@@ -414,6 +470,7 @@ fn normalize_value(
///
fn normalize(e: SubExpr<X, Normalized<'static>>) -> SubExpr<X, X> {
normalize_value(&NormalizationContext::new(), e)
+ .into_expr(&NormalizationContext::new())
}
#[cfg(test)]
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 10:21:37 +0000