git.iko.soy/jibb
on master help sign in
Infer direct higher-order gates from source

Use checked source sample layouts to fit direct named gates while preserving nested record faces. Require closed final call samples and replay the fit under the final substitution; retain projection evidence and reject stale source interfaces. Exercise source provenance, ambiguous layouts, late-bound faces and projection actions under eval and on the ship. This remains partial inference, not island checking.

commit651b8ec0ffe0f983df715df116f09d4cd04de31a authoriko <mail@iko.soy> dateSat 31 Oct 2026, 12:18 (9 hours ago) parent706035c
11 files changed+745−18
compare with master
unifiedsplit
docs/compiler.md+7−1 docs/development.md+2 docs/status.md+5−2 jibb-dev/lib/jibb.hoon+258−15 tests/lib/jibb-direct-gate-guards.hoon+172 tests/lib/jibb-direct-gate-source.hoon+46 tests/type-direct-gate/about.txt+4 tests/type-direct-gate/expected.txt+86 tests/type-direct-gate/source.txt+96 tools/testdata/ship-selftest+5 tools/type-direct-gate-test+64
docs/compiler.md+7−1
@@ -56,7 +56,13 @@ The core is split into chapters, `+| %name`, in this order:
5656| `%span-check` | `+check-spans`, which `+golden` runs on every tree, and `+check-spans-test` |
5757| `%type-inference` | The initial inference fragment and its unification helpers; not yet a module type checker |
5858
59−The inference fragment supports fixed auras, unrestricted `@`, one-way widening into it and toward aura-family ancestors, generic variables and gates, faced and unfaced cells, cell sample binders, known record field reads, a cell pattern of two or more binders, a complete two-arm loobean branch, a complete two-arm unit-shaped branch, closed local mold aliases and acyclic forward value references. For a supported single syntactic top-level recursive gate, the checker infers the sample first and uses that exact sample, including its field faces, in a monomorphic self placeholder. The completed body must unify with the placeholder before the gate is generalized; incompatible recursive arguments can report the call and argument sites. Uses of generalized top-level definitions instantiate their schemes independently. For a complete loobean branch with one direct self-call arm, the checker can infer the other arm independently and use its closed, fully resolved type to seed the recursive result; it then checks the whole body. Open or pending base types do not seed the result, and other branch shapes still depend on the existing partial inference. A supported single local recursive gate also uses a monomorphic self reference while its body is checked, then generalizes variables free of its enclosing environment; captured variables remain shared. Acyclic local value definitions can refer forward. The checker collects written capitals per `++` before inference, excluding nested definitions: a capital used in an enclosing definition is shared with its locals, even when written later, while a capital introduced only in a local definition is generalized there. Sibling locals can introduce independent capitals with the same spelling; generic mold parameters keep their own scope. Top-level groups of syntactic gates are inferred together with monomorphic placeholders and shared substitutions, then generalized only after the whole group checks; downstream uses and library interfaces instantiate those schemes independently. A dependency graph identifies groups with two iterative depth-first passes; its conservative local-reference edges can reject otherwise valid programs. Supported local mutually recursive gate groups also use shared monomorphic placeholders and generalize only after the group checks, preserving captured outer variables. Some proven non-gate value cycles are diagnosed; other mixed gate/value cycles, polymorphic recursion, unresolved literal constraints and unresolved branch joins remain unsupported. Acyclic simple local mold aliases can also refer forward, and are scoped to the body, not its gate's sample. Nonrecursive generic aliases of supported molds can be applied at exact arity, including locally and through library interfaces; their parameters are lexical. Closed, provably disjoint nonrecursive unions and tagged single-case molds support contextual term values, `~` and `|=%tag` constructors. Literal heads compare by their runtime noun, so `|=%$` can construct an explicit null-, loobean-zero- or term-zero-headed case. Equal heads with distinct payloads can be selected when exactly one payload fit is proven; unknown or ambiguous alternatives remain unsupported. Unresolved tags and nulls remain pending, with distinct partial-inference diagnostics. Nonrecursive top-level generic union molds with provably disjoint cases also support contextual tags and constructors at exact arity; their arguments are retained through generalization and supported library interfaces. Nonrecursive generic aliases can reorder, repeat or omit parameters while preserving a supported union’s origin, including through local scopes and library interfaces. A generic union declared directly inside a body and recursive molds remain unsupported. A directly known named union can instantiate an unconstrained generic gate sample while retaining its origin, generic arguments and faces. Unnamed, pending-tag, recursive, unknown-atom and variable-bound union origins remain unsupported. A value with type variable `A` can fit a field whose type is that same `A`, including in generic union payloads and nested or repeated record fields. A differing-variable face constraint remains unsupported. When inference forces two distinct explicitly written capitals equal, it reports both source sites; forcing a capital to a concrete type remains unsupported in this fragment. It can infer and generalize atom constraints arising from explicit capitals or bare sample binders, preserve those constraints through aliases, instantiate them independently, and print multiple constraints. Unresolved decimal variables default to `@ud` for inferred types without gates; defaulting inside gate types and other constraint cases remain incomplete. It does not yet check a module, complete imports, general patterns, general deferred constraints, recursive molds, dependency cycles or most errors with both conflicting excerpts. Definite cast and call mismatches, incompatible branches and overlapping union cases report both sites and excerpts. Concrete branch results can join at an explicitly present parent aura or `@`. Some known tuple and record positions acquire matching faces; other variable-dependent face merges, general branch tag context and ambiguous call-result propagation remain unsupported; function compatibility involving nested `@` and variable-dependent joins remain unsupported except for equal types. 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.
6066
6167A 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.
6268
docs/development.md+2
@@ -74,6 +74,7 @@ git clone https://github.com/urbit/tools /root/src/tools
7474| `tools/type-positional-face-guards-test` | Runs positional-call and nested-face guards under eval and on the ship |
7575| `tools/type-qath-guards-test` | Runs source-provenance, recursive unfolding and face guards under eval and on the ship |
7676| `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 |
7778| `tools/type-closed-gate-guards-test` | Checks closed gate sample labels and face uncertainty under eval and on the ship |
7879| `tools/type-constructor-fit-guards-test` | Checks constructor-case uncertainty and known mismatches under eval and on the ship |
7980| `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
114115tools/type-positional-face-guards-test # positional sample face guards pass
115116tools/type-qath-guards-test # qath source and unfolding guards pass
116117tools/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
117119tools/type-closed-gate-guards-test # closed gate fit guards pass
118120tools/type-constructor-fit-guards-test # constructor fit guards pass
119121tools/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
3131
3232A 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.
3333
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+
3436The 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.
3537
3638For 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:
6264Besides the plan's list:
6365
6466- 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.
6668- `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.
6769- 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.
6870- 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:
158160| a1c5f35 | 2026-10-31 | Infer supported multi-path requests and named closed folds |
159161| 911ca0c | 2026-10-31 | Propagate union context, define subscriptions and match literal nouns |
160162| 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 |
162165
163166## Checking it
164167
jibb-dev/lib/jibb.hoon+258−15
@@ -5674,7 +5674,8 @@
56745674 %jrec [%yes & fuel ~]
56755675 ==
56765676::
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)]
5677++$ igate-prelude-evidence [iface=ifile gates=(map term def)]
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)]
56785679+$ idiag [msg=tape sites=(list [at=span note=tape])]
56795680+$ iresult (each [typ=itype state=istate] idiag)
56805681+$ isample-result (each [typ=itype env=ienv state=istate] tape)
@@ -8257,6 +8258,234 @@
82578258 ?: ?=(%| -.out) [%| p.out]
82588259 [%& [e typ.p.out sub.state.p.out (flop projections.state.p.out)]]
82598260::
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+::
82608489++ infer-call-with-head
82618490 |= [e=expr env=ienv state=istate head=iresult]
82628491 ^- iresult
@@ -8283,6 +8512,10 @@
82838512 =/ fit=ifit
82848513 ?^ t.args.e (itype-fit-inner typ.p.arg sample.ht sub.st next.st & |)
82858514 (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)
82868519 ?: ?=(%unknown -.fit) [%| ["call constraint is not supported by partial inference" ~]]
82878520 ?: ?=(%bad -.fit)
82888521 ?~ t.args.e
@@ -8299,6 +8532,7 @@
82998532 =/ arg-type=itype ?~(bad typ.p.arg typ.u.bad)
83008533 [%| ["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)]]]]
83018534 =/ face-asym=?
8535+ ?^ direct |
83028536 ?^ t.args.e (itype-positional-face-asym args.e typ.p.arg sample.ht sub.fit)
83038537 (itype-face-asym typ.p.arg sample.ht sub.fit)
83048538 ?: &((itype-has-face typ.p.arg sub.fit) face-asym (itype-output-may-be-cell product.ht sub.fit))
@@ -9130,6 +9364,7 @@
91309364++ infer-recursive-gate
91319365 |= [d=def env=ienv state=istate]
91329366 ^- iresult
9367+ =. gate-defs.state ~
91339368 ?. ?=(%value -.d) [%| ["recursive definition is not a gate" ~]]
91349369 ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
91359370 [%| ["recursive definition is not a gate" ~]]
@@ -9358,7 +9593,7 @@
93589593 [%| ["recursive group contains duplicate names" ~]]
93599594 ?: (lien names |=(n=term ?=(^ (ienv-lookup n env))))
93609595 [%| ["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 ~)
93629597 =/ seeded=igate-seeds (seed-gate-group ds env scoped)
93639598 ?: ?=(%| -.seeded) seeded
93649599 =/ seeds=ienv (group-seed-env entries.p.seeded ~)
@@ -9392,7 +9627,7 @@
93929627 `[entry u.rest]
93939628::
93949629++ 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)]
93969631 ^- [env=ienv artifacts=(list iwidth-definition)]
93979632 ?~ ds [env artifacts]
93989633 =/ d=def i.ds
@@ -9400,7 +9635,9 @@
94009635 ?. (unique-value-name name.d globals) $(ds t.ds)
94019636 ?^ (ienv-lookup name.d env) $(ds t.ds)
94029637 =/ 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
94049641 =. initial (reserve-def-caps val.d initial)
94059642 =/ result=iresult (infer-fragment val.d env initial)
94069643 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
@@ -9419,7 +9656,8 @@
94199656 ?~ finalized $(ds t.ds)
94209657 =? artifacts ?=(^ u.finalized)
94219658 [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]
9422− $(ds t.ds, env [[name.d [typ vars]] env])
9659+ =? checked |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) (~(put by checked) name.d d)
9660+ $(ds t.ds, env [[name.d [typ vars]] env], checked checked)
94239661::
94249662+$ iresolved [env=ienv grouped=(list term) artifacts=(list iwidth-definition)]
94259663+$ iadj (map term (list term))
@@ -9542,10 +9780,11 @@
95429780 =/ graph=iadj (graph-make-forward ds nameset ~)
95439781 =/ components=icomponents (graph-components ds names)
95449782 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9783+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)
95459784 |-
95469785 =/ 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)
9548− =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~]
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)
9787+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~]
95499788 =/ out=iresolved (add-groups ds components graph env.next grouped artifacts.next initial)
95509789 ?: =(env env.out) out
95519790 $(env env.out, grouped grouped.out, artifacts artifacts.out)
@@ -10418,7 +10657,7 @@
1041810657 =/ source-unit=(unit ischeme)
1041910658 ?~ unit-decl ~
1042010659 =/ 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 ~ ~ ~]
1042210661 =/ unit-types=imold-types (partial-prelude-molds unit-molds unit-state)
1042310662 =/ unit-iface=ifile [~ unit-types /lib/jibb/prelude/jibb ~ ~ ~ ~ ~]
1042410663 =/ found=(unit ischeme) (find-jibb-mold %unit unit-iface)
@@ -10433,7 +10672,7 @@
1043310672 =/ js=ijimports ~[[face.i.imports.mod primitive]]
1043410673 =/ reserved=(list term) ~[face.i.imports.mod]
1043510674 =/ 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 ~ ~ ~]
1043710676 =/ mts=(each imold-types @t) (module-mold-types molds state)
1043810677 =/ usable=(unit imold-types)
1043910678 ?: ?=(%& -.mts) `p.mts
@@ -10489,7 +10728,7 @@
1048910728 =? env-molds declared
1049010729 (skim molds |=(m=[name=term body=shape] !=(%list name.m)))
1049110730 =/ 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 ~ ~ ~]
1049310732 :: Other prelude molds may use list only after its source has passed
1049410733 :: the standard-list check. The raw declaration remains removed.
1049510734 =/ declared-list=(unit shape) (find-simple-mold %list molds)
@@ -11018,7 +11257,7 @@
1101811257 =/ surs=(list term) (collect-sur-imports imports.mod)
1101911258 =/ reserved=(list term) (weld molds.prep (turn resolved.p.deps |=(j=[face=term interface=ifile] face.j)))
1102011259 =/ 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 ~ ~ ~]
1102211261 =/ mts=(each imold-types @t) (module-mold-types molds state)
1102311262 ?: ?=(%| -.mts) [%| p.mts]
1102411263 =/ resolution=iresolved (resolve-groups ordinary molds globals externals surs marks declared resolved.p.deps reserved file prelude)
@@ -11052,7 +11291,7 @@
1105211291 =/ surs=(list term) (collect-sur-imports imports.mod)
1105311292 =/ reserved=(list term) (weld molds.prep (turn resolved.p.deps |=(j=[face=term interface=ifile] face.j)))
1105411293 =/ 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 ~ ~ ~]
1105611295 =/ mts=(each imold-types @t) (module-mold-types molds state)
1105711296 ?: ?=(%| -.mts) [%| p.mts]
1105811297 =/ resolution=iresolved (resolve-groups ordinary molds globals externals surs marks declared resolved.p.deps reserved file prelude)
@@ -11434,7 +11673,7 @@
1143411673 =/ marks=(list term) (collect-mark-imports imports.mod)
1143511674 =/ reserved=(list term) (weld prelude-molds (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
1143611675 =/ 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 ~ ~ ~]
1143811677 =/ mts=(each imold-types @t) (module-mold-types molds state)
1143911678 ?: ?=(%| -.mts) [%| (crip "{(trip p.mts)}: {(spud at)}")]
1144011679 =/ resolution=iresolved (resolve-groups defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
@@ -11490,7 +11729,7 @@
1149011729 =/ declared=(list term) (collect-mark-imports imports.mod)
1149111730 =/ reserved=(list term) (weld molds.u.prepared (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
1149211731 =/ 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 ~ ~ ~]
1149411733 =/ inferred=(unit [template=ischeme state=istate])
1149511734 (infer-mold-template shape.i.selected state(active ~[name], in-mold &))
1149611735 ?~ inferred [%| 'selected mold needs unsupported inference']
@@ -11607,6 +11846,8 @@
1160711846 =/ resolution=iresolved (resolve-groups ds molds globals externals surs mark-externals marks jimports reserved-molds file prelude)
1160811847 =/ cycles=(list icycle) (definite-value-cycles ds globals)
1160911848 =/ 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)
1161011851 =/ lines=(list @t) ~
1161111852 |-
1161211853 ?~ ds (of-wain:format ['partial inference; module not checked' (flop lines)])
@@ -11626,7 +11867,9 @@
1162611867 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype typ ~)}{(show-atom-constraint typ)}")
1162711868 $(ds t.ds, lines [line lines])
1162811869 =/ 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
1163011873 =. initial (reserve-def-caps val.d initial)
1163111874 =/ result=iresult
1163211875 ?: |(?=(%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):
312312 'tests/lib/jibb-ask-guards.hoon',
313313 'tests/lib/jibb-request-guards.hoon',
314314 'tests/lib/jibb-closed-gate-guards.hoon',
315+ 'tests/lib/jibb-direct-gate-guards.hoon',
316+ 'tests/lib/jibb-direct-gate-source.hoon',
315317 'tests/lib/jibb-todo-api.hoon',
316318 'tests/lib/jibb-constructor-fit-guards.hoon',
317319 'tests/lib/jibb-sub-guards.hoon',
@@ -319,6 +321,9 @@ def generator_checks(tmp):
319321 'tests/lib/jibb-gate-free-guards.hoon',
320322 'tests/lib/jibb-gate-free-source.hoon'}
321323 <= 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))
322327 for label, kwargs in (('custom library', {'lib': STUB}),
323328 ('custom goldens', {'golden': CASES}),
324329 ('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
9+
10+root = Path(__file__).resolve().parent.parent
11+parser = argparse.ArgumentParser(description=__doc__)
12+parser.add_argument('--lib', default=str(root / 'jibb-dev/lib/jibb.hoon'))
13+parser.add_argument('--update', action='store_true')
14+args = parser.parse_args()
15+fixture = root / 'tests/type-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')