|
PMII - JAVA-Packages - Principia Mathematica II | |||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: INNER | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object | +--com.meyling.principia.argument.AbstractArgument | +--com.meyling.principia.argument.AbstractDynamicArgumentList | +--com.meyling.principia.module.Module
Main data object of this project. A Module
is like an
chapter of a mathematical textbook. It is organized in
Paragraph
s that could contain Abbreviation
s,
Axiom
s or Proposition
s. It could reference to
other Module
s.
Constructor Summary | |
Module(Argument[] arguments)
Constructs a module. |
|
Module(Argument[] arguments,
ModuleAddress moduleAddress)
Constructs a module and verifies it. |
Method Summary | |
void |
addAbbreviation(String abbreviationLabel,
Abbreviation abbreviation,
Module module)
Add abbreviation with label abbreviationLabel . |
void |
addAxiom(String axiomLabel,
Axiom axiom,
Module module)
Add axiom with label axiomLabel . |
void |
addRuleDeclaration(String ruleLabel,
RuleDeclaration declaration,
Module module)
Declare a new rule. |
void |
addSentence(String sentenceLabel,
Sentence sentence,
Module module)
Add sentence with label sentenceLabel . |
void |
check()
Verifies this module. |
void |
checkLabel(String label)
Test if label is already known. |
Argument |
create(Argument[] arguments)
Create a new Argument with given arguments. |
Abbreviation |
getAbbreviation(String abbreviationLabel)
Get the abbreviation with label abbreviationLabel . |
Axiom |
getAxiom(String axiomLabel)
Get the axiom with label axiomLabel . |
ImportList |
getImports()
Get all imports of this module. |
Argument |
getLabeledArgument(String label)
Get the sentence or axiom with label label . |
Formula |
getLabeledFormula(String label)
Get the sentence or axiom formula with label label . |
Module |
getLabelModule(String label)
Get module the label was defined in. |
Map |
getLabels()
Get a map of all known labels. |
ModuleAddress |
getModuleAddress()
Get the ModuleAddress where this module is from. |
String |
getModuleFileName()
Get the full module name, with version and rule version, but without path. |
ParagraphList |
getParagraphs()
Get all paragraphs of this module. |
Proposition[] |
getPropositions()
Get all propositions of this module. |
RuleDeclaration |
getRuleDeclaration(Class rule)
Get the declaration for a rule. |
RuleDeclaration |
getRuleDeclaration(String ruleLabel)
Get the declaration for a rule. |
String |
getRuleDeclarationLabel(Class rule)
Get the declaration for a rule. |
Version |
getRuleVersion()
Get the rule version this module could use maximal. |
Sentence |
getSentence(String sentenceLabel)
Get the sentence with label sentenceLabel . |
UsedbyList |
getUsedby()
Get all usedby references of this module. |
boolean |
isRuleDeclared(Class rule)
Is a certain rule declared? |
void |
setModuleAddress(ModuleAddress moduleAddress)
Set the URL where this module is from. |
void |
setRuleVersion(Version version)
Set the rule version this module could use maximal. |
String |
toString()
Get the argument in String form. |
Methods inherited from class com.meyling.principia.argument.AbstractDynamicArgumentList |
add, copy, getArgument, getArgumentSize, insert, remove, replace |
Methods inherited from class com.meyling.principia.argument.AbstractArgument |
containsPatternVariables, equals, getHighestNumber, getPatternVariables, getReplacementParents, getSearchParents, hashCode, matches, matches, replace, replace, replace, replaceMatches |
Methods inherited from class java.lang.Object |
|
Methods inherited from interface com.meyling.principia.argument.Argument |
containsPatternVariables, copy, equals, getArgument, getArgumentSize, getPatternVariables, getReplacementParents, getSearchParents, hashCode, matches, matches, replace, replace, replace, replaceMatches |
Constructor Detail |
public Module(Argument[] arguments) throws ArgumentException
arguments
- see ArgumentException below- Throws:
ArgumentException
- if the arguments are not of the
form Header
, ImportList
?,
UsedbyList
? and {@ParagraphList} (in this
order, the question marks mark arguments as optional).
public Module(Argument[] arguments, ModuleAddress moduleAddress) throws ArgumentException, ParsingException
arguments
- see ArgumentException belowmoduleAddress
- the URL where the module was loaded from- Throws:
ArgumentException
- if the arguments are not of the
form Header
, ImportList
?,
UsedbyList
? and {@ParagraphList} (in this
order, the question marks mark arguments as optional).
Also thrown if the module has any mathematical
verification problem.ParsingException
- if ModuleContext.loadModule()
failed
Method Detail |
public void check() throws ArgumentException, ParsingException
ArgumentException
- if the module has any mathematical
verification problem.ParsingException
- if ModuleContext.loadModule()
failedpublic final Abbreviation getAbbreviation(String abbreviationLabel) throws IllegalArgumentException
abbreviationLabel
.abbreviationLabel
- reference to abbreviationIllegalArgumentException
- if such an abbreviation
doesn't existpublic final void addAbbreviation(String abbreviationLabel, Abbreviation abbreviation, Module module) throws IllegalArgumentException
abbreviationLabel
.abbreviationLabel
- reference to abbreviationabbreviation
- abbreviationIllegalArgumentException
- if such an label
already existspublic final Axiom getAxiom(String axiomLabel) throws IllegalArgumentException
axiomLabel
.axiomLabel
- reference to axiomIllegalArgumentException
- if such an axiom
doesn't existpublic final void addAxiom(String axiomLabel, Axiom axiom, Module module) throws IllegalArgumentException
axiomLabel
.axiomLabel
- reference to axiomaxiom
- axiomIllegalArgumentException
- if such an label
already existspublic final Sentence getSentence(String sentenceLabel) throws IllegalArgumentException
sentenceLabel
.sentenceLabel
- reference to sentenceIllegalArgumentException
- if such an sentence
doesn't existpublic final void addSentence(String sentenceLabel, Sentence sentence, Module module) throws IllegalArgumentException
sentenceLabel
.sentenceLabel
- reference to sentencesentence
- sentenceIllegalArgumentException
- if such an label
already existspublic final RuleDeclaration getRuleDeclaration(Class rule) throws IllegalArgumentException
rule
- look for this rule classIllegalArgumentException
- if such a declaration
doesn't existpublic final RuleDeclaration getRuleDeclaration(String ruleLabel) throws IllegalArgumentException
ruleLabel
- look for this ruleIllegalArgumentException
- if such a declaration
doesn't existpublic final String getRuleDeclarationLabel(Class rule) throws IllegalArgumentException
rule
- look for this rule classIllegalArgumentException
- if such a declaration
doesn't existpublic final boolean isRuleDeclared(Class rule)
rule
- look for this rule classpublic final void addRuleDeclaration(String ruleLabel, RuleDeclaration declaration, Module module) throws IllegalArgumentException, ArgumentException
ruleLabel
- label of this ruledeclaration
- declaration of a rulemodule
- in this module the rule is declaredArgumentException
- if the check failedIllegalArgumentException
- if such an label
already existspublic final Formula getLabeledFormula(String label) throws IllegalArgumentException
label
.label
- reference to an axiom or a propositionIllegalArgumentException
- if such an reference
doesn't existpublic final Argument getLabeledArgument(String label) throws IllegalArgumentException
label
.label
- reference to an axiom or a propositionIllegalArgumentException
- if such an reference
doesn't existpublic final void checkLabel(String label) throws IllegalArgumentException
IllegalArgumentException
- if such an label
already existspublic final Module getLabelModule(String label) throws IllegalArgumentException
label
- reference name to look forIllegalArgumentException
- if such an label
already existspublic final void setModuleAddress(ModuleAddress moduleAddress) throws ArgumentException
address
- URL of this moduleArgumentException
- if URL doesn't end how
the specification sayspublic final String getModuleFileName()
public final ModuleAddress getModuleAddress()
ModuleAddress
where this module is from.public final Map getLabels()
public final ImportList getImports()
public final UsedbyList getUsedby()
public final ParagraphList getParagraphs()
public final Proposition[] getPropositions()
public final Version getRuleVersion()
public final void setRuleVersion(Version version) throws ArgumentException
version
- maximal rule versionArgumentException
- if setting failedpublic final Argument create(Argument[] arguments) throws ArgumentException
Argument
create
in interface Argument
create
in class AbstractDynamicArgumentList
com.meyling.principia.argument.Argument
arguments
- with these arguments the operator should
be createdArgumentException
- if creation failedpublic final String toString()
Argument
String
form.toString
in interface Argument
toString
in class AbstractDynamicArgumentList
com.meyling.principia.argument.Argument
|
PMII - JAVA-Packages - Principia Mathematica II | |||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: INNER | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
©left GNU General Public Licence All Rights Reserved. |