summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2020-02-05 18:33:18 +0000
committerNadrieril2020-02-05 18:33:18 +0000
commit853807b68a8ec8928a4d497fc7ce2b3676036eed (patch)
treef4f9701a72d0989a0d1ae7c07acb7a95d789d905
parentde7664d9dda95dd16742bc30e16a967c43d687ee (diff)
Normalize toMap
Diffstat (limited to '')
-rw-r--r--dhall/build.rs4
-rw-r--r--dhall/src/semantics/builtins.rs15
-rw-r--r--dhall/src/semantics/nze/normalize.rs49
-rw-r--r--dhall/src/semantics/nze/value.rs6
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() {