From 29208b0bf3dd2667f92774dacb3a7f058c4cd895 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 5 Mar 2020 15:50:45 +0000 Subject: Implement some normalization simplifications --- dhall/build.rs | 11 +-- dhall/src/semantics/nze/normalize.rs | 156 ++++++++++++++++++----------------- dhall/src/syntax/ast/expr.rs | 2 +- 3 files changed, 83 insertions(+), 86 deletions(-) diff --git a/dhall/build.rs b/dhall/build.rs index d9bceeb..1612406 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -286,15 +286,8 @@ fn generate_tests() -> std::io::Result<()> { // TODO: doesn't typecheck || path == "unit/RightBiasedRecordMergeWithinRecordProjection" || path == "unit/Sort" - // // TODO: Further record simplifications - || path == "simplifications/rightBiasedMergeWithinRecordProjectionWithinFieldSelection0" - || path == "simplifications/rightBiasedMergeWithinRecordProjectionWithinFieldSelection1" - || path == "simplifications/rightBiasedMergeWithinRecursiveRecordMergeWithinFieldselection" + // TODO: Further record simplifications || path == "simplifications/issue661" - || path == "unit/RecursiveRecordMergeWithinFieldSelection0" - || path == "unit/RecursiveRecordMergeWithinFieldSelection1" - || path == "unit/RecursiveRecordMergeWithinFieldSelection2" - || path == "unit/RecursiveRecordMergeWithinFieldSelection3" }), input_type: FileType::Text, output_type: Some(FileType::Text), @@ -304,7 +297,7 @@ fn generate_tests() -> std::io::Result<()> { directory: "alpha-normalization/success/", variant: "AlphaNormalization", path_filter: Box::new(|path: &str| { - // This test doesn't typecheck + // This test is designed to not typecheck path == "unit/FunctionNestedBindingXXFree" }), input_type: FileType::Text, diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index dedd659..27862ee 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -233,7 +233,7 @@ pub(crate) fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { ExprKind::Builtin(b) => Ret::Nir(Nir::from_builtin_env(b, env)), ExprKind::Assert(_) => Ret::Expr(expr), ExprKind::App(v, a) => Ret::Nir(v.app(a)), - ExprKind::Lit(l) => Ret::NirKind(Lit(l.clone())), + ExprKind::Lit(l) => Ret::NirKind(Lit(l)), ExprKind::SomeLit(e) => Ret::NirKind(NEOptionalLit(e)), ExprKind::EmptyListLit(t) => { let arg = match t.kind() { @@ -286,23 +286,6 @@ pub(crate) fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { None => Ret::Expr(expr), }, - ExprKind::Projection(_, ref ls) if ls.is_empty() => { - Ret::NirKind(RecordLit(HashMap::new())) - } - ExprKind::Projection(ref v, ref ls) => match v.kind() { - RecordLit(kvs) => Ret::NirKind(RecordLit( - ls.iter() - .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone()))) - .collect(), - )), - PartialExpr(ExprKind::Projection(v2, _)) => { - return normalize_one_layer( - ExprKind::Projection(v2.clone(), ls.clone()), - env, - ) - } - _ => Ret::Expr(expr), - }, ExprKind::Field(ref v, ref l) => match v.kind() { RecordLit(kvs) => match kvs.get(l) { Some(r) => Ret::Nir(r.clone()), @@ -311,6 +294,12 @@ pub(crate) fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { UnionType(kts) => { Ret::NirKind(UnionConstructor(l.clone(), kts.clone())) } + PartialExpr(ExprKind::Projection(x, _)) => { + return normalize_one_layer( + ExprKind::Field(x.clone(), l.clone()), + env, + ) + } PartialExpr(ExprKind::BinOp( BinOp::RightBiasedRecordMerge, x, @@ -329,11 +318,11 @@ pub(crate) fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { Some(r) => Ret::Expr(ExprKind::Field( Nir::from_kind(PartialExpr(ExprKind::BinOp( BinOp::RightBiasedRecordMerge, - Nir::from_kind(RecordLit({ - let mut kvs = HashMap::new(); - kvs.insert(l.clone(), r.clone()); - kvs - })), + Nir::from_kind(RecordLit( + Some((l.clone(), r.clone())) + .into_iter() + .collect(), + )), y.clone(), ))), l.clone(), @@ -347,66 +336,81 @@ pub(crate) fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { }, _ => Ret::Expr(expr), }, - PartialExpr(ExprKind::BinOp( - BinOp::RecursiveRecordTypeMerge, - x, - y, - )) => match (x.kind(), y.kind()) { - (RecordLit(kvs), _) => match kvs.get(l) { - Some(_) => Ret::Expr(expr), - None => { - return normalize_one_layer( - ExprKind::Field(y.clone(), l.clone()), - env, - ) - } - }, - (_, RecordLit(kvs)) => match kvs.get(l) { - Some(_) => Ret::Expr(expr), - None => { - return normalize_one_layer( - ExprKind::Field(x.clone(), l.clone()), - env, - ) - } - }, - _ => Ret::Expr(expr), - }, + PartialExpr(ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y)) => { + match (x.kind(), y.kind()) { + (RecordLit(kvs), _) => match kvs.get(l) { + Some(r) => Ret::Expr(ExprKind::Field( + Nir::from_kind(PartialExpr(ExprKind::BinOp( + BinOp::RecursiveRecordMerge, + Nir::from_kind(RecordLit( + Some((l.clone(), r.clone())) + .into_iter() + .collect(), + )), + y.clone(), + ))), + l.clone(), + )), + None => { + return normalize_one_layer( + ExprKind::Field(y.clone(), l.clone()), + env, + ) + } + }, + (_, RecordLit(kvs)) => match kvs.get(l) { + Some(r) => Ret::Expr(ExprKind::Field( + Nir::from_kind(PartialExpr(ExprKind::BinOp( + BinOp::RecursiveRecordMerge, + x.clone(), + Nir::from_kind(RecordLit( + Some((l.clone(), r.clone())) + .into_iter() + .collect(), + )), + ))), + l.clone(), + )), + None => { + return normalize_one_layer( + ExprKind::Field(x.clone(), l.clone()), + env, + ) + } + }, + _ => Ret::Expr(expr), + } + } + _ => Ret::Expr(expr), + }, + ExprKind::Projection(_, ref ls) if ls.is_empty() => { + Ret::NirKind(RecordLit(HashMap::new())) + } + ExprKind::Projection(ref v, ref ls) => match v.kind() { + RecordLit(kvs) => Ret::NirKind(RecordLit( + ls.iter() + .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone()))) + .collect(), + )), PartialExpr(ExprKind::Projection(v2, _)) => { return normalize_one_layer( - ExprKind::Field(v2.clone(), l.clone()), + ExprKind::Projection(v2.clone(), ls.clone()), env, ) } _ => Ret::Expr(expr), }, - - ExprKind::ProjectionByExpr(ref v, ref t) => match dbg!(v).kind() { - RecordLit(kvs) => match dbg!(t).kind() { - RecordType(kts) => Ret::NirKind(RecordLit( - kts.iter() - .filter_map(|(l, _)| { - kvs.get(l).map(|x| (l.clone(), x.clone())) - }) - .collect(), - )), - _ => Ret::Expr(expr), - }, - _ => match dbg!(t).kind() { - RecordType(kts) => { - use crate::syntax::map::DupTreeSet; - use std::iter::FromIterator; - - let ts = DupTreeSet::from_iter( - kts.iter().map(|(l, _)| l.clone()), - ); - return normalize_one_layer( - ExprKind::Projection(v.clone(), ts), - env, - ); - } - _ => Ret::Expr(expr), - }, + ExprKind::ProjectionByExpr(ref v, ref t) => match t.kind() { + RecordType(kts) => { + return normalize_one_layer( + ExprKind::Projection( + v.clone(), + kts.keys().cloned().collect(), + ), + env, + ) + } + _ => Ret::Expr(expr), }, ExprKind::Merge(ref handlers, ref variant, _) => { diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs index bb1a5b3..ce0a3d2 100644 --- a/dhall/src/syntax/ast/expr.rs +++ b/dhall/src/syntax/ast/expr.rs @@ -178,7 +178,7 @@ pub enum ExprKind { Field(SubExpr, Label), /// `e.{ x, y, z }` Projection(SubExpr, DupTreeSet