public abstract class AbstractProblemLoader
extends java.lang.Object
This class provides the basic functionality to load something in KeY.
The loading process is done in the current Thread
and
no user interaction is required.
The basic usage of this class is to instantiate a new
SingleThreadProblemLoader
or ProblemLoader
instance which should load the file configured by the constructor's arguments.
The next step is to call load()
which does the loading process and
tries to instantiate a proof and to apply rules again if possible. The result
of the loading process is available via the getter methods.
Modifier and Type | Class and Description |
---|---|
static class |
AbstractProblemLoader.ReplayResult |
Modifier and Type | Field and Description |
---|---|
private boolean |
askUiToSelectAProofObligationIfNotDefinedByLoadedFile
true to call UserInterfaceControl#selectProofObligation(InitConfig)
if no Proof is defined by the loaded proof or
false otherwise which still allows to work with the loaded InitConfig . |
private java.io.File |
bootClassPath
An optional boot class path.
|
private java.util.List<java.io.File> |
classPath
The optional class path entries to use.
|
private ProblemLoaderControl |
control
The
ProblemLoaderControl to use. |
private EnvInput |
envInput
The instantiated
EnvInput which describes the file to load. |
private java.io.File |
file
The file or folder to load.
|
private boolean |
forceNewProfileOfNewProofs
true
profileOfNewProofs will be used as Profile of new proofs, false Profile specified by problem file will be used for new proofs. |
private java.util.List<java.io.File> |
includes
The global includes to use.
|
private InitConfig |
initConfig
The instantiated
InitConfig which provides access to the loaded source elements and specifications. |
private static java.util.Map<Pair<java.lang.Integer,java.lang.Integer>,java.lang.String> |
mismatchErrors
Maps internal error codes of the parser to human readable strings.
|
private static java.util.Map<java.lang.Integer,java.lang.String> |
missedErrors |
private java.util.Properties |
poPropertiesToForce
Some optional additional
Properties for the PO. |
private ProblemInitializer |
problemInitializer
The instantiated
ProblemInitializer used during the loading process. |
private Profile |
profileOfNewProofs
|
private Proof |
proof
The instantiate proof or
null if no proof was instantiated during loading process. |
private AbstractProblemLoader.ReplayResult |
result
The
AbstractProblemLoader.ReplayResult if available or null otherwise. |
Constructor and Description |
---|
AbstractProblemLoader(java.io.File file,
java.util.List<java.io.File> classPath,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
Profile profileOfNewProofs,
boolean forceNewProfileOfNewProofs,
ProblemLoaderControl control,
boolean askUiToSelectAProofObligationIfNotDefinedByLoadedFile,
java.util.Properties poPropertiesToForce)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
protected EnvInput |
createEnvInput()
Instantiates the
EnvInput which represents the file to load. |
protected InitConfig |
createInitConfig()
Creates the
InitConfig . |
protected ProblemInitializer |
createProblemInitializer()
Instantiates the
ProblemInitializer to use. |
protected ProofAggregate |
createProof(IPersistablePO.LoadedPOContainer poContainer)
Creates a
Proof for the given IPersistablePO.LoadedPOContainer and
tries to apply rules again. |
protected IPersistablePO.LoadedPOContainer |
createProofObligationContainer()
Creates a
IPersistablePO.LoadedPOContainer if available which contains
the ProofOblInput for which a Proof should be instantiated. |
java.io.File |
getBootClassPath()
Returns the optional boot class path.
|
java.util.List<java.io.File> |
getClassPath()
Returns the optional class path entries to use.
|
EnvInput |
getEnvInput()
Returns the instantiated
EnvInput which describes the file to load. |
java.io.File |
getFile()
Returns the file or folder to load.
|
InitConfig |
getInitConfig()
Returns the instantiated
InitConfig which provides access to the loaded source elements and specifications. |
ProblemInitializer |
getProblemInitializer()
Returns the instantiated
ProblemInitializer used during the loading process. |
Proof |
getProof()
Returns the instantiate proof or
null if no proof was instantiated during loading process. |
Pair<java.lang.String,Location> |
getProofScript() |
AbstractProblemLoader.ReplayResult |
getResult()
Returns the
AbstractProblemLoader.ReplayResult if available. |
boolean |
hasProofScript()
Run proof script if it is present in the input data.
|
void |
load()
Executes the loading process and tries to instantiate a proof
and to re-apply rules on it if possible.
|
Pair<java.lang.String,Location> |
readProofScript() |
protected ProblemLoaderException |
recoverParserErrorMessage(java.lang.Exception e)
Tries to recover parser errors and make them human-readable,
rewrap them into ProblemLoaderExceptions.
|
private AbstractProblemLoader.ReplayResult |
replayProof(Proof proof) |
private java.lang.Throwable |
unwrap(java.lang.Throwable e)
Find first 'non-wrapper' exception type in cause chain.
|
private final java.io.File file
private final java.util.List<java.io.File> classPath
private final java.io.File bootClassPath
private final java.util.List<java.io.File> includes
private final ProblemLoaderControl control
ProblemLoaderControl
to use.private final Profile profileOfNewProofs
private final boolean askUiToSelectAProofObligationIfNotDefinedByLoadedFile
true
to call UserInterfaceControl#selectProofObligation(InitConfig)
if no Proof
is defined by the loaded proof or
false
otherwise which still allows to work with the loaded InitConfig
.private final java.util.Properties poPropertiesToForce
Properties
for the PO.private final boolean forceNewProfileOfNewProofs
profileOfNewProofs
will be used as Profile
of new proofs, false
Profile
specified by problem file will be used for new proofs.private ProblemInitializer problemInitializer
ProblemInitializer
used during the loading process.private InitConfig initConfig
InitConfig
which provides access to the loaded source elements and specifications.private Proof proof
null
if no proof was instantiated during loading process.private AbstractProblemLoader.ReplayResult result
AbstractProblemLoader.ReplayResult
if available or null
otherwise.private static final java.util.Map<Pair<java.lang.Integer,java.lang.Integer>,java.lang.String> mismatchErrors
private static final java.util.Map<java.lang.Integer,java.lang.String> missedErrors
public AbstractProblemLoader(java.io.File file, java.util.List<java.io.File> classPath, java.io.File bootClassPath, java.util.List<java.io.File> includes, Profile profileOfNewProofs, boolean forceNewProfileOfNewProofs, ProblemLoaderControl control, boolean askUiToSelectAProofObligationIfNotDefinedByLoadedFile, java.util.Properties poPropertiesToForce)
file
- The file or folder to load.classPath
- The optional class path entries to use.bootClassPath
- An optional boot class path.includes
- Optional includes to consider.profileOfNewProofs
- The Profile
to use for new Proof
s.forceNewProfileOfNewProofs
- true profileOfNewProofs
will be used as Profile
of new proofs, false
Profile
specified by problem file will be used for new proofs.control
- The ProblemLoaderControl
to use.askUiToSelectAProofObligationIfNotDefinedByLoadedFile
- true
to call UserInterfaceControl#selectProofObligation(InitConfig)
if no Proof
is defined by the loaded proof or false
otherwise which still allows to work with the loaded InitConfig
.public void load() throws ProofInputException, java.io.IOException, ProblemLoaderException
ProofInputException
- Occurred Exception.java.io.IOException
- Occurred Exception.ProblemLoaderException
- Occurred Exception.private java.lang.Throwable unwrap(java.lang.Throwable e)
protected ProblemLoaderException recoverParserErrorMessage(java.lang.Exception e)
protected EnvInput createEnvInput() throws java.io.IOException
EnvInput
which represents the file to load.EnvInput
.java.io.IOException
- Occurred Exception.protected ProblemInitializer createProblemInitializer()
ProblemInitializer
to use.registerProof
- Register loaded Proof
ProblemInitializer
to use.protected InitConfig createInitConfig() throws ProofInputException
InitConfig
.InitConfig
.ProofInputException
- Occurred Exception.protected IPersistablePO.LoadedPOContainer createProofObligationContainer() throws java.io.IOException
IPersistablePO.LoadedPOContainer
if available which contains
the ProofOblInput
for which a Proof
should be instantiated.IPersistablePO.LoadedPOContainer
or null
if not available.java.io.IOException
- Occurred Exception.protected ProofAggregate createProof(IPersistablePO.LoadedPOContainer poContainer) throws ProofInputException
Proof
for the given IPersistablePO.LoadedPOContainer
and
tries to apply rules again.poContainer
- The IPersistablePO.LoadedPOContainer
to instantiate a Proof
for.Proof
.ProofInputException
- Occurred Exception.public boolean hasProofScript()
true
iff there is a proof script to runpublic Pair<java.lang.String,Location> readProofScript() throws ProofInputException
ProofInputException
public Pair<java.lang.String,Location> getProofScript() throws ProblemLoaderException
ProblemLoaderException
private AbstractProblemLoader.ReplayResult replayProof(Proof proof) throws ProofInputException, ProblemLoaderException
public java.io.File getFile()
public java.util.List<java.io.File> getClassPath()
public java.io.File getBootClassPath()
public EnvInput getEnvInput()
EnvInput
which describes the file to load.EnvInput
which describes the file to load.public ProblemInitializer getProblemInitializer()
ProblemInitializer
used during the loading process.ProblemInitializer
used during the loading process.public InitConfig getInitConfig()
InitConfig
which provides access to the loaded source elements and specifications.InitConfig
which provides access to the loaded source elements and specifications.public Proof getProof()
null
if no proof was instantiated during loading process.null
if no proof was instantiated during loading process.public AbstractProblemLoader.ReplayResult getResult()
AbstractProblemLoader.ReplayResult
if available.AbstractProblemLoader.ReplayResult
or null
if not available.