Pular para o conteúdo
← Voltar para projetos

Gen Inspect

gen-inspect — queries the state of graphs built with gen: selector algebra primary, logic programs for recursion and why, SQL as the novice surface; IR-decoupled renderers

#gen-inspect

The library that interrogates a materialized gen graph. Which nodes exist and of what kind, which edges are declared, which a policy program produced and why, and what reaches what.

A picture of the same materialization, with the policy's edge visibly distinct, is one output of that pipeline — not the ask.

genInspect = import gen-inspect/lib {
  prelude = gen.prelude;
  graph = gen.graph;
  select = gen.select;
  scope = gen.scope;
};

i = genInspect.mkInspector {
  register  = { … };   # kind -> name -> attrs
  relations = { … };   # label -> src -> [ dst ]
  program   = …;       # a gen-program program
  model     = …;       # its model, already solved by gen-scope
};

i.facts                    # the IR
i.query "SELECT …"         # the text surface
i.select selector          # the programmatic surface; the result is an IR
i.render.mermaid i.facts   # the picture's source

#Why it exists

A person sits down in front of an assembled graph and needs to interrogate it. Interrogating a materialized graph is a capability every gen consumer needs, so it ships as end-user surface at the framework stratum rather than as a demo.

A fixed menu of demo queries fails that by construction. The surface takes an unanticipated query, and every way that query can be wrong is refused by name, with the known set — because against a raw row source each of those mistakes reads [] at exit 0, which is indistinguishable from "the policy produced nothing".

#The IR contract

Between materialize and everything downstream sits ONE named contract. Renderers read the IR and never the scope, and a query's result IS an IR, so filters are the selector algebra rather than an ad-hoc filter set.

nodes   : [ { id; kind; attrs; } ]
edges   : [ { src; dst; label; origin; } ]
origins : { "<label>:<src>:<dst>" -> origin }
origin  : { kind = "declaration"; site; }
        | { kind = "policy"; derivations = [ { rule = { head; pos; neg; };
                                              fired = [ { atom; verdict; sign; } ]; } ]; }
tables  : kind -> name -> { name; kind; <attrs splatted>; },  plus `edge`
kinds   : kind -> { name; }
labels  : [ label ]  (declared ++ derived)
graph   : the gen-graph labeled value over the SAME edge list

origin is constructed at materialization, and the engine is not its source. gen-scope's provenance is a condensation-depth stamp, not per-atom provenance. There is no capture stage and nothing is instrumented: the program value and the model verdicts are both in hand, which is what makes origin derivable at all.

A witness is body-checked, never head-matched. Van Gelder, Ross & Schlipf 1991 Def 3.3: an atom is derived iff some rule has it as head and every body literal is true in the model. A head match alone reports a rule whose body is false, in a field named fired — Def 3.1 calls that a witness of unusability.

Provenance rider. origins is why/derivation provenance in the sense of Cheney, Chiticariu & Tan (2009) — a name taken from the literature rather than a citation checked against a held copy. The semiring is deliberately not realized and is not planned: these are records about a run, and nothing here computes with them algebraically.

#Three layers, one model

layer form what it is where recursion lives
(c) selectors gen-select combinators the primary programmatic API; the guard sublanguage none — no fixpoint
(b) programs gen-program on gen-scope's engine recursion, derivation, why the fixpoint
(a) SQL text the novice surface compiled onto b + c

The compile rule is three routes by executor, not two by recursion.

construct executor
WHERE predicate gen-select
JOIN, projection, ORDER BY, LIMIT gen-inspect's own fold
reachability, transitive closure, WHY the program layer

The selector layer is the guard sublanguage, not "the non-recursive fragment". Measured: gen-select's constructors yield exactly nine tags, and sel ? join, sel ? comprehension and sel ? fix are all false. So a JOIN has no selector to compile to and routes to the fold — a JOIN is not refused. The third route is a refusal door by name, not a stub.

#The example

examples/fleet/ carries a campanology register whose policy derives one edge no declaration states: hemony rings bourdon, through two intermediate derivations. enrolled is both a declared and a derived label, which is why the dynamic label set is derived from the program rather than hand-written — a hand-written list drops the derived edge with no diagnostic.

#The three human entries

The library publishes pure functions only — no app, no CLI. Run from examples/fleet/.

