diff options
Diffstat (limited to 'dhall')
| -rw-r--r-- | dhall/build.rs | 25 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 80 | ||||
| -rw-r--r-- | dhall/tests/type-errors/unit/EmptyToMap.txt | 6 | ||||
| -rw-r--r-- | dhall/tests/type-errors/unit/HeterogenousToMap.txt | 6 | ||||
| -rw-r--r-- | dhall/tests/type-errors/unit/MistypedToMap1.txt | 6 | ||||
| -rw-r--r-- | dhall/tests/type-errors/unit/MistypedToMap2.txt | 6 | ||||
| -rw-r--r-- | dhall/tests/type-errors/unit/MistypedToMap3.txt | 6 | ||||
| -rw-r--r-- | dhall/tests/type-errors/unit/MistypedToMap4.txt | 6 | ||||
| -rw-r--r-- | dhall/tests/type-errors/unit/NonRecordToMap.txt | 6 | ||||
| -rw-r--r-- | dhall/tests/type-errors/unit/ToMapEmptyInvalidAnnotation.txt | 7 | ||||
| -rw-r--r-- | dhall/tests/type-errors/unit/ToMapWrongKind.txt | 6 |
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` + | |