// |Deduction_Prep.java|: Prep class for deductions.

/* Copyright (C) 2008  Hugh McGuire   http://www.cis.gvsu.edu/~mcguire/
 *                     Grand Valley State University, MI  49401-9403
 */
/*
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 3
of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

For a copy of the GNU General Public License, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth floor, Boston, MA  02110-1301, USA.
Another option as of January 1, 2008 is to browse the following URL:
    http://www.gnu.org/copyleft/gpl.html
*/



import java.util.*;
import javax.swing.JTable;

/**
 * Prep class for deductions.
 * @author Hugh McGuire
 */
class Deduction_Prep {
    // This class was originally nested in |Ded_Action|; I chose "Prep"
    // for this class's name there because it appeared amusing to me
    // to use the expression "new Prep". (;-)

		    // polarities:
		    // simply sign is significant: +/-/0
		    // using |+1| for North, |-1| for South, |0| for Both
		    // (equaling polarities of Manna&Waldinger)
    static final int
	NORTH_POLARITY = 1,
	SOUTH_POLARITY = -1,
	BOTH_POLARITY = 0;

    // The fields here are ~~public
    // because the purpose of this class is simply to provide these items.
    final JTable table;	// redundant where this class is used?
    final PB_TableModel table_model;	// redundant where this class is used?
    final Expressions_Mgmt expressionsmgmt;
    final int[] selected_rows;
    final int selected_row;
    final PB_TableModel.Column_ID selected_column_id;
    final Entry entry;
    int start, limit;
    String subexpr_text;
    Expression expr, subexpr, parent, quant;
			// |parent| is supposed to be the parent
			// outside delimiter if any
    int polarity;	// simply sign is significant: +/-/0
		    // using |+1| for North, |-1| for South, |0| for Both
		    // (equaling polarities of Manna&Waldinger)
	// it's convenient if there are nice |toString()| methods for these
    final LinkedList<String> scoped_freeable_vars, scoped_dependent_vars;
				// skolemizable
    String selected_id;
    boolean selected_id_occurs_both_polarities;
    Expression supp_univ_quantified;	// |private| SO CAN HANDLE THIS
					    // WITH MORE CONFIDENCE
					    // AFTER GENERALIZE
					    // INSTANTIATION
					    // TO EXISTENTIAL GOALS
    final Stack<String> supp_univ_vars;
    Expression goal_exst_quantified;
    final Stack<String> goal_exst_vars;
    final String ref_num_name;
    Expression relation;
    Symbol.Specifier relationship;
    TreeSet<Integer> relationship_support;

    // if true, adds indexes of rows needed for inferences
    // to |relationship_support|
    boolean factors_clearly_nonnegative(Expression factors_expr) {
	LinkedList<Expression>
	    factors = factors_expr.multiary_op_args(Symbol.Specifier.TIMES);
	while ( !factors.isEmpty() ) {
	    Expression factor_ungrp = factors.removeFirst().ungroup();
	    if ( factor_ungrp.op_spec_equals(Symbol.Specifier.EXP) ) {
		Expression exponent = factor_ungrp.get_argument2().ungroup();
		if ( exponent.op_spec_equals(Symbol.Specifier.INT)
			&&  exponent.get_operator().get_val() % 2 == 0
			)
		    continue;
		factor_ungrp = factor_ungrp.get_argument1().ungroup();
		}
	    if ( factor_ungrp.op_spec_equals(Symbol.Specifier.INT) ) {
		if ( factor_ungrp.get_operator().get_val() < 0 )
		    return  false;
		continue;
		}
	    int supporting_row_index =
		table_model.can_clearly_infer_nonnegative(
		    factor_ungrp,
		    selected_row
		    );
	    if ( supporting_row_index < 0 )
		return  false;
	    relationship_support.add(supporting_row_index);
	    }
	return  true;
	}

