diff --git a/ci/sembr/Cargo.lock b/ci/sembr/Cargo.lock index 36a50dec5a..3436c860a7 100644 --- a/ci/sembr/Cargo.lock +++ b/ci/sembr/Cargo.lock @@ -4,18 +4,18 @@ version = 4 [[package]] name = "aho-corasick" -version = "1.1.4" +version = "1.1.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ddd31a130427c27518df266943a5308ed92d4b226cc639f5a8f1002816174301" +checksum = "c982642fa9e8606056828ee9a8505737230110bb1099153c79efe865c59d12ba" dependencies = [ "memchr", ] [[package]] name = "anstream" -version = "0.6.21" +version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "43d5b281e737544384e969a5ccad3f1cdd24b48086a0fc1b2a5262a26b8f4f4a" +checksum = "824a212faf96e9acacdbd09febd34438f8f711fb84e09a8916013cd7815ca28d" dependencies = [ "anstyle", "anstyle-parse", @@ -28,15 +28,15 @@ dependencies = [ [[package]] name = "anstyle" -version = "1.0.13" +version = "1.0.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5192cca8006f1fd4f7237516f40fa183bb07f8fbdfedaa0036de5ea9b0b45e78" +checksum = "940b3a0ca603d1eade50a4846a2afffd5ef57a9feac2c0e2ec2e14f9ead76000" [[package]] name = "anstyle-parse" -version = "0.2.7" +version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4e7644824f0aa2c7b9384579234ef10eb7efb6a0deb83f9630a49594dd9c15c2" +checksum = "52ce7f38b242319f7cabaa6813055467063ecdc9d355bbb4ce0c68908cd8130e" dependencies = [ "utf8parse", ] @@ -63,25 +63,25 @@ dependencies = [ [[package]] name = "anyhow" -version = "1.0.100" +version = "1.0.104" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a23eb6b1614318a8071c9b2521f36b424b2c83db5eb3a0fead4a6c0809af6e61" +checksum = "330a5ed07fa54e4702c9d6c4174f74427fc0ef6e214bbd677ae50a5099946470" [[package]] name = "bstr" -version = "1.12.1" +version = "1.13.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "63044e1ae8e69f3b5a92c736ca6269b8d12fa7efe39bf34ddb06d102cf0e2cab" +checksum = "6bb31b46c14244e20ee9984b11bf5c992b91fb6939fea616e3512c8baecdbe5f" dependencies = [ "memchr", - "serde", + "serde_core", ] [[package]] name = "clap" -version = "4.5.51" +version = "4.6.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4c26d721170e0295f191a69bd9a1f93efcdb0aff38684b61ab5750468972e5f5" +checksum = "473c7e07f409a8d772161724aa8db6a765a2532a70f9667eeb7b49d3d02fbdca" dependencies = [ "clap_builder", "clap_derive", @@ -89,9 +89,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.5.51" +version = "4.6.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "75835f0c7bf681bfd05abe44e965760fea999a5286c6eb2d59883634fd02011a" +checksum = "7b48fea5a88e9ae728a2dcbedbfc0e730f7d60da42e1cb049a83c9fb8b789889" dependencies = [ "anstream", "anstyle", @@ -101,9 +101,9 @@ dependencies = [ [[package]] name = "clap_derive" -version = "4.5.49" +version = "4.6.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2a0b5487afeab2deb2ff4e03a807ad1a03ac532ff5a2cee5d86884440c7f7671" +checksum = "d012d2b9d65aca7f18f4d9878a045bc17899bba951561ba5ec3c2ba1eed9a061" dependencies = [ "heck", "proc-macro2", @@ -113,21 +113,21 @@ dependencies = [ [[package]] name = "clap_lex" -version = "0.7.6" +version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a1d728cc89cf3aee9ff92b05e62b19ee65a02b5702cff7d5a377e32c6ae29d8d" +checksum = "c8d4a3bb8b1e0c1050499d1815f5ab16d04f0959b233085fb31653fbfc9d98f9" [[package]] name = "colorchoice" -version = "1.0.4" +version = "1.0.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b05b61dc5112cbb17e4b6cd61790d9845d13888356391624cbe7e41efeac1e75" +checksum = "1d07550c9036bf2ae0c684c4297d503f838287c83c53686d05370d0e139ae570" [[package]] name = "crossbeam-deque" -version = "0.8.6" +version = "0.8.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9dd111b7b7f7d55b72c0a6ae361660ee5853c9af73f70c3c2ef6858b950e2e51" +checksum = "5181e0de7b61eb03a81e347d6dd8797bae9da5146707b51077e2d71a54ec0ceb" dependencies = [ "crossbeam-epoch", "crossbeam-utils", @@ -135,24 +135,24 @@ dependencies = [ [[package]] name = "crossbeam-epoch" -version = "0.9.18" +version = "0.9.20" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5b82ac4a3c2ca9c3460964f020e1402edd5753411d7737aa39c3714ad1b5420e" +checksum = "2d6914041f254d6e9176c01941b21115dcfb7089e55135a35411081bd106ef3f" dependencies = [ "crossbeam-utils", ] [[package]] name = "crossbeam-utils" -version = "0.8.21" +version = "0.8.22" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d0a5c400df2834b80a4c3327b3aad3a4c4cd4de0629063962b03235697506a28" +checksum = "61803da095bee82a81bb1a452ecc25d3b2f1416d1897eb86430c6159ef717c17" [[package]] name = "globset" -version = "0.4.18" +version = "0.4.20" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "52dfc19153a48bde0cbd630453615c8151bce3a5adfac7a0aebfbf0a1e1f57e3" +checksum = "07c34a9410465b45bd9787443bc7370f37735bad04b0f0cd57ff1a3186c98988" dependencies = [ "aho-corasick", "bstr", @@ -169,9 +169,9 @@ checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" [[package]] name = "ignore" -version = "0.4.25" +version = "0.4.33" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d3d782a365a015e0f5c04902246139249abf769125006fbe7649e2ee88169b4a" +checksum = "00b69833ed729dc5aa7d19541d96d6cf8e9137194207a04916d658e43168402f" dependencies = [ "crossbeam-deque", "globset", @@ -191,15 +191,15 @@ checksum = "a6cb138bb79a146c1bd460005623e142ef0181e3d0219cb493e02f7d08a35695" [[package]] name = "log" -version = "0.4.28" +version = "0.4.34" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "34080505efa8e45a4b816c349525ebe327ceaa8559756f0356cba97ef3bf7432" +checksum = "f9f8bd3e56ce4dfc153cf470fffbfa98c7620958b312ca5c3a4b8d5181fd13c6" [[package]] name = "memchr" -version = "2.7.6" +version = "2.8.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f52b00d39961fc5b2736ea853c9cc86238e165017a493d1d5c8eac6bdc4cc273" +checksum = "cf8baf1c55e62ffcace7a9f06f4bd9cd3f0c4beb022d3b367256b91b87513d98" [[package]] name = "once_cell_polyfill" @@ -209,27 +209,27 @@ checksum = "384b8ab6d37215f3c5301a95a4accb5d64aa607f1fcb26a11b5303878451b4fe" [[package]] name = "proc-macro2" -version = "1.0.103" +version = "1.0.107" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5ee95bc4ef87b8d5ba32e8b7714ccc834865276eab0aed5c9958d00ec45f49e8" +checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9" dependencies = [ "unicode-ident", ] [[package]] name = "quote" -version = "1.0.42" +version = "1.0.47" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a338cc41d27e6cc6dce6cefc13a0729dfbb81c262b1f519331575dd80ef3067f" +checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001" dependencies = [ "proc-macro2", ] [[package]] name = "regex" -version = "1.12.2" +version = "1.13.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "843bc0191f75f3e22651ae5f1e72939ab2f72a4bc30fa80a066bd66edefc24d4" +checksum = "f020237b6c8eed93db2e2cb53c00c60a8e1bc73da7d073199a1180401450218d" dependencies = [ "aho-corasick", "memchr", @@ -239,9 +239,9 @@ dependencies = [ [[package]] name = "regex-automata" -version = "0.4.13" +version = "0.4.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5276caf25ac86c8d810222b3dbb938e512c55c6831a10f3e6ed1c93b84041f1c" +checksum = "ad8553b9b26413251cbf30e620595c7a41b3887f03da04579c0e6b0d6a06b4b2" dependencies = [ "aho-corasick", "memchr", @@ -250,9 +250,9 @@ dependencies = [ [[package]] name = "regex-syntax" -version = "0.8.8" +version = "0.8.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7a2d987857b319362043e95f5353c0535c1f58eec5336fdfcf626430af7def58" +checksum = "d6f6ff9a378485b298a5286656da665ba74413d36db0979633275d2e708145d4" [[package]] name = "same-file" @@ -273,29 +273,20 @@ dependencies = [ "regex", ] -[[package]] -name = "serde" -version = "1.0.228" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9a8e94ea7f378bd32cbbd37198a4a91436180c5bb472411e48b5ec2e2124ae9e" -dependencies = [ - "serde_core", -] - [[package]] name = "serde_core" -version = "1.0.228" +version = "1.0.229" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "41d385c7d4ca58e59fc732af25c3983b67ac852c1a25000afe1175de458b67ad" +checksum = "67dca2c9c51e58a4791a4b1ed58308b39c64224d349a935ab5039aa360942a48" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.228" +version = "1.0.229" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d540f220d3187173da220f885ab66608367b6574e925011a9353e4badda91d79" +checksum = "e7a5d71263a5a7d47b41f6b3f06ba276f10cc18b0931f1799f710578e2309348" dependencies = [ "proc-macro2", "quote", @@ -310,9 +301,9 @@ checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f" [[package]] name = "syn" -version = "2.0.110" +version = "3.0.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a99801b5bd34ede4cf3fc688c5919368fea4e4814a4664359503e6015b280aea" +checksum = "e6275cddf4610d1775e6d1fe9469b2e77d0f39fd98fb7450901b821e0c53649f" dependencies = [ "proc-macro2", "quote", @@ -321,9 +312,9 @@ dependencies = [ [[package]] name = "unicode-ident" -version = "1.0.22" +version = "1.0.24" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9312f7c4f6ff9069b165498234ce8be658059c6728633667c526e27dc2cf1df5" +checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" [[package]] name = "utf8parse" diff --git a/ci/sembr/src/main.rs b/ci/sembr/src/main.rs index 954c1536e3..83094681e9 100644 --- a/ci/sembr/src/main.rs +++ b/ci/sembr/src/main.rs @@ -11,8 +11,8 @@ use regex::Regex; struct Cli { /// File or directory to check path: PathBuf, - #[arg(long)] /// Modify files that do not comply + #[arg(long)] overwrite: bool, /// Applies to lines that are to be split #[arg(long, default_value_t = 100)] @@ -40,22 +40,19 @@ fn main() -> Result<()> { continue; } let path = entry.into_path(); - if let Some(extension) = path.extension() { - if extension != "md" { - continue; - } - let old = fs::read_to_string(&path)?; - let new = comply(&old); - if new == old { - compliant.push(path.clone()); - } else { - if cli.overwrite { - fs::write(&path, lengthen_lines(&new, cli.line_length_limit))?; - made_compliant.push(path.clone()); - } else { - not_compliant.push(path.clone()); - } - } + let Some(extension) = path.extension() else { continue }; + if extension != "md" { + continue; + } + let old = fs::read_to_string(&path)?; + let new = comply(&old); + if new == old { + compliant.push(path.clone()); + } else if cli.overwrite { + fs::write(&path, lengthen_lines(&new, cli.line_length_limit))?; + made_compliant.push(path.clone()); + } else { + not_compliant.push(path.clone()); } } if !compliant.is_empty() { @@ -78,8 +75,8 @@ fn display(header: &str, paths: &[PathBuf]) { } } -fn ignore(line: &str, in_code_block: bool) -> bool { - in_code_block +fn ignore(line: &str) -> bool { + REGEX_IGNORE_LINK_TARGETS.is_match(line) || line.to_lowercase().contains("e.g.") || line.to_lowercase().contains("n.b.") || line.contains(" etc.") @@ -91,7 +88,6 @@ fn ignore(line: &str, in_code_block: bool) -> bool { || line.trim_start().starts_with('>') || line.starts_with('#') || line.trim().is_empty() - || REGEX_IGNORE_LINK_TARGETS.is_match(line) } fn comply(content: &str) -> String { @@ -107,7 +103,7 @@ fn comply(content: &str) -> String { in_code_block = !in_code_block; continue; } - if ignore(&line, in_code_block) { + if in_code_block || ignore(&line) { continue; } if REGEX_SPLIT.is_match(&line) { @@ -150,21 +146,24 @@ fn lengthen_lines(content: &str, limit: usize) -> String { in_code_block = !in_code_block; continue; } - if line.trim_start().starts_with("") { in_html_div = false; continue; } + if line.trim_start().starts_with("") { continue; } - if ignore(line, in_code_block) || REGEX_SPLIT.is_match(line) { + if ignore(line) || REGEX_SPLIT.is_match(line) { continue; } let Some(next_line) = content.get(n + 1) else { @@ -173,7 +172,7 @@ fn lengthen_lines(content: &str, limit: usize) -> String { if next_line.trim_start().starts_with("```") { continue; } - if ignore(next_line, in_code_block) + if ignore(next_line) || REGEX_LIST_ENTRY.is_match(next_line) || REGEX_IGNORE_END.is_match(line) { @@ -257,6 +256,7 @@ short sentences
a bit of text inside
+
preserve next line 1. one @@ -288,6 +288,7 @@ do not split short sentences
a bit of text inside
+
preserve next line 1. one @@ -322,3 +323,17 @@ fn should_pass() { let original = "if you see `input isn't interesting! verify interesting-ness test`."; assert_eq!(original, comply(original)); } + +#[test] +#[ignore] +fn split_on_comma() { + let original = " +Because of canonicalization of regions and +inference variables, encountering a cycle doesn't mean that we would get an infinite proof tree. +"; + let expected = " +Because of canonicalization of regions and inference variables, +encountering a cycle doesn't mean that we would get an infinite proof tree. +"; + assert_eq!(expected, lengthen_lines(original, 100)) +} diff --git a/src/borrow-check/type-check.md b/src/borrow-check/type-check.md index edf8dd1ba1..2c1058a138 100644 --- a/src/borrow-check/type-check.md +++ b/src/borrow-check/type-check.md @@ -2,15 +2,21 @@ -"Canonical" type checking (ignoring lifetimes) for Rust happens in the HIR. Despite this, we also do a [type checking pass in MIR][type_check]. +"Canonical" type checking (ignoring lifetimes) for Rust happens in the HIR. +Despite this, we also do a [type checking pass in MIR][type_check]. -The MIR is our fully-typed intermediate representation, the types of all items and the contents of their bodies are known by this point and by constructing the MIR we know its types are correct. The reason to do a type checking pass on this already-typed, already-checked IR is to accumulate information about lifetimes[^lifetimes] for borrow checking. See: [`borrowck_collect_region_constraints`][borrowck_collect_region_constraints]. +The MIR is our fully-typed intermediate representation, the types of all items and the contents of their bodies are known by this point and by constructing the MIR we know its types are correct. +The reason to do a type checking pass on this already-typed, already-checked IR is to accumulate information about lifetimes[^lifetimes] for borrow checking. +See: [`borrowck_collect_region_constraints`][borrowck_collect_region_constraints]. [^lifetimes]: AKA regions AKA loans. -Doing this additional type checking pass on it also allows us to check our working: If something fails in MIR type checking that passed in HIR type checking, something has gone wrong. +Doing this additional type checking pass on it also allows us to check our working: +If something fails in MIR type checking that passed in HIR type checking, something has gone wrong. -Maintaining "MIR type checking should succeed if HIR type checking succeeds" is nontrivial. One major reason for this is that type checking MIR involves erasing the existing lifetimes and replacing them with new unconstrained lifetime variables, while in HIR lifetimes get inferred but not checked. In this way, HIR type checking and MIR type checking each work with subtly different information. +Maintaining "MIR type checking should succeed if HIR type checking succeeds" is nontrivial. +One major reason for this is that type checking MIR involves erasing the existing lifetimes and replacing them with new unconstrained lifetime variables, while in HIR lifetimes get inferred but not checked. +In this way, HIR type checking and MIR type checking each work with subtly different information. The erase-and-re-infer strategy in MIR is called [Region Uniquification](#region-uniquification). @@ -49,7 +55,8 @@ We replace all inference variables with existential bound variables instead. Something like `let x: Vec<_>` would therefore result in `exists UserType::Ty(Vec)`. A pattern like `let Foo(x): Foo<&'a u32>` has a user type `Foo<&'a u32>` but -the actual type of `x` should only be `&'a u32`. For this, we use a [`UserTypeProjection`][proj]. +the actual type of `x` should only be `&'a u32`. +For this, we use a [`UserTypeProjection`][proj]. In the MIR, we deal with user types in two slightly different ways. @@ -62,15 +69,15 @@ Here `T_x` only has to be a subtype of the user type, so we instead use [`StatementKind::AscribeUserType`][stmt] for that. Note that we do not directly use the user type as the MIR typechecker -doesn't really deal with type and const inference variables. We instead store the final -[`inferred_type`][inf] from the HIR type-checker. During MIR typeck, we then replace its regions -with new nll inference vars and relate it with the actual `UserType` to get the correct region -constraints again. +doesn't really deal with type and const inference variables. +We instead store the final [`inferred_type`][inf] from the HIR type-checker. +During MIR typeck, we then replace its regions with new nll inference vars +and relate it with the actual `UserType` to get the correct region constraints again. -After the MIR type-check, all user type annotations get discarded, as they aren't needed anymore. +After the MIR type-check, all user type annotations get discarded as they aren't needed anymore. [annot]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/struct.CanonicalUserTypeAnnotation.html [proj]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/struct.UserTypeProjection.html [decl]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/struct.LocalDecl.html [stmt]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.AscribeUserType -[inf]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/struct.CanonicalUserTypeAnnotation.html#structfield.inferred_ty \ No newline at end of file +[inf]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/struct.CanonicalUserTypeAnnotation.html#structfield.inferred_ty diff --git a/src/building/compiler-documenting.md b/src/building/compiler-documenting.md index 2be8f053a9..881f8eaa0c 100644 --- a/src/building/compiler-documenting.md +++ b/src/building/compiler-documenting.md @@ -54,8 +54,8 @@ like the standard library (std) or the compiler (rustc). Documentation improvements are very welcome. The source of `doc.rust-lang.org` is located in [`src/doc`] in the tree, and standard API documentation is generated -from the source code itself (e.g. [`library/std/src/lib.rs`][std-root]). Documentation pull requests -function in the same way as other pull requests. +from the source code itself (e.g. [`library/std/src/lib.rs`][std-root]). +Documentation pull requests function in the same way as other pull requests. [`src/doc`]: https://github.com/rust-lang/rust/tree/HEAD/src/doc [std-root]: https://github.com/rust-lang/rust/blob/HEAD/library/std/src/lib.rs#L1 diff --git a/src/solve/coinduction.md b/src/solve/coinduction.md index b2b71a5afa..8e5a09a6ca 100644 --- a/src/solve/coinduction.md +++ b/src/solve/coinduction.md @@ -13,7 +13,8 @@ Consider the example of `Vec>>: Debug` which results in the followi - `Vec: Debug` - `u32: Debug` -This tree is finite. But not all goals we would want to hold have finite proof trees, +This tree is finite. +But not all goals we would want to hold have finite proof trees, consider the following example: ```rust @@ -36,7 +37,7 @@ This would result in the following proof tree: - `Box>: Send` - ... -This tree would be infinitely large which is exactly what coinduction is about. +This tree would be infinitely large which is exactly what coinduction is about. > To **inductively** prove a goal you need to provide a finite proof tree for it. > To **coinductively** prove a goal the provided proof tree may be infinite. @@ -44,7 +45,8 @@ This tree would be infinitely large which is exactly what coinduction is about. ## Why is coinduction correct When checking whether some trait goals holds, we're asking "does there exist an `impl` -which satisfies this bound". Even if there are infinite chains of nested goals, we still have a +which satisfies this bound". +Even if there are infinite chains of nested goals, we still have a unique `impl` which should be used. ## How to implement coinduction @@ -54,10 +56,12 @@ tree as that would take infinite resources, it still makes sense to think of coi from this perspective. As we cannot check for infinite trees, we instead search for patterns for which we know that -they would result in an infinite proof tree. Currently, the pattern we detect are (canonical) -cycles. If `T: Send` relies on `T: Send` then it's pretty clear that this will just go on forever. +they would result in an infinite proof tree. +Currently, the pattern we detect are (canonical) cycles. +If `T: Send` relies on `T: Send` then it's pretty clear that this will just go on forever. -With cycles we have to be careful with caching. Because of canonicalization of regions and +With cycles we have to be careful with caching. +Because of canonicalization of regions and inference variables, encountering a cycle doesn't mean that we would get an infinite proof tree. Looking at the following example: ```rust @@ -67,18 +71,19 @@ struct Wrapper(T); impl Foo for Wrapper> where Wrapper: Foo -{} +{} ``` Proving `Wrapper: Foo` uses the impl `impl Foo for Wrapper>` which constrains -`?0` to `Wrapper` and then requires `Wrapper: Foo`. Due to canonicalization this would be -detected as a cycle. +`?0` to `Wrapper` and then requires `Wrapper: Foo`. +Due to canonicalization this would be detected as a cycle. The idea to solve is to return a *provisional result* whenever we detect a cycle and repeatedly -retry goals until the *provisional result* is equal to the final result of that goal. We -start out by using `Yes` with no constraints as the result and then update it to the result of +retry goals until the *provisional result* is equal to the final result of that goal. +We start out by using `Yes` with no constraints as the result and then update it to the result of the previous iteration whenever we have to rerun. -TODO: elaborate here. We use the same approach as chalk for coinductive cycles. +TODO: elaborate here. +We use the same approach as chalk for coinductive cycles. Note that the treatment for inductive cycles currently differs by simply returning `Overflow`. See [the relevant chapters][chalk] in the chalk book. @@ -111,10 +116,13 @@ impl Clone for List { } ``` -We are using `tail.clone()` in this impl. For this we have to prove `Box>: Clone` -which requires `List: Clone` but that relies on the impl which we are currently checking. -By adding that requirement to the `where`-clauses of the impl, which is what we would -do with [perfect derive], we move that cycle into the trait solver and [get an error][ex1]. +We are using `tail.clone()` in this impl. +For this, we have to prove `Box>: Clone`, +which requires `List: Clone`. +But that relies on the impl which we are currently checking. +By adding that requirement to the `where`-clauses of the impl, +something we would do with [perfect derive], +we move that cycle into the trait solver and [get an error][ex1]. ### Recursive data types @@ -167,8 +175,9 @@ Our trait system currently treats super traits, e.g. `trait Trait: SuperTrait`, by 1) requiring that `SuperTrait` has to hold for all types which implement `Trait`, and 2) assuming `SuperTrait` holds if `Trait` holds. -Relying on 2) while proving 1) is unsound. This can only be observed in case of -coinductive cycles. Without cycles, whenever we rely on 2) we must have also +Relying on 2) while proving 1) is unsound. +This can only be observed in case of coinductive cycles. +Without cycles, whenever we rely on 2) we must have also proven 1) without relying on 2) for the used impl of `Trait`. ```rust @@ -197,10 +206,11 @@ at least the ideas of myself - @lcnr - are all far to complex to be reasonable. #### `normalizes_to` goals and progress -A `normalizes_to` goal represents the requirement that `::Assoc` normalizes -to some `U`. This is achieved by defacto first normalizing `::Assoc` and then -equating the resulting type with `U`. It should be a mapping as each projection should normalize -to exactly one type. By simply allowing infinite proof trees, we would get the following behavior: +A `normalizes_to` goal represents the requirement that `::Assoc` normalizes to some `U`. +This is achieved by defacto first normalizing `::Assoc` and then +equating the resulting type with `U`. +It should be a mapping as each projection should normalize to exactly one type. +By simply allowing infinite proof trees, we would get the following behavior: ```rust trait Trait { @@ -213,7 +223,8 @@ impl Trait for () { ``` If we now compute `normalizes_to(<() as Trait>::Assoc, Vec)`, we would resolve the impl -and get the associated type `<() as Trait>::Assoc`. We then equate that with the expected type, +and get the associated type `<() as Trait>::Assoc`. +We then equate that with the expected type, causing us to check `normalizes_to(<() as Trait>::Assoc, Vec)` again. This just goes on forever, resulting in an infinite proof tree. @@ -223,14 +234,16 @@ This means that `<() as Trait>::Assoc` would be equal to any other type which is **WARNING: THIS IS SUBTLE AND MIGHT BE WRONG** -Unlike trait goals, `normalizes_to` has to be *productive*[^1]. A `normalizes_to` goal -is productive once the projection normalizes to a rigid type constructor, +Unlike trait goals, `normalizes_to` has to be *productive*[^1]. +A `normalizes_to` goal is productive once the projection normalizes to a rigid type constructor, so `<() as Trait>::Assoc` normalizing to `Vec<<() as Trait>::Assoc>` would be productive. -A `normalizes_to` goal has two kinds of nested goals. Nested requirements needed to actually -normalize the projection, and the equality between the normalized projection and the -expected type. Only the equality has to be productive. A branch in the proof tree is productive -if it is either finite, or contains at least one `normalizes_to` where the alias is resolved +A `normalizes_to` goal has two kinds of nested goals. +Nested requirements needed to actually normalize the projection, +and the equality between the normalized projection and the expected type. +Only the equality has to be productive. +A branch in the proof tree is productive if it is either finite, +or contains at least one `normalizes_to` where the alias is resolved to a rigid type constructor. Alternatively, we could simply always treat the equate branch of `normalizes_to` as inductive. diff --git a/src/solve/the-solver.md b/src/solve/the-solver.md index 35948042f4..0151c0482d 100644 --- a/src/solve/the-solver.md +++ b/src/solve/the-solver.md @@ -1,27 +1,28 @@ # The solver Also consider reading the documentation for [the recursive solver in chalk][chalk] -as it is very similar to this implementation and also talks about limitations of this -approach. +as it is very similar to this implementation and also talks about limitations of this approach. [chalk]: https://rust-lang.github.io/chalk/book/recursive.html ## A rough walkthrough -The entry-point of the solver is `InferCtxtEvalExt::evaluate_root_goal`. This -function sets up the root `EvalCtxt` and then calls `EvalCtxt::evaluate_goal`, +The entry-point of the solver is `InferCtxtEvalExt::evaluate_root_goal`. +This function sets up the root `EvalCtxt` and then calls `EvalCtxt::evaluate_goal`, to actually enter the trait solver. `EvalCtxt::evaluate_goal` handles [canonicalization](./canonicalization.md), caching, -overflow, and solver cycles. Once that is done, it creates a nested `EvalCtxt` with a +overflow, and solver cycles. +Once that is done, it creates a nested `EvalCtxt` with a separate local `InferCtxt` and calls `EvalCtxt::compute_goal`, which is responsible for the -'actual solver behavior'. We match on the `PredicateKind`, delegating to a separate function -for each one. +'actual solver behavior'. +We match on the `PredicateKind`, delegating to a separate function for each one. For trait goals, such a `Vec: Clone`, `EvalCtxt::compute_trait_goal` has to collect all the possible ways this goal can be proven via -`EvalCtxt::assemble_and_evaluate_candidates`. Each candidate is handled in -a separate "probe", to not leak inference constraints to the other candidates. +`EvalCtxt::assemble_and_evaluate_candidates`. +Each candidate is handled in a separate "probe", +to not leak inference constraints to the other candidates. We then try to merge the assembled candidates via `EvalCtxt::merge_candidates`. @@ -30,10 +31,10 @@ We then try to merge the assembled candidates via `EvalCtxt::merge_candidates`. ### `EvalCtxt::add_goal` To prove nested goals, we don't directly call `EvalCtxt::compute_goal`, but instead -add the goal to the `EvalCtxt` with `EvalCtxt::add_goal`. We then prove all nested -goals together in either `EvalCtxt::try_evaluate_added_goals` or -`EvalCtxt::evaluate_added_goals_and_make_canonical_response`. This allows us to handle -inference constraints from later goals. +add the goal to the `EvalCtxt` with `EvalCtxt::add_goal`. +We then prove all nested goals together in either `EvalCtxt::try_evaluate_added_goals` or +`EvalCtxt::evaluate_added_goals_and_make_canonical_response`. +This allows us to handle inference constraints from later goals. E.g. if we have both `?x: Debug` and `(): ConstrainToU8` as nested goals, then proving `?x: Debug` is initially ambiguous, but after proving `(): ConstrainToU8` @@ -42,16 +43,19 @@ we constrain `?x` to `u8` and proving `u8: Debug` succeeds. ### Matching on `TyKind` We lazily normalize types in the solver, so we always have to assume that any types -and constants are potentially unnormalized. This means that matching on `TyKind` can easily -be incorrect. - -We handle normalization in two different ways. When proving `Trait` goals when normalizing -associated types, we separately assemble candidates depending on whether they structurally -match the self type. Candidates which match on the self type are handled in +and constants are potentially unnormalized. +This means that matching on `TyKind` can easily be incorrect. + +We handle normalization in two different ways. +When proving `Trait` goals when normalizing associated types, +we separately assemble candidates depending on whether they structurally +match the self type. +Candidates which match on the self type are handled in `EvalCtxt::assemble_candidates_via_self_ty` which recurses via -`EvalCtxt::assemble_candidates_after_normalizing_self_ty`, which normalizes the self type -by one level. In all other cases we have to match on a `TyKind` we first use -`EvalCtxt::try_normalize_ty` to normalize the type as much as possible. +`EvalCtxt::assemble_candidates_after_normalizing_self_ty`, +which normalizes the self type by one level. +In all other cases where we have to match on a `TyKind`, +we first use `EvalCtxt::try_normalize_ty` to normalize the type as much as possible. ### Higher ranked goals @@ -61,16 +65,19 @@ eagerly instantiates `'a` with a placeholder and then recursively proves ### Dealing with choice -Some goals can be proven in multiple ways. In these cases we try each option in -a separate "probe" and then attempt to merge the resulting responses by using -`EvalCtxt::try_merge_responses`. If merging the responses fails, we use -`EvalCtxt::flounder` instead, returning ambiguity. For some goals, we try to -incompletely prefer some choices over others in case `EvalCtxt::try_merge_responses` -fails. +Some goals can be proven in multiple ways. +In these cases, +we try each option in a separate "probe", +and then attempt to merge the resulting responses by using `EvalCtxt::try_merge_responses`. +If merging the responses fails, we use `EvalCtxt::flounder` instead, returning ambiguity. +For some goals, +we try to incompletely prefer some choices over others +in case `EvalCtxt::try_merge_responses` fails. ## Learning more -The solver should be fairly self-contained. I hope that the above information provides a -good foundation when looking at the code itself. Please reach out on Zulip if you get stuck +The solver should be fairly self-contained. +I hope that the above information provides a good foundation when looking at the code itself. +Please reach out on Zulip if you get stuck while doing so or there are some quirks and design decisions which were unclear and deserve better comments or should be mentioned here. diff --git a/src/the-parser.md b/src/the-parser.md index 601a81e2e4..b81728ab27 100644 --- a/src/the-parser.md +++ b/src/the-parser.md @@ -4,33 +4,33 @@ The very first thing the compiler does is take the program (in UTF-8 Unicode tex and turn it into a data format the compiler can work with more conveniently than strings. This happens in two stages: Lexing and Parsing. - 1. _Lexing_ takes strings and turns them into streams of [tokens]. For - example, `foo.bar + buz` would be turned into the tokens `foo`, `.`, `bar`, - `+`, and `buz`. This is implemented in [`rustc_lexer`][lexer]. + 1. _Lexing_ takes strings and turns them into streams of [tokens]. + For example, `foo.bar + buz` would be turned into the tokens `foo`, `.`, `bar`, + `+`, and `buz`. + This is implemented in [`rustc_lexer`][lexer]. [tokens]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_ast/token/index.html [lexer]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_lexer/index.html 2. _Parsing_ takes streams of tokens and turns them into a structured form which is easier for the compiler to work with, usually called an [*Abstract - Syntax Tree* (AST)][ast] . + Syntax Tree* (AST)][ast]. ## The AST The AST mirrors the structure of a Rust program in memory, using a `Span` to -link a particular AST node back to its source text. The AST is defined in -[`rustc_ast`][rustc_ast], along with some definitions for tokens and token +link a particular AST node back to its source text. +The AST is defined in [`rustc_ast`][rustc_ast], along with some definitions for tokens and token streams, data structures/traits for mutating ASTs, and shared definitions for -other AST-related parts of the compiler (like the lexer and -macro-expansion). +other AST-related parts of the compiler (like the lexer and macro-expansion). Every node in the AST has its own [`NodeId`], including top-level items -such as structs, but also individual statements and expressions. A [`NodeId`] -is an identifier number that uniquely identifies an AST node within a crate. +such as structs, but also individual statements and expressions. +A [`NodeId`] is an identifier number that uniquely identifies an AST node within a crate. However, because they are absolute within a crate, adding or removing a single -node in the AST causes all the subsequent [`NodeId`]s to change. This renders -[`NodeId`]s pretty much useless for incremental compilation, where you want as +node in the AST causes all the subsequent [`NodeId`]s to change. +This renders [`NodeId`]s pretty much useless for incremental compilation, where you want as few things as possible to change. [`NodeId`]s are used in all the `rustc` bits that operate directly on the AST, @@ -41,15 +41,14 @@ like macro expansion and name resolution (more on these over the next couple cha ## Parsing The parser is defined in [`rustc_parse`][rustc_parse], along with a -high-level interface to the lexer and some validation routines that run after -macro expansion. In particular, the [`rustc_parse::parser`][parser] contains -the parser implementation. +high-level interface to the lexer and some validation routines that run after macro expansion. +In particular, the [`rustc_parse::parser`][parser] contains the parser implementation. The main entrypoint to the parser is via the various `parse_*` functions and others in -[rustc_parse][rustc_parse]. They let you do things like turn a [`SourceFile`][sourcefile] +[rustc_parse][rustc_parse]. +They let you do things like turn a [`SourceFile`][sourcefile] (e.g. the source in a single file) into a token stream, create a parser from -the token stream, and then execute the parser to get a [`Crate`] (the root AST -node). +the token stream, and then execute the parser to get a [`Crate`] (the root AST node). To minimize the amount of copying that is done, both [`Lexer`] and [`Parser`] have lifetimes which bind them to the parent [`ParseSess`]. @@ -63,13 +62,13 @@ Expansion itself may require parsing the output of a macro, which may reveal mor Code for lexical analysis is split between two crates: -- [`rustc_lexer`] crate is responsible for breaking a `&str` into chunks - constituting tokens. Although it is popular to implement lexers as generated - finite state machines, the lexer in [`rustc_lexer`] is hand-written. +- [`rustc_lexer`] crate is responsible for breaking a `&str` into chunks constituting tokens. + Although it is popular to implement lexers as generated finite state machines, + the lexer in [`rustc_lexer`] is hand-written. -- [`Lexer`] integrates [`rustc_lexer`] with data structures specific to - `rustc`. Specifically, it adds `Span` information to tokens returned by - [`rustc_lexer`] and interns identifiers. +- [`Lexer`] integrates [`rustc_lexer`] with data structures specific to `rustc`. + Specifically, + it adds `Span` information to tokens returned by [`rustc_lexer`] and interns identifiers. [`Crate`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_ast/ast/struct.Crate.html [`Parser`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_parse/parser/struct.Parser.html