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/binary.rs | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'dhall/src/phase/binary.rs') 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::>()?, ))) } + [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)) } -- cgit v1.2.3