c0a0b85 · jibb · git.iko.soy

git.iko.soy/jibb

on master help sign in

Take fresh IDs from one pass instead of a budgeted scan

c0a0b85Claude20 hours ago

docs/compiler.md+2−2

compare with master

unifiedsplit

@@ -148,7 +148,7 @@ When only that program's initializer and `main` are unresolved, a bounded transa

148

149Ordinary inference runs for every component before recovery, so a keyed view no longer causes an already-valid initializer to be skipped. Recovery is a fallback for unresolved components, not a replacement for definitions that check normally. The regression uses a call-bodied annotated initializer, which is outside the tuple-bodied initializer recovery shape.

150

151−A component-local recovery sequence handles a recognized direct program whose context-dependent definitions cannot resolve ordinarily. Update first derives its result from its inferred two-slot sample and canonical `cmd`/`list` templates. Subscription recovery then checks the same message/model relation and the canonical fourth slot. A narrow keyed-view proof finds exactly one direct `each (turn xs mapper)` site, derives the mapper from the actual `each` and `turn` schemes, and recovers the view before the existing initializer and ordinary `main` retries. Every recovered scheme must be closed and freshly allocated above the current environment and prelude IDs. Non-gate views and aliases decline without crashing. Final publication still requires all module definitions, the program-mold and gate-free checks, and request-value watchability.

151+A component-local recovery sequence handles a recognized direct program whose context-dependent definitions cannot resolve ordinarily. Update first derives its result from its inferred two-slot sample and canonical `cmd`/`list` templates. Subscription recovery then checks the same message/model relation and the canonical fourth slot. A narrow keyed-view proof finds exactly one direct `each (turn xs mapper)` site, derives the mapper from the actual `each` and `turn` schemes, and recovers the view before the existing initializer and ordinary `main` retries. Every recovered scheme must be closed and freshly allocated above the current environment and prelude IDs. That bound comes from one unbudgeted pass over the environment and prelude schemes, which treats named recursive types as leaves and declines only when a scheme still holds an unresolved literal tag. Non-gate views and aliases decline without crashing. Final publication still requires all module definitions, the program-mold and gate-free checks, and request-value watchability.

152

153Canonical `element` composition has two tightly scoped accommodations. Recursive result context is allowed only when every recursive side has the prepared prelude's `element` origin. When ordinary list-item fitting fails, an `element` target may instead prove its message argument invariantly or select one exact literal case with a full payload fit; a successful ordinary fit always takes precedence. This covers the unchanged todo's union controls and raw constructors without opening those paths to other unions. `tools/type-todo-full-test` checks the byte-identical island through both full APIs, the exact closed `main` type, structural downstream import, and model/message/mapper/watch rejection controls. It does not execute Jibb or implement runtime watching.

154

@@ -220,7 +220,7 @@ Note 4 has examples of each.

220

221Starting `urbit eval` and building the library takes about 27 s, or 24 s without `!:` (`tools/hoon --no-debug`), measured on 2026-11-02. Every timing in this document was measured with `!:`, which the dev tools add so errors have positions, and which makes checker work 2.2 to 2.6 times slower than on a ship; the comparisons hold, but the absolute figures overstate a ship's time. A 2,000-line module of 400 definitions then parses in about a second. Loops over definitions, arms, lines and items are tail calls, so a long module grows no stack; nesting costs a few stack frames a level, and 100,000 nested brackets still parse (note 3).

222

