651b8ec · jibb · git.iko.soy

git.iko.soy/jibb

on master help sign in

Infer direct higher-order gates from source

651b8eciko2 days ago

docs/compiler.md+7−1

compare with master

unifiedsplit

@@ -56,7 +56,13 @@ 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` |

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

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. 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. 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.

60+

61+A 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+

63+The checker retains a per-analysis index of finalized root gates and a prelude source table bound to the entire trusted prepared interface. A dependency screen avoids building the table when the root cannot use it; changing the interface invalidates it. The host remains responsible for supplying a prepared interface paired with its source. The matcher checks each slot and product in both directions with a shared substitution. Before returning its tentative proof it requires both complete call samples to normalize to closed, tag-free types, then repeats every slot check and requires the substitution and fresh-ID counter to remain unchanged. This keeps later argument or enclosing constraints from invalidating an earlier face check, and preserves pending constraints, capital checks and projection evidence. These scans and the bounded second proof add work; they do not establish a global linear-time bound.

64+

65+In single sequential eval runs including startup, 2,000 ordinary gates used 70.20 seconds of user CPU at baseline and 70.64 seconds with the cached source table. Fifty unsupported eligible scalar-slot calls used 24.75 and 25.71 seconds, while fifty function-slot failures used 24.15 and 25.36 seconds. Fifty successful calls took 26.56 seconds before the final stability replay and 26.99 seconds with it. These are synthetic measurements, not production performance limits.

61A single-arm cell pattern can bind two or more positions, with its last binder capturing the remaining tail. Duplicate and shadowed names are rejected. A definite non-cell spine fails; an intermediate union or collection that might contain a cell remains unsupported. For a known non-union cell, a separate one-arm rule also accepts structured patterns, including nested literal and wildcard positions, when the existing coverage proof establishes the whole pattern. It binds payloads with their original types and checks result context; unknown, partially covered, union or recursive spines stay unsupported.

67A single-arm cell pattern can bind two or more positions, with its last binder capturing the remaining tail. Duplicate and shadowed names are rejected. A definite non-cell spine fails; an intermediate union or collection that might contain a cell remains unsupported. For a known non-union cell, a separate one-arm rule also accepts structured patterns, including nested literal and wildcard positions, when the existing coverage proof establishes the whole pattern. It binds payloads with their original types and checks result context; unknown, partially covered, union or recursive spines stay unsupported.

docs/development.md+2

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

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

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

76| `tools/type-todo-api-test` | Exercises the actual todo API through the real Hoon readers and partial checker |

77+| `tools/type-direct-gate-test` | Checks a synthetic source-backed program report and direct gate provenance under eval and on the ship |

77| `tools/type-closed-gate-guards-test` | Checks closed gate sample labels and face uncertainty under eval and on the ship |

78| `tools/type-closed-gate-guards-test` | Checks closed gate sample labels and face uncertainty under eval and on the ship |

78| `tools/type-constructor-fit-guards-test` | Checks constructor-case uncertainty and known mismatches under eval and on the ship |

79| `tools/type-constructor-fit-guards-test` | Checks constructor-case uncertainty and known mismatches under eval and on the ship |

79| `tools/type-nested-union-guards-test` | Checks nested tagged-union case selection and uncertainty under eval and on the ship |

80| `tools/type-nested-union-guards-test` | Checks nested tagged-union case selection and uncertainty under eval and on the ship |

@@ -114,6 +115,7 @@ tools/type-generic-alias-test # generic union alias guards pass

114tools/type-positional-face-guards-test # positional sample face guards pass

115tools/type-positional-face-guards-test # positional sample face guards pass

115tools/type-qath-guards-test # qath source and unfolding guards pass

116tools/type-qath-guards-test # qath source and unfolding guards pass

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

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

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

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

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

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

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

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

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

docs/status.md+5−2

@@ -31,6 +31,8 @@ Known same-origin generic-union result context can now constrain a call before i

32A separate source-backed analysis can prove one named mold gate-free, report a definite gate with a field path, or return unknown. It retains the prepared prelude, source bundle, reader results and resolved imports; the actual todo model proves gate-free, while a callback field reports its path and `*` remains unknown. Its classifier is capped at 256 nodes, not the surrounding parse and import work. API, store and private roots are unsupported, and the artifact does not check a module or island, infer generalized constraints, or prove watchability.

34+The partial checker can also match a directly named, checked root gate against a generic gate sample in a direct, unshadowed source-backed prelude call. It uses the written two-slot sample layouts to preserve nested record faces, then requires the complete call samples to be closed and tag-free and repeats the fit under the final substitution. The proof falls back to existing inference for unavailable or ambiguous source layouts, local or dynamic gates, aliases, recursive placeholders and open generic caller types. It preserves written-capital checks and projection evidence; it does not add `program`, check islands or prove request watchability. Prepared prelude source and interface remain a trusted pair.

35+

34The API path analyzer can retain its source, complete prepared prelude, reader results and resolved dependencies as evidence, and classify a unique declaration as watchable, not watchable or unknown. It does not yet prove the provenance of request values or check island subscriptions. Prepared artifacts and reader results remain trusted host inputs.

36The API path analyzer can retain its source, complete prepared prelude, reader results and resolved dependencies as evidence, and classify a unique declaration as watchable, not watchable or unknown. It does not yet prove the provenance of request values or check island subscriptions. Prepared artifacts and reader results remain trusted host inputs.

36For a unique supported path declaration, the request-parts analysis derives ordered typed path parameters, a full-state reply sample and a fold type for one diff mark. Multiple diffs and unsupported or ambiguous evidence fail closed. By itself it does not create request gates or establish watchability of values.

38For a unique supported path declaration, the request-parts analysis derives ordered typed path parameters, a full-state reply sample and a fold type for one diff mark. Multiple diffs and unsupported or ambiguous evidence fail closed. By itself it does not create request gates or establish watchability of values.

@@ -62,7 +64,7 @@ What the plan asks for, and where it is:

62Besides the plan's list:

64Besides the plan's list:

64- 649 golden cases: 429 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.

66- 649 golden cases: 429 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.

65−- The 649-case corpus passed under `urbit eval` in 91.6 s while other checks were running. The fake ship passed all 678 tests, including the 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 and gate-free guards, with 66.8 s for sync and 81.8 s for tests. 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.

67+- The 649-case corpus passed under `urbit eval` in 109.6 s while other checks were running. The fake ship passed all 680 tests, including the 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, with 80.2 s for sync and 94.0 s for tests. 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.

66- `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.

