karpal_verify/
export.rs

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

karpal_verify/
export.rs
