From 63aa21c581933a10b2b1ab96c632c72834cf2115 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 15 Apr 2019 12:22:02 +0200 Subject: Handle empty optionals correctly Closes #78 --- dhall/src/binary.rs | 4 ++-- dhall/src/normalize.rs | 2 ++ dhall/src/tests.rs | 2 +- dhall/src/typecheck.rs | 14 ++++++++++++++ dhall_core/src/core.rs | 4 ++++ dhall_core/src/parser.rs | 8 ++------ dhall_core/src/printer.rs | 8 ++++++++ dhall_core/src/visitor.rs | 4 ++++ 8 files changed, 37 insertions(+), 9 deletions(-) diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs index 8a23e76..72704de 100644 --- a/dhall/src/binary.rs +++ b/dhall/src/binary.rs @@ -107,7 +107,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result { } [U64(5), t] => { let t = cbor_value_to_dhall(&t)?; - EmptyOptionalLit(t) + OldOptionalLit(None, t) } [U64(5), Null, x] => { let x = cbor_value_to_dhall(&x)?; @@ -116,7 +116,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result { [U64(5), t, x] => { let x = cbor_value_to_dhall(&x)?; let t = cbor_value_to_dhall(&t)?; - Annot(rc(NEOptionalLit(x)), t) + OldOptionalLit(Some(x), t) } [U64(6), x, y] => { let x = cbor_value_to_dhall(&x)?; diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 716b7ee..58deb87 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -265,6 +265,8 @@ fn normalize_ref(expr: &Expr>) -> Expr { BoolIf(BoolLit(false), _, f) => DoneRef(f), // TODO: interpolation // TextLit(t) => + OldOptionalLit(None, t) => Done(EmptyOptionalLit(t.roll())), + OldOptionalLit(Some(x), _) => Done(NEOptionalLit(x.roll())), BinOp(BoolAnd, BoolLit(x), BoolLit(y)) => Done(BoolLit(*x && *y)), BinOp(BoolOr, BoolLit(x), BoolLit(y)) => Done(BoolLit(*x || *y)), BinOp(BoolEQ, BoolLit(x), BoolLit(y)) => Done(BoolLit(x == y)), diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index f57f23f..ce24bfc 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -124,7 +124,7 @@ pub fn run_test( let expected = parse_file_str(&expected_file_path)? .resolve()? .skip_typecheck() - .skip_normalize(); + .normalize(); match feature { Parser => unreachable!(), diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index b8f2d86..5162f4f 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -266,6 +266,9 @@ fn type_of_builtin(b: Builtin) -> Expr> { forall (nothing: optional) -> optional ), + OptionalNone => dhall::expr!( + forall (a: Type) -> Optional a + ), _ => panic!("Unimplemented typecheck case: {:?}", b), } } @@ -544,6 +547,17 @@ fn type_last_layer( let t = x.get_type_move()?.into_normalized()?.into_expr(); Ok(RetExpr(dhall::expr!(List t))) } + OldOptionalLit(None, t) => { + let t = t.into_expr(); + let e = dhall::subexpr!(None t); + Ok(RetType(type_with(ctx, e)?.get_type()?.into_owned())) + } + OldOptionalLit(Some(x), t) => { + let x = x.into_expr(); + let t = t.into_expr(); + let e = dhall::subexpr!(Some x : Optional t); + Ok(RetType(type_with(ctx, e)?.get_type()?.into_owned())) + } EmptyOptionalLit(t) => { let t = t.normalize().into_type(); ensure_simple_type!( diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs index 7859c73..c0e04ed 100644 --- a/dhall_core/src/core.rs +++ b/dhall_core/src/core.rs @@ -174,6 +174,10 @@ pub enum ExprF { EmptyListLit(SubExpr), /// [x, y, z] NEListLit(Vec), + /// Deprecated Optional literal form + /// [] : Optional a + /// [x] : Optional a + OldOptionalLit(Option, SubExpr), /// None t EmptyOptionalLit(SubExpr), /// Some e diff --git a/dhall_core/src/parser.rs b/dhall_core/src/parser.rs index cea7cea..c4ae2e5 100644 --- a/dhall_core/src/parser.rs +++ b/dhall_core/src/parser.rs @@ -641,13 +641,13 @@ make_parser! { spanned(span, EmptyListLit(rc(t))) }, [Optional(_), expression(t)] => { - spanned(span, EmptyOptionalLit(rc(t))) + spanned(span, OldOptionalLit(None, rc(t))) }, )); rule!(non_empty_optional> as expression; span; children!( [expression(x), Optional(_), expression(t)] => { - spanned(span, Annot(rc(NEOptionalLit(rc(x))), rc(t))) + spanned(span, OldOptionalLit(Option::Some(rc(x)), rc(t))) } )); @@ -747,10 +747,6 @@ make_parser! { rule!(application_expression> as expression; span; children!( [expression(e)] => e, - [expression(Builtin(crate::Builtin::OptionalNone)), - expression(e), expression(rest)..] => { - spanned(span, app(EmptyOptionalLit(rc(e)), rest.map(rc).collect())) - }, [Some(()), expression(e), expression(rest)..] => { spanned(span, app(NEOptionalLit(rc(e)), rest.map(rc).collect())) }, diff --git a/dhall_core/src/printer.rs b/dhall_core/src/printer.rs index e53c1ec..bb094de 100644 --- a/dhall_core/src/printer.rs +++ b/dhall_core/src/printer.rs @@ -32,6 +32,12 @@ impl Display for ExprF { NEListLit(es) => { fmt_list("[", ", ", "]", es, f, Display::fmt)?; } + OldOptionalLit(None, t) => { + write!(f, "[] : Optional {}", t)?; + } + OldOptionalLit(Some(x), t) => { + write!(f, "[{}] : Optional {}", x, t)?; + } EmptyOptionalLit(t) => { write!(f, "None {}", t)?; } @@ -149,6 +155,7 @@ impl Expr { | Let(_, _, _, _) | EmptyListLit(_) | NEListLit(_) + | OldOptionalLit(_, _) | EmptyOptionalLit(_) | NEOptionalLit(_) | Merge(_, _, _) @@ -189,6 +196,7 @@ impl Expr { b.phase(PrintPhase::BinOp(op)), ), EmptyListLit(t) => EmptyListLit(t.phase(Import)), + OldOptionalLit(x, t) => OldOptionalLit(x, t.phase(Import)), EmptyOptionalLit(t) => EmptyOptionalLit(t.phase(Import)), NEOptionalLit(e) => NEOptionalLit(e.phase(Import)), ExprF::App(a, args) => ExprF::App( diff --git a/dhall_core/src/visitor.rs b/dhall_core/src/visitor.rs index b0424ac..3b06f8b 100644 --- a/dhall_core/src/visitor.rs +++ b/dhall_core/src/visitor.rs @@ -148,6 +148,10 @@ where ), EmptyListLit(t) => EmptyListLit(v.visit_subexpr(t)?), NEListLit(es) => NEListLit(vec(es, |e| v.visit_subexpr(e))?), + OldOptionalLit(x, t) => OldOptionalLit( + opt(x, |e| v.visit_subexpr(e))?, + v.visit_subexpr(t)?, + ), EmptyOptionalLit(t) => EmptyOptionalLit(v.visit_subexpr(t)?), NEOptionalLit(e) => NEOptionalLit(v.visit_subexpr(e)?), RecordType(kts) => RecordType(btmap(kts, v)?), -- cgit v1.2.3