summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/build.rs11
-rw-r--r--dhall/src/semantics/nze/normalize.rs156
-rw-r--r--dhall/src/syntax/ast/expr.rs2
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<Nir>, 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<Nir>, 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<Nir>, 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<Nir>, 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<Nir>, 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<SubExpr> {
Field(SubExpr, Label),
/// `e.{ x, y, z }`
Projection(SubExpr, DupTreeSet<Label>),
- /// `e.(s)`
+ /// `e.(t)`
ProjectionByExpr(SubExpr, SubExpr),
/// `x::y`
Completion(SubExpr, SubExpr),
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 02:10:29 +0000