// A set of validation tools that reduce complex validation needs to cases that
// can be handled as queries about propositional logic, using the
// PropositionalForm class.

import { Environment } from '../environment.js'
import { PropositionalForm } from './propositional-form.js'

// What attributes are relevant for the propositional meaning of a LogicConcept?
const relevantAttributes = new Set( [
    'symbol text',
    '_type_given'
] )
// Function that deletes all non-meaningful attributes from a LogicConcept
const removeIrrelevantAttributes = LC => {
    const original = new Set( LC.getAttributeKeys() )
    const toRemove = Array.from( original.difference( relevantAttributes ) )
    if ( toRemove.length > 0 ) LC.clearAttributes( ...toRemove )
}

// If we convert the conclusion and all of its accessibles to propositional
// form, not trying to instantiate formulas or respect variable scoping rules,
// does the conclusion follow from its accessibles?
const createPropositionalValidator = classical =>
    ( conclusion/*, options */ ) => {
        // Copy all accessibles into a new sequent we can manipulate,
        // removing any irrelevant attributes such as old feedback:
        const sequent = new Environment(
            ...conclusion.accessibles().reverse().map(
                premise => premise.copy().makeIntoA( 'given' ) ),
            conclusion.copy() )
        sequent.children().forEach( removeIrrelevantAttributes )
        // Convert the sequent to propositional form:
        const proposition = PropositionalForm.fromConclusion(
            sequent.lastChild(), sequent )
        // Validate the sequent and return the result:
        const valid = classical ? proposition.isAClassicalTautology()
                                : proposition.isAnIntuitionisticTautology()
        return {
            result : valid ? 'valid' : 'invalid',
            reason : classical ? 'Classical Propositional Logic'
                               : 'Intuitionistic Propositional Logic'
        }
    }

// Export conveient access to classical propositional validation
/**
 * The Classical Propositional Logic validation tool determines whether the
 * propositional form of the sequent of a conclusion in an environment (not
 * involving formulas or declarations) is a classical tautology.
 * 
 * This tool is installed with the tool name `'Classical Propositional Logic'`. Thus,
 * to use this tool to validate a {@link conclusion}, `C`, call
 * {@link module:Validation.setOptions Validation.setOptions } and {@link module:Validation.validate Validation.validate} as follows:
 * 
 ```
 Validation.setOptions(C,'tool','Classical Propositional Logic')
 Validation.validate(C)
 ```
 * That will result in the validation results being stored in $C$ as an attribute.
 *
 * @function
 * @memberof ValidationTools
 * @param {Environment#conclusions} conclusion - An {@link conclusion} of an
 * {@link Environment}
 * @see {@link module:Validation Validation}
 */
const classicalPropositionalValidator =
    createPropositionalValidator( true )

export { classicalPropositionalValidator }
// Export conveient access to intuitionistic propositional validation
/**
 * The Intuitionistic Propositional Logic validation tool determines whether the
 * propositional form of the sequent of a conclusion in an environment (not
 * involving formulas or declarations) is intuitionistically valid in the 
 * fragment of propositional logic generated by implication and conjunction.
 * 
 * This tool is installed with the tool name `'Intuitionistic Propositional Logic'`. Thus,
 * to use this tool to validate a {@link conclusion}, `C`, call
 * {@link module:Validation.setOptions Validation.setOptions } and {@link module:Validation.validate Validation.validate} as follows:
 * 
 ```
 Validation.setOptions(C,'tool','Intuitionistic Propositional Logic')
 Validation.validate(C)
 ```
 * That will result in the validation results being stored in $C$ as an attribute.
 *
 * @function
 * @memberof ValidationTools
 * @param {Environment#conclusions} conclusion - A conclusion of an 
 * {@link Environment}
 * @see {@link module:Validation Validation}
 */
const intuitionisticPropositionalValidator =
    createPropositionalValidator( false )

export { intuitionisticPropositionalValidator }