From 9df82207e772b830a5d872eb16db7d978f6ed19d Mon Sep 17 00:00:00 2001 From: Thierry Arnoux Date: Sun, 12 Mar 2023 21:43:04 +0100 Subject: [PATCH 1/2] Add a `trace` mechanism to save the trace tree in a more readable way. --- rumm/Cargo.toml | 1 + rumm/src/context.rs | 19 -- rumm/src/lang/expression.rs | 12 +- rumm/src/lang/mod.rs | 1 - rumm/src/lang/proof_definition.rs | 10 +- rumm/src/lang/tactics_definition.rs | 5 +- rumm/src/main.rs | 1 + rumm/src/script.rs | 22 +- rumm/src/tactics/find.rs | 37 ++-- rumm/src/tactics/find_hyp.rs | 25 +-- rumm/src/tactics/hypothesis.rs | 7 +- rumm/src/tactics/match.rs | 25 +-- rumm/src/tactics/mod.rs | 12 +- rumm/src/tactics/skipped.rs | 5 +- rumm/src/tactics/subgoal.rs | 10 +- rumm/src/tactics/try.rs | 10 +- rumm/src/tactics/use_script_tactics.rs | 8 +- rumm/src/trace.rs | 78 +++++++ vendor/treeview/LICENSE | 21 ++ vendor/treeview/dist/treeview.min.css | 2 + vendor/treeview/dist/treeview.min.css.map | 1 + vendor/treeview/dist/treeview.min.js | 2 + vendor/treeview/dist/treeview.min.js.map | 1 + vendor/treeview/src/treeview.js | 259 ++++++++++++++++++++++ 24 files changed, 461 insertions(+), 113 deletions(-) create mode 100644 rumm/src/trace.rs create mode 100644 vendor/treeview/LICENSE create mode 100644 vendor/treeview/dist/treeview.min.css create mode 100644 vendor/treeview/dist/treeview.min.css.map create mode 100644 vendor/treeview/dist/treeview.min.js create mode 100644 vendor/treeview/dist/treeview.min.js.map create mode 100644 vendor/treeview/src/treeview.js diff --git a/rumm/Cargo.toml b/rumm/Cargo.toml index c323e08..0fc1210 100644 --- a/rumm/Cargo.toml +++ b/rumm/Cargo.toml @@ -17,6 +17,7 @@ typed-arena = "2.0" thiserror = "1.0" annotate-snippets = "0.9" simple_logger = "1.13.0" +serde_json = "1.0" # metamath-knife = { path = "../../metamath-knife" } # metamath-knife = { git = "https://github.com/david-a-wheeler/metamath-knife", tag="v0.3.6"} metamath-knife = { git = "https://github.com/david-a-wheeler/metamath-knife", rev="a5a22c8"} diff --git a/rumm/src/context.rs b/rumm/src/context.rs index 3cee365..6f9e6fa 100644 --- a/rumm/src/context.rs +++ b/rumm/src/context.rs @@ -2,7 +2,6 @@ use std::sync::Arc; use crate::tactics::Tactics; use crate::lang::ProofStep; use crate::lang::Db; -use crate::lang::DisplayPair; use crate::lang::Hypotheses; use crate::lang::TacticsDefinition; use crate::lang::TacticsDict; @@ -24,7 +23,6 @@ pub struct Context { tactics_variables: HashMap>, formula_variables: HashMap, subst_variables: HashMap, - depth: usize, } impl Debug for Context { @@ -52,23 +50,9 @@ impl<'a> Context { tactics_variables: HashMap::default(), formula_variables: HashMap::default(), subst_variables: HashMap::default(), - depth: 0, } } - pub fn message(&self, message: &str) { - println!("{:indent$}{message}", "", indent = self.depth); - } - - pub fn enter(&self, message: &str) { - self.message(&format!("Proving {}", DisplayPair(&self.goal, &self.db))); - self.message(&format!(">> {message}")); - } - - pub fn exit(&self, message: &str) { - self.message(&format!("<< {message}")); - } - pub fn get_tactics_definition(&self, name: String) -> Option<&TacticsDefinition> { self.tactics_definitions.get(name) } @@ -85,7 +69,6 @@ impl<'a> Context { tactics_variables: self.tactics_variables.clone(), formula_variables: self.formula_variables.clone(), subst_variables: self.subst_variables.clone(), - depth: self.depth + 1, } } @@ -103,7 +86,6 @@ impl<'a> Context { tactics_variables: self.tactics_variables.clone(), formula_variables: self.formula_variables.clone(), subst_variables: self.subst_variables.clone(), - depth: self.depth + 1, } } @@ -119,7 +101,6 @@ impl<'a> Context { tactics_variables: self.tactics_variables.clone(), formula_variables: self.formula_variables.clone(), subst_variables: self.subst_variables.clone(), - depth: self.depth + 1, } } diff --git a/rumm/src/lang/expression.rs b/rumm/src/lang/expression.rs index 7377709..ca93201 100644 --- a/rumm/src/lang/expression.rs +++ b/rumm/src/lang/expression.rs @@ -1,5 +1,6 @@ use crate::parser::FormulaOrSubstitutionListId; use crate::parser::OptionalTactics; +use crate::trace::Trace; use std::sync::Arc; use crate::tactics::Tactics; use crate::error::Result; @@ -124,8 +125,15 @@ impl TacticsExpression { } } - pub fn execute(&self, context: &mut Context) -> TacticsResult { - self.evaluate(&context)?.execute(context) + pub fn execute(&self, trace: &mut Trace, context: &mut Context) -> TacticsResult { + let tactics = self.evaluate(&context).unwrap(); + let mut trace1 = trace.enter(context, &format!("tactics {}", tactics.get_name())); + let result = tactics.execute_intern(&mut trace1, context); + match result { + TacticsResult::Ok(_) => { trace.exit(trace1, &"tactics : success"); } + TacticsResult::Err(_) => { trace.exit(trace1, &"tactics : failure"); } + } + result } } diff --git a/rumm/src/lang/mod.rs b/rumm/src/lang/mod.rs index c187654..cb6324f 100644 --- a/rumm/src/lang/mod.rs +++ b/rumm/src/lang/mod.rs @@ -10,7 +10,6 @@ mod tactics_definition; pub use database::Db; pub use database::Hypotheses; pub use display::Display; -pub use display::DisplayPair; pub use expression::Expression; pub use expression::FormulaExpression; pub use expression::StatementExpression; diff --git a/rumm/src/lang/proof_definition.rs b/rumm/src/lang/proof_definition.rs index bb87759..3747018 100644 --- a/rumm/src/lang/proof_definition.rs +++ b/rumm/src/lang/proof_definition.rs @@ -5,6 +5,7 @@ use crate::lang::TacticsDict; use crate::lang::{Db, Display}; use crate::parser::{Parse, Parser}; use crate::tactics::TacticsError; +use crate::trace::Trace; use core::fmt::Formatter; use metamath_knife::formula::Substitutions; use metamath_knife::proof::ProofTreeArray; @@ -117,13 +118,10 @@ impl Parse for ProofDefinition { } impl ProofDefinition { - pub fn prove(&self, db: Db, tactics_definitions: TacticsDict) -> std::result::Result { + pub fn prove(&self, db: Db, tactics_definitions: TacticsDict, trace: &mut Trace) -> std::result::Result { if let Some((theorem_formula, essential_hypotheses)) = db.get_theorem_formulas(self.theorem) { - println!("====================================================\n\n"); - println!("Proof for {:?}:", self.theorem.to_string(&db)); - let mut context = - Context::new(db.clone(), theorem_formula, essential_hypotheses, tactics_definitions); - self.tactics.execute(&mut context) + let mut context = Context::new(db.clone(), theorem_formula, essential_hypotheses, tactics_definitions); + self.tactics.execute(trace, &mut context) } else { println!("Unknown theorem {:?}!", self.theorem); Err(TacticsError::UnknownLabel(self.theorem)) diff --git a/rumm/src/lang/tactics_definition.rs b/rumm/src/lang/tactics_definition.rs index e6fba6c..c3a3a6e 100644 --- a/rumm/src/lang/tactics_definition.rs +++ b/rumm/src/lang/tactics_definition.rs @@ -7,6 +7,7 @@ use crate::lang::ParameterDefinition; use crate::lang::{Db, Display}; use crate::parser::{Parse, Parser, Token}; use crate::tactics::TacticsResult; +use crate::trace::Trace; use core::fmt::Formatter; use std::collections::HashMap; use std::sync::Arc; @@ -93,8 +94,8 @@ impl TacticsDefinition { // self.description.clone() // } // - pub fn execute(&self, context: &mut Context) -> TacticsResult { - self.tactics.execute(context) + pub fn execute(&self, trace: &mut Trace, context: &mut Context) -> TacticsResult { + self.tactics.execute(trace, context) } pub fn add_variables(&self, context: &mut Context, parameters: &Vec) -> TacticsResult<()> { diff --git a/rumm/src/main.rs b/rumm/src/main.rs index 5d68793..2de20c6 100644 --- a/rumm/src/main.rs +++ b/rumm/src/main.rs @@ -1,6 +1,7 @@ //! A Metamath Proof Assistant mod context; +mod trace; pub mod error; mod lang; pub mod parser; diff --git a/rumm/src/script.rs b/rumm/src/script.rs index 8e19ad2..036974f 100644 --- a/rumm/src/script.rs +++ b/rumm/src/script.rs @@ -1,7 +1,10 @@ +use colored::Colorize; + use crate::error::Result; use crate::lang::{Db, Display}; use crate::lang::{ProofDefinition, TacticsDefinition, TacticsDict}; use crate::parser::{Parse, Parser}; +use crate::trace::Trace; use core::fmt::{Debug, Formatter}; pub struct Script { @@ -50,16 +53,19 @@ impl Script { pub fn execute(&mut self) -> Result { for proof_def in &self.proof_definitions { - match proof_def.prove(self.db.clone(), self.tactics_definitions.clone()) { - Ok(step) => { - println!("Success"); - let mut arr = step.as_proof_tree_array(self.db.clone()); - arr.calc_indent(); - self.db - .export_mmp(proof_def.theorem(), &arr, &mut std::io::stdout()); + let mut trace = Trace::new(); + print!("Proving {} ... ", &proof_def.theorem().to_string(&self.db)); + match proof_def.prove(self.db.clone(), self.tactics_definitions.clone(), &mut trace) { + Ok(_step) => { + println!("{}", "ok".green()); + // let mut arr = step.as_proof_tree_array(self.db.clone()); + // arr.calc_indent(); + // self.db.export_mmp(proof_def.theorem(), &arr, &mut std::io::stdout()); } Err(_) => { - println!("Failure"); + println!("{}", "failed".red()); + //trace.dump(); + trace.export_js_tree(&proof_def.theorem().to_string(&self.db)); } } } diff --git a/rumm/src/tactics/find.rs b/rumm/src/tactics/find.rs index 102c3a0..8279c7d 100644 --- a/rumm/src/tactics/find.rs +++ b/rumm/src/tactics/find.rs @@ -1,6 +1,5 @@ use metamath_knife::formula::Substitutions; use metamath_knife::Formula; -use crate::lang::DisplayPair; use crate::lang::FormulaExpression; use crate::lang::TacticsExpression; use crate::context::Context; @@ -11,6 +10,7 @@ use crate::parser::{Parse, Parser}; use crate::tactics::Tactics; use crate::tactics::TacticsError; use crate::tactics::TacticsResult; +use crate::trace::Trace; use core::fmt::Formatter; @@ -55,46 +55,43 @@ impl Tactics for Find { "A tactics which searches for a theorem matching the given formula.".to_string() } - fn execute(&self, context: &mut Context) -> TacticsResult { + fn execute_intern(&self, trace: &mut Trace, context: &mut Context) -> TacticsResult { let target = self.formula.evaluate(context)?.substitute(context.variables()); - context.enter(&format!("Find {}", DisplayPair(&target, &context.db))); for (label, formula) in context.clone().hypotheses().iter() { - context.message(&format!("Trying {}", DisplayPair(formula, &context.db))); - if let Ok(step) = self.check_match(context, &target, &*formula, |_subst| { + trace.message(&format!("Trying {}", formula.to_string(&context.db))); + if let Ok(step) = self.check_match(trace, context, &target, &*formula, |_subst, _trace| { Ok(ProofStep::hyp(*label, formula.clone())) }) { - context.exit(&format!("Matched hypothesis {}", DisplayPair(formula, &context.db))); return Ok(step); } } for (hyp, step) in context.clone().subgoals().iter() { - context.message(&format!("Trying {}", DisplayPair(hyp, &context.db))); - if let Ok(step) = self.check_match(context, &target, &*hyp, |_subst| { + trace.message(&format!("Trying {}", hyp.to_string(&context.db))); + if let Ok(step) = self.check_match(trace, context, &target, &*hyp, |_subst, _trace| { Ok(step.clone()) }) { - context.exit(&format!("Matched subgoal {}", DisplayPair(hyp, &context.db))); return Ok(step); } } for (label, formula, hyps) in context.clone().statements() { - if let Ok(step) = self.check_match(context, &target, &formula, |subst| { - context.message(&format!("Found match with {}", DisplayPair(&label, &context.db))); - // context.message(&format!(" subst:{}", DisplayPair(subst, &context.db))); + if let Ok(step) = self.check_match(trace, context, &target, &formula, |subst, trace: &mut Trace| { + trace.message(&format!("Found match with {}", &label.to_string(&context.db))); + // trace.message(&format!(" subst:{}", subst.to_string(&context.db))); let mut substeps = vec![]; let mut failed = false; for (_hyp_label, hyp_formula) in hyps.iter() { let sub_goal = hyp_formula.substitute(&subst); let mut sub_context = context.with_goal(sub_goal).with_variables(&subst); - if let Ok(sub_step) = self.tactics1.execute(&mut sub_context) { + if let Ok(sub_step) = self.tactics1.execute(trace, &mut sub_context) { substeps.push(sub_step); } else { failed = true; } } if failed { return Err(TacticsError::NoMatchFound); }; - context.message("Unification success"); + trace.message("Unification success"); let subgoal = formula.substitute(&subst); - context.message(&format!(" subgoal = {}", DisplayPair(&subgoal, &context.db))); + trace.message(&format!(" subgoal = {}", &subgoal.to_string(&context.db))); let mut subgoal_subst = Substitutions::new(); subgoal.unify(&formula, &mut subgoal_subst)?; Ok(ProofStep::apply( @@ -104,23 +101,21 @@ impl Tactics for Find { Box::new(subgoal_subst.clone()), )) }) { - context.exit("Find Successful!"); return Ok(step); } } - context.exit("Find: No match found"); Err(TacticsError::NoMatchFound) } } impl Find { - fn check_match(&self, context: &Context, target: &Formula, formula: &Formula, make_proof_step: F) -> TacticsResult - where F: Fn(&Box) -> TacticsResult { + fn check_match(&self, trace: &mut Trace, context: &Context, target: &Formula, formula: &Formula, make_proof_step: F) -> TacticsResult + where F: Fn(&Box, &mut Trace) -> TacticsResult { let mut subst = Substitutions::new(); formula.unify(&target, & mut subst)?; - let step1 = make_proof_step(&Box::new(subst.clone()))?; + let step1 = make_proof_step(&Box::new(subst.clone()), trace)?; let mut context2 = context.with_variables(&subst); context2.add_subgoal(step1.result().clone(), step1); - Ok(self.tactics2.execute(&mut context2)?) + Ok(self.tactics2.execute(trace, &mut context2)?) } } diff --git a/rumm/src/tactics/find_hyp.rs b/rumm/src/tactics/find_hyp.rs index 754127d..016cdb2 100644 --- a/rumm/src/tactics/find_hyp.rs +++ b/rumm/src/tactics/find_hyp.rs @@ -1,6 +1,5 @@ use metamath_knife::formula::Substitutions; use metamath_knife::Formula; -use crate::lang::DisplayPair; use crate::lang::FormulaExpression; use crate::lang::TacticsExpression; use crate::context::Context; @@ -11,6 +10,7 @@ use crate::parser::{Parse, Parser}; use crate::tactics::Tactics; use crate::tactics::TacticsError; use crate::tactics::TacticsResult; +use crate::trace::Trace; use core::fmt::Formatter; @@ -51,50 +51,47 @@ impl Tactics for FindHyp { "A tactics which searches for a hypothesis matching the given formula.".to_string() } - fn execute(&self, context: &mut Context) -> TacticsResult { + fn execute_intern(&self, trace: &mut Trace, context: &mut Context) -> TacticsResult { let target = self.formula.evaluate(context)?.substitute(context.variables()); - context.enter(&format!("Find! {}", DisplayPair(&target, &context.db))); + trace.message(&format!("Find! {}", &target.to_string(&context.db))); for (label, formula) in context.clone().hypotheses().iter() { - context.message(&format!("Trying {}", DisplayPair(formula, &context.db))); - match self.check_match(context, &target, &*formula, |_subst| { + trace.message(&format!("Trying {}", formula.to_string(&context.db))); + match self.check_match(trace, context, &target, &*formula, |_subst| { Ok(ProofStep::hyp(*label, formula.clone())) }) { Ok(step) => { - context.exit(&format!("Matched hypothesis {}", DisplayPair(formula, &context.db))); return Ok(step); }, Err(e) => { - context.message(&format!("{:?}", e)); + trace.message(&format!("{:?}", e)); }, } } for (hyp, step) in context.clone().subgoals().iter() { - context.message(&format!("Trying {}", DisplayPair(hyp, &context.db))); - match self.check_match(context, &target, &*hyp, |_subst| { + trace.message(&format!("Trying {}", hyp.to_string(&context.db))); + match self.check_match(trace, context, &target, &*hyp, |_subst| { Ok(step.clone()) }) { Ok(step) => { - context.exit(&format!("Matched subgoal {}", DisplayPair(hyp, &context.db))); return Ok(step); }, Err(e) => { - context.message(&format!("{:?}", e)); + trace.message(&format!("{:?}", e)); }, } } - context.exit("Find: No match found"); Err(TacticsError::NoMatchFound) } } impl FindHyp { - fn check_match(&self, context: &Context, target: &Formula, formula: &Formula, make_proof_step: F) -> TacticsResult + fn check_match(&self, trace: &mut Trace, context: &Context, target: &Formula, formula: &Formula, make_proof_step: F) -> TacticsResult where F: Fn(&Box) -> TacticsResult { let mut subst = Substitutions::new(); formula.unify(&target, & mut subst)?; let step1 = make_proof_step(&Box::new(subst.clone()))?; let mut context2 = context.with_variables(&subst); context2.add_subgoal(step1.result().clone(), step1); - Ok(self.tactics.execute(&mut context2)?) + Ok(self.tactics.execute(trace, &mut context2)?) } } diff --git a/rumm/src/tactics/hypothesis.rs b/rumm/src/tactics/hypothesis.rs index bd211ac..72aecfd 100644 --- a/rumm/src/tactics/hypothesis.rs +++ b/rumm/src/tactics/hypothesis.rs @@ -6,6 +6,7 @@ use crate::parser::{Parse, Parser}; use crate::tactics::Tactics; use crate::tactics::TacticsError; use crate::tactics::TacticsResult; +use crate::trace::Trace; use core::fmt::Formatter; /// A tactics which matches the goal with one of the hypothesis, or a zero-hypothesis theorem or axiom @@ -35,11 +36,9 @@ impl Tactics for Hypothesis { "A tactics which matches the goal with one of the hypothesis.".to_string() } - fn execute(&self, context: &mut Context) -> TacticsResult { - context.enter("!"); + fn execute_intern(&self, _trace: &mut Trace, context: &mut Context) -> TacticsResult { for (label, hyp) in context.hypotheses().iter() { if context.goal().eq(hyp) { - context.exit("Matched hypothesis!"); return Ok(ProofStep::hyp( *label, context.goal().clone(), @@ -48,11 +47,9 @@ impl Tactics for Hypothesis { } for (hyp, step) in context.subgoals().iter() { if context.goal().eq(hyp) { - context.exit("Matched subgoal!"); return Ok(step.clone()); } } - context.exit("Hypothesis failed"); Err(TacticsError::NoMatchFound) } } diff --git a/rumm/src/tactics/match.rs b/rumm/src/tactics/match.rs index a492a9b..551129e 100644 --- a/rumm/src/tactics/match.rs +++ b/rumm/src/tactics/match.rs @@ -1,10 +1,10 @@ use crate::lang::TacticsExpression; +use crate::trace::Trace; use metamath_knife::Formula; use metamath_knife::formula::Substitutions; use crate::lang::FormulaExpression; use crate::context::Context; use crate::error::Result; -use crate::lang::DisplayPair; use crate::lang::{Db, Display}; use crate::parser::{Parse, Parser}; use crate::tactics::Tactics; @@ -44,15 +44,14 @@ impl Parse for Match { impl Tactics for Match { fn get_name(&self) -> String { - "try".to_string() + "match".to_string() } fn get_desc(&self) -> String { - "A tactics which tries a list of tactics until one of them produces a proof.".to_string() + "A tactics which tries matching against a list of templates until one of them produces a proof.".to_string() } - fn execute(&self, context: &mut Context) -> TacticsResult { - context.enter("Match"); + fn execute_intern(&self, trace: &mut Trace, context: &mut Context) -> TacticsResult { let model = self.target.evaluate(&context)?.substitute(context.variables()); // match &self.target { // FormulaExpression::Formula(formula) => formula.substitute(context.variables()), @@ -61,32 +60,30 @@ impl Tactics for Match { // .ok_or(TacticsError::Error)?.0, // unknown statement // }; - context.message(&format!("Target {}", DisplayPair(&model, &context.db))); + trace.message(&format!("Target {}", &model.to_string(&context.db))); // context.message(format!("{}", context.debug_formula(&model))); for m in self.matches.iter() { let m2 = m.0.substitute(context.variables()); - context.message(&format!("Trying {}", DisplayPair(&m2, &context.db))); + trace.message(&format!("Trying {}", &m2.to_string(&context.db))); // context.message(format!(" {}", context.debug_formula(&m2)))); let mut subst = Substitutions::new(); if let std::result::Result::Ok(_) = model.unify(&m2, &mut subst) { - context.message(&format!( + trace.message(&format!( "Matched {} with {}", - DisplayPair(&model, &context.db), - DisplayPair(&m2, &context.db) + &model.to_string(&context.db), + &m2.to_string(&context.db) )); let mut sub_context = context.with_variables(&subst); - match m.1.execute(&mut sub_context) { + match m.1.execute(trace, &mut sub_context) { Ok(step) => { - context.exit("Match successful"); return Ok(step); }, Err(e) => { - context.message(format!("{:?}", e).as_str()); + trace.message(format!("{:?}", e).as_str()); }, } } } - context.exit("-- Match failed --"); Err(TacticsError::NoMatchFound) } } diff --git a/rumm/src/tactics/mod.rs b/rumm/src/tactics/mod.rs index bfd9cc6..74e1bb8 100644 --- a/rumm/src/tactics/mod.rs +++ b/rumm/src/tactics/mod.rs @@ -28,6 +28,7 @@ use crate::context::Context; use crate::lang::Display; use crate::lang::ProofStep; use crate::parser::Parse; +use crate::trace::Trace; pub type TacticsResult = std::result::Result; @@ -59,7 +60,16 @@ pub trait Tactics: Parse + Display { fn get_name(&self) -> String; //fn arg_types(&self) -> fn get_desc(&self) -> String; - fn execute(&self, context: &mut Context) -> TacticsResult; + fn execute_intern(&self, trace: &mut Trace, context: &mut Context) -> TacticsResult; + fn execute (&self, trace: &mut Trace, context: &mut Context) -> TacticsResult where Self: Sized { + let mut trace1 = trace.enter(context, &self.to_string(&context.db)); + let result = self.execute_intern(&mut trace1, context); + match result { + TacticsResult::Ok(_) => { trace.exit(trace1, &format!("{} : success", &self.to_string(&context.db))); } + TacticsResult::Err(_) => { trace.exit(trace1, &format!("{} : failure", &self.to_string(&context.db))); } // "{e:?}" + } + result + } /// Return a Arc to the tactics. fn into_arc(self) -> Arc diff --git a/rumm/src/tactics/skipped.rs b/rumm/src/tactics/skipped.rs index cc835b2..32b8c5e 100644 --- a/rumm/src/tactics/skipped.rs +++ b/rumm/src/tactics/skipped.rs @@ -5,6 +5,7 @@ use crate::parser::{Parse, Parser}; use crate::tactics::Tactics; use crate::tactics::TacticsError; use crate::tactics::TacticsResult; +use crate::trace::Trace; use core::fmt::Formatter; /// A special tactics, representing a proof not completed yet, marked by a question mark. @@ -34,9 +35,7 @@ impl Tactics for Skipped { "The \"to do\" tactics, leaving the goal unproven and filling in the Metamath proof with an incomplete, question mark proof.".to_string() } - fn execute(&self, context: &mut Context) -> TacticsResult { - context.enter("Skip"); - context.exit("Skipped!"); + fn execute_intern(&self, _trace: &mut Trace, _context: &mut Context) -> TacticsResult { Err(TacticsError::Skipped) } } diff --git a/rumm/src/tactics/subgoal.rs b/rumm/src/tactics/subgoal.rs index c86410e..d8262a8 100644 --- a/rumm/src/tactics/subgoal.rs +++ b/rumm/src/tactics/subgoal.rs @@ -5,6 +5,7 @@ use crate::lang::{Db, Display}; use crate::parser::{Parse, Parser}; use crate::tactics::Tactics; use crate::tactics::TacticsResult; +use crate::trace::Trace; use core::fmt::Formatter; /// A tactics which first solves subgoal, @@ -49,19 +50,16 @@ impl Tactics for Subgoal { "A tactics which allows to insert a subgoal, prove it or assume it, and then move forward with the rest of the proof.".to_string() } - fn execute(&self, mut context: &mut Context) -> TacticsResult { - context.enter("Subgoal"); + fn execute_intern(&self, trace: &mut Trace, mut context: &mut Context) -> TacticsResult { let subgoal = self.subgoal.evaluate(context)?.substitute(context.variables()); let mut context1 = context.with_goal(subgoal.clone()); - match self.tactics1.execute(&mut context1) { + match self.tactics1.execute(trace, &mut context1) { Ok(step1) => { context.add_subgoal(subgoal, step1); - let res = self.tactics2.execute(&mut context); - context.exit("Subgoal complete"); + let res = self.tactics2.execute(trace, &mut context); res }, Err(e) => { - context.exit("-- Subgoal failed --"); Err(e) } } diff --git a/rumm/src/tactics/try.rs b/rumm/src/tactics/try.rs index fcec340..8af03ab 100644 --- a/rumm/src/tactics/try.rs +++ b/rumm/src/tactics/try.rs @@ -6,6 +6,7 @@ use crate::parser::{Parse, Parser, OptionalTactics}; use crate::tactics::Tactics; use crate::tactics::TacticsError; use crate::tactics::TacticsResult; +use crate::trace::Trace; use core::fmt::Formatter; /// A tactics which tries a list of tactics until one of them produces a proof. @@ -43,20 +44,17 @@ impl Tactics for Try { "A tactics which tries a list of tactics until one of them produces a proof.".to_string() } - fn execute(&self, context: &mut Context) -> TacticsResult { - context.enter("Try"); + fn execute_intern(&self, trace: &mut Trace, context: &mut Context) -> TacticsResult { for t in &self.tactics { - match t.execute(context) { + match t.execute(trace, context) { Ok(step) => { - context.exit("Try Successful"); return Ok(step); }, Err(e) => { - context.message(format!("{:?}",e).as_str()); + trace.message(format!("{:?}",e).as_str()); }, } } - context.exit("-- Try Failed --"); Err(TacticsError::NoMatchFound) } } diff --git a/rumm/src/tactics/use_script_tactics.rs b/rumm/src/tactics/use_script_tactics.rs index 1da20d4..5b1fdb9 100644 --- a/rumm/src/tactics/use_script_tactics.rs +++ b/rumm/src/tactics/use_script_tactics.rs @@ -6,6 +6,7 @@ use crate::parser::{Parse, Parser}; use crate::tactics::Tactics; use crate::tactics::TacticsError; use crate::tactics::TacticsResult; +use crate::trace::Trace; use core::fmt::Formatter; /// Calling a script tactics. @@ -40,17 +41,14 @@ impl Tactics for UseScriptTactics { "A tactics for calling a tactics defined in the Rumm script.".to_string() } - fn execute(&self, context: &mut Context) -> TacticsResult { - context.enter(&format!("Use {}", self.name)); + fn execute_intern(&self, trace: &mut Trace, context: &mut Context) -> TacticsResult { if let Some(tactics_definition) = context.clone().get_tactics_definition(self.name.clone()) { let mut sub_context = context.without_variables(); tactics_definition.add_variables(&mut sub_context, &self.parameters)?; - let res = tactics_definition.execute(&mut sub_context); - context.exit(&format!("{} complete", self.name)); + let res = tactics_definition.execute(trace, &mut sub_context); res } else { - context.exit(&format!("{} failed", self.name)); Err(TacticsError::UnknownTactics(self.name.to_string())) } } diff --git a/rumm/src/trace.rs b/rumm/src/trace.rs new file mode 100644 index 0000000..e03eca5 --- /dev/null +++ b/rumm/src/trace.rs @@ -0,0 +1,78 @@ +use std::{fs::File, io::{BufWriter, Write}}; +use crate::{lang::Display, context::Context}; +use serde_json::json; + +pub struct Trace { + pub label: String, + children: Option>, + depth: usize, +} + +impl Trace { + pub fn new() -> Self { + Trace { + label: "Entry".to_string(), + children: None, + depth: 0, + } + } + + pub fn message(&mut self, message: &str) { + //println!("{:indent$}{message}", "", indent = self.depth); + self.children.get_or_insert(vec![]).push(Trace{label: message.to_string(), children: None, depth: self.depth + 1}); + } + + #[must_use] + pub fn enter(&mut self, context: &Context, message: &str) -> Self { + self.message(&format!("Proving {}", context.goal().to_string(&context.db))); + self.message(&format!(">> {message}")); + Trace { + label: message.to_string(), + children: None, + depth: self.depth +1, + } + } + + pub fn exit(&mut self, trace: Trace, message: &str) { + self.children.get_or_insert(vec![]).push(trace); + self.message(&format!("<< {message}")); + } + + pub fn dump(&self) { + println!("{:indent$}{label}", "", indent = self.depth, label = self.label); // + for sub_trace in self.children.iter().flatten() { + sub_trace.dump(); + } + } + + pub fn write_json(&self, f: &mut impl Write) -> std::io::Result<()> { + for trace in self.children.iter().flatten() { + f.write((format!("{{ name: {}, children: [", json!(trace.label).to_string())).as_bytes())?; + trace.write_json(f)?; + f.write(format!("] }},\n").as_bytes())?; + } + Ok(()) + } + + pub fn export_js_tree(&self, theorem: &str) { + let mut f = BufWriter::new(File::create(format!("{theorem}.html")).expect("Unable to create file")); + f.write(" + + + + + + +
+ + ".as_bytes())}) + .expect("Error while writing file"); + } +} + diff --git a/vendor/treeview/LICENSE b/vendor/treeview/LICENSE new file mode 100644 index 0000000..7472f77 --- /dev/null +++ b/vendor/treeview/LICENSE @@ -0,0 +1,21 @@ +The MIT License (MIT) + +Copyright (c) 2014 Justin Chmura + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. \ No newline at end of file diff --git a/vendor/treeview/dist/treeview.min.css b/vendor/treeview/dist/treeview.min.css new file mode 100644 index 0000000..455afb9 --- /dev/null +++ b/vendor/treeview/dist/treeview.min.css @@ -0,0 +1,2 @@ +.tree-leaf{position:relative}.tree-leaf .tree-child-leaves{display:block;margin-left:15px}.tree-leaf .hidden{display:none;visibility:hidden}.tree-leaf .tree-expando{background:#ddd;border-radius:3px;cursor:pointer;float:left;height:10px;line-height:10px;position:relative;text-align:center;top:5px;width:10px}.tree-leaf .tree-expando:hover{background:#aaa}.tree-leaf .tree-leaf-text{cursor:pointer;float:left;margin-left:5px}.tree-leaf .tree-leaf-text:hover{color:#00f}.tree-leaf .tree-leaf-content:after,.tree-leaf .tree-leaf-content:before{content:" ";display:table}.tree-leaf .tree-leaf-content:after{clear:both} +/*# sourceMappingURL=treeview.min.css.map */ \ No newline at end of file diff --git a/vendor/treeview/dist/treeview.min.css.map b/vendor/treeview/dist/treeview.min.css.map new file mode 100644 index 0000000..ccc3f22 --- /dev/null +++ b/vendor/treeview/dist/treeview.min.css.map @@ -0,0 +1 @@ +{"version":3,"sources":["src/treeview.css"],"names":[],"mappings":"AAAA,WAAa,SAAU,SACvB,8BAAgC,QAAS,MAAO,YAAa,KAC7D,mBAAqB,QAAS,KAET,WAAY,OADjC,yBAA2B,WAAY,KAAM,cAAe,IAAK,OAAQ,QAAS,MAAO,KAAM,OAAQ,KAAM,YAAa,KAAM,SAAU,SAAU,WAAY,OAAQ,IAAK,IAAK,MAAO,KAEzL,+BAAiC,WAAY,KAC7C,2BAA6B,OAAQ,QAAS,MAAO,KAAM,YAAa,IACxE,iCAAmC,MAAO,KACJ,oCAAtC,qCAA4E,QAAS,IAAK,QAAS,MACnG,oCAAsC,MAAO"} \ No newline at end of file diff --git a/vendor/treeview/dist/treeview.min.js b/vendor/treeview/dist/treeview.min.js new file mode 100644 index 0000000..b3cc4ef --- /dev/null +++ b/vendor/treeview/dist/treeview.min.js @@ -0,0 +1,2 @@ +!function(e){"use strict";!function(t,n){"function"==typeof e&&e.amd?e(n):"object"==typeof exports?module.exports=n():t.TreeView=n()}(window,function(){return function(){function e(e){try{return e instanceof HTMLElement}catch(t){return"object"==typeof e&&1===e.nodeType&&"object"==typeof e.style&&"object"==typeof e.ownerDocument}}function t(e,t,n){var a,o=e.length;for(a=0;a-1))throw new Error(n+" event cannot be found on TreeView.");e.handlers[n]&&e.handlers[n]instanceof Array&&t(e.handlers[n],function(e){window.setTimeout(function(){e.callback.apply(e.context,a)},0)})}function a(a){var o,r=e(a.node)?a.node:document.getElementById(a.node),l=[],d=function(e){var n=document.createElement("div"),a=document.createElement("div"),o=document.createElement("div"),r=document.createElement("div");if(n.setAttribute("class","tree-leaf"),a.setAttribute("class","tree-leaf-content"),a.setAttribute("data-item",JSON.stringify(e)),o.setAttribute("class","tree-leaf-text"),o.textContent=e.name,r.setAttribute("class","tree-expando "+(e.expanded?"expanded":"")),r.textContent=e.expanded?"-":"+",a.appendChild(r),a.appendChild(o),n.appendChild(a),e.children&&e.children.length>0){var l=document.createElement("div");l.setAttribute("class","tree-child-leaves"),t(e.children,function(e){var t=d(e);l.appendChild(t)}),e.expanded||l.classList.add("hidden"),n.appendChild(l)}else r.classList.add("hidden");return n};t(a.data,function(e){l.push(d.call(a,e))}),r.innerHTML=l.map(function(e){return e.outerHTML}).join(""),o=function(e){var t=(e.target||e.currentTarget).parentNode,o=JSON.parse(t.getAttribute("data-item")),r=t.parentNode.querySelector(".tree-child-leaves");r?r.classList.contains("hidden")?a.expand(t,r):a.collapse(t,r):n(a,"select",{target:e,data:o})},t(r.querySelectorAll(".tree-leaf-text"),function(e){e.onclick=o}),t(r.querySelectorAll(".tree-expando"),function(e){e.onclick=o})}function o(e,t){this.handlers={},this.node=t,this.data=e,a(this)}var r=["expand","expandAll","collapse","collapseAll","select"];return o.prototype.expand=function(e,t,a){e.querySelector(".tree-expando").textContent="-",t.classList.remove("hidden"),a||n(this,"expand",{target:e,leaves:t})},o.prototype.expandAll=function(){var e=this;t(document.getElementById(e.node).querySelectorAll(".tree-expando"),function(t){var n=t.parentNode,a=n.parentNode.querySelector(".tree-child-leaves");n&&a&&n.hasAttribute("data-item")&&e.expand(n,a,!0)}),n(this,"expandAll",{})},o.prototype.collapse=function(e,t,a){e.querySelector(".tree-expando").textContent="+",t.classList.add("hidden"),a||n(this,"collapse",{target:e,leaves:t})},o.prototype.collapseAll=function(){var e=this;t(document.getElementById(e.node).querySelectorAll(".tree-expando"),function(t){var n=t.parentNode,a=n.parentNode.querySelector(".tree-child-leaves");n&&a&&n.hasAttribute("data-item")&&e.collapse(n,a,!0)}),n(this,"collapseAll",{})},o.prototype.on=function(e,t,n){if(!(r.indexOf(e)>-1))throw new Error(e+" is not supported by TreeView.");this.handlers[e]||(this.handlers[e]=[]),this.handlers[e].push({callback:t,context:n})},o.prototype.off=function(e,t){var n,a=!1;this.handlers[e]instanceof Array&&(this.handlers[e].forEach(function(e,o){n=o,e.callback!==t||a||(a=!0)}),a&&this.handlers[e].splice(n,1))},o}()})}(window.define); +//# sourceMappingURL=treeview.min.js.map \ No newline at end of file diff --git a/vendor/treeview/dist/treeview.min.js.map b/vendor/treeview/dist/treeview.min.js.map new file mode 100644 index 0000000..267839a --- /dev/null +++ b/vendor/treeview/dist/treeview.min.js.map @@ -0,0 +1 @@ +{"version":3,"sources":["../src/treeview.js"],"names":["define","root","factory","amd","exports","module","TreeView","window","isDOMElement","obj","HTMLElement","e","nodeType","style","ownerDocument","forEach","arr","callback","scope","i","len","length","call","emit","instance","name","args","slice","arguments","events","indexOf","Error","handlers","Array","handle","setTimeout","apply","context","render","self","click","container","node","document","getElementById","leaves","renderLeaf","item","leaf","createElement","content","text","expando","setAttribute","JSON","stringify","textContent","expanded","appendChild","children","child","childLeaf","classList","add","data","push","innerHTML","map","outerHTML","join","parent","target","currentTarget","parentNode","parse","getAttribute","querySelector","contains","expand","collapse","querySelectorAll","onclick","this","prototype","skipEmit","remove","expandAll","hasAttribute","collapseAll","on","off","index","found","splice"],"mappings":"CAAC,SAAUA,GACT,cAEC,SAAUC,EAAMC,GACO,kBAAXF,IAAyBA,EAAOG,IACzCH,EAAOE,GACqB,gBAAZE,SAChBC,OAAOD,QAAUF,IAEjBD,EAAKK,SAAWJ,KAElBK,OAAQ,WACR,MAAQ,YAgBT,QAASC,GAAaC,GACjB,IACE,MAAOA,aAAeC,aACtB,MAAOC,GAGL,MAAsB,gBAARF,IAAqC,IAAjBA,EAAIG,UAAuC,gBAAdH,GAAII,OAAmD,gBAAtBJ,GAAIK,eAU1G,QAASC,GAAQC,EAAKC,EAAUC,GAC9B,GAAIC,GAAGC,EAAMJ,EAAIK,MACjB,KAAKF,EAAI,EAAGA,EAAIC,EAAKD,GAAK,EACxBF,EAASK,KAAKJ,EAAOF,EAAIG,GAAIA,GAQjC,QAASI,GAAKC,EAAUC,GACtB,GAAIC,MAAUC,MAAML,KAAKM,UAAW,EACpC,MAAIC,EAAOC,QAAQL,IAAS,GAS1B,KAAM,IAAIM,OAAMN,EAAO,sCARnBD,GAASQ,SAASP,IAASD,EAASQ,SAASP,YAAiBQ,QAChElB,EAAQS,EAASQ,SAASP,GAAO,SAAUS,GACzC3B,OAAO4B,WAAW,WAChBD,EAAOjB,SAASmB,MAAMF,EAAOG,QAASX,IACrC,KAWX,QAASY,GAAOC,GACd,GACiBC,GADbC,EAAYjC,EAAa+B,EAAKG,MAAQH,EAAKG,KAAOC,SAASC,eAAeL,EAAKG,MAC/EG,KACAC,EAAa,SAAUC,GACzB,GAAIC,GAAOL,SAASM,cAAc,OAC9BC,EAAUP,SAASM,cAAc,OACjCE,EAAOR,SAASM,cAAc,OAC9BG,EAAUT,SAASM,cAAc,MAYrC,IAVAD,EAAKK,aAAa,QAAS,aAC3BH,EAAQG,aAAa,QAAS,qBAC9BH,EAAQG,aAAa,YAAaC,KAAKC,UAAUR,IACjDI,EAAKE,aAAa,QAAS,kBAC3BF,EAAKK,YAAcT,EAAKtB,KACxB2B,EAAQC,aAAa,QAAS,iBAAmBN,EAAKU,SAAW,WAAa,KAC9EL,EAAQI,YAAcT,EAAKU,SAAW,IAAM,IAC5CP,EAAQQ,YAAYN,GACpBF,EAAQQ,YAAYP,GACpBH,EAAKU,YAAYR,GACbH,EAAKY,UAAYZ,EAAKY,SAAStC,OAAS,EAAG,CAC7C,GAAIsC,GAAWhB,SAASM,cAAc,MACtCU,GAASN,aAAa,QAAS,qBAC/BtC,EAAQgC,EAAKY,SAAU,SAAUC,GAC/B,GAAIC,GAAYf,EAAWc,EAC3BD,GAASD,YAAYG,KAElBd,EAAKU,UACRE,EAASG,UAAUC,IAAI,UAEzBf,EAAKU,YAAYC,OAEjBP,GAAQU,UAAUC,IAAI,SAExB,OAAOf,GAGTjC,GAAQwB,EAAKyB,KAAM,SAAUjB,GAC3BF,EAAOoB,KAAKnB,EAAWxB,KAAKiB,EAAMQ,MAEpCN,EAAUyB,UAAYrB,EAAOsB,IAAI,SAAUnB,GACzC,MAAOA,GAAKoB,YACXC,KAAK,IAER7B,EAAQ,SAAU7B,GAChB,GAAI2D,IAAU3D,EAAE4D,QAAU5D,EAAE6D,eAAeC,WACvCT,EAAOV,KAAKoB,MAAMJ,EAAOK,aAAa,cACtC9B,EAASyB,EAAOG,WAAWG,cAAc,qBACzC/B,GACEA,EAAOiB,UAAUe,SAAS,UAC5BtC,EAAKuC,OAAOR,EAAQzB,GAEpBN,EAAKwC,SAAST,EAAQzB,GAGxBtB,EAAKgB,EAAM,UACTgC,OAAQ5D,EACRqD,KAAMA,KAKZjD,EAAQ0B,EAAUuC,iBAAiB,mBAAoB,SAAUtC,GAC/DA,EAAKuC,QAAUzC,IAEjBzB,EAAQ0B,EAAUuC,iBAAiB,iBAAkB,SAAUtC,GAC7DA,EAAKuC,QAAUzC,IAUnB,QAASlC,GAAS0D,EAAMtB,GACtBwC,KAAKlD,YACLkD,KAAKxC,KAAOA,EACZwC,KAAKlB,KAAOA,EACZ1B,EAAO4C,MAzIT,GAAIrD,IACF,SACA,YACA,WACA,cACA,SA2OF,OA/FAvB,GAAS6E,UAAUL,OAAS,SAAUpC,EAAMG,EAAQuC,GACpC1C,EAAKkC,cAAc,iBACzBpB,YAAc,IACtBX,EAAOiB,UAAUuB,OAAO,UACpBD,GACJ7D,EAAK2D,KAAM,UACTX,OAAQ7B,EACRG,OAAQA,KAIZvC,EAAS6E,UAAUG,UAAY,WAC7B,GAAI/C,GAAO2C,IAEXnE,GADY4B,SAASC,eAAeL,EAAKG,MAAMsC,iBAAiB,iBACjD,SAAUtC,GACvB,GAAI4B,GAAS5B,EAAK+B,WACd5B,EAASyB,EAAOG,WAAWG,cAAc,qBACzCN,IAAUzB,GAAUyB,EAAOiB,aAAa,cAC1ChD,EAAKuC,OAAOR,EAAQzB,GAAQ,KAGhCtB,EAAK2D,KAAM,iBAQb5E,EAAS6E,UAAUJ,SAAW,SAAUrC,EAAMG,EAAQuC,GACtC1C,EAAKkC,cAAc,iBACzBpB,YAAc,IACtBX,EAAOiB,UAAUC,IAAI,UACjBqB,GACJ7D,EAAK2D,KAAM,YACTX,OAAQ7B,EACRG,OAAQA,KAMZvC,EAAS6E,UAAUK,YAAc,WAC/B,GAAIjD,GAAO2C,IAEXnE,GADY4B,SAASC,eAAeL,EAAKG,MAAMsC,iBAAiB,iBACjD,SAAUtC,GACvB,GAAI4B,GAAS5B,EAAK+B,WACd5B,EAASyB,EAAOG,WAAWG,cAAc,qBACzCN,IAAUzB,GAAUyB,EAAOiB,aAAa,cAC1ChD,EAAKwC,SAAST,EAAQzB,GAAQ,KAGlCtB,EAAK2D,KAAM,mBASb5E,EAAS6E,UAAUM,GAAK,SAAUhE,EAAMR,EAAUC,GAChD,KAAIW,EAAOC,QAAQL,IAAS,GAS1B,KAAM,IAAIM,OAAMN,EAAO,iCARlByD,MAAKlD,SAASP,KACjByD,KAAKlD,SAASP,OAEhByD,KAAKlD,SAASP,GAAMwC,MAClBhD,SAAUA,EACVoB,QAASnB,KAYfZ,EAAS6E,UAAUO,IAAM,SAAUjE,EAAMR,GACvC,GAAI0E,GAAOC,GAAQ,CACfV,MAAKlD,SAASP,YAAiBQ,SACjCiD,KAAKlD,SAASP,GAAMV,QAAQ,SAAUmB,EAAQf,GAC5CwE,EAAQxE,EACJe,EAAOjB,WAAaA,GAAa2E,IACnCA,GAAQ,KAGRA,GACFV,KAAKlD,SAASP,GAAMoE,OAAOF,EAAO,KAKjCrF,QAGXC,OAAOP","file":"dist/treeview.min.js"} \ No newline at end of file diff --git a/vendor/treeview/src/treeview.js b/vendor/treeview/src/treeview.js new file mode 100644 index 0000000..14dc75a --- /dev/null +++ b/vendor/treeview/src/treeview.js @@ -0,0 +1,259 @@ +(function (define) { + 'use strict'; + + (function (root, factory) { + if (typeof define === 'function' && define.amd) { + define(factory); + } else if (typeof exports === 'object') { + module.exports = factory(); + } else { + root.TreeView = factory(); + } + }(window, function () { + return (function () { + + /** List of events supported by the tree view */ + var events = [ + 'expand', + 'expandAll', + 'collapse', + 'collapseAll', + 'select' + ]; + + /** + * A utilite function to check to see if something is a DOM object + * @param {object} Object to test + * @returns {boolean} If the object is a DOM object + */ + function isDOMElement(obj) { + try { + return obj instanceof HTMLElement; + } catch (e) { + // Some browsers don't support using the HTMLElement so some extra + // checks are needed. + return typeof obj === 'object' && obj.nodeType === 1 && typeof obj.style === 'object' && typeof obj.ownerDocument === 'object'; + } + } + + /** + * A forEach that will work with a NodeList and generic Arrays + * @param {array|NodeList} arr The array to iterate over + * @param {function} callback Function that executes for each element. First parameter is element, second is index + * @param {object} The context to execute callback with + */ + function forEach(arr, callback, scope) { + var i, len = arr.length; + for (i = 0; i < len; i += 1) { + callback.call(scope, arr[i], i); + } + } + + /** + * Emit an event from the tree view + * @param {string} name The name of the event to emit + */ + function emit(instance, name) { + var args = [].slice.call(arguments, 2); + if (events.indexOf(name) > -1) { + if (instance.handlers[name] && instance.handlers[name] instanceof Array) { + forEach(instance.handlers[name], function (handle) { + window.setTimeout(function () { + handle.callback.apply(handle.context, args); + }, 0); + }); + } + } else { + throw new Error(name + ' event cannot be found on TreeView.'); + } + } + + /** + * Renders the tree view in the DOM + */ + function render(self) { + var container = isDOMElement(self.node) ? self.node : document.getElementById(self.node); + var leaves = [], click; + var renderLeaf = function (item) { + var leaf = document.createElement('div'); + var content = document.createElement('div'); + var text = document.createElement('div'); + var expando = document.createElement('div'); + + leaf.setAttribute('class', 'tree-leaf'); + content.setAttribute('class', 'tree-leaf-content'); + content.setAttribute('data-item', JSON.stringify(item)); + text.setAttribute('class', 'tree-leaf-text'); + text.textContent = item.name; + expando.setAttribute('class', 'tree-expando ' + (item.expanded ? 'expanded' : '')); + expando.textContent = item.expanded ? '-' : '+'; + content.appendChild(expando); + content.appendChild(text); + leaf.appendChild(content); + if (item.children && item.children.length > 0) { + var children = document.createElement('div'); + children.setAttribute('class', 'tree-child-leaves'); + forEach(item.children, function (child) { + var childLeaf = renderLeaf(child); + children.appendChild(childLeaf); + }); + if (!item.expanded) { + children.classList.add('hidden'); + } + leaf.appendChild(children); + } else { + expando.classList.add('hidden'); + } + return leaf; + }; + + forEach(self.data, function (item) { + leaves.push(renderLeaf.call(self, item)); + }); + container.innerHTML = leaves.map(function (leaf) { + return leaf.outerHTML; + }).join(''); + + click = function (e) { + var parent = (e.target || e.currentTarget).parentNode; + var data = JSON.parse(parent.getAttribute('data-item')); + var leaves = parent.parentNode.querySelector('.tree-child-leaves'); + if (leaves) { + if (leaves.classList.contains('hidden')) { + self.expand(parent, leaves); + } else { + self.collapse(parent, leaves); + } + } else { + emit(self, 'select', { + target: e, + data: data + }); + } + }; + + forEach(container.querySelectorAll('.tree-leaf-text'), function (node) { + node.onclick = click; + }); + forEach(container.querySelectorAll('.tree-expando'), function (node) { + node.onclick = click; + }); + } + + /** + * @constructor + * @property {object} handlers The attached event handlers + * @property {object} data The JSON object that represents the tree structure + * @property {DOMElement} node The DOM element to render the tree in + */ + function TreeView(data, node) { + this.handlers = {}; + this.node = node; + this.data = data; + render(this); + } + + /** + * Expands a leaflet by the expando or the leaf text + * @param {DOMElement} node The parent node that contains the leaves + * @param {DOMElement} leaves The leaves wrapper element + */ + TreeView.prototype.expand = function (node, leaves, skipEmit) { + var expando = node.querySelector('.tree-expando'); + expando.textContent = '-'; + leaves.classList.remove('hidden'); + if (skipEmit) { return; } + emit(this, 'expand', { + target: node, + leaves: leaves + }); + }; + + TreeView.prototype.expandAll = function () { + var self = this; + var nodes = document.getElementById(self.node).querySelectorAll('.tree-expando'); + forEach(nodes, function (node) { + var parent = node.parentNode; + var leaves = parent.parentNode.querySelector('.tree-child-leaves'); + if (parent && leaves && parent.hasAttribute('data-item')) { + self.expand(parent, leaves, true); + } + }); + emit(this, 'expandAll', {}); + }; + + /** + * Collapses a leaflet by the expando or the leaf text + * @param {DOMElement} node The parent node that contains the leaves + * @param {DOMElement} leaves The leaves wrapper element + */ + TreeView.prototype.collapse = function (node, leaves, skipEmit) { + var expando = node.querySelector('.tree-expando'); + expando.textContent = '+'; + leaves.classList.add('hidden'); + if (skipEmit) { return; } + emit(this, 'collapse', { + target: node, + leaves: leaves + }); + }; + + /** + */ + TreeView.prototype.collapseAll = function () { + var self = this; + var nodes = document.getElementById(self.node).querySelectorAll('.tree-expando'); + forEach(nodes, function (node) { + var parent = node.parentNode; + var leaves = parent.parentNode.querySelector('.tree-child-leaves'); + if (parent && leaves && parent.hasAttribute('data-item')) { + self.collapse(parent, leaves, true); + } + }); + emit(this, 'collapseAll', {}); + }; + + /** + * Attach an event handler to the tree view + * @param {string} name Name of the event to attach + * @param {function} callback The callback to execute on the event + * @param {object} scope The context to call the callback with + */ + TreeView.prototype.on = function (name, callback, scope) { + if (events.indexOf(name) > -1) { + if (!this.handlers[name]) { + this.handlers[name] = []; + } + this.handlers[name].push({ + callback: callback, + context: scope + }); + } else { + throw new Error(name + ' is not supported by TreeView.'); + } + }; + + /** + * Deattach an event handler from the tree view + * @param {string} name Name of the event to deattach + * @param {function} callback The function to deattach + */ + TreeView.prototype.off = function (name, callback) { + var index, found = false; + if (this.handlers[name] instanceof Array) { + this.handlers[name].forEach(function (handle, i) { + index = i; + if (handle.callback === callback && !found) { + found = true; + } + }); + if (found) { + this.handlers[name].splice(index, 1); + } + } + }; + + return TreeView; + }()); + })); + }(window.define)); \ No newline at end of file From fbbbaadb79fec66668e1fdbcbe730ad9cb1191f8 Mon Sep 17 00:00:00 2001 From: Thierry Arnoux Date: Sun, 12 Mar 2023 21:43:45 +0100 Subject: [PATCH 2/2] Update apply.rs --- rumm/src/tactics/apply.rs | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) diff --git a/rumm/src/tactics/apply.rs b/rumm/src/tactics/apply.rs index e23c617..e236f1c 100644 --- a/rumm/src/tactics/apply.rs +++ b/rumm/src/tactics/apply.rs @@ -1,5 +1,5 @@ -use crate::lang::DisplayPair; use crate::lang::SubstitutionListExpression; +use crate::trace::Trace; use metamath_knife::formula::Substitutions; use crate::lang::TacticsExpression; use crate::context::Context; @@ -66,35 +66,32 @@ impl Tactics for Apply { "A tactics which applies a given theorem to prove the goal.".to_string() } - fn execute(&self, context: &mut Context) -> TacticsResult { - context.enter(&format!("Apply {}", DisplayPair(&self.theorem, &context.db))); + fn execute_intern(&self, trace: &mut Trace, context: &mut Context) -> TacticsResult { // context.db.debug_formula(context.goal()); - // println!(" vars:{}", DisplayPair(context.variables(), &context.db)); + // println!(" vars:{}", context.variables().to_string(&context.db)); let mut my_subst = Substitutions::default(); for (l,f) in self.substitutions.evaluate(context)?.iter() { - context.message(format!("Subst: {} {}", DisplayPair(l, &context.db), DisplayPair(f, &context.db)).as_str()); + trace.message(format!("Subst: {} {}", l.to_string(&context.db), f.to_string(&context.db)).as_str()); my_subst.insert(*l, f.substitute(context.variables())); } let theorem = self.theorem.evaluate(context)?; - context.message(&format!(" Attempting apply {}", DisplayPair(&theorem, &context.db))); + trace.message(&format!(" Attempting apply {}", &theorem.to_string(&context.db))); if let Some((theorem_formula, hyps)) = context.get_theorem_formulas(theorem) { let mut subst = Substitutions::new(); if let Err(e) = context.goal().unify(&theorem_formula, &mut subst) { - context.exit("Apply statement doesn't match"); return Err(e.into()); } subst.extend(&my_subst); - // context.message(&format!(" subst:{}", DisplayPair(&subst, &context.db))); + // trace1.message(&format!(" subst:{}", &subst.to_string(&context.db))); if hyps.len() == self.subtactics.len() { let mut substeps = vec![]; // TODO check count! for ((_hyp_label, hyp_formula), tactics) in hyps.iter().zip(&self.subtactics) { let sub_goal = hyp_formula.substitute(&subst); let mut sub_context = context.with_goal(sub_goal); - substeps.push(tactics.execute(&mut sub_context)?); + substeps.push(tactics.execute(trace, &mut sub_context)?); } - context.exit("Apply Unification success"); Ok(ProofStep::apply( theorem, substeps.into_boxed_slice(), @@ -102,11 +99,9 @@ impl Tactics for Apply { Box::new(subst), )) } else { - context.exit("Apply Hyps don't match"); Err(TacticsError::WrongHypCount(self.subtactics.len(), hyps.len())) } } else { - context.exit("Unknown theorem label"); Err(TacticsError::UnknownLabel(theorem)) } }