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 unreifiableFunction, 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 quotingFunction
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 reifiableFunction turns the reify pass on: a KB that has
not declared (quotingFunction 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 `unreifiableFunction`, 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 `quotingFunction` 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 `reifiableFunction` turns the reify pass on: a KB that has not declared `(quotingFunction 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 — (quotingFunction Quasiquote) declared? False ⇒ the
reducer short-circuits, one prop read. Mirrors nat/any-reifiable-functions?.
Gate: is quasiquotation enabled — `(quotingFunction 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, (quotingFunction 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, `(quotingFunction 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.
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 |