From 845abbb0404ac15cefeca8b6ac32d9b3f93e5987 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 21 Mar 2019 16:36:46 +0100
Subject: Represent Optional literals more faithfully

---
 dhall/src/binary.rs    |  6 +++---
 dhall/src/normalize.rs | 25 +++++++++----------------
 dhall/src/typecheck.rs | 28 ++++++++--------------------
 3 files changed, 20 insertions(+), 39 deletions(-)

(limited to 'dhall')

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) => {
-- 
cgit v1.2.3