package edu.kit.iti.formal.pse.worthwhile.common.tests;

import java.io.ByteArrayInputStream;
import java.io.IOException;
import java.io.InputStream;
import java.util.List;

import org.eclipse.emf.common.util.URI;
import org.eclipse.emf.ecore.resource.Resource;
import org.eclipse.xtext.resource.XtextResource;
import org.eclipse.xtext.resource.XtextResourceSet;

import com.google.inject.Injector;

import edu.kit.iti.formal.pse.worthwhile.WorthwhileStandaloneSetup;
import edu.kit.iti.formal.pse.worthwhile.model.ast.ASTNode;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Block;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Expression;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Program;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Statement;
import edu.kit.iti.formal.pse.worthwhile.model.ast.VariableDeclaration;

public class TestASTProvider {

	public static Program getRootASTNode(String parseText) {
		// from http://wiki.pse.ndreke.de/proof_of_concept_ast_output
		// see also http://wiki.eclipse.org/Xtext/FAQ#How_do_I_load_my_model_in_a_standalone_Java_application.C2.A0.3F
		Injector guiceInjector = new WorthwhileStandaloneSetup().createInjectorAndDoEMFRegistration();
		XtextResourceSet resourceSet = guiceInjector.getInstance(XtextResourceSet.class);
		resourceSet.addLoadOption(XtextResource.OPTION_RESOLVE_ALL, Boolean.TRUE);
		Resource resource = resourceSet.createResource(URI.createURI("dummy:/example.ww"));
		InputStream in = new ByteArrayInputStream(parseText.getBytes());
		try {
			resource.load(in, resourceSet.getLoadOptions());
		} catch (IOException e) {
			// TODO
		}

		// System.out.println("Getting syntax errors ...");
		// Iterable<Diagnostic> errors = resource.getErrors();
		Program root = null;

		if (resource.getErrors().isEmpty()) {
			root = (Program) resource.getContents().get(0);
		}

		return root;
	}

	/**
	 * @return A simple, human-readable formula that evaluates to true (i.e. is always satisfiable) and covers a lot of
	 *         the constructs supported by the language
	 */
	public static Expression getTestFormula() {
		return parseFormulaString("((!false || ((9 % 4) = 1)) && true && ((3 + 3) = 6)");
	}

	public static Expression getNegatedTestFormula() {
		return parseFormulaString("!((!false || ((9 % 4) = 1)) && true && ((3 + 3) = 6)");
	}

	public static Expression parseFormulaString(String formulaString) {
		ASTNode n = TestASTProvider.getRootASTNode("{\nBoolean x := " + formulaString + "\n" + "}\n");

		if (n == null) {
			return null;
		}

		List<Statement> statements = ((Block) ((Program) n).getMainBlock().getStatements().get(0)).getStatements();

		return ((VariableDeclaration) (statements.get(0))).getInitialValue();
	}
}

@@ -247,32 +247,91 @@
 ource.Resource;%0A
+import org.eclipse.emf.ecore.resource.Resource.Diagnostic;%0A
 import org.eclip
@@ -1063,16 +1063,21 @@
 see also
+%0A%09%09//
  http://
@@ -1741,65 +1741,8 @@
 %22);%0A
-%09%09// Iterable%3CDiagnostic%3E errors = resource.getErrors();%0A
 %09%09Pr
@@ -1852,21 +1852,333 @@
 get(0);%0A
+%09%09%7D else %7B%0A%09%09%09StringBuilder errorStringBuilder = new StringBuilder();%0A%0A%09%09%09for (Diagnostic diag : resource.getErrors()) %7B%0A%09%09%09%09errorStringBuilder.append(%22%5Cn Line %22 + diag.getLine() + %22: %22 + diag.getMessage());%0A%09%09%09%7D%0A%0A%09%09%09throw new IllegalArgumentException(%22Program contains errors:%22 + errorStringBuilder.toString());%0A
 %09%09%7D%0A
-%0A
 %09%09return
@@ -2310,11 +2310,8 @@
  lot
- of
 %0A%09 *
@@ -2319,16 +2319,19 @@
         
+of 
 the cons
@@ -2773,16 +2773,17 @@
 an x := 
+(
 %22 + form
@@ -2795,16 +2795,17 @@
 ring + %22
+)
 %5Cn%22 + %22%7D
@@ -2943,16 +2943,35 @@
 .get(0))
+%0A%09%09                
 .getStat

Throw exception if program string contains parser errors