translator

de.prob.core/plugin.xml

@@ -4,6 +4,7 @@
    <extension-point id="de.prob.core.lifecycle" name="Lifecycle Events" schema="schema/de.prob.core.lifecycle.exsd"/>
    <extension-point id="de.prob.core.computation" name="Computation Events" schema="schema/de.prob.core.computation.exsd"/>
    <extension-point id="de.prob.core.animation" name="Animation Events" schema="schema/de.prob.core.animation.exsd"/>
+   <extension-point id="de.prob.translator" name="Translator Extensions" schema="schema/de.prob.translator.exsd"/>
    <extension
          point="de.prob.core.animation">
       <listener

de.prob.core/schema/de.prob.translator.exsd

+<?xml version='1.0' encoding='UTF-8'?>
+<!-- Schema file written by PDE -->
+<schema targetNamespace="de.prob.core" xmlns="http://www.w3.org/2001/XMLSchema">
+<annotation>
+      <appInfo>
+         <meta.schema plugin="de.prob.core" id="de.prob.translator" name="Translator Extensions"/>
+      </appInfo>
+      <documentation>
+         [Enter description of this extension point.]
+      </documentation>
+   </annotation>
+
+   <element name="extension">
+      <annotation>
+         <appInfo>
+            <meta.element />
+         </appInfo>
+      </annotation>
+      <complexType>
+         <sequence minOccurs="0" maxOccurs="unbounded">
+            <element ref="translator"/>
+         </sequence>
+         <attribute name="point" type="string" use="required">
+            <annotation>
+               <documentation>
+                  
+               </documentation>
+            </annotation>
+         </attribute>
+         <attribute name="id" type="string">
+            <annotation>
+               <documentation>
+                  
+               </documentation>
+            </annotation>
+         </attribute>
+         <attribute name="name" type="string">
+            <annotation>
+               <documentation>
+                  
+               </documentation>
+               <appInfo>
+                  <meta.attribute translatable="true"/>
+               </appInfo>
+            </annotation>
+         </attribute>
+      </complexType>
+   </element>
+
+   <element name="translator">
+      <complexType>
+         <attribute name="name" type="string">
+            <annotation>
+               <documentation>
+                  
+               </documentation>
+            </annotation>
+         </attribute>
+         <attribute name="class" type="string" use="required">
+            <annotation>
+               <documentation>
+                  
+               </documentation>
+               <appInfo>
+                  <meta.attribute kind="java" basedOn=":de.prob.core.translator.IExternalTranslator"/>
+               </appInfo>
+            </annotation>
+         </attribute>
+      </complexType>
+   </element>
+
+   <annotation>
+      <appInfo>
+         <meta.section type="since"/>
+      </appInfo>
+      <documentation>
+         [Enter the first release in which this extension point appears.]
+      </documentation>
+   </annotation>
+
+   <annotation>
+      <appInfo>
+         <meta.section type="examples"/>
+      </appInfo>
+      <documentation>
+         [Enter extension point usage example here.]
+      </documentation>
+   </annotation>
+
+   <annotation>
+      <appInfo>
+         <meta.section type="apiinfo"/>
+      </appInfo>
+      <documentation>
+         [Enter API information here.]
+      </documentation>
+   </annotation>
+
+   <annotation>
+      <appInfo>
+         <meta.section type="implementation"/>
+      </appInfo>
+      <documentation>
+         [Enter information about supplied implementation of this extension point.]
+      </documentation>
+   </annotation>
+
+
+</schema>

de.prob.core/src/de/prob/core/translator/IExternalTranslator.java

+package de.prob.core.translator;
+
+import de.prob.prolog.output.PrologTermOutput;
+
+public interface IExternalTranslator {
+	public void writeProlog(PrologTermOutput pto);
+}

de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java

@@ -26,6 +26,7 @@ import org.eventb.core.ISCInternalContext;
 import org.eventb.core.ISCMachineRoot;
 import org.eventb.core.ast.FormulaFactory;
 import org.eventb.core.ast.ITypeEnvironment;