223−The experimental deferred constructor path can close a small import-free library transaction when ordinary resolution stalls. It retries definitions whose earlier attempts failed from their original states, retaining only successful attempts. A transaction with at most 64 definitions makes at most 4,096 attempts; it stops after a pass with no progress. This bounds the new attempt count, not each attempt's parsing, type walks or ordinary inference. Deferred definitions are restricted to simple one-component wings, literals, static strings, gates, transparent groups and empty bodies, calls, casts and a restricted boolean branch. Each successful call or cast fit must have exactly equal normalized operands so later substitutions cannot invalidate a face check. A multi-argument call also needs closed argument, sample and product types because positional face checks depend on slot boundaries and whether the result can be a cell. Other fits fail closed. A 512-node screen bounds visited expression nodes and a separate 512-node scan bounds each stability check; neither bounds mold shapes, string-piece checks, parsing, normalization, lookup, or total repeated inference. It accepts only a direct constructor callback with a closed input, records its pending fit under the source-owned inference state, and generalizes each definition against the live environment and pending constraints. Before publication it discharges and replays every edge, rejects unresolved tags or changed replay state, and checks that all molds and values are complete. The reporter reads the committed schemes for definitions added by the transaction. API and store paths, `main`, prepared-prelude recovery, imports, recursive groups, unresolved holes or written capitals, and new projection actions remain outside this full-module path. `%grec` in the constraint or freshness scan is conservatively unsupported. This is not an island-kind, runtime, or watchability check.

223+The experimental deferred constructor path can close a small import-free library transaction when ordinary resolution stalls. It retries definitions whose earlier attempts failed from their original states, retaining only successful attempts. A transaction with at most 64 definitions makes at most 4,096 attempts; it stops after a pass with no progress. This bounds the new attempt count, not each attempt's parsing, type walks or ordinary inference. Deferred definitions are restricted to simple one-component wings, literals, static strings, gates, transparent groups and empty bodies, calls, casts and a restricted boolean branch. Each successful call or cast fit must have exactly equal normalized operands so later substitutions cannot invalidate a face check. A multi-argument call also needs closed argument, sample and product types because positional face checks depend on slot boundaries and whether the result can be a cell. Other fits fail closed. A 512-node screen bounds visited expression nodes and a separate 512-node scan bounds each stability check; neither bounds mold shapes, string-piece checks, parsing, normalization, lookup, or total repeated inference. It accepts only a direct constructor callback with a closed input, records its pending fit under the source-owned inference state, and generalizes each definition against the live environment and pending constraints. Before publication it discharges and replays every edge, rejects unresolved tags or changed replay state, and checks that all molds and values are complete. The reporter reads the committed schemes for definitions added by the transaction. API and store paths, `main`, prepared-prelude recovery, imports, recursive groups, unresolved holes or written capitals, and new projection actions remain outside this full-module path. `%grec` in the constraint scan is conservatively unsupported. This is not an island-kind, runtime, or watchability check.

224

225An expected cell type can supply context to both arms of a loobean branch. This slice first retains any ordinary inference that already fits. Otherwise it retries from the original state only when a syntax screen excludes nested branches, casts, gates and local bodies, and a substitution screen excludes structural bindings. Both arms must fit, their normalized results and the expected type must be closed, their result types must match, and both fits must replay without changing the final substitution or fresh-ID counter. A successful retry retains the original arm type and its written faces; a failed retry returns the original inference result. The source and substitution screens each visit at most 512 entries. This permits at most one extra attempt for an eligible branch; the screens do not bound preexisting inference, type walks, list construction, or work across separate analyses.

226

jibb-dev/lib/jibb.hoon+69−42

@@ -13371,10 +13371,10 @@

13371 (~(put by (direct-checked-gates ds env)) update.parts update-def)

13372 =/ templates=ienv

13373 (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))

13374− =/ scanned=(unit dgscan)

13374+ =/ fresh=(unit @ud)

13375− (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)

13375+ (ienv-fresh-id (weld env (weld values.u.prelude.initial templates)))

13376− ?~ scanned ~

13376+ ?~ fresh ~

13377− =. next.initial (dg-next-id ids.u.scanned 0)

13377+ =. next.initial u.fresh

13378 =/ update-state=istate (reserve-def-caps val.update-def initial)

13379 =/ sam=isample-result (infer-sample u.written-update env update-state)

13380 ?: ?=(%| -.sam) ~

@@ -13533,10 +13533,10 @@

13533 =/ checked=(map term def) (direct-checked-gates ds env)

13534 =/ templates=ienv

13535 (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))

13536− =/ scanned=(unit dgscan)

13536+ =/ fresh=(unit @ud)

13537− (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)

13537+ (ienv-fresh-id (weld env (weld values.u.prelude.initial templates)))

13538− ?~ scanned ~

13538+ ?~ fresh ~

13539− =. next.initial (dg-next-id ids.u.scanned 0)

13539+ =. next.initial u.fresh

13540 =/ subs-state=istate (reserve-def-caps val.subs-def initial)

13541 =/ sam=isample-result (infer-sample u.written-subs env subs-state)

13542 ?: ?=(%| -.sam) ~

@@ -13884,10 +13884,10 @@

13884 =/ checked=(map term def) (direct-checked-gates ds env)

13885 =/ templates=ienv

13886 (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))

13887− =/ scanned=(unit dgscan)

13887+ =/ fresh=(unit @ud)

13888− (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)

13888+ (ienv-fresh-id (weld env (weld values.u.prelude.initial templates)))

13889− ?~ scanned ~

13889+ ?~ fresh ~

13890− =. next.initial (dg-next-id ids.u.scanned 0)

13890+ =. next.initial u.fresh

13891 =/ view-state=istate (reserve-def-caps val.view-def initial)

13892 =/ sam=isample-result (infer-sample u.written-view env view-state)

13893 ?: ?=(%| -.sam) ~

@@ -13998,10 +13998,10 @@

13998 =/ checked=(map term def) (direct-checked-gates ds env)

13999 =/ templates=ienv

14000 (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))

14001− =/ scanned=(unit dgscan)

14001+ =/ fresh=(unit @ud)

14002− (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)

14002+ (ienv-fresh-id (weld env (weld values.u.prelude.initial templates)))

14003− ?~ scanned ~

14003+ ?~ fresh ~

14004− =. next.initial (dg-next-id ids.u.scanned 0)

14004+ =. next.initial u.fresh

14005 =/ view-state=istate (reserve-def-caps val.view-def initial)

14006 =/ sam=isample-result (infer-sample u.written-view env view-state)

14007 ?: ?=(%| -.sam) ~

@@ -14195,10 +14195,10 @@

14195 =/ checked=(map term def) (direct-checked-gates ds env)

14196 =/ templates=ienv

14197 (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))

14198− =/ scanned=(unit dgscan)

14198+ =/ fresh=(unit @ud)

14199− (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)

14199+ (ienv-fresh-id (weld env (weld values.u.prelude.initial templates)))

14200− ?~ scanned ~

14200+ ?~ fresh ~

14201− =. next.initial (dg-next-id ids.u.scanned 0)

14201+ =. next.initial u.fresh

14202 =/ init-state=istate (reserve-def-caps val.init-def initial)

14203 =/ sam=isample-result (infer-sample u.written env init-state)

14204 ?: ?=(%| -.sam) ~

@@ -14267,10 +14267,10 @@

14267 =/ checked=(map term def) (direct-checked-gates ds env)

14268 =/ templates=ienv

14269 (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))

14270− =/ scanned=(unit dgscan)

14270+ =/ fresh=(unit @ud)

14271− (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)

14271+ (ienv-fresh-id (weld env (weld values.u.prelude.initial templates)))

14272− ?~ scanned ~

14272+ ?~ fresh ~

14273− =. next.initial (dg-next-id ids.u.scanned 0)

14273+ =. next.initial u.fresh

14274 =/ instance=[typ=itype state=istate] (instantiate-scheme u.program initial)

14275 ?. ?=(%fn -.typ.instance) ~

14276 ?. ?=(%cell -.sample.typ.instance) ~

@@ -15637,9 +15637,9 @@

15637 =/ free=(unit dgscan) (dg-env base ~ 32.768 ~)

15638 ?~ free ~

15639 ?^ ids.u.free ~

15640− =/ all=(unit dgscan) (dg-all-env-ids base 32.768 ~)

15640+ =/ all=(unit @ud) (ienv-fresh-id base)

15641 ?~ all ~

15642− =/ fresh=@ud (dg-next-id ids.u.all 0)

15642+ =/ fresh=@ud u.all

15643 =/ st=istate *istate

