diff options
| -rw-r--r-- | dhall/src/phase/normalize.rs | 318 |
1 files changed, 153 insertions, 165 deletions
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index d9e4331..048c25e 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -344,6 +344,37 @@ pub(crate) fn squash_textlit( ret } +/// Reduces the imput expression to a Value. Evaluates as little as possible. +pub(crate) fn normalize_whnf( + ctx: NormalizationContext, + expr: InputSubExpr, +) -> Value { + match expr.as_ref() { + ExprF::Embed(e) => return e.to_value(), + ExprF::Var(v) => return ctx.lookup(v), + _ => {} + } + + // Thunk subexpressions + let expr: ExprF<Thunk, Label, X> = + expr.as_ref().map_ref_with_special_handling_of_binders( + |e| Thunk::new(ctx.clone(), e.clone()), + |x, e| Thunk::new(ctx.skip(x), e.clone()), + |_| unreachable!(), + Label::clone, + ); + + normalize_one_layer(expr) +} + +// Small helper enum to avoid repetition +enum Ret<'a> { + RetValue(Value), + RetThunk(Thunk), + RetThunkRef(&'a Thunk), + RetExpr(ExprF<Thunk, Label, X>), +} + fn merge_maps<K, V>( map1: &BTreeMap<K, V>, map2: &BTreeMap<K, V>, @@ -369,45 +400,135 @@ where kvs } -/// Reduces the imput expression to a Value. Evaluates as little as possible. -pub(crate) fn normalize_whnf( - ctx: NormalizationContext, - expr: InputSubExpr, -) -> Value { - match expr.as_ref() { - ExprF::Embed(e) => return e.to_value(), - ExprF::Var(v) => return ctx.lookup(v), - _ => {} - } +fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> { + use BinOp::{ + BoolAnd, BoolEQ, BoolNE, BoolOr, ListAppend, NaturalPlus, NaturalTimes, + RecursiveRecordMerge, RecursiveRecordTypeMerge, RightBiasedRecordMerge, + TextAppend, + }; + use Ret::{RetThunkRef, RetValue}; + use Value::{ + BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType, + TextLit, + }; + let x_borrow = x.as_value(); + let y_borrow = y.as_value(); + Some(match (o, &*x_borrow, &*y_borrow) { + (BoolAnd, BoolLit(true), _) => RetThunkRef(y), + (BoolAnd, _, BoolLit(true)) => RetThunkRef(x), + (BoolAnd, BoolLit(false), _) => RetValue(BoolLit(false)), + (BoolAnd, _, BoolLit(false)) => RetValue(BoolLit(false)), + (BoolAnd, _, _) if x == y => RetThunkRef(x), + (BoolOr, BoolLit(true), _) => RetValue(BoolLit(true)), + (BoolOr, _, BoolLit(true)) => RetValue(BoolLit(true)), + (BoolOr, BoolLit(false), _) => RetThunkRef(y), + (BoolOr, _, BoolLit(false)) => RetThunkRef(x), + (BoolOr, _, _) if x == y => RetThunkRef(x), + (BoolEQ, BoolLit(true), _) => RetThunkRef(y), + (BoolEQ, _, BoolLit(true)) => RetThunkRef(x), + (BoolEQ, BoolLit(x), BoolLit(y)) => RetValue(BoolLit(x == y)), + (BoolEQ, _, _) if x == y => RetValue(BoolLit(true)), + (BoolNE, BoolLit(false), _) => RetThunkRef(y), + (BoolNE, _, BoolLit(false)) => RetThunkRef(x), + (BoolNE, BoolLit(x), BoolLit(y)) => RetValue(BoolLit(x != y)), + (BoolNE, _, _) if x == y => RetValue(BoolLit(false)), - // Thunk subexpressions - let expr: ExprF<Thunk, Label, X> = - expr.as_ref().map_ref_with_special_handling_of_binders( - |e| Thunk::new(ctx.clone(), e.clone()), - |x, e| Thunk::new(ctx.skip(x), e.clone()), - |_| unreachable!(), - Label::clone, - ); + (NaturalPlus, NaturalLit(0), _) => RetThunkRef(y), + (NaturalPlus, _, NaturalLit(0)) => RetThunkRef(x), + (NaturalPlus, NaturalLit(x), NaturalLit(y)) => { + RetValue(NaturalLit(x + y)) + } + (NaturalTimes, NaturalLit(0), _) => RetValue(NaturalLit(0)), + (NaturalTimes, _, NaturalLit(0)) => RetValue(NaturalLit(0)), + (NaturalTimes, NaturalLit(1), _) => RetThunkRef(y), + (NaturalTimes, _, NaturalLit(1)) => RetThunkRef(x), + (NaturalTimes, NaturalLit(x), NaturalLit(y)) => { + RetValue(NaturalLit(x * y)) + } - normalize_one_layer(expr) + (ListAppend, EmptyListLit(_), _) => RetThunkRef(y), + (ListAppend, _, EmptyListLit(_)) => RetThunkRef(x), + (ListAppend, NEListLit(xs), NEListLit(ys)) => { + RetValue(NEListLit(xs.iter().chain(ys.iter()).cloned().collect())) + } + + (TextAppend, TextLit(x), _) if x.is_empty() => RetThunkRef(y), + (TextAppend, _, TextLit(y)) if y.is_empty() => RetThunkRef(x), + (TextAppend, TextLit(x), TextLit(y)) => { + RetValue(TextLit(squash_textlit(x.iter().chain(y.iter()).cloned()))) + } + (TextAppend, TextLit(x), _) => { + use std::iter::once; + let y = InterpolatedTextContents::Expr(y.clone()); + RetValue(TextLit(squash_textlit(x.iter().cloned().chain(once(y))))) + } + (TextAppend, _, TextLit(y)) => { + use std::iter::once; + let x = InterpolatedTextContents::Expr(x.clone()); + RetValue(TextLit(squash_textlit(once(x).chain(y.iter().cloned())))) + } + + (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { + RetThunkRef(x) + } + (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { + RetThunkRef(y) + } + (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { + let mut kvs = kvs2.clone(); + for (x, v) in kvs1 { + // Insert only if key not already present + kvs.entry(x.clone()).or_insert_with(|| v.clone()); + } + RetValue(RecordLit(kvs)) + } + + (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { + RetThunkRef(x) + } + (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { + RetThunkRef(y) + } + (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { + let kvs = merge_maps(kvs1, kvs2, |v1, v2| { + Thunk::from_partial_expr(ExprF::BinOp( + RecursiveRecordMerge, + v1.clone(), + v2.clone(), + )) + }); + RetValue(RecordLit(kvs)) + } + + (RecursiveRecordTypeMerge, _, RecordType(kvs)) if kvs.is_empty() => { + RetThunkRef(x) + } + (RecursiveRecordTypeMerge, RecordType(kvs), _) if kvs.is_empty() => { + RetThunkRef(y) + } + (RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => { + let kvs = merge_maps(kvs1, kvs2, |v1, v2| { + TypeThunk::from_thunk(Thunk::from_partial_expr(ExprF::BinOp( + RecursiveRecordTypeMerge, + v1.to_thunk(), + v2.to_thunk(), + ))) + }); + RetValue(RecordType(kvs)) + } + + _ => return None, + }) } pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Label, X>) -> Value { + use Ret::{RetExpr, RetThunk, RetThunkRef, RetValue}; use Value::{ BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, IntegerLit, Lam, NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType, TextLit, UnionConstructor, UnionLit, UnionType, }; - // Small helper enum to avoid repetition - enum Ret<'a> { - RetValue(Value), - RetThunk(Thunk), - RetThunkRef(&'a Thunk), - RetExpr(ExprF<Thunk, Label, X>), - } - use Ret::{RetExpr, RetThunk, RetThunkRef, RetValue}; - let ret = match expr { ExprF::Embed(_) => unreachable!(), ExprF::Var(_) => unreachable!(), @@ -492,143 +613,10 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Label, X>) -> Value { } } } - ExprF::BinOp(o, ref x, ref y) => { - use BinOp::{ - BoolAnd, BoolEQ, BoolNE, BoolOr, ListAppend, NaturalPlus, - NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge, - RightBiasedRecordMerge, TextAppend, - }; - let x_borrow = x.as_value(); - let y_borrow = y.as_value(); - match (o, &*x_borrow, &*y_borrow) { - (BoolAnd, BoolLit(true), _) => RetThunkRef(y), - (BoolAnd, _, BoolLit(true)) => RetThunkRef(x), - (BoolAnd, BoolLit(false), _) => RetValue(BoolLit(false)), - (BoolAnd, _, BoolLit(false)) => RetValue(BoolLit(false)), - (BoolAnd, _, _) if x == y => RetThunkRef(x), - (BoolOr, BoolLit(true), _) => RetValue(BoolLit(true)), - (BoolOr, _, BoolLit(true)) => RetValue(BoolLit(true)), - (BoolOr, BoolLit(false), _) => RetThunkRef(y), - (BoolOr, _, BoolLit(false)) => RetThunkRef(x), - (BoolOr, _, _) if x == y => RetThunkRef(x), - (BoolEQ, BoolLit(true), _) => RetThunkRef(y), - (BoolEQ, _, BoolLit(true)) => RetThunkRef(x), - (BoolEQ, BoolLit(x), BoolLit(y)) => RetValue(BoolLit(x == y)), - (BoolEQ, _, _) if x == y => RetValue(BoolLit(true)), - (BoolNE, BoolLit(false), _) => RetThunkRef(y), - (BoolNE, _, BoolLit(false)) => RetThunkRef(x), - (BoolNE, BoolLit(x), BoolLit(y)) => RetValue(BoolLit(x != y)), - (BoolNE, _, _) if x == y => RetValue(BoolLit(false)), - - (NaturalPlus, NaturalLit(0), _) => RetThunkRef(y), - (NaturalPlus, _, NaturalLit(0)) => RetThunkRef(x), - (NaturalPlus, NaturalLit(x), NaturalLit(y)) => { - RetValue(NaturalLit(x + y)) - } - (NaturalTimes, NaturalLit(0), _) => RetValue(NaturalLit(0)), - (NaturalTimes, _, NaturalLit(0)) => RetValue(NaturalLit(0)), - (NaturalTimes, NaturalLit(1), _) => RetThunkRef(y), - (NaturalTimes, _, NaturalLit(1)) => RetThunkRef(x), - (NaturalTimes, NaturalLit(x), NaturalLit(y)) => { - RetValue(NaturalLit(x * y)) - } - - (ListAppend, EmptyListLit(_), _) => RetThunkRef(y), - (ListAppend, _, EmptyListLit(_)) => RetThunkRef(x), - (ListAppend, NEListLit(xs), NEListLit(ys)) => RetValue( - NEListLit(xs.iter().chain(ys.iter()).cloned().collect()), - ), - - (TextAppend, TextLit(x), _) if x.is_empty() => RetThunkRef(y), - (TextAppend, _, TextLit(y)) if y.is_empty() => RetThunkRef(x), - (TextAppend, TextLit(x), TextLit(y)) => RetValue(TextLit( - squash_textlit(x.iter().chain(y.iter()).cloned()), - )), - (TextAppend, TextLit(x), _) => { - use std::iter::once; - let y = InterpolatedTextContents::Expr(y.clone()); - RetValue(TextLit(squash_textlit( - x.iter().cloned().chain(once(y)), - ))) - } - (TextAppend, _, TextLit(y)) => { - use std::iter::once; - let x = InterpolatedTextContents::Expr(x.clone()); - RetValue(TextLit(squash_textlit( - once(x).chain(y.iter().cloned()), - ))) - } - - (RightBiasedRecordMerge, _, RecordLit(kvs)) - if kvs.is_empty() => - { - RetThunkRef(x) - } - (RightBiasedRecordMerge, RecordLit(kvs), _) - if kvs.is_empty() => - { - RetThunkRef(y) - } - (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let mut kvs = kvs2.clone(); - for (x, v) in kvs1 { - // Insert only if key not already present - kvs.entry(x.clone()).or_insert_with(|| v.clone()); - } - RetValue(RecordLit(kvs)) - } - - (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - RetThunkRef(x) - } - (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - RetThunkRef(y) - } - (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let kvs = merge_maps(kvs1, kvs2, |v1, v2| { - Thunk::from_partial_expr(ExprF::BinOp( - RecursiveRecordMerge, - v1.clone(), - v2.clone(), - )) - }); - RetValue(RecordLit(kvs)) - } - - (RecursiveRecordTypeMerge, _, RecordType(kvs)) - if kvs.is_empty() => - { - RetThunkRef(x) - } - (RecursiveRecordTypeMerge, RecordType(kvs), _) - if kvs.is_empty() => - { - RetThunkRef(y) - } - ( - RecursiveRecordTypeMerge, - RecordType(kvs1), - RecordType(kvs2), - ) => { - let kvs = merge_maps(kvs1, kvs2, |v1, v2| { - TypeThunk::from_thunk(Thunk::from_partial_expr( - ExprF::BinOp( - RecursiveRecordTypeMerge, - v1.to_thunk(), - v2.to_thunk(), - ), - )) - }); - RetValue(RecordType(kvs)) - } - - _ => { - drop(x_borrow); - drop(y_borrow); - RetExpr(expr) - } - } - } + ExprF::BinOp(o, ref x, ref y) => match apply_binop(o, x, y) { + Some(ret) => ret, + None => RetExpr(expr), + }, ExprF::Projection(_, ls) if ls.is_empty() => { RetValue(RecordLit(std::collections::BTreeMap::new())) |