From 071ba528cd8c6a222be345ddec7560bb45cca6be Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 8 Aug 2019 19:33:07 +0200
Subject: Add support for dependent types

---
 dhall/src/phase/normalize.rs | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

(limited to 'dhall/src/phase/normalize.rs')

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