/**
 * Copyright (c) 2016-2017, the Alpha Team.
 * All rights reserved.
 *
 * Additional changes made by Siemens.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * 1) Redistributions of source code must retain the above copyright notice, this
 *    list of conditions and the following disclaimer.
 *
 * 2) Redistributions in binary form must reproduce the above copyright notice,
 *    this list of conditions and the following disclaimer in the documentation
 *    and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package at.ac.tuwien.kr.alpha.core.parser;

import static org.junit.jupiter.api.Assertions.assertEquals;
import static org.junit.jupiter.api.Assertions.assertFalse;
import static org.junit.jupiter.api.Assertions.assertThrows;
import static org.junit.jupiter.api.Assertions.assertTrue;

import java.io.IOException;
import java.nio.channels.ReadableByteChannel;
import java.util.Arrays;
import java.util.Collections;
import java.util.List;
import java.util.Optional;
import java.util.stream.Stream;

import at.ac.tuwien.kr.alpha.api.programs.tests.Assertion;
import at.ac.tuwien.kr.alpha.api.programs.tests.TestCase;
import org.antlr.v4.runtime.CharStream;
import org.antlr.v4.runtime.CharStreams;
import org.junit.jupiter.api.Test;

import at.ac.tuwien.kr.alpha.api.programs.ASPCore2Program;
import at.ac.tuwien.kr.alpha.api.programs.InlineDirectives;
import at.ac.tuwien.kr.alpha.api.programs.atoms.AggregateAtom;
import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom;
import at.ac.tuwien.kr.alpha.api.programs.literals.AggregateLiteral;
import at.ac.tuwien.kr.alpha.api.programs.literals.Literal;
import at.ac.tuwien.kr.alpha.api.programs.rules.heads.ChoiceHead;
import at.ac.tuwien.kr.alpha.api.programs.terms.FunctionTerm;
import at.ac.tuwien.kr.alpha.api.programs.terms.IntervalTerm;
import at.ac.tuwien.kr.alpha.api.programs.terms.Term;
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.comparisons.ComparisonOperators;
import at.ac.tuwien.kr.alpha.commons.programs.atoms.Atoms;
import at.ac.tuwien.kr.alpha.commons.programs.terms.Terms;
import at.ac.tuwien.kr.alpha.commons.util.Util;

/**
 * Copyright (c) 2016, the Alpha Team.
 */
public class ParserTest {

	private static final String UNIT_TEST_EXPECT_UNSAT =
			"p(1). p(2). "
			+ ":- p(X), p(Y), X + Y = 3."
			+ "#test expected_unsat(expect: unsat) {"
			+ "given {}"
			+ "}";

	private static final String UNIT_TEST_BASIC_TEST =
			"a :- b. #test ensure_a(expect: 1) { given { b. } assertForAll { :- not a. } }";
	private static final String UNIT_TEST_MORE_ASSERTIONS =
			"a :- b. #test ensure_a(expect: 1) { given { b. } assertForAll { :- not a. } assertForSome { :- not a.} }";

	private static final String UNIT_TEST_MORE_TCS =
			"a :- b. #test ensure_a(expect: 1) { given { b. } assertForAll { :- not a. }} " +
					"#test ensure_not_c (expect: 1) { given { b.} assertForAll { :- c. }}";

	private static final String UNIT_TEST_KEYWORDS_AS_IDS =
			"assert(a) :- given(b). # test test(expect: 1) { given { given(b). } assertForAll { :- not assert(a). :- assertForSome(b).}}";

	private final ProgramParserImpl parser = new ProgramParserImpl();

	@Test
	public void parseFact() {
		ASPCore2Program parsedProgram = parser.parse("p(a,b).");

		assertEquals(1, parsedProgram.getFacts().size(), "Program contains one fact.");
		assertEquals("p", parsedProgram.getFacts().get(0).getPredicate().getName(), "Predicate name of fact is p.");
		assertEquals(2, parsedProgram.getFacts().get(0).getPredicate().getArity(), "Fact has two terms.");
		assertEquals("a", (parsedProgram.getFacts().get(0).getTerms().get(0)).toString(), "First term is a.");
		assertEquals("b", (parsedProgram.getFacts().get(0).getTerms().get(1)).toString(), "Second term is b.");
	}

	@Test
	public void parseFactWithFunctionTerms() {
		ASPCore2Program parsedProgram = parser.parse("p(f(a),g(h(Y))).");

		assertEquals(1, parsedProgram.getFacts().size(), "Program contains one fact.");
		assertEquals("p", parsedProgram.getFacts().get(0).getPredicate().getName(), "Predicate name of fact is p.");
		assertEquals(2, parsedProgram.getFacts().get(0).getPredicate().getArity(), "Fact has two terms.");
		assertEquals("f", ((FunctionTerm) parsedProgram.getFacts().get(0).getTerms().get(0)).getSymbol(), "First term is function term f.");
		assertEquals("g", ((FunctionTerm) parsedProgram.getFacts().get(0).getTerms().get(1)).getSymbol(), "Second term is function term g.");
	}

