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

Modules and packages

Structure

Modules take three forms, all equivalent at the symbol table:

  • A .ar file is implicitly a module named for its file stem.
  • A directory containing mod.ar is a module; sibling .ar files (and subdirectories containing mod.ar) are submodules of it.
  • An inline mod Name { … } declaration introduces a nested module in the current file.

A mod Name; declaration with no body has a single meaning — Rust’s child-module declaration: it asserts that a sibling Name.ar (or Name/mod.ar directory module) exists and attaches its contents under the current namespace as Name. A file does not rename itself: a content-carrying file whose mod Name; resolves to no sibling is refused with OE0715 (audit dc-06 retired the legacy “module-header” reading, where the first mod Name; of a file silently relabeled that file’s own declarations as module Name). To set a module’s name, use the file/directory layout — the project entry is module root, and any other .ar file is the module named for its stem; to declare a child, create the sibling Name.ar; to keep declarations where they are, omit the mod line. Explicit mod declarations are required; the compiler emits OW0710 when a sibling .ar file exists but no mod declaration references it.

Both project and package entry default to the root module file — preferring the Cargo-style src/root.ar, falling back to a flat root.ar at the package root. A prelude.ar is not an entry default: a package’s prelude is the manifest [package].prelude import model (the auto-imported use-tails of RFD 0038), and a prelude.ar file is an ordinary re-export module reached through the root — conventionally pub used at the root and imported by dependents via use pkg::prelude::*. The entry’s directory is the source root under which the package’s .ar files are indexed.

visibility ::= 'pub' | 'pub' '(' 'pkg' ')'
mod-decl   ::= 'mod' Ident ';'                                  // file-include
            |  'mod' Ident '{' mod-item* '}'                    // inline
            |  'mod' Ident '=' path '(' expr-list ')'           // functor alias (Functor modules)

Default visibility is module-private, following Rust: a default-visibility item is visible to the module that declares it and every descendant module. A private item declared at the package root is therefore visible package-wide (every module descends from the root); a private item in mod M is visible to M and M’s submodules, but not to the root or to sibling modules. This governs the privacy check only — name resolution is unchanged: a descendant still names an ancestor’s item through pkg::/super::/use (there is no bare-name inheritance from a parent module). pub exposes to dependents; pub(pkg) limits to the package.

Imports

use      ::= 'use' use-tree ';'
use-tree ::= path ('as' Ident)?
          |  path '::' '*'
          |  path '::' '{' use-tree (',' use-tree)* ','? '}'
path     ::= Ident ('::' Ident)*

Rust-style: single-symbol (use std::math::Nat;), brace-list (use std::math::{Nat, Int};), glob (use ufo_foundational::prelude::*; — a third-party vocabulary package), and aliased (use foo::bar::Sym as Other;) forms.

A plain use is a private import — visible only inside the importing module. A pub use re-exports: the imported items join this module’s public surface and are visible transitively to dependents, which is how a package prelude works (pub use pkg::prelude::*).

Import-resolution limits. Three forms parse but do not resolve: a single-item use M::X where X is re-exported by M rather than declared there (the glob re-export use M::* resolves it; the named form does not); pub use path as Alias (re-export with renaming); and a capitalized Self:: type path (lowercase self:: works). Import through the glob re-export or the original declaring path.

The prelude is a package feature, not a compiler default (RFD 0038). A package’s [package].prelude (an array of use-tails in ox.toml) is auto-prepended to every module of that package; it is empty by default and carries no vocabulary. type/rel are not in it unless the package opts them in (prelude = ["std::core::{type, rel}"], or prelude = ["pkg::prelude::*"] pointing at a prelude.ar of pub use re-exports). A module opts out with #![no_implicit_prelude]. There is no auto-imported std::prelude; what is always in scope is the language substrate (step 3 below), which is not a library prelude.

Manifest

ox.toml, Cargo-flavored:

[package]
name = "lease-story"
version = "0.1.0"
edition = 0
# Optional package entry override. Without this, the default search prefers the
# Cargo-style `src/root.ar` and falls back to the flat package root `root.ar`.
entry = "root.ar"

[dependencies]
# PATH dependencies (RFD 0030). The key is the path root the
# consumer uses (`use ufo::endurant::Object;`) and must equal the dependency
# package's `[package].name`.
ufo = { path = "../ufo" }

[lattice]
# Decidability-tier ceiling (Standpoints and modal operators). A declaration whose classified tier exceeds
# this ladder name is refused at `ox check` / `ox build` (OE1230, RFD 0030 D6).
max_tier = "recursive"

[standpoints]
# optional package-boundary declarations

[schema]
# Optional source root for generated or nested package layouts. Entry paths are
# resolved relative to this root when the nested entry exists.
root = "src"

Tooling resolves a package directory entry in this order: [project].entry, [project].main, [package].main, [package].entry, then the conventional defaults. With no explicit entry, the default search prefers the Cargo-style src/ layout and falls back to the flat package root (so existing packages keep resolving): both [project] and [package] try src/root.ar then root.ar. The first that exists wins, and its directory becomes the source root — a package laid out as src/root.ar roots all its .ar sources under src/ with no config (ox new/ox init scaffold exactly this). An explicit [schema].root overrides the source root. When no entry is found, the error names every path it searched.

