karpal_verify/
export.rs

1#[cfg(not(feature = "std"))]
2use alloc::{string::String, vec::Vec};
3#[cfg(feature = "std")]
4use std::{string::String, vec::Vec};
5
6use crate::{
7    LeanExport, LeanPrelude, Obligation, ObligationBundle, export_lean_module,
8    export_module_with_prelude as export_lean_module_with_prelude, export_smt_obligation,
9};
10
11/// Export an entire bundle as one SMT-LIB2 script per obligation.
12pub fn export_smt_bundle(bundle: &ObligationBundle) -> Vec<(String, String)> {
13    bundle
14        .obligations()
15        .iter()
16        .map(|obligation| (obligation.name.clone(), export_smt_obligation(obligation)))
17        .collect()
18}
19
20/// Export a whole bundle as a single Lean 4 module.
21pub fn export_lean_bundle(module_name: &str, bundle: &ObligationBundle) -> String {
22    export_lean_module(module_name, bundle.obligations())
23}
24
25/// Export a whole bundle as a single Lean 4 module with explicit prelude metadata.
26pub fn export_lean_bundle_with_prelude(
27    module_name: &str,
28    bundle: &ObligationBundle,
29    prelude: LeanPrelude,
30) -> String {
31    export_lean_module_with_prelude(module_name, bundle.obligations(), prelude)
32}
33
34/// Export a whole bundle as structured Lean module metadata plus source.
35pub fn export_lean_bundle_structured(module_name: &str, bundle: &ObligationBundle) -> LeanExport {
36    crate::lean::export(module_name, bundle.obligations())
37}
38
39/// Export a whole bundle as structured Lean module metadata plus source with explicit prelude metadata.
40pub fn export_lean_bundle_structured_with_prelude(
41    module_name: &str,
42    bundle: &ObligationBundle,
43    prelude: LeanPrelude,
44) -> LeanExport {
45    crate::lean::export_with_prelude(module_name, bundle.obligations(), prelude)
46}
47
48/// Export a list of obligations as one SMT-LIB2 script per obligation.
49pub fn export_smt_batch(obligations: &[Obligation]) -> Vec<(String, String)> {
50    obligations
51        .iter()
52        .map(|obligation| (obligation.name.clone(), export_smt_obligation(obligation)))
53        .collect()
54}
55
56#[cfg(test)]
57mod tests {
58    use super::*;
59    use crate::{AlgebraicSignature, Origin, Sort};
60
61    #[test]
62    fn smt_bundle_export_returns_one_script_per_obligation() {
63        let sig = AlgebraicSignature::monoid(Sort::Int, "combine", "e");
64        let bundle = ObligationBundle::monoid("sum", Origin::new("karpal-core", "Sum<i32>"), &sig);
65        let scripts = export_smt_bundle(&bundle);
66        assert_eq!(scripts.len(), 3);
67        assert!(scripts[0].1.contains("(check-sat)"));
68    }
69
70    #[test]
71    fn lean_bundle_export_contains_multiple_theorems() {
72        let sig = AlgebraicSignature::group(Sort::Int, "combine", "e", "inv");
73        let bundle = ObligationBundle::group("sum", Origin::new("karpal-algebra", "i32"), &sig);
74        let module = export_lean_bundle("KarpalVerify", &bundle);
75        assert!(module.contains("theorem associativity"));
76        assert!(module.contains("theorem left_inverse"));
77        assert!(module.contains("theorem right_inverse"));
78
79        let structured = export_lean_bundle_structured("KarpalVerify", &bundle);
80        assert_eq!(structured.theorems.len(), 5);
81        assert_eq!(
82            structured
83                .theorem_for_obligation("left_inverse")
84                .map(|t| t.witness_ref("KarpalVerify")),
85            Some("KarpalVerify.left_inverse".into())
86        );
87    }
88
89    #[test]
90    fn lean_bundle_export_with_prelude_renders_imports() {
91        let sig = AlgebraicSignature::semigroup(Sort::Int, "combine");
92        let bundle =
93            ObligationBundle::semigroup("sum", Origin::new("karpal-core", "Sum<i32>"), &sig);
94        let module = export_lean_bundle_with_prelude(
95            "KarpalVerify",
96            &bundle,
97            LeanPrelude::new().with_import("Mathlib"),
98        );
99
100        assert!(module.starts_with("import Mathlib\n\nnamespace KarpalVerify"));
101    }
102}
karpal_verify/export.rs

karpal_verify/
export.rs
