/******************************************************************************
 *
 *	Copyright (c) 2017-2022, INTO-CPS Association,
 *	c/o Professor Peter Gorm Larsen, Department of Engineering
 *	Finlandsgade 22, 8200 Aarhus N.
 *
 *	This file is part of the INTO-CPS toolchain.
 *
 *	MaestroCheck 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 3 of the License, or
 *	(at your option) any later version.
 *
 *	MaestroCheck 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.
 *
 *	You should have received a copy of the GNU General Public License
 *	along with MaestroCheck. If not, see <http://www.gnu.org/licenses/>.
 *	SPDX-License-Identifier: GPL-3.0-or-later
 *
 ******************************************************************************/

package maestro;

import java.io.BufferedOutputStream;
import java.io.File;
import java.io.FileInputStream;
import java.io.FileOutputStream;
import java.io.IOException;
import java.io.InputStream;
import java.nio.file.Files;
import java.nio.file.attribute.FileAttribute;
import java.util.List;
import java.util.Map;
import java.util.Vector;

import javax.xml.XMLConstants;
import javax.xml.transform.Source;
import javax.xml.transform.stream.StreamSource;
import javax.xml.validation.Schema;
import javax.xml.validation.SchemaFactory;
import javax.xml.validation.Validator;

import org.xml.sax.SAXException;

import com.fujitsu.vdmj.Settings;
import com.fujitsu.vdmj.ast.modules.ASTModuleList;
import com.fujitsu.vdmj.config.Properties;
import com.fujitsu.vdmj.in.INNode;
import com.fujitsu.vdmj.in.modules.INModuleList;
import com.fujitsu.vdmj.lex.Dialect;
import com.fujitsu.vdmj.lex.LexTokenReader;
import com.fujitsu.vdmj.mapper.ClassMapper;
import com.fujitsu.vdmj.messages.VDMError;
import com.fujitsu.vdmj.runtime.Interpreter;
import com.fujitsu.vdmj.runtime.ModuleInterpreter;
import com.fujitsu.vdmj.syntax.ModuleReader;
import com.fujitsu.vdmj.tc.TCNode;
import com.fujitsu.vdmj.tc.modules.TCModuleList;
import com.fujitsu.vdmj.typechecker.ModuleTypeChecker;
import com.fujitsu.vdmj.typechecker.TypeChecker;
import com.fujitsu.vdmj.values.Value;

import annotations.in.INOnFailAnnotation;
import types.Type;
import xsd2vdm.Xsd2VDM;

public class MaestroCheck
{
	/**
	 * Main class for testing. Maestro will use the default constructor.
	 */
	public static void main(String[] args) throws Exception
	{
		MaestroCheck checker = new MaestroCheck();
		
		for (OnFailError err: checker.check(new File(args[0])))
		{
			System.out.println(err.errno + " => " + err.message);
		}
	}
	
	public List<OnFailError> check(InputStream modelDescriptionStream) throws Exception
	{
		File xmlfile = Files.createTempFile("fmi", ".xml", new FileAttribute[0]).toFile();
		xmlfile.deleteOnExit();
		copyStream(modelDescriptionStream, xmlfile.getParentFile(), xmlfile.getName());
		return check(xmlfile);
	}

