<commit_before>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;

    @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)) 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;
	}

}<commit_msg>fixed small bugg in For All Introduction<commit_after>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;

    @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)) 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;
	}

}
{'fraction_non_alphanumeric': 0.11286474582492201, 'fraction_numerical': 0.004771517709671499, 'mean_word_length': 3.0132547864506627, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1535123', 'n_tokens_mistral': 1616, 'n_tokens_neox': 1564, 'n_words': 388}