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.
:stops-short facet -> prose: an implication of facet-contract this term does not
satisfy, and the reason. Checked against the set that is actually owed, in
both directions, so the record can neither be missing nor go stale once the
term gains the facet. A recorded exception, not a suppression: the rule
still holds over everything that does not carry one.
:opposing-read prose, on every :arbitrable term and on the one that deliberately
is not: what the conviction's opposing side is read through, and
whether that read survives the nogood defeating either member. Not
decidable from the declaration — arity names a second sentex exactly as
the four arbitrable marks do — so it is a stated claim rather than an
inferred one, which is what checks.clj's comment above arbitrable-kinds
says today in a place no validator could read.
: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 — and, one step further out,
which prover answers a term's goals. There is no :answered-by: applicable? is
per-prover logic over a goal's shape rather than a per-predicate fact, add-prover
registers provers with no entry here at all, and provers/sole-prover already asks the
coordination question a binding would be reaching for. The argument in full is
provers' header, under "Why a prover is not a predicate's property"; the fact about
the declaration that does belong is the :answers facet below.
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.
Two validators, two layers. check-families runs here, at this namespace's
load, over what one entry can say about another. check-facets runs at settle's,
because two of its rules read an arm that lives four layers up and a bottom namespace
cannot see whether an arm exists — it takes those facts as arguments rather than
requiring the layer that holds them.
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 defensible 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.
:stops-short facet -> prose: an implication of `facet-contract` this term does not
satisfy, and the reason. Checked against the set that is actually owed, in
both directions, so the record can neither be missing nor go stale once the
term gains the facet. A recorded exception, not a suppression: the rule
still holds over everything that does not carry one.
:opposing-read prose, on every `:arbitrable` term and on the one that deliberately
is not: what the conviction's opposing side is **read through**, and
whether that read survives the nogood defeating either member. Not
decidable from the declaration — `arity` names a second sentex exactly as
the four arbitrable marks do — so it is a stated claim rather than an
inferred one, which is what `checks.clj`'s comment above `arbitrable-kinds`
says today in a place no validator could read.
: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 — and, one step further out,
which *prover* answers a term's goals. There is no `:answered-by`: `applicable?` is
per-prover logic over a goal's shape rather than a per-predicate fact, `add-prover`
registers provers with no entry here at all, and `provers/sole-prover` already asks the
coordination question a binding would be reaching for. The argument in full is
`provers`' header, under "Why a prover is not a predicate's property"; the fact about
the *declaration* that does belong is the `:answers` facet below.
**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.
**Two validators, two layers.** `check-families` runs *here*, at this namespace's
load, over what one entry can say about another. `check-facets` runs at `settle`'s,
because two of its rules read an arm that lives four layers up and a bottom namespace
cannot see whether an arm exists — it takes those facts as arguments rather than
requiring the layer that holds them.
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 defensible 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 is indistinguishable from 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 is indistinguishable from 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.
(check-facets entries {:keys [recheck-subjects family-rosters]})Refuse at load a declaration whose facets do not add up — the cross-layer half of
check-families, and the one that turns wiring a new predicate into both lanes of a
family from a review item into a build failure.
above carries what the layers above this one enumerate, because this namespace is the
bottom one: a namespace holding both the declarations and the arms could only sit at the
top of the stack, where taxonomy and wff could not read it. So the facts that live
above arrive as arguments, and the validator is called from settle's namespace
load, which is the first place every facet's arm is visible. check-families stays at
this namespace's load, where what it checks is one entry against another and nothing
above is needed.
:recheck-subjects — the functors that post exception re-checks through the shared
path (special/declaration-subjects) rather than from an arm of their own.:family-rosters — family -> {roster-name functors}, the rosters that read a mark
family as a family. Each must enumerate exactly that family.Eight rules, eleven :mismatch values:
facet-contract and facets enumerate different keywords. A facet with no row is
one whose meaning its first user decided.:cached and a :none storage, or a storage and no :cached. The two say the same
thing and cannot disagree.:sweeps without the :reach facet. What a declaration puts back in question is
the reach; a kind without the facet says the sweep runs and nothing sweeps.:arbitrable term with no :opposing-read prose. The third conjunct of
arbitrability — that the read the conviction is made through does not depend on the
belief the nogood moves — is not decidable from data, so the honest encoding is a
required claim. arity carries the same field with the negative answer, which is
why it names a second sentex and is still not arbitrable.:inert term carrying another facet or a storage. The inert constructor makes
that unwritable; this is what says the constructor is still the only way in.:enumeration rule of special/check-declarations at the family level, and it is the
one rule here with no :stops-short escape: where a facet is a claim that an
entry can answer for in prose, a roster is a set sitting in another namespace, and two
enumerations of one fact do not get to disagree. quotedArg is why it exists — the
entry point read it up res/constraining-predicates with its three siblings while
provers/meta-constraint-shape had no row for it, so one declaration meant one thing
to assert and another to ask. The lane rule below caught that and offered a
record; a record is the wrong answer to two rosters disagreeing.:implication (facet-contract), :family-lane (a sibling spelling carries it) or
:recheck (it answers goals about a predicate and posts no re-check) — unless the
entry records the exception in :stops-short. The record is held to being exactly
the owed set, in both directions, so it can neither be missing nor go stale.What no rule can refuse is a spelling dropped from its family outright: membership
is a stated fact, as :inert is, and every rule above is about spellings that are
enrolled agreeing with each other. predicates_test pins tax/functional-family-marks
as a literal for exactly that move.
Rule 1 of the registry — :cached implies the whole integrate / disintegrate / rebuild
triple — is not here. It is special/check-entries, at the arm layer, where the
arms are visible and a special load proves it on its own; duplicating it here would
move the arm check to the top of the stack for nothing.
O(declarations), no KB, no I/O, no reflection: check-entries is the budget. Returns
entries unchanged so it can wrap a def.
Refuse at load a declaration whose facets do not add up — the **cross-layer** half of
`check-families`, and the one that turns wiring a new predicate into both lanes of a
family from a review item into a build failure.
`above` carries what the layers above this one enumerate, because this namespace is the
bottom one: a namespace holding both the declarations and the arms could only sit at the
*top* of the stack, where `taxonomy` and `wff` could not read it. So the facts that live
above arrive as arguments, and the validator is **called** from `settle`'s namespace
load, which is the first place every facet's arm is visible. `check-families` stays at
this namespace's load, where what it checks is one entry against another and nothing
above is needed.
* `:recheck-subjects` — the functors that post exception re-checks through the shared
path (`special/declaration-subjects`) rather than from an arm of their own.
* `:family-rosters` — `family -> {roster-name functors}`, the rosters that read a mark
family **as a family**. Each must enumerate exactly that family.
Eight rules, eleven `:mismatch` values:
* `facet-contract` and `facets` enumerate different keywords. A facet with no row is
one whose meaning its first user decided.
* a field value outside its closed vocabulary — a facet, a storage kind, a family, a
sweep kind, an argument kind.
* `:cached` and a `:none` storage, or a storage and no `:cached`. The two say the same
thing and cannot disagree.
* a `:sweeps` without the `:reach` facet. What a declaration puts back in question is
the reach; a kind without the facet says the sweep runs and nothing sweeps.
* an `:arbitrable` term with no `:opposing-read` prose. The third conjunct of
arbitrability — that the read the conviction is made through does not depend on the
belief the nogood moves — is not decidable from data, so the honest encoding is a
required claim. `arity` carries the same field with the negative answer, which is
why it names a second sentex and is still not arbitrable.
* an `:inert` term carrying another facet or a storage. The `inert` constructor makes
that unwritable; this is what says the constructor is still the only way in.
* a roster that reads a family as a family and enumerates something else. This is the
`:enumeration` rule of `special/check-declarations` at the family level, and it is the
one rule here with **no** `:stops-short` escape: where a facet is a claim that an
entry can answer for in prose, a roster is a set sitting in another namespace, and two
enumerations of one fact do not get to disagree. `quotedArg` is why it exists — the
entry point read it up `res/constraining-predicates` with its three siblings while
`provers/meta-constraint-shape` had no row for it, so one declaration meant one thing
to `assert` and another to `ask`. The lane rule below caught that and offered a
record; a record is the wrong answer to two rosters disagreeing.
* a facet the entry is **committed to** and does not carry, by one of three rules —
`:implication` (`facet-contract`), `:family-lane` (a sibling spelling carries it) or
`:recheck` (it answers goals about a predicate and posts no re-check) — unless the
entry records the exception in `:stops-short`. The record is held to being *exactly*
the owed set, in both directions, so it can neither be missing nor go stale.
**What no rule can refuse** is a spelling dropped from its family outright: membership
is a stated fact, as `:inert` is, and every rule above is about spellings that *are*
enrolled agreeing with each other. `predicates_test` pins `tax/functional-family-marks`
as a literal for exactly that move.
Rule 1 of the registry — `:cached` implies the whole integrate / disintegrate / rebuild
triple — is **not** here. It is `special/check-entries`, at the arm layer, where the
arms are visible and a `special` load proves it on its own; duplicating it here would
move the arm check to the top of the stack for nothing.
O(declarations), no KB, no I/O, no reflection: `check-entries` is the budget. Returns
`entries` unchanged so it can wrap a def.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.
What carrying a facet commits the declaration to — the closed vocabulary's own
contract, and what check-facets walks. Keyed by facet, and the keys are facets
exactly: the validator refuses the pair if they diverge, so growing the vocabulary
is the one commit the facets docstring promises rather than a keyword whose meaning
its first user decides.
:implies the facets carrying this one entails. Each is a bug the repo has paid
for, stated as an implication rather than as a review item: :convicts
without :reach convicts at the entry point and misses everything stored before
it, permanently, in the declaration-last arrival order (#54);
:arbitrable without :convicts arbitrates a violation nothing raises;
:derived and :migrates without :cached name a derivation path for a
triple that does not exist; :query-only without :answers is a term
refused at the entry point and answered by nothing at all; :retriggers without
:answers posts a re-check for a goal no prover takes.
:lane? is this a lane a mark family has to agree about. The enforcement
lanes are: a family joined to one of them in one spelling and not another
fails silently in the arrival order that spelling was the only way into,
which is #52 and #54, one omission and two lanes. So is :answers, for
the same reason seen from the query side — provers/meta-constraint-shape
is one table over the argument-constraint family, and a spelling missing
from it is answered from stored facts alone where its siblings are answered
up the genl closure. :retriggers is not: a re-check posting is one line
inside one arm, aimed at what that arm's own conclusion changes.
:query-only and :inert are classifications of the whole term, which a
family read by anything at all cannot differ about.
An implication a term does not satisfy is not automatically a refusal: it is a
refusal unless the entry records the exception, in :stops-short. Five entries carry
one today, over six facets: three terms convict with no reach, and three answer goals
about a predicate and post no re-check of their own. Each reason is about the engine rather than about the
declaration, and the point of the field is that the reason is written where a validator
can hold it to being exactly the set that is owed.
What carrying a facet commits the declaration to — the closed vocabulary's own
contract, and what `check-facets` walks. Keyed by facet, and the keys are `facets`
**exactly**: the validator refuses the pair if they diverge, so growing the vocabulary
is the one commit the `facets` docstring promises rather than a keyword whose meaning
its first user decides.
:implies the facets carrying this one entails. Each is a bug the repo has paid
for, stated as an implication rather than as a review item: `:convicts`
without `:reach` convicts at the entry point and misses everything stored before
it, permanently, in the declaration-last arrival order (#54);
`:arbitrable` without `:convicts` arbitrates a violation nothing raises;
`:derived` and `:migrates` without `:cached` name a derivation path for a
triple that does not exist; `:query-only` without `:answers` is a term
refused at the entry point and answered by nothing at all; `:retriggers` without
`:answers` posts a re-check for a goal no prover takes.
:lane? is this a lane a mark **family** has to agree about. The enforcement
lanes are: a family joined to one of them in one spelling and not another
fails silently in the arrival order that spelling was the only way into,
which is #52 and #54, one omission and two lanes. So is `:answers`, for
the same reason seen from the query side — `provers/meta-constraint-shape`
is one table over the argument-constraint family, and a spelling missing
from it is answered from stored facts alone where its siblings are answered
up the `genl` closure. `:retriggers` is not: a re-check posting is one line
inside one arm, aimed at what that arm's own conclusion changes.
`:query-only` and `:inert` are classifications of the whole term, which a
family read by anything at all cannot differ about.
An implication a term does not satisfy is not automatically a refusal: it is a
refusal *unless the entry records the exception*, in `:stops-short`. Five entries carry
one today, over six facets: three terms convict with no reach, and three answer goals
about a predicate and post no re-check of their own. Each reason is about the engine rather than about the
declaration, and the point of the field is that the reason is written where a validator
can hold it to being exactly the set that is owed.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-* entry points, 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
entry point 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-*` entry points, 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 entry point 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 entry point and answered by a prover instead.
Every term refused at the assert entry point 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 structure 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 structure 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 |