From deeec70f6bd602f0f178766b8e89ec2585c279c0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 19 Apr 2019 22:29:41 +0200 Subject: Embrace WHNF --- dhall/src/normalize.rs | 156 ++++++++++++++++++++++++------------------------- 1 file changed, 77 insertions(+), 79 deletions(-) (limited to 'dhall/src') 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>, // } // 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), UnionType(NormalizationContext, BTreeMap>), 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), + AppliedBuiltin(NormalizationContext, Builtin, Vec), 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