package de.prob2.ui.verifications.ltl.patterns;

import de.prob.ltl.parser.pattern.Pattern;
import de.prob.ltl.parser.pattern.PatternManager;
import de.prob.ltl.parser.LtlParser.NumVarParamContext;
import de.prob.ltl.parser.LtlParser.Pattern_defContext;
import de.prob.ltl.parser.LtlParser.Pattern_def_paramContext;
import de.prob.ltl.parser.LtlParser.SeqVarParamContext;
import de.prob.ltl.parser.LtlParser.VarParamContext;
import de.prob2.ui.project.machines.Machine;
import de.prob2.ui.verifications.ltl.ILTLItemHandler;
import de.prob2.ui.verifications.ltl.LTLParseListener;
import de.prob2.ui.verifications.ltl.LTLResultHandler;

import org.antlr.v4.runtime.tree.ParseTree;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

import com.google.inject.Singleton;

import javax.inject.Inject;

import java.util.ArrayList;
import java.util.List;
import java.util.stream.Collectors;

@Singleton
public class LTLPatternParser implements ILTLItemHandler {
	
	private static final Logger logger = LoggerFactory.getLogger(LTLPatternParser.class);
	
	private final LTLResultHandler resultHandler;
		
	@Inject
	private LTLPatternParser(final LTLResultHandler resultHandler) {
		this.resultHandler = resultHandler;
	}
		
	public void parsePattern(LTLPatternItem item, Machine machine) {
		logger.trace("Parse ltl pattern");
		Pattern pattern = itemToPattern(item);
		resultHandler.handlePatternResult(checkDefinition(pattern, machine), item);
		item.setName(pattern.getName());
	}
	
	public void addPattern(LTLPatternItem item, Machine machine) {
		Pattern pattern = itemToPattern(item);
		resultHandler.handlePatternResult(checkDefinition(pattern, machine), item);
		item.setName(pattern.getName());
		machine.getPatternManager().getPatterns().add(pattern);
	}
	
	private LTLParseListener checkDefinition(Pattern pattern, Machine machine) {
		LTLParseListener parseListener = initializeParseListener(pattern);
		pattern.updateDefinitions(machine.getPatternManager());
		ParseTree ast = pattern.getAst();
		List<String> patternNames = new ArrayList<>();
		for(int i = 0; i < ast.getChildCount(); i++) {
			ParseTree child = ast.getChild(i);
			StringBuilder signature = new StringBuilder();
			if(child instanceof Pattern_defContext && ((Pattern_defContext) child).ID() != null) {
				String name = ((Pattern_defContext) child).ID().getText();
				signature.append(name);
				signature.append("(");
				signature.append(String.join(", ", ((Pattern_defContext) child).pattern_def_param().stream()
					.map(this::extractParameterFromContext)
					.collect(Collectors.toList())));
				signature.append(")");
				patternNames.add(signature.toString());
			}
		}
		pattern.setName(String.join("\n", patternNames));
		return parseListener;
	}
	
	private String extractParameterFromContext(Pattern_def_paramContext ctx) {
		if(ctx instanceof VarParamContext) {
			return ((VarParamContext) ctx).ID().getText();
		} else if(ctx instanceof NumVarParamContext) {
			return ((NumVarParamContext) ctx).ID().getText();
		} else if(ctx instanceof SeqVarParamContext) {
			return ((SeqVarParamContext) ctx).ID().getText();
		}
		return "";
	}
	
	private LTLParseListener initializeParseListener(Pattern pattern) {
		LTLParseListener parseListener = new LTLParseListener();
		pattern.removeErrorListeners();
		pattern.removeWarningListeners();
		pattern.removeUpdateListeners();
		pattern.addErrorListener(parseListener);
		pattern.addWarningListener(parseListener);
		pattern.addUpdateListener(parseListener);
		return parseListener;
	}
	
	public void removePattern(LTLPatternItem item, Machine machine) {
		PatternManager patternManager = machine.getPatternManager();
		Pattern pattern = patternManager.getUserPattern(item.getName());
		if(pattern != null) {
			patternManager.removePattern(pattern);
		}
	}
	
	private Pattern itemToPattern(LTLPatternItem item) {
		Pattern pattern = new Pattern();
		pattern.setBuiltin(false);
		pattern.setDescription(item.getDescription());
		pattern.setCode(item.getCode());
		return pattern;
	}
	
	public void parseMachine(Machine machine) {
		machine.getLTLPatterns().forEach(item-> {
			this.parsePattern(item, machine);
			this.addPattern(item, machine);
		});
	}
	
}

@@ -2138,58 +2138,8 @@
 i);%0A
-%09%09%09StringBuilder signature = new StringBuilder();%0A
 %09%09%09i
@@ -2226,16 +2226,265 @@
 ll) %7B%0A%09%09
+%09%09patternNames.add(extractPatternSignature(child));%0A%09%09%09%7D%0A%09%09%7D%0A%09%09pattern.setName(String.join(%22%5Cn%22, patternNames));%0A%09%09return parseListener;%0A%09%7D%0A%09%0A%09private String extractPatternSignature(ParseTree tree) %7B%0A%09%09StringBuilder signature = new StringBuilder();%0A
 %09%09String
@@ -2509,29 +2509,28 @@
 defContext) 
-child
+tree
 ).ID().getTe
@@ -2535,18 +2535,16 @@
 Text();%0A
-%09%09
 %09%09signat
@@ -2559,26 +2559,24 @@
 nd(name);%0A%09%09
-%09
-%09
 signature.ap
@@ -2586,18 +2586,16 @@
 d(%22(%22);%0A
-%09%09
 %09%09signat
@@ -2645,21 +2645,20 @@
 ontext) 
-child
+tree
 ).patter
@@ -2680,18 +2680,16 @@
 tream()%0A
-%09%09
 %09%09%09.map(
@@ -2723,18 +2723,16 @@
 ontext)%0A
-%09%09
 %09%09%09.coll
@@ -2759,18 +2759,16 @@
 t())));%0A
-%09%09
 %09%09signat
@@ -2786,35 +2786,23 @@
 %22)%22);%0A%09%09
-%09%09patternNames.add(
+return 
 signatur
@@ -2817,94 +2817,8 @@
 ng()
-);%0A%09%09%09%7D%0A%09%09%7D%0A%09%09pattern.setName(String.join(%22%5Cn%22, patternNames));%0A%09%09return parseListener
 ;%0A%09%7D

Refactor LTLPatternParser