@@ -774,39 +774,38 @@
774774:: (face 2:11 items
775775:: (apply 2:17 list (aura 2:23 @t)))
776776:: (face 2:27 open (flag 2:32))))
777−:: (mold 3:1 cart-action
777+:: (mold 3:1 poke
778778:: (union 4:3
779779:: (cell 4:3
780780:: (const 4:4 %add)
781781:: (face 4:9 item (aura 4:14 @t)))
782782:: (const 5:3 %toggle)))
783−:: (mold 6:1 poke (ref 6:9 cart-action))
784−:: (value 8:1 main
785−:: (group 8:9
786−:: (call 8:10 (wing 8:10 store) (wing 8:16 init) (wing 8:21 update))))
787−:: (value 9:1 init
788−:: (cast 9:9
789−:: (ref 9:12 state)
790−:: (tuple 9:18 (lit 9:19 ~) (lit 9:21 %.n))))
791−:: (value 10:1 update
792−:: (gate 10:11
793−:: (cell 10:14
794−:: (face 10:15 a (ref 10:17 cart-action))
795−:: (face 10:29 s (ref 10:31 state)))
796−:: (body 11:3
797−:: (branch 11:3
798−:: (wing 11:6 a)
783+:: (value 7:1 main
784+:: (group 7:9
785+:: (call 7:10 (wing 7:10 store) (wing 7:16 init) (wing 7:21 update))))
786+:: (value 8:1 init
787+:: (cast 8:9
788+:: (ref 8:12 state)
789+:: (tuple 8:18 (lit 8:19 ~) (lit 8:21 %.n))))
790+:: (value 9:1 update
791+:: (gate 9:11
792+:: (cell 9:14
793+:: (face 9:15 a (ref 9:17 poke))
794+:: (face 9:22 s (ref 9:24 state)))
795+:: (body 10:3
796+:: (branch 10:3
797+:: (wing 10:6 a)
798+:: (arm 11:5
799+:: (cell 11:5 (lit 11:6 %add) (bind 11:11 item))
800+:: (change 11:18 s
801+:: (edit 11:20 items
802+:: (tuple 11:26 (wing 11:27 item) (wing 11:32 items.s)))))
799803:: (arm 12:5
800−:: (cell 12:5 (lit 12:6 %add) (bind 12:11 item))
804+:: (lit 12:5 %toggle)
801805:: (change 12:18 s
802−:: (edit 12:20 items
803−:: (tuple 12:26 (wing 12:27 item) (wing 12:32 items.s)))))
804−:: (arm 13:5
805−:: (lit 13:5 %toggle)
806−:: (change 13:18 s
807−:: (edit 13:20 open
808−:: (group 13:25
809−:: (call 13:26 (wing 13:26 not) (wing 13:30 open.s)))))))))))
806+:: (edit 12:20 open
807+:: (group 12:25
808+:: (call 12:26 (wing 12:26 not) (wing 12:30 open.s)))))))))))
810809::
811810:: 4.3 Errors (+show-error): "<file>:<line>:<col>: <message>", then the
812811:: source line, then a caret under the column (col - 1 spaces, then ^).
@@ -4681,7 +4680,7 @@
46814680 ==
46824681+$ ibinding [id=@ud val=itype]
46834682+$ isub (list ibinding)
4684−+$ ipending [id=@ud literal=lit]
4683++$ ipending [id=@ud literal=lit at=span]
46854684::
46864685++ itype-lookup
46874686 |= [n=@ud sub=isub]
@@ -5203,6 +5202,13 @@
52035202 ?~ (itype-lookup id.i.tags sub) &
52045203 $(tags t.tags)
52055204::
5205+++ pending-tag-diagnostic
5206+ |= [tags=(list ipending) sub=isub]
5207+ ^- (unit [at=span msg=tape])
5208+ ?~ tags ~
5209+ ?^ (itype-lookup id.i.tags sub) $(tags t.tags)
5210+ `[at.i.tags (weld "nothing fixes the union of " (show-lit literal.i.tags))]
5211+::
52065212++ pending-null
52075213 |= [tags=(list ipending) sub=isub]
52085214 ^- ?
@@ -5487,6 +5493,13 @@
54875493 ?:(|(=(0 val.literal.actual) =(1 val.literal.actual)) [%ok sub next] [%bad ~])
54885494 ?: ?=(%any-atom -.expected) [%ok sub next]
54895495 [%bad ~]
5496+ :: A field on an expected sample slot labels the value's type; it does
5497+ :: not become a face on the actual argument. Unify with the slot body
5498+ :: rather than binding either variable to the face around the other.
5499+ ?: &(?=(%var -.actual) ?=(%face -.expected))
5500+ =/ unified=(unit isub) (itype-unify actual body.expected sub)
5501+ ?~ unified [%unknown ~]
5502+ [%ok u.unified next]
54905503 ?: &(uncertain (itype-face-asym actual expected sub)) [%unknown ~]
54915504 :: A known face labels the same noun. Peel it before applying the
54925505 :: directional unrestricted-atom rule, preserving raw-variable guards.
@@ -5516,14 +5529,6 @@
55165529 =/ first=ifit $(actual hed.actual, expected hed.expected, skip-width |, spine-proof |)
55175530 ?. ?=(%ok -.first) first
55185531 $(actual tal.actual, expected tal.expected, sub sub.first, next next.first, skip-width spine-checked, spine-proof spine-checked)
5519− :: A field may add a face to an occurrence of the very same type
5520− :: variable. Binding that variable to a face around itself would fail
5521− :: the occurs check, but its underlying type has already matched.
5522− ?: &(?=(%var -.actual) ?=(%face -.expected) =(actual (itype-walk body.expected sub)))
5523− [%ok sub next]
5524− :: Differing variables and faces need propagation that is not yet
5525− :: represented. Binding one to the face can create a false mismatch.
5526− ?: &(?=(%var -.actual) ?=(%face -.expected)) [%unknown ~]
55275532 ?: &(?=(%face -.actual) ?=(%var -.expected)) [%unknown ~]
55285533 ?: &(?=(%var -.actual) (itype-has-any-atom expected sub))
55295534 [%unknown ~]
@@ -5623,10 +5628,14 @@
56235628:: of an arbitrary ask value. Reader graphs and source inputs are trusted.
56245629+$ irequest-evidence
56255630 [api-at=path name=term path=iapi-path-typed api-source=@t public-source=@t internal-source=@t prelude-values=(list term) prelude-molds=(list term) externals=iexternals marks=imark-externals]
5631+:: Store requests have their own source-bound evidence. In particular, an
5632+:: API path certificate cannot make a store state member watchable, or vice versa.
5633++$ istore-request-evidence
5634+ [store-at=path source=@t state=itype action-name=term action=itype]
56265635:: A unit distinguishes a verified empty closure from a detached legacy file.
56275636:: The opaque prelude is an exact trusted input, not a recursive interface mold.
56285637+$ irequest-graph
5629− [paths=(set path) requests=(list irequest-evidence) bundle-input=* prelude-input=* prelude-values=(list term) prelude-molds=(list term) externals=iexternals marks=imark-externals]
5638+ [paths=(set path) requests=(list irequest-evidence) stores=(list istore-request-evidence) bundle-input=* prelude-input=* prelude-values=(list term) prelude-molds=(list term) externals=iexternals marks=imark-externals]
56305639+$ ifile [values=ienv molds=imold-types at=path derived=(list iderived) elaborations=(list iwidth-definition) dependencies=(list iwidth-dependency) source=(unit @t) graph=(unit irequest-graph)]
56315640+$ ijimports (list [face=term interface=ifile])
56325641+$ icap [name=@t id=@ud at=span]
@@ -7477,7 +7486,12 @@
74777486 =/ target=itype (itype-walk expected sub.state)
74787487 =/ value=iresult (infer-call-context-arg i.items target env state context)
74797488 ?: ?=(%| -.value) value
7480− =/ fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
7489+ =/ ordinary-fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
7490+ =/ fit=ifit
7491+ ?: ?=(%ok -.ordinary-fit) ordinary-fit
7492+ ?: ?&(?=(%union -.target) ?=(^ prelude.state) =(origin.target `[at.u.prelude.state %element]))
7493+ (program-single-generic-fit typ.p.value target sub.state.p.value next.state.p.value)
7494+ ordinary-fit
74817495 ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
74827496 ?: ?=(%bad -.fit)
74837497 ?: |((itype-family-related typ.p.value target sub.state.p.value) (itype-has-any-atom typ.p.value sub.state.p.value) (itype-has-any-atom target sub.state.p.value))
@@ -7494,7 +7508,12 @@
74947508 =/ target=itype (itype-walk expected sub.state)
74957509 =/ value=iresult (infer-call-context-arg i.items target env state context)
74967510 ?: ?=(%| -.value) value
7497− =/ fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
7511+ =/ ordinary-fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
7512+ =/ fit=ifit
7513+ ?: ?=(%ok -.ordinary-fit) ordinary-fit
7514+ ?: ?&(?=(%union -.target) ?=(^ prelude.state) =(origin.target `[at.u.prelude.state %element]))
7515+ (program-single-generic-fit typ.p.value target sub.state.p.value next.state.p.value)
7516+ ordinary-fit
74987517 ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
74997518 ?: ?=(%bad -.fit)
75007519 =/ missing=(unit idiag) (missing-union-tag i.items target sub.state.p.value context)
@@ -8362,8 +8381,8 @@
83628381 %duration [%& [%atom %dr] state]
83638382 %knot [%& [%atom %ta] state]
83648383 %loobean [%& [%flag ~] state]
8365− %term [%& [%tag next.state lit.e |] state(next +(next.state), tags [[next.state lit.e] tags.state])]
8366− %null [%& [%tag next.state lit.e |] state(next +(next.state), tags [[next.state lit.e] tags.state])]
8384+ %term [%& [%tag next.state lit.e |] state(next +(next.state), tags [[next.state lit.e at.e] tags.state])]
8385+ %null [%& [%tag next.state lit.e |] state(next +(next.state), tags [[next.state lit.e at.e] tags.state])]
83678386 ==
83688387 %unit
83698388 ?~ prelude.state [%| ["unit construction needs the standard prelude in partial inference" ~]]
@@ -8430,12 +8449,15 @@
84308449 =/ target=iresult $(e [%wing at.e target.e])
84318450 ?: ?=(%| -.target) target
84328451 (infer-change-edits edits.e typ.p.target env state.p.target ~)
8433− %ctor [%& [%tag next.state tag.e &] state(next +(next.state), tags [[next.state tag.e] tags.state])]
8452+ %ctor [%& [%tag next.state tag.e &] state(next +(next.state), tags [[next.state tag.e at.e] tags.state])]
84348453 %trace
84358454 =/ traced=iresult $(e val.e)
84368455 ?: ?=(%| -.traced) traced
84378456 $(e then.e, state state.p.traced)
8438− %tuple (infer-simple-items items.e env state)
8457+ %tuple
8458+ ?: &(?=(^ defer.state) ?=(^ prelude.state))
8459+ (dg-infer-tuple-items items.e env state)
8460+ (infer-simple-items items.e env state)
84398461 %body
84408462 ?~ defs.e $(e final.e)
84418463 =/ local-names=(list term) (global-value-names defs.e)
@@ -8959,7 +8981,17 @@
89598981 ?~ args.result |
89608982 ?. =((lent args.result) (lent args.expected)) |
89618983 ?: |((itype-has-tag (itype-normalize result sub.state.p.head)) (itype-has-tag (itype-normalize expected sub.state.p.head))) |
8962− ?: |((itype-has-recursive (itype-normalize result sub.state.p.head)) (itype-has-recursive (itype-normalize expected sub.state.p.head))) |
8984+ =/ result-recursive=? (itype-has-recursive (itype-normalize result sub.state.p.head))
8985+ =/ expected-recursive=? (itype-has-recursive (itype-normalize expected sub.state.p.head))
8986+ =/ result-ok=?
8987+ ?. result-recursive &
8988+ ?~ prelude.state |
8989+ &(=(at.u.prelude.state /lib/jibb/prelude/jibb) =(origin.result `[at.u.prelude.state %element]))
8990+ =/ expected-ok=?
8991+ ?. expected-recursive &
8992+ ?~ prelude.state |
8993+ &(=(at.u.prelude.state /lib/jibb/prelude/jibb) =(origin.expected `[at.u.prelude.state %element]))
8994+ ?. &(result-ok expected-ok) |
89638995 ?: |((itype-has-any-atom result sub.state.p.head) (itype-has-any-atom expected sub.state.p.head)) |
89648996 &
89658997 ?. eligible (infer-call-with-head e env state head)
@@ -9241,6 +9273,8 @@
92419273 |= [e=expr expected=itype env=ienv state=istate context=span]
92429274 ^- iresult
92439275 ?: &(?=(^ defer.state) ?=(%branch -.e)) (infer-fragment e env state)
9276+ ?: &(?=(^ defer.state) ?=(^ prelude.state) ?=(%tuple -.e))
9277+ (infer-fragment e env state)
92449278 ?: ?=(%pair -.e) $(e (pair-as-cell e))
92459279 ?: ?=(%group -.e) $(e inner.e)
92469280 ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
@@ -10232,12 +10266,36 @@
1023210266 (resolve-groups-core ds molds globals externals surs mark-externals marks jimports reserved-molds at prelude ~)
1023310267::
1023410268
10269++$ iadded-definition
10270+ [env=ienv checked=(map term def) artifacts=(list iwidth-definition)]
10271+++ add-supported-result
10272+ |= [d=def result=iresult initial=istate env=ienv checked=(map term def) artifacts=(list iwidth-definition)]
10273+ ^- (unit iadded-definition)
10274+ ?> ?=(%value -.d)
10275+ ?: ?=(%| -.result) ~
10276+ =. state.p.result (promote-restricted-numbers state.p.result env)
10277+ =. state.p.result (default-hole-numbers holes.state.p.result holes.initial state.p.result env !(itype-has-gate (itype-normalize typ.p.result sub.state.p.result)))
10278+ ?^ (unresolved-hole holes.state.p.result holes.initial state.p.result) ~
10279+ ?: (constrained-capitals caps.state.p.result sub.state.p.result) ~
10280+ =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
10281+ ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) ~
10282+ ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) ~
10283+ =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
10284+ ?: (gth (lent vars) 26) ~
10285+ =/ finalized=(unit (list iwprojection))
10286+ (width-finalize projections.state.p.result sub.state.p.result vars)
10287+ ?~ finalized ~
10288+ =? artifacts ?=(^ u.finalized)
10289+ [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]
10290+ =? checked |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) (~(put by checked) name.d d)
10291+ `[[[name.d [typ vars]] env] checked artifacts]
1023510292++ add-supported-defs-core
1023610293 |= [ds=(list def) all-defs=(list def) checked=(map term def) heads=(unit igate-prelude-evidence) env=ienv molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile) artifacts=(list iwidth-definition) index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])]
1023710294 ^- [env=ienv artifacts=(list iwidth-definition)]
1023810295 ?~ ds [env artifacts]
1023910296 =/ d=def i.ds
1024010297 ?: ?=(%mold -.d) $(ds t.ds)
10298+ ?: (lien (program-recovery-names all-defs) |=(n=term =(n name.d))) $(ds t.ds)
1024110299 ?. (unique-value-name name.d globals) $(ds t.ds)
1024210300 ?^ (ienv-lookup name.d env) $(ds t.ds)
1024310301 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
@@ -10248,23 +10306,35 @@
1024810306 =. initial (reserve-def-caps val.d initial)
1024910307 =/ result=iresult (infer-fragment val.d env initial)
1025010308 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
10251− ?: ?=(%| -.result) $(ds t.ds)
10252− =. state.p.result (promote-restricted-numbers state.p.result env)
10253− =. state.p.result (default-hole-numbers holes.state.p.result holes.initial state.p.result env !(itype-has-gate (itype-normalize typ.p.result sub.state.p.result)))
10254− ?^ (unresolved-hole holes.state.p.result holes.initial state.p.result) $(ds t.ds)
10255− ?: (constrained-capitals caps.state.p.result sub.state.p.result) $(ds t.ds)
10256− =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
10257− ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) $(ds t.ds)
10258− ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) $(ds t.ds)
10259− =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
10260− ?: (gth (lent vars) 26) $(ds t.ds)
10261− =/ finalized=(unit (list iwprojection))
10262− (width-finalize projections.state.p.result sub.state.p.result vars)
10263− ?~ finalized $(ds t.ds)
10264− =? artifacts ?=(^ u.finalized)
10265− [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]
10266− =? checked |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) (~(put by checked) name.d d)
10267− $(ds t.ds, env [[name.d [typ vars]] env], checked checked)
10309+ =/ added=(unit iadded-definition)
10310+ (add-supported-result d result initial env checked artifacts)
10311+ ?~ added $(ds t.ds)
10312+ $(ds t.ds, env env.u.added, checked checked.u.added, artifacts artifacts.u.added)
10313+::
10314+:: Full checking discards unsupported definitions. On that failure path only,
10315+:: retry a bounded number of missing definitions to explain a pending tag
10316+:: from the same ordinary inference state instead of hiding it behind the
10317+:: generic completeness error. No successful definition takes this path.
10318+++ module-pending-tag
10319+ |= [ds=(list def) env=ienv base=istate fuel=@ud]
10320+ ^- (unit [at=span msg=tape])
10321+ =/ checked=(map term def) (direct-checked-gates ds env)
10322+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.base)
10323+ |-
10324+ ?~ ds ~
10325+ ?: =(0 fuel) ~
10326+ =/ d=def i.ds
10327+ ?: ?=(%mold -.d) $(ds t.ds, fuel (dec fuel))
10328+ ?^ (ienv-lookup name.d env) $(ds t.ds, fuel (dec fuel))
10329+ =/ initial=istate base(gate-defs checked, head-evidence heads)
10330+ =. initial (reserve-def-caps val.d initial)
10331+ =/ result=iresult (infer-fragment val.d env initial)
10332+ =? result ?=(%| -.result) (infer-recursive-gate d env initial)
10333+ ?: ?=(%| -.result) $(ds t.ds, fuel (dec fuel))
10334+ =/ pending=(unit [at=span msg=tape])
10335+ (pending-tag-diagnostic tags.state.p.result sub.state.p.result)
10336+ ?^ pending pending
10337+ $(ds t.ds, fuel (dec fuel))
1026810338::
1026910339++ resolve-groups-core
1027010340 |= [ds=(list def) molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile) index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])]
@@ -11270,22 +11340,6 @@
1127011340 ?. (levy vals |=(n=term &((unique-value-name n vals) !(lien prelude-values |=(v=term =(n v)))))) |
1127111341 (levy mold-names |=(n=term &((unique-value-name n mold-names) !(lien prelude-molds |=(m=term =(n m))))))
1127211342::
11273−:: In an API file or before main's kind is known, a lone `+$ poke`
11274−:: may be a declaration rather than a mold that shadows the prelude. Do not call
11275−:: that one collision definite, and do not hide unrelated scope errors.
11276−++ pending-declared-poke
11277− |= [at=path mod=module prelude-values=(list term) prelude-molds=(list term)]
11278− ^- ?
11279− ?. (lien prelude-molds |=(n=term =(%poke n))) |
11280− ?. |(?=([%ui %api @ %jibb ~] at) (lien defs.mod |=(d=def &(?=(%value -.d) =(%main name.d))))) |
11281− =/ pokes=(list def)
11282− (skim defs.mod |=(d=def &(?=(%mold -.d) =(%poke name.d))))
11283− ?~ pokes |
11284− ?^ t.pokes |
11285− =/ remaining=(list def)
11286− (skim defs.mod |=(d=def !&(?=(%mold -.d) =(%poke name.d))))
11287− (module-scope-valid mod(defs remaining) prelude-values prelude-molds)
11288−::
1128911343:: A detailed failure is attached only to the first mold that actually
1129011344:: failed in this check, using that module's checked source mold table.
1129111345+$ imold-failure [message=@t overlap=(unit [name=term cases=upair])]
@@ -11640,6 +11694,25 @@
1164011694 =(externals.g externals)
1164111695 =(marks.g marks)
1164211696 ==
11697+++ request-graph-bounded
11698+ |= g=irequest-graph
11699+ ^- ?
11700+ =/ total=@ud (add (lent requests.g) (lent stores.g))
11701+ &((lte (lent ~(tap in:..zuse paths.g)) 256) (lte total 256))
11702+::
11703+++ store-graph-requests-add
11704+ |= [pending=(list istore-request-evidence) acc=(list istore-request-evidence) fuel=@ud]
11705+ ^- (unit (list istore-request-evidence))
11706+ ?~ pending `acc
11707+ ?: =(0 fuel) ~
11708+ =/ hit=(list istore-request-evidence)
11709+ (skim acc |=(x=istore-request-evidence =(store-at.x store-at.i.pending)))
11710+ ?^ hit
11711+ ?. ?=([* ~] hit) ~
11712+ ?. =(i.hit i.pending) ~
11713+ $(pending t.pending, fuel (dec fuel))
11714+ $(pending t.pending, acc [i.pending acc], fuel (dec fuel))
11715+::
1164311716++ request-graph-merge
1164411717 |= [imports=ijimports g=irequest-graph fuel=@ud]
1164511718 ^- (unit irequest-graph)
@@ -11660,8 +11733,13 @@
1166011733 =/ rs=(unit (list irequest-evidence))
1166111734 (request-graph-requests-add requests.cg requests.g (add 1 (lent requests.cg)))
1166211735 ?~ rs ~
11663− ?: &(?=(^ u.rs) |((gth (lent ~(tap in:..zuse merged)) 256) (gth (lent u.rs) 256))) ~
11664− $(imports t.imports, g g(paths merged, requests u.rs), fuel (dec fuel))
11736+ =/ ss=(unit (list istore-request-evidence))
11737+ (store-graph-requests-add stores.cg stores.g (add 1 (lent stores.cg)))
11738+ ?~ ss ~
11739+ =/ total=@ud (add (lent u.rs) (lent u.ss))
11740+ ?: &(?=(^ u.rs) |((gth (lent ~(tap in:..zuse merged)) 256) (gth total 256))) ~
11741+ ?: &(?=(^ u.ss) |((gth (lent ~(tap in:..zuse merged)) 256) (gth total 256))) ~
11742+ $(imports t.imports, g g(paths merged, requests u.rs, stores u.ss), fuel (dec fuel))
1166511743++ request-graph-reusable
1166611744 |= [f=ifile src=@t externals=iexternals marks=imark-externals modules=jbundle active=(list path) values=(list term) molds=(list term) prelude=(unit ifile)]
1166711745 ^- ?
@@ -11908,7 +11986,8 @@
1190811986 ?> ?=(%mold -.decl)
1190911987 =/ paths=(unit (list iapi-path)) (api-path-declaration shape.decl declared)
1191011988 ?~ paths ~
11911− ?. (api-derived-names-valid u.paths u.poke-names mod prelude-values) ~
11989+ =/ derived-pokes=(list term) ?~(pokes ~ ~[%poke])
11990+ ?. (api-derived-names-valid u.paths derived-pokes mod prelude-values) ~
1191211991 (api-path-types u.paths externals declared)
1191311992::
1191411993:: Source/graph entry for path analysis only. The returned paths retain
@@ -12119,6 +12198,29 @@
1211912198:: Value watchability remains unproved even for a watchable declaration.
1212012199+$ ione-request-interface
1212112200 [support=iapi-support-evidence parts=iapi-request-parts iface=ifile]
12201+++ compatible-raw-poke
12202+ |= prelude=iprelude
12203+ ^- (unit ischeme)
12204+ =/ public=ifile iface.prelude
12205+ ?. =(at.public /lib/jibb/prelude/jibb) ~
12206+ =/ poke=(unit ischeme) (find-jibb-mold %raw-poke public)
12207+ ?~ poke ~
12208+ ?^ vars.u.poke ~
12209+ ?. ?=(%union -.typ.u.poke) ~
12210+ ?^ args.typ.u.poke ~
12211+ ?. =(origin.typ.u.poke `[/lib/jibb/internal/jibb %raw-poke]) ~
12212+ ?: (itype-has-tag typ.u.poke) ~
12213+ =/ private=(list iwidth-dependency)
12214+ (skim dependencies.public |=(d=iwidth-dependency =(at.d /lib/jibb/internal/jibb)))
12215+ ?. ?=([* ~] private) ~
12216+ ?~ source.i.private ~
12217+ =/ agent-case=itype
12218+ [%cell [%const [%term %tas %agent '%agent']] [%cell [%face %agent [%atom %tas]] [%cell [%face %mark [%atom %tas]] [%face %payload [%noun ~]]]]]
12219+ =/ store-case=itype
12220+ [%cell [%const [%term %tas %store '%store']] [%cell [%face %module [%atom %t]] [%cell [%face %action [%atom %tas]] [%face %payload [%noun ~]]]]]
12221+ ?. =(cases.typ.u.poke ~[agent-case store-case]) ~
12222+ poke
12223+::
1212212224++ request-compatible-ask
1212312225 |= prelude=iprelude
1212412226 ^- (unit ischeme)
@@ -12215,7 +12317,7 @@
1221512317 ?~ source.i.private [%| 'request internal source needs unsupported inference']
1221612318 =/ req=irequest-evidence
1221712319 [file name.path.p p src u.source.public u.source.i.private values.prelude molds.prelude externals marks]
12218− =/ interface=ifile [~[[name.path.p scheme]] exports file ~ ~ ~ `src `[(silt `(list path)`~[file]) ~[req] modules `public values.prelude molds.prelude externals marks]]
12320+ =/ interface=ifile [~[[name.path.p scheme]] exports file ~ ~ ~ `src `[(silt `(list path)`~[file]) ~[req] ~ modules `public values.prelude molds.prelude externals marks]]
1221912321 [%& [support u.parts interface]]
1222012322:: Graph-aware request artifact; resolver use remains type-only.
1222112323++ one-request-interface-graph
@@ -12269,7 +12371,7 @@
1226912371 ?~ source.i.private [%| 'request internal source needs unsupported inference']
1227012372 =/ req=irequest-evidence
1227112373 [file name.path.p p src u.source.public u.source.i.private values.prelude molds.prelude externals marks]
12272− =/ interface=ifile [~[[name.path.p scheme]] exports file ~ ~ ~ `src `[(silt `(list path)`~[file]) ~[req] modules `public values.prelude molds.prelude externals marks]]
12374+ =/ interface=ifile [~[[name.path.p scheme]] exports file ~ ~ ~ `src `[(silt `(list path)`~[file]) ~[req] ~ modules `public values.prelude molds.prelude externals marks]]
1227312375 [%& [support u.parts interface]]
1227412376::
1227512377++ api-mark-exports
@@ -12290,7 +12392,7 @@
1229012392 ?^ (duplicate-defs defs.mod) ~
1229112393 ?~ prelude ~
1229212394 ?. =(at.u.prelude /lib/jibb/prelude/jibb) ~
12293− =/ poke=(unit ischeme) (find-jibb-mold %poke u.prelude)
12395+ =/ poke=(unit ischeme) (find-jibb-mold %raw-poke u.prelude)
1229412396 ?~ poke ~
1229512397 ?. ?=(%union -.typ.u.poke) ~
1229612398 ?^ vars.u.poke ~
@@ -12314,8 +12416,9 @@
1231412416 ?: |((lien prelude-values |=(x=term =(n x))) (lien prelude-molds |=(x=term =(n x)))) ~
1231512417 =/ mark=(unit itype) (find-imported-mark n mark-externals marks)
1231612418 ?~ mark ~
12317− =/ sc=ischeme [[%fn u.mark typ.u.poke] ~]
12318− `[~[[n sc]] (api-mark-exports marks marks mark-externals) at ~[[n i.t.t.at n]] ~ ~ ~ ~]
12419+ =/ sc=(unit ischeme) (derived-poke-command-scheme u.prelude u.mark)
12420+ ?~ sc ~
12421+ `[~[[%poke u.sc]] (api-mark-exports marks marks mark-externals) at ~[[n i.t.t.at n]] ~ ~ ~ ~]
1231912422::
1232012423:: Source-proven ordinary helpers validate each selected /sur dependency.
1232112424:: Unused or less direct cores remain unsupported by this first interface.
@@ -12438,11 +12541,1562 @@
1243812541 [%| 'API exported molds need unsupported inference']
1243912542 =/ env=ienv (weld values.u.gates (weld values.u.poke values.support))
1244012543 =/ graph=irequest-graph
12441− [(silt `(list path)`~[file]) requests.u.gates modules `public values.prep molds.prep externals marks]
12544+ [(silt `(list path)`~[file]) requests.u.gates ~ modules `public values.prep molds.prep externals marks]
1244212545 =/ iface=ifile
1244312546 [env exports file derived.u.poke elaborations.support ~ `src `graph]
1244412547 [%& [iface dependencies.ev]]
1244512548::
12549+:: A checked program main is only the direct four-component source call.
12550+:: Grouping is transparent, but aliases, qualified wings and other module
12551+:: kinds remain outside this slice.
12552+++ program-main-def
12553+ |= ds=(list def)
12554+ ^- (unit def)
12555+ ?~ ds ~
12556+ ?: &(?=(%value -.i.ds) =(%main name.i.ds)) `i.ds
12557+ $(ds t.ds)
12558+::
12559+++ program-main-wing
12560+ |= e=expr
12561+ ^- (unit term)
12562+ ?: ?=(%group -.e) $(e inner.e)
12563+ ?. ?=(%wing -.e) ~
12564+ ?. ?=([@ ~] names.e) ~
12565+ `i.names.e
12566+::
12567+++ program-main-args
12568+ |= d=def
12569+ ^- (unit (list expr))
12570+ ?. ?=(%value -.d) ~
12571+ |-
12572+ ?: ?=(%group -.val.d) $(val.d inner.val.d)
12573+ ?. ?=(%call -.val.d) ~
12574+ =/ head=(unit term) (program-main-wing head.val.d)
12575+ ?~ head ~
12576+ ?. =(%program u.head) ~
12577+ ?. ?=([* * * * ~] args.val.d) ~
12578+ `args.val.d
12579+::
12580+++ program-main-parts
12581+ |= d=def
12582+ ^- (unit [init=term update=term view=term subs=term])
12583+ ?. ?=(%value -.d) ~
12584+ |-
12585+ ?: ?=(%group -.val.d) $(val.d inner.val.d)
12586+ ?. ?=(%call -.val.d) ~
12587+ =/ head=(unit term) (program-main-wing head.val.d)
12588+ ?~ head ~
12589+ ?. =(%program u.head) ~
12590+ ?. ?=([* * * * ~] args.val.d) ~
12591+ =/ args=(list expr) args.val.d
12592+ ?> ?=([* * * * ~] args)
12593+ =/ init=(unit term) (program-main-wing i.args)
12594+ =/ update=(unit term) (program-main-wing i.t.args)
12595+ =/ view=(unit term) (program-main-wing i.t.t.args)
12596+ =/ subs=(unit term) (program-main-wing i.t.t.t.args)
12597+ ?~ init ~
12598+ ?~ update ~
12599+ ?~ view ~
12600+ ?~ subs ~
12601+ `[u.init u.update u.view u.subs]
12602+::
12603+:: A data page is only the direct two-component source call. Grouping is
12604+:: transparent, but page aliases, qualified wings and other kinds are not.
12605+++ page-main-parts
12606+ |= d=def
12607+ ^- (unit [load=term view=term])
12608+ ?. ?=(%value -.d) ~
12609+ |-
12610+ ?: ?=(%group -.val.d) $(val.d inner.val.d)
12611+ ?. ?=(%call -.val.d) ~
12612+ =/ head=(unit term) (program-main-wing head.val.d)
12613+ ?~ head ~
12614+ ?. =(%page u.head) ~
12615+ ?. ?=([* * ~] args.val.d) ~
12616+ =/ args=(list expr) args.val.d
12617+ ?> ?=([* * ~] args)
12618+ =/ load=(unit term) (program-main-wing i.args)
12619+ =/ view=(unit term) (program-main-wing i.t.args)
12620+ ?~ load ~
12621+ ?~ view ~
12622+ `[u.load u.view]
12623+::
12624+:: A store main is only the direct two-wing source call. Its local poke mold
12625+:: is checked here and remains in ordinary mold/value inference.
12626+++ store-main-parts
12627+ |= d=def
12628+ ^- (unit [init=term update=term])
12629+ ?. ?=(%value -.d) ~
12630+ |-
12631+ ?: ?=(%group -.val.d) $(val.d inner.val.d)
12632+ ?. ?=(%call -.val.d) ~
12633+ =/ head=(unit term) (program-main-wing head.val.d)
12634+ ?~ head ~
12635+ ?. =(%store u.head) ~
12636+ ?. ?=([* * ~] args.val.d) ~
12637+ =/ args=(list expr) args.val.d
12638+ ?> ?=([* * ~] args)
12639+ =/ init=(unit term) (program-main-wing i.args)
12640+ =/ update=(unit term) (program-main-wing i.t.args)
12641+ ?~ init ~
12642+ ?~ update ~
12643+ `[u.init u.update]
12644+::
12645++$ istore-declaration [action=term defs=(list def)]
12646+++ store-declaration
12647+ |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
12648+ ^- (unit istore-declaration)
12649+ =/ ds=(list def) defs.mod
12650+ =/ pokes=(list def)
12651+ (skim ds |=(d=def &(?=(%mold -.d) =(%poke name.d))))
12652+ ?. ?=([* ~] pokes) ~
12653+ =/ states=(list def)
12654+ (skim ds |=(d=def &(?=(%mold -.d) =(%state name.d))))
12655+ ?. ?=([* ~] states) ~
12656+ =/ poke=def i.pokes
12657+ =/ state=def i.states
12658+ ?> &(?=(%mold -.poke) ?=(%mold -.state))
12659+ ?: ?=(%generic -.shape.state) ~
12660+ ?: ?=(%generic -.shape.poke) ~
12661+ =/ action=term %poke
12662+ =/ ordinary=(list def) ds
12663+ ?. (module-scope-valid mod prelude-values prelude-molds) ~
12664+ =/ derived=(list term) ~[%state action]
12665+ ?: (lien derived |=(n=term =(n %proj))) ~
12666+ =/ outer=(list term)
12667+ (weld prelude-values (weld (global-value-names ordinary) (api-import-faces imports.mod)))
12668+ ?. (levy derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x)))))) ~
12669+ `[action ordinary]
12670+::
12671+++ program-empty-null
12672+ |= e=expr
12673+ ^- ?
12674+ ?- -.e
12675+ %lit =(%null form.lit.e)
12676+ %cast $(e val.e)
12677+ %group $(e inner.e)
12678+ %body ?~(defs.e $(e final.e) |)
12679+ * |
12680+ ==
12681+::
12682+++ program-subs-empty
12683+ |= d=def
12684+ ^- ?
12685+ ?. ?=(%value -.d) |
12686+ ?- -.val.d
12687+ %gate (program-empty-null body.val.d)
12688+ %gate-wide (program-empty-null body.val.d)
12689+ * |
12690+ ==
12691+::
12692+++ program-transparent
12693+ |= e=expr
12694+ ^- expr
12695+ ?- -.e
12696+ %group $(e inner.e)
12697+ %cast $(e val.e)
12698+ %body ?~(defs.e $(e final.e) e)
12699+ * e
12700+ ==
12701+++ program-init-tuple-null
12702+ |= d=def
12703+ ^- ?
12704+ ?. ?=(%value -.d) |
12705+ ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) |
12706+ =/ body=expr
12707+ ?- -.val.d
12708+ %gate body.val.d
12709+ %gate-wide body.val.d
12710+ * !!
12711+ ==
12712+ =. body (program-transparent body)
12713+ ?. ?=(%tuple -.body) |
12714+ ?~ items.body |
12715+ (program-empty-null val:(rear items.body))
12716+::
12717+:: Recover only the update of an already recognized direct program main.
12718+:: Its written sample determines the message/model relationship; the canonical
12719+:: cmd, unit and update slot determine the result context. Publication is
12720+:: component-local so later subscription/view/initializer retries can accumulate.
12721+++ program-update-context
12722+ |= [main=def parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
12723+ ^- (unit iresolved)
12724+ =/ env=ienv env.resolution
12725+ ?^ (ienv-lookup %main env) ~
12726+ ?^ (ienv-lookup update.parts env) ~
12727+ =/ updates=(list def)
12728+ (skim ds |=(d=def &(?=(%value -.d) =(update.parts name.d))))
12729+ ?. ?=([* ~] updates) ~
12730+ =/ update-def=def i.updates
12731+ ?> ?=(%value -.update-def)
12732+ =/ written-update=(unit sample) (direct-gate-sample update-def)
12733+ ?~ written-update ~
12734+ ?. ?=(%cell -.u.written-update) ~
12735+ ?. ?=([* * ~] items.u.written-update) ~
12736+ ?~ prelude.initial ~
12737+ =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)
12738+ ?~ program ~
12739+ =/ command=(unit ischeme) (find-jibb-mold %cmd u.prelude.initial)
12740+ =/ list-template=(unit ischeme) (find-jibb-mold %list u.prelude.initial)
12741+ ?~ command ~
12742+ ?~ list-template ~
12743+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
12744+ ?~ heads ~
12745+ =/ written=(unit def) (~(get by gates.u.heads) %program)
12746+ ?~ written ~
12747+ =/ written-sample=(unit sample) (direct-gate-sample u.written)
12748+ ?~ written-sample ~
12749+ ?. ?=(%cell -.u.written-sample) ~
12750+ ?. ?=([* * * * ~] items.u.written-sample) ~
12751+ =/ checked=(map term def)
12752+ (~(put by (direct-checked-gates ds env)) update.parts update-def)
12753+ =/ templates=ienv
12754+ (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
12755+ =/ scanned=(unit dgscan)
12756+ (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
12757+ ?~ scanned ~
12758+ =. next.initial (dg-next-id ids.u.scanned 0)
12759+ =/ update-state=istate (reserve-def-caps val.update-def initial)
12760+ =/ sam=isample-result (infer-sample u.written-update env update-state)
12761+ ?: ?=(%| -.sam) ~
12762+ =/ actual-sample=itype (itype-normalize typ.p.sam sub.state.p.sam)
12763+ ?. ?=(%cell -.actual-sample) ~
12764+ =/ message=(unit itype)
12765+ (direct-slot-body hed.actual-sample (direct-sample-name i.items.u.written-update))
12766+ =/ model=(unit itype)
12767+ (direct-slot-body tal.actual-sample (direct-sample-name i.t.items.u.written-update))
12768+ ?~ message ~
12769+ ?~ model ~
12770+ =/ cmd=(unit itype) (template-apply u.command ~[u.message])
12771+ ?~ cmd ~
12772+ =/ command-result=(unit itype) (template-apply u.list-template ~[u.cmd])
12773+ ?~ command-result ~
12774+ =/ product=itype [%cell u.model u.command-result]
12775+ =/ instance=[typ=itype state=istate] (instantiate-scheme u.program state.p.sam)
12776+ ?. ?=(%fn -.typ.instance) ~
12777+ ?. ?=(%cell -.sample.typ.instance) ~
12778+ ?. ?=(%cell -.tal.sample.typ.instance) ~
12779+ =/ expected-update=(unit itype)
12780+ (direct-slot-body hed.tal.sample.typ.instance (direct-sample-name i.t.items.u.written-sample))
12781+ ?~ expected-update ~
12782+ ?. ?=(%fn -.u.expected-update) ~
12783+ :: Sample binders are not value faces. Strip only those two slot faces
12784+ :: for the invariant canonical-gate proof; the source-faced gate is still
12785+ :: used by the complete positional call and final ordinary result cast.
12786+ =/ canonical-candidate=itype [%fn [%cell u.message u.model] product]
12787+ =/ gate-fit=ifit
12788+ (direct-invariant canonical-candidate u.expected-update sub.state.instance next.state.instance)
12789+ ?. ?=(%ok -.gate-fit) ~
12790+ =/ closed=itype
12791+ (itype-normalize [%fn typ.p.sam product] sub.gate-fit)
12792+ ?. ?=(%fn -.closed) ~
12793+ :: The closed product no longer needs the canonical slot substitutions.
12794+ :: Start the body at its ordinary sample state so existing branch retries
12795+ :: keep their substitution guards, but retain the shared fresh-ID high water.
12796+ =/ st=istate state.p.sam(next next.gate-fit, gate-defs checked, head-evidence heads)
12797+ =/ body=expr
12798+ ?- -.val.update-def
12799+ %gate body.val.update-def
12800+ %gate-wide body.val.update-def
12801+ * !!
12802+ ==
12803+ =/ inferred=iresult
12804+ (infer-call-context-arg body product.closed env.p.sam st (span-of body))
12805+ ?: ?=(%| -.inferred) ~
12806+ =/ product-fit=ifit
12807+ (itype-fit typ.p.inferred product.closed sub.state.p.inferred next.state.p.inferred)
12808+ ?. ?=(%ok -.product-fit) ~
12809+ =/ merged-product=itype
12810+ (itype-merge-faces typ.p.inferred product.closed sub.product-fit)
12811+ =/ actual-cast=itype [%fn typ.p.sam merged-product]
12812+ =/ cast=ifit
12813+ (itype-fit actual-cast closed sub.product-fit next.product-fit)
12814+ ?. ?=(%ok -.cast) ~
12815+ =/ merged=itype (itype-merge-faces actual-cast closed sub.cast)
12816+ =/ adjusted=iresult
12817+ [%& merged state.p.inferred(sub sub.cast, next next.cast)]
12818+ =/ added=(unit iadded-definition)
12819+ (add-supported-result update-def adjusted update-state env checked artifacts.resolution)
12820+ ?~ added ~
12821+ =/ recovered=(unit ischeme) (ienv-lookup update.parts env.u.added)
12822+ ?~ recovered ~
12823+ ?. ?=(~ vars.u.recovered) ~
12824+ ?. ?=(~ (itype-vars typ.u.recovered)) ~
12825+ `[env.u.added grouped.resolution artifacts.u.added]
12826+::
12827+++ program-inferred-slot
12828+ |= [typ=itype name=(unit term)]
12829+ ^- itype
12830+ ?~ name typ
12831+ ?: &(?=(%face -.typ) =(name.typ u.name)) body.typ
12832+ typ
12833+::
12834+++ program-inferred-sample
12835+ |= [typ=itype sam=sample]
12836+ ^- itype
12837+ (program-inferred-slot typ (direct-sample-name sam))
12838+::
12839+++ program-two-slot-names
12840+ |= sam=sample
12841+ ^- (unit [first=(unit term) second=(unit term)])
12842+ ?- -.sam
12843+ %cell
12844+ ?. ?=([* * ~] items.sam) ~
12845+ `[(direct-sample-name i.items.sam) (direct-sample-name i.t.items.sam)]
12846+ %face
12847+ ?. ?=(%cell -.shape.sam) ~
12848+ ?. ?=([* * ~] fields.shape.sam) ~
12849+ `[(direct-field-name i.fields.shape.sam) (direct-field-name i.t.fields.shape.sam)]
12850+ * ~
12851+ ==
12852+::
12853+:: Read message/model from the checked update and its written source layout.
12854+:: The source names strip only top-level sample binder faces; nested value
12855+:: faces remain part of the canonical message and model.
12856+++ program-update-relation
12857+ |= [name=term ds=(list def) env=ienv]
12858+ ^- (unit [message=itype model=itype])
12859+ =/ update=(unit ischeme) (ienv-lookup name env)
12860+ ?~ update ~
12861+ ?. ?=(~ vars.u.update) ~
12862+ ?. ?=(~ (itype-vars typ.u.update)) ~
12863+ ?. ?=(%fn -.typ.u.update) ~
12864+ ?. ?=(%cell -.sample.typ.u.update) ~
12865+ =/ defs=(list def)
12866+ (skim ds |=(d=def &(?=(%value -.d) =(name name.d))))
12867+ ?. ?=([* ~] defs) ~
12868+ =/ written=(unit sample) (direct-gate-sample i.defs)
12869+ ?~ written ~
12870+ ?. ?=(%cell -.u.written) ~
12871+ ?. ?=([* * ~] items.u.written) ~
12872+ =/ message=(unit itype)
12873+ (direct-slot-body hed.sample.typ.u.update (direct-sample-name i.items.u.written))
12874+ =/ model=(unit itype)
12875+ (direct-slot-body tal.sample.typ.u.update (direct-sample-name i.t.items.u.written))
12876+ ?~ message ~
12877+ ?~ model ~
12878+ `[u.message u.model]
12879+::
12880+:: Recover an unannotated direct subscription component from the checked
12881+:: update relation and canonical fourth program slot. This establishes only
12882+:: the value type; the final program watch proof remains separate.
12883+++ program-subs-context
12884+ |= [parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
12885+ ^- (unit iresolved)
12886+ =/ env=ienv env.resolution
12887+ ?^ (ienv-lookup %main env) ~
12888+ ?^ (ienv-lookup subs.parts env) ~
12889+ =/ relation=(unit [message=itype model=itype])
12890+ (program-update-relation update.parts ds env)
12891+ ?~ relation ~
12892+ =/ subs=(list def)
12893+ (skim ds |=(d=def &(?=(%value -.d) =(subs.parts name.d))))
12894+ ?. ?=([* ~] subs) ~
12895+ =/ subs-def=def i.subs
12896+ ?> ?=(%value -.subs-def)
12897+ =/ written-subs=(unit sample) (direct-gate-sample subs-def)
12898+ ?~ written-subs ~
12899+ ?~ prelude.initial ~
12900+ =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)
12901+ =/ sub=(unit ischeme) (find-jibb-mold %sub u.prelude.initial)
12902+ =/ list-template=(unit ischeme) (find-jibb-mold %list u.prelude.initial)
12903+ ?~ program ~
12904+ ?~ sub ~
12905+ ?~ list-template ~
12906+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
12907+ ?~ heads ~
12908+ =/ written=(unit def) (~(get by gates.u.heads) %program)
12909+ ?~ written ~
12910+ =/ written-sample=(unit sample) (direct-gate-sample u.written)
12911+ ?~ written-sample ~
12912+ ?. ?=(%cell -.u.written-sample) ~
12913+ ?. ?=([* * * * ~] items.u.written-sample) ~
12914+ =/ checked=(map term def) (direct-checked-gates ds env)
12915+ =/ templates=ienv
12916+ (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
12917+ =/ scanned=(unit dgscan)
12918+ (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
12919+ ?~ scanned ~
12920+ =. next.initial (dg-next-id ids.u.scanned 0)
12921+ =/ subs-state=istate (reserve-def-caps val.subs-def initial)
12922+ =/ sam=isample-result (infer-sample u.written-subs env subs-state)
12923+ ?: ?=(%| -.sam) ~
12924+ =/ actual-model=itype (program-inferred-sample typ.p.sam u.written-subs)
12925+ ?. ?=(~ (itype-vars actual-model)) ~
12926+ ?: (itype-has-tag actual-model) ~
12927+ =/ model-fit=ifit
12928+ (direct-invariant actual-model model.u.relation sub.state.p.sam next.state.p.sam)
12929+ ?. ?=(%ok -.model-fit) ~
12930+ =/ message-sub=(unit itype) (template-apply u.sub ~[message.u.relation])
12931+ ?~ message-sub ~
12932+ =/ product=(unit itype) (template-apply u.list-template ~[u.message-sub])
12933+ ?~ product ~
12934+ =/ instance=[typ=itype state=istate]
12935+ (instantiate-scheme u.program state.p.sam(sub sub.model-fit, next next.model-fit))
12936+ ?. ?=(%fn -.typ.instance) ~
12937+ ?. ?=(%cell -.sample.typ.instance) ~
12938+ ?. ?=(%cell -.tal.sample.typ.instance) ~
12939+ ?. ?=(%cell -.tal.tal.sample.typ.instance) ~
12940+ =/ expected-subs=(unit itype)
12941+ (direct-slot-body tal.tal.tal.sample.typ.instance (direct-sample-name i.t.t.t.items.u.written-sample))
12942+ ?~ expected-subs ~
12943+ ?. ?=(%fn -.u.expected-subs) ~
12944+ =/ canonical=itype [%fn model.u.relation u.product]
12945+ =/ gate-fit=ifit
12946+ (direct-invariant canonical u.expected-subs sub.state.instance next.state.instance)
12947+ ?. ?=(%ok -.gate-fit) ~
12948+ =/ closed=itype
12949+ (itype-normalize [%fn typ.p.sam u.product] sub.gate-fit)
12950+ ?. ?=(%fn -.closed) ~
12951+ =/ body=expr
12952+ ?- -.val.subs-def
12953+ %gate body.val.subs-def
12954+ %gate-wide body.val.subs-def
12955+ * !!
12956+ ==
12957+ =/ st=istate
12958+ state.p.sam(next next.gate-fit, gate-defs checked, head-evidence heads)
12959+ =/ inferred=iresult
12960+ (infer-call-context-arg body product.closed env.p.sam st (span-of body))
12961+ ?: ?=(%| -.inferred) ~
12962+ =/ product-fit=ifit
12963+ (itype-fit typ.p.inferred product.closed sub.state.p.inferred next.state.p.inferred)
12964+ ?. ?=(%ok -.product-fit) ~
12965+ =/ merged-product=itype
12966+ (itype-merge-faces typ.p.inferred product.closed sub.product-fit)
12967+ =/ actual-cast=itype [%fn typ.p.sam merged-product]
12968+ =/ cast=ifit
12969+ (itype-fit actual-cast closed sub.product-fit next.product-fit)
12970+ ?. ?=(%ok -.cast) ~
12971+ =/ merged=itype (itype-merge-faces actual-cast closed sub.cast)
12972+ =/ adjusted=iresult
12973+ [%& merged state.p.inferred(sub sub.cast, next next.cast)]
12974+ =/ added=(unit iadded-definition)
12975+ (add-supported-result subs-def adjusted subs-state env checked artifacts.resolution)
12976+ ?~ added ~
12977+ =/ recovered=(unit ischeme) (ienv-lookup subs.parts env.u.added)
12978+ ?~ recovered ~
12979+ ?. ?=(~ vars.u.recovered) ~
12980+ ?. ?=(~ (itype-vars typ.u.recovered)) ~
12981+ `[env.u.added grouped.resolution artifacts.u.added]
12982+::
12983++$ iview-site [xs=expr mapper=term]
12984+++ program-view-site
12985+ |= e=expr
12986+ ^- (unit iview-site)
12987+ =. e (program-transparent e)
12988+ ?. ?=(%call -.e) ~
12989+ ?. ?=([* ~] args.e) ~
12990+ =/ each=expr (program-transparent head.e)
12991+ ?. ?=(%wing -.each) ~
12992+ ?. ?=([%each ~] names.each) ~
12993+ =/ turned=expr (program-transparent i.args.e)
12994+ ?. ?=(%call -.turned) ~
12995+ ?. ?=([* * ~] args.turned) ~
12996+ =/ turn=expr (program-transparent head.turned)
12997+ ?. ?=(%wing -.turn) ~
12998+ ?. ?=([%turn ~] names.turn) ~
12999+ =/ xs=expr (program-transparent i.args.turned)
13000+ ?. ?=(%wing -.xs) ~
13001+ ?~ names.xs ~
13002+ =/ mapper=(unit term) (program-main-wing i.t.args.turned)
13003+ ?~ mapper ~
13004+ `[xs u.mapper]
13005+::
13006+++ program-recovery-names
13007+ |= ds=(list def)
13008+ ^- (list term)
13009+ =/ main=(unit def) (program-main-def ds)
13010+ ?~ main ~
13011+ =/ parts=(unit [init=term update=term view=term subs=term])
13012+ (program-main-parts u.main)
13013+ ?~ parts ~
13014+ =/ views=(list def)
13015+ (skim ds |=(d=def &(?=(%value -.d) =(view.u.parts name.d))))
13016+ ?. ?=([* ~] views) ~
13017+ =/ view-def=def i.views
13018+ ?> ?=(%value -.view-def)
13019+ =/ written=(unit sample) (direct-gate-sample view-def)
13020+ ?~ written ~
13021+ =/ body=expr
13022+ ?- -.val.view-def
13023+ %gate body.val.view-def
13024+ %gate-wide body.val.view-def
13025+ * !!
13026+ ==
13027+ =/ sites=(unit (list iview-site)) (program-view-sites body ~)
13028+ ?~ sites ~
13029+ ?. ?=([* ~] u.sites) ~
13030+ =/ mapper=term mapper.i.u.sites
13031+ =/ components=(list term)
13032+ :~ init.u.parts
13033+ update.u.parts
13034+ view.u.parts
13035+ subs.u.parts
13036+ ==
13037+ ?: (lien components |=(n=term =(n mapper))) ~
13038+ =/ mappers=(list def)
13039+ (skim ds |=(d=def &(?=(%value -.d) =(mapper name.d))))
13040+ ?. ?=([* ~] mappers) ~
13041+ :~ init.u.parts
13042+ update.u.parts
13043+ view.u.parts
13044+ subs.u.parts
13045+ mapper
13046+ ==
13047+::
13048+++ program-sample-binders
13049+ |= sam=sample
13050+ ^- (list term)
13051+ ?- -.sam
13052+ %bind ~[name.sam]
13053+ %face ~[name.sam]
13054+ %pun ~[name.sam]
13055+ %cell (zing (turn items.sam |=(s=sample (program-sample-binders s))))
13056+ * ~
13057+ ==
13058+::
13059+++ program-pattern-binders
13060+ |= pat=pattern
13061+ ^- (list term)
13062+ ?- -.pat
13063+ %bind ~[name.pat]
13064+ %cell (zing (turn items.pat |=(p=pattern (program-pattern-binders p))))
13065+ * ~
13066+ ==
13067+::
13068+++ program-view-sites-merge
13069+ |= [a=(unit (list iview-site)) b=(unit (list iview-site))]
13070+ ^- (unit (list iview-site))
13071+ ?~ a ~
13072+ ?~ b ~
13073+ `(weld u.a u.b)
13074+::
13075+++ program-view-sites-exprs
13076+ |= [xs=(list expr) locals=(list term)]
13077+ ^- (unit (list iview-site))
13078+ ?~ xs `~
13079+ (program-view-sites-merge (program-view-sites i.xs locals) $(xs t.xs))
13080+::
13081+++ program-view-sites-items
13082+ |= [xs=(list item) locals=(list term)]
13083+ ^- (unit (list iview-site))
13084+ ?~ xs `~
13085+ (program-view-sites-merge (program-view-sites val.i.xs locals) $(xs t.xs))
13086+::
13087+++ program-view-sites-pieces
13088+ |= [xs=(list piece) locals=(list term)]
13089+ ^- (unit (list iview-site))
13090+ ?~ xs `~
13091+ =/ here=(unit (list iview-site))
13092+ ?- -.i.xs
13093+ %expr (program-view-sites p.i.xs locals)
13094+ %text `~
13095+ ==
13096+ (program-view-sites-merge here $(xs t.xs))
13097+::
13098+++ program-view-sites-qsegs
13099+ |= [xs=(list qseg) locals=(list term)]
13100+ ^- (unit (list iview-site))
13101+ ?~ xs `~
13102+ =/ here=(unit (list iview-site))
13103+ ?- -.i.xs
13104+ %expr (program-view-sites p.i.xs locals)
13105+ %knot `~
13106+ ==
13107+ (program-view-sites-merge here $(xs t.xs))
13108+::
13109+++ program-view-sites-edits
13110+ |= [xs=(list edit) locals=(list term)]
13111+ ^- (unit (list iview-site))
13112+ ?~ xs `~
13113+ (program-view-sites-merge (program-view-sites val.i.xs locals) $(xs t.xs))
13114+::
13115+++ program-view-sites-defs
13116+ |= [xs=(list def) locals=(list term)]
13117+ ^- (unit (list iview-site))
13118+ ?~ xs `~
13119+ =/ here=(unit (list iview-site))
13120+ ?: ?=(%mold -.i.xs) `~
13121+ (program-view-sites val.i.xs locals)
13122+ (program-view-sites-merge here $(xs t.xs))
13123+::
13124+++ program-view-sites-arms
13125+ |= [xs=(list arm) locals=(list term)]
13126+ ^- (unit (list iview-site))
13127+ ?~ xs `~
13128+ =/ nested=(list term) (weld (program-pattern-binders pat.i.xs) locals)
13129+ (program-view-sites-merge (program-view-sites val.i.xs nested) $(xs t.xs))
13130+::
13131+++ program-view-sites
13132+ |= [e=expr locals=(list term)]
13133+ ^- (unit (list iview-site))
13134+ =/ site=(unit iview-site) (program-view-site e)
13135+ ?^ site
13136+ =/ names=(list term) ~[%each %turn mapper.u.site]
13137+ ?> ?=(%wing -.xs.u.site)
13138+ =/ root=term (rear names.xs.u.site)
13139+ ?: |((lien names |=(n=term (lien locals |=(x=term =(n x))))) (lien locals |=(x=term =(root x))))
13140+ ~
13141+ `~[u.site]
13142+ ?- -.e
13143+ %str (program-view-sites-pieces pieces.e locals)
13144+ %qath (program-view-sites-qsegs segs.e locals)
13145+ %change (program-view-sites-edits edits.e locals)
13146+ %pair (program-view-sites val.e locals)
13147+ %unit (program-view-sites val.e locals)
13148+ %group (program-view-sites inner.e locals)
13149+ %list (program-view-sites-exprs items.e locals)
13150+ %tuple (program-view-sites-items items.e locals)
13151+ %gate
13152+ (program-view-sites body.e (weld (program-sample-binders sample.e) locals))
13153+ %gate-wide
13154+ (program-view-sites body.e (weld (program-sample-binders sample.e) locals))
13155+ %call
13156+ (program-view-sites-merge (program-view-sites head.e locals) (program-view-sites-exprs args.e locals))
13157+ %cast (program-view-sites val.e locals)
13158+ %trace
13159+ (program-view-sites-merge (program-view-sites val.e locals) (program-view-sites then.e locals))
13160+ %branch
13161+ (program-view-sites-merge (program-view-sites subject.e locals) (program-view-sites-arms arms.e locals))
13162+ %body
13163+ =/ nested=(list term) (weld (global-value-names defs.e) locals)
13164+ (program-view-sites-merge (program-view-sites-defs defs.e nested) (program-view-sites final.e nested))
13165+ * `~
13166+ ==
13167+::
13168+++ program-union-tag-case
13169+ |= [expected=itype tag=@]
13170+ ^- (unit itype)
13171+ ?. ?=(%union -.expected) ~
13172+ =/ remaining=(list itype) cases.expected
13173+ =/ found=(unit itype) ~
13174+ =/ seen=(set @) *(set @)
13175+ |-
13176+ ?~ remaining found
13177+ =/ case=itype i.remaining
13178+ =/ head=(unit @)
13179+ ?: ?=(%const -.case) `val.literal.case
13180+ ?. ?=(%cell -.case) ~
13181+ ?. ?=(%const -.hed.case) ~
13182+ `val.literal.hed.case
13183+ ?~ head ~
13184+ ?: (~(has in:..zuse seen) u.head) ~
13185+ =. seen (~(put in:..zuse seen) u.head)
13186+ =? found =(tag u.head)
13187+ ?^(found ~ `case)
13188+ $(remaining t.remaining)
13189+::
13190+++ program-single-case-fit
13191+ |= [actual=itype expected=itype sub=isub next=@ud]
13192+ ^- ifit
13193+ =. actual (itype-normalize actual sub)
13194+ =. expected (itype-normalize expected sub)
13195+ ?. ?=(%union -.expected) [%unknown ~]
13196+ =/ found=(unit itype)
13197+ ?: ?=(%const -.actual) `actual
13198+ ?: ?=(%tag -.actual) `actual
13199+ ?: ?=(%cell -.actual) `actual
13200+ ?. ?=(%union -.actual) ~
13201+ ?. ?=([* ~] cases.actual) ~
13202+ `i.cases.actual
13203+ ?~ found [%unknown ~]
13204+ =/ case=itype u.found
13205+ =/ tag=(unit lit)
13206+ ?: ?=(%const -.case) `literal.case
13207+ ?: ?=(%tag -.case) `literal.case
13208+ ?. ?=(%cell -.case) ~
13209+ =/ head=itype (projection-field-target hed.case)
13210+ ?: ?=(%const -.head) `literal.head
13211+ ?: ?=(%tag -.head) `literal.head
13212+ ~
13213+ ?~ tag [%unknown ~]
13214+ =/ chosen=(unit itype) (program-union-tag-case expected val.u.tag)
13215+ ?~ chosen [%unknown ~]
13216+ ?: |(?=(%const -.case) ?=(%tag -.case))
13217+ ?. ?=(%const -.u.chosen) [%unknown ~]
13218+ (itype-fit case u.chosen sub next)
13219+ ?. ?=(%cell -.case) [%unknown ~]
13220+ ?. ?=(%cell -.u.chosen) [%unknown ~]
13221+ =/ head-fit=ifit (itype-fit hed.case hed.u.chosen sub next)
13222+ ?. ?=(%ok -.head-fit) head-fit
13223+ (itype-fit tal.case tal.u.chosen sub.head-fit next.head-fit)
13224+::
13225+++ program-single-generic-fit
13226+ |= [actual=itype expected=itype sub=isub next=@ud]
13227+ ^- ifit
13228+ =. actual (itype-normalize actual sub)
13229+ =. expected (itype-normalize expected sub)
13230+ ?. &(?=(%union -.actual) ?=(%union -.expected)) [%unknown ~]
13231+ ?~ origin.actual [%unknown ~]
13232+ ?. =(origin.actual origin.expected) [%unknown ~]
13233+ ?. ?=([* ~] args.actual) [%unknown ~]
13234+ ?. ?=([* ~] args.expected) [%unknown ~]
13235+ =/ argument-fit=ifit (direct-invariant i.args.actual i.args.expected sub next)
13236+ ?: ?=(%ok -.argument-fit) argument-fit
13237+ (program-single-case-fit i.args.actual i.args.expected sub next)
13238+::
13239+++ program-keyed-product-fit
13240+ |= [actual=itype expected=itype element=ischeme sub=isub next=@ud]
13241+ ^- ifit
13242+ =. actual (itype-normalize actual sub)
13243+ =. expected (itype-normalize expected sub)
13244+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) [%unknown ~]
13245+ =/ key-fit=ifit
13246+ (itype-fit (projection-field-target hed.actual) (projection-field-target hed.expected) sub next)
13247+ ?. ?=(%ok -.key-fit) key-fit
13248+ =/ actual-el=itype
13249+ (itype-normalize (projection-field-target tal.actual) sub.key-fit)
13250+ =/ expected-el=itype
13251+ (itype-normalize (projection-field-target tal.expected) sub.key-fit)
13252+ ?. &(?=(%union -.actual-el) ?=(%union -.expected-el)) [%unknown ~]
13253+ ?. =(origin.actual-el origin.expected-el) [%unknown ~]
13254+ ?. ?=([* ~] args.actual-el) [%unknown ~]
13255+ ?. ?=([* ~] args.expected-el) [%unknown ~]
13256+ =/ canonical-actual=(unit itype)
13257+ (template-apply element ~[i.args.actual-el])
13258+ =/ canonical-expected=(unit itype)
13259+ (template-apply element ~[i.args.expected-el])
13260+ ?~ canonical-actual [%unknown ~]
13261+ ?~ canonical-expected [%unknown ~]
13262+ =/ actual-check=ifit
13263+ (direct-invariant actual-el u.canonical-actual sub.key-fit next.key-fit)
13264+ ?. ?=(%ok -.actual-check) actual-check
13265+ =/ expected-check=ifit
13266+ (direct-invariant expected-el u.canonical-expected sub.actual-check next.actual-check)
13267+ ?. ?=(%ok -.expected-check) expected-check
13268+ =/ case-fit=ifit
13269+ (program-single-case-fit i.args.actual-el i.args.expected-el sub.expected-check next.expected-check)
13270+ case-fit
13271+::
13272+:: A direct view without a keyed each/turn site still needs the message type
13273+:: from the checked update. Recover only that closed component; final main
13274+:: checking remains the canonical program-kind boundary.
13275+++ program-plain-view-context
13276+ |= [parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
13277+ ^- (unit iresolved)
13278+ =/ env=ienv env.resolution
13279+ ?^ (ienv-lookup %main env) ~
13280+ ?^ (ienv-lookup view.parts env) ~
13281+ =/ relation=(unit [message=itype model=itype])
13282+ (program-update-relation update.parts ds env)
13283+ ?~ relation ~
13284+ =/ views=(list def)
13285+ (skim ds |=(d=def &(?=(%value -.d) =(view.parts name.d))))
13286+ ?. ?=([* ~] views) ~
13287+ =/ view-def=def i.views
13288+ ?> ?=(%value -.view-def)
13289+ =/ written-view=(unit sample) (direct-gate-sample view-def)
13290+ ?~ written-view ~
13291+ =/ body=expr
13292+ ?- -.val.view-def
13293+ %gate body.val.view-def
13294+ %gate-wide body.val.view-def
13295+ * !!
13296+ ==
13297+ =/ sites=(unit (list iview-site)) (program-view-sites body ~)
13298+ ?~ sites ~
13299+ ?^ u.sites ~
13300+ ?~ prelude.initial ~
13301+ ?~ (ienv-lookup %program values.u.prelude.initial) ~
13302+ =/ element=(unit ischeme) (find-jibb-mold %element u.prelude.initial)
13303+ ?~ element ~
13304+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
13305+ ?~ heads ~
13306+ ?~ (~(get by gates.u.heads) %program) ~
13307+ =/ checked=(map term def) (direct-checked-gates ds env)
13308+ =/ templates=ienv
13309+ (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
13310+ =/ scanned=(unit dgscan)
13311+ (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
13312+ ?~ scanned ~
13313+ =. next.initial (dg-next-id ids.u.scanned 0)
13314+ =/ view-state=istate (reserve-def-caps val.view-def initial)
13315+ =/ sam=isample-result (infer-sample u.written-view env view-state)
13316+ ?: ?=(%| -.sam) ~
13317+ =/ actual-model=itype (program-inferred-sample typ.p.sam u.written-view)
13318+ ?. ?=(~ (itype-vars actual-model)) ~
13319+ ?: (itype-has-tag actual-model) ~
13320+ =/ model-fit=ifit
13321+ (direct-invariant actual-model model.u.relation sub.state.p.sam next.state.p.sam)
13322+ ?. ?=(%ok -.model-fit) ~
13323+ =/ product=(unit itype) (template-apply u.element ~[message.u.relation])
13324+ ?~ product ~
13325+ =/ st=istate
13326+ state.p.sam(sub sub.model-fit, next next.model-fit, gate-defs checked, head-evidence heads)
13327+ =/ inferred=iresult
13328+ (infer-call-context-arg body u.product env.p.sam st (span-of body))
13329+ ?: ?=(%| -.inferred) ~
13330+ =/ product-fit=ifit
13331+ (itype-fit typ.p.inferred u.product sub.state.p.inferred next.state.p.inferred)
13332+ ?. ?=(%ok -.product-fit) ~
13333+ =/ merged-product=itype
13334+ (itype-merge-faces typ.p.inferred u.product sub.product-fit)
13335+ =/ actual-cast=itype [%fn typ.p.sam merged-product]
13336+ =/ closed=itype [%fn typ.p.sam u.product]
13337+ =/ cast=ifit
13338+ (itype-fit actual-cast closed sub.product-fit next.product-fit)
13339+ ?. ?=(%ok -.cast) ~
13340+ =/ merged=itype (itype-merge-faces actual-cast closed sub.cast)
13341+ =/ adjusted=iresult
13342+ [%& merged state.p.inferred(sub sub.cast, next next.cast)]
13343+ =/ added=(unit iadded-definition)
13344+ (add-supported-result view-def adjusted view-state env checked artifacts.resolution)
13345+ ?~ added ~
13346+ =/ recovered=(unit ischeme) (ienv-lookup view.parts env.u.added)
13347+ ?~ recovered ~
13348+ ?. ?=(~ vars.u.recovered) ~
13349+ ?. ?=(~ (itype-vars typ.u.recovered)) ~
13350+ `[env.u.added grouped.resolution artifacts.u.added]
13351+::
13352+:: Recover exactly one direct keyed each/turn row mapper, then its view.
13353+:: The prelude's own each and turn schemes determine the mapper gate: the
13354+:: key is inferred from the mapper body, never selected by this recovery.
13355+++ program-view-context
13356+ |= [parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
13357+ ^- (unit iresolved)
13358+ =/ env=ienv env.resolution
13359+ ?^ (ienv-lookup %main env) ~
13360+ ?^ (ienv-lookup view.parts env) ~
13361+ =/ relation=(unit [message=itype model=itype])
13362+ (program-update-relation update.parts ds env)
13363+ ?~ relation ~
13364+ =/ views=(list def)
13365+ (skim ds |=(d=def &(?=(%value -.d) =(view.parts name.d))))
13366+ ?. ?=([* ~] views) ~
13367+ =/ view-def=def i.views
13368+ ?> ?=(%value -.view-def)
13369+ =/ written-view=(unit sample) (direct-gate-sample view-def)
13370+ ?~ written-view ~
13371+ =/ view-body=expr
13372+ ?- -.val.view-def
13373+ %gate body.val.view-def
13374+ %gate-wide body.val.view-def
13375+ * !!
13376+ ==
13377+ =/ sites=(unit (list iview-site)) (program-view-sites view-body ~)
13378+ ?~ sites ~
13379+ ?. ?=([* ~] u.sites) ~
13380+ =/ site=iview-site i.u.sites
13381+ =/ component-names=(list term) ~[init.parts update.parts view.parts subs.parts]
13382+ ?: (lien component-names |=(n=term =(n mapper.site))) ~
13383+ ?^ (ienv-lookup mapper.site env) ~
13384+ =/ mappers=(list def)
13385+ (skim ds |=(d=def &(?=(%value -.d) =(mapper.site name.d))))
13386+ ?. ?=([* ~] mappers) ~
13387+ =/ mapper-def=def i.mappers
13388+ ?> ?=(%value -.mapper-def)
13389+ =/ written-mapper=(unit sample) (direct-gate-sample mapper-def)
13390+ ?~ written-mapper ~
13391+ ?~ prelude.initial ~
13392+ =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)
13393+ =/ each-scheme=(unit ischeme) (ienv-lookup %each values.u.prelude.initial)
13394+ =/ turn-scheme=(unit ischeme) (ienv-lookup %turn values.u.prelude.initial)
13395+ =/ element=(unit ischeme) (find-jibb-mold %element u.prelude.initial)
13396+ =/ list-template=(unit ischeme) (find-jibb-mold %list u.prelude.initial)
13397+ ?~ program ~
13398+ ?~ each-scheme ~
13399+ ?~ turn-scheme ~
13400+ ?~ element ~
13401+ ?~ list-template ~
13402+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
13403+ ?~ heads ~
13404+ =/ written-program=(unit def) (~(get by gates.u.heads) %program)
13405+ =/ written-each=(unit def) (~(get by gates.u.heads) %each)
13406+ =/ written-turn=(unit def) (~(get by gates.u.heads) %turn)
13407+ ?~ written-program ~
13408+ ?~ written-each ~
13409+ ?~ written-turn ~
13410+ =/ program-sample=(unit sample) (direct-gate-sample u.written-program)
13411+ =/ each-sample=(unit sample) (direct-gate-sample u.written-each)
13412+ =/ turn-sample=(unit sample) (direct-gate-sample u.written-turn)
13413+ ?~ program-sample ~
13414+ ?~ each-sample ~
13415+ ?~ turn-sample ~
13416+ ?. ?=(%cell -.u.program-sample) ~
13417+ ?. ?=([* * * * ~] items.u.program-sample) ~
13418+ =/ turn-names=(unit [first=(unit term) second=(unit term)])
13419+ (program-two-slot-names u.turn-sample)
13420+ ?~ turn-names ~
13421+ =/ checked=(map term def) (direct-checked-gates ds env)
13422+ =/ templates=ienv
13423+ (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
13424+ =/ scanned=(unit dgscan)
13425+ (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
13426+ ?~ scanned ~
13427+ =. next.initial (dg-next-id ids.u.scanned 0)
13428+ =/ view-state=istate (reserve-def-caps val.view-def initial)
13429+ =/ sam=isample-result (infer-sample u.written-view env view-state)
13430+ ?: ?=(%| -.sam) ~
13431+ =/ actual-model=itype (program-inferred-sample typ.p.sam u.written-view)
13432+ =/ model-fit=ifit
13433+ (direct-invariant actual-model model.u.relation sub.state.p.sam next.state.p.sam)
13434+ ?. ?=(%ok -.model-fit) ~
13435+ =/ xs-result=iresult
13436+ (infer-fragment xs.site env.p.sam state.p.sam(sub sub.model-fit, next next.model-fit))
13437+ ?: ?=(%| -.xs-result) ~
13438+ =/ element-var=itype [%var next.state.p.xs-result]
13439+ =/ list-a=(unit itype) (template-apply u.list-template ~[element-var])
13440+ ?~ list-a ~
13441+ =/ xs-fit=ifit
13442+ (itype-fit typ.p.xs-result u.list-a sub.state.p.xs-result +(next.state.p.xs-result))
13443+ ?. ?=(%ok -.xs-fit) ~
13444+ =/ closed-xs=itype (itype-normalize u.list-a sub.xs-fit)
13445+ ?^ (itype-vars closed-xs) ~
13446+ ?: (itype-has-tag closed-xs) ~
13447+ =/ each-instance=[typ=itype state=istate]
13448+ (instantiate-scheme u.each-scheme state.p.xs-result(sub sub.xs-fit, next next.xs-fit))
13449+ ?. ?=(%fn -.typ.each-instance) ~
13450+ =/ turn-instance=[typ=itype state=istate]
13451+ (instantiate-scheme u.turn-scheme state.each-instance)
13452+ ?. ?=(%fn -.typ.turn-instance) ~
13453+ ?. ?=(%cell -.sample.typ.turn-instance) ~
13454+ =/ element-message=(unit itype)
13455+ (template-apply u.element ~[message.u.relation])
13456+ ?~ element-message ~
13457+ =/ each-fit=ifit
13458+ (itype-fit product.typ.each-instance u.element-message sub.state.turn-instance next.state.turn-instance)
13459+ ?. ?=(%ok -.each-fit) ~
13460+ =/ each-input=itype
13461+ (program-inferred-sample sample.typ.each-instance u.each-sample)
13462+ =/ turn-fit=ifit
13463+ (itype-fit product.typ.turn-instance each-input sub.each-fit next.each-fit)
13464+ ?. ?=(%ok -.turn-fit) ~
13465+ =/ turn-list=itype
13466+ (program-inferred-slot hed.sample.typ.turn-instance first.u.turn-names)
13467+ =/ list-fit=ifit
13468+ (itype-fit closed-xs turn-list sub.turn-fit next.turn-fit)
13469+ ?. ?=(%ok -.list-fit) ~
13470+ =/ mapper-type=itype
13471+ (program-inferred-slot tal.sample.typ.turn-instance second.u.turn-names)
13472+ =/ expected-mapper=itype (itype-normalize mapper-type sub.list-fit)
13473+ ?. ?=(%fn -.expected-mapper) ~
13474+ ?^ (itype-vars sample.expected-mapper) ~
13475+ ?: (itype-has-tag sample.expected-mapper) ~
13476+ :: These faces come from the source-backed each sample. Keeping them in
13477+ :: the expected mapper product lets ordinary tuple inference supply key/el.
13478+ ?. ?=(%cell -.product.expected-mapper) ~
13479+ ?. ?=(%face -.hed.product.expected-mapper) ~
13480+ ?. =(%key name.hed.product.expected-mapper) ~
13481+ ?. ?=(%face -.tal.product.expected-mapper) ~
13482+ ?. =(%el name.tal.product.expected-mapper) ~
13483+ =/ mapper-state=istate
13484+ (reserve-def-caps val.mapper-def initial(next next.list-fit))
13485+ =/ mapper-sam=isample-result (infer-sample u.written-mapper env mapper-state)
13486+ ?: ?=(%| -.mapper-sam) ~
13487+ =/ mapper-input=itype (program-inferred-sample typ.p.mapper-sam u.written-mapper)
13488+ =/ mapper-sample-fit=ifit
13489+ (direct-invariant mapper-input sample.expected-mapper sub.state.p.mapper-sam next.state.p.mapper-sam)
13490+ ?. ?=(%ok -.mapper-sample-fit) ~
13491+ =/ mapper-product=itype
13492+ (itype-normalize product.expected-mapper sub.mapper-sample-fit)
13493+ =/ mapper-body=expr
13494+ ?- -.val.mapper-def
13495+ %gate body.val.mapper-def
13496+ %gate-wide body.val.mapper-def
13497+ * !!
13498+ ==
13499+ =/ mapper-inferred=iresult
13500+ (infer-call-context-arg mapper-body mapper-product env.p.mapper-sam state.p.mapper-sam(sub sub.mapper-sample-fit, next next.mapper-sample-fit) (span-of mapper-body))
13501+ ?: ?=(%| -.mapper-inferred) ~
13502+ =/ ordinary-product-fit=ifit
13503+ (itype-fit typ.p.mapper-inferred mapper-product sub.state.p.mapper-inferred next.state.p.mapper-inferred)
13504+ =/ mapper-product-fit=ifit
13505+ ?: ?=(%ok -.ordinary-product-fit) ordinary-product-fit
13506+ (program-keyed-product-fit typ.p.mapper-inferred mapper-product u.element sub.state.p.mapper-inferred next.state.p.mapper-inferred)
13507+ ?. ?=(%ok -.mapper-product-fit) ~
13508+ =/ closed-mapper-product=itype
13509+ (itype-normalize mapper-product sub.mapper-product-fit)
13510+ ?^ (itype-vars closed-mapper-product) ~
13511+ ?: (itype-has-tag closed-mapper-product) ~
13512+ =/ merged-mapper-product=itype
13513+ (itype-merge-faces typ.p.mapper-inferred closed-mapper-product sub.mapper-product-fit)
13514+ =/ mapper-cast=itype [%fn typ.p.mapper-sam merged-mapper-product]
13515+ =/ closed-mapper=itype [%fn typ.p.mapper-sam closed-mapper-product]
13516+ =/ mapper-cast-fit=ifit
13517+ (itype-fit mapper-cast closed-mapper sub.mapper-product-fit next.mapper-product-fit)
13518+ ?. ?=(%ok -.mapper-cast-fit) ~
13519+ =/ merged-mapper=itype
13520+ (itype-merge-faces mapper-cast closed-mapper sub.mapper-cast-fit)
13521+ =/ mapper-adjusted=iresult
13522+ [%& merged-mapper state.p.mapper-inferred(sub sub.mapper-cast-fit, next next.mapper-cast-fit)]
13523+ =/ mapper-added=(unit iadded-definition)
13524+ (add-supported-result mapper-def mapper-adjusted mapper-state env checked artifacts.resolution)
13525+ ?~ mapper-added ~
13526+ =/ mapper-scheme=(unit ischeme) (ienv-lookup mapper.site env.u.mapper-added)
13527+ ?~ mapper-scheme ~
13528+ ?. ?=(~ vars.u.mapper-scheme) ~
13529+ ?. ?=(~ (itype-vars typ.u.mapper-scheme)) ~
13530+ =/ program-instance=[typ=itype state=istate]
13531+ (instantiate-scheme u.program state.p.sam(next next.mapper-cast-fit))
13532+ ?. ?=(%fn -.typ.program-instance) ~
13533+ ?. ?=(%cell -.sample.typ.program-instance) ~
13534+ ?. ?=(%cell -.tal.sample.typ.program-instance) ~
13535+ ?. ?=(%cell -.tal.tal.sample.typ.program-instance) ~
13536+ =/ expected-view=(unit itype)
13537+ (direct-slot-body hed.tal.tal.sample.typ.program-instance (direct-sample-name i.t.t.items.u.program-sample))
13538+ ?~ expected-view ~
13539+ ?. ?=(%fn -.u.expected-view) ~
13540+ =/ canonical-view=itype [%fn model.u.relation u.element-message]
13541+ =/ view-fit=ifit
13542+ (direct-invariant canonical-view u.expected-view sub.state.program-instance next.state.program-instance)
13543+ ?. ?=(%ok -.view-fit) ~
13544+ =/ closed-view=itype
13545+ (itype-normalize [%fn typ.p.sam u.element-message] sub.view-fit)
13546+ ?. ?=(%fn -.closed-view) ~
13547+ =/ view-env=ienv [[mapper.site u.mapper-scheme] env.p.sam]
13548+ =/ final-view-state=istate
13549+ (reserve-def-caps val.view-def state.p.sam(next next.view-fit, gate-defs checked.u.mapper-added, head-evidence heads))
13550+ =/ inferred=iresult
13551+ (infer-call-context-arg view-body product.closed-view view-env final-view-state (span-of view-body))
13552+ ?: ?=(%| -.inferred) ~
13553+ =/ product-fit=ifit
13554+ (itype-fit typ.p.inferred product.closed-view sub.state.p.inferred next.state.p.inferred)
13555+ ?. ?=(%ok -.product-fit) ~
13556+ =/ merged-product=itype
13557+ (itype-merge-faces typ.p.inferred product.closed-view sub.product-fit)
13558+ =/ actual-cast=itype [%fn typ.p.sam merged-product]
13559+ =/ cast=ifit
13560+ (itype-fit actual-cast closed-view sub.product-fit next.product-fit)
13561+ ?. ?=(%ok -.cast) ~
13562+ =/ merged=itype (itype-merge-faces actual-cast closed-view sub.cast)
13563+ =/ adjusted=iresult
13564+ [%& merged state.p.inferred(sub sub.cast, next next.cast)]
13565+ =/ added=(unit iadded-definition)
13566+ (add-supported-result view-def adjusted final-view-state env.u.mapper-added checked.u.mapper-added artifacts.u.mapper-added)
13567+ ?~ added ~
13568+ =/ recovered=(unit ischeme) (ienv-lookup view.parts env.u.added)
13569+ ?~ recovered ~
13570+ ?. ?=(~ vars.u.recovered) ~
13571+ ?. ?=(~ (itype-vars typ.u.recovered)) ~
13572+ `[env.u.added grouped.resolution artifacts.u.added]
13573+::
13574+++ program-init-null-sample
13575+ |= d=def
13576+ ^- ?
13577+ =/ written=(unit sample) (direct-gate-sample d)
13578+ ?~ written |
13579+ ?. ?=(%bare -.u.written) |
13580+ =/ sh=shape shape.u.written
13581+ ?. ?=(%const -.sh) |
13582+ =(%null form.lit.sh)
13583+::
13584+:: The tuple-ending-null initializer retry above intentionally keeps its own
13585+:: boundary. A direct null-sample initializer can instead receive the closed
13586+:: model already established by update, view and subscriptions.
13587+++ program-plain-init-context
13588+ |= [parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
13589+ ^- (unit iresolved)
13590+ =/ env=ienv env.resolution
13591+ ?^ (ienv-lookup %main env) ~
13592+ ?^ (ienv-lookup init.parts env) ~
13593+ ?~ (ienv-lookup update.parts env) ~
13594+ ?~ (ienv-lookup view.parts env) ~
13595+ ?~ (ienv-lookup subs.parts env) ~
13596+ =/ relation=(unit [message=itype model=itype])
13597+ (program-update-relation update.parts ds env)
13598+ ?~ relation ~
13599+ =/ inits=(list def)
13600+ (skim ds |=(d=def &(?=(%value -.d) =(init.parts name.d))))
13601+ ?. ?=([* ~] inits) ~
13602+ =/ init-def=def i.inits
13603+ ?> ?=(%value -.init-def)
13604+ ?. (program-init-null-sample init-def) ~
13605+ =/ written=(unit sample) (direct-gate-sample init-def)
13606+ ?~ written ~
13607+ =/ body=expr
13608+ ?- -.val.init-def
13609+ %gate body.val.init-def
13610+ %gate-wide body.val.init-def
13611+ * !!
13612+ ==
13613+ ?~ prelude.initial ~
13614+ ?~ (ienv-lookup %program values.u.prelude.initial) ~
13615+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
13616+ ?~ heads ~
13617+ ?~ (~(get by gates.u.heads) %program) ~
13618+ =/ checked=(map term def) (direct-checked-gates ds env)
13619+ =/ templates=ienv
13620+ (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
13621+ =/ scanned=(unit dgscan)
13622+ (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
13623+ ?~ scanned ~
13624+ =. next.initial (dg-next-id ids.u.scanned 0)
13625+ =/ init-state=istate (reserve-def-caps val.init-def initial)
13626+ =/ sam=isample-result (infer-sample u.written env init-state)
13627+ ?: ?=(%| -.sam) ~
13628+ ?. ?=(~ (itype-vars typ.p.sam)) ~
13629+ ?: (itype-has-tag typ.p.sam) ~
13630+ =/ st=istate state.p.sam(gate-defs checked, head-evidence heads)
13631+ =/ inferred=iresult
13632+ (infer-call-context-arg body model.u.relation env.p.sam st (span-of body))
13633+ ?: ?=(%| -.inferred) ~
13634+ =/ product-fit=ifit
13635+ (itype-fit typ.p.inferred model.u.relation sub.state.p.inferred next.state.p.inferred)
13636+ ?. ?=(%ok -.product-fit) ~
13637+ =/ merged-product=itype
13638+ (itype-merge-faces typ.p.inferred model.u.relation sub.product-fit)
13639+ =/ actual-cast=itype [%fn typ.p.sam merged-product]
13640+ =/ closed=itype [%fn typ.p.sam model.u.relation]
13641+ =/ cast=ifit
13642+ (itype-fit actual-cast closed sub.product-fit next.product-fit)
13643+ ?. ?=(%ok -.cast) ~
13644+ =/ merged=itype (itype-merge-faces actual-cast closed sub.cast)
13645+ =/ adjusted=iresult
13646+ [%& merged state.p.inferred(sub sub.cast, next next.cast)]
13647+ =/ added=(unit iadded-definition)
13648+ (add-supported-result init-def adjusted init-state env checked artifacts.resolution)
13649+ ?~ added ~
13650+ =/ recovered=(unit ischeme) (ienv-lookup init.parts env.u.added)
13651+ ?~ recovered ~
13652+ ?. ?=(~ vars.u.recovered) ~
13653+ ?. ?=(~ (itype-vars typ.u.recovered)) ~
13654+ `[env.u.added grouped.resolution artifacts.u.added]
13655+::
13656+:: Recover only the initializer of an already recognized direct program main.
13657+:: The derived call is evidence for an ordinary init/main retry, never an
13658+:: interface to publish on its own. Any failure returns the original resolution.
13659+++ program-init-context
13660+ |= [main=def parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
13661+ ^- (unit iresolved)
13662+ =/ env=ienv env.resolution
13663+ ?^ (ienv-lookup %main env) ~
13664+ ?^ (ienv-lookup init.parts env) ~
13665+ =/ update=(unit ischeme) (ienv-lookup update.parts env)
13666+ =/ view=(unit ischeme) (ienv-lookup view.parts env)
13667+ =/ subs=(unit ischeme) (ienv-lookup subs.parts env)
13668+ ?~ update ~
13669+ ?~ view ~
13670+ ?~ subs ~
13671+ =/ inits=(list def)
13672+ (skim ds |=(d=def &(?=(%value -.d) =(init.parts name.d))))
13673+ ?. ?=([* ~] inits) ~
13674+ =/ init-def=def i.inits
13675+ ?> ?=(%value -.init-def)
13676+ ?. (program-init-tuple-null init-def) ~
13677+ =/ args=(unit (list expr)) (program-main-args main)
13678+ ?~ args ~
13679+ ?~ prelude.initial ~
13680+ =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)
13681+ ?~ program ~
13682+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
13683+ ?~ heads ~
13684+ =/ written=(unit def) (~(get by gates.u.heads) %program)
13685+ ?~ written ~
13686+ =/ written-sample=(unit sample) (direct-gate-sample u.written)
13687+ ?~ written-sample ~
13688+ ?. ?=(%cell -.u.written-sample) ~
13689+ ?~ items.u.written-sample ~
13690+ =/ checked=(map term def) (direct-checked-gates ds env)
13691+ =/ templates=ienv
13692+ (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
13693+ =/ scanned=(unit dgscan)
13694+ (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
13695+ ?~ scanned ~
13696+ =. next.initial (dg-next-id ids.u.scanned 0)
13697+ =/ instance=[typ=itype state=istate] (instantiate-scheme u.program initial)
13698+ ?. ?=(%fn -.typ.instance) ~
13699+ ?. ?=(%cell -.sample.typ.instance) ~
13700+ =/ expected-init=(unit itype)
13701+ (direct-slot-body hed.sample.typ.instance (direct-sample-name i.items.u.written-sample))
13702+ ?~ expected-init ~
13703+ ?. ?=(%fn -.u.expected-init) ~
13704+ ?. ?=(%var -.sample.u.expected-init) ~
13705+ =/ data=@ud id.sample.u.expected-init
13706+ =/ init-var=itype [%var next.state.instance]
13707+ =/ st=istate state.instance(next +(next.state.instance))
13708+ =/ up=[typ=itype state=istate] (instantiate-scheme u.update st)
13709+ =/ vw=[typ=itype state=istate] (instantiate-scheme u.view state.up)
13710+ =/ sb=[typ=itype state=istate] (instantiate-scheme u.subs state.vw)
13711+ =. st state.sb(gate-defs checked, head-evidence heads)
13712+ =/ actual=itype [%cell init-var [%cell typ.up [%cell typ.vw typ.sb]]]
13713+ =/ fit=ifit
13714+ (direct-positional-fit u.args items.u.written-sample actual sample.typ.instance env st sub.st next.st)
13715+ ?. ?=(%ok -.fit) ~
13716+ =/ actual-final=itype (itype-normalize actual sub.fit)
13717+ =/ expected-final=itype (itype-normalize sample.typ.instance sub.fit)
13718+ =/ open=(list @ud)
13719+ (unique-type-vars (weld (itype-vars actual-final) (itype-vars expected-final)))
13720+ ?. (levy open |=(n=@ud =(data n))) ~
13721+ ?: |((itype-has-tag actual-final) (itype-has-tag expected-final)) ~
13722+ =/ replay=ifit
13723+ (direct-positional-fit u.args items.u.written-sample actual sample.typ.instance env st sub.fit next.fit)
13724+ ?. ?=(%ok -.replay) ~
13725+ ?. &(=(sub.fit sub.replay) =(next.fit next.replay)) ~
13726+ =/ expected=itype (itype-normalize u.expected-init sub.fit)
13727+ ?. ?=(%fn -.expected) ~
13728+ =. st st(sub sub.fit, next next.fit)
13729+ =/ init-state=istate (reserve-def-caps val.init-def st)
13730+ =/ inferred=iresult (infer-fragment val.init-def env init-state)
13731+ =? inferred ?=(%| -.inferred) (infer-recursive-gate init-def env init-state)
13732+ ?: ?=(%| -.inferred) ~
13733+ ?. ?=(%fn -.typ.p.inferred) ~
13734+ ?^ (itype-vars sample.typ.p.inferred) ~
13735+ =/ data-fit=ifit
13736+ (itype-fit sample.typ.p.inferred sample.expected sub.state.p.inferred next.state.p.inferred)
13737+ ?. ?=(%ok -.data-fit) ~
13738+ =/ closed=itype (itype-normalize expected sub.data-fit)
13739+ ?. ?=(%fn -.closed) ~
13740+ :: Resolve the ordinary tuple cast first, then check the complete gate.
13741+ :: General function fit remains unchanged; only this recovered candidate
13742+ :: receives the derived result context before its whole-type cast fit.
13743+ =/ product-fit=ifit
13744+ (itype-fit product.typ.p.inferred product.closed sub.data-fit next.data-fit)
13745+ ?. ?=(%ok -.product-fit) ~
13746+ =/ product=itype
13747+ (itype-merge-faces product.typ.p.inferred product.closed sub.product-fit)
13748+ =/ actual-cast=itype [%fn sample.typ.p.inferred product]
13749+ =/ cast=ifit
13750+ (itype-fit actual-cast closed sub.product-fit next.product-fit)
13751+ ?. ?=(%ok -.cast) ~
13752+ =/ merged=itype (itype-merge-faces actual-cast closed sub.cast)
13753+ =/ adjusted=iresult
13754+ [%& merged state.p.inferred(sub sub.cast, next next.cast)]
13755+ =/ added=(unit iadded-definition)
13756+ (add-supported-result init-def adjusted init-state env checked artifacts.resolution)
13757+ ?~ added ~
13758+ =/ recovered=(unit ischeme) (ienv-lookup init.parts env.u.added)
13759+ ?~ recovered ~
13760+ ?. ?=(~ vars.u.recovered) ~
13761+ ?. ?=(~ (itype-vars typ.u.recovered)) ~
13762+ `[env.u.added grouped.resolution artifacts.u.added]
13763+::
13764+++ derived-poke-command-scheme
13765+ |= [prelude=ifile action=itype]
13766+ ^- (unit ischeme)
13767+ =/ prep=iprelude [prelude ~ ~]
13768+ =/ raw=(unit ischeme) (compatible-raw-poke prep)
13769+ ?~ raw ~
13770+ =/ command=(unit ischeme) (find-jibb-mold %cmd prelude)
13771+ =/ unit-template=(unit ischeme) (find-jibb-mold %unit prelude)
13772+ ?~ command ~
13773+ ?~ unit-template ~
13774+ ?. (standard-unit-template u.unit-template /lib/jibb/prelude/jibb) ~
13775+ ?. ?=([@ ~] vars.u.command) ~
13776+ ?. ?=(%union -.typ.u.command) ~
13777+ ?. =(origin.typ.u.command `[/lib/jibb/prelude/jibb %cmd]) ~
13778+ ?. (identity-union-parameters vars.u.command args.typ.u.command) ~
13779+ =/ m=@ud i.vars.u.command
13780+ ?: (itype-var-is-atom m typ.u.command) ~
13781+ ?. (levy (itype-vars typ.u.command) |=(n=@ud =(n m))) ~
13782+ ?: (itype-has-tag typ.u.command) ~
13783+ =/ error=(unit itype) (template-apply u.unit-template ~[[%atom %t]])
13784+ ?~ error ~
13785+ ?. ?=(%union -.typ.u.raw) ~
13786+ =/ poke-case=itype
13787+ [%cell [%const [%term %tas %poke '%poke']] [%cell [%face %p typ.u.raw(label `'raw-poke.internal')] [%face %reply [%fn u.error [%var m]]]]]
13788+ =/ go-case=itype
13789+ [%cell [%const [%term %tas %go '%go']] [%face %url [%atom %t]]]
13790+ =/ wait-case=itype
13791+ [%cell [%const [%term %tas %wait '%wait']] [%cell [%face %gap [%atom %dr]] [%face %msg [%var m]]]]
13792+ =/ now-case=itype
13793+ [%cell [%const [%term %tas %now '%now']] [%face %reply [%fn [%atom %da] [%var m]]]]
13794+ =/ who-case=itype
13795+ [%cell [%const [%term %tas %who '%who']] [%face %reply [%fn [%atom %p] [%var m]]]]
13796+ ?. =(cases.typ.u.command ~[poke-case go-case wait-case now-case who-case]) ~
13797+ =/ command-result=(unit itype) (template-apply u.command ~[[%var 0]])
13798+ ?~ command-result ~
13799+ `[[%fn [%cell action [%fn u.error [%var 0]]] u.command-result] ~[0]]
13800+::
13801+++ store-derived-schemes
13802+ |= [prelude=ifile values=(list term) molds=(list term) state=itype action=itype]
13803+ ^- (unit [state=ischeme action=ischeme])
13804+ =/ prep=iprelude [prelude values molds]
13805+ =/ ask=(unit ischeme) (request-compatible-ask prep)
13806+ ?~ ask ~
13807+ ?^ (itype-vars state) ~
13808+ ?^ (itype-vars action) ~
13809+ ?: |((itype-has-tag state) (itype-has-tag action)) ~
13810+ =/ result=(unit itype) (template-apply u.ask ~[[%var 0]])
13811+ ?~ result ~
13812+ =/ request=ischeme [[%fn [%fn state [%var 0]] u.result] ~[0]]
13813+ =/ constructor=(unit ischeme) (derived-poke-command-scheme prelude action)
13814+ ?~ constructor ~
13815+ `[request u.constructor]
13816+::
13817+++ program-subs-watch
13818+ |= [d=def imports=ijimports graph=irequest-graph prelude=ifile]
13819+ ^- ?
13820+ ?. ?=(%value -.d) |
13821+ ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) |
13822+ =/ body=expr
13823+ ?- -.val.d
13824+ %gate body.val.d
13825+ %gate-wide body.val.d
13826+ * val.d
13827+ ==
13828+ =. body (program-transparent body)
13829+ ?. ?=(%list -.body) |
13830+ ?. ?=([* ~] items.body) |
13831+ =/ watch=expr (program-transparent i.items.body)
13832+ ?. ?=(%tuple -.watch) |
13833+ ?. ?=([* * ~] items.watch) |
13834+ =/ tag=item i.items.watch
13835+ =/ payload=item i.t.items.watch
13836+ ?. &(?=(~ face.tag) ?=(~ face.payload)) |
13837+ =/ tag-expr=expr (program-transparent val.tag)
13838+ ?. ?=(%lit -.tag-expr) |
13839+ ?. &(?=(%term form.lit.tag-expr) =(%watch val.lit.tag-expr)) |
13840+ =/ request=expr (program-transparent val.payload)
13841+ ?. ?=(%call -.request) |
13842+ ?. ?=([* ~] args.request) |
13843+ =/ head=expr (program-transparent head.request)
13844+ ?. ?=(%wing -.head) |
13845+ ?. ?=([@ @ ~] names.head) |
13846+ =/ case=term i.names.head
13847+ =/ face=term i.t.names.head
13848+ =/ callback=expr (program-transparent i.args.request)
13849+ ?. ?=(%ctor -.callback) |
13850+ ?. ?=(%term form.tag.callback) |
13851+ ?| ?=(^ (derived-request-member case face imports graph prelude))
13852+ ?=(^ (derived-store-request-member case face imports graph prelude))
13853+ ==
13854+::
13855+:: Exact derived-member and request-evidence identity, shared by direct
13856+:: program watches and direct data-page loads. Only a plain request in the
13857+:: selected interface's own source-backed graph can establish this shape.
13858+++ derived-request-member
13859+ |= [case=term face=term imports=ijimports graph=irequest-graph prelude=ifile]
13860+ ^- (unit ischeme)
13861+ =/ selected=(list [face=term interface=ifile])
13862+ (skim imports |=(j=[face=term interface=ifile] =(face face.j)))
13863+ ?. ?=([* ~] selected) ~
13864+ =/ iface=ifile interface.i.selected
13865+ =/ member=(unit ischeme) (ienv-lookup case values.iface)
13866+ ?~ member ~
13867+ ?~ source.iface ~
13868+ =/ evidence=(list irequest-evidence)
13869+ (skim requests.graph |=(r=irequest-evidence &(=(api-at.r at.iface) =(name.r case))))
13870+ ?. ?=([* ~] evidence) ~
13871+ =/ request-evidence=irequest-evidence i.evidence
13872+ ?. =(u.source.iface api-source.request-evidence) ~
13873+ ?. =(name.path.path.request-evidence case) ~
13874+ ?~ graph.iface ~
13875+ ?. (lien requests.u.graph.iface |=(r=irequest-evidence =(r request-evidence))) ~
13876+ ?. ?=(~ scry.path.path.request-evidence) ~
13877+ ?. &(?=(~ diffs.path.request-evidence) ?=(~ diffs.path.path.request-evidence)) ~
13878+ ?: (lien segments.path.path.request-evidence |=(p=pseg !?=(%knot -.p))) ~
13879+ ?. ?=([@ ~] vars.u.member) ~
13880+ =/ message=@ud i.vars.u.member
13881+ ?. ?=(%fn -.typ.u.member) ~
13882+ ?. ?=(%fn -.sample.typ.u.member) ~
13883+ ?. =(sample.sample.typ.u.member full.path.request-evidence) ~
13884+ ?. =(product.sample.typ.u.member [%var message]) ~
13885+ =/ prep=iprelude [prelude prelude-values.graph prelude-molds.graph]
13886+ =/ ask=(unit ischeme) (request-compatible-ask prep)
13887+ ?~ ask ~
13888+ =/ result=(unit itype) (template-apply u.ask ~[[%var message]])
13889+ ?~ result ~
13890+ ?. =(product.typ.u.member u.result) ~
13891+ member
13892+::
13893+:: Store state is watchable by definition, but only the actual derived member
13894+:: of the uniquely selected source-bound store interface proves that fact.
13895+++ derived-store-request-member
13896+ |= [case=term face=term imports=ijimports graph=irequest-graph prelude=ifile]
13897+ ^- (unit ischeme)
13898+ ?. =(%state case) ~
13899+ =/ selected=(list [face=term interface=ifile])
13900+ (skim imports |=(j=[face=term interface=ifile] =(face face.j)))
13901+ ?. ?=([* ~] selected) ~
13902+ =/ iface=ifile interface.i.selected
13903+ =/ member=(unit ischeme) (ienv-lookup %state values.iface)
13904+ ?~ member ~
13905+ ?~ source.iface ~
13906+ =/ evidence=(list istore-request-evidence)
13907+ (skim stores.graph |=(r=istore-request-evidence =(store-at.r at.iface)))
13908+ ?. ?=([* ~] evidence) ~
13909+ =/ request=istore-request-evidence i.evidence
13910+ ?. =(u.source.iface source.request) ~
13911+ ?~ graph.iface ~
13912+ ?. (lien stores.u.graph.iface |=(r=istore-request-evidence =(r request))) ~
13913+ =/ derived=(unit [state=ischeme action=ischeme])
13914+ (store-derived-schemes prelude prelude-values.graph prelude-molds.graph state.request action.request)
13915+ ?~ derived ~
13916+ ?. =(u.member state.u.derived) ~
13917+ =/ constructor=(unit ischeme) (ienv-lookup action-name.request values.iface)
13918+ ?~ constructor ~
13919+ ?. =(u.constructor action.u.derived) ~
13920+ member
13921+::
13922+++ program-main-context
13923+ |= [main=def ds=(list def) resolution=iresolved initial=istate]
13924+ ^- iresolved
13925+ ?^ (ienv-lookup %main env.resolution) resolution
13926+ =/ heads=(unit igate-prelude-evidence)
13927+ (direct-prelude-evidence ds prelude.initial)
13928+ ?~ heads resolution
13929+ =/ checked=(map term def) (direct-checked-gates ds env.resolution)
13930+ =/ completed=[env=ienv artifacts=(list iwidth-definition)]
13931+ (add-supported-defs-core ~[main] ds checked heads env.resolution molds.initial globals.initial externals.initial surs.initial mark-externals.initial marks.initial jimports.initial reserved-molds.initial at.initial prelude.initial artifacts.resolution grec-index.initial)
13932+ [env.completed grouped.resolution artifacts.completed]
13933+::
13934+:: A static main may retain a generic element message in its ordinary
13935+:: scheme. Instantiate that scheme, specialize it to canonical element !!,
13936+:: and publish only the resulting closed scheme.
13937+++ static-main-specialized
13938+ |= [env=ienv prelude=(unit ifile)]
13939+ ^- (unit ischeme)
13940+ ?~ prelude ~
13941+ =/ element=(unit ischeme) (find-jibb-mold %element u.prelude)
13942+ ?~ element ~
13943+ =/ main=(unit ischeme) (ienv-lookup %main env)
13944+ ?~ main ~
13945+ =/ canonical=(unit itype) (template-apply u.element ~[[%empty ~]])
13946+ ?~ canonical ~
13947+ =/ instance=[typ=itype state=istate] (instantiate-scheme u.main *istate)
13948+ =/ fit=ifit (itype-fit typ.instance u.canonical ~ next.state.instance)
13949+ ?. ?=(%ok -.fit) ~
13950+ =/ closed=itype (itype-normalize typ.instance sub.fit)
13951+ ?^ (itype-vars closed) ~
13952+ ?: (itype-has-tag closed) ~
13953+ ?. ?=(%union -.closed) ~
13954+ ?. ?=(%union -.u.canonical) ~
13955+ ?. &(=(origin.closed origin.u.canonical) =(args.closed args.u.canonical)) ~
13956+ =/ exact=ifit (direct-invariant closed u.canonical ~ next.fit)
13957+ ?. ?=(%ok -.exact) ~
13958+ `[u.canonical ~]
13959+::
13960+:: The load of a direct data page must itself be a direct gate whose
13961+:: transparent body is one plain derived request with a wing or ctor reply.
13962+++ page-load-derived
13963+ |= [name=term ds=(list def) imports=ijimports graph=irequest-graph prelude=ifile]
13964+ ^- ?
13965+ =/ loads=(list def)
13966+ (skim ds |=(d=def &(?=(%value -.d) =(name name.d))))
13967+ ?. ?=([* ~] loads) |
13968+ =/ load=def i.loads
13969+ ?> ?=(%value -.load)
13970+ ?. |(?=(%gate -.val.load) ?=(%gate-wide -.val.load)) |
13971+ =/ body=expr
13972+ ?- -.val.load
13973+ %gate body.val.load
13974+ %gate-wide body.val.load
13975+ * !!
13976+ ==
13977+ =. body (program-transparent body)
13978+ ?. ?=(%call -.body) |
13979+ ?. ?=([* ~] args.body) |
13980+ =/ head=expr (program-transparent head.body)
13981+ ?. ?=(%wing -.head) |
13982+ ?. ?=([@ @ ~] names.head) |
13983+ =/ reply=expr (program-transparent i.args.body)
13984+ ?. ?| &(?=(%wing -.reply) ?=([@ ~] names.reply))
13985+ &(?=(%ctor -.reply) ?=(%term form.tag.reply))
13986+ ==
13987+ |
13988+ ?=(^ (derived-request-member i.names.head i.t.names.head imports graph prelude))
13989+::
13990+++ page-main-closed
13991+ |= [parts=[load=term view=term] ds=(list def) env=ienv prelude=(unit ifile) imports=ijimports graph=irequest-graph]
13992+ ^- ?
13993+ ?~ prelude |
13994+ =/ page=(unit ischeme) (find-jibb-mold %page u.prelude)
13995+ ?~ page |
13996+ =/ main=(unit ischeme) (ienv-lookup %main env)
13997+ ?~ main |
13998+ ?. ?=(~ vars.u.main) |
13999+ ?. ?=(~ (itype-vars typ.u.main)) |
14000+ =/ instance=[typ=itype state=istate] (instantiate-scheme u.page *istate)
14001+ =/ main-fit=ifit (direct-invariant typ.u.main typ.instance ~ next.state.instance)
14002+ ?. ?=(%ok -.main-fit) |
14003+ (page-load-derived load.parts ds imports graph u.prelude)
14004+::
14005+++ program-main-closed
14006+ |= [parts=[init=term update=term view=term subs=term] ds=(list def) env=ienv prelude=(unit ifile) imports=ijimports graph=irequest-graph]
14007+ ^- ?
14008+ ?~ prelude |
14009+ ?~ (ienv-lookup %program values.u.prelude) |
14010+ =/ program=(unit ischeme) (find-jibb-mold %program u.prelude)
14011+ ?~ program |
14012+ =/ main=(unit ischeme) (ienv-lookup %main env)
14013+ ?~ main |
14014+ ?. ?=(~ vars.u.main) |
14015+ ?. ?=(~ (itype-vars typ.u.main)) |
14016+ =/ instance=[typ=itype state=istate] (instantiate-scheme u.program *istate)
14017+ =/ main-fit=ifit (direct-invariant typ.u.main typ.instance ~ next.state.instance)
14018+ ?. ?=(%ok -.main-fit) |
14019+ =/ init=(unit ischeme) (ienv-lookup init.parts env)
14020+ ?~ init |
14021+ ?. ?=(~ vars.u.init) |
14022+ ?. ?=(%fn -.typ.u.init) |
14023+ ?. ?=(~ (itype-vars sample.typ.u.init)) |
14024+ ?. ?=(~ (itype-vars product.typ.u.init)) |
14025+ =/ data=igate-free (gate-free-type sample.typ.u.init 256 ~)
14026+ ?. =(%yes verdict.data) |
14027+ =/ model=igate-free (gate-free-type product.typ.u.init left.data ~)
14028+ ?. =(%yes verdict.model) |
14029+ =/ subs=(list def)
14030+ (skim ds |=(d=def &(?=(%value -.d) =(subs.parts name.d))))
14031+ ?. ?=([* ~] subs) |
14032+ |((program-subs-empty i.subs) (program-subs-watch i.subs imports graph u.prelude))
14033+::
14034+:: The two outer sample faces are binder names, not part of the action/state
14035+:: relation. Leave every face inside either component untouched.
14036+++ store-update-unfaced
14037+ |= typ=itype
14038+ ^- itype
14039+ ?. ?=(%fn -.typ) typ
14040+ ?. ?=(%cell -.sample.typ) typ
14041+ =/ head=itype hed.sample.typ
14042+ =/ tail=itype tal.sample.typ
14043+ =? head ?=(%face -.head) body.head
14044+ =? tail ?=(%face -.tail) body.tail
14045+ typ(sample [%cell head tail])
14046+::
14047+:: The builder erases the action from main. Recover it only from the local
14048+:: poke mold and check both ordinary components invariantly.
14049+++ store-main-closed
14050+ |= [parts=[init=term update=term] action=term env=ienv molds=imold-types prelude=(unit ifile)]
14051+ ^- (unit ischeme)
14052+ ?~ prelude ~
14053+ =/ builder=(unit ischeme) (ienv-lookup %store values.u.prelude)
14054+ ?~ builder ~
14055+ ?. ?=([@ @ ~] vars.u.builder) ~
14056+ =/ state-var=@ud i.vars.u.builder
14057+ =/ action-var=@ud i.t.vars.u.builder
14058+ ?: =(state-var action-var) ~
14059+ =/ builder-sample=itype
14060+ [%cell [%face %init [%var state-var]] [%face %update [%fn [%cell [%var action-var] [%var state-var]] [%var state-var]]]]
14061+ =/ builder-product=itype [%cell [%face %init [%var state-var]] [%face %update [%noun ~]]]
14062+ ?. =(typ.u.builder [%fn builder-sample builder-product]) ~
14063+ =/ store=(unit ischeme) (find-jibb-mold %store u.prelude)
14064+ ?~ store ~
14065+ ?. ?=([@ ~] vars.u.store) ~
14066+ ?. =(typ.u.store [%cell [%face %init [%var i.vars.u.store]] [%face %update [%noun ~]]]) ~
14067+ =/ state=(unit ischeme) (find-jibb-mold %state [~ molds /tmp ~ ~ ~ ~ ~])
14068+ ?~ state ~
14069+ =/ action-mold=(unit ischeme) (find-jibb-mold action [~ molds /tmp ~ ~ ~ ~ ~])
14070+ ?~ action-mold ~
14071+ ?. &(?=(~ vars.u.state) ?=(~ (itype-vars typ.u.state))) ~
14072+ ?. &(?=(~ vars.u.action-mold) ?=(~ (itype-vars typ.u.action-mold))) ~
14073+ =/ canonical=(unit itype) (template-apply u.store ~[typ.u.state])
14074+ ?~ canonical ~
14075+ =/ main=(unit ischeme) (ienv-lookup %main env)
14076+ =/ main-fit=(unit ifit)
14077+ ?~(main ~ `(direct-invariant typ.u.main u.canonical ~ 0))
14078+ =/ main-ok=?
14079+ ?~ main &
14080+ ?. ?=(~ vars.u.main) |
14081+ ?. ?=(~ (itype-vars typ.u.main)) |
14082+ ?~ main-fit |
14083+ ?=(%ok -.u.main-fit)
14084+ ?. main-ok ~
14085+ =/ init=(unit ischeme) (ienv-lookup init.parts env)
14086+ ?~ init ~
14087+ ?. ?=(~ vars.u.init) ~
14088+ ?. ?=(~ (itype-vars typ.u.init)) ~
14089+ =/ init-fit=ifit (direct-invariant typ.u.init typ.u.state ~ 0)
14090+ ?. ?=(%ok -.init-fit) ~
14091+ =/ update=(unit ischeme) (ienv-lookup update.parts env)
14092+ ?~ update ~
14093+ ?. ?=(~ vars.u.update) ~
14094+ ?. ?=(~ (itype-vars typ.u.update)) ~
14095+ =/ expected=itype [%fn [%cell typ.u.action-mold typ.u.state] typ.u.state]
14096+ =/ update-fit=ifit (direct-invariant (store-update-unfaced typ.u.update) expected ~ 0)
14097+ ?. ?=(%ok -.update-fit) ~
14098+ `[u.canonical ~]
14099+::
1244614100++ infer-jibb-file
1244714101 |= [at=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle active=(list path) prelude-values=(list term) prelude-molds=(list term) cache=jcache prelude=(unit ifile)]
1244814102 ^- jfile-result
@@ -12459,10 +14113,12 @@
1245914113 =/ mod=module p.parsed
1246014114 =/ duplicate=(unit idiag) (duplicate-defs defs.mod)
1246114115 ?^ duplicate [%| [(show-duplicate-fields at src u.duplicate) ~]]
14116+ ?: &(?=([%ui %api *] at) ?=(^ (program-main-def defs.mod)))
14117+ [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]
1246214118 ?: ?=([%ui %api *] at)
1246314119 =/ iface=(unit ifile) (api-poke-interface at mod mark-externals prelude-values prelude-molds prelude)
1246414120 ?^ iface
12465− =/ checked=ifile u.iface(source `src, graph `[(silt `(list path)`~[at]) ~ modules prelude prelude-values prelude-molds externals mark-externals])
14121+ =/ checked=ifile u.iface(source `src, graph `[(silt `(list path)`~[at]) ~ ~ modules prelude prelude-values prelude-molds externals mark-externals])
1246614122 [%& [checked [[at checked] cache]]]
1246714123 ?~ prelude [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
1246814124 =/ prepared=iprelude [u.prelude prelude-values prelude-molds]
@@ -12481,18 +14137,29 @@
1248114137 (multi-request-interface-graph at src externals mark-externals modules active cache `prepared)
1248214138 ?: ?=(%| -.multi) [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
1248314139 [%& [iface.p.multi [[at iface.p.multi] cache.p.multi]]]
12484− ?. (module-scope-valid mod prelude-values prelude-molds)
12485− ?: (pending-declared-poke at mod prelude-values prelude-molds)
12486− [%| [(crip "module kind or scope needs unsupported inference: {(spud at)}") ~]]
12487− [%| [(crip "module has conflicting names: {(spud at)}") ~]]
12488− =/ vals=(list term) (global-value-names defs.mod)
12489− ?: (lien vals |=(n=term =(n %main)))
14140+ =/ main=(unit def) (program-main-def defs.mod)
14141+ =/ main-parts=(unit [init=term update=term view=term subs=term])
14142+ ?~(main ~ (program-main-parts u.main))
14143+ =/ page-parts=(unit [load=term view=term])
14144+ ?~(main ~ (page-main-parts u.main))
14145+ =/ store-parts=(unit [init=term update=term])
14146+ ?~(main ~ (store-main-parts u.main))
14147+ =/ declared=(unit istore-declaration)
14148+ ?~(store-parts ~ (store-declaration mod prelude-values prelude-molds))
14149+ ?: &(?=(^ store-parts) ?=(~ declared))
14150+ [%| [(crip "module kind or scope needs unsupported inference: {(spud at)}") ~]]
14151+ ?: &(?=([%ui %stores *] at) ?=(^ main) ?=(~ store-parts))
1249014152 [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]
14153+ =/ ds=(list def) ?~(declared defs.mod defs.u.declared)
14154+ =/ checking=module mod(defs ds)
14155+ ?. (module-scope-valid checking prelude-values prelude-molds)
14156+ [%| [(crip "module has conflicting names: {(spud at)}") ~]]
14157+ =/ vals=(list term) (global-value-names ds)
1249114158 =/ js=jimports-detailed-result (resolve-jibb-imports-detailed imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
1249214159 ?: ?=(%| -.js) [%| p.js]
1249314160 =/ collected=grec-collected
12494− ?^ imports.mod [(collect-simple-molds defs.mod) *(map term shape)]
12495− (grec-collect-molds defs.mod)
14161+ ?^ imports.mod [(collect-simple-molds ds) *(map term shape)]
14162+ (grec-collect-molds ds)
1249614163 =/ molds=imolds molds.collected
1249714164 =/ globals=(list term) (weld prelude-values (weld (import-binding-names imports.mod) vals))
1249814165 =/ surs=(list term) (collect-sur-imports imports.mod)
@@ -12523,24 +14190,96 @@
1252314190 [%| [msg `[at src name.witness cases.witness]]]
1252414191 =/ resolution=iresolved
1252514192 ?~ index
12526− (resolve-groups defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
12527− (resolve-groups-core defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude index)
14193+ (resolve-groups ds molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
14194+ (resolve-groups-core ds molds globals externals surs mark-externals marks resolved.p.js reserved at prelude index)
1252814195 =/ env=ienv env.resolution
14196+ =/ recovered=iresolved
14197+ ?~ main resolution
14198+ ?~ main-parts resolution
14199+ =/ updated=(unit iresolved)
14200+ (program-update-context u.main u.main-parts ds resolution state)
14201+ =/ with-update=iresolved ?~(updated resolution u.updated)
14202+ =/ subscribed=(unit iresolved)
14203+ (program-subs-context u.main-parts ds with-update state)
14204+ =/ with-subs=iresolved ?~(subscribed with-update u.subscribed)
14205+ =/ viewed=(unit iresolved)
14206+ (program-view-context u.main-parts ds with-subs state)
14207+ =/ with-keyed-view=iresolved ?~(viewed with-subs u.viewed)
14208+ =/ plain-view=(unit iresolved)
14209+ ?^(viewed ~ (program-plain-view-context u.main-parts ds with-keyed-view state))
14210+ =/ with-view=iresolved ?~(plain-view with-keyed-view u.plain-view)
14211+ =/ initialized=(unit iresolved)
14212+ (program-init-context u.main u.main-parts ds with-view state)
14213+ =/ with-initialized=iresolved ?~(initialized with-view u.initialized)
14214+ =/ plain-init=(unit iresolved)
14215+ ?^(initialized ~ (program-plain-init-context u.main-parts ds with-initialized state))
14216+ =/ components=iresolved ?~(plain-init with-initialized u.plain-init)
14217+ (program-main-context u.main ds components state)
14218+ =. env env.recovered
14219+ =. artifacts.resolution artifacts.recovered
1252914220 =. env
12530− ?: (module-values-complete defs.mod env) env
14221+ ?: (module-values-complete ds env) env
1253114222 ?: |(?=([%ui %stores *] at) ?=(^ imports.mod) ?=(^ prelude) ?=(^ prelude-values) ?=(^ prelude-molds)) env
1253214223 ?: (gth (met 3 src) 65.536) env
12533− ?: (gth (lent defs.mod) 64) env
12534− ?. (dg-source-candidate defs.mod 64) env
14224+ ?: (gth (lent ds) 64) env
14225+ ?. (dg-source-candidate ds 64) env
1253514226 =/ transaction=(unit dgcommit) (dg-root-source at src)
1253614227 ?~ transaction env
1253714228 ?: (dg-interface-safe env.u.transaction) env.u.transaction
1253814229 env
12539− ?. (module-values-complete defs.mod env)
14230+ =/ required=(list def)
14231+ ?~ store-parts ds
14232+ (skim ds |=(d=def !&(?=(%value -.d) =(%main name.d))))
14233+ ?. (module-values-complete required env)
14234+ =/ pending=(unit [at=span msg=tape]) (module-pending-tag required env state 64)
14235+ ?^ pending
14236+ [%| [(show-error src [at line.beg.at.u.pending col.beg.at.u.pending msg.u.pending]) ~]]
1254014237 [%| [(crip "module definitions need unsupported inference: {(spud at)}") ~]]
12541− =/ initial=irequest-graph [(silt `(list path)`~[at]) ~ modules prelude prelude-values prelude-molds externals mark-externals]
14238+ =/ initial=irequest-graph [(silt `(list path)`~[at]) ~ ~ modules prelude prelude-values prelude-molds externals mark-externals]
1254214239 =/ graph=(unit irequest-graph) (request-graph-merge resolved.p.js initial (add 1 (lent resolved.p.js)))
1254314240 ?~ graph [%| ['module request evidence needs unsupported inference' ~]]
14241+ =/ static-main=(unit ischeme)
14242+ ?~ main ~
14243+ ?^ main-parts ~
14244+ ?^ page-parts ~
14245+ ?^ store-parts ~
14246+ (static-main-specialized env prelude)
14247+ =? env ?=(^ static-main)
14248+ [[%main u.static-main] (skim env |=(entry=[name=term scheme=ischeme] !=(%main name.entry)))]
14249+ =/ store-main=(unit ischeme)
14250+ ?~ store-parts ~
14251+ ?~ declared ~
14252+ (store-main-closed u.store-parts action.u.declared env p.mts prelude)
14253+ =? env ?=(^ store-main)
14254+ [[%main u.store-main] (skim env |=(entry=[name=term scheme=ischeme] !=(%main name.entry)))]
14255+ =/ kind-ok=?
14256+ ?~ main &
14257+ ?^ main-parts (program-main-closed u.main-parts ds env prelude resolved.p.js u.graph)
14258+ ?^ page-parts (page-main-closed u.page-parts ds env prelude resolved.p.js u.graph)
14259+ ?^ store-parts ?=(^ store-main)
14260+ ?=(^ static-main)
14261+ ?. kind-ok
14262+ [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]
14263+ =/ store-derived=(unit [values=ienv evidence=istore-request-evidence])
14264+ ?~ declared ~
14265+ ?~ prelude ~
14266+ =/ state=(unit ischeme) (find-jibb-mold %state [~ p.mts at ~ ~ ~ ~ ~])
14267+ ?~ state ~
14268+ =/ action-mold=(unit ischeme) (find-jibb-mold action.u.declared [~ p.mts at ~ ~ ~ ~ ~])
14269+ ?~ action-mold ~
14270+ =/ schemes=(unit [state=ischeme action=ischeme])
14271+ (store-derived-schemes u.prelude prelude-values prelude-molds typ.u.state typ.u.action-mold)
14272+ ?~ schemes ~
14273+ =/ evidence=istore-request-evidence
14274+ [at src typ.u.state action.u.declared typ.u.action-mold]
14275+ `[~[[%state state.u.schemes] [action.u.declared action.u.schemes]] evidence]
14276+ ?: &(?=(^ declared) ?=(~ store-derived))
14277+ [%| [(crip "store derived gates need unsupported inference: {(spud at)}") ~]]
14278+ =? env ?=(^ store-derived) (weld values.u.store-derived env)
14279+ =? graph ?=(^ store-derived)
14280+ `u.graph(stores [evidence.u.store-derived stores.u.graph])
14281+ ?. (request-graph-bounded u.graph)
14282+ [%| ['module request evidence needs unsupported inference' ~]]
1254414283 =/ iface=ifile [env p.mts at ~ artifacts.resolution ~ `src graph]
1254514284 [%& [iface [[at iface] cache.p.js]]]
1254614285::
@@ -12650,15 +14389,13 @@
1265014389 =/ prelude-molds=(list term) molds.u.prepared
1265114390 =/ iface=(unit ifile) `iface.u.prepared
1265214391 ?. (module-scope-valid p.parsed prelude-values prelude-molds)
12653− ?: (pending-declared-poke file p.parsed prelude-values prelude-molds)
12654− 'partial inference; module not checked\0amodule kind or scope needs unsupported inference'
1265514392 'partial inference; module not checked\0amodule has conflicting names'
1265614393 =/ js=jimports-result
1265714394 (resolve-jibb-imports imports.p.parsed externals mark-externals modules ~[file] prelude-values prelude-molds ~ iface)
1265814395 ?: ?=(%| -.js) (of-wain:format ~['partial inference; module not checked' p.js])
1265914396 =/ scope-values=(list term)
1266014397 (weld prelude-values (weld (collect-sur-imports imports.p.parsed) (collect-mark-imports imports.p.parsed)))
12661− (golden-types-in-context file src externals mark-externals resolved.p.js scope-values prelude-molds iface)
14398+ (golden-types-in-context-core file src externals mark-externals resolved.p.js scope-values prelude-molds iface prepared)
1266214399::
1266314400:: +golden-types-with-marks: supply declared mark types separately from /sur
1266414401:: entries, as [mark result] with the result from +read-mark:jibb-import.
@@ -12689,6 +14426,10 @@
1268914426++ golden-types-in-context
1269014427 |= [file=path src=@t externals=iexternals mark-externals=imark-externals jimports=ijimports prelude-values=(list term) reserved-molds=(list term) prelude=(unit ifile)]
1269114428 ^- @t
14429+ (golden-types-in-context-core file src externals mark-externals jimports prelude-values reserved-molds prelude ~)
14430+++ golden-types-in-context-core
14431+ |= [file=path src=@t externals=iexternals mark-externals=imark-externals jimports=ijimports prelude-values=(list term) reserved-molds=(list term) prelude=(unit ifile) prepared=(unit iprelude)]
14432+ ^- @t
1269214433 =. reserved-molds (weld reserved-molds (turn jimports |=(j=[face=term interface=ifile] face.j)))
1269314434 =/ parsed (parse file src)
1269414435 ?: ?=(%| -.parsed) (show-error src p.parsed)
@@ -12708,19 +14449,27 @@
1270814449 =/ eligible=?
1270914450 ?& ?=(~ imports.p.parsed)
1271014451 ?=(~ jimports)
12711− ?=(~ prelude)
12712− ?=(~ prelude-values)
12713− ?=(~ reserved-molds)
1271414452 !?=([%ui %api *] file)
1271514453 !?=([%ui %stores *] file)
1271614454 !(lien (global-value-names ds) |=(n=term =(n %main)))
12717− (module-scope-valid p.parsed ~ ~)
1271814455 !(module-values-complete ds env)
1271914456 (lte (met 3 src) 65.536)
1272014457 (lte (lent ds) 64)
12721− (dg-source-candidate ds 64)
14458+ ?| &(?=(~ prepared) ?=(~ prelude) ?=(~ prelude-values) ?=(~ reserved-molds) (module-scope-valid p.parsed ~ ~) (dg-source-candidate ds 64))
14459+ ?& ?=(^ prepared)
14460+ ?=(^ prelude)
14461+ =(u.prelude iface.u.prepared)
14462+ =(prelude-values values.u.prepared)
14463+ =(reserved-molds molds.u.prepared)
14464+ (module-scope-valid p.parsed values.u.prepared molds.u.prepared)
14465+ (dg-prepared-candidate ds 64)
14466+ ==
14467+ ==
1272214468 ==
12723− =/ transaction=(unit dgcommit) ?:(eligible (dg-root-source file src) ~)
14469+ =/ transaction=(unit dgcommit)
14470+ ?. eligible ~
14471+ ?~ prepared (dg-root-source file src)
14472+ (dg-root-prepared file src u.prepared)
1272414473 =. recovered
1272514474 ?~ transaction ~
1272614475 ?. &((module-values-complete ds env.u.transaction) (dg-interface-safe env.u.transaction)) ~
@@ -13006,6 +14755,31 @@
1300614755 [%& result st(next +(next.st), obligations [ex ey obligations.st])]
1300714756 [%& typ.p.left state.p.right]
1300814757::
14758+:: A direct tuple literal may wait for a later exact result context.
14759+:: Each pending literal retains its source tag and its own fit obligation.
14760+++ dg-infer-tuple-items
14761+ |= [items=(list item) env=ienv state=istate]
14762+ ^- iresult
14763+ ?~ items [%| ["empty cell is not supported by partial inference" ~]]
14764+ =/ head=iresult (infer-fragment val.i.items env state)
14765+ ?: ?=(%| -.head) head
14766+ =/ typ=itype typ.p.head
14767+ =/ st=istate state.p.head
14768+ =/ adjusted=(unit [typ=itype state=istate])
14769+ ?. (dg-owned-arm-literal val.i.items typ tags.st sub.st next.state) `[typ st]
14770+ ?: (gth (lent obligations.st) 63) ~
14771+ =/ pending=itype [%var next.st]
14772+ =/ edge=dgo [typ pending (span-of val.i.items) at.i.items]
14773+ `[pending st(next +(next.st), obligations [edge obligations.st])]
14774+ ?~ adjusted [%| ["deferred tuple context needs unsupported inference" ~]]
14775+ =. typ typ.u.adjusted
14776+ =. st state.u.adjusted
14777+ =. typ ?~(face.i.items typ [%face u.face.i.items typ])
14778+ ?~ t.items [%& typ st]
14779+ =/ tail=iresult $(items t.items, state st)
14780+ ?: ?=(%| -.tail) tail
14781+ [%& [%cell typ typ.p.tail] state.p.tail]
14782+::
1300914783:: Deferred inference uses only source forms whose successful fit sites are
1301014784:: guarded below; a shared source-node budget bounds this screen.
1301114785++ dg-safe-expressions
@@ -13015,6 +14789,13 @@
1301514789 =/ first=(unit @ud) (dg-safe-expression i.todo fuel)
1301614790 ?~ first ~
1301714791 $(todo t.todo, fuel u.first)
14792+++ dg-safe-items
14793+ |= [items=(list item) fuel=@ud]
14794+ ^- (unit @ud)
14795+ ?~ items `fuel
14796+ =/ first=(unit @ud) (dg-safe-expression val.i.items fuel)
14797+ ?~ first ~
14798+ $(items t.items, fuel u.first)
1301814799++ dg-safe-expression
1301914800 |= [e=expr fuel=@ud]
1302014801 ^- (unit @ud)
@@ -13032,6 +14813,7 @@
1303214813 $(e final.e, fuel fuel)
1303314814 %gate $(e body.e, fuel fuel)
1303414815 %gate-wide $(e body.e, fuel fuel)
14816+ %tuple (dg-safe-items items.e fuel)
1303514817 %branch
1303614818 ?. (dg-boolean-patterns e) ~
1303714819 ?> ?=(^ arms.e)
@@ -13171,6 +14953,28 @@
1317114953 ?: (dg-direct-source val.i.ds 64) &
1317214954 $(ds t.ds, fuel (dec fuel))
1317314955::
14956+++ dg-prepared-source
14957+ |= [e=expr fuel=@ud]
14958+ ^- ?
14959+ ?: (dg-direct-source e fuel) &
14960+ ?: =(0 fuel) |
14961+ ?+ -.e |
14962+ %group $(e inner.e, fuel (dec fuel))
14963+ %gate $(e body.e, fuel (dec fuel))
14964+ %gate-wide $(e body.e, fuel (dec fuel))
14965+ %cast $(e val.e, fuel (dec fuel))
14966+ %body ?~(defs.e $(e final.e, fuel (dec fuel)) |)
14967+ %tuple &
14968+ ==
14969+++ dg-prepared-candidate
14970+ |= [ds=(list def) fuel=@ud]
14971+ ^- ?
14972+ ?~ ds |
14973+ ?: =(0 fuel) |
14974+ ?. ?=(%value -.i.ds) $(ds t.ds, fuel (dec fuel))
14975+ ?: (dg-prepared-source val.i.ds 64) &
14976+ $(ds t.ds, fuel (dec fuel))
14977+::
1317414978++ dg-interface-safe
1317514979 |= [env=ienv]
1317614980 ^- ?
@@ -13216,6 +15020,47 @@
1321615020 (dg-stage defs base base st ~ 64)
1321715021 ::
1321815022 [& (transact)]
15023+:: The caller supplies the trusted prepared prelude. This transaction is
15024+:: only report evidence; the ordinary module resolver does not publish it.
15025+++ dg-root-prepared
15026+ |= [at=path src=@t prepared=iprelude]
15027+ ^- (unit dgcommit)
15028+ ?: ?=([%ui %api *] at) ~
15029+ ?: ?=([%ui %stores *] at) ~
15030+ ?: (gth (met 3 src) 65.536) ~
15031+ =/ parsed (parse at src)
15032+ ?: ?=(%| -.parsed) ~
15033+ ?^ imports.p.parsed ~
15034+ ?. (module-scope-valid p.parsed values.prepared molds.prepared) ~
15035+ ?^ (duplicate-defs defs.p.parsed) ~
15036+ =/ defs=(list def) defs.p.parsed
15037+ ?: (gth (lent defs) 64) ~
15038+ ?: (lien (global-value-names defs) |=(n=term =(n %main))) ~
15039+ ?. (dg-prepared-candidate defs 64) ~
15040+ =/ local-molds=imolds (collect-simple-molds defs)
15041+ =/ globals=(list term) (weld values.prepared (global-value-names defs))
15042+ =/ iface=ifile iface.prepared
15043+ =/ prelude=(unit ifile) `iface
15044+ =/ resolution=iresolved
15045+ (resolve-groups defs local-molds globals ~ ~ ~ ~ ~ molds.prepared at prelude)
15046+ ?^ grouped.resolution ~
15047+ ?^ artifacts.resolution ~
15048+ =/ base=ienv env.resolution
15049+ =/ templates=ienv
15050+ (turn molds.iface |=(x=[name=term template=ischeme] [name.x template.x]))
15051+ =/ all-env=ienv (weld base (weld values.iface templates))
15052+ =/ free=(unit dgscan) (dg-env all-env ~ 32.768 ~)
15053+ ?~ free ~
15054+ ?^ ids.u.free ~
15055+ =/ all=(unit dgscan) (dg-all-env-ids all-env 32.768 ~)
15056+ ?~ all ~
15057+ =/ fresh=@ud (dg-next-id ids.u.all 0)
15058+ =/ st=istate *istate
15059+ =. st st(next fresh, defer `~, molds local-molds, globals globals, at at, reserved-molds molds.prepared, prelude prelude, top-molds (turn local-molds |=(m=[name=term body=shape] name.m)), in-mold |, jrec-fuel 256)
15060+ =/ checked-molds=(each imold-types @t) (module-mold-types local-molds st)
15061+ ?: ?=(%| -.checked-molds) ~
15062+ (dg-stage defs base base st ~ 64)
15063+::
1321915064++ dg-all-env-ids
1322015065 |= [env=ienv fuel=@ud ids=(list @ud)]
1322115066 ^- (unit dgscan)