summaryrefslogtreecommitdiff
path: root/dhall/src/phase/binary.rs
diff options
context:
space:
mode:
authorNadrieril2019-08-08 19:33:07 +0200
committerNadrieril2019-08-08 19:33:07 +0200
commit071ba528cd8c6a222be345ddec7560bb45cca6be (patch)
treef5009c70a2082b7085698ca2cdd5a06e503c73c3 /dhall/src/phase/binary.rs
parent00c5b497446d5415c36bfda5ebc0413da9d086dd (diff)
Add support for dependent types
Diffstat (limited to '')
-rw-r--r--dhall/src/phase/binary.rs7
1 files changed, 7 insertions, 0 deletions
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::<Result<_, _>>()?,
)))
}
+ [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))
}