@@ -24,12 +24,6 @@ pub struct MonoDeferred<'comp, 'pass: 'comp> {
2424
2525 /// If this component should be scheduled, this stores the scheduling type
2626 pub schedule : Option < u64 > ,
27-
28- /// Existential parameter map.
29- /// These are not interned until [Self::sig_complete_mono] as scheduling
30- /// may affect the values of existential parameters.
31- exist_params :
32- SparseInfoMap < ir:: Param , Base < ir:: Expr > , Underlying < ir:: Param > > ,
3327}
3428
3529impl < ' a , ' pass : ' a > MonoDeferred < ' a , ' pass > {
@@ -45,7 +39,6 @@ impl<'a, 'pass: 'a> MonoDeferred<'a, 'pass> {
4539 monosig,
4640 // Set to false if we call `sig_partial_mono` and true once we call `sig_complete_mono`
4741 sig_mono_complete : true ,
48- exist_params : SparseInfoMap :: default ( ) ,
4942 }
5043 }
5144}
@@ -105,12 +98,23 @@ impl MonoDeferred<'_, '_> {
10598
10699 // Insert the existential parameters into the monomorphization
107100 // Also extend the binding with existential parameters
108- for ( param, expr) in self . exist_params . iter ( ) {
101+ let exist_params = self
102+ . monosig
103+ . binding
104+ . iter ( )
105+ . filter ( |( p, _) | self . underlying . get ( * p) . is_existential ( ) )
106+ . copied ( )
107+ . collect_vec ( ) ;
108+
109+ for ( param, expr) in exist_params {
109110 let comp_key = self . monosig . comp_key . clone ( ) ;
110111 let base_comp = self . monosig . base . comp ( ) ;
111- let v = expr. get ( ) . as_concrete ( base_comp) . unwrap ( ) ;
112+ let v = expr. get ( ) . as_concrete ( base_comp) . unwrap_or_else (
113+ || unreachable ! ( "Existential parameter {} was bound to non-constant value {}" , self . underlying. display( param) , base_comp. display( expr. get( ) ) ) ,
114+ ) ;
112115
113116 self . pass . inst_info_mut ( comp_key) . add_exist_val ( param, v) ;
117+ // replace the old binding with this new one
114118 self . monosig . push_binding ( param, v) ;
115119 }
116120
@@ -286,30 +290,20 @@ impl MonoDeferred<'_, '_> {
286290 let ir:: Fact { prop, reason, .. } = fact;
287291
288292 let prop = prop. ul ( ) ;
289- let ( params, _) = self . underlying . relevant_vars ( prop) ;
290293
291- if !params
292- . into_iter ( )
293- . all ( |idx| self . monosig . binding . get ( & idx) . is_some ( ) )
294- {
295- // Discards the assertion if it references parameters that can't be resolved (bundle parameters, etc)
296- // TODO(edmund): Find a better solution to this - we should resolve bundle assertions when bundles are unrolled.
297- None
298- } else {
299- let prop = self . monosig . prop ( & self . underlying , prop, self . pass ) ;
300- let prop = self
301- . monosig
302- . base
303- . resolve_prop ( self . monosig . base . get ( prop) . clone ( ) )
304- . get ( ) ;
294+ let prop = self . monosig . prop ( & self . underlying , prop, self . pass ) ;
295+ // let prop = self
296+ // .monosig
297+ // .base
298+ // .resolve_prop(self.monosig.base.get(prop).clone())
299+ // .get();
305300
306- let reason = reason. ul ( ) ;
307- let reason =
308- self . monosig . info ( & self . underlying , self . pass , reason) . get ( ) ;
301+ let reason = reason. ul ( ) ;
302+ let reason =
303+ self . monosig . info ( & self . underlying , self . pass , reason) . get ( ) ;
309304
310- // After monomorphization, both assumes and asserts become asserts.
311- Some ( ir:: Fact :: assert ( prop, reason) )
312- }
305+ // After monomorphization, both assumes and asserts become asserts.
306+ Some ( ir:: Fact :: assert ( prop. get ( ) , reason) )
313307 }
314308
315309 /// Compile the given command and return the generated command if any.
@@ -380,7 +374,7 @@ impl MonoDeferred<'_, '_> {
380374 let e =
381375 self . monosig . expr ( & self . underlying , expr. ul ( ) , self . pass ) ;
382376
383- self . exist_params . push ( param. ul ( ) , e) ;
377+ self . monosig . binding . push ( param. ul ( ) , e) ;
384378 None
385379 }
386380 // XXX(rachit): We completely get rid of facts in the program here.
0 commit comments