Feat/graphs trees - #41
Open
cmdupuis3 wants to merge 8 commits into
Open
Conversation
The v10-era trees/graphs module rewritten into current Blade semantics: TreeIdx<shape> as one path-domain slot over let-static shapes (the IrrepsIdx + SparseIdx precedents), flat preorder storage on the ragged CSR descriptor, derived dense axes for bulk numerics. Trace<N> and DAGIdx are deleted as index types -- visited sets are values, walks are let rec, collapse is MonadPlus, acyclicity is a checked where-license. plan-graphs-trees.md carries the seam checklist (calibrated on the Ragged/Sparse/Orb landings), the P0 representation decision, and the P0-P8 phase ladder. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Single tuple slot decided (rejected variable-arrow = rank rewrite); domain = complete paths, cardinality = leaf count, preorder = lex. Degree-sequence payload first, nested-leaf sugar deferred. Probes on the baseline: G1 (Nat elements round-trip) PASSES, G2 confirmed (tuple under let rec refuses), G5 new finding -- Nat-tagged elements under let rec hit the same BL3999 gate, so the walk recurrence needs untagged state until P7. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…brute force src/TreeRank.fs is the pure-function layer the plan's P1 row asks for, and it is dependency-free on the OrbRank policy (FSharp.Core only, no Blade module opened) so proofs/ scripts can `#load` it standalone. It sits beside OrbRank.fs in the fsproj for the same reason: IR/IRStorage are its eventual consumers and nothing it needs compiles later. A shape is a preorder degree sequence. `validateDegrees` is the ONE structural gate -- n >= 1, no negative degree, and the prefix walk closing EXACTLY -- and it separates the two genuinely different mistakes rather than collapsing them: a sequence that closes early has a tail belonging to no tree, a truncated one has slots nothing fills. Every entry point Errors through it, so a malformed shape cannot draw different verdicts from different doors. `treeTables` derives everything else in three linear passes: Sizes, LeafCount, LeafStart (the feature doc's `off`, read in the path domain), Parent, ChildIndex, Depth, the child CSR and the leaf-node table. On top of that: treeForward (path -> leaf offset), treeBackward (its total inverse on [0, cardinality)), treeSubtree (partial path -> node + the contiguous leaf block), and treePaths. The domain decision from P0 is what the file is organized around and says so loudly: the value domain is COMPLETE root-to-leaf paths, so cardinality is the leaf count, not the node count. `deg` is node-indexed and the array is leaf-indexed; every table is documented as one or the other, because mixing them is the one arithmetic mistake here. `*Checked` means DOMAIN-checked, not OrbRank's overflow-checked -- nothing here can overflow, so the split is between the guard-free hot path and the door that names the failing step. tests/Test_TreeRank.fs carries its own nested-shape ADT (`Node of Shape list`), its own preorder flattener and its own recursive path enumerator, so the oracle never reads TreeRank's tables. The order is a contract, so it is pinned as an ORDER and not only as a set: a forward/backward round trip cannot catch the convention drifting, both halves shift together. Subtree contiguity gets its own oracle at every node. The two documented shapes are pinned from the nest through the degree sequence to the path list; the degenerate corners (single leaf, whose only complete path is the EMPTY one; unary chain; flat = Idx<k>; deep-narrow; wide-shallow) are pinned by hand as well as swept, plus 40 seeded-random shapes. blade test treerank: 73 passed, 0 failed, 0 skipped. Full default suite: 5179 passed, 0 failed, no Failed tests section. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Declaration and printing only. `type CrystalIdx = TreeIdx<crystal>` parses,
validates its shape, aliases, unifies by shape identity and prints back in
house form; every position that would make a tree-typed VALUE refuses with a
message that says what works today.
The shape is the PREORDER DEGREE SEQUENCE -- P1's canonical internal form --
resolved through StaticEval and validated by TreeRank.treeTables. Extent is the
LEAF count, because a tree slot's domain is complete root-to-leaf paths; the
sequence itself rides ONLY in the Tag, so identity is the shape and not the
(possibly coincident) cardinality.
Three decisions worth naming:
- `IxKTree` is a NEW case in IR.fs's exhaustive family active pattern rather
than a member of `IxDense`. A tree's CELLS are dense -- `placementOf` says so
explicitly -- but its SUBSCRIPT is a path folded through the degree tables,
and grouping it dense would hand every future consumer a plausible dense
reading of a record it has no addressing for. Costs zero consumer edits today
(all three have correct catch-alls) and buys P3/P4 a build failure instead of
a wrong address.
- BL4021 "invalid tree shape" is ONE code for two mistakes -- non-static and
malformed -- differentiated by the message, on BL4018's precedent. USE
refusals mint nothing: `TreeIdxUnsupported` joins BL4003 as
`OrbitStorageUnsupported` does.
- `Unify.indexPairIncompatible` needed its own arm, and the plan doc's "tag
equality decides" reading was wrong: `isSyntheticTag` exempts every `__`
tag, so `__tree:` never gated and two different shapes unified. The TreeTag
arm goes ahead of the exemption, exactly where irreps' BlockSpecTag arm is.
Doc amended in this commit.
Refusal doors are the wreath three-door set, copied wholesale: the let
annotation (which is also the ALLOCATION door -- Blade has no value-less `let`,
so nothing reaches IRStorage and P2 needs no storage arm), the function
signature, and the `range<>` slot; plus a defensive subscript arm for a leak
through an alias the annotation scan never probed.
Corpus: NEW category `tests/corpus/trees/`, 13 files, registered in RunAll's
allTests and CliSelfTests' key map (the memfree precedent -- no Test_*.fs, no
fsproj entry). Two positives, eleven reject probes, including the T1
alias-laundering gate. T2's three strictness seams are physically
unconstructible while every use refuses; 013 pins the type-level half and
records the value-level probes as a P3 gate obligation in its header.
Measured, not guessed: the four empirical unknowns the edit plan left open.
`TreeIdx<>` is BL1999 (parser). `[2,0]` and `[1]` both report "truncated
degree sequence" and differ only in the node count, so they merge into one
file; the genuine tail case is `[0,0]` ("closes early"), which is its own file.
There is NO StaticEval depth cliff on this path -- decoding is a fold and the
table build is three iterative passes, so a literal depth-99 chain lowers
clean -- so the planned depth-cliff test was deleted rather than pinned to a
fiction, and the feature doc's claim is corrected to say the budget binds on
the shape's PRODUCING EXPRESSION, not on the tree.
Two message defects found by running the compiler and fixed forward: the
empty-shape text double-prefixed its own label ("the shape: the shape is
empty"), and the use-refusal's example declaration substituted the rendered
class into its own shape slot ("TreeIdx<CrystalIdx (= TreeIdx<[...]>)>").
Gates: build 0/0; `blade test trees` 13/0; `blade test treerank` still 73/0;
full `blade test` 5192/0 (5179 baseline + 13), Surface block green against the
regenerated protocol/surface.json and the hand-authored BL4021 entry.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…iteral
Construction and static whole-path reads, both lanes at once. The phases merge
because corpus `// EXPECT:` pins validate through the CODEGEN lane, so an
interp-only P3 could land no pinned value test.
It came in at ~200 lines across 4 files, with NO back-end edits at all, and the
two reasons are the whole design:
- CONSTRUCTION IS FREE. A tree binding is an ordinary rank-1 dense Array<T,1>:
the flat literal checks through the generic annotated-literal arm (rank 1,
SymNone, so neither the compact nor the wreath arm claims it), the result
carries the ANNOTATION's array type, and placement/alloc/teardown/print all
key on IxKinds that IxKTree is not. Only the TYPE carries treeness. So P3's
construction work was DELETING P2's let-annotation door, not writing a
storage arm.
- READS FOLD AT TYPECHECK. `T((c0, c1, ...))` recovers the degree sequence from
the Tag, resolves the leaf offset through TreeRank.treeForwardChecked, and
rewrites to a constant subscript. Both lanes then consume the same IRLit, so
they are byte-identical BY CONSTRUCTION rather than by agreement -- the C++
side falls through compoundRead/wreathRead/lazyCompactRead/densePartialSubview
to rawSubscript, the interpreter takes indexArray's dense peel, and neither
needed a line. Deliberately NOT the compound/sparse full-read emitter: that
machinery exists because those offsets are RUNTIME facts, and a static tree
path is not one.
`extents`, printing and `reduce` needed zero edits and are pinned rather than
implemented. New `TreeIdxPath` error joins BL4003 (the index type is fine, this
READ is out of domain), so no new BLxxxx code and no five-touch-point work.
Doors, with the reasoning in the code: the function SIGNATURE door stays (a
binding is a pool this TU allocates; a parameter is an ABI, and the shape rides
the caller's Tag while HM monomorphization learns ELEMENT bindings, not array
SHAPE). `range<>` stays -- it binds COORDINATES, and a tree's coordinates are
paths. NEW: `method_for` refuses, because a loop former PRODUCES an array that
inherits the operand's index record, dragging in output-storage classification,
fusion and exprTypeIfKnown's HM whitelist (failure mode there is a BL6001
spray, not a refusal). `reduce` is the deliberate asymmetry: it CONSUMES the
pool and yields a scalar, so nothing inherits the slot. The door rides the
loop object's own TypedMethodForInfo because inferMethodFor has four exits that
each build their own arrayTypes.
Measured, not guessed -- every unknown the edit plan flagged:
- `S((0))` is a PARENTHESIZED SCALAR (the parser has no 1-tuple form), so it
and `S(0)` are one program and reach the one-element-path arm. It is
self-limiting, not special-cased: it resolves only when the root's c-th child
is a leaf. Both spellings pinned side by side in 102.
- The T2 value-level seams: let-ascription is REACHABLE and fires BL3001;
direct application and declared-return are UNREACHABLE, caught first by the
signature door with BL4003 naming the function. 111/112 pin which door caught
them and say to re-run when the boundary opens.
- The HYBRID annotation Array<F64 like CrystalIdx, Idx<m>> is ACCEPTED and
allocates as a rank-2 dense pool (116); only the READ refuses (117), because
the fold rewrites the whole subscript to one literal and a residual trailing
coordinate has nowhere to go.
TreeIdxUnsupported's message was rewritten: it claimed nothing allocates or
reads a tree, which P3 makes false. It now shows the working program.
Corpus: 18 new files, numbered 100-117 per the edit plan so the P3/P4 block
reads apart from P2's. Three P2 pins are now DEAD and are deleted rather than
left stale -- 009 (annotation refuses), 010 (subscript refuses) and 012 (reduce
refuses, whose own header said a different code arriving was the signal to
revisit). Their positives land as 100, 101 and 105. 013's "P3 OBLIGATION"
header note is discharged in place, pointing at 110/111/112.
Gates, all run from this worktree, serially:
build 0 errors, 0 warnings
blade test trees 28 passed, 0 failed, 0 skipped
blade test treerank 73 passed, 0 failed (unchanged)
blade test interp trees 29 passed, 0 failed, 0 skipped -- and this is the
byte-comparison gate the plan's P4 row demanded:
each of the 10 value-producing files reports
"values identical", per file.
blade test diff-oracle trees SKIPPED, honestly. That verb is a PINNED-ORACLE
lane (current build vs a snapshot at oracle/Blade.exe)
and no snapshot exists in this checkout. It is not
the interp/codegen differential and is not reported
as one; the plan doc's §7 now says so.
full blade test 5207 passed, 0 failed, 0 skipped, no `Failed tests:`
(5192 P2 baseline - 3 deleted + 18 new). Surface
block green with no protocol regeneration, since no
new diagnostic code was minted.
Docs, same commit: the plan's P3/P4 rows merge into one LANDED row with the
actual size and the actual gates; P5 inherits the signature door, the
method_for re-take, and loses the bare-scalar question (already answered).
The v1-refusal list gains five entries with their reasoning. The feature doc's
status line and its "hybrids are free" row are corrected to what was measured.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Full suite 5207/0 independently re-verified; P5 (partial-path views, derived dense axes) is the next arc. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Derived dense axes, the pool retype, static view composition, and the open
function-signature door. Still no back-end edits: ~330 lines across 10 files,
all front end.
THE FINDING FIRST, because it changed the phase's size. The plan named one top
risk -- direct application does not unify plain-call arguments, so a same-rank
tree-identity mismatch might pass silently once the signature door opened -- and
said to probe it before writing anything else. It did pass. With the door open
and no guard,
let A: Array<Float64 like WideIdx> = [...] // [5,0,0,0,0,0]
function f(t: Array<Float64 like DeepIdx>) = { t((1, 2)) }
let v = f(A) // [2,2,0,0,3,0,0,0]
COMPILED AND RAN, printing 5: the callee folded its path against its OWN degree
sequence and read offset 4 of an argument that has no such path. Equal leaf
counts (5 and 5) are exactly the coincidence tree identity exists to reject.
The laundering twin passed too -- `function h(x: T^1)` applied to a tree
binding ran and printed 15. So the door does not ship without its lock, and
`TypeCheckValidate.collectAppTreeErrors` lands in this phase rather than a
later one. It runs post-zonk beside collectAppRankErrors for that sweep's own
reason (an abstract parameter is not closed at its call site, and
concreteClassOf declines on arrays by design), and it restates Unify's TreeTag
predicate VERBATIM -- degree sequence plus nominative alias -- because it exists
only where unify is never asked, not because it wants a different answer.
The rest:
- LeafIdx<S> / NodeIdx<S> lower to PLAIN dense Idx records (Tag None,
IxKPlain). `LeafIdx<crystal>` unifying with `Idx<5>` is the feature, not a
leak: bulk numerics keep every optimization only if the axis is
indistinguishable from a hand-written one, and a nominal tag would make the
leaf axis flow into nothing. Nominal identity stays on the TREE type; a user
who wants a named leaf axis writes `type Leaves = LeafIdx<crystal>` and gets
the ordinary alias tag. Two keywords, not one parameterized former: one
payload, two extents (cardinality vs node count).
- `leaves(T)` is a shadowable plain-call intrinsic returning the SAME node with
a new .Type -- zero copy, zero nodes, nothing emitted. It PERMANENTLY retires
the method_for limitation rather than deferring it again: `method_for(leaves(T))
<@> f` is an ordinary dense loop, so 113's refusal is now a boundary between
two jobs over one pool instead of a phase note. Its message names the way out.
- Composition `T((p))((q))` == `T((p ++ q))` is a pre-typing SURFACE splice, so
the landed fold is untouched and the nested-view identity holds by
construction rather than by a second path agreeing with the first. It claims
the WHOLE curried spine, not two groups: a declined spine folds its prefix to
a scalar and applies the next group to it, which typechecks (over-applying a
scalar is an old general hole -- `A(0)(0)` on a plain rank-1 array passes
`check` too) and dies in g++ with "expression cannot be used as a function".
Claiming the spine turns that into TreeRank's own "outside [0,0)" (130).
- Escaping views CUT, with the evaluation recorded in the plan doc: RaggedRow
would make a view wear a ragged IxKind and lose its tree identity;
IRSlice/IRSubset are deliberately off exprTypeIfKnown's whitelist and turning
one on is a cross-cutting change needing its own justification; materializing
a copy spends emitter work on a copy nobody asked for. The useful case
survives as composition, and the refusal needed no code -- `let sub = T((1))`
still meets "must end at a leaf" (119).
- BL4019 deferred as UNMINTABLE, not merely unneeded, and the plan's diagnostics
bullet now records why: every path is literal, so both outcomes already have
messages, and a registered code needs a diagnostics.json example naming a
corpus file that literally contains "BL4019" -- which no reachable site can
produce. It becomes mintable with dynamic coordinates.
Corpus 41 files (28 + 13). New: 118 composition, 119 escaping view, 120 LeafIdx/
NodeIdx declare, 121 the plain-Idx identity made falsifiable, 122 the retype,
123 the bulk map (the first genuinely positive bulk-numerics test), 124
range<LeafIdx> + reduce, 125 the boundary crossing, 126 laundering, 127
leaves() of a non-tree, 128 the shared bad-shape channel, 129 shadowing, 130
the over-long spine. Pins changed, all in this commit: 111 re-run and re-pinned
to the new guard (its landed header demanded exactly this), 112 re-pinned BL3001
(the return seam was never open -- unify always decided it, which is the
asymmetry the T2 set exists to expose), 008 and 013 REWRITTEN because the
signature door they used is gone -- 008 keeps its T1 claim through the stricter
abstract-param gate, 013 is promoted from the type level to the value level and
now pins that two aliases of the SAME sequence are distinct. 108 and 113 headers
updated in place.
127 lands as BL3999, not BL4003, deliberately: BL4003's template opens with
"<class> is a declarable index class", and a plain array has no class to name,
so routing it there would produce confident nonsense about the user's own type.
Gates, serial, from this worktree:
build 0 errors, 0 warnings
blade test trees 41 passed, 0 failed, 0 skipped
blade test treerank 73 passed, 0 failed (unchanged)
blade test interp trees 42 passed, 0 failed, 0 skipped -- all 18
value-producing files report "values identical"
full blade test 5220 passed, 0 failed, 0 skipped, no `Failed tests:`
(5207 + 13). Surface block green against the
regenerated protocol/surface.json (two new
keywords); diagnostics.json untouched, no new code.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Full suite 5220/0/0 independently re-verified; P6 and the graph arc are next. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.