Add support for dependent types

2 files changed, 22 insertions, 1 deletions

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),
+            ),
         }
     }
 }