From aba7e62e49ac9dead0a2868f739091d2d15ff0d1 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 31 Aug 2019 21:59:39 +0200 Subject: Implement parsing of `toMap` keyword --- dhall/build.rs | 9 --------- dhall/src/phase/binary.rs | 11 +++++++++++ dhall/src/phase/normalize.rs | 1 + dhall/src/phase/typecheck.rs | 1 + dhall_syntax/src/core/expr.rs | 2 ++ dhall_syntax/src/core/visitor.rs | 3 +++ dhall_syntax/src/parser.rs | 8 +++++++- dhall_syntax/src/printer.rs | 11 +++++++++++ tests_buffer | 2 ++ 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 { 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 { UnionType(DupTreeMap>), /// `merge x y : t` Merge(SubExpr, SubExpr, Option), + /// `toMap x : t` + ToMap(SubExpr, Option), /// `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; 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; 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 Display for ExprF { 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 RawExpr { | NEListLit(_) | SomeLit(_) | Merge(_, _, _) + | ToMap(_, _) | Annot(_, _) if phase > Base => { @@ -172,6 +179,10 @@ impl RawExpr { 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 -- cgit v1.2.3