diff options
author | Nadrieril | 2019-05-08 23:23:09 +0200 |
---|---|---|
committer | Nadrieril | 2019-05-08 23:23:09 +0200 |
commit | 0d9b3405021b956fad3a87fc7a8eced16968509d (patch) | |
tree | 083739665d3a62574e1dd178f3fc73088b537ffa /dhall | |
parent | 6febba3f2026a3b8c2bb98d85facad0ad0605d02 (diff) |
Typecheck record projection
Diffstat (limited to '')
-rw-r--r-- | dhall/src/error/mod.rs | 2 | ||||
-rw-r--r-- | dhall/src/phase/typecheck.rs | 37 |
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"); |