Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Macro atom

The macro atom is the fifth substrate atom (meta-calculus, constructs, rule, trait, macro) and the extensibility layer the ontology-neutral doctrine depends on: it is how a vocabulary library grows the surface without a compiler change. Its design is settled by RFD 0037; this chapter is the surface specification.

The declarative expansion engine — pub macro declarations expand at EXPAND (hygiene, repetition, attribute/decl-position invocation, cross-module imports), and their output re-elaborates through the ordinary path to events. The procedural layer (#[procmacro] pub fn, Procedural macros) provides concat_idents, quote/${} antiquotation, decl-reflection, and a total non-recursive body — the mechanism that re-homes #[irreflexive]/#[asymmetric] from compiler builtins to library procedural macros. #[functional] is a builtin-backed macro (Migration: re-homing the hard-coded surface).

The shape of the design. A macro expands to surface syntax, which is re-parsed and re-elaborated through the one existing path to events — never to events directly. Expansion is a phase between parse and resolve, run to a fixed point; the resolver, type checker, Name resolution ontology-neutrality gate, and decidability-tier classifier all run on the post-expansion program, so a macro is invisible to none of them. The declarative layer (pub macro, pattern→template) is the foundation; the procedural layer (#[procmacro], computation over reflected syntax) is layered on top (Procedural macros).

Declarative macros

macro-decl    ::= attribute* 'pub'? 'macro' Ident '{' macro-rule (';' macro-rule)* ';'? '}'
macro-rule    ::= '(' macro-pattern ')' '=>' '{' template '}'
macro-pattern ::= /* token tree with $name:SPEC metavariables and $(...)* / $(...)+ / $(...)? repetitions */

A declarative macro is a sequence of (pattern) => { template } rules. A pattern matches a token tree; metavariables are tagged with a fragment specifier that fixes the syntactic category matched and the binding space the bound name lives in. The template is surface syntax, with metavariable substitution and $( … )*/+/? repetitions (optional separator: $( … ),*).

pub macro vec {
    () => { Vec::empty() };
    ($head:expr $(, $tail:expr)*) => { /* … */ };
}

let xs = vec!(1, 2, 3);

Fragment specifiers. The syntactic categories $x:expr, $t:ty, $i:ident, pat, stmt, block, item, literal, path, tt; plus four Argon-specific specifiers, each a binding-space-targeted parse — $c:concept parses a concept-introducing declaration and binds in the concept space, $r:rel a relation declaration (rel space), $m:metatype a metatype introducer, and $u:rule a rule-body atom (carrying its own rule-variable sub-bindings). The set is closed; a standpoint specifier and a user-extensible registry are out of scope (Out of scope). Because a concept/metatype specifier only binds — the Name resolution gate runs later, at resolution (Hygiene) — and no specifier carries a tier, ontology-neutrality and tier-honesty hold by construction.

The expansion model

Expansion is a distinct compilation phase:

lex → parse → expand* → resolve → check → instantiate (lower to events) → tier-classify → discharge
  • Expand to surface, re-elaborate. A macro produces surface syntax that is spliced into the module and re-parsed; it then flows through the same resolve → check → lower path as hand-written source. The content-addressed AxiomKind event wire is produced only by the unchanged lowering, so a macro inherits the substrate’s identity and drift guarantees for free. A macro never emits events directly.
  • Fixed point. A macro whose output contains further invocations re-expands until none remain, bounded by a fuel cap that errors on exhaustion.
  • Emit into the invocation module. A macro expands at its use site and its output lands in the invoking module, where rules it emits compose with the user’s by the same-module same-head union (derive). It cannot contribute to another module’s heads.
  • Classifier-last gives tier-honesty. The decidability-tier classifier runs after expansion on the lowered events, so the program lands on its true tier — a macro that emits a recursive rule is classified exactly as if the rule were hand-written, and cannot smuggle the program across a tier boundary.
  • Determinism. The declarative layer is strongly normalizing by construction, has no I/O, and emits collections in a canonical order. Rule variables are alpha-canonicalized at lowering (Hygiene), so a macro’s choice of fresh variable names never affects the .oxbin content hash. Expansion is therefore a deterministic function of its input, and reproducible builds need no author discipline.

Hygiene

Macro-introduced binders neither capture nor are captured by names at the use site, across all of Argon’s binder namespaces (rule variables, concept/type, rel/metarel, metatype/metaxis + axis values, individuals, trait members). The model is scope-sets with binding spaces (Flatt 2016 + Racket binding spaces): each namespace is an interned scope inside one scope-set, resolved by the unchanged maximal-subset rule. Hygiene is white-box — the quotation applies a fresh macro scope to the identifiers a macro introduces.

The Name resolution ontology-neutrality gate composes as a commuting pass: scope-set resolution (syntactic) produces a candidate binding, then the gate (semantic) checks that a macro-introduced concept resolves to a visible pub metatype — it may reject, but never re-points a reference. Macro-introduced vocabulary is not exempt from the gate.

Two regimes follow from what reaches event identity:

  • Rule variables are clause-local and alpha-canonicalized at lowering, so hygiene need only guarantee non-capture; their names are irrelevant to identity.
  • Introduced vocabulary (a concept/relation a macro declares) has a semantic, referenceable name, so hygiene gives it a content-derived, stable identity.

Macros are hygienic-only: there is no unhygienic!. A $crate-style self-reference plus syntax-parameter keywords cover the real needs; any future raw escape must name the binding space it breaks into.

Imports and the shared #[…] namespace

A pub macro foo { … } declaration occupies a single symbol in the module namespace. use mod::foo; brings it into scope; foo!(args) invokes it at expression position and #[foo(args)] at declaration position. The ! and #[…] sigils are invocation markers, not separate-namespace tags — there is no distinct macro namespace, and no #[macro_use] form; macro imports follow ordinary item-import rules (Imports).

User macros and compiler-known directives share the #[…] namespace. Resolution is by uniqueness at registration: a name resolves to exactly one implementation, and a user macro colliding with a built-in directive is an OE0705-class error, never a silent shadow (matching the loud-refusal discipline of the directive registry, Directive surface and the MLT decorator path). Identity is keyed to a stable handle, not the spelling, so re-homing a directive (Migration: re-homing the hard-coded surface) does not change how a #[name] resolves.

Procedural macros

A procedural macro computes its expansion by running code, rather than rewriting a pattern into a template. It is not a fn over a TokenStream: the procedural layer is a total, structurally-recursive meta-language over reflected syntax, not general-purpose computation. Totality is what the substrate’s own doctrine requires — it is strongly normalizing and deterministic by construction, and (being a total function over an inductive syntax type) mechanizable in Lean (Lean correspondence).

A procedural macro is a #[procmacro] pub fn in the one macro namespace:

#[procmacro]
pub fn irreflexive(item: Decl) -> Syntax {
    let head = concat_idents("__", item.name, "_irreflexive");
    quote {
        $item;
        pub check $head(x: $item.params[0].ty) :- $item.name(x, x)
          => Diagnostic { severity: Severity::Error, code: "Argon::OE1359",
               message: "relation `${item.name}` is #[irreflexive] but relates an element to itself" };
    }
}

The body is a total, non-recursive fragment: let bindings over the construction builtins and reflection projections, then a trailing quote. The surface is:

  • quote { … } — a QUOTE_EXPR; its body is re-parsed through the ordinary elaboration path (never emitted as events directly). Splices: $name (a let-bound value), $item (the whole reflected declaration, re-emitted verbatim), $item.name (the relation’s name), $item.params[i].ty (a parameter’s type).
  • ${expr} antiquotation — an in-string splice (e.g. inside a diagnostic message:), resolved by the macro renderer at EXPAND. It is render-time, not runtime string concatenation (the runtime has no Text + Text — that is a separate arc).
  • concat_idents(a, b, …) (paste) — builds a raw definition-site identifier from pieces; the single capability the splice-only declarative layer lacks. The result is not freshened — the macro intends it as the stable public head (__{rel}_{prop}); splices are substitution barriers carrying their own use-site identity.

Bodies are non-recursive (trivially total). #[procmacro] resolves as a macro (DefKind::Macro), runs at EXPAND by a dedicated evaluator, and its #[procmacro] directive executes at fn-decl position. #[irreflexive] and #[asymmetric] (Migration: re-homing the hard-coded surface) are genuine procedural macros written exactly this way.

Full structural recursion over reflected Syntax — a totality checker, a derive-class macro inspecting a concept’s fields, #[functional]’s rel-cardinality-cap arm (which re-emits a rel with a modified cardinality bracket), and the classify ∘ expand tier-honesty theorem — is out of scope (Out of scope).

Directive surface and the MLT decorator path

Every #[…] attribute must resolve to a registered compiler directive or an in-scope pub macro (e.g. #[transitive], re-homed to std::rel, Migration: re-homing the hard-coded surface / RFD 0037 D8 — brought in by use). The directive registry (oxc-instantiate’s DIRECTIVE_REGISTRY) is the single declarative table of every directive the toolchain reads or reserves, with its argument shape, valid positions, and status. There are no silently-ignored attributes: an attribute that is neither a registered directive nor an in-scope macro refuses with OE0705 UnknownDirective (nearest-known suggestion), documented-but-unbuilt directives with OE0706 DirectiveReservedUnimplemented, misplaced directives with OE0707 DirectiveInvalidPosition, argument forms on bare-form directives with OE0709 AttributeArgsNotYetImplemented, and conflicting families with OE0714 DirectiveConflict.

The relation-property directives are library macros, split by mechanism (Migration: re-homing the hard-coded surface):

  • Relation-property directives (RFD 0031) — #[transitive] is a declarative pub macro in std::rel (closure derive R(x, z) :- R(x, y), R(y, z) into the relation’s own head); #[irreflexive]/#[asymmetric] are genuine procedural macros (#[procmacro], RFD 0040) that re-emit the decorated declaration and paste a __{rel}_{prop} check head via concat_idents (Procedural macros); #[functional] is a builtin-backed macro (#[builtin] pub macro, the #[rustc_builtin_macro] analogue, OE1362 if unimported), since its rel-cardinality-cap [0..1] arm requires structural re-emission. The declarative and procedural forms format Argon source and re-parse it through the ordinary derive/check pipeline; #[functional]’s privileged path synthesizes the guard (and the cap) directly.
  • MLT decorators — #[categorizes(T)], #[partitions(T)], #[subordinate_to(M)], #[power_type_of(T)], and #[order(N)] are no longer compiler directives at all. They are genuine library #[procmacro]s in the unprivileged mlt package (not std): each re-emits the decorated declaration and emits a MetaProperty on the metarel (or, for #[order], the metaxis) it shares its name with — reading the argument’s name (or, for #[order], an integer), not its structure. Nothing is ambient: a consumer lists mlt in ox.toml and imports the vocabulary (use mlt::*; / use mlt::{categorizes};), and an unimported decorator is an unknown attribute macro, refused by the no-silent-attribute gate (OE0705). The emitted MetaProperty is re-checked at the emission boundary and again at load — #[order]’s value is validated against the mlt::order metaxis’s declared Nat where { _ <= 16 } domain by the self-validating .oxbin load re-check (OE0623), so the bound holds without any compiler privilege. The reasoner-side enforcement of the MLT closure rules over the emitted metaproperties is authored as the mlt package’s own rules/checks over the neutral substrate (Phase 2).

Directives as library macros

The hard-coded directive surface is library macros, with the user-facing syntax byte-identical to a privileged-path synthesis (RFD 0009 RP-003 GAP-3). The mechanism is decided by the directive’s emit target:

  • Relation-property emits ordinary rules (which have surface), so it lives in std::rel, split by what each member needs:
    • #[transitive] is a declarative pub macro: the macro template produces lowered events byte-identical to a direct synthesis (verified differentially).
    • #[irreflexive] / #[asymmetric] are genuine procedural macros (#[procmacro] pub fn … -> Syntax, RFD 0040): each re-emits the decorated declaration ($item) and pastes a pub check whose head is concat_idents("__", item.name, "_{prop}") — the unique ident the splice-only declarative layer cannot build. Their import gate is OE0705 (a bare unimported #[irreflexive] is an unknown attribute macro, like transitive).
    • #[functional] is a #[builtin] macro (importable from std::rel, OE1362 if not), with privileged synthesis as the implementation. It is one attribute covering both a metarel-check (paste-able) and a rel-cardinality-cap [0..1] on the target endpoint — and the cap arm re-emits a rel with a modified cardinality bracket, i.e. structural re-emission. An attribute name is builtin or procmacro, not split across both halves, so functional is entirely builtin.
  • MLT emits MetaProperty events. Its surface is the unprivileged mlt package (RFD 0043): every decorator — the relational #[categorizes]/#[partitions]/#[subordinate_to]/#[power_type_of] and the metaxis-valued #[order(N)] — is a genuine #[procmacro] emitting a re-checked MetaProperty through the emission boundary (Procedural macros). There is no compiler builtin, no std::mlt, and no reserved MLT diagnostic code; the expander is the package’s own procmacro, not a privileged compiler path. MLT is one higher-order type theory among several (potency, ML2, powertype), so the substrate stays neutral about which one a model commits to.
  • std::temporal / std::lifecycle become declarative library macros; whether each operator ships native or library is a scoping choice once the engine exists.
// std/temporal.ar — a declarative desugaring to rule-body atoms (no computation)
pub macro since {
    ( $lhs:rule since [ $lo:literal , $hi:literal ] $rhs:rule ) => {
        @meta_window($t, $lo, $hi), $rhs at $t, holds_throughout($lhs, $t, now)
    };
}

Lean correspondence

The substrate at spec/lean/Argon/Substrate/Macro.lean mechanizes the shape of macro declarations — MacroAtom = declarative MacroDecl | procedural ProcMacroDecl as @[language_interface] carriers policed by the drift gate. Per RFD 0037 D7, the substrate boundary is held at the typed AST: macro expansion is untrusted and Rust-side, and assurance comes from re-checking its output — the tier classifier runs last, the content hash is re-derivable, and the drift gate covers the MacroAtom shape. Mechanize the re-checker, not the producer.

The tier-honesty theorem — that classify ∘ expand lands a program on the same decidability class as its expansion — is statable only once expand is a total Lean object over an inductive Syntax type (RFD 0040 D7). The scope-set hygiene algebra and a full expansion-preservation theorem are out of scope.

The MLT-relational kinds — instanceOf, specializes, categorizes, partitions, subordinates — live in spec/lean/Argon/MetaCalculus/MLTKinds.lean, with the round-trip theorem classify_declOfKind; the elaborator emits canonical metarel_decl events via declOfKind.