package recursion

import (
	"logik/aussagenlogik/formulae"
)

/* ---------------------------------------------------------------- *
 * METHOD: compute NNF
 * ---------------------------------------------------------------- */

// NOTE: diese bedarf einer Art Doppeltrekursion
func NNF(fml formulae.Formula) formulae.Formula {
	// Definiere Schema:
	var schema = func(fml formulae.Formula, prevValues []formulae.FormulaPair) formulae.FormulaPair {
		// separate out positive and negative parts:
		var pairs = formulae.NewFormulaPairs(prevValues)
		var prevPos = pairs.Pos()
		var prevNeg = pairs.Neg()
		// compute value from previous positive/negative parts:
		if fml.IsPositiveLiteral() {
			return formulae.FormulaPair{
				Pos: fml.Deepcopy(),
				Neg: formulae.Negation(fml),
			}
		} else if fml.IsNegativeLiteral() {
			return formulae.FormulaPair{
				Pos: fml.Deepcopy(),
				Neg: prevPos[0],
			}
		} else if fml.IsTautologySymbol() {
			return formulae.FormulaPair{
				Pos: formulae.Tautology,
				Neg: formulae.Contradiction,
			}
		} else if fml.IsContradictionSymbol() {
			return formulae.FormulaPair{
				Pos: formulae.Contradiction,
				Neg: formulae.Tautology,
			}
		} else if fml.IsNegation() {
			return formulae.FormulaPair{
				Pos: prevNeg[0],
				Neg: prevPos[0],
			}
		} else if fml.IsConjunction2() {
			return formulae.FormulaPair{
				Pos: formulae.Conjunction2(prevPos[0], prevPos[1]),
				Neg: formulae.Disjunction2(prevNeg[0], prevNeg[1]),
			}
		} else if fml.IsConjunction() {
			return formulae.FormulaPair{
				Pos: formulae.Conjunction(prevPos),
				Neg: formulae.Disjunction(prevNeg),
			}
		} else if fml.IsDisjunction2() {
			return formulae.FormulaPair{
				Pos: formulae.Disjunction2(prevPos[0], prevPos[1]),
				Neg: formulae.Conjunction2(prevNeg[0], prevNeg[1]),
			}
		} else if fml.IsDisjunction() {
			return formulae.FormulaPair{
				Pos: formulae.Disjunction(prevPos),
				Neg: formulae.Conjunction(prevNeg),
			}
		} else if fml.IsImplication() {
			return formulae.FormulaPair{
				Pos: formulae.Disjunction2(prevNeg[0], prevPos[1]),
				Neg: formulae.Conjunction2(prevPos[0], prevNeg[1]),
			}
		} else if fml.IsDoubleImplication() {
			return formulae.FormulaPair{
				Pos: formulae.Conjunction2(
					formulae.Disjunction2(prevNeg[0], prevPos[1]),
					formulae.Disjunction2(prevNeg[1], prevPos[0]),
				),
				Neg: formulae.Disjunction2(
					formulae.Conjunction2(prevPos[0], prevNeg[1]),
					formulae.Conjunction2(prevPos[1], prevNeg[0]),
				),
			}
		} else {
			panic("Could not evaluate expression!")
		}
	}
	// Erzeuge Funktion aus Schema und berechne Wert:
	fn := formulae.CreateFromSchemeFmlPairValued(schema)
	return fn(fml).Pos
}