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.Pattern_defContext;
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;

@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);
			if(child instanceof Pattern_defContext && ((Pattern_defContext) child).ID() != null) {
				patternNames.add(((Pattern_defContext) child).ID().getText());
			}
		}
		pattern.setName(String.join("/", patternNames));
		return parseListener;
	}
	
	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);
		});
	}
	
}

@@ -171,27 +171,254 @@
 lParser.
-Pattern_def
+NumVarParamContext;%0Aimport de.prob.ltl.parser.LtlParser.Pattern_defContext;%0Aimport de.prob.ltl.parser.LtlParser.Pattern_def_paramContext;%0Aimport de.prob.ltl.parser.LtlParser.SeqVarParamContext;%0Aimport de.prob.ltl.parser.LtlParser.VarParam
 Context;
@@ -846,16 +846,52 @@
 il.List;
+%0Aimport java.util.stream.Collectors;
 %0A%0A@Singl
@@ -2134,16 +2134,66 @@
 ild(i);%0A
+%09%09%09StringBuilder signature = new StringBuilder();%0A
 %09%09%09if(ch
@@ -2282,66 +2282,374 @@
 %09%09%09%09
-patternNames.add(((Pattern_defContext) child).ID().getText
+String name = ((Pattern_defContext) child).ID().getText();%0A%09%09%09%09signature.append(name);%0A%09%09%09%09signature.append(%22(%22);%0A%09%09%09%09signature.append(String.join(%22, %22, ((Pattern_defContext) child).pattern_def_param().stream()%0A%09%09%09%09%09.map(ctx -%3E extractParameterFromContext(ctx))%0A%09%09%09%09%09.collect(Collectors.toList())));%0A%09%09%09%09signature.append(%22)%22);%0A%09%09%09%09patternNames.add(signature.toString
 ());
@@ -2693,9 +2693,10 @@
 in(%22
-/
+%5Cn
 %22, p
@@ -2735,24 +2735,480 @@
 tener;%0A%09%7D%0A%09%0A
+%09private String extractParameterFromContext(Pattern_def_paramContext ctx) %7B%0A%09%09if(ctx instanceof VarParamContext) %7B%0A%09%09%09return ((VarParamContext) ctx).ID().getText();%0A%09%09%7D else if(ctx instanceof NumVarParamContext) %7B%0A%09%09%09return ((NumVarParamContext) ctx).ID().getText();%0A%09%09%7D else if(ctx instanceof SeqVarParamContext) %7B%0A%09%09%09return ((SeqVarParamContext) ctx).ID().getText();%0A%09%09%7D%0A%09%09throw new RuntimeException(%22Unknown parameter context: %22 + ctx.getClass());%0A%09%7D%0A%09%0A
 %09private LTL

Update name of LTL pattern items