PrivateacyclicWhether the last work list to settle left the pins acyclic, which is what lets hasCycle start from the groups a run touched rather than from every group there is. Cleared by a run that gives up halfway, since the constraints it did establish may have closed a cycle nothing went on to check.
false is not known to be acyclic, never cyclic. Nothing reads it as an answer: all it decides is
where hasCycle starts from, so being wrong about it the safe way costs a walk of every group
and nothing else.
ProtectedcleanCounter for generating unique group IDs
ProtectedgroupA history of oldGroups (keys) that got merged into newGroups (values). Needed to dereference removed groups still used in a pin.
ProtectedgroupMaps group ID to what the group is pinned to (if anything) - read through pinOf.
ProtectedgroupMaps group ID to the term types its value may have - read through rangeOf.
ProtectedgroupMaps group ID to the values in it - read through valuesOf and groupEntries.
Protected ReadonlymeetMeets the two pins a group is asked to carry at once, reporting false when no value
satisfies both
PrivatepinThe reverse of childrenOf, keyed by resolved group: the groups whose shape holds this one in one of its positions. It is what isPinChild reads instead of walking every pin there is, that question being asked on every ClusterSet.remove.
Kept as an over-approximation the lookup verifies against the pins themselves, so that the only thing maintenance owes it is never to lose an owner: entries move with the group they are keyed by (migrateGroupData) and are dropped with it (dropGroup), while an owner whose pin has moved on is pruned the next time it is read.
Protected ReadonlytoProtectedvalueMaps a value to the group it is in - read through groupOf.
The state the set is in, as a stamp that no two states of any two sets share.
Every method that writes anything moves it on (touch), so a memo taken off the set is valid for exactly as long as this is what it was taken at - which is a check the memo cannot forget to make, there being nothing to invalidate.
Gives a group the shape of a triple term, creating an anonymous group per position where it has none.
The group to shape
the group per position, or false when the group cannot hold a triple term
ProtectedcarriesA pinned group still constrains its last remaining member, so it survives remove.
The group to check
whether it is pinned
The positions of the shape a group is pinned to.
The group to look up
the group per position, or undefined when it is not pinned to a shape
Resets the set to its initial state, dropping every group.
A copy that shares no state with this one, so that either may be mutated on its own.
the copy
ProtectedcopyCopies the state of this set into target, which subclasses extend with the state they add.
The set to copy into
ProtectedcreateCreates a group holding no values at all, which is only reachable through whatever a subclass makes point at it - the positions of a triple pin, for datastructures/TermClusterSet!TermClusterSet.
the new group
ProtectedcreatePrivatecreateCreates an anonymous group for one position of a shape, holding what that position admits and no more.
The position it stands for
the new group
ProtecteddropDeletes a group and every value in it, which subclasses extend with the state they add.
The group to drop
Gets or creates a group for a value.
The value to get/create a group for
the group ID
Every group and its values, in the order the groups were created.
the pairs
PrivatehasWhether any group is its own descendant, which no value satisfies: a triple term is strictly larger than
each of its components, so ?o ≡ <<( ?o ... )>> is unsatisfiable - and resolving such a group to a term
would not terminate.
Descending from touched alone is the whole graph's answer whenever the graph was acyclic before the run
(acyclic): a cycle that holds none of the groups the run pinned or merged holds none of its new
edges either - the pins of those groups are the only ones it changed, and a merge is the identification
of two groups into one of them - so it was there to be found on the way in. Where that does not hold,
every group is a root again.
The groups the run that is settling pinned or merged
whether the pins close a cycle
Whether the group exists at all - a group nothing points at any more does not.
The group to check
whether it exists
ProtectedisA group a live pin points at survives however few members it has: it is a position of a shape, and dropping it would leave that shape naming a group that is no longer there.
The group to check
whether it is worth keeping
PrivateisWhether some group's shape holds this one in one of its positions, read off pinChildToOwners and checked against the pins of the owners it names - which is also where an owner that no longer points here is pruned.
The group to look for
whether anything points at it
ProtectedmergeMerges two groups by id, which is what a group nothing names can be merged by - the values-only half of a merge, whatever else a subclass hangs off a group being migrated by migrateGroupData.
One group
The other
the ids involved, or undefined when the two ids are the same group
Merges two groups, carrying over everything the disappearing one held.
the ids involved and whether the two could not hold the same value, which leaves the set in a
state no caller may read - what to do about that is up to the two subclasses; undefined when both
values were already in one group
ProtectedmigrateCarries the owners pointing at the disappearing group over: pinChildToOwners is keyed by resolved group, and this is the point at which the two ids become one.
The group disappearing
The group surviving
Narrows what terms a group's value may have.
The group to narrow
The term types to narrow it to
false when nothing is left for it to be, or when its pin is not one of those terms
PrivateplacePuts a pin on a group, meeting it with the one already there and queueing what that decides.
The group to pin
The pin to place
The work list to queue onto
false on a contradiction
PrivaterangeThe term types a group's value may have.
The group to look up
its range, the top of the lattice when nothing narrowed it
PrivateregisterPrivateresolveRuns a work list of merges and pins to exhaustion.
The constraints to establish, which establishing them adds to
false on a contradiction
Dereferences a group id through the merge history.
The id to resolve
the group it has become, or itself when it is still its own group
PrivatesetPins a term onto a group.
The group to pin
The term every value of it equals
false when the group already carries something incompatible, which leaves the set in a state
no caller may read
The term a group is pinned to.
The group to look up
the term, or undefined when nothing pins it, or a shape does instead
ProtectedtouchMoves revision on, invalidating whatever was memoised off the state the set was just in.
Called by the method that writes rather than by whoever asked for the write, so that a caller has
nothing to remember. Most of the calls sit on the choke points the writes of this class pass through -
clear, copyInto, createEmptyGroup, remove, dropGroup,
mergeGroupIds - which is what a subclass extending one of them inherits rather than has to
repeat, and what makes createGroup and every super-chaining override safe without a call of their
own.
A subclass writing state no ancestor writes owes a call here on its own account, since no choke
point of this class covers it. Those are narrowRange and resolveAllConstraints on
datastructures/TermClusterSet!TermClusterSet, assertTermTypeRange on
datastructures/AssertionClusterSet!AssertionClusterSet, and sortClusters,
registerExpressionToGroup and the static-validation branch of register on ClusterSolver!ClusterSolver
Unifies two groups by id - the merge mergeGroups is, for the groups no value names.
One group
The other
false when the two cannot hold the same value
PrivateuniteMerges two live groups, queueing whatever meeting their pins decides.
One group
The other
The work list to queue onto
false on a contradiction
PrivateunregisterThe values of a group.
The group to read
its values, empty when the group does not exist
A ClusterSet whose groups may be pinned: every value in the group equals what the pin says - a term, or the shape of a triple term whose positions are groups in their own right.
Its two users differ in what a pin conflict means, which is why setPin reports one rather than raising it: for the unfolding (ClusterSolver) a group asked to be two terms at once is a broken mapping, for an assertion conjunction it is an ordinary contradiction. They also differ in the terms a pin may hold, hence the second type parameter, and in what meeting two pins comes to, hence meetPins.
Ranges live here rather than only in the solver, since the same question is asked on both sides: a group in a subject position holds no Literal and no triple term, which is what confines the nesting of shapes to the
objectchain.A pin makes the child DAG a real graph, and two invariants keep it well founded:
?o ≡ <<( ?o ... )>>having no solution. Checked once a whole work list settles rather than as each pin lands, since a merge closes a cycle just as a pin does - and only from the groups that work list touched, the rest of the graph having been acyclic before it ran (hasCycle).