68- `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.

67- 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.

69- 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.

68- 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).

70- 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).

@@ -158,7 +160,8 @@ Besides the plan's list:

158| a1c5f35 | 2026-10-31 | Infer supported multi-path requests and named closed folds |

160| a1c5f35 | 2026-10-31 | Infer supported multi-path requests and named closed folds |

159| 911ca0c | 2026-10-31 | Propagate union context, define subscriptions and match literal nouns |

161| 911ca0c | 2026-10-31 | Propagate union context, define subscriptions and match literal nouns |

160| 72acdb3 | 2026-10-31 | Infer selected nested union payloads from context |

162| 72acdb3 | 2026-10-31 | Infer selected nested union payloads from context |

161−| This change | 2026-10-31 | Analyze gate-free source molds with field witnesses |

163+| 706035c | 2026-10-31 | Analyze gate-free source molds with field witnesses |

164+| This change | 2026-10-31 | Match source-proven gate samples in direct calls |

162

165

163## Checking it

166## Checking it

164

167

jibb-dev/lib/jibb.hoon+258−15

@@ -5674,7 +5674,8 @@

5674 %jrec [%yes & fuel ~]

5675 ==

5676::

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

5677−+$ 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)]

5678++$ 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)]

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

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

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

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

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

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

@@ -8257,6 +8258,234 @@

8257 ?: ?=(%| -.out) [%| p.out]

8258 ?: ?=(%| -.out) [%| p.out]

8258 [%& [e typ.p.out sub.state.p.out (flop projections.state.p.out)]]

8259 [%& [e typ.p.out sub.state.p.out (flop projections.state.p.out)]]

8259::

8260::

8261+:: Source-bound gate-layout evidence, confined to checked root gate

8262+:: definitions and direct unshadowed prelude calls. The prepared prelude

8263+:: interface and its retained source are trusted as a matching artifact.

8264+:: Layouts identify sample binder faces; they do not change call arity or

8265+:: authorize stripping nested value faces. Unknown origins use ordinary fit.

8266+++ direct-written-gates

8267+ |= [ds=(list def) out=ivisited]

8268+ ^- ivisited

8269+ ?~ ds out

8270+ ?: ?=(%mold -.i.ds) $(ds t.ds)

8271+ ?. |(?=(%gate -.val.i.ds) ?=(%gate-wide -.val.i.ds)) $(ds t.ds)

8272+ $(ds t.ds, out (~(put by out) name.i.ds &))

8273+++ direct-may-use-prelude

8274+ |= [ds=(list def) root=ivisited heads=ivisited]

8275+ ^- ?

8276+ ?~ ds |

8277+ ?: ?=(%mold -.i.ds) $(ds t.ds)

8278+ =/ refs=(list term) (dependency-expr val.i.ds)

8279+ =/ has-root=? (lien refs |=(n=term ?=(^ (~(get by root) n))))

8280+ =/ has-head=? (lien refs |=(n=term ?=(^ (~(get by heads) n))))

8281+ ?: &(has-root has-head) &

8282+ $(ds t.ds)

8283+++ direct-unique-names

8284+ |= [names=(list term) seen=ivisited]

8285+ ^- ?

8286+ ?~ names &

8287+ ?: ?=(^ (~(get by seen) i.names)) |

8288+ $(names t.names, seen (~(put by seen) i.names &))

8289+++ direct-prelude-evidence

8290+ |= [ds=(list def) prelude=(unit ifile)]

8291+ ^- (unit igate-prelude-evidence)

8292+ ?~ prelude ~

8293+ ?~ source.u.prelude ~

8294+ =/ root=ivisited (direct-written-gates ds ~)

8295+ =/ names=(list term) (turn values.u.prelude |=(e=[name=term scheme=ischeme] name.e))

8296+ =/ heads=ivisited (graph-nameset names ~)

8297+ ?. (direct-may-use-prelude ds root heads) ~

8298+ =/ parsed (parse at.u.prelude u.source.u.prelude)

8299+ ?: ?=(%| -.parsed) ~

8300+ ?^ (duplicate-defs defs.p.parsed) ~

8301+ ?. (direct-unique-names (global-value-names defs.p.parsed) ~) ~

8302+ =/ gates=(map term def) (direct-checked-gates defs.p.parsed values.u.prelude)

8303+ `[u.prelude gates]

8304+++ direct-checked-gates

8305+ |= [ds=(list def) env=ienv]

8306+ ^- (map term def)

8307+ =/ names=(list term) (turn env |=(e=[name=term scheme=ischeme] name.e))

8308+ =/ known=ivisited (graph-nameset names ~)

8309+ =/ out=(map term def) ~

8310+ |-

8311+ ?~ ds out

8312+ =/ d=def i.ds

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

8314+ ?. ?=(^ (~(get by known) name.d)) $(ds t.ds)

8315+ ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) $(ds t.ds)

8316+ $(ds t.ds, out (~(put by out) name.d d))

8317+++ direct-find-gate

8318+ |= [n=term ds=(list def)]

8319+ ^- (unit def)

8320+ ?~ ds ~

8321+ ?: &(?=(%value -.i.ds) =(n name.i.ds)) `i.ds

8322+ $(ds t.ds)

8323+++ direct-gate-sample

8324+ |= d=def

8325+ ^- (unit sample)

8326+ ?. ?=(%value -.d) ~

8327+ ?- -.val.d

8328+ %gate `sample.val.d

8329+ %gate-wide `sample.val.d

8330+ * ~

8331+ ==

8332+++ direct-sample-name

8333+ |= sam=sample

8334+ ^- (unit term)

8335+ ?- -.sam

8336+ %bind `name.sam

8337+ %face `name.sam

8338+ %pun `name.sam

8339+ * ~

8340+ ==

8341+++ direct-field-name

8342+ |= f=field

8343+ ^- (unit term)

8344+ ?- -.f

8345+ %face `name.f

8346+ %pun `name.f

8347+ * ~

8348+ ==

8349+++ direct-slot-body

8350+ |= [typ=itype name=(unit term)]

8351+ ^- (unit itype)

8352+ ?~ name `typ

8353+ ?. ?=(%face -.typ) ~

8354+ ?. =(name.typ u.name) ~

8355+ `body.typ

8356+++ direct-invariant

8357+ |= [a=itype b=itype sub=isub next=@ud]

8358+ ^- ifit

8359+ ?: (itype-face-asym a b sub) [%unknown ~]

8360+ =/ forward=ifit (itype-fit a b sub next)

8361+ ?. ?=(%ok -.forward) [%unknown ~]

8362+ ?: (itype-face-asym a b sub.forward) [%unknown ~]

8363+ =/ reverse=ifit (itype-fit b a sub.forward next.forward)

8364+ ?. ?=(%ok -.reverse) [%unknown ~]

8365+ reverse

8366+++ direct-function-fit

8367+ |= [a=itype b=itype sam=sample sh=shape sub=isub next=@ud]

8368+ ^- ifit

8369+ ?. &(?=(%fn -.a) ?=(%fn -.b) ?=(%cell -.sam) ?=(%fn -.sh)) [%unknown ~]

8370+ ?. ?=(%cell -.sample.sh) [%unknown ~]

8371+ =/ as=(list sample) items.sam

8372+ =/ bs=(list field) fields.sample.sh

8373+ ?~ as [%unknown ~]

8374+ ?~ t.as [%unknown ~]

8375+ ?^ t.t.as [%unknown ~]

8376+ ?~ bs [%unknown ~]

8377+ ?~ t.bs [%unknown ~]

8378+ ?^ t.t.bs [%unknown ~]

8379+ ?. &(?=(%cell -.sample.a) ?=(%cell -.sample.b)) [%unknown ~]

8380+ =/ an=(unit term) (direct-sample-name i.as)

8381+ =/ bn=(unit term) (direct-field-name i.bs)

8382+ ?: &(?=(^ an) ?=(^ bn) !=(u.an u.bn)) [%unknown ~]

8383+ =/ x=(unit itype) (direct-slot-body hed.sample.a an)

8384+ =/ y=(unit itype) (direct-slot-body hed.sample.b bn)

8385+ ?~ x [%unknown ~]

8386+ ?~ y [%unknown ~]

8387+ =/ first=ifit (direct-invariant u.x u.y sub next)

8388+ ?. ?=(%ok -.first) [%unknown ~]

8389+ =. an (direct-sample-name i.t.as)

8390+ =. bn (direct-field-name i.t.bs)

8391+ ?: &(?=(^ an) ?=(^ bn) !=(u.an u.bn)) [%unknown ~]

8392+ =/ x2=(unit itype) (direct-slot-body tal.sample.a an)

8393+ =/ y2=(unit itype) (direct-slot-body tal.sample.b bn)

8394+ ?~ x2 [%unknown ~]

8395+ ?~ y2 [%unknown ~]

8396+ =/ second=ifit (direct-invariant u.x2 u.y2 sub.first next.first)

8397+ ?. ?=(%ok -.second) [%unknown ~]

8398+ (direct-invariant product.a product.b sub.second next.second)

8399+:: This is a tentative proof: its caller must require closed call samples

8400+:: and repeat every positional check under the stable final substitution.

8401+++ direct-positional-fit

8402+ |= [args=(list expr) slots=(list sample) actual=itype expected=itype env=ienv state=istate sub=isub next=@ud]

8403+ ^- ifit

8404+ ?~ args [%unknown ~]

8405+ ?~ slots [%unknown ~]

8406+ =/ last=? ?=(~ t.args)

