@@ -2,7 +2,7 @@ use crate::interner::ChalkIr;
2
2
use chalk_ir:: cast:: { Cast , Caster } ;
3
3
use chalk_ir:: interner:: HasInterner ;
4
4
use chalk_ir:: {
5
- self , AdtId , AssocTypeId , BoundVar , ClausePriority , DebruijnIndex , ImplId , OpaqueTyId ,
5
+ self , AdtId , AssocTypeId , BoundVar , ClausePriority , DebruijnIndex , FnDefId , ImplId , OpaqueTyId ,
6
6
QuantifiedWhereClauses , Substitution , ToGenericArg , TraitId ,
7
7
} ;
8
8
use chalk_parse:: ast:: * ;
@@ -19,9 +19,11 @@ use crate::program::Program as LoweredProgram;
19
19
use crate :: { Identifier as Ident , RawId , TypeKind , TypeSort } ;
20
20
21
21
type AdtIds = BTreeMap < Ident , chalk_ir:: AdtId < ChalkIr > > ;
22
+ type FnDefIds = BTreeMap < Ident , chalk_ir:: FnDefId < ChalkIr > > ;
22
23
type TraitIds = BTreeMap < Ident , chalk_ir:: TraitId < ChalkIr > > ;
23
24
type OpaqueTyIds = BTreeMap < Ident , chalk_ir:: OpaqueTyId < ChalkIr > > ;
24
25
type AdtKinds = BTreeMap < chalk_ir:: AdtId < ChalkIr > , TypeKind > ;
26
+ type FnDefKinds = BTreeMap < chalk_ir:: FnDefId < ChalkIr > , TypeKind > ;
25
27
type TraitKinds = BTreeMap < chalk_ir:: TraitId < ChalkIr > , TypeKind > ;
26
28
type AssociatedTyLookups = BTreeMap < ( chalk_ir:: TraitId < ChalkIr > , Ident ) , AssociatedTyLookup > ;
27
29
type AssociatedTyValueIds =
@@ -36,6 +38,8 @@ pub type LowerResult<T> = Result<T, RustIrError>;
36
38
struct Env < ' k > {
37
39
adt_ids : & ' k AdtIds ,
38
40
adt_kinds : & ' k AdtKinds ,
41
+ fn_def_ids : & ' k FnDefIds ,
42
+ fn_def_kinds : & ' k FnDefKinds ,
39
43
trait_ids : & ' k TraitIds ,
40
44
trait_kinds : & ' k TraitKinds ,
41
45
opaque_ty_ids : & ' k OpaqueTyIds ,
@@ -73,6 +77,7 @@ struct AssociatedTyLookup {
73
77
enum TypeLookup {
74
78
Adt ( chalk_ir:: AdtId < ChalkIr > ) ,
75
79
GenericArg ( BoundVar ) ,
80
+ FnDef ( chalk_ir:: FnDefId < ChalkIr > ) ,
76
81
Opaque ( chalk_ir:: OpaqueTyId < ChalkIr > ) ,
77
82
}
78
83
@@ -96,6 +101,10 @@ impl<'k> Env<'k> {
96
101
return Ok ( TypeLookup :: Adt ( * id) ) ;
97
102
}
98
103
104
+ if let Some ( id) = self . fn_def_ids . get ( & name. str ) {
105
+ return Ok ( TypeLookup :: FnDef ( * id) ) ;
106
+ }
107
+
99
108
if let Some ( id) = self . opaque_ty_ids . get ( & name. str ) {
100
109
return Ok ( TypeLookup :: Opaque ( * id) ) ;
101
110
}
@@ -140,6 +149,10 @@ impl<'k> Env<'k> {
140
149
& self . adt_kinds [ & id]
141
150
}
142
151
152
+ fn fn_def_kind ( & self , id : chalk_ir:: FnDefId < ChalkIr > ) -> & TypeKind {
153
+ & self . fn_def_kinds [ & id]
154
+ }
155
+
143
156
fn trait_kind ( & self , id : chalk_ir:: TraitId < ChalkIr > ) -> & TypeKind {
144
157
& self . trait_kinds [ & id]
145
158
}
@@ -240,9 +253,11 @@ impl LowerProgram for Program {
240
253
}
241
254
242
255
let mut adt_ids = BTreeMap :: new ( ) ;
256
+ let mut fn_def_ids = BTreeMap :: new ( ) ;
243
257
let mut trait_ids = BTreeMap :: new ( ) ;
244
258
let mut opaque_ty_ids = BTreeMap :: new ( ) ;
245
259
let mut adt_kinds = BTreeMap :: new ( ) ;
260
+ let mut fn_def_kinds = BTreeMap :: new ( ) ;
246
261
let mut trait_kinds = BTreeMap :: new ( ) ;
247
262
let mut opaque_ty_kinds = BTreeMap :: new ( ) ;
248
263
let mut object_safe_traits = HashSet :: new ( ) ;
@@ -254,6 +269,12 @@ impl LowerProgram for Program {
254
269
adt_ids. insert ( type_kind. name . clone ( ) , id) ;
255
270
adt_kinds. insert ( id, type_kind) ;
256
271
}
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
+ }
257
278
Item :: TraitDefn ( defn) => {
258
279
let type_kind = defn. lower_type_kind ( ) ?;
259
280
let id = TraitId ( raw_id) ;
@@ -276,6 +297,7 @@ impl LowerProgram for Program {
276
297
}
277
298
278
299
let mut adt_data = BTreeMap :: new ( ) ;
300
+ let mut fn_def_data = BTreeMap :: new ( ) ;
279
301
let mut trait_data = BTreeMap :: new ( ) ;
280
302
let mut well_known_traits = BTreeMap :: new ( ) ;
281
303
let mut impl_data = BTreeMap :: new ( ) ;
@@ -287,6 +309,8 @@ impl LowerProgram for Program {
287
309
let empty_env = Env {
288
310
adt_ids : & adt_ids,
289
311
adt_kinds : & adt_kinds,
312
+ fn_def_ids : & fn_def_ids,
313
+ fn_def_kinds : & fn_def_kinds,
290
314
trait_ids : & trait_ids,
291
315
trait_kinds : & trait_kinds,
292
316
opaque_ty_ids : & opaque_ty_ids,
@@ -299,6 +323,13 @@ impl LowerProgram for Program {
299
323
let adt_id = AdtId ( raw_id) ;
300
324
adt_data. insert ( adt_id, Arc :: new ( d. lower_adt ( adt_id, & empty_env) ?) ) ;
301
325
}
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
+ }
302
333
Item :: TraitDefn ( ref trait_defn) => {
303
334
let trait_id = TraitId ( raw_id) ;
304
335
let trait_datum = trait_defn. lower_trait ( trait_id, & empty_env) ?;
@@ -454,10 +485,13 @@ impl LowerProgram for Program {
454
485
455
486
let program = LoweredProgram {
456
487
adt_ids,
488
+ fn_def_ids,
457
489
trait_ids,
458
490
adt_kinds,
491
+ fn_def_kinds,
459
492
trait_kinds,
460
493
adt_data,
494
+ fn_def_data,
461
495
trait_data,
462
496
well_known_traits,
463
497
impl_data,
@@ -538,6 +572,16 @@ impl LowerParameterMap for StructDefn {
538
572
}
539
573
}
540
574
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
+
541
585
impl LowerParameterMap for Impl {
542
586
fn synthetic_parameters ( & self ) -> Option < NamedGenericArg > {
543
587
None
@@ -631,6 +675,26 @@ impl LowerTypeKind for StructDefn {
631
675
}
632
676
}
633
677
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
+
634
698
impl LowerWhereClauses for StructDefn {
635
699
fn where_clauses ( & self ) -> & [ QuantifiedWhereClause ] {
636
700
& self . where_clauses
@@ -850,6 +914,39 @@ impl LowerAdtDefn for StructDefn {
850
914
}
851
915
}
852
916
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
+ Ok ( rust_ir:: FnDefDatum {
944
+ id : fn_def_id,
945
+ binders,
946
+ } )
947
+ }
948
+ }
949
+
853
950
trait LowerTraitRef {
854
951
fn lower ( & self , env : & Env ) -> LowerResult < chalk_ir:: TraitRef < ChalkIr > > ;
855
952
}
@@ -1121,6 +1218,22 @@ impl LowerTy for Ty {
1121
1218
}
1122
1219
}
1123
1220
TypeLookup :: GenericArg ( d) => Ok ( chalk_ir:: TyData :: BoundVar ( d) . intern ( interner) ) ,
1221
+ TypeLookup :: FnDef ( id) => {
1222
+ let k = env. fn_def_kind ( id) ;
1223
+ if k. binders . len ( interner) > 0 {
1224
+ Err ( RustIrError :: IncorrectNumberOfTypeParameters {
1225
+ identifier : name. clone ( ) ,
1226
+ expected : k. binders . len ( interner) ,
1227
+ actual : 0 ,
1228
+ } )
1229
+ } else {
1230
+ Ok ( chalk_ir:: TyData :: Function ( chalk_ir:: Fn {
1231
+ num_binders : k. binders . len ( interner) ,
1232
+ substitution : chalk_ir:: Substitution :: empty ( interner) ,
1233
+ } )
1234
+ . intern ( interner) )
1235
+ }
1236
+ }
1124
1237
TypeLookup :: Opaque ( id) => Ok ( chalk_ir:: TyData :: Alias ( chalk_ir:: AliasTy :: Opaque (
1125
1238
chalk_ir:: OpaqueTy {
1126
1239
opaque_ty_id : id,
@@ -1157,14 +1270,14 @@ impl LowerTy for Ty {
1157
1270
. intern ( interner) ) ,
1158
1271
1159
1272
Ty :: Apply { name, ref args } => {
1160
- let id = match env. lookup_type ( name) ? {
1161
- TypeLookup :: Adt ( id) => id ,
1273
+ let ( id , k ) = match env. lookup_type ( name) ? {
1274
+ TypeLookup :: Adt ( id) => ( id . 0 , env . adt_kind ( id ) ) ,
1162
1275
TypeLookup :: GenericArg ( _) | TypeLookup :: Opaque ( _) => {
1163
1276
Err ( RustIrError :: CannotApplyTypeParameter ( name. clone ( ) ) ) ?
1164
1277
}
1278
+ TypeLookup :: FnDef ( id) => ( id. 0 , env. fn_def_kind ( id) ) ,
1165
1279
} ;
1166
1280
1167
- let k = env. adt_kind ( id) ;
1168
1281
if k. binders . len ( interner) != args. len ( ) {
1169
1282
Err ( RustIrError :: IncorrectNumberOfTypeParameters {
1170
1283
identifier : name. clone ( ) ,
@@ -1188,11 +1301,18 @@ impl LowerTy for Ty {
1188
1301
}
1189
1302
}
1190
1303
1191
- Ok ( chalk_ir:: TyData :: Apply ( chalk_ir:: ApplicationTy {
1192
- name : chalk_ir:: TypeName :: Adt ( id) ,
1193
- substitution,
1194
- } )
1195
- . intern ( interner) )
1304
+ match k. sort {
1305
+ TypeSort :: FnDef => Ok ( chalk_ir:: TyData :: Apply ( chalk_ir:: ApplicationTy {
1306
+ name : chalk_ir:: TypeName :: FnDef ( FnDefId ( id) ) ,
1307
+ substitution,
1308
+ } )
1309
+ . intern ( interner) ) ,
1310
+ _ => Ok ( chalk_ir:: TyData :: Apply ( chalk_ir:: ApplicationTy {
1311
+ name : chalk_ir:: TypeName :: Adt ( AdtId ( id) ) ,
1312
+ substitution,
1313
+ } )
1314
+ . intern ( interner) ) ,
1315
+ }
1196
1316
}
1197
1317
1198
1318
Ty :: Projection { ref proj } => Ok ( chalk_ir:: TyData :: Alias (
@@ -1485,9 +1605,11 @@ impl LowerGoal<LoweredProgram> for Goal {
1485
1605
1486
1606
let env = Env {
1487
1607
adt_ids : & program. adt_ids ,
1608
+ fn_def_ids : & program. fn_def_ids ,
1488
1609
trait_ids : & program. trait_ids ,
1489
1610
opaque_ty_ids : & program. opaque_ty_ids ,
1490
1611
adt_kinds : & program. adt_kinds ,
1612
+ fn_def_kinds : & program. fn_def_kinds ,
1491
1613
trait_kinds : & program. trait_kinds ,
1492
1614
associated_ty_lookups : & associated_ty_lookups,
1493
1615
parameter_map : BTreeMap :: new ( ) ,
0 commit comments