From f87b4233437f0900c19f462b5e443a3c81b27b6e Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Tue, 15 Jan 2019 12:44:33 -0500 Subject: Initial workspace setup --- .../ecse/dslreasoner/GenerateVampireLanguage.mwe2 | 44 ++++ .../mcgill/ecse/dslreasoner/VampireLanguage.xtext | 278 +++++++++++++++++++++ .../dslreasoner/VampireLanguageRuntimeModule.xtend | 11 + .../VampireLanguageStandaloneSetup.xtend | 15 ++ .../generator/VampireLanguageGenerator.xtend | 25 ++ .../scoping/VampireLanguageScopeProvider.xtend | 15 ++ .../validation/VampireLanguageValidator.xtend | 25 ++ 7 files changed, 413 insertions(+) create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/GenerateVampireLanguage.mwe2 create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguageRuntimeModule.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguageStandaloneSetup.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/generator/VampireLanguageGenerator.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/scoping/VampireLanguageScopeProvider.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/validation/VampireLanguageValidator.xtend (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca') diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/GenerateVampireLanguage.mwe2 b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/GenerateVampireLanguage.mwe2 new file mode 100644 index 00000000..903ac83b --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/GenerateVampireLanguage.mwe2 @@ -0,0 +1,44 @@ +module ca.mcgill.ecse.dslreasoner.GenerateVampireLanguage + +import org.eclipse.xtext.xtext.generator.* +import org.eclipse.xtext.xtext.generator.model.project.* + +var rootPath = ".." + +Workflow { + + component = XtextGenerator { + configuration = { + project = StandardProjectConfig { + baseName = "ca.mcgill.ecse.dslreasoner.vampire.language" + rootPath = rootPath + runtimeTest = { + enabled = true + } + eclipsePlugin = { + enabled = true + } + eclipsePluginTest = { + enabled = true + } + createEclipseMetaData = true + } + code = { + encoding = "UTF-8" + lineDelimiter = "\r\n" + fileHeader = "/*\n * generated by Xtext \${version}\n */" + } + } + language = StandardLanguage { + name = "ca.mcgill.ecse.dslreasoner.VampireLanguage" + fileExtensions = "tptp" + + serializer = { + generateStub = false + } + validator = { + // composedCheck = "org.eclipse.xtext.validation.NamesAreUniqueValidator" + } + } + } +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext new file mode 100644 index 00000000..daa15ca1 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext @@ -0,0 +1,278 @@ +grammar ca.mcgill.ecse.dslreasoner.VampireLanguage with org.eclipse.xtext.common.Terminals hidden (WS) + +generate vampireLanguage "http://www.mcgill.ca/ecse/dslreasoner/VampireLanguage" + +//@@@@@@@@@@@ +//2 things TODO: +//1. fix anotations (ln77) +//2. can only use declared variables in formula (ln 158) + +//@@@@@@@@@@@ + +VampireModel: + // TODO ensures there is always exactly 1 conjecture + ( + includes += VLSInclude | + comments += VLSComment | + formulas += VLSFofFormula + )* +; + + + +////////////////////////////////// +// VLS terminals +////////////////////////////////// + +terminal ALPHA_NUMERIC: ( 'a'..'z' | 'A'..'Z' | '0'..'9' | '_'); +terminal UPPER_WORD_ID: ('A'..'Z') (ALPHA_NUMERIC)*; +terminal LOWER_WORD_ID: ('a'..'z') (ALPHA_NUMERIC)*; + + +//TODO MIGHT NEED TO IMPLEMENT SOME WAY TO ONLY CONSIDER WHAT IS INSIDE QUOTES AS NAME +//incorporate quotes in the line of calling. ex. "'" name=SINGLEQUOTE "'" +terminal DOUBLE_QUOTE: '"' ( '\\' ('"'|'\\') | !('\\'|'"') )* '"';//from terminal STRING rule, positive about this +terminal SINGLE_QUOTE: "'" ( '\\' ("'"|'\\') | !('\\'|"'") )+ "'";//from terminal STRING rule, positive about this + +terminal SIGN: ('+' | '-'); + +terminal DOLLAR_ID: ('$') (LOWER_WORD_ID); +terminal DOUBLE_DOLLAR_ID: ('$$') (LOWER_WORD_ID); + +terminal LITERAL: '0' | ('1'..'9') (INT)?; +terminal SIGNED_LITERAL: (SIGN)* (LITERAL); + +terminal UNSIGNED_REAL_FRAC_ID: (LITERAL) ('.') (INT); +terminal UNSIGNED_REAL_EXP_ID: (LITERAL | UNSIGNED_REAL_FRAC_ID) ('Ee') (SIGN)* (INT) ; +terminal SIGNED_REAL_ID: (SIGN)* (UNSIGNED_REAL_FRAC_ID | UNSIGNED_REAL_EXP_ID); + +terminal UNSIGNED_RAT_ID: (LITERAL) ('/') ('1'..'9') (INT)? ; +terminal SIGNED_RAT_ID: (SIGN)* (UNSIGNED_RAT_ID); + +//Overwriting is necessary +terminal ANY_OTHER: '%' (!('\n'|'\r'))* ('\r'); +terminal SINGLE_COMMENT: ANY_OTHER; +//terminal ID: ( !('('|')'|'\r'|'\n') )+ ; + + + +////////////////////////////////// +// VLS types +////////////////////////////////// + +// +VLSInclude: + 'include(' fileName = SINGLE_QUOTE ( ',[' names += VLSName (',' names += VLSName)* ']' )? +; + +VLSName: + name = (LOWER_WORD_ID | SINGLE_QUOTE | LITERAL | SIGNED_LITERAL) +; + +// +VLSComment: + comment = SINGLE_COMMENT + //need to add a new line at the end of the file for the case where the last line is a comment +; + +//VLSConstantDeclaration: name = (LOWER_WORD_ID | SINGLE_QUOTE | DOLLAR_ID | DOUBLE_DOLLAR_ID ); + +// +VLSFofFormula: + 'fof' '(' name = (LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole = VLSRole ',' fofFormula = VLSTerm (',' annotations = VLSAnnotation)? ')' '.' +; +/* +//NAME +VLSName: + //(atomic_Word = Atomic_Word | integer = Integer | single_quote_word = Single_Quote_Word) + name = (LOWER_WORD_ID | SIGNED_INT_ID | SINGLE_QUOTE) +; +*/ +// +VLSRole: + VLSAxiom | VLSConjecture | VLSHypothesis | VLSDefinition | + VLSAssumption | VLSLemma | VLSTheorem | VLSCorollary | VLSNegated_Conjecture | + VLSPlain | VLSType |VLSFi_Domain | VLSFi_Functors | VLSFi_Predicates | VLSUnknown +; + +VLSAxiom: + "axiom" +; + +VLSConjecture: + "conjecture" +; + +VLSHypothesis: + "hypothesis" +; + +VLSDefinition: + "definition" +; + +VLSAssumption: + "assumption" +; + +VLSLemma: + "lemma" +; + +VLSTheorem: + "theorem" +; + +VLSCorollary: + "corollary" +; + +VLSNegated_Conjecture: + "negated_conjecture" +; + +VLSPlain: + "plain" +; + +VLSType: + "type" +; + +VLSFi_Domain: + "fi_domain" +; + +VLSFi_Functors: + "fi_functors" +; + +VLSFi_Predicates: + "fi_predicates" +; + +VLSUnknown: + "unknown" +; + +// +// Not at all based on the website. based on what we think the output will be like +VLSAnnotation: + ('[')? (name = (LOWER_WORD_ID | SINGLE_QUOTE | VLSRole))? ( '(' followup = VLSAnnotationTerms ')' )? (']')? +; + +VLSAnnotationTerms returns VLSAnnotation: + terms += VLSAnnotation (',' terms += VLSAnnotation )* +; + +////////////////////////////////// +// VLS Terms +////////////////////////////////// + +VLSTerm: + //( VLSLogic | VLSSequent) + VLSBinary +; +//* +//VLSBinaryFormula +VLSBinary returns VLSTerm: + VLSUnitaryFormula + ( + (({VLSEquivalent.left = current} "<=>" | + {VLSImplies.left = current} "=>" | + {VLSRevImplies.left = current} "<=" | + {VLSXnor.left = current} "<~>" | + {VLSNor.left = current} "~|" | + {VLSNand.left = current} "~&") right = VLSUnitaryFormula) + | + ({VLSAnd.left = current} '&' right = VLSUnitaryFormula)+ + | + ({VLSOr.left = current} '|' right = VLSUnitaryFormula)+ + )? +; + +//VLSUnitaryFormula +VLSUnitaryFormula returns VLSTerm: + VLSUniversalQuantifier | VLSExistentialQuantifier | VLSUnaryNegation | VLSUnaryInfix + //| VLSEquality + | '(' VLSTerm ')' +; + +VLSUniversalQuantifier returns VLSTerm: + {VLSUniversalQuantifier} (("!") '[' variables += VLSVariable (',' variables += VLSVariable)* ']' ':') operand = VLSUnitaryFormula +; + +VLSExistentialQuantifier returns VLSTerm: + {VLSExistentialQuantifier} (("?") '[' variables += VLSVariable (',' variables += VLSVariable)* ']' ':') operand = VLSUnitaryFormula +; + +VLSUnaryNegation returns VLSTerm: + {VLSUnaryNegation} ('~') operand = VLSUnitaryFormula +; + +VLSUnaryInfix returns VLSTerm: + VLSAtomic (({VLSInequality.left = current} "!=" | + {VLSEquality.left = current} "=" | + {VLSAssignment.left = current} ":=") + right = VLSAtomic)? +; + +//NOT SUREEEE +//VLSEquality returns VLSTerm: +// VLSFofTerm ({VLSEquality.left = current} "=" right = VLSFofTerm)? +// +//; + +/* +enum VLSDefinedFunctor: + UMINUS='$uminus' | SUM='$sum' | DIFFERENCE='$difference' | PRODUCT='$product' | QUOTIENT='$quotient' | + QUOTIENT_E='$quotient_e' | QUOTIENT_T='$quotient_t' | QUOTIENT_F='$quotient_f' | REMAINDER_E='$remainder_e' | + REMAINDER_T='$remainder_t' | REMAINDER_F='$remainder_f' | FLOOR='$floor' | CEILING='$ceiling' | + TRUNCATE='$truncate' | ROUND='$round' | TO_INT='$to_int' | TO_RAT='$to_rat' | TO_REAL='$to_real' + ; +*/ + +VLSAtomic returns VLSTerm: + VLSAtomicConstant | VLSAtomicFunction | VLSVariable + | VLSDefinedTerm //temporary solution. this is only valid for equality, not for != or := + //| VLSEquality +; + +VLSAtomicConstant returns VLSTerm: + //{VLSConstant} name = VLSConstantDeclaration | + {VLSConstant} name = (LOWER_WORD_ID | SINGLE_QUOTE | DOLLAR_ID | DOUBLE_DOLLAR_ID | VLSRole) | + {VLSTrue} '$true' | + {VLSFalse} '$false' +; + +VLSAtomicFunction returns VLSTerm: + //? on next line causes warning + //TODO might need replace DOLLAR_ID with enum rule + //{VLSFunction} name = VLSConstantDeclaration ( '(' terms += VLSFofTerm (',' terms += VLSFofTerm)* ')' ) | + {VLSFunction} constant = (LOWER_WORD_ID | SINGLE_QUOTE | DOLLAR_ID | DOUBLE_DOLLAR_ID | VLSRole ) ( '(' terms += VLSFofTerm (',' terms += VLSFofTerm)* ')') | + {VLSLess} name = '$less' '(' terms += VLSFofTerm ',' terms += VLSFofTerm ')' +; + +VLSVariable : + + name = UPPER_WORD_ID +; + +VLSFofTerm returns VLSTerm: + //(VLSVariable | VLSFunction | VLSTffConditional | VLSTffLet | VLSTffTuple) + (VLSVariable | VLSFunctionFof | VLSDefinedTerm ) +; + +VLSFunctionFof: + //? on next line causes warning + //TODO might need replace DOLLAR_ID with enum rule + functor = (LOWER_WORD_ID | SINGLE_QUOTE | DOLLAR_ID | DOUBLE_DOLLAR_ID ) ( '(' terms += VLSFofTerm (',' terms += VLSFofTerm)* ')')? +; + +VLSDefinedTerm: + {VLSInt} value = SIGNED_LITERAL | + {VLSReal} value = SIGNED_REAL_ID | + {VLSRational} value = SIGNED_RAT_ID | + {VLSDoubleQuote} value = DOUBLE_QUOTE +; + diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguageRuntimeModule.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguageRuntimeModule.xtend new file mode 100644 index 00000000..162df1e2 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguageRuntimeModule.xtend @@ -0,0 +1,11 @@ +/* + * generated by Xtext 2.12.0 + */ +package ca.mcgill.ecse.dslreasoner + + +/** + * Use this class to register components to be used at runtime / without the Equinox extension registry. + */ +class VampireLanguageRuntimeModule extends AbstractVampireLanguageRuntimeModule { +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguageStandaloneSetup.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguageStandaloneSetup.xtend new file mode 100644 index 00000000..38a05c51 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguageStandaloneSetup.xtend @@ -0,0 +1,15 @@ +/* + * generated by Xtext 2.12.0 + */ +package ca.mcgill.ecse.dslreasoner + + +/** + * Initialization support for running Xtext languages without Equinox extension registry. + */ +class VampireLanguageStandaloneSetup extends VampireLanguageStandaloneSetupGenerated { + + def static void doSetup() { + new VampireLanguageStandaloneSetup().createInjectorAndDoEMFRegistration() + } +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/generator/VampireLanguageGenerator.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/generator/VampireLanguageGenerator.xtend new file mode 100644 index 00000000..f099486a --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/generator/VampireLanguageGenerator.xtend @@ -0,0 +1,25 @@ +/* + * generated by Xtext 2.12.0 + */ +package ca.mcgill.ecse.dslreasoner.generator + +import org.eclipse.emf.ecore.resource.Resource +import org.eclipse.xtext.generator.AbstractGenerator +import org.eclipse.xtext.generator.IFileSystemAccess2 +import org.eclipse.xtext.generator.IGeneratorContext + +/** + * Generates code from your model files on save. + * + * See https://www.eclipse.org/Xtext/documentation/303_runtime_concepts.html#code-generation + */ +class VampireLanguageGenerator extends AbstractGenerator { + + override void doGenerate(Resource resource, IFileSystemAccess2 fsa, IGeneratorContext context) { +// fsa.generateFile('greetings.txt', 'People to greet: ' + +// resource.allContents +// .filter(Greeting) +// .map[name] +// .join(', ')) + } +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/scoping/VampireLanguageScopeProvider.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/scoping/VampireLanguageScopeProvider.xtend new file mode 100644 index 00000000..d6b4a1ae --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/scoping/VampireLanguageScopeProvider.xtend @@ -0,0 +1,15 @@ +/* + * generated by Xtext 2.12.0 + */ +package ca.mcgill.ecse.dslreasoner.scoping + + +/** + * This class contains custom scoping description. + * + * See https://www.eclipse.org/Xtext/documentation/303_runtime_concepts.html#scoping + * on how and when to use it. + */ +class VampireLanguageScopeProvider extends AbstractVampireLanguageScopeProvider { + +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/validation/VampireLanguageValidator.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/validation/VampireLanguageValidator.xtend new file mode 100644 index 00000000..8d7a9f76 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/validation/VampireLanguageValidator.xtend @@ -0,0 +1,25 @@ +/* + * generated by Xtext 2.12.0 + */ +package ca.mcgill.ecse.dslreasoner.validation + + +/** + * This class contains custom validation rules. + * + * See https://www.eclipse.org/Xtext/documentation/303_runtime_concepts.html#validation + */ +class VampireLanguageValidator extends AbstractVampireLanguageValidator { + +// 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', +// VampireLanguagePackage.Literals.GREETING__NAME, +// INVALID_NAME) +// } +// } + +} -- cgit v1.2.3-54-g00ecf