8407+ ?: !=(last ?=(~ t.slots)) [%unknown ~]

8408+ =/ split=(unit [left=itype right=itype])

8409+ ?: last `[actual expected]

8410+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~

8411+ `[hed.actual hed.expected]

8412+ ?~ split [%unknown ~]

8413+ =/ x=itype left.u.split

8414+ =/ y=itype right.u.split

8415+ =/ expected-name=(unit term) (direct-sample-name i.slots)

8416+ =/ expected-body=(unit itype) (direct-slot-body y expected-name)

8417+ ?~ expected-body [%unknown ~]

8418+ =. y u.expected-body

8419+ =/ fit=ifit (itype-fit x y sub next)

8420+ =/ accepted=? &(?=(%ok -.fit) !(itype-positional-slot-face-asym x y sub.fit))

8421+ =/ result=(unit ifit)

8422+ ?: accepted `fit

8423+ ?. &(?=(%face -.i.slots) ?=(%fn -.shape.i.slots)) ~

8424+ ?. ?=(%wing -.i.args) ~

8425+ ?. ?=([@ ~] names.i.args) ~

8426+ ?. (unique-value-name i.names.i.args globals.state) ~

8427+ =/ source=(unit def) (~(get by gate-defs.state) i.names.i.args)

8428+ ?~ source ~

8429+ =/ sample=(unit sample) (direct-gate-sample u.source)

8430+ ?~ sample ~

8431+ =/ trial=ifit (direct-function-fit x y u.sample shape.i.slots sub next)

8432+ ?. ?=(%ok -.trial) ~

8433+ `trial

8434+ ?~ result [%unknown ~]

8435+ =. fit u.result

8436+ ?: last fit

8437+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) [%unknown ~]

8438+ ?. ?=(%ok -.fit) [%unknown ~]

8439+ $(args t.args, slots t.slots, actual tal.actual, expected tal.expected, sub sub.fit, next next.fit)

8440+++ direct-any-gate-arg

8441+ |= [args=(list expr) defs=(map term def)]

8442+ ^- ?

8443+ ?~ args |

8444+ =/ found=?

8445+ ?. ?=(%wing -.i.args) |

8446+ ?. ?=([@ ~] names.i.args) |

8447+ ?=(^ (~(get by defs) i.names.i.args))

8448+ ?: found &

8449+ $(args t.args)

8450+++ direct-gate-call-fit

8451+ |= [e=expr actual=itype expected=itype env=ienv state=istate]

8452+ ^- (unit ifit)

8453+ ?. ?=(%call -.e) ~

8454+ ?~ args.e ~

8455+ ?~ t.args.e ~

8456+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~

8457+ ?. ?=(%wing -.head.e) ~

8458+ ?. ?=([@ ~] names.head.e) ~

8459+ ?. ?=(~ (ienv-lookup i.names.head.e env)) ~

8460+ ?. (unique-value-name i.names.head.e globals.state) ~

8461+ ?. (direct-any-gate-arg args.e gate-defs.state) ~

8462+ ?~ prelude.state ~

8463+ ?~ source.u.prelude.state ~

8464+ ?~ head-evidence.state ~

8465+ ?. =(u.prelude.state iface.u.head-evidence.state) ~

8466+ ?. ?=(^ (ienv-lookup i.names.head.e values.u.prelude.state)) ~

8467+ =/ head=(unit def) (~(get by gates.u.head-evidence.state) i.names.head.e)

8468+ ?~ head ~

8469+ =/ sam=(unit sample) (direct-gate-sample u.head)

8470+ ?~ sam ~

8471+ ?. ?=(%cell -.u.sam) ~

8472+ =/ fit=ifit (direct-positional-fit args.e items.u.sam actual expected env state sub.state next.state)

8473+ ?. ?=(%ok -.fit) ~

8474+ :: Enclosing inference may add constraints after this call. Only a

8475+ :: closed call-sample proof can remain stable under those later bindings.

8476+ =/ actual-final=itype (itype-normalize actual sub.fit)

8477+ =/ expected-final=itype (itype-normalize expected sub.fit)

8478+ ?^ (itype-vars actual-final) ~

8479+ ?^ (itype-vars expected-final) ~

8480+ ?: |((itype-has-tag actual-final) (itype-has-tag expected-final)) ~

8481+ :: A later argument may resolve a variable used by an earlier slot.

8482+ :: Recheck every fit and face against the completed substitution; no

8483+ :: additional binding or fresh variable is permitted in the second pass.

8484+ =/ verified=ifit (direct-positional-fit args.e items.u.sam actual expected env state sub.fit next.fit)

8485+ ?. ?=(%ok -.verified) ~

8486+ ?. &(=(sub.fit sub.verified) =(next.fit next.verified)) ~

8487+ `fit

8488+::

8260++ infer-call-with-head

8489++ infer-call-with-head

8261 |= [e=expr env=ienv state=istate head=iresult]

8490 |= [e=expr env=ienv state=istate head=iresult]

8262 ^- iresult

8491 ^- iresult

@@ -8283,6 +8512,10 @@

8283 =/ fit=ifit

8512 =/ fit=ifit

8284 ?^ t.args.e (itype-fit-inner typ.p.arg sample.ht sub.st next.st & |)

8513 ?^ t.args.e (itype-fit-inner typ.p.arg sample.ht sub.st next.st & |)

8285 (itype-fit typ.p.arg sample.ht sub.st next.st)

8514 (itype-fit typ.p.arg sample.ht sub.st next.st)

8515+ =/ direct=(unit ifit)

8516+ ?: ?=(%ok -.fit) ~

8517+ (direct-gate-call-fit e typ.p.arg sample.ht env st)

8518+ =. fit ?~(direct fit u.direct)

8286 ?: ?=(%unknown -.fit) [%| ["call constraint is not supported by partial inference" ~]]

8519 ?: ?=(%unknown -.fit) [%| ["call constraint is not supported by partial inference" ~]]

8287 ?: ?=(%bad -.fit)

8520 ?: ?=(%bad -.fit)

8288 ?~ t.args.e

8521 ?~ t.args.e

@@ -8299,6 +8532,7 @@

8299 =/ arg-type=itype ?~(bad typ.p.arg typ.u.bad)

8532 =/ arg-type=itype ?~(bad typ.p.arg typ.u.bad)

8300 [%| ["call's sample and argument types do not unify" ~[[(span-of head.e) (site-type-note "called gate" ht sub.st)] [arg-at (site-type-note "argument" arg-type sub.st)]]]]

8533 [%| ["call's sample and argument types do not unify" ~[[(span-of head.e) (site-type-note "called gate" ht sub.st)] [arg-at (site-type-note "argument" arg-type sub.st)]]]]

8301 =/ face-asym=?

8534 =/ face-asym=?

8535+ ?^ direct |

8302 ?^ t.args.e (itype-positional-face-asym args.e typ.p.arg sample.ht sub.fit)

8536 ?^ t.args.e (itype-positional-face-asym args.e typ.p.arg sample.ht sub.fit)

8303 (itype-face-asym typ.p.arg sample.ht sub.fit)

8537 (itype-face-asym typ.p.arg sample.ht sub.fit)

8304 ?: &((itype-has-face typ.p.arg sub.fit) face-asym (itype-output-may-be-cell product.ht sub.fit))

8538 ?: &((itype-has-face typ.p.arg sub.fit) face-asym (itype-output-may-be-cell product.ht sub.fit))

@@ -9130,6 +9364,7 @@

9130++ infer-recursive-gate

9364++ infer-recursive-gate

9131 |= [d=def env=ienv state=istate]

9365 |= [d=def env=ienv state=istate]

9132 ^- iresult

9366 ^- iresult

9367+ =. gate-defs.state ~

9133 ?. ?=(%value -.d) [%| ["recursive definition is not a gate" ~]]

9368 ?. ?=(%value -.d) [%| ["recursive definition is not a gate" ~]]

9134 ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))

9369 ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))

9135 [%| ["recursive definition is not a gate" ~]]

9370 [%| ["recursive definition is not a gate" ~]]

@@ -9358,7 +9593,7 @@

9358 [%| ["recursive group contains duplicate names" ~]]

9593 [%| ["recursive group contains duplicate names" ~]]

9359 ?: (lien names |=(n=term ?=(^ (ienv-lookup n env))))

9594 ?: (lien names |=(n=term ?=(^ (ienv-lookup n env))))

9360 [%| ["recursive group shadows a name" ~]]

9595 [%| ["recursive group shadows a name" ~]]

9361− =/ scoped=istate state(globals (weld names globals.state))

9596+ =/ scoped=istate state(globals (weld names globals.state), gate-defs ~)

9362 =/ seeded=igate-seeds (seed-gate-group ds env scoped)

9597 =/ seeded=igate-seeds (seed-gate-group ds env scoped)

9363 ?: ?=(%| -.seeded) seeded

9598 ?: ?=(%| -.seeded) seeded

9364 =/ seeds=ienv (group-seed-env entries.p.seeded ~)

9599 =/ seeds=ienv (group-seed-env entries.p.seeded ~)

@@ -9392,7 +9627,7 @@

9392 `[entry u.rest]

