From 15602c7cfbfc80b8c826855b94c9f9582650dd21 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Thu, 29 Aug 2019 06:26:02 -0400 Subject: VAMPIRE: adapt grammar to Vampire solution + get model from text --- .../AbstractVampireLanguageProposalProvider.java | 82 +++++++++++---------- .../ui/.VampireLanguageUiModule.xtendbin | Bin 2342 -> 2342 bytes .../.VampireLanguageProposalProvider.xtendbin | Bin 1792 -> 1792 bytes 3 files changed, 44 insertions(+), 38 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui') diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/src-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/AbstractVampireLanguageProposalProvider.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/src-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/AbstractVampireLanguageProposalProvider.java index 8e11f8c7..d22b57df 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/src-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/AbstractVampireLanguageProposalProvider.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/src-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/AbstractVampireLanguageProposalProvider.java @@ -18,9 +18,6 @@ import org.eclipse.xtext.ui.editor.contentassist.ICompletionProposalAcceptor; */ public abstract class AbstractVampireLanguageProposalProvider extends TerminalsProposalProvider { - public void completeVampireModel_Includes(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { - completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor); - } public void completeVampireModel_Comments(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor); } @@ -33,19 +30,10 @@ public abstract class AbstractVampireLanguageProposalProvider extends TerminalsP public void completeVampireModel_Tfformulas(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor); } - public void completeVLSInclude_FileName(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + public void completeVLSComment_Comment(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor); } - public void completeVLSInclude_Names(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { - completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor); - } - public void completeVLSName_Name(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { - completeRuleCall(((RuleCall)((Alternatives)assignment.getTerminal()).getElements().get(0)), context, acceptor); - completeRuleCall(((RuleCall)((Alternatives)assignment.getTerminal()).getElements().get(1)), context, acceptor); - completeRuleCall(((RuleCall)((Alternatives)assignment.getTerminal()).getElements().get(2)), context, acceptor); - completeRuleCall(((RuleCall)((Alternatives)assignment.getTerminal()).getElements().get(3)), context, acceptor); - } - public void completeVLSComment_Comment(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + public void completeVLSConfirmations_Name(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor); } public void completeVLSFofFormula_Name(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { @@ -63,11 +51,9 @@ public abstract class AbstractVampireLanguageProposalProvider extends TerminalsP completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor); } public void completeVLSTffFormula_Name(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { - completeRuleCall(((RuleCall)((Alternatives)assignment.getTerminal()).getElements().get(0)), context, acceptor); - completeRuleCall(((RuleCall)((Alternatives)assignment.getTerminal()).getElements().get(1)), context, acceptor); - completeRuleCall(((RuleCall)((Alternatives)assignment.getTerminal()).getElements().get(2)), context, acceptor); + completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor); } - public void completeVLSTffFormula_FofRole(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + public void completeVLSTffFormula_TffRole(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor); } public void completeVLSTffFormula_FofFormula(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { @@ -87,17 +73,37 @@ public abstract class AbstractVampireLanguageProposalProvider extends TerminalsP public void completeVLSAnnotationTerms_Terms(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor); } + public void completeVLSOtherDeclaration_Type(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor); + } + public void completeVLSVariableDeclaration_Type(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor); + } + public void completeVLSTypeDef_TypeSig(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor); + } + public void completeVLSTypeDef_MapsTo(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor); + } + public void completeVLSUnitaryTerm_InitType(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor); + } + public void completeVLSUnitaryTerm_NextType(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor); + } public void completeVLSBinary_Right(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor); } public void completeVLSUniversalQuantifier_Variables(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { - completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor); + completeRuleCall(((RuleCall)((Alternatives)assignment.getTerminal()).getElements().get(0)), context, acceptor); + completeRuleCall(((RuleCall)((Alternatives)assignment.getTerminal()).getElements().get(1)), context, acceptor); } public void completeVLSUniversalQuantifier_Operand(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor); } public void completeVLSExistentialQuantifier_Variables(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { - completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor); + completeRuleCall(((RuleCall)((Alternatives)assignment.getTerminal()).getElements().get(0)), context, acceptor); + completeRuleCall(((RuleCall)((Alternatives)assignment.getTerminal()).getElements().get(1)), context, acceptor); } public void completeVLSExistentialQuantifier_Operand(EObject model, Assignment assignment, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { completeRuleCall(((RuleCall)assignment.getTerminal()), context, acceptor); @@ -177,58 +183,58 @@ public abstract class AbstractVampireLanguageProposalProvider extends TerminalsP public void complete_SIGNED_LITERAL(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { // subclasses may override } - public void complete_UNSIGNED_REAL_FRAC_ID(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + public void complete_SINGLE_COMMENT(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { // subclasses may override } - public void complete_UNSIGNED_REAL_EXP_ID(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + public void complete_VLSComment(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { // subclasses may override } - public void complete_SIGNED_REAL_ID(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + public void complete_VLSConfirmations(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { // subclasses may override } - public void complete_UNSIGNED_RAT_ID(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + public void complete_VLSFofFormula(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { // subclasses may override } - public void complete_SIGNED_RAT_ID(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + public void complete_VLSTffFormula(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { // subclasses may override } - public void complete_ID(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + public void complete_VLSTffName(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { // subclasses may override } - public void complete_ANY_OTHER(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + public void complete_VLSTffDistinct(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { // subclasses may override } - public void complete_SINGLE_COMMENT(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + public void complete_VLSTffFinite(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { // subclasses may override } - public void complete_VLSInclude(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + public void complete_VLSTffDeclPred(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { // subclasses may override } - public void complete_VLSName(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + public void complete_VLSRole(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { // subclasses may override } - public void complete_VLSComment(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + public void complete_VLSAnnotation(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { // subclasses may override } - public void complete_VLSConfirmations(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + public void complete_VLSAnnotationTerms(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { // subclasses may override } - public void complete_VLSSatisfiable(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + public void complete_VLSTffTerm(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { // subclasses may override } - public void complete_VLSFofFormula(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + public void complete_VLSDeclaration(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { // subclasses may override } - public void complete_VLSTffFormula(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + public void complete_VLSOtherDeclaration(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { // subclasses may override } - public void complete_VLSRole(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + public void complete_VLSVariableDeclaration(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { // subclasses may override } - public void complete_VLSAnnotation(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + public void complete_VLSTypeDef(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { // subclasses may override } - public void complete_VLSAnnotationTerms(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { + public void complete_VLSUnitaryTerm(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { // subclasses may override } public void complete_VLSTerm(EObject model, RuleCall ruleCall, ContentAssistContext context, ICompletionProposalAcceptor acceptor) { diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin index ac318322..854cd91f 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin index 7710f730..3640f798 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin differ -- cgit v1.2.3-54-g00ecf