Split List literal between empty and non-empty

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<ParsedExpr, DecodeError> {
             }
             [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::<Result<Vec<_>, _>>()?;
-                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<Rc<_>> = t1.as_ref().map(Rc::clone);
-                    let t2: Option<Rc<_>> = 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<Expr<_, _>> = 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<Note, Embed> {
     DoubleLit(Double),
     ///  `TextLit t                                ~  t`
     TextLit(InterpolatedText<Note, Embed>),
-    ///  `ListLit t [x, y, z]                      ~  [x, y, z] : List t`
-    ListLit(Option<SubExpr<Note, Embed>>, Vec<SubExpr<Note, Embed>>),
+    ///  [] : List t`
+    EmptyListLit(SubExpr<Note, Embed>),
+    ///  [x, y, z]
+    NEListLit(Vec<SubExpr<Note, Embed>>),
     ///  `OptionalLit t [e]                        ~  [e] : Optional t`
     ///  `OptionalLit t []                         ~  []  : Optional t`
     OptionalLit(Option<SubExpr<Note, Embed>>, Option<SubExpr<Note, Embed>>),
@@ -543,16 +545,12 @@ impl<S, A: Display> Expr<S, A> {
                 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<RcExpr>;
     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<RcExpr>;
     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);