9627 `[entry u.rest]

9393::

9628::

9394++ add-supported-defs

9629++ add-supported-defs

9395− |= [ds=(list def) 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)]

9630+ |= [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)]

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

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

9397 ?~ ds [env artifacts]

9632 ?~ ds [env artifacts]

9398 =/ d=def i.ds

9633 =/ d=def i.ds

@@ -9400,7 +9635,9 @@

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

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

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

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

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

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

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

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

9639+ =. gate-defs.initial checked

9640+ =. head-evidence.initial heads

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

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

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

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

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

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

@@ -9419,7 +9656,8 @@

9419 ?~ finalized $(ds t.ds)

9656 ?~ finalized $(ds t.ds)

9420 =? artifacts ?=(^ u.finalized)

9657 =? artifacts ?=(^ u.finalized)

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

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

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

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

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

9423::

9661::

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

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

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

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

@@ -9542,10 +9780,11 @@

9542 =/ graph=iadj (graph-make-forward ds nameset ~)

9780 =/ graph=iadj (graph-make-forward ds nameset ~)

9543 =/ components=icomponents (graph-components ds names)

9781 =/ components=icomponents (graph-components ds names)

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

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

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

9545 |-

9784 |-

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

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

9547− (add-supported-defs ds env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts)

9786+ (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)

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

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

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

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

9550 ?: =(env env.out) out

9789 ?: =(env env.out) out

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

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

@@ -10418,7 +10657,7 @@

10418 =/ source-unit=(unit ischeme)

10657 =/ source-unit=(unit ischeme)

10419 ?~ unit-decl ~

10658 ?~ unit-decl ~

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

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

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

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

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

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

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

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

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

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

@@ -10433,7 +10672,7 @@

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

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

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

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

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

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

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

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

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

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

10438 =/ usable=(unit imold-types)

10677 =/ usable=(unit imold-types)

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

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

@@ -10489,7 +10728,7 @@

10489 =? env-molds declared

10728 =? env-molds declared

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

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

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

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

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

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

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

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

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

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

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

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

@@ -11018,7 +11257,7 @@

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@@ -11052,7 +11291,7 @@

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@@ -11434,7 +11673,7 @@

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@@ -11490,7 +11729,7 @@

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@@ -11607,6 +11846,8 @@

11607 =/ resolution=iresolved (resolve-groups ds molds globals externals surs mark-externals marks jimports reserved-molds file prelude)

11846 =/ resolution=iresolved (resolve-groups ds molds globals externals surs mark-externals marks jimports reserved-molds file prelude)

11608 =/ cycles=(list icycle) (definite-value-cycles ds globals)

11847 =/ cycles=(list icycle) (definite-value-cycles ds globals)

11609 =/ env=ienv env.resolution

11848 =/ env=ienv env.resolution

11849+ =/ source-defs=(map term def) (direct-checked-gates ds env)

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

11610 =/ lines=(list @t) ~

11851 =/ lines=(list @t) ~

11611 |-

11852 |-

11612 ?~ ds (of-wain:format ['partial inference; module not checked' (flop lines)])

11853 ?~ ds (of-wain:format ['partial inference; module not checked' (flop lines)])

@@ -11626,7 +11867,9 @@

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

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

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

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

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

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

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

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

11871+ =. gate-defs.initial source-defs

11872+ =. head-evidence.initial heads

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

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

11631 =/ result=iresult

11874 =/ result=iresult

11632 ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))

11875 ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))

tests/lib/jibb-direct-gate-guards.hoonnew file+172

@@ -0,0 +1,172 @@

1+:: Direct layout evidence must retain provenance and final face constraints.

2+/+ jibb

3+|%

4+++ direct-evidence-errors

5+ ^- (list tape)

6+ =/ pre=@t '++ apply |= [f=$-([A B] B) n=@t] f\0a'

7+ =/ dupe=@t '++ apply |= [f=$-([A B] B) n=@t] f\0a++ apply |= [f=$-([A B] B) n=@t] f\0a'

8+ =/ root=@t '++ target |= [a=@t b=@p] b\0a++ main (apply target "x")\0a'

9+ =/ parsed (parse:jibb /tests/test/jibb root)

10+ ?> ?=(%& -.parsed)

11+ =/ ds=(list def:jibb) defs.p.parsed

12+ ?> ?=(^ ds)

13+ ?> ?=(^ t.ds)

14+ ?> ?=(%value -.i.t.ds)

15+ =/ expr=expr:jibb val.i.t.ds

16+ =? expr ?=(%group -.expr) inner.expr

17+ =/ txt=itype:jibb [%atom %t]

18+ =/ ship=itype:jibb [%atom %p]

19+ =/ target=itype:jibb [%fn [%cell [%face %a txt] [%face %b ship]] ship]

20+ =/ expected-fn=itype:jibb [%fn [%cell [%var 0] [%var 1]] [%var 1]]

21+ =/ expected-sample=itype:jibb [%cell [%face %f expected-fn] [%face %n txt]]

22+ =/ actual=itype:jibb [%cell target txt]

23+ =/ scheme=ischeme:jibb [[%fn expected-sample expected-fn] ~[0 1]]

24+ =/ changed=ischeme:jibb [[%fn expected-sample ship] ~[0 1]]

25+ =/ iface=ifile:jibb [~[[%apply scheme]] ~ /lib/jibb/prelude/jibb ~ ~ ~ `pre ~]

26+ =/ stale=ifile:jibb iface(values ~[[%apply changed]])

27+ =/ dup=ifile:jibb iface(source `dupe)

28+ =/ env=ienv:jibb ~[[%target [target ~]]]

29+ =/ registry=(map term def:jibb) (direct-checked-gates:jibb ds env)

30+ =/ evidence=(unit igate-prelude-evidence:jibb) (direct-prelude-evidence:jibb ds `iface)

31+ ?> ?=(^ evidence)

32+ =/ st=istate:jibb *istate:jibb

33+ =. st st(globals ~[%apply %target %main], prelude `iface, gate-defs registry, head-evidence evidence, next 10)

34+ =/ good=(unit ifit:jibb) (direct-gate-call-fit:jibb expr actual expected-sample env st)

35+ =/ bad=(unit ifit:jibb) (direct-gate-call-fit:jibb expr actual expected-sample env st(prelude `stale))

36+ =/ dupe-evidence=(unit igate-prelude-evidence:jibb) (direct-prelude-evidence:jibb ds `dup)

37+ =/ head=(unit def:jibb) (~(get by gates.u.evidence) %apply)

38+ ?> ?=(^ head)

39+ =/ head-sample=(unit sample:jibb) (direct-gate-sample:jibb u.head)

40+ ?> ?=(^ head-sample)

41+ ?> ?=(%cell -.u.head-sample)

42+ ?> ?=(%call -.expr)

43+ =/ pos=ifit:jibb (direct-positional-fit:jibb args.expr items.u.head-sample actual expected-sample env st ~ 10)

44+ =/ checks=(list @t)

45+ :~

46+ ?:(?=(%ok -.pos) 'positional-fit-ok' 'BAD-positional-fit')

47+ ?:(?=(^ good) 'original-evidence-usable' 'BAD-original-evidence')

48+ ?: &(?=(~ bad) =(source.iface source.stale) =(at.iface at.stale) !=(values.iface values.stale))

49+ 'changed-value-scheme-rejected'

50+ 'BAD-stale-evidence'

51+ ?:(?=(~ dupe-evidence) 'duplicate-source-rejected' 'BAD-duplicate-source')

52+ ==

53+

54+ ?: =(checks ~['positional-fit-ok' 'original-evidence-usable' 'changed-value-scheme-rejected' 'duplicate-source-rejected']) ~

55+ ~["direct-evidence-errors direct gate guard failed"]

56+++ late-face-errors

57+ ^- (list tape)

58+ =/ pre=@t '++ apply |= [first=[foo=A] second=A f=$-([C D] D)] f\0a'

59+ =/ dupe=@t '++ apply |= [f=$-([A B] B) n=@t] f\0a++ apply |= [f=$-([A B] B) n=@t] f\0a'

60+ =/ root=@t '++ target |= [a=@t b=@p] b\0a++ main (apply x y target)\0a'

61+ =/ parsed (parse:jibb /tests/test/jibb root)

62+ ?> ?=(%& -.parsed)

63+ =/ ds=(list def:jibb) defs.p.parsed

64+ ?> ?=(^ ds)

65+ ?> ?=(^ t.ds)

66+ ?> ?=(%value -.i.t.ds)

67+ =/ expr=expr:jibb val.i.t.ds

68+ =? expr ?=(%group -.expr) inner.expr

69+ =/ txt=itype:jibb [%atom %t]

70+ =/ ship=itype:jibb [%atom %p]

71+ =/ target=itype:jibb [%fn [%cell [%face %a txt] [%face %b ship]] ship]

72+ =/ expected-fn=itype:jibb [%fn [%cell [%var 1] [%var 2]] [%var 2]]

73+ =/ expected-sample=itype:jibb [%cell [%face %first [%face %foo [%var 0]]] [%cell [%face %second [%var 0]] [%face %f expected-fn]]]

74+ =/ actual=itype:jibb [%cell [%var 0] [%cell txt target]]

75+ =/ scheme=ischeme:jibb [[%fn expected-sample expected-fn] ~[0 1]]

76+ =/ changed=ischeme:jibb [[%fn expected-sample ship] ~[0 1]]

77+ =/ iface=ifile:jibb [~[[%apply scheme]] ~ /lib/jibb/prelude/jibb ~ ~ ~ `pre ~]

78+ =/ stale=ifile:jibb iface(values ~[[%apply changed]])

79+ =/ dup=ifile:jibb iface(source `dupe)

80+ =/ env=ienv:jibb ~[[%target [target ~]]]

81+ =/ registry=(map term def:jibb) (direct-checked-gates:jibb ds env)

82+ =/ evidence=(unit igate-prelude-evidence:jibb) (direct-prelude-evidence:jibb ds `iface)

83+ ?> ?=(^ evidence)

84+ =/ st=istate:jibb *istate:jibb

85+ =. st st(globals ~[%apply %target %main], prelude `iface, gate-defs registry, head-evidence evidence, next 10)

86+ =/ good=(unit ifit:jibb) (direct-gate-call-fit:jibb expr actual expected-sample env st)

87+ =/ bad=(unit ifit:jibb) (direct-gate-call-fit:jibb expr actual expected-sample env st(prelude `stale))

88+ =/ dupe-evidence=(unit igate-prelude-evidence:jibb) (direct-prelude-evidence:jibb ds `dup)

89+ =/ head=(unit def:jibb) (~(get by gates.u.evidence) %apply)

90+ ?> ?=(^ head)

91+ =/ head-sample=(unit sample:jibb) (direct-gate-sample:jibb u.head)

92+ ?> ?=(^ head-sample)

93+ ?> ?=(%cell -.u.head-sample)

94+ ?> ?=(%call -.expr)

95+ =/ pos=ifit:jibb (direct-positional-fit:jibb args.expr items.u.head-sample actual expected-sample env st ~ 10)

96+ =/ checks=(list @t)

97+ :~

98+ ?: ?=(%ok -.pos)

99+ ?:((itype-positional-slot-face-asym:jibb [%var 0] [%face %foo [%var 0]] sub.pos) 'LATE-FACE-ASYMMETRY' 'no-late-asymmetry')

100+ 'no-positional-fit'

101+ ?:(?=(%ok -.pos) 'positional-fit-ok' 'BAD-positional-fit')

102+ ?:(?=(^ good) 'original-evidence-usable' 'late-face-rejected')

103+ ?: &(?=(~ bad) =(source.iface source.stale) =(at.iface at.stale) !=(values.iface values.stale))

104+ 'changed-value-scheme-rejected'

105+ 'BAD-stale-evidence'

106+ ?:(?=(~ dupe-evidence) 'duplicate-source-rejected' 'BAD-duplicate-source')

107+ ==

108+

109+ ?: =(checks ~['LATE-FACE-ASYMMETRY' 'positional-fit-ok' 'late-face-rejected' 'changed-value-scheme-rejected' 'duplicate-source-rejected']) ~

110+ ~["late-face-errors direct gate guard failed"]

111+++ symmetric-face-errors

112+ ^- (list tape)

113+ =/ pre=@t '++ apply |= [first=[foo=A] second=A f=$-([C D] D)] f\0a'

114+ =/ dupe=@t '++ apply |= [f=$-([A B] B) n=@t] f\0a++ apply |= [f=$-([A B] B) n=@t] f\0a'

115+ =/ root=@t '++ target |= [a=@t b=@p] b\0a++ main (apply x y target)\0a'

116+ =/ parsed (parse:jibb /tests/test/jibb root)

117+ ?> ?=(%& -.parsed)

118+ =/ ds=(list def:jibb) defs.p.parsed

119+ ?> ?=(^ ds)

120+ ?> ?=(^ t.ds)

121+ ?> ?=(%value -.i.t.ds)

122+ =/ expr=expr:jibb val.i.t.ds

123+ =? expr ?=(%group -.expr) inner.expr

124+ =/ txt=itype:jibb [%atom %t]

125+ =/ ship=itype:jibb [%atom %p]

126+ =/ target=itype:jibb [%fn [%cell [%face %a txt] [%face %b ship]] ship]

127+ =/ expected-fn=itype:jibb [%fn [%cell [%var 1] [%var 2]] [%var 2]]

128+ =/ expected-sample=itype:jibb [%cell [%face %first [%face %foo [%var 0]]] [%cell [%face %second [%var 0]] [%face %f expected-fn]]]

129+ =/ actual=itype:jibb [%cell [%face %foo [%var 0]] [%cell txt target]]

130+ =/ scheme=ischeme:jibb [[%fn expected-sample expected-fn] ~[0 1]]

131+ =/ changed=ischeme:jibb [[%fn expected-sample ship] ~[0 1]]

132+ =/ iface=ifile:jibb [~[[%apply scheme]] ~ /lib/jibb/prelude/jibb ~ ~ ~ `pre ~]

133+ =/ stale=ifile:jibb iface(values ~[[%apply changed]])

134+ =/ dup=ifile:jibb iface(source `dupe)

135+ =/ env=ienv:jibb ~[[%target [target ~]]]

136+ =/ registry=(map term def:jibb) (direct-checked-gates:jibb ds env)

137+ =/ evidence=(unit igate-prelude-evidence:jibb) (direct-prelude-evidence:jibb ds `iface)

138+ ?> ?=(^ evidence)

139+ =/ st=istate:jibb *istate:jibb

140+ =. st st(globals ~[%apply %target %main], prelude `iface, gate-defs registry, head-evidence evidence, next 10)

141+ =/ good=(unit ifit:jibb) (direct-gate-call-fit:jibb expr actual expected-sample env st)

142+ =/ bad=(unit ifit:jibb) (direct-gate-call-fit:jibb expr actual expected-sample env st(prelude `stale))

143+ =/ dupe-evidence=(unit igate-prelude-evidence:jibb) (direct-prelude-evidence:jibb ds `dup)

144+ =/ head=(unit def:jibb) (~(get by gates.u.evidence) %apply)

145+ ?> ?=(^ head)

146+ =/ head-sample=(unit sample:jibb) (direct-gate-sample:jibb u.head)

147+ ?> ?=(^ head-sample)

148+ ?> ?=(%cell -.u.head-sample)

149+ ?> ?=(%call -.expr)

150+ =/ pos=ifit:jibb (direct-positional-fit:jibb args.expr items.u.head-sample actual expected-sample env st ~ 10)

151+ =/ checks=(list @t)

152+ :~

153+ ?: ?=(%ok -.pos)

154+ ?:((itype-positional-slot-face-asym:jibb [%face %foo [%var 0]] [%face %foo [%var 0]] sub.pos) 'LATE-FACE-ASYMMETRY' 'symmetric-after-later-binding')

155+ 'no-positional-fit'

156+ ?:(?=(%ok -.pos) 'positional-fit-ok' 'BAD-positional-fit')

157+ ?:(?=(^ good) 'original-evidence-usable' 'BAD-original-evidence')

158+ ?: &(?=(~ bad) =(source.iface source.stale) =(at.iface at.stale) !=(values.iface values.stale))

159+ 'changed-value-scheme-rejected'

160+ 'BAD-stale-evidence'

161+ ?:(?=(~ dupe-evidence) 'duplicate-source-rejected' 'BAD-duplicate-source')

162+ ==

163+

164+ ?: =(checks ~['symmetric-after-later-binding' 'positional-fit-ok' 'original-evidence-usable' 'changed-value-scheme-rejected' 'duplicate-source-rejected']) ~

165+ ~["symmetric-face-errors direct gate guard failed"]

166+++ direct-gate-guard-errors

167+ ^- (list tape)

168+ (weld direct-evidence-errors (weld late-face-errors symmetric-face-errors))

169+++ test-direct-gate-guards

170+ ^- tang

171+ (turn direct-gate-guard-errors |=(reason=tape leaf+reason))

172+--

tests/lib/jibb-direct-gate-source.hoonnew file+46

@@ -0,0 +1,46 @@

1+:: Exercise direct-source gate layouts through a synthetic program scaffold.

2+/+ jibb

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

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

5+/* source %txt /tests/type-direct-gate/source/txt

6+/* expected %txt /tests/type-direct-gate/expected/txt

7+|%

8+++ text

9+ |= lines=wain

10+ ^- @t

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

12+++ direct-gate-prepared

13+ |= [prelude=@t internal=@t]

14+ ^- (unit iprelude:jibb)

15+ :: This element is test-only; it does not prescribe a runtime shape.

16+ =/ extra=@t '\0a+$ element |$ [M] [%node item=M]\0a+$ program |$ [D X M]\0a [init=$-(D X) update=$-([M X] [X (list (cmd M))]) view=$-(X (element M)) subs=$-(X (list (sub M)))]\0a++ program |= [init=$-(D X) update=$-([M X] [X (list (cmd M))]) view=$-(X (element M)) subs=$-(X (list (sub M)))]\0a ^- (program D X M) [init update view subs]\0a++ choose-layout |= [f=$-([A B] C) value=[A B]] (f value)\0a++ higher |= [f=$-([@t [x=@t y=@p]] @t) marker=?] f\0a++ higher-generic |= [f=$-([@t X] X) state=X] state\0a'

17+ (prepare-prelude-with-internal:jibb (cat 3 prelude extra) internal)

18+++ direct-gate-source-output

19+ |= [src=@t prepared=(unit iprelude:jibb)]

20+ ^- @t

21+ (golden-types-with-prepared-prelude:jibb /tests/sub/client/jibb src ~ ~ ~ prepared)

22+++ direct-gate-projection-errors

23+ |= prepared=(unit iprelude:jibb)

24+ ^- (list tape)

25+ ?~ prepared ~["synthetic prelude did not prepare"]

26+ =/ src=@t '+$ message\0a %start\0a %stop\0a+$ record [count=@ud label=@t]\0a++ init-record |= input=@t ^- record [count=0 label=input]\0a++ view-record |= state=record ^- (element message) [%node %start]\0a++ subs-record |= state=record ^- (list (sub message)) ~\0a++ update-proj-good |= [msg=message state=record]\0a ^- [record (list (cmd message))]\0a [(proj [count=0 label="projected" extra=%.y]) ~]\0a++ program-projection (program init-record update-proj-good view-record subs-record)\0a'

27+ =/ out=jfile-result:jibb (infer-jibb-file:jibb /tests/direct/client/jibb src ~ ~ ~ ~[/tests/direct/client/jibb] values.u.prepared molds.u.prepared ~ `iface.u.prepared)

28+ ?: ?=(%| -.out) ~["projection-bearing module did not infer"]

29+ =/ defs=(list iwidth-definition:jibb) (skim elaborations.iface.p.out |=(d=iwidth-definition:jibb =(%update-proj-good name.d)))

30+ ?~ defs ~["projection-bearing update lost its elaboration"]

31+ ?~ projections.i.defs ~["projection action is missing"]

32+ ?: !=(1 (lent projections.i.defs)) ~["unexpected projection action count"]

33+ ?. =(steps.i.projections.i.defs ~[[%count 2] [%label 6]]) ~["projection axes changed"]

34+ ~

35+++ test-direct-gate-source

36+ ^- tang

37+ ?~ source ~[leaf+"direct gate source is missing"]

38+ ?~ expected ~[leaf+"direct gate expected output is missing"]

39+ =/ prepared=(unit iprelude:jibb) (direct-gate-prepared real-prelude real-internal)

40+ =/ errors=(list tape) (direct-gate-projection-errors prepared)

41+ ?^ errors (turn errors |=(reason=tape leaf+reason))

42+ =/ got=@t (direct-gate-source-output (text source) prepared)

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

44+ ~[leaf+"direct gate source output differs from its golden"]

45+ ~

46+--

tests/type-direct-gate/about.txtnew file+4

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

1+source: Grammar, Types and molds: “A body can't force two distinct capitals to be equal; use the same capital wherever a type must be shared.”

2+tests: A source-backed test prelude with a deliberately synthetic element and program exercises direct named and unnamed higher-order gates, record-valued models, nested field faces, incompatible samples, shared and distinct capitals, pending tags, aliases, captured and distinct capitals, equal-flattened source layouts, and projection-bearing bodies. It does not establish an island kind, runtime representation, or watchability.

3+expect: parses

4+expect-types: a partial inference report

tests/type-direct-gate/expected.txtnew file+86

@@ -0,0 +1,86 @@

1+partial inference; module not checked

2++$ message: cases proven disjoint; mold not checked

3+++ init: $-(@t @ud)

4+++ update: $-([msg=message state=@ud] [@ud (list (cmd message))])

5+++ view: $-(@ud [%node item=message])

6+++ subs: $-(@ud (list (sub message)))

7+++ direct: [init=$-(@t @ud) [update=$-([message @ud] [@ud (list (cmd message))]) [view=$-(@ud [%node item=message]) subs=$-(@ud (list (sub message)))]]]

8+++ wrong-init: $-(@p @ud)

9+++ different-data: [init=$-(@p @ud) [update=$-([message @ud] [@ud (list (cmd message))]) [view=$-(@ud [%node item=message]) subs=$-(@ud (list (sub message)))]]]

10+++ wrong-update: $-([msg=message state=@p] [@p (list (cmd message))])

11+++ mismatched-model: call constraint is not supported by partial inference

12+++ wrong-view: $-(@p [%node item=message])

13+++ mismatched-view: call constraint is not supported by partial inference

14+++ wrong-subs: $-(@p (list (sub message)))

15+++ mismatched-subs: call constraint is not supported by partial inference

16++$ other: cases proven disjoint; mold not checked

17+++ wrong-msg-update: $-([msg=other state=@ud] [@ud (list (cmd other))])

18+++ mismatched-message: call constraint is not supported by partial inference

19+++ pending: tag needs context in partial inference

20+++ program-value: $-([init=$-(A B) [update=$-([C B] [B (list (cmd C))]) [view=$-(B [%node item=C]) subs=$-(B (list (sub C)))]]] [init=$-(A B) [update=$-([C B] [B (list (cmd C))]) [view=$-(B [%node item=C]) subs=$-(B (list (sub C)))]]])

21+++ update-unfaced: $-([message @ud] [@ud (list (cmd message))])

22+++ direct-unfaced: [init=$-(@t @ud) [update=$-([message @ud] [@ud (list (cmd message))]) [view=$-(@ud [%node item=message]) subs=$-(@ud (list (sub message)))]]]

23++$ record: not checked

24+++ init-record: $-(@t [count=@ud label=@t])

25+++ update-record: $-([msg=message state=[count=@ud label=@t]] [[count=@ud label=@t] (list (cmd message))])

26+++ update-record-unfaced: $-([message [count=@ud label=@t]] [[count=@ud label=@t] (list (cmd message))])

27+++ view-record: $-([count=@ud label=@t] [%node item=message])

28+++ subs-record: $-([count=@ud label=@t] (list (sub message)))

29+++ program-record: [init=$-(@t [count=@ud label=@t]) [update=$-([message [count=@ud label=@t]] [[count=@ud label=@t] (list (cmd message))]) [view=$-([count=@ud label=@t] [%node item=message]) subs=$-([count=@ud label=@t] (list (sub message)))]]]

30+++ program-record-unfaced: [init=$-(@t [count=@ud label=@t]) [update=$-([message [count=@ud label=@t]] [[count=@ud label=@t] (list (cmd message))]) [view=$-([count=@ud label=@t] [%node item=message]) subs=$-([count=@ud label=@t] (list (sub message)))]]]

31+++ bad-update-record: $-([msg=message state=[other=@ud label=@t]] [[count=@ud label=@t] (list (cmd message))])

32+++ program-wrong-nested-face: call constraint is not supported by partial inference

33+++ update-pending: tag needs context in partial inference

34+++ program-pending: name is not available to partial inference

35+++ update-proj: $-([msg=message state=[count=@ud [label=@t extra=?]]] [[count=@ud label=@t] (list (cmd message))])

36+++ pass-fn: $-($-([A B] C) $-([A B] C))

37+++ pass-named: $-([msg=message state=@ud] [@ud (list (cmd message))])

38+++ pass-unnamed: $-([message @ud] [@ud (list (cmd message))])

39+++ forced-same: $-($-([A A] @t) $-([A A] @t))

40+++ forced-distinct: distinct type variables `A` and `B` must not be forced equal; use the same capital for a shared type

41+/tests/sub/client.jibb:55:29: first type variable

42+++ forced-distinct |= f=$-([A B] @t) (forced-same f)

43+ ^

44+/tests/sub/client.jibb:55:31: second type variable

45+++ forced-distinct |= f=$-([A B] @t) (forced-same f)

46+ ^

47+++ known-label: $-($-([left=@t right=@p] @ud) $-([left=@t right=@p] @ud))

48+++ matching-label: $-([left=@t right=@p] @ud)

49+++ different-label: $-([x=@t y=@p] @ud)

50+++ match-label: $-([left=@t right=@p] @ud)

51+++ mismatch-label: call's sample and argument types do not unify

52+/tests/sub/client.jibb:60:20: called gate has type $-($-([left=@t right=@p] @ud) $-([left=@t right=@p] @ud))

53+++ mismatch-label (known-label different-label)

54+ ^

55+/tests/sub/client.jibb:60:32: argument has type $-([x=@t y=@p] @ud)

56+++ mismatch-label (known-label different-label)

57+ ^

58+++ unknown-call: $-($-([A B] C) $-([A B] C))

59+++ update-proj-good: $-([msg=message state=[count=@ud label=@t]] [[count=@ud label=@t] (list (cmd message))])

60+++ program-projection: [init=$-(@t [count=@ud label=@t]) [update=$-([message [count=@ud label=@t]] [[count=@ud label=@t] (list (cmd message))]) [view=$-([count=@ud label=@t] [%node item=message]) subs=$-([count=@ud label=@t] (list (sub message)))]]]

61+++ program-alias: $-([init=$-(A B) [update=$-([C B] [B (list (cmd C))]) [view=$-(B [%node item=C]) subs=$-(B (list (sub C)))]]] [init=$-(A B) [update=$-([C B] [B (list (cmd C))]) [view=$-(B [%node item=C]) subs=$-(B (list (sub C)))]]])

62+++ through-head-alias: call constraint is not supported by partial inference

63+++ update-alias: $-([msg=message state=@ud] [@ud (list (cmd message))])

64+++ through-arg-alias: call constraint is not supported by partial inference

65+++ select-update: branch tag or union context is not supported by partial inference

66+++ through-branch: name is not available to partial inference

67+++ local-shadow: sample shadows a name

68+++ nested-layout: $-([a=@t [x=@t y=@p]] @t)

69+++ flat-layout: $-([a=@t [x=@t y=@p]] @t)

70+++ nested-accept: call constraint is not supported by partial inference

71+++ flat-accept: call constraint is not supported by partial inference

72+++ higher-nested: $-([@t [x=@t y=@p]] @t)

73+++ higher-flat: $-([@t [x=@t y=@p]] @t)

74+++ nested-ret: $-([a=@t [x=@t y=@p]] [x=@t y=@p])

75+++ flat-ret: $-([a=@t [x=@t y=@p]] [x=@t y=@p])

76+++ higher-generic-nested: [x=@t y=@p]

77+++ higher-generic-flat: call constraint is not supported by partial inference

78+++ global-id: $-(A A)

79+++ capture-good: $-([a=@t state=A] A)

80+++ capture-text: @t

81+++ capture-ship: @p

82+++ capture-bad: $-([a=A state=B] A)

83+++ capture-distinct: call constraint is not supported by partial inference

84+++ capture-caller: call constraint is not supported by partial inference

85+++ capture-local: call constraint is not supported by partial inference

86+++ capture-distinct-caller: call constraint is not supported by partial inference

tests/type-direct-gate/source.txtnew file+96

@@ -0,0 +1,96 @@

1++$ message

2+ %start

3+ %stop

4+++ init |= input=@t ^- @ud 1

5+++ update |= [msg=message state=@ud]

6+ ^- [@ud (list (cmd message))] [state ~]

7+++ view |= state=@ud ^- (element message) [%node %start]

8+++ subs |= state=@ud ^- (list (sub message)) ~

9+++ direct (program init update view subs)

10+++ wrong-init |= input=@p ^- @ud 1

11+++ different-data (program wrong-init update view subs)

12+++ wrong-update |= [msg=message state=@p]

13+ ^- [@p (list (cmd message))] [state ~]

14+++ mismatched-model (program init wrong-update view subs)

15+++ wrong-view |= state=@p ^- (element message) [%node %start]

16+++ mismatched-view (program init update wrong-view subs)

17+++ wrong-subs |= state=@p ^- (list (sub message)) ~

18+++ mismatched-subs (program init update view wrong-subs)

19++$ other

20+ %start

21+ %stop

22+++ wrong-msg-update |= [msg=other state=@ud]

23+ ^- [@ud (list (cmd other))] [state ~]

24+++ mismatched-message (program init wrong-msg-update view subs)

25+++ pending

26+ ~& %unrelated

27+ (program init update view subs)

28+++ program-value program

29+++ update-unfaced |= input=[message @ud]

30+ ^- [@ud (list (cmd message))] [0 ~]

31+++ direct-unfaced (program init update-unfaced view subs)

32++$ record [count=@ud label=@t]

33+++ init-record |= input=@t ^- record [count=0 label=input]

34+++ update-record |= [msg=message state=record]

