package main

import (
	"fmt"
	"logik/aussagenlogik/formulae"
	"logik/aussagenlogik/recursion"
	"logik/aussagenlogik/schema"
	env "logik/core/environment"
	"logik/core/utils"
	"strings"

	"github.com/lithammer/dedent"
)

var DATA_ENV string = "data.env"

type dataType struct {
	expr           string
	interpretation []string
}

type resultsType struct {
	eval         int
	nnf          formulae.Formula
	atoms        []string
	depth        int
	length       int
	nParentheses int
}

var data dataType

func main() {
	// Extrahiere Daten
	getData()
	// Ausdruck -> Syntaxbaum
	tree := schema.ParseExpr(data.expr)
	results := getResults(tree)
	// Resultate anzeigen:
	displayResults(tree, results)
}

// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
// SONSTIGE METHODEN
// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

func getData() {
	env.ENV_FILE_NAME = DATA_ENV
	data.expr = env.ReadEnvKey("expr")
	s := env.ReadEnvKey("interpretation")
	utils.JsonToArrayOfStrings(s, &data.interpretation)
}

func getResults(tree formulae.Formula) resultsType {
	return resultsType{
		eval:         recursion.Eval(tree, data.interpretation),
		nnf:          recursion.NNF(tree),
		atoms:        recursion.Atoms(tree),
		depth:        recursion.FmlDepth(tree),
		length:       recursion.FmlLength(tree),
		nParentheses: recursion.NrParentheses(tree),
	}
}

func displayResults(tree formulae.Formula, results resultsType) {
	fmt.Println(fmt.Sprintf(
		dedent.Dedent(`
		Syntaxbaum von
		F := %[1]s:

		%[2]s

		Für I = {%[3]s} und F wie oben gilt
		eval(F, I)      = %[4]d;
		F^NNF           = %[5]s;
		atoms(F)        = {%[6]s};  <- *
		depth(F)        = %[7]d;  <- *
		length(F)       = %[8]d;  <- *
		#parentheses(F) = %[9]d;  <- *

		* noch nicht implementiert!
		Challenge: schreibe diese Methoden! (siehe README.md)
		`),
		tree.GetExpr(),
		tree.Pretty("    "),
		strings.Join(data.interpretation, ", "),
		results.eval,
		results.nnf.GetExpr(),
		// string(results.atoms),
		strings.Join(results.atoms, ", "),
		results.depth,
		results.length,
		results.nParentheses,
	))
}