/* $Id: GenerateLatexTest.java,v 1.14 2007/02/25 20:04:33 m31 Exp $
 *
 * This file is part of the project "Hilbert II" - http://www.qedeq.org
 *
 * Copyright 2000-2007,  Michael Meyling <mime@qedeq.org>.
 *
 * "Hilbert II" is free software; you can redistribute
 * it and/or modify it under the terms of the GNU General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 * GNU General Public License for more details.
 */

package org.qedeq.kernel.bo.logic;

import java.io.File;
import java.io.IOException;

import javax.xml.parsers.ParserConfigurationException;

import org.qedeq.kernel.base.module.Qedeq;
import org.qedeq.kernel.bo.control.QedeqBoFactory;
import org.qedeq.kernel.bo.control.QedeqBoFormalLogicChecker;
import org.qedeq.kernel.bo.module.ModuleDataException;
import org.qedeq.kernel.bo.module.QedeqBo;
import org.qedeq.kernel.test.QedeqTestCase;
import org.qedeq.kernel.xml.handler.module.QedeqHandler;
import org.qedeq.kernel.xml.parser.SaxDefaultHandler;
import org.qedeq.kernel.xml.parser.SaxParser;
import org.qedeq.kernel.xml.parser.SyntaxException;
import org.xml.sax.SAXException;

/**
 * Test generating LaTeX files for all known samples.
 * 
 * @version $Revision: 1.14 $
 * @author Michael Meyling
 */
public final class CheckLogicTest extends QedeqTestCase {

    public void testNegative00() throws Exception {
        try {
            generate(new File("."), "data/qedeq_error_sample_00.xml");
            fail("SAXException expected");
        } catch (SAXException e) {
            System.out.println(e.getException().getClass().getName());
            assertTrue(e.getException() instanceof SyntaxException);
            final SyntaxException check = (SyntaxException) e.getException();
            assertEquals(9001, check.getErrorCode());
            assertEquals(36, check.getErrorPosition().getLine());
            assertEquals(20, check.getErrorPosition().getColumn());
        }
    }
    
    public void testNegative01() throws Exception {
        try {
            generate(new File("."), "data/qedeq_error_sample_01.xml");
            fail("SAXException expected");
        } catch (SAXException e) {
            System.out.println(e.getException().getClass().getName());
            assertTrue(e.getException() instanceof SyntaxException);
            final SyntaxException check = (SyntaxException) e.getException();
            assertEquals(9001, check.getErrorCode());
            assertEquals(39, check.getErrorPosition().getLine());
            assertEquals(35, check.getErrorPosition().getColumn());
        }
    }
    
    public void testNegative02() throws Exception {
        try {
            generate(new File("."), "data/qedeq_error_sample_02.xml");
            fail("ModuleDataException expected");
        } catch (ModuleDataException e) {
            System.out.println(e.getClass().getName());
            assertTrue(e instanceof LogicalCheckException);
            final LogicalCheckException check = (LogicalCheckException) e;
            assertEquals(30550, check.getErrorCode());
            assertEquals("getChapterList().get(0).getSectionList().get(0).getSubsectionList().get(0).getNodeType().getAxiom().getFormula().getElement().getList().getElement(1).getList()", check.getContext().getLocationWithinModule());
            assertNull(check.getReferenceContext());
        }
    }
    
    public void testNegative03() throws Exception {
        try {
            generate(new File("."), "data/qedeq_error_sample_03.xml");
            fail("ModuleDataException expected");
        } catch (ModuleDataException e) {
            System.out.println(e.getClass().getName());
            assertTrue(e instanceof LogicalCheckException);
            final LogicalCheckException check = (LogicalCheckException) e;
            assertEquals(30770, check.getErrorCode());
            assertEquals("getChapterList().get(0).getSectionList().get(0).getSubsectionList().get(0).getNodeType().getAxiom().getFormula().getElement().getList().getElement(1)", check.getContext().getLocationWithinModule());
            assertNull(check.getReferenceContext());
        }
    }
    
    public void testNegative04() throws Exception {
        try {
            generate(new File("."), "data/qedeq_error_sample_04.xml");
            fail("ModuleDataException expected");
        } catch (ModuleDataException e) {
            System.out.println(e.getClass().getName());
            assertTrue(e instanceof LogicalCheckException);
            final LogicalCheckException check = (LogicalCheckException) e;
            assertEquals(30780, check.getErrorCode());
            assertEquals("getChapterList().get(0).getSectionList().get(0).getSubsectionList().get(0).getNodeType().getAxiom().getFormula().getElement().getList().getElement(1)", check.getContext().getLocationWithinModule());
            assertNull(check.getReferenceContext());
        }
    }

    /**
     * Call the generation of one LaTeX file and copy XML source to same destination directory.
     *
     * @param   dir         Start directory.
     * @param   xml         Relative path to XML file. Must not be <code>null</code>.
     */
    private static void generate(final File dir, final String xml) throws IOException, 
            ParserConfigurationException, SAXException, ModuleDataException {
        final File xmlFile = new File(dir, xml).getAbsoluteFile();
        
        final String context = xmlFile.getAbsolutePath();
        SaxDefaultHandler handler = new SaxDefaultHandler();
        QedeqHandler simple = new QedeqHandler(handler);
        handler.setBasisDocumentHandler(simple);
        SaxParser parser = new SaxParser(handler);
        parser.parse(xmlFile);
        Qedeq qedeq = simple.getQedeq();
        final QedeqBo qedeqBo = QedeqBoFactory.createQedeq(context, qedeq);
        QedeqBoFormalLogicChecker.check(context, qedeqBo);
    }

}