Skip to content

Commit 19d4430

Browse files
committed
Implement lowering for FnDef
1 parent cc4d257 commit 19d4430

File tree

2 files changed

+135
-9
lines changed

2 files changed

+135
-9
lines changed

chalk-integration/src/lib.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ pub use interner::{Identifier, RawId};
2222
#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
2323
pub enum TypeSort {
2424
Struct,
25+
FnDef,
2526
Trait,
2627
Opaque,
2728
}

chalk-integration/src/lowering.rs

Lines changed: 134 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ use crate::interner::ChalkIr;
22
use chalk_ir::cast::{Cast, Caster};
33
use chalk_ir::interner::HasInterner;
44
use chalk_ir::{
5-
self, AdtId, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, ImplId, OpaqueTyId,
5+
self, AdtId, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, FnDefId, ImplId, OpaqueTyId,
66
QuantifiedWhereClauses, Substitution, ToGenericArg, TraitId,
77
};
88
use chalk_parse::ast::*;
@@ -19,9 +19,11 @@ use crate::program::Program as LoweredProgram;
1919
use crate::{Identifier as Ident, RawId, TypeKind, TypeSort};
2020

2121
type AdtIds = BTreeMap<Ident, chalk_ir::AdtId<ChalkIr>>;
22+
type FnDefIds = BTreeMap<Ident, chalk_ir::FnDefId<ChalkIr>>;
2223
type TraitIds = BTreeMap<Ident, chalk_ir::TraitId<ChalkIr>>;
2324
type OpaqueTyIds = BTreeMap<Ident, chalk_ir::OpaqueTyId<ChalkIr>>;
2425
type AdtKinds = BTreeMap<chalk_ir::AdtId<ChalkIr>, TypeKind>;
26+
type FnDefKinds = BTreeMap<chalk_ir::FnDefId<ChalkIr>, TypeKind>;
2527
type TraitKinds = BTreeMap<chalk_ir::TraitId<ChalkIr>, TypeKind>;
2628
type AssociatedTyLookups = BTreeMap<(chalk_ir::TraitId<ChalkIr>, Ident), AssociatedTyLookup>;
2729
type AssociatedTyValueIds =
@@ -36,6 +38,8 @@ pub type LowerResult<T> = Result<T, RustIrError>;
3638
struct Env<'k> {
3739
adt_ids: &'k AdtIds,
3840
adt_kinds: &'k AdtKinds,
41+
fn_def_ids: &'k FnDefIds,
42+
fn_def_kinds: &'k FnDefKinds,
3943
trait_ids: &'k TraitIds,
4044
trait_kinds: &'k TraitKinds,
4145
opaque_ty_ids: &'k OpaqueTyIds,
@@ -73,6 +77,7 @@ struct AssociatedTyLookup {
7377
enum TypeLookup {
7478
Adt(chalk_ir::AdtId<ChalkIr>),
7579
GenericArg(BoundVar),
80+
FnDef(chalk_ir::FnDefId<ChalkIr>),
7681
Opaque(chalk_ir::OpaqueTyId<ChalkIr>),
7782
}
7883

@@ -96,6 +101,10 @@ impl<'k> Env<'k> {
96101
return Ok(TypeLookup::Adt(*id));
97102
}
98103

104+
if let Some(id) = self.fn_def_ids.get(&name.str) {
105+
return Ok(TypeLookup::FnDef(*id));
106+
}
107+
99108
if let Some(id) = self.opaque_ty_ids.get(&name.str) {
100109
return Ok(TypeLookup::Opaque(*id));
101110
}
@@ -140,6 +149,10 @@ impl<'k> Env<'k> {
140149
&self.adt_kinds[&id]
141150
}
142151

152+
fn fn_def_kind(&self, id: chalk_ir::FnDefId<ChalkIr>) -> &TypeKind {
153+
&self.fn_def_kinds[&id]
154+
}
155+
143156
fn trait_kind(&self, id: chalk_ir::TraitId<ChalkIr>) -> &TypeKind {
144157
&self.trait_kinds[&id]
145158
}
@@ -240,9 +253,11 @@ impl LowerProgram for Program {
240253
}
241254

242255
let mut adt_ids = BTreeMap::new();
256+
let mut fn_def_ids = BTreeMap::new();
243257
let mut trait_ids = BTreeMap::new();
244258
let mut opaque_ty_ids = BTreeMap::new();
245259
let mut adt_kinds = BTreeMap::new();
260+
let mut fn_def_kinds = BTreeMap::new();
246261
let mut trait_kinds = BTreeMap::new();
247262
let mut opaque_ty_kinds = BTreeMap::new();
248263
let mut object_safe_traits = HashSet::new();
@@ -254,6 +269,12 @@ impl LowerProgram for Program {
254269
adt_ids.insert(type_kind.name.clone(), id);
255270
adt_kinds.insert(id, type_kind);
256271
}
272+
Item::FnDefn(defn) => {
273+
let type_kind = defn.lower_type_kind()?;
274+
let id = FnDefId(raw_id);
275+
fn_def_ids.insert(type_kind.name.clone(), id);
276+
fn_def_kinds.insert(id, type_kind);
277+
}
257278
Item::TraitDefn(defn) => {
258279
let type_kind = defn.lower_type_kind()?;
259280
let id = TraitId(raw_id);
@@ -276,6 +297,7 @@ impl LowerProgram for Program {
276297
}
277298

278299
let mut adt_data = BTreeMap::new();
300+
let mut fn_def_data = BTreeMap::new();
279301
let mut trait_data = BTreeMap::new();
280302
let mut well_known_traits = BTreeMap::new();
281303
let mut impl_data = BTreeMap::new();
@@ -287,6 +309,8 @@ impl LowerProgram for Program {
287309
let empty_env = Env {
288310
adt_ids: &adt_ids,
289311
adt_kinds: &adt_kinds,
312+
fn_def_ids: &fn_def_ids,
313+
fn_def_kinds: &fn_def_kinds,
290314
trait_ids: &trait_ids,
291315
trait_kinds: &trait_kinds,
292316
opaque_ty_ids: &opaque_ty_ids,
@@ -299,6 +323,13 @@ impl LowerProgram for Program {
299323
let adt_id = AdtId(raw_id);
300324
adt_data.insert(adt_id, Arc::new(d.lower_adt(adt_id, &empty_env)?));
301325
}
326+
Item::FnDefn(ref defn) => {
327+
let fn_def_id = FnDefId(raw_id);
328+
fn_def_data.insert(
329+
fn_def_id,
330+
Arc::new(defn.lower_fn_def(fn_def_id, &empty_env)?),
331+
);
332+
}
302333
Item::TraitDefn(ref trait_defn) => {
303334
let trait_id = TraitId(raw_id);
304335
let trait_datum = trait_defn.lower_trait(trait_id, &empty_env)?;
@@ -454,10 +485,13 @@ impl LowerProgram for Program {
454485

455486
let program = LoweredProgram {
456487
adt_ids,
488+
fn_def_ids,
457489
trait_ids,
458490
adt_kinds,
491+
fn_def_kinds,
459492
trait_kinds,
460493
adt_data,
494+
fn_def_data,
461495
trait_data,
462496
well_known_traits,
463497
impl_data,
@@ -538,6 +572,16 @@ impl LowerParameterMap for StructDefn {
538572
}
539573
}
540574

575+
impl LowerParameterMap for FnDefn {
576+
fn synthetic_parameters(&self) -> Option<NamedGenericArg> {
577+
None
578+
}
579+
580+
fn declared_parameters(&self) -> &[VariableKind] {
581+
&self.variable_kinds
582+
}
583+
}
584+
541585
impl LowerParameterMap for Impl {
542586
fn synthetic_parameters(&self) -> Option<NamedGenericArg> {
543587
None
@@ -631,6 +675,26 @@ impl LowerTypeKind for StructDefn {
631675
}
632676
}
633677

678+
impl LowerTypeKind for FnDefn {
679+
fn lower_type_kind(&self) -> LowerResult<TypeKind> {
680+
let interner = &ChalkIr;
681+
Ok(TypeKind {
682+
sort: TypeSort::FnDef,
683+
name: self.name.str.clone(),
684+
binders: chalk_ir::Binders::new(
685+
chalk_ir::VariableKinds::from(interner, self.all_parameters().anonymize()),
686+
crate::Unit,
687+
),
688+
})
689+
}
690+
}
691+
692+
impl LowerWhereClauses for FnDefn {
693+
fn where_clauses(&self) -> &[QuantifiedWhereClause] {
694+
&self.where_clauses
695+
}
696+
}
697+
634698
impl LowerWhereClauses for StructDefn {
635699
fn where_clauses(&self) -> &[QuantifiedWhereClause] {
636700
&self.where_clauses
@@ -850,6 +914,42 @@ impl LowerAdtDefn for StructDefn {
850914
}
851915
}
852916

917+
trait LowerFnDefn {
918+
fn lower_fn_def(
919+
&self,
920+
fn_def_id: chalk_ir::FnDefId<ChalkIr>,
921+
env: &Env,
922+
) -> LowerResult<rust_ir::FnDefDatum<ChalkIr>>;
923+
}
924+
925+
impl LowerFnDefn for FnDefn {
926+
fn lower_fn_def(
927+
&self,
928+
fn_def_id: chalk_ir::FnDefId<ChalkIr>,
929+
env: &Env,
930+
) -> LowerResult<rust_ir::FnDefDatum<ChalkIr>> {
931+
let binders = env.in_binders(self.all_parameters(), |env| {
932+
let args: LowerResult<_> = self.argument_types.iter().map(|t| t.lower(env)).collect();
933+
let where_clauses = self.lower_where_clauses(env)?;
934+
let return_type = self.return_type.lower(env)?;
935+
936+
Ok(rust_ir::FnDefDatumBound {
937+
argument_types: args?,
938+
where_clauses,
939+
return_type,
940+
})
941+
})?;
942+
943+
let flags = rust_ir::FnDefFlags {};
944+
945+
Ok(rust_ir::FnDefDatum {
946+
id: fn_def_id,
947+
binders,
948+
flags,
949+
})
950+
}
951+
}
952+
853953
trait LowerTraitRef {
854954
fn lower(&self, env: &Env) -> LowerResult<chalk_ir::TraitRef<ChalkIr>>;
855955
}
@@ -1121,6 +1221,22 @@ impl LowerTy for Ty {
11211221
}
11221222
}
11231223
TypeLookup::GenericArg(d) => Ok(chalk_ir::TyData::BoundVar(d).intern(interner)),
1224+
TypeLookup::FnDef(id) => {
1225+
let k = env.fn_def_kind(id);
1226+
if k.binders.len(interner) > 0 {
1227+
Err(RustIrError::IncorrectNumberOfTypeParameters {
1228+
identifier: name.clone(),
1229+
expected: k.binders.len(interner),
1230+
actual: 0,
1231+
})
1232+
} else {
1233+
Ok(chalk_ir::TyData::Function(chalk_ir::Fn {
1234+
num_binders: k.binders.len(interner),
1235+
substitution: chalk_ir::Substitution::empty(interner),
1236+
})
1237+
.intern(interner))
1238+
}
1239+
}
11241240
TypeLookup::Opaque(id) => Ok(chalk_ir::TyData::Alias(chalk_ir::AliasTy::Opaque(
11251241
chalk_ir::OpaqueTy {
11261242
opaque_ty_id: id,
@@ -1157,14 +1273,14 @@ impl LowerTy for Ty {
11571273
.intern(interner)),
11581274

11591275
Ty::Apply { name, ref args } => {
1160-
let id = match env.lookup_type(name)? {
1161-
TypeLookup::Adt(id) => id,
1276+
let (id, k) = match env.lookup_type(name)? {
1277+
TypeLookup::Adt(id) => (id.0, env.adt_kind(id)),
11621278
TypeLookup::GenericArg(_) | TypeLookup::Opaque(_) => {
11631279
Err(RustIrError::CannotApplyTypeParameter(name.clone()))?
11641280
}
1281+
TypeLookup::FnDef(id) => (id.0, env.fn_def_kind(id)),
11651282
};
11661283

1167-
let k = env.adt_kind(id);
11681284
if k.binders.len(interner) != args.len() {
11691285
Err(RustIrError::IncorrectNumberOfTypeParameters {
11701286
identifier: name.clone(),
@@ -1188,11 +1304,18 @@ impl LowerTy for Ty {
11881304
}
11891305
}
11901306

1191-
Ok(chalk_ir::TyData::Apply(chalk_ir::ApplicationTy {
1192-
name: chalk_ir::TypeName::Adt(id),
1193-
substitution,
1194-
})
1195-
.intern(interner))
1307+
match k.sort {
1308+
TypeSort::FnDef => Ok(chalk_ir::TyData::Apply(chalk_ir::ApplicationTy {
1309+
name: chalk_ir::TypeName::FnDef(FnDefId(id)),
1310+
substitution,
1311+
})
1312+
.intern(interner)),
1313+
_ => Ok(chalk_ir::TyData::Apply(chalk_ir::ApplicationTy {
1314+
name: chalk_ir::TypeName::Adt(AdtId(id)),
1315+
substitution,
1316+
})
1317+
.intern(interner)),
1318+
}
11961319
}
11971320

11981321
Ty::Projection { ref proj } => Ok(chalk_ir::TyData::Alias(
@@ -1485,9 +1608,11 @@ impl LowerGoal<LoweredProgram> for Goal {
14851608

14861609
let env = Env {
14871610
adt_ids: &program.adt_ids,
1611+
fn_def_ids: &program.fn_def_ids,
14881612
trait_ids: &program.trait_ids,
14891613
opaque_ty_ids: &program.opaque_ty_ids,
14901614
adt_kinds: &program.adt_kinds,
1615+
fn_def_kinds: &program.fn_def_kinds,
14911616
trait_kinds: &program.trait_kinds,
14921617
associated_ty_lookups: &associated_ty_lookups,
14931618
parameter_map: BTreeMap::new(),

0 commit comments

Comments
 (0)