export type Operator = '¬' | '∧' | '∨' | '->' | '<->' | '!' | '&' | '|';

// Supported ✅
frege.evaluate('¬(P ∧ Q)', {P: false, Q: true});

// Not supported ❌
frege.evaluate('~(p ^ Q)', {p: false, Q: true});

import { frege } from 'fregejs';

frege.parse.toFormulaObject('P -> Q'); // {1} Implication
frege.parse.toFormulaObject('P <-> Q'); // {2} Biconditional
frege.parse.toFormulaObject('P ∧ Q'); // {3} Conjunction
frege.parse.toFormulaObject('P ∨ Q'); // {4} Disjunction
frege.parse.toFormulaObject('¬P'); // {5} Negation

/*
Alternative Symbols:
*/
frege.parse.toFormulaObject('P & Q'); // {6} Conjunction
frege.parse.toFormulaObject('P | Q'); // {7} Disjunction
frege.parse.toFormulaObject('!P'); // {8} Negation

{ operation: 'Implication', left: 'P', right: 'Q' } // {1} Implication
{ operation: 'Biconditional', left: 'P', right: 'Q' } // {2} Biconditional
{ operation: 'Conjunction', left: 'P', right: 'Q' }   // {3} Conjunction
{ operation: 'Disjunction', left: 'P', right: 'Q' }   // {4} Disjunction
{ operation: 'Negation', value: 'P' } // {5} Negation

/*
Alternative Symbols:
*/
{ operation: 'Conjunction', left: 'P', right: 'Q' }   // {6} Conjunction
{ operation: 'Disjunction', left: 'P', right: 'Q' }   // {7} Disjunction
{ operation: 'Negation', value: 'P' } // {8} Negation

frege.parse.toFormulaString({ operation:  'Implication', left:  'P', right:  'Q' }); // {1} Implication
frege.parse.toFormulaString({ operation:  'Biconditional', left:  'P', right:  'Q' }); // {2} Biconditional
frege.parse.toFormulaString({ operation:  'Conjunction', left:  'P', right:  'Q' }); // {3} Conjunction
frege.parse.toFormulaString({ operation:  'Disjunction', left:  'P', right:  'Q' }); // {4} Disjunction
frege.parse.toFormulaString({ operation:  'Negation', value:  'P' }); // {5} Negation

import { frege } from 'fregejs';

const first = frege.evaluate('P->(Q->P)', { P:  false, Q:  true }); // {1}

const second = frege.evaluate(
	{
		operation:  'Conjunction',
		left:  'P',
		right: { operation:  'Negation', value:  'P' }
	},
	{ P:  true }
); // {2}

const third = frege.evaluate('¬¬P ∨ ¬P', { P:  true }); // {3}

console.log('first:', first)
console.log('second:', second);
console.log('third:', third);

first: true
second: false
third: true  

import { frege } from  'fregejs';
frege.reduce('( P -> Q ) ∨ (A ∧ B)'); // {1}
frege.reduce('P <-> ( Q -> P )'); // {2}

import { frege } from  'fregejs';

frege.generateTruthTable('P->(Q->P)'); // {1}
frege.generateTruthTable({operation:  'Conjunction', left:  'P', right:  'Q'}); // {2}

// {1}
{
	headers: [ 'P', 'Q', 'P->(Q->P)' ],
	truthCombinations: [ [ false, false ], [ false, true ], [ true, false ], [ true, true ] ],
	truthValues: [ true, true, true, true ]
}

// {2}
{
	headers: [ 'P', 'Q', '(P ∧ Q)' ],
	truthCombinations: [ [ false, false ], [ false, true ], [ true, false ], [ true, true ] ],
	truthValues: [ false, false, false, true ]
}

import { printTruthTable, frege } from 'fregejs';

const truthTable = frege.generateTruthTable('P->Q');
printTruthTable(truthTable);

const formula = 'P->(Q->P)';
const isTautology = frege.isTautology(formula);
console.log(`Is "${formula}" a tautology? ${isTautology}`); // Output: Is "P->(Q->P)" a tautology? true

const formula = 'P <-> Q';
const isContingency = frege.isContingency(formula);
console.log(`Is "${formula}" a contingency? ${isContingency}`); // Output: Is "P <-> Q" a contingency? true

const formula = 'P ∧ ¬P';
const isContradiction = frege.isContradiction(formula);
console.log(`Is "${formula}" a contradiction? ${isContradiction}`); // Output: Is "P ∧ ¬P" a contradiction? true

import { frege, Proof } from  'fregejs';
const { toFormulaObject } = frege.parse;

const  proof: Proof = {
	1: {
		id:  1,
		expression:  toFormulaObject('¬P ∧ ¬Q'),
		type:  'Premise'
	},
	2: {
		id:  2,
		expression:  toFormulaObject('(P ∨ Q)'),
		type:  'Hypothesis'
	},
	
	3: {
		id:  3,
		expression:  toFormulaObject('¬P'),
		from: [[1], 'Conjunction Elimination'],
		type:  'Knowledge'
	},
	4: {
		id:  4,
		expression:  toFormulaObject('¬Q'),
		from: [[1], 'Conjunction Elimination'],
		type:  'Knowledge'
	},
	5: {
		id:  5,
		expression:  toFormulaObject('P'),
		from: [[2, 4], 'Disjunctive Syllogism'],
		type:  'Knowledge'
	},
	6: {
		id:  6,
		expression:  toFormulaObject('P ∧ ¬P'),
		type:  'End of Hypothesis',
		hypothesisId:  2,
		from: [[5, 3], 'Conjunction Introduction']
	},
	7: {
		id:  7,
		expression:  toFormulaObject('(P ∨ Q) -> (P ∧ ¬P)'),
		type:  'Knowledge',
		from: [[2,6], 'Conditional Proof']
	},
	8: {
		id:  8,
		expression:  toFormulaObject('¬(P ∨ Q)'),
		type:  'Conclusion',
		from: [[7], 'Reductio Ad Absurdum']
	}
}

frege.checkProof(proof); // {1}

const proof: Proof = {
  1: {
    id: 1,
    expression: toFormulaObject('P -> Q'),
    type: 'Premise'
  },
  2: {
    id: 2,
    expression: toFormulaObject('Q'),
    type: 'Premise'
  },
  3: {
    id: 3,
    expression: toFormulaObject('P'),
    type: 'Conclusion',
    from: [[1, 2], 'Modus Ponens']
  },
}

frege.checkProof(proof); // {2}

import { frege } from  'fregejs';

const first = frege.verifyConsequence.semantic(['P->Q', 'Q'], 'P'); // {1}
const second = frege.verifyConsequence.semantic(['P->Q', 'P'], 'Q'); // {2}

console.log('first: ', first);
console.log('second: ', second);