Skip to content

Commit 1dc3bda

Browse files
nikomatsakisnikomatsakis
committed
accept defaulted binders in traits, remove <>
We don't need this anymore.
1 parent c30ff77 commit 1dc3bda

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

+203
-194
lines changed

‎crates/formality-prove/src/test/adt_wf.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ use crate::{decls::Decls, prove::prove};
1010
fn decls() -> Decls {
1111
Decls {
1212
trait_decls: vec![term("trait Foo<ty Self> where {}")],
13-
impl_decls: vec![term("impl<> Foo(u32) where {}")],
13+
impl_decls: vec![term("impl Foo(u32) where {}")],
1414
adt_decls: vec![term("adt X<ty T> where {Foo(T)}")],
1515
..Decls::empty()
1616
}

‎crates/formality-prove/src/test/magic_copy.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ fn decls() -> Decls {
1515
],
1616
impl_decls: vec![
1717
term("impl<ty T> Magic(T) where {Magic(T)}"),
18-
term("impl<> Copy(u32) where {}"),
18+
term("impl Copy(u32) where {}"),
1919
],
2020
..Decls::empty()
2121
}

‎crates/formality-prove/src/test/simple_impl.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ fn decls() -> Decls {
1111
trait_decls: vec![term("trait Debug<ty Self> where {}")],
1212
impl_decls: vec![
1313
term("impl<ty T> Debug(Vec<T>) where {Debug(T)}"),
14-
term("impl<> Debug(u32) where {}"),
14+
term("impl Debug(u32) where {}"),
1515
],
1616
..Decls::empty()
1717
}

‎crates/formality-rust/src/trait_binder.rs

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -79,6 +79,7 @@ where
7979
T: Term,
8080
{
8181
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
82+
// In Debug output, we include the `Self` to avoid confusion -- is this good?
8283
write!(f, "{:?}", self.explicit_binder)
8384
}
8485
}
@@ -90,9 +91,17 @@ where
9091
#[tracing::instrument(level = "trace", ret)]
9192
fn parse<'t>(scope: &Scope<FormalityLang>, text: &'t str) -> ParseResult<'t, Self> {
9293
Parser::single_variant(scope, text, "TraitBinder", |p| {
93-
p.expect_char('<')?;
94-
let mut bindings: Vec<Binding<FormalityLang>> = p.comma_nonterminal()?;
95-
p.expect_char('>')?;
94+
let mut bindings = match p.expect_char('<') {
95+
Ok(()) => {
96+
let bindings: Vec<Binding<FormalityLang>> = p.comma_nonterminal()?;
97+
p.expect_char('>')?;
98+
bindings
99+
}
100+
Err(_) => {
101+
// If we don't see a `<`, assume there are no add'l bound variables.
102+
vec![]
103+
}
104+
};
96105

97106
// insert the `Self` binding at position 0
98107
let bound_var = BoundVar::fresh(ParameterKind::Ty);

‎examples/formality-eg/grammar/test.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ fn test_struct_decl() {
1515

1616
#[test]
1717
fn test_struct_ty_empty_args() {
18-
let r: Ty = term("Point<>");
18+
let r: Ty = term("Point");
1919
expect_test::expect![[r#"
2020
Point
2121
"#]]

‎fixme_tests/basic--impl_Debug_for_i32.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@
33

44
const PROGRAM: &str = "[
55
crate core {
6-
trait Debug<> { }
6+
trait Debug { }
77
8-
impl<> Debug<> for i32 { }
8+
impl Debug for i32 { }
99
}
1010
]";
1111

@@ -19,7 +19,7 @@ fn test_i32() {
1919
"#]]
2020
.assert_debug_eq(&formality_rust::test_can_prove_where_clause(
2121
PROGRAM,
22-
"i32: Debug<>",
22+
"i32: Debug",
2323
));
2424
}
2525

@@ -33,6 +33,6 @@ fn test_u32() {
3333
"#]]
3434
.assert_debug_eq(&formality_rust::test_can_prove_where_clause(
3535
PROGRAM,
36-
"u32: Debug<>",
36+
"u32: Debug",
3737
));
3838
}

‎fixme_tests/basic--supertraits-hr.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33

44
const PROGRAM: &str = "[
55
crate core {
6-
trait Sub<> where for<lt l> Self: Super<l> { }
6+
trait Sub where for<lt l> Self: Super<l> { }
77
trait Super<lt x> { }
88
}
99
]";

‎fixme_tests/basic--supertraits.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,12 @@
33

44
const PROGRAM: &str = "[
55
crate core {
6-
trait Eq<> where Self: PartialEq<> { }
7-
trait PartialEq<> { }
6+
trait Eq where Self: PartialEq { }
7+
trait PartialEq { }
88
99
// ComparableBase is a supertype, but `T: Eq` is not.
10-
trait Comparable<ty T> where T: Eq<>, Self: ComparableBase<> { }
11-
trait ComparableBase<> { }
10+
trait Comparable<ty T> where T: Eq, Self: ComparableBase { }
11+
trait ComparableBase { }
1212
}
1313
]";
1414

‎fixme_tests/coinductive.rs

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -6,11 +6,11 @@
66
fn magic_copy() {
77
const PROGRAM: &str = "[
88
crate core {
9-
struct Foo<> {}
10-
trait Copy<> {}
11-
trait Magic<> where Self: Copy<> {}
9+
struct Foo {}
10+
trait Copy {}
11+
trait Magic where Self: Copy {}
1212
13-
impl<ty T> Magic<> for T where T: Magic<> {}
13+
impl<ty T> Magic for T where T: Magic {}
1414
}
1515
]";
1616

@@ -28,7 +28,7 @@ fn magic_copy() {
2828
"#]]
2929
.assert_debug_eq(&formality_rust::test_can_prove_where_clause(
3030
PROGRAM,
31-
"Foo: Magic<>",
31+
"Foo: Magic",
3232
));
3333
}
3434

@@ -37,13 +37,13 @@ fn magic_copy() {
3737
fn magic_copy_impl_for_all_copy() {
3838
const PROGRAM: &str = "[
3939
crate core {
40-
struct Foo<> {}
40+
struct Foo {}
4141
struct Vec<ty T> {}
4242
43-
trait Copy<> {}
44-
trait Magic<> where Self: Copy<> {}
43+
trait Copy {}
44+
trait Magic where Self: Copy {}
4545
46-
impl<ty T> Magic<> for T where T: Copy<> {}
46+
impl<ty T> Magic for T where T: Copy {}
4747
}
4848
]";
4949

@@ -82,17 +82,17 @@ fn magic_copy_impl_for_all_copy() {
8282
fn magic_vec_t() {
8383
const PROGRAM: &str = "[
8484
crate core {
85-
struct Foo<> {}
85+
struct Foo {}
8686
struct Vec<ty T> {}
8787
88-
trait Copy<> {}
89-
trait Magic<> where Self: Copy<> {}
88+
trait Copy {}
89+
trait Magic where Self: Copy {}
9090
91-
impl<ty T> Magic<> for Vec<T> where T: Magic<> {
91+
impl<ty T> Magic for Vec<T> where T: Magic {
9292
// FIXME: We need to test that this impl can prove T: Copy,
9393
// but how to do it?
9494
}
95-
impl<ty T> Copy<> for Vec<T> where T: Magic<> {}
95+
impl<ty T> Copy for Vec<T> where T: Magic {}
9696
}
9797
]";
9898

‎fixme_tests/impl-vs-trait-fn.rs

Lines changed: 18 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -6,15 +6,15 @@
66
fn absolutely_same() {
77
const PROGRAM: &str = "[
88
crate core {
9-
trait Debug<> {}
10-
trait Display<> {}
9+
trait Debug {}
10+
trait Display {}
1111
12-
trait Get<> {
13-
fn get<ty T, lt l>(&mut l T) -> () where [T: Debug<>];
12+
trait Get {
13+
fn get<ty T, lt l>(&mut l T) -> () where [T: Debug];
1414
}
1515
16-
impl<> Get<> for () {
17-
fn get<ty T, lt l>(&mut l T) -> () where T: Debug<> {
16+
impl Get for () {
17+
fn get<ty T, lt l>(&mut l T) -> () where T: Debug {
1818
trusted
1919
}
2020
}
@@ -34,16 +34,16 @@ fn absolutely_same() {
3434
fn different_self_type_mut_vs_sh() {
3535
const PROGRAM: &str = "[
3636
crate core {
37-
trait Debug<> {}
38-
trait Display<> {}
37+
trait Debug {}
38+
trait Display {}
3939
40-
trait Get<> {
41-
fn get<ty T, lt l>(&mut l T) -> () where [T: Debug<>];
40+
trait Get {
41+
fn get<ty T, lt l>(&mut l T) -> () where [T: Debug];
4242
// --------
4343
}
4444
45-
impl<> Get<> for () {
46-
fn get<ty T, lt l>(&l T) -> () where T: Debug<> {
45+
impl Get for () {
46+
fn get<ty T, lt l>(&l T) -> () where T: Debug {
4747
// ----
4848
trusted
4949
}
@@ -70,16 +70,16 @@ fn different_self_type_mut_vs_sh() {
7070
fn different_arg_type_u32_vs_i32() {
7171
const PROGRAM: &str = "[
7272
crate core {
73-
trait Debug<> {}
74-
trait Display<> {}
73+
trait Debug {}
74+
trait Display {}
7575
76-
trait Get<> {
77-
fn get<ty T, lt l>(&mut l T, u32) -> () where [T: Debug<>];
76+
trait Get {
77+
fn get<ty T, lt l>(&mut l T, u32) -> () where [T: Debug];
7878
// ---
7979
}
8080
81-
impl<> Get<> for () {
82-
fn get<ty T, lt l>(&mut l T, i32) -> () where T: Debug<> {
81+
impl Get for () {
82+
fn get<ty T, lt l>(&mut l T, i32) -> () where T: Debug {
8383
// ---
8484
trusted
8585
}

0 commit comments

Comments
 (0)