Dependencies (RFD 0030). Only dep = { path = "…" } resolves: each path dependency’s package is loaded and its pub surface folded into the consumer’s workspace under the dependency name as a path root (see Name resolution). The registry/VCS surface — a bare version requirement (ufo = "1.0") or the version/git/branch/tag/rev/registry keys — is recognized and refused with OE1240 (Out of scope), never silently ignored. The dependency name must equal the dependency’s published [package].name (OE1241 otherwise); a dependency cycle is OE1242; the same name resolving to two different directories is OE1243. There is no ox.lock for a path-only graph (path deps are unlocked, Cargo precedent); ox.lock is reserved for the registry/git graph. Manifest honesty (RFD 0030 D6): an unrecognized section or key surfaces a Cargo-style OW1240 “unused manifest key” warning rather than being silently dropped, and [lattice].max_tier is enforced against the Standpoints and modal operators classifier (OE1230).

Name resolution

Resolution of a bare identifier proceeds in order:

  1. Local scope. Definitions in the current module, including the lexical chain of enclosing mod bodies and impl blocks.
  2. Imports + package prelude. Items brought into scope by use in the current module, and — unless #![no_implicit_prelude] is set — the package’s prelude ([package].prelude, auto-prepended uses; RFD 0038). The prelude is empty by default and carries no vocabulary.
  3. Substrate. The fixed, always-in-scope language primitives — not a library, and not opt-outable: the primordial types (Nat, Int, Real, Decimal, Money, Date, Time, DateTime, Duration, Bool, String, Top, Bot) and the builtin type forms (Option, Result, Ordering, List, Set, Map, Range, Truth4, Truth4Of, Diagnostic, Severity, …).

A qualified identifier (containing ::) is resolved by walking the path. The leading segment selects a root:

  • pkg — the current package’s root. This is the sole self-reference anchor: a package never refers to itself by its own name, so internal paths survive a package rename. pkg::a::b::X names item X in module a::b of this package. (Argon has packages, not crates — there is no crate keyword.)
  • self — the current module; super — the parent module (repeatable: super::super::X).
  • A dependency package name declared in [dependencies] — e.g. ufo::endurant::Object (a path-dependency vocabulary package, RFD 0030). The dependency’s pub surface is folded into this workspace under its name as a path root; ufo::X and use ufo::X; resolve into it. The stdlib root std is always available (std::math::Nat).
  • Otherwise the leading segment resolves against the scope chain — a submodule of the current module, or a name brought in by use.

Subsequent segments resolve within the preceding module’s namespace. An item therefore has a single absolute name viewed from outside the package (mypkg::a::b::X); viewed from inside, the equivalent absolute form is pkg::a::b::X.

Contextual introducer identifiers (type, or vocabulary names like kind, role, phase, …) are ordinary identifiers — recognized by an IDENT IDENT shape at declaration position and resolved via the algorithm above against the pub metatype (concepts) / pub metarel (relations) declarations visible in scope: declared in this package, or imported from a vocabulary package (across a [dependencies] path-dependency boundary, RFD 0030). Nothing is ambient here — not even type/rel: a package brings the no-commitment baseline into scope explicitly, via use std::core::{type, rel} or its [package].prelude (RFD 0038), exactly as it brings any vocabulary (appendix A). The compiler emits OE0101 UnresolvedName for general failures, and OE0605 UnknownMetatype / OE0606 UnknownMetarel specifically when a leading identifier at declaration position fails to resolve — at ox check and ox build; no artifact is emitted. A use statement that does not resolve is itself refused with OE0103 UnresolvedUseImport (with a did-you-mean over the visible namespace, RFD 0030 D5) — a broken import is never silently accepted.

Module extraction (tree-shaking)

When a module imports another, the elaborator extracts a ⊥-locality module (Cuenca-Grau–Horrocks–Kazakov–Sattler 2008): the smallest subset of the imported module’s axioms that stays non-trivial once every concept outside the used signature is reinterpreted as ⊥. Extraction is a fixpoint, linear-time per iteration, terminating in at most |B| iterations.

The guarantee is Σ-scoped conservativity: every entailment about the used signature survives extraction. Argon strengthens the classical result for its own semantics — closed-world conclusions are preserved (CWA-conservativity), ghost individuals reachable only through non-Σ concepts are pulled in (domain-conservative extraction), defeasible rules drag in their defeaters (defeat-aware extraction — a classical extractor is unsound under non-monotonic semantics, Bonatti-Faella-Petrova-Sauro 2022), and extraction composes safely across an import chain. All are mechanized at spec/lean/Argon/Locality/.

Extraction is how the substrate composes decidability tiers across heterogeneous modules (Tier ladder): each extracted module is classified independently, and conservativity guarantees no entailment is lost. Failures emit OE0710 (conservativity cannot be proven under the importer’s world assumption) or OE0711 (defeat-aware extraction cannot close the defeat graph).