Skip to content

Commit 6cf0caa

Browse files
nikomatsakisnikomatsakis
committed
make it possible to customize typing
and start moving more things into macros
1 parent 3b605bd commit 6cf0caa

File tree

6 files changed

+95
-146
lines changed

6 files changed

+95
-146
lines changed

‎crates/formality-macros/src/attrs.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -81,5 +81,6 @@ fn remove_formality_attributes_from_vec(attrs: &mut Vec<Attribute>) {
8181
!attr.path().is_ident("grammar")
8282
&& !attr.path().is_ident("cast")
8383
&& !attr.path().is_ident("variable")
84+
&& !attr.path().is_ident("customize")
8485
});
8586
}

‎crates/formality-types/src/grammar/ty.rs

Lines changed: 11 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
use formality_core::{cast_impl, term, Visit};
1+
use formality_core::{cast_impl, term};
22
use std::sync::Arc;
33

44
mod debug_impls;
@@ -11,7 +11,8 @@ use super::{
1111
consts::Const, AdtId, AssociatedItemId, Binder, ExistentialVar, FnId, TraitId, UniversalVar,
1212
};
1313

14-
#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
14+
#[term]
15+
#[cast]
1516
pub struct Ty {
1617
data: Arc<TyData>,
1718
}
@@ -97,27 +98,27 @@ impl DowncastTo<TyData> for Ty {
9798

9899
// NB: TyData doesn't implement Fold; you fold types, not TyData,
99100
// because variables might not map to the same variant.
100-
#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Visit)]
101+
#[term]
102+
#[customize(parse)]
101103
pub enum TyData {
104+
#[cast]
102105
RigidTy(RigidTy),
106+
#[cast]
103107
AliasTy(AliasTy),
108+
#[cast]
104109
PredicateTy(PredicateTy),
110+
#[variable]
105111
Variable(Variable),
106112
}
107113

108-
impl UpcastFrom<TyData> for TyData {
109-
fn upcast_from(term: TyData) -> Self {
110-
term
111-
}
112-
}
113-
114114
impl UpcastFrom<Ty> for TyData {
115115
fn upcast_from(term: Ty) -> Self {
116116
term.data().clone()
117117
}
118118
}
119119

120120
#[term((rigid $name $*parameters))]
121+
#[customize(parse)]
121122
pub struct RigidTy {
122123
pub name: RigidName,
123124
pub parameters: Parameters,
@@ -187,6 +188,7 @@ pub enum ScalarId {
187188
}
188189

189190
#[term((alias $name $*parameters))]
191+
#[customize(parse)]
190192
pub struct AliasTy {
191193
pub name: AliasName,
192194
pub parameters: Parameters,
@@ -353,7 +355,6 @@ impl DowncastTo<Variable> for Parameter {
353355
}
354356
}
355357

356-
cast_impl!(Ty);
357358
cast_impl!((RigidTy) <: (TyData) <: (Ty));
358359
cast_impl!((AliasTy) <: (TyData) <: (Ty));
359360
cast_impl!((ScalarId) <: (TyData) <: (Ty));
@@ -363,10 +364,6 @@ cast_impl!((AliasTy) <: (Ty) <: (Parameter));
363364
cast_impl!((ScalarId) <: (Ty) <: (Parameter));
364365
cast_impl!((PredicateTy) <: (Ty) <: (Parameter));
365366
cast_impl!((TyData) <: (Ty) <: (Parameter));
366-
cast_impl!(TyData::RigidTy(RigidTy));
367-
cast_impl!(TyData::AliasTy(AliasTy));
368-
cast_impl!(TyData::PredicateTy(PredicateTy));
369-
cast_impl!(TyData::Variable(Variable));
370367
cast_impl!((Variable) <: (TyData) <: (Ty));
371368
cast_impl!((UniversalVar) <: (Variable) <: (TyData));
372369
cast_impl!((ExistentialVar) <: (Variable) <: (TyData));

‎crates/formality-types/src/grammar/ty/debug_impls.rs

Lines changed: 0 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,5 @@
11
use crate::grammar::Const;
22

3-
impl std::fmt::Debug for super::Ty {
4-
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
5-
match self.data() {
6-
super::TyData::RigidTy(r) => write!(f, "{r:?}"),
7-
super::TyData::AliasTy(r) => write!(f, "{r:?}"),
8-
super::TyData::PredicateTy(r) => write!(f, "{r:?}"),
9-
super::TyData::Variable(r) => write!(f, "{r:?}"),
10-
}
11-
}
12-
}
13-
143
impl std::fmt::Debug for Const {
154
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
165
match self.data() {

‎crates/formality-types/src/grammar/ty/parse_impls.rs

Lines changed: 81 additions & 82 deletions
Original file line numberDiff line numberDiff line change
@@ -4,25 +4,21 @@ use formality_core::parse::{ActiveVariant, CoreParse, ParseError, ParseResult, P
44
use formality_core::Upcast;
55
use formality_core::{seq, Set};
66

7-
use crate::grammar::{AdtId, AssociatedItemId, Bool, Const, RigidName, Scalar, TraitId};
7+
use crate::grammar::{AdtId, AssociatedItemId, Bool, Const, RefKind, RigidName, Scalar, TraitId};
88

9-
use super::{AliasTy, AssociatedTyName, Lt, LtData, Parameter, PredicateTy, RigidTy, ScalarId, Ty};
9+
use super::{
10+
AliasTy, AssociatedTyName, Lt, LtData, Parameter, PredicateTy, RigidTy, ScalarId, Ty, TyData,
11+
};
1012

1113
use crate::rust::FormalityLang as Rust;
1214

1315
// ANCHOR: ty_parse_impl
1416
// For types, we invest some effort into parsing them decently because it makes
1517
// writing tests so much more pleasant.
16-
impl CoreParse<Rust> for Ty {
18+
impl CoreParse<Rust> for TyData {
1719
fn parse<'t>(scope: &Scope<Rust>, text0: &'t str) -> ParseResult<'t, Self> {
1820
let mut parser = Parser::new(scope, text0, "Ty");
19-
parser.parse_variant_cast::<ScalarId>(1);
2021
parser.parse_variant("Variable", 1, |p| p.variable());
21-
parser.parse_variant("Adt", 0, |p| p.nonterminal_with(parse_adt_ty));
22-
parser.parse_variant("Assoc", 0, |p| p.nonterminal_with(parse_assoc_ty));
23-
parser.parse_variant("Ref", 0, |p| p.nonterminal_with(parse_ref_ty));
24-
parser.parse_variant("RefMut", 0, |p| p.nonterminal_with(parse_ref_mut_ty));
25-
parser.parse_variant("Tuple", 0, |p| p.nonterminal_with(parse_tuple_ty));
2622
parser.parse_variant_cast::<RigidTy>(0);
2723
parser.parse_variant_cast::<AliasTy>(0);
2824
parser.parse_variant_cast::<PredicateTy>(0);
@@ -31,84 +27,87 @@ impl CoreParse<Rust> for Ty {
3127
}
3228
// ANCHOR_END: ty_parse_impl
3329

34-
#[tracing::instrument(level = "trace", ret)]
35-
fn parse_adt_ty<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Ty> {
36-
// Treat plain identifiers as adt ids, with or without parameters.
37-
Parser::single_variant(scope, text, "AdtTy", |p| {
38-
let name: AdtId = p.nonterminal()?;
39-
let parameters: Vec<Parameter> = parse_parameters(p)?;
40-
Ok(Ty::rigid(name, parameters))
41-
})
42-
}
30+
impl CoreParse<Rust> for RigidTy {
31+
fn parse<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Self> {
32+
let mut parser: Parser<'_, '_, RigidTy, Rust> = Parser::new(scope, text, "AliasTy");
4333

44-
#[tracing::instrument(level = "trace", ret)]
45-
fn parse_ref_ty<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Ty> {
46-
Parser::single_variant(scope, text, "RefTy", |p| {
47-
p.expect_char('&')?;
48-
let lt: Lt = p.nonterminal()?;
49-
let ty: Ty = p.nonterminal()?;
50-
let name = crate::grammar::RigidName::Ref(crate::grammar::RefKind::Shared);
51-
Ok(RigidTy {
52-
name,
53-
parameters: seq![lt.upcast(), ty.upcast()],
54-
}
55-
.upcast())
56-
})
57-
}
34+
parser.parse_variant_cast::<ScalarId>(1);
5835

59-
#[tracing::instrument(level = "trace", ret)]
60-
fn parse_ref_mut_ty<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Ty> {
61-
Parser::single_variant(scope, text, "RefMutTy", |p| {
62-
p.expect_char('&')?;
63-
p.expect_keyword("mut")?;
64-
let lt: Lt = p.nonterminal()?;
65-
let ty: Ty = p.nonterminal()?;
66-
let name = crate::grammar::RigidName::Ref(crate::grammar::RefKind::Mut);
67-
Ok(RigidTy {
68-
name,
69-
parameters: seq![lt.upcast(), ty.upcast()],
70-
}
71-
.upcast())
72-
})
73-
}
36+
parser.parse_variant("Adt", 0, |p| {
37+
let name: AdtId = p.nonterminal()?;
38+
let parameters: Vec<Parameter> = parse_parameters(p)?;
39+
Ok(RigidTy {
40+
name: name.upcast(),
41+
parameters,
42+
})
43+
});
7444

75-
#[tracing::instrument(level = "trace", ret)]
76-
fn parse_tuple_ty<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Ty> {
77-
Parser::single_variant(scope, text, "TupleTy", |p| {
78-
p.expect_char('(')?;
79-
p.reject_custom_keywords(&["alias", "rigid", "predicate"])?;
80-
let types: Vec<Ty> = p.comma_nonterminal()?;
81-
p.expect_char(')')?;
82-
let name = RigidName::Tuple(types.len());
83-
Ok(RigidTy {
84-
name,
85-
parameters: types.upcast(),
86-
}
87-
.upcast())
88-
})
45+
parser.parse_variant("Ref", 0, |p| {
46+
p.expect_char('&')?;
47+
let lt: Lt = p.nonterminal()?;
48+
let ty: Ty = p.nonterminal()?;
49+
Ok(RigidTy {
50+
name: RigidName::Ref(RefKind::Shared),
51+
parameters: seq![lt.upcast(), ty.upcast()],
52+
}
53+
.upcast())
54+
});
55+
56+
parser.parse_variant("RefMut", 0, |p| {
57+
p.expect_char('&')?;
58+
p.expect_keyword("mut")?;
59+
let lt: Lt = p.nonterminal()?;
60+
let ty: Ty = p.nonterminal()?;
61+
Ok(RigidTy {
62+
name: RigidName::Ref(RefKind::Mut),
63+
parameters: seq![lt.upcast(), ty.upcast()],
64+
})
65+
});
66+
67+
parser.parse_variant("Tuple", 0, |p| {
68+
p.expect_char('(')?;
69+
p.reject_custom_keywords(&["alias", "rigid", "predicate"])?;
70+
let types: Vec<Ty> = p.comma_nonterminal()?;
71+
p.expect_char(')')?;
72+
let name = RigidName::Tuple(types.len());
73+
Ok(RigidTy {
74+
name,
75+
parameters: types.upcast(),
76+
})
77+
});
78+
79+
parser.finish()
80+
}
8981
}
9082

91-
#[tracing::instrument(level = "trace", ret)]
92-
fn parse_assoc_ty<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Ty> {
93-
Parser::single_variant(scope, text, "AssocTy", |p| {
94-
p.expect_char('<')?;
95-
let ty0: Ty = p.nonterminal()?;
96-
let () = p.expect_keyword("as")?;
97-
let trait_id: TraitId = p.nonterminal()?;
98-
let trait_parameters1 = parse_parameters(p)?;
99-
p.expect_char('>')?;
100-
p.expect_char(':')?;
101-
p.expect_char(':')?;
102-
let item_id: AssociatedItemId = p.nonterminal()?;
103-
let item_parameters = parse_parameters(p)?;
104-
let assoc_ty_id = AssociatedTyName { trait_id, item_id };
105-
let parameters: Vec<Parameter> = std::iter::once(ty0.upcast())
106-
.chain(trait_parameters1)
107-
.chain(item_parameters)
108-
.collect();
109-
Ok(Ty::alias(assoc_ty_id, parameters))
110-
})
111-
// Treat plain identifiers as adt ids, with or without parameters.
83+
impl CoreParse<Rust> for AliasTy {
84+
fn parse<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Self> {
85+
let mut parser: Parser<'_, '_, AliasTy, Rust> = Parser::new(scope, text, "AliasTy");
86+
87+
parser.parse_variant("associated type", 0, |p| {
88+
p.expect_char('<')?;
89+
let ty0: Ty = p.nonterminal()?;
90+
let () = p.expect_keyword("as")?;
91+
let trait_id: TraitId = p.nonterminal()?;
92+
let trait_parameters1 = parse_parameters(p)?;
93+
p.expect_char('>')?;
94+
p.expect_char(':')?;
95+
p.expect_char(':')?;
96+
let item_id: AssociatedItemId = p.nonterminal()?;
97+
let item_parameters = parse_parameters(p)?;
98+
let name = AssociatedTyName { trait_id, item_id };
99+
let parameters: Vec<Parameter> = std::iter::once(ty0.upcast())
100+
.chain(trait_parameters1)
101+
.chain(item_parameters)
102+
.collect();
103+
Ok(AliasTy {
104+
name: name.upcast(),
105+
parameters,
106+
})
107+
});
108+
109+
parser.finish()
110+
}
112111
}
113112

114113
fn parse_parameters<'t>(

‎crates/formality-types/src/grammar/ty/term_impls.rs

Lines changed: 1 addition & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,10 @@
1-
use crate::grammar::{Const, ConstData, Lt, LtData, Parameter, Ty, TyData, ValTree};
1+
use crate::grammar::{Const, ConstData, Lt, LtData, Parameter, ValTree};
22
use crate::rust::Variable;
33
use crate::FormalityLang;
44
use formality_core::{
55
fold::{CoreFold, SubstitutionFn},
66
language::CoreKind,
7-
term::CoreTerm,
87
visit::CoreVisit,
9-
Upcast,
108
};
119

1210
use super::ParameterKind;
@@ -40,10 +38,6 @@ impl CoreVisit<FormalityLang> for LtData {
4038
}
4139
}
4240

43-
impl CoreTerm<FormalityLang> for Ty {}
44-
45-
impl CoreTerm<FormalityLang> for Lt {}
46-
4741
impl formality_core::language::HasKind<FormalityLang> for Parameter {
4842
fn kind(&self) -> CoreKind<FormalityLang> {
4943
match self {
@@ -54,23 +48,6 @@ impl formality_core::language::HasKind<FormalityLang> for Parameter {
5448
}
5549
}
5650

57-
// ANCHOR: core_fold_ty
58-
impl CoreFold<FormalityLang> for Ty {
59-
fn substitute(&self, substitution_fn: SubstitutionFn<'_, FormalityLang>) -> Self {
60-
match self.data() {
61-
TyData::RigidTy(v) => v.substitute(substitution_fn).upcast(),
62-
TyData::AliasTy(v) => v.substitute(substitution_fn).upcast(),
63-
TyData::PredicateTy(v) => v.substitute(substitution_fn).upcast(),
64-
TyData::Variable(v) => match substitution_fn(*v) {
65-
None => self.clone(),
66-
Some(Parameter::Ty(t)) => t,
67-
Some(param) => panic!("ill-kinded substitute: expected type, got {param:?}"),
68-
},
69-
}
70-
}
71-
}
72-
// ANCHOR_END: core_fold_ty
73-
7451
impl CoreFold<FormalityLang> for Const {
7552
fn substitute(&self, substitution_fn: SubstitutionFn<'_, FormalityLang>) -> Self {
7653
match self.data() {
@@ -106,20 +83,6 @@ impl CoreFold<FormalityLang> for Lt {
10683
}
10784
}
10885

109-
impl CoreVisit<FormalityLang> for Ty {
110-
fn free_variables(&self) -> Vec<Variable> {
111-
self.data().free_variables()
112-
}
113-
114-
fn size(&self) -> usize {
115-
self.data().size()
116-
}
117-
118-
fn assert_valid(&self) {
119-
self.data().assert_valid()
120-
}
121-
}
122-
12386
impl CoreVisit<FormalityLang> for Lt {
12487
fn free_variables(&self) -> Vec<Variable> {
12588
self.data().free_variables()

‎tests/projection.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -252,7 +252,7 @@ const PROJECTION_EQUALITY: &str = "[
252252
type Type<> : [] where [];
253253
}
254254
trait Trait2<ty T> where [] {}
255-
impl<ty T, ty U> Trait2<T> for U where [ U: Trait1<>, (alias (Trait1::Type) S) => T ] {}
255+
impl<ty T, ty U> Trait2<T> for U where [ U: Trait1<>, <S as Trait1>::Type => T ] {}
256256
struct S<> where [] {}
257257
impl<> Trait1<> for S<> where [] {
258258
type Type<> = u32 where [];

0 commit comments

Comments
 (0)