Represent Optional literals more faithfully

6 files changed, 61 insertions, 74 deletions

diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs
index 9099afc..e8fcdab 100644
--- a/dhall/src/binary.rs
+++ b/dhall/src/binary.rs
@@ -105,16 +105,16 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
             }
             [U64(5), t] => {
                 let t = cbor_value_to_dhall(&t)?;
-                OptionalLit(Some(t), None)
+                EmptyOptionalLit(t)
             }
             [U64(5), Null, x] => {
                 let x = cbor_value_to_dhall(&x)?;
-                OptionalLit(None, Some(x))
+                NEOptionalLit(x)
             }
             [U64(5), t, x] => {
                 let x = cbor_value_to_dhall(&x)?;
                 let t = cbor_value_to_dhall(&t)?;
-                OptionalLit(Some(t), Some(x))
+                Annot(rc(NEOptionalLit(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 7eba0cc..65a9552 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -50,8 +50,8 @@ where
     let evaled_arg = arg_to_eval.map(|i| args[i].as_ref());
 
     let ret = match (b, evaled_arg, args.as_slice()) {
-        (OptionalSome, _, [x, ..]) => rc(OptionalLit(None, Some(Rc::clone(x)))),
-        (OptionalNone, _, [t, ..]) => rc(OptionalLit(Some(Rc::clone(t)), None)),
+        (OptionalSome, _, [x, ..]) => rc(NEOptionalLit(Rc::clone(x))),
+        (OptionalNone, _, [t, ..]) => rc(EmptyOptionalLit(Rc::clone(t))),
         (NaturalIsZero, Some(NaturalLit(n)), _) => rc(BoolLit(*n == 0)),
         (NaturalEven, Some(NaturalLit(n)), _) => rc(BoolLit(*n % 2 == 0)),
         (NaturalOdd, Some(NaturalLit(n)), _) => rc(BoolLit(*n % 2 != 0)),
@@ -64,16 +64,16 @@ where
         (ListLength, Some(EmptyListLit(_)), _) => rc(NaturalLit(0)),
         (ListLength, Some(NEListLit(ys)), _) => rc(NaturalLit(ys.len())),
         (ListHead, Some(EmptyListLit(t)), _) => {
-            rc(OptionalLit(Some(t.clone()), None))
+            rc(EmptyOptionalLit(t.clone()))
         }
         (ListHead, Some(NEListLit(ys)), _) => {
-            rc(OptionalLit(None, ys.iter().cloned().next()))
+            rc(NEOptionalLit(ys.first().unwrap().clone()))
         }
         (ListLast, Some(EmptyListLit(t)), _) => {
-            rc(OptionalLit(Some(t.clone()), None))
+            rc(EmptyOptionalLit(t.clone()))
         }
         (ListLast, Some(NEListLit(ys)), _) => {
-            rc(OptionalLit(None, ys.iter().cloned().last()))
+            rc(NEOptionalLit(ys.last().unwrap().clone()))
         }
         (ListReverse, Some(EmptyListLit(t)), _) => rc(EmptyListLit(t.clone())),
         (ListReverse, Some(NEListLit(ys)), _) => {
@@ -124,7 +124,7 @@ where
                 };
                 let a0 = Rc::clone(a0);
                 // TODO: use Embed to avoid reevaluating g
-                break dhall_expr!((g (Optional a0)) (λ(x: a0) -> [x] :  Optional a0) ([] :  Optional a0));
+                break dhall_expr!((g (Optional a0)) (λ(x: a0) -> Some x) (None a0));
             }
         }
         (ListFold, Some(EmptyListLit(_)), [_, _, _, _, nil, ..]) => {
@@ -144,7 +144,7 @@ where
         // }
         (
             OptionalFold,
-            Some(OptionalLit(_, Some(x))),
+            Some(NEOptionalLit(x)),
             [_, _, _, just, _, ..],
         ) => {
             let x = x.clone();
@@ -153,7 +153,7 @@ where
         }
         (
             OptionalFold,
-            Some(OptionalLit(_, None)),
+            Some(EmptyOptionalLit(_)),
             [_, _, _, _, nothing, ..],
         ) => Rc::clone(nothing),
         // // fold/build fusion
@@ -254,13 +254,6 @@ where
                 _ => rc(BoolIf(b, t.clone(), f.clone())),
             }
         }
-        OptionalLit(t, es) => {
-            if !es.is_none() {
-                rc(OptionalLit(None, es.clone()))
-            } else {
-                rc(OptionalLit(t.clone(), es.clone()))
-            }
-        }
         // TODO: interpolation
         // TextLit(t) =>
         BinOp(o, x, y) => {
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 15fb344..32ffe0e 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -372,29 +372,17 @@ where
             }
             return Ok(dhall_expr!(List t));
         }
-        OptionalLit(t, xs) => {
-            let mut iter = xs.iter();
-            let t: Rc<Expr<_, _>> = match t {
-                Some(t) => t.clone(),
-                None => {
-                    let x = iter.next().unwrap();
-                    type_with(ctx, x.clone())?
-                }
-            };
-
+        EmptyOptionalLit(t) => {
+            let s = normalized_type_with(ctx, t.clone())?;
+            ensure_is_type(s, InvalidOptionalType(t.clone()))?;
+            let t = normalize(t.clone());
+            return Ok(dhall_expr!(Optional t));
+        }
+        NEOptionalLit(x) => {
+            let t: Rc<Expr<_, _>> = type_with(ctx, x.clone())?;
             let s = normalized_type_with(ctx, t.clone())?;
             ensure_is_type(s, InvalidOptionalType(t.clone()))?;
             let t = normalize(t);
-            for x in iter {
-                let t2 = normalized_type_with(ctx, x.clone())?;
-                if !prop_equal(t.as_ref(), t2.as_ref()) {
-                    return Err(mkerr(InvalidOptionalElement(
-                        t,
-                        x.clone(),
-                        t2,
-                    )));
-                }
-            }
             return Ok(dhall_expr!(Optional t));
         }
         RecordType(kts) => {
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index 1d733aa..52fc0cf 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -195,9 +195,10 @@ pub enum Expr<Note, Embed> {
     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>>),
+    ///  None t
+    EmptyOptionalLit(SubExpr<Note, Embed>),
+    ///  Some e
+    NEOptionalLit(SubExpr<Note, Embed>),
     ///  `Record            [(k1, t1), (k2, t2)]   ~  { k1 : t1, k2 : t1 }`
     RecordType(BTreeMap<Label, SubExpr<Note, Embed>>),
     ///  `RecordLit         [(k1, v1), (k2, v2)]   ~  { k1 = v1, k2 = v2 }`
@@ -346,7 +347,8 @@ where
         BinOp(o, x, y) => BinOp(*o, map(x), map(y)),
         EmptyListLit(t) => EmptyListLit(map(t)),
         NEListLit(es) => NEListLit(vec(es)),
-        OptionalLit(t, es) => OptionalLit(opt(t), opt(es)),
+        EmptyOptionalLit(t) => EmptyOptionalLit(map(t)),
+        NEOptionalLit(e) => NEOptionalLit(map(e)),
         RecordType(kts) => RecordType(btmap(kts)),
         RecordLit(kvs) => RecordLit(btmap(kvs)),
         UnionType(kts) => UnionType(btmap(kts)),
diff --git a/dhall_core/src/parser.rs b/dhall_core/src/parser.rs
index 3310bb9..b07094d 100644
--- a/dhall_core/src/parser.rs
+++ b/dhall_core/src/parser.rs
@@ -123,10 +123,10 @@ macro_rules! match_pair {
         match_pair!(@make_child_match, ($($vars)*), ($($outer_acc)*), ($($acc)*, ParsedValue::$ty($x)), ($($rest_of_match)*) => $body, $($rest)*)
     };
     (@make_child_match, ($($vars:tt)*), ($($outer_acc:tt)*), (, $($acc:tt)*), ($(,)*) => $body:expr, $($rest:tt)*) => {
-        match_pair!(@make_matches, ($($vars)*), ([$($acc)*] => { $body }, $($outer_acc)*), $($rest)*)
+        match_pair!(@make_matches, ($($vars)*), ($($outer_acc)* [$($acc)*] => { $body },), $($rest)*)
     };
     (@make_child_match, ($($vars:tt)*), ($($outer_acc:tt)*), (), ($(,)*) => $body:expr, $($rest:tt)*) => {
-        match_pair!(@make_matches, ($($vars)*), ([] => { $body }, $($outer_acc)*), $($rest)*)
+        match_pair!(@make_matches, ($($vars)*), ($($outer_acc)* [] => { $body },), $($rest)*)
     };
 
     (@make_matches, ($($vars:tt)*), ($($acc:tt)*), [$($args:tt)*] => $body:expr, $($rest:tt)*) => {
@@ -469,17 +469,17 @@ make_parser! {
     rule!(Optional<()>; raw_pair!(_) => ());
 
     rule!(empty_collection<ParsedExpr> as expression; children!(
-        [List(_), expression(y)] => {
-            bx(Expr::EmptyListLit(y))
+        [List(_), expression(t)] => {
+            bx(Expr::EmptyListLit(t))
         },
-        [Optional(_), expression(y)] => {
-            bx(Expr::OptionalLit(Some(y), None))
+        [Optional(_), expression(t)] => {
+            bx(Expr::EmptyOptionalLit(t))
         },
     ));
 
     rule!(non_empty_optional<ParsedExpr> as expression; children!(
-        [expression(x), Optional(_), expression(z)] => {
-            bx(Expr::OptionalLit(Some(z), Some(x)))
+        [expression(x), Optional(_), expression(t)] => {
+            rc(Expr::Annot(rc(Expr::NEOptionalLit(x)), t))
         }
     ));
 
@@ -557,24 +557,36 @@ make_parser! {
     ));
 
     rule!(annotated_expression<ParsedExpr> as expression; children!(
+        [expression(e)] => e,
         [expression(e), expression(annot)] => {
             bx(Expr::Annot(e, annot))
         },
-        [expression(e)] => e,
     ));
 
     rule!(application_expression<ParsedExpr> as expression; children!(
-        [expression(first), expression(rest..)] => {
-            let rest: Vec<_> = rest.collect();
-            if rest.is_empty() {
-                first
-            } else {
-                bx(Expr::App(first, rest))
+        [expression(e)] => e,
+        [expression(first), expression(second)] => {
+            match first.as_ref() {
+                Expr::Builtin(Builtin::OptionalNone) =>
+                    bx(Expr::EmptyOptionalLit(second)),
+                Expr::Builtin(Builtin::OptionalSome) =>
+                    bx(Expr::NEOptionalLit(second)),
+                _ => bx(Expr::App(first, vec![second])),
             }
-        }
+        },
+        [expression(first), expression(second), expression(rest..)] => {
+            match first.as_ref() {
+                Expr::Builtin(Builtin::OptionalNone) =>
+                    bx(Expr::App(bx(Expr::EmptyOptionalLit(second)), rest.collect())),
+                Expr::Builtin(Builtin::OptionalSome) =>
+                    bx(Expr::App(bx(Expr::NEOptionalLit(second)), rest.collect())),
+                _ => bx(Expr::App(first, std::iter::once(second).chain(rest).collect())),
+            }
+        },
     ));
 
     rule!(selector_expression_raw<ParsedExpr> as expression; children!(
+        [expression(e)] => e,
         [expression(first), selector_raw(rest..)] => {
             rest.fold(first, |acc, e| bx(Expr::Field(acc, e)))
         }
diff --git a/dhall_generator/src/lib.rs b/dhall_generator/src/lib.rs
index a246818..328bc3e 100644
--- a/dhall_generator/src/lib.rs
+++ b/dhall_generator/src/lib.rs
@@ -63,10 +63,13 @@ fn dhall_to_tokenstream(
         NaturalLit(n) => {
             quote! { NaturalLit(#n) }
         }
-        OptionalLit(t, e) => {
-            let t = option_to_tokenstream(t, ctx);
-            let e = option_to_tokenstream(e, ctx);
-            quote! { OptionalLit(#t, #e) }
+        EmptyOptionalLit(x) => {
+            let x = dhall_to_tokenstream_bx(x, ctx);
+            quote! { EmptyOptionalLit(#x) }
+        }
+        NEOptionalLit(x) => {
+            let x = dhall_to_tokenstream_bx(x, ctx);
+            quote! { NEOptionalLit(#x) }
         }
         EmptyListLit(t) => {
             let t = dhall_to_tokenstream_bx(t, ctx);
@@ -153,17 +156,6 @@ fn map_to_tokenstream(
     } }
 }
 
-fn option_to_tokenstream(
-    e: &Option<DhallExpr>,
-    ctx: &Context<Label, ()>,
-) -> TokenStream {
-    let e = e.as_ref().map(|x| dhall_to_tokenstream_bx(x, ctx));
-    match e {
-        Some(x) => quote! { Some(#x) },
-        None => quote! { None },
-    }
-}
-
 fn vec_to_tokenstream(
     e: &Vec<DhallExpr>,
     ctx: &Context<Label, ()>,