summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2019-04-20 00:20:41 +0200
committerNadrieril2019-04-20 00:20:41 +0200
commit2f411181e4abe05bf9ad9015654348fa8e13495e (patch)
tree4e9234db765e9a1f30d27cc249ebc33fba21ad97
parent8fbd51228e392e8a6e6281e3f136f4e07760c41f (diff)
Optionals and unions
Diffstat (limited to '')
-rw-r--r--dhall/src/normalize.rs120
1 files changed, 96 insertions, 24 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 5766766..d02dd80 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -244,15 +244,26 @@ where
/// 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.
+///
+/// Each variant captures the relevant contexts when it is constructed. Conceptually each
+/// subexpression has its own context, but in practise contexts can be shared when sensible, to
+/// avoid unnecessary allocations.
#[derive(Debug, Clone)]
enum WHNF {
Closure(Closure),
BoolLit(bool),
NaturalLit(Natural),
+ EmptyOptionalLit(NormalizationContext, InputSubExpr),
+ NEOptionalLit(NormalizationContext, InputSubExpr),
EmptyListLit(NormalizationContext, InputSubExpr),
NEListLit(Vec<(NormalizationContext, Vec<InputSubExpr>)>),
RecordLit(NormalizationContext, BTreeMap<Label, InputSubExpr>),
UnionType(NormalizationContext, BTreeMap<Label, Option<InputSubExpr>>),
+ UnionLit(
+ Label,
+ Box<WHNF>,
+ (NormalizationContext, BTreeMap<Label, Option<InputSubExpr>>),
+ ),
Expr(OutputSubExpr),
}
@@ -263,6 +274,12 @@ impl WHNF {
WHNF::Closure(c) => c.normalize_to_expr(),
WHNF::BoolLit(b) => rc(ExprF::BoolLit(b)),
WHNF::NaturalLit(n) => rc(ExprF::NaturalLit(n)),
+ WHNF::EmptyOptionalLit(ctx, e) => rc(ExprF::EmptyOptionalLit(
+ normalize_whnf(&ctx, e).normalize_to_expr(),
+ )),
+ WHNF::NEOptionalLit(ctx, e) => rc(ExprF::NEOptionalLit(
+ normalize_whnf(&ctx, e).normalize_to_expr(),
+ )),
WHNF::EmptyListLit(ctx, e) => rc(ExprF::EmptyListLit(
normalize_whnf(&ctx, e).normalize_to_expr(),
)),
@@ -282,8 +299,8 @@ impl WHNF {
})
.collect(),
)),
- WHNF::UnionType(ctx, kvs) => rc(ExprF::UnionType(
- kvs.into_iter()
+ WHNF::UnionType(ctx, kts) => rc(ExprF::UnionType(
+ kts.into_iter()
.map(|(k, v)| {
(
k,
@@ -294,6 +311,20 @@ impl WHNF {
})
.collect(),
)),
+ WHNF::UnionLit(l, v, (kts_ctx, kts)) => rc(ExprF::UnionLit(
+ l,
+ v.normalize_to_expr(),
+ kts.into_iter()
+ .map(|(k, v)| {
+ (
+ k,
+ v.map(|v| {
+ normalize_whnf(&kts_ctx, v).normalize_to_expr()
+ }),
+ )
+ })
+ .collect(),
+ )),
WHNF::Expr(e) => e,
}
}
@@ -304,6 +335,12 @@ impl WHNF {
WHNF::Expr(e) => WHNF::Expr(shift0(delta, label, &e)),
WHNF::BoolLit(b) => WHNF::BoolLit(b),
WHNF::NaturalLit(n) => WHNF::NaturalLit(n),
+ WHNF::EmptyOptionalLit(ctx, e) => {
+ WHNF::EmptyOptionalLit(ctx, shift0(delta, label, &e))
+ }
+ WHNF::NEOptionalLit(ctx, e) => {
+ WHNF::NEOptionalLit(ctx, shift0(delta, label, &e))
+ }
WHNF::EmptyListLit(ctx, e) => {
WHNF::EmptyListLit(ctx, shift0(delta, label, &e))
}
@@ -325,12 +362,22 @@ impl WHNF {
.map(|(k, v)| (k, shift0(delta, label, &v)))
.collect(),
),
- WHNF::UnionType(ctx, kvs) => WHNF::UnionType(
+ WHNF::UnionType(ctx, kts) => WHNF::UnionType(
ctx,
- kvs.into_iter()
+ kts.into_iter()
.map(|(k, v)| (k, v.map(|v| shift0(delta, label, &v))))
.collect(),
),
+ WHNF::UnionLit(l, v, (kts_ctx, kts)) => WHNF::UnionLit(
+ l,
+ Box::new(v.shift0(delta, label)),
+ (
+ kts_ctx,
+ kts.into_iter()
+ .map(|(k, v)| (k, v.map(|v| shift0(delta, label, &v))))
+ .collect(),
+ ),
+ ),
}
}
}
@@ -368,18 +415,7 @@ impl Closure {
}
}
Closure::UnionConstructor(ctx, l, kts) => {
- let kts = kts
- .into_iter()
- .map(|(k, v)| {
- (
- k,
- v.map(|v| {
- normalize_whnf(&ctx, v).normalize_to_expr()
- }),
- )
- })
- .collect();
- WHNF::Expr(rc(ExprF::UnionLit(l, val.normalize_to_expr(), kts)))
+ WHNF::UnionLit(l, Box::new(val), (ctx, kts))
}
}
}
@@ -522,10 +558,17 @@ fn reval(ctx: &NormalizationContext, expr: OutputSubExpr) -> WHNF {
}
ExprF::BoolLit(b) => WHNF::BoolLit(b),
ExprF::NaturalLit(n) => WHNF::NaturalLit(n),
+ ExprF::EmptyOptionalLit(e) => WHNF::EmptyOptionalLit(ctx.clone(), e),
+ ExprF::NEOptionalLit(e) => WHNF::NEOptionalLit(ctx.clone(), e),
ExprF::EmptyListLit(e) => WHNF::EmptyListLit(ctx.clone(), e),
ExprF::NEListLit(elts) => WHNF::NEListLit(vec![(ctx.clone(), elts)]),
ExprF::RecordLit(kvs) => WHNF::RecordLit(ctx.clone(), kvs),
ExprF::UnionType(kvs) => WHNF::UnionType(ctx.clone(), kvs),
+ ExprF::UnionLit(l, x, kts) => WHNF::UnionLit(
+ l,
+ Box::new(normalize_whnf(ctx, x)),
+ (ctx.clone(), kts),
+ ),
_ => WHNF::Expr(expr),
}
}
@@ -554,6 +597,18 @@ fn normalize_whnf(ctx: &NormalizationContext, expr: InputSubExpr) -> WHNF {
}
ExprF::BoolLit(b) => return WHNF::BoolLit(*b),
ExprF::NaturalLit(n) => return WHNF::NaturalLit(*n),
+ ExprF::OldOptionalLit(None, t) => {
+ return WHNF::EmptyOptionalLit(ctx.clone(), t.clone())
+ }
+ ExprF::OldOptionalLit(Some(x), _) => {
+ return WHNF::NEOptionalLit(ctx.clone(), x.clone())
+ }
+ ExprF::EmptyOptionalLit(e) => {
+ return WHNF::EmptyOptionalLit(ctx.clone(), e.clone())
+ }
+ ExprF::NEOptionalLit(e) => {
+ return WHNF::NEOptionalLit(ctx.clone(), e.clone())
+ }
ExprF::EmptyListLit(e) => {
return WHNF::EmptyListLit(ctx.clone(), e.clone())
}
@@ -566,6 +621,13 @@ fn normalize_whnf(ctx: &NormalizationContext, expr: InputSubExpr) -> WHNF {
ExprF::UnionType(kvs) => {
return WHNF::UnionType(ctx.clone(), kvs.clone())
}
+ ExprF::UnionLit(l, x, kts) => {
+ return WHNF::UnionLit(
+ l.clone(),
+ Box::new(normalize_whnf(ctx, x.clone())),
+ (ctx.clone(), kts.clone()),
+ )
+ }
ExprF::BoolIf(b, e1, e2) => {
let b = normalize_whnf(ctx, b.clone());
match b {
@@ -687,6 +749,22 @@ fn normalize_last_layer(
t,
),
},
+ Merge(
+ WHNF::RecordLit(record_ctx, mut handlers),
+ WHNF::UnionLit(l, v, (kts_ctx, kts)),
+ t,
+ ) => match handlers.remove(&l) {
+ Some(h) => {
+ let h = normalize_whnf(&kts_ctx, h);
+ return normalize_last_layer(ctx, App(h, *v));
+ }
+ // Return ownership
+ None => Merge(
+ WHNF::RecordLit(record_ctx, handlers),
+ WHNF::UnionLit(l, v, (kts_ctx, kts)),
+ t,
+ ),
+ },
expr => expr,
};
@@ -705,8 +783,7 @@ fn normalize_last_layer(
BoolIf(BoolLit(_), _, _) => unreachable!(),
// TODO: interpolation
// TextLit(t) =>
- OldOptionalLit(None, t) => Done(EmptyOptionalLit(t.roll())),
- OldOptionalLit(Some(x), _) => Done(NEOptionalLit(x.roll())),
+ OldOptionalLit(_, _) => unreachable!(),
BinOp(BoolAnd, BoolLit(_), BoolLit(_)) => unreachable!(),
BinOp(BoolOr, BoolLit(_), BoolLit(_)) => unreachable!(),
BinOp(BoolEQ, BoolLit(_), BoolLit(_)) => unreachable!(),
@@ -717,12 +794,7 @@ fn normalize_last_layer(
BinOp(ListAppend, EmptyListLit(_), _) => unreachable!(),
BinOp(ListAppend, _, EmptyListLit(_)) => unreachable!(),
BinOp(ListAppend, NEListLit(_), NEListLit(_)) => unreachable!(),
- Merge(RecordLit(handlers), UnionLit(l, v, _), _) => {
- match handlers.get(&l) {
- Some(h) => Continue(App(h.clone(), v.clone())),
- None => DoneAsIs,
- }
- }
+ Merge(RecordLit(_), UnionLit(_, _, _), _) => unreachable!(),
Field(RecordLit(_), _) => unreachable!(),
Field(UnionType(_), _) => unreachable!(),
Projection(_, ls) if ls.is_empty() => unreachable!(),