@@ -12558,6 +12558,145 @@
1255812558 ?~ items.body |
1255912559 (program-empty-null val:(rear items.body))
1256012560::
12561+:: Recover only the update of an already recognized direct program main.
12562+:: Its written sample determines the message/model relationship; the canonical
12563+:: cmd and list molds determine the result context. Every candidate is checked
12564+:: against the complete program call before an ordinary update/main retry.
12565+++ program-update-context
12566+ |= [main=def parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
12567+ ^- (unit iresolved)
12568+ =/ env=ienv env.resolution
12569+ ?^ (ienv-lookup %main env) ~
12570+ ?^ (ienv-lookup update.parts env) ~
12571+ =/ init=(unit ischeme) (ienv-lookup init.parts env)
12572+ =/ view=(unit ischeme) (ienv-lookup view.parts env)
12573+ =/ subs=(unit ischeme) (ienv-lookup subs.parts env)
12574+ ?~ init ~
12575+ ?~ view ~
12576+ ?~ subs ~
12577+ =/ updates=(list def)
12578+ (skim ds |=(d=def &(?=(%value -.d) =(update.parts name.d))))
12579+ ?. ?=([* ~] updates) ~
12580+ =/ update-def=def i.updates
12581+ ?> ?=(%value -.update-def)
12582+ =/ written-update=(unit sample) (direct-gate-sample update-def)
12583+ ?~ written-update ~
12584+ ?. ?=(%cell -.u.written-update) ~
12585+ ?. ?=([* * ~] items.u.written-update) ~
12586+ =/ args=(unit (list expr)) (program-main-args main)
12587+ ?~ args ~
12588+ ?~ prelude.initial ~
12589+ =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)
12590+ ?~ program ~
12591+ =/ command=(unit ischeme) (find-jibb-mold %cmd u.prelude.initial)
12592+ =/ list-template=(unit ischeme) (find-jibb-mold %list u.prelude.initial)
12593+ ?~ command ~
12594+ ?~ list-template ~
12595+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
12596+ ?~ heads ~
12597+ =/ written=(unit def) (~(get by gates.u.heads) %program)
12598+ ?~ written ~
12599+ =/ written-sample=(unit sample) (direct-gate-sample u.written)
12600+ ?~ written-sample ~
12601+ ?. ?=(%cell -.u.written-sample) ~
12602+ ?. ?=([* * * * ~] items.u.written-sample) ~
12603+ =/ checked=(map term def)
12604+ (~(put by (direct-checked-gates ds env)) update.parts update-def)
12605+ =/ templates=ienv
12606+ (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
12607+ =/ scanned=(unit dgscan)
12608+ (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
12609+ ?~ scanned ~
12610+ =. next.initial (dg-next-id ids.u.scanned 0)
12611+ =/ update-state=istate (reserve-def-caps val.update-def initial)
12612+ =/ sam=isample-result (infer-sample u.written-update env update-state)
12613+ ?: ?=(%| -.sam) ~
12614+ =/ actual-sample=itype (itype-normalize typ.p.sam sub.state.p.sam)
12615+ ?. ?=(%cell -.actual-sample) ~
12616+ =/ message=(unit itype)
12617+ (direct-slot-body hed.actual-sample (direct-sample-name i.items.u.written-update))
12618+ =/ model=(unit itype)
12619+ (direct-slot-body tal.actual-sample (direct-sample-name i.t.items.u.written-update))
12620+ ?~ message ~
12621+ ?~ model ~
12622+ =/ cmd=(unit itype) (template-apply u.command ~[u.message])
12623+ ?~ cmd ~
12624+ =/ cmds=(unit itype) (template-apply u.list-template ~[u.cmd])
12625+ ?~ cmds ~
12626+ =/ product=itype [%cell u.model u.cmds]
12627+ =/ instance=[typ=itype state=istate] (instantiate-scheme u.program state.p.sam)
12628+ ?. ?=(%fn -.typ.instance) ~
12629+ ?. ?=(%cell -.sample.typ.instance) ~
12630+ ?. ?=(%cell -.tal.sample.typ.instance) ~
12631+ =/ expected-update=(unit itype)
12632+ (direct-slot-body hed.tal.sample.typ.instance (direct-sample-name i.t.items.u.written-sample))
12633+ ?~ expected-update ~
12634+ ?. ?=(%fn -.u.expected-update) ~
12635+ :: Sample binders are not value faces. Strip only those two slot faces
12636+ :: for the invariant canonical-gate proof; the source-faced gate is still
12637+ :: used by the complete positional call and final ordinary result cast.
12638+ =/ canonical-candidate=itype [%fn [%cell u.message u.model] product]
12639+ =/ gate-fit=ifit
12640+ (direct-invariant canonical-candidate u.expected-update sub.state.instance next.state.instance)
12641+ ?. ?=(%ok -.gate-fit) ~
12642+ =/ st=istate state.instance(sub sub.gate-fit, next next.gate-fit)
12643+ =/ ini=[typ=itype state=istate] (instantiate-scheme u.init st)
12644+ =/ vw=[typ=itype state=istate] (instantiate-scheme u.view state.ini)
12645+ =/ sb=[typ=itype state=istate] (instantiate-scheme u.subs state.vw)
12646+ =. st state.sb(gate-defs checked, head-evidence heads)
12647+ =/ expected=itype [%fn typ.p.sam product]
12648+ =/ actual=itype [%cell typ.ini [%cell expected [%cell typ.vw typ.sb]]]
12649+ =/ fit=ifit
12650+ (direct-positional-fit u.args items.u.written-sample actual sample.typ.instance env st sub.st next.st)
12651+ ?. ?=(%ok -.fit) ~
12652+ =/ actual-final=itype (itype-normalize actual sub.fit)
12653+ =/ expected-final=itype (itype-normalize sample.typ.instance sub.fit)
12654+ ?^ (itype-vars actual-final) ~
12655+ ?^ (itype-vars expected-final) ~
12656+ ?: |((itype-has-tag actual-final) (itype-has-tag expected-final)) ~
12657+ =/ replay=ifit
12658+ (direct-positional-fit u.args items.u.written-sample actual sample.typ.instance env st sub.fit next.fit)
12659+ ?. ?=(%ok -.replay) ~
12660+ ?. &(=(sub.fit sub.replay) =(next.fit next.replay)) ~
12661+ =/ closed=itype (itype-normalize expected sub.fit)
12662+ ?. ?=(%fn -.closed) ~
12663+ :: The closed product no longer needs the canonical call substitutions.
12664+ :: Start the body at its ordinary sample state so existing branch retries
12665+ :: keep their substitution guards, but retain the shared fresh-ID high water.
12666+ =. st state.p.sam(next next.fit)
12667+ =/ body=expr
12668+ ?- -.val.update-def
12669+ %gate body.val.update-def
12670+ %gate-wide body.val.update-def
12671+ * !!
12672+ ==
12673+ =/ inferred=iresult
12674+ (infer-call-context-arg body product.closed env.p.sam st (span-of body))
12675+ ?: ?=(%| -.inferred) ~
12676+ =/ product-fit=ifit
12677+ (itype-fit typ.p.inferred product.closed sub.state.p.inferred next.state.p.inferred)
12678+ ?. ?=(%ok -.product-fit) ~
12679+ =/ merged-product=itype
12680+ (itype-merge-faces typ.p.inferred product.closed sub.product-fit)
12681+ =/ actual-cast=itype [%fn typ.p.sam merged-product]
12682+ =/ cast=ifit
12683+ (itype-fit actual-cast closed sub.product-fit next.product-fit)
12684+ ?. ?=(%ok -.cast) ~
12685+ =/ merged=itype (itype-merge-faces actual-cast closed sub.cast)
12686+ =/ adjusted=iresult
12687+ [%& merged state.p.inferred(sub sub.cast, next next.cast)]
12688+ =/ added=(unit iadded-definition)
12689+ (add-supported-result update-def adjusted update-state env checked artifacts.resolution)
12690+ ?~ added ~
12691+ =/ recovered=(unit ischeme) (ienv-lookup update.parts env.u.added)
12692+ ?~ recovered ~
12693+ ?. ?=(~ vars.u.recovered) ~
12694+ ?. ?=(~ (itype-vars typ.u.recovered)) ~
12695+ =/ completed=[env=ienv artifacts=(list iwidth-definition)]
12696+ (add-supported-defs-core ~[main] ds checked.u.added heads env.u.added molds.initial globals.initial externals.initial surs.initial mark-externals.initial marks.initial jimports.initial reserved-molds.initial at.initial prelude.initial artifacts.u.added grec-index.initial)
12697+ ?~ (ienv-lookup %main env.completed) ~
12698+ `[env.completed grouped.resolution artifacts.completed]
12699+::
1256112700:: Recover only the initializer of an already recognized direct program main.
1256212701:: The derived call is evidence for an ordinary init/main retry, never an
1256312702:: interface to publish on its own. Any failure returns the original resolution.
@@ -12853,6 +12992,9 @@
1285312992 =/ recovered=(unit iresolved)
1285412993 ?~ main ~
1285512994 ?~ main-parts ~
12995+ =/ updated=(unit iresolved)
12996+ (program-update-context u.main u.main-parts defs.mod resolution state)
12997+ ?^ updated updated
1285612998 (program-init-context u.main u.main-parts defs.mod resolution state)
1285712999 =. env ?~(recovered env env.u.recovered)
1285813000 =. artifacts.resolution