summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2020-02-05 17:52:27 +0000
committerNadrieril2020-02-05 17:52:27 +0000
commit7ff5974052e3e18109acbe6e4f0588698d6129ba (patch)
treefef73324e9dfa23c03bdd31a4e9e59500b950be5
parent5e50ad90b01ef5f589515280668187b722bfcb5f (diff)
Typecheck projection by type
-rw-r--r--dhall/build.rs10
-rw-r--r--dhall/src/semantics/tck/typecheck.rs27
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"),
})