package formulae

import (
	"fmt"
	"strings"
)

/* ---------------------------------------------------------------- *
 * TYPE Formula
 * ---------------------------------------------------------------- */

type Formula struct {
	kind        string
	expr        string
	valence     int
	subformulae [](*Formula)
}

/* ---------------------------------------------------------------- *
 * METHODS
 * ---------------------------------------------------------------- */

func (fml *Formula) SetKind(kind string) {
	fml.kind = kind
}

func (fml Formula) GetKind() string {
	return fml.kind
}

func (fml *Formula) SetExpr(expr string) {
	fml.expr = expr
}

func (fml Formula) GetExpr() string {
	return fml.expr
}

func (fml *Formula) SetSubformulae(children [](*Formula)) {
	fml.subformulae = children
	fml.valence = len(children)
}

func (fml Formula) GetSubFormulae() []Formula {
	var n int = fml.valence
	var children = make([]Formula, n)
	for i, subfml := range fml.subformulae {
		children[i] = *subfml
	}
	return children
}

func (fml Formula) GetChild(indexOpt ...int) Formula {
	var index int = 0
	if len(indexOpt) > 0 {
		index = indexOpt[0]
	}
	var subfml Formula
	if 0 <= index && index < fml.valence {
		subfml = *(fml.subformulae[index])
	} else {
		panic(fmt.Sprintf("Instance has no child of index %d !", index))
	}
	return subfml
}

func (fml Formula) Pretty(preindentOpt ...string) string {
	var preindent string = ""
	if len(preindentOpt) > 0 {
		preindent = preindentOpt[0]
	}
	return fml.pretty(preindent, "  ", "", 0)
}

func (fml Formula) pretty(preindent string, tab string, prepend string, depth int) string {
	var indent string = preindent + strings.Repeat(tab, depth)
	switch fml.valence {
	case 0:
		switch kind := fml.kind; kind {
		case "atom", "generic":
			return indent + prepend + kind + " " + fml.expr
		default:
			return indent + prepend + kind
		}
	default:
		var lines string = indent + prepend + fml.kind
		prepend = "|__ "
		for _, subfml := range fml.subformulae {
			lines += "\n" + subfml.pretty(preindent, tab, prepend, depth+1)
		}
		return lines
	}
}

func (fml Formula) Deepcopy() Formula {
	var children = make([](*Formula), len(fml.subformulae))
	for i, child := range fml.subformulae {
		childCopy := child.Deepcopy()
		children[i] = &childCopy
	}
	return Formula{
		expr:        fml.expr,
		kind:        fml.kind,
		valence:     fml.valence,
		subformulae: children,
	}
}

/* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *
 * METHODS: Basic constructions
 * ---------------------------------------------------------------- */

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

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

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},
	}
}

/* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *
 * METHODS: Recognition of Formula-Types
 * ---------------------------------------------------------------- */

func (fml Formula) IsIrreducible() bool {
	return fml.valence == 0
}

func (fml Formula) IsAtom() bool {
	return fml.kind == "atom"
}

func (fml Formula) IsPositiveLiteral() bool {
	return fml.IsAtom()
}

func (fml Formula) IsNegativeLiteral() bool {
	return fml.IsNegation() && fml.GetChild().IsAtom()
}

func (fml Formula) IsLiteral() bool {
	return fml.IsPositiveLiteral() || fml.IsNegativeLiteral()
}

func (fml Formula) IsGeneric() bool {
	return fml.kind == "generic"
}

func (fml Formula) IsTautologySymbol() bool {
	return fml.kind == "taut"
}

func (fml Formula) IsContradictionSymbol() bool {
	return fml.kind == "contradiction"
}

func (fml Formula) IsConnective() bool {
	return fml.valence > 0
}

func (fml Formula) IsNegation() bool {
	return fml.kind == "not"
}

func (fml Formula) IsConjunction2() bool {
	return fml.kind == "and2"
}

func (fml Formula) IsConjunction() bool {
	return fml.kind == "and" || fml.kind == "and2"
}

func (fml Formula) IsDisjunction2() bool {
	return fml.kind == "or2"
}

func (fml Formula) IsDisjunction() bool {
	return fml.kind == "or" || fml.kind == "or2"
}

func (fml Formula) IsImplication() bool {
	return fml.kind == "implies"
}