Class MetamathImporter

java.lang.Object

org.episteme.core.mathematics.loaders.logic.MetamathImporter

All Implemented Interfaces:

ResourceIO<Map<String,Object>>, ResourceReader<Map<String,Object>>, FormalSystemImporter

public class MetamathImporter
extends Object
implements FormalSystemImporter

Importer for Metamath database files (.mm).

Parses Metamath databases and extracts:

• Constants ($c statements)
• Variables ($v statements)
• Axioms ($a statements)
• Provable statements ($p statements)

Since:

1.0

Author:

Silvere Martin-Michiellot, Gemini AI (Google DeepMind)

Nested Class Summary

Nested classes/interfaces inherited from interface FormalSystemImporter

FormalSystemImporter.ParseException

Constructor Summary

Constructors

Constructor	Description
MetamathImporter()

Method Summary

Modifier and Type	Method	Description
String[]	getSupportedExtensions()	Returns the file extensions this importer can handle.
Map<String,Object>	importSystem(Reader reader)	Imports a formal system from the specified reader.

Methods inherited from class Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface FormalSystemImporter

getCategory, getDescription, getLongDescription, getName, getResourcePath, getResourceType, getSupportedVersions, importSystem, importSystem, load

Methods inherited from interface ResourceIO

getExpectedResourceFiles, isFileBased, isOutput

Methods inherited from interface ResourceReader

isInput

Constructor Details

MetamathImporter

public MetamathImporter()

Method Details

importSystem

public Map<String,Object> importSystem(Reader reader)
                                throws IOException,
FormalSystemImporter.ParseException

Description copied from interface: FormalSystemImporter

Imports a formal system from the specified reader.

Specified by:

importSystem in interface FormalSystemImporter

Parameters:

reader - the reader to import from

Returns:

a map of module names to their axioms/theorems

Throws:

IOException - if an I/O error occurs

FormalSystemImporter.ParseException - if the input format is invalid

getSupportedExtensions

public String[] getSupportedExtensions()

Description copied from interface: FormalSystemImporter

Returns the file extensions this importer can handle.

Specified by:

getSupportedExtensions in interface FormalSystemImporter

Specified by:

getSupportedExtensions in interface ResourceIO<Map<String,Object>>

Returns:

array of file extensions (e.g., [".v", ".vo"])