+import org.eventb.core.ast.Predicate;
 import org.rodinp.core.IRodinFile;
 import org.rodinp.core.RodinDBException;
 
@@ -50,14 +51,13 @@ public final class ContextTranslator extends AbstractComponentTranslator {
 	private final AEventBContextParseUnit model = new AEventBContextParseUnit();
 	private final Map<String, ISCContext> depContext = new HashMap<String, ISCContext>();
 	private final FormulaFactory ff;
-
-	// Confined in the thread calling the factory method
 	private ITypeEnvironment te;
 
 	public static ContextTranslator create(final ISCContext context)
 			throws TranslationFailedException {
 		ContextTranslator contextTranslator = new ContextTranslator(context);
 		try {
+(new TheoryTranslator()).translate();
 			contextTranslator.translate();
 		} catch (RodinDBException e) {
 			final String message = "A Rodin exception occured during translation process. Possible cause: building aborted or still in progress. Please wait until building has finished before starting ProB. If this does not help, perform a clean and start ProB after building has finished. Original Exception: ";
@@ -74,27 +74,34 @@ public final class ContextTranslator extends AbstractComponentTranslator {
 	 * contains errors)
 	 * 
 	 * @param context
+	 * @throws TranslationFailedException
 	 * @throws RodinDBException
 	 */
-	private ContextTranslator(final ISCContext context) {
+	private ContextTranslator(final ISCContext context)
+			throws TranslationFailedException {
 		this.context = context;
-		ff = FormulaFactory.getDefault();
+		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;
 			ISCMachineRoot machine_root = (ISCMachineRoot) context_internal
 					.getRoot();
 			Assert.isTrue(machine_root.getRodinFile().isConsistent());
-			te = machine_root.getTypeEnvironment(ff);
 		}
 		translateContext();
-
 	}
 
 	public AEventBContextParseUnit getContextAST() {
@@ -237,7 +244,9 @@ public final class ContextTranslator extends AbstractComponentTranslator {
 			}
 			final PredicateVisitor visitor = new PredicateVisitor(
 					new LinkedList<String>());
-			element.getPredicate(ff, te).accept(visitor);
+
+			Predicate ppp = element.getPredicate(ff, te);
+			ppp.accept(visitor);
 			final PPredicate predicate = visitor.getPredicate();
 			list.add(predicate);
 			labelMapping.put(predicate, element);

de.prob.core/src/de/prob/eventb/translator/ExpressionVisitor.java

@@ -20,7 +20,10 @@ import org.eventb.core.ast.BoolExpression;
 import org.eventb.core.ast.BoundIdentDecl;
 import org.eventb.core.ast.BoundIdentifier;
 import org.eventb.core.ast.Expression;
+import org.eventb.core.ast.ExtendedExpression;
+import org.eventb.core.ast.ExtendedPredicate;
 import org.eventb.core.ast.Formula;
+import org.eventb.core.ast.FormulaFactory;
 import org.eventb.core.ast.FreeIdentifier;
 import org.eventb.core.ast.ISimpleVisitor;
 import org.eventb.core.ast.IntegerLiteral;
@@ -48,6 +51,8 @@ import de.be4.classicalb.core.parser.node.AEventBFirstProjectionV2Expression;
 import de.be4.classicalb.core.parser.node.AEventBIdentityExpression;
 import de.be4.classicalb.core.parser.node.AEventBSecondProjectionExpression;
 import de.be4.classicalb.core.parser.node.AEventBSecondProjectionV2Expression;
+import de.be4.classicalb.core.parser.node.AExtendedExprExpression;
+import de.be4.classicalb.core.parser.node.AExtendedPredPredicate;
 import de.be4.classicalb.core.parser.node.AFalseExpression;
 import de.be4.classicalb.core.parser.node.AFunctionExpression;
 import de.be4.classicalb.core.parser.node.AGeneralIntersectionExpression;
@@ -619,6 +624,33 @@ public class ExpressionVisitor extends SimpleVisitorAdapter implements // NOPMD
 		setExpression(setExtensionExpression);
 	}
 
+	@Override
+	public void visitExtendedExpression(ExtendedExpression expression) {
+		AExtendedExprExpression p = new AExtendedExprExpression();
+		String symbol = expression.getExtension().getSyntaxSymbol();
+		p.setIdentifier(new TIdentifierLiteral(symbol));
+		Expression[] expressions = expression.getChildExpressions();
+		List<PExpression> childExprs = new ArrayList<PExpression>();
+		for (Expression e : expressions) {
+			ExpressionVisitor v = new ExpressionVisitor(null);
+			e.accept(v);
+			childExprs.add(v.getExpression());
+		}
+		p.setExpressions(childExprs);
+		
+		Predicate[] childPredicates = expression.getChildPredicates();
+		List<PPredicate> childPreds = new ArrayList<PPredicate>();
+		for (Predicate pd : childPredicates) {
+			PredicateVisitor v = new PredicateVisitor(null);
+			pd.accept(v);
+			childPreds.add(v.getPredicate());
+		}
+		p.setPredicates(childPreds);
+		
+		setExpression(p);
+		
+	}
+
 	@SuppressWarnings("deprecation")
 	@Override
 	public void visitUnaryExpression(final UnaryExpression expression) { // NOPMD

de.prob.core/src/de/prob/eventb/translator/PredicateVisitor.java

@@ -15,6 +15,7 @@ import org.eventb.core.ast.AssociativePredicate;
 import org.eventb.core.ast.BinaryPredicate;
 import org.eventb.core.ast.BoundIdentDecl;
 import org.eventb.core.ast.Expression;
+import org.eventb.core.ast.ExtendedPredicate;
 import org.eventb.core.ast.Formula;
 import org.eventb.core.ast.ISimpleVisitor;
 import org.eventb.core.ast.LiteralPredicate;
@@ -31,6 +32,7 @@ import de.be4.classicalb.core.parser.node.ADisjunctPredicate;
 import de.be4.classicalb.core.parser.node.AEqualPredicate;
 import de.be4.classicalb.core.parser.node.AEquivalencePredicate;
 import de.be4.classicalb.core.parser.node.AExistentialQuantificationPredicate;
+import de.be4.classicalb.core.parser.node.AExtendedPredPredicate;
 import de.be4.classicalb.core.parser.node.AFalsePredicate;
 import de.be4.classicalb.core.parser.node.AFinitePredicate;
 import de.be4.classicalb.core.parser.node.AGreaterEqualPredicate;
@@ -50,6 +52,7 @@ import de.be4.classicalb.core.parser.node.AUnequalPredicate;
 import de.be4.classicalb.core.parser.node.AUniversalQuantificationPredicate;
 import de.be4.classicalb.core.parser.node.PExpression;
 import de.be4.classicalb.core.parser.node.PPredicate;
+import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
 import de.prob.eventb.translator.internal.SimpleVisitorAdapter;
 
 public class PredicateVisitor extends SimpleVisitorAdapter implements // NOPMD
@@ -403,4 +406,35 @@ public class PredicateVisitor extends SimpleVisitorAdapter implements // NOPMD
 		setPredicate(result);
 	}
 
+	@Override
+	public void visitExtendedPredicate(ExtendedPredicate predicate) {
+		AExtendedPredPredicate p = new AExtendedPredPredicate();
+		String symbol = predicate.getExtension().getSyntaxSymbol();
+		p.setIdentifier(new TIdentifierLiteral(symbol));
+
+		Expression[] expressions = predicate.getChildExpressions();
+		List<PExpression> childExprs = new ArrayList<PExpression>();
+		for (Expression e : expressions) {
+			ExpressionVisitor v = new ExpressionVisitor(null);
+			e.accept(v);
+			childExprs.add(v.getExpression());
+		}
+		p.setExpressions(childExprs);
+		
+		Predicate[] childPredicates = predicate.getChildPredicates();
+		List<PPredicate> childPreds = new ArrayList<PPredicate>();
+		for (Predicate pd : childPredicates) {
+			PredicateVisitor v = new PredicateVisitor(null);
+			pd.accept(v);
+			childPreds.add(v.getPredicate());
+		}
+		p.setPredicates(childPreds);
+		setPredicate(p);
+	}
+
+	
+	
+	
+	
+	
 }

de.prob.core/src/de/prob/eventb/translator/TranslatorFactory.java

@@ -33,6 +33,11 @@ public class TranslatorFactory {
 	 */
 	public static void translate(final IEventBRoot root,
 			final IPrologTermOutput pto) throws TranslationFailedException {
+		
+		
+		
+		
+		
 		if (root instanceof IMachineRoot) {
 			final ISCMachineRoot scRoot = ((IMachineRoot) root)
 					.getSCMachineRoot();

de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java

@@ -23,6 +23,7 @@ import org.eventb.core.IPOSource;
 import org.eventb.core.IPSRoot;
 import org.eventb.core.IPSStatus;
 import org.eventb.core.ISCAction;
+import org.eventb.core.ISCContextRoot;
 import org.eventb.core.ISCEvent;
 import org.eventb.core.ISCGuard;
 import org.eventb.core.ISCInternalContext;
@@ -77,13 +78,13 @@ public class ModelTranslator extends AbstractComponentTranslator {
 
 	private final ISCMachineRoot machine;
 	private final AEventBModelParseUnit model = new AEventBModelParseUnit();
-	private final FormulaFactory ff = FormulaFactory.getDefault();;
+	private final FormulaFactory ff;
+	private final ITypeEnvironment te;
 	private final IMachineRoot origin;
 	private final List<DischargedProof> proofs = new ArrayList<DischargedProof>();
 	// private final List<String> depContext = new ArrayList<String>();
 
 	// Confined in the thread calling the factory method
-	private ITypeEnvironment te;
 	private String refines;
 	private boolean broken = false;
 
@@ -137,9 +138,18 @@ public class ModelTranslator extends AbstractComponentTranslator {
 	// ###############################################################################################################################################################
 	// Implementation
 
-	private ModelTranslator(final ISCMachineRoot currentMachine) {
-		this.machine = currentMachine;
+	private ModelTranslator(final ISCMachineRoot machine)
+			throws TranslationFailedException {
+		this.machine = machine;
 		origin = machine.getMachineRoot();
+		ff = ((ISCMachineRoot) machine).getFormulaFactory();
+		try {
+			te = ((ISCMachineRoot) machine).getTypeEnvironment(ff);
+		} catch (RodinDBException e) {
+			final String message = "A Rodin exception occured during translation process. Original Exception: ";
+			throw new TranslationFailedException(machine.getComponentName(),
+					message + e.getLocalizedMessage());
+		}
 	}
 
 	private void translate() throws RodinDBException,
@@ -151,8 +161,6 @@ public class ModelTranslator extends AbstractComponentTranslator {
 		broken = !machine.isAccurate(); // isAccurate() is not transitive, we
 		// need to collect the information also
 		// for the events
-		te = machine.getTypeEnvironment(ff);
-
 		translateMachine();
 
 		// Check for fully discharged Invariants and Events

de.prob2.feature/feature.xml

@@ -242,6 +242,7 @@ litigation.
       <import plugin="org.eclipse.gef" version="3.5.0" match="compatible"/>
       <import plugin="org.eclipse.ui.navigator" version="3.5.0" match="greaterOrEqual"/>
       <import plugin="de.bmotionstudio.gef.editor" version="5.2.1" match="greaterOrEqual"/>
+      <import plugin="org.eventb.theory.core" version="1.3.0" match="greaterOrEqual"/>
    </requires>
 
    <plugin
@@ -280,4 +281,11 @@ litigation.
          fragment="true"
          unpack="false"/>
 
+   <plugin
+         id="de.prob.theory"
+         download-size="0"
+         install-size="0"
+         version="0.0.0"
+         unpack="false"/>
+
 </feature>