15644 =. st st(next fresh, defer `~, molds molds, globals globals, at at, top-molds (turn molds |=(m=[name=term body=shape] name.m)), in-mold |, jrec-fuel 256)

15645 =/ checked-molds=(each imold-types @t) (module-mold-types molds st)

@@ -15679,33 +15679,60 @@

15679 =/ free=(unit dgscan) (dg-env all-env ~ 32.768 ~)

15680 ?~ free ~

15681 ?^ ids.u.free ~

15682− =/ all=(unit dgscan) (dg-all-env-ids all-env 32.768 ~)

15682+ =/ all=(unit @ud) (ienv-fresh-id all-env)

15683 ?~ all ~

15684− =/ fresh=@ud (dg-next-id ids.u.all 0)

15684+ =/ fresh=@ud u.all

15685 =/ st=istate *istate

15686 =. st st(next fresh, defer `~, molds local-molds, globals globals, at at, reserved-molds molds.prepared, prelude prelude, top-molds (turn local-molds |=(m=[name=term body=shape] name.m)), in-mold |, jrec-fuel 256)

15687 =/ checked-molds=(each imold-types @t) (module-mold-types local-molds st)

15688 ?: ?=(%| -.checked-molds) ~

15689 (dg-stage defs base base st ~ 64)

15690::

15691−++ dg-all-env-ids

15691+:: +ienv-fresh-id: one above the largest type variable or tag ID in env

15692+::

15693+:: One pass over every ID in env's schemes, quantified or free, so a

15694+:: variable numbered from it captures none of them. A %recursive or

15695+:: %jrec type names its mold and holds no variable, so it is a leaf,

15696+:: and the pass is linear in the size of the types, with no budget.

15697+:: A scheme that still holds an unresolved tag declines.

15698+::

15699+++ ienv-fresh-id

15692− |= [env=ienv fuel=@ud ids=(list @ud)]

15700+ |= env=ienv

15693− ^- (unit dgscan)

15701+ ^- (unit @ud)

15694− ?~ env `[ids fuel]

15702+ =/ top=@ud 0

15695− ?: =(0 fuel) ~

15703+ |-

15704+ ?~ env `+(top)

15696 =/ sc=ischeme scheme.i.env

15705 =/ sc=ischeme scheme.i.env

15697 ?: (itype-has-tag typ.sc) ~

15706 ?: (itype-has-tag typ.sc) ~

15698− =/ raw=(unit dgscan) (dg-scan ~[typ.sc] ~ (dec fuel) ids)

15707+ $(env t.env, top (itype-max-id typ.sc (max top (roll vars.sc max))))

15699− ?~ raw ~

15708+::

15700− =/ quant=(unit dgscan) (dg-scan-ids vars.sc ~ fuel.u.raw ids.u.raw)

15709+:: +itype-max-id: the largest variable or tag ID in t, or top

15701− ?~ quant ~

15702− $(env t.env, fuel fuel.u.quant, ids ids.u.quant)

15703::

15710::

15704−++ dg-next-id

15711+++ itype-max-id

15705− |= [ids=(list @ud) largest=@ud]

15712+ |= [t=itype top=@ud]

15713+ ^- @ud

15714+ ?- -.t

15715+ %var (max top id.t)

15716+ %fvar (max top id.t)

15717+ %avar (max top id.t)

15718+ %rvar (max top id.t)

15719+ %nvar (max top id.t)

15720+ %rnvar (max top id.t)

15721+ %tag (max top id.t)

15722+ ?(%atom %any-atom %flag %noun %empty %const %recursive %jrec) top

15723+ %collection (itype-max-ids args.t top)

15724+ %grec (itype-max-ids args.t top)

15725+ %union (itype-max-ids args.t (itype-max-ids cases.t top))

15726+ %face $(t body.t)

15727+ %fn $(t sample.t, top $(t product.t))

15728+ %cell $(t hed.t, top $(t tal.t))

15729+ ==

15730+::

15731+++ itype-max-ids

15732+ |= [ts=(list itype) top=@ud]

15706 ^- @ud

