Module search_graph

Modules

global_cache 🔒

Structs

AvailableDepth 🔒

CycleHeads 🔒

All cycle heads a given goal depends on, ordered by their stack depth.

GlobalCache

NestedGoals 🔒

The nested goals of each stack entry and the path from the stack entry to that nested goal.

PathsToNested

Tracks how nested goals have been accessed. This is necessary to disable global cache entries if computing them would otherwise result in a cycle or access a provisional cache entry.

ProvisionalCacheEntry 🔒

A provisional result of an already computed goals which depends on other goals still on the stack.

SearchGraph

StackDepth

StackEntry 🔒

Stack entries of the evaluation stack. Its fields tend to be lazily when popping a child goal or completely immutable.

Enums

AllPathsToHeadCoinductive

For each goal we track whether the paths from this goal to its cycle heads are coinductive.

PathKind

In the initial iteration of a cycle, we do not yet have a provisional result. In the case we return an initial provisional result depending on the kind of cycle.

UpdateParentGoalCtxt 🔒

While SearchGraph::update_parent_goal can be mostly shared between ordinary nested goals/global cache hits and provisional cache hits, using the provisional cache should not add any nested goals.

UsageKind

The kinds of cycles a cycle head was involved in.

Traits

Cx

The search graph does not simply use Interner directly to enable its fuzzing without having to stub the rest of the interner. We don’t make this a super trait of Interner as users of the shared type library shouldn’t have to care about Input and Result as they are implementation details of the search graph.

Delegate