package model.rules;

import model.Box;
import model.formulas.Formula;
import model.formulas.FreshVarFormula;
import model.formulas.QuantifiedFormula;
import start.Constants;


public class ForallIntro extends Rule {
    private Interval intervalRef;
    private String var = null;

    public ForallIntro() {}
    public ForallIntro(char var) {
        this.var = Character.toString(var);
    }

    @Override
    public boolean hasCompleteInfo() {
        return intervalRef != null;
    }

    @Override
    public void updateReference(int index, String newValue) {
        if (index != 1) throw new IllegalArgumentException();
        try {
            intervalRef = ReferenceParser.parseIntervalReference(newValue);
        } catch (NumberFormatException e) {
            intervalRef = null;
            throw new NumberFormatException();
        }

    }

    @Override
    public boolean verifyReferences(Box data, int rowIndex) {
        if (!(data.isInScopeOf(intervalRef, rowIndex))) return false;
        Box refBox = data.getBox(intervalRef);
        if (refBox.size() < 2) return false;
        if (!(refBox.getRow(0).getRule() instanceof FreshVar)) return false;
        
        //check that the second row in box isn't an assumption
        if(refBox.size() < 2 ) return false;
        if ((refBox.getRow(1).getRule() instanceof Assumption) && refBox.getRow(1).getParent() == refBox) 
        	return false;
        return true;
    }

    @Override
    public boolean verifyRow(Box data, int rowIndex) {
        Box refBox = data.getBox(intervalRef);
        String freshVarId = ((FreshVarFormula) refBox.getRow(0).getFormula()).var;
        Formula lastRowInRefBox = refBox.getRow(refBox.size() - 1).getFormula();
        QuantifiedFormula toVerify;
        if (data.getRow(rowIndex).getFormula() instanceof QuantifiedFormula == false) return false;
        toVerify = (QuantifiedFormula) data.getRow(rowIndex).getFormula();
        if(toVerify.type != '∀') return false;
        return toVerify.instantiate(freshVarId).equals(lastRowInRefBox);
    }

    @Override
    public Formula generateRow(Box data) {
//        Box refBox = data.getBox(intervalRef);
//        String freshVarId = ((FreshVarFormula) refBox.getRow(0).getFormula()).var;
//        Formula lastRowInRefBox = refBox.getRow(refBox.size() - 1).getFormula();
//        // We can't know which variable to generate
//        return new QuantifiedFormula(lastRowInRefBox, freshVarId, '∀');
        return null;
    }

    @Override
    public String toString() {
        return String.format("∀i, %s", intervalRef);
    }
	
	@Override
	public String[] getReferenceStrings() {
		String ref1 = intervalRef == null ? "" : (intervalRef.startIndex+1)+"-"+(intervalRef.endIndex+1);
		return new String[]{ref1};
	}

	@Override
	public String getDisplayName() {
        return Constants.forallIntro;
	}

}

@@ -2120,26 +2120,24 @@
 data) %7B%0A
-//
         
 Box refB
@@ -2132,134 +2132,97 @@
     
-Box refBox = data.getBox(intervalRef);%0A//        String freshVarId = ((FreshVarFormula) refBox.getRow(0).getFormula()).var;%0A//
+if (var == null)%0A            return null;%0A        Box refBox = data.getBox(intervalRef);%0A
     
@@ -2302,64 +2302,8 @@
 ();%0A
-//        // We can't know which variable to generate%0A//
     
@@ -2356,45 +2356,17 @@
 ox, 
-freshVarId, '%E2%88%80');%0A        return null
+var, '%E2%88%80')
 ;%0A  

Generate if there is a variable