xpile_contract_backend/
lib.rs

1//! ContractBackend trait — proof-lane rendering abstraction.
2//!
3//! Renders parsed [`xpile_contracts::Contract`] into LaTeX (math +
4//! theorem environments), Lean 4 theorem text (with `@[xpile_contract]`
5//! attribute carrying the verbatim contract ID), or mdBook.
6//!
7//! Architectural invariants codified in
8//! `contracts/xpile-contract-backend-trait-v1.yaml`. The citation bridge
9//! uses **format-native structured constructs** parseable by the host
10//! elaborator/parser, NOT regex over body text. See
11//! `docs/specifications/sub/contract-backend-trait.md` §"Citation bridge".
12
13use serde::{Deserialize, Serialize};
14use xpile_contracts::{Contract, ContractFormat, ContractId};
15
16/// Configuration passed to [`ContractBackend::render`].
17#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
18pub struct ContractRenderConfig {
19    pub format: ContractFormat,
20    /// When true, the citation ID is emitted textually (in addition to
21    /// `RenderedDoc.citations`) via the format's structured construct:
22    /// `\xpileContract{}{}` (LaTeX), `@[xpile_contract ...]` (Lean),
23    /// `<!-- xpile-contract: ... -->` (mdBook).
24    pub embed_citation: bool,
25    /// When true, every falsification_test surfaces as a `\begin{remark}`
26    /// (LaTeX), `-- FALSIFY-<ID>` block (Lean), or `> **Falsification:**`
27    /// block (mdBook). When false, falsification tests are absent.
28    pub include_falsification: bool,
29    /// (major, minor) Lean version. Only Lean 4 is supported
30    /// (`lean_version: Some((4, _))`); rendering with Lean 3 returns
31    /// `Err(ContractBackendError::UnsupportedLeanVersion)`.
32    pub lean_version: Option<(u32, u32)>,
33}
34
35/// Rendered output of a single contract.
36#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
37pub struct RenderedDoc {
38    /// Rendered `.tex` / `.lean` / `.md` text.
39    pub primary: String,
40    /// Optional sidecars (figures, BibTeX entries, oleantheorem files).
41    pub sidecars: Vec<(String, Vec<u8>)>,
42    /// Structural citation chain. Every contract ID in
43    /// `Contract.depends_on` and `Contract.references` MUST be present.
44    pub citations: Vec<ContractId>,
45}
46
47#[derive(Debug, thiserror::Error)]
48pub enum ContractBackendError {
49    #[error("unsupported format for this backend: {0:?}")]
50    UnsupportedFormat(ContractFormat),
51    #[error("unsupported Lean version: {0:?} (only Lean 4 is supported)")]
52    UnsupportedLeanVersion(Option<(u32, u32)>),
53    #[error("rendering error: {0}")]
54    Render(String),
55    #[error("citation bridge violation: {0}")]
56    CitationBridge(String),
57}
58
59/// Proof-lane rendering trait. See `docs/specifications/sub/contract-backend-trait.md`.
60pub trait ContractBackend: Send + Sync {
61    /// Human-readable name, e.g. "latex", "lean-theorem", "mdbook".
62    fn name(&self) -> &'static str;
63
64    /// Formats this backend can render. Each [`ContractFormat`] variant
65    /// is owned by exactly one ContractBackend (`format_ownership`).
66    fn formats(&self) -> &[ContractFormat];
67
68    /// Render a contract under the given config.
69    ///
70    /// Invariants: deterministic per `(contract, config)`; every cited
71    /// contract ID is parseable from `primary` via the host format's
72    /// structured parser (Lean elaborator, LaTeX label machinery,
73    /// mdBook preprocessor) — NOT regex over text.
74    fn render(
75        &self,
76        contract: &Contract,
77        config: &ContractRenderConfig,
78    ) -> Result<RenderedDoc, ContractBackendError>;
79}
xpile_contract_backend/lib.rs

xpile_contract_backend/
lib.rs
