pub enum TokenType {
Show 233 variants
BlockHeader {
block_type: BlockType,
},
All,
No,
Some,
Any,
Both,
Most,
Few,
Many,
Cardinal(u32),
AtLeast(u32),
AtMost(u32),
Anything,
Anyone,
Nothing,
Nobody,
NoOne,
Nowhere,
Ever,
Never,
And,
Or,
If,
Then,
Not,
Iff,
Because,
Although,
Until,
Release,
WeakUntil,
Implies,
Must,
Shall,
Should,
Can,
May,
Cannot,
Would,
Could,
Might,
Had,
Let,
Set,
Return,
Break,
Be,
While,
Repeat,
For,
In,
From,
Assert,
Trust,
Require,
Requires,
Ensures,
Otherwise,
Else,
Elif,
Call,
New,
Either,
Inspect,
Native,
Escape,
EscapeBlock(Symbol),
Given,
Prove,
Auto,
Read,
Write,
Console,
File,
Give,
Show,
Push,
Pop,
Copy,
Through,
Length,
At,
Add,
Remove,
Contains,
Union,
Intersection,
Inside,
Zone,
Called,
Size,
Mapped,
Attempt,
Following,
Simultaneously,
Spawn,
Send,
Await,
Portable,
Manifest,
Chunk,
Shared,
Merge,
Increase,
Decrease,
Tally,
SharedSet,
SharedSequence,
CollaborativeSequence,
SharedMap,
Divergent,
Append,
Resolve,
RemoveWins,
AddWins,
YATA,
Values,
Check,
Listen,
NetConnect,
Sleep,
Sync,
Mount,
Persistent,
Combined,
Followed,
Launch,
Task,
Pipe,
Receive,
Stop,
Try,
Into,
First,
After,
Colon,
Indent,
Dedent,
Newline,
Noun(Symbol),
Adjective(Symbol),
NonIntersectiveAdjective(Symbol),
Adverb(Symbol),
ScopalAdverb(Symbol),
TemporalAdverb(Symbol),
Verb {
lemma: Symbol,
time: Time,
aspect: Aspect,
class: VerbClass,
},
ProperName(Symbol),
Ambiguous {
primary: Box<TokenType>,
alternatives: Vec<TokenType>,
},
Performative(Symbol),
Exclamation,
Article(Definiteness),
Auxiliary(Time),
Is,
Are,
Was,
Were,
That,
Who,
What,
Where,
Whose,
When,
Why,
Does,
Do,
Identity,
Equals,
Reflexive,
Reciprocal,
Respectively,
Pronoun {
gender: Gender,
number: Number,
case: Case,
},
Preposition(Symbol),
Particle(Symbol),
Comparative(Symbol),
Superlative(Symbol),
Than,
To,
PresupTrigger(PresupKind),
Focus(FocusKind),
Measure(MeasureKind),
Number(Symbol),
MoneyLiteral {
amount: Symbol,
currency: Symbol,
},
DurationLiteral {
nanos: i64,
original_unit: Symbol,
},
DateLiteral {
days: i32,
},
TimeLiteral {
nanos_from_midnight: i64,
},
CalendarUnit(CalendarUnit),
Ago,
Hence,
Before,
StringLiteral(Symbol),
InterpolatedString(Symbol),
CharLiteral(Symbol),
Item,
Items,
Possessive,
LParen,
RParen,
LBracket,
RBracket,
LBrace,
Amp,
VBar,
Tilde,
Caret,
RBrace,
Comma,
Period,
Dot,
Xor,
Shifted,
Plus,
Minus,
Star,
Slash,
Percent,
PlusEq,
MinusEq,
StarEq,
SlashEq,
PercentEq,
StarStar,
SlashSlash,
Lt,
Gt,
LtEq,
GtEq,
EqEq,
NotEq,
Arrow,
Assign,
Mut,
Identifier,
EOF,
}Variants§
BlockHeader
All
No
Some
Any
Both
Most
Few
Many
Cardinal(u32)
AtLeast(u32)
AtMost(u32)
Anything
Anyone
Nothing
Nobody
NoOne
Nowhere
Ever
Never
And
Or
If
Then
Not
Iff
Because
Although
Concessive subordinator: “although”/“though”/“even though”.
Until
Temporal binary connective: “P until Q”
Release
Temporal binary connective: “P release Q” (dual of Until)
WeakUntil
Temporal binary connective: “P weak-until Q” (Until or Always)
Implies
Compiler-generated implication (e.g., quantifier restrictions from Kripke lowering).
Distinguished from If which represents user-written conditionals.
This separation gives downstream passes (KG extraction, SVA synthesis)
irrefutable provenance: If = user intent, Implies = compiler glue.
Must
Shall
Should
Can
May
Cannot
Would
Could
Might
Had
Let
Set
Return
Break
Exits the innermost while loop: Break.
Be
While
Repeat
For
In
From
Assert
Trust
Documented assertion with justification string.
Require
Enforced runtime invariant: Require that <cond>. → a hard assert!
(survives release, unlike Assert → debug_assert!).
Requires
Function precondition clause: Requires <check>. (checked at entry).
Ensures
Function postcondition clause: Ensures <check>. (checked before return).
Otherwise
Else
Alias for Otherwise - Pythonic else clause
Elif
Python-style else-if shorthand
Call
New
Constructor keyword for struct instantiation.
Either
Sum type definition keyword.
Inspect
Pattern matching statement keyword.
Native
Native function modifier for FFI bindings.
Escape
Escape hatch header keyword: “Escape to Rust:”
EscapeBlock(Symbol)
Raw code block captured verbatim from an escape hatch body. The Symbol holds the interned raw foreign code (indentation-stripped).
Given
Premise marker in theorem blocks.
Prove
Goal marker in theorem blocks.
Auto
Automatic proof strategy directive.
Read
“Read input from…”
Write
“Write x to file…”
Console
“…from the console”
File
“…from file…” or “…to file…”
Give
Move ownership: “Give x to processor”
Show
Immutable borrow: “Show x to console”
Push
“Push x to items”
Pop
“Pop from items”
Copy
“copy of slice” → slice.to_vec()
Through
“items 1 through 3” → inclusive slice
Length
“length of items” → items.len()
At
“items at i” → items[i]
Add
“Add x to set” (insert)
Remove
“Remove x from set”
Contains
“set contains x”
Union
“a union b”
Intersection
“a intersection b”
Inside
“Inside a new zone…”
Zone
“…zone called…”
Called
“…called ‘Scratch’”
Size
“…of size 1 MB”
Mapped
“…mapped from ‘file.bin’”
Attempt
“Attempt all of the following:” → concurrent (async, I/O-bound)
Following
“the following”
Simultaneously
“Simultaneously:” → parallel (CPU-bound)
Spawn
“Spawn a Worker called ‘w1’” → create agent
Send
“Send Ping to ‘agent’” → send message to agent
Await
“Await response from ‘agent’ into result” → receive message
Portable
“A Message is Portable and has:” → serde derives
Manifest
“the manifest of Zone” → FileSipper manifest
Chunk
“the chunk at N in Zone” → FileSipper chunk
“A Counter is Shared and has:” → CRDT struct
Merge
“Merge remote into local” → CRDT merge
Increase
“Increase x’s count by 10” → GCounter increment
Decrease
“Decrease x’s count by 5” → PNCounter decrement
Tally
“which is a Tally” → PNCounter type
“which is a SharedSet of T” → ORSet type
“which is a SharedSequence of T” → RGA type
CollaborativeSequence
“which is a CollaborativeSequence of T” → YATA type
“which is a SharedMap from K to V” → ORMap type
Divergent
“which is a Divergent T” → MVRegister type
Append
“Append x to seq” → RGA append
Resolve
“Resolve x to value” → MVRegister resolve
RemoveWins
“(RemoveWins)” → ORSet bias
AddWins
“(AddWins)” → ORSet bias (default)
YATA
“(YATA)” → Sequence algorithm
Values
“x’s values” → MVRegister values accessor
Check
“Check that user is admin” → mandatory runtime guard
Listen
“Listen on [addr]” → bind to network address
NetConnect
“Connect to [addr]” → dial a peer (NetConnect to avoid conflict)
Sleep
“Sleep N.” → pause execution for N milliseconds
Sync
“Sync x on ‘topic’” → automatic CRDT replication
Mount
“Mount x at [path]” → load/create persistent CRDT from journal
Persistent
“Persistent Counter” → type wrapped with journaling
Combined
“x combined with y” → string concatenation
Followed
“a followed by b” → sequence concatenation (merge two sequences into one)
Launch
“Launch a task to…” → spawn green thread
Task
“a task” → identifier for task context
Pipe
“Pipe of Type” → channel creation
Receive
“Receive from pipe” → recv from channel
Stop
“Stop handle” → abort task
Try
“Try to send/receive” → non-blocking variant
Into
“Send value into pipe” → channel send
First
“Await the first of:” → select statement
After
“After N seconds:” → timeout branch
Colon
Indent
Dedent
Newline
Noun(Symbol)
Adjective(Symbol)
NonIntersectiveAdjective(Symbol)
Adverb(Symbol)
ScopalAdverb(Symbol)
TemporalAdverb(Symbol)
Verb
ProperName(Symbol)
Ambiguous
Lexically ambiguous token (e.g., “fish” as noun or verb).
The parser tries the primary interpretation first, then alternatives if parsing fails. Used for parse forest generation.
Performative(Symbol)
Exclamation
Article(Definiteness)
Auxiliary(Time)
Is
Are
Was
Were
That
Who
What
Where
Whose
When
Why
Does
Do
Identity
Equals
Reflexive
Reciprocal
Respectively
Pairwise list coordination: “A and B respectively love C and D”
Pronoun
Preposition(Symbol)
Particle(Symbol)
Comparative(Symbol)
Superlative(Symbol)
Than
To
PresupTrigger(PresupKind)
Focus(FocusKind)
Measure(MeasureKind)
Number(Symbol)
MoneyLiteral
Currency-symbol money literal: $19.99, €5, £10, ¥100. Carries the magnitude (digits +
optional decimal point, thousands separators stripped) and the resolved ISO-4217 code, so a
money-aware parser builds money(..) while a magnitude-only consumer can still read amount.
DurationLiteral
Duration literal with SI suffix: 500ms, 2s, 50ns Stores the value normalized to nanoseconds and preserves the original unit.
DateLiteral
Date literal in ISO-8601 format: 2026-05-20 Stores days since Unix epoch (1970-01-01).
TimeLiteral
Time-of-day literal: 4pm, 9:30am, noon, midnight Stores nanoseconds from midnight (00:00:00).
CalendarUnit(CalendarUnit)
Calendar time unit word: day, week, month, year (or plurals) Used in Span expressions like “3 days” or “2 months and 5 days”
Ago
Postfix operator for relative past time: “3 days ago”
Hence
Postfix operator for relative future time: “3 days hence”
Before
Binary operator for span subtraction from a date: “3 days before 2026-05-20”
StringLiteral(Symbol)
String literal: "hello world"
InterpolatedString(Symbol)
Interpolated string literal: "Hello, {name}!"
Contains raw content with {} holes preserved
CharLiteral(Symbol)
Item
Items
Possessive
LParen
RParen
LBracket
RBracket
LBrace
{ — map/set literal opener ({k: v}, {a, b}). Interpolation braces
never reach here (they are consumed inside the string-literal path).
Amp
& in IMPERATIVE code — bitwise AND on Int, intersection on Sets.
In prose the same character stays the coordination/firm-name joiner.
VBar
| in imperative code — bitwise OR on Int, union on Sets. (Pipe
is taken by the channel keyword Pipe of T.)
Tilde
~ in imperative code — bitwise complement (lowers to x ^ -1).
Caret
^ in imperative code — bitwise XOR on Int, symmetric difference on
Sets (the word xor remains the English spelling).
RBrace
} — map/set literal closer.
Comma
Period
Dot
. as the FIELD-ACCESS / UFCS-method operator (imperative only): p.x
(≡ p's x) and xs.f(a) (≡ f(xs, a)). Distinguished from a sentence
Period in the lexer by the no-whitespace + identifier-on-both-sides rule.
Xor
“x xor y” → bitwise XOR (^)
Shifted
“x shifted left/right by y” → bit shift (<</>>)
Plus
Minus
Star
Slash
Percent
PlusEq
Compound assignment operators — x += e desugars to Set x to x <op> e.
MinusEq
StarEq
SlashEq
PercentEq
StarStar
** — the exponentiation operator.
SlashSlash
// — floor division (rounds toward negative infinity).
Lt
<
Gt
>
LtEq
<=
GtEq
>=
EqEq
==
NotEq
!=
Arrow
Arrow for return type syntax: ->
Assign
Assignment operator = for identifier = value syntax
Mut
Mutability keyword mut for explicit mutable declarations
Identifier
Generic identifier (for equals-style assignment)