    Deduction_Prep(JTable table_given, int sel_row_ordinal) {
	table = table_given;
	table_model = (PB_TableModel) table.getModel();
	expressionsmgmt = table_model.get_expressionsmgmt();
	selected_rows = table.getSelectedRows();
	// assert   0 < selected_rows.length  &&  selected_rows.length <= 2;
	// ensure elements of |selected_rows[]| are in order:
	/*
	if ( selected_rows[0] > selected_rows[selected_rows.length - 1] ) {
	    int buf = selected_rows[0];
	    selected_rows[0] = selected_rows[selected_rows.length - 1];
	    selected_rows[selected_rows.length - 1] = buf;
	    }
	*/
	Arrays.sort(selected_rows);		// probably good for future
					    // when resolve (etc.) more
					    // than two rows at once
	selected_row =
	    sel_row_ordinal >= 0
	    ? selected_rows[sel_row_ordinal]
	    : selected_rows[0];
	selected_column_id =
	    table_model.get_entrycolid_of_row(selected_row);
	entry = table_model.get_entry(selected_row);
	String comment =
	    (String)
	    table_model.getValueAt(
		    selected_row,
		    PB_TableModel.Column_ID.COMMENTS.ordinal()
		    );
	String name_addition = "";
		// I'd use "_name" for this variable since it'll actuallly
		// have a space preceding the name, but the tradition in C
		// was that identifiers begin with "_" only for system code.
	if ( comment != null ) {
	    int name_begin = comment.indexOf(Symbol.NAME_COMMENT_START),
	        name_end = comment.lastIndexOf(Symbol.NAME_COMMENT_END);
	    if ( -1 < name_begin  &&  name_begin < name_end )
		name_addition =
		    ' '
		    +
		    comment.substring(
			    name_begin,
			    name_end
				+
				// I want this code to work
				// whether |Symbol.NAME_COMMENT_END|
				// has type |char| or |String|:
				String.valueOf(Symbol.NAME_COMMENT_END)
					.length()
			    );
	    }
	ref_num_name =
		((String)
		    table_model.getValueAt(
			    selected_row,
			    PB_TableModel.Column_ID.REF_NUMS.ordinal()
			    )
		    )
		    .trim()
		+ name_addition;
	expr = entry.get_expr_clone();
	supp_univ_quantified = null;
	supp_univ_vars = new Stack<String>();
	goal_exst_quantified = null;
	goal_exst_vars = new Stack<String>();
	switch ( selected_column_id ) {
	    case SUPPS:
		for ( supp_univ_quantified = expr.ungroup(); 
			supp_univ_quantified
				.op_spec_equals(Symbol.Specifier.QUANT_SEP)
			    && supp_univ_quantified.get_argument1().ungroup()
				.op_spec_equals(Symbol.Specifier.FORALL);
			supp_univ_quantified =
			    supp_univ_quantified.get_argument2().ungroup()
			)
		    supp_univ_vars.addAll(
			expressionsmgmt
				.variables_unquantified(
				    supp_univ_quantified.get_argument1()
					.ungroup().get_argument1()
				    )
			);
		if ( supp_univ_quantified == expr.ungroup() )
		    supp_univ_quantified = null;
		break;

	    case GOALS:
		for ( goal_exst_quantified = expr.ungroup(); 
			goal_exst_quantified
				.op_spec_equals(Symbol.Specifier.QUANT_SEP)
			    && goal_exst_quantified.get_argument1().ungroup()
				.op_spec_equals(Symbol.Specifier.EXISTS);
			goal_exst_quantified =
			    goal_exst_quantified.get_argument2().ungroup()
			)
		    goal_exst_vars.addAll(
			expressionsmgmt
				.variables_unquantified(
				    goal_exst_quantified.get_argument1()
					.ungroup().get_argument1()
				    )
			);
		if ( goal_exst_quantified == expr.ungroup() )
		    goal_exst_quantified = null;
		break;
	    }
	start = entry.get_selection_start();
	limit = entry.get_selection_limit();
	subexpr_text = entry.get_text().substring(start, limit);
	parent = null;
	quant = null;
	scoped_freeable_vars = new LinkedList<String>();
	scoped_dependent_vars = new LinkedList<String>();
	relationship =
	    table_model.get_transformationgoal_relationship(selected_row);
	relationship_support = new TreeSet<Integer>();
	polarity =
	    selected_column_id == PB_TableModel.Column_ID.SUPPS
	    ?  SOUTH_POLARITY
	    :  relationship == Symbol.Specifier.EQUIV
		?  BOTH_POLARITY
		:  NORTH_POLARITY;
	for ( subexpr = expr;
		subexpr.get_begin() != start
		    ||  limit != subexpr.get_limit();
		)
	    {
	    if ( !subexpr.is_group() )
		parent = subexpr;
	    if ( subexpr.op_spec_equals(Symbol.Specifier.EQUIV) )
		polarity = BOTH_POLARITY;
	    else if ( subexpr.op_spec_equals(Symbol.Specifier.QUANT_SEP) )
		quant = subexpr;	// see also below |quant = null;|
	    if ( limit <= subexpr.get_argument1().get_limit() ) {
		if ( subexpr.op_spec_equals(expressionsmgmt.get_lognegsymspec())
			|| subexpr.op_spec_equals(Symbol.Specifier.IMPLIES)
			)
		    polarity *= -1;

		if ( subexpr.get_operator().is_basic_transitive_comparator() ) {
		    relation = subexpr;
		    relationship = subexpr.get_operator().get_specifier();
		    }
		else if ( subexpr.op_spec_equals(Symbol.Specifier.NEGATIVE) ) {
		    if ( relationship != null )
			relationship =
			    Symbol.reverse_numeric_comparator(relationship);
		    }
		else if ( !(subexpr.is_group()
			    ||  subexpr.op_spec_equals(Symbol.Specifier.PLUS)
			    ||  subexpr.op_spec_equals(Symbol.Specifier.MINUS)
			    ||  subexpr.op_spec_equals(Symbol.Specifier.TIMES)
				&&  factors_clearly_nonnegative(
					subexpr.get_argument2().ungroup()
					)
			    )
			)
		    {
		    relation = null;
		    relationship = null;
		    }

		subexpr = subexpr.get_argument1();
		}
	    else {
		if ( subexpr.op_spec_equals(Symbol.Specifier.QUANT_SEP) ) {
		    quant = null;
		    Expression q = subexpr.get_argument1().ungroup();
		    // assert(q.get_operator().is_quantifier());
		    (q.op_spec_equals(Symbol.Specifier.FORALL)
				^ (polarity > 0)
			    // see |freeing_vs_skolemizing| below
			    // (a macro might be nice)
			? scoped_freeable_vars
			: scoped_dependent_vars
			)
			.addAll(
			    expressionsmgmt.variables_unquantified(
				    q.get_argument1()
				    )
			    );
		    }

		if ( subexpr.get_operator().is_basic_transitive_comparator() )
		    {
		    relation = subexpr;
		    relationship =
			Symbol.reverse_numeric_comparator(
			    subexpr.get_operator().get_specifier()
			    );
		    }
		else if ( subexpr.op_spec_equals(Symbol.Specifier.NEGATIVE)
			    || subexpr.op_spec_equals(Symbol.Specifier.MINUS)
			    )
		    {
		    if ( relationship != null )
			relationship =
			    Symbol.reverse_numeric_comparator(relationship);
		    }
		else if ( !(subexpr.is_group()
			    ||  subexpr.op_spec_equals(Symbol.Specifier.PLUS)
			    ||  subexpr.op_spec_equals(Symbol.Specifier.TIMES)
				&&  factors_clearly_nonnegative(
					subexpr.get_argument1().ungroup()
					)
			    )
			)
		    {
		    relation = null;
		    relationship = null;
		    }

		subexpr = subexpr.get_argument2();
		}
	    }
	subexpr = subexpr.ungroup();
	// ~~kludging until implement full multiple selection
	// I no longer remember which code uses |selected_id|;
	// perhaps I should include |selection_boolean()| as a condition here?
	if ( subexpr.op_spec_equals(Symbol.Specifier.IDENTIFIER)
		&&  subexpr.get_argument1() == null
		&&  (parent == null
		     || !parent.op_spec_equals(Symbol.Specifier.COMMA)
			&&  !parent.op_spec_equals(Symbol.Specifier.FORALL)
			&&  !parent.op_spec_equals(Symbol.Specifier.EXISTS)
		     )
		)
	    {
	    selected_id = subexpr.get_operator().get_text();
	    selected_id_occurs_both_polarities =
		polarity == 0
		||  id_occurs_opposite_polarity(
			expr,
			selected_id,
			selected_column_id
				== PB_TableModel.Column_ID.GOALS
			    ?  1
			    :  -1
			);
	    }
	}

