<commit_before>package validator;

import java.io.BufferedReader;
import java.io.File;
import java.io.FileNotFoundException;
import java.io.FileReader;
import java.io.IOException;
import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Queue;
import java.util.Set;
import java.util.Stack;

import util.game.GameRepository;
import util.game.TestGameRepository;
import util.gdl.grammar.Gdl;
import util.gdl.grammar.GdlConstant;
import util.gdl.grammar.GdlDistinct;
import util.gdl.grammar.GdlFunction;
import util.gdl.grammar.GdlLiteral;
import util.gdl.grammar.GdlNot;
import util.gdl.grammar.GdlOr;
import util.gdl.grammar.GdlPool;
import util.gdl.grammar.GdlProposition;
import util.gdl.grammar.GdlRelation;
import util.gdl.grammar.GdlRule;
import util.gdl.grammar.GdlSentence;
import util.gdl.grammar.GdlTerm;
import util.gdl.grammar.GdlVariable;
import validator.exception.StaticValidatorException;

public class StaticValidator {
	private static final GdlConstant ROLE = GdlPool.getConstant("role");
	private static final GdlConstant TERMINAL = GdlPool.getConstant("terminal");
	private static final GdlConstant GOAL = GdlPool.getConstant("goal");
	private static final GdlConstant LEGAL = GdlPool.getConstant("legal");
	private static final GdlConstant DOES = GdlPool.getConstant("does");
	private static final GdlConstant INIT = GdlPool.getConstant("init");
	private static final GdlConstant TRUE = GdlPool.getConstant("true");
	private static final GdlConstant NEXT = GdlPool.getConstant("next");
	private static final GdlConstant BASE = GdlPool.getConstant("base");
	private static final GdlConstant INPUT = GdlPool.getConstant("input");

