Skip to content

Commit 13b4ad8

Browse files
authored
Merge pull request #138 from nikomatsakis/docs
Remove the docusaurus; add some doc comments
2 parents 1608cc2 + 7535bc1 commit 13b4ad8

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

41 files changed

+61
-24629
lines changed

.github/workflows/deploy.yaml

Lines changed: 0 additions & 39 deletions
This file was deleted.

.github/workflows/test-deploy.yaml

Lines changed: 0 additions & 22 deletions
This file was deleted.

book/.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
book

book/book.toml

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
[book]
2+
authors = ["Niko Matsakis"]
3+
language = "en"
4+
multilingual = false
5+
src = "src"
6+
title = "A MIR Formality"

book/src/SUMMARY.md

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
# Summary
2+
3+
- [Intro](./intro.md)
4+
- [Formality](./formality.md)
5+
- [Terms](./terms.md)
6+
- [Inference rules](./inference_rules.md)

book/src/chapter_1.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
# Chapter 1

crates/formality-check/src/coherence.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -97,6 +97,8 @@ impl Check<'_> {
9797

9898
// If we can prove that the parameters cannot be equated *or* the where-clauses don't hold,
9999
// in coherence mode, then they do not overlap.
100+
//
101+
// ∀P_a, ∀P_b. ⌐ (coherence_mode => (Ts_a = Ts_b && WC_a && WC_b))
100102
if let Ok(()) = self.prove_not_goal(
101103
&env.with_coherence_mode(true),
102104
(),

crates/formality-prove/src/decls.rs

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,8 @@ use formality_types::{
1212
#[term]
1313
pub struct Decls {
1414
pub max_size: usize,
15+
16+
/// Each trait in the program
1517
pub trait_decls: Vec<TraitDecl>,
1618
pub impl_decls: Vec<ImplDecl>,
1719
pub neg_impl_decls: Vec<NegImplDecl>,
@@ -95,31 +97,49 @@ impl Decls {
9597
}
9698
}
9799

100+
/// An "impl decl" indicates that a trait is implemented for a given set of types.
101+
/// One "impl decl" is created for each impl in the Rust source.
98102
#[term(impl $binder)]
99103
pub struct ImplDecl {
104+
/// The binder covers the generic variables from the impl
100105
pub binder: Binder<ImplDeclBoundData>,
101106
}
102107

108+
/// Data bound under the generics from [`ImplDecl`][]
103109
#[term($trait_ref where $where_clause)]
104110
pub struct ImplDeclBoundData {
111+
/// The trait ref that is implemented
105112
pub trait_ref: TraitRef,
113+
114+
///
106115
pub where_clause: Wcs,
107116
}
108117

118+
/// A declaration that some trait will *not* be implemented for a type; derived from negative impls
119+
/// like `impl !Foo for Bar`.
109120
#[term(impl $binder)]
110121
pub struct NegImplDecl {
122+
/// Binder comes the generics on the impl
111123
pub binder: Binder<NegImplDeclBoundData>,
112124
}
113125

126+
/// Data bound under the impl generics for a negative impl
114127
#[term(!$trait_ref where $where_clause)]
115128
pub struct NegImplDeclBoundData {
116129
pub trait_ref: TraitRef,
117130
pub where_clause: Wcs,
118131
}
119132

133+
/// A "trait declaration" declares a trait that exists, its generics, and its where-clauses.
134+
/// It doesn't capture the trait items, which will be transformed into other sorts of rules.
135+
///
136+
/// In Rust syntax, it covers the `trait Foo: Bar` part of the declaration, but not what appears in the `{...}`.
120137
#[term(trait $id $binder)]
121138
pub struct TraitDecl {
139+
/// The name of the trait
122140
pub id: TraitId,
141+
142+
/// The binder here captures the generics of the trait; it always begins with a `Self` type.
123143
pub binder: Binder<TraitDeclBoundData>,
124144
}
125145

@@ -163,24 +183,39 @@ impl TraitDecl {
163183
}
164184
}
165185

186+
/// A trait *invariant* is a rule like `<T> Implemented(T: Ord) => Implemented(T: PartialOrd)`.
187+
/// It indices that, if we know that `T: Ord` from the environment,
188+
/// we also know that `T: PartialOrd`.
189+
/// Invariants are produced from trait declarations during lowering; they derive from the
190+
/// where-clauses on the trait.
166191
#[term]
167192
pub struct TraitInvariant {
168193
pub binder: Binder<TraitInvariantBoundData>,
169194
}
170195

196+
/// The "bound data" for a [`TraitInvariant`][] -- i.e., what is covered by the forall.
171197
#[term($trait_ref => $where_clause)]
172198
pub struct TraitInvariantBoundData {
199+
/// Knowing that this trait-ref is implemented...
173200
pub trait_ref: TraitRef,
201+
202+
/// ...implies that these where-clauses hold.
174203
pub where_clause: Wc,
175204
}
176205

206+
/// The "bound data" for a [`TraitDecl`][] -- i.e., what is covered by the forall.
177207
#[term(where $where_clause)]
178208
pub struct TraitDeclBoundData {
209+
/// The where-clauses declared on the trait
179210
pub where_clause: Wcs,
180211
}
181212

213+
/// An "alias equal declaration" declares when an alias type can be normalized
214+
/// to something else. They are derived from `type Foo = Bar` declarations in
215+
/// impls, which would generate an alias eq decl saying that `<T as SomeTrait>::Foo = Bar`.
182216
#[term(alias $binder)]
183217
pub struct AliasEqDecl {
218+
/// The binder includes the generics from the impl and also any generics on the GAT.
184219
pub binder: Binder<AliasEqDeclBoundData>,
185220
}
186221

@@ -190,13 +225,23 @@ impl AliasEqDecl {
190225
}
191226
}
192227

228+
/// Data bound under the impl generics for a [`AliasEqDecl`][]
193229
#[term($alias = $ty where $where_clause)]
194230
pub struct AliasEqDeclBoundData {
231+
/// The alias that is equal
195232
pub alias: AliasTy,
233+
234+
/// The type the alias is equal to
196235
pub ty: Ty,
236+
237+
/// The where-clauses that must hold for this rule to be applicable; derived from the impl and the GAT
197238
pub where_clause: Wcs,
198239
}
199240

241+
/// Alias bounds indicate things that are always known to be true of an alias type,
242+
/// even when its precise value is not known.
243+
/// For example given a trait `trait Foo { type Bar: Baz; }`
244+
/// we know that `<T as Foo>::Bar: Baz` must hold.
200245
#[term(alias $binder)]
201246
pub struct AliasBoundDecl {
202247
pub binder: Binder<AliasBoundDeclBoundData>,

docs/.gitignore

Lines changed: 0 additions & 20 deletions
This file was deleted.

docs/README.md

Lines changed: 0 additions & 41 deletions
This file was deleted.

0 commit comments

Comments
 (0)