1 files changed, 307 insertions, 0 deletions
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..7d20da72
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext
@@ -0,0 +1,307 @@
+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:   
+        (
+                includes += VLSInclude |
+                comments += VLSComment | 
+                confirmations += VLSConfirmations|
+                formulas += VLSFofFormula |
+                tfformulas += VLSTffFormula
+                
+        )*      
+;
+//////////////////////////////////
+// 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 ID: (!('\n'|'\r'))* ;
+terminal ANY_OTHER: ID;
+terminal SINGLE_COMMENT: ANY_OTHER;
+//terminal ID:  ( !('('|')'|'\r'|'\n') )+ ;
+//////////////////////////////////
+// VLS types
+//////////////////////////////////
+// <includes>
+VLSInclude:
+        'include(' fileName = SINGLE_QUOTE ( ',[' names += VLSName (','  names += VLSName)* ']' )?
+;
+VLSName:
+        name = (LOWER_WORD_ID | SINGLE_QUOTE | LITERAL | SIGNED_LITERAL)
+;
+// <comments>
+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 );
+VLSConfirmations:
+          VLSSatisfiable //| VLSFiniteModel// | VLSTrying
+;
+VLSSatisfiable:
+        {VLSSatisfiable} 'Satisfiable!'
+;
+//VLSTrying:
+//      'TRYING' '[' name = LITERAL ']'
+//;
+//
+//VLSFiniteModel:
+//      {VLSFiniteModel} 'Finite' 'Model' 'Found!'
+//;
+// <FOF formulas>
+VLSFofFormula:
+        'fof' '(' name = (LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole = VLSRole ',' fofFormula = VLSTerm (',' annotations = VLSAnnotation)? ')' '.'
+;
+VLSTffFormula:
+        'tff' '(' 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)
+;
+*/
+//<ROLE>
+VLSRole:
+        "axiom" | "conjecture" | "hypothesis" | "definition" | "assumption" | "lemma"
+        | "theorem" |   "corollary" | "negated_conjecture" | "plain" | "type" |
+        "fi_domain" | "fi_functors" | "fi_predicates" | "unknown"
+;
+//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"
+//;
+// <ANNOTATION>
+// 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 | VLSFunctionAsTerm | VLSDefinedTerm )
+;
+VLSFunctionAsTerm:
+        //? 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/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..7d20da72 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext
@@ -0,0 +1,307 @@
	1	grammar ca.mcgill.ecse.dslreasoner.VampireLanguage with org.eclipse.xtext.common.Terminals hidden (WS)
	2
	3	generate vampireLanguage "http://www.mcgill.ca/ecse/dslreasoner/VampireLanguage"
	4
	5	//@@@@@@@@@@@
	6	//2 things TODO:
	7	//1. fix anotations (ln77)
	8	//2. can only use declared variables in formula (ln 158)
	9
	10	//@@@@@@@@@@@
	11
	12	VampireModel:
	13	(
	14	includes += VLSInclude \|
	15	comments += VLSComment \|
	16	confirmations += VLSConfirmations\|
	17	formulas += VLSFofFormula \|
	18	tfformulas += VLSTffFormula
	19
	20	)*
	21	;
	22
	23	//////////////////////////////////
	24	// VLS terminals
	25	//////////////////////////////////
	26
	27	terminal ALPHA_NUMERIC: ( 'a'..'z' \| 'A'..'Z' \| '0'..'9' \| '_');
	28	terminal UPPER_WORD_ID: ('A'..'Z') (ALPHA_NUMERIC)*;
	29	terminal LOWER_WORD_ID: ('a'..'z') (ALPHA_NUMERIC)*;
	30
	31
	32	//TODO MIGHT NEED TO IMPLEMENT SOME WAY TO ONLY CONSIDER WHAT IS INSIDE QUOTES AS NAME
	33	//incorporate quotes in the line of calling. ex. "'" name=SINGLEQUOTE "'"
	34	terminal DOUBLE_QUOTE: '"' ( '\\' ('"'\|'\\') \| !('\\'\|'"') )* '"';//from terminal STRING rule, positive about this
	35	terminal SINGLE_QUOTE: "'" ( '\\' ("'"\|'\\') \| !('\\'\|"'") )+ "'";//from terminal STRING rule, positive about this
	36
	37	terminal SIGN: ('+' \| '-');
	38
	39	terminal DOLLAR_ID: ('$') (LOWER_WORD_ID);
	40	terminal DOUBLE_DOLLAR_ID: ('$$') (LOWER_WORD_ID);
	41
	42	terminal LITERAL: '0' \| ('1'..'9') (INT)?;
	43	terminal SIGNED_LITERAL: (SIGN)* (LITERAL);
	44
	45	terminal UNSIGNED_REAL_FRAC_ID: (LITERAL) ('.') (INT);
	46	terminal UNSIGNED_REAL_EXP_ID: (LITERAL \| UNSIGNED_REAL_FRAC_ID) ('Ee') (SIGN)* (INT) ;
	47	terminal SIGNED_REAL_ID: (SIGN)* (UNSIGNED_REAL_FRAC_ID \| UNSIGNED_REAL_EXP_ID);
	48
	49	terminal UNSIGNED_RAT_ID: (LITERAL) ('/') ('1'..'9') (INT)? ;
	50	terminal SIGNED_RAT_ID: (SIGN)* (UNSIGNED_RAT_ID);
	51
	52	//Overwriting is necessary
	53	terminal ID: (!('\n'\|'\r'))* ;
	54	terminal ANY_OTHER: ID;
	55	terminal SINGLE_COMMENT: ANY_OTHER;
	56	//terminal ID: ( !('('\|')'\|'\r'\|'\n') )+ ;
	57
	58
	59	//////////////////////////////////
	60	// VLS types
	61	//////////////////////////////////
	62
	63	// <includes>
	64	VLSInclude:
	65	'include(' fileName = SINGLE_QUOTE ( ',[' names += VLSName (',' names += VLSName)* ']' )?
	66	;
	67
	68	VLSName:
	69	name = (LOWER_WORD_ID \| SINGLE_QUOTE \| LITERAL \| SIGNED_LITERAL)
	70	;
	71
	72	// <comments>
	73	VLSComment:
	74	'%' comment = SINGLE_COMMENT
	75	//need to add a new line at the end of the file for the case where the last line is a comment
	76	;
	77
	78	//VLSConstantDeclaration: name = (LOWER_WORD_ID \| SINGLE_QUOTE \| DOLLAR_ID \| DOUBLE_DOLLAR_ID );
	79
	80	VLSConfirmations:
	81	VLSSatisfiable //\| VLSFiniteModel// \| VLSTrying
	82	;
	83
	84	VLSSatisfiable:
	85	{VLSSatisfiable} 'Satisfiable!'
	86	;
	87
	88	//VLSTrying:
	89	// 'TRYING' '[' name = LITERAL ']'
	90	//;
	91	//
	92	//VLSFiniteModel:
	93	// {VLSFiniteModel} 'Finite' 'Model' 'Found!'
	94	//;
	95
	96	// <FOF formulas>
	97	VLSFofFormula:
	98	'fof' '(' name = (LOWER_WORD_ID \| SIGNED_LITERAL \| SINGLE_QUOTE) ',' fofRole = VLSRole ',' fofFormula = VLSTerm (',' annotations = VLSAnnotation)? ')' '.'
	99	;
	100
	101
	102	VLSTffFormula:
	103	'tff' '(' name = (LOWER_WORD_ID \| SIGNED_LITERAL \| SINGLE_QUOTE) ',' fofRole = VLSRole ',' fofFormula = VLSTerm (',' annotations = VLSAnnotation)? ')' '.'
	104	;
	105
	106
	107	/*
	108	//NAME
	109	VLSName:
	110	//(atomic_Word = Atomic_Word \| integer = Integer \| single_quote_word = Single_Quote_Word)
	111	name = (LOWER_WORD_ID \| SIGNED_INT_ID \| SINGLE_QUOTE)
	112	;
	113	*/
	114	//<ROLE>
	115	VLSRole:
	116	"axiom" \| "conjecture" \| "hypothesis" \| "definition" \| "assumption" \| "lemma"
	117	\| "theorem" \| "corollary" \| "negated_conjecture" \| "plain" \| "type" \|
	118	"fi_domain" \| "fi_functors" \| "fi_predicates" \| "unknown"
	119	;
	120
	121	//VLSRole:
	122	// VLSAxiom \| VLSConjecture \| VLSHypothesis \| VLSDefinition \|
	123	// VLSAssumption \| VLSLemma \| VLSTheorem \| VLSCorollary \| VLSNegated_Conjecture \|
	124	// VLSPlain \| VLSType \|VLSFi_Domain \| VLSFi_Functors \| VLSFi_Predicates \| VLSUnknown
	125	//;
	126	//
	127	//VLSAxiom:
	128	// "axiom"
	129	//;
	130	//
	131	//VLSConjecture:
	132	// "conjecture"
	133	//;
	134	//
	135	//VLSHypothesis:
	136	// "hypothesis"
	137	//;
	138	//
	139	//VLSDefinition:
	140	// "definition"
	141	//;
	142	//
	143	//VLSAssumption:
	144	// "assumption"
	145	//;
	146	//
	147	//VLSLemma:
	148	// "lemma"
	149	//;
	150	//
	151	//VLSTheorem:
	152	// "theorem"
	153	//;
	154	//
	155	//VLSCorollary:
	156	// "corollary"
	157	//;
	158	//
	159	//VLSNegated_Conjecture:
	160	// "negated_conjecture"
	161	//;
	162	//
	163	//VLSPlain:
	164	// "plain"
	165	//;
	166	//
	167	//VLSType:
	168	// "type"
	169	//;
	170	//
	171	//VLSFi_Domain:
	172	// "fi_domain"
	173	//;
	174	//
	175	//VLSFi_Functors:
	176	// "fi_functors"
	177	//;
	178	//
	179	//VLSFi_Predicates:
	180	// "fi_predicates"
	181	//;
	182	//
	183	//VLSUnknown:
	184	// "unknown"
	185	//;
	186
	187	// <ANNOTATION>
	188	// Not at all based on the website. based on what we think the output will be like
	189	VLSAnnotation:
	190	('[')? (name = (LOWER_WORD_ID \| SINGLE_QUOTE \| VLSRole))? ( '(' followup = VLSAnnotationTerms ')' )? (']')?
	191	;
	192
	193	VLSAnnotationTerms returns VLSAnnotation:
	194	terms += VLSAnnotation (',' terms += VLSAnnotation )*
	195	;
	196
	197	//////////////////////////////////
	198	// VLS Terms
	199	//////////////////////////////////
	200
	201	VLSTerm:
	202	//( VLSLogic \| VLSSequent)
	203	VLSBinary
	204	;
	205	//*
	206	//VLSBinaryFormula
	207	VLSBinary returns VLSTerm:
	208	VLSUnitaryFormula
	209	(
	210	(({VLSEquivalent.left = current} "<=>" \|
	211	{VLSImplies.left = current} "=>" \|
	212	{VLSRevImplies.left = current} "<=" \|
	213	{VLSXnor.left = current} "<~>" \|
	214	{VLSNor.left = current} "~\|" \|
	215	{VLSNand.left = current} "~&") right = VLSUnitaryFormula)
	216	\|
	217	({VLSAnd.left = current} '&' right = VLSUnitaryFormula)+
	218	\|
	219	({VLSOr.left = current} '\|' right = VLSUnitaryFormula)+
	220	)?
	221	;
	222
	223	//VLSUnitaryFormula
	224	VLSUnitaryFormula returns VLSTerm:
	225	VLSUniversalQuantifier \| VLSExistentialQuantifier \| VLSUnaryNegation \| VLSUnaryInfix
	226	//\| VLSEquality
	227	\| '(' VLSTerm ')'
	228	;
	229
	230	VLSUniversalQuantifier returns VLSTerm:
	231	{VLSUniversalQuantifier} (("!") '[' variables += VLSVariable (',' variables += VLSVariable)* ']' ':') operand = VLSUnitaryFormula
	232	;
	233
	234	VLSExistentialQuantifier returns VLSTerm:
	235	{VLSExistentialQuantifier} (("?") '[' variables += VLSVariable (',' variables += VLSVariable)* ']' ':') operand = VLSUnitaryFormula
	236	;
	237
	238	VLSUnaryNegation returns VLSTerm:
	239	{VLSUnaryNegation} ('~') operand = VLSUnitaryFormula
	240	;
	241
	242	VLSUnaryInfix returns VLSTerm:
	243	VLSAtomic (({VLSInequality.left = current} "!=" \|
	244	{VLSEquality.left = current} "=" \|
	245	{VLSAssignment.left = current} ":=")
	246	right = VLSAtomic)?
	247	;
	248
	249	//NOT SUREEEE
	250	//VLSEquality returns VLSTerm:
	251	// VLSFofTerm ({VLSEquality.left = current} "=" right = VLSFofTerm)?
	252	//
	253	//;
	254
	255	/*
	256	enum VLSDefinedFunctor:
	257	UMINUS='$uminus' \| SUM='$sum' \| DIFFERENCE='$difference' \| PRODUCT='$product' \| QUOTIENT='$quotient' \|
	258	QUOTIENT_E='$quotient_e' \| QUOTIENT_T='$quotient_t' \| QUOTIENT_F='$quotient_f' \| REMAINDER_E='$remainder_e' \|
	259	REMAINDER_T='$remainder_t' \| REMAINDER_F='$remainder_f' \| FLOOR='$floor' \| CEILING='$ceiling' \|
	260	TRUNCATE='$truncate' \| ROUND='$round' \| TO_INT='$to_int' \| TO_RAT='$to_rat' \| TO_REAL='$to_real'
	261	;
	262	*/
	263
	264	VLSAtomic returns VLSTerm:
	265	VLSAtomicConstant \| VLSAtomicFunction \| VLSVariable
	266	\| VLSDefinedTerm //temporary solution. this is only valid for equality, not for != or :=
	267	//\| VLSEquality
	268	;
	269
	270	VLSAtomicConstant returns VLSTerm:
	271	//{VLSConstant} name = VLSConstantDeclaration \|
	272	{VLSConstant} name = (LOWER_WORD_ID \| SINGLE_QUOTE \| DOLLAR_ID \| DOUBLE_DOLLAR_ID \| VLSRole) \|
	273	{VLSTrue} '$true' \|
	274	{VLSFalse} '$false'
	275	;
	276
	277	VLSAtomicFunction returns VLSTerm:
	278	//? on next line causes warning
	279	//TODO might need replace DOLLAR_ID with enum rule
	280	//{VLSFunction} name = VLSConstantDeclaration ( '(' terms += VLSFofTerm (',' terms += VLSFofTerm)* ')' ) \|
	281	{VLSFunction} constant = (LOWER_WORD_ID \| SINGLE_QUOTE \| DOLLAR_ID \| DOUBLE_DOLLAR_ID \| VLSRole ) ( '(' terms += VLSFofTerm (',' terms += VLSFofTerm)* ')') \|
	282	{VLSLess} name = '$less' '(' terms += VLSFofTerm ',' terms += VLSFofTerm ')'
	283	;
	284
	285	VLSVariable :
	286
	287	name = UPPER_WORD_ID
	288	;
	289
	290	VLSFofTerm returns VLSTerm:
	291	//(VLSVariable \| VLSFunction \| VLSTffConditional \| VLSTffLet \| VLSTffTuple)
	292	(VLSVariable \| VLSFunctionAsTerm \| VLSDefinedTerm )
	293	;
	294
	295	VLSFunctionAsTerm:
	296	//? on next line causes warning
	297	//TODO might need replace DOLLAR_ID with enum rule
	298	functor = (LOWER_WORD_ID \| SINGLE_QUOTE \| DOLLAR_ID \| DOUBLE_DOLLAR_ID ) ( '(' terms += VLSFofTerm (',' terms += VLSFofTerm)* ')')?
	299	;
	300
	301	VLSDefinedTerm:
	302	{VLSInt} value = SIGNED_LITERAL \|
	303	{VLSReal} value = SIGNED_REAL_ID \|
	304	{VLSRational} value = SIGNED_RAT_ID \|
	305	{VLSDoubleQuote} value = DOUBLE_QUOTE
	306	;
	307