From 7ff5974052e3e18109acbe6e4f0588698d6129ba Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 5 Feb 2020 17:52:27 +0000 Subject: Typecheck projection by type --- dhall/src/semantics/tck/typecheck.rs | 27 +++++++++++++++++++++++++-- 1 file changed, 25 insertions(+), 2 deletions(-) (limited to 'dhall/src/semantics/tck') 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"), }) -- cgit v1.2.3