diff options
Diffstat (limited to '')
| -rw-r--r-- | dhall/src/phase/normalize.rs | 12 |
1 files changed, 9 insertions, 3 deletions
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)) } |