319 lines
14 KiB
Rust
319 lines
14 KiB
Rust
|
//! Inspector panel for viewing theory/instance details
|
||
|
|
//!
|
||
|
|
//! Shows detailed information about the currently selected item.
|
||
|
|
|
||
|
|
use eframe::egui;
|
||
|
|
|
||
|
|
use crate::gui::state::{GuiState, SelectedItem};
|
||
|
|
use crate::repl::{InstanceDetail, TheoryDetail};
|
||
|
|
|
||
|
|
/// Inspector panel for viewing details
|
||
|
|
pub struct InspectorPanel {}
|
||
|
|
|
||
|
|
impl InspectorPanel {
|
||
|
|
pub fn new() -> Self {
|
||
|
|
Self {}
|
||
|
|
}
|
||
|
|
|
||
|
|
pub fn show(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
|
||
|
|
ui.heading("Inspector");
|
||
|
|
ui.separator();
|
||
|
|
|
||
|
|
match &state.selected_item {
|
||
|
|
Some(SelectedItem::Theory(name)) => {
|
||
|
|
if let Some(detail) = state.selected_theory_detail() {
|
||
|
|
self.show_theory_detail(ui, state, &detail);
|
||
|
|
} else {
|
||
|
|
ui.label(format!("Theory '{}' not found", name));
|
||
|
|
}
|
||
|
|
}
|
||
|
|
Some(SelectedItem::Instance(name)) => {
|
||
|
|
if let Some(detail) = state.selected_instance_detail() {
|
||
|
|
self.show_instance_detail(ui, state, &detail);
|
||
|
|
} else {
|
||
|
|
ui.label(format!("Instance '{}' not found", name));
|
||
|
|
}
|
||
|
|
}
|
||
|
|
None => {
|
||
|
|
ui.label("Select a theory or instance to inspect");
|
||
|
|
}
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
fn show_theory_detail(&self, ui: &mut egui::Ui, state: &mut GuiState, detail: &TheoryDetail) {
|
||
|
|
// Theory header
|
||
|
|
ui.horizontal(|ui| {
|
||
|
|
ui.strong("Theory:");
|
||
|
|
ui.label(&detail.name);
|
||
|
|
});
|
||
|
|
|
||
|
|
// Parameters
|
||
|
|
if !detail.params.is_empty() {
|
||
|
|
ui.horizontal(|ui| {
|
||
|
|
ui.label("Parameters:");
|
||
|
|
for (name, theory) in &detail.params {
|
||
|
|
ui.label(format!("{}: {}", name, theory));
|
||
|
|
}
|
||
|
|
});
|
||
|
|
}
|
||
|
|
|
||
|
|
ui.add_space(8.0);
|
||
|
|
|
||
|
|
egui::ScrollArea::vertical()
|
||
|
|
.auto_shrink([false, false])
|
||
|
|
.show(ui, |ui| {
|
||
|
|
// Sorts section
|
||
|
|
egui::CollapsingHeader::new(format!("Sorts ({})", detail.sorts.len()))
|
||
|
|
.default_open(state.inspector_sorts_expanded)
|
||
|
|
.show(ui, |ui| {
|
||
|
|
state.inspector_sorts_expanded = true;
|
||
|
|
if detail.sorts.is_empty() {
|
||
|
|
ui.label("(none)");
|
||
|
|
} else {
|
||
|
|
for sort in &detail.sorts {
|
||
|
|
ui.label(format!(" {} : Sort", sort));
|
||
|
|
}
|
||
|
|
}
|
||
|
|
});
|
||
|
|
|
||
|
|
// Functions section
|
||
|
|
egui::CollapsingHeader::new(format!("Functions ({})", detail.functions.len()))
|
||
|
|
.default_open(state.inspector_functions_expanded)
|
||
|
|
.show(ui, |ui| {
|
||
|
|
state.inspector_functions_expanded = true;
|
||
|
|
if detail.functions.is_empty() {
|
||
|
|
ui.label("(none)");
|
||
|
|
} else {
|
||
|
|
for (name, domain, codomain) in &detail.functions {
|
||
|
|
ui.label(format!(" {} : {} -> {}", name, domain, codomain));
|
||
|
|
}
|
||
|
|
}
|
||
|
|
});
|
||
|
|
|
||
|
|
// Relations section
|
||
|
|
egui::CollapsingHeader::new(format!("Relations ({})", detail.relations.len()))
|
||
|
|
.default_open(state.inspector_relations_expanded)
|
||
|
|
.show(ui, |ui| {
|
||
|
|
state.inspector_relations_expanded = true;
|
||
|
|
if detail.relations.is_empty() {
|
||
|
|
ui.label("(none)");
|
||
|
|
} else {
|
||
|
|
for (name, domain) in &detail.relations {
|
||
|
|
ui.label(format!(" {} : {} -> Prop", name, domain));
|
||
|
|
}
|
||
|
|
}
|
||
|
|
});
|
||
|
|
|
||
|
|
// Instance fields section
|
||
|
|
if !detail.instance_fields.is_empty() {
|
||
|
|
egui::CollapsingHeader::new(format!(
|
||
|
|
"Instance Fields ({})",
|
||
|
|
detail.instance_fields.len()
|
||
|
|
))
|
||
|
|
.default_open(true)
|
||
|
|
.show(ui, |ui| {
|
||
|
|
for (name, theory_type) in &detail.instance_fields {
|
||
|
|
ui.label(format!(" {} : {} instance", name, theory_type));
|
||
|
|
}
|
||
|
|
});
|
||
|
|
}
|
||
|
|
|
||
|
|
// Axioms section
|
||
|
|
egui::CollapsingHeader::new(format!("Axioms ({})", detail.axioms.len()))
|
||
|
|
.default_open(state.inspector_axioms_expanded)
|
||
|
|
.show(ui, |ui| {
|
||
|
|
state.inspector_axioms_expanded = true;
|
||
|
|
if detail.axioms.is_empty() {
|
||
|
|
ui.label("(none)");
|
||
|
|
} else {
|
||
|
|
for (i, axiom) in detail.axioms.iter().enumerate() {
|
||
|
|
let context_str: Vec<String> = axiom
|
||
|
|
.context
|
||
|
|
.iter()
|
||
|
|
.map(|(name, sort)| format!("{}: {}", name, sort))
|
||
|
|
.collect();
|
||
|
|
|
||
|
|
let axiom_str = if axiom.premise == "true" {
|
||
|
|
format!(
|
||
|
|
"[{}] forall {}. |- {}",
|
||
|
|
i,
|
||
|
|
context_str.join(", "),
|
||
|
|
axiom.conclusion
|
||
|
|
)
|
||
|
|
} else {
|
||
|
|
format!(
|
||
|
|
"[{}] forall {}. {} |- {}",
|
||
|
|
i,
|
||
|
|
context_str.join(", "),
|
||
|
|
axiom.premise,
|
||
|
|
axiom.conclusion
|
||
|
|
)
|
||
|
|
};
|
||
|
|
ui.label(axiom_str);
|
||
|
|
}
|
||
|
|
}
|
||
|
|
});
|
||
|
|
});
|
||
|
|
}
|
||
|
|
|
||
|
|
fn show_instance_detail(
|
||
|
|
&self,
|
||
|
|
ui: &mut egui::Ui,
|
||
|
|
state: &mut GuiState,
|
||
|
|
detail: &InstanceDetail,
|
||
|
|
) {
|
||
|
|
// Instance header
|
||
|
|
ui.horizontal(|ui| {
|
||
|
|
ui.strong("Instance:");
|
||
|
|
ui.label(&detail.name);
|
||
|
|
ui.label(":");
|
||
|
|
ui.label(&detail.theory_name);
|
||
|
|
});
|
||
|
|
|
||
|
|
ui.add_space(8.0);
|
||
|
|
|
||
|
|
// Action buttons
|
||
|
|
ui.horizontal(|ui| {
|
||
|
|
let detail_name = detail.name.clone();
|
||
|
|
if ui.button("View Graph").clicked() {
|
||
|
|
state.show_graph(&detail_name, None);
|
||
|
|
}
|
||
|
|
if ui.button("Run Chase").clicked() {
|
||
|
|
state.log_info(format!("Use Chase menu to run chase on '{}'", detail_name));
|
||
|
|
}
|
||
|
|
});
|
||
|
|
|
||
|
|
ui.add_space(8.0);
|
||
|
|
|
||
|
|
egui::ScrollArea::vertical()
|
||
|
|
.auto_shrink([false, false])
|
||
|
|
.show(ui, |ui| {
|
||
|
|
// Elements section
|
||
|
|
let total_elements: usize = detail.elements.iter().map(|(_, v)| v.len()).sum();
|
||
|
|
egui::CollapsingHeader::new(format!("Elements ({})", total_elements))
|
||
|
|
.default_open(state.inspector_elements_expanded)
|
||
|
|
.show(ui, |ui| {
|
||
|
|
state.inspector_elements_expanded = true;
|
||
|
|
if detail.elements.is_empty() {
|
||
|
|
ui.label("(none)");
|
||
|
|
} else {
|
||
|
|
for (sort_name, elements) in &detail.elements {
|
||
|
|
ui.horizontal(|ui| {
|
||
|
|
ui.strong(format!("{} ({}):", sort_name, elements.len()));
|
||
|
|
});
|
||
|
|
ui.indent("elements", |ui| {
|
||
|
|
// Show elements in a grid if there are many
|
||
|
|
if elements.len() <= 10 {
|
||
|
|
for elem in elements {
|
||
|
|
ui.label(format!(" {}", elem));
|
||
|
|
}
|
||
|
|
} else {
|
||
|
|
// Show first few and a count
|
||
|
|
for elem in elements.iter().take(5) {
|
||
|
|
ui.label(format!(" {}", elem));
|
||
|
|
}
|
||
|
|
ui.label(format!(" ... and {} more", elements.len() - 5));
|
||
|
|
}
|
||
|
|
});
|
||
|
|
}
|
||
|
|
}
|
||
|
|
});
|
||
|
|
|
||
|
|
// Functions section
|
||
|
|
let total_func_values: usize = detail.functions.iter().map(|(_, v)| v.len()).sum();
|
||
|
|
if total_func_values > 0 {
|
||
|
|
egui::CollapsingHeader::new(format!("Function Values ({})", total_func_values))
|
||
|
|
.default_open(state.inspector_functions_expanded)
|
||
|
|
.show(ui, |ui| {
|
||
|
|
for (func_name, values) in &detail.functions {
|
||
|
|
ui.horizontal(|ui| {
|
||
|
|
ui.strong(format!("{} ({}):", func_name, values.len()));
|
||
|
|
});
|
||
|
|
ui.indent("func_values", |ui| {
|
||
|
|
if values.len() <= 10 {
|
||
|
|
for value in values {
|
||
|
|
ui.label(format!(" {}", value));
|
||
|
|
}
|
||
|
|
} else {
|
||
|
|
for value in values.iter().take(5) {
|
||
|
|
ui.label(format!(" {}", value));
|
||
|
|
}
|
||
|
|
ui.label(format!(" ... and {} more", values.len() - 5));
|
||
|
|
}
|
||
|
|
});
|
||
|
|
}
|
||
|
|
});
|
||
|
|
}
|
||
|
|
|
||
|
|
// Relations section
|
||
|
|
let total_tuples: usize = detail.relations.iter().map(|(_, _, t)| t.len()).sum();
|
||
|
|
if total_tuples > 0 {
|
||
|
|
egui::CollapsingHeader::new(format!("Relations ({} tuples)", total_tuples))
|
||
|
|
.default_open(state.inspector_relations_expanded)
|
||
|
|
.show(ui, |ui| {
|
||
|
|
for (rel_name, field_names, tuples) in &detail.relations {
|
||
|
|
ui.horizontal(|ui| {
|
||
|
|
ui.strong(format!("{} ({} tuples):", rel_name, tuples.len()));
|
||
|
|
|
||
|
|
// Add button to view as graph
|
||
|
|
let detail_name = detail.name.clone();
|
||
|
|
let rel_name_clone = rel_name.clone();
|
||
|
|
if ui.small_button("View Graph").clicked() {
|
||
|
|
state.show_graph(&detail_name, Some(&rel_name_clone));
|
||
|
|
}
|
||
|
|
});
|
||
|
|
|
||
|
|
ui.indent("rel_tuples", |ui| {
|
||
|
|
let display_tuples = if tuples.len() <= 10 {
|
||
|
|
tuples.as_slice()
|
||
|
|
} else {
|
||
|
|
&tuples[..5]
|
||
|
|
};
|
||
|
|
|
||
|
|
for tuple in display_tuples {
|
||
|
|
let tuple_str = if field_names.is_empty() {
|
||
|
|
// Unary relation
|
||
|
|
format!(" {} {}", tuple.join(", "), rel_name)
|
||
|
|
} else {
|
||
|
|
// Multi-ary relation with field names
|
||
|
|
let fields: Vec<String> = field_names
|
||
|
|
.iter()
|
||
|
|
.zip(tuple.iter())
|
||
|
|
.map(|(f, v)| format!("{}: {}", f, v))
|
||
|
|
.collect();
|
||
|
|
format!(" [{}] {}", fields.join(", "), rel_name)
|
||
|
|
};
|
||
|
|
ui.label(tuple_str);
|
||
|
|
}
|
||
|
|
|
||
|
|
if tuples.len() > 10 {
|
||
|
|
ui.label(format!(" ... and {} more", tuples.len() - 5));
|
||
|
|
}
|
||
|
|
});
|
||
|
|
}
|
||
|
|
});
|
||
|
|
}
|
||
|
|
|
||
|
|
// Nested instances section
|
||
|
|
if !detail.nested.is_empty() {
|
||
|
|
egui::CollapsingHeader::new(format!(
|
||
|
|
"Nested Instances ({})",
|
||
|
|
detail.nested.len()
|
||
|
|
))
|
||
|
|
.default_open(true)
|
||
|
|
.show(ui, |ui| {
|
||
|
|
for (field_name, elem_count) in &detail.nested {
|
||
|
|
ui.label(format!(" {} ({} elements)", field_name, elem_count));
|
||
|
|
}
|
||
|
|
});
|
||
|
|
}
|
||
|
|
});
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
impl Default for InspectorPanel {
|
||
|
|
fn default() -> Self {
|
||
|
|
Self::new()
|
||
|
|
}
|
||
|
|
}
|