What is said about each term of the engine's own grammar, in one place — the declaration half of the twenty-odd functor-keyed rosters scattered across nine namespaces, none of which can see each other.
The problem this is the bottom half of. Adding an engine-interpreted predicate
means finding every place that keys on a functor name and writing an entry there.
special/entries is the one that got it right: a single ordered table walked by four
consumers, refused at load if an entry is half-written. Every other roster —
settle's eight, taxonomy's three, checks' four, provers' four, sentex's
three, kb/equality-predicates, inherit/declarations, vocabulary/roster — is a
projection of the same fact, written where it was needed. The record of what that
costs is #45 (one trio spelled out in two places that had to agree), #52 and #54 (one
spelling wired into one lane of a family and not the other, twice, in different lanes,
from the same omission).
Why data and arms are split, and this half is the data. The arms need functions
from four different layers — taxonomy, wff, checks, settle — so a namespace
holding both could only ever sit at the top of the stack, where taxonomy and wff
cannot read it. This namespace therefore requires nothing but clojure.* and sits
below naming and sentex, at the bottom. It holds what a term says; each layer
above attaches what is done about it. Where a field seems to want a function it
holds a keyword naming one, resolved by the layer that owns the function.
Fields. Each entry is term -> spec:
:shape how the term is written as a sentence, or nil for one that is never a
sentence functor (a collection: string, thing, binary_predicate).
{:args [kind …]}, optionally :optional [kind …] for a trailing
argument that may be omitted and :variadic kind for an open tail.
Argument kinds are argument-kinds below; arity is (count :args).
:storage [kind target] — which of a small closed set of storage shapes the
declaration is cached under, and which table it lands in. [:none] for
a term nothing caches. storage-kinds below.
:checked does special/entries give the functor a structural well-formedness arm.
:facets a set from the closed vocabulary facets below — the lanes the term
takes part in. An open set of keywords would be a roster again, with the
same drift and none of the checking.
:family the family whose spellings must move together, or nil. functional and
functionalInArg are one family written two ways; the four argument
constraints are another. mark-families below.
:sweeps what a declaration arriving after the content it constrains puts back
in question — sweep-kinds below — or absent for a term whose retroactive
half is not settle's clash-exposure pass. The :reach facet says that a
term sweeps; this says what, for the one lane whose reaches have names.
:notes prose, only where the term does something this vocabulary has no facet
for. A note is a finding, not a description: each one is a lane the
facet vocabulary does not reach yet.
:enforced prose naming the code path that reads the term — what a KB author is told
by core/interpreted when they ask whether a declaration does anything.
Carried by the terms CxCore comments and by no others, which is why an
entry without it is not a defect: the seven grammar terms CxCore does not
comment are outside the question rather than unanswered.
:inert prose recording that nothing reads the term and that this is a
decision. Written by the inert constructor, which sets the facet with
it, so the class is never a second opinion about the facets.
What is deliberately not here is the arms themselves.
What reads this. special/entries joins the declarations to special's arms;
taxonomy's three rosters (closure-relations, arg-declaration-props,
functional-family-marks), settle's clash-declaration and trigger rosters,
spec/::prop-kind and vocabulary/roster are field reads.
The rosters that have not moved yet are reconstructed from here by predicates_test
and asserted equal to the live one, which is the only honest proof that the population
is right before a consumer switches over. A roster that has moved is proved
differently: its value becomes a literal in the test, since a reconstruction of a
derived var proves the wiring and nothing about what it holds.
Order is content. entries is a vector, not a map, because special/entries is
ordered and rebuild-taxonomy replays it top to bottom with a rebuild arm allowed to
read what an earlier one wrote. The table's functors come first, in the table's own
order; the rest of CxCore's grammar follows.
What is *said* about each term of the engine's own grammar, in one place — the
declaration half of the twenty-odd functor-keyed rosters scattered across nine
namespaces, none of which can see each other.
**The problem this is the bottom half of.** Adding an engine-interpreted predicate
means finding every place that keys on a functor name and writing an entry there.
`special/entries` is the one that got it right: a single ordered table walked by four
consumers, refused at load if an entry is half-written. Every other roster —
`settle`'s eight, `taxonomy`'s three, `checks`' four, `provers`' four, `sentex`'s
three, `kb/equality-predicates`, `inherit/declarations`, `vocabulary/roster` — is a
*projection* of the same fact, written where it was needed. The record of what that
costs is #45 (one trio spelled out in two places that had to agree), #52 and #54 (one
spelling wired into one lane of a family and not the other, twice, in different lanes,
from the same omission).
**Why data and arms are split, and this half is the data.** The arms need functions
from four different layers — `taxonomy`, `wff`, `checks`, `settle` — so a namespace
holding both could only ever sit at the *top* of the stack, where `taxonomy` and `wff`
cannot read it. This namespace therefore requires nothing but `clojure.*` and sits
below `naming` and `sentex`, at the bottom. It holds what a term *says*; each layer
above attaches what is *done* about it. Where a field seems to want a function it
holds a **keyword naming** one, resolved by the layer that owns the function.
**Fields.** Each entry is `term -> spec`:
:shape how the term is written as a sentence, or nil for one that is never a
sentence functor (a collection: `string`, `thing`, `binary_predicate`).
`{:args [kind …]}`, optionally `:optional [kind …]` for a trailing
argument that may be omitted and `:variadic kind` for an open tail.
Argument kinds are `argument-kinds` below; arity is `(count :args)`.
:storage `[kind target]` — which of a small closed set of storage shapes the
declaration is cached under, and which table it lands in. `[:none]` for
a term nothing caches. `storage-kinds` below.
:checked does `special/entries` give the functor a structural well-formedness arm.
:facets a set from the **closed** vocabulary `facets` below — the lanes the term
takes part in. An open set of keywords would be a roster again, with the
same drift and none of the checking.
:family the family whose spellings must move together, or nil. `functional` and
`functionalInArg` are one family written two ways; the four argument
constraints are another. `mark-families` below.
:sweeps what a declaration arriving *after* the content it constrains puts back
in question — `sweep-kinds` below — or absent for a term whose retroactive
half is not `settle`'s clash-exposure pass. The `:reach` facet says that a
term sweeps; this says *what*, for the one lane whose reaches have names.
:notes prose, only where the term does something this vocabulary has no facet
for. A note is a **finding**, not a description: each one is a lane the
facet vocabulary does not reach yet.
:enforced prose naming the code path that reads the term — what a KB author is told
by `core/interpreted` when they ask whether a declaration does anything.
Carried by the terms CxCore comments and by no others, which is why an
entry without it is not a defect: the seven grammar terms CxCore does not
comment are outside the question rather than unanswered.
:inert prose recording that nothing reads the term **and that this is a
decision**. Written by the `inert` constructor, which sets the facet with
it, so the class is never a second opinion about the facets.
**What is deliberately not here** is the arms themselves.
**What reads this.** `special/entries` joins the declarations to `special`'s arms;
`taxonomy`'s three rosters (`closure-relations`, `arg-declaration-props`,
`functional-family-marks`), `settle`'s clash-declaration and trigger rosters,
`spec/::prop-kind` and `vocabulary/roster` are field reads.
The rosters that have not moved yet are reconstructed from here by `predicates_test`
and asserted equal to the live one, which is the only honest proof that the population
is right before a consumer switches over. A roster that *has* moved is proved
differently: its value becomes a literal in the test, since a reconstruction of a
derived var proves the wiring and nothing about what it holds.
**Order is content.** `entries` is a vector, not a map, because `special/entries` is
ordered and `rebuild-taxonomy` replays it top to bottom with a rebuild arm allowed to
read what an earlier one wrote. The table's functors come first, in the table's own
order; the rest of CxCore's grammar follows.What an argument position denotes, as the wff arms already hold it. Closed: a
kind here is one an arm can be generated from, so a position no kind fits is a
position whose check has to stay hand-written.
The distinction that matters most is :predicate against :relation. A mark read
off a sentence's functor (prop-problems, functional-in-arg-problems) holds its
subject to a symbol that is not an individual — a functor is a symbol. An argument
constraint (arg-constraint-problems, arg-preserving-problems) is looser on
purpose: a function has argument positions exactly as a predicate does, a function is
CapitalCamelCase and so reads as an individual, and a relation may be denoted by a NAT
rather than named. Collapsing the two refuses the conventional spelling and waves the
exotic one through.
What an argument position denotes, as the `wff` arms already hold it. Closed: a kind here is one an arm can be *generated* from, so a position no kind fits is a position whose check has to stay hand-written. The distinction that matters most is `:predicate` against `:relation`. A mark read off a sentence's functor (`prop-problems`, `functional-in-arg-problems`) holds its subject to a symbol that is not an individual — a functor is a symbol. An argument *constraint* (`arg-constraint-problems`, `arg-preserving-problems`) is looser on purpose: a function has argument positions exactly as a predicate does, a function is CapitalCamelCase and so reads as an individual, and a relation may be denoted by a NAT rather than named. Collapsing the two refuses the conventional spelling and waves the exotic one through.
(by-facet facet)Every term carrying facet, as a set — what the lane rosters become.
Every term carrying `facet`, as a set — what the lane rosters become.
(by-family fam)Every spelling of the functional mark family fam, mapped to its written shape —
:mark for the one-place (F P), :mark-in-arg for the two-place (F P n).
The shape is derived from the argument list rather than stated, so a spelling cannot
be enrolled in the family under a shape its own arguments contradict. The marked
predicate is argument 1 of either, which is what lets a reader that only wants the
predicate ignore the shape entirely — and what a family whose spellings are written at
three arities and five (:argument-constraint) has no use for, family being the
reader for that one.
Every spelling of the **functional** mark family `fam`, mapped to its written shape — `:mark` for the one-place `(F P)`, `:mark-in-arg` for the two-place `(F P n)`. The shape is *derived* from the argument list rather than stated, so a spelling cannot be enrolled in the family under a shape its own arguments contradict. The marked predicate is argument 1 of either, which is what lets a reader that only wants the predicate ignore the shape entirely — and what a family whose spellings are written at three arities and five (`:argument-constraint`) has no use for, `family` being the reader for that one.
(by-storage kind)Every term whose storage kind is kind, mapped to the table it lands in.
Every term whose storage kind is `kind`, mapped to the table it lands in.
(by-sweep kind)Every term whose arrival sweeps kind, as a set.
Every term whose arrival sweeps `kind`, as a set.
Every term special/entries gives the integrate / disintegrate / rebuild triple.
Every term `special/entries` gives the integrate / disintegrate / rebuild triple.
Every term special/entries gives a structural well-formedness arm.
Every term `special/entries` gives a structural well-formedness arm.
Every cached term whose triple runs on the derivation path as well.
Every cached term whose triple runs on the derivation path as well.
[term spec] pairs, ordered. special/entries' fifty functors first, in the table's
own order — that order is replayed by rebuild-taxonomy and so is content — then the
rest of the grammar vocabulary/roster covers.
Read entry / by-facet / by-family / by-storage below rather than this vector;
they are what the rosters above become.
`[term spec]` pairs, ordered. `special/entries`' fifty functors first, in the table's own order — that order is replayed by `rebuild-taxonomy` and so is content — then the rest of the grammar `vocabulary/roster` covers. Read `entry` / `by-facet` / `by-family` / `by-storage` below rather than this vector; they are what the rosters above become.
(entry term)The spec for term, or nil for one this grammar does not cover.
Nil is not "nothing reads it": the population is CxCore's own vocabulary, so an ordinary domain predicate is simply not a term this question is asked about.
The spec for `term`, or nil for one this grammar does not cover. Nil is **not** "nothing reads it": the population is CxCore's own vocabulary, so an ordinary domain predicate is simply not a term this question is asked about.
The lanes a term takes part in. Closed, and closed on purpose: growing it is one commit that adds the keyword here and the implication that governs it to the facet validator at the same time, so a facet can never mean whatever its first user assumed.
Six of the ten are reconstructible from a live data structure and are pinned that way
by predicates_test. Four — :answers, :retriggers, :convicts and :inert —
are claims: no roster in the tree states them, which is exactly why they are the
ones that go wrong quietly.
The lanes a term takes part in. **Closed**, and closed on purpose: growing it is one commit that adds the keyword here and the implication that governs it to the facet validator at the same time, so a facet can never mean whatever its first user assumed. Six of the ten are reconstructible from a live data structure and are pinned that way by `predicates_test`. Four — `:answers`, `:retriggers`, `:convicts` and `:inert` — are *claims*: no roster in the tree states them, which is exactly why they are the ones that go wrong quietly.
(family fam)Every spelling in family fam, as a set — the family read as the thing it is, which
is what a reader that acts on all of them wants. by-family adds the written shape,
which only the functional family distinguishes.
Every spelling in family `fam`, as a set — the family read as the thing it is, which is what a reader that acts on all of them wants. `by-family` adds the written shape, which only the functional family distinguishes.
The terms special/entries holds an entry for at all — the ones that are cached, or
structurally checked, or both. check-entries refuses anything else, so this is a
definition and not an observation.
The terms `special/entries` holds an entry for at all — the ones that are cached, or structurally checked, or both. `check-entries` refuses anything else, so this is a definition and not an observation.
The families whose spellings must move together. A family lives in more than one
lane and has twice been joined to only one (#52, #54), so the family is named once and
each spelling carries it. tax/functional-family-marks and
tax/arg-declaration-props are this field read back.
:functional is acted on by the merge lane (special's equate-* doors, where
two fillers of a functional slot are equated) and by the clash exposure lane
(settle's declaration reach and trigger rosters, where two unmergeable fillers are
reported). Both lanes have to recognize the same spellings, and neither fails loudly
when it does not — the merge simply does not happen, or the clash simply is not
reported, in the one arrival order that route was the only way into. Enrolling
functionalInArg by name in each place is what left #52 (the declaration-last merge
door held an exact-functor test) and #54 (the declaration arrived and swept nothing)
open at the same time, in different lanes, from the same omission. So a third
spelling is added here and the lanes follow.
:argument-constraint is the four declarations that constrain a predicate's
argument positions. They are read as one — the descension asks per super-predicate
whether it declares anything, special/entail-existing sweeps three of the four,
checks pairs two of them against each other — and each is written at its own arity,
which is why the family is the thing a reader names and the shape is not.
A family is not a storage roster. functional stores under the :functional
prop where functionalInArg stores [pred n] pairs; the two have no common storage
to be rostered by, only a common family and a common argument 1. Keep :family and
:storage separate or #52 comes back with a new number.
The families whose spellings must move together. A family lives in more than one lane and has twice been joined to only one (#52, #54), so the family is named once and each spelling carries it. `tax/functional-family-marks` and `tax/arg-declaration-props` are this field read back. **`:functional`** is acted on by the *merge* lane (`special`'s `equate-*` doors, where two fillers of a functional slot are equated) and by the *clash exposure* lane (`settle`'s declaration reach and trigger rosters, where two unmergeable fillers are reported). Both lanes have to recognize the same spellings, and neither fails loudly when it does not — the merge simply does not happen, or the clash simply is not reported, in the one arrival order that route was the only way into. Enrolling `functionalInArg` by name in each place is what left #52 (the declaration-last merge door held an exact-functor test) and #54 (the declaration arrived and swept nothing) open at the same time, in different lanes, from the same omission. So a third spelling is added *here* and the lanes follow. **`:argument-constraint`** is the four declarations that constrain a predicate's argument positions. They are read as one — the descension asks per super-predicate whether it declares *anything*, `special/entail-existing` sweeps three of the four, `checks` pairs two of them against each other — and each is written at its own arity, which is why the family is the thing a reader names and the shape is not. A family is **not** a storage roster. `functional` stores under the `:functional` prop where `functionalInArg` stores `[pred n]` pairs; the two have no common storage to be rostered by, only a common family and a common argument 1. Keep `:family` and `:storage` separate or #52 comes back with a new number.
(mark-shape term):mark for a one-place mark (F P), :mark-in-arg for the two-place (F P n) — a
term's written shape read as the distinction every lane that recognizes a mark at its
own arity dispatches on.
Derived from the declared argument list rather than stated, so a spelling cannot be recognized at an arity its own arguments contradict. The marked predicate is argument 1 of either, which is what lets a reader that only wants the predicate ignore the shape.
`:mark` for a one-place mark `(F P)`, `:mark-in-arg` for the two-place `(F P n)` — a term's written shape read as the distinction every lane that recognizes a mark at its own arity dispatches on. Derived from the declared argument list rather than stated, so a spelling cannot be recognized at an arity its own arguments contradict. The marked predicate is argument 1 of either, which is what lets a reader that only wants the predicate ignore the shape.
(prop-kind term)The tax/props keyword term's mark maintains, or nil for a term that maintains
none. special/prop-entry reads its arms' kind through this rather than taking it
as a parameter, which is what makes the set below a fact about the declarations.
The `tax/props` keyword `term`'s mark maintains, or nil for a term that maintains none. `special/prop-entry` reads its arms' kind through this rather than taking it as a parameter, which is what makes the set below a fact about the declarations.
(prop-kinds)The tax/props keywords the grammar declares, as a set — what spec/::prop-kind
enumerates, read off the declarations that maintain them.
The `tax/props` keywords the grammar declares, as a set — what `spec/::prop-kind` enumerates, read off the declarations that maintain them.
(prop-marks facet)The [term prop-keyword] pairs of every term carrying facet and stored as a
tax/props mark, in entries order — a facet read and a storage read at once, because
the two spellings of a mark are what a caller comparing a sentence's functor against a
stored key needs together.
Case conversion is not an alternative to the pairing and never was: anti_transitive
stores under :anti-transitive. The declaration states the keyword; this reads it
back.
The `[term prop-keyword]` pairs of every term carrying `facet` and stored as a `tax/props` mark, in `entries` order — a facet read and a storage read at once, because the two spellings of a mark are what a caller comparing a *sentence's* functor against a *stored* key needs together. Case conversion is not an alternative to the pairing and never was: `anti_transitive` stores under `:anti-transitive`. The declaration states the keyword; this reads it back.
Every term refused at the assert door and answered by a prover instead.
Every term refused at the assert door and answered by a prover instead.
(shape-of term)term's sentence shape, or nil for a term never written as a sentence functor.
`term`'s sentence shape, or nil for a term never written as a sentence functor.
The shapes a declaration is cached under. Each names what the add / drop / rebuild triple looks like, which is the whole of why the set is small: three arms that differ only in the table they call are three arms one shape can write.
:mark is not :prop, and the difference is not cosmetic: :prop means the
tax/props roster, whose keys spec/::prop-kind pins, while disjoint_metatype and
sibling_disjoint are one-term marks into tables of their own. Calling them :prop
would put two keywords in that spec that no has-prop? ever answers.
The shapes a declaration is cached under. Each names what the add / drop / rebuild triple looks like, which is the whole of why the set is small: three arms that differ only in the table they call are three arms one shape can write. `:mark` is **not** `:prop`, and the difference is not cosmetic: `:prop` means the `tax/props` roster, whose keys `spec/::prop-kind` pins, while `disjoint_metatype` and `sibling_disjoint` are one-term marks into tables of their own. Calling them `:prop` would put two keywords in that spec that no `has-prop?` ever answers.
What a declaration arriving after the content it constrains puts back in question
— the reach settle's clash-exposure pass runs for it, and so the shape of the split
settle/clash-declaration-kinds is written as.
A declaration is not its own candidate the way a fact is. (disjoint dog cat) arriving
after both memberships has to reach them, or whether the pair is reported depends on
which was written first. The kind says where that reach goes: over the terms the
declaration separates, or over the facts beneath the predicate a descending mark now
stands over, or both.
A term is a clash declaration by carrying one of these, so enrolling one and leaving
declaration-reach with no arm for it is not a state that roster can be in. Absent is
the answer for a term whose retroactive half is a different mechanism: arity's is a
report that moves no belief, the argument constraints' is special/entail-existing,
which mints rather than convicting, and siblingDisjointException's runs in the removal
direction.
Carrying a sweep is not being in settle/definitional-marks, and reading one roster
as though it were the other is what #54 filed. That roster pairs a functor with the
taxonomy prop key it stores under, which functionalInArg has none of — it stores
[pred n] pairs — so the generalized mark is correctly absent from it, and must still
carry :predicate-marked here and a shape for the lane that recognizes it at its own
arity. Derive a reach from the pairing table and the generalized mark silently loses
the one arrival order — declaration-last over an unmergeable pair — that functional
itself handles.
What a declaration arriving **after** the content it constrains puts back in question — the reach `settle`'s clash-exposure pass runs for it, and so the shape of the split `settle/clash-declaration-kinds` is written as. A declaration is not its own candidate the way a fact is. `(disjoint dog cat)` arriving after both memberships has to reach them, or whether the pair is reported depends on which was written first. The kind says where that reach goes: over the **terms** the declaration separates, or over the **facts beneath the predicate** a descending mark now stands over, or both. **A term is a clash declaration by carrying one of these**, so enrolling one and leaving `declaration-reach` with no arm for it is not a state that roster can be in. Absent is the answer for a term whose retroactive half is a different mechanism: `arity`'s is a *report* that moves no belief, the argument constraints' is `special/entail-existing`, which mints rather than convicting, and `siblingDisjointException`'s runs in the removal direction. **Carrying a sweep is not being in `settle/definitional-marks`**, and reading one roster as though it were the other is what #54 filed. That roster pairs a functor with the taxonomy prop key it stores under, which `functionalInArg` has none of — it stores `[pred n]` pairs — so the generalized mark is correctly absent from it, and must still carry `:predicate-marked` here and a shape for the lane that recognizes it at its own arity. Derive a reach from the pairing table and the generalized mark silently loses the one arrival order — declaration-last over an unmergeable pair — that `functional` itself handles.
(sweeps)term -> sweep kind over every term that sweeps at all, in entries order — what
settle/clash-declaration-kinds groups by kind and clash-declaration-kind reads
back flat.
`term -> sweep kind` over every term that sweeps at all, in `entries` order — what `settle/clash-declaration-kinds` groups by kind and `clash-declaration-kind` reads back flat.
entries as the lookup map every reader below dispatches through — and where
check-families runs, so a half-wired family fails at namespace load rather than in the
one lane it was left out of.
`entries` as the lookup map every reader below dispatches through — and where `check-families` runs, so a half-wired family fails at namespace load rather than in the one lane it was left out of.
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |