Add support for dependent types

8 files changed, 87 insertions, 27 deletions

diff --git a/dhall/build.rs b/dhall/build.rs
index b6df3d0..c05df0d 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -199,7 +199,7 @@ fn main() -> std::io::Result<()> {
             || path == "success/unit/EmptyToMap"
             || path == "success/unit/ToMap"
             || path == "success/unit/ToMapWithType"
-            // Normalize field selection further by inspecting the argument
+            // TODO: Normalize field selection further by inspecting the argument
             || path == "success/simplifications/rightBiasedMergeWithinRecordProjectionWithinFieldSelection0"
             || path == "success/simplifications/rightBiasedMergeWithinRecordProjectionWithinFieldSelection1"
             || path == "success/simplifications/rightBiasedMergeWithinRecursiveRecordMergeWithinFieldselection"
@@ -229,7 +229,10 @@ fn main() -> std::io::Result<()> {
         "Typecheck",
         |path| {
             false
+            // TODO: Enable imports in typecheck tests
             || path == "failure/importBoundary"
+            // Too slow
+            || path == "success/prelude"
             // TODO: Inline headers
             || path == "failure/customHeadersUsingBoundVariable"
             // TODO: projection by expression
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index 5c569e1..5bc25f2 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -221,6 +221,10 @@ impl TypeThunk {
         self.0.to_type()
     }
 
+    pub fn to_typed(&self) -> Typed {
+        self.0.clone()
+    }
+
     pub fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr {
         self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
     }
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index d7b9149..26568b5 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -47,7 +47,7 @@ pub enum Value {
     DoubleLit(NaiveDouble),
     EmptyOptionalLit(TypeThunk),
     NEOptionalLit(Thunk),
-    // EmptyListLit(t) means `[] : List t`
+    // EmptyListLit(t) means `[] : List t`, not `[] : t`
     EmptyListLit(TypeThunk),
     NEListLit(Vec<Thunk>),
     RecordLit(HashMap<Label, Thunk>),
@@ -58,6 +58,7 @@ pub enum Value {
     // Invariant: this must not contain interpolations that are themselves TextLits, and
     // contiguous text values must be merged.
     TextLit(Vec<InterpolatedTextContents<Thunk>>),
+    Equivalence(TypeThunk, TypeThunk),
     // Invariant: this must not contain a value captured by one of the variants above.
     PartialExpr(ExprF<Thunk, X>),
 }
@@ -196,6 +197,11 @@ impl Value {
                         .collect(),
                 ))
             }
+            Value::Equivalence(x, y) => rc(ExprF::BinOp(
+                dhall_syntax::BinOp::Equivalence,
+                x.normalize_to_expr_maybe_alpha(alpha),
+                y.normalize_to_expr_maybe_alpha(alpha),
+            )),
             Value::PartialExpr(e) => {
                 rc(e.map_ref_simple(|v| v.normalize_to_expr_maybe_alpha(alpha)))
             }
@@ -282,6 +288,10 @@ impl Value {
                     }
                 }
             }
+            Value::Equivalence(x, y) => {
+                x.normalize_mut();
+                y.normalize_mut();
+            }
             Value::PartialExpr(e) => {
                 // TODO: need map_mut_simple
                 e.map_ref_simple(|v| {
@@ -418,6 +428,9 @@ impl Shift for Value {
                     })
                     .collect::<Result<_, _>>()?,
             ),
+            Value::Equivalence(x, y) => {
+                Value::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?)
+            }
             Value::PartialExpr(e) => Value::PartialExpr(
                 e.traverse_ref_with_special_handling_of_binders(
                     |v| Ok(v.shift(delta, var)?),
@@ -533,6 +546,10 @@ impl Subst<Typed> for Value {
                     })
                     .collect(),
             ),
+            Value::Equivalence(x, y) => Value::Equivalence(
+                x.subst_shift(var, val),
+                y.subst_shift(var, val),
+            ),
         }
     }
 }
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index a0ee30a..3c00017 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -68,7 +68,6 @@ pub(crate) enum TypeMessage {
     MissingRecordField(Label, Typed),
     MissingUnionField(Label, Normalized),
     BinOpTypeMismatch(BinOp, Typed),
-    NoDependentTypes(Normalized, Normalized),
     InvalidTextInterpolation(Typed),
     Merge1ArgMustBeRecord(Typed),
     Merge2ArgMustBeUnion(Typed),
@@ -86,7 +85,10 @@ pub(crate) enum TypeMessage {
     RecordTypeMergeRequiresRecordType(Type),
     RecordTypeMismatch(Type, Type, Type, Type),
     UnionTypeDuplicateField,
-    // Unimplemented,
+    EquivalenceArgumentMustBeTerm(bool, Typed),
+    EquivalenceTypeMismatch(Typed, Typed),
+    AssertMismatch(Typed, Typed),
+    AssertMustTakeEquivalence,
 }
 
 impl TypeError {
diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs
index 5e7eb40..719b1c7 100644
--- a/dhall/src/phase/binary.rs
+++ b/dhall/src/phase/binary.rs
@@ -119,6 +119,7 @@ fn cbor_value_to_dhall(
                     9 => RightBiasedRecordMerge,
                     10 => RecursiveRecordTypeMerge,
                     11 => ImportAlt,
+                    12 => Equivalence,
                     _ => {
                         Err(DecodeError::WrongFormatError("binop".to_owned()))?
                     }
@@ -211,6 +212,10 @@ fn cbor_value_to_dhall(
                         .collect::<Result<_, _>>()?,
                 )))
             }
+            [U64(19), t] => {
+                let t = cbor_value_to_dhall(&t)?;
+                Assert(t)
+            }
             [U64(24), hash, U64(mode), U64(scheme), rest..] => {
                 let mode = match mode {
                     0 => ImportMode::Code,
@@ -504,6 +509,7 @@ where
             )
         }
         Annot(x, y) => ser_seq!(ser; tag(26), expr(x), expr(y)),
+        Assert(x) => ser_seq!(ser; tag(19), expr(x)),
         SomeLit(x) => ser_seq!(ser; tag(5), null(), expr(x)),
         EmptyListLit(x) => match x.as_ref() {
             App(f, a) => match f.as_ref() {
@@ -541,6 +547,7 @@ where
                 RightBiasedRecordMerge => 9,
                 RecursiveRecordTypeMerge => 10,
                 ImportAlt => 11,
+                Equivalence => 12,
             };
             ser_seq!(ser; tag(3), U64(op), expr(x), expr(y))
         }
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 395cf28..ecad063 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -508,9 +508,9 @@ where
 
 fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
     use BinOp::{
-        BoolAnd, BoolEQ, BoolNE, BoolOr, ListAppend, NaturalPlus, NaturalTimes,
-        RecursiveRecordMerge, RecursiveRecordTypeMerge, RightBiasedRecordMerge,
-        TextAppend,
+        BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
+        NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
+        RightBiasedRecordMerge, TextAppend,
     };
     use Value::{
         BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
@@ -626,6 +626,11 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
             Ret::Value(RecordType(kvs))
         }
 
+        (Equivalence, _, _) => Ret::Value(Value::Equivalence(
+            TypeThunk::from_thunk(x.clone()),
+            TypeThunk::from_thunk(y.clone()),
+        )),
+
         _ => return None,
     })
 }
@@ -641,6 +646,7 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
         ExprF::Embed(_) => unreachable!(),
         ExprF::Var(_) => unreachable!(),
         ExprF::Annot(x, _) => Ret::Thunk(x),
+        ExprF::Assert(_) => Ret::Expr(expr),
         ExprF::Lam(x, t, e) => {
             Ret::Value(Lam(x.into(), TypeThunk::from_thunk(t), e))
         }
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 2e4642c..297a096 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -60,18 +60,7 @@ fn tck_pi_type(
         }
     };
 
-    let k = match function_check(ka, kb) {
-        Ok(k) => k,
-        Err(()) => {
-            return Err(TypeError::new(
-                ctx,
-                NoDependentTypes(
-                    tx.to_normalized(),
-                    te.get_type()?.to_normalized(),
-                ),
-            ))
-        }
-    };
+    let k = function_check(ka, kb);
 
     Ok(Typed::from_thunk_and_type(
         Value::Pi(x.into(), TypeThunk::from_type(tx), TypeThunk::from_type(te))
@@ -164,14 +153,13 @@ fn tck_union_type(
     ))
 }
 
-fn function_check(a: Const, b: Const) -> Result<Const, ()> {
-    use dhall_syntax::Const::*;
-    match (a, b) {
-        (_, Type) => Ok(Type),
-        (Kind, Kind) => Ok(Kind),
-        (Sort, Sort) => Ok(Sort),
-        (Sort, Kind) => Ok(Sort),
-        _ => Err(()),
+fn function_check(a: Const, b: Const) -> Const {
+    use dhall_syntax::Const::Type;
+    use std::cmp::max;
+    if b == Type {
+        Type
+    } else {
+        max(a, b)
     }
 }
 
@@ -403,6 +391,19 @@ fn type_last_layer(
             );
             Ok(RetTypeOnly(x.get_type()?.into_owned()))
         }
+        Assert(t) => {
+            match t.to_value() {
+                Value::Equivalence(x, y) if x == y => {}
+                Value::Equivalence(x, y) => {
+                    return Err(mkerr(AssertMismatch(
+                        x.to_typed(),
+                        y.to_typed(),
+                    )))
+                }
+                _ => return Err(mkerr(AssertMustTakeEquivalence)),
+            }
+            Ok(RetTypeOnly(t.to_type()))
+        }
         BoolIf(x, y, z) => {
             ensure_equal!(
                 x.get_type()?,
@@ -807,6 +808,24 @@ fn type_last_layer(
 
             Ok(RetTypeOnly(l.get_type()?.into_owned()))
         }
+        BinOp(Equivalence, l, r) => {
+            ensure_simple_type!(
+                l.get_type()?,
+                mkerr(EquivalenceArgumentMustBeTerm(true, l.clone())),
+            );
+            ensure_simple_type!(
+                r.get_type()?,
+                mkerr(EquivalenceArgumentMustBeTerm(false, r.clone())),
+            );
+
+            ensure_equal!(
+                l.get_type()?,
+                r.get_type()?,
+                mkerr(EquivalenceTypeMismatch(r.clone(), l.clone()))
+            );
+
+            Ok(RetTypeOnly(Type::from_const(dhall_syntax::Const::Type)))
+        }
         BinOp(o, l, r) => {
             let t = builtin_to_type(match o {
                 BoolAnd => Bool,
@@ -821,6 +840,7 @@ fn type_last_layer(
                 RecursiveRecordMerge => unreachable!(),
                 RecursiveRecordTypeMerge => unreachable!(),
                 ImportAlt => unreachable!("There should remain no import alternatives in a resolved expression"),
+                Equivalence => unreachable!(),
             })?;
 
             ensure_equal!(
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index 9784eec..15bc97a 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -107,6 +107,7 @@ pub fn run_test(
 
             match feature {
                 Parser => {
+                    // This exercices both parsing and binary decoding
                     // Compare parse/decoded
                     let expected_file_path = base_path + "B.dhallb";
                     let expected_file_path = PathBuf::from(&expected_file_path);