@@ -4,25 +4,30 @@ use crate::{
44} ;
55use fil_ir:: {
66 self as ir, Access , AddCtx , Bind , Component , Connect , Ctx , DenseIndexInfo ,
7- DisplayCtx , Expr , Foreign , InvIdx , Invoke , Liveness , MutCtx , Port , PortIdx ,
8- PortOwner , Range , SparseInfoMap , Subst , Time ,
7+ DisplayCtx , Expr , Foreign , InvIdx , Invoke , Liveness , MutCtx , Param , Port ,
8+ PortIdx , PortOwner , Range , SparseInfoMap , Subst , Time ,
99} ;
1010use fil_utils as utils;
1111use itertools:: Itertools ;
1212use std:: collections:: HashMap ;
1313
14- pub type PortInfo =
15- ( /*lens=*/ Vec < usize > , /*gen_ports=*/ Vec < PortIdx > ) ;
14+ /// A mapping from a bundle with a list of dimensions to the list of generated ports.
15+ type PortInfo = ( /*lens=*/ Vec < usize > , /*gen_ports=*/ Vec < PortIdx > ) ;
16+
17+ /// A multi-dimensional index into a possibly multi-dimensional bundle port).
18+ type BundleIdx = ( PortIdx , Vec < usize > ) ;
1619
1720// Eliminates bundle ports by breaking them into multiple len-1 ports, and eliminates local ports altogether.
1821pub struct BundleElim {
1922 /// Mapping from component to the map from signature bundle port to generated port.
2023 context : DenseIndexInfo < Component , SparseInfoMap < Port , PortInfo > > ,
2124 /// Mapping from index into a dst port to an index of the src port.
22- local_map : HashMap <
23- ( PortIdx , /*idxs=*/ Vec < usize > ) ,
24- ( PortIdx , /*idxs=*/ Vec < usize > ) ,
25- > ,
25+ local_map : HashMap < BundleIdx , BundleIdx > ,
26+ /// Set of bundle-owned parameters.
27+ /// Assertions/Assumptions depending on these parameters must be invalidated
28+ /// For safety, discharge should be run before this pass to make sure none of these
29+ /// propositions fail.
30+ bundle_params : SparseInfoMap < Param , ( ) > ,
2631}
2732
2833impl BundleElim {
@@ -62,7 +67,7 @@ impl BundleElim {
6267 }
6368
6469 /// Compiles a port by breaking it into multiple len-1 ports.
65- fn port ( & self , pidx : PortIdx , comp : & mut Component ) -> PortInfo {
70+ fn port ( & mut self , pidx : PortIdx , comp : & mut Component ) -> PortInfo {
6671 let one = comp. add ( Expr :: Concrete ( 1 ) ) ;
6772 let Port {
6873 owner,
@@ -178,13 +183,14 @@ impl BundleElim {
178183 comp. delete ( pidx) ;
179184 // delete the corresponding parameter
180185 for idx in idxs {
186+ self . bundle_params . push ( idx, ( ) ) ;
181187 comp. delete ( idx) ;
182188 }
183189 ( lens, ports)
184190 }
185191
186192 /// Compiles the signature of a component and adds the new ports to the context mapping.
187- fn sig ( & self , comp : & mut Component ) -> SparseInfoMap < Port , PortInfo > {
193+ fn sig ( & mut self , comp : & mut Component ) -> SparseInfoMap < Port , PortInfo > {
188194 // loop through signature ports and compile them
189195 // Allowing filter_map_bool_then as it erroneously triggers
190196 // due to https://github.com/rust-lang/rust-clippy/issues/11617
@@ -200,7 +206,7 @@ impl BundleElim {
200206 /// Compiles the ports defined by an invocation and adds the new ports to the context mapping.
201207 /// Mutates the invocation in place, redefining its defined ports.
202208 fn inv (
203- & self ,
209+ & mut self ,
204210 idx : InvIdx ,
205211 comp : & mut Component ,
206212 ) -> SparseInfoMap < Port , PortInfo > {
@@ -224,17 +230,20 @@ impl Construct for BundleElim {
224230 let mut visitor = Self {
225231 context : DenseIndexInfo :: default ( ) ,
226232 local_map : HashMap :: new ( ) ,
233+ bundle_params : SparseInfoMap :: default ( ) ,
227234 } ;
228235 // compiles signature ports and adds them to the context
229236 for ( idx, c) in ctx. comps . iter_mut ( ) {
230- visitor. context . push ( idx, visitor. sig ( c) ) ;
237+ let sigmap = visitor. sig ( c) ;
238+ visitor. context . push ( idx, sigmap) ;
231239 }
232240
233241 visitor
234242 }
235243
236244 fn clear_data ( & mut self ) {
237245 self . local_map . clear ( ) ;
246+ self . bundle_params . clear ( ) ;
238247 }
239248}
240249
@@ -295,6 +304,19 @@ impl Visitor for BundleElim {
295304 Action :: Change ( vec ! [ ] )
296305 }
297306
307+ /// Discard all bundle-based assumptions/assertions
308+ fn fact ( & mut self , f : & mut fil_ir:: Fact , data : & mut VisitorData ) -> Action {
309+ let pidx = f. prop ;
310+ let ( params, _) = pidx. relevant_vars ( & data. comp ) ;
311+
312+ if params. into_iter ( ) . any ( |p| self . bundle_params . contains ( p) ) {
313+ // This fact depends on a bundle parameter, so it must be invalidated
314+ Action :: Change ( vec ! [ ] )
315+ } else {
316+ Action :: Continue
317+ }
318+ }
319+
298320 /// Compiles the body of a component and replaces all ports with their expanded versions.
299321 fn start ( & mut self , data : & mut VisitorData ) -> Action {
300322 let comp = & mut data. comp ;
0 commit comments