pub mod proof_steps_sidebar;
use crossterm::event::{KeyCode, KeyEvent, MouseButton, MouseEvent, MouseEventKind};
use ratatui::{
layout::{Constraint, Layout, Rect},
style::Color,
Frame,
};
use crate::{
compact_tree::proof_steps_sidebar::{ProofStepsSidebar, ProofStepsSidebarState},
deduction_tree::{
graph::{CompleteProofDag, ProofDagTacticNode},
TacticProofState,
},
interactive::{InteractiveStatefulWidget, Mode},
protocol::NodeId,
selection::{ListSelection, Selection},
theme::Theme,
widgets::{
errors_section::{ErrorsSection, ErrorsSectionState},
legend::{LegendItem, LegendSection},
render_helpers::{render_error, render_no_goals},
AssumptionPane, AssumptionPaneState, GoalsPane, GoalsPaneState,
},
};
#[derive(Default)]
pub struct CompactTree {
state: TacticProofState,
error: Option<String>,
proof_dag: Option<CompleteProofDag>,
current_node_id: Option<NodeId>,
active_goal_name: Option<String>,
errors_section_state: ErrorsSectionState,
sidebar_state: ProofStepsSidebarState,
assumption_state: AssumptionPaneState,
goals_state: GoalsPaneState,
selection: ListSelection,
}
impl CompactTree {
fn has_steps(&self) -> bool {
self.proof_dag.as_ref().is_some_and(|dag| !dag.is_empty())
}
fn current_node(&self) -> Option<&ProofDagTacticNode> {
self.proof_dag
.as_ref()
.and_then(|dag| dag.current_node_id.and_then(|id| dag.get(id)))
}
fn selectable_items(&self) -> Vec<Selection> {
let Some(node_id) = self.current_node_id else {
return Vec::new();
};
let hyp_items = (0..self.state.hypotheses.len())
.map(move |hyp_idx| Selection::Hyp { node_id, hyp_idx });
let goal_items =
(0..self.state.goals.len()).map(move |goal_idx| Selection::Goal { node_id, goal_idx });
hyp_items.chain(goal_items).collect()
}
}
impl Mode for CompactTree {
type Dag = CompleteProofDag;
fn name(&self) -> &'static str {
"Compact Tree"
}
fn keybindings(&self) -> &'static [(&'static str, &'static str)] {
&[("jk", "select"), ("hl", "scroll")]
}
fn current_selection(&self) -> Option<Selection> {
let items = self.selectable_items();
self.selection.current_selection(&items).copied()
}
fn take_clicked_error(&mut self) -> Option<String> {
self.errors_section_state.take_clicked_error()
}
fn legend_sections(&self) -> Vec<LegendSection> {
vec![LegendSection::new(
"Compact Tree",
Color::Yellow,
vec![
LegendItem::new("â–¶", Theme::CURRENT_NODE_BORDER, "current step"),
LegendItem::new("⊢", Theme::GOAL, "open goal"),
],
)]
}
fn update(&mut self, dag: Option<&Self::Dag>, error: Option<String>) {
self.current_node_id = dag.and_then(|dag| dag.current_node_id);
let current_node = self.current_node_id.and_then(|id| dag?.get(id));
let new_state = current_node
.map(|node| node.proof_state.clone())
.unwrap_or_default();
let state_changed = self.state.goals.len() != new_state.goals.len()
|| self.state.hypotheses.len() != new_state.hypotheses.len();
self.state = new_state;
self.active_goal_name = current_node
.and_then(|node| node.proof_state.goals.first())
.and_then(|g| g.username_str().map(String::from));
self.error = error;
self.proof_dag = dag.cloned();
if state_changed {
self.selection.reset(self.selectable_items().len());
}
}
fn handle_key(&mut self, key: KeyEvent) -> bool {
let items = self.selectable_items();
match key.code {
KeyCode::Char('j') | KeyCode::Down => {
self.selection.select_next(items.len());
true
}
KeyCode::Char('k') | KeyCode::Up => {
self.selection.select_previous(items.len());
true
}
KeyCode::Char('h') | KeyCode::Left => {
self.sidebar_state.scroll_left();
true
}
KeyCode::Char('l') | KeyCode::Right => {
self.sidebar_state.scroll_right();
true
}
_ => false,
}
}
fn handle_mouse(&mut self, mouse: MouseEvent) -> bool {
if mouse.kind != MouseEventKind::Down(MouseButton::Left) {
return false;
}
if self
.errors_section_state
.handle_click(mouse.column, mouse.row)
{
return true;
}
let items = self.selectable_items();
self.selection.handle_click(mouse.column, mouse.row, &items)
}
fn render(&mut self, frame: &mut Frame, area: Rect) {
self.selection.clear_regions();
let content = render_error(frame, area, self.error.as_deref());
if self.state.goals.is_empty() && !self.has_steps() {
render_no_goals(frame, content);
return;
}
let current_node_errors = self
.current_node()
.map(|node| node.diagnostics.clone())
.unwrap_or_default();
let error_lines: usize = current_node_errors
.iter()
.map(|e| e.message.lines().count())
.sum();
let (main_area, errors_area) = if error_lines > 0 {
let max_error_height = (content.height / 3).max(3);
let error_height = ((error_lines as u16) + 2).min(max_error_height);
let [main, errors] =
Layout::vertical([Constraint::Fill(1), Constraint::Length(error_height)])
.areas(content);
(main, Some(errors))
} else {
(content, None)
};
ProofStepsSidebar::update_state(&mut self.sidebar_state, self.proof_dag.clone());
let required_width = self.sidebar_state.required_width();
let max_sidebar = (main_area.width * 60) / 100;
let sidebar_width = required_width.clamp(20, max_sidebar);
let [sidebar_area, right_area] =
Layout::horizontal([Constraint::Length(sidebar_width), Constraint::Fill(1)])
.areas(main_area);
frame.render_stateful_widget(ProofStepsSidebar, sidebar_area, &mut self.sidebar_state);
let [hyp_area, goal_area] =
Layout::vertical([Constraint::Percentage(40), Constraint::Percentage(60)])
.areas(right_area);
let is_current = self.current_node_id.is_some();
let selection = self.current_selection();
frame.render_stateful_widget(
AssumptionPane::new(
&self.state,
selection,
true,
is_current,
self.current_node_id,
),
hyp_area,
&mut self.assumption_state,
);
for region in self.assumption_state.click_regions() {
self.selection.add_region(
Rect::new(
region.x as u16,
region.y as u16,
region.width,
region.height,
),
region.selection,
);
}
frame.render_stateful_widget(
GoalsPane::new(
&self.state,
selection,
true,
is_current,
self.current_node_id,
self.active_goal_name.as_deref(),
),
goal_area,
&mut self.goals_state,
);
for region in self.goals_state.click_regions() {
self.selection.add_region(
Rect::new(
region.x as u16,
region.y as u16,
region.width,
region.height,
),
region.selection,
);
}
if let Some(errors_area) = errors_area {
self.errors_section_state.update(current_node_errors);
frame.render_stateful_widget(
ErrorsSection,
errors_area,
&mut self.errors_section_state,
);
}
}
}