c96597d · jibb · git.iko.soy

git.iko.soy/jibb

Track source-proven generic recursive identities

Retain opaque nominal identity for a bounded source-validated generic tree, including across supported module imports and aliases. Keep construction, matching and gate-freedom unresolved.

commitc96597db492b02d717c88e4a1a6d77082b5910f2 authoriko <mail@iko.soy> dateSat 31 Oct 2026, 13:57 (2 days ago) parent142f2e2

23 files changed+628−50

compare with master

unifiedsplit

README.md+1−1

@@ -42,7 +42,7 @@ tools/hoon '(golden /a/b/jibb (crip "++ main view"))'

4242tools/hoon --raw --cord src=tests/golden/foo/source.jibb 'tree:(golden /a/b/jibb src)'

4343```

4444

45−`tools/testdata/selftest` tests both tools against a stub library, and `tools/doc-blocks` against Markdown it writes. `tools/importer-test` compares the partial Hoon importer's fixture projections against their golden file. `tools/type-import-test`, `tools/type-import-overlap-test`, `tools/type-import-structural-test`, `tools/type-tlon-test`, `tools/type-mark-test`, `tools/type-poke-test` and `tools/type-api-paths-test` check importer/checker, prelude and partial API path analysis boundaries under eval; the ship suite runs the same fixtures.

45+`tools/testdata/selftest` tests both tools against a stub library, and `tools/doc-blocks` against Markdown it writes. `tools/importer-test` compares the partial Hoon importer's fixture projections against their golden file. `tools/type-import-test`, `tools/type-import-overlap-test`, `tools/type-import-structural-test`, `tools/type-generic-recursion-test`, `tools/type-tlon-test`, `tools/type-mark-test`, `tools/type-poke-test` and `tools/type-api-paths-test` check importer/checker, prelude and partial API path analysis boundaries under eval; the ship suite runs the same fixtures.

4646

4747### The doc's examples

4848

docs/compiler.md+3−1

@@ -56,7 +56,7 @@ The core is split into chapters, `+| %name`, in this order:

5656| `%span-check` | `+check-spans`, which `+golden` runs on every tree, and `+check-spans-test` |

5757| `%type-inference` | The initial inference fragment and its unification helpers; not yet a module type checker |

5858

59−The inference fragment supports fixed auras, unrestricted `@`, one-way widening into it and toward aura-family ancestors, generic variables and gates, faced and unfaced cells, cell sample binders, known record field reads, a cell pattern of two or more binders, a complete two-arm loobean branch, a complete two-arm unit-shaped branch, closed local mold aliases and acyclic forward value references. For a supported single syntactic top-level recursive gate, the checker infers the sample first and uses that exact sample, including its field faces, in a monomorphic self placeholder. The completed body must unify with the placeholder before the gate is generalized; incompatible recursive arguments can report the call and argument sites. Uses of generalized top-level definitions instantiate their schemes independently. For a complete loobean branch with one direct self-call arm, the checker can infer the other arm independently and use its closed, fully resolved type to seed the recursive result; it then checks the whole body. Open or pending base types do not seed the result, and other branch shapes still depend on the existing partial inference. A supported single local recursive gate also uses a monomorphic self reference while its body is checked, then generalizes variables free of its enclosing environment; captured variables remain shared. Acyclic local value definitions can refer forward. The checker collects written capitals per `++` before inference, excluding nested definitions: a capital used in an enclosing definition is shared with its locals, even when written later, while a capital introduced only in a local definition is generalized there. Sibling locals can introduce independent capitals with the same spelling; generic mold parameters keep their own scope. Top-level groups of syntactic gates are inferred together with monomorphic placeholders and shared substitutions, then generalized only after the whole group checks; downstream uses and library interfaces instantiate those schemes independently. A dependency graph identifies groups with two iterative depth-first passes; its conservative local-reference edges can reject otherwise valid programs. Supported local mutually recursive gate groups also use shared monomorphic placeholders and generalize only after the group checks, preserving captured outer variables. Some proven non-gate value cycles are diagnosed; other mixed gate/value cycles, polymorphic recursion, unresolved literal constraints and unresolved branch joins remain unsupported. Acyclic simple local mold aliases can also refer forward, and are scoped to the body, not its gate's sample. Nonrecursive generic aliases of supported molds can be applied at exact arity, including locally and through library interfaces; their parameters are lexical. Closed, provably disjoint nonrecursive unions and tagged single-case molds support contextual term values, `~` and `|=%tag` constructors. Literal heads compare by their runtime noun, so `|=%$` can construct an explicit null-, loobean-zero- or term-zero-headed case. Equal heads with distinct payloads can be selected when exactly one payload fit is proven; unknown or ambiguous alternatives remain unsupported. Unresolved tags and nulls remain pending, with distinct partial-inference diagnostics. Nonrecursive top-level generic union molds with provably disjoint cases also support contextual tags and constructors at exact arity; their arguments are retained through generalization and supported library interfaces. Nonrecursive generic aliases can reorder, repeat or omit parameters while preserving a supported union’s origin, including through local scopes and library interfaces. A generic union declared directly inside a body and recursive molds remain unsupported. A directly known named union can instantiate an unconstrained generic gate sample while retaining its origin, generic arguments and faces. Unnamed, pending-tag, recursive, unknown-atom and variable-bound union origins remain unsupported. A value with type variable `A` can fit a field whose type is that same `A`, including in generic union payloads and nested or repeated record fields. A differing-variable face constraint remains unsupported. When inference forces two distinct explicitly written capitals equal, it reports both source sites; forcing a capital to a concrete type remains unsupported in this fragment. It can infer and generalize atom constraints arising from explicit capitals or bare sample binders, preserve those constraints through aliases, instantiate them independently, and print multiple constraints. Unresolved decimal variables default to `@ud` for inferred types without gates; defaulting inside gate types and other constraint cases remain incomplete. It does not yet check a module, complete imports, general patterns, general deferred constraints, recursive molds, dependency cycles or most errors with both conflicting excerpts. Definite cast and call mismatches, incompatible branches and overlapping union cases report both sites and excerpts. Concrete branch results can join at an explicitly present parent aura or `@`. Some known tuple and record positions acquire matching faces; other variable-dependent face merges, general branch tag context and ambiguous call-result propagation remain unsupported; function compatibility involving nested `@` and variable-dependent joins remain unsupported except for equal types and the source-bound gate-sample proof below. For a single recursive gate outside a group, the reporting path repeats inference rather than instantiating its generalized interface inside its own body; a group report uses its stored schemes. This adds work, and the current dependency pass can take quadratic time on long forward chains; the milestone's speed target remains unverified. A separate conservative pass reports unions whose cases are provably disjoint or overlapping and leaves other cases unresolved; it does not claim the mold is checked. Unsupported forms are reported as such, and the partial output says the module has not been checked.

59+The inference fragment supports fixed auras, unrestricted `@`, one-way widening into it and toward aura-family ancestors, generic variables and gates, faced and unfaced cells, cell sample binders, known record field reads, a cell pattern of two or more binders, a complete two-arm loobean branch, a complete two-arm unit-shaped branch, closed local mold aliases and acyclic forward value references. For a supported single syntactic top-level recursive gate, the checker infers the sample first and uses that exact sample, including its field faces, in a monomorphic self placeholder. The completed body must unify with the placeholder before the gate is generalized; incompatible recursive arguments can report the call and argument sites. Uses of generalized top-level definitions instantiate their schemes independently. For a complete loobean branch with one direct self-call arm, the checker can infer the other arm independently and use its closed, fully resolved type to seed the recursive result; it then checks the whole body. Open or pending base types do not seed the result, and other branch shapes still depend on the existing partial inference. A supported single local recursive gate also uses a monomorphic self reference while its body is checked, then generalizes variables free of its enclosing environment; captured variables remain shared. Acyclic local value definitions can refer forward. The checker collects written capitals per `++` before inference, excluding nested definitions: a capital used in an enclosing definition is shared with its locals, even when written later, while a capital introduced only in a local definition is generalized there. Sibling locals can introduce independent capitals with the same spelling; generic mold parameters keep their own scope. Top-level groups of syntactic gates are inferred together with monomorphic placeholders and shared substitutions, then generalized only after the whole group checks; downstream uses and library interfaces instantiate those schemes independently. A dependency graph identifies groups with two iterative depth-first passes; its conservative local-reference edges can reject otherwise valid programs. Supported local mutually recursive gate groups also use shared monomorphic placeholders and generalize only after the group checks, preserving captured outer variables. Some proven non-gate value cycles are diagnosed; other mixed gate/value cycles, polymorphic recursion, unresolved literal constraints and unresolved branch joins remain unsupported. Acyclic simple local mold aliases can also refer forward, and are scoped to the body, not its gate's sample. Nonrecursive generic aliases of supported molds can be applied at exact arity, including locally and through library interfaces; their parameters are lexical. Closed, provably disjoint nonrecursive unions and tagged single-case molds support contextual term values, `~` and `|=%tag` constructors. Literal heads compare by their runtime noun, so `|=%$` can construct an explicit null-, loobean-zero- or term-zero-headed case. Equal heads with distinct payloads can be selected when exactly one payload fit is proven; unknown or ambiguous alternatives remain unsupported. Unresolved tags and nulls remain pending, with distinct partial-inference diagnostics. Nonrecursive top-level generic union molds with provably disjoint cases also support contextual tags and constructors at exact arity; their arguments are retained through generalization and supported library interfaces. Nonrecursive generic aliases can reorder, repeat or omit parameters while preserving a supported union’s origin, including through local scopes and library interfaces. Generic unions declared directly inside a body and recursive molds outside the source-proven slices described below remain unsupported. A directly known named union can instantiate an unconstrained generic gate sample while retaining its origin, generic arguments and faces. Unnamed, pending-tag, recursive, unknown-atom and variable-bound union origins remain unsupported. A value with type variable `A` can fit a field whose type is that same `A`, including in generic union payloads and nested or repeated record fields. A differing-variable face constraint remains unsupported. When inference forces two distinct explicitly written capitals equal, it reports both source sites; forcing a capital to a concrete type remains unsupported in this fragment. It can infer and generalize atom constraints arising from explicit capitals or bare sample binders, preserve those constraints through aliases, instantiate them independently, and print multiple constraints. Unresolved decimal variables default to `@ud` for inferred types without gates; defaulting inside gate types and other constraint cases remain incomplete. It does not yet check a module, complete imports, general patterns, general deferred constraints, recursive molds, dependency cycles or most errors with both conflicting excerpts. Definite cast and call mismatches, incompatible branches and overlapping union cases report both sites and excerpts. Concrete branch results can join at an explicitly present parent aura or `@`. Some known tuple and record positions acquire matching faces; other variable-dependent face merges, general branch tag context and ambiguous call-result propagation remain unsupported; function compatibility involving nested `@` and variable-dependent joins remain unsupported except for equal types and the source-bound gate-sample proof below. For a single recursive gate outside a group, the reporting path repeats inference rather than instantiating its generalized interface inside its own body; a group report uses its stored schemes. This adds work, and the current dependency pass can take quadratic time on long forward chains; the milestone's speed target remains unverified. A separate conservative pass reports unions whose cases are provably disjoint or overlapping and leaves other cases unresolved; it does not claim the mold is checked. Unsupported forms are reported as such, and the partial output says the module has not been checked.

6060

6161A direct unshadowed prelude call can use checked source layouts when a positional argument is a directly named, already inferred root gate. For two-slot function samples, the checker can match a named update against an unnamed generic gate sample without confusing a binder face with a nested record face. Both explicitly named slots must agree; source boundaries are evidence for this fit, not a call-arity rule. The source gate and prelude annotation must be available from their checked bindings. Local or dynamic gates, aliases without direct evidence, recursive or SCC placeholder bodies, other sample shapes and unresolved call-sample variables remain unsupported by this proof. Ordinary inference remains the fallback.

6262

@@ -94,6 +94,8 @@ A known closed union can also provide context to each arm of a complete loobean

9494

9595The separate `jibb-dev/lib/jibb-import.hoon` is an unfinished reader for selected Hoon type graphs. It handles named recursion, nested map, set, queue, list, unit, jar and jug arguments, direct ordered maps, and direct `$^` unions whose source branches can be proved disjoint. It also recognizes a direct ordered-map call with two simple named mold operands, as in Tlon `notes.log`, after validating provenance and operand source; revisiting the same map hold fails closed. It also reads ordered map fields in records when the map arguments are syntactically fixed atom molds and other fields are fixed atom molds or standard collections of static atom molds. Collection names must not be shadowed. The reader can also import a mark door sample, removing its outer sample face and validating its build subject. For a mark whose sample is exactly a named arm of its single Ford-imported `/sur` core, it can recover a source-proved nonrecursive union, including source-location wrappers around fields; recursive or unverified fallback results remain unsupported. The reader checks explicit Hoon `$%`, `$?` and `$^` unions against the Grammar’s disjointness rule, as @iko confirmed on 2026-10-30. For an explicit `$%` with distinct literal head tags, it can also prove restricted local named payload dependencies, including bare `~` fields, re-evaluate and validate each source branch, and recover the union before Hoon collapses it. The real Tlon `notes.u-note` exercises its `[%deleted ~]` case. A bounded fallback also recovers one level of local named tagged unions inside such a union, including Tlon `notes.u-notebook` and `notes.u-notes`. Source-proved tagged unions can also be wrapped in Hoon `$~` defaults, including a downstream union using Tlon `epic.saga`; the selected source and projected branches still undergo the same provenance and disjointness checks. The tagged-source helper peels up to four consecutive default wrappers, while default wrappers encountered inside dependency proofs consume the existing semantic-node budget. A source-proved nested self-recursive union retains its named owner, including Tlon `notes.import-node`; deeper, mutually recursive or unproven cases stay unsupported. The nested source proof has a 256-visit semantic-node budget, and source-location wrapper peeling is limited to four per node; Hoon evaluation and source scans are not metered. It rejects recursive or computed dependencies, inherited same-name collisions, unsupported nested unions and proofs exceeding a shared 4,096-node budget. It re-evaluates statically recognizable source branches before Hoon can collapse them, checks materialized fork cases, and rejects shapes it cannot prove disjoint. Static records may also have verified standard-collection and `path` siblings. One direct explicit union argument in a standard list, set, map or unit is accepted when its call wrapper and collection provenance are verified and its static cases are pairwise disjoint. A synthetic regression checks that forged wrapper subjects, samples and tails are rejected. Other collection-union forms, nested ordered maps, general source-level disjointness and complete integration with the checker remain unfinished. `+golden-types-imports` can consume fixed-aura atoms, valid term singletons, Hoon's `%n` zero singleton as Jibb `~`, nested faced or unfaced cells, unions of supported, pairwise-disjoint cases, and opaque standard collections with supported arguments from caller-supplied reader results for declared `/-` imports; `+golden-types-with-marks` accepts the same shapes for declared marks. The caller must pass unchanged results from the source-aware reader: the bridge validates the supplied graph but cannot detect source cases Hoon collapsed before that graph was built. The opaque collection types retain their names and arguments for identity, unification and printing. The validated standard prelude `list` mold shares the imported list representation; other Jibb-written collection molds and most prelude collection operations remain unsupported. Other forms remain unsupported. Its disjointness proof is conservative and can reject a valid union it cannot prove disjoint. Collection recognition requires the originating `/sur` core. The reader validates direct zuse subjects and Ford subjects consisting of faced imported cores and a validated tail, checking imported cores transitively; it rejects shadowed names, inconsistent core subjects and other subject shapes. For a recursive reference, the reader matches the exact Hoon hold against named arms in validated cores, including transitive Ford imports; it rejects missing, unlabelled or ambiguous origins. Its fixtures include three real Tlon files; `tools/importer-test` compares the internal projection under eval, and the ship test compares the same golden output. `tools/type-import-test` and `tools/type-mark-test` compare bridge reports under eval and on the ship. `tools/type-tlon-test` and its ship counterpart exercise four real Tlon presence unions and a field read through the source-aware reader and partial checker. `tools/clay-fixtures` also passes Clay-built `/sur` molds and mark samples through the Clay-built importer and partial checker.

9696

97+An import-free Jibb library can export an opaque single-parameter recursive identity when its source has exactly two distinct term-tagged cases: a text leaf and a node containing `(list (name M))`, optionally with one `$-(@t M)` event field. A module-local index records the exact parsed source, defining path and prepared prelude interface; it is shared across that module's inference passes, and its canonical `list` must be source-backed. The normal resolver publishes an interface only after all ordinary mold and value checks succeed. Same-origin aliases retain the defining identity and independently instantiate type arguments; distinct origins remain unsupported. The opaque identity is conservatively treated as gate-bearing for numeric defaulting, and gate-freedom remains unknown. Recursive source with imports, local recursive molds, construction, matching and structural unfolding are not supported by this slice; the test tree does not prescribe the eventual `element` representation. Caller-supplied detached interfaces and caches retain the existing trusted-input contract.

98+

9799Self-recursive `/sur` molds can cross the bridge as opaque module-and-name identities when their supported source-aware graph passes validation, including one-argument lists containing same-origin recursive references. The real Tlon `notes.import-node` reaches this bridge; it does not unfold or construct the recursive type. Aliases, foreign references, recursive marks, unfolding, construction and field access remain unsupported; the partial printer declines recursive names that are not in scope.

98100

99101The partial checker also recognizes a source-proven Jibb recursive mold consisting of `~` and one faced cell with a fixed-aura head and direct self tail. Its identity includes the defining path and name. It unfolds this shape for supported null and cell construction and for a two-arm null/cell match; static application-path literals use the verified public `qath` alias. The internal prelude defines `qath` as a transparent knot sequence and the public prelude re-exports it. Each inference attempt has 256 unfolding and static-segment steps; parsing and separate retries are not bounded by that limit. Dynamic application-path segments, broader patterns and other recursive shapes remain unsupported. Route and static-file existence checks remain milestone 4.

docs/development.md+2

@@ -72,6 +72,7 @@ git clone https://github.com/urbit/tools /root/src/tools

7272| `tools/type-api-evidence-test` | Runs source, scope, reader-result and declaration-watchability evidence guards under eval and on the ship |

7373| `tools/type-hole-guards-test` | Runs the shared hole-defaulting and API interface guards under eval; the same checks run on the ship |

7474| `tools/type-list-alias-test` | Runs the shared prelude list-alias and provenance guards under eval and on the ship |

75+| `tools/type-generic-recursion-test` | Checks source-backed generic recursive identity and provenance under eval and on the ship |

7576| `tools/type-generic-alias-test` | Runs public/private generic union alias and provenance guards under eval and on the ship |

7677| `tools/type-positional-face-guards-test` | Runs positional-call and nested-face guards under eval and on the ship |

7778| `tools/type-qath-guards-test` | Runs source-provenance, recursive unfolding and face guards under eval and on the ship |

@@ -122,6 +123,7 @@ tools/type-qath-guards-test # qath source and unfolding guards pass

122123tools/type-todo-partial-test # unchanged todo partial report and reader failure controls

123124tools/type-todo-api-test # real todo API partial inference and reader guards pass

124125tools/type-direct-gate-test # direct gate source and provenance guards pass

126+tools/type-generic-recursion-test # source-backed recursive identities and provenance

125127tools/type-closed-gate-guards-test # closed gate fit guards pass

126128tools/type-constructor-fit-guards-test # constructor fit guards pass

127129tools/type-nested-union-guards-test # nested union selector guards pass

docs/status.md+7−3

@@ -23,7 +23,9 @@ The parser accepts `_` in mold positions and typed path segments, retaining each

2323

2424On 2026-10-31, @iko chose explicit, result-directed `(proj record)` to construct a record with exactly the expected fields, and reserved `proj` against definitions and imports. The partial checker handles selected explicit calls with known, closed record types, records field-selection evidence for later lowering, and reserves the name across source bindings. Reordered fields, some nested contexts and several open or recursive cases remain unsupported; lowering and execution are not implemented yet. The field-order question remains open.

2525

26−The internal prelude also defines `qath` as a transparent recursive knot sequence, re-exported by the public prelude. The partial checker recognizes its source identity, supports selected null/cell construction and matching, and types static application-path literals. Other recursive shapes, broader patterns and dynamic application-path segments remain unsupported. A 256-step limit applies per inference attempt, not to parsing or retries; checking routes and static files remains milestone 4.

26+The internal prelude also defines `qath` as a transparent recursive knot sequence, re-exported by the public prelude. The partial checker recognizes its source identity, supports selected null/cell construction and matching, and types static application-path literals. Construction and matching for other recursive shapes, broader patterns and dynamic application-path segments remain unsupported. A 256-step limit applies per inference attempt, not to parsing or retries; checking routes and static files remains milestone 4.

27+

28+The checker also recognizes a limited source-proven generic recursive tree in an import-free defining module. Its opaque identity retains the defining path, mold name and type arguments, including across supported imports and aliases. Construction, pattern matching, unfolding and gate-free proof for this shape remain unsupported; this is not yet the prelude's `element` implementation or island checking. The source index uses fixed-shape checks during mold collection. A single startup-inclusive comparison of 1,000 ordinary gates produced identical reports and used 29.12 seconds of user CPU before the shared-resolver refactor and 28.55 seconds after it, with other work running; it is not a general performance bound.

2729

2830The internal prelude defines a transparent generic `ask` with pure, agent and store cases, re-exported alongside the Jibb-written `pure` gate. The partial checker infers supported constructors and exhaustive matches. Agent and store receivers operate on raw nouns; their fields do not prove schema validity or watchability. The public prelude now defines the documented source-backed `sub` union; supported `%watch` payloads retain the public `(ask M)` type. Constructing a `sub` does not prove that its request is watchable. Request lowering, checked decoding, runtime validation and island watch checking remain unimplemented.

2931

@@ -72,7 +74,7 @@ What the plan asks for, and where it is:

7274Besides the plan's list:

7375

7476- 652 golden cases: 432 that parse and 220 that fail, each failure at a stated line and column. One failing case has an unclear expectation (corpus question 3). The newer type-output cases exercise only the partial inference fragment. Each case's `about.txt` quotes the doc's words it tests.

75−- The 652-case corpus passed under `urbit eval` in 112.2 s while other checks were running. The fake ship passed all 686 tests, including the source-overlap and structural-overlap fixtures, importer, importer/checker and mark/checker bridges, module scope, unification, hole, qath, ask, default-wrapper importer, projection, arithmetic, generic-alias, positional-face, API-evidence, request, closed-gate, todo API, constructor, sub, nested-union, gate-free and direct-gate guards and the unchanged todo report. Desk sync took 83.2 s while other checks were running. The importer golden compares 221 projections; `tools/clay-fixtures` builds the example Hoon fixtures through Clay, checks a recursive Ford import's origin, and passes Clay-built types through the Clay-built importer and partial checker.

77+- The 652-case corpus passed under `urbit eval` in 110.7 s while other checks were running. The fake ship passed all 687 tests, including the source-overlap, structural-overlap and generic-recursion fixtures, importer, importer/checker and mark/checker bridges, module scope, unification, hole, qath, ask, default-wrapper importer, projection, arithmetic, generic-alias, positional-face, API-evidence, request, closed-gate, todo API, constructor, sub, nested-union, gate-free and direct-gate guards and the unchanged todo report. Desk sync took 90.8 s while other checks were running. The importer golden compares 221 projections; `tools/clay-fixtures` builds the example Hoon fixtures through Clay, checks a recursive Ford import's origin, and passes Clay-built types through the Clay-built importer and partial checker.

7678- `tools/testdata/selftest` (22 checks), `tools/testdata/ship-selftest` and `tools/testdata/clay-fixtures-selftest` test the tools themselves; the last checks temporary Clay fixture cleanup and signal handling without a ship.

7779- Two independent audits before 7c739b7, one of which compared the library with a reference parser written in Python from the doc over about 19,000 generated programs. Before ab797a9, a second Python parser, written from the decisions, agreed with the library on 8,000 generated programs and 900 hand-written probes.

7880- Speed: starting `urbit eval` and building the library takes about 8 s. After that, a 2,000-line module of 400 definitions parses in about a second. Loops over definitions, arms, lines and items grow no stack; nesting costs a few stack frames a level, and 100,000 nested brackets still parse (library section 3).

@@ -174,7 +176,8 @@ Besides the plan's list:

174176| 4da6891 | 2026-10-31 | Add source-backed comparisons and nested Hoon union controls |

175177| 09db390 | 2026-10-31 | Skip unnecessary inference environment scans |

176178| 179d717 | 2026-10-31 | Diagnose source-proven Hoon union overlaps |

177−| This change | 2026-10-31 | Prove structural overlaps across Hoon union cases |

179+| 142f2e2 | 2026-10-31 | Prove structural overlaps across Hoon union cases |

180+| This change | 2026-10-31 | Track source-proven generic recursive identities |

178181

179182## Checking it

180183

@@ -195,6 +198,7 @@ tools/type-api-paths-test # partial API path metadata fixture

195198tools/type-hole-guards-test # hole defaulting and API interface guards

196199tools/type-list-alias-test # prelude list-alias guards

197200tools/type-generic-alias-test # generic union alias guards

201+tools/type-generic-recursion-test # source-proven generic recursion guards

198202tools/type-positional-face-guards-test # positional sample face guards

199203tools/type-qath-guards-test # qath source and unfolding guards

200204tools/type-ask-guards-test # ask source and bootstrap guards

jibb-dev/lib/jibb.hoon+231−45

@@ -4672,6 +4672,7 @@

46724672 [%collection name=term args=(list itype)]

46734673 [%recursive module=term name=term label=(unit @t)]

46744674 [%jrec at=path name=term label=(unit @t) head=term aura=@ta tail=term]

4675+ [%grec at=path name=term label=(unit @t) proof=shape args=(list itype)]

46754676 [%union cases=(list itype) origin=(unit [at=path name=term]) label=(unit @t) args=(list itype)]

46764677 [%face name=term body=itype]

46774678 [%fn sample=itype product=itype]

@@ -4743,6 +4744,7 @@

47434744 %union |((lien cases.t |=(c=itype (itype-occurs n c sub))) (lien args.t |=(c=itype (itype-occurs n c sub))))

47444745 %recursive |

47454746 %jrec |

4747+ %grec (lien args.t |=(c=itype (itype-occurs n c sub)))

47464748 %collection (lien args.t |=(c=itype (itype-occurs n c sub)))

47474749 %face $(t body.t)

47484750 %fn |($(t sample.t) $(t product.t))

@@ -4761,6 +4763,9 @@

47614763 =. a (itype-walk a sub)

47624764 =. b (itype-walk b sub)

47634765 ?: =(a b) `sub

