package model.rules;

import model.Box;

public class NegationElim implements Rule{

	private Integer rowRef1;
	private Integer rowRef2;

	public NegationElim() {
		super();
	}
	
	public NegationElim(Integer rowRef1, Integer rowRef2) {
		super();
		this.rowRef1 = rowRef1;
		this.rowRef2 = rowRef2;
	}
	
	@Override
	public boolean hasCompleteInfo() {
		return rowRef1 != null && rowRef2 != null;
	}

	/**
	 * Updates the values for the three rule prompts. 
	 * @param index: the index for the rule prompt box.
	 * @param newValue: the new value for that specific rule prompt box.
	 */
	@Override
	public void updateReference(int index, String newValue) {
		if(index < 1 || index > 2) throw new IllegalArgumentException();

		if(index == 1){
			try{
				rowRef1 = ReferenceParser.parseIntegerReference(newValue);
			}
			catch(NumberFormatException e){
				rowRef1 = null;
				throw new NumberFormatException();
			}
		}
		else{//index == 2
			try{
				rowRef2 = ReferenceParser.parseIntegerReference(newValue);
			}
			catch(NumberFormatException e){
				rowRef2 = null;
				throw new NumberFormatException();
			}
		}
	}
	
	@Override
	public String toString(){
		String p1 = rowRef1 == null ? "" : rowRef1.toString();
		String p2 = rowRef2 == null ? "" : rowRef2.toString();
		return String.format("¬E (%s),(%s)",p1,p2);
	}

	@Override
	public boolean verify(Box data, int rowIndex) {
		// TODO Auto-generated method stub
		return false;
	}

	//lägg till contradiction-symbolen
	//kolla att man har valt två rader som funkar
	//kolla så att de två raderna är negationen av varandra
	//kolla så att själva raden innehåller en contradiction 
}

@@ -32,16 +32,139 @@
 del.Box;
+%0Aimport model.ProofRow;%0Aimport model.formulas.Contradiction;%0Aimport model.formulas.Formula;%0Aimport model.formulas.Negation;
 %0A%0Apublic
@@ -1508,259 +1508,848 @@
 %7B%0A%09%09
-// TODO Auto-generated method stub%0A%09%09return false;%0A%09%7D%0A%0A%09//l%C3%A4gg till contradiction-symbolen%0A%09//kolla att man har valt tv%C3%A5 rader som funkar%0A%09//kolla s%C3%A5 att de tv%C3%A5 raderna %C3%A4r negationen av varandra%0A%09//kolla s%C3%A5 att sj%C3%A4lva raden inneh%C3%A5ller en contradiction 
+%0A%09%09//check the rows are in scope%0A%09%09if(data.isInScopeOf(rowRef1, rowIndex) == false ) return false;%0A%09%09if(data.isInScopeOf(rowRef2, rowIndex) == false ) return false;%0A%09%09%0A%09%09//Check if the formula in the row to verify i a contradiction%0A%09%09ProofRow rowToVerify = data.getRow(rowIndex);%0A%09%09Formula rowToVerifyFormula = data.getRow(rowIndex).getFormula();%0A%09%09if( !(rowToVerifyFormula instanceof Contradiction) ) %7B%0A%09%09%09return false;%0A%09%09%7D%0A%09%09%0A%09%09//Check if the to referenced rows are the negation of each other %0A%09%09Formula rowRef1Formula = data.getRow(rowRef1).getFormula();%0A%09%09Formula rowRef2Formula = data.getRow(rowRef2).getFormula();%0A%09%09if(!(rowRef2Formula instanceof Negation)) %7B%0A%09%09%09return false;%0A%09%09%7D%09%0A%09%09Negation neg = (Negation) rowRef2Formula;%0A%09%09//neg.getPrecedence();%0A%09%09//TODO%0A%09%09return true;%0A%09%7D%0A%0A%09//kolla s%C3%A5 att de tv%C3%A5 raderna %C3%A4r negationen av varandra
 %0A%7D%0A

verify method in NegationElim almost finished