package syntaxbaum

import (
	"errors"
	"fmt"
	"strings"
)

type SyntaxBaum struct {
	kind     string
	expr     string
	valence  int
	children [](*SyntaxBaum)
}

/* ---------------------------------------------------------------- *
 * METHODS
 * ---------------------------------------------------------------- */
func (tree *SyntaxBaum) SetKind(kind string) {
	tree.kind = kind
}

func (tree SyntaxBaum) GetKind() string {
	return tree.kind
}

func (tree *SyntaxBaum) SetExpr(expr string) {
	tree.expr = expr
}

func (tree SyntaxBaum) GetExpr() string {
	return tree.expr
}

func (tree *SyntaxBaum) SetChildren(children [](*SyntaxBaum)) {
	tree.children = children
	tree.valence = len(children)
}

func (tree SyntaxBaum) GetChildren() []SyntaxBaum {
	var n int = tree.valence
	var children = make([]SyntaxBaum, n)
	for i, subtreePtr := range tree.children {
		children[i] = *subtreePtr
	}
	return children
}

func (tree SyntaxBaum) GetChild(indexOpt ...int) (SyntaxBaum, error) {
	var index int = 0
	if len(indexOpt) > 0 {
		index = indexOpt[0]
	}
	var subtree SyntaxBaum
	var err error
	if 0 <= index && index < tree.valence {
		subtree = *(tree.children[index])
	} else {
		err = errors.New(fmt.Sprintf("Instance has no child of index %d !", index))
	}
	return subtree, err
}

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

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

// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
// METHODS: Recognitong of Formula-Types
// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

func (tree SyntaxBaum) IsIrreducible() bool {
	return tree.valence == 0
}

func (tree SyntaxBaum) IsAtom() bool {
	return tree.kind == "atom"
}

func (tree SyntaxBaum) IsLiteral() bool {
	if tree.IsAtom() {
		return true
	} else if tree.IsNegation() {
		subtree, err := tree.GetChild()
		if err == nil {
			return subtree.IsAtom()
		}
	}
	return false
}

func (tree SyntaxBaum) IsGeneric() bool {
	return tree.kind == "generic"
}

func (tree SyntaxBaum) IsTautologySymbol() bool {
	return tree.kind == "taut"
}

func (tree SyntaxBaum) IsContradictionSymbol() bool {
	return tree.kind == "contradiction"
}

func (tree SyntaxBaum) IsConnective() bool {
	return tree.valence > 0
}

func (tree SyntaxBaum) IsNegation() bool {
	return tree.kind == "not"
}

func (tree SyntaxBaum) IsConjunction2() bool {
	return tree.kind == "and2"
}

func (tree SyntaxBaum) IsConjunction() bool {
	return tree.kind == "and" || tree.kind == "and2"
}

func (tree SyntaxBaum) IsDisjunction2() bool {
	return tree.kind == "or2"
}

func (tree SyntaxBaum) IsDisjunction() bool {
	return tree.kind == "or" || tree.kind == "or2"
}

func (tree SyntaxBaum) IsImplication() bool {
	return tree.kind == "implies"
}