4766+ ?: &(?=(%grec -.a) ?=(%grec -.b))

4767+ ?. &(=(at.a at.b) =(name.a name.b)) ~

4768+ (itype-unify-args args.a args.b sub)

47644769 ?: &(?=(%jrec -.a) ?=(%jrec -.b))

47654770 ?:(&(=(at.a at.b) =(name.a name.b) =(head.a head.b) =(aura.a aura.b) =(tail.a tail.b)) `sub ~)

47664771 ?: &(?=(%recursive -.a) ?=(%recursive -.b))

@@ -4871,6 +4876,7 @@

48714876 %union |((lien cases.t |=(c=itype (itype-has-any-atom c sub))) (lien args.t |=(c=itype (itype-has-any-atom c sub))))

48724877 %recursive |

48734878 %jrec |

4879+ %grec (lien args.t |=(c=itype (itype-has-any-atom c sub)))

48744880 %collection (lien args.t |=(c=itype (itype-has-any-atom c sub)))

48754881 %face $(t body.t)

48764882 %fn |($(t sample.t) $(t product.t))

@@ -4945,6 +4951,7 @@

49454951 %union |((lien cases.typ |=(c=itype (itype-has-fixed-atom c))) (lien args.typ |=(c=itype (itype-has-fixed-atom c))))

49464952 %recursive |

49474953 %jrec |

4954+ %grec (lien args.typ |=(c=itype (itype-has-fixed-atom c)))

49484955 %collection (lien args.typ |=(c=itype (itype-has-fixed-atom c)))

49494956 %face $(typ body.typ)

49504957 %fn |($(typ sample.typ) $(typ product.typ))

@@ -4973,6 +4980,7 @@

49734980 ^- ?

49744981 =. t (itype-walk t sub)

49754982 ?- -.t

4983+ %grec (lien args.t |=(c=itype (itype-has-face c sub)))

49764984 %collection (lien args.t |=(c=itype (itype-has-face c sub)))

49774985 %face &

49784986 %cell |($(t hed.t) $(t tal.t))

@@ -5029,6 +5037,9 @@

50295037 ^- ?

50305038 =. a (itype-walk a sub)

50315039 =. b (itype-walk b sub)

5040+ ?: &(?=(%grec -.a) ?=(%grec -.b))

5041+ ?. &(=(at.a at.b) =(name.a name.b)) |

5042+ (itype-face-asym-collection-args args.a args.b sub)

50325043 ?: &(?=(%collection -.a) ?=(%collection -.b))

50335044 ?. =(name.a name.b) |

50345045 (itype-face-asym-collection-args args.a args.b sub)

@@ -5091,6 +5102,7 @@

50915102 %union &

50925103 %recursive &

50935104 %jrec &

5105+ %grec &

50945106 %noun &

50955107 %collection &

50965108 %face $(t body.t)

@@ -5120,6 +5132,7 @@

51205132 ^- ?

51215133 ?- -.t

51225134 %tag &

5135+ %grec (lien args.t |=(c=itype (itype-has-tag c)))

51235136 %collection (lien args.t |=(c=itype (itype-has-tag c)))

51245137 %face $(t body.t)

51255138 %fn |($(t sample.t) $(t product.t))

@@ -5133,6 +5146,7 @@

51335146 ^- ?

51345147 ?- -.t

51355148 %union &

5149+ %grec (lien args.t |=(c=itype (itype-has-union c)))

51365150 %collection (lien args.t |=(c=itype (itype-has-union c)))

51375151 %face $(t body.t)

51385152 %fn |($(t sample.t) $(t product.t))

@@ -5151,6 +5165,7 @@

51515165 %union

51525166 ?: &(?=(~ label.t) ?=(^ args.t)) &

51535167 (lien (weld args.t cases.t) |=(c=itype (itype-has-hidden-generic c)))

5168+ %grec |(?=(~ label.t) (lien args.t |=(c=itype (itype-has-hidden-generic c))))

51545169 %collection (lien args.t |=(c=itype (itype-has-hidden-generic c)))

51555170 %face $(t body.t)

51565171 %fn |($(t sample.t) $(t product.t))

@@ -5164,6 +5179,7 @@

51645179 ?- -.t

51655180 %recursive &

51665181 %jrec &

5182+ %grec &

51675183 %collection (lien args.t |=(c=itype (itype-has-recursive c)))

51685184 %union (lien (weld args.t cases.t) |=(c=itype (itype-has-recursive c)))

51695185 %face $(t body.t)

@@ -5178,6 +5194,7 @@

51785194 ?- -.t

51795195 %recursive ?=(~ label.t)

51805196 %jrec ?=(~ label.t)

5197+ %grec |(?=(~ label.t) (lien args.t |=(c=itype (itype-has-hidden-recursive c))))

51815198 %collection (lien args.t |=(c=itype (itype-has-hidden-recursive c)))

51825199 %union (lien (weld args.t cases.t) |=(c=itype (itype-has-hidden-recursive c)))

51835200 %face $(t body.t)

@@ -5223,7 +5240,7 @@

52235240 ?: ?=(%var -.raw)

52245241 $(cases t.cases, pending &)

52255242 =/ c=itype (itype-walk raw sub)

5226− ?: ?=(?(%var %tag %recursive %jrec %union %face) -.c)

5243+ ?: ?=(?(%var %tag %recursive %jrec %grec %union %face) -.c)

52275244 $(cases t.cases, pending &)

52285245 ?. ?=(%cell -.c) $(cases t.cases)

52295246 =/ raw-head=itype hed.c

@@ -5236,7 +5253,7 @@

52365253 ?: ?=(?(%atom %any-atom %flag %avar %rvar %nvar %rnvar) -.body.head)

52375254 $(cases t.cases)

52385255 $(cases t.cases, pending &)

5239− ?: ?=(?(%var %tag %recursive %jrec %union) -.head)

5256+ ?: ?=(?(%var %tag %recursive %jrec %grec %union) -.head)

52405257 $(cases t.cases, pending &)

52415258 ?. ?=(%const -.head) $(cases t.cases)

52425259 ?. =(val.literal.head val.tag) $(cases t.cases)

@@ -5285,6 +5302,14 @@

52855302 [%ok sub next]

52865303 :: An arbitrary noun is not known to fit a narrower type.

52875304 ?: &(?=(%noun -.actual) !?=(%var -.expected)) [%unknown ~]

5305+ ?: &(!uncertain ?=(%grec -.actual) ?=(%face -.expected)) $(expected body.expected)

5306+ ?: &(!uncertain ?=(%face -.actual) ?=(%grec -.expected)) $(actual body.actual)

5307+ ?: &(?=(%grec -.actual) ?=(%grec -.expected))

5308+ ?. &(=(at.actual at.expected) =(name.actual name.expected)) [%unknown ~]

5309+ =/ matched=(unit isub) (itype-unify-args args.actual args.expected sub)

5310+ ?~ matched [%unknown ~]

5311+ [%ok u.matched next]

5312+ ?: &(|(?=(%grec -.actual) ?=(%grec -.expected)) !|(?=(%var -.actual) ?=(%var -.expected))) [%unknown ~]

52885313 ?: &(!uncertain ?=(%jrec -.actual) ?=(%face -.expected)) $(expected body.expected)

52895314 ?: &(!uncertain ?=(%face -.actual) ?=(%jrec -.expected)) $(actual body.actual)

52905315 ?: &(?=(%jrec -.actual) ?=(%jrec -.expected))

@@ -5674,10 +5699,11 @@

56745699 %tag [%unknown | fuel ~]

56755700 %recursive [%unknown | fuel ~]

56765701 %jrec [%yes & fuel ~]

5702+ %grec [%unknown | fuel ~]

56775703 ==

56785704::

56795705+$ igate-prelude-evidence [iface=ifile gates=(map term def)]

5680−+$ istate [next=@ud sub=isub caps=icaps binders=(list @ud) molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) params=iparams active=(list term) tags=(list ipending) in-mold=? at=path top-molds=(list term) prelude=(unit ifile) holes=(list ihole) jrec-fuel=@ud projections=(list iwprojection) gate-defs=(map term def) head-evidence=(unit igate-prelude-evidence)]

5706++$ istate [next=@ud sub=isub caps=icaps binders=(list @ud) molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) params=iparams active=(list term) tags=(list ipending) in-mold=? at=path top-molds=(list term) prelude=(unit ifile) holes=(list ihole) jrec-fuel=@ud projections=(list iwprojection) gate-defs=(map term def) head-evidence=(unit igate-prelude-evidence) grec-index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])]

56815707+$ idiag [msg=tape sites=(list [at=span note=tape])]

56825708+$ iresult (each [typ=itype state=istate] idiag)

56835709+$ isample-result (each [typ=itype env=ienv state=istate] tape)

@@ -5697,6 +5723,7 @@

56975723 |= [t=itype sub=isub]

56985724 ^- itype

56995725 =. t (itype-walk t sub)

5726+ ?: ?=(%grec -.t) t(args (turn args.t |=(c=itype (itype-normalize c sub))))

57005727 ?: ?=(%collection -.t) [%collection name.t (turn args.t |=(c=itype (itype-normalize c sub)))]

57015728 ?: ?=(%union -.t)

57025729 [%union (turn cases.t |=(c=itype (itype-normalize c sub))) origin.t label.t (turn args.t |=(c=itype (itype-normalize c sub)))]

@@ -5723,6 +5750,7 @@

57235750 %cell |($(t hed.t) $(t tal.t))

57245751 %recursive |

57255752 %jrec |

5753+ %grec &

57265754 %collection (lien args.t |=(c=itype (itype-has-gate c)))

57275755 %face $(t body.t)

57285756 %union (lien cases.t |=(c=itype (itype-has-gate c)))

@@ -5746,6 +5774,7 @@

57465774 ?- -.t

57475775 %nvar [%atom %ud]

57485776 %rnvar [%atom %ud]

5777+ %grec t(args (turn args.t |=(c=itype (default-decimals c))))

57495778 %collection [%collection name.t (turn args.t |=(c=itype (default-decimals c)))]

57505779 %face [%face name.t $(t body.t)]

57515780 %cell [%cell $(t hed.t) $(t tal.t)]

@@ -5787,6 +5816,7 @@

57875816 %tag |

57885817 %any-atom &

57895818 %union &((levy cases.t |=(c=itype (hole-known c state))) (levy args.t |=(c=itype (hole-known c state))))

5819+ %grec (levy args.t |=(c=itype (hole-known c state)))

57905820 %collection (levy args.t |=(c=itype (hole-known c state)))

57915821 %face $(t body.t)

57925822 %fn &($(t sample.t) $(t product.t))

@@ -5834,6 +5864,7 @@

58345864 ?- -.t

58355865 ?(%tag %nvar %rnvar %avar %rvar) !(hole-known t state)

58365866 %union |((lien cases.t |=(c=itype (hole-uncertain c state))) (lien args.t |=(c=itype (hole-uncertain c state))))

5867+ %grec (lien args.t |=(c=itype (hole-uncertain c state)))

58375868 %collection (lien args.t |=(c=itype (hole-uncertain c state)))

58385869 %face $(t body.t)

58395870 %fn |($(t sample.t) $(t product.t))

@@ -5870,6 +5901,7 @@

58705901 %union (zing (turn (weld args.t cases.t) |=(c=itype (itype-vars c))))

58715902 %recursive ~

58725903 %jrec ~

5904+ %grec (zing (turn args.t |=(c=itype (itype-vars c))))

58735905 %collection (zing (turn args.t |=(c=itype (itype-vars c))))

58745906 %face $(t body.t)

58755907 %fn (weld $(t sample.t) $(t product.t))

@@ -5918,6 +5950,7 @@

59185950 %union [%union (turn cases.t |=(c=itype (itype-rename c ren))) origin.t label.t (turn args.t |=(c=itype (itype-rename c ren)))]

59195951 %recursive t

59205952 %jrec t

5953+ %grec t(args (turn args.t |=(c=itype (itype-rename c ren))))

59215954 %collection [%collection name.t (turn args.t |=(c=itype (itype-rename c ren)))]

59225955 %face [%face name.t $(t body.t)]

59235956 %fn [%fn $(t sample.t) $(t product.t)]

@@ -5945,6 +5978,7 @@

59455978 %union |((lien cases.t |=(c=itype (itype-var-is-atom n c))) (lien args.t |=(c=itype (itype-var-is-atom n c))))

59465979 %recursive |

59475980 %jrec |

5981+ %grec (lien args.t |=(c=itype (itype-var-is-atom n c)))

59485982 %collection (lien args.t |=(c=itype (itype-var-is-atom n c)))

59495983 %face $(t body.t)

59505984 %fn |($(t sample.t) $(t product.t))

@@ -5968,6 +6002,7 @@

59686002 %union |((lien cases.t |=(c=itype (itype-var-is-restricted n c))) (lien args.t |=(c=itype (itype-var-is-restricted n c))))

59696003 %recursive |

59706004 %jrec |

6005+ %grec (lien args.t |=(c=itype (itype-var-is-restricted n c)))

59716006 %collection (lien args.t |=(c=itype (itype-var-is-restricted n c)))

59726007 %face $(t body.t)

59736008 %fn |($(t sample.t) $(t product.t))

@@ -6398,6 +6433,16 @@

63986433 ?: &(?=(~ vars.template) ?=(%jrec -.typ.template) =(at.typ.template origin) =(name.typ.template name)) `name.i.molds

63996434 $(molds t.molds)

64006435::

6436+++ grec-visible-alias

6437+ |= [origin=path name=term proof=shape args=(list itype) molds=imold-types]

6438+ ^- (unit term)

6439+ ?~ molds ~

6440+ =/ template=ischeme template.i.molds

6441+ ?. ?=(%grec -.typ.template) $(molds t.molds)

6442+ ?. &(=(at.typ.template origin) =(name.typ.template name) =(proof.typ.template proof)) $(molds t.molds)

6443+ ?. &((identity-union-parameters vars.template args.typ.template) =((lent vars.template) (lent args))) $(molds t.molds)

6444+ `name.i.molds

6445+::

64016446++ itype-in-import

64026447 |= [t=itype iface=ifile face=term prelude=(unit ifile)]

64036448 ^- itype

@@ -6417,6 +6462,11 @@

64176462 `(crip "{(trip u.alias)}.{(trip face)}")

64186463 [%union (turn cases.t |=(c=itype (itype-in-import c iface face prelude))) origin.t label (turn args.t |=(c=itype (itype-in-import c iface face prelude)))]

64196464 %recursive [%recursive module.t name.t ~]

6465+ %grec

6466+ =/ public=(unit term) ?~(prelude ~ (grec-visible-alias at.t name.t proof.t args.t molds.u.prelude))

6467+ =/ alias=(unit term) ?~(public (grec-visible-alias at.t name.t proof.t args.t molds.iface) public)

6468+ =/ label=(unit @t) ?~(alias ~ ?~(public `(crip "{(trip u.alias)}.{(trip face)}") `u.alias))

6469+ t(label label, args (turn args.t |=(c=itype (itype-in-import c iface face prelude))))

64206470 %jrec

64216471 =/ public=(unit term) ?~(prelude ~ (jrec-alias at.t name.t molds.u.prelude))

64226472 ?^ public t(label `u.public)

@@ -6529,9 +6579,29 @@

65296579 ?. =(names.tail ~[name]) ~

65306580 `[%jrec at.state name `name name.i.fs aura.shape.i.fs name.i.t.fs]

65316581::

6582+++ simple-source-generic-recursive

6583+ |= [name=term sh=shape args=(list itype) state=istate]

6584+ ^- (unit itype)

6585+ ?. ?=(%generic -.sh) ~

6586+ ?. ?=([@ ~] vars.sh) ~

6587+ ?. ?=([* ~] args) ~

6588+ ?~ grec-index.state ~

6589+ ?. =(at.u.grec-index.state at.state) ~

6590+ ?~ prelude.state ~

6591+ ?. =(prelude.u.grec-index.state u.prelude.state) ~

6592+ =/ proof=(unit shape) (~(get by shapes.u.grec-index.state) name)

6593+ ?~ proof ~

6594+ ?. =(u.proof sh) ~

6595+ `[%grec at.state name `name sh args]

6596+::

6597+

65326598++ infer-mold-template

65336599 |= [sh=shape state=istate]

65346600 ^- (unit [template=ischeme state=istate])

6601+ =/ generic=(unit itype)

6602+ ?. ?=([@ ~] active.state) ~

6603+ (simple-source-generic-recursive i.active.state sh ~[[%var next.state]] state)

6604+ ?^ generic `[[u.generic ~[next.state]] state(next +(next.state))]

65356605 =/ direct=(unit itype)

65366606 ?. ?=([@ ~] active.state) ~

65376607 (simple-source-recursive i.active.state sh state)

@@ -6744,6 +6814,8 @@

67446814 ?~ applied ~

67456815 `[u.applied state.u.args]

67466816 ?. ?=(%generic -.u.found) ~

6817+ =/ grec=(unit itype) (simple-source-generic-recursive n u.found types.u.args state.u.args)

6818+ ?^ grec `[u.grec state.u.args]

67476819 ?. (distinct-params vars.u.found) ~

67486820 =/ params=(unit iparams) (bind-params vars.u.found types.u.args)

67496821 ?~ params ~

@@ -8982,7 +9054,7 @@

89829054 ?~ t.names |

89839055 =. typ (itype-walk typ sub)

89849056 ?: ?=(%cell -.typ) $(typ tal.typ, names t.names)

8985− |(?=(%union -.typ) ?=(%collection -.typ) ?=(%recursive -.typ) ?=(%jrec -.typ) ?=(%noun -.typ) ?=(%fn -.typ) ?=(%tag -.typ))

9057+ |(?=(%union -.typ) ?=(%collection -.typ) ?=(%recursive -.typ) ?=(%jrec -.typ) ?=(%grec -.typ) ?=(%noun -.typ) ?=(%fn -.typ) ?=(%tag -.typ))

89869058::

89879059++ cell-binder-pattern

89889060 |= e=expr

@@ -9061,6 +9133,7 @@

90619133 "({(trip u.label.t)} {(show-itype-cases args.t sub)})"

90629134 %recursive ?~(label.t "recursive mold" (trip u.label.t))

90639135 %jrec ?~(label.t "recursive mold" (trip u.label.t))

9136+ %grec ?~(label.t "recursive mold" "({(trip u.label.t)} {(show-itype-cases args.t sub)})")

90649137 %collection "({(trip name.t)} {(show-itype-cases args.t sub)})"

90659138 %face "[{(trip name.t)}={(show-itype-context body.t sub)}]"

90669139 %fn "$-({(show-itype-context sample.t sub)} {(show-itype-context product.t sub)})"

@@ -9109,6 +9182,7 @@

91099182 %union |((lien cases.typ |=(c=itype (itype-has-nvar c))) (lien args.typ |=(c=itype (itype-has-nvar c))))

91109183 %recursive |

91119184 %jrec |

9185+ %grec (lien args.typ |=(c=itype (itype-has-nvar c)))

91129186 %collection (lien args.typ |=(c=itype (itype-has-nvar c)))

91139187 %face $(typ body.typ)

91149188 %fn |($(typ sample.typ) $(typ product.typ))

@@ -9225,6 +9299,7 @@

92259299 %union |((lien cases.t |=(c=itype (has-atom-var n c))) (lien args.t |=(c=itype (has-atom-var n c))))

92269300 %recursive |

92279301 %jrec |

9302+ %grec (lien args.t |=(c=itype (has-atom-var n c)))

92289303 %collection (lien args.t |=(c=itype (has-atom-var n c)))

92299304 %face $(t body.t)

92309305 %fn |($(t sample.t) $(t product.t))

@@ -9633,36 +9708,9 @@

96339708++ add-supported-defs

96349709 |= [ds=(list def) all-defs=(list def) checked=(map term def) heads=(unit igate-prelude-evidence) env=ienv molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile) artifacts=(list iwidth-definition)]

96359710 ^- [env=ienv artifacts=(list iwidth-definition)]

9636− ?~ ds [env artifacts]

9637− =/ d=def i.ds

9638− ?: ?=(%mold -.d) $(ds t.ds)

9639− ?. (unique-value-name name.d globals) $(ds t.ds)

9640− ?^ (ienv-lookup name.d env) $(ds t.ds)

9641− =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))

9642− =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~]

