Newer
Older
RDLProofSystem / src / main / java / models / terms / DependencyTerm.java
package models.terms;

import com.google.common.collect.TreeMultiset;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;
import java.util.TreeMap;

import exceptions.SyntaxException;
import lombok.Getter;
import models.algebra.Symbol;

@Getter
public class DependencyTerm extends EvaluatableTerm{

	private EvaluatableTerm dependingTerm;
	private TreeMap<EvaluatableTerm, TreeMultiset<EvaluatableTerm>> termPairs;
	
	
	public DependencyTerm(EvaluatableTerm dependingTerm, List<EvaluatableTerm> terms) {
		super(
				new Symbol(":", 1 + terms.size()),
				-1,
				-1
		);
		if (terms.size() % 2 != 0) {
			throw new SyntaxException("Args size must be odd.");
		}
		this.size = dependingTerm.getSize();
		int dependedOrder = terms.get(0).getOrder();
		int maxArgOrder = 0;
		this.dependingTerm = dependingTerm;
		this.termPairs = new TreeMap<>();
		addChild(dependingTerm);
		for (int i = 0; i < terms.size() / 2; i++) {
			EvaluatableTerm dependedTerm = terms.get(2 * i);
			EvaluatableTerm argTerm = terms.get(2 * i + 1);
			if (dependedTerm.getOrder() != dependedOrder) {
				throw new SyntaxException("depended term's order not same");
			}
			maxArgOrder = Math.max(maxArgOrder, argTerm.getOrder());
			termPairs.computeIfAbsent(dependedTerm, k -> TreeMultiset.create()).add(argTerm);
			this.size += dependedTerm.getSize();
			this.size += argTerm.getSize();
		}
		if (dependedOrder <= maxArgOrder) {
			this.order = maxArgOrder;
		} else {
			this.order = dependedOrder - 1;
		}
		for (EvaluatableTerm dependedTerm : termPairs.keySet()) {
			for (EvaluatableTerm argTerm : termPairs.get(dependedTerm)) {
				addChild(dependedTerm);
				addChild(argTerm);
			}
		}
	}
	
	public DependencyTerm(EvaluatableTerm dependingTerm, EvaluatableTerm ...terms) {
		this(dependingTerm, Arrays.asList(terms));
	}
	
	@Override
	public boolean isLinearRightNormalized() {
		return isLinearRightNormaled(0);
	}
	
	@Override
	public EvaluatableTerm linearRightNormalize() {
		DependencyTerm newTerm = (DependencyTerm) clone();
		newTerm.selfLinearRightNormalize();
		return newTerm;
	}
	
	@Override
	public void selfLinearRightNormalize() {
	}
	
	private boolean isLinearRightNormaled(int depth) {
		return false;
	}
	
	public List<EvaluatableTerm> getDependedTerms() {
		return new ArrayList<>(termPairs.keySet());
	}
	
	public List<EvaluatableTerm> getArgumentTerms() {
		List<EvaluatableTerm> result = new ArrayList<>();
		for (TreeMultiset<EvaluatableTerm> terms: termPairs.values()) {
			result.addAll(terms);
		}
		return result;
	}
	
	@Override
	public String toString() {
		StringBuilder sb = new StringBuilder();
		sb.append('[');
		sb.append(getDependingTerm().toString());
		sb.append(" : ");
		for (EvaluatableTerm dependedTerm: termPairs.keySet()) {
			for (EvaluatableTerm argTerm: termPairs.get(dependedTerm)) {
				sb.append(dependedTerm.toString());
				sb.append(" -> ");
				sb.append(argTerm.toString());
				sb.append(", ");
			}
		}
		sb.deleteCharAt(sb.length() - 1);
		sb.deleteCharAt(sb.length() - 1);
		sb.append(']');
		return sb.toString();
	}
	
	@Override
	public String toStringWithOrder() {
		StringBuilder sb = new StringBuilder();
		sb.append('[');
		sb.append(getDependingTerm().toStringWithOrder());
		sb.append(" : ");
		for (EvaluatableTerm dependedTerm: termPairs.keySet()) {
			for (EvaluatableTerm argTerm : termPairs.get(dependedTerm)) {
				sb.append(dependedTerm.toStringWithOrder());
				sb.append(" -> ");
				sb.append(argTerm.toStringWithOrder());
				sb.append(", ");
			}
		}
		sb.deleteCharAt(sb.length() - 1);
		sb.deleteCharAt(sb.length() - 1);
		sb.append(']');
		sb.append('(');
		sb.append(order);
		sb.append(')');
		return sb.toString();
	}
	
	@Override
	public boolean equals(Object another) {
		if(! (another instanceof DependencyTerm)) {
			return false;
		}
		DependencyTerm term = (DependencyTerm) another;
		
		return dependingTerm.equals(term.getDependingTerm()) && 
				termPairs.equals(term.getTermPairs());
	}

	@Override
	public int hashCode() {
		return ("DT" + toString()).hashCode();
	}

	@Override
	public Object clone() {
		List<EvaluatableTerm> termPairs = new ArrayList<>();
		for (EvaluatableTerm dependedTerm : this.termPairs.keySet()) {
			for (EvaluatableTerm argTerm: this.termPairs.get(dependedTerm)) {
				termPairs.add((EvaluatableTerm) dependedTerm.clone());
				termPairs.add((EvaluatableTerm) argTerm.clone());
			}
		}
		return new DependencyTerm(
				(EvaluatableTerm) dependingTerm.clone(),
				termPairs
		);
	}


}