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

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

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

@Getter
public class DependencyTerm extends EvaluatableTerm{

	private EvaluatableTerm dependingTerm;
	private TreeMap<EvaluatableTerm, 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 maxArgOrder = IntStream.range(0, terms.size()).filter(i -> i % 2 == 1).map(i -> terms.get(i).getOrder()).max().orElse(0);
		int maxDependedOrder = IntStream.range(0, terms.size()).filter(i -> i % 2 == 0).map(i -> terms.get(i).getOrder()).max().orElse(0);
		boolean argOrderType = maxDependedOrder <= maxArgOrder;
		if (argOrderType) {
			this.order = maxArgOrder;
		} else {
			this.order = maxDependedOrder - 1;
		}
		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);
			termPairs.put(dependedTerm, argTerm);
			this.size += dependedTerm.getSize();
			this.size += argTerm.getSize();
		}
		for (EvaluatableTerm dependedTerm : termPairs.keySet()) {
			addChild(dependedTerm);
			addChild(termPairs.get(dependedTerm));
		}
	}
	
	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() {
		return new ArrayList<>(termPairs.values());
	}
	
	@Override
	public String toString() {
		StringBuilder sb = new StringBuilder();
		sb.append('[');
		sb.append(getDependingTerm().toString());
		sb.append(" : ");
		for (EvaluatableTerm dependedTerm: termPairs.keySet()) {
			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()) {
			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()) {
			termPairs.add(dependedTerm);
			termPairs.add(this.termPairs.get(dependedTerm));
		}
		return new DependencyTerm(
				(EvaluatableTerm) dependingTerm.clone(),
				termPairs
		);
	}


}