	@Test
	public void parseSmallProgram() {
		ASPCore2Program parsedProgram = parser.parse(
				"a :- b, not d." + System.lineSeparator() +
						"c(X) :- p(X,a,_), q(Xaa,xaa)." + System.lineSeparator() +
						":- f(Y).");

		assertEquals(3, parsedProgram.getRules().size(), "Program contains three rules.");
	}

	@Test
	public void parseBadSyntax() {
		assertThrows(IllegalArgumentException.class, () -> {
			parser.parse("Wrong Syntax.");
		});
	}

	@Test
	public void parseBuiltinAtom() {
		ASPCore2Program parsedProgram = parser.parse("a :- p(X), X != Y, q(Y).");
		assertEquals(1, parsedProgram.getRules().size());
		assertEquals(3, parsedProgram.getRules().get(0).getBody().size());
	}

	@Test
	// Change expected after Alpha can deal with disjunction.
	public void parseProgramWithDisjunctionInHead() {
		assertThrows(UnsupportedOperationException.class, () -> {
			parser.parse("r(X) | q(X) :- q(X)." + System.lineSeparator() + "q(a)." + System.lineSeparator());
		});
	}

	@Test
	public void parseInterval() {
		ASPCore2Program parsedProgram = parser.parse("fact(2..5). p(X) :- q(a, 3 .. X).");
		IntervalTerm factInterval = (IntervalTerm) parsedProgram.getFacts().get(0).getTerms().get(0);
		assertTrue(factInterval.equals(Terms.newIntervalTerm(Terms.newConstant(2), Terms.newConstant(5))));
		IntervalTerm bodyInterval = (IntervalTerm) parsedProgram.getRules().get(0).getBody().stream().findFirst().get().getTerms().get(1);
		assertTrue(bodyInterval.equals(Terms.newIntervalTerm(Terms.newConstant(3), Terms.newVariable("X"))));
	}

	@Test
	public void parseChoiceRule() {
		ASPCore2Program parsedProgram = parser.parse("dom(1). dom(2). { a ; b } :- dom(X).");
		ChoiceHead choiceHead = (ChoiceHead) parsedProgram.getRules().get(0).getHead();
		assertEquals(2, choiceHead.getChoiceElements().size());
		assertTrue(choiceHead.getChoiceElements().get(0).getChoiceAtom().toString().equals("a"));
		assertTrue(choiceHead.getChoiceElements().get(1).getChoiceAtom().toString().equals("b"));
		assertEquals(null, choiceHead.getLowerBound());
		assertEquals(null, choiceHead.getUpperBound());
	}

	@Test
	public void parseChoiceRuleBounded() {
		ASPCore2Program parsedProgram = parser.parse("dom(1). dom(2). 1 < { a: p(v,w), not r; b } <= 13 :- dom(X). foo.");
		ChoiceHead choiceHead = (ChoiceHead) parsedProgram.getRules().get(0).getHead();
		assertEquals(2, choiceHead.getChoiceElements().size());
		assertTrue(choiceHead.getChoiceElements().get(0).getChoiceAtom().toString().equals("a"));
		assertTrue(choiceHead.getChoiceElements().get(1).getChoiceAtom().toString().equals("b"));
		List<Literal> conditionalLiterals = choiceHead.getChoiceElements().get(0).getConditionLiterals();
		assertEquals(2, conditionalLiterals.size());
		assertFalse(conditionalLiterals.get(0).isNegated());
		assertTrue(conditionalLiterals.get(1).isNegated());
		assertEquals(Terms.newConstant(1), choiceHead.getLowerBound());
		assertEquals(ComparisonOperators.LT, choiceHead.getLowerOperator());
		assertEquals(Terms.newConstant(13), choiceHead.getUpperBound());
		assertEquals(ComparisonOperators.LE, choiceHead.getUpperOperator());
	}

	@Test
	public void literate() throws IOException {
		final ReadableByteChannel input = Util.streamToChannel(Util.literate(Stream.of(
				"This is some description.",
				"",
				"    p(a).",
				"",
				"Test!")));

		final String actual = new ProgramParserImpl().parse(CharStreams.fromChannel(input)).toString();
		final String expected = "p(a)." + System.lineSeparator();

		assertEquals(expected, actual);
	}

	@Test
	public void testMalformedInputNotIgnored() {
		String program = "foo(a) :- p(b).\n" +
				"// rule :- q.\n" +
				"r(1).\n" +
				"r(2).\n";
		assertThrows(IllegalArgumentException.class, () -> {
			parser.parse(program);
		});
	}

	@Test
	public void testMissingDotNotIgnored() {
		assertThrows(IllegalArgumentException.class, () -> {
			parser.parse("p(X,Y) :- q(X), r(Y) p(a). q(b).");
		});
	}

