From 278cf1dcd2e8174cbef831a545db738047585007 Mon Sep 17 00:00:00 2001
From: Thierry Arnoux <5831830+tirix@users.noreply.github.com>
Date: Sun, 29 Oct 2023 16:00:26 +0100
Subject: [PATCH] Add check STS option

---
 src/main.rs       |  8 ++++++++
 src/sts.rs        | 17 +++++++++++++++++
 src/sts_parser.rs | 13 +++++++++----
 3 files changed, 34 insertions(+), 4 deletions(-)

diff --git a/src/main.rs b/src/main.rs
index c52c5a5..e901418 100644
--- 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
index 2d51af9..7ab4584 100644
--- 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
index 962e6c2..67c573e 100644
--- 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)
 }