	public List<OnFailError> check(File modelDescriptionFile) throws Exception
	{
		List<OnFailError> errors = new Vector<>();

		File fmi2 = Files.createTempDirectory("fmi2", new FileAttribute[0]).toFile();
		fmi2.deleteOnExit();
		
		File schema = new File(fmi2, "schema");
		schema.mkdir();
		schema.deleteOnExit();
		
		copyResources(fmi2,
			"/schema/fmi2Annotation.xsd",
			"/schema/fmi2AttributeGroups.xsd",
			"/schema/fmi2ModelDescription.xsd",
			"/schema/fmi2ScalarVariable.xsd",
			"/schema/fmi2Type.xsd",
			"/schema/fmi2Unit.xsd",
			"/schema/fmi2VariableDependency.xsd",
			"/schema/xsd2vdm.properties");
		
		File xsdFile = new File(schema, "fmi2ModelDescription.xsd");
		OnFailError validation = validate(modelDescriptionFile, xsdFile);
		
		if (validation != null)
		{
			errors.add(validation);
		}
		else
		{
			File vdmsl = new File(fmi2, "vdmsl");
			vdmsl.mkdir();
			vdmsl.deleteOnExit();
			
			File vdmFile = new File(vdmsl, "model.vdmsl");
			vdmFile.deleteOnExit();

			Xsd2VDM converter = new Xsd2VDM();
			Xsd2VDM.loadProperties(xsdFile);
			Map<String, Type> vdmSchema = converter.createVDMSchema(xsdFile, modelDescriptionFile, false, true);
			converter.createVDMValue(vdmSchema, vdmFile, modelDescriptionFile, "model");
			
			if (vdmFile.exists())	// Means successful?
			{
				copyResources(vdmsl,
					"/CoSimulation_4.3.1.vdmsl",
					"/DefaultExperiment_2.2.5.vdmsl",
					"/FMI2Schema.vdmsl",
					"/FMIModelDescription_2.2.1.vdmsl",
					"/LogCategories_2.2.4.vdmsl",
					"/Misc.vdmsl",
					"/ModelExchange_3.3.1.vdmsl",
					"/ModelStructure_2.2.8.vdmsl",
					"/ModelVariables_2.2.7.vdmsl",
					"/TypeDefinitions_2.2.3.vdmsl",
					"/UnitDefinitions_2.2.2.vdmsl",
					"/VariableNaming_2.2.9.vdmsl",
					"/VendorAnnotations_2.2.6.vdmsl");
				
				Properties.init();
				Settings.annotations = true;
				ASTModuleList ast = new ASTModuleList();
				
				for (File sl: vdmsl.listFiles())
				{
					LexTokenReader ltr = new LexTokenReader(sl, Dialect.VDM_SL);
					ModuleReader mreader = new ModuleReader(ltr);
					ast.addAll(mreader.readModules());
					
					for (VDMError err: mreader.getErrors())
					{
						errors.add(new OnFailError(err.number, err.message));
					}
				}
				
				if (!errors.isEmpty())
				{
					errors.add(new OnFailError(1, "Syntax errors in VDMSL?"));
				}
				else
				{
					TCModuleList tc = ClassMapper.getInstance(TCNode.MAPPINGS).init().convert(ast);
					tc.combineDefaults();
					TypeChecker tchecker = new ModuleTypeChecker(tc);
					tchecker.typeCheck();
					
					if (TypeChecker.getErrorCount() > 0)
					{
						for (VDMError err: TypeChecker.getErrors())
						{
							errors.add(new OnFailError(err.number, err.message));
						}

						errors.add(new OnFailError(2, "Type errors in VDMSL?"));
					}
					
					INModuleList in = ClassMapper.getInstance(INNode.MAPPINGS).init().convert(tc);
					Interpreter interpreter = new ModuleInterpreter(in, tc);
					interpreter.init();
					INOnFailAnnotation.setErrorList(errors);
					Value result = interpreter.execute("isValidFMIModelDescription(model)");
					
					if (!result.boolValue(null))
					{
						errors.add(new OnFailError(3, "Errors found"));
					}
				}
			}
		}
		
		return errors;
	}
	
	private OnFailError validate(File xml, File xsd)
	{
		try
		{
			// Note that we pass a stream to allow the validator to determine the
			// encoding, rather than passing a File, which seems to use default encoding.
			Source xmlFile = new StreamSource(new FileInputStream(xml));
			xmlFile.setSystemId(xml.toURI().toASCIIString());
			Source xsdFile = new StreamSource(xsd);
			xsdFile.setSystemId(xsd.toURI().toASCIIString());
			SchemaFactory schemaFactory = SchemaFactory.newInstance(XMLConstants.W3C_XML_SCHEMA_NS_URI);
			
			Schema schema = schemaFactory.newSchema(xsdFile);
			Validator validator = schema.newValidator();
			validator.validate(xmlFile);
			
			return null;
		}
		catch (SAXException e)
		{
			return new OnFailError(0, "XML validation: " + e);		// Raw exception gives file/line/col
		}
		catch (Exception e)
		{
			return new OnFailError(0, "XML validation: " + e.getMessage());
		}
	}

	private void copyResources(File target, String... resources) throws Exception
	{
		if (!target.exists())
		{
			throw new Exception("Target of copyResources does not exist: " + target);
		}
		
		for (String resource: resources)
		{
			InputStream is = MaestroCheck.class.getResourceAsStream(resource);
			
			if (is == null)
			{
				throw new Exception("Cannot load resource " + resource);
			}
			
			copyStream(is, target, resource);
			is.close();
		}
	}

	private void copyStream(InputStream data, File target, String file) throws IOException
	{
		File targetFile = new File(target, file);
		BufferedOutputStream bos = new BufferedOutputStream(new FileOutputStream(targetFile));
		
		while (data.available() > 0)
		{
			bos.write(data.read());
		}
		
		bos.close();
		targetFile.deleteOnExit();		// Note! All files temporary
	}
}
