Formula extraction for syntax breakdown

tirix · Nov 11, 2023 · 6cf4e2c · 6cf4e2c
1 parent 5b2a3be
commit 6cf4e2c
Show file tree

Hide file tree

Showing 2 changed files with 46 additions and 26 deletions.
diff --git a/src/statement.rs b/src/statement.rs
@@ -5,6 +5,7 @@ use crate::uni::UnicodeRenderer;
 use handlebars::Handlebars;
 use metamath_knife::comment_parser::CommentItem;
 use metamath_knife::comment_parser::CommentParser;
+use metamath_knife::grammar::FormulaToken;
 use metamath_knife::proof::ProofTreeArray;
 use metamath_knife::statement::as_str;
 use metamath_knife::statement::StatementRef;
@@ -86,29 +87,55 @@ impl ExpressionRenderer {
         use_provables: bool,
     ) -> Result<String, String> {
         match self {
-            ExpressionRenderer::Ascii => self.render_formula(
-                database
-                    .stmt_parse_result()
-                    .get_formula(sref)
-                    .ok_or("Formula not found")?,
-                database,
-                use_provables,
-            ),
+            ExpressionRenderer::Ascii => self.render_formula(&self.get_formula(sref, database, use_provables)?, database, use_provables),
             ExpressionRenderer::Unicode(uni) => uni.render_statement(sref),
             #[cfg(feature = "sts")]
-            ExpressionRenderer::Sts(sts) => sts.render_statement(sref, use_provables),
+            ExpressionRenderer::Sts(sts) => sts.render_formula(&self.get_formula(sref, database, use_provables)?, use_provables)
+        }
+    }
+
+    #[inline]
+    fn get_formula(
+        &self,
+        sref: &StatementRef,
+        database: &Database,
+        use_provables: bool,
+    ) -> Result<Formula, String> {
+        if use_provables {
+            database
+            .stmt_parse_result()
+            .get_formula(sref)
+            .ok_or("Unknown statement".into()).cloned()
+        } else {
+            let nset = database.name_result();
+            let grammar = database.grammar_result();
+            let mut tokens = sref.math_iter();
+            let _typecode = nset.get_atom(&tokens.next().unwrap());
+            grammar.parse_formula(
+                &mut tokens.map(|t| {
+                    Ok(FormulaToken {
+                        symbol: nset.get_atom(&t),
+                        span: metamath_knife::Span::NULL,
+                    })
+                }),
+                &grammar.typecodes(),
+                true,
+                nset,
+            )
+            .map_err(|e| format!("Could not parse formula (GF): {}", e))
         }
     }
 
     fn render_formula(
         &self,
         formula: &Formula,
         database: &Database,
-        #[allow(unused_variables)] use_provables: bool,
+        use_provables: bool,
     ) -> Result<String, String> {
         match self {
             ExpressionRenderer::Ascii => {
-                Ok(format!("<pre>{}</pre>", formula.as_ref(database)).replace("wff ", " |- "))
+                let s = format!("<pre>{}</pre>", formula.as_ref(database));
+                Ok(if use_provables { s.replace("wff ", " |- ") } else { s })
             }
             ExpressionRenderer::Unicode(uni) => uni.render_formula(formula),
             #[cfg(feature = "sts")]

diff --git a/src/sts.rs b/src/sts.rs
@@ -3,7 +3,6 @@ use metamath_knife::formula::Substitutions;
 use metamath_knife::formula::TypeCode;
 use metamath_knife::grammar::FormulaToken;
 use metamath_knife::statement::as_str;
-use metamath_knife::statement::StatementRef;
 use metamath_knife::Database;
 use metamath_knife::Formula;
 use metamath_knife::StatementType;
@@ -131,21 +130,15 @@ impl StsDefinition {
         } else {
             formula.get_typecode()
         };
+        let mut mathml = self.format(typecode, formula)?;
+        if !use_provables && typecode != grammar.provable_typecode() {
+            mathml = format!("<mrow><mo mathcolor=#CCC>{}</mo> {}</mrow>", 
+                as_str(self.database.name_result().atom_name(typecode)),
+                self.format(formula.get_typecode(), formula)?
+            );
+        }
         let display = self.display.clone();
-        Ok(display.replace("###", &self.format(typecode, formula)?))
-    }
-
-    pub fn render_statement(
-        &self,
-        sref: &StatementRef,
-        use_provables: bool,
-    ) -> Result<String, String> {
-        let formula = self
-            .database
-            .stmt_parse_result()
-            .get_formula(sref)
-            .ok_or("Unknown statement")?;
-        self.render_formula(formula, use_provables)
+        Ok(display.replace("###", &mathml))
     }
 
     pub fn check(&self) {