9643− =. gate-defs.initial checked

9644− =. head-evidence.initial heads

9645− =. initial (reserve-def-caps val.d initial)

9646− =/ result=iresult (infer-fragment val.d env initial)

9647− =? result ?=(%| -.result) (infer-recursive-gate d env initial)

9648− ?: ?=(%| -.result) $(ds t.ds)

9649− =. state.p.result (promote-restricted-numbers state.p.result env)

9650− =. state.p.result (default-hole-numbers holes.state.p.result holes.initial state.p.result env !(itype-has-gate (itype-normalize typ.p.result sub.state.p.result)))

9651− ?^ (unresolved-hole holes.state.p.result holes.initial state.p.result) $(ds t.ds)

9652− ?: (constrained-capitals caps.state.p.result sub.state.p.result) $(ds t.ds)

9653− =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))

9654− ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) $(ds t.ds)

9655− ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) $(ds t.ds)

9656− =/ vars=(list @ud) (unique-type-vars (itype-vars typ))

9657− ?: (gth (lent vars) 26) $(ds t.ds)

9658− =/ finalized=(unit (list iwprojection))

9659− (width-finalize projections.state.p.result sub.state.p.result vars)

9660− ?~ finalized $(ds t.ds)

9661− =? artifacts ?=(^ u.finalized)

