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_generated_parser/src/dhall.pest.visibility | 2 -- 1 file changed, 2 deletions(-) (limited to 'dhall_generated_parser/src/dhall.pest.visibility') diff --git a/dhall_generated_parser/src/dhall.pest.visibility b/dhall_generated_parser/src/dhall.pest.visibility index 60de54d..0c48656 100644 --- a/dhall_generated_parser/src/dhall.pest.visibility +++ b/dhall_generated_parser/src/dhall.pest.visibility @@ -134,8 +134,6 @@ import expression annotated_expression let_binding -empty_collection -non_empty_optional # operator_expression import_alt_expression or_expression -- cgit v1.3.1 From e52f50080d8e0e6d6a05b1045e3e0e840acb50d0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 4 Aug 2019 14:07:34 +0200 Subject: Braced escape sequences --- dhall-lang | 2 +- dhall_generated_parser/src/dhall.pest.visibility | 1 + dhall_syntax/src/parser.rs | 28 ++++++++++++++++++++---- 3 files changed, 26 insertions(+), 5 deletions(-) (limited to 'dhall_generated_parser/src/dhall.pest.visibility') diff --git a/dhall-lang b/dhall-lang index 0396b67..dbf4ebc 160000 --- a/dhall-lang +++ b/dhall-lang @@ -1 +1 @@ -Subproject commit 0396b67639a6deaff480844e71b576db998717d3 +Subproject commit dbf4ebcfabf499e87c27e75bec108d91929ccc31 diff --git a/dhall_generated_parser/src/dhall.pest.visibility b/dhall_generated_parser/src/dhall.pest.visibility index 0c48656..2b7c477 100644 --- a/dhall_generated_parser/src/dhall.pest.visibility +++ b/dhall_generated_parser/src/dhall.pest.visibility @@ -21,6 +21,7 @@ label # any_label double_quote_chunk double_quote_escaped +# unicode_escape double_quote_char double_quote_literal single_quote_continue diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs index db1699b..2450c76 100644 --- a/dhall_syntax/src/parser.rs +++ b/dhall_syntax/src/parser.rs @@ -402,11 +402,31 @@ make_parser! { "n" => "\n".to_owned(), "r" => "\r".to_owned(), "t" => "\t".to_owned(), + // "uXXXX" or "u{XXXXX}" _ => { - // "uXXXX" - use std::convert::TryFrom; - let c = u16::from_str_radix(&s[1..5], 16).unwrap(); - let c = char::try_from(u32::from(c)).unwrap(); + use std::convert::{TryFrom, TryInto}; + + let s = &s[1..]; + let s = if &s[0..1] == "{" { + &s[1..s.len()-1] + } else { + &s[0..s.len()] + }; + + if s.len() > 8 { + Err(format!("Escape sequences can't have more than 8 chars: \"{}\"", s))? + } + + // pad with zeroes + let s: String = std::iter::repeat('0') + .take(8 - s.len()) + .chain(s.chars()) + .collect(); + + // `s` has length 8, so `bytes` has length 4 + let bytes: &[u8] = &hex::decode(s).unwrap(); + let c = u32::from_be_bytes(bytes.try_into().unwrap()); + let c = char::try_from(c).unwrap(); std::iter::once(c).collect() } } -- cgit v1.3.1 From 482be29e0f03e10c2469ef80bdd6ac7593207dc5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 6 Aug 2019 20:38:06 +0200 Subject: RFC3986 URLs --- dhall-lang | 2 +- dhall/build.rs | 20 ++++++++++++++++++-- dhall/src/phase/binary.rs | 8 +++++++- dhall_generated_parser/build.rs | 6 ++++++ dhall_generated_parser/src/dhall.pest.visibility | 1 + dhall_syntax/src/core/import.rs | 1 + dhall_syntax/src/parser.rs | 7 +++++++ dhall_syntax/src/printer.rs | 1 + tests_buffer | 1 + 9 files changed, 43 insertions(+), 4 deletions(-) (limited to 'dhall_generated_parser/src/dhall.pest.visibility') diff --git a/dhall-lang b/dhall-lang index e01c734..2c0f238 160000 --- a/dhall-lang +++ b/dhall-lang @@ -1 +1 @@ -Subproject commit e01c734e612daac327b06845e45c34552d65d9e1 +Subproject commit 2c0f2389e11597131b8ce021344322e5ed3a9131 diff --git a/dhall/build.rs b/dhall/build.rs index 7e320c5..cdbd560 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -94,6 +94,12 @@ fn main() -> std::io::Result<()> { || path == "success/recordProjectionByExpression" || path == "success/unit/recordProjectionByExpression" || path == "success/unit/recordProjectionByExpressionEmpty" + // TODO: RFC3986 URLs + || path == "success/unit/import/urls/emptyPath0" + || path == "success/unit/import/urls/emptyPath1" + || path == "success/unit/import/urls/emptyPathSegment" + // Test is broken + || path == "success/unit/import/asLocation" }, )?; @@ -113,6 +119,12 @@ fn main() -> std::io::Result<()> { || path == "success/recordProjectionByExpression" || path == "success/unit/recordProjectionByExpression" || path == "success/unit/recordProjectionByExpressionEmpty" + // TODO: RFC3986 URLs + || path == "success/unit/import/urls/emptyPath0" + || path == "success/unit/import/urls/emptyPath1" + || path == "success/unit/import/urls/emptyPathSegment" + // Test is broken + || path == "success/unit/import/asLocation" }, )?; @@ -137,6 +149,12 @@ fn main() -> std::io::Result<()> { || path == "success/recordProjectionByExpression" || path == "success/unit/recordProjectionByExpression" || path == "success/unit/recordProjectionByExpressionEmpty" + // TODO: RFC3986 URLs + || path == "success/unit/import/urls/emptyPath0" + || path == "success/unit/import/urls/emptyPath1" + || path == "success/unit/import/urls/emptyPathSegment" + // Test is broken + || path == "success/unit/import/asLocation" }, )?; @@ -156,8 +174,6 @@ fn main() -> std::io::Result<()> { || path == "success/unit/RecordProjectionTypeNormalizeProjection" // TODO: fix Double/show || path == "success/prelude/JSON/number/1" - // the test is wrong - || path == "success/prelude/JSON/Type/0" }, )?; 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))?; diff --git a/dhall_generated_parser/build.rs b/dhall_generated_parser/build.rs index 744cb3d..2c1a8f5 100644 --- a/dhall_generated_parser/build.rs +++ b/dhall_generated_parser/build.rs @@ -27,6 +27,7 @@ fn main() -> std::io::Result<()> { } } rules.remove("http"); + rules.remove("url_path"); rules.remove("simple_label"); rules.remove("nonreserved_label"); @@ -53,6 +54,11 @@ fn main() -> std::io::Result<()> { ~ (import_hashed | ^\"(\" ~ whsp ~ import_hashed ~ whsp ~ ^\")\"))? }}" )?; + // TODO: this is a cheat; properly support RFC3986 URLs instead + writeln!( + &mut file, + "url_path = _{{ path }}" + )?; writeln!( &mut file, "nonreserved_label = _{{ diff --git a/dhall_generated_parser/src/dhall.pest.visibility b/dhall_generated_parser/src/dhall.pest.visibility index 2b7c477..97d3a69 100644 --- a/dhall_generated_parser/src/dhall.pest.visibility +++ b/dhall_generated_parser/src/dhall.pest.visibility @@ -48,6 +48,7 @@ builtin Optional Text List +Location # Bool # True # False diff --git a/dhall_syntax/src/core/import.rs b/dhall_syntax/src/core/import.rs index 306460b..d41eae2 100644 --- a/dhall_syntax/src/core/import.rs +++ b/dhall_syntax/src/core/import.rs @@ -41,6 +41,7 @@ pub enum Scheme { pub enum ImportMode { Code, RawText, + Location, } #[derive(Debug, Clone, PartialEq, Eq, Hash)] diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs index 2450c76..2c0cee9 100644 --- a/dhall_syntax/src/parser.rs +++ b/dhall_syntax/src/parser.rs @@ -697,6 +697,7 @@ make_parser! { )); token_rule!(Text<()>); + token_rule!(Location<()>); rule!(import as expression; span; children!( [import_hashed(location_hashed)] => { @@ -711,6 +712,12 @@ make_parser! { location_hashed })) }, + [import_hashed(location_hashed), Location(_)] => { + spanned(span, Embed(Import { + mode: ImportMode::Location, + location_hashed + })) + }, )); token_rule!(lambda<()>); diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs index b585a5b..2b2bbcc 100644 --- a/dhall_syntax/src/printer.rs +++ b/dhall_syntax/src/printer.rs @@ -435,6 +435,7 @@ impl Display for Import { match self.mode { Code => {} RawText => write!(f, " as Text")?, + Location => write!(f, " as Location")?, } Ok(()) } diff --git a/tests_buffer b/tests_buffer index 5234562..ca578e4 100644 --- a/tests_buffer +++ b/tests_buffer @@ -6,6 +6,7 @@ remove `double` remove imports/parenthesizeUsing remove multilet selection by expression unit tests +split aslocation test into actual unit tests success/ imports/ Missing missing -- cgit v1.3.1 From b3791e91b7cb73778cc21844a6999531bf537f77 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 6 Aug 2019 20:59:28 +0200 Subject: Change URL parsing --- dhall-lang | 2 +- dhall/build.rs | 1 + dhall_generated_parser/src/dhall.pest.visibility | 4 +++- 3 files changed, 5 insertions(+), 2 deletions(-) (limited to 'dhall_generated_parser/src/dhall.pest.visibility') diff --git a/dhall-lang b/dhall-lang index 65aa743..40c3e57 160000 --- a/dhall-lang +++ b/dhall-lang @@ -1 +1 @@ -Subproject commit 65aa7435040141dd30d5983695b7ebdb4224b280 +Subproject commit 40c3e57a4f09448b5a7c9d203a81b64f50ed30bd diff --git a/dhall/build.rs b/dhall/build.rs index db66e3c..2fa63c6 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -100,6 +100,7 @@ fn main() -> std::io::Result<()> { || path == "success/unit/import/urls/emptyPath0" || path == "success/unit/import/urls/emptyPath1" || path == "success/unit/import/urls/emptyPathSegment" + || path == "success/unit/import/urls/potPourri" }, )?; diff --git a/dhall_generated_parser/src/dhall.pest.visibility b/dhall_generated_parser/src/dhall.pest.visibility index 97d3a69..24d0a87 100644 --- a/dhall_generated_parser/src/dhall.pest.visibility +++ b/dhall_generated_parser/src/dhall.pest.visibility @@ -10,6 +10,7 @@ # whsp1 # ALPHA # DIGIT +# ALPHANUM # HEXDIG # simple_label_first_char # simple_label_next_char @@ -118,7 +119,8 @@ authority # ls32 # IPv4address # dec_octet -# reg_name +# domain +# domainlabel # pchar query # pct_encoded -- cgit v1.3.1 From 3e157f0a05b0b93753ed377332597a37fa379541 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 6 Aug 2019 21:28:12 +0200 Subject: Add toMap keyword --- dhall-lang | 2 +- dhall/build.rs | 21 +++++++++++++++++++++ dhall_generated_parser/src/dhall.pest.visibility | 1 + dhall_syntax/src/parser.rs | 1 + 4 files changed, 24 insertions(+), 1 deletion(-) (limited to 'dhall_generated_parser/src/dhall.pest.visibility') diff --git a/dhall-lang b/dhall-lang index 40c3e57..cd29db9 160000 --- a/dhall-lang +++ b/dhall-lang @@ -1 +1 @@ -Subproject commit 40c3e57a4f09448b5a7c9d203a81b64f50ed30bd +Subproject commit cd29db992660788fa5d75ccc465562fa3d96fcee diff --git a/dhall/build.rs b/dhall/build.rs index c78f8f9..2d75cbf 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -101,6 +101,8 @@ fn main() -> std::io::Result<()> { || path == "success/unit/import/urls/emptyPath1" || path == "success/unit/import/urls/emptyPathSegment" || path == "success/unit/import/urls/potPourri" + // TODO: toMap + || path == "success/toMap" }, )?; @@ -125,6 +127,8 @@ fn main() -> std::io::Result<()> { || path == "success/unit/import/urls/emptyPath0" || path == "success/unit/import/urls/emptyPath1" || path == "success/unit/import/urls/emptyPathSegment" + // TODO: toMap + || path == "success/toMap" }, )?; @@ -154,6 +158,9 @@ fn main() -> std::io::Result<()> { || path == "success/unit/import/urls/emptyPath0" || path == "success/unit/import/urls/emptyPath1" || path == "success/unit/import/urls/emptyPathSegment" + || path == "success/unit/import/urls/potPourri" + // TODO: toMap + || path == "success/toMap" }, )?; @@ -173,6 +180,10 @@ fn main() -> std::io::Result<()> { || path == "success/unit/RecordProjectionByTypeNormalizeProjection" // TODO: fix Double/show || path == "success/prelude/JSON/number/1" + // TODO: toMap + || path == "success/unit/EmptyToMap" + || path == "success/unit/ToMap" + || path == "success/unit/ToMapWithType" }, )?; @@ -197,6 +208,14 @@ fn main() -> std::io::Result<()> { // TODO: projection by expression || path == "failure/unit/RecordProjectionByTypeFieldTypeMismatch" || path == "failure/unit/RecordProjectionByTypeNotPresent" + // TODO: toMap + || path == "failure/unit/EmptyToMap" + || path == "failure/unit/HeterogenousToMap" + || path == "failure/unit/MistypedToMap1" + || path == "failure/unit/MistypedToMap2" + || path == "failure/unit/MistypedToMap3" + || path == "failure/unit/MistypedToMap4" + || path == "failure/unit/NonRecordToMap" }, )?; @@ -211,6 +230,8 @@ fn main() -> std::io::Result<()> { || path == "success/unit/RecordProjectionByType" || path == "success/unit/RecordProjectionByTypeEmpty" || path == "success/unit/RecordProjectionByTypeJudgmentalEquality" + // TODO: toMap + || path == "success/unit/ToMap" }, )?; diff --git a/dhall_generated_parser/src/dhall.pest.visibility b/dhall_generated_parser/src/dhall.pest.visibility index 24d0a87..3142ad5 100644 --- a/dhall_generated_parser/src/dhall.pest.visibility +++ b/dhall_generated_parser/src/dhall.pest.visibility @@ -44,6 +44,7 @@ missing # Infinity NaN Some_ +toMap # keyword builtin Optional diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs index 2c0cee9..8355ebf 100644 --- a/dhall_syntax/src/parser.rs +++ b/dhall_syntax/src/parser.rs @@ -861,6 +861,7 @@ make_parser! { )); token_rule!(Some_<()>); + token_rule!(toMap<()>); rule!(application_expression as expression; children!( [expression(e)] => e, -- cgit v1.3.1 From d5c3e8f2ef7438b7ac84be34cfe019ce365ae529 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 7 Aug 2019 16:22:00 +0200 Subject: Forbid surrogate pairs and non-characters --- dhall-lang | 2 +- dhall/src/tests.rs | 2 ++ dhall_generated_parser/src/dhall.pest.visibility | 1 + dhall_syntax/src/parser.rs | 23 +++++++++++++++++++++-- 4 files changed, 25 insertions(+), 3 deletions(-) (limited to 'dhall_generated_parser/src/dhall.pest.visibility') diff --git a/dhall-lang b/dhall-lang index ee2fe7d..599f83b 160000 --- a/dhall-lang +++ b/dhall-lang @@ -1 +1 @@ -Subproject commit ee2fe7d9cbd699fc9f40ca4858abcc0f13105324 +Subproject commit 599f83b9d5ed24f4357455aecc794f572234a69a diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 2f68dac..8b32fb4 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -195,6 +195,8 @@ pub fn run_test( let err = parse_file_str(&file_path).unwrap_err(); match err { Error::Parse(_) => {} + Error::IO(e) + if e.kind() == std::io::ErrorKind::InvalidData => {} e => panic!("Expected parse error, got: {:?}", e), } } diff --git a/dhall_generated_parser/src/dhall.pest.visibility b/dhall_generated_parser/src/dhall.pest.visibility index 3142ad5..33018ae 100644 --- a/dhall_generated_parser/src/dhall.pest.visibility +++ b/dhall_generated_parser/src/dhall.pest.visibility @@ -1,4 +1,5 @@ # end_of_line +# valid_non_ascii # tab # block_comment # block_comment_char diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs index 5be8477..8336c74 100644 --- a/dhall_syntax/src/parser.rs +++ b/dhall_syntax/src/parser.rs @@ -425,8 +425,27 @@ make_parser! { // `s` has length 8, so `bytes` has length 4 let bytes: &[u8] = &hex::decode(s).unwrap(); - let c = u32::from_be_bytes(bytes.try_into().unwrap()); - let c = char::try_from(c).unwrap(); + let i = u32::from_be_bytes(bytes.try_into().unwrap()); + let c = char::try_from(i).unwrap(); + match i { + 0xD800..=0xDFFF => { + let c_ecapsed = c.escape_unicode(); + Err(format!("Escape sequences can't contain surrogate pairs: \"{}\"", c_ecapsed))? + }, + 0x0FFFE..=0x0FFFF | 0x1FFFE..=0x1FFFF | + 0x2FFFE..=0x2FFFF | 0x3FFFE..=0x3FFFF | + 0x4FFFE..=0x4FFFF | 0x5FFFE..=0x5FFFF | + 0x6FFFE..=0x6FFFF | 0x7FFFE..=0x7FFFF | + 0x8FFFE..=0x8FFFF | 0x9FFFE..=0x9FFFF | + 0xAFFFE..=0xAFFFF | 0xBFFFE..=0xBFFFF | + 0xCFFFE..=0xCFFFF | 0xDFFFE..=0xDFFFF | + 0xEFFFE..=0xEFFFF | 0xFFFFE..=0xFFFFF | + 0x10FFFE..=0x10FFFF => { + let c_ecapsed = c.escape_unicode(); + Err(format!("Escape sequences can't contain non-characters: \"{}\"", c_ecapsed))? + }, + _ => {} + } std::iter::once(c).collect() } } -- cgit v1.3.1 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-lang | 2 +- dhall/src/core/value.rs | 15 ++----- dhall/src/phase/binary.rs | 12 ++---- dhall/src/phase/normalize.rs | 7 ---- dhall/src/phase/typecheck.rs | 9 ----- dhall_generated_parser/src/dhall.pest.visibility | 6 +-- dhall_syntax/src/core/expr.rs | 2 - dhall_syntax/src/core/visitor.rs | 3 -- dhall_syntax/src/parser.rs | 51 ++---------------------- dhall_syntax/src/printer.rs | 10 ----- 10 files changed, 12 insertions(+), 105 deletions(-) (limited to 'dhall_generated_parser/src/dhall.pest.visibility') diff --git a/dhall-lang b/dhall-lang index 95cfb88..f692f70 160000 --- a/dhall-lang +++ b/dhall-lang @@ -1 +1 @@ -Subproject commit 95cfb88db2f79b3c4bf61c76d9e9869d149cdefd +Subproject commit f692f70bafa0322da5d9c4b535b2d323a9c5ac61 diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index f47f1b2..d7b9149 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -178,19 +178,10 @@ impl Value { .collect(); rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone())) } - Value::UnionLit(l, v, kts) => rc(ExprF::UnionLit( - l.clone(), + Value::UnionLit(l, v, kts) => rc(ExprF::App( + Value::UnionConstructor(l.clone(), kts.clone()) + .normalize_to_expr_maybe_alpha(alpha), v.normalize_to_expr_maybe_alpha(alpha), - kts.iter() - .map(|(k, v)| { - ( - k.clone(), - v.as_ref().map(|v| { - v.normalize_to_expr_maybe_alpha(alpha) - }), - ) - }) - .collect(), )), Value::TextLit(elts) => { use InterpolatedTextContents::{Expr, Text}; 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::*; diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index 2e9f258..3e45240 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -677,13 +677,6 @@ pub fn normalize_one_layer(expr: ExprF) -> Value { .map(|(k, t)| (k, TypeThunk::from_thunk(t))) .collect(), )), - ExprF::UnionLit(l, x, kts) => Ret::Value(UnionLit( - l, - x, - kts.into_iter() - .map(|(k, t)| (k, t.map(|t| TypeThunk::from_thunk(t)))) - .collect(), - )), ExprF::UnionType(kts) => Ret::Value(UnionType( kts.into_iter() .map(|(k, t)| (k, t.map(|t| TypeThunk::from_thunk(t)))) diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 35bf3a9..4b3a03f 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -505,15 +505,6 @@ fn type_last_layer( )? .into_type(), )), - UnionLit(x, v, kvs) => { - use std::iter::once; - let kts = kvs - .iter() - .map(|(x, v)| Ok((x.clone(), v.as_ref().map(|v| v.to_type())))); - let t = v.get_type()?.into_owned(); - let kts = kts.chain(once(Ok((x.clone(), Some(t))))); - Ok(RetTypeOnly(tck_union_type(ctx, kts)?.to_type())) - } Field(r, x) => { match &r.get_type()?.to_value() { Value::RecordType(kts) => match kts.get(&x) { diff --git a/dhall_generated_parser/src/dhall.pest.visibility b/dhall_generated_parser/src/dhall.pest.visibility index 33018ae..dd54578 100644 --- a/dhall_generated_parser/src/dhall.pest.visibility +++ b/dhall_generated_parser/src/dhall.pest.visibility @@ -169,11 +169,9 @@ non_empty_record_type record_type_entry non_empty_record_literal record_literal_entry -union_type_or_literal +union_type empty_union_type -non_empty_union_type_or_literal -union_literal_variant_value +# non_empty_union_type union_type_entry -union_type_or_literal_variant_type non_empty_list_literal # complete_expression diff --git a/dhall_syntax/src/core/expr.rs b/dhall_syntax/src/core/expr.rs index 668ab45..aab4b6a 100644 --- a/dhall_syntax/src/core/expr.rs +++ b/dhall_syntax/src/core/expr.rs @@ -202,8 +202,6 @@ pub enum ExprF { RecordLit(DupTreeMap), /// `< k1 : t1, k2 >` UnionType(DupTreeMap>), - /// `< k1 = t1, k2 : t2, k3 >` - UnionLit(Label, SubExpr, DupTreeMap>), /// `merge x y : t` Merge(SubExpr, SubExpr, Option), /// `e.x` diff --git a/dhall_syntax/src/core/visitor.rs b/dhall_syntax/src/core/visitor.rs index b02544f..68ad956 100644 --- a/dhall_syntax/src/core/visitor.rs +++ b/dhall_syntax/src/core/visitor.rs @@ -141,9 +141,6 @@ where RecordType(kts) => RecordType(dupmap(kts, v)?), RecordLit(kvs) => RecordLit(dupmap(kvs, v)?), UnionType(kts) => UnionType(optdupmap(kts, v)?), - UnionLit(k, x, kts) => { - UnionLit(k.clone(), v.visit_subexpr(x)?, optdupmap(kts, v)?) - } Merge(x, y, t) => Merge( v.visit_subexpr(x)?, v.visit_subexpr(y)?, diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs index 8336c74..a7f419a 100644 --- a/dhall_syntax/src/parser.rs +++ b/dhall_syntax/src/parser.rs @@ -976,67 +976,22 @@ make_parser! { [label(name), expression(expr)] => (name, expr) )); - rule!(union_type_or_literal as expression; span; children!( + rule!(union_type as expression; span; children!( [empty_union_type(_)] => { spanned(span, UnionType(Default::default())) }, - [non_empty_union_type_or_literal((Some((l, e)), entries))] => { - spanned(span, UnionLit(l, e, entries)) - }, - [non_empty_union_type_or_literal((None, entries))] => { - spanned(span, UnionType(entries)) + [union_type_entry(entries)..] => { + spanned(span, UnionType(entries.collect())) }, )); token_rule!(empty_union_type<()>); - rule!(non_empty_union_type_or_literal - <(Option<(Label, ParsedSubExpr)>, - DupTreeMap>)>; - children!( - [label(l), union_literal_variant_value((e, entries))] => { - (Some((l, e)), entries) - }, - [label(l), union_type_or_literal_variant_type((e, rest))] => { - let (x, mut entries) = rest; - entries.insert(l, e); - (x, entries) - }, - )); - - rule!(union_literal_variant_value - <(ParsedSubExpr, DupTreeMap>)>; - children!( - [expression(e), union_type_entry(entries)..] => { - (e, entries.collect()) - }, - )); - rule!(union_type_entry<(Label, Option)>; children!( [label(name), expression(expr)] => (name, Some(expr)), [label(name)] => (name, None), )); - // TODO: unary union variants - rule!(union_type_or_literal_variant_type - <(Option, - (Option<(Label, ParsedSubExpr)>, - DupTreeMap>))>; - children!( - [expression(e), non_empty_union_type_or_literal(rest)] => { - (Some(e), rest) - }, - [expression(e)] => { - (Some(e), (None, Default::default())) - }, - [non_empty_union_type_or_literal(rest)] => { - (None, rest) - }, - [] => { - (None, (None, Default::default())) - }, - )); - rule!(non_empty_list_literal as expression; span; children!( [expression(items)..] => spanned( diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs index 52d3d81..db688bd 100644 --- a/dhall_syntax/src/printer.rs +++ b/dhall_syntax/src/printer.rs @@ -85,16 +85,6 @@ impl Display for ExprF { } Ok(()) })?, - UnionLit(a, b, c) => { - write!(f, "< {} = {}", a, b)?; - for (k, v) in c { - write!(f, " | {}", k)?; - if let Some(v) = v { - write!(f, ": {}", v)?; - } - } - f.write_str(" >")? - } Embed(a) => a.fmt(f)?, } Ok(()) -- cgit v1.3.1 From 51c4f79fe092191d670ffa2f9098693079dbc1be Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 7 Aug 2019 21:18:11 +0200 Subject: Add truncated Natural subtraction --- dhall-lang | 2 +- dhall/src/phase/normalize.rs | 10 ++++++++++ dhall/src/phase/typecheck.rs | 1 + dhall_generated_parser/src/dhall.pest.visibility | 1 + dhall_syntax/src/core/expr.rs | 1 + dhall_syntax/src/parser.rs | 1 + dhall_syntax/src/printer.rs | 1 + 7 files changed, 16 insertions(+), 1 deletion(-) (limited to 'dhall_generated_parser/src/dhall.pest.visibility') diff --git a/dhall-lang b/dhall-lang index f692f70..c7082d9 160000 --- a/dhall-lang +++ b/dhall-lang @@ -1 +1 @@ -Subproject commit f692f70bafa0322da5d9c4b535b2d323a9c5ac61 +Subproject commit c7082d910d956bcedfdc51daae989659a2db67bd diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index 3e45240..395cf28 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -47,6 +47,16 @@ pub fn apply_builtin(b: Builtin, args: Vec) -> Value { )), _ => Err(()), }, + (NaturalSubtract, [a, b, r..]) => { + match (&*a.as_value(), &*b.as_value()) { + (NaturalLit(a), NaturalLit(b)) => { + Ok((r, NaturalLit(if b > a { b - a } else { 0 }))) + } + (NaturalLit(0), b) => Ok((r, b.clone())), + (_, NaturalLit(0)) => Ok((r, NaturalLit(0))), + _ => Err(()), + } + } (IntegerShow, [n, r..]) => match &*n.as_value() { IntegerLit(n) => { let s = if *n < 0 { diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 4b3a03f..2e4642c 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -212,6 +212,7 @@ fn type_of_builtin(b: Builtin) -> Expr { ), NaturalToInteger => dhall::expr!(Natural -> Integer), NaturalShow => dhall::expr!(Natural -> Text), + NaturalSubtract => dhall::expr!(Natural -> Natural -> Natural), IntegerToDouble => dhall::expr!(Integer -> Double), IntegerShow => dhall::expr!(Integer -> Text), diff --git a/dhall_generated_parser/src/dhall.pest.visibility b/dhall_generated_parser/src/dhall.pest.visibility index dd54578..de6dc8d 100644 --- a/dhall_generated_parser/src/dhall.pest.visibility +++ b/dhall_generated_parser/src/dhall.pest.visibility @@ -71,6 +71,7 @@ Location # Natural_show # Integer_toDouble # Integer_show +# Natural_subtract # Double_show # List_build # List_fold diff --git a/dhall_syntax/src/core/expr.rs b/dhall_syntax/src/core/expr.rs index aab4b6a..b293357 100644 --- a/dhall_syntax/src/core/expr.rs +++ b/dhall_syntax/src/core/expr.rs @@ -119,6 +119,7 @@ pub enum Builtin { NaturalOdd, NaturalToInteger, NaturalShow, + NaturalSubtract, IntegerToDouble, IntegerShow, DoubleShow, diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs index a7f419a..72dfcdd 100644 --- a/dhall_syntax/src/parser.rs +++ b/dhall_syntax/src/parser.rs @@ -80,6 +80,7 @@ impl crate::Builtin { "Natural/odd" => Some(NaturalOdd), "Natural/toInteger" => Some(NaturalToInteger), "Natural/show" => Some(NaturalShow), + "Natural/subtract" => Some(NaturalSubtract), "Integer/toDouble" => Some(IntegerToDouble), "Integer/show" => Some(IntegerShow), "Double/show" => Some(DoubleShow), diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs index db688bd..1d6c113 100644 --- a/dhall_syntax/src/printer.rs +++ b/dhall_syntax/src/printer.rs @@ -449,6 +449,7 @@ impl Display for Builtin { NaturalOdd => "Natural/odd", NaturalToInteger => "Natural/toInteger", NaturalShow => "Natural/show", + NaturalSubtract => "Natural/subtract", IntegerToDouble => "Integer/toDouble", IntegerShow => "Integer/show", DoubleShow => "Double/show", -- cgit v1.3.1