diff options
| -rw-r--r-- | dhall/build.rs | 4 | ||||
| -rw-r--r-- | dhall/src/semantics/builtins.rs | 15 | ||||
| -rw-r--r-- | dhall/src/semantics/nze/normalize.rs | 49 | ||||
| -rw-r--r-- | 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<Normalized> = 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<Const> { match &*self.kind() { |