@@ -5623,10 +5623,14 @@
56235623:: of an arbitrary ask value. Reader graphs and source inputs are trusted.
56245624+$ irequest-evidence
56255625 [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]
5626+:: Store requests have their own source-bound evidence. In particular, an
5627+:: API path certificate cannot make a store state member watchable, or vice versa.
5628++$ istore-request-evidence
5629+ [store-at=path source=@t state=itype action-name=term action=itype]
56265630:: A unit distinguishes a verified empty closure from a detached legacy file.
56275631:: The opaque prelude is an exact trusted input, not a recursive interface mold.
56285632+$ 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]
5633+ [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]
56305634+$ 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)]
56315635+$ ijimports (list [face=term interface=ifile])
56325636+$ icap [name=@t id=@ud at=span]
@@ -11676,6 +11680,25 @@
1167611680 =(externals.g externals)
1167711681 =(marks.g marks)
1167811682 ==
11683+++ request-graph-bounded
11684+ |= g=irequest-graph
11685+ ^- ?
11686+ =/ total=@ud (add (lent requests.g) (lent stores.g))
11687+ &((lte (lent ~(tap in:..zuse paths.g)) 256) (lte total 256))
11688+::
11689+++ store-graph-requests-add
11690+ |= [pending=(list istore-request-evidence) acc=(list istore-request-evidence) fuel=@ud]
11691+ ^- (unit (list istore-request-evidence))
11692+ ?~ pending `acc
11693+ ?: =(0 fuel) ~
11694+ =/ hit=(list istore-request-evidence)
11695+ (skim acc |=(x=istore-request-evidence =(store-at.x store-at.i.pending)))
11696+ ?^ hit
11697+ ?. ?=([* ~] hit) ~
11698+ ?. =(i.hit i.pending) ~
11699+ $(pending t.pending, fuel (dec fuel))
11700+ $(pending t.pending, acc [i.pending acc], fuel (dec fuel))
11701+::
1167911702++ request-graph-merge
1168011703 |= [imports=ijimports g=irequest-graph fuel=@ud]
1168111704 ^- (unit irequest-graph)
@@ -11696,8 +11719,13 @@
1169611719 =/ rs=(unit (list irequest-evidence))
1169711720 (request-graph-requests-add requests.cg requests.g (add 1 (lent requests.cg)))
1169811721 ?~ rs ~
11699− ?: &(?=(^ u.rs) |((gth (lent ~(tap in:..zuse merged)) 256) (gth (lent u.rs) 256))) ~
11700− $(imports t.imports, g g(paths merged, requests u.rs), fuel (dec fuel))
11722+ =/ ss=(unit (list istore-request-evidence))
11723+ (store-graph-requests-add stores.cg stores.g (add 1 (lent stores.cg)))
11724+ ?~ ss ~
11725+ =/ total=@ud (add (lent u.rs) (lent u.ss))
11726+ ?: &(?=(^ u.rs) |((gth (lent ~(tap in:..zuse merged)) 256) (gth total 256))) ~
11727+ ?: &(?=(^ u.ss) |((gth (lent ~(tap in:..zuse merged)) 256) (gth total 256))) ~
11728+ $(imports t.imports, g g(paths merged, requests u.rs, stores u.ss), fuel (dec fuel))
1170111729++ request-graph-reusable
1170211730 |= [f=ifile src=@t externals=iexternals marks=imark-externals modules=jbundle active=(list path) values=(list term) molds=(list term) prelude=(unit ifile)]
1170311731 ^- ?
@@ -12155,6 +12183,28 @@
1215512183:: Value watchability remains unproved even for a watchable declaration.
1215612184+$ ione-request-interface
1215712185 [support=iapi-support-evidence parts=iapi-request-parts iface=ifile]
12186+++ store-compatible-poke
12187+ |= prelude=iprelude
12188+ ^- (unit ischeme)
12189+ =/ public=ifile iface.prelude
12190+ ?. =(at.public /lib/jibb/prelude/jibb) ~
12191+ =/ poke=(unit ischeme) (find-jibb-mold %poke public)
12192+ ?~ poke ~
12193+ ?. ?=(%union -.typ.u.poke) ~
12194+ ?^ vars.u.poke ~
12195+ ?. =(origin.typ.u.poke `[/lib/jibb/internal/jibb %poke]) ~
12196+ ?: (itype-has-tag typ.u.poke) ~
12197+ =/ private=(list iwidth-dependency)
12198+ (skim dependencies.public |=(d=iwidth-dependency =(at.d /lib/jibb/internal/jibb)))
12199+ ?. ?=([* ~] private) ~
12200+ ?~ source.i.private ~
12201+ =/ agent-case=itype
12202+ [%cell [%const [%term %tas %agent '%agent']] [%cell [%face %agent [%atom %tas]] [%cell [%face %mark [%atom %tas]] [%face %payload [%noun ~]]]]]
12203+ =/ store-case=itype
12204+ [%cell [%const [%term %tas %store '%store']] [%cell [%face %module [%atom %t]] [%cell [%face %action [%atom %tas]] [%face %payload [%noun ~]]]]]
12205+ ?. =(cases.typ.u.poke ~[agent-case store-case]) ~
12206+ poke
12207+::
1215812208++ request-compatible-ask
1215912209 |= prelude=iprelude
1216012210 ^- (unit ischeme)
@@ -12251,7 +12301,7 @@
1225112301 ?~ source.i.private [%| 'request internal source needs unsupported inference']
1225212302 =/ req=irequest-evidence
1225312303 [file name.path.p p src u.source.public u.source.i.private values.prelude molds.prelude externals marks]
12254− =/ interface=ifile [~[[name.path.p scheme]] exports file ~ ~ ~ `src `[(silt `(list path)`~[file]) ~[req] modules `public values.prelude molds.prelude externals marks]]
12304+ =/ interface=ifile [~[[name.path.p scheme]] exports file ~ ~ ~ `src `[(silt `(list path)`~[file]) ~[req] ~ modules `public values.prelude molds.prelude externals marks]]
1225512305 [%& [support u.parts interface]]
1225612306:: Graph-aware request artifact; resolver use remains type-only.
1225712307++ one-request-interface-graph
@@ -12305,7 +12355,7 @@
1230512355 ?~ source.i.private [%| 'request internal source needs unsupported inference']
1230612356 =/ req=irequest-evidence
1230712357 [file name.path.p p src u.source.public u.source.i.private values.prelude molds.prelude externals marks]
12308− =/ interface=ifile [~[[name.path.p scheme]] exports file ~ ~ ~ `src `[(silt `(list path)`~[file]) ~[req] modules `public values.prelude molds.prelude externals marks]]
12358+ =/ interface=ifile [~[[name.path.p scheme]] exports file ~ ~ ~ `src `[(silt `(list path)`~[file]) ~[req] ~ modules `public values.prelude molds.prelude externals marks]]
1230912359 [%& [support u.parts interface]]
1231012360::
1231112361++ api-mark-exports
@@ -12474,7 +12524,7 @@
1247412524 [%| 'API exported molds need unsupported inference']
1247512525 =/ env=ienv (weld values.u.gates (weld values.u.poke values.support))
1247612526 =/ graph=irequest-graph
12477− [(silt `(list path)`~[file]) requests.u.gates modules `public values.prep molds.prep externals marks]
12527+ [(silt `(list path)`~[file]) requests.u.gates ~ modules `public values.prep molds.prep externals marks]
1247812528 =/ iface=ifile
1247912529 [env exports file derived.u.poke elaborations.support ~ `src `graph]
1248012530 [%& [iface dependencies.ev]]
@@ -12554,6 +12604,61 @@
1255412604 ?~ view ~
1255512605 `[u.load u.view]
1255612606::
12607+:: A store main is only the direct two-wing source call. The poke declaration
12608+:: is checked here, then removed before every ordinary mold/value inference pass.
12609+++ store-main-parts
12610+ |= d=def
12611+ ^- (unit [init=term update=term])
12612+ ?. ?=(%value -.d) ~
12613+ |-
12614+ ?: ?=(%group -.val.d) $(val.d inner.val.d)
12615+ ?. ?=(%call -.val.d) ~
12616+ =/ head=(unit term) (program-main-wing head.val.d)
12617+ ?~ head ~
12618+ ?. =(%store u.head) ~
12619+ ?. ?=([* * ~] args.val.d) ~
12620+ =/ args=(list expr) args.val.d
12621+ ?> ?=([* * ~] args)
12622+ =/ init=(unit term) (program-main-wing i.args)
12623+ =/ update=(unit term) (program-main-wing i.t.args)
12624+ ?~ init ~
12625+ ?~ update ~
12626+ `[u.init u.update]
12627+::
12628++$ istore-declaration [action=term defs=(list def)]
12629+++ store-declaration
12630+ |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
12631+ ^- (unit istore-declaration)
12632+ =/ ds=(list def) defs.mod
12633+ =/ pokes=(list def)
12634+ (skim ds |=(d=def &(?=(%mold -.d) =(%poke name.d))))
12635+ ?. ?=([* ~] pokes) ~
12636+ =/ states=(list def)
12637+ (skim ds |=(d=def &(?=(%mold -.d) =(%state name.d))))
12638+ ?. ?=([* ~] states) ~
12639+ =/ poke=def i.pokes
12640+ =/ state=def i.states
12641+ ?> &(?=(%mold -.poke) ?=(%mold -.state))
12642+ ?: ?=(%generic -.shape.state) ~
12643+ ?. ?=(%ref -.shape.poke) ~
12644+ ?. ?=([@ ~] names.shape.poke) ~
12645+ =/ action=term i.names.shape.poke
12646+ =/ actions=(list def)
12647+ (skim ds |=(d=def &(?=(%mold -.d) =(action name.d))))
12648+ ?. ?=([* ~] actions) ~
12649+ =/ action-def=def i.actions
12650+ ?> ?=(%mold -.action-def)
12651+ ?: ?=(%generic -.shape.action-def) ~
12652+ =/ ordinary=(list def)
12653+ (skim ds |=(d=def !&(?=(%mold -.d) =(%poke name.d))))
12654+ ?. (module-scope-valid mod(defs ordinary) prelude-values prelude-molds) ~
12655+ =/ derived=(list term) ~[%state action]
12656+ ?: (lien derived |=(n=term =(n %proj))) ~
12657+ =/ outer=(list term)
12658+ (weld prelude-values (weld (global-value-names ordinary) (api-import-faces imports.mod)))
12659+ ?. (levy derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x)))))) ~
12660+ `[action ordinary]
12661+::
1255712662++ program-empty-null
1255812663 |= e=expr
1255912664 ^- ?
@@ -13155,6 +13260,86 @@
1315513260 (program-single-case-fit i.args.actual-el i.args.expected-el sub.expected-check next.expected-check)
1315613261 case-fit
1315713262::
13263+:: A direct view without a keyed each/turn site still needs the message type
13264+:: from the checked update. Recover only that closed component; final main
13265+:: checking remains the canonical program-kind boundary.
13266+++ program-plain-view-context
13267+ |= [parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
13268+ ^- (unit iresolved)
13269+ =/ env=ienv env.resolution
13270+ ?^ (ienv-lookup %main env) ~
13271+ ?^ (ienv-lookup view.parts env) ~
13272+ =/ relation=(unit [message=itype model=itype])
13273+ (program-update-relation update.parts ds env)
13274+ ?~ relation ~
13275+ =/ views=(list def)
13276+ (skim ds |=(d=def &(?=(%value -.d) =(view.parts name.d))))
13277+ ?. ?=([* ~] views) ~
13278+ =/ view-def=def i.views
13279+ ?> ?=(%value -.view-def)
13280+ =/ written-view=(unit sample) (direct-gate-sample view-def)
13281+ ?~ written-view ~
13282+ =/ body=expr
13283+ ?- -.val.view-def
13284+ %gate body.val.view-def
13285+ %gate-wide body.val.view-def
13286+ * !!
13287+ ==
13288+ =/ sites=(unit (list iview-site)) (program-view-sites body ~)
13289+ ?~ sites ~
13290+ ?^ u.sites ~
13291+ ?~ prelude.initial ~
13292+ ?~ (ienv-lookup %program values.u.prelude.initial) ~
13293+ =/ element=(unit ischeme) (find-jibb-mold %element u.prelude.initial)
13294+ ?~ element ~
13295+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
13296+ ?~ heads ~
13297+ ?~ (~(get by gates.u.heads) %program) ~
13298+ =/ checked=(map term def) (direct-checked-gates ds env)
13299+ =/ templates=ienv
13300+ (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
13301+ =/ scanned=(unit dgscan)
13302+ (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
13303+ ?~ scanned ~
13304+ =. next.initial (dg-next-id ids.u.scanned 0)
13305+ =/ view-state=istate (reserve-def-caps val.view-def initial)
13306+ =/ sam=isample-result (infer-sample u.written-view env view-state)
13307+ ?: ?=(%| -.sam) ~
13308+ =/ actual-model=itype (program-inferred-sample typ.p.sam u.written-view)
13309+ ?. ?=(~ (itype-vars actual-model)) ~
13310+ ?: (itype-has-tag actual-model) ~
13311+ =/ model-fit=ifit
13312+ (direct-invariant actual-model model.u.relation sub.state.p.sam next.state.p.sam)
13313+ ?. ?=(%ok -.model-fit) ~
13314+ =/ product=(unit itype) (template-apply u.element ~[message.u.relation])
13315+ ?~ product ~
13316+ =/ st=istate
13317+ state.p.sam(sub sub.model-fit, next next.model-fit, gate-defs checked, head-evidence heads)
13318+ =/ inferred=iresult
13319+ (infer-call-context-arg body u.product env.p.sam st (span-of body))
13320+ ?: ?=(%| -.inferred) ~
13321+ =/ product-fit=ifit
13322+ (itype-fit typ.p.inferred u.product sub.state.p.inferred next.state.p.inferred)
13323+ ?. ?=(%ok -.product-fit) ~
13324+ =/ merged-product=itype
13325+ (itype-merge-faces typ.p.inferred u.product sub.product-fit)
13326+ =/ actual-cast=itype [%fn typ.p.sam merged-product]
13327+ =/ closed=itype [%fn typ.p.sam u.product]
13328+ =/ cast=ifit
13329+ (itype-fit actual-cast closed sub.product-fit next.product-fit)
13330+ ?. ?=(%ok -.cast) ~
13331+ =/ merged=itype (itype-merge-faces actual-cast closed sub.cast)
13332+ =/ adjusted=iresult
13333+ [%& merged state.p.inferred(sub sub.cast, next next.cast)]
13334+ =/ added=(unit iadded-definition)
13335+ (add-supported-result view-def adjusted view-state env checked artifacts.resolution)
13336+ ?~ added ~
13337+ =/ recovered=(unit ischeme) (ienv-lookup view.parts env.u.added)
13338+ ?~ recovered ~
13339+ ?. ?=(~ vars.u.recovered) ~
13340+ ?. ?=(~ (itype-vars typ.u.recovered)) ~
13341+ `[env.u.added grouped.resolution artifacts.u.added]
13342+::
1315813343:: Recover exactly one direct keyed each/turn row mapper, then its view.
1315913344:: The prelude's own each and turn schemes determine the mapper gate: the
1316013345:: key is inferred from the mapper body, never selected by this recovery.
@@ -13377,6 +13562,88 @@
1337713562 ?. ?=(~ (itype-vars typ.u.recovered)) ~
1337813563 `[env.u.added grouped.resolution artifacts.u.added]
1337913564::
13565+++ program-init-null-sample
13566+ |= d=def
13567+ ^- ?
13568+ =/ written=(unit sample) (direct-gate-sample d)
13569+ ?~ written |
13570+ ?. ?=(%bare -.u.written) |
13571+ =/ sh=shape shape.u.written
13572+ ?. ?=(%const -.sh) |
13573+ =(%null form.lit.sh)
13574+::
13575+:: The tuple-ending-null initializer retry above intentionally keeps its own
13576+:: boundary. A direct null-sample initializer can instead receive the closed
13577+:: model already established by update, view and subscriptions.
13578+++ program-plain-init-context
13579+ |= [parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
13580+ ^- (unit iresolved)
13581+ =/ env=ienv env.resolution
13582+ ?^ (ienv-lookup %main env) ~
13583+ ?^ (ienv-lookup init.parts env) ~
13584+ ?~ (ienv-lookup update.parts env) ~
13585+ ?~ (ienv-lookup view.parts env) ~
13586+ ?~ (ienv-lookup subs.parts env) ~
13587+ =/ relation=(unit [message=itype model=itype])
13588+ (program-update-relation update.parts ds env)
13589+ ?~ relation ~
13590+ =/ inits=(list def)
13591+ (skim ds |=(d=def &(?=(%value -.d) =(init.parts name.d))))
13592+ ?. ?=([* ~] inits) ~
13593+ =/ init-def=def i.inits
13594+ ?> ?=(%value -.init-def)
13595+ ?. (program-init-null-sample init-def) ~
13596+ =/ written=(unit sample) (direct-gate-sample init-def)
13597+ ?~ written ~
13598+ =/ body=expr
13599+ ?- -.val.init-def
13600+ %gate body.val.init-def
13601+ %gate-wide body.val.init-def
13602+ * !!
13603+ ==
13604+ ?~ prelude.initial ~
13605+ ?~ (ienv-lookup %program values.u.prelude.initial) ~
13606+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
13607+ ?~ heads ~
13608+ ?~ (~(get by gates.u.heads) %program) ~
13609+ =/ checked=(map term def) (direct-checked-gates ds env)
13610+ =/ templates=ienv
13611+ (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
13612+ =/ scanned=(unit dgscan)
13613+ (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
13614+ ?~ scanned ~
13615+ =. next.initial (dg-next-id ids.u.scanned 0)
13616+ =/ init-state=istate (reserve-def-caps val.init-def initial)
13617+ =/ sam=isample-result (infer-sample u.written env init-state)
13618+ ?: ?=(%| -.sam) ~
13619+ ?. ?=(~ (itype-vars typ.p.sam)) ~
13620+ ?: (itype-has-tag typ.p.sam) ~
13621+ =/ st=istate state.p.sam(gate-defs checked, head-evidence heads)
13622+ =/ inferred=iresult
13623+ (infer-call-context-arg body model.u.relation env.p.sam st (span-of body))
13624+ ?: ?=(%| -.inferred) ~
13625+ =/ product-fit=ifit
13626+ (itype-fit typ.p.inferred model.u.relation sub.state.p.inferred next.state.p.inferred)
13627+ ?. ?=(%ok -.product-fit) ~
13628+ =/ merged-product=itype
13629+ (itype-merge-faces typ.p.inferred model.u.relation sub.product-fit)
13630+ =/ actual-cast=itype [%fn typ.p.sam merged-product]
13631+ =/ closed=itype [%fn typ.p.sam model.u.relation]
13632+ =/ cast=ifit
13633+ (itype-fit actual-cast closed sub.product-fit next.product-fit)
13634+ ?. ?=(%ok -.cast) ~
13635+ =/ merged=itype (itype-merge-faces actual-cast closed sub.cast)
13636+ =/ adjusted=iresult
13637+ [%& merged state.p.inferred(sub sub.cast, next next.cast)]
13638+ =/ added=(unit iadded-definition)
13639+ (add-supported-result init-def adjusted init-state env checked artifacts.resolution)
13640+ ?~ added ~
13641+ =/ recovered=(unit ischeme) (ienv-lookup init.parts env.u.added)
13642+ ?~ recovered ~
13643+ ?. ?=(~ vars.u.recovered) ~
13644+ ?. ?=(~ (itype-vars typ.u.recovered)) ~
13645+ `[env.u.added grouped.resolution artifacts.u.added]
13646+::
1338013647:: Recover only the initializer of an already recognized direct program main.
1338113648:: The derived call is evidence for an ordinary init/main retry, never an
1338213649:: interface to publish on its own. Any failure returns the original resolution.
@@ -13484,6 +13751,23 @@
1348413751 ?. ?=(~ (itype-vars typ.u.recovered)) ~
1348513752 `[env.u.added grouped.resolution artifacts.u.added]
1348613753::
13754+++ store-derived-schemes
13755+ |= [prelude=ifile values=(list term) molds=(list term) state=itype action=itype]
13756+ ^- (unit [state=ischeme action=ischeme])
13757+ =/ prep=iprelude [prelude values molds]
13758+ =/ ask=(unit ischeme) (request-compatible-ask prep)
13759+ ?~ ask ~
13760+ =/ poke=(unit ischeme) (store-compatible-poke prep)
13761+ ?~ poke ~
13762+ ?^ (itype-vars state) ~
13763+ ?^ (itype-vars action) ~
13764+ ?: |((itype-has-tag state) (itype-has-tag action)) ~
13765+ =/ result=(unit itype) (template-apply u.ask ~[[%var 0]])
13766+ ?~ result ~
13767+ =/ request=ischeme [[%fn [%fn state [%var 0]] u.result] ~[0]]
13768+ =/ constructor=ischeme [[%fn action typ.u.poke] ~]
13769+ `[request constructor]
13770+::
1348713771++ program-subs-watch
1348813772 |= [d=def imports=ijimports graph=irequest-graph prelude=ifile]
1348913773 ^- ?
@@ -13518,7 +13802,9 @@
1351813802 =/ callback=expr (program-transparent i.args.request)
1351913803 ?. ?=(%ctor -.callback) |
1352013804 ?. ?=(%term form.tag.callback) |
13521− ?=(^ (derived-request-member case face imports graph prelude))
13805+ ?| ?=(^ (derived-request-member case face imports graph prelude))
13806+ ?=(^ (derived-store-request-member case face imports graph prelude))
13807+ ==
1352213808::
1352313809:: Exact derived-member and request-evidence identity, shared by direct
1352413810:: program watches and direct data-page loads. Only a plain request in the
@@ -13558,6 +13844,35 @@
1355813844 ?. =(product.typ.u.member u.result) ~
1355913845 member
1356013846::
13847+:: Store state is watchable by definition, but only the actual derived member
13848+:: of the uniquely selected source-bound store interface proves that fact.
13849+++ derived-store-request-member
13850+ |= [case=term face=term imports=ijimports graph=irequest-graph prelude=ifile]
13851+ ^- (unit ischeme)
13852+ ?. =(%state case) ~
13853+ =/ selected=(list [face=term interface=ifile])
13854+ (skim imports |=(j=[face=term interface=ifile] =(face face.j)))
13855+ ?. ?=([* ~] selected) ~
13856+ =/ iface=ifile interface.i.selected
13857+ =/ member=(unit ischeme) (ienv-lookup %state values.iface)
13858+ ?~ member ~
13859+ ?~ source.iface ~
13860+ =/ evidence=(list istore-request-evidence)
13861+ (skim stores.graph |=(r=istore-request-evidence =(store-at.r at.iface)))
13862+ ?. ?=([* ~] evidence) ~
13863+ =/ request=istore-request-evidence i.evidence
13864+ ?. =(u.source.iface source.request) ~
13865+ ?~ graph.iface ~
13866+ ?. (lien stores.u.graph.iface |=(r=istore-request-evidence =(r request))) ~
13867+ =/ derived=(unit [state=ischeme action=ischeme])
13868+ (store-derived-schemes prelude prelude-values.graph prelude-molds.graph state.request action.request)
13869+ ?~ derived ~
13870+ ?. =(u.member state.u.derived) ~
13871+ =/ constructor=(unit ischeme) (ienv-lookup action-name.request values.iface)
13872+ ?~ constructor ~
13873+ ?. =(u.constructor action.u.derived) ~
13874+ member
13875+::
1356113876++ program-main-context
1356213877 |= [main=def ds=(list def) resolution=iresolved initial=istate]
1356313878 ^- iresolved
@@ -13670,6 +13985,72 @@
1367013985 ?. ?=([* ~] subs) |
1367113986 |((program-subs-empty i.subs) (program-subs-watch i.subs imports graph u.prelude))
1367213987::
13988+:: The two outer sample faces are binder names, not part of the action/state
13989+:: relation. Leave every face inside either component untouched.
13990+++ store-update-unfaced
13991+ |= typ=itype
13992+ ^- itype
13993+ ?. ?=(%fn -.typ) typ
13994+ ?. ?=(%cell -.sample.typ) typ
13995+ =/ head=itype hed.sample.typ
13996+ =/ tail=itype tal.sample.typ
13997+ =? head ?=(%face -.head) body.head
13998+ =? tail ?=(%face -.tail) body.tail
13999+ typ(sample [%cell head tail])
14000+::
14001+:: The builder erases the action from main. Recover it only from the direct
14002+:: local poke declaration and check both ordinary components invariantly.
14003+++ store-main-closed
14004+ |= [parts=[init=term update=term] action=term env=ienv molds=imold-types prelude=(unit ifile)]
14005+ ^- (unit ischeme)
14006+ ?~ prelude ~
14007+ =/ builder=(unit ischeme) (ienv-lookup %store values.u.prelude)
14008+ ?~ builder ~
14009+ ?. ?=([@ @ ~] vars.u.builder) ~
14010+ =/ state-var=@ud i.vars.u.builder
14011+ =/ action-var=@ud i.t.vars.u.builder
14012+ ?: =(state-var action-var) ~
14013+ =/ builder-sample=itype
14014+ [%cell [%face %init [%var state-var]] [%face %update [%fn [%cell [%var action-var] [%var state-var]] [%var state-var]]]]
14015+ =/ builder-product=itype [%cell [%face %init [%var state-var]] [%face %update [%noun ~]]]
14016+ ?. =(typ.u.builder [%fn builder-sample builder-product]) ~
14017+ =/ store=(unit ischeme) (find-jibb-mold %store u.prelude)
14018+ ?~ store ~
14019+ ?. ?=([@ ~] vars.u.store) ~
14020+ ?. =(typ.u.store [%cell [%face %init [%var i.vars.u.store]] [%face %update [%noun ~]]]) ~
14021+ =/ state=(unit ischeme) (find-jibb-mold %state [~ molds /tmp ~ ~ ~ ~ ~])
14022+ ?~ state ~
14023+ =/ action-mold=(unit ischeme) (find-jibb-mold action [~ molds /tmp ~ ~ ~ ~ ~])
14024+ ?~ action-mold ~
14025+ ?. &(?=(~ vars.u.state) ?=(~ (itype-vars typ.u.state))) ~
14026+ ?. &(?=(~ vars.u.action-mold) ?=(~ (itype-vars typ.u.action-mold))) ~
14027+ =/ canonical=(unit itype) (template-apply u.store ~[typ.u.state])
14028+ ?~ canonical ~
14029+ =/ main=(unit ischeme) (ienv-lookup %main env)
14030+ =/ main-fit=(unit ifit)
14031+ ?~(main ~ `(direct-invariant typ.u.main u.canonical ~ 0))
14032+ =/ main-ok=?
14033+ ?~ main &
14034+ ?. ?=(~ vars.u.main) |
14035+ ?. ?=(~ (itype-vars typ.u.main)) |
14036+ ?~ main-fit |
14037+ ?=(%ok -.u.main-fit)
14038+ ?. main-ok ~
14039+ =/ init=(unit ischeme) (ienv-lookup init.parts env)
14040+ ?~ init ~
14041+ ?. ?=(~ vars.u.init) ~
14042+ ?. ?=(~ (itype-vars typ.u.init)) ~
14043+ =/ init-fit=ifit (direct-invariant typ.u.init typ.u.state ~ 0)
14044+ ?. ?=(%ok -.init-fit) ~
14045+ =/ update=(unit ischeme) (ienv-lookup update.parts env)
14046+ ?~ update ~
14047+ ?. ?=(~ vars.u.update) ~
14048+ ?. ?=(~ (itype-vars typ.u.update)) ~
14049+ =/ expected=itype [%fn [%cell typ.u.action-mold typ.u.state] typ.u.state]
14050+ =/ update-fit=ifit (direct-invariant (store-update-unfaced typ.u.update) expected ~ 0)
14051+ ?. ?=(%ok -.update-fit) ~
14052+ `[u.canonical ~]
14053+::
1367314054++ infer-jibb-file
1367414055 |= [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)]
1367514056 ^- jfile-result
@@ -13691,7 +14072,7 @@
1369114072 ?: ?=([%ui %api *] at)
1369214073 =/ iface=(unit ifile) (api-poke-interface at mod mark-externals prelude-values prelude-molds prelude)
1369314074 ?^ iface
13694− =/ checked=ifile u.iface(source `src, graph `[(silt `(list path)`~[at]) ~ modules prelude prelude-values prelude-molds externals mark-externals])
14075+ =/ checked=ifile u.iface(source `src, graph `[(silt `(list path)`~[at]) ~ ~ modules prelude prelude-values prelude-molds externals mark-externals])
1369514076 [%& [checked [[at checked] cache]]]
1369614077 ?~ prelude [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
1369714078 =/ prepared=iprelude [u.prelude prelude-values prelude-molds]
@@ -13710,23 +14091,31 @@
1371014091 (multi-request-interface-graph at src externals mark-externals modules active cache `prepared)
1371114092 ?: ?=(%| -.multi) [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
1371214093 [%& [iface.p.multi [[at iface.p.multi] cache.p.multi]]]
13713− ?. (module-scope-valid mod prelude-values prelude-molds)
13714− ?: (pending-declared-poke at mod prelude-values prelude-molds)
13715− [%| [(crip "module kind or scope needs unsupported inference: {(spud at)}") ~]]
13716− [%| [(crip "module has conflicting names: {(spud at)}") ~]]
13717− =/ vals=(list term) (global-value-names defs.mod)
1371814094 =/ main=(unit def) (program-main-def defs.mod)
1371914095 =/ main-parts=(unit [init=term update=term view=term subs=term])
1372014096 ?~(main ~ (program-main-parts u.main))
1372114097 =/ page-parts=(unit [load=term view=term])
1372214098 ?~(main ~ (page-main-parts u.main))
13723− ?: &(?=([%ui %stores *] at) ?=(^ main))
14099+ =/ store-parts=(unit [init=term update=term])
14100+ ?~(main ~ (store-main-parts u.main))
14101+ =/ declared=(unit istore-declaration)
14102+ ?~(store-parts ~ (store-declaration mod prelude-values prelude-molds))
14103+ ?: &(?=(^ store-parts) ?=(~ declared))
14104+ [%| [(crip "module kind or scope needs unsupported inference: {(spud at)}") ~]]
14105+ ?: &(?=([%ui %stores *] at) ?=(^ main) ?=(~ store-parts))
1372414106 [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]
14107+ =/ ds=(list def) ?~(declared defs.mod defs.u.declared)
14108+ =/ checking=module mod(defs ds)
14109+ ?. (module-scope-valid checking prelude-values prelude-molds)
14110+ ?: (pending-declared-poke at mod prelude-values prelude-molds)
14111+ [%| [(crip "module kind or scope needs unsupported inference: {(spud at)}") ~]]
14112+ [%| [(crip "module has conflicting names: {(spud at)}") ~]]
14113+ =/ vals=(list term) (global-value-names ds)
1372514114 =/ js=jimports-detailed-result (resolve-jibb-imports-detailed imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
1372614115 ?: ?=(%| -.js) [%| p.js]
1372714116 =/ collected=grec-collected
13728− ?^ imports.mod [(collect-simple-molds defs.mod) *(map term shape)]
13729− (grec-collect-molds defs.mod)
14117+ ?^ imports.mod [(collect-simple-molds ds) *(map term shape)]
14118+ (grec-collect-molds ds)
1373014119 =/ molds=imolds molds.collected
1373114120 =/ globals=(list term) (weld prelude-values (weld (import-binding-names imports.mod) vals))
1373214121 =/ surs=(list term) (collect-sur-imports imports.mod)
@@ -13757,56 +14146,93 @@
1375714146 [%| [msg `[at src name.witness cases.witness]]]
1375814147 =/ resolution=iresolved
1375914148 ?~ index
13760− (resolve-groups defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
13761− (resolve-groups-core defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude index)
14149+ (resolve-groups ds molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
14150+ (resolve-groups-core ds molds globals externals surs mark-externals marks resolved.p.js reserved at prelude index)
1376214151 =/ env=ienv env.resolution
1376314152 =/ recovered=iresolved
1376414153 ?~ main resolution
1376514154 ?~ main-parts resolution
1376614155 =/ updated=(unit iresolved)
13767− (program-update-context u.main u.main-parts defs.mod resolution state)
14156+ (program-update-context u.main u.main-parts ds resolution state)
1376814157 =/ with-update=iresolved ?~(updated resolution u.updated)
1376914158 =/ subscribed=(unit iresolved)
13770− (program-subs-context u.main-parts defs.mod with-update state)
14159+ (program-subs-context u.main-parts ds with-update state)
1377114160 =/ with-subs=iresolved ?~(subscribed with-update u.subscribed)
1377214161 =/ viewed=(unit iresolved)
13773− (program-view-context u.main-parts defs.mod with-subs state)
13774− =/ with-view=iresolved ?~(viewed with-subs u.viewed)
14162+ (program-view-context u.main-parts ds with-subs state)
14163+ =/ with-keyed-view=iresolved ?~(viewed with-subs u.viewed)
14164+ =/ plain-view=(unit iresolved)
14165+ ?^(viewed ~ (program-plain-view-context u.main-parts ds with-keyed-view state))
14166+ =/ with-view=iresolved ?~(plain-view with-keyed-view u.plain-view)
1377514167 =/ initialized=(unit iresolved)
13776− (program-init-context u.main u.main-parts defs.mod with-view state)
13777− =/ components=iresolved ?~(initialized with-view u.initialized)
13778− (program-main-context u.main defs.mod components state)
14168+ (program-init-context u.main u.main-parts ds with-view state)
14169+ =/ with-initialized=iresolved ?~(initialized with-view u.initialized)
14170+ =/ plain-init=(unit iresolved)
14171+ ?^(initialized ~ (program-plain-init-context u.main-parts ds with-initialized state))
14172+ =/ components=iresolved ?~(plain-init with-initialized u.plain-init)
14173+ (program-main-context u.main ds components state)
1377914174 =. env env.recovered
1378014175 =. artifacts.resolution artifacts.recovered
1378114176 =. env
13782− ?: (module-values-complete defs.mod env) env
14177+ ?: (module-values-complete ds env) env
1378314178 ?: |(?=([%ui %stores *] at) ?=(^ imports.mod) ?=(^ prelude) ?=(^ prelude-values) ?=(^ prelude-molds)) env
1378414179 ?: (gth (met 3 src) 65.536) env
13785− ?: (gth (lent defs.mod) 64) env
13786− ?. (dg-source-candidate defs.mod 64) env
14180+ ?: (gth (lent ds) 64) env
14181+ ?. (dg-source-candidate ds 64) env
1378714182 =/ transaction=(unit dgcommit) (dg-root-source at src)
1378814183 ?~ transaction env
1378914184 ?: (dg-interface-safe env.u.transaction) env.u.transaction
1379014185 env
13791− ?. (module-values-complete defs.mod env)
14186+ =/ required=(list def)
14187+ ?~ store-parts ds
14188+ (skim ds |=(d=def !&(?=(%value -.d) =(%main name.d))))
14189+ ?. (module-values-complete required env)
1379214190 [%| [(crip "module definitions need unsupported inference: {(spud at)}") ~]]
13793− =/ initial=irequest-graph [(silt `(list path)`~[at]) ~ modules prelude prelude-values prelude-molds externals mark-externals]
14191+ =/ initial=irequest-graph [(silt `(list path)`~[at]) ~ ~ modules prelude prelude-values prelude-molds externals mark-externals]
1379414192 =/ graph=(unit irequest-graph) (request-graph-merge resolved.p.js initial (add 1 (lent resolved.p.js)))
1379514193 ?~ graph [%| ['module request evidence needs unsupported inference' ~]]
1379614194 =/ static-main=(unit ischeme)
1379714195 ?~ main ~
1379814196 ?^ main-parts ~
1379914197 ?^ page-parts ~
14198+ ?^ store-parts ~
1380014199 (static-main-specialized env prelude)
1380114200 =? env ?=(^ static-main)
1380214201 [[%main u.static-main] (skim env |=(entry=[name=term scheme=ischeme] !=(%main name.entry)))]
14202+ =/ store-main=(unit ischeme)
14203+ ?~ store-parts ~
14204+ ?~ declared ~
14205+ (store-main-closed u.store-parts action.u.declared env p.mts prelude)
14206+ =? env ?=(^ store-main)
14207+ [[%main u.store-main] (skim env |=(entry=[name=term scheme=ischeme] !=(%main name.entry)))]
1380314208 =/ kind-ok=?
1380414209 ?~ main &
13805− ?^ main-parts (program-main-closed u.main-parts defs.mod env prelude resolved.p.js u.graph)
13806− ?^ page-parts (page-main-closed u.page-parts defs.mod env prelude resolved.p.js u.graph)
14210+ ?^ main-parts (program-main-closed u.main-parts ds env prelude resolved.p.js u.graph)
14211+ ?^ page-parts (page-main-closed u.page-parts ds env prelude resolved.p.js u.graph)
14212+ ?^ store-parts ?=(^ store-main)
1380714213 ?=(^ static-main)
1380814214 ?. kind-ok
1380914215 [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]
14216+ =/ store-derived=(unit [values=ienv evidence=istore-request-evidence])
14217+ ?~ declared ~
14218+ ?~ prelude ~
14219+ =/ state=(unit ischeme) (find-jibb-mold %state [~ p.mts at ~ ~ ~ ~ ~])
14220+ ?~ state ~
14221+ =/ action-mold=(unit ischeme) (find-jibb-mold action.u.declared [~ p.mts at ~ ~ ~ ~ ~])
14222+ ?~ action-mold ~
14223+ =/ schemes=(unit [state=ischeme action=ischeme])
14224+ (store-derived-schemes u.prelude prelude-values prelude-molds typ.u.state typ.u.action-mold)
14225+ ?~ schemes ~
14226+ =/ evidence=istore-request-evidence
14227+ [at src typ.u.state action.u.declared typ.u.action-mold]
14228+ `[~[[%state state.u.schemes] [action.u.declared action.u.schemes]] evidence]
14229+ ?: &(?=(^ declared) ?=(~ store-derived))
14230+ [%| [(crip "store derived gates need unsupported inference: {(spud at)}") ~]]
14231+ =? env ?=(^ store-derived) (weld values.u.store-derived env)
14232+ =? graph ?=(^ store-derived)
14233+ `u.graph(stores [evidence.u.store-derived stores.u.graph])
14234+ ?. (request-graph-bounded u.graph)
14235+ [%| ['module request evidence needs unsupported inference' ~]]
1381014236 =/ iface=ifile [env p.mts at ~ artifacts.resolution ~ `src graph]
1381114237 [%& [iface [[at iface] cache.p.js]]]
1381214238::