Repository navigation

N7-1b: std.algebra collection callback ops (map, all) realized through the one fold encoding, keyed on named template rows - #13069

Merged

gunbai-bot[bot] merged 119 commits into

mainfrom

session/snappy-eagle-803

Oct 4, 2026

Commits on Sep 26, 2026

docs/plans: arrow elimination model for v2 infer (for ruling)

Brian Searls
and
claude
committed
67f1f49
v2 infer: arrow elimination and the body/declared-return check; one Int and one Bool value type

Brian Searls
and
claude
committed
d5135cb

Commits on Sep 27, 2026

infer_product_introduction: evidence control pins the Int type atom's kind, not the retired inhabitant denotation

Brian Searls
and
claude
committed
f06dce7
Merge remote-tracking branch 'origin/main' into session/quick-owl-368
Brian Searls
committed
2e3012b
Take infer's ObligatedInferredTree through discharge; flip refinement_discharge to holds/violated; one runtime encoding of true

Brian Searls
and
claude
committed
ac1df96
v2 resolve: ResolvedTree carries the SymbolIndex resolution consulted; cut every consumer root-first

Brian Searls
and
claude
committed
03342a3
Merge origin/main; migrate the remaining resolved-tree helpers (typecheck clean)

Brian Searls
and
claude
committed
179c7f1
pick_ingested: the arrow extractor returns the arrow Node (my retype over-reached)

Brian Searls
and
claude
committed
95856ef
Merge origin/main; retype main's new resolved-tree helpers (declared_parameter_order, reference_closure)

Brian Searls
and
claude
committed
84d4768
Merge origin/main into session/quick-owl-368 (resolve 04_infer import conflict with #12361)

Brian Searls
and
claude
committed
274d51d

Commits on Sep 28, 2026

compose #12432 (pinned reference-evidence base)
gunbc-ci-auto-heal
committed
3609145
compose #12379 (pinned reference-evidence base)
gunbc-ci-auto-heal
committed
80e9a04
A reference to a corpus declaration is typed by that declaration

gunbc-ci-auto-heal
and
claude
committed
3c43400
The reference's guard becomes the one an application will ask

gunbc-ci-auto-heal
and
claude
committed
1b73daa
The same-leaf discriminator is not qualified, and the file says so

gunbc-ci-auto-heal
and
claude
committed
707cc49
The application path can now see a reference's callable evidence; it still is not enough

gunbc-ci-auto-heal
and
claude
committed
7fa6d60
A named call grounds: the use carries the facts, the arrow carries the type

gunbc-ci-auto-heal
and
claude
committed
32ea98e
A return that is already a type is consumed, not denoted again

gunbc-ci-auto-heal
and
claude
committed
53022c2
The body/return check becomes reachable, so a return mismatch refuses again

gunbc-ci-auto-heal
and
claude
committed
5359640
The qualification set: identity discriminated, unavailable evidence refused

gunbc-ci-auto-heal
and
claude
committed
117a716
Native execution of a named call: measured, still refused at eval

gunbc-ci-auto-heal
and
claude
committed
2702923
Attribute the eval refusal: the anchor is inside the callee's declaring path

gunbc-ci-auto-heal
and
claude
committed
b65297c
A named call executes: eval consumes the declaration reference it was descending into

gunbc-ci-auto-heal
and
claude
committed
6bf3b29
The remaining refusal is a facts-key collision, not a fact about the call

gunbc-ci-auto-heal
and
claude
committed
e168404
Both remaining reds refuse at the same runtime-built node, measured

gunbc-ci-auto-heal
and
claude
committed
c187a8f
Withdraw the provenance inference; establish the key conflict by enumeration

gunbc-ci-auto-heal
and
claude
committed
3769c83
Enroll the acceptance targets: argument-dependent execution and the Bool pair

gunbc-ci-auto-heal
and
claude
committed
3065331

Commits on Sep 29, 2026

Field projection through resolve, infer and eval, with the field check that closes it

gunbc-ci-auto-heal
and
claude
committed
6f0dff1
The seven's receiver is a match binder, and its blocker is the match form

gunbc-ci-auto-heal
and
claude
committed
b38e6e2
Merge main into the field-projection lane: both carrier threads, not one

gunbc-ci-auto-heal
and
claude
committed
0eddf9f
Restore the application-path repair the merge pass silently dropped

gunbc-ci-auto-heal
and
claude
committed
27f1427
Merge main (#12433, #12510 and four more) into the field-projection lane

gunbc-ci-auto-heal
and
claude
committed
0cb200c
The seven's downstream continuation, qualified past the match boundary

gunbc-ci-auto-heal
and
claude
committed
81e7c77
The chain wins: a bound head resolves local-first, and the interim guard dissolves

gunbc-ci-auto-heal
and
claude
committed
22800fa

Commits on Sep 30, 2026

v2 infer: type a match over a declared (generic) coproduct and its arm binders (#12641)

authored
5ca3b0a
Take the landed match-binder typing (#12641) into the lane
gunbc-ci-auto-heal
committed
83d27a7
Compose #12506, #12641 and current main by hand, preserving all three semantically

gunbc-ci-auto-heal
and
claude
committed
f37bc61
Two readers disagreed about a callee's arrow, so no named call's arguments were judged

gunbc-ci-auto-heal
and
claude
committed
fcce3d8
Route an unadmissible callable grounding to the frontier; retire the match-form blocker

gunbc-ci-auto-heal
and
claude
committed
d933035
Compile the consumers the widened signature broke, and undo two merge reversions

gunbc-ci-auto-heal
and
claude
committed
2627d30
Enrol two rows that nothing was running, and correct the measurement they recorded

gunbc-ci-auto-heal
and
claude
committed
8e9fc28
Merge main: #12566's one-relation declared-return judge beside this lane's reader

gunbc-ci-auto-heal
and
claude
committed
89420be
A declared position that already carries its value type is decidable; Int was masking Bool

gunbc-ci-auto-heal
and
claude
committed
76c9ed5
An ill-typed fixture the skipped check was hiding; the facts-key conflict narrows to a shared key

gunbc-ci-auto-heal
and
claude
committed
a13d507
Merge main (#12407): six conflicts resolved on their merits, plus four seams git reported clean

gunbc-ci-auto-heal
and
claude
committed
e95381c
Merge main (#12714): import union in resolve

gunbc-ci-auto-heal
and
claude
committed
66cd619
The arm-pattern reader asked the construct encoding instead of re-deriving its tag

gunbc-ci-auto-heal
and
claude
committed
0f9d715
Merge remote-tracking branch 'origin/main' into lane/reference-evidence-consumer
gunbc-ci-auto-heal
committed
ee18cd4
A loop carrier is a binder: one value-binder admission, and the Loop walk that uses it

gunbc-ci-auto-heal
and
claude
committed
797a608
Value binders are admitted at one gate: Arrow parameters, lets, match arms, loop carriers

gunbc-ci-auto-heal
and
claude
committed
978cf66
One callable Arrow constructor; value shadowing refuses, with its incidental fixture corrected

gunbc-ci-auto-heal
and
claude
committed
85ad321

Commits on Oct 1, 2026

Eight claims moved to the interface they discriminate; 44 stay end-to-end, by reasoning

gunbc-ci-auto-heal
and
claude
committed
8b83c4a
Merge main (#12550 fold encoding, #12582 facts-key, #12740/#12763 records): one Loop walk

gunbc-ci-auto-heal
and
claude
committed
9b55c96
Delete the duplicate Loop dispatch arm the merge left behind

gunbc-ci-auto-heal
and
claude
committed
78c2444
The fold slot is a generated binder, not the authored step formal; this lane's carrier frame dissolves

gunbc-ci-auto-heal
and
claude
committed
2bd1f0d
A root binding resolves a name but may not be projected through

gunbc-ci-auto-heal
and
claude
committed
bd9d3d3
A root-bound data value's projection: control added, and it is not yet supported

gunbc-ci-auto-heal
and
claude
committed
6df74f8
The cref locator asks the production application reader and selects by full declaring path

gunbc-ci-auto-heal
and
claude
committed
8ea7415
Derive the DAG canonical symbol set from the grammar instead of its serialized image

gunbc-ci-auto-heal
and
claude
committed
6b3490b
Qualified-name resolution retains the binding kind rather than collapsing it to a Boolean

gunbc-ci-auto-heal
and
claude
committed
82b5f15
Field-projection inference distinguishes an unretrievable declaration from a fieldless receiver, and reads the closure's resolved declarations

gunbc-ci-auto-heal
and
claude
committed
a509caa

Commits on Oct 2, 2026

File the diagnosed root: infer cannot derive a child's context from a sibling's result

gunbc-ci-auto-heal
and
claude
committed
54725fe
Merge remote-tracking branch 'origin/main' into lane/reference-evidence-consumer
gunbc-ci-auto-heal
committed
db5b9d5
Revert the canonical-symbol derivation: main narrowed the set it reproduced

gunbc-ci-auto-heal
and
claude
committed
14a8710
Re-point the parameter reader at main's route; record the match-binder loss at its refusal

gunbc-ci-auto-heal
and
claude
committed
f498eb6
Merge remote-tracking branch 'origin/main' into lane/reference-evidence-consumer
gunbc-ci-auto-heal
committed
bb1e03c
The consolidated callable arrow closes its own lowered image

gunbc-ci-auto-heal
and
claude
committed
e60150d
Compile every consumer of the widened constructor, not the five files the matrix chose

gunbc-ci-auto-heal
and
claude
committed
f92c961
The native door passes the resolution, not the whole NativeTestContext

gunbc-ci-auto-heal
and
claude
committed
7f3a0e6
Update the two citations of the renamed fold-carrier row

gunbc-ci-auto-heal
and
claude
committed
8c23004
Facts-key collision controls assert the separation #12582 achieved, not the collision

gunbc-ci-auto-heal
and
claude
committed
edd9788
WIP, NOT YET EFFECTIVE: one full-path key for named-parameter bind and lookup

gunbc-ci-auto-heal
and
claude
committed
72e10bb
Close #12766's eval frontier: a parameter-reference body is admitted and resolves by path

gunbc-ci-auto-heal
and
claude
committed
2eb0676
Merge origin/main into lane/reference-evidence-consumer

Brian Searls
and
claude
committed
ea11297
Repair the merge's cross-side seams: projection base, two fixtures

Brian Searls
and
claude
committed
3bf1880
Where-predicate calls walk unjudged under the where_clause frontier, counted

Brian Searls
and
claude
committed
c84f55b
Hoist three in-body annotations in 05_eval to module-item grain (floor parse refusal)

Brian Searls
and
claude
committed
a4b2b10
fold_lowering: a block-bodied arrow lambda has a block body

gunbc-ci-auto-heal
and
claude
committed
4dda083
Resolve the closure once per context, not once per subject (review 74212)

Brian Searls
and
claude
committed
adb3d63
Total the merge's sixteen unrostered wildcard arms; roster the one that is not a sweep

Brian Searls
and
claude
committed
f09191e
Merge remote-tracking branch 'origin/lane/reference-evidence-consumer' into session/tidy-raven-393
gunbc-ci-auto-heal
committed
b0e566a
N7-1 WIP: lambda-binder projection base is a lexical reference; dependent-child infer driver instantiates the fold member

Brian Searls
and
claude
committed
2ec3636
N7-1: control for the lambda-binder projection base (r)

Brian Searls
and
claude
committed
6425323
N7-1: climb receipt on infer_child_context_cannot_depend_on_a_sibling_result; Bind/Match frontier row

Brian Searls
and
claude
committed
d09ec4f
N7-1: rename the keyword-spelled loop parameters (native parse refusal of 04_infer); strip debug probes; keyword-as-value receipt

Brian Searls
and
claude
committed
422a28c
N7-1: nested payload binder re-boxed in emitted Rust -- receipt with minimal reproducer and the missing build-witness trigger

Brian Searls
and
claude
committed
2a7bf55

Commits on Oct 3, 2026

N7-1 (a): a collection fold iterates its step's BODY; the carrier formal is instantiated from init; the fold Bind judges the body (and a declared return) against the carrier; operand types read thr…

Brian Searls
and
claude
committed
73e5a89
N7-1 (a): frontier row for a lambda value with no derived type in v2 infer

Brian Searls
and
claude
committed
c2ccddc
N7-1: receipt -- the operand reader's second authority for a binder's type

Brian Searls
and
claude
committed
4e1009e
N7-1 (x)(1): a closure root whose own resolve refused is recorded, and every closure-index miss over it carries that refusal

Brian Searls
and
claude
committed
fe498dc
N7-1 (x)(2): v2 std modules that spelled List without importing it import std.types List -- each refused its own native resolve and vanished from the closure index

Brian Searls
and
claude
committed
7eb44d9
N7-1 (x)(2): a projection off a value resolves its base and not its field (diagnostics_fatal(d: d).reason refused v2.std.diagnostic's own resolve)

Brian Searls
and
claude
committed
5585a39
arrow_lambda_block_body: one warm producer for the five claims

gunbc-ci-auto-heal
and
claude
committed
83a31c8
N7-1: value-projection arm reads the field edge through field_projection_edge_field_optional

Brian Searls
and
claude
committed
2dae714
N7-1b: std.algebra collection callback operations (map, all) realized through the one fold encoding, keyed on named template rows

Brian Searls
and
claude
committed
744946f
v2 std: one List binding per module -- drop the v2.std.collection List import where std.types List was added (10 modules double-bound it), and import it in std.compilers.sugar

Brian Searls
and
claude
committed
29a8088
v2 std: import Optional/Present/Absent where four modules used them unimported (data_initializer_identity refused its own native resolve)

Brian Searls
and
claude
committed
126a658
N7-1b: regenerate the std.algebra stage0 mirror (named collection callback shapes)

Brian Searls
and
claude
committed
3e2a256
collection_callback_realization: each fixture program assembled once by a nullary producer; claims read the decided value

Brian Searls
and
claude
committed
4467f51
floor_pure_producer_share: warm rows for collection_callback_realization producers

Brian Searls
and
claude
committed
acc2a93
Merge origin/main into session/tidy-raven-393 (#12506 landed; retargeted to main)

gunbc-ci-auto-heal
and
claude
committed
f7e61a7
Merge remote-tracking branch 'origin/main' into session/silent-crab-339-n7
Brian Searls
committed
3e08ecc
N7-1: exhaustive arms in the dependent-child driver and fold decoders (no wildcard over a closed coproduct)

Brian Searls
and
claude
committed
218eedb
infer_fold_member_instance: one nullary producer per fixture program; claims read the decided value

Brian Searls
and
claude
committed
07a66bb
floor_pure_producer_share: warm rows for infer_fold_member_instance producers

Brian Searls
and
claude
committed
d070e7b
Merge remote-tracking branch 'origin/session/tidy-raven-393' into session/silent-crab-339-n7
Brian Searls
committed
c2aa58a
Merge remote-tracking branch 'origin/session/silent-crab-339-n7' into session/snappy-eagle-803
Brian Searls
committed
5be64e2
Merge remote-tracking branch 'origin/main' into session/silent-crab-339-n7
Brian Searls
committed
8419a00
N7-1: cite the renamed match-binder control (declarations finding); kvr named-call Bool formal now refuses since #12506 types references by declaration -- control rewritten to assert the refusal, a…

Brian Searls
and
claude
committed
c4cd777
Merge remote-tracking branch 'origin/main' into session/silent-crab-339-n7
Brian Searls
committed
a5bf10b
Merge remote-tracking branch 'origin/session/silent-crab-339-n7' into session/snappy-eagle-803
Brian Searls
committed
eb4bdf6
Merge origin/main into session/snappy-eagle-803

Brian Searls
and
claude
committed
449bd0e
floor_pure_producer_share: drop the collection_callback_realization warm rows (freeze until #13043; identities routed to royal-deer-478)

Brian Searls
and
claude
committed
2aa847c
floor_pure_producer_share: restore the warm rows (amended freeze: land now, royal-deer-478 drops them when #13043 merges)

Brian Searls
and
claude
committed
40ded9c
Merge remote-tracking branch 'origin/main' into HEAD
Brian Searls
committed
98b34fb
floor_pure_producer_share: main's file plus only this PR's warm rows

Brian Searls
and
claude
committed
66c125e
Remove the n7probe scratch module (debugging probe, no consumer)

Brian Searls
and
claude
committed
f3f4fef
fold_lowering: a fold-realized Loop's iteration direction is a declared fact of its realization (map right to left, owned by its synthesis); derived from the realized edge; fold_list vs fold_list_r…

Brian Searls
and
claude
committed
e59f8a3
Merge remote-tracking branch 'origin/main' into HEAD
Brian Searls
committed
231e01c