From 32a4f3392a7d0c44439c0c9b960ef1cfb5e3cc2f Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Fri, 25 Oct 2019 04:15:39 -0400 Subject: VAMPIRE: post-submission push --- .../hu/bme/mit/inf/dslreasoner/AlloyLanguage.xtext | 152 +++++++++++++++++++++ .../dslreasoner/AlloyLanguageRuntimeModule.java | 11 ++ .../dslreasoner/AlloyLanguageStandaloneSetup.java | 16 +++ .../mit/inf/dslreasoner/GenerateAlloyLanguage.mwe2 | 133 ++++++++++++++++++ .../formatting/AlloyLanguageFormatter.xtend | 96 +++++++++++++ .../generator/AlloyLanguageGenerator.xtend | 24 ++++ .../scoping/AlloyLanguageScopeProvider.xtend | 81 +++++++++++ .../validation/AlloyLanguageValidator.xtend | 24 ++++ 8 files changed, 537 insertions(+) create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguage.xtext create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguageRuntimeModule.java create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguageStandaloneSetup.java create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/GenerateAlloyLanguage.mwe2 create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/formatting/AlloyLanguageFormatter.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/generator/AlloyLanguageGenerator.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/scoping/AlloyLanguageScopeProvider.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/validation/AlloyLanguageValidator.xtend (limited to 'Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf') diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguage.xtext b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguage.xtext new file mode 100644 index 00000000..fba3838c --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguage.xtext @@ -0,0 +1,152 @@ +grammar hu.bme.mit.inf.dslreasoner.AlloyLanguage with org.eclipse.xtext.common.Terminals + +generate alloyLanguage "http://www.bme.hu/mit/inf/dslreasoner/AlloyLanguage" + +ALSDocument: + ( enumDeclarations += ALSEnumDeclaration | + signatureBodies += ALSSignatureBody | + functionDefinitions += ALSFunctionDefinition | + relationDefinitions += ALSRelationDefinition | + factDeclarations += ALSFactDeclaration)+ + runCommand = ALSRunCommand +; + +////////////////////////////////// +// ALS terminals +////////////////////////////////// + +terminal ID: ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'_'|"'"|'"'|'0'..'9')*; +ALSID: ID; + +enum ALSMultiplicity: all | no | some | lone | one | set; + + +////////////////////////////////// +// ALS types +////////////////////////////////// + +ALSRelationDeclaration: ALSTypeDeclaration | ALSEnumLiteral | ALSFieldDeclaration | ALSVariableDeclaration; + +ALSTypeDeclaration: + ALSEnumDeclaration | ALSSignatureDeclaration +; + +ALSEnumDeclaration: + 'enum' name=ALSID '{' + literal+=ALSEnumLiteral ("," literal+=ALSEnumLiteral)* + '}'; +ALSEnumLiteral: name = ALSID; + +ALSSignatureDeclaration: name = ALSID; + +ALSSignatureBody: + ((multiplicity = ALSMultiplicity?) & (abstract ?= 'abstract')?) + 'sig' + declarations += ALSSignatureDeclaration (',' declarations += ALSSignatureDeclaration)* + (('extends' supertype = [ALSSignatureDeclaration]) + | + ('in' superset += [ALSSignatureDeclaration] ('+' superset += [ALSSignatureDeclaration])*) )? + '{' (fields+=ALSFieldDeclaration ("," fields+=ALSFieldDeclaration)*)? '}' +; + +ALSFieldDeclaration: + name = ALSID ':' (multiplicity = ALSMultiplicity)? type = ALSTerm +; + +ALSDefinition : ALSFunctionDefinition | ALSRelationDefinition; + +ALSFunctionDefinition: + "fun" name = ALSID "[" variables+=ALSVariableDeclaration (',' variables+=ALSVariableDeclaration)* "]" ":" type = ALSTerm + "{" value = ALSTerm "}" +; +ALSRelationDefinition: + "pred" name = ALSID "[" variables+=ALSVariableDeclaration (',' variables+=ALSVariableDeclaration)* "]" + "{" value = ALSTerm "}" +; + +ALSFactDeclaration: {ALSFactDeclaration} 'fact' (name=ALSID)? '{' (term = ALSTerm) '}' ; + +////////////////////////////////// +// ALS terms +////////////////////////////////// +ALSTerm: ALSQuantified; + +ALSQuantified returns ALSTerm: ({ALSQuantifiedEx} type = ALSMultiplicity + (disj?='disj')? variables+=ALSVariableDeclaration (',' variables+=ALSVariableDeclaration)* '{' expression = ALSTerm '}') | ALSOr; + +ALSOr returns ALSTerm: ALSIff ({ALSOr.leftOperand = current} ( "||" | "or" ) rightOperand = ALSIff)?; +ALSIff returns ALSTerm: ALSImpl ({ALSIff.leftOperand = current} ("<=>" | "iff") rightOperand = ALSImpl)?; +ALSImpl returns ALSTerm: ALSAnd ({ALSImpl.leftOperand = current} ("=>" | "implies") rightOperand = ALSAnd ('else' elseOperand = ALSAnd)?)?; +ALSAnd returns ALSTerm: ALSComparison ({ALSAnd.leftOperand = current} ( "&&" | "and" ) rightOperand = ALSComparison)?; + +ALSComparison returns ALSTerm: + ALSOverride + (({ALSEquals.leftOperand = current} "=" | + {ALSNotEquals.leftOperand = current} "!=" | + {ALSSubset.leftOperand = current} "in" | + {ALSLess.leftOperand = current} ">" | + {ALSLeq.leftOperand = current} ">=" | + {ALSMore.leftOperand = current} "<" | + {ALSMeq.leftOperand = current} "<=") + rightOperand = ALSOverride)?; + +ALSOverride returns ALSTerm: ALSRangeRestrictionRight ({ALSOverride.leftOperand = current} '++' rightOperand = ALSRangeRestrictionRight)?; + +ALSRangeRestrictionRight returns ALSTerm: ALSRangeRestrictionLeft ({ALSRangeRestrictionRight.relation = current} ':>' filter = ALSRangeRestrictionLeft)?; +ALSRangeRestrictionLeft returns ALSTerm: ALSJoin ({ALSRangeRestrictionLeft.filter = current} '<:' relation = ALSJoin)?; +ALSJoin returns ALSTerm: ALSMinus ({ALSJoin.leftOperand = current} '.' rightOperand = ALSMinus )*; + +ALSMinus returns ALSTerm: ALSPlus ({ALSMinus.leftOperand = current} '-' rightOperand = ALSPlus)*; +ALSPlus returns ALSTerm: ALSIntersection ({ALSPlus.leftOperand = current} '+' rightOperand = ALSIntersection)*; +ALSIntersection returns ALSTerm: ALSDirectProduct ({ALSIntersection.leftOperand = current} '&' rightOperand = ALSDirectProduct)*; +//ALSMultiply returns ALSTerm: ALSDirectProduct ({ALSMultiply.leftOperand = current} '*' rightOperand = ALSDirectProduct)*; + +ALSDirectProduct returns ALSTerm: + ALSPreficed + ({ALSDirectProduct.leftOperand = current} (leftMultiplicit = ALSMultiplicity)? + '->' + (rightMultiplicit = ALSMultiplicity)? + rightOperand = ALSPreficed)? +; + +ALSPreficed returns ALSTerm: + {ALSNot}=>("!"|'not') operand = ALSBasicRelationTerm | + {ALSInverseRelation}=>"~" operand = ALSBasicRelationTerm | + {AlSTransitiveClosure} "^" operand = ALSBasicRelationTerm | + {ALSReflectiveTransitiveClosure} "*" operand = ALSBasicRelationTerm | + {ALSCardinality} '#' operand = ALSBasicRelationTerm | + {ALSUnaryMinus} =>'-' operand = ALSBasicRelationTerm | + {ALSSum} 'sum' variables+=ALSVariableDeclaration (',' variables+=ALSVariableDeclaration)* '{' expression = ALSTerm '}' | +// {ALSQuantifiedEx} type = ALSMultiplicity +// (disj?='disj')? variables+=ALSVariableDeclaration (',' variables+=ALSVariableDeclaration)* '{' expression = ALSTerm '}' | + {ALSFunctionCall} (referredDefinition=[ALSDefinition]|referredNumericOperator=ALSNumericOperator) '['params+=ALSTerm (',' params+=ALSTerm)*']' | + ALSBasicRelationTerm; + +enum ALSNumericOperator: plus|sub|mul|rem|div; + +//ALSVariable: name = ALSID; +ALSVariableDeclaration: name=ALSID ':' range = ALSTerm; + +ALSBasicRelationTerm returns ALSTerm: + {ALSNone} 'none'| + {ALSIden} 'iden'| + {ALSUniv} 'univ'| + {ALSInt} 'Int' | + {ALSString} 'String' | + {ALSReference} referred = [ALSRelationDeclaration] | + {ALSNumberLiteral} value = INT| + {ALSStringLiteral} value = STRING| + '(' ALSTerm ')' +; + +////////////////////////////////// +// ALS Commands and scopes +////////////////////////////////// +ALSRunCommand: + {ALSRunCommand} 'run' '{' '}' ('for' typeScopes+=ALSTypeScope (',' typeScopes+=ALSTypeScope)*)?; + +ALSTypeScope: ALSSigScope | ALSIntScope | ALSStringScope; + +ALSSigScope: (exactly?='exactly')? number = INT type = [ALSSignatureDeclaration]; +ALSIntScope: number = INT 'Int'; +ALSStringScope: 'exactly' number = INT 'String'; \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguageRuntimeModule.java b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguageRuntimeModule.java new file mode 100644 index 00000000..3fd8e2f0 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguageRuntimeModule.java @@ -0,0 +1,11 @@ +/* + * generated by Xtext + */ +package hu.bme.mit.inf.dslreasoner; + +/** + * Use this class to register components to be used at runtime / without the Equinox extension registry. + */ +public class AlloyLanguageRuntimeModule extends hu.bme.mit.inf.dslreasoner.AbstractAlloyLanguageRuntimeModule { + +} diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguageStandaloneSetup.java b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguageStandaloneSetup.java new file mode 100644 index 00000000..d3112c3d --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguageStandaloneSetup.java @@ -0,0 +1,16 @@ +/* +* generated by Xtext +*/ +package hu.bme.mit.inf.dslreasoner; + +/** + * Initialization support for running Xtext languages + * without equinox extension registry + */ +public class AlloyLanguageStandaloneSetup extends AlloyLanguageStandaloneSetupGenerated{ + + public static void doSetup() { + new AlloyLanguageStandaloneSetup().createInjectorAndDoEMFRegistration(); + } +} + diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/GenerateAlloyLanguage.mwe2 b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/GenerateAlloyLanguage.mwe2 new file mode 100644 index 00000000..0f23b862 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/GenerateAlloyLanguage.mwe2 @@ -0,0 +1,133 @@ +module hu.bme.mit.inf.dslreasoner.GenerateAlloyLanguage + +import org.eclipse.emf.mwe.utils.* +import org.eclipse.xtext.generator.* +import org.eclipse.xtext.ui.generator.* + +var grammarURI = "classpath:/hu/bme/mit/inf/dslreasoner/AlloyLanguage.xtext" +var fileExtensions = "als" +var projectName = "hu.bme.mit.inf.dslreasoner.alloy.language" +var runtimeProject = "../${projectName}" +var generateXtendStub = true +var encoding = "UTF-8" + +Workflow { + bean = StandaloneSetup { + scanClassPath = true + platformUri = "${runtimeProject}/.." + // The following two lines can be removed, if Xbase is not used. + registerGeneratedEPackage = "org.eclipse.xtext.xbase.XbasePackage" + registerGenModelFile = "platform:/resource/org.eclipse.xtext.xbase/model/Xbase.genmodel" + } + + component = DirectoryCleaner { + directory = "${runtimeProject}/src-gen" + } + + component = DirectoryCleaner { + directory = "${runtimeProject}/model/generated" + } + + component = DirectoryCleaner { + directory = "${runtimeProject}.ui/src-gen" + } + +// component = DirectoryCleaner { +// directory = "${runtimeProject}.tests/src-gen" +// } + + component = Generator { + pathRtProject = runtimeProject + pathUiProject = "${runtimeProject}.ui" + //pathTestProject = "${runtimeProject}.tests" + projectNameRt = projectName + projectNameUi = "${projectName}.ui" + encoding = encoding + language = auto-inject { + uri = grammarURI + + // Java API to access grammar elements (required by several other fragments) + fragment = grammarAccess.GrammarAccessFragment auto-inject {} + + // generates Java API for the generated EPackages + fragment = ecore.EMFGeneratorFragment auto-inject {} + + // the old serialization component + // fragment = parseTreeConstructor.ParseTreeConstructorFragment auto-inject {} + + // serializer 2.0 + fragment = serializer.SerializerFragment auto-inject { + generateStub = false + } + + // a custom ResourceFactory for use with EMF + fragment = resourceFactory.ResourceFactoryFragment auto-inject {} + + // The antlr parser generator fragment. + fragment = parser.antlr.XtextAntlrGeneratorFragment auto-inject { + // options = { + // backtrack = true + // } + } + + // Xtend-based API for validation + fragment = validation.ValidatorFragment auto-inject { + // composedCheck = "org.eclipse.xtext.validation.ImportUriValidator" + // composedCheck = "org.eclipse.xtext.validation.NamesAreUniqueValidator" + } + + // old scoping and exporting API + // fragment = scoping.ImportURIScopingFragment auto-inject {} + // fragment = exporting.SimpleNamesFragment auto-inject {} + + // scoping and exporting API + fragment = scoping.ImportNamespacesScopingFragment auto-inject {} + fragment = exporting.QualifiedNamesFragment auto-inject {} + fragment = builder.BuilderIntegrationFragment auto-inject {} + + // generator API + fragment = generator.GeneratorFragment auto-inject {} + + // formatter API + fragment = formatting.FormatterFragment auto-inject {} + + // labeling API + fragment = labeling.LabelProviderFragment auto-inject {} + + // outline API + fragment = outline.OutlineTreeProviderFragment auto-inject {} + fragment = outline.QuickOutlineFragment auto-inject {} + + // quickfix API + fragment = quickfix.QuickfixProviderFragment auto-inject {} + + // content assist API + fragment = contentAssist.ContentAssistFragment auto-inject {} + + // generates a more lightweight Antlr parser and lexer tailored for content assist + fragment = parser.antlr.XtextAntlrUiGeneratorFragment auto-inject {} + + // generates junit test support classes into Generator#pathTestProject + fragment = junit.Junit4Fragment auto-inject {} + + // rename refactoring + fragment = refactoring.RefactorElementNameFragment auto-inject {} + + // provides the necessary bindings for java types integration + fragment = types.TypesGeneratorFragment auto-inject {} + + // generates the required bindings only if the grammar inherits from Xbase + fragment = xbase.XbaseGeneratorFragment auto-inject {} + + // generates the required bindings only if the grammar inherits from Xtype + fragment = xbase.XtypeGeneratorFragment auto-inject {} + + // provides a preference page for template proposals + fragment = templates.CodetemplatesGeneratorFragment auto-inject {} + + // provides a compare view + fragment = compare.CompareFragment auto-inject {} + } + } +} + diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/formatting/AlloyLanguageFormatter.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/formatting/AlloyLanguageFormatter.xtend new file mode 100644 index 00000000..e5ce7773 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/formatting/AlloyLanguageFormatter.xtend @@ -0,0 +1,96 @@ +/* + * generated by Xtext + */ +package hu.bme.mit.inf.dslreasoner.formatting + +import com.google.inject.Inject +import hu.bme.mit.inf.dslreasoner.services.AlloyLanguageGrammarAccess +import org.eclipse.xtext.formatting.impl.AbstractDeclarativeFormatter +import org.eclipse.xtext.formatting.impl.FormattingConfig + +/** + * This class contains custom formatting description. + * + * see : http://www.eclipse.org/Xtext/documentation.html#formatting + * on how and when to use it + * + * Also see {@link org.eclipse.xtext.xtext.XtextFormattingTokenSerializer} as an example + */ +class AlloyLanguageFormatter extends AbstractDeclarativeFormatter { + + @Inject extension AlloyLanguageGrammarAccess + + override protected void configureFormatting(FormattingConfig c) { + // It's usually a good idea to activate the following three statements. + // They will add and preserve newlines around comments + c.setLinewrap(0, 1, 2).before(SL_COMMENTRule) + c.setLinewrap(0, 1, 2).before(ML_COMMENTRule) + c.setLinewrap(0, 1, 1).after(ML_COMMENTRule) + + c.setAutoLinewrap(100000); + + //Signatures + c.setIndentationIncrement.after(ALSSignatureBodyAccess.leftCurlyBracketKeyword_5); + c.setLinewrap.after(ALSSignatureBodyAccess.leftCurlyBracketKeyword_5) + c.setIndentationDecrement.before(ALSSignatureBodyAccess.rightCurlyBracketKeyword_7); + c.setLinewrap.after(ALSSignatureBodyAccess.rightCurlyBracketKeyword_7) + c.setLinewrap.before(ALSSignatureBodyAccess.rightCurlyBracketKeyword_7) + c.setNoSpace.before(ALSSignatureBodyAccess.commaKeyword_3_0) + c.setLinewrap.after(ALSSignatureBodyAccess.commaKeyword_3_0) + c.setNoSpace.before(ALSSignatureBodyAccess.commaKeyword_3_0) + c.setNoSpace.before(ALSSignatureBodyAccess.commaKeyword_6_1_0) + c.setLinewrap.after(ALSSignatureBodyAccess.commaKeyword_6_1_0) + c.setNoSpace.before(ALSSignatureBodyAccess.commaKeyword_6_1_0) + //c.setLinewrap(0,1,2).between(ALSSignatureDeclarationRule,ALSSignatureDeclarationRule) + + //Enums + c.setIndentationIncrement.after(ALSEnumDeclarationAccess.leftCurlyBracketKeyword_2) + c.setLinewrap.after(ALSEnumDeclarationAccess.leftCurlyBracketKeyword_2) + c.setIndentationDecrement.before(ALSEnumDeclarationAccess.rightCurlyBracketKeyword_5) + c.setLinewrap.before(ALSEnumDeclarationAccess.rightCurlyBracketKeyword_5) + c.setLinewrap.after(ALSEnumDeclarationAccess.rightCurlyBracketKeyword_5) + c.setNoSpace.before(ALSEnumDeclarationAccess.commaKeyword_4_0) + + + //facts + c.setIndentationIncrement.after(ALSFactDeclarationAccess.leftCurlyBracketKeyword_3) + c.setLinewrap.after(ALSFactDeclarationAccess.leftCurlyBracketKeyword_3) + c.setIndentationDecrement.before(ALSFactDeclarationAccess.rightCurlyBracketKeyword_5) + c.setLinewrap.before(ALSFactDeclarationAccess.rightCurlyBracketKeyword_5) + c.setLinewrap.after(ALSFactDeclarationAccess.rightCurlyBracketKeyword_5) + + //predicates + c.setIndentationIncrement.after(ALSRelationDefinitionAccess.leftCurlyBracketKeyword_6) + c.setLinewrap.after(ALSRelationDefinitionAccess.leftCurlyBracketKeyword_6) + c.setIndentationDecrement.before(ALSRelationDefinitionAccess.rightCurlyBracketKeyword_8) + c.setLinewrap.before(ALSRelationDefinitionAccess.rightCurlyBracketKeyword_8) + c.setLinewrap.after(ALSRelationDefinitionAccess.rightCurlyBracketKeyword_8) + c.setNoSpace.after(ALSRelationDefinitionAccess.leftSquareBracketKeyword_2) + c.setNoSpace.before(ALSRelationDefinitionAccess.rightSquareBracketKeyword_5) + c.setNoSpace.before(ALSRelationDefinitionAccess.commaKeyword_4_0) + + // terms + //c.setNoSpace.before(ALSJoinAccess.rightSquareBracketKeyword_1_2_1_3) + c.setNoSpace.before(ALSJoinAccess.fullStopKeyword_1_1) + c.setNoSpace.after(ALSJoinAccess.fullStopKeyword_1_1) + + c.setNoSpace.before(ALSDirectProductAccess.hyphenMinusGreaterThanSignKeyword_1_2) + c.setNoSpace.after(ALSDirectProductAccess.hyphenMinusGreaterThanSignKeyword_1_2) + + c.setNoSpace.before(ALSVariableDeclarationAccess.colonKeyword_1) +// c.setNoSpace.before(ALSPreficedAccess.commaKeyword_5_3_0) +// c.setNoSpace.before(ALSPreficedAccess.commaKeyword_6_4_0) +// +// c.setIndentationIncrement.after(ALSPreficedAccess.leftCurlyBracketKeyword_5_4) +// c.setLinewrap.after(ALSPreficedAccess.leftCurlyBracketKeyword_5_4) +// c.setLinewrap.before(ALSPreficedAccess.rightCurlyBracketKeyword_5_6) +// c.setIndentationDecrement.before(ALSPreficedAccess.rightCurlyBracketKeyword_5_6) + + c.setNoSpace.after(ALSBasicRelationTermAccess.leftParenthesisKeyword_8_0) + c.setNoSpace.before(ALSBasicRelationTermAccess.rightParenthesisKeyword_8_2) + + // Quantified expression + c.setNoSpace.before(ALSQuantifiedAccess.commaKeyword_0_4_0) + + } +} diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/generator/AlloyLanguageGenerator.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/generator/AlloyLanguageGenerator.xtend new file mode 100644 index 00000000..c1ad5629 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/generator/AlloyLanguageGenerator.xtend @@ -0,0 +1,24 @@ +/* + * generated by Xtext + */ +package hu.bme.mit.inf.dslreasoner.generator + +import org.eclipse.emf.ecore.resource.Resource +import org.eclipse.xtext.generator.IGenerator +import org.eclipse.xtext.generator.IFileSystemAccess + +/** + * Generates code from your model files on save. + * + * see http://www.eclipse.org/Xtext/documentation.html#TutorialCodeGeneration + */ +class AlloyLanguageGenerator implements IGenerator { + + override void doGenerate(Resource resource, IFileSystemAccess fsa) { +// fsa.generateFile('greetings.txt', 'People to greet: ' + +// resource.allContents +// .filter(typeof(Greeting)) +// .map[name] +// .join(', ')) + } +} diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/scoping/AlloyLanguageScopeProvider.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/scoping/AlloyLanguageScopeProvider.xtend new file mode 100644 index 00000000..b2333f51 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/scoping/AlloyLanguageScopeProvider.xtend @@ -0,0 +1,81 @@ +/* + * generated by Xtext + */ +package hu.bme.mit.inf.dslreasoner.scoping + +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDefinition +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEnumDeclaration +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSFunctionCall +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSQuantifiedEx +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSReference +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRelationDeclaration +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRelationDefinition +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSum +import java.util.ArrayList +import java.util.Collections +import java.util.HashSet +import java.util.LinkedList +import java.util.List +import java.util.Set +import org.eclipse.emf.ecore.EObject +import org.eclipse.emf.ecore.EReference +import org.eclipse.xtext.scoping.IScope +import org.eclipse.xtext.scoping.Scopes +import org.eclipse.xtext.scoping.impl.AbstractDeclarativeScopeProvider + +/** + * This class contains custom scoping description. + * + * see : http://www.eclipse.org/Xtext/documentation.html#scoping + * on how and when to use it + * + */ +class AlloyLanguageScopeProvider extends AbstractDeclarativeScopeProvider { + + def public IScope scope_ALSReference_referred(ALSReference alsReferecnce, EReference ref) { + val Set declarations = new HashSet + + val parent = alsReferecnce.getAllParents(ALSDocument).head as ALSDocument + val signatures = parent.signatureBodies.map[ALSSignatureBody x|x.declarations].flatten + declarations+=parent.enumDeclarations + declarations+=signatures + declarations+=parent.enumDeclarations.map[ALSEnumDeclaration x | x.literal].flatten + declarations+=parent.signatureBodies.map[ALSSignatureBody x|x.fields].flatten + + declarations+=alsReferecnce.getAllParents(ALSQuantifiedEx).map[ALSQuantifiedEx x | x.variables].flatten + declarations+=alsReferecnce.getAllParents(ALSSum).map[ALSSum x | x.variables].flatten + declarations+=alsReferecnce.getAllParents(ALSRelationDefinition).map[ALSRelationDefinition x | x.variables].flatten + +// println("---") +// println(declarations.map[it.name].join(", ")) + + return Scopes.scopeFor(declarations) + } + //{ALSFunctionCall} (/*functionName=ALSID |*/ referredDefinition=[ALSDefinition]) + def public IScope scope_ALSFunctionCall_referredDefinition(ALSFunctionCall call, EReference ref) { + val parent = call.getAllParents(ALSDocument).head as ALSDocument + val list = new LinkedList + list += parent.relationDefinitions + list += parent.functionDefinitions + //list.forEach[println(it.name + " " + it.eContainer)] + return Scopes.scopeFor(list) + } + + def List getAllParents(EObject object, Class type) { + if(object.eContainer == null) { + return Collections.EMPTY_LIST + } else { + val container = object.eContainer; + val previousParents = container.getAllParents(type) + if(type.isInstance(container)){ + val res = new ArrayList(previousParents) + res+= container as X + return res + } + else return previousParents + + } + } +} diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/validation/AlloyLanguageValidator.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/validation/AlloyLanguageValidator.xtend new file mode 100644 index 00000000..daeb9860 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/validation/AlloyLanguageValidator.xtend @@ -0,0 +1,24 @@ +/* + * generated by Xtext + */ +package hu.bme.mit.inf.dslreasoner.validation +//import org.eclipse.xtext.validation.Check + +/** + * Custom validation rules. + * + * see http://www.eclipse.org/Xtext/documentation.html#validation + */ +class AlloyLanguageValidator extends AbstractAlloyLanguageValidator { + +// public static val INVALID_NAME = 'invalidName' +// +// @Check +// def checkGreetingStartsWithCapital(Greeting greeting) { +// if (!Character.isUpperCase(greeting.name.charAt(0))) { +// warning('Name should start with a capital', +// MyDslPackage.Literals.GREETING__NAME, +// INVALID_NAME) +// } +// } +} -- cgit v1.2.3-54-g00ecf