From 92ea98da2f89348c3dfdc7d49594a4d876d06ba2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 18 Mar 2019 05:27:17 +0100 Subject: Split List literal between empty and non-empty --- dhall/src/binary.rs | 4 ++-- dhall/src/normalize.rs | 46 ++++++++++++++++++++++++++------------------ dhall/src/typecheck.rs | 17 ++++++++-------- dhall/tests/normalization.rs | 6 +++--- dhall_core/src/core.rs | 25 ++++++++++++------------ dhall_core/src/parser.rs | 4 ++-- dhall_generator/src/lib.rs | 9 ++++++--- 7 files changed, 61 insertions(+), 50 deletions(-) diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs index 2279a51..1ab7956 100644 --- a/dhall/src/binary.rs +++ b/dhall/src/binary.rs @@ -94,14 +94,14 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result { } [U64(4), t] => { let t = cbor_value_to_dhall(&t)?; - ListLit(Some(t), vec![]) + EmptyListLit(t) } [U64(4), Null, rest..] => { let rest = rest .iter() .map(cbor_value_to_dhall) .collect::, _>>()?; - ListLit(None, rest) + NEListLit(rest) } [U64(5), t] => { let t = cbor_value_to_dhall(&t)?; diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index bf1bff5..c728dd0 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -57,16 +57,26 @@ where (NaturalShow, Some(NaturalLit(n)), _) => { rc(TextLit(n.to_string().into())) } - (ListLength, Some(ListLit(_, ys)), _) => rc(NaturalLit(ys.len())), - (ListHead, Some(ListLit(t, ys)), _) => { - rc(OptionalLit(t.clone(), ys.iter().cloned().next())) + (ListLength, Some(EmptyListLit(_)), _) => rc(NaturalLit(0)), + (ListLength, Some(NEListLit(ys)), _) => rc(NaturalLit(ys.len())), + (ListHead, Some(EmptyListLit(t)), _) => { + rc(OptionalLit(Some(t.clone()), None)) } - (ListLast, Some(ListLit(t, ys)), _) => { - rc(OptionalLit(t.clone(), ys.iter().cloned().last())) + (ListHead, Some(NEListLit(ys)), _) => { + rc(OptionalLit(None, ys.iter().cloned().next())) } - (ListReverse, Some(ListLit(t, ys)), _) => { - let xs = ys.iter().rev().cloned().collect(); - rc(ListLit(t.clone(), xs)) + (ListLast, Some(EmptyListLit(t)), _) => { + rc(OptionalLit(Some(t.clone()), None)) + } + (ListLast, Some(NEListLit(ys)), _) => { + rc(OptionalLit(None, ys.iter().cloned().last())) + } + (ListReverse, Some(EmptyListLit(t)), _) => { + rc(EmptyListLit(t.clone())) + } + (ListReverse, Some(NEListLit(ys)), _) => { + let ys = ys.iter().rev().cloned().collect(); + rc(NEListLit(ys)) } (ListBuild, _, [a0, g, ..]) => { loop { @@ -99,7 +109,10 @@ where break dhall_expr!((g (Optional a0)) (λ(x: a0) -> [x] : Optional a0) ([] : Optional a0)); } } - (ListFold, Some(ListLit(_, xs)), [_, _, _, cons, nil, ..]) => { + (ListFold, Some(EmptyListLit(_)), [_, _, _, _, nil, ..]) => { + Rc::clone(nil) + } + (ListFold, Some(NEListLit(xs)), [_, _, _, cons, nil, ..]) => { xs.iter().rev().fold(Rc::clone(nil), |acc, x| { let x = x.clone(); let acc = acc.clone(); @@ -233,18 +246,13 @@ where NaturalLit(x * y) } (TextAppend, TextLit(x), TextLit(y)) => TextLit(x + y), - (ListAppend, ListLit(t1, xs), ListLit(t2, ys)) => { - let t1: Option> = t1.as_ref().map(Rc::clone); - let t2: Option> = t2.as_ref().map(Rc::clone); - // Drop type annotation if the result is nonempty - let t = if xs.is_empty() && ys.is_empty() { - t1.or(t2) - } else { - None - }; + (ListAppend, EmptyListLit(t), EmptyListLit(_)) => EmptyListLit(Rc::clone(t)), + (ListAppend, EmptyListLit(_), _) => return y, + (ListAppend, _, EmptyListLit(_)) => return x, + (ListAppend, NEListLit(xs), NEListLit(ys)) => { let xs = xs.into_iter().cloned(); let ys = ys.into_iter().cloned(); - ListLit(t, xs.chain(ys).collect()) + NEListLit(xs.chain(ys).collect()) } (o, _, _) => BinOp(*o, x, y), }) diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 26ab360..387327a 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -351,15 +351,16 @@ where } return Ok(ty); } - ListLit(t, xs) => { + EmptyListLit(t) => { + let s = normalized_type_with(ctx, t.clone())?; + ensure_is_type(s, InvalidListType(t.clone()))?; + let t = normalize(Rc::clone(t)); + return Ok(dhall_expr!(List t)); + } + NEListLit(xs) => { let mut iter = xs.iter().enumerate(); - let t: Rc> = match t { - Some(t) => t.clone(), - None => { - let (_, first_x) = iter.next().unwrap(); - type_with(ctx, first_x.clone())? - } - }; + let (_, first_x) = iter.next().unwrap(); + let t = type_with(ctx, first_x.clone())?; let s = normalized_type_with(ctx, t.clone())?; ensure_is_type(s, InvalidListType(t.clone()))?; diff --git a/dhall/tests/normalization.rs b/dhall/tests/normalization.rs index 243cf24..c1ea81d 100644 --- a/dhall/tests/normalization.rs +++ b/dhall/tests/normalization.rs @@ -265,10 +265,10 @@ norm!(spec_normalization_success_unit_NoneNatural, "unit/NoneNatural"); // norm!(spec_normalization_success_unit_OperatorEqualLhsTrue, "unit/OperatorEqualLhsTrue"); // norm!(spec_normalization_success_unit_OperatorEqualNormalizeArguments, "unit/OperatorEqualNormalizeArguments"); // norm!(spec_normalization_success_unit_OperatorEqualRhsTrue, "unit/OperatorEqualRhsTrue"); -// norm!(spec_normalization_success_unit_OperatorListConcatenateLhsEmpty, "unit/OperatorListConcatenateLhsEmpty"); +norm!(spec_normalization_success_unit_OperatorListConcatenateLhsEmpty, "unit/OperatorListConcatenateLhsEmpty"); norm!(spec_normalization_success_unit_OperatorListConcatenateListList, "unit/OperatorListConcatenateListList"); -// norm!(spec_normalization_success_unit_OperatorListConcatenateNormalizeArguments, "unit/OperatorListConcatenateNormalizeArguments"); -// norm!(spec_normalization_success_unit_OperatorListConcatenateRhsEmpty, "unit/OperatorListConcatenateRhsEmpty"); +norm!(spec_normalization_success_unit_OperatorListConcatenateNormalizeArguments, "unit/OperatorListConcatenateNormalizeArguments"); +norm!(spec_normalization_success_unit_OperatorListConcatenateRhsEmpty, "unit/OperatorListConcatenateRhsEmpty"); // norm!(spec_normalization_success_unit_OperatorNotEqualEquivalentArguments, "unit/OperatorNotEqualEquivalentArguments"); // norm!(spec_normalization_success_unit_OperatorNotEqualLhsFalse, "unit/OperatorNotEqualLhsFalse"); // norm!(spec_normalization_success_unit_OperatorNotEqualNormalizeArguments, "unit/OperatorNotEqualNormalizeArguments"); diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs index a3236eb..722506b 100644 --- a/dhall_core/src/core.rs +++ b/dhall_core/src/core.rs @@ -307,8 +307,10 @@ pub enum Expr { DoubleLit(Double), /// `TextLit t ~ t` TextLit(InterpolatedText), - /// `ListLit t [x, y, z] ~ [x, y, z] : List t` - ListLit(Option>, Vec>), + /// [] : List t` + EmptyListLit(SubExpr), + /// [x, y, z] + NEListLit(Vec>), /// `OptionalLit t [e] ~ [e] : Optional t` /// `OptionalLit t [] ~ [] : Optional t` OptionalLit(Option>, Option>), @@ -543,16 +545,12 @@ impl Expr { write!(f, ") → ")?; d.fmt_b(f) } - &ListLit(ref t, ref es) => { - fmt_list("[", "]", es, f, |e, f| e.fmt(f))?; - match t { - Some(t) => { - write!(f, " : List ")?; - t.fmt_e(f)? - } - None => {} - } - Ok(()) + &EmptyListLit(ref t) => { + write!(f, "[] : List ")?; + t.fmt_e(f) + } + &NEListLit(ref es) => { + fmt_list("[", "]", es, f, |e, f| e.fmt(f)) } &OptionalLit(ref t, ref es) => { match es { @@ -902,7 +900,8 @@ where DoubleLit(n) => DoubleLit(*n), TextLit(t) => TextLit(t.map(&map)), BinOp(o, x, y) => BinOp(*o, map(x), map(y)), - ListLit(t, es) => ListLit(opt(t), vec(es)), + EmptyListLit(t) => EmptyListLit(map(t)), + NEListLit(es) => NEListLit(vec(es)), OptionalLit(t, es) => OptionalLit(opt(t), opt(es)), Record(kts) => Record(btmap(kts)), RecordLit(kvs) => RecordLit(btmap(kvs)), diff --git a/dhall_core/src/parser.rs b/dhall_core/src/parser.rs index 9487ebc..6809aa2 100644 --- a/dhall_core/src/parser.rs +++ b/dhall_core/src/parser.rs @@ -650,7 +650,7 @@ rule!(empty_collection; children!(x: str, y: expression) => { match x { "Optional" => bx(Expr::OptionalLit(Some(y), None)), - "List" => bx(Expr::ListLit(Some(y), vec![])), + "List" => bx(Expr::EmptyListLit(y)), _ => unreachable!(), } } @@ -871,7 +871,7 @@ rule!(union_type_entry<(Label, RcExpr)>; rule!(non_empty_list_literal_raw; children!(items*: expression) => { - bx(Expr::ListLit(None, items.collect())) + bx(Expr::NEListLit(items.collect())) } ); diff --git a/dhall_generator/src/lib.rs b/dhall_generator/src/lib.rs index 9c0aacf..528f0ea 100644 --- a/dhall_generator/src/lib.rs +++ b/dhall_generator/src/lib.rs @@ -65,10 +65,13 @@ fn dhall_to_tokenstream( let e = option_to_tokenstream(e, ctx); quote! { OptionalLit(#t, #e) } } - ListLit(t, es) => { - let t = option_to_tokenstream(t, ctx); + EmptyListLit(t) => { + let t = dhall_to_tokenstream_bx(t, ctx); + quote! { EmptyListLit(#t) } + } + NEListLit(es) => { let es = vec_to_tokenstream(es, ctx); - quote! { ListLit(#t, #es) } + quote! { NEListLit(#es) } } Record(m) => { let m = map_to_tokenstream(m, ctx); -- cgit v1.2.3