9662− [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]

9663− =? checked |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) (~(put by checked) name.d d)

9664− $(ds t.ds, env [[name.d [typ vars]] env], checked checked)

9711+ (add-supported-defs-core ds all-defs checked heads env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts ~)

96659712::

9713+

96669714+$ iresolved [env=ienv grouped=(list term) artifacts=(list iwidth-definition)]

96679715+$ iadj (map term (list term))

96689716+$ ivisited (map term ?)

@@ -9776,6 +9824,46 @@

97769824++ resolve-groups

97779825 |= [ds=(list def) molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile)]

97789826 ^- iresolved

9827+ (resolve-groups-core ds molds globals externals surs mark-externals marks jimports reserved-molds at prelude ~)

9828+::

9829+

9830+++ add-supported-defs-core

9831+ |= [ds=(list def) all-defs=(list def) checked=(map term def) heads=(unit igate-prelude-evidence) env=ienv molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile) artifacts=(list iwidth-definition) index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])]

9832+ ^- [env=ienv artifacts=(list iwidth-definition)]

9833+ ?~ ds [env artifacts]

9834+ =/ d=def i.ds

9835+ ?: ?=(%mold -.d) $(ds t.ds)

9836+ ?. (unique-value-name name.d globals) $(ds t.ds)

