Appendix A — Keyword Reference
This appendix enumerates Argon’s keywords. The authoritative source is KEYWORD_TABLE in argon/oxc/src/syntax/kind.rs; everything below is derived from it.
Hard-reserved keywords
These tokens are reserved by the lexer. They cannot appear as plain identifiers anywhere in source. Twenty-seven entries:
enum rel let derive assert query match mod
use compute mutation if else hypothetical with extend
powertype compose not unsafe test fixture expect frame
using true false
A few notes:
frameandrelare hard-reserved as item declarators (frame Name { … },rel name(s, t) { … }). They also appear as values offor <kind>/decorator on <Target>clauses (for frame,on rel); the parser remaps the keyword token to an identifier in those positions.withandcomposeare hard-reserved even though they only appear in narrow contexts (with { … }insidehypothetical,compose <pat>inside structural patterns).powertypeis currently hard-reserved with aPowertypeDeclAST node and a parser test. The team is exploring a redesign that letspowertypebe modelled with the metatype mechanism + a user package; until that lands the keyword stays reserved (see Appendix D).
pub is not in KEYWORD_TABLE — it lexes as an identifier and the parser recognizes it in declaration-head position as the visibility prefix. Treat it as contextual.
Contextual keywords
These names lex as identifiers; their meaning is determined by parse position. Vocabulary packages are free to declare metatypes whose names collide with most of these (the parser disambiguates by context). The list is large; what follows groups them by where they appear.
Substrate-form heads
metaxis,metatype,metarel,decorator— declaration heads for the four substrate forms covered in Chapter 2.1.pub— visibility prefix (described above).
Metatype-keyword identifiers (defined by vocabulary packages, not the language)
These are not built-in. UFO’s prelude.ar declares them as pub metatypes:
kind subkind role phase category mixin rolemixin phasemixin relator
BFO’s prelude declares a different set (continuant, occurrent, independent_continuant, …). The token type is not reserved either — a vocabulary package may declare pub metatype type = { … } if it chooses.
for <kind> / decorator-on <Target> qualifiers
type rel dec field individual frame
rel and frame are hard-reserved tokens elsewhere; in this position the parser accepts them as kind / target identifiers.
Concept-decl clauses
where— refinement predicate clause.as— alias / rename binding.
Metaxis clauses
order condition
Metarel clauses
source target cardinality_default properties
Decorator clauses
on semantics lowers_to fragment
Powertype clauses
categorizes partitions
Mutation clauses (inside mutation Name { … })
require do retract emit return
do is the in-mutation block keyword; it is contextual, not hard-reserved.
Compute clauses (inside compute Name { … })
input out ensure body impl
Query clauses
group by order limit asc desc from to
Lifecycle clauses (inside lifecycle { … } blocks on a concept)
lifecycle phases transitions initial terminal on when brings_about
Diagram clauses (inside diagram "name" { … })
selection include exclude set show hide
style color label highlight group layer collapse
layout direction align ensure encourage
title description format size box diamond connected_by
Reasoning operators
forall exists is unknown ambiguous timeout
Allen-interval relations
The thirteen Allen relations are admitted as binary operators in rule bodies and queries:
before after meets met_by
overlaps overlapped_by starts started_by
during contains finishes finished_by
equals
Subtype-test predicates
specializes generalizes
(Trajectory: these may be renamed is_subtype / is_supertype — see Appendix D.)
Severity-constraint heads
strict error warning info
Used in the [pub] [strict] error|warning|info <Name>(<params>) :- <body> constraint form.
Compiler-built-in attributes
The parser admits attribute applications in two surface forms — #[…] (Rust-style, canonical for test-block annotations) and @[…] (alternate, canonical for rule / derive annotations). Both lower to the same AST shape. The list below is the COMPILER_BUILTIN_ATTRIBUTES set in argon/oxc/src/elaborate/validate.rs; everything else is dispatched through the user-declarable pub decorator registry and emits OE0229 UnknownDecorator if the name does not resolve.
Test-block proof status
#[unproven] #[assumed]
Both @[…] and bare @<name> / #<name> forms are accepted as alternates. Applied to a test block, they lower to CoreTest.proof_status.
Rule annotations
@[scope(N)] @[scope(max: N)]
@[budget(N)] @[budget(heartbeats: N)]
@[complexity(<class>)]
@[monotone]
@[cache]
@[scope(...)] bounds the Kodkod search space for tier:fol rules; @[budget(...)] caps heartbeats for full-FOL execution; @[monotone] asserts monotonicity (the elaborator verifies); @[complexity] is an optional explicit complexity-class annotation; @[cache] requests memoization.
Defeasibility / superiority
@[default] @[override(<rule>)] @[defeat(<rule>)] @[chain(<rule>)]
Used in defeasible-rule networks; see Chapter 5.2.
Theorem marker
@[theorem]
@[theorem] is dispatched through the user-decorator path. The vendored UFO package ships pub decorator theorem() on derive. Application is restricted to derive items; OW0821 fires on misuse.
Directives
Argon’s only top-level directive is #dec(<tier>):
#dec(structural) | #dec(closure) | #dec(expressive) | #dec(recursive)
#dec(fol) | #dec(modal) | #dec(mlt)
Both bare-name and tier:-prefixed forms (#dec(tier:closure)) are accepted. Scope: module-head, block, or per-declaration. The strictest tier on the ambient stack wins; rules whose effective tier exceeds the ambient ceiling produce OE0604 TierViolation. unsafe logic { … } injects whole-block tier:fol ambient — the FOL escape hatch.
Reserved alternates
<:is the canonical specialization operator. The Unicode⊑(U+2291) is accepted as a typeset alternate.- The legacy file extension
.olis accepted with anOW0813deprecation warning. Use.ar.