Add a trace mechanism to save the trace tree in a more readable way.

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"}

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<String, Arc<dyn Tactics>>,
     formula_variables: HashMap<String, Formula>,
     subst_variables: HashMap<String, Substitutions>,
-    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,
         }
     }
 

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
 	}
 }
 

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;

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<ProofStep, TacticsError> {
+    pub fn prove(&self, db: Db, tactics_definitions: TacticsDict, trace: &mut Trace) -> std::result::Result<ProofStep, TacticsError> {
         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))

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<Expression>) -> TacticsResult<()> {

rumm/src/main.rs

@@ -1,6 +1,7 @@
 //! A Metamath Proof Assistant
 
 mod context;
+mod trace;
 pub mod error;
 mod lang;
 pub mod parser;

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));
                 }
             }
         }

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,47 +66,42 @@ 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(),
                     context.goal().clone(),
                     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))
         }
     }

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<F>(&self, context: &Context, target: &Formula, formula: &Formula, make_proof_step: F) -> TacticsResult
-        where F: Fn(&Box<Substitutions>) -> TacticsResult {
+    fn check_match<F>(&self, trace: &mut Trace, context: &Context, target: &Formula, formula: &Formula, make_proof_step: F) -> TacticsResult
+        where F: Fn(&Box<Substitutions>, &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)?)
     }
 }