9837+ ?^ (ienv-lookup name.d env) $(ds t.ds)

9838+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))

9839+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~]

9840+ =. grec-index.initial index

9841+ =. gate-defs.initial checked

9842+ =. head-evidence.initial heads

9843+ =. initial (reserve-def-caps val.d initial)

9844+ =/ result=iresult (infer-fragment val.d env initial)

9845+ =? result ?=(%| -.result) (infer-recursive-gate d env initial)

9846+ ?: ?=(%| -.result) $(ds t.ds)

9847+ =. state.p.result (promote-restricted-numbers state.p.result env)

9848+ =. state.p.result (default-hole-numbers holes.state.p.result holes.initial state.p.result env !(itype-has-gate (itype-normalize typ.p.result sub.state.p.result)))

9849+ ?^ (unresolved-hole holes.state.p.result holes.initial state.p.result) $(ds t.ds)

9850+ ?: (constrained-capitals caps.state.p.result sub.state.p.result) $(ds t.ds)

9851+ =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))

9852+ ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) $(ds t.ds)

9853+ ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) $(ds t.ds)

9854+ =/ vars=(list @ud) (unique-type-vars (itype-vars typ))

9855+ ?: (gth (lent vars) 26) $(ds t.ds)

9856+ =/ finalized=(unit (list iwprojection))

9857+ (width-finalize projections.state.p.result sub.state.p.result vars)

9858+ ?~ finalized $(ds t.ds)

9859+ =? artifacts ?=(^ u.finalized)

9860+ [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]

9861+ =? checked |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) (~(put by checked) name.d d)

9862+ $(ds t.ds, env [[name.d [typ vars]] env], checked checked)

9863+::

9864+++ resolve-groups-core

9865+ |= [ds=(list def) molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile) index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])]

9866+ ^- iresolved

97799867 =/ env=ienv ~

97809868 =/ grouped=(list term) ~

97819869 =/ artifacts=(list iwidth-definition) ~

@@ -9787,8 +9875,9 @@

97879875 =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)

97889876 |-

97899877 =/ next=[env=ienv artifacts=(list iwidth-definition)]

9790− (add-supported-defs ds ds (direct-checked-gates ds env) heads env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts)

9791− =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~]

9878+ (add-supported-defs-core ds ds (direct-checked-gates ds env) heads env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts index)

9879+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~]

9880+ =. grec-index.initial index

97929881 =/ out=iresolved (add-groups ds components graph env.next grouped artifacts.next initial)

97939882 ?: =(env env.out) out

97949883 $(env env.out, grouped grouped.out, artifacts artifacts.out)

@@ -10588,6 +10677,9 @@

1058810677 |= [typ=itype name=term vars=(list @ud)]

1058910678 ^- itype

1059010679 ?: ?=(%jrec -.typ) typ(label `name)

10680+ ?: ?=(%grec -.typ)

10681+ ?. (identity-union-parameters vars args.typ) typ(label ~)

10682+ typ(label `name)

1059110683 ?. ?=(%union -.typ) typ

1059210684 ?. (identity-union-parameters vars args.typ)

1059310685 ?~ origin.typ typ

@@ -10661,7 +10753,7 @@

1066110753 =/ source-unit=(unit ischeme)

1066210754 ?~ unit-decl ~

1066310755 =/ unit-molds=imolds ~[[%unit u.unit-decl]]

10664− =/ unit-state=istate [0 ~ ~ ~ unit-molds ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ | /lib/jibb/prelude/jibb ~[%unit] ~ ~ 256 ~ ~ ~]

10756+ =/ unit-state=istate [0 ~ ~ ~ unit-molds ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ | /lib/jibb/prelude/jibb ~[%unit] ~ ~ 256 ~ ~ ~ ~]

1066510757 =/ unit-types=imold-types (partial-prelude-molds unit-molds unit-state)

1066610758 =/ unit-iface=ifile [~ unit-types /lib/jibb/prelude/jibb ~ ~ ~ ~ ~]

1066710759 =/ found=(unit ischeme) (find-jibb-mold %unit unit-iface)

@@ -10676,7 +10768,7 @@

1067610768 =/ js=ijimports ~[[face.i.imports.mod primitive]]

1067710769 =/ reserved=(list term) ~[face.i.imports.mod]

1067810770 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))

10679− =/ state=istate [0 ~ ~ ~ molds globals ~ ~ ~ ~ js reserved ~ ~ ~ | at top ~ ~ 256 ~ ~ ~]

10771+ =/ state=istate [0 ~ ~ ~ molds globals ~ ~ ~ ~ js reserved ~ ~ ~ | at top ~ ~ 256 ~ ~ ~ ~]

1068010772 =/ mts=(each imold-types @t) (module-mold-types molds state)

1068110773 =/ usable=(unit imold-types)

1068210774 ?: ?=(%& -.mts) `p.mts

@@ -10732,7 +10824,7 @@

1073210824 =? env-molds declared

1073310825 (skim molds |=(m=[name=term body=shape] !=(%list name.m)))

1073410826 =/ reserved=(list term) ?:(declared ~[%list] ~)

10735− =/ state=istate [0 ~ ~ ~ env-molds globals ~ ~ ~ ~ u.private reserved ~ ~ ~ | at names ~ ~ 256 ~ ~ ~]

10827+ =/ state=istate [0 ~ ~ ~ env-molds globals ~ ~ ~ ~ u.private reserved ~ ~ ~ | at names ~ ~ 256 ~ ~ ~ ~]

1073610828 :: Other prelude molds may use list only after its source has passed

1073710829 :: the standard-list check. The raw declaration remains removed.

1073810830 =/ declared-list=(unit shape) (find-simple-mold %list molds)

@@ -11261,7 +11353,7 @@

1126111353 =/ surs=(list term) (collect-sur-imports imports.mod)

1126211354 =/ reserved=(list term) (weld molds.prep (turn resolved.p.deps |=(j=[face=term interface=ifile] face.j)))

1126311355 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))

11264− =/ state=istate [0 ~ ~ ~ molds globals externals surs marks declared resolved.p.deps reserved ~ ~ ~ | file top prelude ~ 256 ~ ~ ~]

11356+ =/ state=istate [0 ~ ~ ~ molds globals externals surs marks declared resolved.p.deps reserved ~ ~ ~ | file top prelude ~ 256 ~ ~ ~ ~]

1126511357 =/ mts=(each imold-types @t) (module-mold-types molds state)

1126611358 ?: ?=(%| -.mts) [%| p.mts]

1126711359 =/ resolution=iresolved (resolve-groups ordinary molds globals externals surs marks declared resolved.p.deps reserved file prelude)

@@ -11295,7 +11387,7 @@

1129511387 =/ surs=(list term) (collect-sur-imports imports.mod)

1129611388 =/ reserved=(list term) (weld molds.prep (turn resolved.p.deps |=(j=[face=term interface=ifile] face.j)))

1129711389 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))

11298− =/ state=istate [0 ~ ~ ~ molds globals externals surs marks declared resolved.p.deps reserved ~ ~ ~ | file top prelude ~ 256 ~ ~ ~]

11390+ =/ state=istate [0 ~ ~ ~ molds globals externals surs marks declared resolved.p.deps reserved ~ ~ ~ | file top prelude ~ 256 ~ ~ ~ ~]

1129911391 =/ mts=(each imold-types @t) (module-mold-types molds state)

1130011392 ?: ?=(%| -.mts) [%| p.mts]

1130111393 =/ resolution=iresolved (resolve-groups ordinary molds globals externals surs marks declared resolved.p.deps reserved file prelude)

@@ -11671,16 +11763,35 @@

1167111763 [%| (crip "module kind needs unsupported inference: {(spud at)}")]

1167211764 =/ js=jimports-result (resolve-jibb-imports imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)

1167311765 ?: ?=(%| -.js) [%| p.js]

11674− =/ molds=imolds (collect-simple-molds defs.mod)

11766+ =/ collected=grec-collected

11767+ ?^ imports.mod [(collect-simple-molds defs.mod) *(map term shape)]

11768+ (grec-collect-molds defs.mod)

11769+ =/ molds=imolds molds.collected

1167511770 =/ globals=(list term) (weld prelude-values (weld (import-binding-names imports.mod) vals))

1167611771 =/ surs=(list term) (collect-sur-imports imports.mod)

1167711772 =/ marks=(list term) (collect-mark-imports imports.mod)

1167811773 =/ reserved=(list term) (weld prelude-molds (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))

1167911774 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))

11680− =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks resolved.p.js reserved ~ ~ ~ | at top prelude ~ 256 ~ ~ ~]

11775+ =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks resolved.p.js reserved ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~]

11776+ :: Source and scope were checked above; preserve that exact root and prelude.

11777+ :: This first integration only indexes import-free library sources.

11778+ =/ index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])

11779+ ?^ imports.mod ~

11780+ ?~ prelude ~

11781+ =/ standard=(unit ischeme) (find-jibb-mold %list u.prelude)

11782+ ?~ standard ~

11783+ ?. =(u.standard [[%collection %list ~[[%var 0]]] ~[0]]) ~

11784+ =/ index=(map term shape) proofs.collected

11785+ ?. !=(index *(map term shape)) ~

11786+ ?: (lien molds |=(m=[name=term body=shape] =(%list name.m))) ~

11787+ `[at src u.prelude index]

