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
//! Contract parsing, resolution, and rendering.
//!
//! Three front-ends — inline attributes, embedded JSON, and `pred!`-style
//! compound-property macros — funnel into `Property::parse_list`, producing a
//! single IR defined in [`types`]; the three share the pest DSL for expressions.
//!
//! ## Layering
//!
//! Contracts go through two stages, each with its own type:
//!
//! ```text
//! #[rapx::requires(...)] text std-*.json pred!(...) / def_property
//! └─ attr.rs ──▶ AttrProperty └─ json.rs ──▶ JsonProperty └─ compound.rs ──▶ CompoundSpec
//! └────────────────── builder.rs ──────────────────▶ Property (Atom | Or)
//! ```
//!
//! Compound tags are the exception: `parse_list` dispatches them to
//! `compound::expand_compound`, which expands `CompoundSpec` into `Property`
//! directly (builder never sees the `CompoundSpec`).
//!
//! Within the resolved IR, the naming follows granularity rather than stage:
//! `Property*` names the formula level (`Property`, `PropertyKind`,
//! `PropertyArg`), while `Contract*` names the expression sub-language that
//! fills `PropertyArg::Expr` (`ContractPlace`, `ContractExpr`,
//! `ContractProjection`).
pub
pub
pub
pub
pub
pub
pub
pub
pub
pub
pub use *;