    Deduction_Prep(JTable table_given) { this(table_given, 0); }

    boolean id_occurs_opposite_polarity(
		Expression subexpr_oop,
		String id_oop,
		int polarity_oop
		)
	{
	return
	    subexpr_oop.op_spec_equals(Symbol.Specifier.IDENTIFIER)
		&&  subexpr_oop.get_operator().get_text().equals(id_oop)
		&&  polarity_oop != polarity
	    ||  subexpr_oop.get_argument1() != null
		&&  id_occurs_opposite_polarity(
			subexpr_oop.get_argument1(),
			id_oop,
			subexpr_oop.op_spec_equals(Symbol.Specifier.EQUIV)
			    ?  0
			    :  subexpr_oop.op_spec_equals(
					expressionsmgmt.get_lognegsymspec()
					)
				    ||  subexpr_oop
					.op_spec_equals(
					    Symbol.Specifier.IMPLIES
					    )
				?  -polarity_oop
				:  polarity_oop
			)
	    ||  subexpr_oop.get_argument2() != null
		&&  id_occurs_opposite_polarity(
			subexpr_oop.get_argument2(),
			id_oop,
			subexpr_oop.op_spec_equals(Symbol.Specifier.EQUIV)
			    ?  0
			    :  polarity_oop
			);
	}

