diff --git a/src/extension/infer.rs b/src/extension/infer.rs index 856681adf..759c3dde5 100644 --- a/src/extension/infer.rs +++ b/src/extension/infer.rs @@ -687,7 +687,7 @@ impl UnificationContext { }); let (rs, other_ms): (Vec<_>, Vec<_>) = plus_constraints.unzip(); - let solution = rs.iter().fold(ExtensionSet::new(), |e1, e2| e1.union(e2)); + let solution = rs.iter().fold(ExtensionSet::new(), ExtensionSet::union); let unresolved_metas = other_ms .into_iter() .filter(|other_m| m != *other_m) @@ -705,9 +705,8 @@ impl UnificationContext { println!("{:?}", relations.node_map); println!("{:?}", relations.graph); - // Process the strongly-connected components. We need to deal with these - // depended-upon before depender. ccs() gives them back in some order - // - this might need to be reversed???? + // Process the strongly-connected components. petgraph/sccs() returns these + // depended-upon before dependant, as we need. for cc in relations.sccs() { // Strongly connected components are looping constraint dependencies. // This means that each metavariable in the CC has the same solution. @@ -1664,22 +1663,36 @@ mod test { // Test that logic for dealing with self-referential constraints doesn't // fall over when a self-referencing group of metas also references a meta // outside the group - fn failing_sccs_test() { + fn sccs() { let hugr = Hugr::default(); let mut ctx = UnificationContext::new(&hugr); + // Make a strongly-connected component (loop) let m1 = ctx.fresh_meta(); let m2 = ctx.fresh_meta(); let m3 = ctx.fresh_meta(); - // Outside of the connected component - let m_other = ctx.fresh_meta(); - // These 3 metavariables form a loop ctx.add_constraint(m1, Constraint::Plus(ExtensionSet::singleton(&A), m3)); - ctx.add_constraint(m2, Constraint::Plus(ExtensionSet::singleton(&A), m1)); + ctx.add_constraint(m2, Constraint::Plus(ExtensionSet::singleton(&B), m1)); ctx.add_constraint(m3, Constraint::Plus(ExtensionSet::singleton(&A), m2)); - // This other meta is outside the loop, but depended on by one of the loop metas - ctx.add_constraint(m2, Constraint::Plus(ExtensionSet::singleton(&A), m_other)); + // And a second scc + let m4 = ctx.fresh_meta(); + let m5 = ctx.fresh_meta(); + ctx.add_constraint(m4, Constraint::Plus(ExtensionSet::singleton(&C), m5)); + ctx.add_constraint(m5, Constraint::Plus(ExtensionSet::singleton(&C), m4)); + // Make second component depend upon first + ctx.add_constraint( + m4, + Constraint::Plus(ExtensionSet::singleton(&UNKNOWN_EXTENSION), m3), + ); ctx.variables.insert(m1); - ctx.variables.insert(m_other); + ctx.variables.insert(m4); ctx.instantiate_variables(); + assert_eq!( + ctx.get_solution(&m1), + Some(&ExtensionSet::from_iter([A, B])) + ); + assert_eq!( + ctx.get_solution(&m4), + Some(&ExtensionSet::from_iter([A, B, C, UNKNOWN_EXTENSION])) + ); } }