From cc03ada4e713f145f2eb1bbf0f131a4c5746cf74 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 3 Aug 2019 22:55:51 +0200 Subject: Inline headers --- dhall/src/phase/binary.rs | 29 ++++++++++++++--------------- 1 file changed, 14 insertions(+), 15 deletions(-) (limited to 'dhall/src/phase/binary.rs') diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs index 1812131..874b4fb 100644 --- a/dhall/src/phase/binary.rs +++ b/dhall/src/phase/binary.rs @@ -216,18 +216,19 @@ fn cbor_value_to_dhall( }; let headers = match rest.next() { Some(Null) => None, - Some(x) => { - match cbor_value_to_dhall(&x)?.as_ref() { - Embed(import) => Some(Box::new( - import.location_hashed.clone(), - )), - _ => Err(DecodeError::WrongFormatError( - "import/remote/headers".to_owned(), - ))?, - } - } + // TODO + // Some(x) => { + // match cbor_value_to_dhall(&x)?.as_ref() { + // Embed(import) => Some(Box::new( + // import.location_hashed.clone(), + // )), + // _ => Err(DecodeError::WrongFormatError( + // "import/remote/headers".to_owned(), + // ))?, + // } + // } _ => Err(DecodeError::WrongFormatError( - "import/remote/headers".to_owned(), + "import/remote/headers is unimplemented".to_owned(), ))?, }; let authority = match rest.next() { @@ -378,7 +379,6 @@ enum Serialize<'a> { CBOR(cbor::Value), RecordMap(&'a DupTreeMap), UnionMap(&'a DupTreeMap>), - Import(&'a Import), } macro_rules! count { @@ -566,10 +566,10 @@ where match &url.headers { None => ser_seq.serialize_element(&Null)?, Some(location_hashed) => ser_seq.serialize_element( - &self::Serialize::Import(&Import { + &self::Serialize::Expr(&SubExpr::from_expr_no_note(ExprF::Embed(Import { mode: ImportMode::Code, location_hashed: location_hashed.as_ref().clone(), - }), + }))), )?, }; ser_seq.serialize_element(&url.authority)?; @@ -617,7 +617,6 @@ impl<'a> serde::ser::Serialize for Serialize<'a> { (cbor::Value::String(k.into()), v) })) } - Serialize::Import(import) => serialize_import(ser, import), } } } -- cgit v1.2.3 From 711164a7a24ab832006b72cac162e78cf434861a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 4 Aug 2019 11:11:37 +0200 Subject: Remove old-style optional literals --- dhall/src/phase/binary.rs | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) (limited to 'dhall/src/phase/binary.rs') diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs index 874b4fb..dcf60bb 100644 --- a/dhall/src/phase/binary.rs +++ b/dhall/src/phase/binary.rs @@ -115,18 +115,22 @@ fn cbor_value_to_dhall( .collect::, _>>()?; NEListLit(rest) } - [U64(5), t] => { - let t = cbor_value_to_dhall(&t)?; - OldOptionalLit(None, t) - } [U64(5), Null, x] => { let x = cbor_value_to_dhall(&x)?; SomeLit(x) } + // Old-style optional literals + [U64(5), t] => { + let t = cbor_value_to_dhall(&t)?; + App(rc(ExprF::Builtin(Builtin::OptionalNone)), t) + } [U64(5), t, x] => { let x = cbor_value_to_dhall(&x)?; let t = cbor_value_to_dhall(&t)?; - OldOptionalLit(Some(x), t) + Annot( + rc(SomeLit(x)), + rc(App(rc(ExprF::Builtin(Builtin::Optional)), t)), + ) } [U64(6), x, y] => { let x = cbor_value_to_dhall(&x)?; @@ -460,8 +464,6 @@ where ) } Annot(x, y) => ser_seq!(ser; tag(26), expr(x), expr(y)), - OldOptionalLit(None, t) => ser_seq!(ser; tag(5), expr(t)), - OldOptionalLit(Some(x), t) => ser_seq!(ser; tag(5), expr(t), expr(x)), SomeLit(x) => ser_seq!(ser; tag(5), null(), expr(x)), EmptyListLit(x) => ser_seq!(ser; tag(4), expr(x)), NEListLit(xs) => ser.collect_seq( -- cgit v1.2.3 From 278cd9be7d93bc1eeecde05c964da5b097668016 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 4 Aug 2019 11:15:28 +0200 Subject: rustfmt --- dhall/src/phase/binary.rs | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) (limited to 'dhall/src/phase/binary.rs') diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs index dcf60bb..443af7e 100644 --- a/dhall/src/phase/binary.rs +++ b/dhall/src/phase/binary.rs @@ -232,7 +232,8 @@ fn cbor_value_to_dhall( // } // } _ => Err(DecodeError::WrongFormatError( - "import/remote/headers is unimplemented".to_owned(), + "import/remote/headers is unimplemented" + .to_owned(), ))?, }; let authority = match rest.next() { @@ -567,12 +568,14 @@ where ImportLocation::Remote(url) => { match &url.headers { None => ser_seq.serialize_element(&Null)?, - Some(location_hashed) => ser_seq.serialize_element( - &self::Serialize::Expr(&SubExpr::from_expr_no_note(ExprF::Embed(Import { - mode: ImportMode::Code, - location_hashed: location_hashed.as_ref().clone(), - }))), - )?, + Some(location_hashed) => { + ser_seq.serialize_element(&self::Serialize::Expr( + &SubExpr::from_expr_no_note(ExprF::Embed(Import { + mode: ImportMode::Code, + location_hashed: location_hashed.as_ref().clone(), + })), + ))? + } }; ser_seq.serialize_element(&url.authority)?; for p in &url.path { -- cgit v1.2.3 From 482be29e0f03e10c2469ef80bdd6ac7593207dc5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 6 Aug 2019 20:38:06 +0200 Subject: RFC3986 URLs --- dhall/src/phase/binary.rs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'dhall/src/phase/binary.rs') diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs index 443af7e..bab3fd8 100644 --- a/dhall/src/phase/binary.rs +++ b/dhall/src/phase/binary.rs @@ -195,8 +195,13 @@ fn cbor_value_to_dhall( } [U64(24), hash, U64(mode), U64(scheme), rest..] => { let mode = match mode { + 0 => ImportMode::Code, 1 => ImportMode::RawText, - _ => ImportMode::Code, + 2 => ImportMode::Location, + _ => Err(DecodeError::WrongFormatError(format!( + "import/mode/unknown_mode: {:?}", + mode + )))?, }; let hash = match hash { Null => None, @@ -545,6 +550,7 @@ where let mode = match import.mode { ImportMode::Code => 0, ImportMode::RawText => 1, + ImportMode::Location => 2, }; ser_seq.serialize_element(&U64(mode))?; -- cgit v1.2.3 From 705433487da3cd3b4517fcf74b0497c76dbb4080 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 6 Aug 2019 22:36:43 +0200 Subject: Prepare for https://github.com/dhall-lang/dhall-lang/pull/630 --- dhall/src/phase/binary.rs | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) (limited to 'dhall/src/phase/binary.rs') diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs index bab3fd8..66b235f 100644 --- a/dhall/src/phase/binary.rs +++ b/dhall/src/phase/binary.rs @@ -106,7 +106,7 @@ fn cbor_value_to_dhall( } [U64(4), t] => { let t = cbor_value_to_dhall(&t)?; - EmptyListLit(t) + EmptyListLit(rc(App(rc(ExprF::Builtin(Builtin::List)), t))) } [U64(4), Null, rest..] => { let rest = rest @@ -413,6 +413,7 @@ where S: serde::ser::Serializer, { use cbor::Value::{String, I64, U64}; + use dhall_syntax::Builtin; use dhall_syntax::ExprF::*; use std::iter::once; @@ -471,7 +472,13 @@ where } Annot(x, y) => ser_seq!(ser; tag(26), expr(x), expr(y)), SomeLit(x) => ser_seq!(ser; tag(5), null(), expr(x)), - EmptyListLit(x) => ser_seq!(ser; tag(4), expr(x)), + EmptyListLit(x) => match x.as_ref() { + App(f, a) => match f.as_ref() { + ExprF::Builtin(Builtin::List) => ser_seq!(ser; tag(4), expr(a)), + _ => unreachable!(), + }, + _ => unreachable!(), + }, NEListLit(xs) => ser.collect_seq( once(tag(4)).chain(once(null())).chain(xs.iter().map(expr)), ), -- cgit v1.2.3 From f7b0c6b9c52f65624dc765fb9eaa7d0d94eeae76 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 6 Aug 2019 23:03:01 +0200 Subject: Generalize empty list annotations --- dhall/src/phase/binary.rs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'dhall/src/phase/binary.rs') diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs index 66b235f..f88eee2 100644 --- a/dhall/src/phase/binary.rs +++ b/dhall/src/phase/binary.rs @@ -341,6 +341,10 @@ fn cbor_value_to_dhall( let y = cbor_value_to_dhall(&y)?; Annot(x, y) } + [U64(27), x] => { + let x = cbor_value_to_dhall(&x)?; + EmptyListLit(x) + } _ => Err(DecodeError::WrongFormatError(format!("{:?}", data)))?, }, _ => Err(DecodeError::WrongFormatError(format!("{:?}", data)))?, @@ -475,9 +479,9 @@ where EmptyListLit(x) => match x.as_ref() { App(f, a) => match f.as_ref() { ExprF::Builtin(Builtin::List) => ser_seq!(ser; tag(4), expr(a)), - _ => unreachable!(), + _ => ser_seq!(ser; tag(27), expr(x)), }, - _ => unreachable!(), + _ => ser_seq!(ser; tag(27), expr(x)), }, NEListLit(xs) => ser.collect_seq( once(tag(4)).chain(once(null())).chain(xs.iter().map(expr)), -- cgit v1.2.3 From 98e7751fb8deb22685b6991367404515c35f502f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 7 Aug 2019 16:28:48 +0200 Subject: Various parsing tweaks --- dhall/src/phase/binary.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'dhall/src/phase/binary.rs') diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs index f88eee2..e44b1e2 100644 --- a/dhall/src/phase/binary.rs +++ b/dhall/src/phase/binary.rs @@ -341,7 +341,7 @@ fn cbor_value_to_dhall( let y = cbor_value_to_dhall(&y)?; Annot(x, y) } - [U64(27), x] => { + [U64(28), x] => { let x = cbor_value_to_dhall(&x)?; EmptyListLit(x) } @@ -479,9 +479,9 @@ where EmptyListLit(x) => match x.as_ref() { App(f, a) => match f.as_ref() { ExprF::Builtin(Builtin::List) => ser_seq!(ser; tag(4), expr(a)), - _ => ser_seq!(ser; tag(27), expr(x)), + _ => ser_seq!(ser; tag(28), expr(x)), }, - _ => ser_seq!(ser; tag(27), expr(x)), + _ => ser_seq!(ser; tag(28), expr(x)), }, NEListLit(xs) => ser.collect_seq( once(tag(4)).chain(once(null())).chain(xs.iter().map(expr)), -- cgit v1.2.3 From d248762095908246951b6aa6c211587c6e333c0e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 7 Aug 2019 21:05:01 +0200 Subject: Remove union literals from the language --- dhall/src/phase/binary.rs | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) (limited to 'dhall/src/phase/binary.rs') diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs index e44b1e2..bfe217f 100644 --- a/dhall/src/phase/binary.rs +++ b/dhall/src/phase/binary.rs @@ -160,12 +160,9 @@ fn cbor_value_to_dhall( let map = cbor_map_to_dhall_opt_map(map)?; UnionType(map) } - [U64(12), String(l), x, Object(map)] => { - let map = cbor_map_to_dhall_opt_map(map)?; - let x = cbor_value_to_dhall(&x)?; - let l = Label::from(l.as_str()); - UnionLit(l, x, map) - } + [U64(12), ..] => Err(DecodeError::WrongFormatError( + "Union literals are not supported anymore".to_owned(), + ))?, [U64(14), x, y, z] => { let x = cbor_value_to_dhall(&x)?; let y = cbor_value_to_dhall(&y)?; @@ -496,9 +493,6 @@ where RecordType(map) => ser_seq!(ser; tag(7), RecordMap(map)), RecordLit(map) => ser_seq!(ser; tag(8), RecordMap(map)), UnionType(map) => ser_seq!(ser; tag(11), UnionMap(map)), - UnionLit(l, x, map) => { - ser_seq!(ser; tag(12), label(l), expr(x), UnionMap(map)) - } Field(x, l) => ser_seq!(ser; tag(9), expr(x), label(l)), BinOp(op, x, y) => { use dhall_syntax::BinOp::*; -- cgit v1.2.3 From 6654d441e5741013a8618907773ac54101e3fdf2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 7 Aug 2019 21:38:01 +0200 Subject: Add binary-decode tests --- dhall/src/phase/binary.rs | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) (limited to 'dhall/src/phase/binary.rs') diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs index bfe217f..cab3c8e 100644 --- a/dhall/src/phase/binary.rs +++ b/dhall/src/phase/binary.rs @@ -48,10 +48,21 @@ fn cbor_value_to_dhall( Bool(b) => BoolLit(*b), Array(vec) => match vec.as_slice() { [String(l), U64(n)] => { + if l.as_str() == "_" { + Err(DecodeError::WrongFormatError( + "`_` variable was encoded incorrectly".to_owned(), + ))? + } let l = Label::from(l.as_str()); Var(V(l, *n as usize)) } [U64(0), f, args..] => { + if args.is_empty() { + Err(DecodeError::WrongFormatError( + "Function application must have at least one argument" + .to_owned(), + ))? + } let mut f = cbor_value_to_dhall(&f)?; for a in args { let a = cbor_value_to_dhall(&a)?; @@ -65,6 +76,11 @@ fn cbor_value_to_dhall( Lam(Label::from("_"), x, y) } [U64(1), String(l), x, y] => { + if l.as_str() == "_" { + Err(DecodeError::WrongFormatError( + "`_` variable was encoded incorrectly".to_owned(), + ))? + } let x = cbor_value_to_dhall(&x)?; let y = cbor_value_to_dhall(&y)?; let l = Label::from(l.as_str()); @@ -76,6 +92,11 @@ fn cbor_value_to_dhall( Pi(Label::from("_"), x, y) } [U64(2), String(l), x, y] => { + if l.as_str() == "_" { + Err(DecodeError::WrongFormatError( + "`_` variable was encoded incorrectly".to_owned(), + ))? + } let x = cbor_value_to_dhall(&x)?; let y = cbor_value_to_dhall(&y)?; let l = Label::from(l.as_str()); -- cgit v1.2.3 From c2cb7d38dfec05b6337aa5dcd0dc3068e73c9a58 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 7 Aug 2019 22:25:35 +0200 Subject: Flatten nested let bindings --- dhall/src/phase/binary.rs | 46 ++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 40 insertions(+), 6 deletions(-) (limited to 'dhall/src/phase/binary.rs') diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs index cab3c8e..5e7eb40 100644 --- a/dhall/src/phase/binary.rs +++ b/dhall/src/phase/binary.rs @@ -477,12 +477,23 @@ where ser_seq!(ser; tag(2), expr(x), expr(y)) } Pi(l, x, y) => ser_seq!(ser; tag(2), label(l), expr(x), expr(y)), - // TODO: multilet - Let(l, None, x, y) => { - ser_seq!(ser; tag(25), label(l), null(), expr(x), expr(y)) - } - Let(l, Some(t), x, y) => { - ser_seq!(ser; tag(25), label(l), expr(t), expr(x), expr(y)) + Let(_, _, _, _) => { + let (bound_e, bindings) = collect_nested_lets(e); + let count = 1 + 3 * bindings.len() + 1; + + use serde::ser::SerializeSeq; + let mut ser_seq = ser.serialize_seq(Some(count))?; + ser_seq.serialize_element(&tag(25))?; + for (l, t, v) in bindings { + ser_seq.serialize_element(&label(l))?; + match t { + Some(t) => ser_seq.serialize_element(&expr(t))?, + None => ser_seq.serialize_element(&null())?, + } + ser_seq.serialize_element(&expr(v))?; + } + ser_seq.serialize_element(&expr(bound_e))?; + ser_seq.end() } App(_, _) => { let (f, args) = collect_nested_applications(e); @@ -677,3 +688,26 @@ fn collect_nested_applications<'a, N, E>( let e = go(e, &mut vec); (e, vec) } + +type LetBinding<'a, N, E> = + (&'a Label, &'a Option>, &'a SubExpr); + +fn collect_nested_lets<'a, N, E>( + e: &'a SubExpr, +) -> (&'a SubExpr, Vec>) { + fn go<'a, N, E>( + e: &'a SubExpr, + vec: &mut Vec>, + ) -> &'a SubExpr { + match e.as_ref() { + ExprF::Let(l, t, v, e) => { + vec.push((l, t, v)); + go(e, vec) + } + _ => e, + } + } + let mut vec = vec![]; + let e = go(e, &mut vec); + (e, vec) +} -- cgit v1.2.3 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 From 80c8d87db595c91293af75d710464ac5379c7e28 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 10 Aug 2019 22:48:21 +0200 Subject: Update dhall-lang submodule --- dhall/src/phase/binary.rs | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'dhall/src/phase/binary.rs') diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs index 719b1c7..f4a9cc1 100644 --- a/dhall/src/phase/binary.rs +++ b/dhall/src/phase/binary.rs @@ -178,6 +178,19 @@ fn cbor_value_to_dhall( let l = Label::from(l.as_str()); Field(x, l) } + [U64(10), x, rest..] => { + let x = cbor_value_to_dhall(&x)?; + let labels = rest + .iter() + .map(|s| match s { + String(s) => Ok(Label::from(s.as_str())), + _ => Err(DecodeError::WrongFormatError( + "projection".to_owned(), + )), + }) + .collect::>()?; + Projection(x, labels) + } [U64(11), Object(map)] => { let map = cbor_map_to_dhall_opt_map(map)?; UnionType(map) -- cgit v1.2.3