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/src/semantics/tck/typecheck.rs | 80 +++++++++++++++++++++++++++++++++++- 1 file changed, 79 insertions(+), 1 deletion(-) (limited to 'dhall/src/semantics') 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() { -- 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/src/semantics/tck/typecheck.rs | 27 +++++++++++++++++++++++++-- 1 file changed, 25 insertions(+), 2 deletions(-) (limited to 'dhall/src/semantics') 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/src/semantics/tck/typecheck.rs | 76 ++++++++++++++++++++++++------------ 1 file changed, 51 insertions(+), 25 deletions(-) (limited to 'dhall/src/semantics') 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/src/semantics/builtins.rs | 15 ++++------- dhall/src/semantics/nze/normalize.rs | 49 ++++++++++++++++++++++++++++++++---- dhall/src/semantics/nze/value.rs | 6 +++++ 3 files changed, 55 insertions(+), 15 deletions(-) (limited to 'dhall/src/semantics') 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/src/semantics/nze/normalize.rs | 94 +++++++++++++++++++++++++++++++++++- 1 file changed, 92 insertions(+), 2 deletions(-) (limited to 'dhall/src/semantics') 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