rapx/verify/contract/
mod.rs

1//! Contract parsing, resolution, and rendering.
2//!
3//! Three front-ends (inline attributes, embedded JSON, and `pred!`-style
4//! compound-property macros, plus the pest DSL for expressions) all funnel into
5//! `Property::parse_list`, producing a single IR defined in [`types`].
6//!
7//! ## Layering
8//!
9//! Contracts go through two stages, each with its own type:
10//!
11//! ```text
12//! #[rapx::requires(...)] text        std-*.json            pred!(...) / def_property
13//!    └─ attr.rs ──▶ AttrProperty      └─ json.rs ──▶ JsonProperty   └─ compound.rs ──▶ CompoundSpec
14//!                      └────────────────── builder.rs ──────────────────▶ Property   (Atom | Or)
15//! ```
16//!
17//! Within the resolved IR, the naming follows granularity rather than stage:
18//! `Property*` names the formula level (`Property`, `PropertyKind`,
19//! `PropertyArg`), while `Contract*` names the expression sub-language that
20//! fills `PropertyArg::Expr` (`ContractPlace`, `ContractExpr`,
21//! `ContractProjection`).
22
23pub(crate) mod attr;
24pub(crate) mod builder;
25pub(crate) mod compound;
26pub(crate) mod json;
27pub(crate) mod pest_conv;
28pub(crate) mod pest_grammar;
29pub(crate) mod place;
30pub(crate) mod render;
31pub(crate) mod resolve;
32pub(crate) mod spec;
33pub(crate) mod types;
34
35pub(crate) use types::*;
rapx/verify/contract/mod.rs

rapx/verify/contract/
mod.rs
