package inference;

import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Collections;
import java.util.Deque;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.stream.Collectors;

import models.formulas.Formula;

public class InferenceHistory {

	private Map<Formula, Set<InferenceHistoryNode>> inferenceHistory;
	
	public InferenceHistory() {
		inferenceHistory = new HashMap<>();
	}
	
	public void addHistory(Formula conclusion, InferenceHistoryNode node) {
		this.inferenceHistory.computeIfAbsent(conclusion, k -> new HashSet<>()).add(node);
	}
	
	public String getHistoryString(Formula conclusion) {
		if (! inferenceHistory.containsKey(conclusion)) {
			return "Inference failed";
		}
		List<String> result = new ArrayList<>();
		Deque<Formula> q = new ArrayDeque<>();
		q.add(conclusion);
		result.add(conclusion.toString());
		while (! q.isEmpty()) {
			Formula formula = q.pollFirst();
			if (! inferenceHistory.containsKey(formula)) {
				continue;
			}
			InferenceHistoryNode node = inferenceHistory.get(formula).iterator().next();
			result.add("--------------------------------" + node.getUsedRule().getName());
			result.add(node.getAssumptions().stream().map(v -> v.toString()).collect(Collectors.joining(", ")));
			for (Formula f: node.getAssumptions()) {
				q.add(f);
			}
		}
		Collections.reverse(result);
		return result.stream().collect(Collectors.joining("\n"));
	}
	
}