cycle_participants to nested_goals

This commit is contained in:
lcnr 2024-07-09 09:39:13 +02:00
parent e38109d7f0
commit dd175feb25

View file

@ -71,7 +71,7 @@ struct StackEntry<I: Interner> {
/// C :- D /// C :- D
/// D :- C /// D :- C
/// ``` /// ```
cycle_participants: HashSet<CanonicalInput<I>>, nested_goals: HashSet<CanonicalInput<I>>,
/// Starts out as `None` and gets set when rerunning this /// Starts out as `None` and gets set when rerunning this
/// goal in case we encounter a cycle. /// goal in case we encounter a cycle.
provisional_result: Option<QueryResult<I>>, provisional_result: Option<QueryResult<I>>,
@ -215,8 +215,8 @@ impl<I: Interner> SearchGraph<I> {
let current_cycle_root = &mut stack[current_root.as_usize()]; let current_cycle_root = &mut stack[current_root.as_usize()];
for entry in cycle_participants { for entry in cycle_participants {
entry.non_root_cycle_participant = entry.non_root_cycle_participant.max(Some(head)); entry.non_root_cycle_participant = entry.non_root_cycle_participant.max(Some(head));
current_cycle_root.cycle_participants.insert(entry.input); current_cycle_root.nested_goals.insert(entry.input);
current_cycle_root.cycle_participants.extend(mem::take(&mut entry.cycle_participants)); current_cycle_root.nested_goals.extend(mem::take(&mut entry.nested_goals));
} }
} }
@ -335,7 +335,7 @@ impl<I: Interner> SearchGraph<I> {
non_root_cycle_participant: None, non_root_cycle_participant: None,
encountered_overflow: false, encountered_overflow: false,
has_been_used: HasBeenUsed::empty(), has_been_used: HasBeenUsed::empty(),
cycle_participants: Default::default(), nested_goals: Default::default(),
provisional_result: None, provisional_result: None,
}; };
assert_eq!(self.stack.push(entry), depth); assert_eq!(self.stack.push(entry), depth);
@ -389,7 +389,7 @@ impl<I: Interner> SearchGraph<I> {
// //
// We must not use the global cache entry of a root goal if a cycle // We must not use the global cache entry of a root goal if a cycle
// participant is on the stack. This is necessary to prevent unstable // participant is on the stack. This is necessary to prevent unstable
// results. See the comment of `StackEntry::cycle_participants` for // results. See the comment of `StackEntry::nested_goals` for
// more details. // more details.
self.global_cache(cx).insert( self.global_cache(cx).insert(
cx, cx,
@ -397,7 +397,7 @@ impl<I: Interner> SearchGraph<I> {
proof_tree, proof_tree,
reached_depth, reached_depth,
final_entry.encountered_overflow, final_entry.encountered_overflow,
final_entry.cycle_participants, final_entry.nested_goals,
dep_node, dep_node,
result, result,
) )
@ -544,27 +544,27 @@ impl<I: Interner> SearchGraph<I> {
non_root_cycle_participant, non_root_cycle_participant,
encountered_overflow: _, encountered_overflow: _,
has_been_used, has_been_used,
ref cycle_participants, ref nested_goals,
provisional_result, provisional_result,
} = *entry; } = *entry;
let cache_entry = provisional_cache.get(&entry.input).unwrap(); let cache_entry = provisional_cache.get(&entry.input).unwrap();
assert_eq!(cache_entry.stack_depth, Some(depth)); assert_eq!(cache_entry.stack_depth, Some(depth));
if let Some(head) = non_root_cycle_participant { if let Some(head) = non_root_cycle_participant {
assert!(head < depth); assert!(head < depth);
assert!(cycle_participants.is_empty()); assert!(nested_goals.is_empty());
assert_ne!(stack[head].has_been_used, HasBeenUsed::empty()); assert_ne!(stack[head].has_been_used, HasBeenUsed::empty());
let mut current_root = head; let mut current_root = head;
while let Some(parent) = stack[current_root].non_root_cycle_participant { while let Some(parent) = stack[current_root].non_root_cycle_participant {
current_root = parent; current_root = parent;
} }
assert!(stack[current_root].cycle_participants.contains(&input)); assert!(stack[current_root].nested_goals.contains(&input));
} }
if !cycle_participants.is_empty() { if !nested_goals.is_empty() {
assert!(provisional_result.is_some() || !has_been_used.is_empty()); assert!(provisional_result.is_some() || !has_been_used.is_empty());
for entry in stack.iter().take(depth.as_usize()) { for entry in stack.iter().take(depth.as_usize()) {
assert_eq!(cycle_participants.get(&entry.input), None); assert_eq!(nested_goals.get(&entry.input), None);
} }
} }
} }