Quasiquotation — the metalinguistic constructor (mention-opacity: docs/argtypes.md).
(Quasiquote T) builds the syntactic term T with each (Unquote v) hole replaced by
v, and names the result as syntax — a mention. (Quasiquote (isa (Unquote ?x) Dog))
fired with ?x=Fido constructs the term for (isa Fido Dog).
The model is skolemization, not the evaluate prover: a Quasiquote is a
term-constructor sitting in argument position ((believes Tom (Quasiquote …))), built
deterministically from a firing's bindings and reified before placement. Reduction of a
ground (Quasiquote T) strips its Unquote holes to the expression E, then reifies
(Quote E) — Quote being a reifiable quoting function, so E reifies to an opaque
nat/ constant that mention-opacity holds apart from its referents' merges. Determinism
is content-addressed for free: E is the content, so nat/reify-or-mint-nat dedups two
firings on one binding to one constant (no rule digest / frontier is needed, unlike a
skolem witness, which is anonymous).
Quasiquote is an unreifiable_function, so an open template — the one that lives in a
rule consequent until the antecedent binds its Unquote holes — stays structural and is
never minted; range restriction (rules/check-range-restricted) already refuses a hole no
antecedent binds, so an open template never reaches storage. It is a quoting_function
too, so while it waits in the rule its Unquote-marked spellings are held opaque to an
identity merge exactly as a Quote payload is.
Turned on by declaration, like reifiable_function turns the reify pass on: a KB that has
not declared (quoting_function Quasiquote) pays one taxonomy-prop read per firing/assert
and the reducer is a no-op. And like reification, it is declared before use: opacity is
applied when a mention is reified and again in the equality congruence, each gated on the
mark being present then, so ensure-quasiquote-functions (or the four marks) must precede
the constructions it governs and any identity merge over the referents inside them. A reify
or merge processed while the mark is absent — before it is declared, or after it is retracted
— is not held opaque and folds the mention onto its referent's class.
Quasiquotation — the metalinguistic constructor (mention-opacity: docs/argtypes.md). `(Quasiquote T)` builds the syntactic term `T` with each `(Unquote v)` hole replaced by `v`, and names the result *as syntax* — a mention. `(Quasiquote (isa (Unquote ?x) Dog))` fired with `?x`=Fido constructs the term for `(isa Fido Dog)`. The model is **skolemization**, not the `evaluate` prover: a `Quasiquote` is a term-constructor sitting in argument position (`(believes Tom (Quasiquote …))`), built deterministically from a firing's bindings and reified before placement. Reduction of a ground `(Quasiquote T)` strips its `Unquote` holes to the expression `E`, then reifies `(Quote E)` — `Quote` being a reifiable **quoting** function, so `E` reifies to an opaque `nat/` constant that mention-opacity holds apart from its referents' merges. Determinism is content-addressed for free: `E` *is* the content, so `nat/reify-or-mint-nat` dedups two firings on one binding to one constant (no rule digest / frontier is needed, unlike a skolem witness, which is anonymous). `Quasiquote` is an `unreifiable_function`, so an *open* template — the one that lives in a rule consequent until the antecedent binds its `Unquote` holes — stays structural and is never minted; range restriction (`rules/check-range-restricted`) already refuses a hole no antecedent binds, so an open template never reaches storage. It is a `quoting_function` too, so while it waits in the rule its `Unquote`-marked spellings are held opaque to an identity merge exactly as a `Quote` payload is. Turned on by declaration, like `reifiable_function` turns the reify pass on: a KB that has not declared `(quoting_function Quasiquote)` pays one taxonomy-prop read per firing/assert and the reducer is a no-op. And like reification, it is **declared before use**: opacity is applied when a mention is reified and again in the equality congruence, each gated on the mark being present then, so `ensure-quasiquote-functions` (or the four marks) must precede the constructions it governs and any identity merge over the referents inside them. A reify or merge processed while the mark is absent — before it is declared, or after it is retracted — is not held opaque and folds the mention onto its referent's class.
(any-quasiquote? kb)Gate: is quasiquotation enabled — (quoting_function Quasiquote) declared? False ⇒ the
reducer short-circuits, one prop read. Mirrors nat/any-reifiable-functions?.
Gate: is quasiquotation enabled — `(quoting_function Quasiquote)` declared? False ⇒ the reducer short-circuits, one prop read. Mirrors `nat/any-reifiable-functions?`.
(ensure-quasiquote-functions kb)Enable quasiquotation as a unit — declare the four marks it needs, each only if absent:
Quote reifiable + quoting (the constructed expression reifies to a mention constant) and
Quasiquote unreifiable + quoting (an open template stays structural and is a mention).
The last of them, (quoting_function Quasiquote), is the gate any-quasiquote? reads, so
this call is what turns the reducer on. Idempotent, asserted without chaining or settling
since it is pure metadata — the shape skolem/ensure-skolem-function uses.
Enable quasiquotation as a unit — declare the four marks it needs, each only if absent: `Quote` reifiable + quoting (the constructed expression reifies to a mention constant) and `Quasiquote` unreifiable + quoting (an open template stays structural and is a mention). The last of them, `(quoting_function Quasiquote)`, is the gate `any-quasiquote?` reads, so this call is what turns the reducer on. Idempotent, asserted without chaining or settling since it is pure metadata — the shape `skolem/ensure-skolem-function` uses.
(maybe-reduce kb sentence)Strip ground Quasiquotes to their (Quote E) mention form on the write and read
paths, and stop — the reify pass beside it (maybe-reify-nats on write, mints;
maybe-reify-for-read on read, dedups) reifies (Quote E), so the two spellings of one
construction meet at one constant. Structural: mints nothing itself. Gated — a no-op
unless quasiquotation is declared.
Strip ground `Quasiquote`s to their `(Quote E)` mention form on the write and read paths, and stop — the reify pass beside it (`maybe-reify-nats` on write, mints; `maybe-reify-for-read` on read, dedups) reifies `(Quote E)`, so the two spellings of one construction meet at one constant. Structural: mints nothing itself. Gated — a no-op unless quasiquotation is declared.
(prepare-goal-for-read kb goal context)Bring a prove / query / ask goal (a formula, or a vector of them = a conjunction)
into the form the stored content is in, so a lookup can meet it: reify ground
NATs to their existing constants, then rewrite terms to their equality-class
representatives and schematic normal forms (kb/rewrite-goal).
This is the parity every read path holds to, and the backward chainers need it as
much as the rest: without the rewrite step a goal naming a merged spelling — or one
an oriented equation would normalize — is answered by sentexes-matching/ask but
silently missed by prove/query, and the same knowledge answers path-dependently.
It is the top goal that is normalized, exactly as sentexes-matching/ask
normalize theirs; stored facts are already in normal form (migration), so subgoals a
rule expansion generates need no further rewriting — the same reliance ask makes.
rewrite-goal exempts
different, whose arguments must stay un-rewritten to read class membership, and the
congruence walk under it exempts a mention — a quoting_function's arguments, and the
proposition a modal_predicate attributes to its agent, which is normalized against the
agent's partition where the projection reads it rather than against the asker's
(docs/belief.md). Both exemptions hold on the stored side too, so the goal and the
sentex still meet at one form.
Rewritten by the merges context sees, since that is where the goal is asked. It lives
here, beside maybe-reduce, because it composes the two read-time reductions
(maybe-reduce and nat/maybe-reify-for-read) with the equality rewrite, and both
vaelii.core's read entry points and vaelii.impl.predall's audit prepare a goal the
same way through this one function.
Bring a `prove` / `query` / `ask` goal (a formula, or a vector of them = a conjunction) into the form the stored content is in, so a lookup can meet it: **reify** ground NATs to their existing constants, then **rewrite** terms to their equality-class representatives and schematic normal forms (`kb/rewrite-goal`). This is the parity every read path holds to, and the backward chainers need it as much as the rest: without the rewrite step a goal naming a merged spelling — or one an oriented equation would normalize — is answered by `sentexes-matching`/`ask` but silently missed by `prove`/`query`, and the same knowledge answers path-dependently. It is the **top** goal that is normalized, exactly as `sentexes-matching`/`ask` normalize theirs; stored facts are already in normal form (migration), so subgoals a rule expansion generates need no further rewriting — the same reliance `ask` makes. `rewrite-goal` exempts `different`, whose arguments must stay un-rewritten to read class membership, and the congruence walk under it exempts a **mention** — a `quoting_function`'s arguments, and the proposition a `modal_predicate` attributes to its agent, which is normalized against the *agent's* partition where the projection reads it rather than against the asker's (docs/belief.md). Both exemptions hold on the stored side too, so the goal and the sentex still meet at one form. Rewritten by the merges `context` sees, since that is where the goal is asked. It lives here, beside `maybe-reduce`, because it composes the two read-time reductions (`maybe-reduce` and `nat/maybe-reify-for-read`) with the equality rewrite, and both `vaelii.core`'s read entry points and `vaelii.impl.predall`'s audit prepare a goal the same way through this one function.
The reserved template-constructor functor, keyed on by name like skolem/SkolemFn.
The reserved template-constructor functor, keyed on by name like `skolem/SkolemFn`.
The reifiable quoting function a reduced template mentions its result through.
The reifiable quoting function a reduced template mentions its result through.
(reduce-in-conclusion kb raw)Reduce ground Quasiquotes in a fired conclusion, minting (Quote E) to its constant
— the chain path (chain/derive-conclusion) places its conclusion directly and does not
run the write reify pass, so it reifies here, beside skolemization. The mints run under
*defer-settle?* like a skolem's, so a mid-fixpoint construction does not settle belief.
Gated.
Reduce ground `Quasiquote`s in a fired conclusion, minting `(Quote E)` to its constant — the chain path (`chain/derive-conclusion`) places its conclusion directly and does not run the write reify pass, so it reifies here, beside skolemization. The mints run under `*defer-settle?*` like a skolem's, so a mid-fixpoint construction does not settle belief. Gated.
The reserved hole marker: (Unquote v) inside a template splices v into the
constructed expression. Meaningful only inside a Quasiquote body.
The reserved hole marker: `(Unquote v)` inside a template splices `v` into the constructed expression. Meaningful only inside a `Quasiquote` body.
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 |