@@ -1250,6 +1250,14 @@ impl<T: HasInterner> Binders<T> {
12501250 Self { binders, value }
12511251 }
12521252
1253+ /// Wraps the given value in a binder without variables, i.e. `for<>
1254+ /// (value)`. Since our deBruijn indices count binders, not variables, this
1255+ /// is sometimes useful.
1256+ pub fn empty ( interner : & T :: Interner , value : T ) -> Self {
1257+ let binders = ParameterKinds :: new ( interner) ;
1258+ Self { binders, value }
1259+ }
1260+
12531261 /// Skips the binder and returns the "bound" value. This is a
12541262 /// risky thing to do because it's easy to get confused about
12551263 /// De Bruijn indices and the like. `skip_binder` is only valid
@@ -1287,6 +1295,20 @@ impl<T: HasInterner> Binders<T> {
12871295 }
12881296 }
12891297
1298+ /// Transforms the inner value according to the given function; returns
1299+ /// `None` if the function returns `None`.
1300+ pub fn filter_map < U , OP > ( self , op : OP ) -> Option < Binders < U > >
1301+ where
1302+ OP : FnOnce ( T ) -> Option < U > ,
1303+ U : HasInterner < Interner = T :: Interner > ,
1304+ {
1305+ let value = op ( self . value ) ?;
1306+ Some ( Binders {
1307+ binders : self . binders ,
1308+ value,
1309+ } )
1310+ }
1311+
12901312 pub fn map_ref < ' a , U , OP > ( & ' a self , op : OP ) -> Binders < U >
12911313 where
12921314 OP : FnOnce ( & ' a T ) -> U ,
@@ -1295,6 +1317,19 @@ impl<T: HasInterner> Binders<T> {
12951317 self . as_ref ( ) . map ( op)
12961318 }
12971319
1320+ /// Creates a `Substitution` containing bound vars such that applying this
1321+ /// substitution will not change the value, i.e. `^0.0, ^0.1, ^0.2` and so
1322+ /// on.
1323+ pub fn identity_substitution ( & self , interner : & T :: Interner ) -> Substitution < T :: Interner > {
1324+ Substitution :: from (
1325+ interner,
1326+ self . binders
1327+ . iter ( interner)
1328+ . enumerate ( )
1329+ . map ( |( i, pk) | ( pk, i) . to_parameter ( interner) ) ,
1330+ )
1331+ }
1332+
12981333 /// Creates a fresh binders that contains a single type
12991334 /// variable. The result of the closure will be embedded in this
13001335 /// binder. Note that you should be careful with what you return
@@ -1317,6 +1352,36 @@ impl<T: HasInterner> Binders<T> {
13171352 }
13181353}
13191354
1355+ impl < T , I > Binders < Binders < T > >
1356+ where
1357+ T : Fold < I , I > + HasInterner < Interner = I > ,
1358+ T :: Result : HasInterner < Interner = I > ,
1359+ I : Interner ,
1360+ {
1361+ /// This turns two levels of binders (`for<A> for<B>`) into one level (`for<A, B>`).
1362+ pub fn fuse_binders ( self , interner : & T :: Interner ) -> Binders < T :: Result > {
1363+ let num_binders = self . len ( interner) ;
1364+ // generate a substitution to shift the indexes of the inner binder:
1365+ let subst = Substitution :: from (
1366+ interner,
1367+ self . value
1368+ . binders
1369+ . iter ( interner)
1370+ . enumerate ( )
1371+ . map ( |( i, pk) | ( pk, i + num_binders) . to_parameter ( interner) ) ,
1372+ ) ;
1373+ let value = self . value . substitute ( interner, & subst) ;
1374+ let binders = ParameterKinds :: from (
1375+ interner,
1376+ self . binders
1377+ . iter ( interner)
1378+ . chain ( self . value . binders . iter ( interner) )
1379+ . cloned ( ) ,
1380+ ) ;
1381+ Binders { binders, value }
1382+ }
1383+ }
1384+
13201385impl < T : HasInterner > From < Binders < T > > for ( ParameterKinds < T :: Interner > , T ) {
13211386 fn from ( binders : Binders < T > ) -> Self {
13221387 ( binders. binders , binders. value )
@@ -2073,6 +2138,40 @@ where
20732138 }
20742139}
20752140
2141+ pub trait ToParameter {
2142+ /// Utility for converting a list of all the binders into scope
2143+ /// into references to those binders. Simply pair the binders with
2144+ /// the indices, and invoke `to_parameter()` on the `(binder,
2145+ /// index)` pair. The result will be a reference to a bound
2146+ /// variable of appropriate kind at the corresponding index.
2147+ fn to_parameter < I : Interner > ( & self , interner : & I ) -> Parameter < I > {
2148+ self . to_parameter_at_depth ( interner, DebruijnIndex :: INNERMOST )
2149+ }
2150+
2151+ fn to_parameter_at_depth < I : Interner > (
2152+ & self ,
2153+ interner : & I ,
2154+ debruijn : DebruijnIndex ,
2155+ ) -> Parameter < I > ;
2156+ }
2157+
2158+ impl < ' a > ToParameter for ( & ' a ParameterKind < ( ) > , usize ) {
2159+ fn to_parameter_at_depth < I : Interner > (
2160+ & self ,
2161+ interner : & I ,
2162+ debruijn : DebruijnIndex ,
2163+ ) -> Parameter < I > {
2164+ let & ( binder, index) = self ;
2165+ let bound_var = BoundVar :: new ( debruijn, index) ;
2166+ match * binder {
2167+ ParameterKind :: Lifetime ( _) => LifetimeData :: BoundVar ( bound_var)
2168+ . intern ( interner)
2169+ . cast ( interner) ,
2170+ ParameterKind :: Ty ( _) => TyData :: BoundVar ( bound_var) . intern ( interner) . cast ( interner) ,
2171+ }
2172+ }
2173+ }
2174+
20762175impl < ' i , I : Interner > Folder < ' i , I > for & SubstFolder < ' i , I > {
20772176 fn as_dyn ( & mut self ) -> & mut dyn Folder < ' i , I > {
20782177 self
0 commit comments