/*
* 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);
	}
}

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

import java.util.HashSet;
import java.util.Set;

import jkind.xtext.jkind.Assertion;
import jkind.xtext.jkind.Constant;
import jkind.xtext.jkind.Equation;
import jkind.xtext.jkind.Field;
import jkind.xtext.jkind.JkindPackage;
import jkind.xtext.jkind.Property;
import jkind.xtext.jkind.RecordExpr;
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");
		}
	}

	@Check
	public void checkRecordExprFieldsUnique(RecordExpr record) {
		Set<Field> seen = new HashSet<>();
		Set<Field> marked = new HashSet<>();
		for (Field field : record.getFields()) {
			if (seen.contains(field) && !marked.contains(field)) {
				marked.add(field);
				errorDuplicateField(record, field);
			}
			seen.add(field);
		}
	}

	private void errorDuplicateField(RecordExpr record, Field field) {
		for (int i = 0; i < record.getFields().size(); i++) {
			if (record.getFields().get(i).equals(field)) {
				error("Duplicate field " + field.getName(), record,
						JkindPackage.Literals.RECORD_EXPR__FIELDS, i);
			}
		}
	}

	private void error(String message) {
		error(message, null);
	}
}

Check for duplicate fields