Skip to content
Snippets Groups Projects
Commit f378f99e authored by Sebastian Krings's avatar Sebastian Krings
Browse files

Merge branch 'develop' into feature/units

parents 870d48aa c3435fa1
Branches
Tags
No related merge requests found
......@@ -4,20 +4,20 @@
<classpathentry exported="true" kind="lib" path="lib/dependencies/xmlpull-1.1.3.1.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/xpp3_min-1.1.4c.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/xstream-1.4.3.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/answerparser-2.4.8-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/bparser-2.4.8-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/cliparser-2.4.8-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/commons-lang-2.6.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/jgrapht-0.8.3.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/jsr305-1.3.9.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/ltlparser-2.4.8-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/parserbase-2.4.8-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/prologlib-2.4.8-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/unicode-2.4.8-SNAPSHOT.jar"/>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.6"/>
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry kind="src" path="src"/>
<classpathentry kind="src" path="test"/>
<classpathentry kind="con" path="org.eclipse.jdt.junit.JUNIT_CONTAINER/4"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/parserbase-2.4.12-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/answerparser-2.4.12-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/cliparser-2.4.12-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/prologlib-2.4.12-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/bparser-2.4.12-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/unicode-2.4.12-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/ltlparser-2.4.12-SNAPSHOT.jar"/>
<classpathentry kind="output" path="bin"/>
</classpath>
......@@ -70,7 +70,6 @@ Export-Package: com.thoughtworks.xstream,
de.prob.core.domainobjects,
de.prob.core.domainobjects.eval,
de.prob.core.domainobjects.ltl,
de.prob.core.domainobjects.ltl.unittests,
de.prob.core.internal,
de.prob.core.langdep,
de.prob.core.prolog,
......@@ -119,11 +118,11 @@ Bundle-ClassPath: .,
lib/dependencies/bparser-2.4.12-SNAPSHOT.jar,
lib/dependencies/cliparser-2.4.12-SNAPSHOT.jar,
lib/dependencies/commons-codec-1.6.jar,
lib/dependencies/parserbase-2.4.12-SNAPSHOT.jar,
lib/dependencies/commons-lang-2.6.jar,
lib/dependencies/jgrapht-0.8.3.jar,
lib/dependencies/jsr305-1.3.9.jar,
lib/dependencies/ltlparser-2.4.12-SNAPSHOT.jar,
lib/dependencies/parserbase-2.4.12-SNAPSHOT.jar,
lib/dependencies/prologlib-2.4.12-SNAPSHOT.jar,
lib/dependencies/unicode-2.4.12-SNAPSHOT.jar,
lib/dependencies/xmlpull-1.1.3.1.jar,
......
......@@ -64,8 +64,6 @@ public final class ContextTranslator extends AbstractComponentTranslator {
private final Map<String, ISCContext> depContext = new HashMap<String, ISCContext>();
private final List<ProofObligation> proofs = new ArrayList<ProofObligation>();
private final List<ClassifiedPragma> proofspragmas = new ArrayList<ClassifiedPragma>();
private final FormulaFactory ff;
private ITypeEnvironment te;
public static ContextTranslator create(final ISCContext context)
throws TranslationFailedException {
......@@ -94,21 +92,12 @@ public final class ContextTranslator extends AbstractComponentTranslator {
private ContextTranslator(final ISCContext context)
throws TranslationFailedException {
this.context = context;
ff = ((ISCContextRoot) context).getFormulaFactory();
try {
te = ((ISCContextRoot) context).getTypeEnvironment(ff);
} catch (RodinDBException e) {
final String message = "A Rodin exception occured during translation process. Original Exception: ";
throw new TranslationFailedException(context.getComponentName(),
message + e.getLocalizedMessage());
}
}
private void translate() throws RodinDBException {
if (context instanceof ISCContextRoot) {
ISCContextRoot context_root = (ISCContextRoot) context;
Assert.isTrue(context_root.getRodinFile().isConsistent());
te = context_root.getTypeEnvironment(ff);
} else if (context instanceof ISCInternalContext) {
ISCInternalContext context_internal = (ISCInternalContext) context;
......@@ -155,7 +144,8 @@ public final class ContextTranslator extends AbstractComponentTranslator {
String name = sequent.getDescription();
ArrayList<SequentSource> s = new ArrayList<SequentSource>(sources.length);
ArrayList<SequentSource> s = new ArrayList<SequentSource>(
sources.length);
for (IPOSource source : sources) {
IRodinElement srcElement = source.getSource();
......@@ -167,7 +157,8 @@ public final class ContextTranslator extends AbstractComponentTranslator {
ILabeledElement le = (ILabeledElement) srcElement;
s.add(new SequentSource(srcElement.getElementType(), le.getLabel()));
s.add(new SequentSource(srcElement.getElementType(), le
.getLabel()));
}
proofs.add(new ProofObligation(origin, s, name, discharged));
......@@ -315,6 +306,8 @@ public final class ContextTranslator extends AbstractComponentTranslator {
}
final PredicateVisitor visitor = new PredicateVisitor(
new LinkedList<String>());
final FormulaFactory ff = FormulaFactory.getDefault();
final ITypeEnvironment te = ff.makeTypeEnvironment();
element.getPredicate(ff, te).accept(visitor);
final PPredicate predicate = visitor.getPredicate();
list.add(predicate);
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment