Add check STS option

tirix · Oct 29, 2023 · 278cf1d · 278cf1d
1 parent 9a455b1
commit 278cf1d
Show file tree

Hide file tree

Showing 3 changed files with 34 additions and 4 deletions.
diff --git a/src/main.rs b/src/main.rs
@@ -68,6 +68,14 @@ fn command_args() -> ArgMatches {
                 .short('b')
                 .takes_value(true),
         )
+        .arg(
+            Arg::new("check_sts")
+                .help(
+                    "Check that all constructs defined in the database are covered by the STS file",
+                )
+                .long("check-sts")
+                .short('S'),
+        )
         .get_matches()
 }
 

diff --git a/src/sts.rs b/src/sts.rs
@@ -5,6 +5,7 @@ use metamath_knife::statement::as_str;
 use metamath_knife::statement::StatementRef;
 use metamath_knife::Database;
 use metamath_knife::Formula;
+use metamath_knife::StatementType;
 use std::collections::HashMap;
 use std::sync::Arc;
 
@@ -145,4 +146,20 @@ impl StsDefinition {
             .ok_or("Unknown statement")?;
         self.render_formula(formula, use_provables)
     }
+
+    pub fn check(&self) {
+        let stmt_parse = self.database.stmt_parse_result();
+        for sref in self.database.statements() {
+            match sref.statement_type() {
+                StatementType::Axiom => {
+                    if let Some(formula) = stmt_parse.get_formula(&sref) {
+                        if let Err(error) = self.format(formula.get_typecode(), formula) {
+                            eprintln!("{}", error);
+                        }
+                    }
+                }
+                _ => {}
+            }
+        }
+    }
 }
diff --git a/src/sts_parser.rs b/src/sts_parser.rs
@@ -147,9 +147,10 @@ impl StsDefinition {
         for directive in directives {
             match directive {
                 Directive::Comment => {}
-                Directive::Scheme((i, m, s)) => {
-                    schemes.push(StsScheme::parse(db.clone(), i, m, s)?);
-                }
+                Directive::Scheme((i, m, s)) => match StsScheme::parse(db.clone(), i, m, s) {
+                    Ok(scheme) => schemes.push(scheme),
+                    Err(error) => eprintln!("{}", error),
+                },
                 Directive::Command(c) => {
                     command = c.to_string();
                 }
@@ -180,5 +181,9 @@ pub fn parse_sts(db: Database, args: &ArgMatches, format: &str) -> Result<StsDef
     let filename = format!("{}{}-{}.mmts", path, name, format);
     let contents =
         read_to_string(filename).expect("Something went wrong reading the STS definition file");
-    StsDefinition::parse(db, contents)
+    let definition = StsDefinition::parse(db, contents)?;
+    if args.is_present("check_sts") {
+        definition.check();
+    }
+    Ok(definition)
 }