lolli_viz/lib.rs
1//! # lolli-viz
2//!
3//! Visualization for the Lolli linear logic workbench.
4//!
5//! This crate provides rendering of proofs as trees, LaTeX, and graphs.
6//!
7//! ## Output Formats
8//!
9//! - **ASCII/Unicode**: Terminal-friendly proof trees
10//! - **LaTeX**: Using bussproofs package
11//! - **DOT**: Graphviz format for graph visualization
12//!
13//! ## Example
14//!
15//! ```
16//! use lolli_viz::{TreeRenderer, render_ascii};
17//! use lolli_core::{Formula, Proof, Rule, Sequent};
18//!
19//! let proof = Proof {
20//! conclusion: Sequent::new(vec![Formula::neg_atom("A"), Formula::atom("A")]),
21//! rule: Rule::Axiom,
22//! premises: vec![],
23//! };
24//!
25//! let ascii = render_ascii(&proof);
26//! println!("{}", ascii);
27//! ```
28
29#![warn(missing_docs)]
30#![warn(clippy::all)]
31
32pub use lolli_core::{Formula, Proof, Rule, Sequent};
33
34mod ascii;
35mod latex;
36mod dot;
37
38pub use ascii::TreeRenderer;
39pub use latex::LatexRenderer;
40pub use dot::DotRenderer;
41
42/// Render a proof as ASCII text.
43pub fn render_ascii(proof: &Proof) -> String {
44 TreeRenderer::new().render(proof)
45}
46
47/// Render a proof as Unicode text (with box-drawing characters).
48pub fn render_unicode(proof: &Proof) -> String {
49 let mut renderer = TreeRenderer::new();
50 renderer.unicode = true;
51 renderer.render(proof)
52}
53
54/// Render a proof as LaTeX (bussproofs package).
55pub fn render_latex(proof: &Proof) -> String {
56 LatexRenderer::new().render(proof)
57}
58
59/// Render a proof as Graphviz DOT format.
60pub fn render_dot(proof: &Proof) -> String {
61 DotRenderer::new().render(proof)
62}