oxiz_proof/
format.rs

1//! Unified proof format conversion API.
2//!
3//! This module provides a high-level interface for converting proofs to different
4//! formats, including Coq, Lean, and Isabelle.
5
6use crate::coq;
7use crate::isabelle;
8use crate::lean;
9use crate::proof::Proof;
10use std::fmt;
11
12/// Supported proof formats for export.
13#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
14pub enum ProofFormat {
15    /// Coq proof assistant
16    Coq,
17    /// Lean 3 theorem prover
18    Lean3,
19    /// Lean 4 theorem prover
20    Lean4,
21    /// Isabelle/HOL theorem prover
22    Isabelle,
23}
24
25impl ProofFormat {
26    /// Get file extension for this format.
27    #[must_use]
28    pub fn extension(&self) -> &str {
29        match self {
30            ProofFormat::Coq => "v",
31            ProofFormat::Lean3 | ProofFormat::Lean4 => "lean",
32            ProofFormat::Isabelle => "thy",
33        }
34    }
35
36    /// Get a human-readable name for this format.
37    #[must_use]
38    pub fn name(&self) -> &str {
39        match self {
40            ProofFormat::Coq => "Coq",
41            ProofFormat::Lean3 => "Lean 3",
42            ProofFormat::Lean4 => "Lean 4",
43            ProofFormat::Isabelle => "Isabelle/HOL",
44        }
45    }
46
47    /// Convert a proof to this format.
48    #[must_use]
49    pub fn convert(&self, proof: &Proof) -> String {
50        match self {
51            ProofFormat::Coq => coq::export_to_coq(proof),
52            ProofFormat::Lean3 => lean::export_to_lean3(proof),
53            ProofFormat::Lean4 => lean::export_to_lean(proof),
54            ProofFormat::Isabelle => isabelle::export_to_isabelle(proof, "Proof"),
55        }
56    }
57}
58
59impl fmt::Display for ProofFormat {
60    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
61        write!(f, "{}", self.name())
62    }
63}
64
65/// Quick conversion helpers.
66pub mod quick {
67    use super::*;
68
69    /// Convert proof to Coq format.
70    #[must_use]
71    pub fn to_coq(proof: &Proof) -> String {
72        ProofFormat::Coq.convert(proof)
73    }
74
75    /// Convert proof to Lean 3 format.
76    #[must_use]
77    pub fn to_lean3(proof: &Proof) -> String {
78        ProofFormat::Lean3.convert(proof)
79    }
80
81    /// Convert proof to Lean 4 format.
82    #[must_use]
83    pub fn to_lean(proof: &Proof) -> String {
84        ProofFormat::Lean4.convert(proof)
85    }
86
87    /// Convert proof to Isabelle format.
88    #[must_use]
89    pub fn to_isabelle(proof: &Proof) -> String {
90        ProofFormat::Isabelle.convert(proof)
91    }
92}
93
94#[cfg(test)]
95mod tests {
96    use super::*;
97
98    #[test]
99    fn test_format_extension() {
100        assert_eq!(ProofFormat::Coq.extension(), "v");
101        assert_eq!(ProofFormat::Lean4.extension(), "lean");
102        assert_eq!(ProofFormat::Isabelle.extension(), "thy");
103    }
104
105    #[test]
106    fn test_format_name() {
107        assert_eq!(ProofFormat::Coq.name(), "Coq");
108        assert_eq!(ProofFormat::Lean3.name(), "Lean 3");
109        assert_eq!(ProofFormat::Isabelle.name(), "Isabelle/HOL");
110    }
111
112    #[test]
113    fn test_format_display() {
114        assert_eq!(ProofFormat::Coq.to_string(), "Coq");
115        assert_eq!(ProofFormat::Lean4.to_string(), "Lean 4");
116    }
117
118    #[test]
119    fn test_convert_to_coq() {
120        let mut proof = Proof::new();
121        proof.add_axiom("p");
122
123        let result = ProofFormat::Coq.convert(&proof);
124        assert!(!result.is_empty());
125    }
126
127    #[test]
128    fn test_convert_to_lean() {
129        let mut proof = Proof::new();
130        proof.add_axiom("p");
131
132        let result = ProofFormat::Lean4.convert(&proof);
133        assert!(!result.is_empty());
134    }
135
136    #[test]
137    fn test_convert_to_isabelle() {
138        let mut proof = Proof::new();
139        proof.add_axiom("p");
140
141        let result = ProofFormat::Isabelle.convert(&proof);
142        assert!(!result.is_empty());
143    }
144
145    #[test]
146    fn test_quick_conversion_coq() {
147        let mut proof = Proof::new();
148        proof.add_axiom("p");
149
150        let result = quick::to_coq(&proof);
151        assert!(!result.is_empty());
152    }
153
154    #[test]
155    fn test_quick_conversion_lean() {
156        let mut proof = Proof::new();
157        proof.add_axiom("p");
158
159        let result = quick::to_lean(&proof);
160        assert!(!result.is_empty());
161    }
162
163    #[test]
164    fn test_quick_conversion_isabelle() {
165        let mut proof = Proof::new();
166        proof.add_axiom("p");
167
168        let result = quick::to_isabelle(&proof);
169        assert!(!result.is_empty());
170    }
171}
oxiz_proof/format.rs

oxiz_proof/
format.rs