	/**
	 * Validates whether a GDL description follows the rules of GDL,
	 * to the extent that it can be determined. If the description is
	 * invalid, throws an exception of type StaticValidatorException
	 * explaining the problem.
	 * 
	 * Features like finitism and monotonicity can't be definitively determined
	 * with a static analysis; these are left to the other validator. (See
	 * GdlValidator and the ValidatorPanel in apps.validator.)
	 * 
	 * @param description A parsed GDL game description.
	 * @throws StaticValidatorException The description did not pass validation.
	 * The error message explains the error found in the GDL description.
	 */
	public static void validateDescription(List<Gdl> description) throws StaticValidatorException {
		/* This assumes that the description is already well-formed enough
		 * to be made into a list of Gdl objects. We need to check those
		 * remaining features that can be verified here.
		 * 
		 * A + is an implemented test; a - is not (fully) implemented.
		 *
		 * Features of negated datalog with functions:
		 * + All negations apply directly to sentences
		 * + All rules are safe: All variables in the rule must appear
		 *   in some positive relation in the body.
		 * + Arities of relation constants and function constants are fixed
		 * + The rules are stratified: The dependency graph generated by
		 *   the rules must contain no cycles with a negative edge.
		 * + Added restriction on functions and recursion
		 * Additional features of GDL:
		 * + Role relations must be ground sentences, not in rules
		 * - Inits only in heads of rules; not in same CC as true, does, next, legal, goal, terminal
		 * + Trues only in bodies of rules, not heads
		 * + Nexts only in heads of rules
		 * - Does only in bodies of rules; no paths between does and legal/goal/terminal
		 *
		 * + Arities: Role 1, true 1, init 1, next 1, legal 2, does 2, goal 2, terminal 0
		 * - Legal's first argument must be a player; ditto does, goal
		 * - Goal values are integers between 0 and 100
		 * Misc.:
		 * + All objects are relations or rules
		 *
		 * Things we can't really test here:
		 * - In all cases, valid arguments to does, goal, legal
		 * - Game terminality
		 * - Players have goals in all states, exactly one goal in each state,
		 *   and those goals are monotonic
		 * - Playability: legal moves for each player in each non-terminal state
		 * - Weak winnability
		 *
		 * Reference for the restrictions: http://games.stanford.edu/language/spec/gdl_spec_2008_03.pdf
		 */
		
		List<GdlRelation> relations = new ArrayList<GdlRelation>();
		List<GdlRule> rules = new ArrayList<GdlRule>();
		//1) Are all objects in the description rules or relations?
		for(Gdl gdl : description) {
			if(gdl instanceof GdlRelation) {
				relations.add((GdlRelation) gdl);
			} else if(gdl instanceof GdlRule) {
				rules.add((GdlRule) gdl);
			} else {
				throw new StaticValidatorException("The rules include a GDL object of type " + gdl.getClass().getSimpleName() + ". Only GdlRelations and GdlRules are expected.");
			}
		}
		//2) Do all negations apply directly to sentences?
		for(GdlRule rule : rules) {
			for(GdlLiteral literal : rule.getBody()) {
				testLiteralForImproperNegation(literal);
			}
		}
		//3) Are the arities of all relations and all functions fixed?
		Map<GdlConstant, Integer> sentenceArities = new HashMap<GdlConstant, Integer>();
		Map<GdlConstant, Integer> functionArities = new HashMap<GdlConstant, Integer>();
		for(GdlRelation relation : relations) {
			addSentenceArity(relation, sentenceArities);
			addFunctionArities(relation, functionArities);
		}
		for(GdlRule rule : rules) {<commit_msg>Improve an error message.<commit_after>package validator;

import java.io.BufferedReader;
import java.io.File;
import java.io.FileNotFoundException;
import java.io.FileReader;
import java.io.IOException;
import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Queue;
import java.util.Set;
import java.util.Stack;

import util.game.GameRepository;
import util.game.TestGameRepository;
import util.gdl.grammar.Gdl;
import util.gdl.grammar.GdlConstant;
import util.gdl.grammar.GdlDistinct;
import util.gdl.grammar.GdlFunction;
import util.gdl.grammar.GdlLiteral;
import util.gdl.grammar.GdlNot;
import util.gdl.grammar.GdlOr;
import util.gdl.grammar.GdlPool;
import util.gdl.grammar.GdlProposition;
import util.gdl.grammar.GdlRelation;
import util.gdl.grammar.GdlRule;
import util.gdl.grammar.GdlSentence;
import util.gdl.grammar.GdlTerm;
import util.gdl.grammar.GdlVariable;
import validator.exception.StaticValidatorException;

public class StaticValidator {
	private static final GdlConstant ROLE = GdlPool.getConstant("role");
	private static final GdlConstant TERMINAL = GdlPool.getConstant("terminal");
	private static final GdlConstant GOAL = GdlPool.getConstant("goal");
	private static final GdlConstant LEGAL = GdlPool.getConstant("legal");
	private static final GdlConstant DOES = GdlPool.getConstant("does");
	private static final GdlConstant INIT = GdlPool.getConstant("init");
	private static final GdlConstant TRUE = GdlPool.getConstant("true");
	private static final GdlConstant NEXT = GdlPool.getConstant("next");
	private static final GdlConstant BASE = GdlPool.getConstant("base");
	private static final GdlConstant INPUT = GdlPool.getConstant("input");

	/**
	 * Validates whether a GDL description follows the rules of GDL,
	 * to the extent that it can be determined. If the description is
	 * invalid, throws an exception of type StaticValidatorException
	 * explaining the problem.
	 * 
	 * Features like finitism and monotonicity can't be definitively determined
	 * with a static analysis; these are left to the other validator. (See
	 * GdlValidator and the ValidatorPanel in apps.validator.)
	 * 
	 * @param description A parsed GDL game description.
	 * @throws StaticValidatorException The description did not pass validation.
	 * The error message explains the error found in the GDL description.
	 */
	public static void validateDescription(List<Gdl> description) throws StaticValidatorException {
		/* This assumes that the description is already well-formed enough
		 * to be made into a list of Gdl objects. We need to check those
		 * remaining features that can be verified here.
		 * 
		 * A + is an implemented test; a - is not (fully) implemented.
		 *
		 * Features of negated datalog with functions:
		 * + All negations apply directly to sentences
		 * + All rules are safe: All variables in the rule must appear
		 *   in some positive relation in the body.
		 * + Arities of relation constants and function constants are fixed
		 * + The rules are stratified: The dependency graph generated by
		 *   the rules must contain no cycles with a negative edge.
		 * + Added restriction on functions and recursion
		 * Additional features of GDL:
		 * + Role relations must be ground sentences, not in rules
		 * - Inits only in heads of rules; not in same CC as true, does, next, legal, goal, terminal
		 * + Trues only in bodies of rules, not heads
		 * + Nexts only in heads of rules
		 * - Does only in bodies of rules; no paths between does and legal/goal/terminal
		 *
		 * + Arities: Role 1, true 1, init 1, next 1, legal 2, does 2, goal 2, terminal 0
		 * - Legal's first argument must be a player; ditto does, goal
		 * - Goal values are integers between 0 and 100
		 * Misc.:
		 * + All objects are relations or rules
		 *
		 * Things we can't really test here:
		 * - In all cases, valid arguments to does, goal, legal
		 * - Game terminality
		 * - Players have goals in all states, exactly one goal in each state,
		 *   and those goals are monotonic
		 * - Playability: legal moves for each player in each non-terminal state
		 * - Weak winnability
		 *
		 * Reference for the restrictions: http://games.stanford.edu/language/spec/gdl_spec_2008_03.pdf
		 */
		
		List<GdlRelation> relations = new ArrayList<GdlRelation>();
		List<GdlRule> rules = new ArrayList<GdlRule>();
		//1) Are all objects in the description rules or relations?
		for(Gdl gdl : description) {
			if(gdl instanceof GdlRelation) {
				relations.add((GdlRelation) gdl);
			} else if(gdl instanceof GdlRule) {
				rules.add((GdlRule) gdl);
			} else {
				throw new StaticValidatorException("The rules include a GDL object of type " + gdl.getClass().getSimpleName() + ". Only GdlRelations and GdlRules are expected. The Gdl object is: " + gdl);
			}
		}
		//2) Do all negations apply directly to sentences?
		for(GdlRule rule : rules) {
			for(GdlLiteral literal : rule.getBody()) {
				testLiteralForImproperNegation(literal);
			}
		}
		//3) Are the arities of all relations and all functions fixed?
		Map<GdlConstant, Integer> sentenceArities = new HashMap<GdlConstant, Integer>();
		Map<GdlConstant, Integer> functionArities = new HashMap<GdlConstant, Integer>();
		for(GdlRelation relation : relations) {
			addSentenceArity(relation, sentenceArities);
			addFunctionArities(relation, functionArities);
		}
		for(GdlRule rule : rules) {
{'fraction_non_alphanumeric': 0.08486782133090247, 'fraction_numerical': 0.003828623518687329, 'mean_word_length': 4.165254237288136, 'pattern_counts': {'":': 0, '<': 21, '<?xml version=': 0, '>': 21, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1358539', 'n_tokens_mistral': 3455, 'n_tokens_neox': 3099, 'n_words': 1152}