Skip to content

GitLab

Commit e66f6d1c authored by Sebastian Voss's avatar Sebastian Voss
Browse files

Adding Lambda-Expressions to Yices Model (incl. AccessFacade and TextGen) 

refs 724
parent 942457e0
Hide whitespace changes
Inline Side-by-side
org.fortiss.af3.tools/trunk/model/yices.ecore
View file @ e66f6d1c
......@@ -54,6 +54,7 @@
eType="#//types/YicesTypeBase"/>
<eStructuralFeatures xsi:type="ecore:EAttribute" name="memberNames" upperBound="-1"
eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
<eStructuralFeatures xsi:type="ecore:EReference" name="lambda" eType="#//commands/Lambda"/>
</eClassifiers>
<eClassifiers xsi:type="ecore:EClass" name="SelectTerm" eSuperTypes="platform:/plugin/org.fortiss.af3.expression/model/expression.ecore#//terms/IExpressionTerm">
<eStructuralFeatures xsi:type="ecore:EAttribute" name="identifier" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
......@@ -80,6 +81,14 @@
<eStructuralFeatures xsi:type="ecore:EReference" name="name" eType="ecore:EClass platform:/plugin/org.fortiss.af3.expression/model/expression.ecore#//terms/IExpressionTerm"/>
</eClassifiers>
<eClassifiers xsi:type="ecore:EClass" name="Select" eSuperTypes="#//YicesFileContent"/>
<eClassifiers xsi:type="ecore:EClass" name="Lambda" eSuperTypes="platform:/plugin/org.fortiss.af3.expression/model/expression.ecore#//terms/IExpressionTerm">
<eStructuralFeatures xsi:type="ecore:EAttribute" name="memberNames" upperBound="-1"
eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
<eStructuralFeatures xsi:type="ecore:EReference" name="memberTypes" upperBound="-1"
eType="#//types/YicesTypeBase"/>
<eStructuralFeatures xsi:type="ecore:EReference" name="expression" lowerBound="1"
eType="ecore:EClass platform:/plugin/org.fortiss.af3.expression/model/expression.ecore#//terms/IExpressionTerm"/>
</eClassifiers>
</eSubpackages>
<eSubpackages name="run" nsURI="http://www.fortiss.org/af3/tools/yices/run" nsPrefix="org-fortiss-af3-tools-yices-run">
<eClassifiers xsi:type="ecore:EClass" name="YicesResult">
......
org.fortiss.af3.tools/trunk/model/yices.genmodel
View file @ e66f6d1c
......@@ -55,6 +55,8 @@
<genFeatures notify="false" createChild="false" propertySortChoices="true"
ecoreFeature="ecore:EReference yices.ecore#//types/DependentFunctionType/memberTypes"/>
<genFeatures createChild="false" ecoreFeature="ecore:EAttribute yices.ecore#//types/DependentFunctionType/memberNames"/>
<genFeatures notify="false" createChild="false" propertySortChoices="true"
ecoreFeature="ecore:EReference yices.ecore#//types/DependentFunctionType/lambda"/>
</genClasses>
<genClasses ecoreClass="yices.ecore#//types/SelectTerm">
<genFeatures notify="false" createChild="false" propertySortChoices="true"
......@@ -84,6 +86,13 @@
<genFeatures createChild="false" ecoreFeature="ecore:EReference yices.ecore#//commands/Function/name"/>
</genClasses>
<genClasses ecoreClass="yices.ecore#//commands/Select"/>
<genClasses ecoreClass="yices.ecore#//commands/Lambda">
<genFeatures createChild="false" ecoreFeature="ecore:EAttribute yices.ecore#//commands/Lambda/memberNames"/>
<genFeatures notify="false" createChild="false" propertySortChoices="true"
ecoreFeature="ecore:EReference yices.ecore#//commands/Lambda/memberTypes"/>
<genFeatures notify="false" createChild="false" propertySortChoices="true"
ecoreFeature="ecore:EReference yices.ecore#//commands/Lambda/expression"/>
</genClasses>
</nestedGenPackages>
<nestedGenPackages prefix="AF3YicesRun" basePackage="org.fortiss.af3.tools.yices.model"
disposableProviderFactory="true" ecorePackage="yices.ecore#//run">
......
org.fortiss.af3.tools/trunk/src/org/fortiss/af3/tools/yices/model/YicesModelAccessFacade.java
View file @ e66f6d1c
......@@ -39,7 +39,7 @@ import org.fortiss.af3.tools.yices.model.types.YicesTypeBase;
* @author ratiu
* @author $Author: ratiu $
* @version $Rev: 1270 $
* @ConQAT.Rating GREEN Hash: 66001C63B582DC5010D8272AD6183EDC
* @ConQAT.Rating YELLOW Hash: F22D6EEF1A132F95E34E06A73C3292F7
*/
public class YicesModelAccessFacade {
......
org.fortiss.af3.tools/trunk/src/org/fortiss/af3/tools/yices/model/YicesModelFactory.java
View file @ e66f6d1c
......@@ -26,6 +26,7 @@ import org.fortiss.af3.tools.yices.model.commands.AF3YicesCommandsFactory;
import org.fortiss.af3.tools.yices.model.commands.Assert;
import org.fortiss.af3.tools.yices.model.commands.Check;
import org.fortiss.af3.tools.yices.model.commands.Function;
import org.fortiss.af3.tools.yices.model.commands.Lambda;
import org.fortiss.af3.tools.yices.model.run.AF3YicesRunFactory;
import org.fortiss.af3.tools.yices.model.run.EvidenceEntry;
import org.fortiss.af3.tools.yices.model.run.YicesResult;
......@@ -183,7 +184,7 @@ public class YicesModelFactory {
return ft;
}
/** Factory for {@link FunctionType} objects. */
/** Factory for {@link DependentFunctionType} objects. */
public static DependentFunctionType createDependentFunctionType(
List<YicesTypeBase> memberTypes, List<String> memberNames, SubType subtype) {
DependentFunctionType dft = AF3YicesTypesFactory.eINSTANCE.createDependentFunctionType();
......@@ -193,6 +194,15 @@ public class YicesModelFactory {
return dft;
}
/** Factory for {@link DependentFunctionType} objects. */
public static DependentFunctionType createDependentFunctionType(
List<YicesTypeBase> memberTypes, Lambda lambda) {
DependentFunctionType dft = AF3YicesTypesFactory.eINSTANCE.createDependentFunctionType();
dft.getMemberTypesList().addAll(memberTypes);
dft.setLambda(lambda);
return dft;
}
/** Factory for {@link SelectTerm} objects. */
public static SelectTerm createSelectTerm(String identifier, String field) {
SelectTerm select = AF3YicesTypesFactory.eINSTANCE.createSelectTerm();
......@@ -215,4 +225,14 @@ public class YicesModelFactory {
subrange.getExpressionMembersList().addAll(values);
return subrange;
}
/** Factory for {@link Function} objects. */
public static Lambda createLambda(List<YicesTypeBase> memberTypes, List<String> memberNames,
IExpressionTerm name) {
Lambda lambda = AF3YicesCommandsFactory.eINSTANCE.createLambda();
lambda.getMemberTypesList().addAll(memberTypes);
lambda.getMemberNamesList().addAll(memberNames);
lambda.setExpression(name);
return lambda;
}
}
org.fortiss.af3.tools/trunk/src/org/fortiss/af3/tools/yices/textgen/YicesTextGenerator.java
View file @ e66f6d1c
......@@ -41,6 +41,7 @@ import org.fortiss.af3.tools.yices.model.commands.Assert;
import org.fortiss.af3.tools.yices.model.commands.Check;
import org.fortiss.af3.tools.yices.model.commands.ExtendedAssert;
import org.fortiss.af3.tools.yices.model.commands.Function;
import org.fortiss.af3.tools.yices.model.commands.Lambda;
import org.fortiss.af3.tools.yices.model.types.BoolType;
import org.fortiss.af3.tools.yices.model.types.DefineType;
import org.fortiss.af3.tools.yices.model.types.DefinedType;
......@@ -126,9 +127,22 @@ public class YicesTextGenerator implements ITextGenerator<YicesFile> {
generateText(w, (DependentFunctionType)type);
} else if(type instanceof Subrange) {
generateText(w, (Subrange)type);
} else if(type instanceof Lambda) {
generateText(w, (Lambda)type);
}
}
/** Generate text for lambda */
private void generateText(Writer w, Lambda lambda) throws IOException,
UnknownLanguageFragmentException {
w.append("(lambda (");
for(int i = 0; i < lambda.getMemberNamesLength(); i++) {
w.append(" " + lambda.getMemberNames(i)).append("::");
generateText(w, lambda.getMemberTypes(i));
}
w.append(")" + convertExpressionToString(lambda.getExpression()) + ")");
}
/** Generate text for record type. */
private void generateText(Writer w, RecordType recordType) throws IOException,
UnknownLanguageFragmentException {
......@@ -186,13 +200,25 @@ public class YicesTextGenerator implements ITextGenerator<YicesFile> {
private void generateText(Writer w, DependentFunctionType dependantfunctionType)
throws IOException, UnknownLanguageFragmentException {
w.append("(->");
for(int i = 0; i < dependantfunctionType.getMemberNamesLength(); i++) {
w.append(" ");
w.append(dependantfunctionType.getMemberNames(i)).append("::");
generateText(w, dependantfunctionType.getMemberTypes(i));
if(dependantfunctionType.getMemberNamesLength() != 0) {
for(int i = 0; i < dependantfunctionType.getMemberNamesLength(); i++) {
w.append(" ");
w.append(dependantfunctionType.getMemberNames(i)).append("::");
generateText(w, dependantfunctionType.getMemberTypes(i));
}
} else {
for(int i = 0; i < dependantfunctionType.getMemberTypesLength(); i++) {
w.append(" ");
generateText(w, dependantfunctionType.getMemberTypes(i));
}
w.append(")");
}
if(dependantfunctionType.getSubType() != null) {
generateText(w, dependantfunctionType.getSubType());
w.append(")");
} else {
generateText(w, dependantfunctionType.getLambda());
}
generateText(w, dependantfunctionType.getSubType());
w.append(")");
}
/** Generate text for scalar type. */
......@@ -224,7 +250,7 @@ public class YicesTextGenerator implements ITextGenerator<YicesFile> {
w.append("(select " + st.getIdentifier() + ") " + st.getField() + ")");
}
/** Generate text for record type. */
/** Generate text for Subrange type. */
private void generateText(Writer w, Subrange subrange) throws IOException,
UnknownLanguageFragmentException {
w.append("(subrange ");
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment