From 63aa21c581933a10b2b1ab96c632c72834cf2115 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 15 Apr 2019 12:22:02 +0200
Subject: Handle empty optionals correctly

Closes #78
---
 dhall/src/binary.rs    |  4 ++--
 dhall/src/normalize.rs |  2 ++
 dhall/src/tests.rs     |  2 +-
 dhall/src/typecheck.rs | 14 ++++++++++++++
 4 files changed, 19 insertions(+), 3 deletions(-)

(limited to 'dhall/src')

diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs
index 8a23e76..72704de 100644
--- a/dhall/src/binary.rs
+++ b/dhall/src/binary.rs
@@ -107,7 +107,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
             }
             [U64(5), t] => {
                 let t = cbor_value_to_dhall(&t)?;
-                EmptyOptionalLit(t)
+                OldOptionalLit(None, t)
             }
             [U64(5), Null, x] => {
                 let x = cbor_value_to_dhall(&x)?;
@@ -116,7 +116,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
             [U64(5), t, x] => {
                 let x = cbor_value_to_dhall(&x)?;
                 let t = cbor_value_to_dhall(&t)?;
-                Annot(rc(NEOptionalLit(x)), t)
+                OldOptionalLit(Some(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 716b7ee..58deb87 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -265,6 +265,8 @@ fn normalize_ref(expr: &Expr<X, Normalized<'static>>) -> Expr<X, X> {
         BoolIf(BoolLit(false), _, f) => DoneRef(f),
         // TODO: interpolation
         // TextLit(t) =>
+        OldOptionalLit(None, t) => Done(EmptyOptionalLit(t.roll())),
+        OldOptionalLit(Some(x), _) => Done(NEOptionalLit(x.roll())),
         BinOp(BoolAnd, BoolLit(x), BoolLit(y)) => Done(BoolLit(*x && *y)),
         BinOp(BoolOr, BoolLit(x), BoolLit(y)) => Done(BoolLit(*x || *y)),
         BinOp(BoolEQ, BoolLit(x), BoolLit(y)) => Done(BoolLit(x == y)),
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index f57f23f..ce24bfc 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -124,7 +124,7 @@ pub fn run_test(
             let expected = parse_file_str(&expected_file_path)?
                 .resolve()?
                 .skip_typecheck()
-                .skip_normalize();
+                .normalize();
 
             match feature {
                 Parser => unreachable!(),
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index b8f2d86..5162f4f 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -266,6 +266,9 @@ fn type_of_builtin<S>(b: Builtin) -> Expr<S, Normalized<'static>> {
             forall (nothing: optional) ->
             optional
         ),
+        OptionalNone => dhall::expr!(
+            forall (a: Type) -> Optional a
+        ),
         _ => panic!("Unimplemented typecheck case: {:?}", b),
     }
 }
@@ -544,6 +547,17 @@ fn type_last_layer(
             let t = x.get_type_move()?.into_normalized()?.into_expr();
             Ok(RetExpr(dhall::expr!(List t)))
         }
+        OldOptionalLit(None, t) => {
+            let t = t.into_expr();
+            let e = dhall::subexpr!(None t);
+            Ok(RetType(type_with(ctx, e)?.get_type()?.into_owned()))
+        }
+        OldOptionalLit(Some(x), t) => {
+            let x = x.into_expr();
+            let t = t.into_expr();
+            let e = dhall::subexpr!(Some x : Optional t);
+            Ok(RetType(type_with(ctx, e)?.get_type()?.into_owned()))
+        }
         EmptyOptionalLit(t) => {
             let t = t.normalize().into_type();
             ensure_simple_type!(
-- 
cgit v1.2.3