15733 ^- @ud

15707− ?~ ids +(largest)

15734+ ?~ ts top

15708− $(ids t.ids, largest (max largest i.ids))

15735+ $(ts t.ts, top (itype-max-id i.ts top))

15709::

15736::

15710++ dg-eligible-ctor

15737++ dg-eligible-ctor

15711 |= [e=expr head=itype actual=itype expected=itype state=istate]

15738 |= [e=expr head=itype actual=itype expected=itype state=istate]

tests/lib/jibb-deferred.hoon+4−8

@@ -78,11 +78,8 @@

78++ case-fresh

79 ^- (list @t)

80 =/ env=ienv:jibb ~[[%x [[%fn [%var 1.000.007] [%var 1.000.007]] ~[1.000.007 2.000.001]]]]

81− =/ scanned=(unit dgscan:jibb) (dg-all-env-ids:jibb env 200 ~)

82− =/ small=(unit dgscan:jibb) (dg-all-env-ids:jibb env 1 ~)

83− ?~ scanned ~['BAD-scan']

84− :~ ?:(=(2.000.002 (dg-next-id:jibb ids.u.scanned 0)) 'fresh ID exceeds raw and quantified IDs' 'BAD-fresh')

81+ :~ ?:(=(`2.000.002 (ienv-fresh-id:jibb env)) 'fresh ID exceeds raw and quantified IDs' 'BAD-fresh')

85− ?:(?=(~ small) 'fresh ID scan respects budget' 'BAD-fuel')

82+ ?:(=(`1 (ienv-fresh-id:jibb ~)) 'fresh ID of an empty environment is 1' 'BAD-empty')

86 ==

83 ==

87++ case-safety

84++ case-safety

88 ^- (list @t)

85 ^- (list @t)

@@ -178,10 +175,9 @@

178 ^- (list @t)

175 ^- (list @t)

179 =/ tree=itype:jibb [%grec /ui/test/jibb %tree ~ *shape:jibb ~[[%var 7]]]

176 =/ tree=itype:jibb [%grec /ui/test/jibb %tree ~ *shape:jibb ~[[%var 7]]]

180 =/ bounded=(unit dgscan:jibb) (dg-scan:jibb ~[tree] ~ 256 ~)

177 =/ bounded=(unit dgscan:jibb) (dg-scan:jibb ~[tree] ~ 256 ~)

181− =/ env=ienv:jibb ~[[%t [tree ~[7]]]]

178+ =/ env=ienv:jibb ~[[%t [tree ~[7]]] [%r [[%cell [%recursive %notes %node ~] [%var 9]] ~]]]

182− =/ all=(unit dgscan:jibb) (dg-all-env-ids:jibb env 256 ~)

183 :~ ?:(?=(~ bounded) 'grec constraint scan declines' 'BAD-grec-scan')

179 :~ ?:(?=(~ bounded) 'grec constraint scan declines' 'BAD-grec-scan')

184− ?:(?=(~ all) 'grec fresh-id scan declines' 'BAD-grec-freshness')

180+ ?:(=(`10 (ienv-fresh-id:jibb env)) 'fresh ID passes over grec arguments and recursive leaves' 'BAD-grec-freshness')

185 ==

181 ==

186++ case-default-behavior

182++ case-default-behavior

187 ^- @t

183 ^- @t

tests/type-deferred/expected.txt+2−2

@@ -13,7 +13,7 @@ local deferred definition declined

13recursive deferred group declined

14unused mold hole declined

15fresh ID exceeds raw and quantified IDs

16−fresh ID scan respects budget

16+fresh ID of an empty environment is 1

17original structural binding rejects wrong face

18dropping binding would accept wrong face

19unresolved edge remains open after fit

@@ -34,6 +34,6 @@ post-fit face asymmetry is absent

34record output stays cell-capable

35prebound incompatible callback is rejected

36grec constraint scan declines

37−grec fresh-id scan declines

37+fresh ID passes over grec arguments and recursive leaves

38default inference declines; explicit capability creates obligation

39candidate screen boundaries passed