diff options
author | Nadrieril | 2019-08-08 19:33:07 +0200 |
---|---|---|
committer | Nadrieril | 2019-08-08 19:33:07 +0200 |
commit | 071ba528cd8c6a222be345ddec7560bb45cca6be (patch) | |
tree | f5009c70a2082b7085698ca2cdd5a06e503c73c3 /dhall/src/phase/normalize.rs | |
parent | 00c5b497446d5415c36bfda5ebc0413da9d086dd (diff) |
Add support for dependent types
Diffstat (limited to 'dhall/src/phase/normalize.rs')
-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)) } |