35+ ^- [record (list (cmd message))] [state ~]

36+++ update-record-unfaced |= args=[message record]

37+ ^- [record (list (cmd message))] [[count=0 label=""] ~]

38+++ view-record |= state=record ^- (element message) [%node %start]

39+++ subs-record |= state=record ^- (list (sub message)) ~

40+++ program-record (program init-record update-record view-record subs-record)

41+++ program-record-unfaced (program init-record update-record-unfaced view-record subs-record)

42+++ bad-update-record |= [msg=message state=[other=@ud label=@t]]

43+ ^- [record (list (cmd message))] [[count=0 label=""] ~]

44+++ program-wrong-nested-face (program init-record bad-update-record view-record subs-record)

45+++ update-pending |= [msg=message state=record]

46+ ~& %orphan

47+ ^- [record (list (cmd message))] [state ~]

48+++ program-pending (program init-record update-pending view-record subs-record)

49+++ update-proj |= [msg=message state=[count=@ud label=@t extra=?]]

50+ ^- [record (list (cmd message))] [(proj state) ~]

51+++ pass-fn |= f=$-([A B] C) f

52+++ pass-named (pass-fn update)

53+++ pass-unnamed (pass-fn update-unfaced)

54+++ forced-same |= f=$-([A A] @t) f

55+++ forced-distinct |= f=$-([A B] @t) (forced-same f)

56+++ known-label |= f=$-([left=@t right=@p] @ud) f

57+++ matching-label |= [left=@t right=@p] ^- @ud 0

58+++ different-label |= [x=@t y=@p] ^- @ud 0

59+++ match-label (known-label matching-label)

60+++ mismatch-label (known-label different-label)

61+++ unknown-call |= f (pass-fn f)

62+++ update-proj-good |= [msg=message state=record]

63+ ^- [record (list (cmd message))]

64+ [(proj [count=0 label="projected" extra=%.y]) ~]

65+++ program-projection (program init-record update-proj-good view-record subs-record)

66+++ program-alias program

67+++ through-head-alias (program-alias init update view subs)

68+++ update-alias update

69+++ through-arg-alias (program init update-alias view subs)

70+++ select-update |= flag=?

71+ ?- flag

72+ %.y update

73+ %.n update-unfaced

74+++ through-branch (program init (select-update %.y) view subs)

75+++ local-shadow |= update (program init update view subs)

76+++ nested-layout |= [a=@t [x=@t y=@p]] a

77+++ flat-layout |= [a=@t x=@t y=@p] a

78+++ nested-accept (choose-layout nested-layout ["first" ["second" ~zod]])

79+++ flat-accept (choose-layout flat-layout ["first" ["second" ~zod]])

80+++ higher-nested (higher nested-layout %.y)

81+++ higher-flat (higher flat-layout %.y)

82+++ nested-ret |= [a=@t [x=@t y=@p]] [x=x y=y]

83+++ flat-ret |= [a=@t x=@t y=@p] [x=x y=y]

84+++ higher-generic-nested (higher-generic nested-ret [x="two" y=~zod])

85+++ higher-generic-flat (higher-generic flat-ret [x="two" y=~zod])

86+++ global-id |= x=A x

87+++ capture-good |= [a=@t state=A] (global-id state)

88+++ capture-text (higher-generic capture-good "hello")

89+++ capture-ship (higher-generic capture-good ~zod)

90+++ capture-bad |= [a=A state=B] (global-id a)

91+++ capture-distinct (higher-generic capture-bad ~zod)

92+++ capture-caller |= value=A (higher-generic capture-good value)

93+++ capture-local |= value=A

94+ ++ local-function |= [a=@t state=A] value

95+ (higher-generic local-function value)

96+++ capture-distinct-caller |= [left=A right=B] ^- B (higher-generic capture-good left)

tools/testdata/ship-selftest+5

@@ -312,6 +312,8 @@ def generator_checks(tmp):

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

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

314 'tests/lib/jibb-closed-gate-guards.hoon',

315+ 'tests/lib/jibb-direct-gate-guards.hoon',

316+ 'tests/lib/jibb-direct-gate-source.hoon',

315 'tests/lib/jibb-todo-api.hoon',

317 'tests/lib/jibb-todo-api.hoon',

316 'tests/lib/jibb-constructor-fit-guards.hoon',

318 'tests/lib/jibb-constructor-fit-guards.hoon',

317 'tests/lib/jibb-sub-guards.hoon',

319 'tests/lib/jibb-sub-guards.hoon',

@@ -319,6 +321,9 @@ def generator_checks(tmp):

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

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

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

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

321 <= normal_tests, sorted(normal_tests))

323 <= normal_tests, sorted(normal_tests))

324+ check('direct gate source and golden are assembled',

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

326+ <= set(normal.files))

322 for label, kwargs in (('custom library', {'lib': STUB}),

327 for label, kwargs in (('custom library', {'lib': STUB}),

323 ('custom goldens', {'golden': CASES}),

328 ('custom goldens', {'golden': CASES}),

324 ('both overrides', {'lib': STUB, 'golden': CASES})):

329 ('both overrides', {'lib': STUB, 'golden': CASES})):

tools/type-direct-gate-testnew file+64

@@ -0,0 +1,64 @@

1+#!/usr/bin/env python3

2+"""Check source-backed direct gate layouts and provenance under eval."""

3+from pathlib import Path

4+import argparse

5+import difflib

6+import subprocess

7+import sys

8+import tempfile

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

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

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

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

14+args = parser.parse_args()

15+fixture = root / 'tests/type-direct-gate'

16+prelude = root / 'jibb-dev/lib/jibb/prelude.jibb'

17+internal = root / 'jibb-dev/lib/jibb/internal.jibb'

18+

19+def body(name):

20+ text = (root / 'tests/lib' / name).read_text()

21+ return text[text.index('\n|%\n') + 1:]

22+

23+def run(program, cords=()):

24+ with tempfile.TemporaryDirectory(prefix='jibb-direct-gate-') as tmp:

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

26+ path.write_text(program)

27+ return subprocess.run([str(root / 'tools/hoon'), '--lib', args.lib, '--raw',

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

29+

30+source_program = ('=/ jibb .\n=/ real-prelude=@t prelude\n=/ real-internal=@t internal\n'

31+ '=/ source=wain (to-wain:format source-text)\n=/ expected=wain ~\n'

32+ '=/ suite\n' + body('jibb-direct-gate-source.hoon') +

33+ '\n^- @t\n=/ prepared=(unit iprelude:jibb) (direct-gate-prepared:suite real-prelude real-internal)\n'

34+ '=/ failures=(list tape) (direct-gate-projection-errors:suite prepared)\n'

35+ '?~ failures (direct-gate-source-output:suite source-text prepared)\n'

36+ '(of-wain:format (turn failures crip))\n')

37+result = run(source_program, ['--cord', 'source-text=' + str(fixture / 'source.txt'),

38+ '--cord', 'prelude=' + str(prelude),

39+ '--cord', 'internal=' + str(internal)])

40+if result.returncode:

41+ sys.exit(result.returncode)

42+expected_path = fixture / 'expected.txt'

43+if args.update:

44+ expected_path.write_bytes(result.stdout)

45+else:

46+ expected = expected_path.read_bytes()

47+ if result.stdout != expected:

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

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

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

51+ fromfile='expected.txt', tofile='actual types'))

52+ sys.exit(1)

53+

54+guard_program = ('=/ jibb .\n=/ suite\n' + body('jibb-direct-gate-guards.hoon') +

55+ '\n=/ failures=(list tape) direct-gate-guard-errors:suite\n^- @t\n'

56+ "?~ failures 'direct gate guards passed'\n"

57+ '(of-wain:format (turn failures crip))\n')

58+result = run(guard_program)

59+if result.returncode:

60+ sys.exit(result.returncode)

61+if result.stdout != b'direct gate guards passed\n':

62+ sys.stderr.buffer.write(result.stdout)

63+ sys.exit(1)

64+print('direct gate source and provenance guards passed')