git.iko.soy/jibb
on master help sign in
Track source-proven generic recursive identities
c96597diko
README.md+1−1
compare with master
unifiedsplit
@@ -42,7 +42,7 @@ tools/hoon '(golden /a/b/jibb (crip "++ main view"))'
42tools/hoon --raw --cord src=tests/golden/foo/source.jibb 'tree:(golden /a/b/jibb src)'
42tools/hoon --raw --cord src=tests/golden/foo/source.jibb 'tree:(golden /a/b/jibb src)'
43```
43```
44
44
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.
46
46
47### The doc's examples
47### The doc's examples
48
48
docs/compiler.md+3−1
@@ -56,7 +56,7 @@ The core is split into chapters, `+| %name`, in this order:
56| `%span-check` | `+check-spans`, which `+golden` runs on every tree, and `+check-spans-test` |
56| `%span-check` | `+check-spans`, which `+golden` runs on every tree, and `+check-spans-test` |
57| `%type-inference` | The initial inference fragment and its unification helpers; not yet a module type checker |
57| `%type-inference` | The initial inference fragment and its unification helpers; not yet a module type checker |
58
58
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.
60
60
61A 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.
61A 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.
62
62
@@ -94,6 +94,8 @@ A known closed union can also provide context to each arm of a complete loobean
94
94
95The 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.
95The 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.
96
96
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+
97Self-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.
99Self-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.
98
100
99The 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.
101The 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
72| `tools/type-api-evidence-test` | Runs source, scope, reader-result and declaration-watchability evidence guards under eval and on the ship |
72| `tools/type-api-evidence-test` | Runs source, scope, reader-result and declaration-watchability evidence guards under eval and on the ship |
73| `tools/type-hole-guards-test` | Runs the shared hole-defaulting and API interface guards under eval; the same checks run on the ship |
73| `tools/type-hole-guards-test` | Runs the shared hole-defaulting and API interface guards under eval; the same checks run on the ship |
74| `tools/type-list-alias-test` | Runs the shared prelude list-alias and provenance guards under eval and on the ship |
74| `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 |
75| `tools/type-generic-alias-test` | Runs public/private generic union alias and provenance guards under eval and on the ship |
76| `tools/type-generic-alias-test` | Runs public/private generic union alias and provenance guards under eval and on the ship |
76| `tools/type-positional-face-guards-test` | Runs positional-call and nested-face guards under eval and on the ship |
77| `tools/type-positional-face-guards-test` | Runs positional-call and nested-face guards under eval and on the ship |
77| `tools/type-qath-guards-test` | Runs source-provenance, recursive unfolding and face guards under eval and on the ship |
78| `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
122tools/type-todo-partial-test # unchanged todo partial report and reader failure controls
123tools/type-todo-partial-test # unchanged todo partial report and reader failure controls
123tools/type-todo-api-test # real todo API partial inference and reader guards pass
124tools/type-todo-api-test # real todo API partial inference and reader guards pass
124tools/type-direct-gate-test # direct gate source and provenance guards pass
125tools/type-direct-gate-test # direct gate source and provenance guards pass
126+tools/type-generic-recursion-test # source-backed recursive identities and provenance
125tools/type-closed-gate-guards-test # closed gate fit guards pass
127tools/type-closed-gate-guards-test # closed gate fit guards pass
126tools/type-constructor-fit-guards-test # constructor fit guards pass
128tools/type-constructor-fit-guards-test # constructor fit guards pass
127tools/type-nested-union-guards-test # nested union selector guards pass
129tools/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
23
23
24On 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.
24On 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.
25
25
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.
27
29
28The 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.
30The 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.
29
31
@@ -72,7 +74,7 @@ What the plan asks for, and where it is:
72Besides the plan's list:
74Besides the plan's list:
73
75
74- 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.
76- 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.
76- `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.
78- `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.
77- 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.
79- 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.
78- 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).
80- 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:
174| 4da6891 | 2026-10-31 | Add source-backed comparisons and nested Hoon union controls |
176| 4da6891 | 2026-10-31 | Add source-backed comparisons and nested Hoon union controls |
175| 09db390 | 2026-10-31 | Skip unnecessary inference environment scans |
177| 09db390 | 2026-10-31 | Skip unnecessary inference environment scans |
176| 179d717 | 2026-10-31 | Diagnose source-proven Hoon union overlaps |
178| 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 |
178
181
179## Checking it
182## Checking it
180
183
@@ -195,6 +198,7 @@ tools/type-api-paths-test # partial API path metadata fixture
195tools/type-hole-guards-test # hole defaulting and API interface guards
198tools/type-hole-guards-test # hole defaulting and API interface guards
196tools/type-list-alias-test # prelude list-alias guards
199tools/type-list-alias-test # prelude list-alias guards
197tools/type-generic-alias-test # generic union alias guards
200tools/type-generic-alias-test # generic union alias guards
201+tools/type-generic-recursion-test # source-proven generic recursion guards
198tools/type-positional-face-guards-test # positional sample face guards
202tools/type-positional-face-guards-test # positional sample face guards
199tools/type-qath-guards-test # qath source and unfolding guards
203tools/type-qath-guards-test # qath source and unfolding guards
200tools/type-ask-guards-test # ask source and bootstrap guards
204tools/type-ask-guards-test # ask source and bootstrap guards
jibb-dev/lib/jibb.hoon+231−45
@@ -4672,6 +4672,7 @@
4672 [%collection name=term args=(list itype)]
4672 [%collection name=term args=(list itype)]
4673 [%recursive module=term name=term label=(unit @t)]
4673 [%recursive module=term name=term label=(unit @t)]
4674 [%jrec at=path name=term label=(unit @t) head=term aura=@ta tail=term]
4674 [%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)]
4675 [%union cases=(list itype) origin=(unit [at=path name=term]) label=(unit @t) args=(list itype)]
4676 [%union cases=(list itype) origin=(unit [at=path name=term]) label=(unit @t) args=(list itype)]
4676 [%face name=term body=itype]
4677 [%face name=term body=itype]
4677 [%fn sample=itype product=itype]
4678 [%fn sample=itype product=itype]
@@ -4743,6 +4744,7 @@
4743 %union |((lien cases.t |=(c=itype (itype-occurs n c sub))) (lien args.t |=(c=itype (itype-occurs n c sub))))
4744 %union |((lien cases.t |=(c=itype (itype-occurs n c sub))) (lien args.t |=(c=itype (itype-occurs n c sub))))
4744 %recursive |
4745 %recursive |
4745 %jrec |
4746 %jrec |
4747+ %grec (lien args.t |=(c=itype (itype-occurs n c sub)))
4746 %collection (lien args.t |=(c=itype (itype-occurs n c sub)))
4748 %collection (lien args.t |=(c=itype (itype-occurs n c sub)))
4747 %face $(t body.t)
4749 %face $(t body.t)
4748 %fn |($(t sample.t) $(t product.t))
4750 %fn |($(t sample.t) $(t product.t))
@@ -4761,6 +4763,9 @@
4761 =. a (itype-walk a sub)
4763 =. a (itype-walk a sub)
4762 =. b (itype-walk b sub)
4764 =. b (itype-walk b sub)
4763 ?: =(a b) `sub
4765 ?: =(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)
4764 ?: &(?=(%jrec -.a) ?=(%jrec -.b))
4769 ?: &(?=(%jrec -.a) ?=(%jrec -.b))
4765 ?:(&(=(at.a at.b) =(name.a name.b) =(head.a head.b) =(aura.a aura.b) =(tail.a tail.b)) `sub ~)
4770 ?:(&(=(at.a at.b) =(name.a name.b) =(head.a head.b) =(aura.a aura.b) =(tail.a tail.b)) `sub ~)
4766 ?: &(?=(%recursive -.a) ?=(%recursive -.b))
4771 ?: &(?=(%recursive -.a) ?=(%recursive -.b))
@@ -4871,6 +4876,7 @@
4871 %union |((lien cases.t |=(c=itype (itype-has-any-atom c sub))) (lien args.t |=(c=itype (itype-has-any-atom c sub))))
4876 %union |((lien cases.t |=(c=itype (itype-has-any-atom c sub))) (lien args.t |=(c=itype (itype-has-any-atom c sub))))
4872 %recursive |
4877 %recursive |
4873 %jrec |
4878 %jrec |
4879+ %grec (lien args.t |=(c=itype (itype-has-any-atom c sub)))
4874 %collection (lien args.t |=(c=itype (itype-has-any-atom c sub)))
4880 %collection (lien args.t |=(c=itype (itype-has-any-atom c sub)))
4875 %face $(t body.t)
4881 %face $(t body.t)
4876 %fn |($(t sample.t) $(t product.t))
4882 %fn |($(t sample.t) $(t product.t))
@@ -4945,6 +4951,7 @@
4945 %union |((lien cases.typ |=(c=itype (itype-has-fixed-atom c))) (lien args.typ |=(c=itype (itype-has-fixed-atom c))))
4951 %union |((lien cases.typ |=(c=itype (itype-has-fixed-atom c))) (lien args.typ |=(c=itype (itype-has-fixed-atom c))))
4946 %recursive |
4952 %recursive |
4947 %jrec |
4953 %jrec |
4954+ %grec (lien args.typ |=(c=itype (itype-has-fixed-atom c)))
4948 %collection (lien args.typ |=(c=itype (itype-has-fixed-atom c)))
4955 %collection (lien args.typ |=(c=itype (itype-has-fixed-atom c)))
4949 %face $(typ body.typ)
4956 %face $(typ body.typ)
4950 %fn |($(typ sample.typ) $(typ product.typ))
4957 %fn |($(typ sample.typ) $(typ product.typ))
@@ -4973,6 +4980,7 @@
4973 ^- ?
4980 ^- ?
4974 =. t (itype-walk t sub)
4981 =. t (itype-walk t sub)
4975 ?- -.t
4982 ?- -.t
4983+ %grec (lien args.t |=(c=itype (itype-has-face c sub)))
4976 %collection (lien args.t |=(c=itype (itype-has-face c sub)))
4984 %collection (lien args.t |=(c=itype (itype-has-face c sub)))
4977 %face &
4985 %face &
4978 %cell |($(t hed.t) $(t tal.t))
4986 %cell |($(t hed.t) $(t tal.t))
@@ -5029,6 +5037,9 @@
5029 ^- ?
5037 ^- ?
5030 =. a (itype-walk a sub)
5038 =. a (itype-walk a sub)
5031 =. b (itype-walk b sub)
5039 =. 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)
5032 ?: &(?=(%collection -.a) ?=(%collection -.b))
5043 ?: &(?=(%collection -.a) ?=(%collection -.b))
5033 ?. =(name.a name.b) |
5044 ?. =(name.a name.b) |
5034 (itype-face-asym-collection-args args.a args.b sub)
5045 (itype-face-asym-collection-args args.a args.b sub)
@@ -5091,6 +5102,7 @@
5091 %union &
5102 %union &
5092 %recursive &
5103 %recursive &
5093 %jrec &
5104 %jrec &
5105+ %grec &
5094 %noun &
5106 %noun &
5095 %collection &
5107 %collection &
5096 %face $(t body.t)
5108 %face $(t body.t)
@@ -5120,6 +5132,7 @@
5120 ^- ?
5132 ^- ?
5121 ?- -.t
5133 ?- -.t
5122 %tag &
5134 %tag &
5135+ %grec (lien args.t |=(c=itype (itype-has-tag c)))
5123 %collection (lien args.t |=(c=itype (itype-has-tag c)))
5136 %collection (lien args.t |=(c=itype (itype-has-tag c)))
5124 %face $(t body.t)
5137 %face $(t body.t)
5125 %fn |($(t sample.t) $(t product.t))
5138 %fn |($(t sample.t) $(t product.t))
@@ -5133,6 +5146,7 @@
5133 ^- ?
5146 ^- ?
5134 ?- -.t
5147 ?- -.t
5135 %union &
5148 %union &
5149+ %grec (lien args.t |=(c=itype (itype-has-union c)))
5136 %collection (lien args.t |=(c=itype (itype-has-union c)))
5150 %collection (lien args.t |=(c=itype (itype-has-union c)))
5137 %face $(t body.t)
5151 %face $(t body.t)
5138 %fn |($(t sample.t) $(t product.t))
5152 %fn |($(t sample.t) $(t product.t))
@@ -5151,6 +5165,7 @@
5151 %union
5165 %union
5152 ?: &(?=(~ label.t) ?=(^ args.t)) &
5166 ?: &(?=(~ label.t) ?=(^ args.t)) &
5153 (lien (weld args.t cases.t) |=(c=itype (itype-has-hidden-generic c)))
5167 (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))))
5154 %collection (lien args.t |=(c=itype (itype-has-hidden-generic c)))
5169 %collection (lien args.t |=(c=itype (itype-has-hidden-generic c)))
5155 %face $(t body.t)
5170 %face $(t body.t)
5156 %fn |($(t sample.t) $(t product.t))
5171 %fn |($(t sample.t) $(t product.t))
@@ -5164,6 +5179,7 @@
5164 ?- -.t
5179 ?- -.t
5165 %recursive &
5180 %recursive &
5166 %jrec &
5181 %jrec &
5182+ %grec &
5167 %collection (lien args.t |=(c=itype (itype-has-recursive c)))
5183 %collection (lien args.t |=(c=itype (itype-has-recursive c)))
5168 %union (lien (weld args.t cases.t) |=(c=itype (itype-has-recursive c)))
5184 %union (lien (weld args.t cases.t) |=(c=itype (itype-has-recursive c)))
5169 %face $(t body.t)
5185 %face $(t body.t)
@@ -5178,6 +5194,7 @@
5178 ?- -.t
5194 ?- -.t
5179 %recursive ?=(~ label.t)
5195 %recursive ?=(~ label.t)
5180 %jrec ?=(~ label.t)
5196 %jrec ?=(~ label.t)
5197+ %grec |(?=(~ label.t) (lien args.t |=(c=itype (itype-has-hidden-recursive c))))
5181 %collection (lien args.t |=(c=itype (itype-has-hidden-recursive c)))
5198 %collection (lien args.t |=(c=itype (itype-has-hidden-recursive c)))
5182 %union (lien (weld args.t cases.t) |=(c=itype (itype-has-hidden-recursive c)))
5199 %union (lien (weld args.t cases.t) |=(c=itype (itype-has-hidden-recursive c)))
5183 %face $(t body.t)
5200 %face $(t body.t)
@@ -5223,7 +5240,7 @@
5223 ?: ?=(%var -.raw)
5240 ?: ?=(%var -.raw)
5224 $(cases t.cases, pending &)
5241 $(cases t.cases, pending &)
5225 =/ c=itype (itype-walk raw sub)
5242 =/ c=itype (itype-walk raw sub)
5226− ?: ?=(?(%var %tag %recursive %jrec %union %face) -.c)
5243+ ?: ?=(?(%var %tag %recursive %jrec %grec %union %face) -.c)
5227 $(cases t.cases, pending &)
5244 $(cases t.cases, pending &)
5228 ?. ?=(%cell -.c) $(cases t.cases)
5245 ?. ?=(%cell -.c) $(cases t.cases)
5229 =/ raw-head=itype hed.c
5246 =/ raw-head=itype hed.c
@@ -5236,7 +5253,7 @@
5236 ?: ?=(?(%atom %any-atom %flag %avar %rvar %nvar %rnvar) -.body.head)
5253 ?: ?=(?(%atom %any-atom %flag %avar %rvar %nvar %rnvar) -.body.head)
5237 $(cases t.cases)
5254 $(cases t.cases)
5238 $(cases t.cases, pending &)
5255 $(cases t.cases, pending &)
5239− ?: ?=(?(%var %tag %recursive %jrec %union) -.head)
5256+ ?: ?=(?(%var %tag %recursive %jrec %grec %union) -.head)
5240 $(cases t.cases, pending &)
5257 $(cases t.cases, pending &)
5241 ?. ?=(%const -.head) $(cases t.cases)
5258 ?. ?=(%const -.head) $(cases t.cases)
5242 ?. =(val.literal.head val.tag) $(cases t.cases)
5259 ?. =(val.literal.head val.tag) $(cases t.cases)
@@ -5285,6 +5302,14 @@
5285 [%ok sub next]
5302 [%ok sub next]
5286 :: An arbitrary noun is not known to fit a narrower type.
5303 :: An arbitrary noun is not known to fit a narrower type.
5287 ?: &(?=(%noun -.actual) !?=(%var -.expected)) [%unknown ~]
5304 ?: &(?=(%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 ~]
5288 ?: &(!uncertain ?=(%jrec -.actual) ?=(%face -.expected)) $(expected body.expected)
5313 ?: &(!uncertain ?=(%jrec -.actual) ?=(%face -.expected)) $(expected body.expected)
5289 ?: &(!uncertain ?=(%face -.actual) ?=(%jrec -.expected)) $(actual body.actual)
5314 ?: &(!uncertain ?=(%face -.actual) ?=(%jrec -.expected)) $(actual body.actual)
5290 ?: &(?=(%jrec -.actual) ?=(%jrec -.expected))
5315 ?: &(?=(%jrec -.actual) ?=(%jrec -.expected))
@@ -5674,10 +5699,11 @@
5674 %tag [%unknown | fuel ~]
5699 %tag [%unknown | fuel ~]
5675 %recursive [%unknown | fuel ~]
5700 %recursive [%unknown | fuel ~]
5676 %jrec [%yes & fuel ~]
5701 %jrec [%yes & fuel ~]
5702+ %grec [%unknown | fuel ~]
5677 ==
5703 ==
5678::
5704::
5679+$ igate-prelude-evidence [iface=ifile gates=(map term def)]
5705+$ 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)])]
5681+$ idiag [msg=tape sites=(list [at=span note=tape])]
5707+$ idiag [msg=tape sites=(list [at=span note=tape])]
5682+$ iresult (each [typ=itype state=istate] idiag)
5708+$ iresult (each [typ=itype state=istate] idiag)
5683+$ isample-result (each [typ=itype env=ienv state=istate] tape)
5709+$ isample-result (each [typ=itype env=ienv state=istate] tape)
@@ -5697,6 +5723,7 @@
5697 |= [t=itype sub=isub]
5723 |= [t=itype sub=isub]
5698 ^- itype
5724 ^- itype
5699 =. t (itype-walk t sub)
5725 =. t (itype-walk t sub)
5726+ ?: ?=(%grec -.t) t(args (turn args.t |=(c=itype (itype-normalize c sub))))
5700 ?: ?=(%collection -.t) [%collection name.t (turn args.t |=(c=itype (itype-normalize c sub)))]
5727 ?: ?=(%collection -.t) [%collection name.t (turn args.t |=(c=itype (itype-normalize c sub)))]
5701 ?: ?=(%union -.t)
5728 ?: ?=(%union -.t)
5702 [%union (turn cases.t |=(c=itype (itype-normalize c sub))) origin.t label.t (turn args.t |=(c=itype (itype-normalize c sub)))]
5729 [%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 @@
5723 %cell |($(t hed.t) $(t tal.t))
5750 %cell |($(t hed.t) $(t tal.t))
5724 %recursive |
5751 %recursive |
5725 %jrec |
5752 %jrec |
5753+ %grec &
5726 %collection (lien args.t |=(c=itype (itype-has-gate c)))
5754 %collection (lien args.t |=(c=itype (itype-has-gate c)))
5727 %face $(t body.t)
5755 %face $(t body.t)
5728 %union (lien cases.t |=(c=itype (itype-has-gate c)))
5756 %union (lien cases.t |=(c=itype (itype-has-gate c)))
@@ -5746,6 +5774,7 @@
5746 ?- -.t
5774 ?- -.t
5747 %nvar [%atom %ud]
5775 %nvar [%atom %ud]
5748 %rnvar [%atom %ud]
5776 %rnvar [%atom %ud]
5777+ %grec t(args (turn args.t |=(c=itype (default-decimals c))))
5749 %collection [%collection name.t (turn args.t |=(c=itype (default-decimals c)))]
5778 %collection [%collection name.t (turn args.t |=(c=itype (default-decimals c)))]
5750 %face [%face name.t $(t body.t)]
5779 %face [%face name.t $(t body.t)]
5751 %cell [%cell $(t hed.t) $(t tal.t)]
5780 %cell [%cell $(t hed.t) $(t tal.t)]
@@ -5787,6 +5816,7 @@
5787 %tag |
5816 %tag |
5788 %any-atom &
5817 %any-atom &
5789 %union &((levy cases.t |=(c=itype (hole-known c state))) (levy args.t |=(c=itype (hole-known c state))))
5818 %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)))
5790 %collection (levy args.t |=(c=itype (hole-known c state)))
5820 %collection (levy args.t |=(c=itype (hole-known c state)))
5791 %face $(t body.t)
5821 %face $(t body.t)
5792 %fn &($(t sample.t) $(t product.t))
5822 %fn &($(t sample.t) $(t product.t))
@@ -5834,6 +5864,7 @@
5834 ?- -.t
5864 ?- -.t
5835 ?(%tag %nvar %rnvar %avar %rvar) !(hole-known t state)
5865 ?(%tag %nvar %rnvar %avar %rvar) !(hole-known t state)
5836 %union |((lien cases.t |=(c=itype (hole-uncertain c state))) (lien args.t |=(c=itype (hole-uncertain c state))))
5866 %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)))
5837 %collection (lien args.t |=(c=itype (hole-uncertain c state)))
5868 %collection (lien args.t |=(c=itype (hole-uncertain c state)))
5838 %face $(t body.t)
5869 %face $(t body.t)
5839 %fn |($(t sample.t) $(t product.t))
5870 %fn |($(t sample.t) $(t product.t))
@@ -5870,6 +5901,7 @@
5870 %union (zing (turn (weld args.t cases.t) |=(c=itype (itype-vars c))))
5901 %union (zing (turn (weld args.t cases.t) |=(c=itype (itype-vars c))))
5871 %recursive ~
5902 %recursive ~
5872 %jrec ~
5903 %jrec ~
5904+ %grec (zing (turn args.t |=(c=itype (itype-vars c))))
5873 %collection (zing (turn args.t |=(c=itype (itype-vars c))))
5905 %collection (zing (turn args.t |=(c=itype (itype-vars c))))
5874 %face $(t body.t)
5906 %face $(t body.t)
5875 %fn (weld $(t sample.t) $(t product.t))
5907 %fn (weld $(t sample.t) $(t product.t))
@@ -5918,6 +5950,7 @@
5918 %union [%union (turn cases.t |=(c=itype (itype-rename c ren))) origin.t label.t (turn args.t |=(c=itype (itype-rename c ren)))]
5950 %union [%union (turn cases.t |=(c=itype (itype-rename c ren))) origin.t label.t (turn args.t |=(c=itype (itype-rename c ren)))]
5919 %recursive t
5951 %recursive t
5920 %jrec t
5952 %jrec t
5953+ %grec t(args (turn args.t |=(c=itype (itype-rename c ren))))
5921 %collection [%collection name.t (turn args.t |=(c=itype (itype-rename c ren)))]
5954 %collection [%collection name.t (turn args.t |=(c=itype (itype-rename c ren)))]
5922 %face [%face name.t $(t body.t)]
5955 %face [%face name.t $(t body.t)]
5923 %fn [%fn $(t sample.t) $(t product.t)]
5956 %fn [%fn $(t sample.t) $(t product.t)]
@@ -5945,6 +5978,7 @@
5945 %union |((lien cases.t |=(c=itype (itype-var-is-atom n c))) (lien args.t |=(c=itype (itype-var-is-atom n c))))
5978 %union |((lien cases.t |=(c=itype (itype-var-is-atom n c))) (lien args.t |=(c=itype (itype-var-is-atom n c))))
5946 %recursive |
5979 %recursive |
5947 %jrec |
5980 %jrec |
5981+ %grec (lien args.t |=(c=itype (itype-var-is-atom n c)))
5948 %collection (lien args.t |=(c=itype (itype-var-is-atom n c)))
5982 %collection (lien args.t |=(c=itype (itype-var-is-atom n c)))
5949 %face $(t body.t)
5983 %face $(t body.t)
5950 %fn |($(t sample.t) $(t product.t))
5984 %fn |($(t sample.t) $(t product.t))
@@ -5968,6 +6002,7 @@
5968 %union |((lien cases.t |=(c=itype (itype-var-is-restricted n c))) (lien args.t |=(c=itype (itype-var-is-restricted n c))))
6002 %union |((lien cases.t |=(c=itype (itype-var-is-restricted n c))) (lien args.t |=(c=itype (itype-var-is-restricted n c))))
5969 %recursive |
6003 %recursive |
5970 %jrec |
6004 %jrec |
6005+ %grec (lien args.t |=(c=itype (itype-var-is-restricted n c)))
5971 %collection (lien args.t |=(c=itype (itype-var-is-restricted n c)))
6006 %collection (lien args.t |=(c=itype (itype-var-is-restricted n c)))
5972 %face $(t body.t)
6007 %face $(t body.t)
5973 %fn |($(t sample.t) $(t product.t))
6008 %fn |($(t sample.t) $(t product.t))
@@ -6398,6 +6433,16 @@
6398 ?: &(?=(~ vars.template) ?=(%jrec -.typ.template) =(at.typ.template origin) =(name.typ.template name)) `name.i.molds
6433 ?: &(?=(~ vars.template) ?=(%jrec -.typ.template) =(at.typ.template origin) =(name.typ.template name)) `name.i.molds
6399 $(molds t.molds)
6434 $(molds t.molds)
6400::
6435::
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+::
6401++ itype-in-import
6446++ itype-in-import
6402 |= [t=itype iface=ifile face=term prelude=(unit ifile)]
6447 |= [t=itype iface=ifile face=term prelude=(unit ifile)]
6403 ^- itype
6448 ^- itype
@@ -6417,6 +6462,11 @@
6417 `(crip "{(trip u.alias)}.{(trip face)}")
6462 `(crip "{(trip u.alias)}.{(trip face)}")
6418 [%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)))]
6463 [%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)))]
6419 %recursive [%recursive module.t name.t ~]
6464 %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))))
6420 %jrec
6470 %jrec
6421 =/ public=(unit term) ?~(prelude ~ (jrec-alias at.t name.t molds.u.prelude))
6471 =/ public=(unit term) ?~(prelude ~ (jrec-alias at.t name.t molds.u.prelude))
6422 ?^ public t(label `u.public)
6472 ?^ public t(label `u.public)
@@ -6529,9 +6579,29 @@
6529 ?. =(names.tail ~[name]) ~
6579 ?. =(names.tail ~[name]) ~
6530 `[%jrec at.state name `name name.i.fs aura.shape.i.fs name.i.t.fs]
6580 `[%jrec at.state name `name name.i.fs aura.shape.i.fs name.i.t.fs]
6531::
6581::
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+
6532++ infer-mold-template
6598++ infer-mold-template
6533 |= [sh=shape state=istate]
6599 |= [sh=shape state=istate]
6534 ^- (unit [template=ischeme state=istate])
6600 ^- (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))]
6535 =/ direct=(unit itype)
6605 =/ direct=(unit itype)
6536 ?. ?=([@ ~] active.state) ~
6606 ?. ?=([@ ~] active.state) ~
6537 (simple-source-recursive i.active.state sh state)
6607 (simple-source-recursive i.active.state sh state)
@@ -6744,6 +6814,8 @@
6744 ?~ applied ~
6814 ?~ applied ~
6745 `[u.applied state.u.args]
6815 `[u.applied state.u.args]
6746 ?. ?=(%generic -.u.found) ~
6816 ?. ?=(%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]
6747 ?. (distinct-params vars.u.found) ~
6819 ?. (distinct-params vars.u.found) ~
6748 =/ params=(unit iparams) (bind-params vars.u.found types.u.args)
6820 =/ params=(unit iparams) (bind-params vars.u.found types.u.args)
6749 ?~ params ~
6821 ?~ params ~
@@ -8982,7 +9054,7 @@
8982 ?~ t.names |
9054 ?~ t.names |
8983 =. typ (itype-walk typ sub)
9055 =. typ (itype-walk typ sub)
8984 ?: ?=(%cell -.typ) $(typ tal.typ, names t.names)
9056 ?: ?=(%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))
8986::
9058::
8987++ cell-binder-pattern
9059++ cell-binder-pattern
8988 |= e=expr
9060 |= e=expr
@@ -9061,6 +9133,7 @@
9061 "({(trip u.label.t)} {(show-itype-cases args.t sub)})"
9133 "({(trip u.label.t)} {(show-itype-cases args.t sub)})"
9062 %recursive ?~(label.t "recursive mold" (trip u.label.t))
9134 %recursive ?~(label.t "recursive mold" (trip u.label.t))
9063 %jrec ?~(label.t "recursive mold" (trip u.label.t))
9135 %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)})")
9064 %collection "({(trip name.t)} {(show-itype-cases args.t sub)})"
9137 %collection "({(trip name.t)} {(show-itype-cases args.t sub)})"
9065 %face "[{(trip name.t)}={(show-itype-context body.t sub)}]"
9138 %face "[{(trip name.t)}={(show-itype-context body.t sub)}]"
9066 %fn "$-({(show-itype-context sample.t sub)} {(show-itype-context product.t sub)})"
9139 %fn "$-({(show-itype-context sample.t sub)} {(show-itype-context product.t sub)})"
@@ -9109,6 +9182,7 @@
9109 %union |((lien cases.typ |=(c=itype (itype-has-nvar c))) (lien args.typ |=(c=itype (itype-has-nvar c))))
9182 %union |((lien cases.typ |=(c=itype (itype-has-nvar c))) (lien args.typ |=(c=itype (itype-has-nvar c))))
9110 %recursive |
9183 %recursive |
9111 %jrec |
9184 %jrec |
9185+ %grec (lien args.typ |=(c=itype (itype-has-nvar c)))
9112 %collection (lien args.typ |=(c=itype (itype-has-nvar c)))
9186 %collection (lien args.typ |=(c=itype (itype-has-nvar c)))
9113 %face $(typ body.typ)
9187 %face $(typ body.typ)
9114 %fn |($(typ sample.typ) $(typ product.typ))
9188 %fn |($(typ sample.typ) $(typ product.typ))
@@ -9225,6 +9299,7 @@
9225 %union |((lien cases.t |=(c=itype (has-atom-var n c))) (lien args.t |=(c=itype (has-atom-var n c))))
9299 %union |((lien cases.t |=(c=itype (has-atom-var n c))) (lien args.t |=(c=itype (has-atom-var n c))))
9226 %recursive |
9300 %recursive |
9227 %jrec |
9301 %jrec |
9302+ %grec (lien args.t |=(c=itype (has-atom-var n c)))
9228 %collection (lien args.t |=(c=itype (has-atom-var n c)))
9303 %collection (lien args.t |=(c=itype (has-atom-var n c)))
9229 %face $(t body.t)
9304 %face $(t body.t)
9230 %fn |($(t sample.t) $(t product.t))
9305 %fn |($(t sample.t) $(t product.t))
@@ -9633,36 +9708,9 @@
9633++ add-supported-defs
9708++ add-supported-defs
9634 |= [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)]
9709 |= [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)]
9635 ^- [env=ienv artifacts=(list iwidth-definition)]
9710 ^- [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 ~ ~ ~]
9711+ (add-supported-defs-core ds all-defs checked heads env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts ~)
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)
9665::
9712::
9713+
9666+$ iresolved [env=ienv grouped=(list term) artifacts=(list iwidth-definition)]
9714+$ iresolved [env=ienv grouped=(list term) artifacts=(list iwidth-definition)]
9667+$ iadj (map term (list term))
9715+$ iadj (map term (list term))
9668+$ ivisited (map term ?)
9716+$ ivisited (map term ?)
@@ -9776,6 +9824,46 @@
9776++ resolve-groups
9824++ resolve-groups
9777 |= [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)]
9825 |= [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)]
9778 ^- iresolved
9826 ^- 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
9779 =/ env=ienv ~
9867 =/ env=ienv ~
9780 =/ grouped=(list term) ~
9868 =/ grouped=(list term) ~
9781 =/ artifacts=(list iwidth-definition) ~
9869 =/ artifacts=(list iwidth-definition) ~
@@ -9787,8 +9875,9 @@
9787 =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)
9875 =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)
9788 |-
9876 |-
9789 =/ next=[env=ienv artifacts=(list iwidth-definition)]
9877 =/ 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)
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)
9791− =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~]
9879+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~]
9880+ =. grec-index.initial index
9792 =/ out=iresolved (add-groups ds components graph env.next grouped artifacts.next initial)
9881 =/ out=iresolved (add-groups ds components graph env.next grouped artifacts.next initial)
9793 ?: =(env env.out) out
9882 ?: =(env env.out) out
9794 $(env env.out, grouped grouped.out, artifacts artifacts.out)
9883 $(env env.out, grouped grouped.out, artifacts artifacts.out)
@@ -10588,6 +10677,9 @@
10588 |= [typ=itype name=term vars=(list @ud)]
10677 |= [typ=itype name=term vars=(list @ud)]
10589 ^- itype
10678 ^- itype
10590 ?: ?=(%jrec -.typ) typ(label `name)
10679 ?: ?=(%jrec -.typ) typ(label `name)
10680+ ?: ?=(%grec -.typ)
10681+ ?. (identity-union-parameters vars args.typ) typ(label ~)
10682+ typ(label `name)
10591 ?. ?=(%union -.typ) typ
10683 ?. ?=(%union -.typ) typ
10592 ?. (identity-union-parameters vars args.typ)
10684 ?. (identity-union-parameters vars args.typ)
10593 ?~ origin.typ typ
10685 ?~ origin.typ typ
@@ -10661,7 +10753,7 @@
10661 =/ source-unit=(unit ischeme)
10753 =/ source-unit=(unit ischeme)
10662 ?~ unit-decl ~
10754 ?~ unit-decl ~
10663 =/ unit-molds=imolds ~[[%unit u.unit-decl]]
10755 =/ 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 ~ ~ ~ ~]
10665 =/ unit-types=imold-types (partial-prelude-molds unit-molds unit-state)
10757 =/ unit-types=imold-types (partial-prelude-molds unit-molds unit-state)
10666 =/ unit-iface=ifile [~ unit-types /lib/jibb/prelude/jibb ~ ~ ~ ~ ~]
10758 =/ unit-iface=ifile [~ unit-types /lib/jibb/prelude/jibb ~ ~ ~ ~ ~]
10667 =/ found=(unit ischeme) (find-jibb-mold %unit unit-iface)
10759 =/ found=(unit ischeme) (find-jibb-mold %unit unit-iface)
@@ -10676,7 +10768,7 @@
10676 =/ js=ijimports ~[[face.i.imports.mod primitive]]
10768 =/ js=ijimports ~[[face.i.imports.mod primitive]]
10677 =/ reserved=(list term) ~[face.i.imports.mod]
10769 =/ reserved=(list term) ~[face.i.imports.mod]
10678 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10770 =/ 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 ~ ~ ~ ~]
10680 =/ mts=(each imold-types @t) (module-mold-types molds state)
10772 =/ mts=(each imold-types @t) (module-mold-types molds state)
10681 =/ usable=(unit imold-types)
10773 =/ usable=(unit imold-types)
10682 ?: ?=(%& -.mts) `p.mts
10774 ?: ?=(%& -.mts) `p.mts
@@ -10732,7 +10824,7 @@
10732 =? env-molds declared
10824 =? env-molds declared
10733 (skim molds |=(m=[name=term body=shape] !=(%list name.m)))
10825 (skim molds |=(m=[name=term body=shape] !=(%list name.m)))
10734 =/ reserved=(list term) ?:(declared ~[%list] ~)
10826 =/ 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 ~ ~ ~ ~]
10736 :: Other prelude molds may use list only after its source has passed
10828 :: Other prelude molds may use list only after its source has passed
10737 :: the standard-list check. The raw declaration remains removed.
10829 :: the standard-list check. The raw declaration remains removed.
10738 =/ declared-list=(unit shape) (find-simple-mold %list molds)
10830 =/ declared-list=(unit shape) (find-simple-mold %list molds)
@@ -11261,7 +11353,7 @@
11261 =/ surs=(list term) (collect-sur-imports imports.mod)
11353 =/ surs=(list term) (collect-sur-imports imports.mod)
11262 =/ reserved=(list term) (weld molds.prep (turn resolved.p.deps |=(j=[face=term interface=ifile] face.j)))
11354 =/ reserved=(list term) (weld molds.prep (turn resolved.p.deps |=(j=[face=term interface=ifile] face.j)))
11263 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
11355 =/ 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 ~ ~ ~ ~]
11265 =/ mts=(each imold-types @t) (module-mold-types molds state)
11357 =/ mts=(each imold-types @t) (module-mold-types molds state)
11266 ?: ?=(%| -.mts) [%| p.mts]
11358 ?: ?=(%| -.mts) [%| p.mts]
11267 =/ resolution=iresolved (resolve-groups ordinary molds globals externals surs marks declared resolved.p.deps reserved file prelude)
11359 =/ resolution=iresolved (resolve-groups ordinary molds globals externals surs marks declared resolved.p.deps reserved file prelude)
@@ -11295,7 +11387,7 @@
11295 =/ surs=(list term) (collect-sur-imports imports.mod)
11387 =/ surs=(list term) (collect-sur-imports imports.mod)
11296 =/ reserved=(list term) (weld molds.prep (turn resolved.p.deps |=(j=[face=term interface=ifile] face.j)))
11388 =/ reserved=(list term) (weld molds.prep (turn resolved.p.deps |=(j=[face=term interface=ifile] face.j)))
11297 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
11389 =/ 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 ~ ~ ~ ~]
11299 =/ mts=(each imold-types @t) (module-mold-types molds state)
11391 =/ mts=(each imold-types @t) (module-mold-types molds state)
11300 ?: ?=(%| -.mts) [%| p.mts]
11392 ?: ?=(%| -.mts) [%| p.mts]
11301 =/ resolution=iresolved (resolve-groups ordinary molds globals externals surs marks declared resolved.p.deps reserved file prelude)
11393 =/ resolution=iresolved (resolve-groups ordinary molds globals externals surs marks declared resolved.p.deps reserved file prelude)
@@ -11671,16 +11763,35 @@
11671 [%| (crip "module kind needs unsupported inference: {(spud at)}")]
11763 [%| (crip "module kind needs unsupported inference: {(spud at)}")]
11672 =/ js=jimports-result (resolve-jibb-imports imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
11764 =/ js=jimports-result (resolve-jibb-imports imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
11673 ?: ?=(%| -.js) [%| p.js]
11765 ?: ?=(%| -.js) [%| p.js]
11766+ =/ collected=grec-collected
11674− =/ molds=imolds (collect-simple-molds defs.mod)
11767+ ?^ imports.mod [(collect-simple-molds defs.mod) *(map term shape)]
11768+ (grec-collect-molds defs.mod)
11769+ =/ molds=imolds molds.collected
11675 =/ globals=(list term) (weld prelude-values (weld (import-binding-names imports.mod) vals))
11770 =/ globals=(list term) (weld prelude-values (weld (import-binding-names imports.mod) vals))
11676 =/ surs=(list term) (collect-sur-imports imports.mod)
11771 =/ surs=(list term) (collect-sur-imports imports.mod)
11677 =/ marks=(list term) (collect-mark-imports imports.mod)
11772 =/ marks=(list term) (collect-mark-imports imports.mod)
11678 =/ reserved=(list term) (weld prelude-molds (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
11773 =/ reserved=(list term) (weld prelude-molds (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
11679 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
11774 =/ 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
11681 =/ mts=(each imold-types @t) (module-mold-types molds state)
11789 =/ mts=(each imold-types @t) (module-mold-types molds state)
11682 ?: ?=(%| -.mts) [%| (crip "{(trip p.mts)}: {(spud at)}")]
11790 ?: ?=(%| -.mts) [%| (crip "{(trip p.mts)}: {(spud at)}")]
11791+ =/ resolution=iresolved
11792+ ?~ index
11683− =/ resolution=iresolved (resolve-groups defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
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)
11684 =/ env=ienv env.resolution
11795 =/ env=ienv env.resolution
11685 ?. (module-values-complete defs.mod env)
11796 ?. (module-values-complete defs.mod env)
11686 [%| (crip "module definitions need unsupported inference: {(spud at)}")]
11797 [%| (crip "module definitions need unsupported inference: {(spud at)}")]
@@ -11733,7 +11844,7 @@
11733 =/ declared=(list term) (collect-mark-imports imports.mod)
11844 =/ declared=(list term) (collect-mark-imports imports.mod)
11734 =/ reserved=(list term) (weld molds.u.prepared (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
11845 =/ reserved=(list term) (weld molds.u.prepared (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
11735 =/ top=(list term) (turn ms |=(m=[name=term body=shape] name.m))
11846 =/ 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 ~ ~ ~ ~]
11737 =/ inferred=(unit [template=ischeme state=istate])
11848 =/ inferred=(unit [template=ischeme state=istate])
11738 (infer-mold-template shape.i.selected state(active ~[name], in-mold &))
11849 (infer-mold-template shape.i.selected state(active ~[name], in-mold &))
11739 ?~ inferred [%| 'selected mold needs unsupported inference']
11850 ?~ inferred [%| 'selected mold needs unsupported inference']
@@ -11871,7 +11982,7 @@
11871 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype typ ~)}{(show-atom-constraint typ)}")
11982 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype typ ~)}{(show-atom-constraint typ)}")
11872 $(ds t.ds, lines [line lines])
11983 $(ds t.ds, lines [line lines])
11873 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
11984 =/ 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 ~ ~ ~ ~]
11875 =. gate-defs.initial source-defs
11986 =. gate-defs.initial source-defs
11876 =. head-evidence.initial heads
11987 =. head-evidence.initial heads
11877 =. initial (reserve-def-caps val.d initial)
11988 =. initial (reserve-def-caps val.d initial)
@@ -11913,4 +12024,79 @@
11913 =/ printable=itype (canonical-itype typ vars)
12024 =/ printable=itype (canonical-itype typ vars)
11914 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")
12025 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")
11915 $(ds t.ds, lines [line lines])
12026 $(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+
11916--
12102--
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.
2+
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
7+
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
7+
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):
310 'tests/lib/jibb-arithmetic-guards.hoon',
310 'tests/lib/jibb-arithmetic-guards.hoon',
311 'tests/lib/jibb-positional-face-guards.hoon',
311 'tests/lib/jibb-positional-face-guards.hoon',
312 'tests/lib/jibb-generic-alias.hoon',
312 'tests/lib/jibb-generic-alias.hoon',
313+ 'tests/lib/jibb-generic-recursion.hoon',
313 'tests/lib/jibb-api-evidence.hoon',
314 'tests/lib/jibb-api-evidence.hoon',
314 'tests/lib/jibb-ask-guards.hoon',
315 'tests/lib/jibb-ask-guards.hoon',
315 'tests/lib/jibb-request-guards.hoon',
316 'tests/lib/jibb-request-guards.hoon',
@@ -324,6 +325,11 @@ def generator_checks(tmp):
324 'tests/lib/jibb-gate-free-guards.hoon',
325 'tests/lib/jibb-gate-free-guards.hoon',
325 'tests/lib/jibb-gate-free-source.hoon'}
326 'tests/lib/jibb-gate-free-source.hoon'}
326 <= normal_tests, sorted(normal_tests))
327 <= 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))
327 check('direct gate source and golden are assembled',
333 check('direct gate source and golden are assembled',
328 {'tests/type-direct-gate/source.txt', 'tests/type-direct-gate/expected.txt'}
334 {'tests/type-direct-gate/source.txt', 'tests/type-direct-gate/expected.txt'}
329 <= set(normal.files))
335 <= 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
9+
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')