ogar-elk: borrowed lens over the baked edge table - #258
Conversation
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_df3393b2-5085-4d07-bed4-33d5e0a901f0) |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 3c6f4b54a0
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| let merged = Spine { | ||
| base: self.base, | ||
| overlay: &overlay, |
There was a problem hiding this comment.
When merge is called on a Spine produced by with_overlay, this reconstruction drops self.overlay and checks cycles using only the base plus the new axioms. For example, base 1→2, existing overlay 2→3, and candidate 3→1 form a cycle, but this code reports is_sound() == true; include the existing overlay in the graph used for the merged cycle check.
Useful? React with 👍 / 👎.
AdaWorldAPI
changed the title
`ogar-elk` runs after the bake. Joining -- resolving a CURIE, reconciling which source asserts what -- completes upstream, and the bake freezes the result into positions; this crate observes what the resulting spine entails. The module documentation now states that position. The previous text placed the crate before the bake, which does not match what it consumes. The shape follows from the position: an observation over a bake borrows what the bake already holds. - `Closure`, which owned a `HashMap<ClassAddr, Vec<ClassAddr>>`, becomes `Spine<'a>`, a lens over a sorted `&'a [Subsumption]` -- the caller's projection of `Bake::triples` to its is_a edges. The bake already lays that adjacency out in sorted order, so the map was a second copy of it, and a second copy is a second thing that can disagree with the first. - `from_asserted(impl IntoIterator)` becomes `Spine::over(&[..])`. - `parents_of` is an equal-range binary search returning a subslice of the caller's data. `parents_are_a_borrowed_window_not_a_copy` asserts pointer identity against the source slice, so the borrowing is verified rather than documented. - `extended`, which cloned the whole map, becomes `with_overlay`, a second borrowed slice. Evaluating a candidate merge now costs a lens. Sortedness is a precondition of the search: an unsorted slice makes it miss parents, surfacing as `entails() == false` -- a wrong answer that looks like a legitimate one. `over` debug-asserts it (the bake emits sorted output); `try_over` validates in release builds and returns None rather than sorting a copy, since sorting would reintroduce ownership. Two scope notes are now in the documentation. The `HashSet` in `supers_of` is the traversal frontier, holding the answer being accumulated, not a copy of the edge table. And R3 is not redundant with `ogar_obo::BakeStats::is_a_cycles`: that field reports cycles within a single baked core, whereas R3 reports what an additional axiom set would introduce into a spine already baked. 10 tests pass (up from 8; adds the borrowed-window and sortedness cases), clippy clean.
3c6f4b5 to
0a93a83
Compare
1 participant
Reshapes
ogar-elkfrom an owning graph into a borrowed lens over the bakededge table, and states the crate's position in the pipeline explicitly.
Position
ogar-elkruns after the bake. Joining — resolving a CURIE, reconcilingwhich source asserts what, deciding two labels name one concept — completes
upstream, and the bake freezes the result into positions. This crate observes
what the resulting spine entails. The module documentation now says so; the
previous text placed the crate before the bake, which does not match what it
consumes.
The shape that follows from it
An observation over a bake borrows what the bake already holds:
ClosureowningHashMap<ClassAddr, Vec<ClassAddr>>Spine<'a>— a lens over a sorted&'a [Subsumption]from_asserted(impl IntoIterator<Item = …>)Spine::over(&[…])supers_ofwalks an owned mapparents_of— equal-range binary search returning a subslice of the caller's dataextendedclones the whole mapwith_overlay— a second borrowed sliceBake::triplesalready lays the adjacency out in sorted order, so the map was asecond copy of it. Removing the copy removes a second thing that can disagree
with the first, and makes "what would this merge do" cost a lens rather than a
clone of the spine.
parents_are_a_borrowed_window_not_a_copyasserts pointer identity against thesource slice, so the borrowing is verified rather than documented.
Sortedness
The binary search requires edges sorted by subclass. An unsorted slice makes it
miss parents, which surfaces as
entails() == false— a wrong answer that lookslike a legitimate one.
overdocuments the precondition and debug-asserts it(the bake emits sorted output);
try_overvalidates in release builds andreturns
None, rather than sorting a copy, since sorting would reintroduceownership.
Scope notes
HashSetinsupers_ofis the traversal frontier — it holds the answerbeing accumulated, bounded by the answer's size, not a copy of the edge table.
The documentation distinguishes the two.
MergeVerdict(R3) is not redundant withogar_obo::BakeStats::is_a_cycles:that field reports cycles within a single baked core, whereas R3 reports what
an additional axiom set would introduce into a spine already baked.
Verification
cargo test -p ogar-elk— 10 passed, 0 failed (up from 8; adds theborrowed-window and sortedness cases)
cargo clippy -p ogar-elk --all-targets— cleanTouches
crates/ogar-elk/src/lib.rsonly. Follow-up to #256.