    boolean selection_boolean() {
	Expression subexpr_ungrp = subexpr.ungroup();
	if ( subexpr_ungrp.get_operator().spec_boolean()
		||  subexpr_ungrp.op_spec_equals(
			expressionsmgmt.get_lognegsymspec()
			)
		)
	    return  true;
	if ( subexpr_ungrp.get_operator().spec_domainval() )
	    return  false;
	if ( subexpr.op_spec_equals(Symbol.Specifier.IDENTIFIER) ) {
	    if ( parent == null
		    || parent.get_operator().spec_id_arg_boolean()
		    || parent.op_spec_equals(
			    expressionsmgmt.get_lognegsymspec()
			    )
		    )
		return  true;
	    if ( parent.get_operator().spec_id_arg_domainval() )
		return  false;
	    }
	System.err.println(
	    "|selection_boolean()| reached default |false|"
	    + " for " + subexpr_ungrp.get_operator().get_specifier()
	    );
	return  false;
	}

    boolean seems_axiomatic() {
	return
	    selected_column_id == PB_TableModel.Column_ID.SUPPS
	    &&  subexpr == expr
	    &&  expr.op_spec_equals(Symbol.Specifier.QUANT_SEP)
	    &&  expr.get_argument1().ungroup()
		.op_spec_equals(Symbol.Specifier.FORALL)
	    ;
	}

    boolean subexpr_among_suq_vars() {
	return
	    supp_univ_quantified != null
	    &&  expressionsmgmt.is_variable(subexpr)
	    &&  subexpr.get_limit() < supp_univ_quantified.get_begin();
	}

    boolean subexpr_among_geq_vars() {
	return
	    goal_exst_quantified != null
	    &&  expressionsmgmt.is_variable(subexpr)
	    &&  subexpr.get_limit() < goal_exst_quantified.get_begin();
	}

    /**
     * @return |true| if doing 'suq free', |false| otherwise
     */
	// facilitate using material inside a universally quantified
	// supposition --- avoiding requiring removing the quantifier:
    boolean try_expr_suq_free() {
	/*
	assert
	    selected_column_id == PB_TableModel.Column_ID.SUPPS
		&&  expr.op_spec_equals(Symbol.Specifier.QUANT_SEP)
		&&  expr.get_argument1().ungroup()
		    .op_spec_equals(Symbol.Specifier.FORALL)
	    : "selected_column_id == PB_TableModel.Column_ID.SUPPS\n"
		+ "&&  expr.op_spec_equals(Symbol.Specifier.QUANT_SEP)\n"
		+ "&&  expr.get_argument1().ungroup()\n"
		    + "\t.op_spec_equals(Symbol.Specifier.FORALL);";
	*/
	if ( supp_univ_quantified == null
		||  subexpr != expr
		    &&  subexpr.get_begin()
			< supp_univ_quantified.get_begin()
		)
	    return  false;
	if ( subexpr == expr ) {
	    subexpr = supp_univ_quantified;
	    start = subexpr.get_begin();
	    limit = subexpr.get_limit();
	    }
	expr = supp_univ_quantified;
	scoped_freeable_vars.removeAll(supp_univ_vars);
	return  true;
	}

    }