diff options
| -rw-r--r-- | dhall/build.rs | 10 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 27 |
2 files changed, 25 insertions, 12 deletions
diff --git a/dhall/build.rs b/dhall/build.rs index 5523ef3..36acc02 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -309,10 +309,6 @@ fn generate_tests() -> std::io::Result<()> { false // Too slow || path == "prelude" - // TODO: projection by expression - || path == "unit/RecordProjectionByType" - || path == "unit/RecordProjectionByTypeEmpty" - || path == "unit/RecordProjectionByTypeJudgmentalEquality" // TODO: record completion || path == "simple/completion" || path == "unit/Completion" @@ -326,9 +322,6 @@ fn generate_tests() -> std::io::Result<()> { variant: "TypeInferenceFailure", path_filter: Box::new(|path: &str| { false - // TODO: projection by expression - || path == "unit/RecordProjectionByTypeFieldTypeMismatch" - || path == "unit/RecordProjectionByTypeNotPresent" // TODO: record completion || path == "unit/CompletionMissingRequiredField" || path == "unit/CompletionWithWrongDefaultType" @@ -346,9 +339,6 @@ fn generate_tests() -> std::io::Result<()> { variant: "TypeError", path_filter: Box::new(|path: &str| { false - // TODO: projection by expression - || path == "unit/RecordProjectionByTypeFieldTypeMismatch" - || path == "unit/RecordProjectionByTypeNotPresent" // TODO: record completion || path == "unit/CompletionMissingRequiredField" || path == "unit/CompletionWithWrongDefaultType" diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 516ef42..e3ae129 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -726,8 +726,31 @@ fn type_one_layer( record_type.get_type()?, ) } - ExprKind::ProjectionByExpr(_, _) => { - unimplemented!("selection by expression") + ExprKind::ProjectionByExpr(record, selection) => { + let record_type = record.get_type()?; + let rec_kts = match record_type.kind() { + ValueKind::RecordType(kts) => kts, + _ => return span_err("ProjectionMustBeRecord"), + }; + + let selection_val = selection.eval(env.as_nzenv()); + let sel_kts = match selection_val.kind() { + ValueKind::RecordType(kts) => kts, + _ => return span_err("ProjectionByExprTakesRecordType"), + }; + + for (l, sel_ty) in sel_kts { + match rec_kts.get(l) { + Some(rec_ty) => { + if rec_ty != sel_ty { + return span_err("ProjectionWrongType"); + } + } + None => return span_err("ProjectionMissingEntry"), + } + } + + selection_val } ExprKind::Completion(_, _) => unimplemented!("record completion"), }) |