Class CoqImporter

java.lang.Object

org.episteme.core.mathematics.loaders.logic.CoqImporter

All Implemented Interfaces:

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

public class CoqImporter
extends Object
implements FormalSystemImporter

Importer for Coq Proof Assistant files (.v).

Parses Coq vernacular files and extracts:

• Module definitions
• Axioms and Parameters
• Theorems and Lemmas
• Definitions

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
CoqImporter()

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

CoqImporter

public CoqImporter()

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"])