summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2020-02-04 19:04:27 +0000
committerNadrieril2020-02-04 19:05:08 +0000
commit5e50ad90b01ef5f589515280668187b722bfcb5f (patch)
tree3864cb9b3a107aeef0813e18877e7eb8c1d32dbf
parenteb9129312edf574948df777acb340189dc147724 (diff)
Implement typechecking of toMap
Diffstat (limited to '')
-rw-r--r--dhall/build.rs25
-rw-r--r--dhall/src/semantics/tck/typecheck.rs80
-rw-r--r--dhall/tests/type-errors/unit/EmptyToMap.txt6
-rw-r--r--dhall/tests/type-errors/unit/HeterogenousToMap.txt6
-rw-r--r--dhall/tests/type-errors/unit/MistypedToMap1.txt6
-rw-r--r--dhall/tests/type-errors/unit/MistypedToMap2.txt6
-rw-r--r--dhall/tests/type-errors/unit/MistypedToMap3.txt6
-rw-r--r--dhall/tests/type-errors/unit/MistypedToMap4.txt6
-rw-r--r--dhall/tests/type-errors/unit/NonRecordToMap.txt6
-rw-r--r--dhall/tests/type-errors/unit/ToMapEmptyInvalidAnnotation.txt7
-rw-r--r--dhall/tests/type-errors/unit/ToMapWrongKind.txt6
11 files changed, 134 insertions, 26 deletions
diff --git a/dhall/build.rs b/dhall/build.rs
index 9cc07ea..5523ef3 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -313,11 +313,6 @@ fn generate_tests() -> std::io::Result<()> {
|| path == "unit/RecordProjectionByType"
|| path == "unit/RecordProjectionByTypeEmpty"
|| path == "unit/RecordProjectionByTypeJudgmentalEquality"
- // TODO: toMap
- || path == "unit/ToMap"
- || path == "unit/ToMapAnnotated"
- || path == "unit/ToMapInferTypeFromRecord"
- || path == "simple/toMapEmptyNormalizeAnnotation"
// TODO: record completion
|| path == "simple/completion"
|| path == "unit/Completion"
@@ -334,16 +329,6 @@ fn generate_tests() -> std::io::Result<()> {
// TODO: projection by expression
|| path == "unit/RecordProjectionByTypeFieldTypeMismatch"
|| path == "unit/RecordProjectionByTypeNotPresent"
- // TODO: toMap
- || path == "unit/EmptyToMap"
- || path == "unit/HeterogenousToMap"
- || path == "unit/MistypedToMap1"
- || path == "unit/MistypedToMap2"
- || path == "unit/MistypedToMap3"
- || path == "unit/MistypedToMap4"
- || path == "unit/NonRecordToMap"
- || path == "unit/ToMapEmptyInvalidAnnotation"
- || path == "unit/ToMapWrongKind"
// TODO: record completion
|| path == "unit/CompletionMissingRequiredField"
|| path == "unit/CompletionWithWrongDefaultType"
@@ -364,16 +349,6 @@ fn generate_tests() -> std::io::Result<()> {
// TODO: projection by expression
|| path == "unit/RecordProjectionByTypeFieldTypeMismatch"
|| path == "unit/RecordProjectionByTypeNotPresent"
- // TODO: toMap
- || path == "unit/EmptyToMap"
- || path == "unit/HeterogenousToMap"
- || path == "unit/MistypedToMap1"
- || path == "unit/MistypedToMap2"
- || path == "unit/MistypedToMap3"
- || path == "unit/MistypedToMap4"
- || path == "unit/NonRecordToMap"
- || path == "unit/ToMapEmptyInvalidAnnotation"
- || path == "unit/ToMapWrongKind"
// 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 c3c589b..516ef42 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -619,7 +619,85 @@ fn type_one_layer(
(None, None) => return span_err("MergeEmptyNeedsAnnotation"),
}
}
- ExprKind::ToMap(_, _) => unimplemented!("toMap"),
+ ExprKind::ToMap(record, annot) => {
+ let record_t = record.get_type()?;
+ let kts = match record_t.kind() {
+ ValueKind::RecordType(kts) => kts,
+ _ => {
+ return span_err("The argument to `toMap` must be a record")
+ }
+ };
+
+ if kts.is_empty() {
+ let annot = if let Some(annot) = annot {
+ annot
+ } else {
+ return span_err(
+ "`toMap` applied to an empty record requires a type \
+ annotation",
+ );
+ };
+ let annot_val = annot.eval(env.as_nzenv());
+
+ let err_msg = "The type of `toMap x` must be of the form \
+ `List { mapKey : Text, mapValue : T }`";
+ let arg = match annot_val.kind() {
+ ValueKind::AppliedBuiltin(BuiltinClosure {
+ b: Builtin::List,
+ args,
+ ..
+ }) if args.len() == 1 => &args[0],
+ _ => return span_err(err_msg),
+ };
+ let kts = match arg.kind() {
+ ValueKind::RecordType(kts) => kts,
+ _ => return span_err(err_msg),
+ };
+ if kts.len() != 2 {
+ return span_err(err_msg);
+ }
+ match kts.get(&"mapKey".into()) {
+ Some(t) if *t == Value::from_builtin(Builtin::Text) => {}
+ _ => return span_err(err_msg),
+ }
+ match kts.get(&"mapValue".into()) {
+ Some(_) => {}
+ None => return span_err(err_msg),
+ }
+ annot_val
+ } else {
+ let entry_type = kts.iter().next().unwrap().1.clone();
+ if entry_type.get_type()?.as_const() != Some(Const::Type) {
+ return span_err(
+ "`toMap` only accepts records of type `Type`",
+ );
+ }
+ for (_, t) in kts.iter() {
+ if *t != entry_type {
+ return span_err(
+ "Every field of the record must have the same type",
+ );
+ }
+ }
+
+ let mut kts = HashMap::new();
+ kts.insert("mapKey".into(), Value::from_builtin(Builtin::Text));
+ kts.insert("mapValue".into(), entry_type);
+ let output_type = Value::from_builtin(Builtin::List).app(
+ Value::from_kind_and_type(
+ ValueKind::RecordType(kts),
+ Value::from_const(Const::Type),
+ ),
+ );
+ if let Some(annot) = annot {
+ let annot_val = annot.eval(env.as_nzenv());
+ if output_type != annot_val {
+ return span_err("Annotation mismatch");
+ }
+ }
+ output_type
+ }
+ }
ExprKind::Projection(record, labels) => {
let record_type = record.get_type()?;
let kts = match record_type.kind() {
diff --git a/dhall/tests/type-errors/unit/EmptyToMap.txt b/dhall/tests/type-errors/unit/EmptyToMap.txt
new file mode 100644
index 0000000..000fac7
--- /dev/null
+++ b/dhall/tests/type-errors/unit/EmptyToMap.txt
@@ -0,0 +1,6 @@
+Type error: error: `toMap` applied to an empty record requires a type annotation
+ --> <current file>:1:0
+ |
+1 | toMap {=}
+ | ^^^^^^^^^ `toMap` applied to an empty record requires a type annotation
+ |
diff --git a/dhall/tests/type-errors/unit/HeterogenousToMap.txt b/dhall/tests/type-errors/unit/HeterogenousToMap.txt
new file mode 100644
index 0000000..2f8abf2
--- /dev/null
+++ b/dhall/tests/type-errors/unit/HeterogenousToMap.txt
@@ -0,0 +1,6 @@
+Type error: error: Every field of the record must have the same type
+ --> <current file>:1:0
+ |
+1 | toMap { foo= 1, bar= "Bar" }
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Every field of the record must have the same type
+ |
diff --git a/dhall/tests/type-errors/unit/MistypedToMap1.txt b/dhall/tests/type-errors/unit/MistypedToMap1.txt
new file mode 100644
index 0000000..14d9791
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MistypedToMap1.txt
@@ -0,0 +1,6 @@
+Type error: error: Annotation mismatch
+ --> <current file>:1:0
+ |
+1 | toMap { foo= 1, bar= 4 } : Natural
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Annotation mismatch
+ |
diff --git a/dhall/tests/type-errors/unit/MistypedToMap2.txt b/dhall/tests/type-errors/unit/MistypedToMap2.txt
new file mode 100644
index 0000000..88e303e
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MistypedToMap2.txt
@@ -0,0 +1,6 @@
+Type error: error: Annotation mismatch
+ --> <current file>:1:0
+ |
+1 | toMap { foo= 1, bar= 4 } : List Natural
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Annotation mismatch
+ |
diff --git a/dhall/tests/type-errors/unit/MistypedToMap3.txt b/dhall/tests/type-errors/unit/MistypedToMap3.txt
new file mode 100644
index 0000000..6b3772d
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MistypedToMap3.txt
@@ -0,0 +1,6 @@
+Type error: error: Annotation mismatch
+ --> <current file>:1:0
+ |
+1 | toMap { foo= 1, bar= 4 } : List { mapKey : Natural, mapValue : Natural }
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Annotation mismatch
+ |
diff --git a/dhall/tests/type-errors/unit/MistypedToMap4.txt b/dhall/tests/type-errors/unit/MistypedToMap4.txt
new file mode 100644
index 0000000..e0cf651
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MistypedToMap4.txt
@@ -0,0 +1,6 @@
+Type error: error: Annotation mismatch
+ --> <current file>:1:0
+ |
+1 | toMap { foo= 1, bar= 4 } : List { mapKey : Text, mapValue : Text }
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Annotation mismatch
+ |
diff --git a/dhall/tests/type-errors/unit/NonRecordToMap.txt b/dhall/tests/type-errors/unit/NonRecordToMap.txt
new file mode 100644
index 0000000..8e83002
--- /dev/null
+++ b/dhall/tests/type-errors/unit/NonRecordToMap.txt
@@ -0,0 +1,6 @@
+Type error: error: The argument to `toMap` must be a record
+ --> <current file>:1:0
+ |
+1 | toMap "text"
+ | ^^^^^^^^^^^^ The argument to `toMap` must be a record
+ |
diff --git a/dhall/tests/type-errors/unit/ToMapEmptyInvalidAnnotation.txt b/dhall/tests/type-errors/unit/ToMapEmptyInvalidAnnotation.txt
new file mode 100644
index 0000000..c28073e
--- /dev/null
+++ b/dhall/tests/type-errors/unit/ToMapEmptyInvalidAnnotation.txt
@@ -0,0 +1,7 @@
+Type error: error: The type of `toMap x` must be of the form `List { mapKey : Text, mapValue : T }`
+ --> <current file>:2:0
+ |
+1 | -- The mapKey must be Text
+2 | toMap {=} : List { mapKey : Bool, mapValue : Text }
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ The type of `toMap x` must be of the form `List { mapKey : Text, mapValue : T }`
+ |
diff --git a/dhall/tests/type-errors/unit/ToMapWrongKind.txt b/dhall/tests/type-errors/unit/ToMapWrongKind.txt
new file mode 100644
index 0000000..8158c08
--- /dev/null
+++ b/dhall/tests/type-errors/unit/ToMapWrongKind.txt
@@ -0,0 +1,6 @@
+Type error: error: `toMap` only accepts records of type `Type`
+ --> <current file>:1:0
+ |
+1 | toMap { x = Bool }
+ | ^^^^^^^^^^^^^^^^^^ `toMap` only accepts records of type `Type`
+ |