From 5e50ad90b01ef5f589515280668187b722bfcb5f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 4 Feb 2020 19:04:27 +0000 Subject: Implement typechecking of toMap --- dhall/build.rs | 25 ------- dhall/src/semantics/tck/typecheck.rs | 80 +++++++++++++++++++++- dhall/tests/type-errors/unit/EmptyToMap.txt | 6 ++ dhall/tests/type-errors/unit/HeterogenousToMap.txt | 6 ++ dhall/tests/type-errors/unit/MistypedToMap1.txt | 6 ++ dhall/tests/type-errors/unit/MistypedToMap2.txt | 6 ++ dhall/tests/type-errors/unit/MistypedToMap3.txt | 6 ++ dhall/tests/type-errors/unit/MistypedToMap4.txt | 6 ++ dhall/tests/type-errors/unit/NonRecordToMap.txt | 6 ++ .../unit/ToMapEmptyInvalidAnnotation.txt | 7 ++ dhall/tests/type-errors/unit/ToMapWrongKind.txt | 6 ++ 11 files changed, 134 insertions(+), 26 deletions(-) create mode 100644 dhall/tests/type-errors/unit/EmptyToMap.txt create mode 100644 dhall/tests/type-errors/unit/HeterogenousToMap.txt create mode 100644 dhall/tests/type-errors/unit/MistypedToMap1.txt create mode 100644 dhall/tests/type-errors/unit/MistypedToMap2.txt create mode 100644 dhall/tests/type-errors/unit/MistypedToMap3.txt create mode 100644 dhall/tests/type-errors/unit/MistypedToMap4.txt create mode 100644 dhall/tests/type-errors/unit/NonRecordToMap.txt create mode 100644 dhall/tests/type-errors/unit/ToMapEmptyInvalidAnnotation.txt create mode 100644 dhall/tests/type-errors/unit/ToMapWrongKind.txt 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 + --> :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 + --> :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 + --> :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 + --> :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 + --> :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 + --> :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 + --> :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 }` + --> :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` + --> :1:0 + | +1 | toMap { x = Bool } + | ^^^^^^^^^^^^^^^^^^ `toMap` only accepts records of type `Type` + | -- cgit v1.2.3 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/build.rs | 10 ---------- dhall/src/semantics/tck/typecheck.rs | 27 +++++++++++++++++++++++++-- 2 files changed, 25 insertions(+), 12 deletions(-) diff --git a/dhall/build.rs b/dhall/build.rs index 5523ef3..36acc02 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -309,10 +309,6 @@ fn generate_tests() -> std::io::Result<()> { false // Too slow || path == "prelude" - // TODO: projection by expression - || path == "unit/RecordProjectionByType" - || path == "unit/RecordProjectionByTypeEmpty" - || path == "unit/RecordProjectionByTypeJudgmentalEquality" // TODO: record completion || path == "simple/completion" || path == "unit/Completion" @@ -326,9 +322,6 @@ fn generate_tests() -> std::io::Result<()> { variant: "TypeInferenceFailure", path_filter: Box::new(|path: &str| { false - // TODO: projection by expression - || path == "unit/RecordProjectionByTypeFieldTypeMismatch" - || path == "unit/RecordProjectionByTypeNotPresent" // TODO: record completion || path == "unit/CompletionMissingRequiredField" || path == "unit/CompletionWithWrongDefaultType" @@ -346,9 +339,6 @@ fn generate_tests() -> std::io::Result<()> { variant: "TypeError", path_filter: Box::new(|path: &str| { false - // TODO: projection by expression - || path == "unit/RecordProjectionByTypeFieldTypeMismatch" - || path == "unit/RecordProjectionByTypeNotPresent" // 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 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 From de7664d9dda95dd16742bc30e16a967c43d687ee Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 5 Feb 2020 18:10:41 +0000 Subject: Typecheck record completion --- dhall/build.rs | 13 ------ dhall/src/semantics/tck/typecheck.rs | 76 ++++++++++++++++++++++++------------ 2 files changed, 51 insertions(+), 38 deletions(-) diff --git a/dhall/build.rs b/dhall/build.rs index 36acc02..ab709b8 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -309,9 +309,6 @@ fn generate_tests() -> std::io::Result<()> { false // Too slow || path == "prelude" - // TODO: record completion - || path == "simple/completion" - || path == "unit/Completion" }), input_type: FileType::Text, output_type: Some(FileType::Text), @@ -322,11 +319,6 @@ fn generate_tests() -> std::io::Result<()> { variant: "TypeInferenceFailure", path_filter: Box::new(|path: &str| { false - // TODO: record completion - || path == "unit/CompletionMissingRequiredField" - || path == "unit/CompletionWithWrongDefaultType" - || path == "unit/CompletionWithWrongFieldName" - || path == "unit/CompletionWithWrongOverridenType" // TODO: enable free variable checking || path == "unit/MergeHandlerFreeVar" }), @@ -339,11 +331,6 @@ fn generate_tests() -> std::io::Result<()> { variant: "TypeError", path_filter: Box::new(|path: &str| { false - // TODO: record completion - || path == "unit/CompletionMissingRequiredField" - || path == "unit/CompletionWithWrongDefaultType" - || path == "unit/CompletionWithWrongFieldName" - || path == "unit/CompletionWithWrongOverridenType" // TODO: enable free variable checking || path == "unit/MergeHandlerFreeVar" }), diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index e3ae129..6817712 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -51,9 +51,9 @@ fn mkerr(x: S) -> Result { /// layer. fn type_one_layer( env: &TyEnv, - kind: &ExprKind, + ekind: ExprKind, span: Span, -) -> Result { +) -> Result { let span_err = |msg: &str| { mkerr( ErrorBuilder::new(msg.to_string()) @@ -62,7 +62,7 @@ fn type_one_layer( ) }; - Ok(match kind { + let ty = match &ekind { ExprKind::Import(..) => unreachable!( "There should remain no imports in a resolved expression" ), @@ -74,13 +74,8 @@ fn type_one_layer( let body_ty = body.get_type()?; let body_ty = body_ty.to_tyexpr(env.as_varenv().insert()); let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty); - let pi_ty = type_one_layer(env, &pi_ekind, Span::Artificial)?; - let ty = TyExpr::new( - TyExprKind::Expr(pi_ekind), - Some(pi_ty), - Span::Artificial, - ); - ty.eval(env.as_nzenv()) + type_one_layer(env, pi_ekind, Span::Artificial)? + .eval(env.as_nzenv()) } ExprKind::Pi(_, annot, body) => { let ks = match annot.get_type()?.as_const() { @@ -187,7 +182,7 @@ fn type_one_layer( } let ty = type_of_recordtype( - span, + span.clone(), kts.iter() .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))), )?; @@ -206,7 +201,10 @@ fn type_one_layer( }; } - type_of_recordtype(span, kts.iter().map(|(_, t)| Cow::Borrowed(t)))? + type_of_recordtype( + span.clone(), + kts.iter().map(|(_, t)| Cow::Borrowed(t)), + )? } ExprKind::UnionType(kts) => { use std::collections::hash_map::Entry; @@ -389,7 +387,7 @@ fn type_one_layer( // Construct the final record type let ty = type_of_recordtype( - span, + span.clone(), kts.iter() .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))), )?; @@ -401,9 +399,7 @@ fn type_one_layer( x.get_type()?.to_tyexpr(env.as_varenv()), y.get_type()?.to_tyexpr(env.as_varenv()), ); - let ty = type_one_layer(env, &ekind, Span::Artificial)?; - TyExpr::new(TyExprKind::Expr(ekind), Some(ty), Span::Artificial) - .eval(env.as_nzenv()) + type_one_layer(env, ekind, Span::Artificial)?.eval(env.as_nzenv()) } ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => { let x_val = x.eval(env.as_nzenv()); @@ -420,7 +416,7 @@ fn type_one_layer( if let Some(ty) = kts_y.get(k) { type_one_layer( env, - &ExprKind::BinOp( + ExprKind::BinOp( BinOp::RecursiveRecordTypeMerge, tx.to_tyexpr(env.as_varenv()), ty.to_tyexpr(env.as_varenv()), @@ -547,9 +543,14 @@ fn type_one_layer( ); } - closure.remove_binder().or_else(|()| { - span_err("MergeReturnTypeIsDependent") - })? + match closure.remove_binder() { + Ok(v) => v, + Err(()) => { + return span_err( + "MergeReturnTypeIsDependent", + ) + } + } } _ => { return mkerr( @@ -752,8 +753,35 @@ fn type_one_layer( selection_val } - ExprKind::Completion(_, _) => unimplemented!("record completion"), - }) + ExprKind::Completion(ty, compl) => { + let ty_field_default = type_one_layer( + env, + ExprKind::Field(ty.clone(), "default".into()), + span.clone(), + )?; + let ty_field_type = type_one_layer( + env, + ExprKind::Field(ty.clone(), "Type".into()), + span.clone(), + )?; + let merge = type_one_layer( + env, + ExprKind::BinOp( + BinOp::RightBiasedRecordMerge, + ty_field_default, + compl.clone(), + ), + span.clone(), + )?; + return type_one_layer( + env, + ExprKind::Annot(merge, ty_field_type), + span.clone(), + ); + } + }; + + Ok(TyExpr::new(TyExprKind::Expr(ekind), Some(ty), span)) } /// `type_with` typechecks an expressio in the provided environment. @@ -809,9 +837,7 @@ pub(crate) fn type_with( } _ => ekind.traverse_ref(|e| type_with(env, e))?, }; - - let ty = type_one_layer(env, &ekind, expr.span())?; - (TyExprKind::Expr(ekind), Some(ty)) + return type_one_layer(env, ekind, expr.span()); } }; -- cgit v1.2.3 From 853807b68a8ec8928a4d497fc7ce2b3676036eed Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 5 Feb 2020 18:33:18 +0000 Subject: Normalize toMap --- dhall/build.rs | 4 --- dhall/src/semantics/builtins.rs | 15 ++++------- dhall/src/semantics/nze/normalize.rs | 49 ++++++++++++++++++++++++++++++++---- dhall/src/semantics/nze/value.rs | 6 +++++ 4 files changed, 55 insertions(+), 19 deletions(-) diff --git a/dhall/build.rs b/dhall/build.rs index ab709b8..b6c30be 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -260,10 +260,6 @@ fn generate_tests() -> std::io::Result<()> { || path == "unit/RecordProjectionByTypeNormalizeProjection" // TODO: fix Double/show || path == "prelude/JSON/number/1" - // TODO: toMap - || path == "unit/EmptyToMap" - || path == "unit/ToMap" - || path == "unit/ToMapWithType" // TODO: Further record simplifications || path == "simplifications/rightBiasedMergeWithinRecordProjectionWithinFieldSelection0" || path == "simplifications/rightBiasedMergeWithinRecordProjectionWithinFieldSelection1" diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index c20fb77..907d449 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -1,5 +1,5 @@ use crate::semantics::{ - self, typecheck, NzEnv, TyExpr, TyExprKind, Value, ValueKind, VarEnv, + typecheck, NzEnv, TyExpr, TyExprKind, Value, ValueKind, VarEnv, }; use crate::syntax::map::DupTreeMap; use crate::syntax::Const::Type; @@ -301,9 +301,7 @@ fn apply_builtin( _ => Ret::DoneAsIs, }, (NaturalShow, [n]) => match &*n.kind() { - NaturalLit(n) => Ret::ValueKind(TextLit( - semantics::TextLit::from_text(n.to_string()), - )), + NaturalLit(n) => Ret::Value(Value::from_text(n)), _ => Ret::DoneAsIs, }, (NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) { @@ -322,7 +320,7 @@ fn apply_builtin( } else { format!("+{}", n) }; - Ret::ValueKind(TextLit(semantics::TextLit::from_text(s))) + Ret::Value(Value::from_text(s)) } _ => Ret::DoneAsIs, }, @@ -343,9 +341,7 @@ fn apply_builtin( _ => Ret::DoneAsIs, }, (DoubleShow, [n]) => match &*n.kind() { - DoubleLit(n) => Ret::ValueKind(TextLit( - semantics::TextLit::from_text(n.to_string()), - )), + DoubleLit(n) => Ret::Value(Value::from_text(n)), _ => Ret::DoneAsIs, }, (TextShow, [v]) => match &*v.kind() { @@ -355,8 +351,7 @@ fn apply_builtin( let txt: InterpolatedText = std::iter::once(InterpolatedTextContents::Text(s)) .collect(); - let s = txt.to_string(); - Ret::ValueKind(TextLit(semantics::TextLit::from_text(s))) + Ret::Value(Value::from_text(txt)) } else { Ret::DoneAsIs } diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index e9d140b..fbb3647 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -1,3 +1,4 @@ +use itertools::Itertools; use std::collections::HashMap; use crate::semantics::NzEnv; @@ -242,9 +243,9 @@ pub(crate) fn normalize_one_layer( env: &NzEnv, ) -> ValueKind { use ValueKind::{ - BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit, - NEOptionalLit, NaturalLit, RecordLit, RecordType, UnionConstructor, - UnionLit, UnionType, + BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, IntegerLit, + NEListLit, NEOptionalLit, NaturalLit, RecordLit, RecordType, + UnionConstructor, UnionLit, UnionType, }; let ret = match expr { @@ -271,7 +272,7 @@ pub(crate) fn normalize_one_layer( ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)), ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)), ExprKind::EmptyListLit(t) => { - let arg = match &*t.kind() { + let arg = match t.kind() { ValueKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, args, @@ -373,7 +374,45 @@ pub(crate) fn normalize_one_layer( _ => Ret::Expr(expr), } } - ExprKind::ToMap(_, _) => unimplemented!("toMap"), + ExprKind::ToMap(ref v, ref annot) => match v.kind() { + RecordLit(kvs) if kvs.is_empty() => { + match annot.as_ref().map(|v| v.kind()) { + Some(ValueKind::AppliedBuiltin(BuiltinClosure { + b: Builtin::List, + args, + .. + })) if args.len() == 1 => { + Ret::ValueKind(EmptyListLit(args[0].clone())) + } + _ => Ret::Expr(expr), + } + } + RecordLit(kvs) => Ret::ValueKind(NEListLit( + kvs.iter() + .sorted_by_key(|(k, _)| k.clone()) + .map(|(k, v)| { + let mut rec = HashMap::new(); + let mut rec_ty = HashMap::new(); + rec.insert("mapKey".into(), Value::from_text(k)); + rec.insert("mapValue".into(), v.clone()); + rec_ty.insert( + "mapKey".into(), + Value::from_builtin(Builtin::Text), + ); + rec_ty.insert("mapValue".into(), v.get_type_not_sort()); + + Value::from_kind_and_type( + ValueKind::RecordLit(rec), + Value::from_kind_and_type( + ValueKind::RecordType(rec_ty), + Value::from_const(Const::Type), + ), + ) + }) + .collect(), + )), + _ => Ret::Expr(expr), + }, }; match ret { diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 1143781..607aa0d 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -167,6 +167,12 @@ impl Value { typecheck(&type_of_builtin(b)).unwrap().eval_closed_expr(), ) } + pub(crate) fn from_text(txt: impl ToString) -> Self { + Value::from_kind_and_type( + ValueKind::TextLit(TextLit::from_text(txt.to_string())), + Value::from_builtin(Builtin::Text), + ) + } pub(crate) fn as_const(&self) -> Option { match &*self.kind() { -- cgit v1.2.3 From c27d8ff15988b914d21135dadffe9871441c127f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 6 Feb 2020 16:34:08 +0000 Subject: Implement some record simplifications --- dhall/build.rs | 17 +++---- dhall/src/semantics/nze/normalize.rs | 94 +++++++++++++++++++++++++++++++++++- 2 files changed, 98 insertions(+), 13 deletions(-) diff --git a/dhall/build.rs b/dhall/build.rs index b6c30be..83c154e 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -258,27 +258,22 @@ fn generate_tests() -> std::io::Result<()> { || path == "unit/RecordProjectionByTypeEmpty" || path == "unit/RecordProjectionByTypeNonEmpty" || path == "unit/RecordProjectionByTypeNormalizeProjection" + || path == "unit/RecordProjectionByTypeWithinFieldSelection" + || path == "unit/RecursiveRecordMergeWithinFieldSelection1" + || path == "unit/NestedRecordProjectionByType" // TODO: fix Double/show || path == "prelude/JSON/number/1" - // TODO: Further record simplifications + // TODO: doesn't typecheck + || path == "unit/RightBiasedRecordMergeWithinRecordProjection" + // // TODO: Further record simplifications || path == "simplifications/rightBiasedMergeWithinRecordProjectionWithinFieldSelection0" || path == "simplifications/rightBiasedMergeWithinRecordProjectionWithinFieldSelection1" || path == "simplifications/rightBiasedMergeWithinRecursiveRecordMergeWithinFieldselection" || path == "simplifications/issue661" - || path == "unit/RecordProjectionByTypeWithinFieldSelection" || path == "unit/RecordProjectionWithinFieldSelection" || path == "unit/RecursiveRecordMergeWithinFieldSelection0" - || path == "unit/RecursiveRecordMergeWithinFieldSelection1" || path == "unit/RecursiveRecordMergeWithinFieldSelection2" || path == "unit/RecursiveRecordMergeWithinFieldSelection3" - || path == "unit/RightBiasedMergeWithinFieldSelection0" - || path == "unit/RightBiasedMergeWithinFieldSelection1" - || path == "unit/RightBiasedMergeWithinFieldSelection2" - || path == "unit/RightBiasedMergeWithinFieldSelection3" - || path == "unit/RightBiasedRecordMergeWithinRecordProjection" - || path == "unit/RightBiasedMergeEquivalentArguments" - || path == "unit/NestedRecordProjection" - || path == "unit/NestedRecordProjectionByType" // TODO: record completion || path == "simple/completion" || path == "unit/Completion" diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index fbb3647..a00b7ff 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -185,6 +185,7 @@ fn apply_binop<'a>( } Ret::ValueKind(RecordLit(kvs)) } + (RightBiasedRecordMerge, _, _) if x == y => Ret::ValueRef(y), (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { Ret::ValueRef(x) @@ -244,8 +245,8 @@ pub(crate) fn normalize_one_layer( ) -> ValueKind { use ValueKind::{ BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, IntegerLit, - NEListLit, NEOptionalLit, NaturalLit, RecordLit, RecordType, - UnionConstructor, UnionLit, UnionType, + NEListLit, NEOptionalLit, NaturalLit, PartialExpr, RecordLit, + RecordType, UnionConstructor, UnionLit, UnionType, }; let ret = match expr { @@ -331,6 +332,13 @@ pub(crate) fn normalize_one_layer( .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone()))) .collect(), )), + PartialExpr(ExprKind::Projection(v2, _)) => { + return normalize_one_layer( + ExprKind::Projection(v2.clone(), ls.clone()), + ty, + env, + ) + } _ => Ret::Expr(expr), }, ExprKind::Field(ref v, ref l) => match v.kind() { @@ -343,6 +351,88 @@ pub(crate) fn normalize_one_layer( kts.clone(), v.get_type().unwrap(), )), + PartialExpr(ExprKind::BinOp( + BinOp::RightBiasedRecordMerge, + x, + y, + )) => match (x.kind(), y.kind()) { + (_, RecordLit(kvs)) => match kvs.get(l) { + Some(r) => Ret::Value(r.clone()), + None => { + return normalize_one_layer( + ExprKind::Field(x.clone(), l.clone()), + ty, + env, + ) + } + }, + (RecordLit(kvs), _) => match kvs.get(l) { + Some(r) => Ret::Expr(ExprKind::Field( + Value::from_kind_and_type( + PartialExpr(ExprKind::BinOp( + BinOp::RightBiasedRecordMerge, + Value::from_kind_and_type( + RecordLit({ + let mut kvs = HashMap::new(); + kvs.insert(l.clone(), r.clone()); + kvs + }), + Value::from_kind_and_type( + RecordType({ + let mut kvs = HashMap::new(); + kvs.insert( + l.clone(), + r.get_type_not_sort(), + ); + kvs + }), + r.get_type_not_sort() + .get_type_not_sort(), + ), + ), + y.clone(), + )), + v.get_type_not_sort(), + ), + l.clone(), + )), + None => { + return normalize_one_layer( + ExprKind::Field(y.clone(), l.clone()), + ty, + env, + ) + } + }, + _ => Ret::Expr(expr), + }, + PartialExpr(ExprKind::BinOp( + BinOp::RecursiveRecordTypeMerge, + x, + y, + )) => match (x.kind(), y.kind()) { + (RecordLit(kvs), _) => match kvs.get(l) { + Some(_) => Ret::Expr(expr), + None => { + return normalize_one_layer( + ExprKind::Field(y.clone(), l.clone()), + ty, + env, + ) + } + }, + (_, RecordLit(kvs)) => match kvs.get(l) { + Some(_) => Ret::Expr(expr), + None => { + return normalize_one_layer( + ExprKind::Field(x.clone(), l.clone()), + ty, + env, + ) + } + }, + _ => Ret::Expr(expr), + }, _ => Ret::Expr(expr), }, ExprKind::ProjectionByExpr(_, _) => { -- cgit v1.2.3