Skip to main content

Module mirror

Module mirror 

Source
Expand description

The core beside a Context: a Kernel::logos per thread, kept in step with the context it last mirrored through that context’s admission log.

A Context is persistent and shared between threads; the core is a mutable, single-threaded kernel. So the core is not a field of the context but a mirror of one context lineage per thread, and sync brings it to a context:

  • the context’s log head is the mirror’s: nothing changed;
  • the log reaches the mirror’s head: the entries since name what was registered, and those declarations are admitted in dependency order, unless the entries change something the mirror holds (a held name removed or registered again, a constructor added to a held family, a name a refused declaration referenced, a change to how Int literals read), which is a branch. The quotient needs no rule of its own: its certification logs all four primitives, so they arrive together and are installed whole, or a held one is registered again;
  • the log reaches the standard library’s head instead: the mirror restarts from a snapshot of the standard library’s core, kept per thread, and advances from there;
  • anything else, a branch included: the context is replayed whole (logos_env::replay).

Every route ends where a replay of the context ends: the same declarations admitted, with the same verdicts.

A thread’s mirror lives on a core thread of its own: an admission recurses as deep as the declaration it checks, deeper than a caller’s stack may reach, and the core is single-threaded state that never moves between threads. sync and with run there and answer the caller.

Structs§

Synced
What one sync did: its route, and the core’s verdict on each declaration it admitted.

Enums§

Route
How sync brought the mirror to a context.

Functions§

sync
Bring this thread’s mirror to ctx.
with
Bring this thread’s mirror to ctx and run f on its kernel. The mirror is out of its slot while f runs, so a sync inside f builds its own and this one is put back after.