Fix/improve STS check

* axiom/definition display * page titles
tirix · Oct 29, 2023 · 8ae52bf · 8ae52bf
1 parent 436c35c
commit 8ae52bf
Show file tree

Hide file tree

Showing 4 changed files with 55 additions and 16 deletions.
diff --git a/src/statement.hbs b/src/statement.hbs
@@ -1,6 +1,7 @@
 <!DOCTYPE html>
 <html>
 	<head>
+		<title>{{label}}</title>
 		<link rel="shortcut icon" href="/static/favicon.ico" type="image/x-icon">
 		<link rel="stylesheet" href="/static/metamath.css">
 		<link rel="preconnect" href="https://fonts.googleapis.com">

diff --git a/src/statement.rs b/src/statement.rs
@@ -115,19 +115,29 @@ impl ExpressionRenderer {
         self,
         proof_tree: &ProofTreeArray,
         tree_index: usize,
-        #[allow(unused_variables)] use_provables: bool,
+        use_provables: bool,
     ) -> Result<String, String> {
         match self {
             ExpressionRenderer::Ascii => Ok(format!(
                 "<pre> |- {}</pre>",
                 &String::from_utf8_lossy(&proof_tree.exprs[tree_index])
             )),
-            ExpressionRenderer::Unicode(uni) => uni.render_formula(
-                &ExpressionRenderer::as_formula(&uni.database, proof_tree, tree_index)?,
-            ),
+            ExpressionRenderer::Unicode(uni) => {
+                uni.render_formula(&ExpressionRenderer::as_formula(
+                    &uni.database,
+                    proof_tree,
+                    tree_index,
+                    use_provables,
+                )?)
+            }
             #[cfg(feature = "sts")]
             ExpressionRenderer::Sts(sts) => sts.render_formula(
-                &ExpressionRenderer::as_formula(&sts.database, proof_tree, tree_index)?,
+                &ExpressionRenderer::as_formula(
+                    &sts.database,
+                    proof_tree,
+                    tree_index,
+                    use_provables,
+                )?,
                 use_provables,
             ),
         }
@@ -146,18 +156,28 @@ impl ExpressionRenderer {
         database: &Database,
         proof_tree: &ProofTreeArray,
         tree_index: usize,
+        use_provables: bool,
     ) -> Result<Formula, String> {
         let formula_string = String::from_utf8_lossy(&proof_tree.exprs[tree_index]);
         let nset = database.name_result();
         let grammar = database.grammar_result();
-        let provable_symbol = as_str(nset.atom_name(grammar.provable_typecode()));
-        let formula = grammar
-            .parse_string(
-                format!("{} {}", provable_symbol, formula_string.trim()).as_str(),
-                nset,
-            )
-            .map_err(|diag| format!("{} - Could not parse formula: {:?}", formula_string, diag));
-        formula
+        let typecodes = if use_provables {
+            Box::new([grammar.provable_typecode()])
+        } else {
+            grammar.typecodes()
+        };
+        typecodes
+            .iter()
+            .find_map(|tc| {
+                grammar
+                    .parse_string(
+                        format!("{} {}", as_str(nset.atom_name(*tc)), formula_string.trim())
+                            .as_str(),
+                        nset,
+                    )
+                    .ok()
+            })
+            .ok_or_else(|| format!("{} - Could not parse formula", formula_string))
     }
 }
 

diff --git a/src/sts.rs b/src/sts.rs
@@ -1,6 +1,7 @@
 use metamath_knife::formula::Label;
 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;
@@ -148,11 +149,27 @@ impl StsDefinition {
     }
 
     pub fn check(&self) {
-        let stmt_parse = self.database.stmt_parse_result();
+        let provable = self.database.grammar_result().provable_typecode();
+        let nset = self.database.name_result();
         for sref in self.database.statements() {
             if sref.statement_type() == StatementType::Axiom {
-                if let Some(formula) = stmt_parse.get_formula(&sref) {
-                    if let Err(error) = self.format(formula.get_typecode(), formula) {
+                let mut tokens = sref.math_iter();
+                let typecode = nset.get_atom(&tokens.next().unwrap());
+                if typecode != provable {
+                    let formula = self
+                        .database
+                        .grammar_result()
+                        .parse_formula(
+                            &mut tokens.map(|t| FormulaToken {
+                                symbol: nset.get_atom(&t),
+                                span: metamath_knife::Span::NULL,
+                            }),
+                            &[typecode],
+                            false,
+                            nset,
+                        )
+                        .unwrap();
+                    if let Err(error) = self.format(typecode, &formula) {
                         eprintln!("{}", error);
                     }
                 }

diff --git a/src/toc.hbs b/src/toc.hbs
@@ -1,6 +1,7 @@
 <!DOCTYPE html>
 <html>
 	<head>
+		<title>{{name}}</title>
 		<link rel="shortcut icon" href="/static/favicon.ico" type="image/x-icon">
 		<link rel="stylesheet" href="/static/metamath.css">
 		<link rel="preconnect" href="https://fonts.googleapis.com">