summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2019-05-08 23:23:09 +0200
committerNadrieril2019-05-08 23:23:09 +0200
commit0d9b3405021b956fad3a87fc7a8eced16968509d (patch)
tree083739665d3a62574e1dd178f3fc73088b537ffa
parent6febba3f2026a3b8c2bb98d85facad0ad0605d02 (diff)
Typecheck record projection
-rw-r--r--dhall/src/error/mod.rs2
-rw-r--r--dhall/src/phase/typecheck.rs37
2 files changed, 32 insertions, 7 deletions
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 3efa77e..89568a3 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -69,6 +69,8 @@ pub(crate) enum TypeMessage {
MergeVariantMissingHandler(Label),
MergeAnnotMismatch,
MergeHandlerTypeMismatch,
+ ProjectionMustBeRecord,
+ ProjectionMissingEntry,
Sort,
Unimplemented,
}
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 100a04c..fa37379 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -605,6 +605,7 @@ fn type_last_layer(
Some(Value::UnionType(kts)) => match kts.get(&x) {
// Constructor has type T -> < x: T, ... >
Some(Some(t)) => {
+ // TODO: avoid capture
Ok(RetTypeIntermediate(
TypeIntermediate::Pi(
"_".into(),
@@ -774,7 +775,29 @@ fn type_last_layer(
(None, None) => return Err(mkerr(MergeEmptyNeedsAnnotation)),
}
}
- Projection(_, _) => unimplemented!(),
+ Projection(record, labels) => {
+ let trecord = record.get_type()?;
+ let kts = match trecord.to_value() {
+ Value::RecordType(kts) => kts,
+ _ => return Err(mkerr(ProjectionMustBeRecord)),
+ };
+
+ let mut new_kts = BTreeMap::new();
+ for l in labels {
+ match kts.get(l) {
+ None => return Err(mkerr(ProjectionMissingEntry)),
+ Some(t) => new_kts.insert(l.clone(), t.clone()),
+ };
+ }
+
+ Ok(RetType(
+ Typed::from_thunk_and_type(
+ Value::RecordType(new_kts).into_thunk(),
+ trecord.get_type()?.into_owned(),
+ )
+ .to_type(),
+ ))
+ }
}
}
@@ -1137,12 +1160,12 @@ mod spec_tests {
ti_success!(ti_success_unit_RecordOneKind, "unit/RecordOneKind");
ti_success!(ti_success_unit_RecordOneType, "unit/RecordOneType");
ti_success!(ti_success_unit_RecordOneValue, "unit/RecordOneValue");
- // ti_success!(ti_success_unit_RecordProjectionEmpty, "unit/RecordProjectionEmpty");
- // ti_success!(ti_success_unit_RecordProjectionKind, "unit/RecordProjectionKind");
- // ti_success!(ti_success_unit_RecordProjectionType, "unit/RecordProjectionType");
- // ti_success!(ti_success_unit_RecordProjectionValue, "unit/RecordProjectionValue");
- // ti_success!(ti_success_unit_RecordSelectionKind, "unit/RecordSelectionKind");
- // ti_success!(ti_success_unit_RecordSelectionType, "unit/RecordSelectionType");
+ ti_success!(ti_success_unit_RecordProjectionEmpty, "unit/RecordProjectionEmpty");
+ ti_success!(ti_success_unit_RecordProjectionKind, "unit/RecordProjectionKind");
+ ti_success!(ti_success_unit_RecordProjectionType, "unit/RecordProjectionType");
+ ti_success!(ti_success_unit_RecordProjectionValue, "unit/RecordProjectionValue");
+ ti_success!(ti_success_unit_RecordSelectionKind, "unit/RecordSelectionKind");
+ ti_success!(ti_success_unit_RecordSelectionType, "unit/RecordSelectionType");
ti_success!(ti_success_unit_RecordSelectionValue, "unit/RecordSelectionValue");
ti_success!(ti_success_unit_RecordType, "unit/RecordType");
ti_success!(ti_success_unit_RecordTypeEmpty, "unit/RecordTypeEmpty");