	@Test
	public void parseEnumerationDirective() {
		ASPCore2Program parsedProgram = parser.parse("p(a,1)." +
				"# enumeration_predicate_is mune." +
				"r(X) :- p(X), mune(X)." +
				"p(b,2).");
		String directive = parsedProgram.getInlineDirectives().getDirectiveValue(InlineDirectives.DIRECTIVE.enum_predicate_is);
		assertEquals("mune", directive);
	}

	@Test
	public void cardinalityAggregate() {
		ASPCore2Program parsedProgram = parser.parse("num(K) :-  K <= #count {X,Y,Z : p(X,Y,Z) }, dom(K).");
		Optional<Literal> optionalBodyElement = parsedProgram.getRules().get(0).getBody().stream().filter((lit) -> lit instanceof AggregateLiteral).findFirst();
		assertTrue(optionalBodyElement.isPresent());
		Literal bodyElement = optionalBodyElement.get();
		AggregateLiteral parsedAggregate = (AggregateLiteral) bodyElement;
		VariableTerm x = Terms.newVariable("X");
		VariableTerm y = Terms.newVariable("Y");
		VariableTerm z = Terms.newVariable("Z");
		List<Term> basicTerms = Arrays.asList(x, y, z);
		AggregateAtom.AggregateElement aggregateElement = Atoms.newAggregateElement(basicTerms,
				Collections.singletonList(Atoms.newBasicAtom(Predicates.getPredicate("p", 3), x, y, z).toLiteral()));
		AggregateAtom expectedAggregate = Atoms.newAggregateAtom(ComparisonOperators.LE, Terms.newVariable("K"), null, null,
				AggregateAtom.AggregateFunctionSymbol.COUNT, Collections.singletonList(aggregateElement));
		assertEquals(expectedAggregate, parsedAggregate.getAtom());
	}

	@Test
	public void stringWithEscapedQuotes() throws IOException {
		CharStream stream = CharStreams.fromStream(ParserTest.class.getResourceAsStream("/escaped_quotes.asp"));
		ASPCore2Program prog = parser.parse(stream);
		assertEquals(1, prog.getFacts().size());
		Atom stringAtom = prog.getFacts().get(0);
		String stringWithQuotes = stringAtom.getTerms().get(0).toString();
		assertEquals("\"a string with \"quotes\"\"", stringWithQuotes);
	}

	@Test
	public void unitTestExpectUnsat() {
		ASPCore2Program prog = parser.parse(UNIT_TEST_EXPECT_UNSAT);
		assertEquals(1, prog.getTestCases().size());
		TestCase tc = prog.getTestCases().get(0);
		assertEquals("expected_unsat", tc.getName());
		assertTrue(tc.getInput().isEmpty());
		assertTrue(tc.getAssertions().isEmpty());
	}

	@Test
	public void unitTestBasicTest() {
		ASPCore2Program prog = parser.parse(UNIT_TEST_BASIC_TEST);
		assertEquals(1, prog.getTestCases().size());
		TestCase tc = prog.getTestCases().get(0);
		assertEquals("ensure_a", tc.getName());
		assertEquals(1, tc.getInput().size());
		assertEquals(1, tc.getAssertions().size());
		assertEquals(Assertion.Mode.FOR_ALL, tc.getAssertions().get(0).getMode());
	}

	@Test
	public void unitTestMultipleAsserts() {
		ASPCore2Program prog = parser.parse(UNIT_TEST_MORE_ASSERTIONS);
		assertEquals(1, prog.getTestCases().size());
		TestCase tc = prog.getTestCases().get(0);
		assertEquals("ensure_a", tc.getName());
		assertEquals(1, tc.getInput().size());
		assertEquals(2, tc.getAssertions().size());
		assertEquals(Assertion.Mode.FOR_ALL, tc.getAssertions().get(0).getMode());
		assertEquals(Assertion.Mode.FOR_SOME, tc.getAssertions().get(1).getMode());
	}

	@Test
	public void unitTestMoreTCs() {
		ASPCore2Program prog = parser.parse(UNIT_TEST_MORE_TCS);
		assertEquals(2, prog.getTestCases().size());
		TestCase tc1 = prog.getTestCases().get(0);
		assertEquals("ensure_a", tc1.getName());
		TestCase tc2 = prog.getTestCases().get(1);
		assertEquals("ensure_not_c", tc2.getName());
	}

	@Test
	public void unitTestKeywordsAsIds() {
		ASPCore2Program prog = parser.parse(UNIT_TEST_KEYWORDS_AS_IDS);
		assertEquals(1, prog.getTestCases().size());
		TestCase tc = prog.getTestCases().get(0);
		assertEquals("test", tc.getName());
		assertEquals(1, tc.getInput().size());
		assertEquals(1, tc.getAssertions().size());
		assertEquals(Assertion.Mode.FOR_ALL, tc.getAssertions().get(0).getMode());
	}

}
