lean-tui 1.1.0

Standalone TUI infoview for Lean 4 theorem prover
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147

use ratatui::{
    buffer::Buffer,
    layout::{Alignment, Constraint, Layout, Rect},
    style::{Modifier, Style},
    text::{Line, Span},
    widgets::{Paragraph, StatefulWidget, Widget},
};

use crate::{
    deduction_tree::TacticProofState,
    protocol::NodeId,
    selection::{Region, Selection},
    theme::{Gray, Theme},
    widgets::{AssumptionPane, AssumptionPaneState, GoalsPane, GoalsPaneState},
};

#[derive(Default)]
pub struct DiffPaneState {
    assumption_state: AssumptionPaneState,
    goals_state: GoalsPaneState,
}

impl DiffPaneState {
    pub fn click_regions(&self) -> impl Iterator<Item = &Region> {
        self.assumption_state
            .click_regions()
            .iter()
            .chain(self.goals_state.click_regions().iter())
    }
}

#[derive(Clone, Copy, PartialEq, Eq)]
pub enum DiffPaneKind {
    Before,
    Current,
    After,
}

impl DiffPaneKind {
    const fn title(self) -> &'static str {
        match self {
            Self::Before => " Before ",
            Self::Current => " Current ",
            Self::After => " After ",
        }
    }

    fn title_style(self) -> Style {
        match self {
            Self::Before | Self::After => Style::new().fg(Gray::DIM).add_modifier(Modifier::BOLD),
            Self::Current => Style::new()
                .fg(Theme::CURRENT_NODE_BORDER)
                .add_modifier(Modifier::BOLD),
        }
    }

    const fn is_current(self) -> bool {
        matches!(self, Self::Current)
    }
}

pub struct DiffPane<'a> {
    kind: DiffPaneKind,
    state: &'a TacticProofState,
    selection: Option<Selection>,
    node_id: Option<NodeId>,
    active_goal_name: Option<&'a str>,
}

impl<'a> DiffPane<'a> {
    pub fn new(
        kind: DiffPaneKind,
        state: &'a TacticProofState,
        selection: Option<Selection>,
        node_id: Option<NodeId>,
        active_goal_name: Option<&'a str>,
    ) -> Self {
        Self {
            kind,
            state,
            selection,
            node_id,
            active_goal_name,
        }
    }

    fn is_hyp_focused(&self) -> bool {
        self.kind.is_current() && matches!(self.selection, Some(Selection::Hyp { .. }))
    }

    fn is_goal_focused(&self) -> bool {
        self.kind.is_current() && matches!(self.selection, Some(Selection::Goal { .. }))
    }
}

impl StatefulWidget for DiffPane<'_> {
    type State = DiffPaneState;

    fn render(self, area: Rect, buf: &mut Buffer, state: &mut Self::State) {
        let title_line = Line::from(Span::styled(self.kind.title(), self.kind.title_style()));
        let title_area = Rect::new(area.x, area.y, area.width, 1);
        Paragraph::new(title_line)
            .alignment(Alignment::Center)
            .render(title_area, buf);

        let content_area = Rect::new(
            area.x,
            area.y + 1,
            area.width,
            area.height.saturating_sub(1),
        );

        let visible_hyp_count = self.state.hypotheses.len();

        let hyp_pane_height =
            (visible_hyp_count + 2).min(content_area.height.saturating_sub(4) as usize / 2);

        let [hyp_area, goal_area] = Layout::vertical([
            Constraint::Length(hyp_pane_height as u16),
            Constraint::Fill(1),
        ])
        .areas(content_area);

        let is_current = self.kind.is_current();
        let selection = if is_current { self.selection } else { None };
        let node_id = if is_current { self.node_id } else { None };

        AssumptionPane::new(
            self.state,
            selection,
            self.is_hyp_focused(),
            is_current,
            node_id,
        )
        .render(hyp_area, buf, &mut state.assumption_state);

        GoalsPane::new(
            self.state,
            selection,
            self.is_goal_focused(),
            is_current,
            node_id,
            self.active_goal_name,
        )
        .render(goal_area, buf, &mut state.goals_state);
    }
}