assura_types/
lib.rs

1// TypeError is a diagnostic struct (only allocated on the error path) and
2// intentionally carries rich context. Suppressing because boxing 200+
3// return sites would add noise with no performance benefit.
4#![allow(clippy::result_large_err)]
5
6//! Type checking for the Assura contract language.
7//!
8//! Builds a `TypeEnv` (type environment) from a `ResolvedFile` by mapping
9//! each symbol in the symbol table to its `Type`. For T013 this creates the
10//! scaffolding: type environment construction and the `type_check` entry
11//! point. Actual expression-level type checking (T014-T018) builds on this.
12
13/// Structural checkers: linearity, typestate, effects, info-flow, generics, etc.
14///
15/// See `CHECKER-LAYERS.md` for how `checkers/`, `checks/`, and `domain/` differ.
16pub mod checkers;
17/// Wiring functions that run domain and structural checkers.
18mod checks;
19/// Clause-body type checking (requires/ensures/invariant expressions).
20pub mod clauses;
21/// Type conversion functions (AST TypeExpr, raw tokens -> Type).
22pub(crate) mod convert;
23/// Domain-specific checkers (memory, concurrency, security, formatting, etc.).
24pub mod domain;
25/// Type environment construction.
26pub(crate) mod env;
27/// Generic type instantiation and arity checking.
28pub(crate) mod generics;
29/// Ghost and lemma function effect checking.
30pub(crate) mod ghost_effects;
31/// Expression type inference (`infer_expr`).
32pub mod inference;
33/// Type checking pipeline entry points.
34mod pipeline;
35/// Core type definitions (Type, TypeEnv, TypeError, TypedFile).
36mod types;
37
38// ---- Re-exports: maintain the exact public API ----
39
40// From types module
41pub use types::{Type, TypeEnv, TypeError, TypedFile};
42
43// From checkers module
44pub use checkers::{FrameChecker, PendingDecreaseCheck, TaintLabel};
45
46// From domain module
47pub use domain::{GeneratedTest, TableSmtObligation, TestGenerator, TestKind, TestableContract};
48
49// From checks module (public API for pipeline)
50pub use checks::collect_table_smt_obligations;
51
52// Re-export checks/ helpers so domain/ can call them at crate scope.
53pub(crate) use checks::{
54    clauses_contract_fn, clauses_contract_fn_block, fn_or_contract_name_clauses,
55    runtime_decl_clauses_params,
56};
57
58// From convert module (pub(crate) items accessed within crate)
59pub(crate) use convert::parse_type_tokens;
60
61// From inference module
62pub(crate) use inference::*;
63
64// From generics module (only used in tests)
65#[cfg(test)]
66pub(crate) use generics::{check_generic_instantiation, instantiate_builtin_generic, substitute};
67
68// From ghost_effects module
69pub(crate) use ghost_effects::{check_ghost_fn_effects, check_lemma_fn_effects};
70
71// From pipeline module
72pub use pipeline::{TypeChecker, type_check};
73
74// Test-only re-exports: make checker types, domain types, and internal
75// functions visible to the tests/ module via `use super::*;`.
76#[cfg(test)]
77pub(crate) use checkers::*;
78#[cfg(test)]
79pub(crate) use checks::*;
80#[cfg(test)]
81pub(crate) use domain::*;
82
83#[cfg(test)]
84mod tests;
assura_types/lib.rs

assura_types/
lib.rs
