package org.ai4fm.proofprocess.zeves.ui.parse;

import java.io.IOException;
import java.util.ArrayList;
import java.util.Collections;
import java.util.List;

import net.sourceforge.czt.eclipse.editors.zeditor.ZEditorUtil;
import net.sourceforge.czt.eclipse.zeves.core.ZEvesResultConverter;
import net.sourceforge.czt.session.CommandException;
import net.sourceforge.czt.session.SectionInfo;
import net.sourceforge.czt.session.SectionManager;
import net.sourceforge.czt.z.ast.Pred;
import net.sourceforge.czt.zeves.response.ZEvesOutput;

import org.ai4fm.proofprocess.Term;
import org.ai4fm.proofprocess.zeves.UnparsedTerm;
import org.ai4fm.proofprocess.zeves.ZEvesProofProcessFactory;
import org.ai4fm.proofprocess.zeves.ui.ZEvesProofUIPlugin;

/**
 * @author Andrius Velykis
 */
public class TermParser {

	private static final ZEvesProofProcessFactory FACTORY = ZEvesProofProcessFactory.eINSTANCE;
	
	public static List<Term> parseGoals(SectionInfo sectInfo, String sectName, ZEvesOutput result) {
		
		Object goalObj = result.getFirstResult();
		String goalStr = goalObj.toString().trim();
		
		if (ZEvesOutput.UNPRINTABLE_PREDICATE.equals(goalStr)) {
			// a special case - do not try parsing
			
			UnparsedTerm term = FACTORY.createUnparsedTerm();
			term.setDisplay(goalStr);
			return Collections.<Term>singletonList(term);
		}
		
		try {
			
			if (sectInfo instanceof SectionManager) {
				// a bit of a hack, will need to review whether a sectInfo could be enough eventually
				
				List<Term> goals = new ArrayList<Term>();
				Pred goalPred = ZEvesResultConverter.parseZEvesPred((SectionManager) sectInfo, sectName, goalStr);
				
				// TODO convert the parsed predicate
				UnparsedTerm term = FACTORY.createUnparsedTerm();
				term.setDisplay(goalStr);
				goals.add(term);
				
				return goals;
			}
			
		} catch (IOException e) {
			ZEvesProofUIPlugin.log(e);
		} catch (CommandException e) {
			Throwable cause = e.getCause();
			if (cause == null) {
				cause = e;
			}
			
			String msg = "Cannot parse Z/Eves result: " + ZEditorUtil.clean(cause.getMessage()).trim();
			ZEvesProofUIPlugin.log(msg, e);
		}
		
		// problems parsing - just output unparsed
		UnparsedTerm term = FACTORY.createUnparsedTerm();
		term.setDisplay(goalStr);
		return Collections.<Term>singletonList(term);
	}
	
}

@@ -314,80 +314,283 @@
 czt.
-session.CommandException;%0Aimport net.sourceforge.czt.session.SectionInfo
+parser.util.DeleteAnnVisitor;%0Aimport net.sourceforge.czt.print.util.XmlString;%0Aimport net.sourceforge.czt.session.CommandException;%0Aimport net.sourceforge.czt.session.Key;%0Aimport net.sourceforge.czt.session.SectionInfo;%0Aimport net.sourceforge.czt.session.SectionInfoException
 ;%0Aim
@@ -1003,16 +1003,107 @@
 rser %7B%0A%0A
+%09private static final String ZML_PRINT_KEY = ZEvesProofUIPlugin.PLUGIN_ID + %22.term-zml%22;%0A%09%0A
 %09private
@@ -1820,24 +1820,69 @@
 st%3CTerm%3E();%0A
+%09%09%09%09long start = System.currentTimeMillis();%0A
 %09%09%09%09Pred goa
@@ -1968,24 +1968,307 @@
 , goalStr);%0A
+%09%09%09%09System.out.println(%22Parsing term: %22 + (System.currentTimeMillis() - start));%0A%09%09%09%09%0A%09%09%09%09start = System.currentTimeMillis();%0A%09%09%09%09String zmlPred = printZml((SectionManager) sectInfo, goalPred);%0A%09%09%09%09System.out.println(%22Printing term to ZML: %22 + (System.currentTimeMillis() - start));%0A
 %09%09%09%09%0A%09%09%09%09// 
@@ -2371,31 +2371,31 @@
 .setDisplay(
-goalStr
+zmlPred
 );%0A%09%09%09%09goals
@@ -2927,10 +2927,615 @@
 );%0A%09%7D%0A%09%0A
+%09private static String printZml(SectionManager sectInfo, net.sourceforge.czt.base.ast.Term cztTerm)%0A%09%09%09throws CommandException %7B%0A%09%09%0A%09%09// strip all annotations (e.g. LocAnn, etc) during serialization%0A%09%09cztTerm.accept(new DeleteAnnVisitor());%0A%09%09%0A%09%09SectionManager cloned = sectInfo.clone();%0A%09%09%0A%09%09Key%3Cnet.sourceforge.czt.base.ast.Term%3E termKey = new Key%3Cnet.sourceforge.czt.base.ast.Term%3E(%0A%09%09%09%09ZML_PRINT_KEY, net.sourceforge.czt.base.ast.Term.class);%0A%09%09%0A%09%09cloned.put(termKey, cztTerm);%0A%09%09XmlString printed = cloned.get(new Key%3CXmlString%3E(ZML_PRINT_KEY, XmlString.class));%0A%09%09%0A%09%09return printed.toString();%0A%09%7D%0A%09%0A
 %7D%0A

Test implementation of printing terms to ZML.