package formulae

/* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *
 * CONSTANTS
 * ---------------------------------------------------------------- */

var Tautology = Formula{
	kind:        "taut",
	expr:        "1",
	valence:     0,
	subformulae: [](*Formula){},
}

var Contradiction = Formula{
	kind:        "contradiction",
	expr:        "0",
	valence:     0,
	subformulae: [](*Formula){},
}

/* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *
 * METHODS: Constructions
 * ---------------------------------------------------------------- */

func Atom(expr string) Formula {
	return Formula{
		kind:        "atom",
		expr:        expr,
		valence:     0,
		subformulae: [](*Formula){},
	}
}

func NegatedAtom(expr string) Formula {
	return Negation(Atom(expr))
}

func Generic(expr string) Formula {
	return Formula{
		kind:        "generic",
		expr:        expr,
		valence:     0,
		subformulae: [](*Formula){},
	}
}

func Negation(fml Formula) Formula {
	return Formula{
		kind:        "not",
		expr:        "!" + " " + fml.expr,
		valence:     1,
		subformulae: [](*Formula){&fml},
	}
}

func Conjunction2(fml1 Formula, fml2 Formula) Formula {
	return Formula{
		kind:        "and2",
		expr:        "(" + fml1.expr + " && " + fml2.expr + ")",
		valence:     2,
		subformulae: [](*Formula){&fml1, &fml2},
	}
}

func Conjunction(fmls []Formula) Formula {
	var expr string = ""
	var children = make([](*Formula), len(fmls))
	for i, fml := range fmls {
		if i > 0 {
			expr += " && "
		}
		expr += fml.expr
		children[i] = &fml
	}
	return Formula{
		kind:        "and",
		expr:        "(" + expr + ")",
		valence:     len(children),
		subformulae: children,
	}
}

func Disjunction2(fml1 Formula, fml2 Formula) Formula {
	return Formula{
		kind:        "or2",
		expr:        "(" + fml1.expr + " || " + fml2.expr + ")",
		valence:     2,
		subformulae: [](*Formula){&fml1, &fml2},
	}
}

func Disjunction(fmls []Formula) Formula {
	var expr string = ""
	var children = make([](*Formula), len(fmls))
	for i, fml := range fmls {
		if i > 0 {
			expr += " || "
		}
		expr += fml.expr
		children[i] = &fml
	}
	return Formula{
		kind:        "or",
		expr:        "(" + expr + ")",
		valence:     len(children),
		subformulae: children,
	}
}

func Implies(fml1 Formula, fml2 Formula) Formula {
	return Formula{
		kind:        "implies",
		expr:        "(" + fml1.expr + " -> " + fml2.expr + ")",
		valence:     2,
		subformulae: [](*Formula){&fml1, &fml2},
	}
}

func DoubleImplication(fml1 Formula, fml2 Formula) Formula {
	return Formula{
		kind:        "iff",
		expr:        "(" + fml1.expr + " <-> " + fml2.expr + ")",
		valence:     2,
		subformulae: [](*Formula){&fml1, &fml2},
	}
}