11788+ =. grec-index.state index

1168111789 =/ mts=(each imold-types @t) (module-mold-types molds state)

1168211790 ?: ?=(%| -.mts) [%| (crip "{(trip p.mts)}: {(spud at)}")]

11683− =/ resolution=iresolved (resolve-groups defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)

11791+ =/ resolution=iresolved

11792+ ?~ index

11793+ (resolve-groups defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)

11794+ (resolve-groups-core defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude index)

1168411795 =/ env=ienv env.resolution

1168511796 ?. (module-values-complete defs.mod env)

1168611797 [%| (crip "module definitions need unsupported inference: {(spud at)}")]

@@ -11733,7 +11844,7 @@

1173311844 =/ declared=(list term) (collect-mark-imports imports.mod)

1173411845 =/ reserved=(list term) (weld molds.u.prepared (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))

1173511846 =/ top=(list term) (turn ms |=(m=[name=term body=shape] name.m))

11736− =/ state=istate [0 ~ ~ ~ ms globals externals surs marks declared resolved.p.js reserved ~ ~ ~ | file top `public ~ 256 ~ ~ ~]

11847+ =/ state=istate [0 ~ ~ ~ ms globals externals surs marks declared resolved.p.js reserved ~ ~ ~ | file top `public ~ 256 ~ ~ ~ ~]

1173711848 =/ inferred=(unit [template=ischeme state=istate])

1173811849 (infer-mold-template shape.i.selected state(active ~[name], in-mold &))

1173911850 ?~ inferred [%| 'selected mold needs unsupported inference']

@@ -11871,7 +11982,7 @@

1187111982 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype typ ~)}{(show-atom-constraint typ)}")

1187211983 $(ds t.ds, lines [line lines])

1187311984 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))

11874− =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | file top prelude ~ 256 ~ ~ ~]

11985+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | file top prelude ~ 256 ~ ~ ~ ~]

1187511986 =. gate-defs.initial source-defs

1187611987 =. head-evidence.initial heads

1187711988 =. initial (reserve-def-caps val.d initial)

@@ -11913,4 +12024,79 @@

1191312024 =/ printable=itype (canonical-itype typ vars)

1191412025 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")

1191512026 $(ds t.ds, lines [line lines])

12027+:: Experimental per-module, source-derived recursive tree index.

12028+:: The two tags and the exact children/list/self layout are fixed-shape

12029+:: checks, so ordinary definitions incur no type-tree or source scans.

12030+++ grec-tagged-fields

12031+ |= sh=shape

12032+ ^- (unit [tag=@ fields=(list field)])

12033+ ?. ?=(%cell -.sh) ~

12034+ ?~ fields.sh ~

12035+ =/ head=field i.fields.sh

12036+ ?. ?=(%bare -.head) ~

12037+ ?. ?=(%const -.shape.head) ~

12038+ ?. &(?=(%term form.lit.shape.head) =(%tas aura.lit.shape.head)) ~

12039+ `[val.lit.shape.head t.fields.sh]

12040+++ grec-tree-children

12041+ |= [fs=(list field) param=@t]

12042+ ^- (unit field)

12043+ ?~ fs ~

12044+ ?~ t.fs `i.fs

12045+ ?^ t.t.fs ~

12046+ =/ event=field i.fs

12047+ =/ kids=field i.t.fs

12048+ ?. &(?=(%face -.event) ?=(%face -.kids)) ~

12049+ ?. !=(name.event name.kids) ~

12050+ ?. ?=(%fn -.shape.event) ~

12051+ ?. ?=(%aura -.sample.shape.event) ~

12052+ ?. =(%t aura.sample.shape.event) ~

12053+ ?. ?=(%tvar -.product.shape.event) ~

12054+ ?. =(param name.product.shape.event) ~

12055+ `kids

12056+::

12057+++ grec-tree-proof

12058+ |= [name=term sh=shape]

12059+ ^- ?

12060+ ?. ?=(%generic -.sh) |

12061+ ?. ?=([@ ~] vars.sh) |

12062+ =/ param=@t i.vars.sh

12063+ ?. ?=(%union -.body.sh) |

12064+ ?. ?=([* [* ~]] cases.body.sh) |

12065+ =/ a=(unit [tag=@ fields=(list field)]) (grec-tagged-fields i.cases.body.sh)

12066+ =/ b=(unit [tag=@ fields=(list field)]) (grec-tagged-fields i.t.cases.body.sh)

12067+ ?~ a |

12068+ ?~ b |

12069+ ?. !=(tag.u.a tag.u.b) |

12070+ ?. ?=([* ~] fields.u.a) |

12071+ =/ value=field i.fields.u.a

12072+ ?. ?=(%face -.value) |

12073+ ?. ?=(%aura -.shape.value) |

12074+ ?. =(%t aura.shape.value) |

12075+ =/ selected=(unit field) (grec-tree-children fields.u.b param)

12076+ ?~ selected |

12077+ =/ kids=field u.selected

12078+ ?. ?=(%face -.kids) |

12079+ ?. ?=(%apply -.shape.kids) |

12080+ ?. =(ref.shape.kids ~[%list]) |

12081+ ?. ?=([* ~] args.shape.kids) |

12082+ =/ self=shape i.args.shape.kids

12083+ ?. ?=(%apply -.self) |

12084+ ?. =(ref.self ~[name]) |

12085+ ?. ?=([* ~] args.self) |

12086+ ?. ?=(%tvar -.i.args.self) |

12087+ =(name.i.args.self param)

12088++$ grec-collected [molds=imolds proofs=(map term shape)]

12089+++ grec-collect-molds

12090+ |= ds=(list def)

12091+ ^- grec-collected

12092+ ?~ ds [~ *(map term shape)]

12093+ =/ rest=grec-collected $(ds t.ds)

12094+ ?. ?=(%mold -.i.ds) rest

12095+ =/ name=term name.i.ds

12096+ =/ body=shape shape.i.ds

12097+ =/ proofs=(map term shape) proofs.rest

12098+ =? proofs (grec-tree-proof name body) (~(put by proofs) name body)

12099+ [[[name body] molds.rest] proofs]

12100+::

12101+

1191612102--

tests/lib/jibb-generic-recursion.hoonnew file+170

@@ -0,0 +1,170 @@

1+:: Source-backed recursive identities; this is not a runtime element model.

2+/+ jibb

3+/* real-prelude %jibb /lib/jibb/prelude/jibb

4+/* real-internal %jibb /lib/jibb/internal/jibb

5+/* tree %txt /tests/type-generic-recursion/tree/txt

6+/* changed %txt /tests/type-generic-recursion/tree-changed/txt

7+/* alias %txt /tests/type-generic-recursion/alias/txt

8+/* client %txt /tests/type-generic-recursion/client/txt

9+/* bad-mold %txt /tests/type-generic-recursion/bad-mold/txt

10+/* bad-constructor %txt /tests/type-generic-recursion/bad-constructor/txt

11+/* bad-parameter %txt /tests/type-generic-recursion/bad-parameter/txt

12+/* local-shadow %txt /tests/type-generic-recursion/local-shadow/txt

13+/* local-distinct %txt /tests/type-generic-recursion/local-distinct/txt

14+/* local-only %txt /tests/type-generic-recursion/local-only/txt

15+/* list-shadow %txt /tests/type-generic-recursion/list-shadow/txt

16+/* chain %txt /tests/type-generic-recursion/chain/txt

17+/* bad-match %txt /tests/type-generic-recursion/bad-match/txt

18+/* expected %txt /tests/type-generic-recursion/expected/txt

19+|%

20+++ text

21+ |= lines=wain

22+ ^- @t

23+ (rap 3 (turn lines |=(line=@t (cat 3 line '\0a'))))

24+++ altered-list-source

25+ |= pre=@t

26+ ^- (unit @t)

27+ =/ lines=wain (to-wain:format pre)

28+ =/ old=@t ' [i=A t=(list A)]'

29+ =/ matches=(list @t) (skim lines |=(line=@t =(line old)))

30+ ?. =(1 (lent matches)) ~

31+ =/ changed=wain (turn lines |=(line=@t ?:(=(line old) ' [i=@t t=(list A)]' line)))

32+ `(text changed)

33+++ result-line

34+ |= [label=@t ok=?]

35+ ^- @t

36+ (crip "{(trip label)}: {?:(ok "ok" "BAD")}")

37+++ generic-output

38+ |= [pre=@t internal=@t tree=@t changed=@t alias=@t client=@t invalid=(list [label=@t src=@t]) shadow=@t chain=@t]

39+ ^- @t

40+ =/ prep=(unit iprelude:jibb) (prepare-prelude-with-internal:jibb pre internal)

41+ ?~ prep 'BAD prelude preparation'

42+ =/ module=jfile-result:jibb

43+ (infer-jibb-file:jibb /ui/tree/jibb tree ~ ~ ~ ~[/ui/tree/jibb] values.u.prep molds.u.prep ~ `iface.u.prep)

44+ ?: ?=(%| -.module) (cat 3 'BAD recursive module: ' p.module)

45+ =/ scheme=(unit ischeme:jibb) (find-jibb-mold:jibb %element iface.p.module)

46+ ?~ scheme 'BAD missing recursive mold'

47+ ?. ?=(%grec -.typ.u.scheme) 'BAD missing recursive identity'

48+ =/ typ=itype:jibb typ.u.scheme

49+ ?> ?=(%grec -.typ)

50+ =/ t=itype:jibb typ(args ~[[%atom %t]])

51+ ?> ?=(%grec -.t)

52+ =/ p=itype:jibb typ(args ~[[%atom %p]])

53+ =/ variable=itype:jibb typ(args ~[[%var 91]])

54+ =/ other=itype:jibb t(at /ui/other/jibb)

55+ =/ numeric=itype:jibb [%cell t [%nvar 99]]

56+ =/ chain-parsed=(each module:jibb error:jibb) (parse:jibb /ui/tree/jibb chain)

57+ ?: ?=(%| -.chain-parsed) 'BAD chain source parse'

58+ =/ chain-molds=imolds:jibb (collect-simple-molds:jibb defs.p.chain-parsed)

59+ =/ chain-shape=(unit shape:jibb) (find-simple-mold:jibb %chain chain-molds)

60+ ?~ chain-shape 'BAD chain source mold'

61+ =/ no-index=istate:jibb *istate:jibb

62+ =. no-index no-index(at /ui/tree/jibb, molds chain-molds, top-molds ~[%chain], prelude `iface.u.prep)