$ nix eval --json .#inspect --apply 'i: i.query "SELECT src, dst FROM edge WHERE label = '\''rings'\''"'
[{"dst":"bourdon","src":"hemony"}]
$ nix eval --raw .#inspect --apply 'i: i.render.mermaid i.facts'
flowchart LR
  campanile["campanile<br/>belfry"]
  lantern["lantern<br/>belfry"]
  compline["compline<br/>chime"]
  evensong["evensong<br/>chime"]
  matins["matins<br/>chime"]
  chiming["chiming<br/>peal"]
  full_circle["full-circle<br/>peal"]
  hemony["hemony<br/>ringer"]
  mears["mears<br/>ringer"]
  rudhall["rudhall<br/>ringer"]
  angelus["angelus<br/>tocsin"]
  bourdon["bourdon<br/>tocsin"]
  sanctus["sanctus<br/>tocsin"]
  tenor["tenor<br/>tocsin"]
  full_circle -->|absorbs| chiming
  bourdon -->|admits| full_circle
  tenor -->|admits| chiming
  hemony -->|enrolled| chiming
  rudhall -->|enrolled| chiming
  angelus -->|housed| lantern
  bourdon -->|housed| campanile
  sanctus -->|housed| lantern
  tenor -->|housed| campanile
  compline -->|hung| sanctus
  evensong -->|hung| bourdon
  matins -->|hung| tenor
  hemony -.->|enrolled| full_circle
  hemony -.->|rings| bourdon

The two dashed edges are the policy's; the twelve solid ones are declared. hemony -.->|rings| bourdon is the edge no relations entry states.

$ nix repl .#
Loading installable 'git+file:///…/gen-inspect?dir=examples/fleet#'...
Added 3 variables.

nix-repl> :p (builtins.head inspect.facts.origins."rings:hemony:bourdon".derivations).fired
[
  { atom = "enrolled:hemony:full-circle"; sign = "pos"; verdict = "true"; }
  { atom = "admits:bourdon:full-circle"; sign = "pos"; verdict = "true"; }
  { atom = "silenced:hemony:bourdon"; sign = "neg"; verdict = "false"; }
]

The picture itself is a build, and not a CI cell:

nix build .#fleet-graph-svg

Picture fidelity needs an element-scoped predicate: mermaid emits edge-pattern-dotted in its stylesheet unconditionally, so a whole-file count reds against a correct build and greens at the red state, and stroke-dasharray discriminates not at all. What CI asserts is the source.

#Every way a query can be wrong

$ nix eval .#inspect --apply 'i: i.query "SELECT name FROM anvils"'
error: gen-inspect: unknown name 'anvils'; known: belfry, chime, edge, peal, ringer, tocsin

$"SELECT name FROM tocsin WHERE wieght = 'heavy'"
error: gen-inspect: unknown name 'wieght'; known: belfry, kind, name, weight

$"SELECT src FROM edge WHERE label = 'anvils'"
error: gen-inspect: unknown label 'anvils'; known: absorbs, admits, enrolled, housed, hung, rings

$"SELECT src FROM reaches"
error: gen-inspect: unsupported construct 'reaches' (reachability); it compiles onto the program
layer, which this gate does not build.

The third one is the sharp case: WHERE label = 'anvils' is a well-formed query over a known column, so without its door it returns [] at exit 0 and reads as "the policy produced nothing".

#Dependencies, and what is not one

Four gen libraries, all injected as values — only plain data crosses a gen↔gen boundary. gen-prelude, gen-graph and gen-select are what this gate evaluates through; gen-scope is the program route's evaluator, declared now so that route's landing changes no caller.

The design names a fifth, gen-program, and it is absent by measurement. The hub injects a framework member's substrate through a function of its members binding — exactly the eighteen roster entries whose .lib is published applied — and program is one of the three unapplied members that the substrate fold itself produces, so it is not in scope where a fourth substrate entry is written. Declaring it here would pin a dependency the hub has no way to inject. Gate 2 adds it in the commit that replaces compile's body.

nixpkgs is not a dependency. The SQL parser and executor are copied from gen-scope/examples/sql-schema, which took nixpkgs lib — twelve distinct lib.* names, six of them absent from gen-prelude. lib/extras.nix supplies those seven names over builtins instead, because every gen library's lib/ is free of the nixpkgs standard library, and a library at this layer declaring nixpkgs as a dependency would hand its whole closure to every consumer of this one. ci/tests/purity.nix is what keeps that from reverting.

The copies carry an origin header naming the source revision and the whole diff against it. The kind-alias table is stripped to the identity: its 23 entries sit at kind position and name machines, users and networks, and this library's vocabulary is invented end to end.

#Tests

nix flake check ./ci                    # the suites, through the batch asserter
nix-unit --flake ./ci#tests             # the same cells, per cell
nix-unit --flake ./ci#testsError        # the refusals, asserted by message
cd ci && nix fmt -- --ci

Cells whose subject is an error message live on testsError: the asserter behind checks.default forces every flake.tests cell's expr unconditionally, so a throwing expr crashes that gate instead of failing it.

Nova versão disponível.