/*
* generated by Xtext
*/
package jkind.xtext.validation;

import jkind.xtext.jkind.Assertion;
import jkind.xtext.jkind.Constant;
import jkind.xtext.jkind.Equation;
import jkind.xtext.jkind.Property;
import jkind.xtext.jkind.SubrangeType;
import jkind.xtext.typing.TypeChecker;

import org.eclipse.xtext.validation.Check;

/**
 * Custom validation rules. 
 *
 * see http://www.eclipse.org/Xtext/documentation.html#validation
 */
public class JKindJavaValidator extends jkind.xtext.validation.AbstractJKindJavaValidator {
	@Check
	public void checkEquationType(Equation equation) {
		new TypeChecker(getMessageAcceptor()).check(equation);
	}
	
	@Check
	public void checkAssertionType(Assertion assertion) {
		new TypeChecker(getMessageAcceptor()).check(assertion);
	}
	
	@Check
	public void checkPropertyType(Property property) {
		new TypeChecker(getMessageAcceptor()).check(property);
	}
	
	@Check
	public void checkConstantType(Constant constant) {
		new TypeChecker(getMessageAcceptor()).check(constant);
	}
	
	@Check
	public void checkSubrangeNonempty(SubrangeType subrangeType) {
		if (subrangeType.getLow().compareTo(subrangeType.getHigh()) > 0) {
			error("Subrange must be non-empty");
		}
	}
	
	@Check
	public void checkConstantHasConstantValue(Constant constant) {
		if (!new ConstantAnalyzer().doSwitch(constant.getExpr())) {
			error(constant.getName() + " does not have constant value");
		}
	}
	
	private void error(String message) {
		error(message, null);
	}
}

@@ -1,11 +1,12 @@
 /*%0A
+ 
 * genera
@@ -18,16 +18,17 @@
 y Xtext%0A
+ 
 */%0Apacka
@@ -55,16 +55,65 @@
 ation;%0A%0A
+import java.util.HashSet;%0Aimport java.util.Set;%0A%0A
 import j
@@ -235,24 +235,132 @@
 t.jkind.
-Property
+Field;%0Aimport jkind.xtext.jkind.JkindPackage;%0Aimport jkind.xtext.jkind.Property;%0Aimport jkind.xtext.jkind.RecordExpr
 ;%0Aimport
@@ -511,12 +511,12 @@
 les.
- 
 %0A *
+ 
 %0A * 
@@ -786,33 +786,32 @@
 k(equation);%0A%09%7D%0A
-%09
 %0A%09@Check%0A%09public
@@ -915,25 +915,24 @@
 ertion);%0A%09%7D%0A
-%09
 %0A%09@Check%0A%09pu
@@ -1036,25 +1036,24 @@
 operty);%0A%09%7D%0A
-%09
 %0A%09@Check%0A%09pu
@@ -1157,25 +1157,24 @@
 nstant);%0A%09%7D%0A
-%09
 %0A%09@Check%0A%09pu
@@ -1350,17 +1350,16 @@
 %0A%09%09%7D%0A%09%7D%0A
-%09
 %0A%09@Check
@@ -1556,17 +1556,655 @@
 %0A%09%09%7D%0A%09%7D%0A
-%09
+%0A%09@Check%0A%09public void checkRecordExprFieldsUnique(RecordExpr record) %7B%0A%09%09Set%3CField%3E seen = new HashSet%3C%3E();%0A%09%09Set%3CField%3E marked = new HashSet%3C%3E();%0A%09%09for (Field field : record.getFields()) %7B%0A%09%09%09if (seen.contains(field) && !marked.contains(field)) %7B%0A%09%09%09%09marked.add(field);%0A%09%09%09%09errorDuplicateField(record, field);%0A%09%09%09%7D%0A%09%09%09seen.add(field);%0A%09%09%7D%0A%09%7D%0A%0A%09private void errorDuplicateField(RecordExpr record, Field field) %7B%0A%09%09for (int i = 0; i %3C record.getFields().size(); i++) %7B%0A%09%09%09if (record.getFields().get(i).equals(field)) %7B%0A%09%09%09%09error(%22Duplicate field %22 + field.getName(), record,%0A%09%09%09%09%09%09JkindPackage.Literals.RECORD_EXPR__FIELDS, i);%0A%09%09%09%7D%0A%09%09%7D%0A%09%7D%0A
 %0A%09privat

Check for duplicate fields