@@ -849,6 +849,90 @@
849:: %submitt [m(note="") ~]
849:: %submitt [m(note="") ~]
852+:: ===================================================================
853+:: 5. General checker core (design; not implemented yet)
854+:: ===================================================================
856+:: The existing inference and recovery paths are described in
857+:: docs/compiler.md. This section is a plan for replacing them, not a
858+:: claim that the current checker implements these rules. The Grammar and
859+:: Decisions are authoritative if this design needs adjustment.
861+:: 5.1 State and unification. Give each inference variable an identity and
862+:: a union-find entry: parent or binding, rank, level, source, rigidity,
863+:: and the atom, arithmetic-atom and gate-free obligations it carries.
864+:: Hoon's immutable maps hold the entries; operations return the updated
865+:: state. Find compresses paths in that returned state. Bind only after an
866+:: occurs check, merge obligations at roots, and lower levels throughout
867+:: the bound type to the root's level. A rigid written capital may acquire
868+:: allowed constraints but cannot be forced to a concrete type or a
869+:: different written capital. Keep origins for both sides of each fit so
870+:: a failure can show both excerpts. Recursive named molds retain their
871+:: identity; the occurs check is for inference variables, not a ban on
872+:: declared recursion.
874+:: A scheme quantifies eligible variables above the enclosing level;
875+:: instantiate with fresh variables and copy their obligations. Written
876+:: capitals respect their lexical scope, including sharing with a local
877+:: definition when the enclosing definition uses the same name. Retain
878+:: aura variables and directional aura fits, rather than turning every
879+:: fit into symmetric equality. At a faced position a capital binds the
880+:: type under the face; joining an unnamed position with a faced one keeps
881+:: the face, independently of the order of the inputs. Different explicit
882+:: faces conflict. No gate may hide inside a gate-free type, including in
883+:: a container; propagate the obligation through its arguments.
885+:: 5.2 Work queue. A constraint owns its source span, the types and
886+:: expression shape it depends on, and the information needed to report
887+:: failure. Tags and constructors, null, decimal and cell literals,
888+:: wings, changes, unface and unknown match subjects enter the same queue.
889+:: Index waiting constraints by the roots they read. Binding or merging a
890+:: root wakes its dependants; a retry either solves, fails with its sites,
891+:: or registers the roots still needed. Run to a fixed point, without
892+:: losing constraints when a root is redirected. Check patterns once the
893+:: subject is known. Contextual tags inspect case shapes and noun-equal
894+:: heads, retaining the named union and its site in diagnostics.
896+:: Variables reachable from an open tag constraint remain monomorphic
897+:: across definitions, so a later use, including main, can fix them.
898+:: Other eligible variables can generalize, with their atom and gate-free
899+:: obligations intact. At each definition boundary resolve its holes and
900+:: apply the specified decimal and cell defaults, without defaulting a
901+:: decimal whose definition is generic over its aura. A decimal fits @ud,
902+:: @u, @ and *; other concrete auras need their own literal. At module
903+:: completion retry the queue and report each still-open constraint at its
904+:: source; an unresolved tag asks for a ^-, never a guessed union.
906+:: 5.3 Definition order and kinds. Use the existing dependency graph's
907+:: strongly connected components in dependency order. Give a recursive
908+:: group of gates monomorphic placeholders, infer all members in one state,
909+:: solve what can be solved, then generalize together. Reject a cycle
910+:: involving a non-gate value, including one through a gate, and show the
911+:: cycle. Check a named definition's holes before later uses can fix them.
912+:: Infer main as an ordinary expression against ordinary prelude schemes;
913+:: only its resulting type determines library, page, island or store.
914+:: Afterwards check kind-specific invariants: recursively find the field
915+:: containing a gate in island data or a model, and inspect subscriptions
916+:: for watchability only at %watch. A page load may be any gate to ask,
917+:: including pure and typed paths. Preserve request provenance needed for
918+:: a watchability proof through ordinary calls and aliases.
920+:: 5.4 Matches and migration. A reusable usefulness matrix over noun
921+:: constructors, constants, cells and wildcards checks nested patterns;
922+:: loobeans, lists and units expand to their cases. Test an arm against
923+:: previous rows for usefulness, then test a wildcard for exhaustiveness;
924+:: keep a witness for a missing case and the covering arm's site for a
925+:: dead one. Recursive types require memoized specialization and a
926+:: terminating treatment of recursive states. The same matrix can later
927+:: drive lowering. The bare-name/tag spelling rule is checked against the
928+:: subject and the cases the rest of the pattern can match.
930+:: Migrate in small stages with eval and ship goldens for every change.
931+:: Keep diagnostics and source sites in the single full result; types.txt
932+:: is a rendering of that result. As general inference covers an existing
933+:: recovery or source-proven slice, remove that slice and retain its tests.
934+:: An unsupported construct fails closed at its own site until then.
853+| %positions
937+| %positions
@@ -11307,7 +11391,7 @@
11307 `[entry u.rest]
11391 `[entry u.rest]
11310−+$ iresolved [env=ienv grouped=(list term) artifacts=(list iwidth-definition)]
11394++$ iresolved [env=ienv grouped=(list term) artifacts=(list iwidth-definition) failures=(list [name=term diag=idiag])]
11311+$ iadj (map term (list term))
11395+$ iadj (map term (list term))
11312+$ ivisited (map term ?)
11396+$ ivisited (map term ?)
11313+$ iwork (list [name=term done=?])
11397+$ iwork (list [name=term done=?])
@@ -11403,7 +11487,7 @@
11403++ add-groups
11487++ add-groups
11404 |= [ds=(list def) components=icomponents graph=iadj env=ienv grouped=(list term) artifacts=(list iwidth-definition) state=istate]
11488 |= [ds=(list def) components=icomponents graph=iadj env=ienv grouped=(list term) artifacts=(list iwidth-definition) state=istate]
11405 ^- iresolved
11489 ^- iresolved
11406− ?~ components [env grouped artifacts]
11490+ ?~ components [env grouped artifacts ~]
11407 =/ component=(list term) i.components
11491 =/ component=(list term) i.components
11408 ?. (graph-cycle component graph) $(components t.components)
11492 ?. (graph-cycle component graph) $(components t.components)
11409 ?: (lien component |=(n=term ?=(^ (ienv-lookup n env)))) $(components t.components)
11493 ?: (lien component |=(n=term ?=(^ (ienv-lookup n env)))) $(components t.components)
@@ -11447,8 +11531,10 @@
11447 `[[[name.d (cap-names typ vars caps.state.p.result sub.state.p.result)] env] checked artifacts]
11531 `[[[name.d (cap-names typ vars caps.state.p.result sub.state.p.result)] env] checked artifacts]
11448++ add-supported-defs-core
11532++ add-supported-defs-core
11449 |= [ds=(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)])]
11533 |= [ds=(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)])]
11450− ^- [env=ienv artifacts=(list iwidth-definition)]
11534+ ^- [env=ienv artifacts=(list iwidth-definition) failures=(list [name=term diag=idiag])]
11535+ =/ failures=(list [name=term diag=idiag]) ~
11451− ?~ ds [env artifacts]
11537+ ?~ ds [env artifacts (flop failures)]
11452 =/ d=def i.ds
11538 =/ d=def i.ds
11453 ?: ?=(%mold -.d) $(ds t.ds)
11539 ?: ?=(%mold -.d) $(ds t.ds)
11454 ?. (unique-value-name name.d globals) $(ds t.ds)
11540 ?. (unique-value-name name.d globals) $(ds t.ds)
@@ -11459,37 +11545,34 @@
11459 =. gate-defs.initial checked
11545 =. gate-defs.initial checked
11460 =. head-evidence.initial heads
11546 =. head-evidence.initial heads
11461 =. initial (reserve-def-caps val.d initial)
11547 =. initial (reserve-def-caps val.d initial)
11462− =/ result=iresult (infer-fragment val.d env initial)
11548+ =/ plain=iresult (infer-fragment val.d env initial)
11549+ =/ result=iresult plain
11463 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
11550 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
11551+ ?: ?=(%| -.result)
11553+ ?: (definite-diag p.result) p.result
11554+ ?: ?=(%| -.plain) p.plain
11556+ =? failures (definite-diag failure) [[name.d failure] failures]
11464 =/ added=(unit iadded-definition)
11558 =/ added=(unit iadded-definition)
11465 (add-supported-result d result initial env checked artifacts)
11559 (add-supported-result d result initial env checked artifacts)
11466 ?~ added $(ds t.ds)
11560 ?~ added $(ds t.ds)
11467 $(ds t.ds, env env.u.added, checked checked.u.added, artifacts artifacts.u.added)
11561 $(ds t.ds, env env.u.added, checked checked.u.added, artifacts artifacts.u.added)
11469−:: Full checking discards unsupported definitions. On that failure path only,
11563+:: Retry one unresolved definition to explain a pending tag. The gate
11470−:: retry a bounded number of missing definitions to explain a pending tag
11564+:: evidence is built from the whole module, not only this definition.
11471−:: from the same ordinary inference state instead of hiding it behind the
11472−:: generic completeness error. No successful definition takes this path.
11473−++ module-pending-tag
11565+++ module-pending-tag-one
11474− |= [ds=(list def) env=ienv base=istate fuel=@ud]
11566+ |= [d=def env=ienv base=istate checked=(map term def) heads=(unit igate-prelude-evidence)]
11475 ^- (unit [at=span msg=tape])
11567 ^- (unit [at=span msg=tape])
11476− =/ checked=(map term def) (direct-checked-gates ds env)
11568+ ?. ?=(%value -.d) ~
11477− =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.base)
11482− ?: ?=(%mold -.d) $(ds t.ds, fuel (dec fuel))
11483− ?^ (ienv-lookup name.d env) $(ds t.ds, fuel (dec fuel))
11569+ ?^ (ienv-lookup name.d env) ~
11484 =/ initial=istate base(gate-defs checked, head-evidence heads)
11570 =/ initial=istate base(gate-defs checked, head-evidence heads)
11485 =. initial (reserve-def-caps val.d initial)
11571 =. initial (reserve-def-caps val.d initial)
11486 =/ result=iresult (infer-fragment val.d env initial)
11572 =/ result=iresult (infer-fragment val.d env initial)
11487 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
11573 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
11488− ?: ?=(%| -.result) $(ds t.ds, fuel (dec fuel))
11574+ ?: ?=(%| -.result) ~
11489− =/ pending=(unit [at=span msg=tape])
11490− (pending-tag-diagnostic tags.state.p.result sub.state.p.result)
11575+ (pending-tag-diagnostic tags.state.p.result sub.state.p.result)
11491− ?^ pending pending
11492− $(ds t.ds, fuel (dec fuel))
11494++ resolve-groups-core
11577++ resolve-groups-core
11495 |= [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)])]
11578 |= [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)])]
@@ -11505,12 +11588,12 @@
11505 =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)
11588 =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)
11506 =/ ordered=(list def) (dependency-order ds components)
11589 =/ ordered=(list def) (dependency-order ds components)
11508− =/ next=[env=ienv artifacts=(list iwidth-definition)]
11591+ =/ next=[env=ienv artifacts=(list iwidth-definition) failures=(list [name=term diag=idiag])]
11509 (add-supported-defs-core ordered (direct-checked-gates ds env) heads env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts index)
11592 (add-supported-defs-core ordered (direct-checked-gates ds env) heads env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts index)
11510 =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~ ~ ~]
11593 =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~ ~ ~]
11511 =. grec-index.initial index
11594 =. grec-index.initial index
11512 =/ out=iresolved (add-groups ds components graph env.next grouped artifacts.next initial)
11595 =/ out=iresolved (add-groups ds components graph env.next grouped artifacts.next initial)
11513− ?: =(env env.out) out
11596+ ?: =(env env.out) out(failures failures.next)
11514 $(env env.out, grouped grouped.out, artifacts artifacts.out)
11597 $(env env.out, grouped grouped.out, artifacts artifacts.out)
11516:: +dependency-order: the value definitions, dependencies first
11599:: +dependency-order: the value definitions, dependencies first
@@ -12540,6 +12623,80 @@
12540 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
12623 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
12541 |((lien (weld imported (weld vals mold-names)) reserved-name) (lien defs.mod reserved-def))
12624 |((lien (weld imported (weld vals mold-names)) reserved-name) (lien defs.mod reserved-def))
12626+:: A scope collision retains source sites. Prelude declarations may be in
12627+:: another source, so their name and namespace are retained separately.
12628++$ iscope-diagnostic
12629+ [issue=idiag prelude=(unit [name=term kind=?(%value %mold %any)])]
12630+++ scope-import-diagnostic
12631+ |= [imports=(list import) prelude-values=(list term) prelude-molds=(list term) seen=written-fields]
12632+ ^- (each written-fields iscope-diagnostic)
12633+ ?~ imports [%& seen]
12634+ =/ imp=import i.imports
12641+ ?: (reserved-name n)
12642+ [%| [["`{(trip n)}` is reserved and cannot be bound" ~[[at.imp "reserved name"]]] ~]]
12643+ =/ earlier=(unit span) (~(get by seen) n)
12645+ [%| [["import `{(trip n)}` shadows an earlier import" ~[[u.earlier "earlier import"] [at.imp "conflicting import"]]] ~]]
12646+ ?: |((lien prelude-values |=(x=term =(n x))) (lien prelude-molds |=(x=term =(n x))))
12647+ [%| [["import `{(trip n)}` shadows a prelude name" ~[[at.imp "conflicting import"]]] `[n %any]]]
12648+ $(imports t.imports, seen (~(put by seen) n at.imp))
12649+++ scope-def-diagnostic
12650+ |= [defs=(list def) imports=written-fields prelude-values=(list term) prelude-molds=(list term) values=written-fields molds=written-fields]
12651+ ^- (unit iscope-diagnostic)
12655+ ?: (reserved-name n)
12656+ `[["`{(trip n)}` is reserved and cannot be bound" ~[[at.d "reserved name"]]] ~]
12657+ =/ imported=(unit span) (~(get by imports) n)
12659+ `[["definition `{(trip n)}` shadows an import" ~[[u.imported "import"] [at.d "conflicting definition"]]] ~]
12660+ =/ seen=written-fields ?:(?=(%value -.d) values molds)
12661+ =/ earlier=(unit span) (~(get by seen) n)
12663+ `[["definition `{(trip n)}` shadows an earlier definition" ~[[u.earlier "earlier definition"] [at.d "conflicting definition"]]] ~]
12664+ =/ prelude-names=(list term) ?:(?=(%value -.d) prelude-values prelude-molds)
12665+ ?: (lien prelude-names |=(x=term =(n x)))
12666+ `[["definition `{(trip n)}` shadows a prelude name" ~[[at.d "conflicting definition"]]] `[n ?:(?=(%value -.d) %value %mold)]]
12668+ $(defs t.defs, values (~(put by values) n at.d))
12669+ $(defs t.defs, molds (~(put by molds) n at.d))
12670+++ module-scope-diagnostic
12671+ |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
12672+ ^- (unit iscope-diagnostic)
12673+ =/ imports=(each written-fields iscope-diagnostic)
12674+ (scope-import-diagnostic imports.mod prelude-values prelude-molds ~)
12675+ ?: ?=(%| -.imports) `p.imports
12676+ (scope-def-diagnostic defs.mod p.imports prelude-values prelude-molds ~ ~)
12677+++ show-scope-diagnostic
12678+ |= [file=path src=@t diagnostic=iscope-diagnostic prelude=(unit ifile)]
12680+ =/ excerpts=(list @t)
12681+ %+ turn sites.issue.diagnostic
12682+ |= site=[at=span note=tape]
12683+ (show-error src [file line.beg.at.site col.beg.at.site note.site])
12684+ =/ previous=(list @t)
12685+ ?~ prelude.diagnostic ~
12687+ ?~ source.u.prelude ~
12688+ =/ parsed (parse at.u.prelude u.source.u.prelude)
12689+ ?: ?=(%| -.parsed) ~
12690+ =/ matching=(list def)
12691+ %+ skim defs.p.parsed
12693+ ?& =(name.d name.u.prelude.diagnostic)
12694+ |(=(%any kind.u.prelude.diagnostic) =(-.d kind.u.prelude.diagnostic))
12697+ ~[(show-error u.source.u.prelude [at.u.prelude line.beg.at.i.matching col.beg.at.i.matching "prelude declaration"])]
12698+ (of-wain:format [(crip msg.issue.diagnostic) (weld excerpts previous)])
12543++ module-scope-valid
12700++ module-scope-valid
12544 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
12701 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
@@ -12970,6 +13127,31 @@
12970 ?. (lien values |=(n=term =(n u.name))) $(ds t.ds)
13127 ?. (lien values |=(n=term =(n u.name))) $(ds t.ds)
12971 `[u.name at.s]
13128 `[u.name at.s]
13130+:: Select the first available reason in dependency order, rather than
13131+:: preferring one class of diagnostic across the whole module. Only the
13132+:: first 64 definitions are retried for pending tags, as before.
13133+++ module-unresolved-diagnostic
13134+ |= [ds=(list def) env=ienv base=istate checked=(map term def) heads=(unit igate-prelude-evidence) failures=(list [name=term diag=idiag]) values=(list term) file=path src=@t fuel=@ud]
13138+ =/ remaining=@ud ?:(=(0 fuel) 0 (dec fuel))
13139+ ?: ?=(%mold -.d) $(ds t.ds, fuel remaining)
13140+ ?^ (ienv-lookup name.d env) $(ds t.ds, fuel remaining)
13141+ =/ found=(list [name=term diag=idiag])
13142+ (skim failures |=(failure=[name=term diag=idiag] =(name.failure name.d)))
13143+ ?^ found `(show-inference-diagnostic file src name.d diag.i.found)
13144+ =/ pending=(unit [at=span msg=tape])
13146+ (module-pending-tag-one d env base checked heads)
13148+ `(show-error src [file line.beg.at.u.pending col.beg.at.u.pending msg.u.pending])
13149+ =/ shadow=(unit [name=term at=span]) (module-sample-shadow ~[d] env values)
13151+ =/ msg=tape "sample `{(trip name.u.shadow)}` shadows a name already in scope"
13152+ `(show-error src [file line.beg.at.u.shadow col.beg.at.u.shadow msg])
13153+ $(ds t.ds, fuel remaining)
12973:: Cache only completed interfaces for this invocation. The source bundle,
13155:: Cache only completed interfaces for this invocation. The source bundle,
12974:: imported Hoon types and prelude are fixed for the whole graph. Check the
13156:: imported Hoon types and prelude are fixed for the whole graph. Check the
12975:: active path and duplicate sources before consulting it, so a cache hit
13157:: active path and duplicate sources before consulting it, so a cache hit
@@ -14230,7 +14412,7 @@
14230 ?~ recovered ~
14412 ?~ recovered ~
14231 ?. ?=(~ vars.u.recovered) ~
14413 ?. ?=(~ vars.u.recovered) ~
14232 ?. ?=(~ (itype-vars typ.u.recovered)) ~
14414 ?. ?=(~ (itype-vars typ.u.recovered)) ~
14233− `[env.u.added grouped.resolution artifacts.u.added]
14415+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]
14235++ program-inferred-slot
14417++ program-inferred-slot
14236 |= [typ=itype name=(unit term)]
14418 |= [typ=itype name=(unit term)]
@@ -14386,7 +14568,7 @@
14386 ?~ recovered ~
14568 ?~ recovered ~
14387 ?. ?=(~ vars.u.recovered) ~
14569 ?. ?=(~ vars.u.recovered) ~
14388 ?. ?=(~ (itype-vars typ.u.recovered)) ~
14570 ?. ?=(~ (itype-vars typ.u.recovered)) ~
14389− `[env.u.added grouped.resolution artifacts.u.added]
14571+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]
14391+$ iview-site [xs=expr mapper=term]
14573+$ iview-site [xs=expr mapper=term]
14392++ program-view-site
14574++ program-view-site
@@ -14713,7 +14895,7 @@
14713 ?~ recovered ~
14895 ?~ recovered ~
14714 ?. ?=(~ vars.u.recovered) ~
14896 ?. ?=(~ vars.u.recovered) ~
14715 ?. ?=(~ (itype-vars typ.u.recovered)) ~
14897 ?. ?=(~ (itype-vars typ.u.recovered)) ~
14716− `[env.u.added grouped.resolution artifacts.u.added]
14898+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]
14718:: Recover exactly one direct keyed each/turn row mapper, then its view.
14900:: Recover exactly one direct keyed each/turn row mapper, then its view.
14719:: The prelude's own each and turn schemes determine the mapper gate: the
14901:: The prelude's own each and turn schemes determine the mapper gate: the
@@ -14935,7 +15117,7 @@
14935 ?~ recovered ~
15117 ?~ recovered ~
14936 ?. ?=(~ vars.u.recovered) ~
15118 ?. ?=(~ vars.u.recovered) ~
14937 ?. ?=(~ (itype-vars typ.u.recovered)) ~
15119 ?. ?=(~ (itype-vars typ.u.recovered)) ~
14938− `[env.u.added grouped.resolution artifacts.u.added]
15120+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]
14940:: The model a direct program's initializer must produce. Update's written
15122:: The model a direct program's initializer must produce. Update's written
14941:: two-item sample gives it when it can be read. Otherwise main's own program
15123:: two-item sample gives it when it can be read. Otherwise main's own program
@@ -15092,7 +15274,7 @@
15092 ?~ recovered ~
15274 ?~ recovered ~
15093 ?. ?=(~ vars.u.recovered) ~
15275 ?. ?=(~ vars.u.recovered) ~
15094 ?. ?=(~ (itype-vars typ.u.recovered)) ~
15276 ?. ?=(~ (itype-vars typ.u.recovered)) ~
15095− `[env.u.added grouped.resolution artifacts.u.added]
15277+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]
15097++ derived-poke-command-scheme
15279++ derived-poke-command-scheme
15098 |= [prelude=ifile action=itype]
15280 |= [prelude=ifile action=itype]
@@ -15260,9 +15442,9 @@
15260 (direct-prelude-evidence ds prelude.initial)
15442 (direct-prelude-evidence ds prelude.initial)
15261 ?~ heads resolution
15443 ?~ heads resolution
15262 =/ checked=(map term def) (direct-checked-gates ds env.resolution)
15444 =/ checked=(map term def) (direct-checked-gates ds env.resolution)
15263− =/ completed=[env=ienv artifacts=(list iwidth-definition)]
15445+ =/ completed=[env=ienv artifacts=(list iwidth-definition) failures=(list [name=term diag=idiag])]
15264 (add-supported-defs-core ~[main] 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)
15446 (add-supported-defs-core ~[main] 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)
15265− [env.completed grouped.resolution artifacts.completed]
15447+ [env.completed grouped.resolution artifacts.completed failures.resolution]
15267:: A static main may retain a generic element message in its ordinary
15449:: A static main may retain a generic element message in its ordinary
15268:: scheme. Instantiate that scheme, specialize it to canonical element !!,
15450:: scheme. Instantiate that scheme, specialize it to canonical element !!,
@@ -15478,6 +15660,9 @@
15478 !(lien prelude-molds |=(m=term =(m n)))
15660 !(lien prelude-molds |=(m=term =(m n)))
15663+ =/ scope=(unit iscope-diagnostic)
15664+ (module-scope-diagnostic mod(defs ordinary, imports faces) prelude-values prelude-molds)
15665+ ?^ scope [%| [(show-scope-diagnostic at src u.scope prelude) ~]]
15481 [%| [(crip "module has conflicting names: {(spud at)}") ~]]
15666 [%| [(crip "module has conflicting names: {(spud at)}") ~]]
15482 ?~ prelude [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
15667 ?~ prelude [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
15483 =/ prepared=iprelude [u.prelude prelude-values prelude-molds]
15668 =/ prepared=iprelude [u.prelude prelude-values prelude-molds]
@@ -15526,6 +15711,9 @@
15526 =/ ds=(list def) ?~(declared defs.mod defs.u.declared)
15711 =/ ds=(list def) ?~(declared defs.mod defs.u.declared)
15527 =/ checking=module mod(defs ds)
15712 =/ checking=module mod(defs ds)
15528 ?. (module-scope-valid checking prelude-values prelude-molds)
15713 ?. (module-scope-valid checking prelude-values prelude-molds)
15714+ =/ scope=(unit iscope-diagnostic)
15715+ (module-scope-diagnostic checking prelude-values prelude-molds)
15716+ ?^ scope [%| [(show-scope-diagnostic at src u.scope prelude) ~]]
15529 [%| [(crip "module has conflicting names: {(spud at)}") ~]]
15717 [%| [(crip "module has conflicting names: {(spud at)}") ~]]
15530 =/ vals=(list term) (global-value-names ds)
15718 =/ vals=(list term) (global-value-names ds)
15531 =/ js=jimports-detailed-result (resolve-jibb-imports-detailed imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
15719 =/ js=jimports-detailed-result (resolve-jibb-imports-detailed imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
@@ -15601,15 +15789,14 @@
15601 ?~ store-parts ds
15789 ?~ store-parts ds
15602 (skim ds |=(d=def !&(?=(%value -.d) =(%main name.d))))
15790 (skim ds |=(d=def !&(?=(%value -.d) =(%main name.d))))
15603 ?. (module-values-complete required env)
15791 ?. (module-values-complete required env)
15604− =/ pending=(unit [at=span msg=tape]) (module-pending-tag required env state 64)
15792+ =/ components=icomponents (graph-components required (global-value-names required))
15605− ?^ pending
15793+ =/ ordered=(list def) (dependency-order required components)
15606− [%| [(show-error src [at line.beg.at.u.pending col.beg.at.u.pending msg.u.pending]) ~]]
15607− :: A shadowing sample is an error, so it comes before any named value.
15608 =/ values=(list term) (weld prelude-values (weld (api-import-faces imports.mod) vals))
15794 =/ values=(list term) (weld prelude-values (weld (api-import-faces imports.mod) vals))
15609− =/ shadow=(unit [name=term at=span]) (module-sample-shadow required env values)
15795+ =/ checked=(map term def) (direct-checked-gates required env)
15610− ?^ shadow
15796+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence required prelude.state)
15611− =/ msg=tape "sample `{(trip name.u.shadow)}` shadows a name already in scope"
15797+ =/ diagnostic=(unit @t)
15612− [%| [(show-error src [at line.beg.at.u.shadow col.beg.at.u.shadow msg]) ~]]
15798+ (module-unresolved-diagnostic ordered env state checked heads failures.resolution values at src 64)
15799+ ?^ diagnostic [%| [u.diagnostic ~]]
15613 =/ missing=(unit term) (module-missing-value required env)
15800 =/ missing=(unit term) (module-missing-value required env)
15614 =/ named=tape ?~(missing "" ": ++ {(trip u.missing)}")
15801 =/ named=tape ?~(missing "" ": ++ {(trip u.missing)}")
15615 [%| [(crip "module definitions need unsupported inference: {(spud at)}{named}") ~]]
15802 [%| [(crip "module definitions need unsupported inference: {(spud at)}{named}") ~]]