git.iko.soy/jibb
on master help sign in
Infer record faces and check nested Hoon unions
8bf1b12iko
docs/compiler.md+2−2
compare with master
unifiedsplit
@@ -56,9 +56,9 @@ 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, unfaced cells, a two-binder cell pattern, a complete two-arm loobean branch, closed local mold aliases and acyclic forward value references. It instantiates generalized top-level definitions when they are used. Acyclic local value definitions can refer forward and generalize variables that are free of their enclosing environment; captured variables and explicit capitals remain shared. Acyclic simple local mold aliases can also refer forward, and are scoped to the body, not its gate's sample. Recursive local groups, and recursive, generic, union or faced local molds remain unsupported. 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, its imports, faces, general patterns, deferred constraints, recursive or generic 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 `@`; function compatibility involving nested `@` and variable-dependent joins remain unsupported except for equal types. 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 two-binder cell pattern, a complete two-arm loobean branch, closed local mold aliases and acyclic forward value references. It instantiates generalized top-level definitions when they are used. Acyclic local value definitions can refer forward and generalize variables that are free of their enclosing environment; captured variables and explicit capitals remain shared. Acyclic simple local mold aliases can also refer forward, and are scoped to the body, not its gate's sample. Recursive local groups, and recursive, generic or union local molds remain unsupported. 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, deferred constraints, recursive or generic 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, while variable-dependent face merges and ambiguous call-result propagation remain unsupported; function compatibility involving nested `@` and variable-dependent joins remain unsupported except for equal types. 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
61−The 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 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. Nested `$^`, including `$^` in collection arguments, is rejected until its source branches can be checked; other nested ordered maps, general source-level disjointness and complete integration with the checker remain unfinished. `+golden-types-imports` can consume fixed-aura atoms and unfaced cells from caller-supplied reader results for declared `/-` imports; `+golden-types-with-marks` accepts those same shapes from declared mark imports in a separate list. 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/clay-fixtures` also passes Clay-built `/sur` molds and mark samples through the Clay-built importer and partial checker.
61+The 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 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. A single nested `$^` in a record is checked when its branches and sibling fields use only aura atom molds such as `@ud` and records built from them; both source branches are re-evaluated, unchanged siblings are verified and overlapping cases are rejected. Other nested `$^`, including `$^` in collection arguments, is rejected; other nested ordered maps, general source-level disjointness and complete integration with the checker remain unfinished. `+golden-types-imports` can consume fixed-aura atoms and unfaced cells from caller-supplied reader results for declared `/-` imports; `+golden-types-with-marks` accepts those same shapes from declared mark imports in a separate list. 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/clay-fixtures` also passes Clay-built `/sur` molds and mark samples through the Clay-built importer and partial checker.
62
62
63Callers that have a `/sur` core and a name can use `+read-named`: it checks for a locally declared arm before asking Hoon to evaluate the mold, and reports evaluation failures with the final Hoon trace line. `+read-mold-in` remains available when the caller already has the selected type. The checker currently treats a failed import as unsupported rather than rendering the importer's error.
63Callers that have a `/sur` core and a name can use `+read-named`: it checks for a locally declared arm before asking Hoon to evaluate the mold, and reports evaluation failures with the final Hoon trace line. `+read-mold-in` remains available when the caller already has the selected type. The checker currently treats a failed import as unsupported rather than rendering the importer's error.
64
64
docs/status.md+7−6
@@ -19,7 +19,7 @@ On 2026-10-30, @iko decided that Jibb drops `$?`, so a `+$` takes a union's case
19
19
20## Milestone 2: in progress
20## Milestone 2: in progress
21
21
22−The repository spec records the subsequent type-system and prelude decisions; those changes also need synchronization to the Claude document. An initial inference fragment and a standalone Hoon type reader are being tested. The fragment explicitly reports that it does not check a module; partial bridges pass selected Hoon atoms and unfaced cells from `/sur` molds and marks into inference. The reader handles mark samples, recursive molds whose origins can be verified through Ford imports, nested collections, direct ordered maps, certain ordered-map fields, and direct `$^` unions whose cases can be proved disjoint. Ambiguous recursive origins fail closed; nested `$^`, other nested ordered maps, general union disjointness and complete import integration remain unfinished. The partial checker resolves a subset of ordinary library imports in dependency order using supplied Jibb sources and the current prelude names, and detects missing sources and cycles. It does not yet check API or kind semantics, and the prelude inventory is incomplete. The inference fragment supports unrestricted `@`, selected one-way widenings including aura-family ancestors, generalized atom constraints arising from explicit capitals or bare sample binders, acyclic local value definitions with captures, and simple acyclic local mold aliases. Unfixed decimal literals default to `@ud` in gate-free inferred types; recursive local groups, more complex local molds, other constraint cases and defaulting inside gate types still need work. Collection recognition checks the originating core and fails closed on shadows or unsupported Ford subject shapes; its golden fixtures include three real Tlon files. The prelude currently has only a few functions, and [prelude-inventory.md](prelude-inventory.md) is a source audit, not the complete inventory or signatures. The milestone remains unfinished.
22+The repository spec records the subsequent type-system and prelude decisions; those changes also need synchronization to the Claude document. An initial inference fragment and a standalone Hoon type reader are being tested. The fragment explicitly reports that it does not check a module; partial bridges pass selected Hoon atoms and unfaced cells from `/sur` molds and marks into inference. The reader handles mark samples, recursive molds whose origins can be verified through Ford imports, nested collections, direct ordered maps, certain ordered-map fields, and direct `$^` unions whose cases can be proved disjoint. Ambiguous recursive origins fail closed; one nested `$^` in a static record of aura molds is checked, while other nested `$^`, nested ordered maps, general union disjointness and complete import integration remain unfinished. The partial checker resolves a subset of ordinary library imports in dependency order using supplied Jibb sources and the current prelude names, and detects missing sources and cycles. It does not yet check API or kind semantics, and the prelude inventory is incomplete. The inference fragment supports unrestricted `@`, selected one-way widenings including aura-family ancestors, generalized atom constraints arising from explicit capitals or bare sample binders, acyclic local value definitions with captures, simple acyclic local mold aliases, and selected faced record casts and field reads. Variable-dependent face merges remain unsupported. Unfixed decimal literals default to `@ud` in gate-free inferred types; recursive local groups, more complex local molds, other constraint cases and defaulting inside gate types still need work. Collection recognition checks the originating core and fails closed on shadows or unsupported Ford subject shapes; its golden fixtures include three real Tlon files. The prelude currently has only a few functions, and [prelude-inventory.md](prelude-inventory.md) is a source audit, not the complete inventory or signatures. The milestone remains unfinished.
23
23
24## Milestone 1: parser and mark
24## Milestone 1: parser and mark
25
25
@@ -37,8 +37,8 @@ What the plan asks for, and where it is:
37
37
38Besides the plan's list:
38Besides the plan's list:
39
39
40−- 435 golden cases: 219 that parse and 216 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.
40+- 441 golden cases: 225 that parse and 216 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.
41−- The 435-case corpus passed under `urbit eval` in 25.7 s. The fake ship passed all 440 tests, including the importer, importer/checker and mark/checker bridges, module scope and unification checks, with 20.3 s for sync and 27.3 s for tests. The importer golden compares 90 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.
41+- The 441-case corpus passed under `urbit eval` in 25.8 s. The fake ship passed all 446 tests, including the importer, importer/checker and mark/checker bridges, module scope and unification checks, with 21.5 s for sync and 28.5 s for tests. The importer golden compares 99 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.
42- `tools/testdata/selftest` (22 checks) and `tools/testdata/ship-selftest` test the tools themselves.
42- `tools/testdata/selftest` (22 checks) and `tools/testdata/ship-selftest` test the tools themselves.
43- 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.
43- 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.
44- 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).
44- 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).
@@ -64,14 +64,15 @@ Besides the plan's list:
64| 2d5deb2 | 2026-10-30 | Default gate-free decimal types, validate named Hoon mold lookup, and isolate fixture failures |
64| 2d5deb2 | 2026-10-30 | Default gate-free decimal types, validate named Hoon mold lookup, and isolate fixture failures |
65| 1b7dbae | 2026-10-30 | Infer acyclic local definitions and parse case-local Jibb module fixtures |
65| 1b7dbae | 2026-10-30 | Infer acyclic local definitions and parse case-local Jibb module fixtures |
66| 8b9c9ac | 2026-10-30 | Preserve recursive import origins, infer simple local molds, and supply Jibb module sources to the partial checker |
66| 8b9c9ac | 2026-10-30 | Preserve recursive import origins, infer simple local molds, and supply Jibb module sources to the partial checker |
67−| This change | 2026-10-30 | Infer supported library import graphs and guard nested Hoon `$^` in collections |
67+| 529736a | 2026-10-30 | Infer supported library import graphs and guard nested Hoon `$^` in collections |
68+| This change | 2026-10-30 | Infer selected record faces and check nested `$^` in static Hoon records |
68
69
69## Checking it
70## Checking it
70
71
71On a machine set up as [development.md](development.md) says:
72On a machine set up as [development.md](development.md) says:
72
73
73```
74```
74−tools/golden # 435 cases under urbit eval
75+tools/golden # 441 cases under urbit eval
75tools/importer-test # the Hoon importer fixture projection
76tools/importer-test # the Hoon importer fixture projection
76tools/type-import-test # the importer/checker bridge fixture
77tools/type-import-test # the importer/checker bridge fixture
77tools/type-mark-test # the mark/checker bridge fixture
78tools/type-mark-test # the mark/checker bridge fixture
@@ -81,7 +82,7 @@ tools/testdata/selftest # the tools themselves
81tools/doc-blocks docs/spec # the doc's examples are golden cases
82tools/doc-blocks docs/spec # the doc's examples are golden cases
82tools/ship start
83tools/ship start
83tools/ship gen-tests --check # tests/lib/jibb.hoon is up to date
84tools/ship gen-tests --check # tests/lib/jibb.hoon is up to date
84−tools/ship test # the same 435 cases as -test arms on the ship
85+tools/ship test # the same 441 cases as -test arms on the ship
85tools/testdata/ship-selftest
86tools/testdata/ship-selftest
86tools/ship check-commit # |commit stores .jibb files
87tools/ship check-commit # |commit stores .jibb files
87tools/clay-fixtures # example /sur files and marks build through Clay
88tools/clay-fixtures # example /sur files and marks build through Clay
jibb-dev/lib/jibb-import.hoon+102−3
@@ -11,8 +11,9 @@
11:: a repeated named hold becomes a module-qualified reference.
11:: a repeated named hold becomes a module-qualified reference.
12::
12::
13:: A direct $^ is read from its original branches and accepted only when
13:: A direct $^ is read from its original branches and accepted only when
14−:: their imported shapes prove disjoint. Nested $^ and some valid but
14+:: their imported shapes prove disjoint. A single nested $^ in a
15+:: static record is checked by splitting and reassembling its branches;
15−:: unprovably disjoint cases remain unsupported. Source-level overlap in
16+:: other nested forms and unprovably disjoint cases remain unsupported. Source-level overlap in
16:: other unions, general nested ordered maps, broader Ford subject
17:: other unions, general nested ordered maps, broader Ford subject
17:: shapes, ambiguous recursive origins and full error locations still
18:: shapes, ambiguous recursive origins and full error locations still
18:: need work. A nested ordered map is recovered only when its key and
19:: need work. A nested ordered map is recovered only when its key and
@@ -428,6 +429,77 @@
428 [%| *] ~
429 [%| *] ~
429 ==
430 ==
430::
431::
432+:: A static branch contains only literal atom molds and record cells.
433+++ fixed-cell-mold
434+ |= h=hoon
435+ ^- ?
436+ ?^ -.h &($(h -.h) $(h +.h))
437+ ?+ h |
438+ [%note *] $(h q.h)
439+ [%ktts *] $(h q.h)
440+ [%ktls *] ?=([%sand *] p.h)
441+ ==
442+::
443+:: Return two source records with a single $^ replaced by each branch.
444+++ split-cell-record
445+ |= [h=hoon axis=@ud]
446+ ^- (unit [one=hoon two=hoon])
447+ ?^ -.h
448+ =/ left $(h -.h, axis (mul 2 axis))
449+ =/ right $(h +.h, axis (add 1 (mul 2 axis)))
450+ ?^ left
451+ ?^ right ~
452+ ?. (fixed-cell-mold +.h) ~
453+ [~ [[one.u.left +.h] [two.u.left +.h]]]
454+ ?~ right ~
455+ ?. (fixed-cell-mold -.h) ~
456+ [~ [[-.h one.u.right] [-.h two.u.right]]]
457+ ?+ h ~
458+ [%note *]
459+ =/ out $(h q.h)
460+ ?~ out ~
461+ [~ [h(q one.u.out) h(q two.u.out)]]
462+ [%ktts *]
463+ =/ out $(h q.h)
464+ ?~ out ~
465+ [~ [h(q one.u.out) h(q two.u.out)]]
466+ [%wtcl *]
467+ ?. =(p.h [%dtwt [%$ (mul 2 axis)]]) ~
468+ ?. &((fixed-cell-mold q.h) (fixed-cell-mold r.h)) ~
469+ [~ [q.h r.h]]
470+ ==
471+::
472+:: Reassemble a split source record. Non-union fields must have remained
473+:: unchanged; the replaced field must have provably disjoint branches.
474+++ merge-cell-record
475+ |= [h=hoon axis=@ud a=imported b=imported]
476+ ^- (each imported @t)
477+ ?^ -.h
478+ ?. &(?=([%cell *] a) ?=([%cell *] b))
479+ [%| 'a nested Hoon $^ union needs a source-level disjointness check']
480+ =/ left $(h -.h, axis (mul 2 axis), a head.a, b head.b)
481+ ?. ?=([%& *] left) left
482+ =/ right $(h +.h, axis (add 1 (mul 2 axis)), a tail.a, b tail.b)
483+ ?. ?=([%& *] right) right
484+ [%& [%cell p.left p.right]]
485+ ?+ h
486+ ?: =(a b) [%& a]
487+ [%| 'a nested Hoon $^ union needs a source-level disjointness check']
488+ [%note *] $(h q.h)
489+ [%ktts *]
490+ ?. &(?=([%face *] a) ?=([%face *] b))
491+ [%| 'a nested Hoon $^ union needs a source-level disjointness check']
492+ ?. &(=(p.h name.a) =(p.h name.b))
493+ [%| 'a nested Hoon $^ union needs a source-level disjointness check']
494+ =/ child $(h q.h, a body.a, b body.b)
495+ ?. ?=([%& *] child) child
496+ [%& [%face name.a p.child]]
497+ [%wtcl *]
498+ ?. =(p.h [%dtwt [%$ (mul 2 axis)]])
499+ [%| 'a nested Hoon $^ union needs a source-level disjointness check']
500+ ?. (disjoint a b) [%| 'a Hoon $^ union has overlapping cases']
501+ [%& [%fork (sort ~[a b] |=(pair=[imported imported] (dor -.pair +.pair)))]]
502+ ==
431++ disjoint
503++ disjoint
432 |= [a=imported b=imported]
504 |= [a=imported b=imported]
433 ^- ?
505 ^- ?
@@ -721,7 +793,25 @@
721 [%fork (sort ~[first second] |=(pair=[imported imported] (dor -.pair +.pair)))]
793 [%fork (sort ~[first second] |=(pair=[imported imported] (dor -.pair +.pair)))]
722 [%bad 'a Hoon $^ union has overlapping cases']
794 [%bad 'a Hoon $^ union has overlapping cases']
723 ?: (has-cell-union q.typ)
795 ?: (has-cell-union q.typ)
796+ ?. ?=([%tsls [%note * *] *] q.typ)
797+ [%bad 'a Hoon $^ union needs a source-level disjointness check']
798+ =/ original=hoon q.typ
799+ ?> ?=([%tsls [%note * *] *] original)
800+ =/ body=hoon q.p.original
801+ =/ split (split-cell-record body 6)
802+ ?~ split [%bad 'a Hoon $^ union needs a source-level disjointness check']
803+ =/ try=(each [type type] tang)
804+ (mule |.([(~(play ut p.typ) original(q.p one.u.split)) (~(play ut p.typ) original(q.p two.u.split))]))
724− [%bad 'a Hoon $^ union needs a source-level disjointness check']
805+ ?. ?=([%& *] try) [%bad 'a Hoon $^ union needs a source-level disjointness check']
806+ =/ first $(typ -.p.try, seen [[typ nm] seen])
807+ =/ second $(typ +.p.try, seen [[typ nm] seen])
808+ =/ err (first-bads ~[first second])
809+ ?^ err [%bad u.err]
810+ =/ combined (merge-cell-record body 6 first second)
811+ ?- combined
812+ [%& *] p.combined
813+ [%| *] [%bad p.combined]
814+ ==
725 =/ alias (hold-alias q.typ)
815 =/ alias (hold-alias q.typ)
726 =/ hidden (has-hidden-alias q.typ)
816 =/ hidden (has-hidden-alias q.typ)
727 =/ body $(typ ~(repo ut typ), seen [[typ nm] seen])
817 =/ body $(typ ~(repo ut typ), seen [[typ nm] seen])
@@ -1032,6 +1122,15 @@
1032 (crip "set-direct-invalid-cell: {(show-result (sample %set-direct-invalid-cell))}")
1122 (crip "set-direct-invalid-cell: {(show-result (sample %set-direct-invalid-cell))}")
1033 (crip "map-key-invalid-cell: {(show-result (sample %map-key-invalid-cell))}")
1123 (crip "map-key-invalid-cell: {(show-result (sample %map-key-invalid-cell))}")
1034 (crip "nested-atom-cell: {(show-result (sample %nested-atom-cell))}")
1124 (crip "nested-atom-cell: {(show-result (sample %nested-atom-cell))}")
1125+ (crip "nested-first-cell: {(show-result (sample %nested-first-cell))}")
1126+ (crip "nested-alias-cell: {(show-result (sample %nested-alias-cell))}")
1127+ (crip "nested-multiple-cell: {(show-result (sample %nested-multiple-cell))}")
1128+ (crip "nested-named-sibling: {(show-result (sample %nested-named-sibling))}")
1129+ (crip "nested-list-sibling: {(show-result (sample %nested-list-sibling))}")
1130+ (crip "nested-validated-sibling: {(show-result (sample %nested-validated-sibling))}")
1131+ (crip "nested-validated-branch: {(show-result (sample %nested-validated-branch))}")
1132+ (crip "nested-named-branch: {(show-result (sample %nested-named-branch))}")
1133+ (crip "nested-ford-cell: {(show-result (read-named %outer %nested trans))}")
1035 (crip "nested-valid-cell: {(show-result (sample %nested-valid-cell))}")
1134 (crip "nested-valid-cell: {(show-result (sample %nested-valid-cell))}")
1036 (crip "nested-invalid-cell: {(show-result (sample %nested-invalid-cell))}")
1135 (crip "nested-invalid-cell: {(show-result (sample %nested-invalid-cell))}")
1037 (crip "valid-cell: {(show-result (sample %valid-cell))}")
1136 (crip "valid-cell: {(show-result (sample %valid-cell))}")
jibb-dev/lib/jibb.hoon+180−12
@@ -4606,6 +4606,7 @@
4606 [%atom aura=@ta]
4606 [%atom aura=@ta]
4607 [%any-atom ~]
4607 [%any-atom ~]
4608 [%flag ~]
4608 [%flag ~]
4609+ [%face name=term body=itype]
4609 [%fn sample=itype product=itype]
4610 [%fn sample=itype product=itype]
4610 [%cell hed=itype tal=itype]
4611 [%cell hed=itype tal=itype]
4611 ==
4612 ==
@@ -4648,6 +4649,7 @@
4648 %atom |
4649 %atom |
4649 %any-atom |
4650 %any-atom |
4650 %flag |
4651 %flag |
4652+ %face $(t body.t)
4651 %fn |($(t sample.t) $(t product.t))
4653 %fn |($(t sample.t) $(t product.t))
4652 %cell |($(t hed.t) $(t tal.t))
4654 %cell |($(t hed.t) $(t tal.t))
4653 ==
4655 ==
@@ -4687,6 +4689,9 @@
4687 ?. |(?=(%atom -.a) ?=(%any-atom -.a) ?=(%flag -.a)) ~
4689 ?. |(?=(%atom -.a) ?=(%any-atom -.a) ?=(%flag -.a)) ~
4688 `[[id.b a] sub]
4690 `[[id.b a] sub]
4689 ?: &(?=(%atom -.a) ?=(%atom -.b)) ~
4691 ?: &(?=(%atom -.a) ?=(%atom -.b)) ~
4692+ ?: &(?=(%face -.a) ?=(%face -.b))
4693+ ?. =(name.a name.b) ~
4694+ $(a body.a, b body.b)
4690 ?: &(?=(%fn -.a) ?=(%fn -.b))
4695 ?: &(?=(%fn -.a) ?=(%fn -.b))
4691 =/ first=(unit isub) $(a sample.a, b sample.b)
4696 =/ first=(unit isub) $(a sample.a, b sample.b)
4692 ?~ first ~
4697 ?~ first ~
@@ -4714,6 +4719,7 @@
4714 %atom |
4719 %atom |
4715 %any-atom &
4720 %any-atom &
4716 %flag |
4721 %flag |
4722+ %face $(t body.t)
4717 %fn |($(t sample.t) $(t product.t))
4723 %fn |($(t sample.t) $(t product.t))
4718 %cell |($(t hed.t) $(t tal.t))
4724 %cell |($(t hed.t) $(t tal.t))
4719 ==
4725 ==
@@ -4744,6 +4750,9 @@
4744 ?: &(?=(%atom -.a) ?=(%atom -.b))
4750 ?: &(?=(%atom -.a) ?=(%atom -.b))
4745 ?. !=(aura.a aura.b) |
4751 ?. !=(aura.a aura.b) |
4746 |((aura-prefix aura.a aura.b) (aura-prefix aura.b aura.a))
4752 |((aura-prefix aura.a aura.b) (aura-prefix aura.b aura.a))
4753+ ?: &(?=(%face -.a) ?=(%face -.b))
4754+ ?. =(name.a name.b) |
4755+ $(a body.a, b body.b)
4747 ?: &(?=(%cell -.a) ?=(%cell -.b))
4756 ?: &(?=(%cell -.a) ?=(%cell -.b))
4748 |($(a hed.a, b hed.b) $(a tal.a, b tal.b))
4757 |($(a hed.a, b hed.b) $(a tal.a, b tal.b))
4749 ?: &(?=(%fn -.a) ?=(%fn -.b))
4758 ?: &(?=(%fn -.a) ?=(%fn -.b))
@@ -4764,6 +4773,7 @@
4764 %atom &
4773 %atom &
4765 %any-atom &
4774 %any-atom &
4766 %flag &
4775 %flag &
4776+ %face $(typ body.typ)
4767 %fn |($(typ sample.typ) $(typ product.typ))
4777 %fn |($(typ sample.typ) $(typ product.typ))
4768 %cell |($(typ hed.typ) $(typ tal.typ))
4778 %cell |($(typ hed.typ) $(typ tal.typ))
4769 ==
4779 ==
@@ -4781,6 +4791,63 @@
4781 ?: &(?=(%any-atom -.b) |(?=(%atom -.a) ?=(%flag -.a))) `b
4791 ?: &(?=(%any-atom -.b) |(?=(%atom -.a) ?=(%flag -.a))) `b
4782 ~
4792 ~
4783::
4793::
4794+:: Unifying an already-bound tuple with a faced position would need to
4795+:: update the bound type. Until substitutions can retain that information,
4796+:: variable-dependent face merges stay unresolved.
4797+::
4798+++ itype-has-face
4799+ |= [t=itype sub=isub]
4800+ ^- ?
4801+ =. t (itype-walk t sub)
4802+ ?- -.t
4803+ %face &
4804+ %cell |($(t hed.t) $(t tal.t))
4805+ %fn |($(t sample.t) $(t product.t))
4806+ * |
4807+ ==
4808+::
4809+++ itype-face-asym
4810+ |= [a=itype b=itype sub=isub]
4811+ ^- ?
4812+ =. a (itype-walk a sub)
4813+ =. b (itype-walk b sub)
4814+ ?: &(?=(%face -.a) ?=(%face -.b)) $(a body.a, b body.b)
4815+ ?: ?=(%face -.a) !|(?=(%var -.b) ?=(%avar -.b) ?=(%nvar -.b))
4816+ ?: ?=(%face -.b) !|(?=(%var -.a) ?=(%avar -.a) ?=(%nvar -.a))
4817+ ?: &(?=(%cell -.a) ?=(%cell -.b)) |($(a hed.a, b hed.b) $(a tal.a, b tal.b))
4818+ ?: &(?=(%fn -.a) ?=(%fn -.b)) |($(a sample.a, b sample.b) $(a product.a, b product.b))
4819+ |
4820+::
4821+:: A successful cast keeps any explicit faces from either side while
4822+:: retaining the target's aura choices. Both faces have already matched.
4823+::
4824+++ itype-merge-faces
4825+ |= [actual=itype expected=itype sub=isub]
4826+ ^- itype
4827+ =. actual (itype-walk actual sub)
4828+ =. expected (itype-walk expected sub)
4829+ ?: &(?=(%face -.actual) ?=(%face -.expected))
4830+ [%face name.expected $(actual body.actual, expected body.expected)]
4831+ ?: ?=(%face -.actual)
4832+ [%face name.actual $(actual body.actual)]
4833+ ?: ?=(%face -.expected)
4834+ [%face name.expected $(expected body.expected)]
4835+ ?: &(?=(%cell -.actual) ?=(%cell -.expected))
4836+ [%cell $(actual hed.actual, expected hed.expected) $(actual tal.actual, expected tal.expected)]
4837+ expected
4838+::
4839+++ itype-output-may-be-cell
4840+ |= [t=itype sub=isub]
4841+ ^- ?
4842+ =. t (itype-walk t sub)
4843+ ?- -.t
4844+ %var &
4845+ %cell &
4846+ %face $(t body.t)
4847+ %fn |($(t sample.t) $(t product.t))
4848+ * |
4849+ ==
4850+::
4784++ itype-fit
4851++ itype-fit
4785 |= [actual=itype expected=itype sub=isub next=@ud]
4852 |= [actual=itype expected=itype sub=isub next=@ud]
4786 ^- ifit
4853 ^- ifit
@@ -4789,6 +4856,7 @@
4789 =. actual (itype-walk actual sub)
4856 =. actual (itype-walk actual sub)
4790 =. expected (itype-walk expected sub)
4857 =. expected (itype-walk expected sub)
4791 ?: =(actual expected) [%ok sub next]
4858 ?: =(actual expected) [%ok sub next]
4859+ ?: &(uncertain (itype-face-asym actual expected sub)) [%unknown ~]
4792 ?: ?=(%any-atom -.expected)
4860 ?: ?=(%any-atom -.expected)
4793 ?: |(?=(%atom -.actual) ?=(%avar -.actual) ?=(%nvar -.actual) ?=(%flag -.actual)) [%ok sub next]
4861 ?: |(?=(%atom -.actual) ?=(%avar -.actual) ?=(%nvar -.actual) ?=(%flag -.actual)) [%ok sub next]
4794 ?: ?=(%var -.actual)
4862 ?: ?=(%var -.actual)
@@ -4819,6 +4887,12 @@
4819 ?: (itype-family-related actual expected sub) [%unknown ~]
4887 ?: (itype-family-related actual expected sub) [%unknown ~]
4820 [%bad ~]
4888 [%bad ~]
4821 [%ok u.unified next]
4889 [%ok u.unified next]
4890+ ?: &(?=(%face -.actual) ?=(%face -.expected))
4891+ ?. =(name.actual name.expected) [%bad ~]
4892+ $(actual body.actual, expected body.expected)
4893+ ?: ?=(%face -.actual) $(actual body.actual)
4894+ ?: ?=(%face -.expected) $(expected body.expected)
4895+ ?: (itype-face-asym actual expected sub) [%unknown ~]
4822 ?: |((itype-has-any-atom actual sub) (itype-has-any-atom expected sub))
4896 ?: |((itype-has-any-atom actual sub) (itype-has-any-atom expected sub))
4823 [%unknown ~]
4897 [%unknown ~]
4824 =/ unified=(unit isub) (itype-unify actual expected sub)
4898 =/ unified=(unit isub) (itype-unify actual expected sub)
@@ -4888,6 +4962,8 @@
4888 |= [t=itype sub=isub]
4962 |= [t=itype sub=isub]
4889 ^- itype
4963 ^- itype
4890 =. t (itype-walk t sub)
4964 =. t (itype-walk t sub)
4965+ ?: ?=(%face -.t)
4966+ [%face name.t $(t body.t)]
4891 ?: ?=(%fn -.t)
4967 ?: ?=(%fn -.t)
4892 [%fn $(t sample.t) $(t product.t)]
4968 [%fn $(t sample.t) $(t product.t)]
4893 ?: ?=(%cell -.t)
4969 ?: ?=(%cell -.t)
@@ -4905,6 +4981,7 @@
4905 ?- -.t
4981 ?- -.t
4906 %fn &
4982 %fn &
4907 %cell |($(t hed.t) $(t tal.t))
4983 %cell |($(t hed.t) $(t tal.t))
4984+ %face $(t body.t)
4908 %var |
4985 %var |
4909 %avar |
4986 %avar |
4910 %nvar |
4987 %nvar |
@@ -4919,6 +4996,7 @@
4919 ?: (itype-has-gate t) t
4996 ?: (itype-has-gate t) t
4920 ?- -.t
4997 ?- -.t
4921 %nvar [%atom %ud]
4998 %nvar [%atom %ud]
4999+ %face [%face name.t $(t body.t)]
4922 %cell [%cell $(t hed.t) $(t tal.t)]
5000 %cell [%cell $(t hed.t) $(t tal.t)]
4923 * t
5001 * t
4924 ==
5002 ==
@@ -4933,6 +5011,7 @@
4933 %atom ~
5011 %atom ~
4934 %any-atom ~
5012 %any-atom ~
4935 %flag ~
5013 %flag ~
5014+ %face $(t body.t)
4936 %fn (weld $(t sample.t) $(t product.t))
5015 %fn (weld $(t sample.t) $(t product.t))
4937 %cell (weld $(t hed.t) $(t tal.t))
5016 %cell (weld $(t hed.t) $(t tal.t))
4938 ==
5017 ==
@@ -4965,6 +5044,7 @@
4965 %atom t
5044 %atom t
4966 %any-atom t
5045 %any-atom t
4967 %flag t
5046 %flag t
5047+ %face [%face name.t $(t body.t)]
4968 %fn [%fn $(t sample.t) $(t product.t)]
5048 %fn [%fn $(t sample.t) $(t product.t)]
4969 %cell [%cell $(t hed.t) $(t tal.t)]
5049 %cell [%cell $(t hed.t) $(t tal.t)]
4970 ==
5050 ==
@@ -4982,6 +5062,7 @@
4982 %atom |
5062 %atom |
4983 %any-atom |
5063 %any-atom |
4984 %flag |
5064 %flag |
5065+ %face $(t body.t)
4985 %fn |($(t sample.t) $(t product.t))
5066 %fn |($(t sample.t) $(t product.t))
4986 %cell |($(t hed.t) $(t tal.t))
5067 %cell |($(t hed.t) $(t tal.t))
4987 ==
5068 ==
@@ -5176,13 +5257,25 @@
5176 |= [fields=(list field) state=istate]
5257 |= [fields=(list field) state=istate]
5177 ^- (unit [typ=itype state=istate])
5258 ^- (unit [typ=itype state=istate])
5178 ?~ fields ~
5259 ?~ fields ~
5260+ =/ field-shape=shape
5261+ ?- -.i.fields
5179− ?. ?=(%bare -.i.fields) ~
5262+ %bare shape.i.fields
5263+ %face shape.i.fields
5264+ %pun [%ref at.i.fields ~[name.i.fields]]
5265+ ==
5180− =/ head=(unit [typ=itype state=istate]) (infer-simple-shape shape.i.fields state)
5266+ =/ head=(unit [typ=itype state=istate]) (infer-simple-shape field-shape state)
5181 ?~ head ~
5267 ?~ head ~
5268+ =/ t=itype typ.u.head
5269+ =. t
5270+ ?- -.i.fields
5271+ %bare t
5272+ %face [%face name.i.fields t]
5273+ %pun [%face name.i.fields t]
5274+ ==
5182− ?~ t.fields head
5275+ ?~ t.fields `[t state.u.head]
5183 =/ tail=(unit [typ=itype state=istate]) $(fields t.fields, state state.u.head)
5276 =/ tail=(unit [typ=itype state=istate]) $(fields t.fields, state state.u.head)
5184 ?~ tail ~
5277 ?~ tail ~
5185− `[[%cell typ.u.head typ.u.tail] state.u.tail]
5278+ `[[%cell t typ.u.tail] state.u.tail]
5186::
5279::
5187++ infer-sample
5280++ infer-sample
5188 |= [s=sample env=ienv state=istate]
5281 |= [s=sample env=ienv state=istate]
@@ -5203,9 +5296,34 @@
5203 =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
5296 =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
5204 ?~ t [%| "sample mold is not supported by partial inference"]
5297 ?~ t [%| "sample mold is not supported by partial inference"]
5205 [%& typ.u.t env state.u.t]
5298 [%& typ.u.t env state.u.t]
5206− * [%| "sample is not supported by partial inference"]
5299+ %pun
5300+ $(s [%face at.s name.s [%ref at.s ~[name.s]]])
5301+ %cell
5302+ (infer-sample-items items.s env state)
5207 ==
5303 ==
5208::
5304::
5305+:: Cell-sample binders are faces on their positions; at the top of a
5306+:: sample a binder only supplies a name for the whole sample.
5307+::
5308+++ infer-sample-items
5309+ |= [items=(list sample) env=ienv state=istate]
5310+ ^- isample-result
5311+ ?~ items [%| "empty sample is not supported by partial inference"]
5312+ =/ head=isample-result (infer-sample i.items env state)
5313+ ?: ?=(%| -.head) head
5314+ =/ ht=itype typ.p.head
5315+ =. ht
5316+ ?- -.i.items
5317+ %bind [%face name.i.items ht]
5318+ %face [%face name.i.items ht]
5319+ %pun [%face name.i.items ht]
5320+ * ht
5321+ ==
5322+ ?~ t.items [%& ht env.p.head state.p.head]
5323+ =/ tail=isample-result $(items t.items, env env.p.head, state state.p.head)
5324+ ?: ?=(%| -.tail) tail
5325+ [%& [%cell ht typ.p.tail] env.p.tail state.p.tail]
5326+::
5209:: Local definitions generalize only variables outside their enclosing
5327:: Local definitions generalize only variables outside their enclosing
5210:: environment and explicit-capital scope. Unresolved groups stay
5328:: environment and explicit-capital scope. Unresolved groups stay
5211:: unsupported: this fragment does not infer recursive definitions.
5329:: unsupported: this fragment does not infer recursive definitions.
@@ -5300,6 +5418,38 @@
5300 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
5418 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
5301 $(ds t.ds, env [[name.d [typ vars]] env], state state.p.inferred, progressed &)
5419 $(ds t.ds, env [[name.d [typ vars]] env], state state.p.inferred, progressed &)
5302::
5420::
5421+:: Read only fields of a known record. Unresolved field constraints and
5422+:: ambiguous repeated faces are outside this fragment.
5423+::
5424+++ record-fields-named
5425+ |= [name=term t=itype sub=isub]
5426+ ^- (list itype)
5427+ =. t (itype-walk t sub)
5428+ ?: ?=(%face -.t)
5429+ ?:(=(name name.t) ~[body.t] ~)
5430+ ?. ?=(%cell -.t) ~
5431+ =/ first=(list itype) ~
5432+ =/ head=itype (itype-walk hed.t sub)
5433+ =? first ?=(%face -.head) ?:(=(name name.head) ~[body.head] ~)
5434+ (weld first $(t tal.t))
5435+::
5436+++ infer-field-wing
5437+ |= [names=(list term) env=ienv state=istate]
5438+ ^- iresult
5439+ =/ reverse=(list term) (flop names)
5440+ ?~ reverse [%| ["empty wing" ~]]
5441+ =/ scheme=(unit ischeme) (ienv-lookup i.reverse env)
5442+ ?~ scheme [%| ["field access is not supported by partial inference" ~]]
5443+ =/ inst=[typ=itype state=istate] (instantiate-scheme u.scheme state)
5444+ =/ fields=(list term) t.reverse
5445+ =/ typ=itype typ.inst
5446+ |-
5447+ ?~ fields [%& typ state.inst]
5448+ =/ found=(list itype) (record-fields-named i.fields typ sub.state.inst)
5449+ ?~ found [%| ["field is not available to partial inference" ~]]
5450+ ?^ t.found [%| ["field name is ambiguous in partial inference" ~]]
5451+ $(fields t.fields, typ i.found)
5452+::
5303++ infer-fragment
5453++ infer-fragment
5304 |= [e=expr env=ienv state=istate]
5454 |= [e=expr env=ienv state=istate]
5305 ^- iresult
5455 ^- iresult
@@ -5323,9 +5473,9 @@
5323 %wing
5473 %wing
5324 ?~ names.e [%| ["empty wing" ~]]
5474 ?~ names.e [%| ["empty wing" ~]]
5325 ?^ t.names.e
5475 ?^ t.names.e
5326− ?^ t.t.names.e [%| ["field access is not supported by partial inference" ~]]
5476+ ?^ t.t.names.e (infer-field-wing names.e env state)
5327 =/ iface=(unit ifile) (find-jibb-interface i.t.names.e jimports.state)
5477 =/ iface=(unit ifile) (find-jibb-interface i.t.names.e jimports.state)
5328− ?~ iface [%| ["field access is not supported by partial inference" ~]]
5478+ ?~ iface (infer-field-wing names.e env state)
5329 =/ member=(unit ischeme) (ienv-lookup i.names.e values.u.iface)
5479 =/ member=(unit ischeme) (ienv-lookup i.names.e values.u.iface)
5330 ?~ member [%| ["module member is not available to partial inference" ~]]
5480 ?~ member [%| ["module member is not available to partial inference" ~]]
5331 =/ instance=[typ=itype state=istate] (instantiate-scheme u.member state)
5481 =/ instance=[typ=itype state=istate] (instantiate-scheme u.member state)
@@ -5386,6 +5536,8 @@
5386 ?~ joined
5536 ?~ joined
5387 =/ common=(unit itype) (itype-concrete-join typ.p.left typ.p.right sub.state.p.right)
5537 =/ common=(unit itype) (itype-concrete-join typ.p.left typ.p.right sub.state.p.right)
5388 ?^ common [%& u.common state.p.right]
5538 ?^ common [%& u.common state.p.right]
5539+ ?: |((itype-has-face typ.p.left sub.state.p.right) (itype-has-face typ.p.right sub.state.p.right))
5540+ [%| ["record branch matching is not supported by partial inference" ~]]
5389 ?: |((itype-has-any-atom typ.p.left sub.state.p.right) (itype-has-any-atom typ.p.right sub.state.p.right) (itype-family-related typ.p.left typ.p.right sub.state.p.right))
5541 ?: |((itype-has-any-atom typ.p.left sub.state.p.right) (itype-has-any-atom typ.p.right sub.state.p.right) (itype-family-related typ.p.left typ.p.right sub.state.p.right))
5390 [%| ["branch widening is not supported by partial inference" ~]]
5542 [%| ["branch widening is not supported by partial inference" ~]]
5391 [%| ["branch arms have incompatible types" ~[[(span-of val.x) (site-type-note "first arm" typ.p.left sub.state.p.right)] [(span-of val.y) (site-type-note "second arm" typ.p.right sub.state.p.right)]]]]
5543 [%| ["branch arms have incompatible types" ~[[(span-of val.x) (site-type-note "first arm" typ.p.left sub.state.p.right)] [(span-of val.y) (site-type-note "second arm" typ.p.right sub.state.p.right)]]]]
@@ -5399,7 +5551,8 @@
5399 ?: ?=(%unknown -.fit) [%| ["cast constraint is not supported by partial inference" ~]]
5551 ?: ?=(%unknown -.fit) [%| ["cast constraint is not supported by partial inference" ~]]
5400 ?: ?=(%bad -.fit)
5552 ?: ?=(%bad -.fit)
5401 [%| ["cast mold and expression type do not unify" ~[[at.shape.e (site-type-note "cast mold" typ.u.target sub.state.p.value)] [(span-of val.e) (site-type-note "expression" typ.p.value sub.state.p.value)]]]]
5553 [%| ["cast mold and expression type do not unify" ~[[at.shape.e (site-type-note "cast mold" typ.u.target sub.state.p.value)] [(span-of val.e) (site-type-note "expression" typ.p.value sub.state.p.value)]]]]
5554+ =/ merged=itype (itype-merge-faces typ.p.value typ.u.target sub.fit)
5402− [%& typ.u.target state.p.value(sub sub.fit, next next.fit)]
5555+ [%& merged state.p.value(sub sub.fit, next next.fit)]
5403 %crash [%& [%var next.state] state(next +(next.state))]
5556 %crash [%& [%var next.state] state(next +(next.state))]
5404 %gate
5557 %gate
5405 =/ sam=isample-result (infer-sample sample.e env state)
5558 =/ sam=isample-result (infer-sample sample.e env state)
@@ -5427,6 +5580,8 @@
5427 ?: ?=(%unknown -.fit) [%| ["call constraint is not supported by partial inference" ~]]
5580 ?: ?=(%unknown -.fit) [%| ["call constraint is not supported by partial inference" ~]]
5428 ?: ?=(%bad -.fit)
5581 ?: ?=(%bad -.fit)
5429 [%| ["call's sample and argument types do not unify" ~[[(span-of head.e) (site-type-note "called gate" ht sub.st)] [(span-of i.args.e) (site-type-note "argument" typ.p.arg sub.st)]]]]
5582 [%| ["call's sample and argument types do not unify" ~[[(span-of head.e) (site-type-note "called gate" ht sub.st)] [(span-of i.args.e) (site-type-note "argument" typ.p.arg sub.st)]]]]
5583+ ?: &((itype-has-face typ.p.arg sub.fit) (itype-face-asym typ.p.arg sample.ht sub.fit) (itype-output-may-be-cell product.ht sub.fit))
5584+ [%| ["call result face propagation is not supported by partial inference" ~]]
5430 [%& product.ht st(sub sub.fit, next next.fit)]
5585 [%& product.ht st(sub sub.fit, next next.fit)]
5431 =/ result=itype [%var next.st]
5586 =/ result=itype [%var next.st]
5432 =/ uni=(unit isub) (itype-unify ht [%fn typ.p.arg result] sub.st)
5587 =/ uni=(unit isub) (itype-unify ht [%fn typ.p.arg result] sub.st)
@@ -5443,13 +5598,14 @@
5443 |= [items=(list item) env=ienv state=istate]
5598 |= [items=(list item) env=ienv state=istate]
5444 ^- iresult
5599 ^- iresult
5445 ?~ items [%| ["empty cell is not supported by partial inference" ~]]
5600 ?~ items [%| ["empty cell is not supported by partial inference" ~]]
5446− ?^ face.i.items [%| ["record faces are not supported by partial inference" ~]]
5447 =/ head=iresult (infer-fragment val.i.items env state)
5601 =/ head=iresult (infer-fragment val.i.items env state)
5448 ?: ?=(%| -.head) head
5602 ?: ?=(%| -.head) head
5603+ =/ ht=itype typ.p.head
5604+ =. ht ?~(face.i.items ht [%face u.face.i.items ht])
5449− ?~ t.items head
5605+ ?~ t.items [%& ht state.p.head]
5450 =/ tail=iresult $(items t.items, state state.p.head)
5606 =/ tail=iresult $(items t.items, state state.p.head)
5451 ?: ?=(%| -.tail) tail
5607 ?: ?=(%| -.tail) tail
5452− [%& [%cell typ.p.head typ.p.tail] state.p.tail]
5608+ [%& [%cell ht typ.p.tail] state.p.tail]
5453::
5609::
5454:: A single two-binder cell pattern covers every value of a cell type.
5610:: A single two-binder cell pattern covers every value of a cell type.
5455:: No other pattern matrix is implemented here.
5611:: No other pattern matrix is implemented here.
@@ -5474,6 +5630,8 @@
5474 =/ subject=iresult (infer-fragment subject.e env state)
5630 =/ subject=iresult (infer-fragment subject.e env state)
5475 ?: ?=(%| -.subject) subject
5631 ?: ?=(%| -.subject) subject
5476 =/ st=istate state.p.subject
5632 =/ st=istate state.p.subject
5633+ ?: (itype-has-face typ.p.subject sub.st)
5634+ [%| ["record patterns are not supported by partial inference" ~]]
5477 =/ head=itype [%var next.st]
5635 =/ head=itype [%var next.st]
5478 =/ tail=itype [%var +(next.st)]
5636 =/ tail=itype [%var +(next.st)]
5479 =/ sub=(unit isub) (itype-unify typ.p.subject [%cell head tail] sub.st)
5637 =/ sub=(unit isub) (itype-unify typ.p.subject [%cell head tail] sub.st)
@@ -5497,10 +5655,18 @@
5497 %atom "@{(trip aura.t)}"
5655 %atom "@{(trip aura.t)}"
5498 %any-atom "@"
5656 %any-atom "@"
5499 %flag "?"
5657 %flag "?"
5658+ %face "[{(trip name.t)}={$(t body.t)}]"
5500 %fn "$-({$(t sample.t)} {$(t product.t)})"
5659 %fn "$-({$(t sample.t)} {$(t product.t)})"
5501− %cell "[{$(t hed.t)} {$(t tal.t)}]"
5660+ %cell "[{(show-itype-item hed.t sub)} {(show-itype-item tal.t sub)}]"
5502 ==
5661 ==
5503::
5662::
5663+++ show-itype-item
5664+ |= [t=itype sub=isub]
5665+ ^- tape
5666+ =. t (itype-walk t sub)
5667+ ?: ?=(%face -.t) "{(trip name.t)}={(show-itype body.t sub)}"
5668+ (show-itype t sub)
5669+::
5504:: Include the type at a conflicting site where it can be printed.
5670:: Include the type at a conflicting site where it can be printed.
5505:: A lone unresolved variable or decimal variable keeps the neutral label.
5671:: A lone unresolved variable or decimal variable keeps the neutral label.
5506::
5672::
@@ -5514,6 +5680,7 @@
5514 %atom |
5680 %atom |
5515 %any-atom |
5681 %any-atom |
5516 %flag |
5682 %flag |
5683+ %face $(typ body.typ)
5517 %fn |($(typ sample.typ) $(typ product.typ))
5684 %fn |($(typ sample.typ) $(typ product.typ))
5518 %cell |($(typ hed.typ) $(typ tal.typ))
5685 %cell |($(typ hed.typ) $(typ tal.typ))
5519 ==
5686 ==
@@ -5564,6 +5731,7 @@
5564 %atom |
5731 %atom |
5565 %any-atom |
5732 %any-atom |
5566 %flag |
5733 %flag |
5734+ %face $(t body.t)
5567 %fn |($(t sample.t) $(t product.t))
5735 %fn |($(t sample.t) $(t product.t))
5568 %cell |($(t hed.t) $(t tal.t))
5736 %cell |($(t hed.t) $(t tal.t))
5569 ==
5737 ==
my-app/sur/import-fixture.hoon+1
@@ -3,4 +3,5 @@
3|%
3|%
4+$ sample [title=title:blog values=(list @ud)]
4+$ sample [title=title:blog values=(list @ud)]
5+$ recursive chain:blog
5+$ recursive chain:blog
6++$ nested [id=@ud value=$^(@ud [a=@ud b=@t])]
6--
7--
tests/clay-fixtures/ford-nested-union-expected.txtnew file+1
@@ -0,0 +1 @@
1+"[id=@ud value=(union [a=@ud b=@t] @ud)]"
tests/clay-fixtures/ford-nested-union.txtnew file+9
@@ -0,0 +1,9 @@
1+=/ m (strand ,vase)
2+;< =bowl:spider bind:m get-bowl
3+=/ now=@da now.bowl
4+=/ src=vase .^(vase %ca /[(scot %p our.bowl)]/my-app/[(scot %da now)]/sur/import-fixture/hoon)
5+=/ reader=vase .^(vase %ca /[(scot %p our.bowl)]/my-app/[(scot %da now)]/lib/jibb-import/hoon)
6+=/ read-gate=vase (slap reader (ream 'read-named'))
7+=/ got=vase (slym read-gate [%import-fixture %nested -.src])
8+=/ show-gate=vase (slap reader (ream 'show-result'))
9+(pure:m (slym show-gate +.got))
tests/golden/types-record-bound-variable/about.txtnew file+4
@@ -0,0 +1,4 @@
1+source: Grammar, Molds: "Faces are part of the type" and "An unnamed position can unify with a faced position and take its face"; Expressions: "Wing ... also for imports and prelude groups".
2+tests: An inferred variable can acquire field names, while adding faces after it is already bound to a tuple is explicitly unsupported.
3+expect: parses
4+expect-types: a partial inference report
tests/golden/types-record-bound-variable/source.jibbnew file+6
@@ -0,0 +1,6 @@
1+++ id |=(x x)
2+++ constrained |= x ^- [x=@t y=@p] (id x)
3+++ bound-first |= v
4+ ~& ^- [@t @p] v
5+ ^- [x=@t y=@p] v
6+++ sample (id [x="hi" y=~zod])
tests/golden/types-record-bound-variable/tokens.txtnew file+65
@@ -0,0 +1,65 @@
1+1:1 glyph ++
2+1:4 name id
3+1:7 glyph |=(
4+1:10 tight name x
5+1:12 name x
6+1:13 tight glyph )
7+2:1 NEWLINE
8+2:1 glyph ++
9+2:4 name constrained
10+2:16 glyph |=
11+2:19 name x
12+2:21 glyph ^-
13+2:24 glyph [
14+2:25 tight name x
15+2:26 tight glyph =
16+2:27 tight aura @t
17+2:30 name y
18+2:31 tight glyph =
19+2:32 tight aura @p
20+2:34 tight glyph ]
21+2:36 glyph (
22+2:37 tight name id
23+2:40 name x
24+2:41 tight glyph )
25+3:1 NEWLINE
26+3:1 glyph ++
27+3:4 name bound-first
28+3:16 glyph |=
29+3:19 name v
30+4:3 INDENT
31+4:3 glyph ~&
32+4:6 glyph ^-
33+4:9 glyph [
34+4:10 tight aura @t
35+4:13 aura @p
36+4:15 tight glyph ]
37+4:17 name v
38+5:5 INDENT
39+5:5 glyph ^-
40+5:8 glyph [
41+5:9 tight name x
42+5:10 tight glyph =
43+5:11 tight aura @t
44+5:14 name y
45+5:15 tight glyph =
46+5:16 tight aura @p
47+5:18 tight glyph ]
48+5:20 name v
49+6:1 DEDENT
50+6:1 DEDENT
51+6:1 NEWLINE
52+6:1 glyph ++
53+6:4 name sample
54+6:11 glyph (
55+6:12 tight name id
56+6:15 glyph [
57+6:16 tight name x
58+6:17 tight glyph =
59+6:18 tight str "hi"
60+6:23 name y
61+6:24 tight glyph =
62+6:25 tight lit ~zod
63+6:29 tight glyph ]
64+6:30 tight glyph )
65+6:31 NEWLINE
tests/golden/types-record-bound-variable/tree.txtnew file+33
@@ -0,0 +1,33 @@
1+(module
2+ (value 1:1 id
3+ (gate-wide 1:7 (bind 1:10 x) (wing 1:12 x)))
4+ (value 2:1 constrained
5+ (gate 2:16
6+ (bind 2:19 x)
7+ (cast 2:21
8+ (cell 2:24
9+ (face 2:25 x (aura 2:27 @t))
10+ (face 2:30 y (aura 2:32 @p)))
11+ (group 2:36
12+ (call 2:37 (wing 2:37 id) (wing 2:40 x))))))
13+ (value 3:1 bound-first
14+ (gate 3:16
15+ (bind 3:19 v)
16+ (body 4:3
17+ (trace 4:3
18+ (cast 4:6
19+ (cell 4:9 (aura 4:10 @t) (aura 4:13 @p))
20+ (wing 4:17 v))
21+ (body 5:5
22+ (cast 5:5
23+ (cell 5:8
24+ (face 5:9 x (aura 5:11 @t))
25+ (face 5:14 y (aura 5:16 @p)))
26+ (wing 5:20 v)))))))
27+ (value 6:1 sample
28+ (group 6:11
29+ (call 6:12
30+ (wing 6:12 id)
31+ (tuple 6:15
32+ (face 6:16 x (str 6:18 "hi"))
33+ (face 6:23 y (lit 6:25 ~zod)))))))
tests/golden/types-record-bound-variable/types.txtnew file+5
@@ -0,0 +1,5 @@
1+partial inference; module not checked
2+++ id: $-(A A)
3+++ constrained: $-([x=@t y=@p] [x=@t y=@p])
4+++ bound-first: cast constraint is not supported by partial inference
5+++ sample: [x=@t y=@p]
tests/golden/types-record-faces/about.txtnew file+4
@@ -0,0 +1,4 @@
1+source: Grammar, Molds: "Faces are part of the type" and "An unnamed position can unify with a faced position and take its face"; Expressions: "Wing ... also for imports and prelude groups".
2+tests: Faced samples and returns retain their faces; cell sample names bind, tuple values acquire expected faces, a missing field is rejected and differently named faces do not unify.
3+expect: parses
4+expect-types: a partial inference report
tests/golden/types-record-faces/source.jibbnew file+8
@@ -0,0 +1,8 @@
1++$ point [x=@t y=@p]
2+++ echo |= p=point p
3+++ tuple ^- point ["hi" ~zod]
4+++ named ^- point [x="hi" y=~zod]
5+++ first |= p=point x.p
6+++ cell-sample |= [a=@t b=@p] [a b]
7+++ missing |= p=point z.p
8+++ mismatch |= p=point ^- [a=@t b=@p] p
tests/golden/types-record-faces/tokens.txtnew file+90
@@ -0,0 +1,90 @@
1+1:1 glyph +$
2+1:4 name point
3+1:10 glyph [
4+1:11 tight name x
5+1:12 tight glyph =
6+1:13 tight aura @t
7+1:16 name y
8+1:17 tight glyph =
9+1:18 tight aura @p
10+1:20 tight glyph ]
11+2:1 NEWLINE
12+2:1 glyph ++
13+2:4 name echo
14+2:9 glyph |=
15+2:12 name p
16+2:13 tight glyph =
17+2:14 tight name point
18+2:20 name p
19+3:1 NEWLINE
20+3:1 glyph ++
21+3:4 name tuple
22+3:10 glyph ^-
23+3:13 name point
24+3:19 glyph [
25+3:20 tight str "hi"
26+3:25 lit ~zod
27+3:29 tight glyph ]
28+4:1 NEWLINE
29+4:1 glyph ++
30+4:4 name named
31+4:10 glyph ^-
32+4:13 name point
33+4:19 glyph [
34+4:20 tight name x
35+4:21 tight glyph =
36+4:22 tight str "hi"
37+4:27 name y
38+4:28 tight glyph =
39+4:29 tight lit ~zod
40+4:33 tight glyph ]
41+5:1 NEWLINE
42+5:1 glyph ++
43+5:4 name first
44+5:10 glyph |=
45+5:13 name p
46+5:14 tight glyph =
47+5:15 tight name point
48+5:21 wing x.p
49+6:1 NEWLINE
50+6:1 glyph ++
51+6:4 name cell-sample
52+6:16 glyph |=
53+6:19 glyph [
54+6:20 tight name a
55+6:21 tight glyph =
56+6:22 tight aura @t
57+6:25 name b
58+6:26 tight glyph =
59+6:27 tight aura @p
60+6:29 tight glyph ]
61+6:31 glyph [
62+6:32 tight name a
63+6:34 name b
64+6:35 tight glyph ]
65+7:1 NEWLINE
66+7:1 glyph ++
67+7:4 name missing
68+7:12 glyph |=
69+7:15 name p
70+7:16 tight glyph =
71+7:17 tight name point
72+7:23 wing z.p
73+8:1 NEWLINE
74+8:1 glyph ++
75+8:4 name mismatch
76+8:13 glyph |=
77+8:16 name p
78+8:17 tight glyph =
79+8:18 tight name point
80+8:24 glyph ^-
81+8:27 glyph [
82+8:28 tight name a
83+8:29 tight glyph =
84+8:30 tight aura @t
85+8:33 name b
86+8:34 tight glyph =
87+8:35 tight aura @p
88+8:37 tight glyph ]
89+8:39 name p
90+8:40 NEWLINE
tests/golden/types-record-faces/tree.txtnew file+41
@@ -0,0 +1,41 @@
1+(module
2+ (mold 1:1 point
3+ (cell 1:10
4+ (face 1:11 x (aura 1:13 @t))
5+ (face 1:16 y (aura 1:18 @p))))
6+ (value 2:1 echo
7+ (gate 2:9
8+ (face 2:12 p (ref 2:14 point))
9+ (wing 2:20 p)))
10+ (value 3:1 tuple
11+ (cast 3:10
12+ (ref 3:13 point)
13+ (tuple 3:19 (str 3:20 "hi") (lit 3:25 ~zod))))
14+ (value 4:1 named
15+ (cast 4:10
16+ (ref 4:13 point)
17+ (tuple 4:19
18+ (face 4:20 x (str 4:22 "hi"))
19+ (face 4:27 y (lit 4:29 ~zod)))))
20+ (value 5:1 first
21+ (gate 5:10
22+ (face 5:13 p (ref 5:15 point))
23+ (wing 5:21 x.p)))
24+ (value 6:1 cell-sample
25+ (gate 6:16
26+ (cell 6:19
27+ (face 6:20 a (aura 6:22 @t))
28+ (face 6:25 b (aura 6:27 @p)))
29+ (tuple 6:31 (wing 6:32 a) (wing 6:34 b))))
30+ (value 7:1 missing
31+ (gate 7:12
32+ (face 7:15 p (ref 7:17 point))
33+ (wing 7:23 z.p)))
34+ (value 8:1 mismatch
35+ (gate 8:13
36+ (face 8:16 p (ref 8:18 point))
37+ (cast 8:24
38+ (cell 8:27
39+ (face 8:28 a (aura 8:30 @t))
40+ (face 8:33 b (aura 8:35 @p)))
41+ (wing 8:39 p)))))
tests/golden/types-record-faces/types.txtnew file+15
@@ -0,0 +1,15 @@
1+partial inference; module not checked
2++$ point: not checked
3+++ echo: $-([x=@t y=@p] [x=@t y=@p])
4+++ tuple: [x=@t y=@p]
5+++ named: [x=@t y=@p]
6+++ first: $-([x=@t y=@p] @t)
7+++ cell-sample: $-([a=@t b=@p] [@t @p])
8+++ missing: field is not available to partial inference
9+++ mismatch: cast mold and expression type do not unify
10+/tests/golden/types-record-faces/source.jibb:8:27: cast mold has type [a=@t b=@p]
11+++ mismatch |= p=point ^- [a=@t b=@p] p
12+ ^
13+/tests/golden/types-record-faces/source.jibb:8:39: expression has type [x=@t y=@p]
14+++ mismatch |= p=point ^- [a=@t b=@p] p
15+ ^
tests/golden/types-record-import/about.txtnew file+4
@@ -0,0 +1,4 @@
1+source: Grammar, Modules: "Everything is exported and read through the import's face"; Molds: "Faces are part of the type".
2+tests: An imported gate carries its faced sample and result across a module interface.
3+expect: parses
4+expect-types: a partial inference report
tests/golden/types-record-import/module-trees.txtnew file+9
@@ -0,0 +1,9 @@
1+/ui/lib.jibb
2+(module
3+ (value 1:1 echo
4+ (gate 1:9
5+ (face 1:12 p
6+ (cell 1:14
7+ (face 1:15 x (aura 1:17 @t))
8+ (face 1:20 y (aura 1:22 @p))))
9+ (wing 1:26 p))))
tests/golden/types-record-import/modules.txtnew file+1
@@ -0,0 +1 @@
1+/ui/lib.jibb
tests/golden/types-record-import/modules/ui/lib.jibbnew file+1
@@ -0,0 +1 @@
1+++ echo |= p=[x=@t y=@p] p
tests/golden/types-record-import/source.jibbnew file+3
@@ -0,0 +1,3 @@
1+/= lib /ui/lib
2+++ value (echo.lib [x="hi" y=~zod])
3+++ first |= p=[x=@t y=@p] x.p
tests/golden/types-record-import/tokens.txtnew file+36
@@ -0,0 +1,36 @@
1+1:1 glyph /=
2+1:5 name lib
3+1:9 glyph /
4+1:10 tight knot ui
5+1:12 tight glyph /
6+1:13 tight knot lib
7+2:1 NEWLINE
8+2:1 glyph ++
9+2:4 name value
10+2:10 glyph (
11+2:11 tight wing echo.lib
12+2:20 glyph [
13+2:21 tight name x
14+2:22 tight glyph =
15+2:23 tight str "hi"
16+2:28 name y
17+2:29 tight glyph =
18+2:30 tight lit ~zod
19+2:34 tight glyph ]
20+2:35 tight glyph )
21+3:1 NEWLINE
22+3:1 glyph ++
23+3:4 name first
24+3:10 glyph |=
25+3:13 name p
26+3:14 tight glyph =
27+3:15 tight glyph [
28+3:16 tight name x
29+3:17 tight glyph =
30+3:18 tight aura @t
31+3:21 name y
32+3:22 tight glyph =
33+3:23 tight aura @p
34+3:25 tight glyph ]
35+3:27 wing x.p
36+3:30 NEWLINE
tests/golden/types-record-import/tree.txtnew file+16
@@ -0,0 +1,16 @@
1+(module
2+ (jibb 1:1 lib /ui/lib)
3+ (value 2:1 value
4+ (group 2:10
5+ (call 2:11
6+ (wing 2:11 echo.lib)
7+ (tuple 2:20
8+ (face 2:21 x (str 2:23 "hi"))
9+ (face 2:28 y (lit 2:30 ~zod))))))
10+ (value 3:1 first
11+ (gate 3:10
12+ (face 3:13 p
13+ (cell 3:15
14+ (face 3:16 x (aura 3:18 @t))
15+ (face 3:21 y (aura 3:23 @p))))
16+ (wing 3:27 x.p))))
tests/golden/types-record-import/types.txtnew file+3
@@ -0,0 +1,3 @@
1+partial inference; module not checked
2+++ value: [x=@t y=@p]
3+++ first: $-([x=@t y=@p] @t)
tests/golden/types-record-local-scheme/about.txtnew file+4
@@ -0,0 +1,4 @@
1+source: Grammar, Runes: "A sample's mold may be left out" and "Local definitions may start any body"; Molds: "Faces are part of the type".
2+tests: A local polymorphic identity preserves a named record's faces, and a sample with bare cell binders infers their types.
3+expect: parses
4+expect-types: a partial inference report
tests/golden/types-record-local-scheme/source.jibbnew file+5
@@ -0,0 +1,5 @@
1+++ keep-local |= r
2+ ++ identity |=(x x)
3+ (identity r)
4+++ record (keep-local [x="hi" y=~zod])
5+++ binders |= [a b] [a b]
tests/golden/types-record-local-scheme/tokens.txtnew file+44
@@ -0,0 +1,44 @@
1+1:1 glyph ++
2+1:4 name keep-local
3+1:15 glyph |=
4+1:18 name r
5+2:3 INDENT
6+2:3 glyph ++
7+2:6 name identity
8+2:15 glyph |=(
9+2:18 tight name x
10+2:20 name x
11+2:21 tight glyph )
12+3:3 NEWLINE
13+3:3 glyph (
14+3:4 tight name identity
15+3:13 name r
16+3:14 tight glyph )
17+4:1 DEDENT
18+4:1 NEWLINE
19+4:1 glyph ++
20+4:4 name record
21+4:11 glyph (
22+4:12 tight name keep-local
23+4:23 glyph [
24+4:24 tight name x
25+4:25 tight glyph =
26+4:26 tight str "hi"
27+4:31 name y
28+4:32 tight glyph =
29+4:33 tight lit ~zod
30+4:37 tight glyph ]
31+4:38 tight glyph )
32+5:1 NEWLINE
33+5:1 glyph ++
34+5:4 name binders
35+5:12 glyph |=
36+5:15 glyph [
37+5:16 tight name a
38+5:18 name b
39+5:19 tight glyph ]
40+5:21 glyph [
41+5:22 tight name a
42+5:24 name b
43+5:25 tight glyph ]
44+5:26 NEWLINE
tests/golden/types-record-local-scheme/tree.txtnew file+20
@@ -0,0 +1,20 @@
1+(module
2+ (value 1:1 keep-local
3+ (gate 1:15
4+ (bind 1:18 r)
5+ (body 2:3
6+ (value 2:3 identity
7+ (gate-wide 2:15 (bind 2:18 x) (wing 2:20 x)))
8+ (group 3:3
9+ (call 3:4 (wing 3:4 identity) (wing 3:13 r))))))
10+ (value 4:1 record
11+ (group 4:11
12+ (call 4:12
13+ (wing 4:12 keep-local)
14+ (tuple 4:23
15+ (face 4:24 x (str 4:26 "hi"))
16+ (face 4:31 y (lit 4:33 ~zod))))))
17+ (value 5:1 binders
18+ (gate 5:12
19+ (cell 5:15 (bind 5:16 a) (bind 5:18 b))
20+ (tuple 5:21 (wing 5:22 a) (wing 5:24 b)))))
tests/golden/types-record-local-scheme/types.txtnew file+4
@@ -0,0 +1,4 @@
1+partial inference; module not checked
2+++ keep-local: $-(A A)
3+++ record: [x=@t y=@p]
4+++ binders: $-([a=A b=B] [A B])
tests/golden/types-record-nested/about.txtnew file+4
@@ -0,0 +1,4 @@
1+source: Grammar, Molds: "Faces are part of the type" and "An unnamed position can unify with a faced position and take its face"; Expressions: "Wing ... also for imports and prelude groups".
2+tests: Nested named fields and records passed through a generalized identity retain their faces.
3+expect: parses
4+expect-types: a partial inference report
tests/golden/types-record-nested/source.jibbnew file+4
@@ -0,0 +1,4 @@
1++$ outer [inner=[x=@t y=@p] enabled=?]
2+++ extract |= p=outer x.inner.p
3+++ keep |=(v v)
4+++ saved (keep [inner=[x="hi" y=~zod] enabled=%.y])
tests/golden/types-record-nested/tokens.txtnew file+54
@@ -0,0 +1,54 @@
1+1:1 glyph +$
2+1:4 name outer
3+1:10 glyph [
4+1:11 tight name inner
5+1:16 tight glyph =
6+1:17 tight glyph [
7+1:18 tight name x
8+1:19 tight glyph =
9+1:20 tight aura @t
10+1:23 name y
11+1:24 tight glyph =
12+1:25 tight aura @p
13+1:27 tight glyph ]
14+1:29 name enabled
15+1:36 tight glyph =
16+1:37 tight glyph ?
17+1:38 tight glyph ]
18+2:1 NEWLINE
19+2:1 glyph ++
20+2:4 name extract
21+2:12 glyph |=
22+2:15 name p
23+2:16 tight glyph =
24+2:17 tight name outer
25+2:23 wing x.inner.p
26+3:1 NEWLINE
27+3:1 glyph ++
28+3:4 name keep
29+3:9 glyph |=(
30+3:12 tight name v
31+3:14 name v
32+3:15 tight glyph )
33+4:1 NEWLINE
34+4:1 glyph ++
35+4:4 name saved
36+4:10 glyph (
37+4:11 tight name keep
38+4:16 glyph [
39+4:17 tight name inner
40+4:22 tight glyph =
41+4:23 tight glyph [
42+4:24 tight name x
43+4:25 tight glyph =
44+4:26 tight str "hi"
45+4:31 name y
46+4:32 tight glyph =
47+4:33 tight lit ~zod
48+4:37 tight glyph ]
49+4:39 name enabled
50+4:46 tight glyph =
51+4:47 tight lit %.y
52+4:50 tight glyph ]
53+4:51 tight glyph )
54+4:52 NEWLINE
tests/golden/types-record-nested/tree.txtnew file+24
@@ -0,0 +1,24 @@
1+(module
2+ (mold 1:1 outer
3+ (cell 1:10
4+ (face 1:11 inner
5+ (cell 1:17
6+ (face 1:18 x (aura 1:20 @t))
7+ (face 1:23 y (aura 1:25 @p))))
8+ (face 1:29 enabled (flag 1:37))))
9+ (value 2:1 extract
10+ (gate 2:12
11+ (face 2:15 p (ref 2:17 outer))
12+ (wing 2:23 x.inner.p)))
13+ (value 3:1 keep
14+ (gate-wide 3:9 (bind 3:12 v) (wing 3:14 v)))
15+ (value 4:1 saved
16+ (group 4:10
17+ (call 4:11
18+ (wing 4:11 keep)
19+ (tuple 4:16
20+ (face 4:17 inner
21+ (tuple 4:23
22+ (face 4:24 x (str 4:26 "hi"))
23+ (face 4:31 y (lit 4:33 ~zod))))
24+ (face 4:39 enabled (lit 4:47 %.y)))))))
tests/golden/types-record-nested/types.txtnew file+5
@@ -0,0 +1,5 @@
1+partial inference; module not checked
2++$ outer: not checked
3+++ extract: $-([inner=[x=@t y=@p] enabled=?] @t)
4+++ keep: $-(A A)
5+++ saved: [inner=[x=@t y=@p] enabled=?]
tests/golden/types-record-to-tuple/about.txtnew file+4
@@ -0,0 +1,4 @@
1+source: Grammar, Molds: "Faces are part of the type" and "An unnamed position can unify with a faced position and take its face"; Expressions: "Wing ... also for imports and prelude groups".
2+tests: A cast to an unfaced tuple preserves a record's faces; propagating those faces through a call result remains unsupported.
3+expect: parses
4+expect-types: a partial inference report
tests/golden/types-record-to-tuple/source.jibbnew file+4
@@ -0,0 +1,4 @@
1+++ plain |= p=[@t @p] p
2+++ data [x="hi" y=~zod]
3+++ called (plain data)
4+++ cast ^- [@t @p] data
tests/golden/types-record-to-tuple/tokens.txtnew file+38
@@ -0,0 +1,38 @@
1+1:1 glyph ++
2+1:4 name plain
3+1:10 glyph |=
4+1:13 name p
5+1:14 tight glyph =
6+1:15 tight glyph [
7+1:16 tight aura @t
8+1:19 aura @p
9+1:21 tight glyph ]
10+1:23 name p
11+2:1 NEWLINE
12+2:1 glyph ++
13+2:4 name data
14+2:9 glyph [
15+2:10 tight name x
16+2:11 tight glyph =
17+2:12 tight str "hi"
18+2:17 name y
19+2:18 tight glyph =
20+2:19 tight lit ~zod
21+2:23 tight glyph ]
22+3:1 NEWLINE
23+3:1 glyph ++
24+3:4 name called
25+3:11 glyph (
26+3:12 tight name plain
27+3:18 name data
28+3:22 tight glyph )
29+4:1 NEWLINE
30+4:1 glyph ++
31+4:4 name cast
32+4:9 glyph ^-
33+4:12 glyph [
34+4:13 tight aura @t
35+4:16 aura @p
36+4:18 tight glyph ]
37+4:20 name data
38+4:24 NEWLINE
tests/golden/types-record-to-tuple/tree.txtnew file+17
@@ -0,0 +1,17 @@
1+(module
2+ (value 1:1 plain
3+ (gate 1:10
4+ (face 1:13 p
5+ (cell 1:15 (aura 1:16 @t) (aura 1:19 @p)))
6+ (wing 1:23 p)))
7+ (value 2:1 data
8+ (tuple 2:9
9+ (face 2:10 x (str 2:12 "hi"))
10+ (face 2:17 y (lit 2:19 ~zod))))
11+ (value 3:1 called
12+ (group 3:11
13+ (call 3:12 (wing 3:12 plain) (wing 3:18 data))))
14+ (value 4:1 cast
15+ (cast 4:9
16+ (cell 4:12 (aura 4:13 @t) (aura 4:16 @p))
17+ (wing 4:20 data))))
tests/golden/types-record-to-tuple/types.txtnew file+5
@@ -0,0 +1,5 @@
1+partial inference; module not checked
2+++ plain: $-([@t @p] [@t @p])
3+++ data: [x=@t y=@p]
4+++ called: call result face propagation is not supported by partial inference
5+++ cast: [x=@t y=@p]
tests/importer/about.txt+4−3
@@ -2,9 +2,10 @@
2recursion, and unsupported forms. `shadow.txt` checks local generator
2recursion, and unsupported forms. `shadow.txt` checks local generator
3shadowing and missing provenance. `shadow-static.txt` checks that a local
3shadowing and missing provenance. `shadow-static.txt` checks that a local
4list shadow alongside a nested ordered map is rejected. Static sibling
4list shadow alongside a nested ordered map is rejected. Static sibling
5−collections and dependent sibling molds are tested separately. Nested `$^`
5+collections and dependent sibling molds are tested separately. A single nested `$^` in a record of aura atom molds and records is checked
6+from its source branches. Named or validated siblings and branches, multiple `$^` cases,
6−cases and `$^` in collection arguments fail closed before Hoon can
7+and `$^` in collection arguments fail closed before Hoon can collapse
7−collapse overlapping branches; nested `$@` cases remain supported. `ford.txt`
8+overlapping branches; nested `$@` cases remain supported. `ford.txt`
8checks a synthetic imported subject and selected mold; other cases check
9checks a synthetic imported subject and selected mold; other cases check
9transitive imports, named mold lookup, missing names, shadowing, unprovenanced
10transitive imports, named mold lookup, missing names, shadowing, unprovenanced
10recursive holds, malformed
11recursive holds, malformed
tests/importer/ford.txt+1
@@ -2,5 +2,6 @@
2+$ lists (list @ud)
2+$ lists (list @ud)
3+$ wrapped item:small
3+$ wrapped item:small
4+$ recursive chain:small
4+$ recursive chain:small
5++$ nested-record nested-valid-cell:small
5+$ local $@(~ [v=@ud next=local])
6+$ local $@(~ [v=@ud next=local])
6--
7--
tests/importer/origin-transitive.txt+1
@@ -1,3 +1,4 @@
1|%
1|%
2+$ wrapped recursive:intermediate
2+$ wrapped recursive:intermediate
3++$ nested nested-record:intermediate
3--
4--
tests/importer/small.txt+8
@@ -36,6 +36,14 @@
36+$ set-direct-invalid-cell (set $^(@ud @ud))
36+$ set-direct-invalid-cell (set $^(@ud @ud))
37+$ map-key-invalid-cell (map $^(@ud @ud) @t)
37+$ map-key-invalid-cell (map $^(@ud @ud) @t)
38+$ nested-atom-cell [left=$@(@ud [a=@ud b=@t]) right=$@(@t [c=@ud d=@t])]
38+$ nested-atom-cell [left=$@(@ud [a=@ud b=@t]) right=$@(@t [c=@ud d=@t])]
39++$ nested-first-cell [value=$^(@ud [a=@ud b=@t]) id=@t]
40++$ nested-alias-cell nested-valid-cell
41++$ nested-multiple-cell [id=$^(@ud @ud) value=$^(@ud [a=@ud b=@t])]
42++$ nested-named-sibling [id=word value=$^(@ud [a=@ud b=@t])]
43++$ nested-list-sibling [id=(list @ud) value=$^(@ud [a=@ud b=@t])]
44++$ nested-validated-sibling [id=$|(@ud |=(a=@ud =(a 0))) value=$^(@ud [a=@ud b=@t])]
45++$ nested-validated-branch [id=@ud value=$^($|(@ud |=(a=@ud =(a 0))) [a=@ud b=@t])]
46++$ nested-named-branch [id=@ud value=$^(word [a=@ud b=@t])]
39+$ nested-valid-cell [id=@ud value=$^(@ud [a=@ud b=@t])]
47+$ nested-valid-cell [id=@ud value=$^(@ud [a=@ud b=@t])]
40+$ nested-invalid-cell [id=@ud value=$^(@ud @ud)]
48+$ nested-invalid-cell [id=@ud value=$^(@ud @ud)]
41+$ valid-cell $^(@ud [x=@ud y=@ud])
49+$ valid-cell $^(@ud [x=@ud y=@ud])
tests/importer/tree.txt+11−2
@@ -56,8 +56,17 @@ map-nested-invalid-cell: error: a Hoon $^ union needs a source-level disjointnes
56set-direct-invalid-cell: error: a Hoon $^ union needs a source-level disjointness check
56set-direct-invalid-cell: error: a Hoon $^ union needs a source-level disjointness check
57map-key-invalid-cell: error: a Hoon $^ union needs a source-level disjointness check
57map-key-invalid-cell: error: a Hoon $^ union needs a source-level disjointness check
58nested-atom-cell: [left=(union [a=@ud b=@t] @ud) right=(union [c=@ud d=@t] @t)]
58nested-atom-cell: [left=(union [a=@ud b=@t] @ud) right=(union [c=@ud d=@t] @t)]
59−nested-valid-cell: error: a Hoon $^ union needs a source-level disjointness check
59+nested-first-cell: [value=(union [a=@ud b=@t] @ud) id=@t]
60+nested-alias-cell: [id=@ud value=(union [a=@ud b=@t] @ud)]
61+nested-multiple-cell: error: a Hoon $^ union needs a source-level disjointness check
62+nested-named-sibling: error: a Hoon $^ union needs a source-level disjointness check
63+nested-list-sibling: error: a Hoon $^ union needs a source-level disjointness check
64+nested-validated-sibling: error: a Hoon $^ union needs a source-level disjointness check
65+nested-validated-branch: error: a Hoon $^ union needs a source-level disjointness check
66+nested-named-branch: error: a Hoon $^ union needs a source-level disjointness check
67+nested-ford-cell: [id=@ud value=(union [a=@ud b=@t] @ud)]
68+nested-valid-cell: [id=@ud value=(union [a=@ud b=@t] @ud)]
60−nested-invalid-cell: error: a Hoon $^ union needs a source-level disjointness check
69+nested-invalid-cell: error: a Hoon $^ union has overlapping cases
61valid-cell: (union [x=@ud y=@ud] @ud)
70valid-cell: (union [x=@ud y=@ud] @ud)
62invalid-cell: error: a Hoon $^ union has overlapping cases
71invalid-cell: error: a Hoon $^ union has overlapping cases
63chapter-malformed: unsafe
72chapter-malformed: unsafe
tests/lib/jibb.hoon+38
@@ -1438,6 +1438,32 @@
1438/* tok-435 %txt /tests/golden/types-partial-unresolved-tag/tokens/txt
1438/* tok-435 %txt /tests/golden/types-partial-unresolved-tag/tokens/txt
1439/* tre-435 %txt /tests/golden/types-partial-unresolved-tag/tree/txt
1439/* tre-435 %txt /tests/golden/types-partial-unresolved-tag/tree/txt
1440/* typ-435 %txt /tests/golden/types-partial-unresolved-tag/types/txt
1440/* typ-435 %txt /tests/golden/types-partial-unresolved-tag/types/txt
1441+/* src-436 %jibb /tests/golden/types-record-bound-variable/source/jibb
1442+/* tok-436 %txt /tests/golden/types-record-bound-variable/tokens/txt
1443+/* tre-436 %txt /tests/golden/types-record-bound-variable/tree/txt
1444+/* typ-436 %txt /tests/golden/types-record-bound-variable/types/txt
1445+/* src-437 %jibb /tests/golden/types-record-faces/source/jibb
1446+/* tok-437 %txt /tests/golden/types-record-faces/tokens/txt
1447+/* tre-437 %txt /tests/golden/types-record-faces/tree/txt
1448+/* typ-437 %txt /tests/golden/types-record-faces/types/txt
1449+/* src-438 %jibb /tests/golden/types-record-import/source/jibb
1450+/* tok-438 %txt /tests/golden/types-record-import/tokens/txt
1451+/* tre-438 %txt /tests/golden/types-record-import/tree/txt
1452+/* mod-438-1 %jibb /tests/golden/types-record-import/modules/ui/lib/jibb
1453+/* typ-438 %txt /tests/golden/types-record-import/types/txt
1454+/* mtre-438 %txt /tests/golden/types-record-import/module-trees/txt
1455+/* src-439 %jibb /tests/golden/types-record-local-scheme/source/jibb
1456+/* tok-439 %txt /tests/golden/types-record-local-scheme/tokens/txt
1457+/* tre-439 %txt /tests/golden/types-record-local-scheme/tree/txt
1458+/* typ-439 %txt /tests/golden/types-record-local-scheme/types/txt
1459+/* src-440 %jibb /tests/golden/types-record-nested/source/jibb
1460+/* tok-440 %txt /tests/golden/types-record-nested/tokens/txt
1461+/* tre-440 %txt /tests/golden/types-record-nested/tree/txt
1462+/* typ-440 %txt /tests/golden/types-record-nested/types/txt
1463+/* src-441 %jibb /tests/golden/types-record-to-tuple/source/jibb
1464+/* tok-441 %txt /tests/golden/types-record-to-tuple/tokens/txt
1465+/* tre-441 %txt /tests/golden/types-record-to-tuple/tree/txt
1466+/* typ-441 %txt /tests/golden/types-record-to-tuple/types/txt
1441|%
1467|%
1442:: one arm per case
1468:: one arm per case
1443::
1469::
@@ -2311,6 +2337,18 @@
2311 (weld (check ~.types-partial-union-edges src-434 `tok-434 `tre-434) (check-types ~.types-partial-union-edges ~[%tests %golden ~.types-partial-union-edges %source %jibb] src-434 `typ-434))
2337 (weld (check ~.types-partial-union-edges src-434 `tok-434 `tre-434) (check-types ~.types-partial-union-edges ~[%tests %golden ~.types-partial-union-edges %source %jibb] src-434 `typ-434))
2312++ test-types-partial-unresolved-tag
2338++ test-types-partial-unresolved-tag
2313 (weld (check ~.types-partial-unresolved-tag src-435 `tok-435 `tre-435) (check-types ~.types-partial-unresolved-tag ~[%tests %golden ~.types-partial-unresolved-tag %source %jibb] src-435 `typ-435))
2339 (weld (check ~.types-partial-unresolved-tag src-435 `tok-435 `tre-435) (check-types ~.types-partial-unresolved-tag ~[%tests %golden ~.types-partial-unresolved-tag %source %jibb] src-435 `typ-435))
2340+++ test-types-record-bound-variable
2341+ (weld (check ~.types-record-bound-variable src-436 `tok-436 `tre-436) (check-types ~.types-record-bound-variable ~[%tests %golden ~.types-record-bound-variable %source %jibb] src-436 `typ-436))
2342+++ test-types-record-faces
2343+ (weld (check ~.types-record-faces src-437 `tok-437 `tre-437) (check-types ~.types-record-faces ~[%tests %golden ~.types-record-faces %source %jibb] src-437 `typ-437))
2344+++ test-types-record-import
2345+ (weld (weld (check ~.types-record-import src-438 `tok-438 `tre-438) (check-module-types ~.types-record-import ~[%tests %golden ~.types-record-import %source %jibb] src-438 `typ-438 ~ ~ ~[['/ui/lib.jibb' ~[~.ui ~.lib ~.jibb] mod-438-1]])) (check-module-trees ~.types-record-import `mtre-438 ~[['/ui/lib.jibb' ~[~.ui ~.lib ~.jibb] mod-438-1]]))
2346+++ test-types-record-local-scheme
2347+ (weld (check ~.types-record-local-scheme src-439 `tok-439 `tre-439) (check-types ~.types-record-local-scheme ~[%tests %golden ~.types-record-local-scheme %source %jibb] src-439 `typ-439))
2348+++ test-types-record-nested
2349+ (weld (check ~.types-record-nested src-440 `tok-440 `tre-440) (check-types ~.types-record-nested ~[%tests %golden ~.types-record-nested %source %jibb] src-440 `typ-440))
2350+++ test-types-record-to-tuple
2351+ (weld (check ~.types-record-to-tuple src-441 `tok-441 `tre-441) (check-types ~.types-record-to-tuple ~[%tests %golden ~.types-record-to-tuple %source %jibb] src-441 `typ-441))
2314::
2352::
2315:: +check: run golden:jibb on a case and compare both outputs
2353:: +check: run golden:jibb on a case and compare both outputs
2316::
2354::
tools/clay-fixtures+13
@@ -103,6 +103,19 @@ if result.stdout != expected:
103 sys.exit(1)
103 sys.exit(1)
104print('Clay recursive Ford importer golden passed')
104print('Clay recursive Ford importer golden passed')
105
105
106+try:
107+ result = subprocess.run([str(ship), 'run', str(fixtures / 'ford-nested-union.txt')],
108+ stdout=subprocess.PIPE, check=True)
109+except subprocess.CalledProcessError as error:
110+ sys.exit(error.returncode)
111+expected = (fixtures / 'ford-nested-union-expected.txt').read_bytes()
112+if result.stdout != expected:
113+ print('Clay nested union import differs from tests/clay-fixtures/ford-nested-union-expected.txt', file=sys.stderr)
114+ print('expected:', expected.decode().rstrip(), file=sys.stderr)
115+ print('actual: ', result.stdout.decode().rstrip(), file=sys.stderr)
116+ sys.exit(1)
117+print('Clay nested Ford union importer golden passed')
118+
106try:
119try:
107 result = subprocess.run([str(ship), 'run', str(fixtures / 'mark-shape.txt')],
120 result = subprocess.run([str(ship), 'run', str(fixtures / 'mark-shape.txt')],
108 stdout=subprocess.PIPE, check=True)
121 stdout=subprocess.PIPE, check=True)
tools/importer-test+1−1
@@ -34,4 +34,4 @@ if result.stdout != expected:
34 result.stdout.decode().splitlines(keepends=True),
34 result.stdout.decode().splitlines(keepends=True),
35 fromfile='expected tree.txt', tofile='actual types'))
35 fromfile='expected tree.txt', tofile='actual types'))
36 sys.exit(1)
36 sys.exit(1)
37−print('importer golden: 90 projections passed')
37+print('importer golden: 99 projections passed')