@@ -118,52 +118,49 @@ impl Env<'_> {
118
118
}
119
119
} ;
120
120
121
- if let Ok ( lookup) = self . lookup_apply_type ( name) {
122
- match lookup {
123
- ApplyTypeLookup :: Param ( p) => {
124
- let b = p. skip_kind ( ) ;
125
- match & p. kind {
126
- chalk_ir:: VariableKind :: Ty ( _) => Ok ( chalk_ir:: TyData :: BoundVar ( * b)
127
- . intern ( interner)
128
- . cast ( interner) ) ,
129
- chalk_ir:: VariableKind :: Lifetime => {
130
- Ok ( chalk_ir:: LifetimeData :: BoundVar ( * b)
131
- . intern ( interner)
132
- . cast ( interner) )
133
- }
134
- chalk_ir:: VariableKind :: Const ( ty) => {
135
- Ok ( b. to_const ( interner, ty. clone ( ) ) . cast ( interner) )
136
- }
121
+ match self . lookup_apply_type ( name) {
122
+ Ok ( ApplyTypeLookup :: Param ( p) ) => {
123
+ let b = p. skip_kind ( ) ;
124
+ match & p. kind {
125
+ chalk_ir:: VariableKind :: Ty ( _) => Ok ( chalk_ir:: TyData :: BoundVar ( * b)
126
+ . intern ( interner)
127
+ . cast ( interner) ) ,
128
+ chalk_ir:: VariableKind :: Lifetime => Ok ( chalk_ir:: LifetimeData :: BoundVar ( * b)
129
+ . intern ( interner)
130
+ . cast ( interner) ) ,
131
+ chalk_ir:: VariableKind :: Const ( ty) => {
132
+ Ok ( b. to_const ( interner, ty. clone ( ) ) . cast ( interner) )
137
133
}
138
134
}
139
- ApplyTypeLookup :: Adt ( id) => apply ( self . adt_kind ( id) , chalk_ir:: TypeName :: Adt ( id) ) ,
140
- ApplyTypeLookup :: FnDef ( id) => {
141
- apply ( self . fn_def_kind ( id) , chalk_ir:: TypeName :: FnDef ( id) )
142
- }
143
- ApplyTypeLookup :: Closure ( id) => {
144
- apply ( self . closure_kind ( id) , chalk_ir:: TypeName :: Closure ( id) )
145
- }
146
- ApplyTypeLookup :: Opaque ( id) => Ok ( chalk_ir:: TyData :: Alias (
147
- chalk_ir:: AliasTy :: Opaque ( chalk_ir:: OpaqueTy {
148
- opaque_ty_id : id,
149
- substitution : chalk_ir:: Substitution :: empty ( interner) ,
150
- } ) ,
151
- )
152
- . intern ( interner)
153
- . cast ( interner) ) ,
154
135
}
155
- } else {
156
- if let Some ( id) = self . foreign_ty_ids . get ( & name. str ) {
157
- Ok ( chalk_ir:: TyData :: Apply ( chalk_ir:: ApplicationTy {
158
- name : chalk_ir:: TypeName :: Foreign ( * id) ,
136
+ Ok ( ApplyTypeLookup :: Adt ( id) ) => apply ( self . adt_kind ( id) , chalk_ir:: TypeName :: Adt ( id) ) ,
137
+ Ok ( ApplyTypeLookup :: FnDef ( id) ) => {
138
+ apply ( self . fn_def_kind ( id) , chalk_ir:: TypeName :: FnDef ( id) )
139
+ }
140
+ Ok ( ApplyTypeLookup :: Closure ( id) ) => {
141
+ apply ( self . closure_kind ( id) , chalk_ir:: TypeName :: Closure ( id) )
142
+ }
143
+ Ok ( ApplyTypeLookup :: Opaque ( id) ) => Ok ( chalk_ir:: TyData :: Alias (
144
+ chalk_ir:: AliasTy :: Opaque ( chalk_ir:: OpaqueTy {
145
+ opaque_ty_id : id,
159
146
substitution : chalk_ir:: Substitution :: empty ( interner) ,
160
- } )
161
- . intern ( interner)
162
- . cast ( interner) )
163
- } else if let Some ( _) = self . trait_ids . get ( & name. str ) {
164
- Err ( RustIrError :: NotStruct ( name. clone ( ) ) )
165
- } else {
166
- Err ( RustIrError :: InvalidParameterName ( name. clone ( ) ) )
147
+ } ) ,
148
+ )
149
+ . intern ( interner)
150
+ . cast ( interner) ) ,
151
+ Err ( _) => {
152
+ if let Some ( id) = self . foreign_ty_ids . get ( & name. str ) {
153
+ Ok ( chalk_ir:: TyData :: Apply ( chalk_ir:: ApplicationTy {
154
+ name : chalk_ir:: TypeName :: Foreign ( * id) ,
155
+ substitution : chalk_ir:: Substitution :: empty ( interner) ,
156
+ } )
157
+ . intern ( interner)
158
+ . cast ( interner) )
159
+ } else if let Some ( _) = self . trait_ids . get ( & name. str ) {
160
+ Err ( RustIrError :: NotStruct ( name. clone ( ) ) )
161
+ } else {
162
+ Err ( RustIrError :: InvalidParameterName ( name. clone ( ) ) )
163
+ }
167
164
}
168
165
}
169
166
}
@@ -343,47 +340,29 @@ pub fn lower_program(program: &Program) -> LowerResult<LoweredProgram> {
343
340
let mut opaque_ty_kinds = BTreeMap :: new ( ) ;
344
341
let mut object_safe_traits = HashSet :: new ( ) ;
345
342
346
- macro_rules! lower_type_kind {
347
- ( $self: ident, $sort: ident, $params: expr) => {
348
- Ok ( TypeKind {
349
- sort: TypeSort :: $sort,
350
- name: $self. name. str . clone( ) ,
351
- binders: chalk_ir:: Binders :: new(
352
- VariableKinds :: from_iter( & ChalkIr , $params. anonymize( ) ) ,
353
- crate :: Unit ,
354
- ) ,
355
- } )
356
- } ;
357
- }
358
-
359
343
for ( item, & raw_id) in program. items . iter ( ) . zip ( & raw_ids) {
360
344
match item {
361
345
Item :: AdtDefn ( defn) => {
362
- let type_kind = lower_type_kind ! ( defn, Adt , defn . all_parameters ( ) ) ?;
346
+ let type_kind = defn. lower_type_kind ( ) ?;
363
347
let id = AdtId ( raw_id) ;
364
348
adt_ids. insert ( type_kind. name . clone ( ) , id) ;
365
349
adt_kinds. insert ( id, type_kind) ;
366
350
}
367
351
Item :: FnDefn ( defn) => {
368
- let type_kind = lower_type_kind ! ( defn, FnDef , defn . all_parameters ( ) ) ?;
352
+ let type_kind = defn. lower_type_kind ( ) ?;
369
353
let id = FnDefId ( raw_id) ;
370
354
fn_def_ids. insert ( type_kind. name . clone ( ) , id) ;
371
355
fn_def_kinds. insert ( id, type_kind) ;
372
356
fn_def_abis. insert ( id, lower_fn_abi ( & defn. sig . abi ) ?) ;
373
357
}
374
358
Item :: ClosureDefn ( defn) => {
375
- let type_kind = lower_type_kind ! ( defn, Closure , defn . all_parameters ( ) ) ?;
359
+ let type_kind = defn. lower_type_kind ( ) ?;
376
360
let id = ClosureId ( raw_id) ;
377
361
closure_ids. insert ( defn. name . str . clone ( ) , id) ;
378
362
closure_kinds. insert ( id, type_kind) ;
379
363
}
380
364
Item :: TraitDefn ( defn) => {
381
- let variable_kinds = defn
382
- . variable_kinds
383
- . iter ( )
384
- . map ( lower_variable_kind)
385
- . collect :: < Vec < _ > > ( ) ;
386
- let type_kind = lower_type_kind ! ( defn, Trait , variable_kinds) ?;
365
+ let type_kind = defn. lower_type_kind ( ) ?;
387
366
let id = TraitId ( raw_id) ;
388
367
trait_ids. insert ( type_kind. name . clone ( ) , id) ;
389
368
trait_kinds. insert ( id, type_kind) ;
@@ -394,12 +373,7 @@ pub fn lower_program(program: &Program) -> LowerResult<LoweredProgram> {
394
373
}
395
374
}
396
375
Item :: OpaqueTyDefn ( defn) => {
397
- let variable_kinds = defn
398
- . variable_kinds
399
- . iter ( )
400
- . map ( lower_variable_kind)
401
- . collect :: < Vec < _ > > ( ) ;
402
- let type_kind = lower_type_kind ! ( defn, Opaque , variable_kinds) ?;
376
+ let type_kind = defn. lower_type_kind ( ) ?;
403
377
let id = OpaqueTyId ( raw_id) ;
404
378
opaque_ty_ids. insert ( defn. name . str . clone ( ) , id) ;
405
379
opaque_ty_kinds. insert ( id, type_kind) ;
@@ -735,6 +709,42 @@ lower_param_map!(
735
709
) )
736
710
) ;
737
711
712
+ trait LowerTypeKind {
713
+ fn lower_type_kind ( & self ) -> LowerResult < TypeKind > ;
714
+ }
715
+
716
+ macro_rules! lower_type_kind {
717
+ ( $type: ident, $sort: ident, $params: expr) => {
718
+ impl LowerTypeKind for $type {
719
+ fn lower_type_kind( & self ) -> LowerResult <TypeKind > {
720
+ Ok ( TypeKind {
721
+ sort: TypeSort :: $sort,
722
+ name: self . name. str . clone( ) ,
723
+ binders: chalk_ir:: Binders :: new(
724
+ VariableKinds :: from_iter( & ChalkIr , $params( self ) . anonymize( ) ) ,
725
+ crate :: Unit ,
726
+ ) ,
727
+ } )
728
+ }
729
+ }
730
+ } ;
731
+ }
732
+
733
+ lower_type_kind ! ( AdtDefn , Adt , |defn: & AdtDefn | defn. all_parameters( ) ) ;
734
+ lower_type_kind ! ( FnDefn , FnDef , |defn: & FnDefn | defn. all_parameters( ) ) ;
735
+ lower_type_kind ! ( ClosureDefn , Closure , |defn: & ClosureDefn | defn
736
+ . all_parameters( ) ) ;
737
+ lower_type_kind ! ( TraitDefn , Trait , |defn: & TraitDefn | defn
738
+ . variable_kinds
739
+ . iter( )
740
+ . map( lower_variable_kind)
741
+ . collect:: <Vec <_>>( ) ) ;
742
+ lower_type_kind ! ( OpaqueTyDefn , Opaque , |defn: & OpaqueTyDefn | defn
743
+ . variable_kinds
744
+ . iter( )
745
+ . map( lower_variable_kind)
746
+ . collect:: <Vec <_>>( ) ) ;
747
+
738
748
fn get_type_of_u32 ( ) -> chalk_ir:: Ty < ChalkIr > {
739
749
chalk_ir:: ApplicationTy {
740
750
name : chalk_ir:: TypeName :: Scalar ( chalk_ir:: Scalar :: Uint ( chalk_ir:: UintTy :: U32 ) ) ,
@@ -1713,7 +1723,10 @@ impl Lower for Goal {
1713
1723
// `if (FromEnv(T: Trait)) { ... /* this part is untouched */ ... }`.
1714
1724
let where_clauses = hyp
1715
1725
. iter ( )
1716
- . flat_map ( |clause| apply_result ( clause. lower ( env) ) )
1726
+ . flat_map ( |clause| match clause. lower ( env) {
1727
+ Ok ( v) => v. into_iter ( ) . map ( Ok ) . collect ( ) ,
1728
+ Err ( e) => vec ! [ Err ( e) ] ,
1729
+ } )
1717
1730
. map ( |result| result. map ( |h| h. into_from_env_clause ( interner) ) ) ;
1718
1731
let where_clauses =
1719
1732
chalk_ir:: ProgramClauses :: from_fallible ( interner, where_clauses) ;
@@ -1752,13 +1765,6 @@ fn lower_quantified(
1752
1765
Ok ( chalk_ir:: GoalData :: Quantified ( quantifier_kind, subgoal) . intern ( interner) )
1753
1766
}
1754
1767
1755
- fn apply_result < T > ( result : LowerResult < Vec < T > > ) -> Vec < LowerResult < T > > {
1756
- match result {
1757
- Ok ( v) => v. into_iter ( ) . map ( Ok ) . collect ( ) ,
1758
- Err ( e) => vec ! [ Err ( e) ] ,
1759
- }
1760
- }
1761
-
1762
1768
fn lower_well_known_trait ( well_known_trait : WellKnownTrait ) -> rust_ir:: WellKnownTrait {
1763
1769
match well_known_trait {
1764
1770
WellKnownTrait :: Sized => rust_ir:: WellKnownTrait :: Sized ,
0 commit comments