package at.ac.tuwien.kr.alpha.core.atoms;

import static org.junit.jupiter.api.Assertions.assertEquals;

import org.junit.jupiter.api.Test;

import at.ac.tuwien.kr.alpha.api.grounder.Substitution;
import at.ac.tuwien.kr.alpha.api.programs.Predicate;
import at.ac.tuwien.kr.alpha.api.programs.ProgramParser;
import at.ac.tuwien.kr.alpha.api.programs.atoms.BasicAtom;
import at.ac.tuwien.kr.alpha.api.programs.rules.Rule;
import at.ac.tuwien.kr.alpha.api.programs.rules.heads.Head;
import at.ac.tuwien.kr.alpha.api.programs.terms.ConstantTerm;
import at.ac.tuwien.kr.alpha.api.programs.terms.VariableTerm;
import at.ac.tuwien.kr.alpha.commons.Predicates;
import at.ac.tuwien.kr.alpha.commons.programs.atoms.Atoms;
import at.ac.tuwien.kr.alpha.commons.programs.rules.Rules;
import at.ac.tuwien.kr.alpha.commons.programs.terms.Terms;
import at.ac.tuwien.kr.alpha.commons.substitutions.BasicSubstitution;
import at.ac.tuwien.kr.alpha.commons.substitutions.Instance;
import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl;
import at.ac.tuwien.kr.alpha.core.programs.atoms.RuleAtom;
import at.ac.tuwien.kr.alpha.core.programs.rules.CompiledRule;
import at.ac.tuwien.kr.alpha.core.programs.rules.InternalRule;

/**
 * Copyright (c) 2022, the Alpha Team.
 */
public class RuleAtomTest {
	private static final ProgramParser PARSER = new ProgramParserImpl();

	private static final VariableTerm X = Terms.newVariable("X");
	private static final VariableTerm Y = Terms.newVariable("Y");
	private static final Predicate PREDICATE = Predicates.getPredicate("p", 1);
	private static final BasicAtom PX = Atoms.newBasicAtom(PREDICATE, X);
	private static final BasicAtom PY = Atoms.newBasicAtom(PREDICATE, Y);

	@Test
	public void substitutionObtainableFromRuleAtom() {
		Rule<Head> rule = PARSER.parse("q(X) :- p(X,Y).").getRules().get(0);
		CompiledRule nonGroundRule = InternalRule.fromNormalRule(Rules.toNormalRule(rule));
		// Build substitution X -> a, Y -> b.
		Substitution substitution = BasicSubstitution.specializeSubstitution(
			PY, new Instance(Terms.newSymbolicConstant("b")), BasicSubstitution.specializeSubstitution(
			PX, new Instance(Terms.newSymbolicConstant("a")), BasicSubstitution.EMPTY_SUBSTITUTION));

		RuleAtom ruleAtom = new RuleAtom(nonGroundRule, substitution);
		RuleAtom.RuleAtomData substitutionFromRuleAtom = (RuleAtom.RuleAtomData) ((ConstantTerm<?>) ruleAtom.getTerms().get(0)).getObject();
		assertEquals(substitution, substitutionFromRuleAtom.getSubstitution());
	}

	@Test
	public void substitutionWithFunctionTermsObtainableFromRuleAtom() {
		Rule<Head> rule = PARSER.parse("q(X) :- p(X,Y).").getRules().get(0);
		CompiledRule nonGroundRule = InternalRule.fromNormalRule(Rules.toNormalRule(rule));
		// Build substitution X -> b(a,a), Y -> b(b(a,a),b(a,a)).
		BasicAtom atomForSpecialize = Atoms.newBasicAtom(Predicates.getPredicate("p", 2), X, Y);
		ConstantTerm<String> aTerm = Terms.newSymbolicConstant("a");
		Instance instanceForSpecialize = new Instance(Terms.newFunctionTerm("b", aTerm, aTerm),
			Terms.newFunctionTerm("b",
				Terms.newFunctionTerm("b", aTerm, aTerm),
				Terms.newFunctionTerm("b", aTerm, aTerm)));
		Substitution substitution = BasicSubstitution.specializeSubstitution(
			atomForSpecialize, instanceForSpecialize, BasicSubstitution.EMPTY_SUBSTITUTION);

		RuleAtom ruleAtom = new RuleAtom(nonGroundRule, substitution);
		RuleAtom.RuleAtomData substitutionFromRuleAtom = (RuleAtom.RuleAtomData) ((ConstantTerm<?>) ruleAtom.getTerms().get(0)).getObject();
		assertEquals(substitution, substitutionFromRuleAtom.getSubstitution());
	}
}