From 83bc67d4572fe7961842f915d5559ee489e13dfd Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 20 Apr 2019 23:12:25 +0200 Subject: An empty optional value is purely semantic --- dhall/src/binary.rs | 2 +- dhall/src/normalize.rs | 13 +++++-------- dhall/src/typecheck.rs | 8 +------- dhall_core/src/core.rs | 4 +--- dhall_core/src/parser.rs | 2 +- dhall_core/src/printer.rs | 11 +++-------- dhall_core/src/visitor.rs | 3 +-- dhall_generator/src/quote.rs | 7 ++----- 8 files changed, 15 insertions(+), 35 deletions(-) diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs index 62ebcf7..7ded3a5 100644 --- a/dhall/src/binary.rs +++ b/dhall/src/binary.rs @@ -111,7 +111,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result { } [U64(5), Null, x] => { let x = cbor_value_to_dhall(&x)?; - NEOptionalLit(x) + SomeLit(x) } [U64(5), t, x] => { let x = cbor_value_to_dhall(&x)?; diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 9e7c531..f092c4d 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -366,10 +366,12 @@ impl WHNF { WHNF::NaturalLit(n) => rc(ExprF::NaturalLit(n)), WHNF::IntegerLit(n) => rc(ExprF::IntegerLit(n)), WHNF::EmptyOptionalLit(n) => { - rc(ExprF::EmptyOptionalLit(n.normalize().normalize_to_expr())) + WHNF::Expr(rc(ExprF::Builtin(Builtin::OptionalNone))) + .app(n.normalize()) + .normalize_to_expr() } WHNF::NEOptionalLit(n) => { - rc(ExprF::NEOptionalLit(n.normalize().normalize_to_expr())) + rc(ExprF::SomeLit(n.normalize().normalize_to_expr())) } WHNF::EmptyListLit(n) => { rc(ExprF::EmptyListLit(n.normalize().normalize_to_expr())) @@ -628,12 +630,7 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF { ExprF::OldOptionalLit(Some(e), _) => { WHNF::NEOptionalLit(Now::new(ctx, e.clone())) } - ExprF::EmptyOptionalLit(e) => { - WHNF::EmptyOptionalLit(Now::new(ctx, e.clone())) - } - ExprF::NEOptionalLit(e) => { - WHNF::NEOptionalLit(Now::new(ctx, e.clone())) - } + ExprF::SomeLit(e) => WHNF::NEOptionalLit(Now::new(ctx, e.clone())), ExprF::EmptyListLit(e) => WHNF::EmptyListLit(Now::new(ctx, e.clone())), ExprF::NEListLit(elts) => WHNF::NEListLit( elts.iter() diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index ddb96da..b26f845 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -563,13 +563,7 @@ fn type_last_layer( let e = dhall::subexpr!(Some x : Optional t); Ok(RetType(type_with(ctx, e)?.get_type()?.into_owned())) } - EmptyOptionalLit(t) => { - let t = t.normalize(); - ensure_simple_type!(t, mkerr(InvalidOptionalType(t))); - let t = t.embed(); - Ok(RetExpr(dhall::expr!(Optional t))) - } - NEOptionalLit(x) => { + SomeLit(x) => { let tx = x.get_type_move()?; ensure_simple_type!( tx, diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs index 9a8acc2..fa6fca4 100644 --- a/dhall_core/src/core.rs +++ b/dhall_core/src/core.rs @@ -180,10 +180,8 @@ pub enum ExprF { /// `[] : Optional a` /// `[x] : Optional a` OldOptionalLit(Option, SubExpr), - /// `None t` - EmptyOptionalLit(SubExpr), /// `Some e` - NEOptionalLit(SubExpr), + SomeLit(SubExpr), /// `{ k1 : t1, k2 : t1 }` RecordType(BTreeMap), /// `{ k1 = v1, k2 = v2 }` diff --git a/dhall_core/src/parser.rs b/dhall_core/src/parser.rs index 31249a9..ba15bae 100644 --- a/dhall_core/src/parser.rs +++ b/dhall_core/src/parser.rs @@ -754,7 +754,7 @@ make_parser! { children!( [expression(e)] => e, [Some_(()), expression(e)] => { - spanned(span, NEOptionalLit(rc(e))) + spanned(span, SomeLit(rc(e))) }, [merge(()), expression(x), expression(y)] => { spanned(span, Merge(rc(x), rc(y), None)) diff --git a/dhall_core/src/printer.rs b/dhall_core/src/printer.rs index ea291a9..c4bad71 100644 --- a/dhall_core/src/printer.rs +++ b/dhall_core/src/printer.rs @@ -38,10 +38,7 @@ impl Display for ExprF { OldOptionalLit(Some(x), t) => { write!(f, "[{}] : Optional {}", x, t)?; } - EmptyOptionalLit(t) => { - write!(f, "None {}", t)?; - } - NEOptionalLit(e) => { + SomeLit(e) => { write!(f, "Some {}", e)?; } Merge(a, b, c) => { @@ -159,8 +156,7 @@ impl Expr { | EmptyListLit(_) | NEListLit(_) | OldOptionalLit(_, _) - | EmptyOptionalLit(_) - | NEOptionalLit(_) + | SomeLit(_) | Merge(_, _, _) | Annot(_, _) if phase > Base => @@ -200,8 +196,7 @@ impl Expr { ), 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)), + SomeLit(e) => SomeLit(e.phase(Import)), ExprF::App(f, a) => ExprF::App(f.phase(Import), a.phase(Import)), Field(a, b) => Field(a.phase(Primitive), b), Projection(e, ls) => Projection(e.phase(Primitive), ls), diff --git a/dhall_core/src/visitor.rs b/dhall_core/src/visitor.rs index c15aacd..caaefce 100644 --- a/dhall_core/src/visitor.rs +++ b/dhall_core/src/visitor.rs @@ -153,8 +153,7 @@ where 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)?), + SomeLit(e) => SomeLit(v.visit_subexpr(e)?), RecordType(kts) => RecordType(btmap(kts, v)?), RecordLit(kvs) => RecordLit(btmap(kvs, v)?), UnionType(kts) => UnionType(btoptmap(kts, v)?), diff --git a/dhall_generator/src/quote.rs b/dhall_generator/src/quote.rs index 38910a8..c588eda 100644 --- a/dhall_generator/src/quote.rs +++ b/dhall_generator/src/quote.rs @@ -66,11 +66,8 @@ where BoolLit(b) => { quote! { dhall_core::ExprF::BoolLit(#b) } } - EmptyOptionalLit(x) => { - quote! { dhall_core::ExprF::EmptyOptionalLit(#x) } - } - NEOptionalLit(x) => { - quote! { dhall_core::ExprF::NEOptionalLit(#x) } + SomeLit(x) => { + quote! { dhall_core::ExprF::SomeLit(#x) } } EmptyListLit(t) => { quote! { dhall_core::ExprF::EmptyListLit(#t) } -- cgit v1.2.3