1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
//! AXON compiler frontend.
//!
//! Pure frontend of the AXON language: lexer, parser, AST, epistemic
//! type primitives, type checker, IR generator, and the top-level
//! compile-time checker that glues them together.
//!
//! # Design contract
//!
//! This crate has **zero runtime dependencies**. The only allowed
//! external dep is `serde` (plus its proc-macro chain). Any addition
//! of a runtime dep (tokio, axum, sqlx, reqwest, aws-*, jsonwebtoken,
//! …) is rejected at CI time.
//!
//! # Consumers
//!
//! - `axon` crate (the AXON runtime in `../axon-rs/`) re-exports these
//! modules so existing callers keep working.
//! - `axon-lsp` (Language Server, separate repo) consumes the frontend
//! directly without dragging runtime deps.
//!
//! # Byte-identical parity
//!
//! Outputs must match the Python reference implementation
//! (`../axon/`) on the golden-file test corpus. Divergences are
//! release blockers.
// §Fase 11.a — compile-time catalogs used by the type checker.
// `refinement` declares the closed Trust<T> catalog; `stream_effect`
// declares the closed backpressure policy catalog. Both are pure
// enum-like definitions with `std::fmt` only — no runtime deps.
// The matching runtime implementations (`trust_verifiers`,
// `stream_runtime`) live in the `axon` runtime crate.
// §Fase 11.c — closed catalogue of regulatory authorisations
// (GDPR/CCPA/SOX/HIPAA/GLBA/PCI-DSS) used by the type checker to
// enforce `@legal_basis` annotations. Pure catalog, no runtime deps.
// §Fase 11.e — OTS (Ontological Tool Synthesis) compile-time slug
// catalogs. Runtime pipeline execution lives in `axon::ots` and
// re-exports these for backward compatibility.
// §Fase 13.g — LSP-facing analysis primitives for typed channels.
// Pure AST helpers consumed by `axon-lsp` (sibling repo) to implement
// hover, completion, go-to-definition and find-references. Zero
// runtime deps — stays inside the Fase 12.c contract.
// §Fase 41.a — session types: the pure algebra of typed bidirectional
// dialogue (WebSocket as a cognitive primitive). The session-type
// grammar + the duality involution `(·)⊥` + regular-coinductive
// equality for `μ`-types + the connection law (`peer ≡ self⊥`).
// Grounded in Caires–Pfenning (session types = intuitionistic linear
// propositions). Pure — no runtime deps; the `socket` surface (41.b),
// credit-refined backpressure (41.c) and the typed-WS runtime (41.d,
// in the `axon` crate) build on this. See
// docs/paper_websocket_cognitive_primitive.md.
// §Fase 41.h — multiparty session types (Honda–Yoshida–Carbone). A
// `GlobalType` declares an n-party protocol; projection `G⌐r` extracts
// each role's binary `SessionType` (the §41.a algebra). The safe-
// realizability gate is `project_all`: a `Result::Ok` is the structural
// certificate that independent per-role runtimes faithfully realise `G`.
// §Fase 6.a — the closed registry of every primitive AXON exposes as
// a named language construct. Single source of truth for the ℰMCP
// coverage gate + scaffold CLI + future LSP completions / docs-site
// generators. Pure const data, no runtime deps. See the module-level
// docs for the discipline (registry + corpus = atomic addition).
pub use ;