63+ =/ checks=(list [label=@t ok=?])

64+ :~ ['source module complete' ?=([%& *] module)]

65+ ['generic mold quantified' =(1 (lent vars.u.scheme))]

66+ ['distinct arguments decline' ?=(~ (itype-unify:jibb t p ~))]

67+ ['distinct origins decline' ?=(~ (itype-unify:jibb t other ~))]

68+ ['occurs check' ?=(~ (itype-unify:jibb [%var 91] variable ~))]

69+ ['cell construction stays opaque' =(%unknown -:(itype-fit:jibb [%cell [%atom %tas] [%atom %t]] t ~ 0))]

70+ ['noun construction stays opaque' =(%unknown -:(itype-fit:jibb [%noun ~] t ~ 0))]

71+ ['unindexed recursion declined' ?=(~ (simple-source-generic-recursive:jibb %chain u.chain-shape ~[[%atom %t]] no-index))]

72+ ['alteration rejects missing line' ?=(~ (altered-list-source 'absent'))]

73+ ['alteration rejects repeated line' ?=(~ (altered-list-source (text ~[' [i=A t=(list A)]' ' [i=A t=(list A)]'])))]

74+ ['gate freedom unknown' =(%unknown verdict:(gate-free-type:jibb t 64 ~))]

75+ ['gate defaulting conservative' &((itype-has-gate:jibb t) =(numeric (default-decimals:jibb numeric)))]

76+ ==

77+ =/ invalid-lines=(list @t)

78+ %+ turn invalid

79+ |= c=[label=@t src=@t]

80+ =/ parsed=(each module:jibb error:jibb) (parse:jibb /ui/tree/jibb src.c)

81+ =/ r=jfile-result:jibb

82+ (infer-jibb-file:jibb /ui/tree/jibb src.c ~ ~ ~ ~[/ui/tree/jibb] values.u.prep molds.u.prep ~ `iface.u.prep)

83+ (result-line label.c &(?=(%& -.parsed) ?=(%| -.r)))

84+ =/ shadow-result=jfile-result:jibb

85+ (infer-jibb-file:jibb /ui/tree/jibb shadow ~ ~ ~ ~[/ui/tree/jibb] values.u.prep ~ ~ `iface.u.prep)

86+ =/ altered-source=(unit @t) (altered-list-source pre)

87+ ?~ altered-source 'BAD canonical list source was missing or repeated'

88+ =/ altered=@t u.altered-source

89+ =/ altered-prep=(unit iprelude:jibb) (prepare-prelude-with-internal:jibb altered internal)

90+ =/ altered-result=jfile-result:jibb

91+ ?~ altered-prep [%| 'altered prelude unavailable']

92+ (infer-jibb-file:jibb /ui/tree/jibb tree ~ ~ ~ ~[/ui/tree/jibb] values.u.altered-prep molds.u.altered-prep ~ `iface.u.altered-prep)

93+ =/ parsed=(each module:jibb error:jibb) (parse:jibb /tests/tree/client/jibb client)

94+ ?: ?=(%| -.parsed) 'BAD client parse'

95+ =/ modules=jbundle:jibb ~[[/ui/tree/jibb tree] [/ui/tree-two/jibb tree] [/ui/tree-alias/jibb alias]]

96+ =/ first=jimports-result:jibb

97+ (resolve-jibb-imports:jibb imports.p.parsed ~ ~ modules ~[/tests/tree/client/jibb] values.u.prep molds.u.prep ~ `iface.u.prep)

98+ ?: ?=(%| -.first) 'BAD import resolution'

99+ =/ reuse=jimports-result:jibb

100+ (resolve-jibb-imports:jibb imports.p.parsed ~ ~ modules ~[/tests/tree/client/jibb] values.u.prep molds.u.prep cache.p.first `iface.u.prep)

101+ =/ changed-modules=jbundle:jibb ~[[/ui/tree/jibb changed] [/ui/tree-two/jibb tree] [/ui/tree-alias/jibb alias]]

102+ =/ stale=jimports-result:jibb

103+ (resolve-jibb-imports:jibb imports.p.parsed ~ ~ changed-modules ~[/tests/tree/client/jibb] values.u.prep molds.u.prep cache.p.first `iface.u.prep)

104+ =/ fresh=jimports-result:jibb

105+ (resolve-jibb-imports:jibb imports.p.parsed ~ ~ changed-modules ~[/tests/tree/client/jibb] values.u.prep molds.u.prep ~ `iface.u.prep)

106+ =/ duplicate-modules=jbundle:jibb [[/ui/tree/jibb tree] modules]

107+ =/ duplicate=jimports-result:jibb

108+ (resolve-jibb-imports:jibb imports.p.parsed ~ ~ duplicate-modules ~[/tests/tree/client/jibb] values.u.prep molds.u.prep cache.p.first `iface.u.prep)

109+ =/ cycle=jimports-result:jibb

110+ (resolve-jibb-imports:jibb imports.p.parsed ~ ~ modules ~[/ui/tree/jibb] values.u.prep molds.u.prep cache.p.first `iface.u.prep)

111+ =/ prelude-other=ifile:jibb iface.u.prep(source ~)

112+ =/ mismatch=jimports-result:jibb

113+ (resolve-jibb-imports:jibb imports.p.parsed ~ ~ modules ~[/tests/tree/client/jibb] values.u.prep molds.u.prep cache.p.first `prelude-other)

114+ =/ old=(unit ifile:jibb) (find-jibb-interface:jibb %first resolved.p.first)

115+ =/ new=(unit ifile:jibb) ?:(?=(%& -.fresh) (find-jibb-interface:jibb %first resolved.p.fresh) ~)

116+ =/ shape-changed=?

117+ ?~ old |

118+ ?~ new |

119+ =/ a=(unit ischeme:jibb) (find-jibb-mold:jibb %element u.old)

120+ =/ b=(unit ischeme:jibb) (find-jibb-mold:jibb %element u.new)

121+ ?~ a |

122+ ?~ b |

123+ ?. &(?=(%grec -.typ.u.a) ?=(%grec -.typ.u.b)) |

124+ !=(proof.typ.u.a proof.typ.u.b)

125+ =/ reuse-ok=? ?:(?=(%| -.reuse) | =(resolved.p.first resolved.p.reuse))

126+ =/ shadow-parsed=(each module:jibb error:jibb) (parse:jibb /ui/tree/jibb shadow)

127+ =/ altered-parsed=(each module:jibb error:jibb) (parse:jibb /lib/jibb/prelude/jibb altered)

128+ =/ more=(list [label=@t ok=?])

129+ :~ ['unreserved local list shadow declined' &(?=(%& -.shadow-parsed) ?=(%| -.shadow-result))]

130+ ['altered prelude list declined' &(?=(%& -.altered-parsed) ?=(%| -.altered-result))]

131+ ['cached source reuse' reuse-ok]

132+ ['changed source invalidates cache' ?=(%| -.stale)]

133+ ['changed source fresh proof' &(?=(%& -.fresh) shape-changed)]

134+ ['duplicate source declined' ?=(%| -.duplicate)]

135+ ['active import cycle declined' ?=(%| -.cycle)]

136+ ['changed prelude invalidates cache' ?=(%| -.mismatch)]

137+ ==

138+ =/ lines=(list @t) (weld (turn checks result-line) (weld invalid-lines (turn more result-line)))

139+ =/ report=@t (golden-types-with-prepared-prelude:jibb /tests/tree/client/jibb client ~ ~ modules prep)

140+ (cat 3 (of-wain:format lines) (cat 3 '\0a' report))

141+++ test-generic-recursion

142+ ^- tang

143+ ?~ tree ~[leaf+"recursive source is missing"]

144+ ?~ changed ~[leaf+"changed recursive source is missing"]

145+ ?~ alias ~[leaf+"recursive alias is missing"]

146+ ?~ client ~[leaf+"recursive client is missing"]

147+ ?~ bad-mold ~[leaf+"invalid mold fixture is missing"]

148+ ?~ bad-constructor ~[leaf+"constructor fixture is missing"]

149+ ?~ bad-match ~[leaf+"match fixture is missing"]

150+ ?~ bad-parameter ~[leaf+"parameter fixture is missing"]

151+ ?~ local-shadow ~[leaf+"local shadow fixture is missing"]

152+ ?~ local-distinct ~[leaf+"distinct local shadow fixture is missing"]

153+ ?~ local-only ~[leaf+"local recursion fixture is missing"]

154+ ?~ list-shadow ~[leaf+"list shadow fixture is missing"]

155+ ?~ chain ~[leaf+"unindexed chain fixture is missing"]

156+ ?~ expected ~[leaf+"recursive expected output is missing"]

157+ =/ invalid=(list [label=@t src=@t])

158+ :~ ['unused mold hole declined' (text bad-mold)]

159+ ['constructor declined' (text bad-constructor)]

160+ ['matching declined' (text bad-match)]

161+ ['nonuniform recursion declined' (text bad-parameter)]

162+ ['identical local shadow declined' (text local-shadow)]

163+ ['different local shadow declined' (text local-distinct)]

164+ ['local recursion declined' (text local-only)]

165+ ==

166+ =/ actual=@t (generic-output real-prelude real-internal (text tree) (text changed) (text alias) (text client) invalid (text list-shadow) (text chain))

167+ ?. =((to-wain:format (cat 3 actual '\0a')) expected)

168+ ~[leaf+"generic recursion output differs from expected"]

169+ ~

170+--

tests/type-generic-recursion/about.txtnew file+14

@@ -0,0 +1,14 @@

1+source: docs/spec/grammar.md:57,135,162 — “Molds may be recursive”; “recursive molds go by name and module”; a number defaults when its `++` is checked.

3+This shared eval and ship fixture checks a deliberately narrow source-backed

4+recursive identity: two distinct tagged cases, a text leaf and a node with a

5+message-producing gate and a list of recursive children. The test-only tree is

6+not a chosen element representation. A complete import-free owner module must

7+check before its interface is published. Same-origin aliases retain identity,

8+while different origins and unproved casts, construction and matching remain

9+unsupported. An opaque recursive type prevents premature numeric defaulting;

10+its gate-freedom remains unknown. Source/cache/prelude changes, cycles,

11+nonuniform recursion, invalid unused molds and local shadows fail closed.

12+

13+The client report explicitly remains partial. No runtime layout, program kind,

14+watchability or backend behavior is claimed.

tests/type-generic-recursion/alias.txtnew file+3

@@ -0,0 +1,3 @@

1+/= source /ui/tree

2++$ alias |$ [A] (element.source A)

3+++ identity |= x=(alias A) x

tests/type-generic-recursion/bad-constructor.txtnew file+8

@@ -0,0 +1,8 @@

1++$ element |$ [M]

2+ [%text value=@t]

3+ [%node event=$-(@t M) children=(list (element M))]

4+++ text-id |= x=(element @t) x

5+++ ship-id |= x=(element @p) x

6+++ generic-id |= x=(element A) x

8+++ construct ^- (element @t) [%text value="hi"]

tests/type-generic-recursion/bad-match.txtnew file+10

@@ -0,0 +1,10 @@

1++$ element |$ [M]

2+ [%text value=@t]

3+ [%node event=$-(@t M) children=(list (element M))]

4+++ text-id |= x=(element @t) x

5+++ ship-id |= x=(element @p) x

6+++ generic-id |= x=(element A) x

7+++ match |= x=(element @t)

8+ ?- x

9+ [%text value] value

10+ [%node event children] "node"

tests/type-generic-recursion/bad-mold.txtnew file+8

@@ -0,0 +1,8 @@

1++$ element |$ [M]

2+ [%text value=@t]

3+ [%node event=$-(@t M) children=(list (element M))]

4+++ text-id |= x=(element @t) x

5+++ ship-id |= x=(element @p) x

6+++ generic-id |= x=(element A) x

8++$ unused _

tests/type-generic-recursion/bad-parameter.txtnew file+6

@@ -0,0 +1,6 @@

1++$ element |$ [M]

2+ [%text value=@t]

3+ [%node event=$-(@t M) children=(list (element @t))]

4+++ text-id |= x=(element @t) x

5+++ ship-id |= x=(element @p) x

6+++ generic-id |= x=(element A) x

tests/type-generic-recursion/chain.txtnew file+3

@@ -0,0 +1,3 @@

1++$ chain |$ [A]

2+ ~

3+ [i=A t=(chain A)]

tests/type-generic-recursion/client.txtnew file+11

@@ -0,0 +1,11 @@

1+/= first /ui/tree

2+/= again /ui/tree

3+/= second /ui/tree-two

4+/= via /ui/tree-alias

5+++ from-first |= x=(element.first @t) x

6+++ from-again |= x=(element.again @p) x

7+++ same-origin |= x=(element.first @t) ^- (element.again @t) x

8+++ from-alias |= x=(alias.via @t) x

9+++ through-alias |= x=(element.first @t) ^- (alias.via @t) x

10+++ different-origin |= x=(element.first @t) ^- (element.second @t) x

11+++ independent |= [a=(element.first @t) b=(element.first @p)] [(generic-id.first a) (generic-id.first b)]

tests/type-generic-recursion/expected.txtnew file+35

@@ -0,0 +1,35 @@

1+source module complete: ok

2+generic mold quantified: ok

3+distinct arguments decline: ok

4+distinct origins decline: ok

5+occurs check: ok

6+cell construction stays opaque: ok

7+noun construction stays opaque: ok

8+unindexed recursion declined: ok

9+alteration rejects missing line: ok

10+alteration rejects repeated line: ok

11+gate freedom unknown: ok

12+gate defaulting conservative: ok

13+unused mold hole declined: ok

14+constructor declined: ok

15+matching declined: ok

16+nonuniform recursion declined: ok

17+identical local shadow declined: ok

18+different local shadow declined: ok

19+local recursion declined: ok

20+unreserved local list shadow declined: ok

21+altered prelude list declined: ok

22+cached source reuse: ok

23+changed source invalidates cache: ok

24+changed source fresh proof: ok

25+duplicate source declined: ok

26+active import cycle declined: ok

27+changed prelude invalidates cache: ok

28+partial inference; module not checked

29+++ from-first: $-((element.first @t) (element.first @t))

30+++ from-again: $-((element.again @p) (element.again @p))

31+++ same-origin: $-((element.first @t) (element.again @t))

32+++ from-alias: $-((alias.via @t) (alias.via @t))

33+++ through-alias: $-((element.first @t) (alias.via @t))

34+++ different-origin: cast constraint is not supported by partial inference

35+++ independent: $-([a=(element.first @t) b=(element.first @p)] [(element.first @t) (element.first @p)])

tests/type-generic-recursion/list-shadow.txtnew file+4

@@ -0,0 +1,4 @@

1++$ list |$ [M] [%fake value=M]

2++$ element |$ [M]

3+ [%text value=@t]

4+ [%node children=(list (element M))]

tests/type-generic-recursion/local-distinct.txtnew file+11

@@ -0,0 +1,11 @@

1++$ element |$ [M]

2+ [%text value=@t]

3+ [%node event=$-(@t M) children=(list (element M))]

4+++ text-id |= x=(element @t) x

5+++ ship-id |= x=(element @p) x

6+++ generic-id |= x=(element A) x

7+++ shadow |= x=@t

8+ +$ element |$ [M]

9+ [%different value=@t]

10+ [%node event=$-(@t M) children=(list (element M))]

11+ x

tests/type-generic-recursion/local-only.txtnew file+11

@@ -0,0 +1,11 @@

1++$ element |$ [M]

2+ [%text value=@t]

3+ [%node event=$-(@t M) children=(list (element M))]

4+++ text-id |= x=(element @t) x

5+++ ship-id |= x=(element @p) x

6+++ generic-id |= x=(element A) x

7+++ local-only |= x=@t

8+ +$ local-tree |$ [M]

9+ [%text value=@t]

10+ [%node event=$-(@t M) children=(list (local-tree M))]

11+ x

tests/type-generic-recursion/local-shadow.txtnew file+11

@@ -0,0 +1,11 @@

1++$ element |$ [M]

2+ [%text value=@t]

3+ [%node event=$-(@t M) children=(list (element M))]

4+++ text-id |= x=(element @t) x

5+++ ship-id |= x=(element @p) x

6+++ generic-id |= x=(element A) x

7+++ shadow |= x=@t

8+ +$ element |$ [M]

9+ [%text value=@t]

10+ [%node event=$-(@t M) children=(list (element M))]

11+ x

tests/type-generic-recursion/tree-changed.txtnew file+6

@@ -0,0 +1,6 @@

1++$ element |$ [M]

2+ [%text value=@t]

3+ [%branch event=$-(@t M) children=(list (element M))]

4+++ text-id |= x=(element @t) x

5+++ ship-id |= x=(element @p) x

6+++ generic-id |= x=(element A) x

tests/type-generic-recursion/tree.txtnew file+6

@@ -0,0 +1,6 @@

1++$ element |$ [M]

2+ [%text value=@t]

3+ [%node event=$-(@t M) children=(list (element M))]

4+++ text-id |= x=(element @t) x

5+++ ship-id |= x=(element @p) x

6+++ generic-id |= x=(element A) x

tools/testdata/ship-selftest+6

@@ -310,6 +310,7 @@ def generator_checks(tmp):

310310 'tests/lib/jibb-arithmetic-guards.hoon',

311311 'tests/lib/jibb-positional-face-guards.hoon',

312312 'tests/lib/jibb-generic-alias.hoon',

313+ 'tests/lib/jibb-generic-recursion.hoon',

313314 'tests/lib/jibb-api-evidence.hoon',

314315 'tests/lib/jibb-ask-guards.hoon',

315316 'tests/lib/jibb-request-guards.hoon',

@@ -324,6 +325,11 @@ def generator_checks(tmp):

324325 'tests/lib/jibb-gate-free-guards.hoon',

325326 'tests/lib/jibb-gate-free-source.hoon'}

326327 <= normal_tests, sorted(normal_tests))

328+ check('generic recursion source and golden are assembled',

329+ {f'tests/type-generic-recursion/{name}.txt' for name in (

330+ 'tree', 'tree-changed', 'alias', 'client', 'bad-mold',

331+ 'bad-constructor', 'bad-match', 'bad-parameter', 'local-shadow',

332+ 'local-distinct', 'local-only', 'list-shadow', 'chain', 'expected')} <= set(normal.files))

327333 check('direct gate source and golden are assembled',

328334 {'tests/type-direct-gate/source.txt', 'tests/type-direct-gate/expected.txt'}

329335 <= set(normal.files))

tools/type-generic-recursion-testnew file+61

@@ -0,0 +1,61 @@

1+#!/usr/bin/env python3

2+"""Check indexed recursive source identity, aliases and cache under eval."""

3+from pathlib import Path

4+import argparse

5+import difflib

6+import subprocess

7+import sys

8+import tempfile

10+root = Path(__file__).resolve().parent.parent

11+parser = argparse.ArgumentParser(description=__doc__)

12+parser.add_argument('--lib', default=str(root / 'jibb-dev/lib/jibb.hoon'))

13+parser.add_argument('--update', action='store_true')

14+args = parser.parse_args()

15+fixture = root / 'tests/type-generic-recursion'

16+source = (root / 'tests/lib/jibb-generic-recursion.hoon').read_text()

17+source = source[source.index('\n|%\n') + 1:]

18+names = ['tree', 'changed', 'alias', 'client', 'bad-mold', 'bad-constructor',

19+ 'bad-parameter', 'local-shadow', 'local-distinct', 'local-only',

20+ 'list-shadow', 'chain', 'bad-match']

21+files = ['tree', 'tree-changed', 'alias', 'client', 'bad-mold', 'bad-constructor',

22+ 'bad-parameter', 'local-shadow', 'local-distinct', 'local-only',

23+ 'list-shadow', 'chain', 'bad-match']

24+cords = [item for name, file in zip(names, files)

25+ for item in ('--cord', f'{name}-text={fixture / (file + ".txt")}')]

26+cords += ['--cord', f'prelude={root / "jibb-dev/lib/jibb/prelude.jibb"}',

27+ '--cord', f'internal={root / "jibb-dev/lib/jibb/internal.jibb"}']

28+bindings = ''.join(f'=/ {name}=wain (to-wain:format {name}-text)\n'

29+ for name in names)

30+program = ("=/ jibb .\n=/ real-prelude=@t prelude\n"

31+ "=/ real-internal=@t internal\n" + bindings +

32+ "=/ expected=wain ~\n=/ suite\n" + source +

33+ "\n^- @t\n=/ invalid=(list [label=@t src=@t])\n"

34+ " :~ ['unused mold hole declined' bad-mold-text]\n"

35+ " ['constructor declined' bad-constructor-text]\n"

36+ " ['matching declined' bad-match-text]\n"

37+ " ['nonuniform recursion declined' bad-parameter-text]\n"

38+ " ['identical local shadow declined' local-shadow-text]\n"

39+ " ['different local shadow declined' local-distinct-text]\n"

40+ " ['local recursion declined' local-only-text]\n"

41+ " ==\n"

42+ "(generic-output:suite prelude internal tree-text changed-text alias-text client-text invalid list-shadow-text chain-text)\n")

43+with tempfile.TemporaryDirectory(prefix='jibb-generic-recursion-') as tmp:

44+ path = Path(tmp) / 'test.hoon'

45+ path.write_text(program)

46+ result = subprocess.run([str(root / 'tools/hoon'), '--lib', args.lib, '--raw',

47+ '-f', str(path), *cords], stdout=subprocess.PIPE)

48+if result.returncode:

49+ sys.exit(result.returncode)

50+expected_path = fixture / 'expected.txt'

51+if args.update:

52+ expected_path.write_bytes(result.stdout)

53+else:

54+ expected = expected_path.read_bytes()

55+ if result.stdout != expected:

56+ sys.stderr.writelines(difflib.unified_diff(

57+ expected.decode().splitlines(keepends=True),

58+ result.stdout.decode().splitlines(keepends=True),

59+ fromfile='expected.txt', tofile='actual'))

60+ sys.exit(1)

61+print('source-backed generic recursion guards passed')