summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/build.rs9
-rw-r--r--dhall/src/phase/binary.rs11
-rw-r--r--dhall/src/phase/normalize.rs1
-rw-r--r--dhall/src/phase/typecheck.rs1
-rw-r--r--dhall_syntax/src/core/expr.rs2
-rw-r--r--dhall_syntax/src/core/visitor.rs3
-rw-r--r--dhall_syntax/src/parser.rs8
-rw-r--r--dhall_syntax/src/printer.rs11
-rw-r--r--tests_buffer2
9 files changed, 38 insertions, 10 deletions
diff --git a/dhall/build.rs b/dhall/build.rs
index 4c654c9..e31e39d 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -133,8 +133,6 @@ fn main() -> std::io::Result<()> {
|| path == "unit/import/urls/emptyPath0"
|| path == "unit/import/urls/emptyPath1"
|| path == "unit/import/urls/emptyPathSegment"
- // TODO: toMap
- || path == "toMap"
},
input_type: FileType::Text,
output_type: Some(FileType::Binary),
@@ -172,8 +170,6 @@ fn main() -> std::io::Result<()> {
|| path == "unit/import/urls/emptyPath0"
|| path == "unit/import/urls/emptyPath1"
|| path == "unit/import/urls/emptyPathSegment"
- // TODO: toMap
- || path == "toMap"
},
input_type: FileType::Text,
output_type: Some(FileType::Binary),
@@ -203,8 +199,6 @@ fn main() -> std::io::Result<()> {
|| path == "unit/import/urls/emptyPath0"
|| path == "unit/import/urls/emptyPath1"
|| path == "unit/import/urls/emptyPathSegment"
- // TODO: toMap
- || path == "toMap"
},
input_type: FileType::Text,
output_type: Some(FileType::Binary),
@@ -222,9 +216,6 @@ fn main() -> std::io::Result<()> {
// TODO: projection by expression
|| path == "unit/RecordProjectFields"
|| path == "unit/recordProjectionByExpression"
- // TODO: toMap
- || path == "unit/ToMap"
- || path == "unit/ToMapAnnotated"
},
input_type: FileType::Binary,
output_type: Some(FileType::Text),
diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs
index 7dc9be2..40219d9 100644
--- a/dhall/src/phase/binary.rs
+++ b/dhall/src/phase/binary.rs
@@ -366,6 +366,15 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
let y = cbor_value_to_dhall(&y)?;
Annot(x, y)
}
+ [U64(27), x] => {
+ let x = cbor_value_to_dhall(&x)?;
+ ToMap(x, None)
+ }
+ [U64(27), x, y] => {
+ let x = cbor_value_to_dhall(&x)?;
+ let y = cbor_value_to_dhall(&y)?;
+ ToMap(x, Some(y))
+ }
[U64(28), x] => {
let x = cbor_value_to_dhall(&x)?;
EmptyListLit(x)
@@ -550,6 +559,8 @@ where
Merge(x, y, Some(z)) => {
ser_seq!(ser; tag(6), expr(x), expr(y), expr(z))
}
+ ToMap(x, None) => ser_seq!(ser; tag(27), expr(x)),
+ ToMap(x, Some(y)) => ser_seq!(ser; tag(27), expr(x), expr(y)),
Projection(x, ls) => ser.collect_seq(
once(tag(10))
.chain(once(expr(x)))
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 82a378c..3f6e99c 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -765,6 +765,7 @@ pub(crate) fn normalize_one_layer(
}
}
}
+ ExprF::ToMap(_, _) => unimplemented!("toMap"),
};
match ret {
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 52a4e47..9013c1f 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -757,6 +757,7 @@ fn type_last_layer(
(None, None) => return mkerr(MergeEmptyNeedsAnnotation),
}
}
+ ToMap(_, _) => unimplemented!("toMap"),
Projection(record, labels) => {
let record_type = record.get_type()?;
let record_borrow = record_type.as_whnf();
diff --git a/dhall_syntax/src/core/expr.rs b/dhall_syntax/src/core/expr.rs
index 2d73a64..51b6c47 100644
--- a/dhall_syntax/src/core/expr.rs
+++ b/dhall_syntax/src/core/expr.rs
@@ -243,6 +243,8 @@ pub enum ExprF<SubExpr, Embed> {
UnionType(DupTreeMap<Label, Option<SubExpr>>),
/// `merge x y : t`
Merge(SubExpr, SubExpr, Option<SubExpr>),
+ /// `toMap x : t`
+ ToMap(SubExpr, Option<SubExpr>),
/// `e.x`
Field(SubExpr, Label),
/// `e.{ x, y, z }`
diff --git a/dhall_syntax/src/core/visitor.rs b/dhall_syntax/src/core/visitor.rs
index 49fff60..435771e 100644
--- a/dhall_syntax/src/core/visitor.rs
+++ b/dhall_syntax/src/core/visitor.rs
@@ -150,6 +150,9 @@ where
v.visit_subexpr(y)?,
opt(t, |e| v.visit_subexpr(e))?,
),
+ ToMap(x, t) => {
+ ToMap(v.visit_subexpr(x)?, opt(t, |e| v.visit_subexpr(e))?)
+ }
Field(e, l) => Field(v.visit_subexpr(e)?, l.clone()),
Projection(e, ls) => Projection(v.visit_subexpr(e)?, ls.clone()),
Assert(e) => Assert(v.visit_subexpr(e)?),
diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index defa79b..24ecc1e 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -827,6 +827,7 @@ make_parser! {
rule!(assert<()>);
rule!(if_<()>);
rule!(in_<()>);
+ rule!(toMap<()>);
rule!(empty_list_literal<ParsedExpr>; span; children!(
[application_expression(e)] => {
@@ -863,6 +864,9 @@ make_parser! {
[assert(()), expression(x)] => {
spanned(span, Assert(x))
},
+ [toMap(()), import_expression(x), application_expression(y)] => {
+ spanned(span, ToMap(x, Some(y)))
+ },
[operator_expression(e)] => e,
[operator_expression(e), expression(annot)] => {
spanned(span, Annot(e, annot))
@@ -934,7 +938,6 @@ make_parser! {
));
rule!(Some_<()>);
- rule!(toMap<()>);
rule!(application_expression<ParsedExpr>; children!(
[first_application_expression(e)] => e,
@@ -951,6 +954,9 @@ make_parser! {
[merge(()), import_expression(x), import_expression(y)] => {
spanned(span, Merge(x, y, None))
},
+ [toMap(()), import_expression(x)] => {
+ spanned(span, ToMap(x, None))
+ },
[import_expression(e)] => e,
));
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index 276590e..8571d11 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -41,6 +41,12 @@ impl<SE: Display + Clone, E: Display> Display for ExprF<SE, E> {
write!(f, " : {}", c)?;
}
}
+ ToMap(a, b) => {
+ write!(f, "toMap {}", a)?;
+ if let Some(b) = b {
+ write!(f, " : {}", b)?;
+ }
+ }
Annot(a, b) => {
write!(f, "{} : {}", a, b)?;
}
@@ -144,6 +150,7 @@ impl<A: Display + Clone> RawExpr<A> {
| NEListLit(_)
| SomeLit(_)
| Merge(_, _, _)
+ | ToMap(_, _)
| Annot(_, _)
if phase > Base =>
{
@@ -172,6 +179,10 @@ impl<A: Display + Clone> RawExpr<A> {
b.phase(PrintPhase::Import),
c.map(|x| x.phase(PrintPhase::App)),
),
+ ToMap(a, b) => ToMap(
+ a.phase(PrintPhase::Import),
+ b.map(|x| x.phase(PrintPhase::App)),
+ ),
Annot(a, b) => Annot(a.phase(Operator), b),
ExprF::BinOp(op, a, b) => ExprF::BinOp(
op,
diff --git a/tests_buffer b/tests_buffer
index 67de9eb..446c3f0 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -10,6 +10,8 @@ success/
LetNoAnnot let x = y in e
LetAnnot let x: T = y in e
EmptyRecordLiteral {=}
+ ToMap toMap x
+ ToMapAnnot toMap x : T
failure/
AssertNoAnnotation assert
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-01 12:42:01 +0000